Commit 3ce99d1f authored by Léo Gourdin's avatar Léo Gourdin
Browse files

others case for ccompimm

parent e8322076
......@@ -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 *)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment