Symbolic Analysis via Semantic Reinterpretation
File(s)
Date
2008Author
Lim, Junghee
Lal, Akash
Reps, Thomas
Publisher
University of Wisconsin-Madison Department of Computer Sciences
Metadata
Show full item recordAbstract
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.
Permanent Link
http://digital.library.wisc.edu/1793/60644Citation
TR1640