Skip to main content

Symbolic Execution

Topic appears in the following WE1 Exams:

  • 2021 09 03 Q3
  • 2021 06 24 Q2 (5 points) Even/Odd
  • 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 1 2 3 4 5 8 9 2 3 4 6 7 8 9 2 10 11:

0  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;
12 }

Then:

Step Definitions Path Conditions
1 x=X
2
3 y=2X X>0
4
5 y=X-1 X>0, X>10
8 x=X-1
9
2 X>0, X>10, X-1>0
3 y=2(X-1)
4
6 X>0, X>10, X>1, X-1<=10
7 x = X - 1 + 2 = X + 1
8 x = X + 1 - 1 = X
9
2
10 x = X - 1 X>0, X>10, X>1, X-1<=10, X<=0
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.

Past exam exercises

2021 06 24 Q2 (5 points) Even/Odd

0 int funct(int x, int y)
1     if(x > 0 && y > 0) {
2         if (y % 2 == 0)
3             return -1;
4         while (x*y % 2 == 0)
5             x = x / 2;
6         while ((x+y) % 2 == 0)
7             x = x - 1;
8     }
9 return x+y;

Point 1: find path conditions

Symbolically execute the program covering the following paths, highlighting the path condition associated with each path:

  1. 0, 1, 2, 4, 5, 4, 5, 4, 6, 7, 6, 7, 6, 8, 9
  2. 0, 1, 2, 4, 6, 8, 9

The execution of the first path:

Step Definitions Path Conditions
0 x=X, y=Y
1
2 X>0, Y>0
4 X>0, Y>0, Y odd
5 x=X/2 X>0, Y>0, Y odd, X even
4
5 x=X/4 X>0, Y>0, Y odd, X even, X/2 even
4
6 X>0, Y>0, Y odd, X even, X/2 even, X/4 odd
7 x=X/4 - 1 X>0, Y>0, Y odd, X even, X/2 even, X/4 odd, Y+X/4 even
6
7 x=X/4 - 2 X>0, Y>0, Y odd, X even, X/2 even, X/4 odd, Y+X/4 even, Y+X/4 -1 even
6
8 X>0, Y>0, Y odd, X even, X/2 even, X/4 odd, Y+X/4 even, Y+X/4 -1 even, Y+X/4-2 odd
9

The path is taken if X>0, Y>0, Y odd, X even, X/2 even, X/4 odd, Y+X/4 even, Y+X/4 -1 even, Y+X/4-2 odd which is impossible because if both X and Y are greater than 0 than Y+X/4 and Y+X/4 -1 cannot be even at the same time.

The execution of the second path:

Step Definitions Path Conditions
0 x=X, y=Y
1
2 X>0, Y>0
4 X>0, Y>0, Y odd
6 X>0, Y>0, Y odd, X odd
8 X>0, Y>0, Y odd, X odd, X+Y odd
9

The path is taken if X>0, Y>0, Y odd, X odd, X+Y odd which is impossible because if X and Y are both odd positive number then X+Y is even

Point 2

Are all instructions in the code reachable through some path, even one not listed in the text, or not? Motivate your answer.

Even thought the two described paths are not feasible all instructions are reachable: based on the analysis of path 0, 1, 2, 4, 5, 4, 5, 4, 6, 7, 6, 7, 6, 8, 9, which is unfeasible, we can conclude, instead, that it is possible to jump out of the second loop following the path: 0, 1, 2, 4, 5, 4, 5, 4, 6, 7, 6, 8, 9. This one allows all instructions except the one at line 3 to be covered. In turn, instruction 3 can be covered by path 0, 1, 2, 3, for which it is enough that x and y are both positive, and y is even.

Back to top