Lesson 13: Program Synthesis

[sampsyo]

The tasks for the program synthesis lesson are extremely open-ended: just do something interesting on top of the basic synthesizer that we built in class!

[MelindaFang-code]

Summary

https://github.com/MelindaFang-code/bril/blob/main/assignment/task13/foo.py
@collinzrj We extended the program synthesizer built in class with the array initialization and access feature. In the new synthesizer, users can initialize an arbitrary length of array, and also access elements using indexing. We defined the grammar as "get index [ele1, ele2, ...]". To achieve this, we expand the "GRAMMAR" part and the "interp" function to unroll elements in the array recursively.

Hardest Part

The most challenging part of this task is to define the grammar of array and represent array as constraint. We studied and experimented with Lark a lot to define the grammar of array. After defined array, we have to represent array access as arithmetic expressions.
Given an array of this format, and we want to access a specific element
get h1 [1, 2, x]
We translate it to
(h1 == 0) * 1 + (h1 == 1) * 2 + (h1 == 2) * x
It acts as an if-else style, only if h1 matches a specific index, the branch will be activated, and the result will be a specific element.

Testing

For testing, we constructs some manual test cases. This covers cases such as array index being an variable and array elements being accessed as variables.

[willwng]

Vivian and I worked on lesson 13 together.
Desugaring Tool
Updated Grammar and Z3
Examples

Summary

• Starting with the example in class, we extended the DSL to include boolean operators (and, not, xor, or).
• We wanted the synthesizer to be able to reference more variables than just the hard-coded x, so we added a feature
  to allow users to specify variable holes, where the value of the hole may be selected from one of multiple possible
  named variables.

Implementation details

• We initially wanted to implement boolean operations, but realized that in order to test our implementation in any
  nontrivial way, we needed to extend the desugaring process to permit multiple variables to be used in generated code.
• We realized that ?? only allowed for variable x. To support any choice of variable, we made a desugaring function
  that took a variable hole {x,y} and transformed it into h# ? x : y.
• This approach could be extended to support any number of variables, since the desugaring can be applied recursively.
• After implementing this new and improved desugaring, we were able to synthesize both of DeMorgan's laws.

What was the hardest part of the task? How did you solve this problem?

• One thing we realized is that the speed of the solver depended heavily on the input being "convenient". For instance,
  attempting to solve the synthesis problem

not (x and y)
(not {x,y}) or (not {x,y})

crashed Vivian's computer, while

not (x and y)
(not {x,y}) or (not {y,x})

returned almost instantly.

• The desugaring was actually very tricky. We tried at first to do regex matches and replaces, but eventually found it
  easiest to just linearly scan through the source and replace variable holes explicitly

[matth2k]

• Summary

  • Given some univariate expression written with arithmetic, logical, and conditional operators, my solver will determine if it is (1) polynomial in variable 'x' and (2) equal to zero modulo 8.
    • Code
    • usage: smt.py [-h] [-v] [-N BITS] expression
    • This exercise was inspired by Drane and Constantinides on the formal verification of datapaths. In short, the paper uses the technique of "vanishing polynomials mod 2^k" to verify if a datapath and its optimized alternative are in fact equivalent. In my toy program, I only check if a polynomial vanishes modulo 2^3.

• Implementation Details

  • When working with RTL (register-transfer level), there are many instances where the logic depends on individual wires. For example, if we wanted to take an unsigned integer modulo 16, you could take the lower 4 bits of number as a bitslice and concatenate it with zeros: wire[15:0] moduloEight = {12'h000, number[3:0]}. Hence, I wanted to be able handle bitslicing in my application.
  • I also wanted to represent exponents, so that I can test polynomials themselves directly in my solver.
  • Given the last two points, it led me to augment the syntax with:
    • Bit slices like x[3:0]
    • Bit selection x[1]
    • Exponents like x^3 or (x+1)^2
    • Coefficents like 20x or 4x^2
  • With the augmented grammar and interpreter, I can formulate the general form of a vanishing polynomial: A*x*(x - 1)*(x - 2)*(x - 3) + 4*B*x*(x - 1)*(x - 2) + 4*C*x*(x - 1) + 8*D*x + 8*E. A through E are my "holes." The derivation for this polynomial is on pages 5-7 of the reference.
    • This will not catch every single vanishing polynomial, because A is modeled as a bit vector, when really it can be its own polynomial in general. But close enough to find some interesting cases.
  • Finally, my program has an optional command line argument -N <bits> to specify the bit length of variable x, which can be any number greater than or equal to 8. By default, I set it to 16.

• Evaluation

  To find test cases, we can start with polynomials that do vanish modulo 8, then scramble them up. Basically, anytime we get a "Yes", we know we can just optimize the circuit away to 0. Here are some interesting evaluations of my program:

  ~$ python3 smt.py "16x"
  Q: Is this expression polynomial in 'x' and zero modulo 8?
  A: Yes it is, with vanishing polynomial
  16x
  

  Let's use a bunch of ternary operators in a bunch of ways that is still polynomial:

  ~$ python3 smt.py "x[3:0] ? (x[1] - 1 ? x[1] : 0) : x[2:0]"
  Q: Is this expression polynomial in 'x' and zero modulo 8?
  A: Yes it is, with vanishing polynomial
  0
  

  Let's combine that with logical shift:

  ~$ python3 smt.py "((x[15:8] << 8) + x[7:0] - 1)^2 * (x << 1) * (x - 2)"
  Q: Is this expression polynomial in 'x' and zero modulo 8?
  A: Yes it is, with vanishing polynomial
  2x(x-1)(x-2)(x-3) + 4x(x-1)(x-2)
  

  Let's sanity check by making the formula wrong:

  ~$ python3 smt.py "((x[15:8] << 7) + x[7:0] - 1)^2 * (x << 1) * (x - 2)"
  Q: Is this expression polynomial in 'x' and zero modulo 8?
  A: No
  

• Anything Hard or Interesting?

  • It was hard to get the associativity right on my polynomial parsing. However, having a out-of-the-box way to define a grammar is pretty cool. It's fun.

[bcarlet]

Summary

• Synthesis Extension

Details

I extended the synthesizer from the tutorial with imperative assignments. Each program consists of a sequence of assignments to variables followed by evaluation of an expression representing the result of the program.

For example, the following program swaps a and b, and then returns their difference:

tmp := a;
a := b;
b := tmp;
a - b

Given an appropriate sketch, the synthesizer can come up with the equivalent XOR-swap version:

a := (0 ? a : b) ^ (255 ? a : b);
b := (0 ? a : b) ^ (255 ? a : b);
a := (255 ? a : b) ^ (0 ? a : b);
a - b

The solver discharges the goal instantly.

Difficulties

Mostly just keeping track of the Z3 variables: which ones needed to be the same across programs, and which ones are bound at any given point in time.

[bennyrubin]

Summary

For this assignment, I modified the ex2.py program to include the exponent operator, for constant exponents. This required some changes to the grammar and the interpreter, but was overall fairly straightforward to implement. My code can be accessed here.

Hardest part

The most challenging part of this assignment is that Z3 does not support non-linear constraints. I can get around this by encoding x^n as x * x n times, which means I can support this for constant exponent values.

Testing

I created some handwritten test cases. Despite the fact that holes and variables cannot be placed as the exponent, I was able to come up with some interested examples that the synthesizer was able to solve.

Given more time in the future, I would love to mess around with using Z3 and an interpreter to come up with some more interesting programs. Perhaps some sort of IMP language, where the synthesizer can look through the entire search space (this might explode really fast with a language like IMP) to find equivalent programs.

[SanjitBasker]

I worked with @obhalerao on this assignment. We were inspired by the discussion of strength reduction in our compilers class and wanted to see if this library could be used to search for strength reductions automatically.

Implementation

We came up with two improvements to the code:

• a special syntax for a hole ??, which can signify a sum of variables, or a constant. in particular it allows the solver to select a single variable from the source expression. this required a slight tweak to how the interp function handles constants.
• allowing the bit-vectors to be of a configurable width (this allows us to see how the runtime of the code scales with the width of the integers)
• switching from signed operations to unsigned operations (we felt that these are simpler to reason about)

Testing

To demonstrate the first improvement, we used the following testcase on bitvectors of width 8:

w * 0 + x * 13 + y * 8 + z * 4
?? + ?? << ?? + ?? << ??

The expected output is something like x + (x + y) << 3 + (x + z) << 2. The program outputs ((x + 144) + (((x + z) + 128) << 2)) + (((x + y) + 238) << 3), which is also correct because the constants cancel out. While this is a quirk of the implementation (the token ?? gets turned into a term like _c + (_b0 ? z : 0) + (_b1 ? x : 0) + (_b2 ? y : 0) + (_b3 ? z : 0)), it also reminds us of the importance of the "cleanup" step in which we interpret the output of the solver on our de-sugared input. We decided that pretty-printing the relevant variables was plenty of work and stopped here.

For the second improvement, we changed the width to 32 and used the following testcase:

(x >> 16) / 10
((x >> 16) * ??) >> ??

Based on Wikipedia, we expect that for a value of z which fits in a uint16_t, the expressions ((uint32_t) z * (uint32_t)0xCCCD) >> 19) and z / 10 are equal. The x >> 16 input is our way of telling the solver that only the upper 16 bits of the input must be 0. We get the output ((x >> 16) * 52429) >> 19, which agrees with Wikipedia 🎉

This part of the assignment was the most fun, we did some more reading on general magic division but didn't have time to implement a more fleshed out pipeline.

[stephenverderame]

Summary

• Repo

I modified ex2.py to include a sketch-like disjunction of expressions which is basically sugar for nested condtionals. So for example, {x | y | h1 | x + y | x - y | -x | -y} would give the synthesizer the choice of x, y, x + y, x - y, -x, -y and a constant. I also added other bitwise operators such as xor, and, and or.

Testing

I added a few sketches, first starting with rewriting s4 in the new syntax

x * 9
x << {x | h1} + {x | h2}

I also wrote some sketches testing the new bitwise operators such as this one which Z3 solved instantly

z
x ^ y ^ z ^ {x | y | z | h1} ^ {x | y | z | h2} ^ {x | y | z | h3}

[NgaiJustin]

Summary

• Repo (link)

Details

I used the ex2.py as a template and extended support for %, ==, !=, <, >, <=, >=. I updated the grammar to support these new operators and also updated the implementer code to support these new operators.

Testing/Evaluation and Difficulties

• I added the custom tests eq.txt, neq.txt, lt.txt, gt.txt, lte.txt,
  gte.txt, mod.txt to test the new operators.
• An issue I ran into was that the application of parenthesis would be very
  particular. For example the following is fine:

3 * x == 207
x == ((1 - 23) * (69 + 23) + 23 * (69 - 1 + 23))

But this would not work:

3 * x == 207
x == ((1 - 23) * (69 + 23) + 23 * (69 - 1 + 23))

[keikun555]

Summarize what you did.

• Lesson 13 Task
• ex2.py with bitwise operators: I added bitwise operators &, |, ^, and ~.
• Test files

Explain how you know your implementation works—how did you test it? Which test inputs did you use? Do you have any quantitative results to report?

• I made test files inspired from this wiki page
• I used this turnt configuration and made sure the output was commensurate with the inputs.

❯ turnt -j $(find . -iname "*.txt" | sort)
1..6
ok 1 - ./sketch/b1.txt sketch
ok 2 - ./sketch/b2.txt sketch
ok 3 - ./sketch/b3.txt sketch
ok 4 - ./sketch/b4.txt sketch
ok 5 - ./sketch/b5.txt sketch
ok 6 - ./sketch/s2.txt sketch
❯

What was the hardest part of the task? How did you solve this problem?

• It was hard coming up with test files since the language itself had many restrictions on what could be on the left hand side and the right hand side.
• I ended up showing there are identity elements of the new binary operators since they were the easiest.

[ryanwmao]

@xalbt , he-andy, and I worked together on lesson 13.

Summary

repo

Implementation

• We used the ex2.py code as a starting point.
• We initially wanted to do something related to strength reduction, but we found ourselves fighting with z3 quite a bit. We extended the language in ex2.py to support some of the operations we wanted to use, but we couldn't get the sketch to work.
• We wrote a sketch that performs an lea instruction that we thought was somewhat interesting to work with in z3.

Difficulties

Our biggest difficulties were with z3 usage. We came across some error messages that were not easy to interpret, which led to a bit of tedious debugging.

Testing

test5.txt:

x * 5
(x + ((65535 ? (x) : (y)) << (0 ? (0) : (0 ? (1) : (65535 ? (2) : (3)))))) + 0

the corresponding lea instruction is lea dst, [x+x*4]

test4.txt:

(2 * ((x + (y * 4)) + 3)) - x
(x + ((0 ? (x) : (y)) << (0 ? (0) : (0 ? (1) : (0 ? (2) : (3)))))) + 6

the corresponding lea instruction is lea dst, [x + y*8 + 6]

bonus:
test3.txt:

x % 2
x & 1

[alifarahbakhsh]

Repo

A very simple synthesizer using Z3. I have added exponentiation via the operator ^ to the simple grammer introduced in the class.
Most of the code comes from the ex2.py program from the sampsyo/minisynth repository. The solver allows us to find the coefficients in the expanded version of a polynomial like (x-1) ^ 2. The holes can only be in the coefficients.

The only challenge I faced was the one mentioned by Benny as well: I had to implement x^n by literally multiplying x by itself n times.

[zachary-kent]

@rcplane and @zachary-kent worked together

Summary

Link to repo.

We extended the grammar of minisynth to include mutable
assignments, (roughly) based off @bcarlet's task implementation with some
modifications, and then for loops with a fixed lower and upper bound.

Implementation

• We first extended the grammar with mutable assignments of the form x := e
  where x is an identifier and e is an expression. The start non-terminal of
  the grammar was then 0 or more statements in sequence followed by an
  expression. Semantically, each of these assignments are evaluated one by one
  and then the final expression is evaluated in the environment extended by the
  bindings introduced by mutable assignments. For example, the following code
  snippet would evaluate to 2:

  x := 0
  x := x + 1;
  x + 1
  

  This syntax was adapted from @bcarlet's implementation, alongside the
  structure of the modified interpreter, which is parameterized over functions
  assign and lookup are used to introduce and access mutable bindings.

• However, we implemented the assign and lookup operations themselves
  differently, drawing from symbolic execution. In symbolic execution, we
  maintain an environment from identifiers to symbolic values, which are
  expressed entirely in terms of the inputs to the program; in this case,
  universally quantified variables. By the time all mutable assignments in the
  program are evaluated, every variable, including those introduced/modified by
  mutable assignment, can be expressed in terms of the universally quantified
  variables. Finally, for a program x1 := e1; ...; xn := en; e, after
  evaluating all mutable assignments, we can then use the map from variables to
  symbolic values to express e purely in terms of program inputs.

• We then extended the grammar with bounded for loops so that there were two
  variants of top level statements:

  start ::= stmt* exprs
  stmt ::= for i = start to end do stmt* done; | x := expr
  

  Because the lower and upper bounds of loops are known statically, we simply
  unroll them when interpreting them. That is, we can unroll every arbitrarily
  nested loop into a finite sequence of assignments. This did not require too
  many modifications to the interpreter beyond those introduced for assignments.

• Holes can still only be placed within expressions; that is, a hole cannot
  stand in for an entire statement.

Tests and Results

• We initially tested sketch completion starting with regression testing for
  addition expression solving and simple assignment then moved up to small loops
  and nested loops, varying the location of the hole.
• A simple bash script
  was written to repeat tests and confirm pretty output behavior. Sample ouptut
  is included below:

examples/assign.txt
x := 1;
x := x + 1;
x
----
??
Synthesized:
2
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
examples/assign_sketch.txt
x := 0;
x := x + 10;
x
----
x + ??
Synthesized:
0 + 10
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
examples/basic.txt
x * 9
----
x << ?? + ??
Synthesized:
(x << 3) + x
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
examples/body_hole.txt
for i = 1 to 2 do
  for j = 1 to 2 do
    x := x * 2;
  done; 
done;
x
----
for i = 1 to 2 do
  for j = 1 to 2 do
    x := x + ??;
  done; 
done;
x
Synthesized:
for i = 1 to 2 do
for j = 1 to 2 do
x := x + x;
done;
done;
x
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
examples/loop_sketch.txt
a := 0;
for i = 1 to 2 do a := a + 1; done;
a
----
a := 0;
a := a + ??;
a
Synthesized:
a := 0;
a := a + 2;
a
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
examples/loop_sum.txt
for i = 1 to 2 do
  a := a + 1; 
done;
a
----
a + ??
Synthesized:
a + 2
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+
examples/loops.txt
for i = 1 to 2 do
  for j = 1 to 3 do
    a := a * 2; 
  done; 
done;
a
----
a * ??
Synthesized:
a * 64
+-+-+-+-+-+-+-+-+-+-+-+-+-+-+

Difficulties

• Ideally, we would be able to represent entire statements using holes that
  could be filled in. However, it was not clear how to do this. We considered
  using an axiomatized program logic, like one based of KAT, but this seemed
  much too difficult for this task.
• We struggled with how best to represent the synthesized program, striking a
  balance between readibility and degree of simplification. For example, you can
  display the entire unrolled program, but this would be very difficult to read.
  In the end, we decided to maintain the structure of loops when displaying the
  synthesized program to the user.
• Large loop counts and broad holes in loop bodies led to invalid model errors
  in z3 expression construction. Specifically, we very quickly overflowed the
  bit vector when doing computations with nested loops.

Generative AI

• Both of us used GitHub Copilot throughout the task, which was mildly helpful,
  especially for generating documentation. However, completions for printing
  functions and interpreter logic was lacking, often taking on javascript syntax
  instead of python perhaps getting confused by the context conditioning of semi
  colons in the lark grammar early in the solve.py file. It was mainly useful
  for generating debugging statements, such as the following for printing the
  sketch program:

  print(f"Sketch: {pretty(tree1)}")
  

• Chat GPT4 April 2023 was used in early brainstorming to transcribe Stein's
  algorithm for binary GCD calcuation as an expression loop body to compare
  operation count Z3 optimization against a Euclid loop body, but using opt was
  a different track of project than augmenting Z3 solve lark interpretation.

[AliceSzzze]

Summary

I wrote two small snippets for this week's assignment.

• sort.py: I was looking into the theory of arrays in Z3 and came across a really cool StackOverflow post. The code outputs a potentially unsorted array A and S which is a sorted version of array A. It does this by adding the constraints that the elements in S have to be non-increasing, and that the two arrays contain the same set of elements by keeping a counter of occurrences. I modified the code from this post to take in an array A with hardcoded elements, which outputs a sorted array S. The output of this program is

A = [9984, 4, -5, 75, -9]
S = [-9, -5, 4, 75, 9984]

• function.py

x = Int('x')
# f takes in an int and returns an int
f = Function('f', IntSort(), IntSort())
solve (ForAll([x], f(x) == x*x*(x+2)))

I read that there are functions in Z3 from the Z3py documentation and wanted to try it out. Perhaps not the most exciting example, but I found it a little surprising that it didn't spit out the same formula but instead rewrote it slightly

[f = [else -> 2*Var(0)*Var(0) + Var(0)*Var(0)*Var(0)]]

Challenges

I feel like I have only scratched the surface of Z3. I see that it is able to solve sudoku and eight queens, a flavor of subset-sum etc. but it is not easy to formulate a problem in Z3 terms. I tried to solve 3-sum (see if there are three elements in an array that sum to a target) but ran into an issue

s.add (Exists([x, y, z], a[x] + a[y]+ a[z] == -10))
                             ~^^^
TypeError: list indices must be integers or slices, not ArithRef

[yxd97]

Summary

• Implementation code
• I was trying to synthesis a binary adder from an inteter add where one of the operands are constant.
• However, I was not able to finish a functional design before the deadline.

Implementation

• The idea is to treat the constant side as a hole variable, write out the logic expressions using each bit of it, and let the solver to solve.
• To facilitate logic operations, I added a new operator to the example grammar: getbit (::). When writing x::3 that is getting the 3rd bit (starting from 0) of variable x. This operator is implemented as (lhs >> rhs) & 1.
• In the main solver, there is a loop that forms the expressions of each bit of sum and carry, all written as an if operation depending on the corresponding bit of the hole.
  • for sum: s_i = h_i ^ x_i ^ cin = h_i ? not(x_i) ^ cin : x_i ^ cin
  • for carry: cout = h_i && x_i || h_i && cin || x_i && cin = h_i ? x_i && cin : x_i || cin
• The final equation would be x + const = s_0 + s_1 * 2 + s_2 * 4 + ..., every s_i is a function of x and the hole
• I was able to confirm that the logic expressions are correct, but when solving the equation, I got an sort mismatch exception from z3, which is because the type of two sides of the equation are z3.BitVecRef and z3.AirthRef. I did not find a way to solve it.

Testing

• I leveraged pytest to test the newly added getbit operation. I randomly generated 10 groups of input values and they all produce correct results. The test can be found in test_intrp.py.
• When composing the logic function, I did ad-hoc testing of the output of the logic functions by feeding some inputs to them. I was able to confirm they are correct, but I don't have systemetic test cases to show.

Difficult part

Learning z3 is the biggest headache for me. I actually started with adding logic operations to the example grammar but later realized that symbolic values can not be used with python's if statements. I had to forcing myself thinking in the symbolic way of writing programs. I have to admit that I didn't do well in such a way of programming.

[evanmwilliams]

Summary

I worked on this with @emwangs. See the repo here.

Implementation

We added more arithmetic operations to the example from class - we were both a bit busy this week so we opted not to do anything super ambitious. It was simple enough though - we just had to modify the grammar, interpreter, and pretty printer a bit to support operations such as MOD and XOR.

Testing/Evaluation

I wrote one test per new instruction added. One of the interesting ones was MOD:

12 % x
(y * 3) % x

which gave:

[ForAll(x, 12%x == (y*3)%x)]
12 % x
(4 * 3) % x

Difficulties

None! We found this one to be pretty fun :)

[jiahanxie353]

Summary

In this assignment, I worked from ex2.py and supported more binary operations.

Implementation and Testing

I added implementation and updated the grammar to support more binary operations, namely >, >=, <, <=, ==, !=, and %.
Then I wrote corresponding tests for each operation to verify that they work as expected.
It's been a busy week so I chose a straightforward task, but synthesis is very fun and I'd like to delve in more in the future :)

[jdroob]

@20ashah and I implemented the following here

Implementation

The main features we added to the language were simply the boolean operators &, |, ^, and the comparison operators >, <, !=, and ==. This allowed us to verify the equivalence of expressions such as:

A | 1
and
h

However, we wanted to be able to verify the equivalence of slightly more complex expressions such as De Morgan’s Law:

~A | ~B
~(h1 & h2)

The desired output would be ~(A & B) but to start, we didn’t have support for this kind of functionality. The key insight was that for expressions such as hb1 ? x : hn1 the SMT solver could use either quantified variables (in this case x) or the hole variables (in this case hn1). To neatly write the expressions we were interested in, we decided to use the convention that hole variables beginning with ‘h_’ were the ones we wanted to replace with plain variables. Otherwise, we were just interested in replacing them with constants like in the tutorial.

To implement this functionality, we modified the synthesize function such that expr2 would be passed into a new function called preprocess. preprocess replaced each ‘h_’ hole variable with a conditional switch expression like the one mentioned above.

Next, the Z3 solve function was called as usual. Lastly, expr2 and the model returned by solve are passed into a function called postprocess. Essentially, postprocess constant folds the conditional branches based on the values returned by solve which is either a constant or a quantified variable.

Testing

De Morgan’s Law

Input:

~x | ~y
~(h_ & h_1)

Output:

{'h_': y, 'h_1': x}

Distributive

Input:

(A | B) & (A | C)
h_1 | (h_2 & h_3)

Output

{'h_1': A, 'h_2': C, 'h_3': B}

Absorption

Input:

A&(A|B)
h_1

Output:

{'h_1': A}

Challenges

The preprocess and postprocess functions were challenging to implement. We did run into a roadblock with the below example:

Input:

(x+y)*(x+y)
h_1*h_1 + 2*h_1*h_2 + h_2*h_2

When running this example, our synthesizer would hang until we aborted the program. We weren’t sure if this was an example you discussed where Z3 would take a while or if there was an issue on our end. It seemed like our program should’ve been able to support this but my guess is that we’re still missing something. Either way - this was a fun task!