others case for ccompimm

1 files changed, 51 insertions, 53 deletions

diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v
index a5f6cf46..bce428e3 100644
--- a/scheduling/RTLpathSE_impl.v
+++ b/scheduling/RTLpathSE_impl.v
@@ -1234,22 +1234,24 @@ Proof.
 Qed.
 
 Lemma cmp_ltle_add_one: forall v n,
+  Int.eq n (Int.repr Int.max_signed) = false ->
   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)).
+  intros v n EQMAX. unfold Val.cmp_bool; destruct v; simpl; auto.
+  unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1).
+  destruct (zlt (Int.signed n) (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)).
+  specialize (Int.eq_spec n (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.
+  assert (Int.signed n <> Int.max_signed).
+  { red; intros E. elim H. rewrite <- (Int.repr_signed n). rewrite E. auto. }
+  generalize (Int.signed_range n); omega.
+Qed.
 
-(*Lemma cmp_le_max: forall v*)
+(* TODO gourdinl Lemma cmp_le_max: forall v*)
   (*(CONTRA: Some*)
        (*(Val.of_optbool (Val.cmp_bool Cle v (Vint (Int.repr Int.max_signed)))) =*)
      (*None -> False),*)
@@ -1443,53 +1445,49 @@ Proof.
   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 cmp_ltle_add_one; auto. }
   { 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.
+    apply cmp_ltle_add_one; auto. }
+  { rewrite <- H. apply cmp_ltle_add_one; auto. }
+  { rewrite (Int.add_commut (Int.shl hi (Int.repr 12))). rewrite Int.add_zero_l.
+    apply cmp_ltle_add_one. rewrite Int.add_commut, Int.add_zero_l in EQMAX.
+    auto. }
+  { apply Int.same_if_eq in H2; subst.
+    rewrite (Int.add_commut (Int.shl hi0 (Int.repr 12)) Int.zero) in H.
+    rewrite Int.add_zero_l in H. rewrite <- H.
+    rewrite (Int.add_commut (Int.shl hi (Int.repr 12)) Int.zero) in *.
+    rewrite Int.add_zero_l in *. apply cmp_ltle_add_one; auto. }
+  { rewrite <- H.
+    rewrite (Int.add_commut (Int.shl hi (Int.repr 12)) Int.zero) in *.
+    rewrite Int.add_zero_l in *. apply cmp_ltle_add_one; auto. }
+  { apply cmp_ltle_add_one; auto. }
+  { apply Int.same_if_eq in H2; subst.
+    rewrite (Int.add_commut (Int.shl hi0 (Int.repr 12)) Int.zero) in H.
+    rewrite Int.add_zero_l in H. rewrite <- H.
+     apply cmp_ltle_add_one; auto. }
+  { rewrite <- H. apply cmp_ltle_add_one; auto. }
+  { intros; replace (Clt) with (negate_comparison Cge) by auto;
+    rewrite Val.negate_cmp_bool.
+    rewrite xor_neg_optb; trivial. }
+  { intros; replace (Clt) with (negate_comparison Cge) by auto;
+    rewrite Val.negate_cmp_bool.
+    rewrite xor_neg_optb; trivial. }
+  { intros; replace (Clt) with (negate_comparison Cge) by auto;
+    rewrite Val.negate_cmp_bool.
+    rewrite xor_neg_optb; trivial. }
+  { intros; replace (Clt) with (negate_comparison Cge) by auto;
+    rewrite Val.negate_cmp_bool.
+    rewrite xor_neg_optb; trivial. }
+  { intros; replace (Clt) with (negate_comparison Cge) by auto;
+    rewrite Val.negate_cmp_bool.
+    rewrite xor_neg_optb; trivial. }
+  { intros; replace (Clt) with (negate_comparison Cge) by auto;
+    rewrite Val.negate_cmp_bool.
+    rewrite xor_neg_optb; trivial. }
+Admitted.
+(*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
@@ -2207,7 +2205,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 *)