Merge branch 'BTL-SEimpl' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL-SEimpl

9 files changed, 103 insertions, 64 deletions

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 6536addb..96377943 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -205,7 +205,7 @@ Definition find_function (ros: reg + ident) (rs: regset) : option fundef :=
 
 Local Open Scope option_monad_scope.
 
-(* (* TODO: a new (hopefully simpler) scheme to support "NOTRAP" wrt current scheme of RTL *)
+(* TODO: a new (hopefully simpler) scheme to support "NOTRAP" wrt current scheme of RTL *)
 
 Inductive has_loaded sp rs m chunk addr args v: trapping_mode -> Prop :=
   | has_loaded_normal a trap
@@ -217,11 +217,10 @@ Inductive has_loaded sp rs m chunk addr args v: trapping_mode -> Prop :=
       (DEFAULT: v = default_notrap_load_value chunk)
       : has_loaded sp rs m chunk addr args v NOTRAP 
   .
+Local Hint Constructors has_loaded: core.
 
 (* TODO: move this scheme in "Memory" module if this scheme is useful ! *)
 
-*)
-
 (** internal big-step execution of one iblock *)
 Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option final -> Prop :=
   | exec_final rs m fin iinfo: iblock_istep sp rs m (BF fin iinfo) rs m (Some fin)
@@ -229,15 +228,9 @@ Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option fi
   | exec_op rs m op args res v iinfo
      (EVAL: eval_operation ge sp op rs##args m = Some v)
      : iblock_istep sp rs m (Bop op args res iinfo) (rs#res <- v) m None
-  | exec_load_TRAP rs m chunk addr args dst a v iinfo
-     (EVAL: eval_addressing ge sp addr rs##args = Some a)
-     (LOAD: Mem.loadv chunk m a = Some v)
-     : iblock_istep sp rs m (Bload TRAP chunk addr args dst iinfo) (rs#dst <- v) m None
-(* TODO: replace [exec_load_TRAP] above by this one. See "new scheme" for "NOTRAP" above
-  | exec_load rs m trap chunk addr args dst v
+  | exec_load rs m trap chunk addr args dst v iinfo
       (LOAD: has_loaded sp rs m chunk addr args v trap)
-     : iblock_istep sp rs m (Bload trap chunk addr args dst) (rs#dst <- v) m None
-*)
+     : iblock_istep sp rs m (Bload trap chunk addr args dst iinfo) (rs#dst <- v) m None
   | exec_store rs m chunk addr args src a m' iinfo
      (EVAL: eval_addressing ge sp addr rs##args = Some a)
      (STORE: Mem.storev chunk m a rs#src = Some m')
@@ -274,7 +267,18 @@ Fixpoint iblock_istep_run sp ib rs m: option outcome :=
       SOME v <- Mem.loadv chunk m a IN
       Some {| _rs := rs#dst <- v; _m:= m; _fin := None |}
   | Bload NOTRAP chunk addr args dst _ =>
-      None (* TODO *)
+      match eval_addressing ge sp addr rs##args with
+      | Some a =>
+          match Mem.loadv chunk m a with
+          | Some v => Some {| _rs := rs#dst <- v; _m:= m; _fin := None |}
+          | None =>
+              let v := default_notrap_load_value chunk in
+              Some {| _rs := rs#dst <- v; _m:= m; _fin := None |}
+          end
+      | None =>
+          let v := default_notrap_load_value chunk in
+          Some {| _rs := rs#dst <- v; _m:= m; _fin := None |}
+      end
   | Bstore chunk addr args src _ =>
       SOME a <- eval_addressing ge sp addr rs##args IN
       SOME m' <- Mem.storev chunk m a rs#src IN
@@ -291,13 +295,34 @@ Fixpoint iblock_istep_run sp ib rs m: option outcome :=
       iblock_istep_run sp (if b then ifso else ifnot) rs m
   end.
 
+Lemma iblock_istep_run_equiv_load sp ib v rs rs' m trap chunk addr args dst iinfo ofin:
+  ib = (Bload trap chunk addr args dst iinfo) ->
+  rs' = rs # dst <- v ->
+  has_loaded sp rs m chunk addr args v trap ->
+  iblock_istep sp rs m ib rs' m ofin <->
+  iblock_istep_run sp ib rs m = Some {| _rs := rs'; _m := m; _fin := ofin |}.
+Proof.
+  split; subst; inv H1; simpl in *; intros.
+  - destruct trap; inv H; simpl in *; repeat autodestruct.
+  - inv H; autodestruct; rewrite LOAD; auto.
+  - destruct trap; inv H; simpl in *;
+    rewrite EVAL, LOAD in H1; inv H1; repeat econstructor; eauto.
+  - generalize H; autodestruct.
+    + rewrite LOAD in *; inv H; auto; constructor.
+      eapply has_loaded_default; eauto; try_simplify_someHyps.
+    + inv H; constructor. eapply has_loaded_default; eauto; try_simplify_someHyps.
+Qed.
+Local Hint Resolve iblock_istep_run_equiv_load: core.
+
 Lemma iblock_istep_run_equiv sp rs m ib rs' m' ofin:
   iblock_istep sp rs m ib rs' m' ofin <-> iblock_istep_run sp ib rs m = Some {| _rs := rs'; _m:= m'; _fin := ofin |}.
 Proof.
   constructor.
-  - induction 1; simpl; try autodestruct; try_simplify_someHyps.
+  - induction 1; try (eapply iblock_istep_run_equiv_load; eauto; fail);
+    simpl; try autodestruct; try_simplify_someHyps.
   - generalize rs m rs' m' ofin; clear rs m rs' m' ofin.
     induction ib; simpl; repeat (try autodestruct; try_simplify_someHyps).
+    1,2: constructor; eapply has_loaded_default; try_simplify_someHyps.
     destruct o; try_simplify_someHyps; subst; eauto.
 Qed.
 
diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v
index 9f96e74e..d200b9bd 100644
--- a/scheduling/BTL_Livecheck.v
+++ b/scheduling/BTL_Livecheck.v
@@ -546,12 +546,14 @@ Proof.
   - (* Bload *)
     erewrite <- eqlive_reg_listmem; eauto.
     try_simplify_someHyps; intros.
-    rewrite LOAD; eauto.
-    repeat econstructor.
-    apply eqlive_reg_update.
-    eapply eqlive_reg_monotonic; eauto.
-    intros r0; rewrite regset_add_spec. 
-    intuition.
+    destruct trap; inv LOAD;
+    rewrite EVAL, LOAD0 || (autodestruct; try rewrite LOAD0; auto).
+    all:
+      repeat econstructor;
+      apply eqlive_reg_update;
+      eapply eqlive_reg_monotonic; eauto;
+      intros r0; rewrite regset_add_spec; 
+      intuition.
   - (* Bstore *)
     erewrite <- eqlive_reg_listmem; eauto.
     rewrite <- (REGS src); auto.
diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v
index 305c3cfa..aa27bd19 100644
--- a/scheduling/BTL_SEimpl.v
+++ b/scheduling/BTL_SEimpl.v
@@ -823,11 +823,11 @@ Proof.
   simpl in *; econstructor; eauto.
 Qed.
 
-Lemma hrs_ok_load_okpreserv ctx chunk addr args dest hrs:
-  WHEN hrs_sreg_set dest args (Rload TRAP chunk addr) hrs ~> rst THEN
+Lemma hrs_ok_load_okpreserv ctx chunk addr args dest hrs trap:
+  WHEN hrs_sreg_set dest args (Rload trap chunk addr) hrs ~> rst THEN
   ris_ok ctx rst -> ris_ok ctx hrs.
 Proof.
-  wlp_simplify; inv H1;
+  wlp_simplify; inv H2 || inv H1;
   simpl in *; econstructor; eauto.
 Qed.
 
@@ -1071,10 +1071,9 @@ Fixpoint hrexec_rec f ib hrs (k: ristate -> ?? rstate): ?? rstate :=
   | Bop op args dst _ =>
       DO next <~ hrs_sreg_set dst args (Rop op) hrs;;
       k next
-  | Bload TRAP chunk addr args dst _ =>
-      DO next <~ hrs_sreg_set dst args (Rload TRAP chunk addr) hrs;;
+  | Bload trap chunk addr args dst _ =>
+      DO next <~ hrs_sreg_set dst args (Rload trap chunk addr) hrs;;
       k next
-  | Bload NOTRAP chunk addr args dst _ => RET Rabort
   | Bstore chunk addr args src _ =>
       DO next <~ hrexec_store chunk addr args src hrs;;
       k next
@@ -1122,7 +1121,6 @@ Proof.
     intros X; apply H0 in X.
     exploit hrexec_final_sfv_correct; eauto.
   - (* Bnop *) wlp_simplify; eapply CONT; eauto.
-  - (* Bload *) destruct trap; wlp_simplify.
   - (* Bseq *)
     wlp_simplify.
     eapply IHib1. 3-7: eauto.
@@ -1171,7 +1169,7 @@ Proof.
   - (* Bop *)
     wlp_simplify; exploit hrs_ok_op_okpreserv; eauto.
   - (* Bload *)
-    destruct trap; wlp_simplify; try_simplify_someHyps.
+    destruct trap; wlp_simplify; try_simplify_someHyps;
     exploit hrs_ok_load_okpreserv; eauto.
   - (* Bstore *)
     wlp_simplify; exploit hrs_ok_store_okpreserv; eauto.
@@ -1207,7 +1205,6 @@ Proof.
     intros X; apply H0 in X.
     exploit hrexec_final_sfv_correct; eauto.
   - (* Bnop *) wlp_simplify; eapply CONT; eauto.
-  - (* Bload *) destruct trap; wlp_simplify.
   - (* Bseq *)
     wlp_simplify.
     eapply IHib1. 3-6: eauto.
diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index 7af1af62..d47e53b8 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -348,7 +348,7 @@ Proof.
   unfold sexec_op. rewrite ok_set_sreg. intuition.
 Qed.
 
-Lemma si_ok_load_okpreserv ctx chunk addr args dest sis: si_ok ctx (sexec_load TRAP chunk addr args dest sis) -> si_ok ctx sis.
+Lemma si_ok_load_okpreserv ctx chunk addr args dest sis trap: si_ok ctx (sexec_load trap chunk addr args dest sis) -> si_ok ctx sis.
 Proof.
   unfold sexec_load. rewrite ok_set_sreg. intuition.
 Qed.
@@ -705,8 +705,7 @@ Fixpoint rexec_rec f ib ris (k: ristate -> rstate): rstate :=
   (* basic instructions *)
   | Bnop _ => k ris
   | Bop op args res _ => k (rexec_op op args res ris)
-  | Bload TRAP chunk addr args dst _ => k (rexec_load TRAP chunk addr args dst ris)
-  | Bload NOTRAP chunk addr args dst _ => Rabort
+  | Bload trap chunk addr args dst _ => k (rexec_load trap chunk addr args dst ris)
   | Bstore chunk addr args src _ => k (rexec_store chunk addr args src ris)
  (* composed instructions *)
   | Bseq ib1 ib2 =>
@@ -739,7 +738,6 @@ Lemma rexec_rec_correct1 ctx ib:
   , rst_refines ctx (rexec_rec (cf ctx) ib ris rk) st.
 Proof.
   induction ib; simpl; try (intros; subst; eauto; fail).
-  - (* load *) intros; subst; autodestruct; simpl in *; subst; eauto.
   - (* seq *)
     intros; subst.
     eapply IHib1. 3-6: eauto.
@@ -774,7 +772,7 @@ Proof.
   unfold rexec_op. rewrite ok_rset_sreg. intuition.
 Qed.
 
-Lemma ris_ok_load_okpreserv ctx chunk addr args dest ris: ris_ok ctx (rexec_load TRAP chunk addr args dest ris) -> ris_ok ctx ris.
+Lemma ris_ok_load_okpreserv ctx chunk addr args dest ris trap: ris_ok ctx (rexec_load trap chunk addr args dest ris) -> ris_ok ctx ris.
 Proof.
   unfold rexec_load. rewrite ok_rset_sreg. intuition.
 Qed.
@@ -818,7 +816,6 @@ Lemma rexec_rec_correct2 ctx ib:
   , rst_refines ctx st (sexec_rec (cf ctx) ib sis k).
 Proof.
   induction ib; simpl; try (intros; subst; eauto; fail).
-  - (* load *) intros; subst; autodestruct; simpl in *; subst; eauto.
   - (* seq *)
     intros; subst.
     eapply IHib1. 3-6: eauto.
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;
diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v
index 27efe56f..40ad0d88 100644
--- a/scheduling/BTL_Schedulerproof.v
+++ b/scheduling/BTL_Schedulerproof.v
@@ -354,7 +354,7 @@ Proof.
   - repeat econstructor; eauto.
   - repeat econstructor; eauto.
     erewrite args_eqregs; eauto.
-  - repeat econstructor; eauto.
+  - inv LOAD; repeat econstructor; eauto;
     erewrite args_eqregs; eauto.
   - repeat econstructor; eauto.
     erewrite args_eqregs; eauto.
diff --git a/scheduling/BTLmatchRTL.v b/scheduling/BTLmatchRTL.v
index a59c847e..c271ae02 100644
--- a/scheduling/BTLmatchRTL.v
+++ b/scheduling/BTLmatchRTL.v
@@ -48,11 +48,15 @@ Proof.
     do 2 eexists; rewrite EVAL'. repeat (split; eauto).
     eapply set_reg_lessdef; eauto.
   - (* Bload *)
-    exploit (@eval_addressing_lessdef _ _ ge sp addr (rs ## args)); eauto.
-    intros (v2 & EVAL' & LESSDEF). exploit Mem.loadv_extends; eauto.
-    intros (v3 & LOAD' & LESSDEF').
-    do 2 eexists; rewrite EVAL', LOAD'. repeat (split; eauto).
-    eapply set_reg_lessdef; eauto.
+    inv LOAD.
+    + exploit (@eval_addressing_lessdef _ _ ge sp addr (rs ## args)); eauto.
+      intros (v2 & EVAL' & LESSDEF). exploit Mem.loadv_extends; eauto.
+      intros (v3 & LOAD' & LESSDEF'); autodestruct;
+      do 2 eexists; rewrite EVAL', LOAD';
+      repeat (split; eauto); eapply set_reg_lessdef; eauto.
+    + destruct (eval_addressing ge sp addr rs ## args) eqn:EQA;
+      repeat autodestruct; do 2 eexists;
+      repeat (split; eauto); eapply set_reg_lessdef; eauto.
   - (* Bstore *)
     exploit (@eval_addressing_lessdef _ _ ge sp addr (rs ## args)); eauto.
     intros (v2 & EVAL' & LESSDEF). exploit Mem.storev_extends; eauto.
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
index 9b8dabab..324f1d14 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -230,7 +230,8 @@ Proof.
     intros; rewrite symbols_preserved; trivial.
   - (* exec_load *)
     inv MIB. exists pc'; split; auto; constructor.
-    apply plus_one. eapply exec_Iload; eauto.
+    apply plus_one. inv LOAD.
+    eapply exec_Iload; eauto.
     all: erewrite <- eval_addressing_preserved; eauto;
          intros; rewrite symbols_preserved; trivial.
   - (* exec_store *)
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index 8a352434..13ba5a29 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -123,12 +123,15 @@ Lemma normRTLrec_iblock_istep_correct tge sp ib rs0 m0 rs1 m1 ofin1:
   iblock_istep tge sp rs0 m0 (normRTLrec ib k) rs2 m2 ofin2.
 Proof.
   induction 1; simpl; intuition subst; eauto.
-  { (* Bnop *) autodestruct; eauto. }
-  1-3: (* Bop, Bload, Bstore *)
-     intros; repeat econstructor; eauto.
-  (* Bcond *)
-  destruct ofin; intuition subst;
-  destruct b; eapply IHISTEP; eauto.
+  - (* Bnop *) autodestruct; eauto.
+  - (* Bop *) repeat econstructor; eauto.
+  - (* Bload *) inv LOAD.
+    + repeat econstructor; eauto.
+    + do 2 (econstructor; eauto).
+      eapply has_loaded_default; eauto.
+  - (* Bcond *) repeat econstructor; eauto.
+    destruct ofin; intuition subst;
+    destruct b; eapply IHISTEP; eauto.
 Qed.
 
 Lemma normRTL_iblock_istep_correct tge sp ib rs0 m0 rs1 m1 ofin: