Merge branch 'mppa-RTLpathSE-verif' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-RTLpathSE-verif

4 files changed, 183 insertions, 34 deletions

diff --git a/kvx/lib/RTLpathSE_impl.v b/kvx/lib/RTLpathSE_impl.v
index 480b647f..a1bd8638 100644
--- a/kvx/lib/RTLpathSE_impl.v
+++ b/kvx/lib/RTLpathSE_impl.v
@@ -513,15 +513,15 @@ Proof.
   - simpl in CORE. rewrite <- CORE. constructor; [apply svident_simu_refl|].
     erewrite <- list_sval_eval_preserved; [| eapply ctx]. constructor.
   (* Sbuiltin *)
-  - simpl in CORE. destruct hf2; try contradiction. destruct CORE as (PCEQ & ? & ? & ?). subst.
-    constructor; [assumption | reflexivity].
+  - (* simpl in CORE. destruct hf2; try contradiction. destruct CORE as (PCEQ & ? & ? & ?). subst.
+    constructor; [assumption | reflexivity]. *) admit.
   (* Sjumptable *)
   - simpl in CORE. destruct hf2; try contradiction. destruct CORE as (PCEQ & ?). subst.
     constructor; [assumption|].
     erewrite <- seval_preserved; [| eapply ctx]. constructor.
   (* Sreturn *)
   - simpl in CORE. subst. constructor.
-Qed.
+Admitted.
 
 Record hsstate := { hinternal:> hsistate; hfinal: sfval }.
 
@@ -1612,9 +1612,9 @@ Proof.
     + admit.
     + admit.
   (* Sbuiltin *)
-  - destruct fv2; try discriminate. intro. explore.
+  - (* destruct fv2; try discriminate. intro. explore.
     apply revmap_check_single_correct in EQ1. apply list_builtin_arg_simub_correct in EQ2.
-    subst. constructor; auto.
+    subst. constructor; auto. *) admit.
   (* Sjumptable *)
   - destruct fv2; try discriminate. intro. explore.
     apply revmap_check_list_correct in EQ. apply sval_simub_correct in EQ0. subst.
diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v
index 7a017047..342c9f30 100644
--- a/kvx/lib/RTLpathSE_impl_junk.v
+++ b/kvx/lib/RTLpathSE_impl_junk.v
@@ -577,9 +577,9 @@ Proof.
 Qed.
 
 Definition hsilocal_simu_core (oalive: option Regset.t) (hst1 hst2: hsistate_local) :=
-(*      is_subset (hsi_lsmem hst2) (hsi_lsmem hst1) *)
      incl (hsi_ok_lsval hst2) (hsi_ok_lsval hst1)
-  /\ (forall r, (match oalive with Some alive => Regset.In r alive | _ => True end) -> hsi_sreg_get hst2 r = hsi_sreg_get hst1 r)
+  /\ (forall r, (match oalive with Some alive => Regset.In r alive | _ => True end) -> (* hsi_sreg_get hst2 r = hsi_sreg_get hst1 r *)
+              PTree.get r hst2 = PTree.get r hst1)
   /\ hsi_smem hst1 = hsi_smem hst2.
 
 Lemma hseval_preserved ge ge' rs0 m0 sp hsv:
@@ -621,7 +621,7 @@ Definition seval_sval_partial ge sp rs0 m0 hsv :=
 Definition select_first (ox oy: option val) :=
   match ox with
   | Some v => Some v
-  | None => SOME v <- oy IN Some v
+  | None => oy
   end.
 
 (** If the register was computed by hrs, evaluate the symbolic value from hrs.
@@ -684,16 +684,21 @@ Proof.
       ++ unfold seval_sval_partial.
          assert (seval_hsval ge2 sp h rs0 m0 = hsi_sreg_eval ge2 sp hst2 r rs0 m0). {
            unfold hsi_sreg_eval. rewrite HST2. reflexivity. }
-         rewrite H. clear H. assert (TODO: exists hv, hsi_sreg_get hst2 r ~~> hv) by admit.
-         destruct TODO as (hv & HGET2). rewrite hsi_sreg_eval_correct; [|eassumption].
-         rewrite C in HGET2; [|assumption]. erewrite hseval_preserved; [| eapply GFS].
-         rewrite <- hsi_sreg_eval_correct; [|eassumption]. rewrite B; [|assumption].
-         rewrite RSEQ. reflexivity.
-      ++ rewrite <- RSEQ. rewrite <- B; [|assumption].
-         assert (TODO: exists hv, hsi_sreg_get hst1 r ~~> hv) by admit.
+         rewrite H. clear H. (*assert (TODO: exists hv, hsi_sreg_get hst2 r ~~> hv) by admit.
+         destruct TODO as (hv & HGET2). rewrite hsi_sreg_eval_correct; [|eassumption].*)
+         unfold hsi_sreg_eval. rewrite HST2.
+         erewrite hseval_preserved; [| eapply GFS].
+         unfold hsi_sreg_eval in B.
+         generalize (B HOK1 r); clear B; intro B.
+         rewrite <- C in B; eauto.
+         rewrite HST2 in B.
+         rewrite B, RSEQ.
+         reflexivity.
+      ++ rewrite <- RSEQ. rewrite <- B; [|assumption]. admit. (* FIXME *)
+(*          assert (TODO: exists hv, hsi_sreg_get hst1 r ~~> hv) by admit.
          destruct TODO as (hv & HGET1). rewrite hsi_sreg_eval_correct; [|eassumption].
          rewrite <- C in HGET1; [|assumption].  rewrite <- hsi_sreg_eval_correct; [|eassumption].
-         unfold hsi_sreg_eval. rewrite HST2. reflexivity.
+         unfold hsi_sreg_eval. rewrite HST2. reflexivity. *)
   - constructor; [|constructor].
     + destruct HREF2 as (OKEQ & _ & _). rewrite <- OKEQ in HOK2. apply HOK2.
     + destruct HREF2 as (_ & MEMEQ2 & _). destruct HREF1 as (_ & MEMEQ1 & _).
@@ -701,13 +706,13 @@ Proof.
       rewrite <- MEMEQ2; auto. rewrite <- MEMEQ3. erewrite hsmem_eval_preserved; [| eapply GFS].
       rewrite MEMEQ1; auto.
     + intro r. destruct HREF2 as (_ & _ & A & _). destruct HREF1 as (_ & _ & B & _).
-      destruct CORE as (_ & C & _). rewrite <- A; auto.
-      assert (TODO: exists hv, hsi_sreg_get hst2 r ~~> hv) by admit. destruct TODO as (hv & HGET2).
+      destruct CORE as (_ & C & _). rewrite <- A; auto. admit. (* FIXME *)
+(*       assert (TODO: exists hv, hsi_sreg_get hst2 r ~~> hv) by admit. destruct TODO as (hv & HGET2).
       rewrite hsi_sreg_eval_correct; [|eassumption].
       rewrite C in HGET2; [|auto]. erewrite hseval_preserved; [| eapply GFS].
       rewrite <- hsi_sreg_eval_correct; [|eassumption].
       rewrite B; auto.
-Admitted. (** FIXME - requires to add some hypothesis that hsi_sreg_get may return something *)
+ *)Admitted. (** FIXME - requires to add some hypothesis that hsi_sreg_get may return something *)
 
 Definition hsilocal_simu_check hst1 hst2 : ?? unit :=
   phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_simu_check: hsi_smem sets aren't equiv";;
@@ -747,14 +752,17 @@ Proof.
   apply setoid_in. assumption.
 Qed.
 
+Local Hint Resolve PTree_frame_eq_check_correct: wlp.
+Local Hint Resolve regset_elements_in: core.
+
 Theorem hsilocal_frame_simu_check_correct hst1 hst2 alive:
   WHEN hsilocal_frame_simu_check (Regset.elements alive) hst1 hst2 ~> tt THEN
   hsilocal_simu_core (Some alive) hst1 hst2.
 Proof.
   wlp_simplify. constructor; [|constructor]; [assumption | | congruence].
-  intros. unfold hsi_sreg_get.
-  rewrite (PTree_frame_eq_check_correct _ (Regset.elements alive) hst1 hst2); [reflexivity | eassumption | ].
-  apply regset_elements_in. assumption.
+  intros. symmetry. eauto.
+(*   rewrite (PTree_frame_eq_check_correct _ (Regset.elements alive) hst1 hst2); [reflexivity | eassumption | ].
+  apply regset_elements_in. assumption. *)
 Qed.
 Hint Resolve hsilocal_frame_simu_check_correct: wlp.
 Global Opaque hsilocal_frame_simu_check.
@@ -937,14 +945,11 @@ Theorem hsiexits_simu_check_correct dm f: forall le1 le2,
   WHEN hsiexits_simu_check dm f le1 le2 ~> tt THEN
   hsiexits_simu_core dm f le1 le2.
 Proof.
-  induction le1; intros; wlp_simplify.
-  - destruct le2; [constructor|]. simpl in Hexta. (* Absurd case *) admit.
-  - destruct le2.
-    + (* Absurd case again *) admit.
-    + assert (hsiexit_simu_check dm f a h ~~> tt /\ hsiexits_simu_check dm f le1 le2 ~~> exta). { admit. }
-      destruct H as (A & B). apply hsiexit_simu_check_correct in A.
-      constructor; [assumption|]. apply IHle1 in B. assumption.
-Admitted.
+  induction le1; simpl.
+  - destruct le2; wlp_simplify. constructor.
+  - destruct le2; wlp_simplify. constructor; [assumption|].
+    eapply IHle1. eassumption.
+Qed.
 Hint Resolve hsiexits_simu_check_correct: wlp.
 Global Opaque hsiexits_simu_check.
 
@@ -1258,6 +1263,27 @@ Proof.
     erewrite IHlist_refines; eauto.
 Qed.
 
+Lemma barg_proj_refines_eq ge ge' sp rs0 m0: forall lsv lhsv,
+  (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) ->
+  list_forall2 (barg_refines ge sp rs0 m0) lhsv lsv ->
+  forall lhsv' lsv',
+  list_forall2 (barg_refines ge' sp rs0 m0) lhsv' lsv' ->
+  barg_list_proj lhsv = barg_list_proj lhsv' ->
+  seval_list_builtin_sval ge sp lsv rs0 m0 = seval_list_builtin_sval ge' sp lsv' rs0 m0.
+Proof.
+  induction 2; rename H into GFS.
+  - simpl. intros. destruct lhsv'; try discriminate. clear H0.
+    inv H. simpl. reflexivity.
+  - simpl. intros. destruct lhsv'; try discriminate.
+    simpl in H2. inv H2. destruct lsv'; [inv H|].
+    inv H. simpl.
+    assert (SVALEQ: seval_builtin_sval ge sp b1 rs0 m0 = seval_builtin_sval ge' sp b0 rs0 m0). {
+      admit.
+(*       rewrite <- H10. rewrite <- H1. unfold seval_hsval. erewrite <- seval_preserved; [| eapply GFS]. congruence. *)
+    } rewrite SVALEQ.
+    erewrite IHlist_forall2; eauto.
+Admitted.
+
 Definition final_simu_core (dm: PTree.t node) (f: RTLpath.function) (pc1 pc2: node) (f1 f2: sfval): Prop :=
   match f1 with
   | Scall sig1 svos1 lsv1 res1 pc1 =>
@@ -1328,9 +1354,27 @@ Proof.
         simpl in SVOSEQ. inv SVOSEQ. congruence.
     + erewrite list_proj_refines_eq; eauto. constructor.
   (* Stailcall *)
-  - admit.
+  - rename H3 into SREF1. rename H4 into LREF1.
+    destruct hf2; try (inv CORE; fail). inv FREF2.
+    rename H4 into LREF2. rename H3 into SREF2.
+    inv CORE. rename H1 into SVOSEQ. rename H2 into LSVEQ.
+    constructor.
+    + destruct svos. (** Copy-paste from Scall *)
+      * destruct svos0; try discriminate. destruct ros; try contradiction.
+        destruct ros0; try contradiction. constructor.
+        simpl in SVOSEQ. inv SVOSEQ.
+        simpl in SREF1. simpl in SREF2.
+        rewrite <- SREF1. rewrite <- SREF2. unfold seval_hsval.
+        erewrite <- seval_preserved; [| eapply GFS]. congruence.
+      * destruct svos0; try discriminate. destruct ros; try contradiction.
+        destruct ros0; try contradiction. constructor.
+        simpl in SVOSEQ. inv SVOSEQ. congruence.
+    + erewrite list_proj_refines_eq; eauto. constructor.
   (* Sbuiltin *)
-  - admit.
+  - rename H4 into BREF1. destruct hf2; try (inv CORE; fail). inv FREF2.
+    rename H4 into BREF2. inv CORE. destruct H0 as (? & ? & ?). subst.
+    rename H into PCEQ. rename H1 into ARGSEQ. constructor; [assumption|]. clear PCEQ.
+    admit. (* too strong to prove *)
   (* Sjumptable *)
   - admit.
   (* Sreturn *)
diff --git a/kvx/lib/RTLpathSE_theory.v b/kvx/lib/RTLpathSE_theory.v
index ad8d899e..3ae6e713 100644
--- a/kvx/lib/RTLpathSE_theory.v
+++ b/kvx/lib/RTLpathSE_theory.v
@@ -1715,6 +1715,108 @@ Proof.
       constructor; eauto. congruence.
 Qed.
 
+Fixpoint seval_builtin_sval ge sp bsv rs0 m0 := match bsv with
+  | BA sv => SOME v <- seval_sval ge sp sv rs0 m0 IN Some (BA v)
+  | BA_splitlong sv1 sv2 =>
+      SOME v1 <- seval_builtin_sval ge sp sv1 rs0 m0 IN
+      SOME v2 <- seval_builtin_sval ge sp sv2 rs0 m0 IN
+      Some (BA_splitlong v1 v2)
+  | BA_addptr sv1 sv2 =>
+      SOME v1 <- seval_builtin_sval ge sp sv1 rs0 m0 IN
+      SOME v2 <- seval_builtin_sval ge sp sv2 rs0 m0 IN
+      Some (BA_addptr v1 v2)
+  | BA_int i => Some (BA_int i)
+  | BA_long l => Some (BA_long l)
+  | BA_float f => Some (BA_float f)
+  | BA_single s => Some (BA_single s)
+  | BA_loadstack chk ptr => Some (BA_loadstack chk ptr)
+  | BA_addrstack ptr => Some (BA_addrstack ptr)
+  | BA_loadglobal chk id ptr => Some (BA_loadglobal chk id ptr)
+  | BA_addrglobal id ptr => Some (BA_addrglobal id ptr)
+  end.
+
+Fixpoint seval_list_builtin_sval ge sp lbsv rs0 m0 := match lbsv with
+  | nil => Some nil
+  | bsv::lbsv => SOME v <- seval_builtin_sval ge sp bsv rs0 m0 IN
+                 SOME lv <- seval_list_builtin_sval ge sp lbsv rs0 m0 IN
+                 Some (v::lv)
+  end.
+
+Lemma seval_list_builtin_sval_nil ge sp rs0 m0 lbs2:
+  seval_list_builtin_sval ge sp lbs2 rs0 m0 = Some nil ->
+  lbs2 = nil.
+Proof.
+  destruct lbs2; simpl; auto.
+  intros. destruct (seval_builtin_sval _ _ _ _ _);
+    try destruct (seval_list_builtin_sval _ _ _ _ _); discriminate.
+Qed.
+
+Lemma seval_builtin_arg_sval ge sp m rs0 m0 v: forall bs,
+  seval_builtin_arg ge sp m rs0 m0 bs v ->
+  exists ba,
+    seval_builtin_sval ge sp bs rs0 m0 = Some ba
+    /\ eval_builtin_arg ge (fun id => id) sp m ba v.
+Proof.
+  induction 1.
+  all: try (eexists; constructor; [simpl; reflexivity | constructor]).
+  2-3: try assumption.
+  - eexists. constructor.
+    + simpl. rewrite H. reflexivity.
+    + constructor.
+  - destruct IHseval_builtin_arg1 as (ba1 & A1 & B1).
+    destruct IHseval_builtin_arg2 as (ba2 & A2 & B2).
+    eexists. constructor.
+    + simpl. rewrite A1. rewrite A2. reflexivity.
+    + constructor; assumption. 
+  - destruct IHseval_builtin_arg1 as (ba1 & A1 & B1).
+    destruct IHseval_builtin_arg2 as (ba2 & A2 & B2).
+    eexists. constructor.
+    + simpl. rewrite A1. rewrite A2. reflexivity.
+    + constructor; assumption.
+Qed.
+
+Lemma seval_builtin_args_sval ge sp m rs0 m0 lv: forall lbs,
+  seval_builtin_args ge sp m rs0 m0 lbs lv ->
+  exists lba,
+    seval_list_builtin_sval ge sp lbs rs0 m0 = Some lba
+    /\ list_forall2 (eval_builtin_arg ge (fun id => id) sp m) lba lv.
+Proof.
+  induction 1.
+  - eexists. constructor.
+    + simpl. reflexivity.
+    + constructor.
+  - destruct IHlist_forall2 as (lba & A & B).
+    apply seval_builtin_arg_sval in H. destruct H as (ba & A' & B').
+    eexists. constructor.
+    + simpl. rewrite A'. rewrite A. reflexivity.
+    + constructor; assumption.
+Qed.
+
+Lemma seval_builtin_sval_correct ge sp m rs0 m0 v bs2: forall bs1,
+  seval_builtin_arg ge sp m rs0 m0 bs1 v ->
+  opt_simu (seval_builtin_sval ge sp bs1 rs0 m0) (seval_builtin_sval ge sp bs2 rs0 m0) ->
+  seval_builtin_arg ge sp m rs0 m0 bs2 v.
+Proof.
+  induction 1.
+  - simpl. rewrite H. intros. lapply H0; [| discriminate]; clear H0; intro H0.
+Admitted.
+
+Lemma seval_list_builtin_sval_correct ge sp m rs0 m0 vargs: forall lbs1,
+  seval_builtin_args ge sp m rs0 m0 lbs1 vargs ->
+  forall lbs2, opt_simu (seval_list_builtin_sval ge sp lbs1 rs0 m0) (seval_list_builtin_sval ge sp lbs2 rs0 m0) ->
+  seval_builtin_args ge sp m rs0 m0 lbs2 vargs.
+Proof.
+  induction 1.
+  - simpl. intros. unfold opt_simu in H. lapply H; [|discriminate]; clear H; intro H.
+    exploit seval_list_builtin_sval_nil; eauto. intro. subst. constructor.
+  - eapply seval_builtin_arg_sval in H. destruct H as (ba & A & B).
+    eapply seval_builtin_args_sval in H0. destruct H0 as (lba & A' & B').
+    intros. destruct lbs2.
+    + simpl in H. rewrite A in H. rewrite A' in H. lapply H; [|discriminate]; clear H; intro H.
+      discriminate.
+    + constructor. 2: apply IHlist_forall2. 2: admit.
+Admitted.
+
 (* NOTE: we need to mix semantical simulation and syntactic definition on [sfval] in order to abstract the [match_states] *)
 Inductive sfval_simu (dm: PTree.t node) (f: RTLpath.function) (opc1 opc2: node) (ctx: simu_proof_context f): sfval -> sfval -> Prop :=
   | Snone_simu: 
@@ -1733,7 +1835,8 @@ Inductive sfval_simu (dm: PTree.t node) (f: RTLpath.function) (opc1 opc2: node)
       sfval_simu dm f opc1 opc2 ctx (Stailcall sig svos1 lsv1) (Stailcall sig svos2 lsv2)
   | Sbuiltin_simu ef lbs1 lbs2 br pc1 pc2:
       dm!pc2 = Some pc1 ->
-      lbs1 = lbs2 -> (* FIXME: TOO STRONG *)
+      opt_simu (seval_list_builtin_sval (the_ge1 ctx) (the_sp ctx) lbs1 (the_rs0 ctx) (the_m0 ctx))
+               (seval_list_builtin_sval (the_ge2 ctx) (the_sp ctx) lbs2 (the_rs0 ctx) (the_m0 ctx)) ->
       sfval_simu dm f opc1 opc2 ctx (Sbuiltin ef lbs1 br pc1) (Sbuiltin ef lbs2 br pc2)
   | Sjumptable_simu sv1 sv2 lpc1 lpc2:
       ptree_get_list dm lpc2 = Some lpc1 ->
diff --git a/kvx/lib/RTLpathSchedulerproof.v b/kvx/lib/RTLpathSchedulerproof.v
index 5c32847e..437f1e0a 100644
--- a/kvx/lib/RTLpathSchedulerproof.v
+++ b/kvx/lib/RTLpathSchedulerproof.v
@@ -215,6 +215,8 @@ Proof.
     intros (path & PATH).
     eexists; split; econstructor; eauto.
     + eapply seval_builtin_args_preserved; eauto.
+      eapply seval_list_builtin_sval_correct; eauto.
+      admit. (* something like seval_list_builtin_sval_preserved *)
     + eapply external_call_symbols_preserved; eauto.
     + eapply eqlive_reg_refl.
   - (* Sjumptable *)
@@ -229,7 +231,7 @@ Proof.
     + erewrite <- preserv_fnstacksize; eauto.
     + destruct os; auto.
       erewrite <- seval_preserved; eauto.
-Qed.
+Admitted.
 
 (* The main theorem on simulation of symbolic states ! *)
 Theorem ssem_sstate_simu dm f f' stk stk' sp st st' rs m t s: