diff options
Diffstat (limited to 'arm')
-rw-r--r-- | arm/Asm.v | 2 | ||||
-rw-r--r-- | arm/Asmgenproof1.v | 24 | ||||
-rw-r--r-- | arm/ConstpropOp.vp | 8 | ||||
-rw-r--r-- | arm/ConstpropOpproof.v | 2 | ||||
-rw-r--r-- | arm/Conventions1.v | 7 | ||||
-rw-r--r-- | arm/Op.v | 4 | ||||
-rw-r--r-- | arm/SelectOp.vp | 6 | ||||
-rw-r--r-- | arm/Stacklayout.v | 6 |
8 files changed, 32 insertions, 27 deletions
@@ -900,7 +900,7 @@ Proof. { intros. inv H; inv H0; congruence. } assert (B: forall p v1 v2, extcall_arg_pair rs m p v1 -> extcall_arg_pair rs m p v2 -> v1 = v2). - { intros. inv H; inv H0. + { intros. inv H; inv H0. eapply A; eauto. f_equal; eapply A; eauto. } assert (C: forall ll vl1, list_forall2 (extcall_arg_pair rs m) ll vl1 -> diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 252a294a..eec531dc 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -30,7 +30,7 @@ Require Import Asmgen. Require Import Conventions. Require Import Asmgenproof0. -Local Transparent Archi.ptr64. +Local Transparent Archi.ptr64. (** Useful properties of the R14 registers. *) @@ -530,7 +530,7 @@ Lemma loadind_int_correct: Proof. intros; unfold loadind_int. assert (Val.offset_ptr (rs base) ofs = Val.add (rs base) (Vint (Ptrofs.to_int ofs))). - { destruct (rs base); try discriminate. simpl. f_equal; f_equal. symmetry; auto with ptrofs. } + { destruct (rs base); try discriminate. simpl. f_equal; f_equal. symmetry; auto with ptrofs. } apply indexed_memory_access_correct; intros. econstructor; split. apply exec_straight_one. simpl. unfold exec_load. rewrite H1, <- H0, H. eauto. auto. @@ -546,9 +546,9 @@ Lemma loadind_correct: /\ rs'#(preg_of dst) = v /\ forall r, if_preg r = true -> r <> IR14 -> r <> preg_of dst -> rs'#r = rs#r. Proof. - unfold loadind; intros. + unfold loadind; intros. assert (Val.offset_ptr (rs base) ofs = Val.add (rs base) (Vint (Ptrofs.to_int ofs))). - { destruct (rs base); try discriminate. simpl. f_equal; f_equal. symmetry; auto with ptrofs. } + { destruct (rs base); try discriminate. simpl. f_equal; f_equal. symmetry; auto with ptrofs. } destruct ty; destruct (preg_of dst); inv H; simpl in H0. - (* int *) apply loadind_int_correct; auto. @@ -587,32 +587,32 @@ Proof. unfold storeind; intros. assert (DATA: data_preg (preg_of src) = true) by eauto with asmgen. assert (Val.offset_ptr (rs base) ofs = Val.add (rs base) (Vint (Ptrofs.to_int ofs))). - { destruct (rs base); try discriminate. simpl. f_equal; f_equal. symmetry; auto with ptrofs. } + { destruct (rs base); try discriminate. simpl. f_equal; f_equal. symmetry; auto with ptrofs. } 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. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto. + apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto. intros; Simpl. - (* float *) apply indexed_memory_access_correct; intros. econstructor; split. - apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto. + apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto. intros; Simpl. - (* single *) apply indexed_memory_access_correct; intros. econstructor; split. - apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto. + apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto. intros; Simpl. - (* any32 *) apply indexed_memory_access_correct; intros. econstructor; split. - apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto. + apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto. intros; Simpl. - (* any64 *) apply indexed_memory_access_correct; intros. econstructor; split. - apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto. + apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto. intros; Simpl. Qed. @@ -1306,7 +1306,7 @@ Proof. exists rs', exec_straight ge fn c rs m k rs' m /\ 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). - { intros (rs' & A & B & C). subst v; exists rs'; auto. } + { intros (rs' & A & B & C). subst v; exists rs'; auto. } destruct op; try (apply SAME; eapply transl_op_correct_same; eauto; fail). - (* Oaddrstack *) clear SAME; simpl in *; ArgsInv. @@ -1372,7 +1372,7 @@ Proof. erewrite ! ireg_of_eq; eauto. rewrite transl_shift_correct. auto. (* Ainstack *) inv TR. apply indexed_memory_access_correct. intros. eapply MK1; eauto. - rewrite H. destruct (rs IR13); try contradiction. simpl. f_equal; f_equal. auto with ptrofs. + rewrite H. destruct (rs IR13); try contradiction. simpl. f_equal; f_equal. auto with ptrofs. Qed. Lemma transl_load_int_correct: diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp index e0f0889f..cb7a73eb 100644 --- a/arm/ConstpropOp.vp +++ b/arm/ConstpropOp.vp @@ -10,7 +10,7 @@ (* *) (* *********************************************************************) -(** Static analysis and strength reduction for operators +(** Static analysis and strength reduction for operators and conditions. This is the machine-dependent part of [Constprop]. *) Require Import Coqlib. @@ -51,7 +51,7 @@ Definition eval_static_shift (s: shift) (n: int) : int := | Sror x => Int.ror n x end. -Nondetfunction cond_strength_reduction +Nondetfunction cond_strength_reduction (cond: condition) (args: list reg) (vl: list aval) := match cond, args, vl with | Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil => @@ -98,7 +98,7 @@ Nondetfunction cond_strength_reduction if Float32.eq_dec n2 Float32.zero then (Cnotcompfszero c, r1 :: nil) else (cond, args) - | _, _, _ => + | _, _, _ => (cond, args) end. @@ -206,7 +206,7 @@ Definition make_cast8signed (r: reg) (a: aval) := Definition make_cast16signed (r: reg) (a: aval) := if vincl a (Sgn Ptop 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil). -Nondetfunction op_strength_reduction +Nondetfunction op_strength_reduction (op: operation) (args: list reg) (vl: list aval) := match op, args, vl with | Ocast8signed, r1 :: nil, v1 :: nil => make_cast8signed r1 v1 diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index e1ae80a2..c9f97aa8 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -116,7 +116,7 @@ Proof. + (* global *) inv H2. exists (Genv.symbol_address ge id ofs); auto. + (* stack *) - inv H2. exists (Vptr sp ofs); split; auto. simpl. rewrite Ptrofs.add_zero_l; auto. + inv H2. exists (Vptr sp ofs); split; auto. simpl. rewrite Ptrofs.add_zero_l; auto. Qed. Lemma eval_static_shift_correct: diff --git a/arm/Conventions1.v b/arm/Conventions1.v index ecf03e1d..86be8c95 100644 --- a/arm/Conventions1.v +++ b/arm/Conventions1.v @@ -60,6 +60,8 @@ Definition destroyed_at_call := Definition dummy_int_reg := R0. (**r Used in [Coloring]. *) Definition dummy_float_reg := F0. (**r Used in [Coloring]. *) +Definition callee_save_type := mreg_type. + Definition is_float_reg (r: mreg): bool := match r with | R0 | R1 | R2 | R3 @@ -136,7 +138,10 @@ Lemma loc_result_pair: forall sg, match loc_result sg with | One _ => True - | Twolong r1 r2 => r1 <> r2 /\ sg.(sig_res) = Some Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true /\ Archi.splitlong = true + | Twolong r1 r2 => + r1 <> r2 /\ sg.(sig_res) = Some Tlong + /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true + /\ Archi.ptr64 = false end. Proof. intros; unfold loc_result; destruct (sig_res sg) as [[]|]; destruct Archi.big_endian; auto. @@ -1102,7 +1102,7 @@ Proof. rewrite eval_shift_stack_addressing. eapply eval_addressing_inj with (sp1 := Vptr sp1 Ptrofs.zero); eauto. intros. apply symbol_address_inject. - econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. + econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. Qed. Lemma eval_operation_inject: @@ -1122,7 +1122,7 @@ Proof. intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. intros; eapply Mem.different_pointers_inject; eauto. intros; apply symbol_address_inject. - econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. + econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. Qed. End EVAL_INJECT. diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index 4ea1e1a1..fc2fbe6b 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -199,7 +199,7 @@ Definition mulhu (e1: expr) (e2: expr) := Eop Omulhu (e1 ::: e2 ::: Enil). (** ** Bitwise and, or, xor *) -Nondetfunction andimm (n1: int) (e2: expr) := +Nondetfunction andimm (n1: int) (e2: expr) := if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else if Int.eq n1 Int.mone then e2 else match e2 with @@ -343,14 +343,14 @@ Nondetfunction compimm (default: comparison -> int -> condition) Eop (Ocmp (negate_condition c)) el else if Int.eq_dec n2 Int.one then Eop (Ocmp c) el - else + else Eop (Ointconst Int.zero) Enil | Cne, Eop (Ocmp c) el => if Int.eq_dec n2 Int.zero then Eop (Ocmp c) el else if Int.eq_dec n2 Int.one then Eop (Ocmp (negate_condition c)) el - else + else Eop (Ointconst Int.one) Enil | _, _ => Eop (Ocmp (default c n2)) (e1 ::: Enil) diff --git a/arm/Stacklayout.v b/arm/Stacklayout.v index f5c07fff..c867ba59 100644 --- a/arm/Stacklayout.v +++ b/arm/Stacklayout.v @@ -86,16 +86,16 @@ Local Opaque Z.add Z.mul sepconj range. retaddr back link *) rewrite sep_swap12. - rewrite sep_swap45. + rewrite sep_swap45. rewrite sep_swap34. rewrite sep_swap45. (* Apply range_split and range_split2 repeatedly *) unfold fe_ofs_arg. apply range_split_2. fold ol; omega. omega. - apply range_split. omega. + apply range_split. omega. apply range_split_2. fold ora; omega. omega. apply range_split. omega. - apply range_drop_right with ostkdata. omega. + apply range_drop_right with ostkdata. omega. eapply sep_drop2. eexact H. Qed. |