Some more proofs on branch expansion, using make_immed32_sound

1 files changed, 221 insertions, 59 deletions

diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v
index 32761c6e..a5f6cf46 100644
--- a/scheduling/RTLpathSE_impl.v
+++ b/scheduling/RTLpathSE_impl.v
@@ -7,7 +7,7 @@ Require Import RTL RTLpath.
 Require Import Errors.
 Require Import RTLpathSE_theory RTLpathLivegenproof.
 Require Import Axioms RTLpathSE_simu_specs.
-Require Import Asmgen.
+Require Import Asmgen Asmgenproof1.
 
 Local Open Scope error_monad_scope.
 Local Open Scope option_monad_scope.
@@ -936,20 +936,20 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hs
   end.
 
 Lemma simplify_nothing lr (hst: hsistate_local) op:
-WHEN DO lhsv <~ hlist_args hst lr;; hSop op lhsv ~> hv
-THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) 
-        (m0 : mem) (st : sistate_local),
-      hsilocal_refines ge sp rs0 m0 hst st ->
-      hsok_local ge sp rs0 m0 hst ->
-      (SOME args <-
-       seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0
-       IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
-          IN eval_operation ge sp op args m) <> None ->
-      seval_sval ge sp (hsval_proj hv) rs0 m0 =
-      (SOME args <-
-       seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0
-       IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
-          IN eval_operation ge sp op args m)).
+  WHEN DO lhsv <~ hlist_args hst lr;; hSop op lhsv ~> hv
+  THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) 
+          (m0 : mem) (st : sistate_local),
+        hsilocal_refines ge sp rs0 m0 hst st ->
+        hsok_local ge sp rs0 m0 hst ->
+        (SOME args <-
+         seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0
+         IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
+            IN eval_operation ge sp op args m) <> None ->
+        seval_sval ge sp (hsval_proj hv) rs0 m0 =
+        (SOME args <-
+         seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0
+         IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
+            IN eval_operation ge sp op args m)).
 Proof.
   wlp_simplify.
   generalize (H0 ge sp rs0 m0 (list_sval_inj (map (si_sreg st) lr)) (si_smem st)); clear H0.
@@ -979,6 +979,18 @@ Proof.
   destruct b; simpl; auto.
 Qed.
 
+Lemma xor_ceq_zero: forall v n cmp,
+  cmp = Ceq \/ cmp = Cne ->
+  Some
+    (Val.of_optbool (Val.cmp_bool cmp (Val.xor v (Vint n)) (Vint Int.zero))) =
+  Some (Val.of_optbool (Val.cmp_bool cmp v (Vint n))).
+Proof.
+  intros; destruct v; unfold Val.xor; simpl; auto.
+  destruct cmp, H; try discriminate; simpl;
+  destruct (Int.eq (Int.xor i n) Int.zero) eqn:EQ;
+  rewrite Int.xor_is_zero in EQ; rewrite EQ; trivial.
+Qed.
+
 (* TODO gourdinl Lemma xor_neg_ltge_cmp: forall v1 v2,
   Some (Val.xor (Val.cmp Clt v1 v2) (Vint Int.one)) =
   Some (Val.of_optbool (Val.cmp_bool Cge v1 v2)).
@@ -1221,6 +1233,31 @@ Proof.
   destruct (Float.cmp _ _ _); simpl; auto.
 Qed.
 
+Lemma cmp_ltle_add_one: forall v n,
+  Some (Val.of_optbool (Val.cmp_bool Clt v (Vint (Int.add n Int.one)))) =
+  Some (Val.of_optbool (Val.cmp_bool Cle v (Vint n))).
+Proof.
+  intros. unfold Val.cmp_bool; destruct 6; simpl; auto.
+  unfold Int.lt. replace (Int.signed (Int.add imm Int.one)) with (Int.signed imm + 1).
+  destruct (zlt (Int.signed imm) (Int.signed i)).
+  rewrite zlt_false by omega. auto.
+  rewrite zlt_true by omega. auto.
+  rewrite Int.add_signed. symmetry; apply Int.signed_repr. 
+  specialize (Int.eq_spec imm (Int.repr Int.max_signed)).
+  rewrite EQMAX; simpl; intros.
+  assert (Int.signed imm <> Int.max_signed).
+  { red; intros E. elim H2. rewrite <- (Int.repr_signed imm). rewrite E. auto. }
+  generalize (Int.signed_range imm); omega.
+
+(*Lemma cmp_le_max: forall v*)
+  (*(CONTRA: Some*)
+       (*(Val.of_optbool (Val.cmp_bool Cle v (Vint (Int.repr Int.max_signed)))) =*)
+     (*None -> False),*)
+  (*Some (Vint Int.one) =*)
+  (*Some (Val.of_optbool (Val.cmp_bool Cle v (Vint (Int.repr Int.max_signed)))).*)
+(*Proof.*)
+  (*intros; destruct v. simpl in *; try discriminate CONTRA; auto.*)
+
 Lemma simplify_ccomp_correct: forall c r r0 (hst: hsistate_local),
   WHEN DO hv1 <~ hsi_sreg_get hst r;;
        DO hv2 <~ hsi_sreg_get hst r0;;
@@ -1305,6 +1342,16 @@ Proof.
   destruct (Int.eq _ _); inv H; auto.
 Qed.
 
+Lemma mkimm_pair_equal: forall n hi lo,
+  make_immed32 n = Imm32_pair hi lo ->
+  hi = (Int.shru (Int.sub n (Int.sign_ext 12 n)) (Int.repr 12)) /\
+  lo = (Int.sign_ext 12 n).
+Proof.
+  intros. unfold make_immed32 in H.
+  destruct (Int.eq _ _) in H; try congruence.
+  inv H. auto.
+Qed.
+
 (* TODO gourdinl Lemma mkimm_pair_lo_zero_equal: forall n hi lo,
   make_immed32 n = Imm32_pair hi lo ->
   Int.eq n Int.zero = false ->
@@ -1317,8 +1364,8 @@ Proof.
   rewrite Int.sub_zero_l. unfold Int.shru, Int.shl.
  *)
 
-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
+Lemma simplify_ccompimm_correct: forall c n r (hst: hsistate_local),
+  WHEN DO hv1 <~ hsi_sreg_get hst r;; expanse_condimm_int32s c hv1 n ~> hv
   THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) 
           (m0 : mem) (st : sistate_local),
         hsilocal_refines ge sp rs0 m0 hst st ->
@@ -1326,66 +1373,180 @@ Lemma simplify_ccompuimm_correct: forall c n r (hst: hsistate_local),
         (SOME args <-
          seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r])) rs0 m0
          IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
-            IN eval_operation ge sp (Ocmp (Ccompuimm c n)) args m) <> None ->
+            IN eval_operation ge sp (Ocmp (Ccompimm c n)) args m) <> None ->
         seval_sval ge sp (hsval_proj hv) rs0 m0 =
         (SOME args <-
          seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r])) rs0 m0
          IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
-            IN eval_operation ge sp (Ocmp (Ccompuimm c n)) args m)).
+            IN eval_operation ge sp (Ocmp (Ccompimm c n)) args m)).
 Proof.
-  unfold expanse_condimm_int32u, cond_int32u in *; destruct c;
-  intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl.
-  - wlp_simplify;
-    destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
-    all: try (simplify_SOME z; contradiction; fail).
+  unfold expanse_condimm_int32s, cond_int32s in *; destruct c;
+  intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl;
+  unfold loadimm32, sltimm32, xorimm32, opimm32, load_hilo32.
+  1,3,5,7,9,11: 
+    wlp_simplify;
+    destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence;
+    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.
-    apply Int.same_if_eq in EQIMM; subst. trivial.
-  - unfold loadimm32. destruct (make_immed32 n) eqn:EQMKI;
+  4: rewrite <- xor_neg_ltle_cmp; unfold Val.cmp.
+  5: intros; replace (Clt) with (swap_comparison Cgt) by auto;
+     unfold Val.cmp; rewrite Val.swap_cmp_bool; trivial.
+  6: intros; replace (Clt) with (negate_comparison Cge) by auto;
+     unfold Val.cmp; rewrite Val.negate_cmp_bool; rewrite xor_neg_optb.
+  1,2,3,4,5,6: apply Int.same_if_eq in EQIMM; subst; trivial.
+  all:
+    specialize make_immed32_sound with n;
+    destruct (make_immed32 n) eqn:EQMKI;
+    try destruct (Int.eq n (Int.repr Int.max_signed)) eqn:EQMAX;
+    try destruct (Int.eq lo Int.zero) eqn:EQLO.
+  19,21,22:
+    specialize make_immed32_sound with (Int.one);
+    destruct (make_immed32 Int.one) eqn:EQMKI_A1.
+  25,26,27:
+    specialize make_immed32_sound with (Int.add n Int.one);
+    destruct (make_immed32 (Int.add n Int.one)) eqn:EQMKI_A2.
+  all:
     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;
+  all: try (simplify_SOME z; contradiction; fail).
+  all:
+    try erewrite H12; eauto; try erewrite H11; eauto;
+    try erewrite H10; eauto; 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.
-    + apply mkimm_single_equal in EQMKI; subst.
-      rewrite Int.add_commut, Int.add_zero_l. trivial.
-    + admit.
-    + admit.
-  - (* TODO gourdinl same as first goal *)
+    simplify_SOME z; unfold Val.cmp, zero32; intros; try contradiction.
+  all: try apply Int.same_if_eq in H1; subst.
+  all: try apply Int.same_if_eq in EQLO; subst.
+  all: try apply Int.same_if_eq in EQMAX; subst.
+  all: try rewrite Int.add_commut, Int.add_zero_l; trivial.
+  all: try apply xor_ceq_zero; auto.
+  (* Problème d'implémentation lié au addiwr0 ?
+     --> On dirait que comme l'instruction n'a pas d'argument une fois expansée,
+     un cas spécial se produit si l'argument de départ n'est pas un entier :
+     L'instruction addiwr0 est configurée pour toujours renvoyer Int.one,
+     mais si le premier argument de la comparaison originelle n'est pas un
+     Vint, alors on se retrouve avec :
+      Some (Vint Int.one) = Some (Val.of_optbool None)
+      <-> Some (Vint Int.zero) = Some (Vundef)
+     Il faudrait peut-être modifier la sémantique dans Op pour éliminer ce cas. *)
+  admit.
+  admit.
+  admit.
+  admit.
+  admit.
+  admit.
+  admit.
+  admit.
+  admit.
+  { unfold Val.cmp_bool; destruct z0; simpl; auto.
+    unfold Int.lt. replace (Int.signed (Int.add imm Int.one)) with (Int.signed imm + 1).
+    destruct (zlt (Int.signed imm) (Int.signed i)).
+    rewrite zlt_false by omega. auto.
+    rewrite zlt_true by omega. auto.
+    rewrite Int.add_signed. symmetry; apply Int.signed_repr. 
+    specialize (Int.eq_spec imm (Int.repr Int.max_signed)).
+    rewrite EQMAX; simpl; intros.
+    assert (Int.signed imm <> Int.max_signed).
+    { red; intros E. elim H8. rewrite <- (Int.repr_signed imm). rewrite E. auto. }
+    generalize (Int.signed_range imm); omega. }
+
+  { apply Int.same_if_eq in H2; subst.
+    rewrite (Int.add_commut (Int.shl hi (Int.repr 12)) Int.zero) in H.
+    rewrite Int.add_zero_l in H. rewrite <- H.
+
+    unfold Val.cmp_bool; destruct z6; simpl; auto.
+    unfold Int.lt. replace (Int.signed (Int.add imm Int.one)) with (Int.signed imm + 1).
+    destruct (zlt (Int.signed imm) (Int.signed i)).
+    rewrite zlt_false by omega. auto.
+    rewrite zlt_true by omega. auto.
+    rewrite Int.add_signed. symmetry; apply Int.signed_repr. 
+    specialize (Int.eq_spec imm (Int.repr Int.max_signed)).
+    rewrite EQMAX; simpl; intros.
+    assert (Int.signed imm <> Int.max_signed).
+    { red; intros E. elim H2. rewrite <- (Int.repr_signed imm). rewrite E. auto. }
+    generalize (Int.signed_range imm); omega. }
+
+
+
+    rewrite Int.not_lt. destruct (Int.eq i imm) eqn:EQ.
+    - apply Int.same_if_eq in EQ; subst.
+      rewrite orb_true_r. rewrite Int.lt_not.
+      assert ((Int.eq (Int.add imm Int.one) imm) = false).
+      { apply Int.eq_false. unfold Int.add.
+      erewrite Int.translate_lt; eauto.
+      destruct (Int.lt _ _) eqn:CONTRA; auto.
+      unfold Int.lt in CONTRA.
+      assert ((Int.signed imm) < (Int.signed (Int.add imm Int.one))).
+      { 
+  
+apply xor_ceq_zero.
+  
+  all: try rewrite <- xor_neg_ltle_cmp; unfold Val.cmp; trivial.
+  all: intros; replace (Clt) with (negate_comparison Cge) by auto;
+     rewrite Val.negate_cmpu_bool; rewrite xor_neg_optb; trivial.
+Qed.
+
+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),
+        hsilocal_refines ge sp rs0 m0 hst st ->
+        hsok_local ge sp rs0 m0 hst ->
+        (SOME args <-
+         seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r])) rs0 m0
+         IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
+            IN eval_operation ge sp (Ocmp (Ccompuimm c n)) args m) <> None ->
+        seval_sval ge sp (hsval_proj hv) rs0 m0 =
+        (SOME args <-
+         seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r])) rs0 m0
+         IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0
+            IN eval_operation ge sp (Ocmp (Ccompuimm c n)) args m)).
+Proof.
+  unfold expanse_condimm_int32u, cond_int32u in *; destruct c;
+  intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl;
+  unfold loadimm32, sltuimm32, opimm32, load_hilo32.
+  1,3,5,7,9,11: 
     wlp_simplify;
-    destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
-    all: try (simplify_SOME z; contradiction; fail).
+    destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence;
+    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.
-    apply Int.same_if_eq in EQIMM; subst. trivial.
-  - admit.
-  - (* TODO gourdinl same as first goal *)
+  4: rewrite <- xor_neg_ltle_cmpu; unfold Val.cmpu.
+  5: intros; replace (Clt) with (swap_comparison Cgt) by auto;
+     rewrite Val.swap_cmpu_bool; trivial.
+  6: intros; replace (Clt) with (negate_comparison Cge) by auto;
+     rewrite Val.negate_cmpu_bool; rewrite xor_neg_optb.
+  1,2,3,4,5,6: apply Int.same_if_eq in EQIMM; subst; trivial.
+  all:
+    specialize make_immed32_sound with n;
+    destruct (make_immed32 n) eqn:EQMKI;
+    try destruct (Int.eq lo Int.zero) eqn:EQLO.
+  all:
     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;
+  all: try (simplify_SOME z; contradiction; fail).
+  all:
+    try erewrite H11; eauto;
+    try erewrite H10; eauto; 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.
-    apply Int.same_if_eq in EQIMM; subst. trivial.
-  - (* same *) admit.
-  - (* same *) admit.
-  - (* same *) admit.
-  - (* same *) admit.
-  - (* same *) admit.
-  - (* same *) admit.
-  - (* same *) admit.
-Admitted.
+  all: try apply Int.same_if_eq in H1; subst.
+  all: try apply Int.same_if_eq in EQLO; subst.
+  all: try rewrite Int.add_commut, Int.add_zero_l; trivial.
+  all: try rewrite <- xor_neg_ltle_cmpu; unfold Val.cmpu; trivial.
+  all: intros; replace (Clt) with (negate_comparison Cge) by auto;
+     rewrite Val.negate_cmpu_bool; rewrite xor_neg_optb; trivial.
+Qed.
 
 Lemma simplify_ccompl_correct: forall c r r0 (hst: hsistate_local),
   WHEN DO hv1 <~ hsi_sreg_get hst r;;
@@ -2046,7 +2207,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. Admitted. (*
+Proof.
   destruct i; simpl;
   try (wlp_simplify; try_simplify_someHyps; eexists; intuition eauto; fail).
   - (* refines_dyn Iop *)
@@ -2086,7 +2247,7 @@ Proof. Admitted. (*
       destruct (Int.eq _ _) eqn:EQIMM; simpl.
       1: admit.
       
-      unfold loadimm32; destruct make_immed32.
+      unfold loadimm32; destruct make_immed32 eqn:EQMKI.
       {
       wlp_simplify; try_simplify_someHyps; eexists; intuition eauto.
       * unfold hsistate_refines_stat, hsiexits_refines_stat in *; simpl; intuition.
@@ -2098,13 +2259,14 @@ Proof. Admitted. (*
            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.
+           { simpl in *. apply mkimm_single_equal in EQMKI; subst.
+             destruct (seval_smem _ _ _ _ _) eqn:EQSM; try congruence.
+             - erewrite H4; eauto; erewrite H3; eauto;
+               erewrite H2; eauto; erewrite H1; eauto;
+               try erewrite H0; eauto; try erewrite H; eauto;
+               simplify_SOME z. rewrite Int.add_zero. trivial.
+             - simplify_SOME x.
+           }
            2: {
     generalize (sok_local_set_sreg_simp (Rop (OEaddiwr0 imm))); simpl; eauto.
     intros.j