4 Homework 4
Released: Wednesday, February 1, 2023 at 6:00pm
Due: Wednesday, February 8, 2023 at 6:00pm
What to Download:
Please start with this file, filling in where appropriate, and submit your homework to the HW4 assignment on Gradescope. This page has additional information, and allows us to format things nicely.
4.1 Superoptimization
Superoptimization is the idea of replacing a given loop-free sequence of instructions with an equivalent sequence of instructions that is somehow better (usually, shorter and as a result, faster). It’s used in compilers at the very lowest level, to optimize numeric operations into often counter-intuitive sequences of instructions that can be baffling at first. It was invented by computer scientist Alexia Massalin in 1987: her idea was to find the shortest sequence of instructions, given a particular instruction set, to compute a given function. This is in contrast to most compiler optimization, which merely aim to improve performance, rather than finding truly optimal solutions.
The resulting programs often rely somewhat complex interactions between different instructions, and sometimes "startling" programs that rely on strange overlap between representations of different values: often times, code with branches is replaced with equivalent code that doesn’t use branches, for example.
4.2 Problem 1
While super-optimization is something that can be done using SMT solvers, in this homework, we will tackle a simpler problem: verifying ordinary optimizations. In particular, showing that a program before and after an optimization are equivalent.
Our first optimization will use a slightly extended version of the same stack-based calculator
from HW2. Note that since we are using the language #lang rosette/safe instead of #lang isl-spec, define-struct is slightly different, in that by default the struct values will
print out without showing their contents. The #:transparent optional argument changes
that.
(define-struct push [num] #:transparent)
(define-struct add [] #:transparent)
(define-struct mul [] #:transparent)
(define-struct sub [] #:transparent)
; A SimpleInstr is one of:
; - (make-push Number)
; - (make-add)
; - (make-mul)
; - (make-sub)
(define (simple-eval stk instrs)
(local [; stack-binop : [Number Number -> Number] [List-of Number]
; [List-of SimpleInstr] -> [List-of Number]
; evaluates a binary operator on top two numbers of stack, if present
(define (stack-binop op stk instrs)
(if (>= (length stk) 2)
(simple-eval (cons (op (first stk) (second stk))
(rest (rest stk)))
instrs)
(list)))
; eval-instr : Instr [List-of Number] [List-of SimpleInstr] -> [List-of Number]
; evaluates a single instruction, given a stack and rest of instructions
(define (eval-instr i stk instrs)
(cond [(add? i) (stack-binop + stk instrs)]
[(mul? i) (stack-binop * stk instrs)]
[(sub? i) (stack-binop - stk instrs)]
[(push? i) (simple-eval (cons (push-num i) stk) instrs)]))]
(cond [(empty? instrs) stk]
[(cons? instrs) (eval-instr (first instrs) stk (rest instrs))])))
Your task is to first implement a function that verifies that two programs written in this language are equivalent, where equivalent means runs to the same thing:
; simple-stack-verify : [List-of SimpleInstr] [List-of SimpleInstr] -> Boolean
(define (simple-stack-verify p1 p2)
...)
4.3 Problem 2
The next problem is to implement a simple optimization. In this case, we want you to implement
a simple form of constant folding. Constant folding is the idea of replacing a series of
operations that are all on constants with the result of running those operations at optimization time. By doing it at optimization time, it won’t have to be done when the program is actually running. In this case,
we want your optimization to replace the sequence (make-push n) (make-push m) (make-add) with (make-push o) where o is m plus n. You do not need to (and should not) replace
sequences that only appear after the initial constant folding has been done. i.e., the sequence (make-push l) (make-push n) (make-push m) (make-add) (make-add) should turn into (make-push l) (make-push o) (make-add), where o is the result of adding n and m, but should not be further optimized into a single (make-push p), where p is the result of adding l and o.
; simple-const-fold: [List-of SimpleInstr] -> [List-of SimpleInstr]
(define (simple-const-fold p)
...)
4.4 Problem 3
To check that your constant folding works, we are going to take two approaches. First, we’ll
use Property Based Testing (PBT) using the Quickcheck library. In order to do that, you need to
define a generator for SimpleInstrs. Note that, since we are in a #lang rosette/safe file, we have required the quickcheck library directly, so there are no qc: prefixes on the functions.
; choose-simple-instr : [Generator SimpleInstr]
(define choose-simple-instr ...)
With that, you can now define a property that generates a list of instructions, runs the constant
folding optimization on it, and then verifies that the result is equivalent to the original program. Note that property is how the quickcheck library writes for-all.
(quickcheck (property [...] ...))
4.5 Problem 4
To gain more confidence in our approach, we’ll use Rosette to do a limited form of exhaustive
testing. First, we’ll define a symbolic version of a SimpleInstr, using choose* to enumerate different possibilies (for reference on how to do this, see lecture notes: 2/1):
; symbolic-simpl-instr : -> [Symbolic SimpleInstr]
(define (symbolic-simple-instr) ...)
Using that, we can define a program that a is list of up to 6 instructions. Think about how you could have it be up to 6 instructions, rather than exactly 6 instructions.
; symbolic-simple-prog : [Symbolic [List-of SimpleInstr]]
(define symbolic-simple-prog ...)
Finally, we can now use this symbolic program to verify that the constant folding optimization
works on all programs of up to 6 instructions by using verify and
assert from Rosette.
(verify (assert ...))
4.6 Problem 5
In this problem, we’ll extend the stack calculator to include variables, so that
there are real limits to what even the best constant folding could do. We represent variable
names with numbers, to make things easier, and now eval takes a set of
variable bindings that give values for each variable.
(define-struct var [name] #:transparent)
; An Instr is one of:
; - (make-push Number)
; - (make-add)
; - (make-mul)
; - (make-sub)
; - (make-var Number)
(define-struct bind [name value] #:transparent)
; A Binding is a (make-bind Number Number)
; eval : [List-of Binding] [List-of Number] [List-of Instr] -> [List-of Number]
; will return an empty list if it reaches an unbound variable, or a malformed
; program (trying to do an operation without enough values on stack).
(define (eval env stk instrs)
(local [; stack-binop : [Number Number -> Number] [List-of Number]
; [List-of Instr] -> [List-of Number]
; evaluates a binary operator on top two numbers of stack, if present
(define (stack-binop op stk instrs)
(if (>= (length stk) 2)
(eval env
(cons (op (first stk) (second stk))
(rest (rest stk)))
instrs)
(list)))
; lookup-var : String [List-of Binding] [List-of Number]
; [List-of Instr] -> [List-of Number]
(define (lookup-var name env stk instrs)
(cond [(empty? env) (list)]
[(cons? env) (if (equal? name (bind-name (first env)))
(eval env
(cons (bind-value (first env))
stk)
instrs)
(lookup-var name (rest env) stk instrs))]))
; eval-instr : Instr [List-of Number] [List-of SimpleInstr] -> [List-of Number]
; evaluates a single instruction, given a stack and rest of instructions
(define (eval-instr i stk instrs)
(cond [(add? i) (stack-binop + stk instrs)]
[(mul? i) (stack-binop * stk instrs)]
[(sub? i) (stack-binop - stk instrs)]
[(push? i) (eval env (cons (push-num i) stk) instrs)]
[(var? i) (lookup-var (var-name i) env stk instrs)]))]
(cond [(empty? instrs) stk]
[(cons? instrs) (eval-instr (first instrs) stk (rest instrs))])))
Your first task is to make an updated version of your verify function, to check that two programs are equivalent. Now, you take in a set of variable bindings that both programs will use.
; stack-verify : [List-of Binding] [List-of Instr] [List-of Instr] -> Boolean
(define (stack-verify env p1 p2) ...)
Your next task is to define a more general version of constant folding. This time, look for
any sequence of (make-push n) (make-push m) (make-op) where op is one of add, sub, or mul. You still
shouldn’t replace sequences that only appear after the initial constant folding has been done.
; const-fold : [List-of Instr] -> [List-of Instr]
(define (const-fold p) ...)
Now, define a new generator for instructions:
; choose-instr : [Generator Instr]
(define choose-instr ...)
And a generator for bindings:
; choose-bind : [Generator Binding]
(define choose-bind ...)
So you can do PBT testing of your constant folding:
(quickcheck (property [...] ...))
Now you’ll update the symbolic version, by defining a symbolic instruction, program, binding, and environment. Note that for this example, to keep things running fast, have the program have only up to 4 instructions, and have the environment have only up to 2 bindings.
; symbolic-instr : [Symbolic Instr]
(define (symbolic-instr) ...)
; symbolic-prog : [Symbolic [List-of Instr]]
(define symbolic-prog ...)
; symbolic-bind : [Symbolic Binding]
(define (symbolic-bind) ...)
; symbolic-env : [Symbolic [List-of [Symbolic Binding]]]
(define symbolic-env ...)
And finally using that, we can run the same verification as before:
(verify (assert ...))