Commit 5286c418 authored by Jonathan Moerman's avatar Jonathan Moerman
Browse files

Prove 2 of the problems and fix a weird postcondition

parent 42292a0a
......@@ -650,10 +650,10 @@ let bld (dst: register) (bit: int): unit
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
reg.data <- data_set reg.data dst (bv8_to_int (BV8.bw_and rd (BV8.bw_not mask)))
else
if !tf then
reg.data <- data_set reg.data dst (bv8_to_int (BV8.bw_or rd mask))
else
reg.data <- data_set reg.data dst (bv8_to_int (BV8.bw_and rd (BV8.bw_not mask)))
(*
let bld' (dst: register) (bit: int): unit
......
......@@ -11,6 +11,7 @@ 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
lemma xor_1': forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) (of_int 0xFF)) = 255 - w
lemma or_0: forall w. bw_or zeros w = w
......@@ -440,17 +441,23 @@ end;
S.init();
begin
ensures { S.synchronized S.shadow reg }
ensures { uint 6 reg 20 + pow2 48*uint 2 reg 2 = ?cf*(pow2 64 - 1) + (if ?tf = 0 then -1 else 1)*old(uint 6 reg 20 + pow2 48*uint 2 reg 2) }
ensures { let cor = reg[26] + (pow2 8+pow2 16+pow2 24)*reg[0] in cor = old ?cf - ?cf \/ cor = pow2 32 + old ?cf - ?cf }
ensures { uint 6 reg 20 + pow2 48*uint 2 reg 2 = ?cf*(pow2 64 - 1) + (if !tf then 1 else -1)*old(uint 6 reg 20 + pow2 48*uint 2 reg 2) }
ensures { let cor = reg[26] + (pow2 8+pow2 16+pow2 24)*reg[0] in cor = (old ?cf) - ?cf \/ cor = pow2 32 + (old ?cf) - ?cf }
(*
ensures { let cor = reg[26] + (pow2 8+pow2 16+pow2 24)*reg[0] in cor = (old ?cf) - ?cf + (if ?cf > old ?cf then pow2 32 else 0) }
*)
ensures { valid_addr_space reg }
ensures { valid_addr_space mem }
ensures { valid_addr_space stack }
(* process sign bit *)
label B in
assert { reg[27] = 0 };
bld r27 0;
dec 27;
assert { reg[27] = 0xFF*(1 - ?tf) };
assert { reg[27] = 0xFF*(1 - ?tf) by mod (- 1) 256 = 0xFF };
(* merge carry and borrow *)
adc r26 r27;
......@@ -460,13 +467,21 @@ assert { reg[27] = 0xFF*(1 - ?tf) };
label B in
(* invert all bits or do nothing *)
eor r20 r27;
assert {(reg[20] = reg[20] at B /\ reg[27] = 0) \/ (reg[20] = 255 - reg[20] at B /\ reg[27] = 0xFF)};
eor r21 r27;
assert {(reg[21] = reg[21] at B /\ reg[27] = 0) \/ (reg[21] = 255 - reg[21] at B /\ reg[27] = 0xFF)};
eor r22 r27;
assert {(reg[22] = reg[22] at B /\ reg[27] = 0) \/ (reg[22] = 255 - reg[22] at B /\ reg[27] = 0xFF)};
eor r23 r27;
assert {(reg[23] = reg[23] at B /\ reg[27] = 0) \/ (reg[23] = 255 - reg[23] at B /\ reg[27] = 0xFF)};
eor r24 r27;
assert {(reg[24] = reg[24] at B /\ reg[27] = 0) \/ (reg[24] = 255 - reg[24] at B /\ reg[27] = 0xFF)};
eor r25 r27;
assert {(reg[25] = reg[25] at B /\ reg[27] = 0) \/ (reg[25] = 255 - reg[25] at B /\ reg[27] = 0xFF)};
eor r2 r27;
assert {(reg[2] = reg[2] at B /\ reg[27] = 0) \/ (reg[2] = 255 - reg[2] at B /\ reg[27] = 0xFF)};
eor r3 r27;
assert {(reg[3] = reg[3] at B /\ reg[27] = 0) \/ (reg[3] = 255 - reg[3] at B /\ reg[27] = 0xFF)};
label B in
add r27 r27; (* sets carry flag if r27 = 0xff *)
S.modify_r0(); S.modify_r26(); S.modify_r27();
......@@ -478,8 +493,6 @@ S.init();
begin ensures { S.synchronized S.shadow reg }
ensures { uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + pow2 96* ?cf = old(?cf + uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18 + uint 6 reg 20 + pow2 48*uint 2 reg 2 + pow2 64*(uint 1 reg 26 + (pow2 8+pow2 16+pow2 24)*reg[0])) }
ensures { valid_addr_space reg }
ensures { valid_addr_space mem }
ensures { valid_addr_space stack }
(* add in m *)
adc r10 r20;
......@@ -500,19 +513,14 @@ S.modify_r10(); S.modify_r11(); S.modify_r12(); S.modify_r13(); S.modify_r14();
S.modify_r28(); S.modify_r29(); S.modify_r18(); S.modify_r19();
end;
(* the checks will speed things up, but are not necessary *)
(*
check { 0 <= ((uint 4 reg 10) at L11) /\ 0 <= uint 8 reg 10 /\ 0 <= uint 2 reg 28 /\ 0 <= pow2 16*uint 2 reg 18 };
*)
assert { 0 <= ((uint 4 reg 10) at L11) + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 < pow2 128 };
assert { 0 <= ((uint 4 reg 2 + pow2 32*uint 4 reg 18) at L11) <= pow2 64-1 };
assert { 0 <= ((uint 4 reg 6 + pow2 32*uint 4 reg 22) at L11) <= pow2 64-1 };
assert { 0 <= ((((uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22))) at L11) <= (pow2 64-1)*(pow2 64-1) };
(*
check {
assert {
((uint 4 reg 10) at L11) + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18 + ?cf * pow2 128 =
((( (uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )) at L11)
\/
......@@ -521,11 +529,11 @@ check {
+ pow2 128
};
check { ((uint 4 reg 10) at L11) + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18
assert { ((uint 4 reg 10) at L11) + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18
= ((( (uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )) at L11)
};
*)
label Pre in
std rZ 4 r10;
std rZ 5 r11;
std rZ 6 r12;
......@@ -538,6 +546,21 @@ check { ((uint 4 reg 10) at L11) + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg
std rZ 13 r29;
std rZ 14 r18;
std rZ 15 r19;
assert { uint 12 mem (uint 2 reg rZ+4) = (uint 8 reg 10 + pow2 64*uint 2 reg 28 + pow2 80*uint 2 reg 18) at Pre
};
assert { ((uint 4 reg 10) at L11) + pow2 32*uint 8 reg 10 + pow2 96*uint 2 reg 28 + pow2 112*uint 2 reg 18
= uint 16 mem (uint 2 reg rZ)
};
assert { uint 16 mem (uint 2 reg rZ) =
((( (uint 4 reg 2 + pow2 32*uint 4 reg 18)*(uint 4 reg 6 + pow2 32*uint 4 reg 22) )) at L11) =
old (uint 8 mem (uint 2 reg rX) * uint 8 mem (uint 2 reg rY))
};
assert { uint 16 mem (old (uint 2 reg rZ)) =
old (uint 8 mem (uint 2 reg rX) * uint 8 mem (uint 2 reg rY))
by uint 2 reg rZ = old(uint 2 reg rZ)
};
()
end
This diff is collapsed.
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