Branch expansions activated and configured in the checker (but admitted) and bugfix in the expansion liveness modification

2 files changed, 152 insertions, 54 deletions

diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 32c8731f..9a3518c0 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -442,7 +442,7 @@ let expanse (sb : superblock) code pm =
           exp := cbranch_int32u false c a1 a2 info succ1 succ2 [];
           was_branch := true;
           was_exp := true
-      (*| Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) ->
+      | Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) ->
           debug "Icond/Ccompimm\n";
           exp := expanse_cbranchimm_int32s c a1 imm info succ1 succ2 [];
           was_branch := true;
@@ -451,7 +451,7 @@ let expanse (sb : superblock) code pm =
           debug "Icond/Ccompuimm\n";
           exp := expanse_cbranchimm_int32u c a1 imm info succ1 succ2 [];
           was_branch := true;
-          was_exp := true*)
+          was_exp := true
       | Icond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, info) ->
           debug "Icond/Ccompl\n";
           exp := cbranch_int64s false c a1 a2 info succ1 succ2 [];
@@ -462,7 +462,7 @@ let expanse (sb : superblock) code pm =
           exp := cbranch_int64u false c a1 a2 info succ1 succ2 [];
           was_branch := true;
           was_exp := true
-      (*| Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) ->
+      | Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) ->
           debug "Icond/Ccomplimm\n";
           exp := expanse_cbranchimm_int64s c a1 imm info succ1 succ2 [];
           was_branch := true;
@@ -492,7 +492,7 @@ let expanse (sb : superblock) code pm =
           debug "Icond/Cnotcompfs\n";
           exp := expanse_cbranch_fp true cond_single c f1 f2 info succ1 succ2 [];
           was_branch := true;
-          was_exp := true*)
+          was_exp := true
       | _ -> new_order := n :: !new_order);
       if !was_exp then (
         node := !node + 1;
@@ -500,7 +500,8 @@ let expanse (sb : superblock) code pm =
          let lives = PTree.get n !liveins in
          match lives with
          | Some lives ->
-             liveins := PTree.set (n2p ()) lives !liveins;
+             let new_branch_pc = Camlcoq.P.of_int (!node - ((List.length !exp) - 1)) in
+             liveins := PTree.set new_branch_pc lives !liveins;
              liveins := PTree.remove n !liveins
          | _ -> ());
         write_pathmap sb.instructions.(0) (List.length !exp) pm';
diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v
index b7b58ae5..32761c6e 100644
--- a/scheduling/RTLpathSE_impl.v
+++ b/scheduling/RTLpathSE_impl.v
@@ -893,6 +893,12 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hs
         let optR0 := make_optR0 false is_inv in
         DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
         cond_int64u c lhsv optR0
+    | (Ccomplimm c imm), a1 :: nil =>
+        DO hv1 <~ hsi_sreg_get hst a1;;
+        expanse_condimm_int64s c hv1 imm
+    | (Ccompluimm c imm), a1 :: nil =>
+        DO hv1 <~ hsi_sreg_get hst a1;;
+        expanse_condimm_int64u c hv1 imm
     | (Ccompf c), f1 :: f2 :: nil =>
         DO hv1 <~ hsi_sreg_get hst f1;;
         DO hv2 <~ hsi_sreg_get hst f2;;
@@ -917,12 +923,6 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hs
         let is_inv := is_inv_cmp_float c in
         DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
         expanse_cond_fp true cond_single c lhsv
-    | (Ccomplimm c imm), a1 :: nil =>
-        DO hv1 <~ hsi_sreg_get hst a1;;
-        expanse_condimm_int64s c hv1 imm
-    | (Ccompluimm c imm), a1 :: nil =>
-        DO hv1 <~ hsi_sreg_get hst a1;;
-        expanse_condimm_int64u c hv1 imm
     | _, _ =>
         DO lhsv <~ hlist_args hst lr;;
         hSop op lhsv
@@ -1317,7 +1317,7 @@ Proof.
   rewrite Int.sub_zero_l. unfold Int.shru, Int.shl.
  *)
 
-(* TODO gourdinl Lemma simplify_ccompuimm_correct: forall c n r (hst: hsistate_local),
+Lemma simplify_ccompuimm_correct: forall c n r (hst: hsistate_local),
   WHEN DO hv1 <~ hsi_sreg_get hst r;; expanse_condimm_int32u c hv1 n ~> hv
   THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) 
           (m0 : mem) (st : sistate_local),
@@ -1355,51 +1355,37 @@ Proof.
     simplify_SOME z; unfold Val.cmpu, zero32; intros; try contradiction.
     + apply mkimm_single_equal in EQMKI; subst.
       rewrite Int.add_commut, Int.add_zero_l. trivial.
-    + 
-
-  2: { intros. destruct (Int.eq n Int.zero) eqn:EQIMM; simpl.
-       2: { unfold loadimm32. destruct (make_immed32 n) eqn:EQMKI.
-            2: { 
-                wlp_simplify;
-                destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
-                all: try (simplify_SOME z; contradiction; fail);
+    + admit.
+    + admit.
+  - (* TODO gourdinl same as first goal *)
+    wlp_simplify;
+    destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
+    all: try (simplify_SOME z; contradiction; fail).
     try erewrite H9; eauto; try erewrite H8; eauto;
     try erewrite H7; eauto; try erewrite H6; eauto; try erewrite H5; eauto;
     try erewrite H4; eauto; try erewrite H3; eauto; try erewrite H2; eauto;
     try erewrite H1; eauto; try erewrite H0; eauto; try erewrite H; eauto;
     simplify_SOME z; unfold Val.cmpu, zero32; intros; try contradiction.
-    2: {
-    apply mkimm_single_equal in EQMKI; subst.
-    rewrite Int.add_commut, Int.add_zero_l. trivial.
-
-
-  2: {
+    apply Int.same_if_eq in EQIMM; subst. trivial.
+  - admit.
+  - (* TODO gourdinl same as first goal *)
     wlp_simplify;
     destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
-  all: try (simplify_SOME z; contradiction; fail).
-
-  2: {
-
-  all:
-    try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto);
+    all: try (simplify_SOME z; contradiction; fail).
+    try erewrite H9; eauto; try erewrite H8; eauto;
+    try erewrite H7; eauto; try erewrite H6; eauto; try erewrite H5; eauto;
     try erewrite H4; eauto; try erewrite H3; eauto; try erewrite H2; eauto;
     try erewrite H1; eauto; try erewrite H0; eauto; try erewrite H; eauto;
-    simplify_SOME z; unfold Val.cmp, zero32.
-  all:
-    try apply Int.same_if_eq in H0; subst; trivial.
-
-  erewrite H0.
-
-
-    - intros; apply xor_neg_ltle_cmpu.
-    - intros; replace (Clt) with (swap_comparison Cgt) by auto;
-      rewrite Val.swap_cmpu_bool; trivial.
-    - intros; replace (Clt) with (negate_comparison Cge) by auto;
-      rewrite Val.negate_cmpu_bool.
-      rewrite xor_neg_optb; trivial.
-Qed.
-
- *)
+    simplify_SOME z; unfold Val.cmpu, zero32; intros; try contradiction.
+    apply Int.same_if_eq in EQIMM; subst. trivial.
+  - (* same *) admit.
+  - (* same *) admit.
+  - (* same *) admit.
+  - (* same *) admit.
+  - (* same *) admit.
+  - (* same *) admit.
+  - (* same *) admit.
+Admitted.
 
 Lemma simplify_ccompl_correct: forall c r r0 (hst: hsistate_local),
   WHEN DO hv1 <~ hsi_sreg_get hst r;;
@@ -1791,7 +1777,7 @@ Proof.
     rewrite <- X, sok_local_set_sreg. intuition eauto.
     - destruct REF; intuition eauto.
     - generalize REF; intros (OKEQ & _). rewrite OKEQ in * |-; erewrite red_PTree_set_refines; eauto.
-Qed.
+     Qed.
 Global Opaque hslocal_set_sreg.
 Local Hint Resolve hslocal_set_sreg_correct: wlp.
 
@@ -1843,6 +1829,13 @@ Definition transl_cbranch_int64u (cmp: comparison) (optR0: option bool) :=
   | Cge => CEbgeul optR0
   end.
 
+Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) : ?? (condition * list_hsval) :=
+  let normal := is_normal_cmp cmp in
+  let normal' := if cnot then negb normal else normal in
+  DO hvs <~ fn_cond cmp lhsv;;
+  DO hl <~ make_lhsv_cmp false hvs hvs;;
+  if normal' then RET ((CEbnew (Some false)), hl) else RET ((CEbeqw (Some false)), hl).
+  
 Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : ?? (condition * list_hsval) :=
   match cond, args with
   | (Ccomp c), (a1 :: a2 :: nil) =>
@@ -1859,6 +1852,30 @@ Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list
       DO hv2 <~ hsi_sreg_get prev a2;;
       DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
       RET (cond, lhsv)
+  | (Ccompimm c n), (a1 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      DO hv1 <~ hsi_sreg_get prev a1;;
+      (if Int.eq n Int.zero then
+        DO lhsv <~ make_lhsv_cmp is_inv hv1 hv1;;
+        let cond := transl_cbranch_int32s c (make_optR0 true is_inv) in
+        RET (cond, lhsv)
+      else
+        DO hvs <~ loadimm32 n;;
+        DO lhsv <~ make_lhsv_cmp is_inv hv1 hvs;;
+        let cond := transl_cbranch_int32s c (make_optR0 false is_inv) in
+        RET (cond, lhsv))
+  | (Ccompuimm c n), (a1 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      DO hv1 <~ hsi_sreg_get prev a1;;
+      (if Int.eq n Int.zero then
+        DO lhsv <~ make_lhsv_cmp is_inv hv1 hv1;;
+        let cond := transl_cbranch_int32u c (make_optR0 true is_inv) in
+        RET (cond, lhsv)
+      else
+        DO hvs <~ loadimm32 n;;
+        DO lhsv <~ make_lhsv_cmp is_inv hv1 hvs;;
+        let cond := transl_cbranch_int32u c (make_optR0 false is_inv) in
+        RET (cond, lhsv))
   | (Ccompl c), (a1 :: a2 :: nil) =>
       let is_inv := is_inv_cmp_int c in
       let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in
@@ -1873,9 +1890,54 @@ Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list
       DO hv2 <~ hsi_sreg_get prev a2;;
       DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
       RET (cond, lhsv)
-      (*  | Icond (Ccompimm c n) (a1 :: nil) _ _ _ =>
-      let cond := transl_cbranch_int32s c (make_optR0 c) in
-         RET (cond, a1 :: a1 :: nil)*)
+  | (Ccomplimm c n), (a1 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      DO hv1 <~ hsi_sreg_get prev a1;;
+      (if Int64.eq n Int64.zero then
+        DO lhsv <~ make_lhsv_cmp is_inv hv1 hv1;;
+        let cond := transl_cbranch_int64s c (make_optR0 true is_inv) in
+        RET (cond, lhsv)
+      else
+        DO hvs <~ loadimm64 n;;
+        DO lhsv <~ make_lhsv_cmp is_inv hv1 hvs;;
+        let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in
+        RET (cond, lhsv))
+  | (Ccompluimm c n), (a1 :: nil) =>
+      let is_inv := is_inv_cmp_int c in
+      DO hv1 <~ hsi_sreg_get prev a1;;
+      (if Int64.eq n Int64.zero then
+        DO lhsv <~ make_lhsv_cmp is_inv hv1 hv1;;
+        let cond := transl_cbranch_int64u c (make_optR0 true is_inv) in
+        RET (cond, lhsv)
+      else
+        DO hvs <~ loadimm64 n;;
+        DO lhsv <~ make_lhsv_cmp is_inv hv1 hvs;;
+        let cond := transl_cbranch_int64u c (make_optR0 false is_inv) in
+        RET (cond, lhsv))
+  | (Ccompf c), (f1 :: f2 :: nil) =>
+      DO hv1 <~ hsi_sreg_get prev f1;;
+      DO hv2 <~ hsi_sreg_get prev f2;;
+      let is_inv := is_inv_cmp_float c in
+      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
+      expanse_cbranch_fp false cond_float c lhsv
+  | (Cnotcompf c), (f1 :: f2 :: nil) =>
+      DO hv1 <~ hsi_sreg_get prev f1;;
+      DO hv2 <~ hsi_sreg_get prev f2;;
+      let is_inv := is_inv_cmp_float c in
+      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
+      expanse_cbranch_fp true cond_float c lhsv
+  | (Ccompfs c), (f1 :: f2 :: nil) =>
+      DO hv1 <~ hsi_sreg_get prev f1;;
+      DO hv2 <~ hsi_sreg_get prev f2;;
+      let is_inv := is_inv_cmp_float c in
+      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
+      expanse_cbranch_fp false cond_single c lhsv
+  | (Cnotcompfs c), (f1 :: f2 :: nil) =>
+      DO hv1 <~ hsi_sreg_get prev f1;;
+      DO hv2 <~ hsi_sreg_get prev f2;;
+      let is_inv := is_inv_cmp_float c in
+      DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;;
+      expanse_cbranch_fp true cond_single c lhsv
   | _, _ =>
       DO vargs <~ hlist_args prev args;;
          RET (cond, vargs)
@@ -1984,7 +2046,7 @@ Lemma hsiexec_inst_correct i hst:
    exists st', siexec_inst i st = Some st'
     /\ (forall (REF:hsistate_refines_stat hst st), hsistate_refines_stat hst' st')
     /\ (forall ge sp rs0 m0 (REF:hsistate_refines_dyn ge sp rs0 m0 hst st), hsistate_refines_dyn ge sp rs0 m0 hst' st').
-Proof.
+Proof. Admitted. (*
   destruct i; simpl;
   try (wlp_simplify; try_simplify_someHyps; eexists; intuition eauto; fail).
   - (* refines_dyn Iop *)
@@ -2020,9 +2082,44 @@ Proof.
            destruct NEST as [|st0 se lse TOP NEST];
            econstructor; simpl; auto; constructor; auto.
     + admit.
+    + repeat (destruct l; try apply hsiexec_cond_noexp).
+      destruct (Int.eq _ _) eqn:EQIMM; simpl.
+      1: admit.
+      
+      unfold loadimm32; destruct make_immed32.
+      {
+      wlp_simplify; try_simplify_someHyps; eexists; intuition eauto.
+      * unfold hsistate_refines_stat, hsiexits_refines_stat in *; simpl; intuition.
+        constructor; simpl; eauto.
+        constructor.
+      * destruct REF as (EXREF & LREF & NEST).
+        split.
+        -- do 2 (constructor; simpl; auto).
+           intros; erewrite seval_condition_refines; eauto.
+           destruct c0; simpl; unfold seval_condition.
+
+           { simpl in *.
+           erewrite H4; eauto.
+           erewrite H3; eauto; erewrite H2; eauto.
+           simpl.
+
+           erewrite H1; eauto. try erewrite H0; eauto;
+           try erewrite H; eauto; simplify_SOME z.
+           2: {
+    generalize (sok_local_set_sreg_simp (Rop (OEaddiwr0 imm))); simpl; eauto.
+    intros.j
+           apply hsilocal_refines_smem_refines in LREF; auto.
+
+           rewrite <- LREF. auto.
+           2: { eauto.
+           all: intros; destruct z0, z2; auto.
+        -- split; simpl; auto.
+           destruct NEST as [|st0 se lse TOP NEST];
+           econstructor; simpl; auto; constructor; auto.
+
     + admit.
     + admit.
-Admitted.
+                  *)
 (*Qed.*)
 Global Opaque hsiexec_inst.
 Local Hint Resolve hsiexec_inst_correct: wlp.