Symbolic Analysis via Semantic Reinterpretation
Junghee Lim, Akash Lal, and Thomas Reps
In recent years, the use of symbolic analysis in systems for testing
and verifying programs has experienced a resurgence. By ``symbolic
program analysis'', we mean logic-based techniques to analyze state
changes along individual program paths. The three basic primitives
used in symbolic analysis are functions that perform forward
symbolic evaluation, weakest precondition, and symbolic
composition by manipulating formulas.
The conventional approach to implementing systems that use symbolic
analysis is to write each of the three symbolic-analysis functions by
hand for the programming language of interest. In this paper, we
develop a method to create implementations of these primitives so that
they can be made available easily for multiple programming
languages -- particularly for multiple machine-code instruction sets.
In particular, we have created a system in which, for the cost of
writing just one specification -- of the semantics of the
programming language of interest, in the form of an interpreter
expressed in a functional language -- one obtains
automatically-generated implementations of all three
symbolic-analysis functions. We show that this can be carried out
even for programming languages with pointers, aliasing, dereferencing,
and address arithmetic.
The technique has been implemented, and used to automatically generate
symbolic-analysis primitives for multiple machine-code instruction
sets.
(Click here to access the paper:
PDF.)
University of Wisconsin