Commit 5d08ecc9 authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

added markings to reduce the number of invariants/asserts needed

parent 402accd8
This diff is collapsed.
No preview for this file type
......@@ -107,7 +107,6 @@ let add (dst src: register): unit
else
cf.value <- False
let adc (dst src: register): unit
writes { cf }
reads { cf }
......@@ -141,6 +140,19 @@ let sbc (dst src: register): unit
cf.value <- (-div sum 256 <> 0);
()
(* these instructions do not modify the carry flag *)
let inc (dst: register): unit
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] + 1)) 256] }
= let sum = Map.get reg.data dst + 1 in
reg.data <- Map.set reg.data dst (mod sum 256)
let dec (dst: register): unit
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] - 1)) 256] }
= let sum = Map.get reg.data dst - 1 in
reg.data <- Map.set reg.data dst (mod sum 256)
constant rX: register = 26
constant rY: register = 28
constant rZ: register = 30
......@@ -204,6 +216,7 @@ goal eq_combine:
goal eq_uint:
forall reg reg', lo w. eq w reg reg' lo -> uint w reg lo = uint w reg' lo
(*
lemma uint_0:
forall reg, lo. B.sum (reg,lo) 0 0 = 0
lemma uint_1:
......@@ -243,6 +256,57 @@ meta rewrite prop uint_9
meta rewrite prop uint_10
meta rewrite prop uint_11
meta rewrite prop uint_12
*)
lemma uint_0:
forall reg, lo. B.sum (reg,lo) 0 0 = 0
lemma uint_1:
forall reg, lo. B.sum (reg,lo) 0 1 = reg[lo]
meta rewrite prop uint_1
lemma uint_2:
forall reg, lo. B.sum (reg,lo) 0 2 = reg[lo] + pow2 8*reg[lo+1]
meta rewrite prop uint_2
lemma uint_3:
forall reg, lo. B.sum (reg,lo) 0 3 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2]
meta rewrite prop uint_3
lemma uint_4:
forall reg, lo. B.sum (reg,lo) 0 4 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3]
meta rewrite prop uint_4
lemma uint_5:
forall reg, lo. B.sum (reg,lo) 0 5 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4]
meta rewrite prop uint_5
lemma uint_6:
forall reg, lo. B.sum (reg,lo) 0 6 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5]
meta rewrite prop uint_6
lemma uint_7:
forall reg, lo. B.sum (reg,lo) 0 7 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6]
meta rewrite prop uint_7
lemma uint_8:
forall reg, lo. B.sum (reg,lo) 0 8 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7]
meta rewrite prop uint_8
lemma uint_9:
forall reg, lo. B.sum (reg,lo) 0 9 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8]
meta rewrite prop uint_9
lemma uint_10:
forall reg, lo. B.sum (reg,lo) 0 10 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9]
meta rewrite prop uint_10
lemma uint_11:
forall reg, lo. B.sum (reg,lo) 0 11 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10]
meta rewrite prop uint_11
lemma uint_12:
forall reg, lo. B.sum (reg,lo) 0 12 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11]
meta rewrite prop uint_12
lemma uint_13:
forall reg, lo. B.sum (reg,lo) 0 13 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12]
meta rewrite prop uint_13
lemma uint_14:
forall reg, lo. B.sum (reg,lo) 0 14 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13]
meta rewrite prop uint_14
lemma uint_15:
forall reg, lo. B.sum (reg,lo) 0 15 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14]
meta rewrite prop uint_15
lemma uint_16:
forall reg, lo. B.sum (reg,lo) 0 16 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15]
meta rewrite prop uint_16
meta compute_max_steps 0x1000000
(*************** BITVECTOR IMPORTS ********************)
......@@ -263,6 +327,19 @@ let add_ (dst src: register): unit
else
cf.value <- False
let inc_ (dst: register): unit
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] + 1)) 256] }
= let rd = BV8.of_int (Map.get reg.data dst) in
let rd' = BV8.add rd (BV8.of_int 1) in
reg.data <- Map.set reg.data dst (BV8.to_uint rd')
let dec_ (dst: register): unit
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] - 1)) 256] }
= let sum = Map.get reg.data dst - 1 in
reg.data <- Map.set reg.data dst (mod sum 256)
let eor (dst src: register): unit
writes { reg }
ensures { reg = old reg[dst <- BV8.to_uint (BV8.bw_xor (BV8.of_int reg[dst]) (BV8.of_int reg[src])) ] }
......@@ -287,6 +364,121 @@ let asr (dst: register): unit
= cf.value <- BV8.nth (BV8.of_int (Map.get reg.data dst)) 0;
reg.data <- Map.set reg.data dst (BV8.to_uint (BV8.asr (BV8.of_int (Map.get reg.data dst)) 1))
(* t flag operations *)
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 (Map.get reg.data dst)) bit
function bitset (w: BV8.t) (b: int) (v: bool): BV8.t =
let mask = BV8.lsl (BV8.of_int 1) b in
if v then
BV8.bw_or w mask
else
BV8.bw_and w (BV8.bw_not mask)
function bitset' (w: BV8.t) (b: int) (v: bool): BV8.t =
let v' = BV8.of_int (if v then 1 else 0) in
let one = BV8.of_int 1 in
BV8.bw_or (BV8.bw_and w (BV8.bw_not (BV8.lsl one b))) (BV8.lsl v' b)
function bitsetx (w: BV8.t) (b: int) (v: bool): BV8.t =
let mask = BV8.lsl (BV8.of_int 1) b in
if BV8.nth w b = v then
w
else
BV8.bw_xor w mask
let bld (dst: register) (bit: int): unit
writes { reg }
requires { 0 <= bit < 8 }
ensures { reg = (old reg)[dst <- BV8.to_uint (bitset (BV8.of_int (old reg)[dst]) bit tf.value)] }
= let rd = BV8.of_int (Map.get reg.data dst) in
let mask = BV8.lsl (BV8.of_int 1) bit in
if ?tf = 0 then
reg.data <- Map.set reg.data dst (BV8.to_uint (BV8.bw_and rd (BV8.bw_not mask)))
else
reg.data <- Map.set reg.data dst (BV8.to_uint (BV8.bw_or rd mask))
let bld' (dst: register) (bit: int): unit
writes { reg }
requires { 0 <= bit < 8 }
ensures { reg = (old reg)[dst <- BV8.to_uint (bitset' (BV8.of_int (old reg)[dst]) bit tf.value)] }
= let rd = BV8.of_int (Map.get reg.data dst) in
let mask = BV8.lsl (BV8.of_int 1) bit in
assert { forall w, b, v. 0 <= b < 8 -> BV8.eq (bitset w b v) (bitset' w b v) };
if ?tf = 0 then
reg.data <- Map.set reg.data dst (BV8.to_uint (BV8.bw_and rd (BV8.bw_not mask)))
else
reg.data <- Map.set reg.data dst (BV8.to_uint (BV8.bw_or rd mask))
let bld'' (dst: register) (bit: int): unit
writes { reg }
requires { 0 <= bit < 8 }
ensures { reg = (old reg)[dst <- BV8.to_uint (bitsetx (BV8.of_int (old reg)[dst]) bit tf.value)] }
= let rd = BV8.of_int (Map.get reg.data dst) in
let mask = BV8.lsl (BV8.of_int 1) bit in
assert { BV8.nth (BV8.of_int 1) 0 /\ forall b. 0 < b < 8 -> not BV8.nth (BV8.of_int 1) b };
assert { forall w, b, v. 0 <= b < 8 -> BV8.eq (bitset w b v) (bitsetx w b v) };
if ?tf = 0 then
reg.data <- Map.set reg.data dst (BV8.to_uint (BV8.bw_and rd (BV8.bw_not mask)))
else
reg.data <- Map.set reg.data dst (BV8.to_uint (BV8.bw_or rd mask))
(*
let bld_incorrect (dst: register) (bit: int): unit
writes { reg }
requires { 0 <= bit < 8 }
ensures { let mask = BV8.lsl (BV8.of_int ?tf) bit in
let prev = BV8.of_int (old reg)[dst] in
reg = (old reg)[dst <- BV8.to_uint (BV8.bw_or (BV8.bw_and prev (BV8.bw_not mask)) mask)] }
= let mask = BV8.lsl (BV8.of_int ?tf) bit in
let prev = BV8.of_int (Map.get reg.data dst) in
reg.data <- Map.set reg.data dst (BV8.to_uint (BV8.bw_or (BV8.bw_and prev (BV8.bw_not mask)) mask))
let bld_xor_incorrect (dst: register) (bit: int): unit
writes { reg }
requires { 0 <= bit < 8 }
ensures { let mask = BV8.lsl (BV8.of_int ?tf) bit in
let prev = BV8.of_int (old reg)[dst] in
let upd = if BV8.nth prev bit = tf.value then prev else BV8.bw_xor prev mask in
reg = (old reg)[dst <- BV8.to_uint upd] }
= let rd = BV8.of_int (Map.get reg.data dst) in
let mask = BV8.lsl (BV8.of_int 1) bit in
if ?tf = 0 then
reg.data <- Map.set reg.data dst (BV8.to_uint (BV8.bw_and rd (BV8.bw_not mask)))
else
reg.data <- Map.set reg.data dst (BV8.to_uint (BV8.bw_or rd mask))
*)
end
theory Validation
use import int.Int
use import bv.BV8
use import AVRint
lemma one_def:
BV8.nth (BV8.of_int 1) 0 /\ forall b. 0 < b < 8 -> not BV8.nth (BV8.of_int 1) b
goal bitset_correct1:
forall w, b, v. 0 <= b < 8 ->
BV8.nth (bitset w b v) b = v
goal bitset_correct2:
forall w, b i, v. 0 <= b < 8 -> 0 <= i < 8 -> i <> b ->
BV8.nth (bitset w b v) i = BV8.nth w i
goal bitset_equiv_def:
forall w, b, v. 0 <= b < 8 -> BV8.eq (bitset w b v) (bitset' w b v)
goal bitsetx_equiv_def:
forall w, b, v. 0 <= b < 8 -> BV8.eq (bitset w b v) (bitsetx w b v)
end
module AVRint_limit
......@@ -1726,7 +1918,7 @@ use import ref.Ref
use import AVRint as AVR
use map.Map
type shadow_registers = {
type shadow_registers = {
ghost r0: ref int;
ghost r1: ref int;
ghost r2: ref int;
......@@ -1793,7 +1985,7 @@ predicate synchronized (self: shadow_registers) (avr: address_space) =
avr[28] = !(self.r28) /\
avr[29] = !(self.r29) /\
avr[30] = !(self.r30) /\
avr[31] = !(self.r31)
avr[31] = !(self.r31)
val shadow: shadow_registers
......@@ -1869,7 +2061,7 @@ let ghost init() ensures { synchronized shadow reg } =
let init (): unit
writes { shadow }
ensures { synchronized AVR.reg shadow }
= shadow.data.contents
= shadow.data.contents
val modify_r0 (): unit
writes { shadow.r0 }
......@@ -1926,7 +2118,7 @@ val modifyw_r30 (): unit writes { shadow.r30, shadow.r31 } ensures { synchronize
*)
(*
type shadow_registers = {
type shadow_registers = {
ghost reg: address_space;
ghost r0: ref int;
ghost r1: ref int;
......@@ -1993,7 +2185,7 @@ type shadow_registers = {
self.reg[28] = !(self.r28) /\
self.reg[29] = !(self.r29) /\
self.reg[30] = !(self.r30) /\
self.reg[31] = !(self.r31)
self.reg[31] = !(self.r31)
}
predicate synchronized (x: shadow_registers) (y: address_space) =
......
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