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

a version based on range types; this produces larger smt2 input but seems to...

a version based on range types; this produces larger smt2 input but seems to perform quite okay on schoolbook
parent a7386507
module AVRbyte
use int.Int
use int.EuclideanDivision
use ref.Ref
use map.Map
use bv.Pow2int
use export map.Map
(***** FORMAL MODEL OF AVR ******)
type register = int
let constant r0: register = 0
let constant r1: register = 1
let constant r2: register = 2
let constant r3: register = 3
let constant r4: register = 4
let constant r5: register = 5
let constant r6: register = 6
let constant r7: register = 7
let constant r8: register = 8
let constant r9: register = 9
let constant r10: register = 10
let constant r11: register = 11
let constant r12: register = 12
let constant r13: register = 13
let constant r14: register = 14
let constant r15: register = 15
let constant r16: register = 16
let constant r17: register = 17
let constant r18: register = 18
let constant r19: register = 19
let constant r20: register = 20
let constant r21: register = 21
let constant r22: register = 22
let constant r23: register = 23
let constant r24: register = 24
let constant r25: register = 25
let constant r26: register = 26
let constant r27: register = 27
let constant r28: register = 28
let constant r29: register = 29
let constant r30: register = 30
let 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 byte = < range 0 255 >
meta coercion function byte'int
type address_space = { mutable data: map int byte }
meta coercion function data
function get_uint_term (rlo: (address_space, int)) (i: int): int
= let (reg, lo) = rlo in pow2 (8*i) * (reg.data[lo+i])
let rec ghost function uint_sum (rlo: (address_space, int)) (i: int) (j: int) : int =
variant { j - i }
if i >= j then 0 else get_uint_term rlo i + uint_sum rlo (i+1) j
(* TODO: we probably don't need to clone this anymore; the above definition is more elegant *)
type container = (address_space, int)
clone sum.Sum as B with type container = container, function f = get_uint_term, function sum = uint_sum
function uint (w: int) (reg: address_space) (lo: register): int
= uint_sum (reg,lo) 0 w
let ghost function ($_) (x: int): byte
requires { 0 <= x < 256 }
ensures { result = x }
= for i = (0:byte) to (255:byte) do
invariant { x >= i }
if pure{i = x} then return i
done;
absurd
(* WIP COMMENT: i'm not sure if this is beneficial for the proof context *)
let ghost function lo8 (x: int): byte
ensures { result = mod x 256 }
= $mod x 256
let ghost function hi8 (x: int): byte
requires { 0 <= x < 0x10000 }
ensures { result = div x 256 }
= $div x 256
val reg: address_space
(* WIP COMMENT: in why3 1.x, the "ghost" vs "non-ghost" distinction seems to be converging towards
the notion of "not computable" and "computable"; however, we can still use non-computable stuff
in non-ghost code by conjuring it into existence using the 'any' expression. in Why3 1.x, this is
safe (a witness must be provided), whereas in Why3 0.8x it would not be safe.
this comment can be removed at any time.*)
let data_set (m: map int byte) (i: register) (v: int): map int byte
requires { 0 <= v < 256 }
ensures { result = Map.set m i ($v) }
= let v' = any byte ensures { result = v } in
any map int byte ensures { result = Map.set m i v' }
let read (m: address_space) (i: int): int
= any int ensures { m[i] = result }
let mov (dst src: register): unit
writes { reg }
ensures { reg = old reg[dst<-reg[src]] }
= reg.data <- data_set reg.data dst (read reg src)
(* WIP: mul,add,adc,made abstract for now; other instructions disabled *)
val mul (dst src: register): unit
writes { cf }
writes { reg }
ensures { let p = old (reg[src]*reg[dst]) in reg = (old reg)[0 <- lo8 p][1 <- hi8 p] }
ensures { let p = old (reg[src]*reg[dst]) in ?cf = div p (pow2 15) }
(* ensures { reg[1] < 255 } *)
(*
= let prod = read reg dst*read reg src in
reg.data <- data_set (data_set reg.data 0 (mod prod 256)) 1 (div prod 256);
cf.value <- (div prod 0x8000 <> 0);
()
*)
let add (dst src: register): unit
writes { cf }
writes { reg }
ensures { reg = old reg[dst <- lo8 (old (reg[dst] + reg[src]))] }
ensures { ?cf = div (old (reg[dst] + reg[src])) 256 }
= let sum = read reg src + read reg dst in
let r1 = (read reg dst) in
let r2 = (read reg src) in
reg.data <- data_set reg.data dst (mod sum 256);
let res = (read reg dst) in
if r1 >= 128 && r2 >= 128 ||
r1 >= 128 && res < 128 ||
r2 >= 128 && res < 128
then
cf.value <- True
else
cf.value <- False
let adc (dst src: register): unit
writes { cf }
reads { cf }
writes { reg }
ensures { reg = old reg[dst <- lo8 (old (reg[dst] + reg[src] + ?cf))] }
ensures { ?cf = div (old (reg[dst] + reg[src] + ?cf)) 256 }
= let sum = read reg src + read reg dst + ?cf in
reg.data <- data_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 <- lo8 (old (reg[dst] - reg[src]))] }
ensures { ?cf = -div (old (reg[dst] - reg[src])) 256 }
= let sum = read reg dst - read reg src in
reg.data <- data_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 <- lo8 (old (reg[dst] - reg[src] - ?cf))] }
ensures { ?cf = -div (old (reg[dst] - reg[src] - ?cf)) 256 }
= let sum = read reg dst - read reg src - ?cf in
reg.data <- data_set reg.data dst (mod sum 256);
cf.value <- (-div sum 256 <> 0);
()
let neg (dst: register): unit
writes { cf }
writes { reg }
ensures { reg = old reg[dst <- lo8 (old (-reg[dst]))] }
(* TODO: which one is useful?
ensures { ?cf = if reg[dst] = 0 then 0 else 1 }
ensures { ?cf = -div (old (-reg[dst])) 256 }
*)
= let sum = - read reg dst in
reg.data <- data_set reg.data dst (mod sum 256);
assert { -255 <= sum <= 255 };
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 <- lo8 (old (reg[dst] - k))] }
ensures { ?cf = -div (old (reg[dst] - k)) 256 }
= let sum = read reg dst - k in
reg.data <- data_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 <- lo8 (old (reg[dst] - k - ?cf))] }
ensures { ?cf = -div (old (reg[dst] - k - ?cf)) 256 }
= let sum = read reg dst - k - ?cf in
reg.data <- data_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 }
ensures { reg = old reg[dst <- lo8 (old (reg[dst] + 1))] }
= let sum = read reg dst + 1 in
reg.data <- data_set reg.data dst (mod sum 256)
let dec (dst: register): unit
writes { reg }
ensures { reg = old reg[dst <- lo8 (old (reg[dst] - 1))] }
= let sum = read reg dst - 1 in
reg.data <- data_set reg.data dst (mod sum 256)
let constant rX: register = 26
let constant rY: register = 28
let constant rZ: register = 30
val mem: address_space
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 <- lo8 inc][src+1 <- hi8 inc] }
ensures { uint 2 reg src = old(uint 2 reg src)+1 }
= let cur = read reg src + 256*read reg (src+1) in
let nxt = mod (cur+1) 0x10000 in
reg.data <- data_set (data_set (data_set reg.data dst (read mem cur)) src (mod nxt 256)) (src+1) (div nxt 256)
let ldd (dst src ofs: register): unit
writes { reg }
reads { mem }
requires { 32 <= uint 2 reg src + ofs < pow2 16 }
ensures { let cur = uint 2 (old reg) src in
reg = (old reg)[dst <- mem[cur+ofs]] }
= let cur = read reg src + 256*read reg (src+1) in
reg.data <- data_set reg.data dst (read mem (cur+ofs))
let std (dst ofs src: register): unit
writes { mem }
reads { reg }
requires { 32 <= uint 2 reg dst + ofs < pow2 16 }
ensures { let cur = uint 2 (old reg) dst in
mem = (old mem)[cur+ofs <- reg[src]] }
= let cur = read reg dst + 256*read reg (dst+1) in
mem.data <- data_set mem.data (cur+ofs) (read reg 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 <- data_set stack.data (!stack_pointer) (read reg 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 <- data_set reg.data dst (read stack !stack_pointer)
let nop (): unit
= ()
(****** 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. uint_sum (reg,lo) 0 0 = 0
lemma uint_1:
forall reg, lo. uint_sum (reg,lo) 0 1 = reg[lo]
meta rewrite lemma uint_1
lemma uint_2:
forall reg, lo. uint_sum (reg,lo) 0 2 = reg[lo] + pow2 8*reg[lo+1]
meta rewrite lemma uint_2
lemma uint_3:
forall reg, lo. uint_sum (reg,lo) 0 3 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2]
meta rewrite lemma uint_3
lemma uint_4:
forall reg, lo. uint_sum (reg,lo) 0 4 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3]
meta rewrite lemma uint_4
lemma uint_5:
forall reg, lo. uint_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]
meta rewrite lemma uint_5
lemma uint_6:
forall reg, lo. uint_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]
meta rewrite lemma uint_6
lemma uint_7:
forall reg, lo. uint_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 48*reg[lo+6]
meta rewrite lemma uint_7
lemma uint_8:
forall reg, lo. uint_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]
meta rewrite lemma uint_8
lemma uint_9:
forall reg, lo. uint_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]
meta rewrite lemma uint_9
lemma uint_10:
forall reg, lo. uint_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]
meta rewrite lemma uint_10
lemma uint_11:
forall reg, lo. uint_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]
meta rewrite lemma uint_11
lemma uint_12:
forall reg, lo. uint_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 lemma uint_12
lemma uint_13:
forall reg, lo. uint_sum (reg,lo) 0 13 = 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]
meta rewrite lemma uint_13
lemma uint_14:
forall reg, lo. uint_sum (reg,lo) 0 14 = 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]
meta rewrite lemma uint_14
lemma uint_15:
forall reg, lo. uint_sum (reg,lo) 0 15 = 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]
meta rewrite lemma uint_15
lemma uint_16:
forall reg, lo. uint_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 lemma uint_16
lemma uint_17:
forall reg, lo. uint_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 lemma uint_17
lemma uint_18:
forall reg, lo. uint_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 lemma uint_18
lemma uint_19:
forall reg, lo. uint_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 lemma uint_19
lemma uint_20:
forall reg, lo. uint_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 lemma uint_20
lemma uint_21:
forall reg, lo. uint_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 lemma uint_21
lemma uint_22:
forall reg, lo. uint_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 lemma uint_22
lemma uint_23:
forall reg, lo. uint_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 lemma uint_23
lemma uint_24:
forall reg, lo. uint_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 lemma uint_24
lemma uint_25:
forall reg, lo. uint_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 lemma uint_25
lemma uint_26:
forall reg, lo. uint_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 lemma uint_26
lemma uint_27:
forall reg, lo. uint_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 lemma uint_27
lemma uint_28:
forall reg, lo. uint_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 lemma uint_28
lemma uint_29:
forall reg, lo. uint_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 lemma uint_29
lemma uint_30:
forall reg, lo. uint_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 lemma uint_30
lemma uint_31:
forall reg, lo. uint_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 lemma uint_31
lemma uint_32:
forall reg, lo. uint_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 lemma 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 <- data_set (data_set reg.data dst (read reg src)) (dst+1) (read reg (src+1))
let adiw (dst: register) (k: int): unit
requires { 0 <= k < 64 }
(* TODO unnecessary
requires { dst = 24 \/ dst = 26 \/ dst = 28 \/ dst = 30 }
*)
writes { reg }
writes { cf }
ensures { reg = old reg[dst <- lo8 (old (reg[dst] + k))]
[dst+1 <- lo8 (old (reg[dst+1] + div (reg[dst] + k) 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 = read reg dst + 256*read reg (dst+1) +k in
reg.data <- data_set reg.data dst (mod sum 256);
assert { mod sum 256 = mod (old (reg[dst] + k)) 256 };
reg.data <- data_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 }
(* TODO unnecessary
requires { dst = 24 \/ dst = 26 \/ dst = 28 \/ dst = 30 }
*)
writes { reg }
writes { cf }
ensures { reg = old reg[dst <- lo8 (old (reg[dst] - k))]
[dst+1 <- lo8 (old (reg[dst+1] + div (reg[dst] - k) 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 ********************)
val clr (dst: register): unit
writes { reg }
ensures { reg = old reg[dst<-(0:byte)] }
(* WIP TODO: this needs to be ported to 'byte' still
use bv.BV8
val bv8_to_int (x: BV8.t): int
ensures { result = BV8.t'int x }
axiom bv8_nth_def: forall x y. (256 > x >= 0 /\ 8 > y >= 0) -> (BV8.nth (BV8.of_int x) y <-> mod (div x (pow2 y)) 2 = 1)
(*
let add_ (dst src: register): unit
writes { reg, cf }
ensures { reg = old (reg[dst <- lo8 (reg[dst] + reg[src])]) }
ensures { ?cf = old (div (reg[dst] + reg[src]) 256) }
= let rd = BV8.of_int (read reg dst) in
let rr = BV8.of_int (read reg src) in
let rd' = BV8.add rd rr in
reg.data <- data_set reg.data dst (bv8_to_int rd');
cf.value <- (BV8.nth rd 7 && BV8.nth rr 7 || BV8.nth rd 7 && not BV8.nth rd' 7 || not BV8.nth rd' 7 && BV8.nth rr 7)
let sub_ (dst src: register): unit
writes { reg, cf }
ensures { reg = old reg[dst <- lo8 (old (reg[dst] - reg[src]))] }
ensures { ?cf = -div (old (reg[dst] - reg[src])) 256 }
= let rd = BV8.of_int (read reg dst) in
let rr = BV8.of_int (read reg src) in
let rd' = BV8.sub rd rr in
reg.data <- data_set reg.data dst (bv8_to_int rd');
cf.value <- (not BV8.nth rd 7 && BV8.nth rr 7 || BV8.nth rr 7 && BV8.nth rd' 7 || BV8.nth rd' 7 && not BV8.nth rd 7)
*)
let inc_ (dst: register): unit
writes { reg }
ensures { reg = old reg[dst <- lo8 (old (reg[dst] + 1))] }
= let rd = BV8.of_int (read reg dst) in
let rd' = BV8.add rd (BV8.of_int 1) in
reg.data <- data_set reg.data dst (bv8_to_int rd')
let dec_ (dst: register): unit
writes { reg }
ensures { reg = old reg[dst <- lo8 (old (reg[dst] - 1))] }
= let sum = read reg dst - 1 in
reg.data <- data_set reg.data dst (mod sum 256)
let eor (dst src: register): unit
writes { reg }
ensures { reg = old reg[dst <- BV8.t'int (BV8.bw_xor (BV8.of_int reg[dst]) (BV8.of_int reg[src])) ] }
= let tmp = bv8_to_int (BV8.bw_xor (BV8.of_int (readb reg dst)) (BV8.of_int (readb reg src))) in
reg.data <- data_set reg.data dst tmp
let clr (dst: register): unit
writes { reg }
ensures { reg = old reg[dst<-0] }
= eor dst dst
let com (dst: register): unit
writes { reg }
ensures { reg = old reg[dst<- BV8.t'int (BV8.bw_not (BV8.of_int reg[dst]))] }
= let tmp = bv8_to_int (BV8.bw_not (BV8.of_int (read reg dst))) in
reg.data <- data_set reg.data dst tmp
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 (read reg dst)) 0;
reg.data <- data_set reg.data dst (bv8_to_int (BV8.asr (BV8.of_int (read reg dst)) 1))
let lsr (dst: register): unit
writes { reg, cf }
ensures { reg = old reg[dst<- BV8.t'int (BV8.lsr (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 (read reg dst)) 0;
reg.data <- data_set reg.data dst (bv8_to_int (BV8.lsr (BV8.of_int (read reg dst)) 1))
(* WIP: this will become the future definition, since 'lsl rX' is the same opcode as 'add rX, rX' *)
(*
let lsl (dst: register): unit
writes { reg, cf }
ensures { reg = old reg[dst <- lo8 (old (2*reg[dst]))] }
ensures { ?cf = div (old (2*reg[dst])) 256 }
= add dst dst
*)
let lsl (dst: register): unit
writes { reg, cf }
ensures { reg = old reg[dst<- BV8.t'int (BV8.lsl (BV8.of_int reg[dst]) 1)] }
ensures { ?cf = 0 <-> old reg[dst] < 128 }
ensures { cf.value = BV8.nth (BV8.of_int (old reg[dst])) 7 }
= cf.value <- BV8.nth (BV8.of_int (read reg dst)) 7;
reg.data <- data_set reg.data dst (bv8_to_int (BV8.lsl (BV8.of_int (read reg dst)) 1))
(* t flag operations *)
val tf: cpu_flag
let bst (dst: register) (bit: int): unit
writes { tf }
requires { 0 <= bit < 8 }
ensures { tf.value = BV8.nth (BV8.of_int reg[dst]) bit }
= tf.value <- BV8.nth (BV8.of_int (read reg dst)) bit
function bitset (w: BV8.t) (b: int) (v: bool): BV8.t =
let mask = BV8.lsl (BV8.of_int 1) b in
if v then
BV8.bw_or w mask
else
BV8.bw_and w (BV8.bw_not mask)
function bitset' (w: BV8.t) (b: int) (v: bool): BV8.t =
let v' = BV8.of_int (if v then 1 else 0) in
let one = BV8.of_int 1 in
BV8.bw_or (BV8.bw_and w (BV8.bw_not (BV8.lsl one b))) (BV8.lsl v' b)
function bitsetx (w: BV8.t) (b: int) (v: bool): BV8.t =
let mask = BV8.lsl (BV8.of_int 1) b in
if BV8.nth w b = v then
w
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 -> (bitset w b v) = (bitset' w b v)
goal bitsetx_equiv_def:
forall w, b, v. 0 <= b < 8 -> (bitset w b v) = (bitsetx w b v)
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 (read reg dst) in
let mask = BV8.lsl (BV8.of_int 1) bit in
if ?tf = 0 then
reg.data <- data_set reg.data dst (bv8_to_int (BV8.bw_and rd (BV8.bw_not mask)))
else
reg.data <- data_set reg.data dst (bv8_to_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 (read reg dst) in
let mask = BV8.lsl (BV8.of_int 1) bit in
if ?tf = 0 then
reg.data <- data_set reg.data dst (BV8.t'int (BV8.bw_and rd (BV8.bw_not mask)))
else
reg.data <- data_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 (bitsetx (BV8.of_int (old reg)[dst]) bit tf.value)] }
= let rd = BV8.of_int (read reg dst) in
let mask = BV8.lsl (BV8.of_int 1) bit in
if ?tf = 0 then
reg.data <- data_set reg.data dst (BV8.t'int (BV8.bw_and rd (BV8.bw_not mask)))
else
reg.data <- data_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 { uint_sum (reg,lo) 1 w = 256*uint_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
let rec ghost uint_bound (reg: address_space) (lo w: int): unit
requires { w >= 0 }
ensures { 0 <= uint_sum (reg,lo) 0 w < pow2 (8*w) }
variant { w }
= if w > 0 then begin
uint_recursion reg lo w;
assert { uint_sum (reg,lo) 0 w = reg[lo] + 256*uint_sum (reg,lo+1) 0 (w-1) };
uint_bound reg (lo+1) (w-1);
(* otherwise Z3 is needed *)
assert { 256*pow2 (8*(w-1)) = pow2 (8*w) };
end
*)
end
module Shadow
use int.Int
use ref.Ref
use import AVRbyte as AVR
use map.Map
type shadow_registers = {