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

replace M with Map

parent 83147d46
......@@ -3,7 +3,7 @@ module AVRint
use import int.Int
use import int.EuclideanDivision
use import ref.Ref
use import map.Map as M
use import map.Map
use import bv.Pow2int
(***** FORMAL MODEL OF AVR ******)
......@@ -55,9 +55,9 @@ type address_space = { mutable data: map int int }
invariant { (forall i. 0 <= self.data[i] < 256) && (forall i j. 0 <= self.data[i]*self.data[j] <= 255*255) }
*)
function ([]) (r: address_space) (i: register): int = M.get r.data i
function ([]) (r: address_space) (i: register): int = Map.get r.data i
function ([<-]) (r: address_space) (i: register) (v: int): address_space
= { data = M.set r.data i v }
= { data = Map.set r.data i v }
function get_uint_term (rlo: (address_space, int)) (i: int): int
= let (reg, lo) = rlo in pow2 (8*i) * reg[lo+i]
......@@ -72,12 +72,12 @@ val reg: address_space
let mov (dst src: register): unit
writes { reg }
ensures { reg = old reg[dst<-reg[src]] }
= reg.data <- M.set reg.data dst (M.get reg.data src)
= reg.data <- Map.set reg.data dst (Map.get reg.data src)
let movw (dst src: register): unit
writes { reg }
ensures { reg = old reg[dst<-reg[src]][dst+1<-reg[src+1]] }
= reg.data <- M.set (M.set reg.data dst (M.get reg.data src)) (dst+1) (M.get reg.data (src+1))
= reg.data <- Map.set (Map.set reg.data dst (Map.get reg.data src)) (dst+1) (Map.get reg.data (src+1))
let mul (dst src: register): unit
writes { cf }
......@@ -85,8 +85,8 @@ let mul (dst src: register): unit
ensures { let p = old (reg[src]*reg[dst]) in reg = (old reg)[0 <- mod p 256][1 <- div p 256] }
ensures { let p = old (reg[src]*reg[dst]) in ?cf = div p (pow2 15) }
(* ensures { reg[1] < 255 } *)
= let prod = M.get reg.data dst*M.get reg.data src in
reg.data <- M.set (M.set reg.data 0 (mod prod 256)) 1 (div prod 256);
= let prod = Map.get reg.data dst*Map.get reg.data src in
reg.data <- Map.set (Map.set reg.data 0 (mod prod 256)) 1 (div prod 256);
cf.value <- div prod (pow2 15);
()
......@@ -95,11 +95,11 @@ let add (dst src: register): unit
writes { reg }
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);
let res = (M.get reg.data dst) in
= let sum = Map.get reg.data src + Map.get reg.data dst in
let r1 = (Map.get reg.data dst) in
let r2 = (Map.get reg.data src) in
reg.data <- Map.set reg.data dst (mod sum 256);
let res = (Map.get reg.data dst) in
if r1 >= 128 && r2 >= 128 ||
r1 >= 128 && res < 128 ||
r2 >= 128 && res < 128
......@@ -116,8 +116,8 @@ let adc (dst src: register): unit
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] + reg[src] + ?cf)) 256] }
ensures { ?cf = div (old (reg[dst] + reg[src] + ?cf)) 256 }
= let sum = M.get reg.data src + M.get reg.data dst + cf.value in
reg.data <- M.set reg.data dst (mod sum 256);
= let sum = Map.get reg.data src + Map.get reg.data dst + cf.value in
reg.data <- Map.set reg.data dst (mod sum 256);
cf.value <- div sum 256;
()
......@@ -126,8 +126,8 @@ let sub (dst src: register): unit
writes { reg }
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 dst - M.get reg.data src in
reg.data <- M.set reg.data dst (mod sum 256);
= let sum = Map.get reg.data dst - Map.get reg.data src in
reg.data <- Map.set reg.data dst (mod sum 256);
assert { -255 <= sum <= 255 };
cf.value <- -div sum 256;
()
......@@ -138,8 +138,8 @@ let sbc (dst src: register): unit
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] - reg[src] - ?cf)) 256] }
ensures { ?cf = -div (old (reg[dst] - reg[src] - ?cf)) 256 }
= let sum = M.get reg.data dst - M.get reg.data src - cf.value in
reg.data <- M.set reg.data dst (mod sum 256);
= let sum = Map.get reg.data dst - Map.get reg.data src - cf.value in
reg.data <- Map.set reg.data dst (mod sum 256);
cf.value <- -div sum 256;
()
......@@ -159,9 +159,9 @@ let ld_inc (dst src: register): unit
ensures { let cur = uint 2 (old reg) src in
let inc = cur+1 in
reg = (old reg)[dst <- mem[cur]][src <- mod inc 256][src+1 <- div inc 256] }
= let cur = M.get reg.data src + 256*M.get reg.data (src+1) in
= let cur = Map.get reg.data src + 256*Map.get reg.data (src+1) in
let nxt = mod (cur+1) (pow2 16) in
reg.data <- M.set (M.set (M.set reg.data dst (M.get mem.data cur)) src (mod nxt 256)) (src+1) (div nxt 256)
reg.data <- Map.set (Map.set (Map.set reg.data dst (Map.get mem.data cur)) src (mod nxt 256)) (src+1) (div nxt 256)
let ldd (dst src ofs: register): unit
writes { reg }
......@@ -169,8 +169,8 @@ let ldd (dst src ofs: register): unit
requires { uint 2 reg src + ofs < pow2 16 }
ensures { let cur = uint 2 (old reg) src in
reg = (old reg)[dst <- mem[cur+ofs]] }
= let cur = M.get reg.data src + 256*M.get reg.data (src+1) in
reg.data <- M.set reg.data dst (M.get mem.data (cur+ofs))
= let cur = Map.get reg.data src + 256*Map.get reg.data (src+1) in
reg.data <- Map.set reg.data dst (Map.get mem.data (cur+ofs))
let std (dst ofs src: register): unit
writes { mem }
......@@ -178,8 +178,8 @@ let std (dst ofs src: register): unit
requires { uint 2 reg dst + ofs < pow2 16 }
ensures { let cur = uint 2 (old reg) dst in
mem = (old mem)[cur+ofs <- reg[src]] }
= let cur = M.get reg.data dst + 256*M.get reg.data (dst+1) in
mem.data <- M.set mem.data (cur+ofs) (M.get reg.data src)
= let cur = Map.get reg.data dst + 256*Map.get reg.data (dst+1) in
mem.data <- Map.set mem.data (cur+ofs) (Map.get reg.data src)
let nop (): unit
= ()
......@@ -191,8 +191,8 @@ let sbci (dst: register) (k: int): unit
writes { reg }
ensures { reg = old reg[dst <- mod (old (reg[dst] - k - ?cf)) 256] }
ensures { ?cf = -div (old (reg[dst] - k - ?cf)) 256 }
= let sum = M.get reg.data dst - k - cf.value in
reg.data <- M.set reg.data dst (mod sum 256);
= let sum = Map.get reg.data dst - k - cf.value in
reg.data <- Map.set reg.data dst (mod sum 256);
cf.value <- -div sum 256;
()
......@@ -359,11 +359,25 @@ let add_ (dst src: register): unit
writes { reg, cf }
ensures { reg = old (reg[dst <- mod (reg[dst] + reg[src]) 256]) }
ensures { ?cf = old (div (reg[dst] + reg[src]) 256) }
= let r1 = BV8.of_int (M.get reg.data dst) in
let r2 = BV8.of_int (M.get reg.data src) in
let r3 = BV8.add r1 r2 in
reg.data <- M.set reg.data dst (BV8.to_uint r3);
if BV8.nth r1 7 && BV8.nth r2 7 || BV8.nth r1 7 && not BV8.nth r3 7 || not BV8.nth r3 7 && BV8.nth r2 7
= let rd = BV8.of_int (Map.get reg.data dst) in
let rr = BV8.of_int (Map.get reg.data src) in
let rd' = BV8.add rd rr in
reg.data <- Map.set reg.data dst (BV8.to_uint rd');
if 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
then
cf.value <- 1
else
cf.value <- 0
let add__ (dst src: register): unit
writes { reg, cf }
ensures { reg = old (reg[dst <- mod (reg[dst] + reg[src]) 256]) }
ensures { ?cf = old (div (reg[dst] + reg[src]) 256) }
= let rd = BV8.of_int (get reg.data dst) in
let rr = BV8.of_int (get reg.data src) in
let rd' = BV8.add rd rr in
reg.data <- set reg.data dst (BV8.to_uint rd');
if 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
then
cf.value <- 1
else
......@@ -373,8 +387,8 @@ let add_ (dst src: register): unit
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])) ] }
= let tmp = BV8.to_uint (BV8.bw_xor (BV8.of_int (M.get reg.data dst)) (BV8.of_int (M.get reg.data src))) in
reg.data <- M.set reg.data dst tmp
= let tmp = BV8.to_uint (BV8.bw_xor (BV8.of_int (Map.get reg.data dst)) (BV8.of_int (Map.get reg.data src))) in
reg.data <- Map.set reg.data dst tmp
let clr (dst: register): unit
writes { reg }
......@@ -384,15 +398,15 @@ let clr (dst: register): unit
let com (dst: register): unit
writes { reg }
ensures { reg = old reg[dst<- BV8.to_uint (BV8.bw_not (BV8.of_int reg[dst]))] }
= let tmp = BV8.to_uint (BV8.bw_not (BV8.of_int (M.get reg.data dst))) in
reg.data <- M.set reg.data dst tmp
= let tmp = BV8.to_uint (BV8.bw_not (BV8.of_int (Map.get reg.data dst))) in
reg.data <- Map.set reg.data dst tmp
let asr (dst: register): unit
writes { reg, cf }
ensures { reg = old reg[dst<- BV8.to_uint (BV8.asr (BV8.of_int reg[dst]) 1)] }
ensures { ?cf = mod (old reg[dst]) 2 }
= cf.value <- if BV8.nth (BV8.of_int (M.get reg.data dst)) 0 then 1 else 0;
reg.data <- M.set reg.data dst (BV8.to_uint (BV8.asr (BV8.of_int (M.get reg.data dst)) 1))
= cf.value <- if BV8.nth (BV8.of_int (Map.get reg.data dst)) 0 then 1 else 0;
reg.data <- Map.set reg.data dst (BV8.to_uint (BV8.asr (BV8.of_int (Map.get reg.data dst)) 1))
end
......
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