Towards a Vertically Integrated Compiler Infrastructure to Improve Solver Time during Symbolic Execution

Abstract

Symbolic execution is a dynamic software verification and testing technique that formally reasons about branches in a software under test using satisfiability modulo theories (SMT). This requires encoding branch conditions as logical formulas in the SMT-LIB format consumed by SMT solvers. Due to the complex semantics of modern programming languages, this transformation is conducted based on an intermediate representation (IR). To obtain this representation, prior work facilitates off-the-shelf compiler infrastructures (e.g., LLVM). Unfortunately, these established compilers are tailored to emitting program representations for fast execution on physical hardware, not for fast formal reasoning. We propose integrating the compiler infrastructure with symbolic execution, thereby obtaining a program representation optimized for SMT solving. To explore this idea, we build upon an existing extensible IR to ease a co-design of the compiler, IR, and symbolic execution engine. We illustrate the potential of this integration by contributing conditional representation, a novel compiler transformation tailored to symbolic execution that results in a solver-efficient representation of pure functions with branches. Specifically, with conditional representation, such functions are represented as a single SMT expression, decreasing the number of solver queries while increasing per-query information. In our performed experiments, we symbolically execute real-world components from embedded operating systems and show that conditional representation reduces solver time by a geometric mean of 80%.