**CSL 862: Assignment 1 - Verifying a
Compilation**

- Write a compiler to translate the following src language into the following dst language.
- Write a verifier that checks that the code in dst language is semantically equivalent to the code in the src language.
- 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

- Use your verifier to check that the unoptimized and optimized programs are equivalent.

Assume that expressions and registers hold 32-bit values.

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.

- 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 . . .