Symbolic Execution

Topic appears in the following WE1 Exams:

• 2021 09 03 Q3
• 2021 06 24 Q2
• 2021 01 13 Q2.2

Therefore it appears in 50% of the WE1 exams.

Summary

A Symbolic state is made by the tuple: <path-condition, symbolic bindings>.

A simple example of a symbolic execution:

read(a); read(b);
x = a + b;
write(x);

We assign A to a and B to b, the printed result will be: A+B.

When we have more than one path the execution is performed on a single specific path. For example for the code:

read (y, a);
x = y + 2;
if x > a
  a = a + 2;
else
  y = x + 3;
x = x + a + y;

And the execution path <1, 2, 3, 5, 6, 7> which is the used path if Y + 2 ≤ A we get the following execution result: {a=A, y=Y+5, x=2Y+A+7}.

Find the path conditions example

Using symbolic execution, identify the path condition that allows the program to follow the path 2 3 4 5 6 9 10 3 4 5 7 8 9 10 3 11 12:

int foo() {
  x = input();
  while (x > 0) {
    y = 2 * x;
    if (x > 10)
      y = x - 1;
    else
      x = x + 2;
    x = x - 1;
  }
  x = x - 1;
  return x;
}

Then:

2. x = X
3. X>0
4. y=2*X
5. X>10
6. y=X-1
9. x = X-1
10.
3. X-1 > 0
4. y = 2*(X-1)
5. X-1<=10
7.
8. x = X-1+2=X+1
9. x = X+1-1=X
3. X<=0
11.
12.

The path condition for the given path is then X>10 and X<=11 and X<=0. This is clearly an inconsistent condition, the given path is impossible.