Rewrite systems for symbolic evaluation of C-like preprocessing

Parsing of programs with preprocessing directives and conditional compilation is challenging. Symbolic evaluation offers a fundamental and general approach to solve the main difficulties. It can find, for every line of code, the Boolean expression under which it is compiled or reached and 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.