aboutsummaryrefslogtreecommitdiffstats
path: root/kvx/abstractbb/ImpSimuTest.v
diff options
context:
space:
mode:
Diffstat (limited to 'kvx/abstractbb/ImpSimuTest.v')
-rw-r--r--kvx/abstractbb/ImpSimuTest.v82
1 files changed, 45 insertions, 37 deletions
diff --git a/kvx/abstractbb/ImpSimuTest.v b/kvx/abstractbb/ImpSimuTest.v
index c914eee1..b1a3b985 100644
--- a/kvx/abstractbb/ImpSimuTest.v
+++ b/kvx/abstractbb/ImpSimuTest.v
@@ -10,13 +10,16 @@
(* *)
(* *************************************************************)
-(** Implementation of a symbolic execution of sequential semantics of Abstract Basic Blocks
+(** Implementation of a simulation test (ie a "scheduling verifier") for the sequential semantics of Abstract Basic Blocks.
+
+It is based on a symbolic execution procedure of Abstract Basic Blocks with imperative hash-consing and rewriting.
+
+It also provides debugging information when the test fails.
-with imperative hash-consing, and rewriting.
*)
-Require Export Impure.ImpHCons.
+Require Export Impure.ImpHCons. (**r Import the Impure library. See https://github.com/boulme/ImpureDemo *)
Export Notations.
Import HConsing.
@@ -32,6 +35,7 @@ Import ListNotations.
Local Open Scope list_scope.
+(** * Interface of (impure) equality tests for operators *)
Module Type ImpParam.
Include LangParam.
@@ -54,6 +58,8 @@ Include MkSeqLanguage LP.
End ISeqLanguage.
+(** * A generic dictinary on PseudoRegisters with an impure equality test *)
+
Module Type ImpDict.
Declare Module R: PseudoRegisters.
@@ -91,26 +97,27 @@ Parameter eq_test_correct: forall A (d1 d2: t A),
(* NB: we could also take an eq_test on R.t (but not really useful with "pure" dictionaries *)
-
-(* only for debugging *)
+(** only for debugging *)
Parameter not_eq_witness: forall {A}, t A -> t A -> ?? option R.t.
End ImpDict.
+(** * Specification of the provided tests *)
Module Type ImpSimuInterface.
Declare Module CoreL: ISeqLanguage.
Import CoreL.
Import Terms.
+(** the silent test (without debugging informations) *)
Parameter bblock_simu_test: reduction -> bblock -> bblock -> ?? bool.
Parameter bblock_simu_test_correct: forall reduce (p1 p2 : bblock),
WHEN bblock_simu_test reduce p1 p2 ~> b
THEN b = true -> forall ge : genv, bblock_simu ge p1 p2.
-
+(** the verbose test extended with debugging informations *)
Parameter verb_bblock_simu_test
: reduction ->
(R.t -> ?? pstring) ->
@@ -127,6 +134,7 @@ Parameter verb_bblock_simu_test_correct:
End ImpSimuInterface.
+(** * Implementation of the provided tests *)
Module ImpSimu (L: ISeqLanguage) (Dict: ImpDict with Module R:=L.LP.R): ImpSimuInterface with Module CoreL := L.
@@ -152,13 +160,13 @@ Definition list_term_set_hid (l: list_term) (hid: hashcode): list_term :=
Lemma term_eval_set_hid ge t hid m:
term_eval ge (term_set_hid t hid) m = term_eval ge t m.
Proof.
- destruct t; simpl; auto.
+ destruct t; cbn; auto.
Qed.
Lemma list_term_eval_set_hid ge l hid m:
list_term_eval ge (list_term_set_hid l hid) m = list_term_eval ge l m.
Proof.
- destruct l; simpl; auto.
+ destruct l; cbn; auto.
Qed.
(* Local nickname *)
@@ -168,7 +176,7 @@ Section SimuWithReduce.
Variable reduce: reduction.
-Section CanonBuilding.
+Section CanonBuilding. (** Implementation of the symbolic execution (ie a "canonical form" representing the semantics of an abstract basic block) *)
Variable hC_term: hashinfo term -> ?? term.
Hypothesis hC_term_correct: forall t, WHEN hC_term t ~> t' THEN forall ge m, term_eval ge (hdata t) m = term_eval ge t' m.
@@ -307,7 +315,7 @@ Proof.
destruct (DM0 m) as (PRE & VALID0); clear DM0.
assert (VALID1: allvalid ge hd.(hpre) m -> pre d ge m). { unfold smem_valid in PRE; tauto. }
assert (VALID2: allvalid ge hd.(hpre) m -> forall x : Dict.R.t, ST.term_eval ge (d x) m <> None). { unfold smem_valid in PRE; tauto. }
- rewrite !allvalid_extensionality in * |- *; simpl.
+ rewrite !allvalid_extensionality in * |- *; cbn.
intuition (subst; eauto).
+ eapply smem_valid_set_proof; eauto.
erewrite <- EQT; eauto.
@@ -315,11 +323,11 @@ Proof.
intros X1; exploit smem_valid_set_decompose_2; eauto.
rewrite <- EQT; eauto.
+ exploit smem_valid_set_decompose_1; eauto.
- - clear DM0. unfold hsmem_post_eval, hsmem_post_eval in * |- *; simpl.
+ - clear DM0. unfold hsmem_post_eval, hsmem_post_eval in * |- *; cbn.
Local Hint Resolve smem_valid_set_decompose_1: core.
intros; case (R.eq_dec x x0).
- + intros; subst; rewrite !Dict.set_spec_eq; simpl; eauto.
- + intros; rewrite !Dict.set_spec_diff; simpl; eauto.
+ + intros; subst; rewrite !Dict.set_spec_eq; cbn; eauto.
+ + intros; rewrite !Dict.set_spec_diff; cbn; eauto.
Qed.
Local Hint Resolve naive_set_correct: core.
@@ -396,10 +404,10 @@ Lemma hterm_append_correct l: forall lh,
WHEN hterm_append l lh ~> lh' THEN (forall ge m, allvalid ge lh' m <-> (allvalid ge l m /\ allvalid ge lh m)).
Proof.
Local Hint Resolve eq_trans: localhint.
- induction l as [|t l']; simpl; wlp_xsimplify ltac:(eauto with wlp).
+ induction l as [|t l']; cbn; wlp_xsimplify ltac:(eauto with wlp).
- intros; rewrite! allvalid_extensionality; intuition eauto.
- intros REC ge m; rewrite REC; clear IHl' REC. rewrite !allvalid_extensionality.
- simpl; intuition (subst; eauto with wlp localhint).
+ cbn; intuition (subst; eauto with wlp localhint).
Qed.
(*Local Hint Resolve hterm_append_correct: wlp.*)
Global Opaque hterm_append.
@@ -423,8 +431,8 @@ Lemma smart_set_correct hd x ht:
forall ge m y, hsmem_post_eval ge d y m = hsmem_post_eval ge (Dict.set hd x ht) y m.
Proof.
destruct ht; wlp_simplify.
- unfold hsmem_post_eval; simpl. case (R.eq_dec x0 y).
- - intros; subst. rewrite Dict.set_spec_eq, Dict.rem_spec_eq. simpl; congruence.
+ unfold hsmem_post_eval; cbn. case (R.eq_dec x0 y).
+ - intros; subst. rewrite Dict.set_spec_eq, Dict.rem_spec_eq. cbn; congruence.
- intros; rewrite Dict.set_spec_diff, Dict.rem_spec_diff; auto.
Qed.
(*Local Hint Resolve smart_set_correct: wlp.*)
@@ -448,17 +456,17 @@ Proof.
generalize (hterm_append_correct _ _ _ Hexta0); intro APPEND.
generalize (hterm_lift_correct _ _ Hexta1); intro LIFT.
generalize (smart_set_correct _ _ _ _ Hexta3); intro SMART.
- eapply equiv_hsmem_models; eauto; unfold equiv_hsmem; simpl.
+ eapply equiv_hsmem_models; eauto; unfold equiv_hsmem; cbn.
destruct H as (VALID & EFFECT); split.
- intros; rewrite APPEND, <- VALID.
- rewrite !allvalid_extensionality in * |- *; simpl; intuition (subst; eauto).
+ rewrite !allvalid_extensionality in * |- *; cbn; intuition (subst; eauto).
- intros m x0 ALLVALID; rewrite SMART.
destruct (term_eval ge ht m) eqn: Hht.
* case (R.eq_dec x x0).
- + intros; subst. unfold hsmem_post_eval; simpl. rewrite !Dict.set_spec_eq.
+ + intros; subst. unfold hsmem_post_eval; cbn. rewrite !Dict.set_spec_eq.
erewrite LIFT, EFFECT; eauto.
- + intros; unfold hsmem_post_eval; simpl. rewrite !Dict.set_spec_diff; auto.
- * rewrite allvalid_extensionality in ALLVALID; destruct (ALLVALID ht); simpl; auto.
+ + intros; unfold hsmem_post_eval; cbn. rewrite !Dict.set_spec_diff; auto.
+ * rewrite allvalid_extensionality in ALLVALID; destruct (ALLVALID ht); cbn; auto.
Qed.
Local Hint Resolve hsmem_set_correct: wlp.
Global Opaque hsmem_set.
@@ -473,7 +481,7 @@ Proof.
intro H.
induction e using exp_mut with (P0:=fun le => forall d hd,
smem_model ge d hd -> forall m, smem_valid ge d m -> smem_valid ge od m -> list_term_eval ge (list_exp_term le hd hod) m = list_term_eval ge (list_exp_term le d od) m);
- unfold smem_model in * |- * ; simpl; intuition eauto.
+ unfold smem_model in * |- * ; cbn; intuition eauto.
- erewrite IHe; eauto.
- erewrite IHe0, IHe; eauto.
Qed.
@@ -508,10 +516,10 @@ Lemma exp_hterm_correct_x ge e hod od:
induction e using exp_mut with (P0:=fun le => forall d hd,
smem_model ge d hd ->
WHEN list_exp_hterm le hd hod ~> lt THEN forall m, smem_valid ge d m -> smem_valid ge od m -> list_term_eval ge lt m = ST.list_term_eval ge (list_exp_term le d od) m);
- unfold smem_model, hsmem_post_eval in * |- * ; simpl; wlp_simplify.
+ unfold smem_model, hsmem_post_eval in * |- * ; cbn; wlp_simplify.
- rewrite H1, <- H4; auto.
- - rewrite H4, <- H0; simpl; auto.
- - rewrite H5, <- H0, <- H4; simpl; auto.
+ - rewrite H4, <- H0; cbn; auto.
+ - rewrite H5, <- H0, <- H4; cbn; auto.
Qed.
Global Opaque exp_hterm.
@@ -536,7 +544,7 @@ Lemma hinst_smem_correct i: forall hd hod,
forall ge od d, smem_model ge od hod -> smem_model ge d hd -> (forall m, smem_valid ge d m -> smem_valid ge od m) -> smem_model ge (inst_smem i d od) hd'.
Proof.
Local Hint Resolve smem_valid_set_proof: core.
- induction i; simpl; wlp_simplify; eauto 15 with wlp.
+ induction i; cbn; wlp_simplify; eauto 15 with wlp.
Qed.
Global Opaque hinst_smem.
Local Hint Resolve hinst_smem_correct: wlp.
@@ -556,7 +564,7 @@ Fixpoint bblock_hsmem_rec (p: bblock) (d: hsmem): ?? hsmem :=
Lemma bblock_hsmem_rec_correct p: forall hd,
WHEN bblock_hsmem_rec p hd ~> hd' THEN forall ge d, smem_model ge d hd -> smem_model ge (bblock_smem_rec p d) hd'.
Proof.
- induction p; simpl; wlp_simplify.
+ induction p; cbn; wlp_simplify.
Qed.
Global Opaque bblock_hsmem_rec.
Local Hint Resolve bblock_hsmem_rec_correct: wlp.
@@ -565,8 +573,8 @@ Definition hsmem_empty: hsmem := {| hpre:= nil ; hpost := Dict.empty |}.
Lemma hsmem_empty_correct ge: smem_model ge smem_empty hsmem_empty.
Proof.
- unfold smem_model, smem_valid, hsmem_post_eval; simpl; intuition try congruence.
- rewrite !Dict.empty_spec; simpl; auto.
+ unfold smem_model, smem_valid, hsmem_post_eval; cbn; intuition try congruence.
+ rewrite !Dict.empty_spec; cbn; auto.
Qed.
Definition bblock_hsmem: bblock -> ?? hsmem
@@ -714,7 +722,7 @@ Theorem g_bblock_simu_test_correct p1 p2:
WHEN g_bblock_simu_test p1 p2 ~> b THEN b=true -> forall ge, bblock_simu ge p1 p2.
Proof.
wlp_simplify.
- destruct exta0; simpl in * |- *; auto.
+ destruct exta0; cbn in * |- *; auto.
Qed.
Global Opaque g_bblock_simu_test.
@@ -1117,9 +1125,9 @@ Extraction Inline lift.
End ImpSimu.
-Require Import FMapPositive.
-
+(** * Implementation of the Dictionary (based on PositiveMap) *)
+Require Import FMapPositive.
Require Import PArith.
Require Import FMapPositive.
@@ -1201,12 +1209,12 @@ Lemma eq_test_correct A d1: forall (d2: t A),
WHEN eq_test d1 d2 ~> b THEN
b=true -> forall x, get d1 x = get d2 x.
Proof.
- unfold get; induction d1 as [|l1 Hl1 [x1|] r1 Hr1]; destruct d2 as [|l2 [x2|] r2]; simpl;
- wlp_simplify; (discriminate || (subst; destruct x; simpl; auto)).
+ unfold get; induction d1 as [|l1 Hl1 [x1|] r1 Hr1]; destruct d2 as [|l2 [x2|] r2]; cbn;
+ wlp_simplify; (discriminate || (subst; destruct x; cbn; auto)).
Qed.
Global Opaque eq_test.
-(* ONLY FOR DEBUGGING INFO: get some key of a non-empty d *)
+(** ONLY FOR DEBUGGING INFO: get some key of a non-empty d *)
Fixpoint pick {A} (d: t A): ?? R.t :=
match d with
| Leaf _ => FAILWITH "unexpected empty dictionary"
@@ -1219,7 +1227,7 @@ Fixpoint pick {A} (d: t A): ?? R.t :=
RET (xO p)
end.
-(* ONLY FOR DEBUGGING INFO: find one variable on which d1 and d2 differs *)
+(** ONLY FOR DEBUGGING INFO: find one variable on which d1 and d2 differs *)
Fixpoint not_eq_witness {A} (d1 d2: t A): ?? option R.t :=
match d1, d2 with
| Leaf _, Leaf _ => RET None
generated by cgit (git 2.34.1) at 2024-07-14 10:12:53 +0000