Commit 0c61c50b authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

added a coercion; disabled the type invariant; other minor changes

parent d7201cfe
...@@ -5,6 +5,7 @@ use int.EuclideanDivision ...@@ -5,6 +5,7 @@ use int.EuclideanDivision
use ref.Ref use ref.Ref
use map.Map use map.Map
use bv.Pow2int use bv.Pow2int
use export map.Map
(***** FORMAL MODEL OF AVR ******) (***** FORMAL MODEL OF AVR ******)
...@@ -51,32 +52,38 @@ let (?) (x: cpu_flag) ensures { result = ?x } = if x.value then 1 else 0 ...@@ -51,32 +52,38 @@ let (?) (x: cpu_flag) ensures { result = ?x } = if x.value then 1 else 0
val cf: cpu_flag val cf: cpu_flag
(*
type byte = < range 0 255 >
meta coercion function byte'int
*)
(*WIP: invariant is disabled for now*)
(*
let lemma address_space_exists (): map int int let lemma address_space_exists (): map int int
ensures { forall x. 0 <= result x < 256 } ensures { forall x. 0 <= result x < 256 }
= fun x -> 0 = fun x -> 0
type address_space = { mutable data: map int int } type address_space = { mutable data: map int int }
invariant { forall i. 0 <= data[i] < 256 } invariant { forall i. 0 <= data[i] < 256 }
*)
type address_space = { mutable data: map int int }
axiom addr_space_eq: forall x y: address_space. x.data = y.data <-> x = y meta coercion function data
let function ([]) (r: address_space) (i: register): int = Map.get r.data i
let ghost function ([<-]) (r: address_space) (i: register) (v: int): address_space
requires { 0 <= v < 256 }
= { data = Map.set r.data i v }
val pow2 (x: int): int
ensures {result = pow2 x}
type container = (address_space, int) (* WIP: only needed in case we have an invariant *)
goal address_space_eq:
forall m1 m2. m1.data = m2.data <-> m1 = m2
let function get_uint_term (rlo: (address_space, int)) (i: int): int function get_uint_term (rlo: (address_space, int)) (i: int): int
= let (reg, lo) = rlo in pow2 (8*i) * reg[lo+i] = let (reg, lo) = rlo in pow2 (8*i) * reg.data[lo+i]
let rec function uint_sum (rlo: (address_space, int)) (i: int) (j: int) : int = let rec ghost function uint_sum (rlo: (address_space, int)) (i: int) (j: int) : int =
variant { j - i } variant { j - i }
if i >= j then 0 else get_uint_term rlo i + uint_sum rlo (i+1) j 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 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 function uint (w: int) (reg: address_space) (lo: register): int
...@@ -84,8 +91,15 @@ function uint (w: int) (reg: address_space) (lo: register): int ...@@ -84,8 +91,15 @@ function uint (w: int) (reg: address_space) (lo: register): int
val reg: address_space val reg: address_space
val data_set (d: map int int) (i: register) (v: int): map int int (* 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 (d: map int int) (i: register) (v: int): map int int
ensures { result = Map.set d i v } ensures { result = Map.set d i v }
= any map int int ensures { result = Map.set d i v }
let mov (dst src: register): unit let mov (dst src: register): unit
writes { reg } writes { reg }
...@@ -100,7 +114,7 @@ let mul (dst src: register): unit ...@@ -100,7 +114,7 @@ let mul (dst src: register): unit
(* ensures { reg[1] < 255 } *) (* ensures { reg[1] < 255 } *)
= let prod = Map.get reg.data dst*Map.get reg.data src in = let prod = Map.get reg.data dst*Map.get reg.data src in
reg.data <- data_set (data_set reg.data 0 (mod prod 256)) 1 (div prod 256); reg.data <- data_set (data_set reg.data 0 (mod prod 256)) 1 (div prod 256);
cf.value <- (div prod (pow2 15) <> 0); cf.value <- (div prod 0x8000 <> 0);
() ()
let add (dst src: register): unit let add (dst src: register): unit
...@@ -223,7 +237,7 @@ let ld_inc (dst src: register): unit ...@@ -223,7 +237,7 @@ let ld_inc (dst src: register): unit
reg = (old reg)[dst <- mem[cur]][src <- mod inc 256][src+1 <- div inc 256] } 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 } 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 cur = Map.get reg.data src + 256*Map.get reg.data (src+1) in
let nxt = mod (cur+1) (pow2 16) in let nxt = mod (cur+1) 0x10000 in
reg.data <- data_set (data_set (data_set reg.data dst (Map.get mem.data cur)) src (mod nxt 256)) (src+1) (div nxt 256) reg.data <- data_set (data_set (data_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 let ldd (dst src ofs: register): unit
...@@ -268,7 +282,6 @@ let pop (dst: register): unit ...@@ -268,7 +282,6 @@ let pop (dst: register): unit
let nop (): unit let nop (): unit
= () = ()
(****** REASONING ABOUT MACHINE STATE *) (****** REASONING ABOUT MACHINE STATE *)
predicate eq (w: int) (reg reg': address_space) (lo: int) predicate eq (w: int) (reg reg': address_space) (lo: int)
...@@ -428,7 +441,7 @@ use bv.BV8 ...@@ -428,7 +441,7 @@ use bv.BV8
val bv8_to_int (x: BV8.t): int val bv8_to_int (x: BV8.t): int
ensures { result = BV8.t'int x } 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) 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)
(* (*
...@@ -499,6 +512,15 @@ let lsr (dst: register): unit ...@@ -499,6 +512,15 @@ let lsr (dst: register): unit
= cf.value <- BV8.nth (BV8.of_int (Map.get reg.data dst)) 0; = cf.value <- BV8.nth (BV8.of_int (Map.get reg.data dst)) 0;
reg.data <- data_set reg.data dst (bv8_to_int (BV8.lsr (BV8.of_int (Map.get reg.data dst)) 1)) reg.data <- data_set reg.data dst (bv8_to_int (BV8.lsr (BV8.of_int (Map.get reg.data 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 <- mod (old (2*reg[dst])) 256] }
ensures { ?cf = div (old (2*reg[dst])) 256 }
= add dst dst
*)
let lsl (dst: register): unit let lsl (dst: register): unit
writes { reg, cf } writes { reg, cf }
ensures { reg = old reg[dst<- BV8.t'int (BV8.lsl (BV8.of_int reg[dst]) 1)] } ensures { reg = old reg[dst<- BV8.t'int (BV8.lsl (BV8.of_int reg[dst]) 1)] }
...@@ -607,7 +629,6 @@ let rec ghost uint_bound (reg: address_space) (lo w: int): unit ...@@ -607,7 +629,6 @@ let rec ghost uint_bound (reg: address_space) (lo w: int): unit
(* otherwise Z3 is needed *) (* otherwise Z3 is needed *)
assert { 256*pow2 (8*(w-1)) = pow2 (8*w) }; assert { 256*pow2 (8*(w-1)) = pow2 (8*w) };
end end
end end
module Shadow module Shadow
......
...@@ -5,9 +5,9 @@ use int.Int ...@@ -5,9 +5,9 @@ use int.Int
use bv.Pow2int use bv.Pow2int
use int.EuclideanDivision use int.EuclideanDivision
lemma asr_0: (asr zeros 1) = zeros lemma asr_0: (asr zeros 1) == zeros
lemma asr_1: (asr (of_int 1) 1) = zeros lemma asr_1: (asr (of_int 1) 1) == zeros
lemma asr_f: (asr ones 1) = ones lemma asr_f: (asr ones 1) == ones
lemma xor_0: forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) zeros) = w lemma xor_0: forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) zeros) = w
lemma xor_1: forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) ones) = 255 - w lemma xor_1: forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) ones) = 255 - w
...@@ -38,74 +38,111 @@ module KaratAvr ...@@ -38,74 +38,111 @@ module KaratAvr
use int.Int use int.Int
use int.EuclideanDivision use int.EuclideanDivision
use bv.Pow2int use bv.Pow2int
use avrmodel.AVRint
use AvrModelLemmas use AvrModelLemmas
use BV_asr_Lemmas use BV_asr_Lemmas
use bv.BV8
use avrmodel.AVRint
let mul8 (): unit
ensures { uint 2 reg 12 = old(uint 1 reg 3 * uint 1 reg 8) }
= mul r3 r8;
movw r12 r0
(* WIP: i've left the checks in for possible future debugging, for now *)
let mul16 (): unit let mul16 (): unit
requires { forall i. 0 <= reg[i] < 256 }
ensures { uint 4 reg 12 = old(uint 2 reg 2 * uint 2 reg 7) } ensures { uint 4 reg 12 = old(uint 2 reg 2 * uint 2 reg 7) }
= =
clr r23; clr r23;
label Before in
mul r3 r8; mul r3 r8;
check { reg[0] = mod ((reg[8]*reg[3]) at Before) 256 };
check { reg[1] = div ((reg[8]*reg[3]) at Before) 256 };
check { reg[0] + reg[1]*256 = (reg[3]*reg[8]) at Before };
movw r14 r0; movw r14 r0;
check { reg[14] + reg[15]*256 = (reg[3]*reg[8]) at Before };
mul r2 r7; mul r2 r7;
movw r12 r0; movw r12 r0;
check { reg[12] + reg[13]*256 = (reg[2]*reg[7]) at Before };
mul r2 r8; mul r2 r8;
check { reg[0] + reg[1]*256 = (reg[2]*reg[8]) at Before };
label B in
check { reg[23] = 0 };
add r13 r0; add r13 r0;
adc r14 r1; adc r14 r1;
adc r15 r23; adc r15 r23;
check { uint 3 reg 13 + ?cf*pow2 24 = uint 3 reg 13 at B + uint 2 reg 0 at B = uint 3 reg 13 at B + (reg[2]*reg[8]) at B };
check { uint 4 reg 12 + ?cf*pow2 32 = uint 4 reg 12 at B + pow2 8*uint 2 reg 0 at B = uint 4 reg 12 at B + pow2 8*(reg[2]*reg[8]) at B };
check { uint 4 reg 12 + ?cf*pow2 32 = (pow2 16*reg[3]*reg[8]+reg[2]*reg[7]+pow2 8*reg[2]*reg[8]) at Before };
(*
begin ensures { ?cf = 0 }
assert { forall i. 0 <= reg[i] < 256 };
assert { reg[3]*reg[8] <= 255*255 by 0 <= reg[3] <= 255 /\ 0 <= reg[8] <= 255 };
assert { 0 <= uint 4 reg 12 + ?cf*pow2 32 = (pow2 16*reg[3]*reg[8]+reg[2]*reg[7]+pow2 8*reg[2]*reg[8]) at Before < pow2 32 };
assert { 0 <= uint 4 reg 12 + ?cf*pow2 32 < pow2 32 };
end;
*)
mul r3 r7; mul r3 r7;
check { reg[0] + reg[1]*256 = reg[3]*reg[7] };
add r13 r0; add r13 r0;
adc r14 r1; adc r14 r1;
adc r15 r23 adc r15 r23;
(*
begin ensures { ?cf = 0 }
assert { 0 <= uint 4 reg 12 + ?cf*pow2 32 = (uint 2 reg 2 * uint 2 reg 7) at Before < pow2 32 };
end
*) ()
(* NOTE: by changing (some of) the checks into asserts, we can test the impact on performance
of having vs. not having an explicit mention of the 8bit-ness of the AVR architecture in the proof context.
in the polished version, these checks should probably take place elsewhere (e.g. in avrmodel.mlw) *)
let mul24_flat (): unit let mul24_flat (): unit
requires { forall i. 0 <= reg[i] < 256 }
ensures { uint 6 reg 12 = old (uint 3 reg 2 * uint 3 reg 7) } ensures { uint 6 reg 12 = old (uint 3 reg 2 * uint 3 reg 7) }
= =
clr r23; clr r23; check { forall i. 0 <= reg[i] < 256 };
mul r2 r9; mul r2 r9; check { forall i. 0 <= reg[i] < 256 };
movw r14 r0; movw r14 r0; check { forall i. 0 <= reg[i] < 256 };
mul r2 r7; mul r2 r7; check { forall i. 0 <= reg[i] < 256 };
movw r12 r0; movw r12 r0; check { forall i. 0 <= reg[i] < 256 };
mul r2 r8; mul r2 r8; check { forall i. 0 <= reg[i] < 256 };
add r13 r0; add r13 r0; check { forall i. 0 <= reg[i] < 256 };
adc r14 r1; adc r14 r1; check { forall i. 0 <= reg[i] < 256 };
adc r15 r23; adc r15 r23; check { forall i. 0 <= reg[i] < 256 };
clr r16; clr r16; check { forall i. 0 <= reg[i] < 256 };
mul r3 r9; mul r3 r9; check { forall i. 0 <= reg[i] < 256 };
movw r24 r0; movw r24 r0; check { forall i. 0 <= reg[i] < 256 };
mul r3 r7; mul r3 r7; check { forall i. 0 <= reg[i] < 256 };
add r13 r0; add r13 r0; check { forall i. 0 <= reg[i] < 256 };
adc r14 r1; adc r14 r1; check { forall i. 0 <= reg[i] < 256 };
adc r15 r24; adc r15 r24; check { forall i. 0 <= reg[i] < 256 };
adc r25 r23; adc r25 r23; check { forall i. 0 <= reg[i] < 256 };
mul r3 r8; mul r3 r8; check { forall i. 0 <= reg[i] < 256 };
add r14 r0; add r14 r0; check { forall i. 0 <= reg[i] < 256 };
adc r15 r1; adc r15 r1; check { forall i. 0 <= reg[i] < 256 };
adc r16 r25; adc r16 r25; check { forall i. 0 <= reg[i] < 256 };
clr r17; clr r17; check { forall i. 0 <= reg[i] < 256 };
mul r4 r9; mul r4 r9; check { forall i. 0 <= reg[i] < 256 };
movw r24 r0; movw r24 r0; check { forall i. 0 <= reg[i] < 256 };
mul r4 r7; mul r4 r7; check { forall i. 0 <= reg[i] < 256 };
add r14 r0; add r14 r0; check { forall i. 0 <= reg[i] < 256 };
adc r15 r1; adc r15 r1; check { forall i. 0 <= reg[i] < 256 };
adc r16 r24; adc r16 r24; check { forall i. 0 <= reg[i] < 256 };
adc r25 r23; adc r25 r23; check { forall i. 0 <= reg[i] < 256 };
mul r4 r8; mul r4 r8; check { forall i. 0 <= reg[i] < 256 };
add r15 r0; add r15 r0; check { forall i. 0 <= reg[i] < 256 };
adc r16 r1; adc r16 r1; check { forall i. 0 <= reg[i] < 256 };
adc r17 r25 adc r17 r25; check { forall i. 0 <= reg[i] < 256 }
let mul32_flat(): unit let mul32_flat(): unit
requires { forall i. 0 <= reg[i] < 256 }
ensures { uint 8 reg 12 = old (uint 4 reg 2 * uint 4 reg 7) } ensures { uint 8 reg 12 = old (uint 4 reg 2 * uint 4 reg 7) }
= =
clr r23; clr r23;
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment