Skip to content
GitLab
Commit f104ac14 authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

rename register_file -> address_space

parent bbb5e818
Hide whitespace changes
Inline Side-by-side
avrmodel.mlw
View file @ f104ac14
......@@ -49,25 +49,25 @@ function (?) (x: int_flag): int = x.value
val cf: int_flag
type register_file = { mutable data: map int int }
type address_space = { mutable data: map int int }
invariant { forall i. 0 <= self.data[i] < 256 }
(*
invariant { (forall i. 0 <= self.data[i] < 256) && (forall i j. 0 <= self.data[i]*self.data[j] <= 255*255) }
*)
function ([]) (r: register_file) (i: register): int = M.get r.data i
function ([<-]) (r: register_file) (i: register) (v: int): register_file
function ([]) (r: address_space) (i: register): int = M.get r.data i
function ([<-]) (r: address_space) (i: register) (v: int): address_space
= { data = M.set r.data i v }
function get_uint_term (rlo: (register_file, int)) (i: int): int
function get_uint_term (rlo: (address_space, int)) (i: int): int
= let (reg, lo) = rlo in pow2 (8*i) * reg[lo+i]
clone sum.Sum as B with type container = (register_file, int), function f = get_uint_term
clone sum.Sum as B with type container = (address_space, int), function f = get_uint_term
function uint (w: int) (reg: register_file) (lo: register): int
function uint (w: int) (reg: address_space) (lo: register): int
= B.sum (reg,lo) 0 w
val reg: register_file
val reg: address_space
let mov (dst src: register): unit
writes { reg }
......@@ -96,10 +96,20 @@ let add (dst src: register): unit
ensures { reg = old reg[dst <- mod (old (reg[dst] + reg[src])) 256] }
ensures { ?cf = div (old (reg[dst] + reg[src])) 256 }
= let sum = M.get reg.data src + M.get reg.data dst in
let r1 = (M.get reg.data dst) in
let r2 = (M.get reg.data src) in
reg.data <- M.set reg.data dst (mod sum 256);
cf.value <- div sum 256;
let res = (M.get reg.data dst) in
if r1 >= 128 && r2 >= 128 ||
r1 >= 128 && res < 128 ||
r2 >= 128 && res < 128
then
cf.value <- 1
else
cf.value <- 0;
()
let adc (dst src: register): unit
writes { cf }
reads { cf }
......@@ -137,7 +147,7 @@ constant rX: register = 26
constant rY: register = 28
constant rZ: register = 30
val mem: register_file
val mem: address_space
(* TODO mem and reg overlap *)
(* TODO memory wrap around *)
......@@ -188,7 +198,7 @@ let sbci (dst: register) (k: int): unit
(****** REASONING ABOUT MACHINE STATE *)
predicate eq (w: int) (reg reg': register_file) (lo: int)
predicate eq (w: int) (reg reg': address_space) (lo: int)
= forall i. lo <= i < lo+w -> reg[i] = reg'[i]
goal eq_narrow:
......@@ -268,7 +278,7 @@ meta rewrite prop uint_11
meta rewrite prop uint_12
meta compute_max_steps 0x1000000
let rec ghost uint_recursion (reg: register_file) (lo w: int): unit
let rec ghost uint_recursion (reg: address_space) (lo w: int): unit
requires { w >= 0 }
ensures { B.sum (reg,lo) 1 w = 256*B.sum (reg,lo+1) 0 (w-1) }
variant { w }
......@@ -277,7 +287,7 @@ let rec ghost uint_recursion (reg: register_file) (lo w: int): unit
uint_recursion reg lo (w-1)
end
let rec ghost uint_bound (reg: register_file) (lo w: int): unit
let rec ghost uint_bound (reg: address_space) (lo w: int): unit
requires { w >= 0 }
ensures { 0 <= uint w reg lo < pow2 (w*8) }
variant { w }
......@@ -287,7 +297,7 @@ let rec ghost uint_bound (reg: register_file) (lo w: int): unit
uint_bound reg (lo+1) (w-1);
end
let ghost eq_uint_rev (reg reg': register_file) (lo w: int): unit
let ghost eq_uint_rev (reg reg': address_space) (lo w: int): unit
requires { uint w reg lo = uint w reg' lo }
ensures { eq w reg reg' lo }
= for w' = 0 to w-1 do
......@@ -298,7 +308,7 @@ let ghost eq_uint_rev (reg reg': register_file) (lo w: int): unit
assert { mod(uint w' reg' lo + pow2 (8*w')*reg'[lo+w']) (pow2 (8*w')) = uint w' reg' lo };
done
let rec ghost uint_extend (reg: register_file) (lo w w': int): unit
let rec ghost uint_extend (reg: address_space) (lo w w': int): unit
variant { w' }
requires { w >= 0 }
requires { w' >= 0 }
......@@ -309,7 +319,7 @@ let rec ghost uint_extend (reg: register_file) (lo w w': int): unit
uint_extend reg lo w (w'-1);
end
let ghost uint_shift (reg reg': register_file) (lo lo' w w' arg: int): unit
let ghost uint_shift (reg reg': address_space) (lo lo' w w' arg: int): unit
requires { w >= 0 }
requires { w' >= 0 }
requires { forall i. 0 < i <= w' -> reg[lo-i] = reg'[lo'-i] }
......@@ -328,7 +338,7 @@ let ghost uint_shift (reg reg': register_file) (lo lo' w w' arg: int): unit
assert { pow2 8*pow2 (8*n) = pow2 (8*(n+1)) }
done
let ghost uint_combine (reg: register_file) (b w w': int)
let ghost uint_combine (reg: address_space) (b w w': int)
requires { w >= 0 /\ w' >= 0 }
ensures { uint (w+w') reg b = uint w reg b + pow2 (8*w)*uint w' reg (b+w) }
= for n = 0 to w'-1 do
......@@ -423,18 +433,18 @@ function (?) (x: int_flag): int = if x.value then 1 else 0
val cf: int_flag
type register_file = { mutable data: map int BV8.t }
type address_space = { mutable data: map int BV8.t }
function ([]) (r: register_file) (i: register): int = BV8.to_uint (M.get r.data i)
function ([<-]) (r: register_file) (i: register) (v: int): register_file
function ([]) (r: address_space) (i: register): int = BV8.to_uint (M.get r.data i)
function ([<-]) (r: address_space) (i: register) (v: int): address_space
= { data = M.set r.data i (BV8.of_int v) }
function get_uint_term (rlo: (register_file, int)) (i: int): int
function get_uint_term (rlo: (address_space, int)) (i: int): int
= let (reg, lo) = rlo in pow2 (8*i) * reg[lo+i]
clone sum.Sum as B with type container = (register_file, int), function f = get_uint_term
clone sum.Sum as B with type container = (address_space, int), function f = get_uint_term
function uint (w: int) (reg: register_file) (lo: register): int
function uint (w: int) (reg: address_space) (lo: register): int
= B.sum (reg,lo) 0 w
lemma uint_0:
......@@ -460,7 +470,7 @@ lemma uint_9:
lemma uint_10:
forall reg, lo. uint 10 reg lo = 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]
val reg: register_file
val reg: address_space
let movw (dst src: register): unit
writes { reg }
......@@ -524,7 +534,7 @@ constant rX: register = 26
constant rY: register = 28
constant rZ: register = 30
val mem: register_file
val mem: address_space
(* TODO mem and reg overlap *)
(* TODO memory wrap around *)
......@@ -586,7 +596,7 @@ let clr (dst: register): unit
(****** REASONING ABOUT MACHINE STATE *)
predicate eq (w: int) (reg reg': register_file) (lo: int)
predicate eq (w: int) (reg reg': address_space) (lo: int)
= forall i. lo <= i < lo+w -> reg[i] = reg'[i]
goal eq_narrow:
......@@ -596,7 +606,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
let rec ghost uint_recursion (reg: register_file) (lo w: int): unit
let rec ghost uint_recursion (reg: address_space) (lo w: int): unit
requires { w >= 0 }
ensures { B.sum (reg,lo) 1 w = 256*B.sum (reg,lo+1) 0 (w-1) }
variant { w }
......@@ -605,7 +615,7 @@ let rec ghost uint_recursion (reg: register_file) (lo w: int): unit
uint_recursion reg lo (w-1)
end
let rec ghost uint_bound (reg: register_file) (lo w: int): unit
let rec ghost uint_bound (reg: address_space) (lo w: int): unit
requires { w >= 0 }
ensures { 0 <= uint w reg lo < pow2 (w*8) }
variant { w }
......@@ -615,7 +625,7 @@ let rec ghost uint_bound (reg: register_file) (lo w: int): unit
uint_bound reg (lo+1) (w-1);
end
let ghost eq_uint_rev (reg reg': register_file) (lo w: int): unit
let ghost eq_uint_rev (reg reg': address_space) (lo w: int): unit
requires { uint w reg lo = uint w reg' lo }
ensures { eq w reg reg' lo }
= for w' = 0 to w-1 do
......@@ -626,7 +636,7 @@ let ghost eq_uint_rev (reg reg': register_file) (lo w: int): unit
assert { mod(uint w' reg' lo + pow2 (8*w')*reg'[lo+w']) (pow2 (8*w')) = mod(uint w' reg' lo) (pow2 (8*w')) = uint w' reg' lo };
done
let rec ghost uint_extend (reg: register_file) (lo w w': int): unit
let rec ghost uint_extend (reg: address_space) (lo w w': int): unit
variant { w' }
requires { w >= 0 }
requires { w' >= 0 }
......@@ -637,7 +647,7 @@ let rec ghost uint_extend (reg: register_file) (lo w w': int): unit
uint_extend reg lo w (w'-1);
end
let ghost uint_shift (reg reg': register_file) (lo lo' w w' arg: int): unit
let ghost uint_shift (reg reg': address_space) (lo lo' w w' arg: int): unit
requires { w >= 0 }
requires { w' >= 0 }
requires { forall i. 0 < i <= w' -> reg[lo-i] = reg'[lo'-i] }
......@@ -655,7 +665,7 @@ let ghost uint_shift (reg reg': register_file) (lo lo' w w' arg: int): unit
}
done
let ghost uint_combine (reg: register_file) (b w w': int)
let ghost uint_combine (reg: address_space) (b w w': int)
requires { w >= 0 /\ w' >= 0 }
ensures { uint (w+w') reg b = uint w reg b + pow2 (8*w)*uint w' reg (b+w) }
= for n = 0 to w'-1 do
......@@ -756,14 +766,14 @@ val sbc (dst: register) (src: int): unit
ensures { !dst = mod (old (!dst - src - ?cf)) 256 }
ensures { ?cf = -div (old (!dst - src - ?cf)) 256 }
type register_file = { mutable byte: map int int }
type address_space = { mutable byte: map int int }
invariant { forall i. 0 <= self.byte[i] < 256 }
function ([]) (r: register_file) (i: int): int = M.get r.byte i
function ([<-]) (r: register_file) (i: int) (v: int): register_file
function ([]) (r: address_space) (i: int): int = M.get r.byte i
function ([<-]) (r: address_space) (i: int) (v: int): address_space
= { byte = M.set r.byte i v }
val mem: register_file
val mem: address_space
(*
let ld_inc (dst: register) (src: int): unit
......@@ -809,7 +819,7 @@ val sbci (dst: register) (k: int): unit
(****** REASONING ABOUT MACHINE STATE *)
predicate eq (w: int) (reg reg': register_file) (lo: int)
predicate eq (w: int) (reg reg': address_space) (lo: int)
= forall i. lo <= i < lo+w -> reg[i] = reg'[i]
goal eq_narrow:
......@@ -818,7 +828,7 @@ goal eq_combine:
forall reg reg', lo lo' w w'. eq w reg reg' lo -> eq w' reg reg' lo' -> lo' = lo+w -> eq (w+w') reg reg' lo
(*
let rec ghost uint_recursion (reg: register_file) (lo w: int): unit
let rec ghost uint_recursion (reg: address_space) (lo w: int): unit
requires { w >= 0 }
ensures { B.sum (reg,lo) 1 w = 256*B.sum (reg,lo+1) 0 (w-1) }
variant { w }
......@@ -827,7 +837,7 @@ let rec ghost uint_recursion (reg: register_file) (lo w: int): unit
uint_recursion reg lo (w-1)
end
let rec ghost uint_bound (reg: register_file) (lo w: int): unit
let rec ghost uint_bound (reg: address_space) (lo w: int): unit
requires { w >= 0 }
ensures { 0 <= uint w reg lo < pow2 (w*8) }
variant { w }
......@@ -837,7 +847,7 @@ let rec ghost uint_bound (reg: register_file) (lo w: int): unit
uint_bound reg (lo+1) (w-1);
end
let ghost eq_uint_rev (reg reg': register_file) (lo w: int): unit
let ghost eq_uint_rev (reg reg': address_space) (lo w: int): unit
requires { uint w reg lo = uint w reg' lo }
ensures { eq w reg reg' lo }
= for w' = 0 to w-1 do
......@@ -848,7 +858,7 @@ let ghost eq_uint_rev (reg reg': register_file) (lo w: int): unit
assert { mod(uint w' reg' lo + pow2 (8*w')*reg'[lo+w']) (pow2 (8*w')) = uint w' reg' lo };
done
let rec ghost uint_extend (reg: register_file) (lo w w': int): unit
let rec ghost uint_extend (reg: address_space) (lo w w': int): unit
variant { w' }
requires { w >= 0 }
requires { w' >= 0 }
......@@ -859,7 +869,7 @@ let rec ghost uint_extend (reg: register_file) (lo w w': int): unit
uint_extend reg lo w (w'-1);
end
let ghost uint_shift (reg reg': register_file) (lo lo' w w' arg: int): unit
let ghost uint_shift (reg reg': address_space) (lo lo' w w' arg: int): unit
requires { w >= 0 }
requires { w' >= 0 }
requires { forall i. 0 < i <= w' -> reg[lo-i] = reg'[lo'-i] }
......@@ -877,7 +887,7 @@ let ghost uint_shift (reg reg': register_file) (lo lo' w w' arg: int): unit
}
done
let ghost uint_combine (reg: register_file) (b w w': int)
let ghost uint_combine (reg: address_space) (b w w': int)
requires { w >= 0 /\ w' >= 0 }
ensures { uint (w+w') reg b = uint w reg b + pow2 (8*w)*uint w' reg (b+w) }
= for n = 0 to w'-1 do
......
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