From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- arm/Asmgenproof1.v | 284 ++++++++++++++++++++++++++--------------------------- 1 file changed, 142 insertions(+), 142 deletions(-) (limited to 'arm/Asmgenproof1.v') diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index f0a698eb..3e222ba4 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -51,7 +51,7 @@ Hint Resolve ireg_of_not_R14': asmgen. Lemma nextinstr_nf_pc: forall rs, (nextinstr_nf rs)#PC = Val.add rs#PC Vone. Proof. - intros. reflexivity. + intros. reflexivity. Qed. Definition if_preg (r: preg) : bool := @@ -83,7 +83,7 @@ Qed. Lemma nextinstr_nf_inv1: forall r rs, data_preg r = true -> (nextinstr_nf rs)#r = rs#r. Proof. - intros. destruct r; reflexivity || discriminate. + intros. destruct r; reflexivity || discriminate. Qed. (** Useful simplification tactic *) @@ -143,14 +143,14 @@ Proof. auto. predSpec Int.eq Int.eq_spec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero. auto. - simpl. rewrite IHN. rewrite Int.add_assoc. decEq. rewrite Int.add_and. + simpl. rewrite IHN. rewrite Int.add_assoc. decEq. rewrite Int.add_and. rewrite Int.or_not_self. apply Int.and_mone. apply Int.and_not_self. Qed. Remark decompose_int_arm_nil: forall N n p, decompose_int_arm N n p = nil -> n = Int.zero. Proof. - intros. generalize (decompose_int_arm_or N n p Int.zero). rewrite H. simpl. + intros. generalize (decompose_int_arm_or N n p Int.zero). rewrite H. simpl. rewrite Int.or_commut; rewrite Int.or_zero; auto. Qed. @@ -189,14 +189,14 @@ Proof. auto. predSpec Int.eq Int.eq_spec (Int.and n (Int.shl Int.one p)) Int.zero. auto. - simpl. rewrite IHN. rewrite Int.add_assoc. decEq. rewrite Int.add_and. + simpl. rewrite IHN. rewrite Int.add_assoc. decEq. rewrite Int.add_and. rewrite Int.or_not_self. apply Int.and_mone. apply Int.and_not_self. Qed. Remark decompose_int_thumb_nil: forall N n p, decompose_int_thumb N n p = nil -> n = Int.zero. Proof. - intros. generalize (decompose_int_thumb_or N n p Int.zero). rewrite H. simpl. + intros. generalize (decompose_int_thumb_or N n p Int.zero). rewrite H. simpl. rewrite Int.or_commut; rewrite Int.or_zero; auto. Qed. @@ -219,16 +219,16 @@ Proof. rewrite IHl. rewrite DISTR. decEq. decEq. auto. intros. unfold decompose_int, decompose_int_base. destruct (thumb tt); [destruct (is_immed_arith_thumb_special n)|]. -- reflexivity. +- reflexivity. - destruct (decompose_int_thumb 24%nat n Int.zero) eqn:DB. + simpl. exploit decompose_int_thumb_nil; eauto. congruence. + simpl. rewrite B. decEq. - generalize (DECOMP2 24%nat n Int.zero Int.zero). + generalize (DECOMP2 24%nat n Int.zero Int.zero). rewrite DB; simpl. rewrite ! ZERO. auto. - destruct (decompose_int_arm 12%nat n Int.zero) eqn:DB. + simpl. exploit decompose_int_arm_nil; eauto. congruence. + simpl. rewrite B. decEq. - generalize (DECOMP1 12%nat n Int.zero Int.zero). + generalize (DECOMP1 12%nat n Int.zero Int.zero). rewrite DB; simpl. rewrite ! ZERO. auto. Qed. @@ -240,7 +240,7 @@ Proof. intros. rewrite Val.or_assoc. auto. apply Int.or_assoc. intros. rewrite Int.or_commut. apply Int.or_zero. - apply decompose_int_arm_or. apply decompose_int_thumb_or. + apply decompose_int_arm_or. apply decompose_int_thumb_or. Qed. Lemma decompose_int_bic: @@ -259,7 +259,7 @@ Lemma decompose_int_xor: List.fold_left (fun v i => Val.xor v (Vint i)) (decompose_int n) v = Val.xor v (Vint n). Proof. intros. apply decompose_int_general with (f := fun v n => Val.xor v (Vint n)) (g := Int.xor). - intros. rewrite Val.xor_assoc. auto. + intros. rewrite Val.xor_assoc. auto. apply Int.xor_assoc. intros. rewrite Int.xor_commut. apply Int.xor_zero. apply decompose_int_arm_xor. apply decompose_int_thumb_xor. @@ -270,10 +270,10 @@ Lemma decompose_int_add: List.fold_left (fun v i => Val.add v (Vint i)) (decompose_int n) v = Val.add v (Vint n). Proof. intros. apply decompose_int_general with (f := fun v n => Val.add v (Vint n)) (g := Int.add). - intros. rewrite Val.add_assoc. auto. + intros. rewrite Val.add_assoc. auto. apply Int.add_assoc. intros. rewrite Int.add_commut. apply Int.add_zero. - apply decompose_int_arm_add. apply decompose_int_thumb_add. + apply decompose_int_arm_add. apply decompose_int_thumb_add. Qed. Lemma decompose_int_sub: @@ -281,11 +281,11 @@ Lemma decompose_int_sub: List.fold_left (fun v i => Val.sub v (Vint i)) (decompose_int n) v = Val.sub v (Vint n). Proof. intros. apply decompose_int_general with (f := fun v n => Val.sub v (Vint n)) (g := Int.add). - intros. repeat rewrite Val.sub_add_opp. rewrite Val.add_assoc. decEq. simpl. decEq. + intros. repeat rewrite Val.sub_add_opp. rewrite Val.add_assoc. decEq. simpl. decEq. rewrite Int.neg_add_distr; auto. apply Int.add_assoc. intros. rewrite Int.add_commut. apply Int.add_zero. - apply decompose_int_arm_add. apply decompose_int_thumb_add. + apply decompose_int_arm_add. apply decompose_int_thumb_add. Qed. Lemma iterate_op_correct: @@ -311,16 +311,16 @@ Proof. split. apply exec_straight_one. rewrite SEM1. reflexivity. reflexivity. intuition Simpl. (* inductive case *) - intros. - rewrite List.map_app. simpl. rewrite app_ass. simpl. + intros. + rewrite List.map_app. simpl. rewrite app_ass. simpl. destruct (H (op2 (SOimm x) :: k)) as [rs' [A [B C]]]. econstructor. split. eapply exec_straight_trans. eexact A. apply exec_straight_one. rewrite SEM2. reflexivity. reflexivity. - split. rewrite fold_left_app; simpl. Simpl. rewrite B. auto. + split. rewrite fold_left_app; simpl. Simpl. rewrite B. auto. intros; Simpl. Qed. - + (** Loading a constant. *) Lemma loadimm_correct: @@ -335,28 +335,28 @@ Proof. set (l2 := length (decompose_int (Int.not n))). destruct (NPeano.leb l1 1%nat). { (* single mov *) - econstructor; split. apply exec_straight_one. simpl; reflexivity. auto. + econstructor; split. apply exec_straight_one. simpl; reflexivity. auto. split; intros; Simpl. } destruct (NPeano.leb l2 1%nat). { (* single movn *) econstructor; split. apply exec_straight_one. - simpl. rewrite Int.not_involutive. reflexivity. auto. + simpl. rewrite Int.not_involutive. reflexivity. auto. split; intros; Simpl. } destruct (thumb tt). { (* movw / movt *) unfold loadimm_thumb. destruct (Int.eq (Int.shru n (Int.repr 16)) Int.zero). econstructor; split. - apply exec_straight_one. simpl; eauto. auto. split; intros; Simpl. + apply exec_straight_one. simpl; eauto. auto. split; intros; Simpl. econstructor; split. eapply exec_straight_two. simpl; reflexivity. simpl; reflexivity. auto. auto. - split; intros; Simpl. simpl. f_equal. rewrite Int.zero_ext_and by omega. + split; intros; Simpl. simpl. f_equal. rewrite Int.zero_ext_and by omega. rewrite Int.and_assoc. change 65535 with (two_p 16 - 1). rewrite Int.and_idem. - apply Int.same_bits_eq; intros. + apply Int.same_bits_eq; intros. rewrite Int.bits_or, Int.bits_and, Int.bits_shl, Int.testbit_repr by auto. rewrite Int.Ztestbit_two_p_m1 by omega. change (Int.unsigned (Int.repr 16)) with 16. destruct (zlt i 16). rewrite andb_true_r, orb_false_r; auto. - rewrite andb_false_r; simpl. rewrite Int.bits_shru by omega. + rewrite andb_false_r; simpl. rewrite Int.bits_shru by omega. change (Int.unsigned (Int.repr 16)) with 16. rewrite zlt_true by omega. f_equal; omega. } destruct (NPeano.leb l1 l2). @@ -388,8 +388,8 @@ Proof. intros. unfold addimm. destruct (Int.ltu (Int.repr (-256)) n). (* sub *) - econstructor; split. apply exec_straight_one; simpl; auto. - split; intros; Simpl. apply Val.sub_opp_add. + econstructor; split. apply exec_straight_one; simpl; auto. + split; intros; Simpl. apply Val.sub_opp_add. destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.neg n)))). (* add - add* *) replace (Val.add (rs r2) (Vint n)) @@ -445,7 +445,7 @@ Proof. auto. intros. simpl. destruct (rs r2); auto. simpl. rewrite Int.sub_add_opp. rewrite Int.add_commut; auto. - rewrite decompose_int_add. + rewrite decompose_int_add. destruct (rs r2); simpl; auto. rewrite Int.sub_add_opp. rewrite Int.add_commut; auto. Qed. @@ -497,14 +497,14 @@ Lemma indexed_memory_access_correct: (forall (r: preg), if_preg r = true -> r <> IR14 -> rs1 r = rs r) -> exists rs', exec_straight ge fn (mk_instr r1 n1 :: k) rs1 m k rs' m' /\ P rs') -> - exists rs', + exists rs', exec_straight ge fn (indexed_memory_access mk_instr mk_immed base n k) rs m k rs' m' /\ P rs'. Proof. intros until m'; intros SEM. - unfold indexed_memory_access. + unfold indexed_memory_access. destruct (Int.eq n (mk_immed n)). - apply SEM; auto. - destruct (addimm_correct IR14 base (Int.sub n (mk_immed n)) (mk_instr IR14 (mk_immed n) :: k) rs m) @@ -512,10 +512,10 @@ Proof. destruct (SEM IR14 rs1 (mk_immed n) k) as (rs2 & D & E). rewrite B. rewrite Val.add_assoc. f_equal. simpl. rewrite Int.sub_add_opp. rewrite Int.add_assoc. - rewrite (Int.add_commut (Int.neg (mk_immed n))). + rewrite (Int.add_commut (Int.neg (mk_immed n))). rewrite Int.add_neg_zero. rewrite Int.add_zero. auto. - auto with asmgen. - exists rs2; split; auto. eapply exec_straight_trans; eauto. + auto with asmgen. + exists rs2; split; auto. eapply exec_straight_trans; eauto. Qed. Lemma loadind_int_correct: @@ -527,7 +527,7 @@ Lemma loadind_int_correct: /\ forall r, if_preg r = true -> r <> IR14 -> r <> dst -> rs'#r = rs#r. Proof. intros; unfold loadind_int. apply indexed_memory_access_correct; intros. - econstructor; split. + econstructor; split. apply exec_straight_one. simpl. unfold exec_load. rewrite H0; rewrite H; eauto. auto. split; intros; Simpl. Qed. @@ -543,26 +543,26 @@ Lemma loadind_correct: Proof. unfold loadind; intros. destruct ty; destruct (preg_of dst); inv H; simpl in H0. - (* int *) - apply loadind_int_correct; auto. + apply loadind_int_correct; auto. - (* float *) apply indexed_memory_access_correct; intros. - econstructor; split. - apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto. + econstructor; split. + apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto. split; intros; Simpl. - (* single *) apply indexed_memory_access_correct; intros. - econstructor; split. - apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto. + econstructor; split. + apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto. split; intros; Simpl. - (* any32 *) apply indexed_memory_access_correct; intros. - econstructor; split. - apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto. + econstructor; split. + apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto. split; intros; Simpl. - (* any64 *) apply indexed_memory_access_correct; intros. - econstructor; split. - apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto. + econstructor; split. + apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto. split; intros; Simpl. Qed. @@ -581,32 +581,32 @@ Proof. destruct ty; destruct (preg_of src); inv H; simpl in H0. - (* int *) apply indexed_memory_access_correct; intros. - econstructor; split. - apply exec_straight_one. simpl. unfold exec_store. + econstructor; split. + apply exec_straight_one. simpl. unfold exec_store. rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto. intros; Simpl. - (* float *) apply indexed_memory_access_correct; intros. - econstructor; split. - apply exec_straight_one. simpl. unfold exec_store. + econstructor; split. + apply exec_straight_one. simpl. unfold exec_store. rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto. intros; Simpl. - (* single *) apply indexed_memory_access_correct; intros. - econstructor; split. - apply exec_straight_one. simpl. unfold exec_store. + econstructor; split. + apply exec_straight_one. simpl. unfold exec_store. rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto. intros; Simpl. - (* any32 *) apply indexed_memory_access_correct; intros. - econstructor; split. - apply exec_straight_one. simpl. unfold exec_store. + econstructor; split. + apply exec_straight_one. simpl. unfold exec_store. rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto. intros; Simpl. - (* any64 *) apply indexed_memory_access_correct; intros. - econstructor; split. - apply exec_straight_one. simpl. unfold exec_store. + econstructor; split. + apply exec_straight_one. simpl. unfold exec_store. rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto. intros; Simpl. Qed. @@ -639,19 +639,19 @@ Lemma compare_int_inv: forall r', data_preg r' = true -> rs1#r' = rs#r'. Proof. intros. unfold rs1, compare_int. - repeat Simplif. + 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. + 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: @@ -660,8 +660,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. @@ -677,8 +677,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. @@ -733,16 +733,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). @@ -780,7 +780,7 @@ Proof. assert (nextinstr (rs#CN <- Vundef #CZ <- Vundef #CC <- Vundef #CV <- Vundef) r' = rs r'). { repeat Simplif. } destruct v1; destruct v2; auto. - repeat Simplif. + repeat Simplif. Qed. Lemma compare_float_nextpc: @@ -797,7 +797,7 @@ Lemma cond_for_float_cmp_correct: Some(Float.cmp c n1 n2). Proof. intros. - generalize (compare_float_spec rs n1 n2). + 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. @@ -809,7 +809,7 @@ Proof. (* lt *) destruct (Float.cmp Clt n1 n2); auto. (* le *) - rewrite Float.cmp_le_lt_eq. + 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; @@ -819,7 +819,7 @@ Proof. exfalso; eapply Float.cmp_gt_eq_false; eauto. exfalso; eapply Float.cmp_lt_gt_false; eauto. (* ge *) - rewrite Float.cmp_ge_gt_eq. + 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. @@ -847,7 +847,7 @@ Proof. (* lt *) destruct (Float.cmp Clt n1 n2); auto. (* le *) - rewrite Float.cmp_le_lt_eq. + 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; @@ -857,7 +857,7 @@ Proof. exfalso; eapply Float.cmp_gt_eq_false; eauto. exfalso; eapply Float.cmp_lt_gt_false; eauto. (* ge *) - rewrite Float.cmp_ge_gt_eq. + 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. @@ -886,7 +886,7 @@ Proof. assert (nextinstr (rs#CN <- Vundef #CZ <- Vundef #CC <- Vundef #CV <- Vundef) r' = rs r'). { repeat Simplif. } destruct v1; destruct v2; auto. - repeat Simplif. + repeat Simplif. Qed. Lemma compare_float32_nextpc: @@ -903,7 +903,7 @@ Lemma cond_for_float32_cmp_correct: Some(Float32.cmp c n1 n2). Proof. intros. - generalize (compare_float32_spec rs n1 n2). + generalize (compare_float32_spec rs n1 n2). set (rs' := nextinstr (compare_float32 rs (Vsingle n1) (Vsingle n2))). intros [A [B [C D]]]. unfold eval_testcond. rewrite A; rewrite B; rewrite C; rewrite D. @@ -915,7 +915,7 @@ Proof. (* lt *) destruct (Float32.cmp Clt n1 n2); auto. (* le *) - rewrite Float32.cmp_le_lt_eq. + rewrite Float32.cmp_le_lt_eq. destruct (Float32.cmp Clt n1 n2); destruct (Float32.cmp Ceq n1 n2); auto. (* gt *) destruct (Float32.cmp Ceq n1 n2) eqn:EQ; @@ -925,7 +925,7 @@ Proof. exfalso; eapply Float32.cmp_gt_eq_false; eauto. exfalso; eapply Float32.cmp_lt_gt_false; eauto. (* ge *) - rewrite Float32.cmp_ge_gt_eq. + rewrite Float32.cmp_ge_gt_eq. destruct (Float32.cmp Ceq n1 n2) eqn:EQ; destruct (Float32.cmp Clt n1 n2) eqn:LT; destruct (Float32.cmp Cgt n1 n2) eqn:GT; auto. @@ -953,7 +953,7 @@ Proof. (* lt *) destruct (Float32.cmp Clt n1 n2); auto. (* le *) - rewrite Float32.cmp_le_lt_eq. + rewrite Float32.cmp_le_lt_eq. destruct (Float32.cmp Clt n1 n2) eqn:LT; destruct (Float32.cmp Ceq n1 n2) eqn:EQ; auto. (* gt *) destruct (Float32.cmp Ceq n1 n2) eqn:EQ; @@ -963,7 +963,7 @@ Proof. exfalso; eapply Float32.cmp_gt_eq_false; eauto. exfalso; eapply Float32.cmp_lt_gt_false; eauto. (* ge *) - rewrite Float32.cmp_ge_gt_eq. + rewrite Float32.cmp_ge_gt_eq. destruct (Float32.cmp Ceq n1 n2) eqn:EQ; destruct (Float32.cmp Clt n1 n2) eqn:LT; destruct (Float32.cmp Cgt n1 n2) eqn:GT; auto. @@ -998,14 +998,14 @@ Lemma transl_cond_correct: end /\ forall r, data_preg r = true -> rs'#r = rs r. Proof. - intros until c; intros TR. + intros until c; intros TR. unfold transl_cond in TR; destruct cond; ArgsInv. - (* Ccomp *) econstructor. split. apply exec_straight_one. simpl. eauto. auto. split. destruct (Val.cmp_bool c0 (rs x) (rs x0)) eqn:CMP; auto. split; apply cond_for_signed_cmp_correct; auto. rewrite Val.negate_cmp_bool, CMP; auto. - apply compare_int_inv. + apply compare_int_inv. - (* Ccompu *) econstructor. split. apply exec_straight_one. simpl. eauto. auto. @@ -1030,17 +1030,17 @@ Proof. destruct (is_immed_arith i). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. destruct (Val.cmp_bool c0 (rs x) (Vint i)) eqn:CMP; auto. + split. destruct (Val.cmp_bool c0 (rs x) (Vint i)) eqn:CMP; auto. split; apply cond_for_signed_cmp_correct; auto. rewrite Val.negate_cmp_bool, CMP; auto. apply compare_int_inv. exploit (loadimm_correct IR14). intros [rs' [P [Q R]]]. econstructor. split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl. rewrite Q. rewrite R; eauto with asmgen. auto. - split. rewrite <- R by (eauto with asmgen). + split. rewrite <- R by (eauto with asmgen). destruct (Val.cmp_bool c0 (rs' x) (Vint i)) eqn:CMP; auto. split; apply cond_for_signed_cmp_correct; auto. rewrite Val.negate_cmp_bool, CMP; auto. - intros. rewrite compare_int_inv by auto. auto with asmgen. + intros. rewrite compare_int_inv by auto. auto with asmgen. - (* Ccompuimm *) destruct (is_immed_arith i). econstructor. @@ -1052,17 +1052,17 @@ Proof. econstructor. split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl. rewrite Q. rewrite R; eauto with asmgen. auto. - split. rewrite <- R by (eauto 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. split; apply cond_for_unsigned_cmp_correct; auto. rewrite Val.negate_cmpu_bool, CMP; auto. - intros. rewrite compare_int_inv by auto. auto with asmgen. + intros. rewrite compare_int_inv by auto. auto with asmgen. - (* Ccompf *) econstructor. 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. - split. apply cond_for_float_cmp_correct. apply cond_for_float_not_cmp_correct. + split. apply cond_for_float_cmp_correct. apply cond_for_float_not_cmp_correct. apply compare_float_inv. - (* Cnotcompf *) econstructor. @@ -1080,7 +1080,7 @@ Local Opaque compare_float. simpl. split. destruct (Val.cmpf_bool c0 (rs x) (Vfloat Float.zero)) eqn:CMP; auto. destruct (rs x); try discriminate. simpl in CMP. inv CMP. - split. apply cond_for_float_cmp_correct. apply cond_for_float_not_cmp_correct. + split. apply cond_for_float_cmp_correct. apply cond_for_float_not_cmp_correct. apply compare_float_inv. - (* Cnotcompfzero *) econstructor. @@ -1096,7 +1096,7 @@ Local Opaque compare_float. simpl. split. apply exec_straight_one. simpl. eauto. apply compare_float32_nextpc. split. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) eqn:CMP; auto. destruct (rs x); try discriminate. destruct (rs x0); try discriminate. - simpl in CMP. inv CMP. + simpl in CMP. inv CMP. split. apply cond_for_float32_cmp_correct. apply cond_for_float32_not_cmp_correct. apply compare_float32_inv. - (* Cnotcompfs *) @@ -1144,7 +1144,7 @@ Lemma transl_op_correct_same: /\ rs'#(preg_of res) = v /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs'#r = rs#r. Proof. - intros until v; intros TR EV NOCMP. + intros until v; intros TR EV NOCMP. unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; inv EV; try (TranslOpSimpl; fail). (* Omove *) destruct (preg_of res) eqn:RES; try discriminate; @@ -1152,12 +1152,12 @@ Proof. econstructor; split. apply exec_straight_one; simpl; eauto. intuition Simpl. econstructor; split. apply exec_straight_one; simpl; eauto. intuition Simpl. (* Ointconst *) - generalize (loadimm_correct x i k rs m). intros [rs' [A [B C]]]. - exists rs'; auto with asmgen. + generalize (loadimm_correct x i k rs m). intros [rs' [A [B C]]]. + exists rs'; auto with asmgen. (* Oaddrstack *) - generalize (addimm_correct x IR13 i k rs m). + generalize (addimm_correct x IR13 i k rs m). intros [rs' [EX [RES OTH]]]. - exists rs'; auto with asmgen. + exists rs'; auto with asmgen. (* Ocast8signed *) destruct (thumb tt). econstructor; split. apply exec_straight_one; simpl; eauto. intuition Simpl. @@ -1165,12 +1165,12 @@ Proof. set (rs1 := nextinstr_nf (rs#x <- (Val.shl rs#x0 (Vint (Int.repr 24))))). set (rs2 := nextinstr_nf (rs1#x <- (Val.shr rs1#x (Vint (Int.repr 24))))). exists rs2. - split. apply exec_straight_two with rs1 m; auto. + split. apply exec_straight_two with rs1 m; auto. split. unfold rs2; Simpl. unfold rs1; Simpl. - unfold Val.shr, Val.shl; destruct (rs x0); auto. + unfold Val.shr, Val.shl; destruct (rs x0); auto. change (Int.ltu (Int.repr 24) Int.iwordsize) with true; simpl. f_equal. symmetry. apply (Int.sign_ext_shr_shl 8). compute; auto. - intros. unfold rs2, rs1; Simpl. + intros. unfold rs2, rs1; Simpl. (* Ocast16signed *) destruct (thumb tt). econstructor; split. apply exec_straight_one; simpl; eauto. intuition Simpl. @@ -1178,15 +1178,15 @@ Proof. set (rs1 := nextinstr_nf (rs#x <- (Val.shl rs#x0 (Vint (Int.repr 16))))). set (rs2 := nextinstr_nf (rs1#x <- (Val.shr rs1#x (Vint (Int.repr 16))))). exists rs2. - split. apply exec_straight_two with rs1 m; auto. + split. apply exec_straight_two with rs1 m; auto. split. unfold rs2; Simpl. unfold rs1; Simpl. - unfold Val.shr, Val.shl; destruct (rs x0); auto. + unfold Val.shr, Val.shl; destruct (rs x0); auto. change (Int.ltu (Int.repr 16) Int.iwordsize) with true; simpl. f_equal. symmetry. apply (Int.sign_ext_shr_shl 16). compute; auto. - intros. unfold rs2, rs1; Simpl. + intros. unfold rs2, rs1; Simpl. (* Oaddimm *) generalize (addimm_correct x x0 i k rs m). - intros [rs' [A [B C]]]. + intros [rs' [A [B C]]]. exists rs'; auto with asmgen. (* Orsbimm *) generalize (rsubimm_correct x x0 i k rs m). @@ -1195,44 +1195,44 @@ Proof. (* divs *) Local Transparent destroyed_by_op. econstructor. split. apply exec_straight_one. simpl. rewrite H0. reflexivity. auto. - split. Simpl. simpl; intros. intuition Simpl. + split. Simpl. simpl; intros. intuition Simpl. (* divu *) econstructor. split. apply exec_straight_one. simpl. rewrite H0. reflexivity. auto. - split. Simpl. simpl; intros. intuition Simpl. + split. Simpl. simpl; intros. intuition Simpl. (* Oandimm *) - generalize (andimm_correct x x0 i k rs m). - intros [rs' [A [B C]]]. + generalize (andimm_correct x x0 i k rs m). + intros [rs' [A [B C]]]. exists rs'; auto with asmgen. (* Oorimm *) generalize (orimm_correct x x0 i k rs m). - intros [rs' [A [B C]]]. + intros [rs' [A [B C]]]. exists rs'; auto with asmgen. (* Oxorimm *) generalize (xorimm_correct x x0 i k rs m). - intros [rs' [A [B C]]]. + intros [rs' [A [B C]]]. exists rs'; auto with asmgen. (* Oshrximm *) - destruct (rs x0) eqn: X0; simpl in H0; try discriminate. - destruct (Int.ltu i (Int.repr 31)) eqn: LTU; inv H0. - revert EQ2. predSpec Int.eq Int.eq_spec i Int.zero; intros EQ2. + destruct (rs x0) eqn: X0; simpl in H0; try discriminate. + destruct (Int.ltu i (Int.repr 31)) eqn: LTU; inv H0. + revert EQ2. predSpec Int.eq Int.eq_spec i Int.zero; intros EQ2. (* i = 0 *) - inv EQ2. econstructor. - split. apply exec_straight_one. simpl. reflexivity. auto. - split. Simpl. unfold Int.shrx. rewrite Int.shl_zero. unfold Int.divs. + inv EQ2. econstructor. + split. apply exec_straight_one. simpl. reflexivity. auto. + split. Simpl. unfold Int.shrx. rewrite Int.shl_zero. unfold Int.divs. change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed. auto. - intros. Simpl. + intros. Simpl. (* i <> 0 *) inv EQ2. assert (LTU': Int.ltu (Int.sub Int.iwordsize i) Int.iwordsize = true). { generalize (Int.ltu_inv _ _ LTU). intros. - unfold Int.sub, Int.ltu. rewrite Int.unsigned_repr_wordsize. + unfold Int.sub, Int.ltu. rewrite Int.unsigned_repr_wordsize. rewrite Int.unsigned_repr. apply zlt_true. - assert (Int.unsigned i <> 0). + assert (Int.unsigned i <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned i). rewrite H1; reflexivity. } - omega. + omega. change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1) in H0. - generalize Int.wordsize_max_unsigned; omega. + generalize Int.wordsize_max_unsigned; omega. } assert (LTU'': Int.ltu i Int.iwordsize = true). { @@ -1250,16 +1250,16 @@ Local Transparent destroyed_by_op. simpl. rewrite X0; reflexivity. simpl. f_equal. Simpl. replace (rs1 x0) with (rs x0). rewrite X0; reflexivity. unfold rs1; Simpl. - reflexivity. + reflexivity. auto. auto. auto. - split. unfold rs3; Simpl. unfold rs2; Simpl. unfold rs1; Simpl. - simpl. change (Int.ltu (Int.repr 31) Int.iwordsize) with true. simpl. - rewrite LTU'; simpl. rewrite LTU''; simpl. - f_equal. symmetry. apply Int.shrx_shr_2. assumption. - intros. unfold rs3; Simpl. unfold rs2; Simpl. unfold rs1; Simpl. + split. unfold rs3; Simpl. unfold rs2; Simpl. unfold rs1; Simpl. + simpl. change (Int.ltu (Int.repr 31) Int.iwordsize) with true. simpl. + rewrite LTU'; simpl. rewrite LTU''; simpl. + f_equal. symmetry. apply Int.shrx_shr_2. assumption. + intros. unfold rs3; Simpl. unfold rs2; Simpl. unfold rs1; Simpl. (* intoffloat *) econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto. -Transparent destroyed_by_op. +Transparent destroyed_by_op. simpl. intuition Simpl. (* intuoffloat *) econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto. @@ -1295,21 +1295,21 @@ Lemma transl_op_correct: /\ Val.lessdef v rs'#(preg_of res) /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs'#r = rs#r. Proof. - intros. + intros. assert (EITHER: match op with Ocmp _ => False | _ => True end \/ exists cmp, op = Ocmp cmp). destruct op; auto. right; exists c0; auto. - destruct EITHER as [A | [cmp A]]. + destruct EITHER as [A | [cmp A]]. exploit transl_op_correct_same; eauto. intros [rs' [P [Q R]]]. - subst v. exists rs'; eauto. + subst v. exists rs'; eauto. (* Ocmp *) - subst op. simpl in H. monadInv H. simpl in H0. inv H0. + subst op. simpl in H. monadInv H. simpl in H0. inv H0. rewrite (ireg_of_eq _ _ EQ). exploit transl_cond_correct; eauto. instantiate (1 := rs). instantiate (1 := m). intros [rs1 [A [B C]]]. econstructor; split. eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto. split; intros; Simpl. destruct (eval_condition cmp rs ## (preg_of ## args) m) as [b|]; simpl; auto. - destruct B as [B1 B2]; rewrite B1. destruct b; auto. + destruct B as [B1 B2]; rewrite B1. destruct b; auto. Qed. (** Translation of loads and stores. *) @@ -1352,7 +1352,7 @@ Proof. simpl. erewrite ! ireg_of_eq; eauto. (* Aindexed2shift *) destruct mk_instr_gen as [mk | ]; monadInv TR. apply MK2. - erewrite ! ireg_of_eq; eauto. rewrite transl_shift_correct. auto. + erewrite ! ireg_of_eq; eauto. rewrite transl_shift_correct. auto. (* Ainstack *) inv TR. apply indexed_memory_access_correct. exact MK1. Qed. @@ -1370,13 +1370,13 @@ Lemma transl_load_int_correct: /\ rs'#(preg_of dst) = v /\ forall r, data_preg r = true -> r <> preg_of dst -> rs'#r = rs#r. Proof. - intros. monadInv H. erewrite ireg_of_eq by eauto. + intros. monadInv H. erewrite ireg_of_eq by eauto. eapply transl_memory_access_correct; eauto. - intros; simpl. econstructor; split. apply exec_straight_one. + intros; simpl. econstructor; split. apply exec_straight_one. rewrite H2. unfold exec_load. simpl eval_shift_op. rewrite H. rewrite H1. eauto. auto. - split. Simpl. intros; Simpl. - simpl; intros. - econstructor; split. apply exec_straight_one. + split. Simpl. intros; Simpl. + simpl; intros. + econstructor; split. apply exec_straight_one. rewrite H2. unfold exec_load. rewrite H. rewrite H1. eauto. auto. split. Simpl. intros; Simpl. Qed. @@ -1394,9 +1394,9 @@ Lemma transl_load_float_correct: /\ rs'#(preg_of dst) = v /\ forall r, data_preg r = true -> r <> preg_of dst -> rs'#r = rs#r. Proof. - intros. monadInv H. erewrite freg_of_eq by eauto. + intros. monadInv H. erewrite freg_of_eq by eauto. eapply transl_memory_access_correct; eauto. - intros; simpl. econstructor; split. apply exec_straight_one. + intros; simpl. econstructor; split. apply exec_straight_one. rewrite H2. unfold exec_load. rewrite H. rewrite H1. eauto. auto. split. Simpl. intros; Simpl. simpl; auto. @@ -1415,14 +1415,14 @@ Lemma transl_store_int_correct: /\ forall r, data_preg r = true -> preg_notin r mr -> rs'#r = rs#r. Proof. intros. assert (DR: data_preg (preg_of src) = true) by eauto with asmgen. - monadInv H. erewrite ireg_of_eq in * by eauto. + monadInv H. erewrite ireg_of_eq in * by eauto. eapply transl_memory_access_correct; eauto. - intros; simpl. econstructor; split. apply exec_straight_one. - rewrite H2. unfold exec_store. simpl eval_shift_op. rewrite H. rewrite H3; eauto with asmgen. + intros; simpl. econstructor; split. apply exec_straight_one. + rewrite H2. unfold exec_store. simpl eval_shift_op. rewrite H. rewrite H3; eauto with asmgen. rewrite H1. eauto. auto. intros; Simpl. - simpl; intros. - econstructor; split. apply exec_straight_one. + simpl; intros. + econstructor; split. apply exec_straight_one. rewrite H2. unfold exec_store. rewrite H. rewrite H1. eauto. auto. intros; Simpl. Qed. @@ -1440,9 +1440,9 @@ Lemma transl_store_float_correct: /\ forall r, data_preg r = true -> preg_notin r mr -> rs'#r = rs#r. Proof. intros. assert (DR: data_preg (preg_of src) = true) by eauto with asmgen. - monadInv H. erewrite freg_of_eq in * by eauto. + monadInv H. erewrite freg_of_eq in * by eauto. eapply transl_memory_access_correct; eauto. - intros; simpl. econstructor; split. apply exec_straight_one. + intros; simpl. econstructor; split. apply exec_straight_one. rewrite H2. unfold exec_store. rewrite H. rewrite H3; auto with asmgen. rewrite H1. eauto. auto. intros; Simpl. simpl; auto. -- cgit