diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-05 22:46:14 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-05 22:46:14 +0200 |
commit | 8d1c157bf4f262de656abfee51afd2f56f8127db (patch) | |
tree | 6971dc1b3d443add315d6975076114218a469dda /kvx/abstractbb/SeqSimuTheory.v | |
parent | d1a06a9c8dac42e43e9a2145a3914438e868496e (diff) | |
parent | eafda94d27cb246c1614b51d75d32931a58d9b31 (diff) | |
download | compcert-kvx-8d1c157bf4f262de656abfee51afd2f56f8127db.tar.gz compcert-kvx-8d1c157bf4f262de656abfee51afd2f56f8127db.zip |
Merge remote-tracking branch 'origin/kvx-work' into mppa-RTLpathSE-verif-hash-junk
iMe
Diffstat (limited to 'kvx/abstractbb/SeqSimuTheory.v')
-rw-r--r-- | kvx/abstractbb/SeqSimuTheory.v | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/kvx/abstractbb/SeqSimuTheory.v b/kvx/abstractbb/SeqSimuTheory.v index 61f8f2ec..a957c50a 100644 --- a/kvx/abstractbb/SeqSimuTheory.v +++ b/kvx/abstractbb/SeqSimuTheory.v @@ -55,13 +55,14 @@ with list_term_eval ge (l: list_term) (m: mem) {struct l}: option (list value) : end end. -(* the symbolic memory: - - pre: pre-condition expressing that the computation has not yet abort on a None. - - post: the post-condition for each pseudo-register -*) -Record smem:= {pre: genv -> mem -> Prop; post:> R.t -> term}. - -(** initial symbolic memory *) +(** The (abstract) symbolic memory state *) +Record smem := +{ + pre: genv -> mem -> Prop; (**r pre-condition expressing that the computation has not yet abort on a None. *) + post:> R.t -> term (**r the output term computed on each pseudo-register *) +}. + +(** Initial symbolic memory state *) Definition smem_empty := {| pre:=fun _ _ => True; post:=(fun x => Input x) |}. Fixpoint exp_term (e: exp) (d old: smem) : term := @@ -78,11 +79,12 @@ with list_exp_term (le: list_exp) (d old: smem) : list_term := end. -(** assignment of the symbolic memory *) +(** assignment of the symbolic memory state *) Definition smem_set (d:smem) x (t:term) := {| pre:=(fun ge m => (term_eval ge (d x) m) <> None /\ (d.(pre) ge m)); post:=fun y => if R.eq_dec x y then t else d y |}. +(** Simulation theory: the theorem [bblock_smem_simu] ensures that the simulation between two abstract basic blocks is implied by the simulation between their symbolic execution. *) Section SIMU_THEORY. Variable ge: genv. @@ -375,8 +377,7 @@ Qed. End SIMU_THEORY. -(** REMARKS: more abstract formulation of the proof... - but relying on functional_extensionality. +(** REMARK: this theorem reformulates the lemma above in a more abstract way (but relies on functional_extensionality axiom). *) Definition smem_correct ge (d: smem) (m: mem) (om: option mem): Prop:= forall m', om=Some m' <-> (d.(pre) ge m /\ forall x, term_eval ge (d x) m = Some (m' x)). |