Assignment 2

Submission Instructions This assignment is due at 5pm on the date indicated in the class calendar. The starter code for the assignment can be found here. In order to submit your code, submit your q1.sk and q2.py files on Canvas.

Collaboration: You are allowed to collaborate with one other person for this assignment, but each of you is responsible for submitting your own solution. If you do collaborate with someone else, make sure to name your collaborator in your submission.

If you have any questions, please ask!

Problem 1 (35 pts)

The goal of this problem is to use Sketch to solve some non-trivial synthesis problem. You might recall from a Programming Languages or Theory of Computation course that context-free grammars correspond to a particular class of languages, for which there exist standard representations (e.g., BNF) and compilers that can transform these representations into efficient parsers.

However, some simple languages do not have a context-free grammar representation. For example, consider the following language of () and [] pairs where the following are valid:

		([])
		([)]
		()(([[(])]))
	

and the following are not:

		((
		]][[
	

The idea here is that the () and [] pairs must be matched and appropriately nested, but the () and [] pairs can be interleaved arbitrarily.

Your task in this assignment is to write a sketch generator that can produce a parser for such a language from a small number of examples. For simplicity, the parser will be a function that takes a string and returns true if the string is in the language and false otherwise.

See test_1, test_2, and test_3 for examples of languages that your generator should be able to handle.

Some important notes:

• The standard technique for parsing languages like this involves stacks.
• Implementing stacks in sketch is usually accomplished by using fixed-length lists with a pointer.
• Your parser should be able to handle characters that are not obviously parentheses. See test_3.
• To run your code, run

  sketch q1.sk --bnd-unroll-amnt 20

  Replace sketch with the path to your sketch binary.

Your solution should be written into a file named q1.sk.

Part 2 (65 pts)

For this part you will be working in Python, using the CVC5 library, which implements the Sygus solver. For an example of how to use the CVC5 library, see the file q2/example.py. Full documentation can be found here. Note that since we are using the Sygus solver, you must use the Base Python API, not the Pythonic API.

The goal of the second problem will be to synthesize invariants necessary to prove that a piece of code is correct. We will be working in the context of a very simple language involving variables, simple arithmetic operations, and a set of simple commands (if, while, assignment and sequential composition). You will implement this in two parts, first, you will generate the verification condition as an AST using the same AST nodes provided to you for representing the program, and then you will generate CVC5 code and solve from this AST.

a) VC as an AST: For this part, you may need to introduce additional Expr nodes in order to represent the unknown invariants and to indicate the variables that may be used by this. Other than that, this should be a relatively straightforward implementation of verification condition generation. To check your work, ensure that

python q2/q2.py 2a

runs without errors.

b) Verification using CVC5: For the second part, you will need to implement two functions. First, on each Expr node, implement to_cvc5 which takes an Expr and returns a CVC5 expression. The full list of Kinds is useful for determining what functions are available. Also look at q2/example.py for examples of how to use the CVC5 library. You will need to implement this for any Expr nodes you added in part a. Note that variables is a dictionary mapping variable names to CVC5 variables, and invariants is a dictionary mapping Expr nodes to CVC5 functions, like min/max from the example. Second, implement solve. In this function you will need to set up variables and invariants and then call to_cvc5 on the assumption and VC. To check your work, ensure that

python q2/q2.py 2b

runs without errors.

c) Test cases: You need to submit five test cases for which your system can generate interesting invariants. Place these in example_N for N from 2-6. You can run your code on these test cases by running

python q2/q2.py 2c

Note: the invariants you generate should be relatively shallow when thought of as trees, otherwise the solver won't find a solution quickly. For example, the following invariant does not work well:

x >= 0 && y >= 0 && 3x + 2y >= 0