Information Technology Reference
In-Depth Information
supports a limited set of instructions (enough to represent while programs over
the integers) and a small set of transformations (simple constant propagation,
dead-code-elimination, loop invariant code motion). The generated witnesses are
checked for validity with the Z3 SMT solver [3]. Our experience has been en-
couraging: the witness generation approach is feasible and requires only small
amounts of additional code. The overhead of witness checking is high, but we
expect this to reduce with better implementation techniques.
2 Transformations and Witnesses
This section summarizes ideas described in more depth in [7].
Definition 1 (Program). A program is described as a tuple ( V,Θ,
T
) ,where
- V is a finite set of (typed) state variables , including a distinguished program
location variable , π ,
- Θ is an initial condition characterizing the initial states of the program,
-
T
is a transition relation , relating a state to its possible successors.
A program state is a type-consistent interpretation of its variables. The tran-
sition relation is denoted syntactically as a predicate on V and V , which is a
primed copy of V . For every variable x in V , its primed version x refers to the
value of x in the successor state.
To match the LLVM structure, we consider programs described by a control
flow graph (CFG), where each node is a basic block (BB) consisting of a single-
entry single-exit straight line code. The transition relation of the program can
thus be viewed as a disjunction of transition relations T ij , each describing the
transition between basic block i ( BB i ) and basic block j ( BB j ) such that BB j
is an immediate successor of BB i . The program location variable π ranges over
the set of basic block identifiers. We assume that a CFG has a unique initial BB
with no incoming edges, and a unique terminal BB without outgoing edges.
A witness relation connects the values of source and target program locations
at corresponding basic blocks. In the simplified view, we define a witness relation
to have two components:
- A control mapping κ from the basic blocks of T to those of S . The function
κ maps the initial block of T to the initial block of S , and the terminal block
of T to that of S .
- A data relation , ϕ i,κ ( i ) ( V T ,V S ), which connects the values of target and
source variables at corresponding blocks i and κ ( i ). For this paper, it suces
to have relations which are defined as conjunctions of the form v = e where
v is a program variable and e is an expression, over variables of either S or
T . For instance, one can define equality of corresponding source and target
variables by a set of conjunctions of this form.
There are three conditions, shown in Figure 1, which are checked to ensure
that a relation is a proper witness (i.e., it ensures the correctness of the transfor-
mation). The first checks that the witness relation is a (stuttering) simulation;
 
Search WWH ::




Custom Search