User Tools

Site Tools


This is an old revision of the document!

A PCRE internal error occured. This might be caused by a faulty plugin

====== Automatic Program Verifier ====== ===== Introduction ==== 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). ===== Language ==== 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// | * <Id> represents a sequence of letters, digits and underscores, starting with a letter and which is not a keyword. Identifiers are case-sensitive. * <Int> the domain of (unbounded) integer numbers, with usual operations on them. * <EOF> represents the special end-of-file character ===== Interface ===== 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. ===== Task 1 ===== Generate the control-flow-graph for the input program, as discussed in [[plt17:lecture_23|Lecture 23]]. For better testing the generated CFG, plot it using the //dot// program. //dot// is a very simple program for drawing directed graphs ([[|]]). 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. ===== Task 2 ===== 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. ===== Task 3 ===== Verify the input program by checking the satisfiability of the generated Horn solvers by consulting 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. ===== Task 4 (Bonus) ===== 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) ==== Deadline and Deliverables ==== The deadline of this project is November 10 at 11:59pm ( Please do **not** upload binary and executable files. Make a zip from your files to make uploading the files easier. * Read the [[plt17:assignment_policies|Homework Assignment Policies]] for the assignment policies of the course. * This project can be done in groups of two students. If you choose to collaborate with another student, only one of you needs to upload the solution. * Since you are free in choosing your programming language, it is important that you make it easy to build your project. Please include a Readme file in your submission to note how the user can build and run your program.

plt17/assignment_4.1509638692.txt.gz · Last modified: 2017/11/02 12:04 by hossein