In-class Assignment 2

In class assignment 2 (due Thursday 10:59 AM, right before class).

Symbolic Execution

Show the symbolic execution tree to each program below

• Clearly label symbolic inputs (e.g., a=A, b=B, b=C or a=\(\alpha\), b = \(\beta\), c = \(\gamma\))
• Show EVERY path to the assertion violation (including the INFEASIBLE one)
• Label each path P1 ... Pn
• Create a table as shown below at the end and fill in the answers (examples are given).
• Hint: use Z3 to solve the constraints and obtain input values.
• If there is an assertion violation, clearly show the path and inputs causing the violation

Path	Path Condition	Feasible	Inputs	Local Variables	Assertion Violation?
1	A !=0 && B < 5 && (A == 0 && C != 0 )	NO	NA	NA	NA
2	A !=0 && B < 5 && !(A == 0 && C != 0 )	YES	a=1,b=4,c=1	x=-2,y=0,z=2	NO
...

---

Programs

1. Note: this is the example shown in class

   def f1(a, b, c):
       x = 0 , y = 0 , z = 0
       if (a!=0):
           x = -2
       if (b < 5):
           if (a==0 and c!=0):
               y = 1
           z = 2
       assert (x+y+z != 3)
   

2. Another example

   def f2 (a , b):
       x = 1
       y = 0
       if ( a != 0):
           y = 3+ x
           if ( b == 0):
               x = 2* (a + b)
   
       assert (x - y != 0)
   

3. Perform symbolic execution to find inputs causing division-by-0 error (i.e., at the last line i=j/i)

   def f3(i):
       j = 2 * i
       i += 1
       i = i * j
       if (j < 1)
           i = -i
       i = j / i