diff options
Diffstat (limited to 'kvx/abstractbb/AbstractBasicBlocksDef.v')
| -rw-r--r-- | kvx/abstractbb/AbstractBasicBlocksDef.v | 44 |
1 files changed, 31 insertions, 13 deletions
diff --git a/kvx/abstractbb/AbstractBasicBlocksDef.v b/kvx/abstractbb/AbstractBasicBlocksDef.v index 0b1c502d..948ed660 100644 --- a/kvx/abstractbb/AbstractBasicBlocksDef.v +++ b/kvx/abstractbb/AbstractBasicBlocksDef.v @@ -45,7 +45,7 @@ End LangParam. -(** * Syntax and (sequential) semantics of "basic blocks" *) +(** * Syntax and (sequential) semantics of "abstract basic blocks" *) Module MkSeqLanguage(P: LangParam). Export P. @@ -62,12 +62,12 @@ Definition assign (m: mem) (x:R.t) (v: value): mem := fun y => if R.eq_dec x y then v else m y. -(** expressions *) +(** Expressions *) Inductive exp := - | PReg (x:R.t) - | Op (o:op) (le: list_exp) - | Old (e: exp) + | PReg (x:R.t) (**r pseudo-register *) + | Op (o:op) (le: list_exp) (**r operation *) + | Old (e: exp) (**r evaluation of [e] in the initial state of the instruction (see [inst] below) *) with list_exp := | Enil | Econs (e:exp) (le:list_exp) @@ -95,7 +95,8 @@ with list_exp_eval (le: list_exp) (m old: mem): option (list value) := | LOld le => list_exp_eval le old old end. -Definition inst := list (R.t * exp). (* = a sequence of assignments *) +(** An instruction represents a sequence of assignments where [Old] refers to the initial state of the sequence. *) +Definition inst := list (R.t * exp). Fixpoint inst_run (i: inst) (m old: mem): option mem := match i with @@ -107,6 +108,7 @@ Fixpoint inst_run (i: inst) (m old: mem): option mem := end end. +(** A basic block is a sequence of instructions. *) Definition bblock := list inst. Fixpoint run (p: bblock) (m: mem): option mem := @@ -250,12 +252,16 @@ Qed. End SEQLANG. -Module Terms. -(** terms in the symbolic evaluation -NB: such a term represents the successive computations in one given pseudo-register +(** * Terms in the symbolic execution *) + +(** Such a term represents the successive computations in one given pseudo-register. +The [hid] has no formal semantics: it is only used by the hash-consing oracle (itself dynamically checked to behave like an identity function). + *) +Module Terms. + Inductive term := | Input (x:R.t) (hid:hashcode) | App (o: op) (l: list_term) (hid:hashcode) @@ -334,11 +340,21 @@ Proof. - rewrite IHl; clear IHl. intuition (congruence || eauto). Qed. +(** * Rewriting rules in the symbolic execution *) + +(** The symbolic execution is parametrized by rewriting rules on pseudo-terms. *) + Record pseudo_term: Type := intro_fail { mayfail: list term; effect: term }. +(** Simulation relation between a term and a pseudo-term *) + +Definition match_pt (t: term) (pt: pseudo_term) := + (forall ge m, term_eval ge t m <> None <-> allvalid ge pt.(mayfail) m) + /\ (forall ge m0 m1, term_eval ge t m0 = Some m1 -> term_eval ge pt.(effect) m0 = Some m1). + Lemma inf_option_equivalence (A:Type) (o1 o2: option A): (o1 <> None -> o1 = o2) <-> (forall m1, o1 = Some m1 -> o2 = Some m1). Proof. @@ -346,10 +362,6 @@ Proof. symmetry; eauto. Qed. -Definition match_pt (t: term) (pt: pseudo_term) := - (forall ge m, term_eval ge t m <> None <-> allvalid ge pt.(mayfail) m) - /\ (forall ge m0 m1, term_eval ge t m0 = Some m1 -> term_eval ge pt.(effect) m0 = Some m1). - Lemma intro_fail_correct (l: list term) (t: term) : (forall ge m, term_eval ge t m <> None <-> allvalid ge l m) -> match_pt t (intro_fail l t). Proof. @@ -357,6 +369,7 @@ Proof. Qed. Hint Resolve intro_fail_correct: wlp. +(** The default reduction of a term to a pseudo-term *) Definition identity_fail (t: term):= intro_fail [t] t. Lemma identity_fail_correct (t: term): match_pt t (identity_fail t). @@ -366,6 +379,7 @@ Qed. Global Opaque identity_fail. Hint Resolve identity_fail_correct: wlp. +(** The reduction for constant term *) Definition nofail (is_constant: op -> bool) (t: term):= match t with | Input x _ => intro_fail ([])%list t @@ -385,6 +399,7 @@ Qed. Global Opaque nofail. Hint Resolve nofail_correct: wlp. +(** Term equivalence preserve the simulation by pseudo-terms *) Definition term_equiv t1 t2:= forall ge m, term_eval ge t1 m = term_eval ge t2 m. Global Instance term_equiv_Equivalence : Equivalence term_equiv. @@ -401,6 +416,7 @@ Proof. Qed. Hint Resolve match_pt_term_equiv: wlp. +(** Other generic reductions *) Definition app_fail (l: list term) (pt: pseudo_term): pseudo_term := {| mayfail := List.rev_append l pt.(mayfail); effect := pt.(effect) |}. @@ -431,6 +447,8 @@ Extraction Inline app_fail. Import ImpCore.Notations. Local Open Scope impure_scope. +(** Specification of rewriting functions in parameter of the symbolic execution: in the impure monad, because the rewriting functions produce hash-consed terms (wrapped in pseudo-terms). +*) Record reduction:= { result:> term -> ?? pseudo_term; result_correct: forall t, WHEN result t ~> pt THEN match_pt t pt; |