The goal of this assignment is to write a simple program verification engine to verify a simple imperative language. For implementing the engine in this project you are free to use any programming language that you are comfortable with. The input to your engine is textual and the output is printed on the screen (standard output).
The small language of this assignment has the following expressions and statements. The type of identifiers in this language is (unbounded) integers. There is no need to type check a given program prior to verification, we assume that if the syntax of a program matches the given BNF then the program is valid. Due to simplicity of the language, no prior specific compiler construction knowledge is required for this assignment, you can use any simple syntax analysis technique to recognize the program structure.
Program | ::= | Stmt ; <EOF> |
Stmt | ::= | skip |
Id := IExp | ||
Stmt ; Stmt | ||
if ( BExp ) Stmt else Stmt endif | ||
while ( BExp ) Stmt endwhile | ||
assert ( BExp ) | ||
BExp | ::= | IExp <= IExp |
IExp == IExp | ||
not BExp | ||
BExp and BExp | ||
BExp or BExp | ||
IExp | ::= | Int |
Id | ||
IExp + IExp | ||
IExp - IExp |
Try to come up with a cool name for your verification engine that is related to what is does (e.g. bugkiller, securer, …).
Your program will be called from the command-line using the following format where NAME
is the name of your tool:
NAME [options] <sourcefile>.imp
Try to avoid using any other format since it will make grading the of your project difficult (and you may lose points if you do not follow this format). We will describe the possible options to your tool in each task.
Generate the control-flow-graph for the input program, as discussed in Lecture 23. For better testing the generated CFG, plot it using the dot program. dot is a very simple program for drawing directed graphs (http://www.graphviz.org/).
If your program is called with the -c option, it will generate a png
file that shows the CFG of the input imp
program.
Test your program with different benchmarks, it is important to ensure about the correctness of CFG generation before trying to verify programs.
Generate the set of Horn clauses representing the input program. If your verification engine is called with the -h option, it will print out the generated Horn clauses on the screen using the SMT-LIB format. Try a set of examples and inspect your Horn clauses to see if they are correct.
When the user calls your program with the -v argument, it will verify the input file by checking the satisfiability of the generated Horn clauses. For satisfiability you can consult an off-the-shelf Horn solver (e.g. Z3, Eldarica or Spacer).
Your program will either print correct
for a program with no bug.
Or, it will write incorrect
for a program that has bug.
Note that if the program has no assert
at all, we assume that there is nothing to be checked for it and it should be correct.
Bonus Print out the values under which the program will hit the error.
Note You can either install the theorem prover on your machine and your code executes the theorem prover as an external application (i.e. z3 can be called from the command line), or you can add the required libraries to call the theorem prover from its libraries.
The verification problem for the imp
language in this project is undecidable.
Can you find a simple program for which the back-end theorem prover runs forever?
(if it does not return a result for e.g. half an hour it is a good sign that it will never stop)
The deadline of this project is November 10 at 11:59pm (https://mycourses.rit.edu). Please do not upload binary and executable files. Make a zip from your files to make uploading the files easier.