How Symbolic Execution Works

Question

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:

1. 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.
2. It seems that by using these symbolic objects you would inevitably have to use the heap/memory of the program (e.g. the Expression object is messing with the heap, etc.). It seems like this theoretically interferes with the proof / model checking.
3. 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.
4. 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 Expression.

(2) Second, the field accesses are instrumented. Field reads are replaced by get methods 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 set methods which update the field’s value. The get and set methods for a field also set a flag to indicate that the field is initialized.

(3) The key idea behind symbolic execution [35] 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.

See: Generalized Symbolic Execution for Model Checking and Testing

Answer 1

When you say "But at some point it seems like you are going to end up recreating the whole program, like a Virtual Machine sort of thing" --> you are right. Symbolic execution does indeed try to recreate all the paths of the program (as much as the resources allow). However, this: " ... it seems like you might as well run the original source code." is not correct. When you run an actual program, only one control flow path is executed and it can very well give you an idea of the things happening or any bugs occurring in that control flow path of the program, but you do not know anything about the rest of the program. What if some rare input drives the program along with a path which is buggy? Your testing process will never be able to find it out if all you have is regular, non-rare input driven tests. What symbolic execution does is that it tracks all the paths of the code that are feasible (executable). A SE tool will fork two states of the program whenever it comes across a conditional construct, one with a 'true' branch and another with a 'false' branch. So, visualize it as a tree where every node is a conditional juncture from where a concrete execution will choose a single path from the multiple paths that may emanate from that node. The symbolic execution tool, however, will keep track of all the options by forming different path conditions along the respective paths. To check the feasibility of a path, the tool presents the path constraints collected so far to a constraint solver.

To answer your questions:

1. If you read this whole answer, you may get an idea of how symbolic execution works. It assumes a set of symbolic values for some user-specified variables instead of the concrete ones and whenever an expression is encountered on a path which is concerned with that symbolic variable, a symbolic expression is created in the state of the program and that must be used further along the path. For instance, an instruction x = x+y is modeled as sym_x = sym_x+sym_y in the state of the program which changes after the "pretend" execution of an instruction. A state captures the state of the symbolic variables and the path condition seen so far.

2. Yes, symbolic execution uses the system's memory especially in cases where the tool has to model the environment in which the program executes. See this.

3. I am not sure if I understand what you mean by 'clone' of the program. Symbolic execution does no cloning business. It is a systematic software testing process which lets you find those rare inputs under which the program may crash. It is true that instead of executing the program with concrete inputs, it "executes" it with symbolic ones and keeps track of all the paths by maintaining the set of constraints along each path.

4. The inputs which you want to make as symbolic, you specify in the tool using their syntax. For example, SPF lets you specify which functions are to be executed as symbolic and which parameters are to made symbolic using this syntax: symbolic.method=Example.run(sym#sym) in the case where 'run' is a method in class Example which takes two parameters which you want to treat as symbolic. A symbolic execution tool creates a place-holder for each symbolic variable and uses it in the assignments and expressions instead of concrete value. At the end of each path of the program, you have a set of constraints which you can feed to a constraint solver to get any two of the following results: 1. UNSAT which shows that the constraints can not be satisfied and thus, the path is not feasible. 2. SAT, in which case a concrete value is assigned to each symbolic one such that the constraints are satisfied. This is the input which drives the program through that particular path. So, you see: you did not have to find the inputs manually so as to drive the program towards any particular path. The tool automatically found those rare inputs for you. Also, this process of input generation is not at all random. It is systematic and exercises every path.