1 files changed, 104 insertions, 1 deletions

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 ->