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 86 9 210 3 4 65 7 8 9 2 10 11:3 11 12:

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;
    8x = x - 1;
  }
  x = x - 1;
9 }
10 x = x - 1;
11
  return x;
}

Then:

1.2. x = X
2.3. X>0
3.4. y=2*X
4.5. X>10
5.6. y=X-1
8.9. x = X-1
9.10.
2.3. X-1 > 0
3.4. y = 2*(X-1)
4.5. X-1<=10
6.7.
7.8. x = X-1+2=X+1
8.9. x = X+1-1=X
2.3. X<=0
10.11.
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.

Back to top