non trapping loads

1 files changed, 27 insertions, 17 deletions

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 2a335790..e2e6be6b 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -626,18 +626,22 @@ Definition sexec_load trap chunk addr args dst sis: sistate :=
    let args := list_sval_inj (List.map sis.(si_sreg) args) in
    set_sreg dst (fSload sis.(si_smem) trap chunk addr args) sis.
 
-Lemma sexec_load_TRAP_correct ctx chunk addr args dst sis rs m a v
- (EVAL: eval_addressing (cge ctx) (csp ctx) addr rs ## args = Some a)
- (LOAD: Mem.loadv chunk m a = Some v)
+Lemma sexec_load_correct ctx chunk addr args dst sis rs m v trap
+ (HLOAD: has_loaded (cge ctx) (csp ctx) rs m chunk addr args v trap)
  (SIS: sem_sistate ctx sis rs m)
- :(sem_sistate ctx (sexec_load TRAP chunk addr args dst sis) (rs#dst <- v) m).
+ :(sem_sistate ctx (sexec_load trap chunk addr args dst sis) (rs#dst <- v) m).
 Proof.
-  eapply set_sreg_correct; eauto.
+  inv HLOAD; eapply set_sreg_correct; eauto.
+  2,4: intros; rewrite Regmap.gso; auto.
+  - simpl. destruct SIS as (PRE&MEM&REG).
+    destruct trap; rewrite Regmap.gss; simpl; auto;
+    erewrite eval_list_sval_inj; simpl; auto;
+    try_simplify_someHyps.
+    intros. rewrite LOAD; auto.
   - simpl. destruct SIS as (PRE&MEM&REG).
     rewrite Regmap.gss; simpl; auto.
     erewrite eval_list_sval_inj; simpl; auto.
-    try_simplify_someHyps.
-  - intros; rewrite Regmap.gso; auto.
+    autodestruct; rewrite MEM, LOAD; auto.
 Qed.
 
 Definition sexec_store chunk addr args src sis: sistate :=
@@ -812,8 +816,7 @@ Fixpoint sexec_rec f ib sis (k: sistate -> sstate): sstate :=
   (* basic instructions *)
   | Bnop _ => k sis
   | Bop op args res _ => k (sexec_op op args res sis)
-  | Bload TRAP chunk addr args dst _ => k (sexec_load TRAP chunk addr args dst sis)
-  | Bload NOTRAP chunk addr args dst _ => Sabort (* TODO *)
+  | Bload trap chunk addr args dst _ => k (sexec_load trap chunk addr args dst sis)
   | Bstore chunk addr args src _ => k (sexec_store chunk addr args src sis)
  (* composed instructions *)
   | Bseq ib1 ib2 =>
@@ -830,7 +833,7 @@ Definition sexec f ib := sexec_rec f ib sis_init (fun _ => Sabort).
 
 Local Hint Constructors sem_sstate: core.
 Local Hint Resolve sexec_op_correct sexec_final_sfv_correct tr_sis_regs_correct_aux tr_sis_regs_correct
-                   sexec_load_TRAP_correct sexec_store_correct sis_init_correct: core.
+                   sexec_load_correct sexec_store_correct sis_init_correct: core.
 
 Lemma sexec_rec_correct ctx stk t s ib rs m rs1 m1 ofin
   (ISTEP: iblock_istep (cge ctx) (csp ctx) rs m ib rs1 m1 ofin): forall sis k
@@ -921,9 +924,9 @@ Proof.
   intros; eapply set_sreg_preserves_abort; eauto.
 Qed.
 
-Lemma sexec_load_preserves_abort ctx chunk addr args dest sis:
+Lemma sexec_load_preserves_abort ctx chunk addr args dest sis trap:
   abort_sistate ctx sis
-  -> abort_sistate ctx (sexec_load TRAP chunk addr args dest sis).
+  -> abort_sistate ctx (sexec_load trap chunk addr args dest sis).
 Proof.
   intros; eapply set_sreg_preserves_abort; eauto.
 Qed.
@@ -962,8 +965,6 @@ Lemma sexec_exclude_abort ctx stk ib t s1: forall sis k
 Proof.
   induction ib; simpl; intros; eauto.
   - (* final *) inversion SEXEC; subst; eauto.
-  - (* load *) destruct trap; eauto.
-    inversion SEXEC.
   - (* seq *)
     eapply IHib1; eauto.
     simpl. eauto.
@@ -1052,11 +1053,20 @@ Proof.
     * intros; rewrite REG, str_tr_regs_equiv; auto.
     * intros (s2 & EQUIV & SFV'); eauto.
   - (* Bop *) autodestruct; eauto.
-  - destruct trap; [| inv SEXEC ].
-    repeat autodestruct; eauto.
-    all: intros; eapply CONT; eauto;
+  - destruct trap.
+    + repeat autodestruct.
+      { eexists; split; eauto.
+        eapply sexec_load_correct; eauto.
+        econstructor; eauto. }
+      all:
+        intros; eapply CONT; eauto;
         eapply sexec_load_TRAP_abort; eauto;
         intros; try_simplify_someHyps.
+    + repeat autodestruct;
+      eexists; split; eauto;
+      eapply sexec_load_correct; eauto;
+      try (econstructor; eauto; fail).
+      all: eapply has_loaded_default; auto; try_simplify_someHyps.
   - repeat autodestruct; eauto.
     all: intros; eapply CONT; eauto;
         eapply sexec_store_abort; eauto;