CSL 862: Assignment 1 - Verifying a Compilation
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.
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 . . .