Some progress on notrap load

3 files changed, 61 insertions, 23 deletions

diff --git a/mppa_k1c/lib/RTLpath.v b/mppa_k1c/lib/RTLpath.v
index e2e6659f..6aa0258e 100644
--- a/mppa_k1c/lib/RTLpath.v
+++ b/mppa_k1c/lib/RTLpath.v
@@ -143,17 +143,26 @@ Coercion program_RTL: program >-> RTL.program.
 
 Record istate := ist { continue: bool; the_pc: node; the_rs: regset; the_mem: mem }.
 
-(* FIXME - prediction + no trapping load *)
+(* FIXME - prediction *)
 Definition istep (ge: RTL.genv) (i: instruction) (sp: val) (rs: regset) (m: mem): option istate :=
   match i with
   | Inop pc' => Some (ist true pc' rs m)
   | Iop op args res pc' =>
       SOME v <- eval_operation ge sp op rs##args m IN
       Some (ist true pc' (rs#res <- v) m)
-  | Iload _ chunk addr args dst pc' =>
+  | Iload TRAP chunk addr args dst pc' =>
       SOME a <- eval_addressing ge sp addr rs##args IN
       SOME v <- Mem.loadv chunk m a IN
       Some (ist true pc' (rs#dst <- v) m)
+  | Iload NOTRAP chunk addr args dst pc' =>
+      let default_state := ist true pc' rs#dst <- (default_notrap_load_value chunk) m in
+      match (eval_addressing ge sp addr rs##args) with
+      | None => Some default_state
+      | Some a => match (Mem.loadv chunk m a) with
+          | None => Some default_state
+          | Some v => Some (ist true pc' (rs#dst <- v) m)
+          end
+      end
   | Istore chunk addr args src pc' =>
       SOME a <- eval_addressing ge sp addr rs##args IN
       SOME m' <- Mem.storev chunk m a rs#src IN
@@ -352,6 +361,14 @@ Ltac simplify_someHyp :=
   | H: _ = Some _ |- _ => (try rewrite !H in * |- *); generalize H; clear H
   end.
 
+Ltac explore_destruct :=
+  repeat (match goal with
+  | [H: ?expr = ?val |- context[match ?expr with | _ => _ end]] => rewrite H
+  | [H: match ?var with | _ => _ end |- _] => destruct var
+  | [ |- context[match ?m with | _ => _ end] ] => destruct m
+  | _ => discriminate
+  end).
+
 Ltac simplify_someHyps := 
   repeat (simplify_someHyp; simpl in * |- *).
 
@@ -368,7 +385,7 @@ This way can be viewed as a correctness property: all transitions in RTLpath are
 
 *)
 
-Local Hint Resolve RTL.exec_Inop RTL.exec_Iop RTL.exec_Iload RTL.exec_Istore RTL.exec_Icond: core.
+Local Hint Resolve RTL.exec_Inop RTL.exec_Iop RTL.exec_Iload RTL.exec_Istore RTL.exec_Icond RTL.exec_Iload_notrap1 RTL.exec_Iload_notrap2: core.
 
 Lemma istep_correct ge i stack (f:function) sp rs m st :
   istep ge i sp rs m = Some st ->
@@ -376,6 +393,7 @@ Lemma istep_correct ge i stack (f:function) sp rs m st :
   RTL.step ge (State stack f sp pc rs m) E0 (State stack f sp st.(the_pc) st.(the_rs) st.(the_mem)).
 Proof.
   destruct i; simpl; try congruence; simplify_SOME x.
+  1-3: explore_destruct; simplify_SOME x.
 Qed.
 
 Local Hint Resolve star_refl: core.
@@ -587,7 +605,7 @@ Lemma istep_successors ge i sp rs m st:
   In (the_pc st) (successors_instr i).
 Proof.
   destruct i; simpl; try congruence; simplify_SOME x.
-  destruct x; simpl in * |- *; intuition congruence.
+  all: explore_destruct; simplify_SOME x.
 Qed.
 
 Lemma istep_normal_exit ge i sp rs m st:
@@ -596,7 +614,7 @@ Lemma istep_normal_exit ge i sp rs m st:
   default_succ i = Some st.(the_pc).
 Proof.
   destruct i; simpl; try congruence; simplify_SOME x.
-  destruct x; simpl in * |- *; try congruence.
+  all: explore_destruct; simplify_SOME x.
 Qed.
 
 Lemma isteps_normal_exit ge path f sp: forall rs m pc st,
@@ -686,8 +704,7 @@ Lemma istep_early_exit ge i sp rs m st :
 Proof.
   Local Hint Resolve Icond_early_exit: core.
   destruct i; simpl; try congruence; simplify_SOME b; simpl; try congruence.
-  destruct b; simpl in * |- *; intuition eauto.
-  congruence.
+  all: explore_destruct; simplify_SOME b; try discriminate.
 Qed.
 
 Section COMPLETENESS.
@@ -777,7 +794,8 @@ Lemma istep_complete t i stack f sp rs m pc s':
 Proof.
   intros H X; inversion H; simpl; subst; try rewrite X in * |-; clear X; simplify_someHyps; try congruence;
   (split; auto); simplify_someHyps; eexists; split; simplify_someHyps; eauto.
-Admitted.
+  all: explore_destruct; simplify_SOME a.
+Qed.
 
 Lemma stuttering path idx stack f sp rs m pc st t s1':
    isteps ge (path.(psize)-(S idx)) f sp rs m pc = Some st ->
diff --git a/mppa_k1c/lib/RTLpathLiveproofs.v b/mppa_k1c/lib/RTLpathLiveproofs.v
index 1cdd6168..a807279b 100644
--- a/mppa_k1c/lib/RTLpathLiveproofs.v
+++ b/mppa_k1c/lib/RTLpathLiveproofs.v
@@ -125,15 +125,34 @@ Proof.
     intuition.
   - (* Iload *)
     inversion_ASSERT; try_simplify_someHyps.
-    inversion_SOME a0. intros EVAL.
-    erewrite <- eqlive_reg_listmem; eauto.
-    try_simplify_someHyps.
-    inversion_SOME v; try_simplify_someHyps.
-    repeat (econstructor; simpl; eauto).
-    eapply eqlive_reg_update.
-    eapply eqlive_reg_monotonic; eauto.
-    intros r0; rewrite regset_add_spec. 
-    intuition.
+    destruct t. (* TODO - simplify that proof ? *)
+    + inversion_SOME a0. intros EVAL.
+      erewrite <- eqlive_reg_listmem; eauto.
+      try_simplify_someHyps.
+      inversion_SOME v; try_simplify_someHyps.
+      repeat (econstructor; simpl; eauto).
+      eapply eqlive_reg_update.
+      eapply eqlive_reg_monotonic; eauto.
+      intros r0; rewrite regset_add_spec.
+      intuition.
+    + erewrite <- (eqlive_reg_listmem _ _ rs1 rs2); eauto.
+      destruct (eval_addressing _ _ _ _).
+      * destruct (Memory.Mem.loadv _ _ _).
+        ** intros. inv H1. repeat (econstructor; simpl; eauto).
+           eapply eqlive_reg_update.
+           eapply eqlive_reg_monotonic; eauto.
+           intros r0; rewrite regset_add_spec.
+           intuition.
+        ** intros. inv H1. repeat (econstructor; simpl; eauto).
+           eapply eqlive_reg_update.
+           eapply eqlive_reg_monotonic; eauto.
+           intros r0; rewrite regset_add_spec.
+           intuition.
+      * intros. inv H1. repeat (econstructor; simpl; eauto).
+        eapply eqlive_reg_update.
+        eapply eqlive_reg_monotonic; eauto.
+        intros r0; rewrite regset_add_spec.
+        intuition.
   - (* Istore *)
     (repeat inversion_ASSERT); try_simplify_someHyps.
     inversion_SOME a0. intros EVAL.
@@ -186,6 +205,7 @@ Proof.
   intros EQLIVE.
   set (tmp := istep ge i sp rs2).
   destruct i; simpl; try_simplify_someHyps; repeat (inversion_ASSERT || inversion_SOME b);  try_simplify_someHyps; try congruence.
+  1-3: explore_destruct; simpl; try_simplify_someHyps; repeat (inversion_ASSERT || inversion_SOME b);  try_simplify_someHyps; try congruence.
   (* Icond *)
   unfold tmp; clear tmp; simpl.
   intros EVAL; erewrite <- eqlive_reg_listmem; eauto.
@@ -558,4 +578,4 @@ Proof.
     * eapply eqlive_states_intro; eauto.
 Qed.
 
-End LivenessProperties.
\ No newline at end of file
+End LivenessProperties.
diff --git a/mppa_k1c/lib/RTLpathSE_theory.v b/mppa_k1c/lib/RTLpathSE_theory.v
index cf277368..ebea3b33 100644
--- a/mppa_k1c/lib/RTLpathSE_theory.v
+++ b/mppa_k1c/lib/RTLpathSE_theory.v
@@ -416,10 +416,10 @@ Proof.
       exists r. destruct (Pos.eq_dec r r); try congruence.
       simpl. erewrite list_sval_eval_inj; simpl; auto.
       try_simplify_someHyps.
-  + (* LOAD *)
-    inversion_SOME a0; intros ADD.
+  + (* LOAD *) admit. (* FIXME *)
+(*     inversion_SOME a0; intros ADD.
     { inversion_SOME v; intros LOAD; simpl.
-      - unfold sem_istate, sem_local_istate; simpl; intuition.
+      - explore_destruct; unfold sem_istate, sem_local_istate; simpl; intuition.
         * exploit REG. try_simplify_someHyps.
         * destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto].
           subst; rewrite Regmap.gss; simpl.
@@ -434,7 +434,7 @@ Proof.
       left. right. right.
       exists r. destruct (Pos.eq_dec r r); try congruence.
       simpl. erewrite list_sval_eval_inj; simpl; auto.
-      rewrite ADD; simpl; auto. }
+      rewrite ADD; simpl; auto. } *)
    + (* STORE *)
     inversion_SOME a0; intros ADD.
     { inversion_SOME m'; intros STORE; simpl.
@@ -471,7 +471,7 @@ Proof.
         unfold seval_condition.
         erewrite list_sval_eval_inj; simpl; auto.
         try_simplify_someHyps. }
-Qed.
+Admitted.
 
 Lemma symb_istep_correct_None ge sp i st rs0 m0 rs m:
   sem_local_istate ge sp (st.(curr)) rs0 m0 rs m ->