From 3ce99d1f53b24704b45b6984d0fd0bc156016309 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 23 Feb 2021 10:36:14 +0100 Subject: others case for ccompimm --- scheduling/RTLpathSE_impl.v | 104 ++++++++++++++++++++++---------------------- 1 file changed, 51 insertions(+), 53 deletions(-) (limited to 'scheduling') 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 *) -- cgit