diff options
Diffstat (limited to 'ia32/Asmgenproof1.v')
| -rw-r--r-- | ia32/Asmgenproof1.v | 280 |
1 files changed, 140 insertions, 140 deletions
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 0ca343fb..d2a8206e 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -36,19 +36,19 @@ Lemma agree_nextinstr_nf: forall ms sp rs, agree ms sp rs -> agree ms sp (nextinstr_nf rs). Proof. - intros. unfold nextinstr_nf. apply agree_nextinstr. + intros. unfold nextinstr_nf. apply agree_nextinstr. apply agree_undef_nondata_regs. auto. - intro. simpl. ElimOrEq; auto. + intro. simpl. ElimOrEq; auto. Qed. (** Useful properties of the PC register. *) Lemma nextinstr_nf_inv: - forall r rs, + forall r rs, match r with PC => False | CR _ => False | _ => True end -> (nextinstr_nf rs)#r = rs#r. Proof. - intros. unfold nextinstr_nf. rewrite nextinstr_inv. + intros. unfold nextinstr_nf. rewrite nextinstr_inv. simpl. repeat rewrite Pregmap.gso; auto; red; intro; subst; contradiction. red; intro; subst; contradiction. @@ -109,13 +109,13 @@ Lemma mk_mov_correct: /\ rs2#rd = rs1#rs /\ forall r, data_preg r = true -> r <> rd -> rs2#r = rs1#r. Proof. - unfold mk_mov; intros. + unfold mk_mov; intros. destruct rd; try (monadInv H); destruct rs; monadInv H. (* mov *) - econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. Simplifs. intros; Simplifs. + econstructor. split. apply exec_straight_one. simpl. eauto. auto. + split. Simplifs. intros; Simplifs. (* movd *) - econstructor. split. apply exec_straight_one. simpl. eauto. auto. + econstructor. split. apply exec_straight_one. simpl. eauto. auto. split. Simplifs. intros; Simplifs. Qed. @@ -130,7 +130,7 @@ Remark divs_mods_exist: end. Proof. intros. unfold Val.divs, Val.mods. destruct v1; auto. destruct v2; auto. - destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); auto. + destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); auto. Qed. Remark divu_modu_exist: @@ -142,7 +142,7 @@ Remark divu_modu_exist: end. Proof. intros. unfold Val.divu, Val.modu. destruct v1; auto. destruct v2; auto. - destruct (Int.eq i0 Int.zero); auto. + destruct (Int.eq i0 Int.zero); auto. Qed. (** Smart constructor for [shrx] *) @@ -167,10 +167,10 @@ Proof. set (rs5 := nextinstr_nf (rs4#EAX <- (Val.shr rs4#EAX (Vint n)))). assert (rs3#EAX = Vint x). unfold rs3. Simplifs. assert (rs3#ECX = Vint x'). unfold rs3. Simplifs. - exists rs5. split. + exists rs5. split. apply exec_straight_step with rs2 m. simpl. rewrite A. simpl. rewrite Int.and_idem. auto. auto. - apply exec_straight_step with rs3 m. simpl. - change (rs2 EAX) with (rs1 EAX). rewrite A. simpl. + apply exec_straight_step with rs3 m. simpl. + change (rs2 EAX) with (rs1 EAX). rewrite A. simpl. rewrite (Int.add_commut Int.zero tnm1). rewrite Int.add_zero. auto. auto. apply exec_straight_step with rs4 m. simpl. rewrite Int.lt_sub_overflow. unfold rs4. destruct (Int.lt x Int.zero); simpl; auto. @@ -178,10 +178,10 @@ Proof. apply exec_straight_one. auto. auto. split. unfold rs5. Simplifs. unfold rs4. rewrite nextinstr_inv; auto with asmgen. destruct (Int.lt x Int.zero). rewrite Pregmap.gss. rewrite A; auto. rewrite A; rewrite H; auto. - intros. unfold rs5. Simplifs. unfold rs4. Simplifs. - transitivity (rs3#r). destruct (Int.lt x Int.zero). Simplifs. auto. - unfold rs3. Simplifs. unfold rs2. Simplifs. - unfold compare_ints. Simplifs. + intros. unfold rs5. Simplifs. unfold rs4. Simplifs. + transitivity (rs3#r). destruct (Int.lt x Int.zero). Simplifs. auto. + unfold rs3. Simplifs. unfold rs2. Simplifs. + unfold compare_ints. Simplifs. Qed. (** Smart constructor for integer conversions *) @@ -197,11 +197,11 @@ Lemma mk_intconv_correct: /\ forall r, data_preg r = true -> r <> rd -> r <> EAX -> rs2#r = rs1#r. Proof. unfold mk_intconv; intros. destruct (low_ireg rs); monadInv H. - econstructor. split. apply exec_straight_one. rewrite H0. eauto. auto. + econstructor. split. apply exec_straight_one. rewrite H0. eauto. auto. + split. Simplifs. intros. Simplifs. + econstructor. split. eapply exec_straight_two. + simpl. eauto. apply H0. auto. auto. split. Simplifs. intros. Simplifs. - econstructor. split. eapply exec_straight_two. - simpl. eauto. apply H0. auto. auto. - split. Simplifs. intros. Simplifs. Qed. (** Smart constructor for small stores *) @@ -228,40 +228,40 @@ Lemma mk_smallstore_correct: exec_straight ge fn c rs1 m1 k rs2 m2 /\ forall r, data_preg r = true -> r <> EAX /\ r <> ECX -> rs2#r = rs1#r. Proof. - unfold mk_smallstore; intros. + unfold mk_smallstore; intros. remember (low_ireg r) as low. destruct low. (* low reg *) - monadInv H. econstructor; split. apply exec_straight_one. rewrite H1. + monadInv H. econstructor; split. apply exec_straight_one. rewrite H1. unfold exec_store. rewrite H0. eauto. auto. intros; Simplifs. (* high reg *) remember (addressing_mentions addr EAX) as mentions. destruct mentions; monadInv H. (* EAX is mentioned. *) - assert (r <> ECX). red; intros; subst r; discriminate. + assert (r <> ECX). red; intros; subst r; discriminate. set (rs2 := nextinstr (rs1#ECX <- (eval_addrmode ge addr rs1))). set (rs3 := nextinstr (rs2#EAX <- (rs1 r))). econstructor; split. - apply exec_straight_three with rs2 m1 rs3 m1. - simpl. auto. - simpl. replace (rs2 r) with (rs1 r). auto. symmetry. unfold rs2; Simplifs. - rewrite H1. unfold exec_store. simpl. rewrite Int.add_zero. + apply exec_straight_three with rs2 m1 rs3 m1. + simpl. auto. + simpl. replace (rs2 r) with (rs1 r). auto. symmetry. unfold rs2; Simplifs. + rewrite H1. unfold exec_store. simpl. rewrite Int.add_zero. change (rs3 EAX) with (rs1 r). change (rs3 ECX) with (eval_addrmode ge addr rs1). replace (Val.add (eval_addrmode ge addr rs1) (Vint Int.zero)) with (eval_addrmode ge addr rs1). rewrite H0. eauto. destruct (eval_addrmode ge addr rs1); simpl in H0; try discriminate. - simpl. rewrite Int.add_zero; auto. - auto. auto. auto. - intros. destruct H3. Simplifs. unfold rs3; Simplifs. unfold rs2; Simplifs. + simpl. rewrite Int.add_zero; auto. + auto. auto. auto. + intros. destruct H3. Simplifs. unfold rs3; Simplifs. unfold rs2; Simplifs. (* EAX is not mentioned *) set (rs2 := nextinstr (rs1#EAX <- (rs1 r))). econstructor; split. apply exec_straight_two with rs2 m1. simpl. auto. - rewrite H1. unfold exec_store. + rewrite H1. unfold exec_store. rewrite (addressing_mentions_correct addr EAX rs2 rs1); auto. - change (rs2 EAX) with (rs1 r). rewrite H0. eauto. + change (rs2 EAX) with (rs1 r). rewrite H0. eauto. intros. unfold rs2; Simplifs. auto. auto. intros. destruct H2. simpl. Simplifs. unfold rs2; Simplifs. @@ -281,7 +281,7 @@ Proof. unfold loadind; intros. set (addr := Addrmode (Some base) None (inl (ident * int) ofs)) in *. assert (eval_addrmode ge addr rs = Val.add rs#base (Vint ofs)). - unfold addr. simpl. rewrite Int.add_commut; rewrite Int.add_zero; auto. + unfold addr. simpl. rewrite Int.add_commut; rewrite Int.add_zero; auto. exists (nextinstr_nf (rs#(preg_of dst) <- v)); split. - destruct ty; try discriminate; destruct (preg_of dst); inv H; simpl in H0; apply exec_straight_one; auto; simpl; unfold exec_load; rewrite H1, H0; auto. @@ -300,7 +300,7 @@ Local Transparent destroyed_by_setstack. unfold storeind; intros. set (addr := Addrmode (Some base) None (inl (ident * int) ofs)) in *. assert (eval_addrmode ge addr rs = Val.add rs#base (Vint ofs)). - unfold addr. simpl. rewrite Int.add_commut; rewrite Int.add_zero; auto. + unfold addr. simpl. rewrite Int.add_commut; rewrite Int.add_zero; auto. destruct ty; try discriminate; destruct (preg_of src); inv H; simpl in H0; (econstructor; split; [apply exec_straight_one; [simpl; unfold exec_store; rewrite H1, H0; eauto|auto] @@ -315,10 +315,10 @@ Lemma transl_addressing_mode_correct: eval_addressing ge (rs ESP) addr (List.map rs (List.map preg_of args)) = Some v -> Val.lessdef v (eval_addrmode ge am rs). Proof. - assert (A: forall n, Int.add Int.zero n = n). + assert (A: forall n, Int.add Int.zero n = n). intros. rewrite Int.add_commut. apply Int.add_zero. assert (B: forall n i, (if Int.eq i Int.one then Vint n else Vint (Int.mul n i)) = Vint (Int.mul n i)). - intros. predSpec Int.eq Int.eq_spec i Int.one. + intros. predSpec Int.eq Int.eq_spec i Int.one. subst i. rewrite Int.mul_one. auto. auto. assert (C: forall v i, Val.lessdef (Val.mul v (Vint i)) @@ -332,22 +332,22 @@ Proof. monadInv H. rewrite (ireg_of_eq _ _ EQ). simpl. rewrite A; auto. (* indexed2 *) monadInv H. rewrite (ireg_of_eq _ _ EQ); rewrite (ireg_of_eq _ _ EQ1). simpl. - rewrite Val.add_assoc; auto. + rewrite Val.add_assoc; auto. (* scaled *) - monadInv H. rewrite (ireg_of_eq _ _ EQ). unfold eval_addrmode. - rewrite Val.add_permut. simpl. rewrite A. apply Val.add_lessdef; auto. + monadInv H. rewrite (ireg_of_eq _ _ EQ). unfold eval_addrmode. + rewrite Val.add_permut. simpl. rewrite A. apply Val.add_lessdef; auto. (* indexed2scaled *) monadInv H. rewrite (ireg_of_eq _ _ EQ); rewrite (ireg_of_eq _ _ EQ1); simpl. - apply Val.add_lessdef; auto. apply Val.add_lessdef; auto. + apply Val.add_lessdef; auto. apply Val.add_lessdef; auto. (* global *) inv H. simpl. unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); simpl; auto. repeat rewrite Int.add_zero. auto. (* based *) monadInv H. rewrite (ireg_of_eq _ _ EQ). simpl. unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); simpl; auto. - rewrite Int.add_zero. rewrite Val.add_commut. auto. + rewrite Int.add_zero. rewrite Val.add_commut. auto. (* basedscaled *) - monadInv H. rewrite (ireg_of_eq _ _ EQ). unfold eval_addrmode. + monadInv H. rewrite (ireg_of_eq _ _ EQ). unfold eval_addrmode. rewrite (Val.add_commut Vzero). rewrite Val.add_assoc. rewrite Val.add_permut. apply Val.add_lessdef; auto. destruct (rs x); simpl; auto. rewrite B. simpl. rewrite Int.add_zero. auto. @@ -367,7 +367,7 @@ Lemma compare_ints_spec: /\ (forall r, data_preg r = true -> rs'#r = rs#r). Proof. intros. unfold rs'; unfold compare_ints. - split. auto. + split. auto. split. auto. split. auto. split. auto. @@ -377,13 +377,13 @@ 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. + 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. + 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. + rewrite e. apply Int.eqm_signed_unsigned. Qed. Lemma int_not_lt: @@ -392,8 +392,8 @@ 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. + destruct (zeq (Int.signed x) (Int.signed y)). + rewrite zlt_false. auto. omega. rewrite zlt_true. auto. omega. Qed. @@ -409,8 +409,8 @@ 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. + destruct (zeq (Int.unsigned x) (Int.unsigned y)). + rewrite zlt_false. auto. omega. rewrite zlt_true. auto. omega. Qed. @@ -465,16 +465,16 @@ Proof. destruct (Int.eq i Int.zero && (Mem.valid_pointer m b0 (Int.unsigned i0) || Mem.valid_pointer m b0 (Int.unsigned i0 - 1))) eqn:?; try discriminate. destruct c; simpl in *; inv H1. - rewrite Heqb1; reflexivity. + rewrite Heqb1; reflexivity. rewrite Heqb1; reflexivity. (* ptr int *) destruct (Int.eq i0 Int.zero && (Mem.valid_pointer m b0 (Int.unsigned i) || Mem.valid_pointer m b0 (Int.unsigned i - 1))) eqn:?; try discriminate. destruct c; simpl in *; inv H1. - rewrite Heqb1; reflexivity. + rewrite Heqb1; reflexivity. rewrite Heqb1; reflexivity. (* ptr ptr *) - simpl. + 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). @@ -501,7 +501,7 @@ Lemma compare_floats_spec: /\ (forall r, data_preg r = true -> rs'#r = rs#r). Proof. intros. unfold rs'; unfold compare_floats. - split. auto. + split. auto. split. auto. split. auto. intros. Simplifs. @@ -516,7 +516,7 @@ Lemma compare_floats32_spec: /\ (forall r, data_preg r = true -> rs'#r = rs#r). Proof. intros. unfold rs'; unfold compare_floats32. - split. auto. + split. auto. split. auto. split. auto. intros. Simplifs. @@ -574,19 +574,19 @@ Proof. simpl. rewrite Float.cmp_ne_eq. rewrite Float.cmp_le_lt_eq. caseEq (Float.cmp Clt n1 n2); intros; simpl. - caseEq (Float.cmp Ceq n1 n2); intros; simpl. - elimtype False. eapply Float.cmp_lt_eq_false; eauto. - auto. + caseEq (Float.cmp Ceq n1 n2); intros; simpl. + elimtype False. eapply Float.cmp_lt_eq_false; eauto. + auto. destruct (Float.cmp Ceq n1 n2); auto. (* le *) rewrite <- (Float.cmp_swap Cge n1 n2). simpl. destruct (Float.cmp Cle n1 n2); auto. (* gt *) - rewrite Float.cmp_ne_eq. rewrite Float.cmp_ge_gt_eq. + rewrite Float.cmp_ne_eq. rewrite Float.cmp_ge_gt_eq. caseEq (Float.cmp Cgt n1 n2); intros; simpl. - caseEq (Float.cmp Ceq n1 n2); intros; simpl. - elimtype False. eapply Float.cmp_gt_eq_false; eauto. - auto. + caseEq (Float.cmp Ceq n1 n2); intros; simpl. + elimtype False. eapply Float.cmp_gt_eq_false; eauto. + auto. destruct (Float.cmp Ceq n1 n2); auto. (* ge *) destruct (Float.cmp Cge n1 n2); auto. @@ -622,19 +622,19 @@ Proof. simpl. rewrite Float.cmp_ne_eq. rewrite Float.cmp_le_lt_eq. caseEq (Float.cmp Clt n1 n2); intros; simpl. - caseEq (Float.cmp Ceq n1 n2); intros; simpl. + caseEq (Float.cmp Ceq n1 n2); intros; simpl. elimtype False. eapply Float.cmp_lt_eq_false; eauto. - auto. + auto. destruct (Float.cmp Ceq n1 n2); auto. (* le *) rewrite <- (Float.cmp_swap Cge n1 n2). simpl. destruct (Float.cmp Cle n1 n2); auto. (* gt *) - rewrite Float.cmp_ne_eq. rewrite Float.cmp_ge_gt_eq. + rewrite Float.cmp_ne_eq. rewrite Float.cmp_ge_gt_eq. caseEq (Float.cmp Cgt n1 n2); intros; simpl. - caseEq (Float.cmp Ceq n1 n2); intros; simpl. - elimtype False. eapply Float.cmp_gt_eq_false; eauto. - auto. + caseEq (Float.cmp Ceq n1 n2); intros; simpl. + elimtype False. eapply Float.cmp_gt_eq_false; eauto. + auto. destruct (Float.cmp Ceq n1 n2); auto. (* ge *) destruct (Float.cmp Cge n1 n2); auto. @@ -670,19 +670,19 @@ Proof. simpl. rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_le_lt_eq. caseEq (Float32.cmp Clt n1 n2); intros; simpl. - caseEq (Float32.cmp Ceq n1 n2); intros; simpl. - elimtype False. eapply Float32.cmp_lt_eq_false; eauto. - auto. + caseEq (Float32.cmp Ceq n1 n2); intros; simpl. + elimtype False. eapply Float32.cmp_lt_eq_false; eauto. + auto. destruct (Float32.cmp Ceq n1 n2); auto. (* le *) rewrite <- (Float32.cmp_swap Cge n1 n2). simpl. destruct (Float32.cmp Cle n1 n2); auto. (* gt *) - rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_ge_gt_eq. + rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_ge_gt_eq. caseEq (Float32.cmp Cgt n1 n2); intros; simpl. - caseEq (Float32.cmp Ceq n1 n2); intros; simpl. - elimtype False. eapply Float32.cmp_gt_eq_false; eauto. - auto. + caseEq (Float32.cmp Ceq n1 n2); intros; simpl. + elimtype False. eapply Float32.cmp_gt_eq_false; eauto. + auto. destruct (Float32.cmp Ceq n1 n2); auto. (* ge *) destruct (Float32.cmp Cge n1 n2); auto. @@ -718,19 +718,19 @@ Proof. simpl. rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_le_lt_eq. caseEq (Float32.cmp Clt n1 n2); intros; simpl. - caseEq (Float32.cmp Ceq n1 n2); intros; simpl. + caseEq (Float32.cmp Ceq n1 n2); intros; simpl. elimtype False. eapply Float32.cmp_lt_eq_false; eauto. - auto. + auto. destruct (Float32.cmp Ceq n1 n2); auto. (* le *) rewrite <- (Float32.cmp_swap Cge n1 n2). simpl. destruct (Float32.cmp Cle n1 n2); auto. (* gt *) - rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_ge_gt_eq. + rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_ge_gt_eq. caseEq (Float32.cmp Cgt n1 n2); intros; simpl. - caseEq (Float32.cmp Ceq n1 n2); intros; simpl. - elimtype False. eapply Float32.cmp_gt_eq_false; eauto. - auto. + caseEq (Float32.cmp Ceq n1 n2); intros; simpl. + elimtype False. eapply Float32.cmp_gt_eq_false; eauto. + auto. destruct (Float32.cmp Ceq n1 n2); auto. (* ge *) destruct (Float32.cmp Cge n1 n2); auto. @@ -739,7 +739,7 @@ Qed. Remark swap_floats_commut: forall (A B: Type) c (f: A -> B) x y, swap_floats c (f x) (f y) = f (swap_floats c x y). Proof. - intros. destruct c; auto. + intros. destruct c; auto. Qed. Remark compare_floats_inv: @@ -747,10 +747,10 @@ Remark compare_floats_inv: r <> CR ZF -> r <> CR CF -> r <> CR PF -> r <> CR SF -> r <> CR OF -> compare_floats vx vy rs r = rs r. Proof. - intros. + intros. assert (DFL: undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil) rs r = rs r). - simpl. Simplifs. - unfold compare_floats; destruct vx; destruct vy; auto. Simplifs. + simpl. Simplifs. + unfold compare_floats; destruct vx; destruct vy; auto. Simplifs. Qed. Remark compare_floats32_inv: @@ -758,10 +758,10 @@ Remark compare_floats32_inv: r <> CR ZF -> r <> CR CF -> r <> CR PF -> r <> CR SF -> r <> CR OF -> compare_floats32 vx vy rs r = rs r. Proof. - intros. + intros. assert (DFL: undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil) rs r = rs r). - simpl. Simplifs. - unfold compare_floats32; destruct vx; destruct vy; auto. Simplifs. + simpl. Simplifs. + unfold compare_floats32; destruct vx; destruct vy; auto. Simplifs. Qed. Lemma transl_cond_correct: @@ -775,83 +775,83 @@ Lemma transl_cond_correct: end /\ forall r, data_preg r = true -> rs'#r = rs r. Proof. - unfold transl_cond; intros. + unfold transl_cond; intros. destruct cond; repeat (destruct args; try discriminate); monadInv H. (* comp *) simpl. rewrite (ireg_of_eq _ _ EQ). rewrite (ireg_of_eq _ _ EQ1). econstructor. split. apply exec_straight_one. simpl. eauto. auto. split. destruct (Val.cmp_bool c0 (rs x) (rs x0)) eqn:?; auto. - eapply testcond_for_signed_comparison_correct; eauto. + eapply testcond_for_signed_comparison_correct; eauto. intros. unfold compare_ints. Simplifs. (* compu *) simpl. rewrite (ireg_of_eq _ _ EQ). rewrite (ireg_of_eq _ _ EQ1). econstructor. split. apply exec_straight_one. simpl. eauto. auto. split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (rs x0)) eqn:?; auto. - eapply testcond_for_unsigned_comparison_correct; eauto. + eapply testcond_for_unsigned_comparison_correct; eauto. intros. unfold compare_ints. Simplifs. (* compimm *) simpl. rewrite (ireg_of_eq _ _ EQ). destruct (Int.eq_dec i Int.zero). - econstructor; split. apply exec_straight_one. simpl; eauto. auto. + econstructor; split. apply exec_straight_one. simpl; eauto. auto. split. destruct (rs x); simpl; auto. subst. rewrite Int.and_idem. - eapply testcond_for_signed_comparison_correct; eauto. + eapply testcond_for_signed_comparison_correct; eauto. intros. unfold compare_ints. Simplifs. - econstructor; split. apply exec_straight_one. simpl; eauto. auto. + econstructor; split. apply exec_straight_one. simpl; eauto. auto. split. destruct (Val.cmp_bool c0 (rs x) (Vint i)) eqn:?; auto. - eapply testcond_for_signed_comparison_correct; eauto. + eapply testcond_for_signed_comparison_correct; eauto. intros. unfold compare_ints. Simplifs. (* compuimm *) simpl. rewrite (ireg_of_eq _ _ EQ). econstructor. split. apply exec_straight_one. simpl. eauto. auto. split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (Vint i)) eqn:?; auto. - eapply testcond_for_unsigned_comparison_correct; eauto. + eapply testcond_for_unsigned_comparison_correct; eauto. intros. unfold compare_ints. Simplifs. (* compf *) simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1). exists (nextinstr (compare_floats (swap_floats c0 (rs x) (rs x0)) (swap_floats c0 (rs x0) (rs x)) rs)). - split. apply exec_straight_one. + split. apply exec_straight_one. destruct c0; simpl; auto. - unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats_inv; auto with asmgen. + unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats_inv; auto with asmgen. split. destruct (rs x); destruct (rs x0); simpl; auto. repeat rewrite swap_floats_commut. apply testcond_for_float_comparison_correct. - intros. Simplifs. apply compare_floats_inv; auto with asmgen. + intros. Simplifs. apply compare_floats_inv; auto with asmgen. (* notcompf *) simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1). exists (nextinstr (compare_floats (swap_floats c0 (rs x) (rs x0)) (swap_floats c0 (rs x0) (rs x)) rs)). - split. apply exec_straight_one. + split. apply exec_straight_one. destruct c0; simpl; auto. - unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats_inv; auto with asmgen. + unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats_inv; auto with asmgen. split. destruct (rs x); destruct (rs x0); simpl; auto. repeat rewrite swap_floats_commut. apply testcond_for_neg_float_comparison_correct. - intros. Simplifs. apply compare_floats_inv; auto with asmgen. + intros. Simplifs. apply compare_floats_inv; auto with asmgen. (* compfs *) simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1). exists (nextinstr (compare_floats32 (swap_floats c0 (rs x) (rs x0)) (swap_floats c0 (rs x0) (rs x)) rs)). - split. apply exec_straight_one. + split. apply exec_straight_one. destruct c0; simpl; auto. - unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats32_inv; auto with asmgen. + unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats32_inv; auto with asmgen. split. destruct (rs x); destruct (rs x0); simpl; auto. repeat rewrite swap_floats_commut. apply testcond_for_float32_comparison_correct. - intros. Simplifs. apply compare_floats32_inv; auto with asmgen. + intros. Simplifs. apply compare_floats32_inv; auto with asmgen. (* notcompfs *) simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1). exists (nextinstr (compare_floats32 (swap_floats c0 (rs x) (rs x0)) (swap_floats c0 (rs x0) (rs x)) rs)). - split. apply exec_straight_one. + split. apply exec_straight_one. destruct c0; simpl; auto. - unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats32_inv; auto with asmgen. + unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats32_inv; auto with asmgen. split. destruct (rs x); destruct (rs x0); simpl; auto. repeat rewrite swap_floats_commut. apply testcond_for_neg_float32_comparison_correct. - intros. Simplifs. apply compare_floats32_inv; auto with asmgen. + intros. Simplifs. apply compare_floats32_inv; auto with asmgen. (* maskzero *) simpl. rewrite (ireg_of_eq _ _ EQ). econstructor. split. apply exec_straight_one. simpl; eauto. auto. - split. destruct (rs x); simpl; auto. + split. destruct (rs x); simpl; auto. generalize (compare_ints_spec rs (Vint (Int.and i0 i)) Vzero m). intros [A B]. rewrite A. unfold Val.cmpu; simpl. destruct (Int.eq (Int.and i0 i) Int.zero); auto. intros. unfold compare_ints. Simplifs. (* masknotzero *) simpl. rewrite (ireg_of_eq _ _ EQ). econstructor. split. apply exec_straight_one. simpl; eauto. auto. - split. destruct (rs x); simpl; auto. + split. destruct (rs x); simpl; auto. generalize (compare_ints_spec rs (Vint (Int.and i0 i)) Vzero m). intros [A B]. rewrite A. unfold Val.cmpu; simpl. destruct (Int.eq (Int.and i0 i) Int.zero); auto. intros. unfold compare_ints. Simplifs. @@ -879,8 +879,8 @@ Proof. intros. destruct cond; simpl in *. - (* base *) econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. Simplifs. intros; Simplifs. + apply exec_straight_one. simpl; eauto. auto. + split. Simplifs. intros; Simplifs. - (* or *) assert (Val.of_optbool match eval_testcond c1 rs1 with @@ -892,7 +892,7 @@ Proof. | None => None end = Val.or (Val.of_optbool (eval_testcond c1 rs1)) (Val.of_optbool (eval_testcond c2 rs1))). - destruct (eval_testcond c1 rs1). destruct (eval_testcond c2 rs1). + destruct (eval_testcond c1 rs1). destruct (eval_testcond c2 rs1). destruct b; destruct b0; auto. destruct b; auto. auto. @@ -908,11 +908,11 @@ Proof. econstructor; split. eapply exec_straight_three. simpl; eauto. - simpl. rewrite eval_testcond_nextinstr. repeat rewrite eval_testcond_set_ireg. eauto. - simpl. eauto. + simpl. rewrite eval_testcond_nextinstr. repeat rewrite eval_testcond_set_ireg. eauto. + simpl. eauto. auto. auto. auto. split. Simplifs. rewrite Val.or_commut. decEq; Simplifs. - intros. destruct H0; Simplifs. + intros. destruct H0; Simplifs. - (* and *) assert (Val.of_optbool match eval_testcond c1 rs1 with @@ -925,7 +925,7 @@ Proof. end = Val.and (Val.of_optbool (eval_testcond c1 rs1)) (Val.of_optbool (eval_testcond c2 rs1))). { - destruct (eval_testcond c1 rs1). destruct (eval_testcond c2 rs1). + destruct (eval_testcond c1 rs1). destruct (eval_testcond c2 rs1). destruct b; destruct b0; auto. destruct b; auto. auto. @@ -942,11 +942,11 @@ Proof. econstructor; split. eapply exec_straight_three. simpl; eauto. - simpl. rewrite eval_testcond_nextinstr. repeat rewrite eval_testcond_set_ireg. eauto. - simpl. eauto. + simpl. rewrite eval_testcond_nextinstr. repeat rewrite eval_testcond_set_ireg. eauto. + simpl. eauto. auto. auto. auto. split. Simplifs. rewrite Val.and_commut. decEq; Simplifs. - intros. destruct H0; Simplifs. + intros. destruct H0; Simplifs. Qed. Lemma mk_setcc_correct: @@ -959,10 +959,10 @@ Proof. intros. unfold mk_setcc. destruct (low_ireg rd). - apply mk_setcc_base_correct. - exploit mk_setcc_base_correct. intros [rs2 [A [B C]]]. - econstructor; split. eapply exec_straight_trans. eexact A. apply exec_straight_one. + econstructor; split. eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl. eauto. simpl. auto. - intuition Simplifs. -Qed. + intuition Simplifs. +Qed. (** Translation of arithmetic operations. *) @@ -980,7 +980,7 @@ Ltac ArgsInv := Ltac TranslOp := econstructor; split; - [ apply exec_straight_one; [ simpl; eauto | auto ] + [ apply exec_straight_one; [ simpl; eauto | auto ] | split; [ Simplifs | intros; Simplifs ]]. Lemma transl_op_correct: @@ -1005,12 +1005,12 @@ Transparent destroyed_by_op. /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r). { intros [rs' [A [B C]]]. subst v. exists rs'; auto. - } + } destruct op; simpl in TR; ArgsInv; simpl in EV; try (inv EV); try (apply SAME; TranslOp; fail). (* move *) - exploit mk_mov_correct; eauto. intros [rs2 [A [B C]]]. - apply SAME. exists rs2. eauto. + exploit mk_mov_correct; eauto. intros [rs2 [A [B C]]]. + apply SAME. exists rs2. eauto. (* intconst *) apply SAME. destruct (Int.eq_dec i Int.zero). subst i. TranslOp. TranslOp. (* floatconst *) @@ -1020,39 +1020,39 @@ Transparent destroyed_by_op. (* cast8signed *) apply SAME. eapply mk_intconv_correct; eauto. (* cast8unsigned *) - apply SAME. eapply mk_intconv_correct; eauto. + apply SAME. eapply mk_intconv_correct; eauto. (* cast16signed *) apply SAME. eapply mk_intconv_correct; eauto. (* cast16unsigned *) apply SAME. eapply mk_intconv_correct; eauto. (* mulhs *) - apply SAME. TranslOp. destruct H1. Simplifs. + apply SAME. TranslOp. destruct H1. Simplifs. (* mulhu *) - apply SAME. TranslOp. destruct H1. Simplifs. + apply SAME. TranslOp. destruct H1. Simplifs. (* div *) apply SAME. - specialize (divs_mods_exist (rs EAX) (rs ECX)). rewrite H0. + specialize (divs_mods_exist (rs EAX) (rs ECX)). rewrite H0. destruct (Val.mods (rs EAX) (rs ECX)) as [vr|] eqn:?; intros; try contradiction. TranslOp. change (rs#EDX<-Vundef ECX) with (rs#ECX). rewrite H0; rewrite Heqo. eauto. auto. auto. simpl in H3. destruct H3; Simplifs. (* divu *) apply SAME. - specialize (divu_modu_exist (rs EAX) (rs ECX)). rewrite H0. + specialize (divu_modu_exist (rs EAX) (rs ECX)). rewrite H0. destruct (Val.modu (rs EAX) (rs ECX)) as [vr|] eqn:?; intros; try contradiction. TranslOp. change (rs#EDX<-Vundef ECX) with (rs#ECX). rewrite H0; rewrite Heqo. eauto. auto. auto. simpl in H3. destruct H3; Simplifs. (* mod *) apply SAME. - specialize (divs_mods_exist (rs EAX) (rs ECX)). rewrite H0. + specialize (divs_mods_exist (rs EAX) (rs ECX)). rewrite H0. destruct (Val.divs (rs EAX) (rs ECX)) as [vr|] eqn:?; intros; try contradiction. TranslOp. change (rs#EDX<-Vundef ECX) with (rs#ECX). rewrite H0; rewrite Heqo. eauto. auto. auto. simpl in H3. destruct H3; Simplifs. (* modu *) apply SAME. - specialize (divu_modu_exist (rs EAX) (rs ECX)). rewrite H0. + specialize (divu_modu_exist (rs EAX) (rs ECX)). rewrite H0. destruct (Val.divu (rs EAX) (rs ECX)) as [vr|] eqn:?; intros; try contradiction. TranslOp. change (rs#EDX<-Vundef ECX) with (rs#ECX). rewrite H0; rewrite Heqo. eauto. auto. auto. @@ -1093,7 +1093,7 @@ Lemma transl_load_correct: /\ rs'#(preg_of dest) = v /\ forall r, data_preg r = true -> r <> preg_of dest -> rs'#r = rs#r. Proof. - unfold transl_load; intros. monadInv H. + unfold transl_load; intros. monadInv H. exploit transl_addressing_mode_correct; eauto. intro EA. assert (EA': eval_addrmode ge x rs = a). destruct a; simpl in H1; try discriminate; inv EA; auto. set (rs2 := nextinstr_nf (rs#(preg_of dest) <- v)). @@ -1102,10 +1102,10 @@ Proof. assert (rs2 PC = Val.add (rs PC) Vone). transitivity (Val.add ((rs#(preg_of dest) <- v) PC) Vone). auto. decEq. apply Pregmap.gso; auto with asmgen. - exists rs2. split. + exists rs2. split. destruct chunk; ArgsInv; apply exec_straight_one; auto. split. unfold rs2. rewrite nextinstr_nf_inv1. Simplifs. apply preg_of_data. - intros. unfold rs2. Simplifs. + intros. unfold rs2. Simplifs. Qed. Lemma transl_store_correct: @@ -1117,7 +1117,7 @@ Lemma transl_store_correct: exec_straight ge fn c rs m k rs' m' /\ forall r, data_preg r = true -> preg_notin r (destroyed_by_store chunk addr) -> rs'#r = rs#r. Proof. - unfold transl_store; intros. monadInv H. + unfold transl_store; intros. monadInv H. exploit transl_addressing_mode_correct; eauto. intro EA. assert (EA': eval_addrmode ge x rs = a). destruct a; simpl in H1; try discriminate; inv EA; auto. rewrite <- EA' in H1. destruct chunk; ArgsInv. @@ -1129,7 +1129,7 @@ Proof. eapply mk_smallstore_correct; eauto. (* int16signed *) econstructor; split. - apply exec_straight_one. simpl. unfold exec_store. + apply exec_straight_one. simpl. unfold exec_store. replace (Mem.storev Mint16unsigned m (eval_addrmode ge x rs) (rs x0)) with (Mem.storev Mint16signed m (eval_addrmode ge x rs) (rs x0)). rewrite H1. eauto. |