V&V: Symbolic Execution Coursework
Due 5 April, 2022 @ 4:00PM (UK time)
Term 2
(5% of the Total Course Mark)
Introduction
For this assignment, you will given an interpreter for FLP, a fictional programming
language (written in Python) that you will modify it into a symbolic execution engine.
Your modified interpreter will be automatically graded by running it against several test
cases, each increasing in difficulty.
As this task is worth only 5% of the module mark, FPL is not Turing Complete. This
means that it is not able perform all the computations that a Turing Machine (or, equiva-
lently, any widely used programming language) can. FPL’s limitations aside, modifying
its interpreter into a symbolic execution engine will help you better understand what
design choices need to be made when implementing symbolic execution.
FPL
FPL ignores excess whitespace. Its context-free grammar follows
p = l | p l
l = SKIP
| DEFINE var
| var := exp
| PRINT exp
| IF pred THEN p ELSE p ENDIF
| REPEAT int TIMES p ENDREPEAT
where int is an integer, var is a variable name consisting of lowercase letters only, exp
is an arithmetic expression (may include brackets and +,-,*,/), and pred is a pair of
expressions, separated by a binary predicate symbol <, >, or =.
As FPL’s expression grammar is ambiguous, we use the standard precedence rules for
operations from left to right beginning with expressions in brackets, followed by +,−,
followed by ∗,/.
FPL’s interpreter takes the file name of a program to run and constructs the parse tree
using Lark. Provided parsing succeeds, FPL’s interpreter executes the program. A define
statement prompts the user to input an integer value that is assigned to the (possibly new)
1
variable name. All other statements are executed as you would expect in a conventional
programming language. It is important to note that all variables are in a single global
scope, thus only one symbol table is needed.
Since all values in the program are integers, FPL evaluates division as integer division.
The possible runtime errors are division by 0 or referencing unassigned variable. The
Appendix contains an example FPL program and its run.
Your Symbolic Execution Engine
You should modify the interpreter so it assigns symbolic values to variables wherever
the user would otherwise be prompted to enter them. You should name the symbolic
values s0, s1, s2, ... in order the user is prompted to enter them. For example, if the
program prompts the user to define i on the first and j on the second line, the initial
symbolic values of i, j should be s0, s1 respectively.
The symbolic execution engine should exhaustively check all the paths in the program.
If it encounters a feasible erroneous path, it should print the error, followed by the model
input values resulting in this erroneous path. You may use the z3 SMT solver to do that.
Otherwise, it should output “NO ERRORS FOUND”.
As an additional challenge for those aiming to achieve the highest mark you may also
modify the language by adding the while loop with syntax below.
WHILE pred DO p ENDWHILE
With this addition, FPL is Turing Complete. Consequently, exhaustively executing
all the paths of an arbitrary program is impossible. To handle divergent loops, the
interpreter will take a parameter that bounds the maximum of loop iterations. If not
supplied, this bound defaults to three. The Appendix contains examples.
Assessment
You will be awarded up to 100 marks, based on five test validation suites. You will
submit your work via git; our GradeBot server will automatically run the submission
against the test suite and email you the results. You will be able to submit your code to
GradeBot as many times as you wish and receive feedback via email within minutes.
The test case groups are specified in the table below.
2
Objective for Validation Marks
Symbolically execute programs including define, assign, and print
statements and identify division by 0 errors
20 marks
Symbolically execute programs including define, assign, and print
statements and identify reference to unassigned variables errors
20 marks
Add symbolic execution functionality for repeat-loops 20 marks
Add symbolic execution functionality for if-else statements 20 marks
Amend parser and the symbolic execution engine to support while
loops
20 marks
This assignment is intended to be worked on individually. This is why you are not
allowed to use public repositories for your code. However, you are encouraged to share
example input files with your peers.
Submitting Your Work
Ensure that you can SSH into the department before continuing. Run the following
command:
$ ssh CS_USR@scm4.cs.ucl.ac.uk
where CS_USR is your CS Linux username. If you do not have access, you are probably
using the wrong username: your CS username is different to your UCL username (which
you use to log in to Moodle, Portico etc.). Do not try to log in more than three times
with an incorrect username, as your IP address will be banned by the department. Please
email the Technical Support Group to figure out what your CS username is.
Download the project directory from Moodle and unzip it. It includes two identical
files interpret.py, symbolic.py — keep the former one for reference and modify the
latter one only. Do not add any additional files containing code as the GradeBot will
not be able to recognise those. Continue by initialising a git repository. Add your UCL
repository as a remote using
$ git remote add origin CS_USR@scm4.cs.ucl.ac.uk:/cs/student/COMP0103/CS_USR
Once you are ready to submit create a text file called student.txt in the root of your
repository with a single line containing your student number, UCL email, and name, in
this format:
12345678 Grace Hopper
You MUST provide the correct student number and UCL email address; otherwise,
your submission will be rejected. You MUST use the email address containing your
name and year of entry (e.g. f.bloggs.14@ucl.ac.uk), whereas UCLID@ucl.ac.uk
(e.g.ucaaxxx@ucl.ac.uk) is your Windows Live ID, not the actual address. The server
will reject submissions without the student.txt file.
Every time you push your changes, you should get an email from the Gradebot within a
few minutes.
3
Appendix: Examples
Example Interpreter Run
For example, let the code below be the contents of the file named log.in that asks
user for the value of x and then outputs max(log2 x,20) if log2 x is defined, and −1
otherwise.
DEFINE x
base := 2
log := 0
IF x > 0 THEN
REPEAT 20 TIMES
IF x = 1 THEN SKIP ELSE
log := (log + 1)
x := (x/base)
ENDIF
ENDREPEAT
ELSE
log := -1
ENDIF
PRINT log
You can run the program as follows:
$ python3 interpret.py log.in
Enter value for x: 32
5
Example Symbolic Execution Engine Run
Now let us execute the program log.in symbolically. We get the following mes-
sage.
python3 symbolic.py log.in
NO ERRORS FOUND
Now suppose that the user is also prompted to define the base by changing the line
base := 2 to DEFINE base. The symbolic execution after this modification is shown
below.
$ python3 symbolic.py log.in
RUNTIME ERROR, DIVISION BY 0
[s1 = 0, s0 = 2]
Example Symbolic Execution Engine Run withWhile Capabilty
You do not need to modify the interpreter to support while loops — you will only be
assessed on modifying the symbolic execution engine. However, you may choose to
modify the interpreter first to familiarise yourself with how while loops work.
4
Let us now look at a while-implementation of the integer log function that is not bound
by a maximum value of 20.
DEFINE x
base := 2
log := 0
IF x > 0 THEN
WHILE x > 1 DO
log := log + 1
x := x/base
ENDWHILE
ELSE
log := -1
ENDIF
PRINT log
We can run it with the maximum bound of 20 repetitions of the loop body using the
following command
$ python3 symbolic.py log.in 20
NO ERRORS FOUND
Public Test Cases
Here we show some of the test cases used for grading. If your output matches these
when testing, but the Gradebot server notifies you that these test cases are failing, you
should email the PGTA listed at the bottom of the Gradebot email.
test-1-1
Source:
DEFINE x
y := x*2
PRINT y
Model Otput: Print the following line
NO ERRORS FOUND
test-2-4
Source:
x := 5
y := 6
z := 7
PRINT x+y*z-w
Model Otput: Raise an error, followed by any z3 model, for example
RUNTIME ERROR, VARIABLE REFERENCE PRE ASSIGNMENT
[]
5
test-3-1
Source:
DEFINE x
REPEAT 5 TIMES
x := x-1
ENDREPEAT
PRINT 10/x
Model Otput: Raise an error, followed by any z3 model with s0 equal to 5
RUNTIME ERROR, DIVISION BY 0
[s0 = 5]
6