Symbolic Analysis via Semantic Reinterpretation

Abstract

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.