CSL 862: Assignment 1 - Verifying a Compilation

1. Write a compiler to translate the following src language into the following dst language.
2. Write a verifier that checks that the code in dst language is semantically equivalent to the code in the src language.
3. Implement some of the following optimizations/analyses on the dst language:
   • Liveness analysis
   • Reaching definitions analysis
   • Common subexpression elimination
   • Constant Propagation
   • Constant Folding
   • Register Allocation (for this you may want to define an intermediate representation that has infinite registers)
   • Dead code elimination
4. Use your verifier to check that the unoptimized and optimized programs are equivalent.

Assume that expressions and registers hold 32-bit values.

Tools

You can use Z3 as the SAT solver for use in your verifier. Z3 is available for C, C++, Python, OCaml and .Net. Please have a look at the stock examples of Z3. You should use the Z3's "bitvector" support.

Testing

• Write some test programs, and compile them using your compiler to test your verifier
• Generate hand-optimized dst programs semantically equivalent to your original program, and check them for equivalence.

SRC Language:

exp -> “(” exp op exp “)”

| num

| ident

| “(” cond_expr ? exp : exp “)”

ident -> {alphabetic char}

num -> natural number

op -> “+” | “*”

exp_right -> exp

statement -> ident ":=" exp_right ";" statement | ""

return -> exp

ident_list -> ident ident_list | ""

fun_decl -> "fun" ident "("ident_list")"

program -> fun_decl "{"statement"}" return ";"

cond -> “(” exp == exp “)”

| “(” exp > exp “)”

| “(“ exp < exp “)”

| “true” | “false”

| “false”

| “(” cond_expr ")"

cond_expr -> cond_expr “&&” cond

| cond_expr “||” cond

| cond

Semantics:

program.value = return.value

return.value = exp.value

exp.value = num

| ident.value

| (num + exp.value)

| (num * exp.value)

| if cond is true then exp1 else exp2

ident.value = exp_right.value [second assignment to ident shadows the earlier binding]

exp_right.value = exp.value

DST Language:

cmd -> "mov" r1 r2/num ";"

| "add" r1 r2/num ";"

| "mul" r1 r2/num

| "load" r1 r2/num

| "store" r1 r2/num

| "and" r1 r2/num

| "or" r1 r2/num

| "not" r1 r2/num ";"

| "cmp" r1 r2/num ";"

| "movf" r1 ";"

| "je" label ";"

| "jl" label ";"

| “jg” label “;”

| “jle” label “;”

| “jge” label “;”

| “jmp” label “;”

program -> {cmd}

Semantics:

There are 32 GP registers are available, a flag register, and a program counter (PC) register. There is also 32-bit byte-addressable memory.

program.value = r0.value

"mov" r1 r2/num ";" stores r2/num value in r1

"add" r1 r2/num ";" stores r2/num + r1 in r1

"mul" r1 r2/num ";" stores r2/num * r1 in r1

"and" r1 r2/num ";" stores r2/num && r1 in r1

"or" r1 r2/num ";" stores r2/num || r1 in r1

"not" r1 r2/num ";" stores not(r2/num) in r1

"load" r1 r2/num ";" loads value at address r2/num from memory, and stores it in r1

"store" r1 r2/num ";" stores value in r1 to address r2/num in memory

"cmp" r1 r2/num ";" stores r1/num - r2/num in flag register. The flags register is 33-bits long (to avoid overflow)

"movf" r1 ";" move flags to register r1.

"je" label ";" jump to label if flag == 0

"jg" label ";" jump to label if flag > 0

"jl" label ";" jump to label if flag < 0

"jge" label ";" jump to label if flag >= 0

"jle" label ";" jump to label if flag <= 0

Initially, assume that the arguments to the function (if any) are stored starting at address r1. i.e., first argument is at memory address (r1), second argument is at memory address 4(r1), third at 8(r1), and so on . . .