Symbolic Execution for Mortals

• stmt: Statement. The next statement to evaluate.

• σ : Symbolic Store. Maps program variables to concrete values or symbols αi.

• π : Path Constraints. A set of all conditions the symbols must meet in order to reach the stmt in the execution branch. Always true at the beginning.

void myFunct(int a, int b){
  int x = 1, y = 0;
  if (a != 5){
    y = 3 * x;
  if (b == 1){
    x = 5 * (a + b);
  }
  }
  assert(x - y != 0);
}

1. The function receives two parameters, a and b. The symbolic execution engine assigns symbols for each parameter: a → αa , b → αb. Since the program hasn’t really began executing, we don’t yet have any paths and therefore no constraints, thus π is always true at the beginning. The next statement to execute is int x = 1, y = 0; leaving our engine in state A: σ = {a → αa , b→ αb} π = true.

2. The next statement is executed and two values are assigned. This adds x →1, y → 0 to our σ. No conditions have been established so π is still true. The next statement to execute is if (a != 5) leaving our engine in state B: σ = {a → αa , b → αb, x = 1, y = 0} π = true.

3. Here a decision is made based on the value of the first parameter, a. Since symbolic execution doesn’t assign concrete values to input the initial symbols remain and a will still be equal to αa. Symbolic execution analyses multiple paths, so the execution tree must continue whether the condition is met or not. The symbolic execution engine can take two states. If the condition is met, αa!= 5, that implies a constraint which is added to π leaving our engine in state C: σ = {a → αa , b → αb, x = 1, y = 0} π = αa != 5 where the next statement to execute would be y = 3 * x. If the condition is not met, αa = 5, that also implies a constraint and it must also be added to our π leaving our engine in state D: σ = {a → αa , b → αb, x= 1, y = 0} π = αa = 5 and the next statement to execute would be the assert which when executed would pass all checks meaning the end of that branch.

4. The value of y is assigned to be three times that of x. The only thing this changes is the value of y in our σ and the next statement to execute is a condition leaving our engine in state E: σ = {a → αa , b →αb, x = 1, y = 3} π = αa != 5.

5. A decision is made based on the value of the second parameter, b. Both possibilities are evaluated. If the condition is met, αb = 1, that is another constraint and it is added to our π. The next statement to execute would be ``x= 5 * a b;+ leaving our engine in state F: σ = {a → αa , b → αb, x = 1, y= 3} π = αa != 5 ∧ αb = 1. If the condition is not met, αb != 1, that constraint must also be added to our πleaving our engine in state G: σ = {a → αa , b → αb, x = 1, y = 3} π = αa!= 5 ∧ αb != 1` where the next statement to execute would be the assert which when executed would pass all checks meaning the end of that branch.

6. The value of x is assigned to be five times the sum of a and b. The only thing this changes is the value of x in our σ leaving our engine in state H: σ = {a → αa , b → αb, x = 5(αa αb), y = 3} π = αa != 5 ∧ αb = 1+ where the next statement to execute would be the assert. When the assert, x -y != 0 is evaluated the values are replaced for what our engine has. 5(αa αb) - 3 = 0 ∧ αa != 5 ∧ αb = 1+ this is the expression that tells me what values will make my assert fail. To satisfy the previous expression αa has to be equal to 0.6 and αb has to be 1.

1. A Survey of Symbolic Execution Techniques. Retrieved May 4, 2017