Library AbGoto
Require Import
Coqlib Utf8 String ToString Util
IntSet
Containers.Maps
Integers
Goto GotoString GotoSem
LatticeSignatures AdomLib
AbMachineNonrel.
Set Implicit Arguments.
Record mem_dom (ab_mem ab_num: Type) :=
{ as_wl: weak_lattice ab_mem
; var: ab_mem → register → ab_num
; load_single: ab_mem → addr → ab_num
; store_single: ab_mem → addr → ab_num → ab_mem
; assign: ab_mem → register → ab_num → ab_mem
; compare: ab_mem → register → register → ab_mem
; assume: ab_mem → flag → bool → ab_mem+⊥
; init: memory → list addr → ab_mem
}.
Definition pre_machine_config : Type :=
(flag_state × register_state × memory)%type.
Definition pmc_flg : pre_machine_config → flag_state := fst ∘ fst.
Definition pmc_reg : pre_machine_config → register_state := snd ∘ fst.
Definition pmc_mem : pre_machine_config → memory := snd.
Instance gamma_to_mc {A} `(gamma_op A pre_machine_config) :
gamma_op A machine_config :=
λ a mc, (mc_flg mc, mc_reg mc, mc_mem mc) ∈ γ(a).
Lemma gamma_to_mc_adom {A} wl (G: gamma_op A pre_machine_config) :
adom A _ wl G →
adom A _ wl (gamma_to_mc G).
Section MEM_DOM_SOUND.
Definition Assign {ab_num: Type} `{ab_machine_int ab_num}
(E: 𝒫 machine_config) (rd: register) (v: ab_num) : 𝒫 machine_config :=
fun mci ⇒ ∃ m, ∃ v',
E m ∧ γ v v'
∧ mci.(mc_flg) = m.(mc_flg)
∧ mci.(mc_reg) = m.(mc_reg) # rd ← v'
∧ mci.(mc_mem) = m.(mc_mem).
Definition Store {ab_num: Type} `{ab_machine_int ab_num}
(E: 𝒫 machine_config) (dst:addr) (v: ab_num) : 𝒫 machine_config :=
fun mci ⇒ ∃ m v',
E {| pc := mci.(pc); mc_flg := mci.(mc_flg)
; mc_reg := mci.(mc_reg); mc_mem := m |}
∧ v' ∈ γ(v)
∧ ∀ a, mci.(mc_mem) a = (m # dst ← v') a.
Definition Compare {ab_num: Type} `{ab_machine_int ab_num}
(E: 𝒫 machine_config) (rs rd: register) : 𝒫 machine_config :=
fun mci ⇒ ∃ f,
E {| pc := mci.(pc); mc_flg := f
; mc_reg := mci.(mc_reg); mc_mem := mci.(mc_mem) |}
∧ mci.(mc_flg) = eval_flag (mci.(mc_reg) rd) (mci.(mc_reg) rs).
Definition Assume {ab_num: Type} `{ab_machine_int ab_num}
(E: 𝒫 machine_config) (f: flag) (b: bool) : 𝒫 machine_config :=
fun mci ⇒ E mci ∧ mci.(mc_flg) f = b.
Let mc_mem' (mc: machine_config) : int → int := mc.(mc_mem).
Local Coercion mc_mem' : machine_config >-> Funclass.
Record mem_dom_sound {ab_mem ab_num} `{ab_machine_int ab_num} (M: mem_dom ab_mem ab_num) (G: gamma_op ab_mem pre_machine_config) : Prop :=
{ as_adom : adom ab_mem pre_machine_config M.(as_wl) G
; var_sound: ∀ ab:ab_mem, ∀ m: machine_config,
m ∈ γ(ab) → ∀ r, mc_reg m r ∈ γ(M.(var) ab r)
; load_sound: ∀ ab:ab_mem, ∀ m: machine_config,
m ∈ γ(ab) → ∀ a:addr, m(a) ∈ γ(M.(load_single) ab a)
; assign_sound: ∀ ab:ab_mem, ∀ rd v,
Assign (γ ab) rd v ⊆ γ(M.(assign) ab rd v)
; store_sound: ∀ ab:ab_mem, ∀ dst v,
Store (γ ab) dst v ⊆ γ (M.(store_single) ab dst v)
; compare_sound: ∀ ab:ab_mem, ∀ rs rd,
Compare (γ ab) rs rd ⊆ γ(M.(compare) ab rs rd)
; assume_sound: ∀ ab:ab_mem, ∀ f b,
Assume (γ ab) f b ⊆ γ(M.(assume) ab f b)
; init_sound: ∀ (m: memory) (dom: list addr) f r (m': memory),
(∀ a, List.In a dom → m a = m' a) →
(f, r, m') ∈ γ(M.(init) m dom)
}.
Context {ab_mem ab_num: Type} `{D: ab_machine_int ab_num} (M: mem_dom ab_mem ab_num).
Definition assume_mem : ab_mem → addr → int → ab_mem := λ ab a val,
M.(store_single) ab a (const_int val).
Definition AssumeMem (E: 𝒫 machine_config) (dst: addr) (v: int) : 𝒫 machine_config :=
fun mci ⇒ ∃ m,
E {| pc := mci.(pc); mc_flg := mci.(mc_flg)
; mc_reg := mci.(mc_reg); mc_mem := m |}
∧ ∀ a, mci.(mc_mem) a = (m # dst ← v) a.
Context (D_correct: ab_machine_int_correct D)
(G: gamma_op ab_mem pre_machine_config)
(M_correct: mem_dom_sound M G).
Lemma assume_mem_sound (ab:ab_mem) (a: addr) (val: int) :
AssumeMem (γ ab) a val ⊆ γ(assume_mem ab a val).
End MEM_DOM_SOUND.
Require Generate.
Definition value_lt : relation int :=
fun i j ⇒ Int.unsigned i < Int.unsigned j.
Definition value_cmp : int → int → Datatypes.comparison :=
fun x y ⇒ if Int.ltu x y then Lt else if Int.eq x y then Eq else Gt.
Instance OT_ints : OrderedType int := { _eq := eq; _lt := value_lt; _cmp := value_cmp }.
Lemma register_neq_neq : ∀ u v : register,
u ≠ v → u =/= v.
Lemma register_eq_eq : ∀ u v: register, u === v → u = v.
Section AbMachineConfig.
Variable d: Type.
Variable n: ab_machine_int d.
Hypothesis n_correct: ab_machine_int_correct n.
Variable alocs : int_set.
Definition is_aloc (v: addr) : bool :=
if IntSet.mem (proj v) alocs then true else false.
Lemma is_aloc_cases v :
∀ P,
(IntSet.Mem v alocs → P true) →
(¬ IntSet.Mem v alocs → P false) →
P (is_aloc v).
Record ab_machine_config :=
{ ab_flg: (register × register)+⊤
; ab_reg: Map [ register , d ]
; ab_mem: Map [ int, d ]
}.
Definition find_def {A B} `{OrderedType A} `{weak_lattice B} (f: Map [A, B]) (x: A) : B :=
match (f)[x] with
| Some b ⇒ b
| None ⇒ top
end.
Definition find_aloc (m: Map [int, d]) (v: int) : d :=
if is_aloc v
then find_def m v
else ⊤.
Definition find_bot {A B} `{OrderedType A} (f: Map [A, B]) (x: A) : B+⊥ :=
match (f)[x] with
| Some b ⇒ NotBot b
| None ⇒ Bot
end.
Definition ab_machine_state : Type := (ab_machine_config + d)%type.
Definition flag_LE (x y: (register × register)+⊤) : Prop :=
match x, y with
| _, All ⇒ True
| All, Just _ ⇒ False
| Just x', Just y' ⇒ x' = y'
end.
Definition flag_LE_dec x y : { flag_LE x y } + { ¬ flag_LE x y } :=
match x, y with
| _, All ⇒ left I
| All, _ ⇒ right (λ x, x)
| Just x', Just y' ⇒ eq_dec x' y'
end.
Definition map_LE {A B: Type} `{OrderedType A} (leb : B → B → bool) (x y: Map [ A, B ]) : Prop :=
∀ a b, MapsTo a b x → ∃ b', MapsTo a b' y ∧ leb b b' = true.
Definition map_LE_dec {A B: Type} `{OrderedType A} (leb : B → B → bool) (x y: Map [ A, B ]) :
{ map_LE leb x y } + { ¬ map_LE leb x y }.
Definition wmap_LE {A B: Type} `{OrderedType A} `{weak_lattice B} (x y: Map [ A, B ]) : Prop :=
∀ a, find_def x a ⊑ find_def y a = true
∨ (x)[a] = (y)[a] ∧ (x)[a] = None.
Definition wmap_LE_dec {A B: Type} `{OrderedType A} `{weak_lattice B} (x y: Map [ A, B ]) :
{ wmap_LE x y } + { ¬ wmap_LE x y }.
Definition abmc_LE (x y: ab_machine_config) : Prop :=
flag_LE x.(ab_flg) y.(ab_flg)
∧ wmap_LE x.(ab_reg) y.(ab_reg)
∧ wmap_LE x.(ab_mem) y.(ab_mem).
Definition abmc_LE_dec x y : { abmc_LE x y } + { ¬ abmc_LE x y } :=
match flag_LE_dec x.(ab_flg) y.(ab_flg) with
| right NE ⇒ right (λ K, NE (proj1 K))
| left F ⇒
match wmap_LE_dec x.(ab_reg) y.(ab_reg) with
| right NE ⇒ right (λ K, NE (proj1 (proj2 K)))
| left R ⇒
match wmap_LE_dec x.(ab_mem) y.(ab_mem) with
| right NE ⇒ right (λ K, NE (proj2 (proj2 K)))
| left MEM ⇒ left (conj F (conj R MEM))
end
end
end.
Definition abms_LE (x y: ab_machine_state) : Prop :=
match x, y with
| inl x', inl y' ⇒ abmc_LE x' y'
| inr x', inr y' ⇒ leb x' y' = true
| _, _ ⇒ False
end.
Definition abms_LE_dec x y : { abms_LE x y } + { ¬ abms_LE x y }.
Definition flg_join x y :=
if flag_LE_dec x y
then y
else All.
Definition map_join {A B: Type} `{OrderedType A} (join: B → B → B) (f g: Map [ A, B ]) : Map [ A, B ] :=
fold
(fun k y ⇒ add k match (f)[k] with None ⇒ y | ⌊x⌋ ⇒ join x y end)
g
f
.
Definition map_join_get {A B: Type} `{OrderedType A} (join : B → B → B) (f g: Map [ A, B ]) :
∀ k, find_bot (map_join join f g) k = match find_bot f k, find_bot g k with
| NotBot x, NotBot y ⇒ NotBot (join x y)
| NotBot x, Bot ⇒ NotBot x
| Bot, NotBot y ⇒ NotBot y
| Bot, Bot ⇒ Bot
end.
Definition wmap_join {A B: Type} `{OrderedType A} (join: B → B → B) `{weak_lattice B} (f g: Map [ A, B ]) : Map [ A, B ] :=
fold
(fun k y ⇒ let y' := join (find_def f k) y in if ⊤ ⊑ y' then id else add k y')
g
[]
.
Definition wmap_join_get {A B: Type} `{OrderedType A} (join: B → B → B) `{weak_lattice B} (f g: Map [ A, B ]) (q:A) :
find_def (wmap_join join f g) q = match (g)[q] with
| None ⇒ (⊤)
| Some y ⇒ let y' := join (find_def f q) y in
if ⊤ ⊑ y' then ⊤ else y'
end.
Definition abmc_join (x y: ab_machine_config) : ab_machine_config :=
{| ab_flg := flg_join x.(ab_flg) y.(ab_flg)
; ab_reg := wmap_join join x.(ab_reg) y.(ab_reg)
; ab_mem := wmap_join join x.(ab_mem) y.(ab_mem) |}.
Definition abmc_widen (x y: ab_machine_config) : ab_machine_config :=
{| ab_flg := flg_join x.(ab_flg) y.(ab_flg)
; ab_reg := wmap_join widen x.(ab_reg) y.(ab_reg)
; ab_mem := wmap_join widen x.(ab_mem) y.(ab_mem) |}.
Definition abms_join (x y: ab_machine_state) : ab_machine_state+⊤ :=
match x, y with
| inl x', inl y' ⇒ Just (inl (abmc_join x' y'))
| inr x', inr y' ⇒ Just (inr (join x' y'))
| _, _ ⇒ All
end.
Definition flg_gamma (x: (register × register)+⊤) (mci: pre_machine_config) : Prop :=
match x with
| Just (r1, r2) ⇒ ∀ f, pmc_flg mci f = eval_flag (pmc_reg mci r2) (pmc_reg mci r1) f
| All ⇒ True
end.
Definition map_gamma {A B C: Type} `{OrderedType A} `{weak_lattice B} `{gamma_op B C} (x: Map [ A, B ]) (v: A → C): Prop :=
∀ k, γ (find_bot x k) (v k).
Lemma map_join_sound {A B C: Type} `{OrderedType A} `{WL:weak_lattice B}
`{G:gamma_op B C} `{adom B C WL G} :
∀ P, Proper (_eq ==> eq) P →
∀ x y: Map [ A, B ],
map_gamma x P ∨ map_gamma y P → map_gamma (map_join join x y) P.
Definition wmap_gamma {A B C: Type} `{OrderedType A} `{weak_lattice B} `{gamma_op B C} (x: Map [ A, B ]) (v: A → C): Prop :=
∀ k, γ (find_def x k) (v k).
Lemma wmap_join_sound {A B C: Type} `{OrderedType A} `{WL: weak_lattice B} `{G: gamma_op B C} `{AD: adom _ _ WL G} (x y: Map [ A, B ]) :
∀ P, Proper (_eq ==> eq) P →
wmap_gamma x P ∨ wmap_gamma y P → wmap_gamma (wmap_join join x y) P.
Definition gamma_mem {C: Type} `{G: gamma_op d C} (x: Map [ int, d ]) (v: int → C) : Prop :=
∀ k, v(k) ∈ γ(find_aloc x k).
Lemma gamma_mem_sound {C: Type} `{G: gamma_op d C} `{AD: adom _ _ _ G} (x y: Map [ int, d ]) :
(gamma_mem x ∪ gamma_mem y) ⊆ gamma_mem (wmap_join join x y).
Instance abmc_gamma : gamma_op ab_machine_config pre_machine_config :=
λ x mc,
flg_gamma x.(ab_flg) mc
∧ wmap_gamma x.(ab_reg) (pmc_reg mc)
∧ gamma_mem x.(ab_mem) (pmc_mem mc).
Definition abms_gamma (x: ab_machine_state) (m: machine_state) : Prop :=
match x, m with
| inl x', Running m' ⇒ m' ∈ γ(x')
| inr x', Halted m' ⇒ γ x' m'
| _, _ ⇒ False
end.
Definition map_to_string {A B: Type} `{OrderedType A}
(A_to_string : A → string) (B_to_string : B → string)
(m: Map [A,B]) : string :=
(fold
(fun k v acc ⇒ A_to_string k ++ " ↦ " ++ B_to_string v ++ "; " ++ acc)
m
""
)%string.
Instance abmc_toString `{ToString d} : ToString ab_machine_config :=
{ to_string x :=
("⟨" ++
match x.(ab_flg) with
| All ⇒ ""
| Just (r1,r2) ⇒ "(" ++ string_of_reg r1 ++ ", " ++ string_of_reg r2 ++ ")"
end ++
map_to_string string_of_reg to_string x.(ab_reg) ++
map_to_string string_of_int to_string x.(ab_mem) ++
"⟩"
)%string
}.
Definition ab_machine_config_pl : pre_lattice ab_machine_config :=
{| pl_leb x y := abmc_LE_dec x y
; pl_join x y := Just (abmc_join x y)
; pl_widen x y := Just (abmc_widen x y)
|}.
Lemma ab_machine_config_pl_sound : pre_lattice_spec ab_machine_config_pl abmc_gamma.
Hint Resolve as_int_adom.
Definition invalidate_flag (r:register) f :=
match f with
| All ⇒ All
| Just (r1, r2) ⇒ if eq_dec r r1 then All else if eq_dec r r2 then All else f
end.
Lemma invalidate_flag_preserve : ∀ {R F p1 p2},
invalidate_flag R F = Just (p1,p2) →
R ≠ p1 ∧ R ≠ p2.
Definition ab_store_strong (m: Map [ addr, d ]) (a: addr) (v: d) : Map [ addr, d ] :=
if is_aloc a
then if ⊤ ⊑ v
then remove a m
else (m)[a <- v]
else m.
Definition abmc_init (m: memory) (dom: list int) : Map [ int, d ] :=
List.fold_left (fun a i ⇒ (a)[ i <- const_int (m i) ]) dom [].
Definition ab_machine_config_mem_dom : mem_dom (ab_machine_config+⊤) d :=
{|
as_wl := weak_lattice_of_pre_lattice ab_machine_config_pl
; var x := match x with
| Just x' ⇒ find_def x'.(ab_reg)
| _ ⇒ fun _ ⇒ top
end
; load_single x := match x with
| Just x' ⇒ find_aloc x'.(ab_mem)
| _ ⇒ fun _ ⇒ top
end
; compare x rs rd := top_lift (λ x', {| ab_flg := Just (rs, rd)
; ab_reg := x'.(ab_reg)
; ab_mem := x'.(ab_mem) |}) x
; assume x f b :=
match x with
| Just x' ⇒
match x'.(ab_flg) with
| Just (Ru, Rv) ⇒
let u := find_def x'.(ab_reg) Ru in
let v := find_def x'.(ab_reg) Rv in
let op := match f with FLE ⇒ Cle | FLT ⇒ Clt | FEQ ⇒ Ceq end in
let v'u' := backward_int_binop (OpCmp op) v u
(const_int (IntervalDomain.Interval.of_bool b)) in
match v'u' with
| (NotBot v', NotBot u') ⇒
NotBot (Just {| ab_flg := x'.(ab_flg)
; ab_reg := (x'.(ab_reg)) [ Ru <- u' ] [ Rv <- v' ]
; ab_mem := x'.(ab_mem) |})
| _ ⇒ Bot
end
| All ⇒ NotBot x
end
| All ⇒ NotBot x
end
; assign x := match x with
| Just x' ⇒ fun r v ⇒ Just {| ab_flg := invalidate_flag r x'.(ab_flg)
; ab_reg := (x'.(ab_reg)) [ r <- v ]
; ab_mem := x'.(ab_mem) |}
| _ ⇒ fun _ _ ⇒ All
end
; store_single x a v := do_top x' <- x;
Just {| ab_flg := x'.(ab_flg)
; ab_reg := x'.(ab_reg)
; ab_mem := ab_store_strong x'.(ab_mem) a v |}
; init m dom := Just {| ab_flg := All; ab_reg := []; ab_mem := abmc_init m dom |}
|}.
Lemma ab_machine_config_mem_dom_sound : mem_dom_sound ab_machine_config_mem_dom (toplift_gamma abmc_gamma).
End AbMachineConfig.
Coqlib Utf8 String ToString Util
IntSet
Containers.Maps
Integers
Goto GotoString GotoSem
LatticeSignatures AdomLib
AbMachineNonrel.
Set Implicit Arguments.
Record mem_dom (ab_mem ab_num: Type) :=
{ as_wl: weak_lattice ab_mem
; var: ab_mem → register → ab_num
; load_single: ab_mem → addr → ab_num
; store_single: ab_mem → addr → ab_num → ab_mem
; assign: ab_mem → register → ab_num → ab_mem
; compare: ab_mem → register → register → ab_mem
; assume: ab_mem → flag → bool → ab_mem+⊥
; init: memory → list addr → ab_mem
}.
Definition pre_machine_config : Type :=
(flag_state × register_state × memory)%type.
Definition pmc_flg : pre_machine_config → flag_state := fst ∘ fst.
Definition pmc_reg : pre_machine_config → register_state := snd ∘ fst.
Definition pmc_mem : pre_machine_config → memory := snd.
Instance gamma_to_mc {A} `(gamma_op A pre_machine_config) :
gamma_op A machine_config :=
λ a mc, (mc_flg mc, mc_reg mc, mc_mem mc) ∈ γ(a).
Lemma gamma_to_mc_adom {A} wl (G: gamma_op A pre_machine_config) :
adom A _ wl G →
adom A _ wl (gamma_to_mc G).
Section MEM_DOM_SOUND.
Definition Assign {ab_num: Type} `{ab_machine_int ab_num}
(E: 𝒫 machine_config) (rd: register) (v: ab_num) : 𝒫 machine_config :=
fun mci ⇒ ∃ m, ∃ v',
E m ∧ γ v v'
∧ mci.(mc_flg) = m.(mc_flg)
∧ mci.(mc_reg) = m.(mc_reg) # rd ← v'
∧ mci.(mc_mem) = m.(mc_mem).
Definition Store {ab_num: Type} `{ab_machine_int ab_num}
(E: 𝒫 machine_config) (dst:addr) (v: ab_num) : 𝒫 machine_config :=
fun mci ⇒ ∃ m v',
E {| pc := mci.(pc); mc_flg := mci.(mc_flg)
; mc_reg := mci.(mc_reg); mc_mem := m |}
∧ v' ∈ γ(v)
∧ ∀ a, mci.(mc_mem) a = (m # dst ← v') a.
Definition Compare {ab_num: Type} `{ab_machine_int ab_num}
(E: 𝒫 machine_config) (rs rd: register) : 𝒫 machine_config :=
fun mci ⇒ ∃ f,
E {| pc := mci.(pc); mc_flg := f
; mc_reg := mci.(mc_reg); mc_mem := mci.(mc_mem) |}
∧ mci.(mc_flg) = eval_flag (mci.(mc_reg) rd) (mci.(mc_reg) rs).
Definition Assume {ab_num: Type} `{ab_machine_int ab_num}
(E: 𝒫 machine_config) (f: flag) (b: bool) : 𝒫 machine_config :=
fun mci ⇒ E mci ∧ mci.(mc_flg) f = b.
Let mc_mem' (mc: machine_config) : int → int := mc.(mc_mem).
Local Coercion mc_mem' : machine_config >-> Funclass.
Record mem_dom_sound {ab_mem ab_num} `{ab_machine_int ab_num} (M: mem_dom ab_mem ab_num) (G: gamma_op ab_mem pre_machine_config) : Prop :=
{ as_adom : adom ab_mem pre_machine_config M.(as_wl) G
; var_sound: ∀ ab:ab_mem, ∀ m: machine_config,
m ∈ γ(ab) → ∀ r, mc_reg m r ∈ γ(M.(var) ab r)
; load_sound: ∀ ab:ab_mem, ∀ m: machine_config,
m ∈ γ(ab) → ∀ a:addr, m(a) ∈ γ(M.(load_single) ab a)
; assign_sound: ∀ ab:ab_mem, ∀ rd v,
Assign (γ ab) rd v ⊆ γ(M.(assign) ab rd v)
; store_sound: ∀ ab:ab_mem, ∀ dst v,
Store (γ ab) dst v ⊆ γ (M.(store_single) ab dst v)
; compare_sound: ∀ ab:ab_mem, ∀ rs rd,
Compare (γ ab) rs rd ⊆ γ(M.(compare) ab rs rd)
; assume_sound: ∀ ab:ab_mem, ∀ f b,
Assume (γ ab) f b ⊆ γ(M.(assume) ab f b)
; init_sound: ∀ (m: memory) (dom: list addr) f r (m': memory),
(∀ a, List.In a dom → m a = m' a) →
(f, r, m') ∈ γ(M.(init) m dom)
}.
Context {ab_mem ab_num: Type} `{D: ab_machine_int ab_num} (M: mem_dom ab_mem ab_num).
Definition assume_mem : ab_mem → addr → int → ab_mem := λ ab a val,
M.(store_single) ab a (const_int val).
Definition AssumeMem (E: 𝒫 machine_config) (dst: addr) (v: int) : 𝒫 machine_config :=
fun mci ⇒ ∃ m,
E {| pc := mci.(pc); mc_flg := mci.(mc_flg)
; mc_reg := mci.(mc_reg); mc_mem := m |}
∧ ∀ a, mci.(mc_mem) a = (m # dst ← v) a.
Context (D_correct: ab_machine_int_correct D)
(G: gamma_op ab_mem pre_machine_config)
(M_correct: mem_dom_sound M G).
Lemma assume_mem_sound (ab:ab_mem) (a: addr) (val: int) :
AssumeMem (γ ab) a val ⊆ γ(assume_mem ab a val).
End MEM_DOM_SOUND.
Require Generate.
Definition value_lt : relation int :=
fun i j ⇒ Int.unsigned i < Int.unsigned j.
Definition value_cmp : int → int → Datatypes.comparison :=
fun x y ⇒ if Int.ltu x y then Lt else if Int.eq x y then Eq else Gt.
Instance OT_ints : OrderedType int := { _eq := eq; _lt := value_lt; _cmp := value_cmp }.
Lemma register_neq_neq : ∀ u v : register,
u ≠ v → u =/= v.
Lemma register_eq_eq : ∀ u v: register, u === v → u = v.
Section AbMachineConfig.
Variable d: Type.
Variable n: ab_machine_int d.
Hypothesis n_correct: ab_machine_int_correct n.
Variable alocs : int_set.
Definition is_aloc (v: addr) : bool :=
if IntSet.mem (proj v) alocs then true else false.
Lemma is_aloc_cases v :
∀ P,
(IntSet.Mem v alocs → P true) →
(¬ IntSet.Mem v alocs → P false) →
P (is_aloc v).
Record ab_machine_config :=
{ ab_flg: (register × register)+⊤
; ab_reg: Map [ register , d ]
; ab_mem: Map [ int, d ]
}.
Definition find_def {A B} `{OrderedType A} `{weak_lattice B} (f: Map [A, B]) (x: A) : B :=
match (f)[x] with
| Some b ⇒ b
| None ⇒ top
end.
Definition find_aloc (m: Map [int, d]) (v: int) : d :=
if is_aloc v
then find_def m v
else ⊤.
Definition find_bot {A B} `{OrderedType A} (f: Map [A, B]) (x: A) : B+⊥ :=
match (f)[x] with
| Some b ⇒ NotBot b
| None ⇒ Bot
end.
Definition ab_machine_state : Type := (ab_machine_config + d)%type.
Definition flag_LE (x y: (register × register)+⊤) : Prop :=
match x, y with
| _, All ⇒ True
| All, Just _ ⇒ False
| Just x', Just y' ⇒ x' = y'
end.
Definition flag_LE_dec x y : { flag_LE x y } + { ¬ flag_LE x y } :=
match x, y with
| _, All ⇒ left I
| All, _ ⇒ right (λ x, x)
| Just x', Just y' ⇒ eq_dec x' y'
end.
Definition map_LE {A B: Type} `{OrderedType A} (leb : B → B → bool) (x y: Map [ A, B ]) : Prop :=
∀ a b, MapsTo a b x → ∃ b', MapsTo a b' y ∧ leb b b' = true.
Definition map_LE_dec {A B: Type} `{OrderedType A} (leb : B → B → bool) (x y: Map [ A, B ]) :
{ map_LE leb x y } + { ¬ map_LE leb x y }.
Definition wmap_LE {A B: Type} `{OrderedType A} `{weak_lattice B} (x y: Map [ A, B ]) : Prop :=
∀ a, find_def x a ⊑ find_def y a = true
∨ (x)[a] = (y)[a] ∧ (x)[a] = None.
Definition wmap_LE_dec {A B: Type} `{OrderedType A} `{weak_lattice B} (x y: Map [ A, B ]) :
{ wmap_LE x y } + { ¬ wmap_LE x y }.
Definition abmc_LE (x y: ab_machine_config) : Prop :=
flag_LE x.(ab_flg) y.(ab_flg)
∧ wmap_LE x.(ab_reg) y.(ab_reg)
∧ wmap_LE x.(ab_mem) y.(ab_mem).
Definition abmc_LE_dec x y : { abmc_LE x y } + { ¬ abmc_LE x y } :=
match flag_LE_dec x.(ab_flg) y.(ab_flg) with
| right NE ⇒ right (λ K, NE (proj1 K))
| left F ⇒
match wmap_LE_dec x.(ab_reg) y.(ab_reg) with
| right NE ⇒ right (λ K, NE (proj1 (proj2 K)))
| left R ⇒
match wmap_LE_dec x.(ab_mem) y.(ab_mem) with
| right NE ⇒ right (λ K, NE (proj2 (proj2 K)))
| left MEM ⇒ left (conj F (conj R MEM))
end
end
end.
Definition abms_LE (x y: ab_machine_state) : Prop :=
match x, y with
| inl x', inl y' ⇒ abmc_LE x' y'
| inr x', inr y' ⇒ leb x' y' = true
| _, _ ⇒ False
end.
Definition abms_LE_dec x y : { abms_LE x y } + { ¬ abms_LE x y }.
Definition flg_join x y :=
if flag_LE_dec x y
then y
else All.
Definition map_join {A B: Type} `{OrderedType A} (join: B → B → B) (f g: Map [ A, B ]) : Map [ A, B ] :=
fold
(fun k y ⇒ add k match (f)[k] with None ⇒ y | ⌊x⌋ ⇒ join x y end)
g
f
.
Definition map_join_get {A B: Type} `{OrderedType A} (join : B → B → B) (f g: Map [ A, B ]) :
∀ k, find_bot (map_join join f g) k = match find_bot f k, find_bot g k with
| NotBot x, NotBot y ⇒ NotBot (join x y)
| NotBot x, Bot ⇒ NotBot x
| Bot, NotBot y ⇒ NotBot y
| Bot, Bot ⇒ Bot
end.
Definition wmap_join {A B: Type} `{OrderedType A} (join: B → B → B) `{weak_lattice B} (f g: Map [ A, B ]) : Map [ A, B ] :=
fold
(fun k y ⇒ let y' := join (find_def f k) y in if ⊤ ⊑ y' then id else add k y')
g
[]
.
Definition wmap_join_get {A B: Type} `{OrderedType A} (join: B → B → B) `{weak_lattice B} (f g: Map [ A, B ]) (q:A) :
find_def (wmap_join join f g) q = match (g)[q] with
| None ⇒ (⊤)
| Some y ⇒ let y' := join (find_def f q) y in
if ⊤ ⊑ y' then ⊤ else y'
end.
Definition abmc_join (x y: ab_machine_config) : ab_machine_config :=
{| ab_flg := flg_join x.(ab_flg) y.(ab_flg)
; ab_reg := wmap_join join x.(ab_reg) y.(ab_reg)
; ab_mem := wmap_join join x.(ab_mem) y.(ab_mem) |}.
Definition abmc_widen (x y: ab_machine_config) : ab_machine_config :=
{| ab_flg := flg_join x.(ab_flg) y.(ab_flg)
; ab_reg := wmap_join widen x.(ab_reg) y.(ab_reg)
; ab_mem := wmap_join widen x.(ab_mem) y.(ab_mem) |}.
Definition abms_join (x y: ab_machine_state) : ab_machine_state+⊤ :=
match x, y with
| inl x', inl y' ⇒ Just (inl (abmc_join x' y'))
| inr x', inr y' ⇒ Just (inr (join x' y'))
| _, _ ⇒ All
end.
Definition flg_gamma (x: (register × register)+⊤) (mci: pre_machine_config) : Prop :=
match x with
| Just (r1, r2) ⇒ ∀ f, pmc_flg mci f = eval_flag (pmc_reg mci r2) (pmc_reg mci r1) f
| All ⇒ True
end.
Definition map_gamma {A B C: Type} `{OrderedType A} `{weak_lattice B} `{gamma_op B C} (x: Map [ A, B ]) (v: A → C): Prop :=
∀ k, γ (find_bot x k) (v k).
Lemma map_join_sound {A B C: Type} `{OrderedType A} `{WL:weak_lattice B}
`{G:gamma_op B C} `{adom B C WL G} :
∀ P, Proper (_eq ==> eq) P →
∀ x y: Map [ A, B ],
map_gamma x P ∨ map_gamma y P → map_gamma (map_join join x y) P.
Definition wmap_gamma {A B C: Type} `{OrderedType A} `{weak_lattice B} `{gamma_op B C} (x: Map [ A, B ]) (v: A → C): Prop :=
∀ k, γ (find_def x k) (v k).
Lemma wmap_join_sound {A B C: Type} `{OrderedType A} `{WL: weak_lattice B} `{G: gamma_op B C} `{AD: adom _ _ WL G} (x y: Map [ A, B ]) :
∀ P, Proper (_eq ==> eq) P →
wmap_gamma x P ∨ wmap_gamma y P → wmap_gamma (wmap_join join x y) P.
Definition gamma_mem {C: Type} `{G: gamma_op d C} (x: Map [ int, d ]) (v: int → C) : Prop :=
∀ k, v(k) ∈ γ(find_aloc x k).
Lemma gamma_mem_sound {C: Type} `{G: gamma_op d C} `{AD: adom _ _ _ G} (x y: Map [ int, d ]) :
(gamma_mem x ∪ gamma_mem y) ⊆ gamma_mem (wmap_join join x y).
Instance abmc_gamma : gamma_op ab_machine_config pre_machine_config :=
λ x mc,
flg_gamma x.(ab_flg) mc
∧ wmap_gamma x.(ab_reg) (pmc_reg mc)
∧ gamma_mem x.(ab_mem) (pmc_mem mc).
Definition abms_gamma (x: ab_machine_state) (m: machine_state) : Prop :=
match x, m with
| inl x', Running m' ⇒ m' ∈ γ(x')
| inr x', Halted m' ⇒ γ x' m'
| _, _ ⇒ False
end.
Definition map_to_string {A B: Type} `{OrderedType A}
(A_to_string : A → string) (B_to_string : B → string)
(m: Map [A,B]) : string :=
(fold
(fun k v acc ⇒ A_to_string k ++ " ↦ " ++ B_to_string v ++ "; " ++ acc)
m
""
)%string.
Instance abmc_toString `{ToString d} : ToString ab_machine_config :=
{ to_string x :=
("⟨" ++
match x.(ab_flg) with
| All ⇒ ""
| Just (r1,r2) ⇒ "(" ++ string_of_reg r1 ++ ", " ++ string_of_reg r2 ++ ")"
end ++
map_to_string string_of_reg to_string x.(ab_reg) ++
map_to_string string_of_int to_string x.(ab_mem) ++
"⟩"
)%string
}.
Definition ab_machine_config_pl : pre_lattice ab_machine_config :=
{| pl_leb x y := abmc_LE_dec x y
; pl_join x y := Just (abmc_join x y)
; pl_widen x y := Just (abmc_widen x y)
|}.
Lemma ab_machine_config_pl_sound : pre_lattice_spec ab_machine_config_pl abmc_gamma.
Hint Resolve as_int_adom.
Definition invalidate_flag (r:register) f :=
match f with
| All ⇒ All
| Just (r1, r2) ⇒ if eq_dec r r1 then All else if eq_dec r r2 then All else f
end.
Lemma invalidate_flag_preserve : ∀ {R F p1 p2},
invalidate_flag R F = Just (p1,p2) →
R ≠ p1 ∧ R ≠ p2.
Definition ab_store_strong (m: Map [ addr, d ]) (a: addr) (v: d) : Map [ addr, d ] :=
if is_aloc a
then if ⊤ ⊑ v
then remove a m
else (m)[a <- v]
else m.
Definition abmc_init (m: memory) (dom: list int) : Map [ int, d ] :=
List.fold_left (fun a i ⇒ (a)[ i <- const_int (m i) ]) dom [].
Definition ab_machine_config_mem_dom : mem_dom (ab_machine_config+⊤) d :=
{|
as_wl := weak_lattice_of_pre_lattice ab_machine_config_pl
; var x := match x with
| Just x' ⇒ find_def x'.(ab_reg)
| _ ⇒ fun _ ⇒ top
end
; load_single x := match x with
| Just x' ⇒ find_aloc x'.(ab_mem)
| _ ⇒ fun _ ⇒ top
end
; compare x rs rd := top_lift (λ x', {| ab_flg := Just (rs, rd)
; ab_reg := x'.(ab_reg)
; ab_mem := x'.(ab_mem) |}) x
; assume x f b :=
match x with
| Just x' ⇒
match x'.(ab_flg) with
| Just (Ru, Rv) ⇒
let u := find_def x'.(ab_reg) Ru in
let v := find_def x'.(ab_reg) Rv in
let op := match f with FLE ⇒ Cle | FLT ⇒ Clt | FEQ ⇒ Ceq end in
let v'u' := backward_int_binop (OpCmp op) v u
(const_int (IntervalDomain.Interval.of_bool b)) in
match v'u' with
| (NotBot v', NotBot u') ⇒
NotBot (Just {| ab_flg := x'.(ab_flg)
; ab_reg := (x'.(ab_reg)) [ Ru <- u' ] [ Rv <- v' ]
; ab_mem := x'.(ab_mem) |})
| _ ⇒ Bot
end
| All ⇒ NotBot x
end
| All ⇒ NotBot x
end
; assign x := match x with
| Just x' ⇒ fun r v ⇒ Just {| ab_flg := invalidate_flag r x'.(ab_flg)
; ab_reg := (x'.(ab_reg)) [ r <- v ]
; ab_mem := x'.(ab_mem) |}
| _ ⇒ fun _ _ ⇒ All
end
; store_single x a v := do_top x' <- x;
Just {| ab_flg := x'.(ab_flg)
; ab_reg := x'.(ab_reg)
; ab_mem := ab_store_strong x'.(ab_mem) a v |}
; init m dom := Just {| ab_flg := All; ab_reg := []; ab_mem := abmc_init m dom |}
|}.
Lemma ab_machine_config_mem_dom_sound : mem_dom_sound ab_machine_config_mem_dom (toplift_gamma abmc_gamma).
End AbMachineConfig.