Skip to content
GitLab
Commit a7386507 authored by Jonathan Moerman's avatar Jonathan Moerman
Browse files

Merge branch 'newversion' into 'master' 

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

See merge request jmoerman/why3-avr!1
parents d7201cfe 0c61c50b
Hide whitespace changes
Inline Side-by-side
avrmodel.mlw
View file @ a7386507
......@@ -5,6 +5,7 @@ use int.EuclideanDivision
use ref.Ref
use map.Map
use bv.Pow2int
use export map.Map
(***** FORMAL MODEL OF AVR ******)
......@@ -51,32 +52,38 @@ 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
*)
(*WIP: invariant is disabled for now*)
(*
let lemma address_space_exists (): map int int
ensures { forall x. 0 <= result x < 256 }
= fun x -> 0
type address_space = { mutable data: map int int }
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
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}
meta coercion function data
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
= let (reg, lo) = rlo in pow2 (8*i) * reg[lo+i]
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 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 }
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
......@@ -84,8 +91,15 @@ function uint (w: int) (reg: address_space) (lo: register): int
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 }
= any map int int ensures { result = Map.set d i v }
let mov (dst src: register): unit
writes { reg }
......@@ -100,7 +114,7 @@ let mul (dst src: register): unit
(* ensures { reg[1] < 255 } *)
= 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);
cf.value <- (div prod (pow2 15) <> 0);
cf.value <- (div prod 0x8000 <> 0);
()
let add (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] }
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
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)
let ldd (dst src ofs: register): unit
......@@ -268,7 +282,6 @@ let pop (dst: register): unit
let nop (): unit
= ()
(****** REASONING ABOUT MACHINE STATE *)
predicate eq (w: int) (reg reg': address_space) (lo: int)
......@@ -428,7 +441,7 @@ 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)
(*
......@@ -499,6 +512,15 @@ let lsr (dst: register): unit
= 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))
(* 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
writes { reg, cf }
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
(* otherwise Z3 is needed *)
assert { 256*pow2 (8*(w-1)) = pow2 (8*w) };
end
end
module Shadow
......
schoolbook.mlw
View file @ a7386507
......@@ -5,9 +5,9 @@ use int.Int
use bv.Pow2int
use int.EuclideanDivision
lemma asr_0: (asr zeros 1) = zeros
lemma asr_1: (asr (of_int 1) 1) = zeros
lemma asr_f: (asr ones 1) = ones
lemma asr_0: (asr zeros 1) == zeros
lemma asr_1: (asr (of_int 1) 1) == zeros
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_1: forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) ones) = 255 - w
......@@ -38,74 +38,111 @@ module KaratAvr
use int.Int
use int.EuclideanDivision
use bv.Pow2int
use avrmodel.AVRint
use AvrModelLemmas
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
requires { forall i. 0 <= reg[i] < 256 }
ensures { uint 4 reg 12 = old(uint 2 reg 2 * uint 2 reg 7) }
=
clr r23;
label Before in
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;
check { reg[14] + reg[15]*256 = (reg[3]*reg[8]) at Before };
mul r2 r7;
movw r12 r0;
check { reg[12] + reg[13]*256 = (reg[2]*reg[7]) at Before };
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;
adc r14 r1;
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;
check { reg[0] + reg[1]*256 = reg[3]*reg[7] };
add r13 r0;
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
requires { forall i. 0 <= reg[i] < 256 }
ensures { uint 6 reg 12 = old (uint 3 reg 2 * uint 3 reg 7) }
=
clr r23;
mul r2 r9;
movw r14 r0;
clr r23; check { forall i. 0 <= reg[i] < 256 };
mul r2 r9; check { forall i. 0 <= reg[i] < 256 };
movw r14 r0; check { forall i. 0 <= reg[i] < 256 };
mul r2 r7;
movw r12 r0;
mul r2 r7; check { forall i. 0 <= reg[i] < 256 };
movw r12 r0; check { forall i. 0 <= reg[i] < 256 };
mul r2 r8;
add r13 r0;
adc r14 r1;
adc r15 r23;
mul r2 r8; check { forall i. 0 <= reg[i] < 256 };
add r13 r0; check { forall i. 0 <= reg[i] < 256 };
adc r14 r1; check { forall i. 0 <= reg[i] < 256 };
adc r15 r23; check { forall i. 0 <= reg[i] < 256 };
clr r16;
mul r3 r9;
movw r24 r0;
clr r16; check { forall i. 0 <= reg[i] < 256 };
mul r3 r9; check { forall i. 0 <= reg[i] < 256 };
movw r24 r0; check { forall i. 0 <= reg[i] < 256 };
mul r3 r7;
add r13 r0;
adc r14 r1;
adc r15 r24;
adc r25 r23;
mul r3 r7; check { forall i. 0 <= reg[i] < 256 };
add r13 r0; check { forall i. 0 <= reg[i] < 256 };
adc r14 r1; check { forall i. 0 <= reg[i] < 256 };
adc r15 r24; check { forall i. 0 <= reg[i] < 256 };
adc r25 r23; check { forall i. 0 <= reg[i] < 256 };
mul r3 r8;
add r14 r0;
adc r15 r1;
adc r16 r25;
mul r3 r8; check { forall i. 0 <= reg[i] < 256 };
add r14 r0; check { forall i. 0 <= reg[i] < 256 };
adc r15 r1; check { forall i. 0 <= reg[i] < 256 };
adc r16 r25; check { forall i. 0 <= reg[i] < 256 };
clr r17;
mul r4 r9;
movw r24 r0;
clr r17; check { forall i. 0 <= reg[i] < 256 };
mul r4 r9; check { forall i. 0 <= reg[i] < 256 };
movw r24 r0; check { forall i. 0 <= reg[i] < 256 };
mul r4 r7;
add r14 r0;
adc r15 r1;
adc r16 r24;
adc r25 r23;
mul r4 r7; check { forall i. 0 <= reg[i] < 256 };
add r14 r0; check { forall i. 0 <= reg[i] < 256 };
adc r15 r1; check { forall i. 0 <= reg[i] < 256 };
adc r16 r24; check { forall i. 0 <= reg[i] < 256 };
adc r25 r23; check { forall i. 0 <= reg[i] < 256 };
mul r4 r8;
add r15 r0;
adc r16 r1;
adc r17 r25
mul r4 r8; check { forall i. 0 <= reg[i] < 256 };
add r15 r0; check { forall i. 0 <= reg[i] < 256 };
adc r16 r1; check { forall i. 0 <= reg[i] < 256 };
adc r17 r25; check { forall i. 0 <= reg[i] < 256 }
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) }
=
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