Skip to main content

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:

1 read (y, a);
2 x = y + 2;
3 if x > a
4   a = a + 2;
5 else
6   y = x + 3;
7 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 1 2 3 4 5 8 9 2 3 4 6 7 8 9 2 10 11:

int foo() {
1 x = input();
2 while (x > 0) {
3   y = 2 * x;
4   if (x > 10)
5     y = x - 1;
6   else
7     x = x + 2;
8   x = x - 1;
9 }
10 x = x - 1;
11 return x;
}

Then:

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

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.

Back to top