From reading (1) below, it seems they have implemented an abstraction layer on top of the code that does what the code already does to some degree. They built an
Expression class for symbolic integer manipulation, and they replace any native integer calls with these in their symbolic execution.
Wondering what it takes to do symbolic execution, at a high level. Not sure if you need to create your own entire abstraction on top of every type of object in the language, or what needs to happen. I'm not quite following the paper, but then in (2) it seems they do some more abstraction. There's not much else in terms of description there. Another paper in (3) says to create symbolic expressions as well. But at some point it seems like you are going to end up recreating the whole program, like a Virtual Machine sort of thing, which at that point it seems like you might as well run the original source code. Not sure what I'm missing in this interpretation.
In (4) they describe some more. They mention a symbolic path constraint PC, a first order quantifier free formula over symbolic expressions. Wondering how exactly this accumulates constraints. This seems like the core of it. Not much more is said there though.
The questions are:
- How does symbolic execution work (at a high level)? If you need to really create a full model of the system (types, datatypes, operations, etc.) to "pretend" execute. How it keeps track of, and assigns, the symbolic execution constraints to the path constraint.
- It seems that by using these symbolic objects you would inevitably have to use the heap/memory of the program (e.g. the
Expressionobject is messing with the heap, etc.). It seems like this theoretically interferes with the proof / model checking.
- Where is the boundary is between creating a clone of the program and creating a symbolic representation of it? I feel like I'm missing something here.
- How does it decides which values to use when calling a method or doing some assignment of some sort? I keep imagining they would end up doing essentially Unit Tests (generating random variations of input), but not sure. Basically, at a high level, how does the input selection/generation works?
(1) 6.1 Instrumentation
Conceptually, the instrumentation proceeds in two steps. First, the integer fields and operations are instrumented. The declared type of integer fields of input objects is changed to
Expression, which is a library class we provide to support manipulation of symbolic integer expressions. A type analysis is used to determine which integer variables have their declared types changed to
Expression. Operations involving these variables are replaced with method calls that implement “equivalent” operations that manipulate objects of type
(2) Second, the field accesses are instrumented. Field reads are replaced by
getmethods that return a value based on whether the field is initialized or not (get methods implement the lazy initialization, as described in Section 4). Field updates are replaced by
setmethods which update the field’s value. The
setmethods for a field also set a flag to indicate that the field is initialized.
(3) The key idea behind symbolic execution  is to use as input values symbolic values instead of actual data, and to represent values of program variables as symbolic expressions.
(4) Symbolic execution maintains a symbolic state, which maps variables to symbolic expressions, and a symbolic path constraint PC, a first order quantifier free formula over symbolic expressions. PC accumulates constraints on the inputs that trigger the execution to follow the associated path. At every conditional statement
if (e) S1 else S2, PC is updated with conditions on the inputs to choose between alternative paths. A fresh path condition PC' is created and initialized to PC ∧ ¬σ(e) (“else” branch) and PC is updated to PC ∧ σ(e) (“then” branch), where σ(e) denotes the symbolic predicate obtained by evaluating e in symbolic state σ. Note that unlike in concrete execution, both branches can be taken, resulting in two execution paths. If any of PC or PC0 becomes un-satisfiable, symbolic execution terminates along the corresponding path. Satisfiability is checked with a constraint solver.