Wiki

Clone wiki

sketch-frontend / Tutorial

Sketch is a simple imperative language that allows programmers to leave holes in place of complicated code fragments. The sketch synthesizer is able to generate the code missing from the holes, and produce a program that satisfies the programmer's requirements. In this tutorial, we cover the basics of the sketch language, and show how the capabilities of the language can be leveraged to derive complicated code fragments that would be too difficult to derive by hand. We also recommend that you visit the sketch gallery, which contains more examples of interesting sketches.

Getting Started

To illustrate the process of sketching, we begin with the simplest sketch one can possibly write: the "hello world" of sketching.

harness void doubleSketch(int x){
  int t = x * ??;
  assert t == x + x;
}

The syntax of the code fragment above should be familiar to anyone who has programmed in C or Java. The only new feature is the symbol ??, which is Sketch syntax to represent an integer hole. Whenever the synthesizer encounters an integer hole in the program, it will search for an integer constant that will satisfy the programmer's requirements. In the case of this example, the programmer's requirements are stated in the form of an assertion. The keyword harness indicates to the synthesizer that it should find a value for ?? that satisfies the assertion for all possible inputs x (in practice, the system may only verify the result for inputs below a fixed bound).

To try this sketch out on your own, place it in a file, say test1.sk. Then, run the synthesizer with the following command line:

$ sketch   test1.sk

The command line above runs the sketch synthesizer and outputs the result to the terminal.

You can also ask the synthesizer for a C++ implementation by passing the flag --fe-output-code. Additionally, you can ask the synthesizer to generate a test harness by passing the flag --fe-output-test. The test harness runs the synthesized program against randomly generated inputs, and is there to give you confidence that the function produced by the synthesizer indeed satisfies your specification.

$ sketch  --fe-output-code  --fe-output-test  test1.sk

In this case, the synthesizer will produce the following four files:

test1.cpp    test1.h    test1_test.cpp    script

The script compiles and runs the test harness, and reports on whether anything failed along the way.

Specifications

In the example above, we used assertions to declare our correctness condition for the sketch, and we used the keyword harness to indicate to the synthesizer that the function doubleSketch must satisfy the assertion for all possible inputs. An alternative mechanism for providing a specification is to use the implements keyword to establish the equivalence of two functions. Using this keyword, the above example now looks like this.

int doubleSpec(int x){
    return x + x;
}

int doubleSketch(int x) implements doubleSpec{
     int t = x * ??;
    return t;
}

The implements keyword tells the system that for all inputs, the sketch doubleSketch should have the same behavior as the concrete program doubleSpec.

When running this sketch, you don't need the harness keyword; the implements keyword already tells the system that the function doubleSketch should be tested against all inputs.

$ sketch  test1.sk

Example

To show how the integer hole can help in a more realistic example, consider the problem of isolating the rightmost 0-bit in a word x. For example, for the word 01010011, we would like to produce a word containing a 1 in the position of the rightmost 0; that is 00000100. There is a trick to do this using only three instructions. You may remember it: the trick takes advantage of the fact that adding a 1 to a string of ones preceded by a zero turns all the ones into zeros and turns the next zero into a one (i.e. 000111 + 1 = 001000) . You may not remember the details, but with sketching you don't have to; you can let the synthesizer discover them.

For this first example, we will assume the programmer already knows the solution is of the form

~(x + ??) & (x + ??)

where the unknowns correspond to bit-masks. We can write a sketch that uses exactly this expression.

int W = 32;

bit[W] isolate0 (bit[W] x) {      // W: word size
	bit[W] ret = 0;
	for (int i = 0; i < W; i++)  
		if (!x[i]) { ret[i] = 1; return ret;  } 
}


bit[W] isolate0sk (bit[W] x)  implements isolate0 {	
	return !(x + ??) & (x + ??); 
}

If you put this sketch in a file named isolateRightmost.sk, then you can synthesize the missing bit-masks with the following command line.

$ sketch  --outputcode  isolateRightmost.sk

The resulting code uses a bit-vector library contained in the header file bitvec.h which is included as part of the distribution in the folder sketch-frontend/src/runtime/include. The library is not very efficient. There is a code-generator that produces more efficient code, but it is in the experimental phase; if you need this code generator, contact the sketch development team.

Expressing Insight with Complex Holes

In many cases, the expressions that one wants to synthesize are not simple integer constants, but complex expressions. The sketch language provides a simple notation to describe these holes using regular expression syntax. Let us first illustrate this concept through an example.

Example

Consider again the problem of isolating the rightmost bit, only this time, you don't really remember the structure of the solution. Instead, you simply remember that it involved the operators +, & and negation. You can express this insight in the following sketch:

int W = 32;

bit[W] isolate0 (bit[W] x) {      // W: word size
	bit[W] ret = 0;
	for (int i = 0; i < W; i++)  
		if (!x[i]) { ret[i] = 1; return ret;  } 
}


bit[W] isolate0sk (bit[W] x)  implements isolate0 {	
	bit[W] tmp=0;
       {| x | tmp |} = {| (!)?((x | tmp) (& | +) (x | tmp | ??)) |};
       {| x | tmp |} = {| (!)?((x | tmp) (& | +) (x | tmp | ??)) |};
       {| x | tmp |} = {| (!)?((x | tmp) (& | +) (x | tmp | ??)) |};
       return tmp;
}

Regular Expression Holes Explained

Regular expression holes describe to the synthesizer a set of choices from which to chose in searching for a correct solution to the sketch. The basic syntax is

{| regexp |}

Where the regexp can use the operator | to describe choices, and the operator ? to define optional subexpressions.

For example, in the sketch above, the regular expression hole {| x | tmp |} gives the synthesizer the choice of using either x or tmp.

The other regular expression hole is more complicated, because it contains many parts. First, the expression (!)? is giving the synthesizer the option of adding a negation. The regular expression (& | +) gives the system the choice of using the & or the + operators. Overall, the regular expression {| (!)?((x | tmp) (& | +) (x | tmp | ??)) |} gives the synthesizer 24 choices on how to construct the expression, and for choices involving the constant ??, an additional 2^32 choices of how to select that constant.

Regular expression holes can also be used with pointer expressions, as the following example will illustrate.

Example

Suppose you want to create a method to push a value into a stack, represented as a linked list. You could sketch the method with the following code:

push(Stack s, int val){
  Node n = new Node();
  n.val = val;
  {|  (s.head | n)(.next)? |} =   {|  (s.head | n)(.next)? |};
  {|  (s.head | n)(.next)? |} =   {|  (s.head | n)(.next)? |};
}

Generators

Generators offer another mechanism to describe a space of possible expressions and statements. In the case of the isolate rightmost problem, you can use generators to define a grammar of possible expressions for the synthesizer to search.

int W = 32;

bit[W] isolate0 (bit[W] x) {     
	bit[W] ret = 0;
	for (int i = 0; i < W; i++)  
		if (!x[i]) { ret[i] = 1; return ret;  } 
}

generator bit[W] gen(bit[W] x, int bnd){
    assert bnd > 0;
    if(??) return x;
    if(??) return ??;
    if(??) return ~gen(x, bnd-1);
    if(??){
        return {| gen(x, bnd-1) (+ | & | ^) gen(x, bnd-1) |};
    }
}

bit[W] isolate0sk (bit[W] x)  implements isolate0 {		
	return gen(x, 3);
}

The generator gen describes all possible expressions involving addition, bitwise and, bitwise xor and negation, constants, and the input parameter x. The generator takes an extra parameter bnd which is used to bound the size of the generated expression.

Challenge Problems

Updated

Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.