Improving Code Optimization

Improving Code Optimization: Abstract Interpretation of C language with Bit-Vector SMT

What you will learn in this whitepaper:

We present a comparison of a traditional method, as implemented in a popular compiler, and one utilizing translation to quantifier-free fixed-size bit-vector logic (QF_BV). Accuracy and run time of each approach has been assessed, and in some cases the SMT method has been found to produce surprising, but nonetheless correct results. A combination of both approaches is proposed, focusing on the strengths of each method.

As a precursor of this study we compared various QF_BV solvers, to determine which performed the best over input corresponding to a representative collection of short C programs.

Thumb-abstract-interpretation-of-C.png
  • Comparative study on compiler optimization

  • Benchmark the experimental results against GCC compiler

  • Discuss future work

Abstract interpretation of C language with bit-vector SMT: