Commit db0572e2 authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

major cleanup of directory structure

parent ca07259c
*.bak
*.swp
......@@ -35,7 +35,7 @@ end
module KaratAvr
use import avrmodel2.AVRint
use import avrmodel.AVRint
use import int.Int
use import int.EuclideanDivision
use import bv.Pow2int
......@@ -1234,7 +1234,7 @@ assert { at(uint 3 reg 8)'L11 + pow2 24*uint 6 reg 8 + pow2 72*uint 3 reg 20 +
std rZ 10 r21;
std rZ 11 r22
use avrmodel2.Shadow as S
use avrmodel.Shadow as S
lemma mul_bound_preserve:
forall x y l. 0 <= x <= l -> 0 <= y <= l -> x*y <= l*l
......
......@@ -73,6 +73,11 @@ let mov (dst src: register): unit
ensures { reg = old reg[dst<-reg[src]] }
= reg.data <- Map.set reg.data dst (Map.get reg.data src)
let movw (dst src: register): unit
writes { reg }
ensures { reg = old reg[dst<-reg[src]][dst+1<-reg[src+1]] }
= reg.data <- Map.set (Map.set reg.data dst (Map.get reg.data src)) (dst+1) (Map.get reg.data (src+1))
let mul (dst src: register): unit
writes { cf }
writes { reg }
......@@ -89,19 +94,12 @@ let add (dst src: register): unit
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] + reg[src])) 256] }
ensures { ?cf = div (old (reg[dst] + reg[src])) 256 }
= let sum = Map.get reg.data src + Map.get reg.data dst in
let r1 = (Map.get reg.data dst) in
let r2 = (Map.get reg.data src) in
reg.data <- Map.set reg.data dst (mod sum 256);
let res = (Map.get reg.data dst) in
if r1 >= 128 && r2 >= 128 ||
r1 >= 128 && res < 128 ||
r2 >= 128 && res < 128
then
cf.value <- True
else
cf.value <- False
cf.value <- (r1 >= 128 && r2 >= 128 || r1 >= 128 && res < 128 || r2 >= 128 && res < 128)
let adc (dst src: register): unit
writes { cf }
......@@ -136,30 +134,6 @@ let sbc (dst src: register): unit
cf.value <- (-div sum 256 <> 0);
()
(* immediate versions *)
let subi (dst: register) (k: int): unit
requires { 0 <= k <= 255 }
writes { cf }
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] - k)) 256] }
ensures { ?cf = -div (old (reg[dst] - k)) 256 }
= let sum = Map.get reg.data dst - k in
reg.data <- Map.set reg.data dst (mod sum 256);
cf.value <- (-div sum 256 <> 0);
()
let sbci (dst: register) (k: int): unit
requires { 0 <= k <= 255 }
writes { cf }
reads { cf }
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] - k - ?cf)) 256] }
ensures { ?cf = -div (old (reg[dst] - k - ?cf)) 256 }
= let sum = Map.get reg.data dst - k - ?cf in
reg.data <- Map.set reg.data dst (mod sum 256);
cf.value <- (-div sum 256 <> 0);
()
(* these instructions do not modify the carry flag *)
let inc (dst: register): unit
writes { reg }
......@@ -183,13 +157,10 @@ let ld_inc (dst src: register): unit
writes { reg }
reads { mem }
requires { 32 <= uint 2 reg src < pow2 16-1 }
(* TODO: unnecessary
requires { dst <> src /\ dst <> src+1 }
*)
ensures { let cur = uint 2 (old reg) src in
let inc = cur+1 in
reg = (old reg)[dst <- mem[cur]][src <- mod inc 256][src+1 <- div inc 256] }
ensures { uint 2 reg src = old(uint 2 reg src)+1 }
= let cur = Map.get reg.data src + 256*Map.get reg.data (src+1) in
let nxt = mod (cur+1) (pow2 16) in
reg.data <- Map.set (Map.set (Map.set reg.data dst (Map.get mem.data cur)) src (mod nxt 256)) (src+1) (div nxt 256)
......@@ -212,31 +183,21 @@ let std (dst ofs src: register): unit
= let cur = Map.get reg.data dst + 256*Map.get reg.data (dst+1) in
mem.data <- Map.set mem.data (cur+ofs) (Map.get reg.data src)
(* stack operations *)
constant stack_limit: int
val stack_pointer: ref int
val stack: address_space
let push (src: register): unit
writes { stack, stack_pointer }
reads { reg }
ensures { stack = old(stack[!stack_pointer <- reg[src]]) }
ensures { !stack_pointer = old !stack_pointer - 1 }
= stack.data <- Map.set stack.data (!stack_pointer) (Map.get reg.data src);
stack_pointer := !stack_pointer - 1
let pop (dst: register): unit
writes { reg, stack_pointer }
reads { stack }
ensures { reg = (old reg)[dst <- stack[!stack_pointer]] }
ensures { !stack_pointer = old !stack_pointer + 1 }
= stack_pointer := !stack_pointer + 1;
reg.data <- Map.set reg.data dst (Map.get stack.data !stack_pointer)
let nop (): unit
= ()
let sbci (dst: register) (k: int): unit
requires { 0 <= k <= 255 }
writes { cf }
reads { cf }
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] - k - ?cf)) 256] }
ensures { ?cf = -div (old (reg[dst] - k - ?cf)) 256 }
= let sum = Map.get reg.data dst - k - ?cf in
reg.data <- Map.set reg.data dst (mod sum 256);
cf.value <- (-div sum 256 <> 0);
()
(****** REASONING ABOUT MACHINE STATE *)
predicate eq (w: int) (reg reg': address_space) (lo: int)
......@@ -249,6 +210,47 @@ goal eq_combine:
goal eq_uint:
forall reg reg', lo w. eq w reg reg' lo -> uint w reg lo = uint w reg' lo
(*
lemma uint_0:
forall reg, lo. B.sum (reg,lo) 0 0 = 0
lemma uint_1:
forall reg, lo. B.sum (reg,lo) 0 1 = reg[lo]
lemma uint_2:
forall reg, lo. B.sum (reg,lo) 0 2 = reg[lo] + pow2 8*reg[lo+1]
lemma uint_3:
forall reg, lo. B.sum (reg,lo) 0 3 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2]
lemma uint_4:
forall reg, lo. B.sum (reg,lo) 0 4 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3]
lemma uint_5:
forall reg, lo. B.sum (reg,lo) 0 5 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4]
lemma uint_6:
forall reg, lo. B.sum (reg,lo) 0 6 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5]
lemma uint_7:
forall reg, lo. B.sum (reg,lo) 0 7 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 32*pow2 16*reg[lo+6]
lemma uint_8:
forall reg, lo. B.sum (reg,lo) 0 8 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7]
lemma uint_9:
forall reg, lo. B.sum (reg,lo) 0 9 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8]
lemma uint_10:
forall reg, lo. B.sum (reg,lo) 0 10 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9]
lemma uint_11:
forall reg, lo. B.sum (reg,lo) 0 11 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10]
lemma uint_12:
forall reg, lo. B.sum (reg,lo) 0 12 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11]
meta rewrite prop uint_1
meta rewrite prop uint_2
meta rewrite prop uint_3
meta rewrite prop uint_4
meta rewrite prop uint_5
meta rewrite prop uint_6
meta rewrite prop uint_7
meta rewrite prop uint_8
meta rewrite prop uint_9
meta rewrite prop uint_10
meta rewrite prop uint_11
meta rewrite prop uint_12
*)
lemma uint_0:
forall reg, lo. B.sum (reg,lo) 0 0 = 0
lemma uint_1:
......@@ -299,114 +301,8 @@ meta rewrite prop uint_15
lemma uint_16:
forall reg, lo. B.sum (reg,lo) 0 16 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15]
meta rewrite prop uint_16
lemma uint_17:
forall reg, lo. B.sum (reg,lo) 0 17 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16]
meta rewrite prop uint_17
lemma uint_18:
forall reg, lo. B.sum (reg,lo) 0 18 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17]
meta rewrite prop uint_18
lemma uint_19:
forall reg, lo. B.sum (reg,lo) 0 19 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18]
meta rewrite prop uint_19
lemma uint_20:
forall reg, lo. B.sum (reg,lo) 0 20 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19]
meta rewrite prop uint_20
lemma uint_21:
forall reg, lo. B.sum (reg,lo) 0 21 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20]
meta rewrite prop uint_21
lemma uint_22:
forall reg, lo. B.sum (reg,lo) 0 22 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21]
meta rewrite prop uint_22
lemma uint_23:
forall reg, lo. B.sum (reg,lo) 0 23 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22]
meta rewrite prop uint_23
lemma uint_24:
forall reg, lo. B.sum (reg,lo) 0 24 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23]
meta rewrite prop uint_24
lemma uint_25:
forall reg, lo. B.sum (reg,lo) 0 25 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23] + pow2 192*reg[lo+24]
meta rewrite prop uint_25
lemma uint_26:
forall reg, lo. B.sum (reg,lo) 0 26 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23] + pow2 192*reg[lo+24] + pow2 200*reg[lo+25]
meta rewrite prop uint_26
lemma uint_27:
forall reg, lo. B.sum (reg,lo) 0 27 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23] + pow2 192*reg[lo+24] + pow2 200*reg[lo+25] + pow2 208*reg[lo+26]
meta rewrite prop uint_27
lemma uint_28:
forall reg, lo. B.sum (reg,lo) 0 28 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23] + pow2 192*reg[lo+24] + pow2 200*reg[lo+25] + pow2 208*reg[lo+26] + pow2 216*reg[lo+27]
meta rewrite prop uint_28
lemma uint_29:
forall reg, lo. B.sum (reg,lo) 0 29 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23] + pow2 192*reg[lo+24] + pow2 200*reg[lo+25] + pow2 208*reg[lo+26] + pow2 216*reg[lo+27] + pow2 224*reg[lo+28]
meta rewrite prop uint_29
lemma uint_30:
forall reg, lo. B.sum (reg,lo) 0 30 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23] + pow2 192*reg[lo+24] + pow2 200*reg[lo+25] + pow2 208*reg[lo+26] + pow2 216*reg[lo+27] + pow2 224*reg[lo+28] + pow2 232*reg[lo+29]
meta rewrite prop uint_30
lemma uint_31:
forall reg, lo. B.sum (reg,lo) 0 31 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23] + pow2 192*reg[lo+24] + pow2 200*reg[lo+25] + pow2 208*reg[lo+26] + pow2 216*reg[lo+27] + pow2 224*reg[lo+28] + pow2 232*reg[lo+29] + pow2 240*reg[lo+30]
meta rewrite prop uint_31
lemma uint_32:
forall reg, lo. B.sum (reg,lo) 0 32 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23] + pow2 192*reg[lo+24] + pow2 200*reg[lo+25] + pow2 208*reg[lo+26] + pow2 216*reg[lo+27] + pow2 224*reg[lo+28] + pow2 232*reg[lo+29] + pow2 240*reg[lo+30] + pow2 248*reg[lo+31]
meta rewrite prop uint_32
meta compute_max_steps 0x1000000
(* word operations *)
let movw (dst src: register): unit
(* TODO: unnecessary
requires { mod dst 2 = 0 /\ mod src 2 = 0 }
*)
writes { reg }
ensures { reg = old reg[dst<-reg[src]][dst+1<-reg[src+1]] }
= reg.data <- Map.set (Map.set reg.data dst (Map.get reg.data src)) (dst+1) (Map.get reg.data (src+1))
(*
let adiw (dst src: register): unit
requires { mod dst 2 = 0 /\ mod src = 0 }
writes { reg }
writes { cf }
ensures { reg = old reg[dst <- mod (old (reg[dst] + reg[src])) 256]
[dst+1 <- mod (old (reg[dst+1] + reg[src+1] + div (reg[dst] + reg[src]) 256)) 256] }
ensures { ?cf = div (old (uint 2 reg dst + uint 2 reg src)) 65536 }
ensures { ?cf*pow2 16 + uint 2 reg dst = old (uint 2 reg dst + uint 2 reg src) }
= add dst src;
adc (dst+1) (src+1)
let sbiw (dst src: register): unit
requires { mod dst 2 = 0 /\ mod src = 0 }
writes { reg }
writes { cf }
ensures { reg = old reg[dst <- mod (old (reg[dst] - reg[src])) 256]
[dst+1 <- mod (old (reg[dst+1] - reg[src+1] + div (reg[dst] - reg[src]) 256)) 256] }
ensures { ?cf = -div (old (uint 2 reg dst - uint 2 reg src)) 65536 }
ensures { uint 2 reg dst = ?cf*pow2 16 + old (uint 2 reg dst - uint 2 reg src) }
= sub dst src;
sbc (dst+1) (src+1)
*)
let adiw (dst: register) (k: int): unit
requires { 0 <= k < 64 }
writes { reg }
writes { cf }
ensures { reg = old reg[dst <- mod (old (reg[dst] + k)) 256]
[dst+1 <- mod (old (reg[dst+1] + div (reg[dst] + k) 256)) 256] }
ensures { ?cf = div (old (uint 2 reg dst + k)) 65536 }
ensures { ?cf*pow2 16 + uint 2 reg dst = old (uint 2 reg dst + k) }
= let sum = Map.get reg.data dst + 256*Map.get reg.data (dst+1) +k in
reg.data <- Map.set reg.data dst (mod sum 256);
reg.data <- Map.set reg.data (dst+1) (mod (div sum 256) 256);
cf.value <- (sum > 65535)
let sbiw (dst: register) (k: int): unit
requires { 0 <= k < 64 }
writes { reg }
writes { cf }
ensures { reg = old reg[dst <- mod (old (reg[dst] - k)) 256]
[dst+1 <- mod (old (reg[dst+1] + div (reg[dst] - k) 256)) 256] }
ensures { ?cf = -div (old (uint 2 reg dst - k)) 65536 }
ensures { uint 2 reg dst = ?cf*pow2 16 + old (uint 2 reg dst - k) }
= subi dst k;
sbci (dst+1) 0
(*************** BITVECTOR IMPORTS ********************)
use bv.BV8
......@@ -454,10 +350,7 @@ let com (dst: register): unit
let asr (dst: register): unit
writes { reg, cf }
ensures { reg = old reg[dst<- BV8.t'int (BV8.asr (BV8.of_int reg[dst]) 1)] }
(*
ensures { ?cf = mod (old reg[dst]) 2 }
*)
ensures { cf.value = BV8.nth (BV8.of_int (old reg[dst])) 0 }
= cf.value <- BV8.nth (BV8.of_int (Map.get reg.data dst)) 0;
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.asr (BV8.of_int (Map.get reg.data dst)) 1))
......@@ -489,23 +382,6 @@ function bitsetx (w: BV8.t) (b: int) (v: bool): BV8.t =
else
BV8.bw_xor w mask
lemma one_def:
BV8.nth (BV8.of_int 1) 0 /\ forall b. 0 < b < 8 -> not BV8.nth (BV8.of_int 1) b
goal bitset_correct1:
forall w, b, v. 0 <= b < 8 ->
BV8.nth (bitset w b v) b = v
goal bitset_correct2:
forall w, b i, v. 0 <= b < 8 -> 0 <= i < 8 -> i <> b ->
BV8.nth (bitset w b v) i = BV8.nth w i
goal bitset_equiv_def:
forall w, b, v. 0 <= b < 8 -> BV8.eq (bitset w b v) (bitset' w b v)
goal bitsetx_equiv_def:
forall w, b, v. 0 <= b < 8 -> BV8.eq (bitset w b v) (bitsetx w b v)
let bld (dst: register) (bit: int): unit
writes { reg }
requires { 0 <= bit < 8 }
......@@ -517,13 +393,13 @@ let bld (dst: register) (bit: int): unit
else
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.bw_or rd mask))
(*
let bld' (dst: register) (bit: int): unit
writes { reg }
requires { 0 <= bit < 8 }
ensures { reg = (old reg)[dst <- BV8.t'int (bitset' (BV8.of_int (old reg)[dst]) bit tf.value)] }
= let rd = BV8.of_int (Map.get reg.data dst) in
let mask = BV8.lsl (BV8.of_int 1) bit in
assert { forall w, b, v. 0 <= b < 8 -> BV8.eq (bitset w b v) (bitset' w b v) };
if ?tf = 0 then
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.bw_and rd (BV8.bw_not mask)))
else
......@@ -535,27 +411,28 @@ let bld'' (dst: register) (bit: int): unit
ensures { reg = (old reg)[dst <- BV8.t'int (bitsetx (BV8.of_int (old reg)[dst]) bit tf.value)] }
= let rd = BV8.of_int (Map.get reg.data dst) in
let mask = BV8.lsl (BV8.of_int 1) bit in
assert { BV8.nth (BV8.of_int 1) 0 /\ forall b. 0 < b < 8 -> not BV8.nth (BV8.of_int 1) b };
assert { forall w, b, v. 0 <= b < 8 -> BV8.eq (bitset w b v) (bitsetx w b v) };
if ?tf = 0 then
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.bw_and rd (BV8.bw_not mask)))
else
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.bw_or rd mask))
*)
(*
let bld_incorrect (dst: register) (bit: int): unit
writes { reg }
requires { 0 <= bit < 8 }
ensures { let mask = BV8.lsl (BV8.of_int ?tf) bit in
ensures { let mask = BV8.lsl (BV8.of_int ?tf) bit in
let prev = BV8.of_int (old reg)[dst] in
reg = (old reg)[dst <- BV8.t'int (BV8.bw_or (BV8.bw_and prev (BV8.bw_not mask)) mask)] }
= let mask = BV8.lsl (BV8.of_int ?tf) bit in
= let mask = BV8.lsl (BV8.of_int ?tf) bit in
let prev = BV8.of_int (Map.get reg.data dst) in
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.bw_or (BV8.bw_and prev (BV8.bw_not mask)) mask))
let bld_xor_incorrect (dst: register) (bit: int): unit
writes { reg }
requires { 0 <= bit < 8 }
ensures { let mask = BV8.lsl (BV8.of_int ?tf) bit in
ensures { let mask = BV8.lsl (BV8.of_int ?tf) bit in
let prev = BV8.of_int (old reg)[dst] in
let upd = if BV8.nth prev bit = tf.value then prev else BV8.bw_xor prev mask in
reg = (old reg)[dst <- BV8.t'int upd] }
......@@ -567,24 +444,1435 @@ let bld_xor_incorrect (dst: register) (bit: int): unit
reg.data <- Map.set reg.data dst (BV8.t'int (BV8.bw_or rd mask))
*)
let rec ghost uint_recursion (reg: address_space) (lo w: int): unit
requires { w >= 0 }
ensures { B.sum (reg,lo) 1 w = 256*B.sum (reg,lo+1) 0 (w-1) }
variant { w }
= assert { forall k. 0 <= k < w-1 -> get_uint_term (reg,lo) (k+1) = 256*get_uint_term (reg,lo+1) k };
if w > 0 then begin
uint_recursion reg lo (w-1)
end
end
let rec ghost uint_bound (reg: address_space) (lo w: int): unit
requires { w >= 0 }
ensures { 0 <= B.sum (reg,lo) 0 w < pow2 (8*w) }
variant { w }
= if w > 0 then begin
uint_recursion reg lo w;
assert { B.sum (reg,lo) 0 w = reg[lo] + 256*B.sum (reg,lo+1) 0 (w-1) };
uint_bound reg (lo+1) (w-1);
end
theory Validation
use import int.Int
use import bv.BV8
use import AVRint
lemma one_def:
BV8.nth (BV8.of_int 1) 0 /\ forall b. 0 < b < 8 -> not BV8.nth (BV8.of_int 1) b
goal bitset_correct1:
forall w, b, v. 0 <= b < 8 ->
BV8.nth (bitset w b v) b = v
goal bitset_correct2:
forall w, b i, v. 0 <= b < 8 -> 0 <= i < 8 -> i <> b ->
BV8.nth (bitset w b v) i = BV8.nth w i
goal bitset_equiv_def:
forall w, b, v. 0 <= b < 8 -> BV8.eq (bitset w b v) (bitset' w b v)
goal bitsetx_equiv_def:
forall w, b, v. 0 <= b < 8 -> BV8.eq (bitset w b v) (bitsetx w b v)
end
module AVRint_limit
use import int.Int
use import int.EuclideanDivision
use import ref.Ref
use import map.Map
use import bv.Pow2int
(***** FORMAL MODEL OF AVR ******)
type register = int
constant r0: register = 0
constant r1: register = 1
constant r2: register = 2
constant r3: register = 3
constant r4: register = 4
constant r5: register = 5
constant r6: register = 6
constant r7: register = 7
constant r8: register = 8
constant r9: register = 9
constant r10: register = 10
constant r11: register = 11
constant r12: register = 12
constant r13: register = 13
constant r14: register = 14
constant r15: register = 15
constant r16: register = 16
constant r17: register = 17
constant r18: register = 18
constant r19: register = 19
constant r20: register = 20
constant r21: register = 21
constant r22: register = 22
constant r23: register = 23
constant r24: register = 24
constant r25: register = 25
constant r26: register = 26
constant r27: register = 27
constant r28: register = 28
constant r29: register = 29
constant r30: register = 30
constant r31: register = 31
type cpu_flag = { mutable value: bool }
function (?) (x: cpu_flag): int = if x.value then 1 else 0
let (?) (x: cpu_flag) ensures { result = ?x } = if x.value then 1 else 0
val cf: cpu_flag
type address_space = { mutable data: map int int }
invariant { forall i. 0 <= self.data[i] < 256 }
(*
invariant { (forall i. 0 <= self.data[i] < 256) && (forall i j. 0 <= self.data[i]*self.data[j] <= 255*255) }
*)
function ([]) (r: address_space) (i: register): int = Map.get r.data i
function ([<-]) (r: address_space) (i: register) (v: int): address_space
= { data = Map.set r.data i v }
function get_uint_term (rlo: (address_space, int)) (i: int): int
= let (reg, lo) = rlo in pow2 (8*i) * reg[lo+i]
clone sum.Sum as B with type container = (address_space, int), function f = get_uint_term
function uint (w: int) (reg: address_space) (lo: register): int
= B.sum (reg,lo) 0 w
val reg: address_space
let mov (dst src: register): unit
writes { reg }
ensures { reg = old reg[dst<-reg[src]] }
= reg.data <- Map.set reg.data dst (Map.get reg.data src)
let movw (dst src: register): unit
writes { reg }
ensures { reg = old reg[dst<-reg[src]][dst+1<-reg[src+1]] }
= reg.data <- Map.set (Map.set reg.data dst (Map.get reg.data src)) (dst+1) (Map.get reg.data (src+1))
let mul (dst src: register): unit
writes { cf }
writes { reg }
ensures { let p = old (reg[src]*reg[dst]) in reg = (old reg)[0 <- mod p 256][1 <- div p 256] }
ensures { let p = old (reg[src]*reg[dst]) in ?cf = div p (pow2 15) }
(* ensures { reg[1] < 255 } *)
= let prod = Map.get reg.data dst*Map.get reg.data src in
reg.data <- Map.set (Map.set reg.data 0 (mod prod 256)) 1 (div prod 256);
cf.value <- (div prod (pow2 15) <> 0);
()
let add (dst src: register): unit
writes { cf }
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] + reg[src])) 256] }
ensures { ?cf = div (old (reg[dst] + reg[src])) 256 }
= let sum = Map.get reg.data src + Map.get reg.data dst in
let r1 = (Map.get reg.data dst) in
let r2 = (Map.get reg.data src) in
reg.data <- Map.set reg.data dst (mod sum 256);
let res = (Map.get reg.data dst) in
cf.value <- (r1 >= 128 && r2 >= 128 || r1 >= 128 && res < 128 || r2 >= 128 && res < 128)
let adc (dst src: register): unit
writes { cf }
reads { cf }
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] + reg[src] + ?cf)) 256] }
ensures { ?cf = div (old (reg[dst] + reg[src] + ?cf)) 256 }
= let sum = Map.get reg.data src + Map.get reg.data dst + ?cf in
reg.data <- Map.set reg.data dst (mod sum 256);
cf.value <- (div sum 256 <> 0);
()
let sub (dst src: register): unit
writes { cf }
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] - reg[src])) 256] }
ensures { ?cf = -div (old (reg[dst] - reg[src])) 256 }
= let sum = Map.get reg.data dst - Map.get reg.data src in
reg.data <- Map.set reg.data dst (mod sum 256);
assert { -255 <= sum <= 255 };
cf.value <- (-div sum 256 <> 0);
()
let sbc (dst src: register): unit
writes { cf }
reads { cf }
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] - reg[src] - ?cf)) 256] }
ensures { ?cf = -div (old (reg[dst] - reg[src] - ?cf)) 256 }
= let sum = Map.get reg.data dst - Map.get reg.data src - ?cf in
reg.data <- Map.set reg.data dst (mod sum 256);
cf.value <- (-div sum 256 <> 0);
()
constant rX: register = 26
constant rY: register = 28
constant rZ: register = 30
val mem: address_space
constant ram_begin: int
constant ram_end: int
(* TODO mem and reg overlap *)
(* TODO memory wrap around *)
let ld_inc (dst src: register): unit
writes { reg }
reads { mem }
requires { ram_begin <= uint 2 reg src < ram_end-1 }
requires { uint 2 reg src < pow2 16-1 }
requires { dst <> src /\ dst <> src+1 }
ensures { let cur = uint 2 (old reg) src in
let inc = cur+1 in
reg = (old reg)[dst <- mem[cur]][src <- mod inc 256][src+1 <- div inc 256] }
= let cur = Map.get reg.data src + 256*Map.get reg.data (src+1) in
let nxt = mod (cur+1) (pow2 16) in
reg.data <- Map.set (Map.set (Map.set reg.data dst (Map.get mem.data cur)) src (mod nxt 256)) (src+1) (div nxt 256)
let ldd (dst src ofs: register): unit
writes { reg }
reads { mem }
requires { ram_begin <= uint 2 reg src + ofs < ram_end }
ensures { let cur = uint 2 (old reg) src in
reg = (old reg)[dst <- mem[cur+ofs]] }
= let cur = Map.get reg.data src + 256*Map.get reg.data (src+1) in
reg.data <- Map.set reg.data dst (Map.get mem.data (cur+ofs))
let std (dst ofs src: register): unit
writes { mem }
reads { reg }
requires { ram_begin <= uint 2 reg dst + ofs < ram_end }
ensures { let cur = uint 2 (old reg) dst in
mem = (old mem)[cur+ofs <- reg[src]] }
= let cur = Map.get reg.data dst + 256*Map.get reg.data (dst+1) in
mem.data <- Map.set mem.data (cur+ofs) (Map.get reg.data src)
let nop (): unit
= ()
let sbci (dst: register) (k: int): unit
requires { 0 <= k <= 255 }
writes { cf }
reads { cf }
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] - k - ?cf)) 256] }
ensures { ?cf = -div (old (reg[dst] - k - ?cf)) 256 }
= let sum = Map.get reg.data dst - k - ?cf in
reg.data <- Map.set reg.data dst (mod sum 256);
cf.value <- (-div sum 256 <> 0);
()
(****** REASONING ABOUT MACHINE STATE *)
predicate eq (w: int) (reg reg': address_space) (lo: int)
= forall i. lo <= i < lo+w -> reg[i] = reg'[i]
goal eq_narrow:
forall reg reg', lo lo' w w'. lo <= lo' -> lo'+w' <= lo+w -> eq w reg reg' lo -> eq w' reg reg' lo'
goal eq_combine:
forall reg reg', lo lo' w w'. eq w reg reg' lo -> eq w' reg reg' lo' -> lo' = lo+w -> eq (w+w') reg reg' lo
goal eq_uint:
forall reg reg', lo w. eq w reg reg' lo -> uint w reg lo = uint w reg' lo
lemma uint_0:
forall reg, lo. B.sum (reg,lo) 0 0 = 0
lemma uint_1:
forall reg, lo. B.sum (reg,lo) 0 1 = reg[lo]
lemma uint_2:
forall reg, lo. B.sum (reg,lo) 0 2 = reg[lo] + pow2 8*reg[lo+1]
lemma uint_3:
forall reg, lo. B.sum (reg,lo) 0 3 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2]
lemma uint_4:
forall reg, lo. B.sum (reg,lo) 0 4 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3]
lemma uint_5:
forall reg, lo. B.sum (reg,lo) 0 5 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4]
lemma uint_6:
forall reg, lo. B.sum (reg,lo) 0 6 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5]