Commit fd2acc75 authored by Jonathan Moerman's avatar Jonathan Moerman
Browse files

Why3's interface hates me for this, but we seem to be at 0.88 parity now

parent 996cae87
This diff is collapsed.
This diff is collapsed.
No preview for this file type
......@@ -44,11 +44,11 @@ let constant r29: register = 29
let constant r30: register = 30
let constant r31: register = 31
type cpu_flag = { mutable value: bool }
type cpu_flag = ref bool
function (?) (x: cpu_flag): int = if x.value then 1 else 0
function (?) (x: cpu_flag): int = if !x then 1 else 0
let (?) (x: cpu_flag) ensures { result = ?x } = if x.value then 1 else 0
let (?) (x: cpu_flag) ensures { result = ?x } = if !x then 1 else 0
meta rewrite_def function (?)
......@@ -95,6 +95,9 @@ let ghost function hi8 (x: int): byte
ensures { result = div x 256 }
= $div x 256
meta rewrite_def function lo8
meta rewrite_def function hi8
val reg: address_space
(* WIP COMMENT: in why3 1.x, the "ghost" vs "non-ghost" distinction seems to be converging towards
......@@ -133,7 +136,7 @@ let mul (dst src: register): unit
(* 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);
cf := (div prod 0x8000 <> 0);
()
let add (dst src: register): unit
......@@ -150,9 +153,9 @@ let add (dst src: register): unit
r1 >= 128 && res < 128 ||
r2 >= 128 && res < 128
then
cf.value <- True
cf := True
else
cf.value <- False
cf := False
let adc (dst src: register): unit
writes { cf }
......@@ -162,7 +165,7 @@ let adc (dst src: register): unit
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);
cf := (div sum 256 <> 0);
()
let sub (dst src: register): unit
......@@ -173,7 +176,7 @@ let sub (dst src: register): unit
= 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);
cf := (-div sum 256 <> 0);
()
let sbc (dst src: register): unit
......@@ -184,7 +187,7 @@ let sbc (dst src: register): unit
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);
cf := (-div sum 256 <> 0);
()
let neg (dst: register): unit
......@@ -198,7 +201,7 @@ let neg (dst: register): unit
= 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);
cf := (-div sum 256 <> 0);
()
(* immediate versions *)
......@@ -210,7 +213,7 @@ let subi (dst: register) (k: int): unit
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);
cf := (-div sum 256 <> 0);
()
let sbci (dst: register) (k: int): unit
......@@ -222,7 +225,7 @@ let sbci (dst: register) (k: int): unit
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);
cf := (-div sum 256 <> 0);
()
(* these instructions do not modify the carry flag *)
......@@ -437,7 +440,7 @@ let adiw (dst: register) (k: int): unit
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)
cf := (sum > 65535)
let sbiw (dst: register) (k: int): unit
......@@ -477,6 +480,7 @@ let add_ (dst src: register): unit
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
......@@ -487,6 +491,7 @@ let sub_ (dst src: register): unit
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)
*)
......@@ -524,16 +529,16 @@ 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;
ensures { !cf = BV8.nth (BV8.of_int (old reg[dst])) 0 }
= cf := 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;
ensures { !cf = BV8.nth (BV8.of_int (old reg[dst])) 0 }
= cf := 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' *)
......@@ -549,8 +554,8 @@ 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;
ensures { !cf = BV8.nth (BV8.of_int (old reg[dst])) 7 }
= cf := 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 *)
......@@ -559,8 +564,8 @@ 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
ensures { !tf = BV8.nth (BV8.of_int reg[dst]) bit }
= tf := 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
......@@ -601,7 +606,7 @@ goal bitsetx_equiv_def:
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)] }
ensures { reg = (old reg)[dst <- BV8.t'int (bitset (BV8.of_int (old reg)[dst]) bit !tf)] }
= let rd = BV8.of_int (read reg dst) in
let mask = BV8.lsl (BV8.of_int 1) bit in
if ?tf = 0 then
......@@ -613,7 +618,7 @@ let bld (dst: register) (bit: int): unit
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)] }
ensures { reg = (old reg)[dst <- BV8.t'int (bitset' (BV8.of_int (old reg)[dst]) bit !tf)] }
= let rd = BV8.of_int (read reg dst) in
let mask = BV8.lsl (BV8.of_int 1) bit in
if ?tf = 0 then
......@@ -624,7 +629,7 @@ let bld' (dst: register) (bit: int): unit
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)] }
ensures { reg = (old reg)[dst <- BV8.t'int (bitsetx (BV8.of_int (old reg)[dst]) bit !tf)] }
= let rd = BV8.of_int (read reg dst) in
let mask = BV8.lsl (BV8.of_int 1) bit in
if ?tf = 0 then
......
......@@ -26,10 +26,8 @@ use map.Map
use int.EuclideanDivision
use bv.Pow2int
(*
lemma register_file_invariant_strengthen:
forall m: map int int. (forall i. 0 <= m[i] < 256) -> (forall i j. 0 <= m[i]*m[j] <= 255*255)
*)
lemma pow_split: forall k. k >= 0 -> pow2 (2*k) = pow2 k*pow2 k
......@@ -40,21 +38,24 @@ module KaratAvr
use int.Int
use int.EuclideanDivision
use bv.Pow2int
use avrmodel_alt.AVRbyte
use avrmodel.AVRint
use AvrModelLemmas
use BV_asr_Lemmas
(*WIP: this replaces the above in case avrmodel_rng is used *)
lemma register_file_invariant_strengthen:
forall m: map int byte. (forall i j. 0 <= m[i]*m[j] <= 255*255)
(*
axiom addr_contains_bytes: forall reg:address_space. forall i. 0 <= reg[i] < 256
*)
let mul8 (): unit
requires { valid_addr_space reg }
ensures { valid_addr_space reg }
ensures { uint 2 reg 12 = old(uint 1 reg 3 * uint 1 reg 8) }
= mul r3 r8;
movw r12 r0
let mul16 (): unit
requires { forall i. 0 <= reg[i] < 256 }
requires { valid_addr_space reg }
ensures { valid_addr_space reg }
ensures { uint 4 reg 12 = old(uint 2 reg 2 * uint 2 reg 7) }
=
clr r23;
......@@ -76,53 +77,55 @@ let mul16 (): unit
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 }
requires { valid_addr_space reg }
ensures { valid_addr_space reg }
ensures { uint 6 reg 12 = old (uint 3 reg 2 * uint 3 reg 7) }
=
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; check { forall i. 0 <= reg[i] < 256 };
movw r12 r0; check { forall i. 0 <= reg[i] < 256 };
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; 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; 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; 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; 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; 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; 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 }
clr r23;
mul r2 r9;
movw r14 r0;
mul r2 r7;
movw r12 r0;
mul r2 r8;
add r13 r0;
adc r14 r1;
adc r15 r23;
clr r16;
mul r3 r9;
movw r24 r0;
mul r3 r7;
add r13 r0;
adc r14 r1;
adc r15 r24;
adc r25 r23;
mul r3 r8;
add r14 r0;
adc r15 r1;
adc r16 r25;
clr r17;
mul r4 r9;
movw r24 r0;
mul r4 r7;
add r14 r0;
adc r15 r1;
adc r16 r24;
adc r25 r23;
mul r4 r8;
add r15 r0;
adc r16 r1;
adc r17 r25
let mul32_flat(): unit
requires { forall i. 0 <= reg[i] < 256 }
requires { valid_addr_space reg }
ensures { valid_addr_space reg }
ensures { uint 8 reg 12 = old (uint 4 reg 2 * uint 4 reg 7) }
=
clr r23;
......@@ -189,6 +192,8 @@ let mul32_flat(): unit
adc r19 r23
let mul40(): unit
requires { valid_addr_space reg }
ensures { valid_addr_space reg }
ensures { uint 10 reg 12 = old (uint 5 reg 2 * uint 5 reg 7) }
= label S in
begin
......@@ -196,6 +201,7 @@ ensures { uint 10 reg 12 = old(uint 3 reg 2*uint 5 reg 7) }
ensures { eq 5 reg (reg at S) 2 }
ensures { eq 5 reg (reg at S) 7 }
ensures { reg[20] = 0 /\ reg[21] = 0 }
ensures { valid_addr_space reg }
clr r18;
clr r19;
movw r20 r18;
......@@ -258,6 +264,7 @@ ensures { uint 7 reg 15 = old(uint 7 reg 15 + uint 2 reg 5*uint 5 reg 7) }
ensures { eq 3 reg (old reg) 12 }
ensures { eq 5 reg (reg at S) 2 }
ensures { eq 5 reg (reg at S) 7 }
ensures { valid_addr_space reg }
label B in
(* ? check { uint 10 reg 12 < pow2 64 -> uint 7 reg 15 < pow2 40 }; *)
mul r5 r9;
......@@ -302,6 +309,8 @@ label B in
end
let mul40_flat(): unit
requires { valid_addr_space reg }
ensures { valid_addr_space reg }
ensures { uint 10 reg 12 = old (uint 5 reg 2 * uint 5 reg 7) }
= label S in
clr r18;
......@@ -399,6 +408,8 @@ let mul40_flat(): unit
adc r21 r1
let mul48 (): unit
requires { valid_addr_space reg }
ensures { valid_addr_space reg }
ensures { uint 12 reg 14 = old (uint 6 reg 2 * uint 6 reg 8) }
= label S in
begin
......@@ -406,6 +417,7 @@ ensures { uint 12 reg 14 = (uint 3 reg 2*uint 6 reg 8) at S }
ensures { eq 6 reg (reg at S) 2 }
ensures { eq 6 reg (reg at S) 8 }
ensures { reg[23] = 0 /\ reg[24] = 0 /\ reg[25] = 0 }
ensures { valid_addr_space reg }
clr r20;
clr r21;
movw r22 r20;
......@@ -479,6 +491,7 @@ ensures { uint 9 reg 17 = old(uint 9 reg 17 + uint 3 reg 5*uint 6 reg 8) }
ensures { eq 3 reg (old reg) 14 }
ensures { eq 6 reg (reg at S) 2 }
ensures { eq 6 reg (reg at S) 8 }
ensures { valid_addr_space reg }
label B in
mul r5 r10;
movw r26 r0;
......@@ -552,6 +565,8 @@ label B in
end
let mul48_flat (): unit
requires { valid_addr_space reg }
ensures { valid_addr_space reg }
ensures { uint 12 reg 14 = old (uint 6 reg 2 * uint 6 reg 8) }
= label S in
clr r20;
......
This diff is collapsed.
No preview for this file type
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