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 (only for problem 2). In order to submit your code, pack your Assignment2.js, default.html and question1.sk files into a tar file and submit through stellar.

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. Your goal for this problem is to synthesize a simple controller for an agent navigating a 2-Dimensional grid. The agent starts at position 0,0, and it's goal is to reach position with coordinates given by goal that are each between 0 and N inclusive. Scattered across the space, however, are some obstacles, so your goal is to write a controller that moves the agent from its starting point to its goal without ever landing in a position that includes an obstacle. Specifically, you must set up a harness that helps you synthesize a function with the following interface: void control([int n], ref int myi, ref int myj, int[2][n] obstacles, int[2] goal) The parameters are as follows:

• n is the number of obstacles in the space
• myi is the current i coordinate of the agent which needs to be updated by the function.
• myj is the current j coordinate of the agent which needs to be updated by the function.
• obstacles is an array with the i and j coordinates of all the obstacles.
• goal is an array with the i and j coordinates of the goal stored in positions 0 and 1 respectively.

The specification. The goal is to synthesize a control function that satisfies the following constraints.

• Works correctly for between zero and eight obstacles $(0 \leq n < 8)$
• Works correctly for positions of the goal and the obstacles with coordinates in the range $[0, 8)$.
• Can assume that no obstacle is in the goal position or in the start position.
• Can assume that the manhattan distance between any two obstacles is > 3.
• At each step, the controller can add or subtract at most one from each coordinate.
• The position of the agent can never equal the position of one of the obstacles.
• The position of the agent at the end of the process must equal the goal position.
• The agent cannot take more than 24 steps to reach the goal.
• The coordinates of the agent must stay within the range $[0, 8)$

Clarification: The control is not meant to reach the goal in one call. Rather, at each of the up to 24 steps that the agent is allowed to take, the agent calls the control to make a move and update its coordinates. After 24 moves, the agent should be at the goal state.

The program space. The space of programs is given by the following (very stylized) grammar: exp = 0 | 1 | -1 | rect(exp) | myi | myj | goal[??] | exp - exp | exp + exp prog = condassign* condassign = let tmpi = myi + exp, tmpj = myj + exp in if(!hasObstacle(tmpi, tmpj)){ myi = tmpi; myj = tmpj; return; } In other words, the controller is a sequence of conditional assignments, each of which tries a new update of the position and accepts the update if it succeeds in not hitting the obstacle. The function rect is listed below. int rect(int x){ if(x > 0){ return 1; } if(x < 0){ return -1; } return 0; } It is worth pointing out that in the grammar I am only using let as a shorthand notation. Sketch does not actually support a let statement, so those have to be actual variable declarations. In order for things to synthesize efficiently, your generators will have to bound the number of assignments and the depth of the expression trees. In order to solve this problem, you are likely to find the following flags useful: --bnd-inbits n bounds the number of bits for the input to the harness. --slv-lightverif Performs only lightweight verification. --slv-simiters n Performs n iterations of data-drive simplification before attempting to verify. In my implementation, the synthesis time was on the order of 10 minutes. Your solution should be written into a file named question1.sk.

Part 2 (65 pts)

For this part you will once again be working in JavaScript. 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 sketch code from this AST.

a) VC as an AST: For this part, you may need to introduce additional AST 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.

b) VC as a sketch: For the second part, you will need to pretty-print your VC as a sketch so that we can rely on the sketch synthesizer to discover loop invariants for us. If you like, you can write your generators as a separate library that is included by your generated sketch, although you may do better by creating specialized generators based on what you observe in the program. The sketch should have a function named invariant_i for each loop in the program to help identify the loop invariants.

c) Test cases: You need to submit five test cases for which your system can generate interesting invariants.

Graduate Credit

If you are taking the class for graduate credit, you must also implement the following to get full credit for Part 2. If you are taking the class for undergraduate credit, you can complete this problem for 10 points of extra credit.

For this part, you should extend your solution to part2 to support linear expression holes as part of the input program. The hole should resolve to a linear expression of a subset of the variables present in the program. Your goal is to synthesize expressions for these holes such that the program verifies and terminates.