Commit 7193c010 authored by Jonathan Moerman's avatar Jonathan Moerman
Browse files

Fix schoolbookl.mlw (assembly code is currently still to prove for why3)

parent b21bc8b9
...@@ -10,38 +10,38 @@ use bv.Pow2int ...@@ -10,38 +10,38 @@ use bv.Pow2int
type register = int type register = int
constant r0: register = 0 let constant r0: register = 0
constant r1: register = 1 let constant r1: register = 1
constant r2: register = 2 let constant r2: register = 2
constant r3: register = 3 let constant r3: register = 3
constant r4: register = 4 let constant r4: register = 4
constant r5: register = 5 let constant r5: register = 5
constant r6: register = 6 let constant r6: register = 6
constant r7: register = 7 let constant r7: register = 7
constant r8: register = 8 let constant r8: register = 8
constant r9: register = 9 let constant r9: register = 9
constant r10: register = 10 let constant r10: register = 10
constant r11: register = 11 let constant r11: register = 11
constant r12: register = 12 let constant r12: register = 12
constant r13: register = 13 let constant r13: register = 13
constant r14: register = 14 let constant r14: register = 14
constant r15: register = 15 let constant r15: register = 15
constant r16: register = 16 let constant r16: register = 16
constant r17: register = 17 let constant r17: register = 17
constant r18: register = 18 let constant r18: register = 18
constant r19: register = 19 let constant r19: register = 19
constant r20: register = 20 let constant r20: register = 20
constant r21: register = 21 let constant r21: register = 21
constant r22: register = 22 let constant r22: register = 22
constant r23: register = 23 let constant r23: register = 23
constant r24: register = 24 let constant r24: register = 24
constant r25: register = 25 let constant r25: register = 25
constant r26: register = 26 let constant r26: register = 26
constant r27: register = 27 let constant r27: register = 27
constant r28: register = 28 let constant r28: register = 28
constant r29: register = 29 let constant r29: register = 29
constant r30: register = 30 let constant r30: register = 30
constant r31: register = 31 let constant r31: register = 31
type cpu_flag = { mutable value: bool } type cpu_flag = { mutable value: bool }
...@@ -205,9 +205,9 @@ let dec (dst: register): unit ...@@ -205,9 +205,9 @@ let dec (dst: register): unit
= let sum = Map.get reg.data dst - 1 in = let sum = Map.get reg.data dst - 1 in
reg.data <- data_set reg.data dst (mod sum 256) reg.data <- data_set reg.data dst (mod sum 256)
constant rX: register = 26 let constant rX: register = 26
constant rY: register = 28 let constant rY: register = 28
constant rZ: register = 30 let constant rZ: register = 30
val mem: address_space val mem: address_space
......
module BV_asr_Lemmas module BV_asr_Lemmas
use import bv.BV8 use bv.BV8
use import int.Int use int.Int
use import bv.Pow2int use bv.Pow2int
use import int.EuclideanDivision use int.EuclideanDivision
lemma asr_0: eq (asr zeros 1) zeros lemma asr_0: (asr zeros 1) = zeros
lemma asr_1: eq (asr (of_int 1) 1) zeros lemma asr_1: (asr (of_int 1) 1) = zeros
lemma asr_f: eq (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
...@@ -21,10 +21,10 @@ end ...@@ -21,10 +21,10 @@ end
module AvrModelLemmas module AvrModelLemmas
use import int.Int use int.Int
use import map.Map use map.Map
use import int.EuclideanDivision use int.EuclideanDivision
use import bv.Pow2int use bv.Pow2int
lemma register_file_invariant_strengthen: 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) forall m: map int int. (forall i. 0 <= m[i] < 256) -> (forall i j. 0 <= m[i]*m[j] <= 255*255)
...@@ -35,13 +35,13 @@ end ...@@ -35,13 +35,13 @@ end
module KaratAvr module KaratAvr
use import avrmodel.AVRint use int.Int
use import int.Int use int.EuclideanDivision
use import int.EuclideanDivision use bv.Pow2int
use import bv.Pow2int use AvrModelLemmas
use import AvrModelLemmas
use BV_asr_Lemmas use BV_asr_Lemmas
use bv.BV8 use bv.BV8
use avrmodel.AVRint
let mul16 (): unit let mul16 (): unit
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) }
...@@ -173,11 +173,11 @@ let mul32_flat(): unit ...@@ -173,11 +173,11 @@ let mul32_flat(): unit
let mul40(): unit let mul40(): unit
ensures { uint 10 reg 12 = old (uint 5 reg 2 * uint 5 reg 7) } ensures { uint 10 reg 12 = old (uint 5 reg 2 * uint 5 reg 7) }
= 'S: = label S in
abstract begin
ensures { uint 10 reg 12 = old(uint 3 reg 2*uint 5 reg 7) } ensures { uint 10 reg 12 = old(uint 3 reg 2*uint 5 reg 7) }
ensures { eq 5 reg (at reg 'S) 2 } ensures { eq 5 reg (reg at S) 2 }
ensures { eq 5 reg (at reg 'S) 7 } ensures { eq 5 reg (reg at S) 7 }
ensures { reg[20] = 0 /\ reg[21] = 0 } ensures { reg[20] = 0 /\ reg[21] = 0 }
clr r18; clr r18;
clr r19; clr r19;
...@@ -235,13 +235,13 @@ ensures { reg[20] = 0 /\ reg[21] = 0 } ...@@ -235,13 +235,13 @@ ensures { reg[20] = 0 /\ reg[21] = 0 }
adc r18 r1; adc r18 r1;
adc r19 r21; adc r19 r21;
end; end;
abstract begin
ensures { uint 7 reg 15 = old(uint 7 reg 15 + uint 2 reg 5*uint 5 reg 7) } ensures { uint 7 reg 15 = old(uint 7 reg 15 + uint 2 reg 5*uint 5 reg 7) }
(*ensures { uint 10 reg 12 = old(uint 10 reg 12 + pow2 24*uint 2 reg 5*uint 5 reg 7) }*) (*ensures { uint 10 reg 12 = old(uint 10 reg 12 + pow2 24*uint 2 reg 5*uint 5 reg 7) }*)
ensures { eq 3 reg (old reg) 12 } ensures { eq 3 reg (old reg) 12 }
ensures { eq 5 reg (at reg 'S) 2 } ensures { eq 5 reg (reg at S) 2 }
ensures { eq 5 reg (at reg 'S) 7 } ensures { eq 5 reg (reg at S) 7 }
'B: label B in
(* ? check { uint 10 reg 12 < pow2 64 -> uint 7 reg 15 < pow2 40 }; *) (* ? check { uint 10 reg 12 < pow2 64 -> uint 7 reg 15 < pow2 40 }; *)
mul r5 r9; mul r5 r9;
movw r24 r0; movw r24 r0;
...@@ -286,7 +286,7 @@ end ...@@ -286,7 +286,7 @@ end
let mul40_flat(): unit let mul40_flat(): unit
ensures { uint 10 reg 12 = old (uint 5 reg 2 * uint 5 reg 7) } ensures { uint 10 reg 12 = old (uint 5 reg 2 * uint 5 reg 7) }
= 'S: = label S in
clr r18; clr r18;
clr r19; clr r19;
movw r20 r18; movw r20 r18;
...@@ -383,11 +383,11 @@ let mul40_flat(): unit ...@@ -383,11 +383,11 @@ let mul40_flat(): unit
let mul48 (): unit let mul48 (): unit
ensures { uint 12 reg 14 = old (uint 6 reg 2 * uint 6 reg 8) } ensures { uint 12 reg 14 = old (uint 6 reg 2 * uint 6 reg 8) }
= 'S: = label S in
abstract begin
ensures { uint 12 reg 14 = at(uint 3 reg 2*uint 6 reg 8)'S } ensures { uint 12 reg 14 = (uint 3 reg 2*uint 6 reg 8) at S }
ensures { eq 6 reg (at reg 'S) 2 } ensures { eq 6 reg (reg at S) 2 }
ensures { eq 6 reg (at reg 'S) 8 } ensures { eq 6 reg (reg at S) 8 }
ensures { reg[23] = 0 /\ reg[24] = 0 /\ reg[25] = 0 } ensures { reg[23] = 0 /\ reg[24] = 0 /\ reg[25] = 0 }
clr r20; clr r20;
clr r21; clr r21;
...@@ -457,12 +457,12 @@ ensures { reg[23] = 0 /\ reg[24] = 0 /\ reg[25] = 0 } ...@@ -457,12 +457,12 @@ ensures { reg[23] = 0 /\ reg[24] = 0 /\ reg[25] = 0 }
adc r21 r0; adc r21 r0;
adc r22 r1; adc r22 r1;
end; end;
abstract begin
ensures { uint 9 reg 17 = old(uint 9 reg 17 + uint 3 reg 5*uint 6 reg 8) } 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 3 reg (old reg) 14 }
ensures { eq 6 reg (at reg 'S) 2 } ensures { eq 6 reg (reg at S) 2 }
ensures { eq 6 reg (at reg 'S) 8 } ensures { eq 6 reg (reg at S) 8 }
'B: label B in
mul r5 r10; mul r5 r10;
movw r26 r0; movw r26 r0;
mul r5 r8; mul r5 r8;
...@@ -536,7 +536,7 @@ end ...@@ -536,7 +536,7 @@ end
let mul48_flat (): unit let mul48_flat (): unit
ensures { uint 12 reg 14 = old (uint 6 reg 2 * uint 6 reg 8) } ensures { uint 12 reg 14 = old (uint 6 reg 2 * uint 6 reg 8) }
= 'S: = label S in
clr r20; clr r20;
clr r21; clr r21;
movw r22 r20; movw r22 r20;
......
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