lemma on HC_set_reg

2 files changed, 165 insertions, 52 deletions

diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v
index b007a07e..6e86bebb 100644
--- a/scheduling/BTL_SEimpl.v
+++ b/scheduling/BTL_SEimpl.v
@@ -400,10 +400,10 @@ Definition root_happly (rsv: root_sval) (lr: list reg) (hrs: ristate): ?? sval :
   end.
 
 Lemma root_happly_correct (rsv: root_sval) lr hrs:
-  WHEN root_happly rsv lr hrs ~> sv THEN forall ctx st
-  (REF: ris_refines ctx hrs st)
+  WHEN root_happly rsv lr hrs ~> sv THEN forall ctx sis
+  (REF: ris_refines ctx hrs sis)
   (OK: ris_ok ctx hrs),
-  sval_refines ctx sv (rsv lr st).
+  sval_refines ctx sv (rsv lr sis).
 Proof.
   unfold root_apply, root_happly; destruct rsv; wlp_simplify; inv REF;
   erewrite H0, H; eauto.
@@ -472,16 +472,16 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hrs: ristate): ?? sval :=
            end*)
      end
   | Rload _ chunk addr => 
-       DO lhsv <~ hlist_args hrs lr;;
-       hSload hrs NOTRAP chunk addr lhsv
+       DO lsv <~ hlist_args hrs lr;;
+       hSload hrs NOTRAP chunk addr lsv
   end.
 
 Lemma simplify_correct rsv lr hrs:
-  WHEN simplify rsv lr hrs ~> hv THEN forall ctx st
-    (REF: ris_refines ctx hrs st)
+  WHEN simplify rsv lr hrs ~> hv THEN forall ctx sis
+    (REF: ris_refines ctx hrs sis)
     (OK0: ris_ok ctx hrs)
-    (OK1: eval_sval ctx (rsv lr st) <> None),
-    sval_refines ctx hv (rsv lr st).
+    (OK1: eval_sval ctx (rsv lr sis) <> None),
+    sval_refines ctx hv (rsv lr sis).
 Proof.
   destruct rsv; simpl; auto.
   - (* Rop *)
@@ -500,22 +500,22 @@ Proof.
       * rewrite H1 in OK1; congruence.
     + erewrite H0; eauto.
 Qed.
+Global Opaque simplify.
+Local Hint Resolve simplify_correct: wlp.
+
+Definition red_PTree_set (r: reg) (sv: sval) (hrs: ristate): PTree.t sval :=
+  match (ris_input_init hrs), sv with
+  | true, Sinput r' _ =>
+      if Pos.eq_dec r r' 
+      then PTree.remove r' hrs
+      else PTree.set r sv hrs
+  | false, Sundef _ =>
+      PTree.remove r hrs
+  | _, _ => PTree.set r sv hrs
+  end.
 
-Definition red_PTree_set (r: reg) (sv: sval) (hrs: ristate): ristate :=
-  let sreg :=
-    match (ris_input_init hrs), sv with
-    | true, Sinput r' _ =>
-        if Pos.eq_dec r r' 
-        then PTree.remove r' hrs
-        else PTree.set r sv hrs
-    | false, Sundef _ =>
-        PTree.remove r hrs
-    | _, _ => PTree.set r sv hrs
-    end in
-  ris_sreg_set hrs sreg.
-
-Lemma red_PTree_set_correct (r r0:reg) sv hrs ctx:
-  sval_refines ctx ((red_PTree_set r sv hrs) r0) ((ris_sreg_set hrs (PTree.set r sv hrs)) r0).
+Lemma red_PTree_set_correct (r r0:reg) sv (hrs: ristate) ctx:
+  sval_refines ctx ((ris_sreg_set hrs (red_PTree_set r sv hrs)) r0) ((ris_sreg_set hrs (PTree.set r sv hrs)) r0).
 Proof.
   unfold red_PTree_set, ris_sreg_set, ris_sreg_get; simpl.
   destruct (ris_input_init hrs) eqn:Hinit, sv; simpl; auto.
@@ -526,11 +526,11 @@ Proof.
          rewrite PTree.gro, PTree.gso; simpl; auto].
 Qed.
 
-Lemma red_PTree_set_refines (r r0:reg) ctx hrs st sv1 sv2:
- ris_refines ctx hrs st ->
+Lemma red_PTree_set_refines (r r0:reg) ctx hrs sis sv1 sv2:
+ ris_refines ctx hrs sis ->
  sval_refines ctx sv1 sv2 ->
  ris_ok ctx hrs ->
- sval_refines ctx ((red_PTree_set r sv1 hrs) r0) (if Pos.eq_dec r r0 then sv2 else si_sreg st r0).
+ sval_refines ctx (ris_sreg_set hrs (red_PTree_set r sv1 hrs) r0) (if Pos.eq_dec r r0 then sv2 else si_sreg sis r0).
 Proof.
   intros REF SREF OK; rewrite red_PTree_set_correct.
   unfold ris_sreg_set, ris_sreg_get.
@@ -551,11 +551,11 @@ Definition cbranch_expanse (prev: ristate) (cond: condition) (args: list reg): ?
     (*end.*)
 
 Lemma cbranch_expanse_correct hrs c l:
- WHEN cbranch_expanse hrs c l ~> r THEN forall ctx st
-  (REF : ris_refines ctx hrs st)
+ WHEN cbranch_expanse hrs c l ~> r THEN forall ctx sis
+  (REF : ris_refines ctx hrs sis)
   (OK: ris_ok ctx hrs),
   eval_scondition ctx (fst r) (snd r) =
-  eval_scondition ctx c (list_sval_inj (map (si_sreg st) l)).
+  eval_scondition ctx c (list_sval_inj (map (si_sreg sis) l)).
 Proof.
   unfold cbranch_expanse.
   wlp_simplify; inv REF.
@@ -586,43 +586,145 @@ Proof.
     intros; rewrite PTree.gempty; eauto.
 Qed.
 
-Fixpoint hrexec_rec f ib ris (k: ristate -> rstate): ?? rstate := 
+Definition hrset_sreg r lr rsv (hrs: ristate): ?? ristate :=
+  DO ok_lsv <~
+    (if may_trap rsv lr
+     then DO hv <~ root_happly rsv lr hrs;;
+          XDEBUG hv (fun hv => DO hv_name <~ string_of_hashcode (sval_get_hid hv);; RET ("-- insert undef behavior of hashcode:" +; (CamlStr hv_name))%string);;
+          RET (hv::(ok_rsval hrs))
+     else RET (ok_rsval hrs));;
+  DO simp <~ simplify rsv lr hrs;;
+  RET {| ris_smem := hrs.(ris_smem);
+         ris_input_init := hrs.(ris_input_init);
+         ok_rsval := ok_lsv;
+         ris_sreg:= red_PTree_set r simp hrs |}.
+
+Lemma ok_hrset_sreg (rsv:root_sval) ctx (st: sistate) r lr:
+  si_ok ctx (set_sreg r (rsv lr st) st)
+  <-> (si_ok ctx st /\ eval_sval ctx (rsv lr st) <> None).
+Proof.
+  unfold set_sreg; simpl; split.
+  - intros. destruct H as [[OK_SV OK_PRE] OK_SMEM OK_SREG]; simpl in *.
+    repeat (split; try tauto).
+    + intros r0; generalize (OK_SREG r0); clear OK_SREG; destruct (Pos.eq_dec r r0); try congruence.
+    + generalize (OK_SREG r); clear OK_SREG; destruct (Pos.eq_dec r r); try congruence.
+  - intros (OK & SEVAL). inv OK.
+    repeat (split; try tauto; eauto).
+    intros r0; destruct (Pos.eq_dec r r0) eqn:Heq; simpl;
+    rewrite Heq; eauto.
+Qed.
+
+(* TODO gourdinl move this in BTL_SEtheory? *)
+Lemma eval_list_sval_inj_not_none ctx st: forall l,
+  (forall r, List.In r l -> eval_sval ctx (si_sreg st r) = None -> False) ->
+  eval_list_sval ctx (list_sval_inj (map (si_sreg st) l)) = None -> False.
+Proof.
+  induction l.
+  - intuition discriminate.
+  - intros ALLR. simpl.
+    inversion_SOME v.
+    + intro SVAL. inversion_SOME lv; [discriminate|].
+      assert (forall r : reg, In r l -> eval_sval ctx (si_sreg st r) = None -> False).
+      { intros r INR. eapply ALLR. right. assumption. }
+      intro SVALLIST. intro. eapply IHl; eauto.
+    + intros. exploit (ALLR a); simpl; eauto.
+Qed.
+
+Lemma hrset_sreg_correct r lr rsv hrs:
+  WHEN hrset_sreg r lr rsv hrs ~> hrs' THEN forall ctx sis
+  (REF: ris_refines ctx hrs sis),
+  ris_refines ctx hrs' (set_sreg r (rsv lr sis) sis).
+Proof.
+  wlp_simplify; inversion REF.
+  - (* may_trap -> true *)
+    assert (X: si_ok ctx (set_sreg r (rsv lr sis) sis) <->
+               ris_ok ctx {| ris_smem := hrs;
+                             ris_input_init := ris_input_init hrs;
+                             ok_rsval := exta :: ok_rsval hrs;
+                             ris_sreg := red_PTree_set r exta0 hrs |}).
+    {
+      rewrite ok_hrset_sreg, OK_EQUIV.
+      split.
+      + intros (ROK & SEVAL); inv ROK.
+        assert (ROK: ris_ok ctx hrs) by (econstructor; eauto).
+        econstructor; eauto; simpl.
+        intuition (subst; eauto).
+        erewrite H0 in *; eauto.
+      + intros (OK_RMEM & OK_RREG); simpl in *.
+        assert (ROK: ris_ok ctx hrs) by (econstructor; eauto).
+        erewrite <- H0 in *; eauto. }
+    split; auto; rewrite <- X, ok_hrset_sreg.
+    + intuition eauto.
+    + intros (SOK & SEVAL) r0.
+      rewrite ris_sreg_set_access.
+      erewrite red_PTree_set_refines; intuition eauto.
+  - (* may_trap -> false *)
+    assert (X: si_ok ctx (set_sreg r (rsv lr sis) sis) <->
+               ris_ok ctx {| ris_smem := hrs;
+                             ris_input_init := ris_input_init hrs;
+                             ok_rsval := ok_rsval hrs;
+                             ris_sreg := red_PTree_set r exta hrs |}).
+    {
+      rewrite ok_hrset_sreg, OK_EQUIV.
+      split.
+      + intros (ROK & SEVAL); inv ROK.
+        econstructor; eauto.
+      + intros (OK_RMEM & OK_RREG).
+        assert (ROK: ris_ok ctx hrs) by (econstructor; eauto).
+        split; auto.
+        intros SNONE; exploit may_trap_correct; eauto.
+        * intros LNONE; eapply eval_list_sval_inj_not_none; eauto.
+          assert (SOK: si_ok ctx sis) by intuition.
+          inv SOK. intuition eauto.
+        * rewrite <- MEM_EQ; auto. }
+    split; auto; rewrite <- X, ok_hrset_sreg.
+    + intuition eauto.
+    + intros (SOK & SEVAL) r0.
+      rewrite ris_sreg_set_access.
+      erewrite red_PTree_set_refines; intuition eauto.
+Qed.
+
+Fixpoint hrexec_rec f ib hrs (k: ristate -> ?? rstate): ?? rstate := 
   match ib with
-  (*| BF fin _ => Rfinal (tr_ris f fin ris) (sexec_final_sfv fin ris)*)
+  | BF fin _ => RET (Rfinal (tr_ris f fin hrs) (sexec_final_sfv fin hrs))
   (* basic instructions *)
-  | Bnop _ => RET (k ris)
-  | Bop op args res _ =>
-      DO next <~ ris_sreg_set hrs 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
-  | Bstore chunk addr args src _ => k (rexec_store chunk addr args src ris)
+  | Bnop _ => k hrs
+  | Bop op args dst _ =>
+      DO next <~ hrset_sreg dst args (Rop op) hrs;;
+      k next
+  | Bload TRAP chunk addr args dst _ =>
+      DO next <~ hrset_sreg 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
  (* composed instructions *)
   | Bseq ib1 ib2 =>
-      rexec_rec f ib1 ris (fun ris2 => rexec_rec f ib2 ris2 k)
+      hrexec_rec f ib1 hrs (fun hrs2 => hrexec_rec f ib2 hrs2 k)
   | Bcond cond args ifso ifnot _ =>
-      let args := list_sval_inj (List.map ris args) in
-      let ifso := rexec_rec f ifso ris k in
-      let ifnot := rexec_rec f ifnot ris k in
-      Rcond cond args ifso ifnot
-
-  (* TODO to remove *)
-  | _ => RET (k ris)
+      DO res <~ cbranch_expanse hrs cond args;;
+      let (cond, vargs) := res in
+      DO ifso <~ hrexec_rec f ifso hrs k;;
+      DO ifnot <~ hrexec_rec f ifnot hrs k;;
+      RET (Rcond cond vargs ifso ifnot)
   end
   .
 
-Definition hrexec f ib := hrexec_rec f ib hris_init (fun _ => Rabort).
+Definition hrexec f ib :=
+  DO init <~ hris_init;;
+  hrexec_rec f ib init (fun _ => RET Rabort).
 
-Definition hsexec (f: function) (pc:node): ?? ristate :=
+Definition hsexec (f: function) (pc:node): ?? rstate :=
   DO path <~ some_or_fail ((fn_code f)!pc) "hsexec.internal_error.1";;
-  DO hinit <~ init_ristate;;
-  DO hst <~ hsiexec_path path.(psize) f hinit;;
+  (*DO hinit <~ init_ristate;;*)
+  DO hst <~ hrexec f f.(fn_entrypoint);;
   DO i <~ some_or_fail ((fn_code f)!(hst.(hsi_pc))) "hsexec.internal_error.2";;
   DO ohst <~ hsiexec_inst i hst;;
   match ohst with
   | Some hst' => RET {| hinternal := hst'; hfinal := HSnone |}
   | None => DO hsvf <~ hsexec_final i hst.(hsi_local);;
             RET {| hinternal := hst; hfinal := hsvf |}
-   end.*)
+   end.
 
 End CanonBuilding.
diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index 60c49e04..c812c607 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -44,6 +44,17 @@ Definition ris_sreg_set (ris: ristate) (sreg: PTree.t sval): ristate :=
      ok_rsval := ok_rsval ris;
      ris_sreg := sreg |}.
 
+Lemma ris_sreg_set_access (ris: ristate) (sreg: PTree.t sval) r smem rsval:
+  {| ris_smem := smem;
+     ris_input_init := ris_input_init ris;
+     ok_rsval := rsval;
+     ris_sreg := sreg |} r =
+  ris_sreg_set ris sreg r.
+Proof.
+  unfold ris_sreg_set, ris_sreg_get; simpl.
+  reflexivity.
+Qed.
+
 Record ris_ok ctx (ris: ristate) : Prop := {
   OK_RMEM: (eval_smem ctx (ris_smem ris)) <> None;
   OK_RREG: forall sv, List.In sv (ok_rsval ris) -> eval_sval ctx sv <> None