From f995bde28d1098b51f42a38f3577b903d0420688 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 13 Jul 2013 14:02:07 +0000 Subject: More accurate model of condition register flags for ARM and IA32. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2297 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Asmgenproof1.v | 434 +++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 304 insertions(+), 130 deletions(-) (limited to 'arm/Asmgenproof1.v') diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 2f5f8680..d77006ad 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -536,39 +536,243 @@ Qed. Lemma compare_int_spec: forall rs v1 v2 m, let rs1 := nextinstr (compare_int rs v1 v2 m) in - rs1#CReq = (Val.cmpu (Mem.valid_pointer m) Ceq v1 v2) - /\ rs1#CRne = (Val.cmpu (Mem.valid_pointer m) Cne v1 v2) - /\ rs1#CRhs = (Val.cmpu (Mem.valid_pointer m) Cge v1 v2) - /\ rs1#CRlo = (Val.cmpu (Mem.valid_pointer m) Clt v1 v2) - /\ rs1#CRhi = (Val.cmpu (Mem.valid_pointer m) Cgt v1 v2) - /\ rs1#CRls = (Val.cmpu (Mem.valid_pointer m) Cle v1 v2) - /\ rs1#CRge = (Val.cmp Cge v1 v2) - /\ rs1#CRlt = (Val.cmp Clt v1 v2) - /\ rs1#CRgt = (Val.cmp Cgt v1 v2) - /\ rs1#CRle = (Val.cmp Cle v1 v2) - /\ forall r', data_preg r' = true -> rs1#r' = rs#r'. + rs1#CN = Val.negative (Val.sub v1 v2) + /\ rs1#CZ = Val.cmpu (Mem.valid_pointer m) Ceq v1 v2 + /\ rs1#CC = Val.cmpu (Mem.valid_pointer m) Cge v1 v2 + /\ rs1#CV = Val.sub_overflow v1 v2. Proof. - intros. unfold rs1. intuition; try reflexivity. - unfold compare_int. Simpl. + intros. unfold rs1. intuition. +Qed. + +Lemma compare_int_inv: + forall rs v1 v2 m, + let rs1 := nextinstr (compare_int rs v1 v2 m) in + forall r', data_preg r' = true -> rs1#r' = rs#r'. +Proof. + intros. unfold rs1, compare_int. + repeat Simplif. +Qed. + +Lemma int_signed_eq: + forall x y, Int.eq x y = zeq (Int.signed x) (Int.signed y). +Proof. + intros. unfold Int.eq. unfold proj_sumbool. + destruct (zeq (Int.unsigned x) (Int.unsigned y)); + destruct (zeq (Int.signed x) (Int.signed y)); auto. + elim n. unfold Int.signed. rewrite e; auto. + elim n. apply Int.eqm_small_eq; auto with ints. + eapply Int.eqm_trans. apply Int.eqm_sym. apply Int.eqm_signed_unsigned. + rewrite e. apply Int.eqm_signed_unsigned. +Qed. + +Lemma int_not_lt: + forall x y, negb (Int.lt y x) = (Int.lt x y || Int.eq x y). +Proof. + intros. unfold Int.lt. rewrite int_signed_eq. unfold proj_sumbool. + destruct (zlt (Int.signed y) (Int.signed x)). + rewrite zlt_false. rewrite zeq_false. auto. omega. omega. + destruct (zeq (Int.signed x) (Int.signed y)). + rewrite zlt_false. auto. omega. + rewrite zlt_true. auto. omega. +Qed. + +Lemma int_lt_not: + forall x y, Int.lt y x = negb (Int.lt x y) && negb (Int.eq x y). +Proof. + intros. rewrite <- negb_orb. rewrite <- int_not_lt. rewrite negb_involutive. auto. +Qed. + +Lemma int_not_ltu: + forall x y, negb (Int.ltu y x) = (Int.ltu x y || Int.eq x y). +Proof. + intros. unfold Int.ltu, Int.eq. + destruct (zlt (Int.unsigned y) (Int.unsigned x)). + rewrite zlt_false. rewrite zeq_false. auto. omega. omega. + destruct (zeq (Int.unsigned x) (Int.unsigned y)). + rewrite zlt_false. auto. omega. + rewrite zlt_true. auto. omega. +Qed. + +Lemma int_ltu_not: + forall x y, Int.ltu y x = negb (Int.ltu x y) && negb (Int.eq x y). +Proof. + intros. rewrite <- negb_orb. rewrite <- int_not_ltu. rewrite negb_involutive. auto. +Qed. + +Lemma cond_for_signed_cmp_correct: + forall c v1 v2 rs m b, + Val.cmp_bool c v1 v2 = Some b -> + eval_testcond (cond_for_signed_cmp c) + (nextinstr (compare_int rs v1 v2 m)) = Some b. +Proof. + intros. generalize (compare_int_spec rs v1 v2 m). + set (rs' := nextinstr (compare_int rs v1 v2 m)). + intros [A [B [C D]]]. + destruct v1; destruct v2; simpl in H; inv H. + unfold eval_testcond. rewrite A; rewrite B; rewrite C; rewrite D. + simpl. unfold Val.cmp, Val.cmpu. + rewrite Int.lt_sub_overflow. + destruct c; simpl. + destruct (Int.eq i i0); auto. + destruct (Int.eq i i0); auto. + destruct (Int.lt i i0); auto. + rewrite int_not_lt. destruct (Int.lt i i0); simpl; destruct (Int.eq i i0); auto. + rewrite (int_lt_not i i0). destruct (Int.lt i i0); destruct (Int.eq i i0); reflexivity. + destruct (Int.lt i i0); reflexivity. +Qed. + +Lemma cond_for_unsigned_cmp_correct: + forall c v1 v2 rs m b, + Val.cmpu_bool (Mem.valid_pointer m) c v1 v2 = Some b -> + eval_testcond (cond_for_unsigned_cmp c) + (nextinstr (compare_int rs v1 v2 m)) = Some b. +Proof. + intros. generalize (compare_int_spec rs v1 v2 m). + set (rs' := nextinstr (compare_int rs v1 v2 m)). + intros [A [B [C D]]]. + unfold eval_testcond. rewrite B; rewrite C. unfold Val.cmpu, Val.cmp. + destruct v1; destruct v2; simpl in H; inv H. +(* int int *) + destruct c; simpl; auto. + destruct (Int.eq i i0); reflexivity. + destruct (Int.eq i i0); auto. + destruct (Int.ltu i i0); auto. + rewrite (int_not_ltu i i0). destruct (Int.ltu i i0); destruct (Int.eq i i0); auto. + rewrite (int_ltu_not i i0). destruct (Int.ltu i i0); destruct (Int.eq i i0); reflexivity. + destruct (Int.ltu i i0); reflexivity. +(* int ptr *) + destruct (Int.eq i Int.zero) eqn:?; try discriminate. + destruct c; simpl in *; inv H1. + rewrite Heqb1; reflexivity. + rewrite Heqb1; reflexivity. +(* ptr int *) + destruct (Int.eq i0 Int.zero) eqn:?; try discriminate. + destruct c; simpl in *; inv H1. + rewrite Heqb1; reflexivity. + rewrite Heqb1; reflexivity. +(* ptr ptr *) + simpl. + fold (Mem.weak_valid_pointer m b0 (Int.unsigned i)) in *. + fold (Mem.weak_valid_pointer m b1 (Int.unsigned i0)) in *. + destruct (eq_block b0 b1). + destruct (Mem.weak_valid_pointer m b0 (Int.unsigned i) && + Mem.weak_valid_pointer m b1 (Int.unsigned i0)); inversion H1. + destruct c; simpl; auto. + destruct (Int.eq i i0); reflexivity. + destruct (Int.eq i i0); auto. + destruct (Int.ltu i i0); auto. + rewrite (int_not_ltu i i0). destruct (Int.ltu i i0); simpl; destruct (Int.eq i i0); auto. + rewrite (int_ltu_not i i0). destruct (Int.ltu i i0); destruct (Int.eq i i0); reflexivity. + destruct (Int.ltu i i0); reflexivity. + destruct (Mem.valid_pointer m b0 (Int.unsigned i) && + Mem.valid_pointer m b1 (Int.unsigned i0)); try discriminate. + destruct c; simpl in *; inv H1; reflexivity. Qed. Lemma compare_float_spec: + forall rs f1 f2, + let rs1 := nextinstr (compare_float rs (Vfloat f1) (Vfloat f2)) in + rs1#CN = Val.of_bool (Float.cmp Clt f1 f2) + /\ rs1#CZ = Val.of_bool (Float.cmp Ceq f1 f2) + /\ rs1#CC = Val.of_bool (negb (Float.cmp Clt f1 f2)) + /\ rs1#CV = Val.of_bool (negb (Float.cmp Ceq f1 f2 || Float.cmp Clt f1 f2 || Float.cmp Cgt f1 f2)). +Proof. + intros. intuition. +Qed. + +Lemma compare_float_inv: forall rs v1 v2, - let rs' := nextinstr (compare_float rs v1 v2) in - rs'#CReq = (Val.cmpf Ceq v1 v2) - /\ rs'#CRne = (Val.cmpf Cne v1 v2) - /\ rs'#CRmi = (Val.cmpf Clt v1 v2) - /\ rs'#CRpl = (Val.notbool (Val.cmpf Clt v1 v2)) - /\ rs'#CRhi = (Val.notbool (Val.cmpf Cle v1 v2)) - /\ rs'#CRls = (Val.cmpf Cle v1 v2) - /\ rs'#CRge = (Val.cmpf Cge v1 v2) - /\ rs'#CRlt = (Val.notbool (Val.cmpf Cge v1 v2)) - /\ rs'#CRgt = (Val.cmpf Cgt v1 v2) - /\ rs'#CRle = (Val.notbool (Val.cmpf Cgt v1 v2)) - /\ forall r', data_preg r' = true -> rs'#r' = rs#r'. + let rs1 := nextinstr (compare_float rs v1 v2) in + forall r', data_preg r' = true -> rs1#r' = rs#r'. Proof. - intros. unfold rs'. intuition; try reflexivity. - unfold compare_float. Simpl. + intros. unfold rs1, compare_float. + assert (nextinstr (rs#CN <- Vundef #CZ <- Vundef #CC <- Vundef #CV <- Vundef) r' = rs r'). + { repeat Simplif. } + destruct v1; destruct v2; auto. + repeat Simplif. +Qed. + +Lemma compare_float_nextpc: + forall rs v1 v2, + nextinstr (compare_float rs v1 v2) PC = Val.add (rs PC) Vone. +Proof. + intros. unfold compare_float. destruct v1; destruct v2; reflexivity. +Qed. + +Lemma cond_for_float_cmp_correct: + forall c n1 n2 rs, + eval_testcond (cond_for_float_cmp c) + (nextinstr (compare_float rs (Vfloat n1) (Vfloat n2))) = + Some(Float.cmp c n1 n2). +Proof. + intros. + generalize (compare_float_spec rs n1 n2). + set (rs' := nextinstr (compare_float rs (Vfloat n1) (Vfloat n2))). + intros [A [B [C D]]]. + unfold eval_testcond. rewrite A; rewrite B; rewrite C; rewrite D. + destruct c; simpl. +(* eq *) + destruct (Float.cmp Ceq n1 n2); auto. +(* ne *) + rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq n1 n2); auto. +(* lt *) + destruct (Float.cmp Clt n1 n2); auto. +(* le *) + rewrite Float.cmp_le_lt_eq. + destruct (Float.cmp Clt n1 n2); destruct (Float.cmp Ceq n1 n2); auto. +(* gt *) + destruct (Float.cmp Ceq n1 n2) eqn:EQ; + destruct (Float.cmp Clt n1 n2) eqn:LT; + destruct (Float.cmp Cgt n1 n2) eqn:GT; auto. + exfalso; eapply Float.cmp_lt_gt_false; eauto. + exfalso; eapply Float.cmp_gt_eq_false; eauto. + exfalso; eapply Float.cmp_lt_gt_false; eauto. +(* ge *) + rewrite Float.cmp_ge_gt_eq. + destruct (Float.cmp Ceq n1 n2) eqn:EQ; + destruct (Float.cmp Clt n1 n2) eqn:LT; + destruct (Float.cmp Cgt n1 n2) eqn:GT; auto. + exfalso; eapply Float.cmp_lt_eq_false; eauto. + exfalso; eapply Float.cmp_lt_eq_false; eauto. + exfalso; eapply Float.cmp_lt_gt_false; eauto. +Qed. + +Lemma cond_for_float_not_cmp_correct: + forall c n1 n2 rs, + eval_testcond (cond_for_float_not_cmp c) + (nextinstr (compare_float rs (Vfloat n1) (Vfloat n2)))= + Some(negb(Float.cmp c n1 n2)). +Proof. + intros. + generalize (compare_float_spec rs n1 n2). + set (rs' := nextinstr (compare_float rs (Vfloat n1) (Vfloat n2))). + intros [A [B [C D]]]. + unfold eval_testcond. rewrite A; rewrite B; rewrite C; rewrite D. + destruct c; simpl. +(* eq *) + destruct (Float.cmp Ceq n1 n2); auto. +(* ne *) + rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq n1 n2); auto. +(* lt *) + destruct (Float.cmp Clt n1 n2); auto. +(* le *) + rewrite Float.cmp_le_lt_eq. + destruct (Float.cmp Clt n1 n2) eqn:LT; destruct (Float.cmp Ceq n1 n2) eqn:EQ; auto. +(* gt *) + destruct (Float.cmp Ceq n1 n2) eqn:EQ; + destruct (Float.cmp Clt n1 n2) eqn:LT; + destruct (Float.cmp Cgt n1 n2) eqn:GT; auto. + exfalso; eapply Float.cmp_lt_gt_false; eauto. + exfalso; eapply Float.cmp_gt_eq_false; eauto. + exfalso; eapply Float.cmp_lt_gt_false; eauto. +(* ge *) + rewrite Float.cmp_ge_gt_eq. + destruct (Float.cmp Ceq n1 n2) eqn:EQ; + destruct (Float.cmp Clt n1 n2) eqn:LT; + destruct (Float.cmp Cgt n1 n2) eqn:GT; auto. + exfalso; eapply Float.cmp_lt_eq_false; eauto. + exfalso; eapply Float.cmp_lt_eq_false; eauto. + exfalso; eapply Float.cmp_lt_gt_false; eauto. Qed. Ltac ArgsInv := @@ -591,119 +795,92 @@ Lemma transl_cond_correct: exists rs', exec_straight ge fn c rs m k rs' m /\ match eval_condition cond (map rs (map preg_of args)) m with - | Some b => rs'#(CR (crbit_for_cond cond)) = Val.of_bool b + | Some b => eval_testcond (cond_for_cond cond) rs' = Some b | None => True end /\ forall r, data_preg r = true -> rs'#r = rs r. Proof. intros until c; intros TR. - assert (MATCH: forall v ob, - v = Val.of_optbool ob -> - match ob with Some b => v = Val.of_bool b | None => True end). - intros. subst v. destruct ob; auto. - assert (MATCH2: forall cmp v1 v2 v, - v = Val.cmpu (Mem.valid_pointer m) cmp v1 v2 -> - cmp = Ceq \/ cmp = Cne -> - match Val.cmp_bool cmp v1 v2 with - | Some b => v = Val.of_bool b - | None => True - end). - intros. destruct v1; simpl; auto; destruct v2; simpl; auto. - unfold Val.cmpu, Val.cmpu_bool in H. subst v. destruct H0; subst cmp; auto. - unfold transl_cond in TR; destruct cond; ArgsInv. - (* Ccomp *) - generalize (compare_int_spec rs (rs x) (rs x0) m). - intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). - auto. + split. destruct (Val.cmp_bool c0 (rs x) (rs x0)) eqn:CMP; auto. apply cond_for_signed_cmp_correct; auto. + apply compare_int_inv. - (* Ccompu *) - generalize (compare_int_spec rs (rs x) (rs x0) m). - intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). - auto. + split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (rs x0)) eqn:CMP; auto. apply cond_for_unsigned_cmp_correct; auto. + apply compare_int_inv. - (* Ccompshift *) - generalize (compare_int_spec rs (rs x) (eval_shift s (rs x0)) m). - intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - rewrite transl_shift_correct. - split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). - auto. + split. rewrite transl_shift_correct. + destruct (Val.cmp_bool c0 (rs x) (eval_shift s (rs x0))) eqn:CMP; auto. apply cond_for_signed_cmp_correct; auto. + apply compare_int_inv. - (* Ccompushift *) - generalize (compare_int_spec rs (rs x) (eval_shift s (rs x0)) m). - intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - rewrite transl_shift_correct. - split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). - auto. + split. rewrite transl_shift_correct. + destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (eval_shift s (rs x0))) eqn:CMP; auto. apply cond_for_unsigned_cmp_correct; auto. + apply compare_int_inv. - (* Ccompimm *) destruct (is_immed_arith i). - generalize (compare_int_spec rs (rs x) (Vint i) m). - intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. - split. apply exec_straight_one. simpl. eauto. auto. - split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). - auto. + split. apply exec_straight_one. simpl. eauto. auto. + split. destruct (Val.cmp_bool c0 (rs x) (Vint i)) eqn:CMP; auto. apply cond_for_signed_cmp_correct; auto. + apply compare_int_inv. exploit (loadimm_correct IR14). intros [rs' [P [Q R]]]. - generalize (compare_int_spec rs' (rs x) (Vint i) m). - intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl. rewrite Q. rewrite R; eauto with asmgen. auto. - split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). - intros. rewrite C; auto with asmgen. + split. rewrite <- R by (eauto with asmgen). + destruct (Val.cmp_bool c0 (rs' x) (Vint i)) eqn:CMP; auto. apply cond_for_signed_cmp_correct; auto. + intros. rewrite compare_int_inv by auto. auto with asmgen. - (* Ccompuimm *) destruct (is_immed_arith i). - generalize (compare_int_spec rs (rs x) (Vint i) m). - intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. - split. apply exec_straight_one. simpl. eauto. auto. - split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). - auto. + split. apply exec_straight_one. simpl. eauto. auto. + split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (Vint i)) eqn:CMP; auto. apply cond_for_unsigned_cmp_correct; auto. + apply compare_int_inv. exploit (loadimm_correct IR14). intros [rs' [P [Q R]]]. - generalize (compare_int_spec rs' (rs x) (Vint i) m). - intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl. rewrite Q. rewrite R; eauto with asmgen. auto. - split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). - intros. rewrite C; auto with asmgen. + split. rewrite <- R by (eauto with asmgen). + destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs' x) (Vint i)) eqn:CMP; auto. apply cond_for_unsigned_cmp_correct; auto. + intros. rewrite compare_int_inv by auto. auto with asmgen. - (* Ccompf *) - generalize (compare_float_spec rs (rs x) (rs x0)). - intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. - split. apply exec_straight_one. simpl. eauto. auto. - split. case c0; apply MATCH; assumption. - auto. + split. apply exec_straight_one. simpl. eauto. apply compare_float_nextpc. + split. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) eqn:CMP; auto. + destruct (rs x); try discriminate. destruct (rs x0); try discriminate. + simpl in CMP. inv CMP. apply cond_for_float_cmp_correct. + apply compare_float_inv. - (* Cnotcompf *) - generalize (compare_float_spec rs (rs x) (rs x0)). - intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. - split. apply exec_straight_one. simpl. eauto. auto. - split. rewrite <- Val.negate_cmpf_ne in C2. rewrite <- Val.negate_cmpf_eq in C1. - destruct c0; apply MATCH; simpl; rewrite Val.notbool_negb_3; auto. - auto. + split. apply exec_straight_one. simpl. eauto. apply compare_float_nextpc. + split. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) eqn:CMP; auto. + destruct (rs x); try discriminate. destruct (rs x0); try discriminate. + simpl in CMP. inv CMP. +Local Opaque compare_float. simpl. apply cond_for_float_not_cmp_correct. + exact I. + apply compare_float_inv. - (* Ccompfzero *) - generalize (compare_float_spec rs (rs x) (Vfloat Float.zero)). - intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. - split. apply exec_straight_one. simpl. eauto. auto. - split. case c0; apply MATCH; assumption. - auto. -- (* Cnotcompf *) - generalize (compare_float_spec rs (rs x) (Vfloat Float.zero)). - intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). + split. apply exec_straight_one. simpl. eauto. apply compare_float_nextpc. + split. destruct (Val.cmpf_bool c0 (rs x) (Vfloat Float.zero)) eqn:CMP; auto. + destruct (rs x); try discriminate. + simpl in CMP. inv CMP. apply cond_for_float_cmp_correct. + apply compare_float_inv. +- (* Cnotcompfzero *) econstructor. - split. apply exec_straight_one. simpl. eauto. auto. - split. rewrite <- Val.negate_cmpf_ne in C2. rewrite <- Val.negate_cmpf_eq in C1. - destruct c0; apply MATCH; simpl; rewrite Val.notbool_negb_3; auto. - auto. + split. apply exec_straight_one. simpl. eauto. apply compare_float_nextpc. + split. destruct (Val.cmpf_bool c0 (rs x) (Vfloat Float.zero)) eqn:CMP; auto. + destruct (rs x); try discriminate. simpl in CMP. inv CMP. +Local Opaque compare_float. simpl. apply cond_for_float_not_cmp_correct. + exact I. + apply compare_float_inv. Qed. (** Translation of arithmetic operations. *) @@ -788,8 +965,7 @@ Proof. set (islt := Int.lt n Int.zero) in *. set (rs1 := nextinstr (compare_int rs (Vint n) (Vint Int.zero) m)). assert (OTH1: forall r', data_preg r' = true -> rs1#r' = rs#r'). - generalize (compare_int_spec rs (Vint n) (Vint Int.zero) m). - fold rs1. intros [A B]. intuition. + { apply compare_int_inv; auto. } exploit (addimm_correct IR14 x0 (Int.sub (Int.shl Int.one i) Int.one)). intros [rs2 [EXEC2 [RES2 OTH2]]]. set (rs3 := nextinstr (if islt then rs2 else rs2#IR14 <- (Vint n))). @@ -799,18 +975,19 @@ Proof. simpl. rewrite ARG1. auto. auto. eapply exec_straight_trans. eexact EXEC2. apply exec_straight_two with rs3 m. - simpl. rewrite OTH2; eauto with asmgen. - change (rs1 CRge) with (Val.cmp Cge (Vint n) (Vint Int.zero)). - unfold Val.cmp, Val.cmp_bool. change (Int.cmp Cge n Int.zero) with (negb islt). - rewrite OTH2; eauto with asmgen. rewrite OTH1. rewrite ARG1. - unfold rs3. case islt; reflexivity. - rewrite <- (ireg_of_eq _ _ EQ1). auto with asmgen. - auto. - unfold rs3. destruct islt; auto. auto. - split. unfold rs4; Simpl. unfold rs3. destruct islt. - Simpl. rewrite RES2. unfold rs1. Simpl. - Simpl. congruence. - intros. unfold rs4, rs3; Simpl. destruct islt; Simpl; rewrite OTH2; auto with asmgen. + unfold exec_instr. + assert (TC: eval_testcond TCge rs2 = Some (negb islt)). + { simpl. rewrite ! OTH2 by auto with asmgen. simpl. + rewrite Int.lt_sub_overflow. fold islt. destruct islt; auto. } + rewrite TC. simpl. rewrite OTH2 by eauto with asmgen. rewrite OTH1. rewrite ARG1. + unfold rs3; destruct islt; reflexivity. + rewrite <- (ireg_of_eq _ _ EQ1). auto with asmgen. + reflexivity. + unfold rs3; destruct islt; reflexivity. + reflexivity. + split. unfold rs4; Simpl. unfold rs3. destruct islt. + Simpl. rewrite RES2. unfold rs1. Simpl. Simpl. congruence. + intros. unfold rs4, rs3; Simpl. destruct islt; Simpl; rewrite OTH2; auto with asmgen. (* intoffloat *) econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto. Transparent destroyed_by_op. @@ -848,25 +1025,22 @@ Proof. rewrite (ireg_of_eq _ _ EQ). exploit transl_cond_correct; eauto. instantiate (1 := rs). instantiate (1 := m). intros [rs1 [A [B C]]]. set (rs2 := nextinstr (rs1#x <- (Vint Int.zero))). - set (rs3 := nextinstr (match rs2#(crbit_for_cond cmp) with - | Vint n => if Int.eq n Int.zero then rs2 else rs2#x <- Vone - | _ => rs2#x <- Vundef - end)). + set (rs3 := nextinstr (match eval_testcond (cond_for_cond cmp) rs2 with + | Some true => rs2 # x <- (Vint Int.one) + | Some false => rs2 + | None => rs2 # x <- Vundef end)). exists rs3; split. eapply exec_straight_trans. eexact A. apply exec_straight_two with rs2 m. auto. - simpl. unfold rs3. destruct (rs2 (crbit_for_cond cmp)); auto. destruct (Int.eq i Int.zero); auto. - auto. unfold rs3. destruct (rs2 (crbit_for_cond cmp)); auto. destruct (Int.eq i Int.zero); auto. - split. unfold rs3. Simpl. - replace (rs2 (crbit_for_cond cmp)) with (rs1 (crbit_for_cond cmp)). - destruct (eval_condition cmp rs##(preg_of##args) m) as [[]|]; simpl in *. - rewrite B. simpl. rewrite Int.eq_false. Simpl. apply Int.one_not_zero. - rewrite B. simpl. rewrite Int.eq_true. unfold rs2. Simpl. - auto. - destruct cmp; reflexivity. + simpl. unfold rs3. destruct (eval_testcond (cond_for_cond cmp) rs2) as [[]|]; auto. + auto. unfold rs3. destruct (eval_testcond (cond_for_cond cmp) rs2) as [[]|]; auto. + split. destruct (eval_condition cmp rs ## (preg_of ## args) m) as [b|]; simpl; auto. + unfold rs3. + change (eval_testcond (cond_for_cond cmp) rs2) with (eval_testcond (cond_for_cond cmp) rs1). rewrite B. + Simpl. destruct b. Simpl. unfold rs2. Simpl. intros. transitivity (rs2 r). - unfold rs3. destruct (rs2 (crbit_for_cond cmp)); Simpl. destruct (Int.eq i Int.zero); auto; Simpl. - unfold rs2. Simpl. + unfold rs3. Simpl. destruct (eval_testcond (cond_for_cond cmp) rs2) as [[]|]; Simpl; auto. + unfold rs2. Simpl. Qed. (** Translation of loads and stores. *) -- cgit