Rewrite Systems for Symbolic Evaluation of C-like Preprocessing

Abstract

Automatic analysis of programs with preprocessing directives and conditional compilation is challenging. The difficulties range from parsing to program understanding. Symbolic evaluation offers a fundamental and general approach to solve these difficulties. It finds, for every line of code, the Boolean expression under which it is compiled or reached. It can also find all the possible values of preprocessing variables (macros) for each line of code. Conditional values have been shown an effective representation to do fast practical symbolic evaluation of preprocessing; but their interaction with macro expansion and evaluation has not been formally investigated. We present convergent rewrite systems over conditional values that can interact with macro expansion and evaluation and transform them into Boolean expressions. Once transformed, well known simplification techniques for Boolean expressions can be applied. This entails a more complete solution to the efficient symbolic evaluation of C-preprocessing using conditional values.