Library GotoAnalysis
Require Import
Coqlib Utf8 String
Integers TreeAl Util
Goto GotoSem AbGoto
LatticeSignatures AdomLib
AbMachineNonrel.
Require
DebugAbMachineNonrel
Containers.Maps
CompleteLattice.
Set Implicit Arguments.
Section ONMAPS.
Import Containers.Maps.
Context {A B: Type} `{OT:OrderedType A}.
Definition map_any_fun (m: Map [ A, B ]) : option (A × B) :=
fold (fun k v _ ⇒ Some (k,v)) m None.
Lemma map_any_fun_spec (m: Map [A, B]) :
match map_any_fun m with
| Some kv ⇒ MapsTo (fst kv) (snd kv) m
| None ⇒ Empty m
end.
Definition map_any (m: Map [A, B]) : { kv : A × B | MapsTo (fst kv) (snd kv) m } + { Empty m } :=
match map_any_fun m as res return match res with
| Some kv ⇒ MapsTo (fst kv) (snd kv) m
| None ⇒ Empty m end → _ with
| Some kv ⇒ fun H ⇒ inleft (exist _ kv H)
| None ⇒ inright
end (map_any_fun_spec m).
End ONMAPS.
Section GOTOANALYSIS.
Variables ab_mc d: Type.
Variables (D: ab_machine_int d) (T: mem_dom ab_mc d).
Hypothesis D_correct : ab_machine_int_correct D.
Inductive ab_post_res :=
| Run (pp:addr) (m:ab_mc)
| Hlt (res: d)
| GiveUp.
Definition abstract_op (op: int_binary_operation) (m: ab_mc) (rs rd: register) : ab_mc+⊥ :=
do_bot v <- forward_int_binop (ab_machine_int := D) op (var T m rs) (var T m rd);
NotBot (assign T m rd v).
Let abstract_cond (f: flag) (m: ab_mc) : ab_mc+⊥ := assume T m f true.
Let abstract_ncond (f: flag) (m: ab_mc) : ab_mc+⊥ := assume T m f false.
Variable max_deref: N.
Definition concretize_with_care (v:d) : IntSet.fint_set :=
match size v with
| Just sz ⇒
if N.leb sz max_deref
then concretize v
else All
| All ⇒ All
end.
Lemma concretize_with_care_two_cases (v:d) :
concretize_with_care v = All
∨ ∃ l, concretize_with_care v = Just l ∧ concretize v = Just l.
Definition load_many_aux (m: ab_mc) (addr_set: IntSet.int_set) : d+⊥ :=
IntSet.fold (λ acc addr, acc ⊔ NotBot (T.(load_single) m addr)) addr_set Bot.
Lemma load_many_aux_sound (m: ab_mc) (addr_set: IntSet.int_set) :
∀ a: int,
a ∈ γ (Just addr_set) →
γ (NotBot (T.(load_single) m a)) ⊆ γ (load_many_aux m addr_set).
Hint Resolve as_int_adom.
Definition load_many (m: ab_mc) (a: d) : d+⊥ :=
match concretize_with_care a with
| Just addr_set ⇒ load_many_aux m addr_set
| All ⇒ NotBot top
end.
Local Instance T_as_wl : weak_lattice ab_mc := T.(as_wl).
Definition store_many (m: ab_mc) (a: d) (v: d) : ab_mc :=
match concretize_with_care a with
| Just addr_set ⇒
union_list_map (λ a : addr, T.(store_single) m a v) m join (IntSet.as_list addr_set)
| All ⇒ top
end.
Definition abstract_goto_ind (m: ab_mc) (v: d) : list ab_post_res :=
match concretize_with_care v with
| Just tgt ⇒
IntSet.fold
(λ acc addr,
Run addr m :: acc
) tgt nil
| All ⇒ GiveUp :: nil
end.
Lemma abstract_goto_ind_sound m v :
abstract_goto_ind m v = GiveUp :: nil
∨ (∀ x,
x ∈ γ(v) → In (Run x m) (abstract_goto_ind m v)).
Definition bot_cons {A B: Type} (a: botlift A) (f: A → B) (l: list B) : list B :=
match a with
| NotBot a' ⇒ f a' :: l
| Bot ⇒ l
end.
Lemma In_bot_cons_right {A B} (a: A+⊥) (f: A → B) (l: list B) :
∀ b, In b l → In b (bot_cons a f l).
Lemma bot_cons_nil_r {A B} (a: A+⊥) (f: A → B) (l: list B) :
bot_cons a f l = nil → l = nil.
Local Open Scope goto_scope.
Definition abstract_goto_cond (f: flag) (m: ab_mc) (pp: int) (tgt: d): list ab_post_res :=
bot_cons (abstract_ncond f m) (Run (pp + 2))
match abstract_cond f m with
| NotBot m' ⇒
match concretize_with_care tgt with
| Just tgt ⇒
IntSet.fold
(λ acc addr,
bot_cons (abstract_cond f (assume_mem T m' (pp+1) addr))
(Run addr)
acc
) tgt nil
| All ⇒ GiveUp :: nil
end
| Bot ⇒ nil
end.
Lemma abstract_goto_cond_sound f m pp tgt :
match abstract_ncond f m with
| Bot ⇒ True
| NotBot m' ⇒ In (Run (pp + 2) m') (abstract_goto_cond f m pp tgt)
end
∧
match abstract_cond f m with
| Bot ⇒ True
| NotBot m' ⇒
In GiveUp (abstract_goto_cond f m pp tgt) ∨
(∀ v, v ∈ γ(tgt) →
match abstract_cond f (assume_mem T m' (pp+1) v) with
| Bot ⇒ True
| NotBot m'' ⇒ In (Run v m'') (abstract_goto_cond f m pp tgt)
end
)
end.
Inductive ab_instruction :=
Coqlib Utf8 String
Integers TreeAl Util
Goto GotoSem AbGoto
LatticeSignatures AdomLib
AbMachineNonrel.
Require
DebugAbMachineNonrel
Containers.Maps
CompleteLattice.
Set Implicit Arguments.
Section ONMAPS.
Import Containers.Maps.
Context {A B: Type} `{OT:OrderedType A}.
Definition map_any_fun (m: Map [ A, B ]) : option (A × B) :=
fold (fun k v _ ⇒ Some (k,v)) m None.
Lemma map_any_fun_spec (m: Map [A, B]) :
match map_any_fun m with
| Some kv ⇒ MapsTo (fst kv) (snd kv) m
| None ⇒ Empty m
end.
Definition map_any (m: Map [A, B]) : { kv : A × B | MapsTo (fst kv) (snd kv) m } + { Empty m } :=
match map_any_fun m as res return match res with
| Some kv ⇒ MapsTo (fst kv) (snd kv) m
| None ⇒ Empty m end → _ with
| Some kv ⇒ fun H ⇒ inleft (exist _ kv H)
| None ⇒ inright
end (map_any_fun_spec m).
End ONMAPS.
Section GOTOANALYSIS.
Variables ab_mc d: Type.
Variables (D: ab_machine_int d) (T: mem_dom ab_mc d).
Hypothesis D_correct : ab_machine_int_correct D.
Inductive ab_post_res :=
| Run (pp:addr) (m:ab_mc)
| Hlt (res: d)
| GiveUp.
Definition abstract_op (op: int_binary_operation) (m: ab_mc) (rs rd: register) : ab_mc+⊥ :=
do_bot v <- forward_int_binop (ab_machine_int := D) op (var T m rs) (var T m rd);
NotBot (assign T m rd v).
Let abstract_cond (f: flag) (m: ab_mc) : ab_mc+⊥ := assume T m f true.
Let abstract_ncond (f: flag) (m: ab_mc) : ab_mc+⊥ := assume T m f false.
Variable max_deref: N.
Definition concretize_with_care (v:d) : IntSet.fint_set :=
match size v with
| Just sz ⇒
if N.leb sz max_deref
then concretize v
else All
| All ⇒ All
end.
Lemma concretize_with_care_two_cases (v:d) :
concretize_with_care v = All
∨ ∃ l, concretize_with_care v = Just l ∧ concretize v = Just l.
Definition load_many_aux (m: ab_mc) (addr_set: IntSet.int_set) : d+⊥ :=
IntSet.fold (λ acc addr, acc ⊔ NotBot (T.(load_single) m addr)) addr_set Bot.
Lemma load_many_aux_sound (m: ab_mc) (addr_set: IntSet.int_set) :
∀ a: int,
a ∈ γ (Just addr_set) →
γ (NotBot (T.(load_single) m a)) ⊆ γ (load_many_aux m addr_set).
Hint Resolve as_int_adom.
Definition load_many (m: ab_mc) (a: d) : d+⊥ :=
match concretize_with_care a with
| Just addr_set ⇒ load_many_aux m addr_set
| All ⇒ NotBot top
end.
Local Instance T_as_wl : weak_lattice ab_mc := T.(as_wl).
Definition store_many (m: ab_mc) (a: d) (v: d) : ab_mc :=
match concretize_with_care a with
| Just addr_set ⇒
union_list_map (λ a : addr, T.(store_single) m a v) m join (IntSet.as_list addr_set)
| All ⇒ top
end.
Definition abstract_goto_ind (m: ab_mc) (v: d) : list ab_post_res :=
match concretize_with_care v with
| Just tgt ⇒
IntSet.fold
(λ acc addr,
Run addr m :: acc
) tgt nil
| All ⇒ GiveUp :: nil
end.
Lemma abstract_goto_ind_sound m v :
abstract_goto_ind m v = GiveUp :: nil
∨ (∀ x,
x ∈ γ(v) → In (Run x m) (abstract_goto_ind m v)).
Definition bot_cons {A B: Type} (a: botlift A) (f: A → B) (l: list B) : list B :=
match a with
| NotBot a' ⇒ f a' :: l
| Bot ⇒ l
end.
Lemma In_bot_cons_right {A B} (a: A+⊥) (f: A → B) (l: list B) :
∀ b, In b l → In b (bot_cons a f l).
Lemma bot_cons_nil_r {A B} (a: A+⊥) (f: A → B) (l: list B) :
bot_cons a f l = nil → l = nil.
Local Open Scope goto_scope.
Definition abstract_goto_cond (f: flag) (m: ab_mc) (pp: int) (tgt: d): list ab_post_res :=
bot_cons (abstract_ncond f m) (Run (pp + 2))
match abstract_cond f m with
| NotBot m' ⇒
match concretize_with_care tgt with
| Just tgt ⇒
IntSet.fold
(λ acc addr,
bot_cons (abstract_cond f (assume_mem T m' (pp+1) addr))
(Run addr)
acc
) tgt nil
| All ⇒ GiveUp :: nil
end
| Bot ⇒ nil
end.
Lemma abstract_goto_cond_sound f m pp tgt :
match abstract_ncond f m with
| Bot ⇒ True
| NotBot m' ⇒ In (Run (pp + 2) m') (abstract_goto_cond f m pp tgt)
end
∧
match abstract_cond f m with
| Bot ⇒ True
| NotBot m' ⇒
In GiveUp (abstract_goto_cond f m pp tgt) ∨
(∀ v, v ∈ γ(tgt) →
match abstract_cond f (assume_mem T m' (pp+1) v) with
| Bot ⇒ True
| NotBot m'' ⇒ In (Run v m'') (abstract_goto_cond f m pp tgt)
end
)
end.
Inductive ab_instruction :=
arithmetic
| AICst (v:d) (dst:register)
| AIBinop (op: int_binary_operation) (src dst: register)
| AICmp (src dst: register)
| AIBinop (op: int_binary_operation) (src dst: register)
| AICmp (src dst: register)
memory
control
| AIGoto (tgt: d)
| AIGotoCond (f: flag) (tgt: d)
| AIGotoInd (r: register)
| AISkip
| AIHalt (r: register)
.
Definition abstract_decode_instr_at (m: ab_mc) (base: int) (i: int) : option (ab_instruction × nat) :=
match split_instruction i with
| (0, 0, src, 0) ⇒ do_opt rs <- decode_register src; Some (AIHalt rs, 1%nat)
| (1, 0, 0, 0) ⇒ Some (AISkip, 1%nat)
| (2, 0, src, 0) ⇒ do_opt rs <- decode_register src; Some (AIGotoInd rs, 1%nat)
| (3, flg, 0, 0) ⇒
do_opt f <- decode_flag flg;
Some (AIGotoCond f (T.(load_single) m (base+1)), 2%nat)
| (4, 0, 0, 0) ⇒ Some (AIGoto (T.(load_single) m (base+1)), 2%nat)
| (5, 0, src, dst) ⇒ do_opt rs <- decode_register src;
do_opt rd <- decode_register dst;
Some (AIStore rs rd, 1%nat)
| (6, 0, src, dst) ⇒ do_opt rs <- decode_register src;
do_opt rd <- decode_register dst;
Some (AILoad rs rd, 1%nat)
| (7, 0, src, dst) ⇒ do_opt rs <- decode_register src;
do_opt rd <- decode_register dst;
Some (AICmp rs rd, 1%nat)
| (8, o, src, dst) ⇒ do_opt op <- decode_binop o;
do_opt rs <- decode_register src;
do_opt rd <- decode_register dst;
Some (AIBinop op rs rd, 1%nat)
| (9, 0, 0, dst) ⇒ do_opt rd <- decode_register dst;
Some (AICst (T.(load_single) m (base+1)) rd, 2%nat)
| _ ⇒ None
end.
Definition abstract_decode_at (pp:int) (ab:ab_mc) : (list (ab_instruction × nat))+⊤ :=
do_top instr <- concretize_with_care (T.(load_single) ab pp);
Just (IntSet.fold (λ acc inst,
match abstract_decode_instr_at
ab
pp
inst with
| Some i ⇒ i :: acc
| None ⇒ acc
end)
instr nil).
Lemma abstract_decode_at_inv (pp: int) (ab:ab_mc) l :
abstract_decode_at pp ab = Just l →
∀ (instr : int) i,
abstract_decode_instr_at ab pp instr = Some i →
instr ∈ γ ((T.(load_single) ab pp):d) →
List.In i l.
Definition ab_post_single (m: ab_mc) (pp: addr) (instr:ab_instruction × nat) : list ab_post_res :=
match instr with
| (AIHalt rs, z) ⇒ Hlt (T.(var) m rs) :: nil
| (AISkip, z) ⇒ Run (pp + z) m :: nil
| (AIGotoInd rs, z) ⇒ abstract_goto_ind m (T.(var) m rs)
| (AIGotoCond f v, z) ⇒ abstract_goto_cond f m pp v
| (AIGoto v, z) ⇒ abstract_goto_ind m v
| (AIStore rs rd, z) ⇒ Run (pp + z) (store_many m (T.(var) m rd) (T.(var) m rs)) :: nil
| (AILoad rs rd, z) ⇒
match load_many m (T.(var) m rs) with
| NotBot v ⇒ Run (pp + z) (T.(assign) m rd v) :: nil
| Bot ⇒ nil
end
| (AICmp rs rd, z) ⇒ Run (pp + z) (T.(compare) m rs rd ) :: nil
| (AIBinop op rs rd, z) ⇒ bot_cons (abstract_op op m rs rd) (Run (pp + z)) nil
| (AICst v rd, z) ⇒ Run (pp + z) (T.(assign) m rd v) :: nil
end.
Definition ab_post_many (pp: addr) (m:ab_mc) : list ab_post_res :=
match abstract_decode_at pp m with
| Just instr ⇒ flat_map (ab_post_single m pp) instr
| All ⇒ GiveUp :: nil
end.
| AIGotoCond (f: flag) (tgt: d)
| AIGotoInd (r: register)
| AISkip
| AIHalt (r: register)
.
Definition abstract_decode_instr_at (m: ab_mc) (base: int) (i: int) : option (ab_instruction × nat) :=
match split_instruction i with
| (0, 0, src, 0) ⇒ do_opt rs <- decode_register src; Some (AIHalt rs, 1%nat)
| (1, 0, 0, 0) ⇒ Some (AISkip, 1%nat)
| (2, 0, src, 0) ⇒ do_opt rs <- decode_register src; Some (AIGotoInd rs, 1%nat)
| (3, flg, 0, 0) ⇒
do_opt f <- decode_flag flg;
Some (AIGotoCond f (T.(load_single) m (base+1)), 2%nat)
| (4, 0, 0, 0) ⇒ Some (AIGoto (T.(load_single) m (base+1)), 2%nat)
| (5, 0, src, dst) ⇒ do_opt rs <- decode_register src;
do_opt rd <- decode_register dst;
Some (AIStore rs rd, 1%nat)
| (6, 0, src, dst) ⇒ do_opt rs <- decode_register src;
do_opt rd <- decode_register dst;
Some (AILoad rs rd, 1%nat)
| (7, 0, src, dst) ⇒ do_opt rs <- decode_register src;
do_opt rd <- decode_register dst;
Some (AICmp rs rd, 1%nat)
| (8, o, src, dst) ⇒ do_opt op <- decode_binop o;
do_opt rs <- decode_register src;
do_opt rd <- decode_register dst;
Some (AIBinop op rs rd, 1%nat)
| (9, 0, 0, dst) ⇒ do_opt rd <- decode_register dst;
Some (AICst (T.(load_single) m (base+1)) rd, 2%nat)
| _ ⇒ None
end.
Definition abstract_decode_at (pp:int) (ab:ab_mc) : (list (ab_instruction × nat))+⊤ :=
do_top instr <- concretize_with_care (T.(load_single) ab pp);
Just (IntSet.fold (λ acc inst,
match abstract_decode_instr_at
ab
pp
inst with
| Some i ⇒ i :: acc
| None ⇒ acc
end)
instr nil).
Lemma abstract_decode_at_inv (pp: int) (ab:ab_mc) l :
abstract_decode_at pp ab = Just l →
∀ (instr : int) i,
abstract_decode_instr_at ab pp instr = Some i →
instr ∈ γ ((T.(load_single) ab pp):d) →
List.In i l.
Definition ab_post_single (m: ab_mc) (pp: addr) (instr:ab_instruction × nat) : list ab_post_res :=
match instr with
| (AIHalt rs, z) ⇒ Hlt (T.(var) m rs) :: nil
| (AISkip, z) ⇒ Run (pp + z) m :: nil
| (AIGotoInd rs, z) ⇒ abstract_goto_ind m (T.(var) m rs)
| (AIGotoCond f v, z) ⇒ abstract_goto_cond f m pp v
| (AIGoto v, z) ⇒ abstract_goto_ind m v
| (AIStore rs rd, z) ⇒ Run (pp + z) (store_many m (T.(var) m rd) (T.(var) m rs)) :: nil
| (AILoad rs rd, z) ⇒
match load_many m (T.(var) m rs) with
| NotBot v ⇒ Run (pp + z) (T.(assign) m rd v) :: nil
| Bot ⇒ nil
end
| (AICmp rs rd, z) ⇒ Run (pp + z) (T.(compare) m rs rd ) :: nil
| (AIBinop op rs rd, z) ⇒ bot_cons (abstract_op op m rs rd) (Run (pp + z)) nil
| (AICst v rd, z) ⇒ Run (pp + z) (T.(assign) m rd v) :: nil
end.
Definition ab_post_many (pp: addr) (m:ab_mc) : list ab_post_res :=
match abstract_decode_at pp m with
| Just instr ⇒ flat_map (ab_post_single m pp) instr
| All ⇒ GiveUp :: nil
end.
Flow-sensitive analysis.
Import Containers.Maps.
Record analysis_state :=
{ worklist : list int
; result_fs : Map [ int, ab_mc ]
; result_hlt: d+⊥
}.
Notation result_at_run := (fun (E:analysis_state) (pp:int) ⇒ find_bot E.(result_fs) pp).
Local Instance lifted_mem_wl : weak_lattice (ab_mc+⊥) := lift_bot_wl T.(as_wl).
Let push (n:int) wl :=
if List.in_dec LatticeSignatures.eq_dec n wl
then wl else n :: wl.
Let bot_set m (x: int) (v: ab_mc+⊥) :=
match v with
| NotBot v' ⇒ (m)[ x <- v' ]
| Bot ⇒ MapInterface.remove x m
end.
Definition propagate (widenp:bool) (E:analysis_state) (n: ab_post_res) : analysis_state+⊤ :=
match n with
| GiveUp ⇒ All
| Run n' ab ⇒
let old := result_at_run E n' in
let new := (if widenp then widen else join) old (NotBot ab) in
if new ⊑ old
then Just E
else Just {| worklist := push n' E.(worklist)
; result_fs := bot_set E.(result_fs) n' new
; result_hlt := E.(result_hlt) |}
| Hlt res ⇒
let old := E.(result_hlt) in
let new := (if widenp then widen else join) old (NotBot res) in
if new ⊑ old
then Just E
else Just {| worklist := E.(worklist)
; result_fs := E.(result_fs)
; result_hlt := new
|}
end.
Variable widen_oracle : int → ab_post_res → bool.
Local Open Scope top_monad_scope.
Definition analysis_step (E:analysis_state) : analysis_state+⊤ :=
match worklist E with
| nil ⇒ Just E
| n :: l ⇒
match result_at_run E n with
| NotBot ab_mc ⇒
let next := ab_post_many n ab_mc in
List.fold_left
(λ acc res, do E' <- acc; propagate (widen_oracle n res) E' res)
next
(Just {| worklist := l
; result_fs := E.(result_fs)
; result_hlt:= E.(result_hlt) |})
| Bot ⇒ All
end
end.
Definition is_final (E: analysis_state) : bool :=
match worklist E with nil ⇒ true | _ :: _ ⇒ false end.
Fixpoint analysis_loop (fuel: nat) (E: analysis_state) : analysis_state+⊤ :=
match fuel with
| O ⇒ Just E
| S fuel' ⇒
do E' <- analysis_step E;
if is_final E' then Just E' else analysis_loop fuel' E'
end.
Definition analysis_init I : analysis_state :=
{| worklist := Int.zero :: nil
; result_fs := ([])[ Int.zero <- I ]
; result_hlt := Bot
|}.
Definition analysis (P: memory) (dom: list int) n : analysis_state+⊤ :=
analysis_loop n (analysis_init (init T P dom)).
End GOTOANALYSIS.
Section VALIDATE.
Variables ab_mc d: Type.
Context (D: ab_machine_int d) (T: mem_dom ab_mc d) (G: gamma_op ab_mc pre_machine_config).
Hypotheses (D_correct: ab_machine_int_correct D) (T_sound: mem_dom_sound T G).
Variable max_deref : N.
Import Containers.Maps.
Local Instance t_wl : weak_lattice ab_mc := T.(as_wl).
Local Instance ltd_wl : weak_lattice ((ab_mc × d)+⊥) := lift_bot_wl (WProd.make_wl T.(as_wl) _).
Definition AbEnv : Type := (Map [int, ab_mc] × d+⊥)%type.
Definition ab_env_leb (x y: AbEnv) : bool :=
match x, y with
| (xr,xh), (yr,yh) ⇒ map_LE_dec leb xr yr && xh ⊑ yh
end.
Definition ab_env_join (x y: AbEnv) : AbEnv :=
match x, y with
| (xr,xh), (yr, yh) ⇒ (map_join join xr yr, xh ⊔ yh)
end.
Definition ab_env_widen (x y: AbEnv) : AbEnv :=
match x, y with
| (xr,xh), (yr, yh) ⇒ (map_join widen xr yr, xh ⊔ yh)
end.
Definition fs_pl : pre_lattice AbEnv :=
{| pl_leb := ab_env_leb
; pl_join x y := Just (ab_env_join x y)
; pl_widen x y := Just (ab_env_widen x y)
|}.
Instance fs_gamma : gamma_op AbEnv machine_state :=
λ x, let '(xr, xh) := x in
λ m,
match m with
| ⌈res⌉ ⇒ res ∈ γ(xh)
| Running mci ⇒ mci ∈ γ (gamma_op := lift_gamma _) (find_bot xr mci.(pc))
end.
Lemma fs_pl_sound : pre_lattice_spec fs_pl fs_gamma.
Hint Resolve as_int_adom.
Definition fs_adom : adom _ _ (weak_lattice_of_pre_lattice fs_pl) _ := adom_of_pre_lattice fs_pl_sound.
Definition abEnv_of_analysis_state (E: analysis_state ab_mc d) : AbEnv :=
(E.(result_fs), E.(result_hlt)).
Instance instr_gamm : gamma_op (ab_instruction d) instruction :=
λ a i,
match a, i with
| AICst v r, ICst v' r' ⇒ v' ∈ γ(v) ∧ r = r'
| AIBinop op rs rd, IBinop op' rs' rd' ⇒ op = op' ∧ rs = rs' ∧ rd = rd'
| AICmp rs rd, ICmp rs' rd' ⇒ rs = rs' ∧ rd = rd'
| AILoad rs rd, ILoad rs' rd' ⇒ rs = rs' ∧ rd = rd'
| AIStore rs rd, IStore rs' rd' ⇒ rs = rs' ∧ rd = rd'
| AIGoto v, IGoto v' ⇒ v' ∈ γ(v)
| AIGotoCond f v, IGotoCond f' v' ⇒ f' = f ∧ v' ∈ γ(v)
| AIGotoInd rs, IGotoInd rs' ⇒ rs = rs'
| AISkip, ISkip ⇒ True
| AIHalt rs, IHalt rs' ⇒ rs = rs'
| _, _ ⇒ False
end.
Local Instance ListAsSet E E' `{G: gamma_op E E'} : gamma_op (list E) E' :=
λ l e', ∃ e, List.In e l ∧ e' ∈ γ(e).
Remark flat_map_gamma {F E E'} `{gamma_op E E'} :
∀ f : F → list E,
∀ l : list F,
∀ x : E',
(∃ y : F, List.In y l ∧ x ∈ γ(f(y))) →
x ∈ γ (flat_map f l).
Local Instance ProdGamma A B A' B' `{Ga: gamma_op A A'}
`{Gb: gamma_op B B'} : gamma_op (A × B) (A' × B') :=
λ ab a'b',
let (a, b) := ab in let (a', b') := a'b' in
a' ∈ γ(a) ∧ b' ∈ γ(b).
Local Instance IdGamma : gamma_op nat nat := @eq nat.
Local Instance OptGamm {A B: Type} `{gamma_op A B} : gamma_op A (option B) :=
λ a b', match b' with Some b ⇒ b ∈ γ(a) | None ⇒ True end.
Lemma abstract_decode_at_sound :
∀ (m:machine_config) (ab:ab_mc) (pp: int),
m ∈ γ(ab) →
decode_from m.(mc_mem) pp ∈ γ(abstract_decode_at D T max_deref pp ab).
Lemma abstract_decode_instr_at_complete ab mci m pp :
mci ∈ γ(ab) →
m = mci.(mc_mem) →
decode_from m pp = None →
abstract_decode_instr_at T ab pp (m pp) = None.
Local Instance AbPostResGamma : gamma_op (ab_post_res ab_mc d) machine_state :=
λ r ms,
match r, ms with
| Run pp' ab, ⟨pp, f, r, m⟩ ⇒ pp = pp' ∧ {| pc := pp; mc_flg := f; mc_reg := r; mc_mem := m |} ∈ γ(ab)
| Hlt v', ⌈v⌉ ⇒ v ∈ γ(v')
| GiveUp, _ ⇒ True
| _, _ ⇒ False
end.
Local Open Scope goto_scope.
Local Coercion Running : machine_config >-> machine_state.
Lemma ab_post_many_correct (m: machine_config) (m': machine_state) (ab: ab_mc) :
m ∈ γ(ab) →
m =~> m' →
m' ∈ γ(ab_post_many D T max_deref m.(pc) ab).
Corollary ab_post_many_correct' m m' (ab: ab_mc) :
m ∈ γ(ab) → Running m =~> m' →
∃ r, List.In r (ab_post_many D T max_deref m.(pc) ab) ∧
m' ∈ γ(r).
Definition validate_fixpoint (P: memory) (dom: list addr) (E: AbEnv) : bool :=
NotBot (init T P dom) ⊑ find_bot (fst E) Int.zero
&&
MF.for_all
(fun (pp: addr) (ab: ab_mc) ⇒
List.forallb
(fun abr : ab_post_res ab_mc d ⇒
match abr with
| Run pp' ab' ⇒ NotBot ab' ⊑ find_bot (fst E) pp'
| Hlt res ⇒ NotBot res ⊑ snd E
| GiveUp ⇒ false
end
)
(ab_post_many D T max_deref pp ab)
)
(fst E).
Theorem validate_correct : ∀ P dom E,
validate_fixpoint P dom E = true →
⟦ P ⟧ ⊆ γ(E).
Definition check_safety (E': AbEnv) : bool :=
let run := fst E' in
MF.for_all
(λ pp mc,
match concretize_with_care D max_deref (T.(load_single) mc pp) with
| All ⇒ false
| Just ab_instr ⇒
IntSet.forallb
(λ i, match abstract_decode_instr_at T mc pp (Int.repr i) with
| Some _ ⇒ true
| None ⇒ false
end)
ab_instr
end)
run.
Lemma check_safety_not_stuck (E': AbEnv) :
check_safety E' = true →
∀ s, γ(E') s → ¬ stuck s.
Theorem check_safety_sound: ∀ P E, ⟦ P ⟧ ⊆ γ(E) →
check_safety E = true → safe P.
Corollary safety_check P dom E:
validate_fixpoint P dom E = true →
check_safety E = true →
safe P.
End VALIDATE.
Section ValuePartitionning.
Variables ab_mc d: Type.
Variables (D: ab_machine_int d) (T: mem_dom ab_mc d) (G: gamma_op ab_mc pre_machine_config).
Hypothesis D_correct : ab_machine_int_correct D.
Hypothesis T_correct : mem_dom_sound T G.
Local Instance vp_t_wl : weak_lattice ab_mc := T.(as_wl).
Local Instance vp_ltd_wl : weak_lattice ((ab_mc × d)+⊥) := lift_bot_wl (WProd.make_wl T.(as_wl) _).
Variable δ : ab_mc → int.
Variable max_deref : N.
Import Containers.Maps.
Record vpstate :=
{ vp_worklist : list (int × int)
; vp_run : Map [ int, Map [ int, ab_mc ] ]
; vp_hlt : d+⊥
}.
Definition vpInit (I: ab_mc) : vpstate :=
let v := δ I in
{| vp_worklist := (Int.zero, v)::nil
; vp_run := ([])[ Int.zero <- ([])[ v <- I ] ]
; vp_hlt := Bot
|}.
Inductive vpresult := VP_top | VP_fix (e: vpstate) | VP_cont (e: vpstate).
Let push (n:int × int) wl :=
if List.in_dec LatticeSignatures.eq_dec n wl
then wl else n :: wl.
Definition vpPropagate (widenp: bool) (succ: ab_post_res ab_mc d) (E: vpstate) : vpstate+⊤ :=
match succ with
| GiveUp ⇒ All
| Run pp ab ⇒
let v := δ ab in
let old := do_bot m <- find_bot E.(vp_run) pp; find_bot m v in
let new := (if widenp then widen else join) old (NotBot ab) in
if new ⊑ old
then Just E
else
match new with
| Bot ⇒ DebugAbMachineNonrel.print "anomaly: vpPropagate" (Just E)
| NotBot new' ⇒
let v' := δ new' in
let m' := match find_bot E.(vp_run) pp with NotBot m' ⇒ m' | Bot ⇒ [] end in
Just {| vp_worklist := push (pp, v') E.(vp_worklist)
; vp_run := (E.(vp_run)) [ pp <- (m') [ v' <- new' ] ]
; vp_hlt := E.(vp_hlt) |}
end
| Hlt res ⇒
let old := E.(vp_hlt) in
let new := (if widenp then widen else join) old (NotBot res) in
if new ⊑ old
then Just E
else Just {| vp_worklist := E.(vp_worklist)
; vp_run := E.(vp_run)
; vp_hlt := new
|}
end.
Variable widen_oracle : int → ab_post_res ab_mc d → bool.
Definition vpStep (E: vpstate) : vpresult :=
match E.(vp_worklist) with
| nil ⇒ VP_fix E
| (pp, v) :: wl ⇒
match find_bot E.(vp_run) pp with
| NotBot m ⇒
match find_bot m v with
| NotBot mc ⇒
let next : list (ab_post_res ab_mc d) := ab_post_many D T max_deref pp mc in
let r := List.fold_left
(λ acc res, do_top x <- acc; vpPropagate (widen_oracle pp res) res x)
next
(Just {| vp_worklist := wl
; vp_run := E.(vp_run)
; vp_hlt := E.(vp_hlt) |}) in
match r with
| All ⇒ VP_top
| Just E' ⇒ VP_cont E'
end
| Bot ⇒ VP_top
end
| Bot ⇒ VP_top
end
end.
Fixpoint vpLoop (fuel: nat) (E: vpstate) : vpresult :=
match fuel with
| O ⇒ VP_cont E
| S fuel' ⇒ match vpStep E with
| VP_cont E' ⇒ vpLoop fuel' E'
| x ⇒ x
end
end.
Definition vpAnalysis (P: memory) (dom: list int) n : vpresult :=
vpLoop n (vpInit (init T P dom)).
Definition vpAbEnv : Type := (Map [int, Map [int, ab_mc] ] × d+⊥)%type.
Definition vp_ab_env_leb (x y: vpAbEnv) : bool :=
match x, y with
| (xr,xh), (yr,yh) ⇒ map_LE_dec (map_LE_dec leb) xr yr && xh ⊑ yh
end.
Definition vp_ab_env_join (x y: vpAbEnv) : vpAbEnv :=
match x, y with
| (xr,xh), (yr, yh) ⇒ (map_join (map_join join) xr yr, xh ⊔ yh)
end.
Definition vp_pl : pre_lattice vpAbEnv :=
{| pl_leb := vp_ab_env_leb
; pl_join x y := Just (vp_ab_env_join x y)
; pl_widen x y := All
|}.
Instance vp_gamma : gamma_op vpAbEnv machine_state :=
λ x, let '(xr, xh) := x in
λ m,
match m with
| ⌈res⌉ ⇒ res ∈ γ(xh)
| Running mci ⇒
∃ v,
γ (gamma_op := lift_gamma _)
(do_bot m' <- find_bot xr mci.(pc);
find_bot m' v)
mci
end.
Hint Resolve gamma_to_mc_adom.
Lemma vp_pl_sound : pre_lattice_spec vp_pl vp_gamma.
Hint Resolve as_int_adom T_correct.(as_adom).
Definition vpAbEnv_of_vpstate (E: vpstate) : vpAbEnv :=
(E.(vp_run), E.(vp_hlt)).
Definition vp_validate_fixpoint (P: memory) (dom: list int) (E: vpAbEnv) : bool :=
let I := init T P dom in
let iv := δ I in
NotBot I ⊑ (do_bot m <- find_bot (fst E) Int.zero; find_bot m iv)
&&
MF.for_all
(fun (pp: int) (m: Map [ int , ab_mc ]) ⇒
MF.for_all
(fun (_: int) (ab: ab_mc) ⇒
List.forallb
(fun abr : ab_post_res ab_mc d ⇒
match abr with
| Run pp' ab' ⇒
match find_bot (fst E) pp' with
| NotBot q ⇒ NotBot ab' ⊑ find_bot q (δ ab')
| _ ⇒ false
end
| Hlt res ⇒ NotBot res ⊑ snd E
| GiveUp ⇒ false
end
)
(ab_post_many D T max_deref pp ab)
)
m
)
(fst E).
Definition forget_vp (E: vpAbEnv) : AbEnv ab_mc d :=
let fs : Map [ int, ab_mc ] :=
map (fun m ⇒
match map_any m with
| inleft (exist kv _) ⇒ fold (fun _ ab acc ⇒ acc ⊔ ab) m (snd kv)
| inright _ ⇒ ⊤
end) (fst E) in
(fs, snd E).
Local Open Scope goto_scope.
Theorem vp_validate_correct : ∀ P dom E,
vp_validate_fixpoint P dom E = true →
⟦ P ⟧ ⊆ γ(E).
Lemma forget_morph E : γ(E) ⊆ γ(forget_vp E).
Let check_safety := check_safety D T max_deref.
Corollary vp_safety_check P dom E:
vp_validate_fixpoint P dom E = true →
check_safety (forget_vp E) = true →
safe P.
End ValuePartitionning.
Record analysis_state :=
{ worklist : list int
; result_fs : Map [ int, ab_mc ]
; result_hlt: d+⊥
}.
Notation result_at_run := (fun (E:analysis_state) (pp:int) ⇒ find_bot E.(result_fs) pp).
Local Instance lifted_mem_wl : weak_lattice (ab_mc+⊥) := lift_bot_wl T.(as_wl).
Let push (n:int) wl :=
if List.in_dec LatticeSignatures.eq_dec n wl
then wl else n :: wl.
Let bot_set m (x: int) (v: ab_mc+⊥) :=
match v with
| NotBot v' ⇒ (m)[ x <- v' ]
| Bot ⇒ MapInterface.remove x m
end.
Definition propagate (widenp:bool) (E:analysis_state) (n: ab_post_res) : analysis_state+⊤ :=
match n with
| GiveUp ⇒ All
| Run n' ab ⇒
let old := result_at_run E n' in
let new := (if widenp then widen else join) old (NotBot ab) in
if new ⊑ old
then Just E
else Just {| worklist := push n' E.(worklist)
; result_fs := bot_set E.(result_fs) n' new
; result_hlt := E.(result_hlt) |}
| Hlt res ⇒
let old := E.(result_hlt) in
let new := (if widenp then widen else join) old (NotBot res) in
if new ⊑ old
then Just E
else Just {| worklist := E.(worklist)
; result_fs := E.(result_fs)
; result_hlt := new
|}
end.
Variable widen_oracle : int → ab_post_res → bool.
Local Open Scope top_monad_scope.
Definition analysis_step (E:analysis_state) : analysis_state+⊤ :=
match worklist E with
| nil ⇒ Just E
| n :: l ⇒
match result_at_run E n with
| NotBot ab_mc ⇒
let next := ab_post_many n ab_mc in
List.fold_left
(λ acc res, do E' <- acc; propagate (widen_oracle n res) E' res)
next
(Just {| worklist := l
; result_fs := E.(result_fs)
; result_hlt:= E.(result_hlt) |})
| Bot ⇒ All
end
end.
Definition is_final (E: analysis_state) : bool :=
match worklist E with nil ⇒ true | _ :: _ ⇒ false end.
Fixpoint analysis_loop (fuel: nat) (E: analysis_state) : analysis_state+⊤ :=
match fuel with
| O ⇒ Just E
| S fuel' ⇒
do E' <- analysis_step E;
if is_final E' then Just E' else analysis_loop fuel' E'
end.
Definition analysis_init I : analysis_state :=
{| worklist := Int.zero :: nil
; result_fs := ([])[ Int.zero <- I ]
; result_hlt := Bot
|}.
Definition analysis (P: memory) (dom: list int) n : analysis_state+⊤ :=
analysis_loop n (analysis_init (init T P dom)).
End GOTOANALYSIS.
Section VALIDATE.
Variables ab_mc d: Type.
Context (D: ab_machine_int d) (T: mem_dom ab_mc d) (G: gamma_op ab_mc pre_machine_config).
Hypotheses (D_correct: ab_machine_int_correct D) (T_sound: mem_dom_sound T G).
Variable max_deref : N.
Import Containers.Maps.
Local Instance t_wl : weak_lattice ab_mc := T.(as_wl).
Local Instance ltd_wl : weak_lattice ((ab_mc × d)+⊥) := lift_bot_wl (WProd.make_wl T.(as_wl) _).
Definition AbEnv : Type := (Map [int, ab_mc] × d+⊥)%type.
Definition ab_env_leb (x y: AbEnv) : bool :=
match x, y with
| (xr,xh), (yr,yh) ⇒ map_LE_dec leb xr yr && xh ⊑ yh
end.
Definition ab_env_join (x y: AbEnv) : AbEnv :=
match x, y with
| (xr,xh), (yr, yh) ⇒ (map_join join xr yr, xh ⊔ yh)
end.
Definition ab_env_widen (x y: AbEnv) : AbEnv :=
match x, y with
| (xr,xh), (yr, yh) ⇒ (map_join widen xr yr, xh ⊔ yh)
end.
Definition fs_pl : pre_lattice AbEnv :=
{| pl_leb := ab_env_leb
; pl_join x y := Just (ab_env_join x y)
; pl_widen x y := Just (ab_env_widen x y)
|}.
Instance fs_gamma : gamma_op AbEnv machine_state :=
λ x, let '(xr, xh) := x in
λ m,
match m with
| ⌈res⌉ ⇒ res ∈ γ(xh)
| Running mci ⇒ mci ∈ γ (gamma_op := lift_gamma _) (find_bot xr mci.(pc))
end.
Lemma fs_pl_sound : pre_lattice_spec fs_pl fs_gamma.
Hint Resolve as_int_adom.
Definition fs_adom : adom _ _ (weak_lattice_of_pre_lattice fs_pl) _ := adom_of_pre_lattice fs_pl_sound.
Definition abEnv_of_analysis_state (E: analysis_state ab_mc d) : AbEnv :=
(E.(result_fs), E.(result_hlt)).
Instance instr_gamm : gamma_op (ab_instruction d) instruction :=
λ a i,
match a, i with
| AICst v r, ICst v' r' ⇒ v' ∈ γ(v) ∧ r = r'
| AIBinop op rs rd, IBinop op' rs' rd' ⇒ op = op' ∧ rs = rs' ∧ rd = rd'
| AICmp rs rd, ICmp rs' rd' ⇒ rs = rs' ∧ rd = rd'
| AILoad rs rd, ILoad rs' rd' ⇒ rs = rs' ∧ rd = rd'
| AIStore rs rd, IStore rs' rd' ⇒ rs = rs' ∧ rd = rd'
| AIGoto v, IGoto v' ⇒ v' ∈ γ(v)
| AIGotoCond f v, IGotoCond f' v' ⇒ f' = f ∧ v' ∈ γ(v)
| AIGotoInd rs, IGotoInd rs' ⇒ rs = rs'
| AISkip, ISkip ⇒ True
| AIHalt rs, IHalt rs' ⇒ rs = rs'
| _, _ ⇒ False
end.
Local Instance ListAsSet E E' `{G: gamma_op E E'} : gamma_op (list E) E' :=
λ l e', ∃ e, List.In e l ∧ e' ∈ γ(e).
Remark flat_map_gamma {F E E'} `{gamma_op E E'} :
∀ f : F → list E,
∀ l : list F,
∀ x : E',
(∃ y : F, List.In y l ∧ x ∈ γ(f(y))) →
x ∈ γ (flat_map f l).
Local Instance ProdGamma A B A' B' `{Ga: gamma_op A A'}
`{Gb: gamma_op B B'} : gamma_op (A × B) (A' × B') :=
λ ab a'b',
let (a, b) := ab in let (a', b') := a'b' in
a' ∈ γ(a) ∧ b' ∈ γ(b).
Local Instance IdGamma : gamma_op nat nat := @eq nat.
Local Instance OptGamm {A B: Type} `{gamma_op A B} : gamma_op A (option B) :=
λ a b', match b' with Some b ⇒ b ∈ γ(a) | None ⇒ True end.
Lemma abstract_decode_at_sound :
∀ (m:machine_config) (ab:ab_mc) (pp: int),
m ∈ γ(ab) →
decode_from m.(mc_mem) pp ∈ γ(abstract_decode_at D T max_deref pp ab).
Lemma abstract_decode_instr_at_complete ab mci m pp :
mci ∈ γ(ab) →
m = mci.(mc_mem) →
decode_from m pp = None →
abstract_decode_instr_at T ab pp (m pp) = None.
Local Instance AbPostResGamma : gamma_op (ab_post_res ab_mc d) machine_state :=
λ r ms,
match r, ms with
| Run pp' ab, ⟨pp, f, r, m⟩ ⇒ pp = pp' ∧ {| pc := pp; mc_flg := f; mc_reg := r; mc_mem := m |} ∈ γ(ab)
| Hlt v', ⌈v⌉ ⇒ v ∈ γ(v')
| GiveUp, _ ⇒ True
| _, _ ⇒ False
end.
Local Open Scope goto_scope.
Local Coercion Running : machine_config >-> machine_state.
Lemma ab_post_many_correct (m: machine_config) (m': machine_state) (ab: ab_mc) :
m ∈ γ(ab) →
m =~> m' →
m' ∈ γ(ab_post_many D T max_deref m.(pc) ab).
Corollary ab_post_many_correct' m m' (ab: ab_mc) :
m ∈ γ(ab) → Running m =~> m' →
∃ r, List.In r (ab_post_many D T max_deref m.(pc) ab) ∧
m' ∈ γ(r).
Definition validate_fixpoint (P: memory) (dom: list addr) (E: AbEnv) : bool :=
NotBot (init T P dom) ⊑ find_bot (fst E) Int.zero
&&
MF.for_all
(fun (pp: addr) (ab: ab_mc) ⇒
List.forallb
(fun abr : ab_post_res ab_mc d ⇒
match abr with
| Run pp' ab' ⇒ NotBot ab' ⊑ find_bot (fst E) pp'
| Hlt res ⇒ NotBot res ⊑ snd E
| GiveUp ⇒ false
end
)
(ab_post_many D T max_deref pp ab)
)
(fst E).
Theorem validate_correct : ∀ P dom E,
validate_fixpoint P dom E = true →
⟦ P ⟧ ⊆ γ(E).
Definition check_safety (E': AbEnv) : bool :=
let run := fst E' in
MF.for_all
(λ pp mc,
match concretize_with_care D max_deref (T.(load_single) mc pp) with
| All ⇒ false
| Just ab_instr ⇒
IntSet.forallb
(λ i, match abstract_decode_instr_at T mc pp (Int.repr i) with
| Some _ ⇒ true
| None ⇒ false
end)
ab_instr
end)
run.
Lemma check_safety_not_stuck (E': AbEnv) :
check_safety E' = true →
∀ s, γ(E') s → ¬ stuck s.
Theorem check_safety_sound: ∀ P E, ⟦ P ⟧ ⊆ γ(E) →
check_safety E = true → safe P.
Corollary safety_check P dom E:
validate_fixpoint P dom E = true →
check_safety E = true →
safe P.
End VALIDATE.
Section ValuePartitionning.
Variables ab_mc d: Type.
Variables (D: ab_machine_int d) (T: mem_dom ab_mc d) (G: gamma_op ab_mc pre_machine_config).
Hypothesis D_correct : ab_machine_int_correct D.
Hypothesis T_correct : mem_dom_sound T G.
Local Instance vp_t_wl : weak_lattice ab_mc := T.(as_wl).
Local Instance vp_ltd_wl : weak_lattice ((ab_mc × d)+⊥) := lift_bot_wl (WProd.make_wl T.(as_wl) _).
Variable δ : ab_mc → int.
Variable max_deref : N.
Import Containers.Maps.
Record vpstate :=
{ vp_worklist : list (int × int)
; vp_run : Map [ int, Map [ int, ab_mc ] ]
; vp_hlt : d+⊥
}.
Definition vpInit (I: ab_mc) : vpstate :=
let v := δ I in
{| vp_worklist := (Int.zero, v)::nil
; vp_run := ([])[ Int.zero <- ([])[ v <- I ] ]
; vp_hlt := Bot
|}.
Inductive vpresult := VP_top | VP_fix (e: vpstate) | VP_cont (e: vpstate).
Let push (n:int × int) wl :=
if List.in_dec LatticeSignatures.eq_dec n wl
then wl else n :: wl.
Definition vpPropagate (widenp: bool) (succ: ab_post_res ab_mc d) (E: vpstate) : vpstate+⊤ :=
match succ with
| GiveUp ⇒ All
| Run pp ab ⇒
let v := δ ab in
let old := do_bot m <- find_bot E.(vp_run) pp; find_bot m v in
let new := (if widenp then widen else join) old (NotBot ab) in
if new ⊑ old
then Just E
else
match new with
| Bot ⇒ DebugAbMachineNonrel.print "anomaly: vpPropagate" (Just E)
| NotBot new' ⇒
let v' := δ new' in
let m' := match find_bot E.(vp_run) pp with NotBot m' ⇒ m' | Bot ⇒ [] end in
Just {| vp_worklist := push (pp, v') E.(vp_worklist)
; vp_run := (E.(vp_run)) [ pp <- (m') [ v' <- new' ] ]
; vp_hlt := E.(vp_hlt) |}
end
| Hlt res ⇒
let old := E.(vp_hlt) in
let new := (if widenp then widen else join) old (NotBot res) in
if new ⊑ old
then Just E
else Just {| vp_worklist := E.(vp_worklist)
; vp_run := E.(vp_run)
; vp_hlt := new
|}
end.
Variable widen_oracle : int → ab_post_res ab_mc d → bool.
Definition vpStep (E: vpstate) : vpresult :=
match E.(vp_worklist) with
| nil ⇒ VP_fix E
| (pp, v) :: wl ⇒
match find_bot E.(vp_run) pp with
| NotBot m ⇒
match find_bot m v with
| NotBot mc ⇒
let next : list (ab_post_res ab_mc d) := ab_post_many D T max_deref pp mc in
let r := List.fold_left
(λ acc res, do_top x <- acc; vpPropagate (widen_oracle pp res) res x)
next
(Just {| vp_worklist := wl
; vp_run := E.(vp_run)
; vp_hlt := E.(vp_hlt) |}) in
match r with
| All ⇒ VP_top
| Just E' ⇒ VP_cont E'
end
| Bot ⇒ VP_top
end
| Bot ⇒ VP_top
end
end.
Fixpoint vpLoop (fuel: nat) (E: vpstate) : vpresult :=
match fuel with
| O ⇒ VP_cont E
| S fuel' ⇒ match vpStep E with
| VP_cont E' ⇒ vpLoop fuel' E'
| x ⇒ x
end
end.
Definition vpAnalysis (P: memory) (dom: list int) n : vpresult :=
vpLoop n (vpInit (init T P dom)).
Definition vpAbEnv : Type := (Map [int, Map [int, ab_mc] ] × d+⊥)%type.
Definition vp_ab_env_leb (x y: vpAbEnv) : bool :=
match x, y with
| (xr,xh), (yr,yh) ⇒ map_LE_dec (map_LE_dec leb) xr yr && xh ⊑ yh
end.
Definition vp_ab_env_join (x y: vpAbEnv) : vpAbEnv :=
match x, y with
| (xr,xh), (yr, yh) ⇒ (map_join (map_join join) xr yr, xh ⊔ yh)
end.
Definition vp_pl : pre_lattice vpAbEnv :=
{| pl_leb := vp_ab_env_leb
; pl_join x y := Just (vp_ab_env_join x y)
; pl_widen x y := All
|}.
Instance vp_gamma : gamma_op vpAbEnv machine_state :=
λ x, let '(xr, xh) := x in
λ m,
match m with
| ⌈res⌉ ⇒ res ∈ γ(xh)
| Running mci ⇒
∃ v,
γ (gamma_op := lift_gamma _)
(do_bot m' <- find_bot xr mci.(pc);
find_bot m' v)
mci
end.
Hint Resolve gamma_to_mc_adom.
Lemma vp_pl_sound : pre_lattice_spec vp_pl vp_gamma.
Hint Resolve as_int_adom T_correct.(as_adom).
Definition vpAbEnv_of_vpstate (E: vpstate) : vpAbEnv :=
(E.(vp_run), E.(vp_hlt)).
Definition vp_validate_fixpoint (P: memory) (dom: list int) (E: vpAbEnv) : bool :=
let I := init T P dom in
let iv := δ I in
NotBot I ⊑ (do_bot m <- find_bot (fst E) Int.zero; find_bot m iv)
&&
MF.for_all
(fun (pp: int) (m: Map [ int , ab_mc ]) ⇒
MF.for_all
(fun (_: int) (ab: ab_mc) ⇒
List.forallb
(fun abr : ab_post_res ab_mc d ⇒
match abr with
| Run pp' ab' ⇒
match find_bot (fst E) pp' with
| NotBot q ⇒ NotBot ab' ⊑ find_bot q (δ ab')
| _ ⇒ false
end
| Hlt res ⇒ NotBot res ⊑ snd E
| GiveUp ⇒ false
end
)
(ab_post_many D T max_deref pp ab)
)
m
)
(fst E).
Definition forget_vp (E: vpAbEnv) : AbEnv ab_mc d :=
let fs : Map [ int, ab_mc ] :=
map (fun m ⇒
match map_any m with
| inleft (exist kv _) ⇒ fold (fun _ ab acc ⇒ acc ⊔ ab) m (snd kv)
| inright _ ⇒ ⊤
end) (fst E) in
(fs, snd E).
Local Open Scope goto_scope.
Theorem vp_validate_correct : ∀ P dom E,
vp_validate_fixpoint P dom E = true →
⟦ P ⟧ ⊆ γ(E).
Lemma forget_morph E : γ(E) ⊆ γ(forget_vp E).
Let check_safety := check_safety D T max_deref.
Corollary vp_safety_check P dom E:
vp_validate_fixpoint P dom E = true →
check_safety (forget_vp E) = true →
safe P.
End ValuePartitionning.