diff options
Diffstat (limited to 'x86')
| -rw-r--r-- | x86/Asm.v | 6 | ||||
| -rw-r--r-- | x86/Asmexpand.ml | 10 | ||||
| -rw-r--r-- | x86/Asmgenproof.v | 8 | ||||
| -rw-r--r-- | x86/Asmgenproof1.v | 2 | ||||
| -rw-r--r-- | x86/CombineOpproof.v | 4 | ||||
| -rw-r--r-- | x86/ConstpropOp.vp | 6 | ||||
| -rw-r--r-- | x86/ConstpropOpproof.v | 48 | ||||
| -rw-r--r-- | x86/Conventions1.v | 32 | ||||
| -rw-r--r-- | x86/Machregs.v | 4 | ||||
| -rw-r--r-- | x86/NeedOp.v | 2 | ||||
| -rw-r--r-- | x86/Op.v | 18 | ||||
| -rw-r--r-- | x86/SelectLongproof.v | 6 | ||||
| -rw-r--r-- | x86/SelectOp.vp | 8 | ||||
| -rw-r--r-- | x86/SelectOpproof.v | 18 | ||||
| -rw-r--r-- | x86/Stacklayout.v | 10 |
15 files changed, 92 insertions, 90 deletions
@@ -209,7 +209,7 @@ Inductive instruction: Type := | Pcmpl_ri (r1: ireg) (n: int) | Pcmpq_ri (r1: ireg) (n: int64) | Ptestl_rr (r1 r2: ireg) - | Ptestq_rr (r1 r2: ireg) + | Ptestq_rr (r1 r2: ireg) | Ptestl_ri (r1: ireg) (n: int) | Ptestq_ri (r1: ireg) (n: int64) | Pcmov (c: testcond) (rd: ireg) (r1: ireg) @@ -792,7 +792,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pxorl_rr rd r1 => Next (nextinstr_nf (rs#rd <- (Val.xor rs#rd rs#r1))) m | Pxorq_rr rd r1 => - Next (nextinstr_nf (rs#rd <- (Val.xorl rs#rd rs#r1))) m + Next (nextinstr_nf (rs#rd <- (Val.xorl rs#rd rs#r1))) m | Pxorl_ri rd n => Next (nextinstr_nf (rs#rd <- (Val.xor rs#rd (Vint n)))) m | Pxorq_ri rd n => @@ -1145,7 +1145,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/x86/Asmexpand.ml b/x86/Asmexpand.ml index 90dc0e69..8e69061e 100644 --- a/x86/Asmexpand.ml +++ b/x86/Asmexpand.ml @@ -29,7 +29,7 @@ let _1 = Integers.Int.one let _2 = coqint_of_camlint 2l let _4 = coqint_of_camlint 4l let _8 = coqint_of_camlint 8l - + let _0z = Z.zero let _1z = Z.one let _2z = Z.of_sint 2 @@ -49,7 +49,7 @@ let _Plea (r, addr) = let align n a = if n >= 0 then (n + a - 1) land (-a) else n land (-a) -let sp_adjustment_32 sz = +let sp_adjustment_32 sz = let sz = Z.to_int sz in (* Preserve proper alignment of the stack *) let sz = align sz (stack_alignment ()) in @@ -72,7 +72,7 @@ let sp_adjustment_64 sz = (* The top 8 bytes have already been allocated by the "call" instruction. *) (sz - 8, -1) end - + (* Built-ins. They come in two flavors: - annotation statements: take their arguments in registers or stack locations; generate no code; @@ -500,7 +500,7 @@ let expand_instruction instr = emit (Pleaq (RAX, addr1)); emit (Pmovq_mr (addr2, RAX)); current_function_stacksize := Int64.of_int fullsz - end else begin + end else begin let sz = sp_adjustment_32 sz in (* Allocate frame *) let sz' = Z.of_uint sz in @@ -512,7 +512,7 @@ let expand_instruction instr = emit (Pleal (RAX,addr1)); emit (Pmovl_mr (addr2,RAX)); PrintAsmaux.current_function_stacksize := Int32.of_int sz - end + end | Pfreeframe(sz, ofs_ra, ofs_link) -> if Archi.ptr64 then begin let (sz, _) = sp_adjustment_64 sz in diff --git a/x86/Asmgenproof.v b/x86/Asmgenproof.v index e56dc429..6caf4531 100644 --- a/x86/Asmgenproof.v +++ b/x86/Asmgenproof.v @@ -780,7 +780,7 @@ Opaque loadind. exploit functions_transl; eauto. intro FN. generalize (transf_function_no_overflow _ _ H5); intro NOOV. set (rs1 := rs0 #RAX <- Vundef #RDX <- Vundef). - exploit (find_label_goto_label f tf lbl rs1); eauto. + exploit (find_label_goto_label f tf lbl rs1); eauto. intros [tc' [rs' [A [B C]]]]. exploit ireg_val; eauto. rewrite H. intros LD; inv LD. left; econstructor; split. @@ -789,7 +789,7 @@ Opaque loadind. simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eexact A. econstructor; eauto. Transparent destroyed_by_jumptable. - apply agree_undef_regs with rs0; auto. + apply agree_undef_regs with rs0; auto. simpl; intros. destruct H8. rewrite C by auto with asmgen. unfold rs1; Simplifs. congruence. @@ -834,7 +834,7 @@ Transparent destroyed_by_jumptable. left; econstructor; split. apply plus_one. econstructor; eauto. simpl. rewrite Ptrofs.unsigned_zero. simpl. eauto. - simpl. rewrite C. simpl in F, P. + simpl. rewrite C. simpl in F, P. replace (chunk_of_type Tptr) with Mptr in F, P by (unfold Tptr, Mptr; destruct Archi.ptr64; auto). rewrite (sp_val _ _ _ AG) in F. rewrite F. rewrite ATLR. rewrite P. eauto. @@ -883,7 +883,7 @@ Proof. econstructor; eauto. constructor. apply Mem.extends_refl. - split. reflexivity. simpl. + split. reflexivity. simpl. unfold Vnullptr; destruct Archi.ptr64; congruence. intros. rewrite Regmap.gi. auto. unfold Genv.symbol_address. diff --git a/x86/Asmgenproof1.v b/x86/Asmgenproof1.v index 6191ea39..aade95d2 100644 --- a/x86/Asmgenproof1.v +++ b/x86/Asmgenproof1.v @@ -254,7 +254,7 @@ Proof. set (rs5 := nextinstr_nf (rs4#RAX <- v4)). assert (X: forall v1 v2, Val.addl v1 (Val.addl v2 (Vlong Int64.zero)) = Val.addl v1 v2). - { intros. unfold Val.addl; destruct Archi.ptr64 eqn:SF, v0; auto; destruct v5; auto. + { intros. unfold Val.addl; destruct Archi.ptr64 eqn:SF, v0; auto; destruct v5; auto. rewrite Int64.add_zero; auto. rewrite Ptrofs.add_zero; auto. rewrite Int64.add_zero; auto. diff --git a/x86/CombineOpproof.v b/x86/CombineOpproof.v index f59e582b..a7024501 100644 --- a/x86/CombineOpproof.v +++ b/x86/CombineOpproof.v @@ -125,7 +125,7 @@ Theorem combine_addr_32_sound: Proof. intros. functional inversion H; subst. (* indexed - lea *) - UseGetSound. simpl. unfold offset_addressing in H7. destruct (addressing_valid (offset_addressing_total a n)); inv H7. + UseGetSound. simpl. unfold offset_addressing in H7. destruct (addressing_valid (offset_addressing_total a n)); inv H7. eapply eval_offset_addressing_total_32; eauto. Qed. @@ -136,7 +136,7 @@ Theorem combine_addr_64_sound: Proof. intros. functional inversion H; subst. (* indexed - leal *) - UseGetSound. simpl. unfold offset_addressing in H7. destruct (addressing_valid (offset_addressing_total a n)); inv H7. + UseGetSound. simpl. unfold offset_addressing in H7. destruct (addressing_valid (offset_addressing_total a n)); inv H7. eapply eval_offset_addressing_total_64; eauto. Qed. diff --git a/x86/ConstpropOp.vp b/x86/ConstpropOp.vp index 0bf143d2..759d7c16 100644 --- a/x86/ConstpropOp.vp +++ b/x86/ConstpropOp.vp @@ -46,7 +46,7 @@ Definition const_for_result (a: aval) : option operation := one if some of its arguments are statically known. These are again large pattern-matchings expressed in indirect style. *) -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 => @@ -65,7 +65,7 @@ Nondetfunction cond_strength_reduction (Ccompluimm (swap_comparison c) n1, r2 :: nil) | Ccomplu c, r1 :: r2 :: nil, v1 :: L n2 :: nil => (Ccompluimm c n2, r1 :: nil) - | _, _, _ => + | _, _, _ => (cond, args) end. @@ -350,7 +350,7 @@ Definition make_cast16signed (r: reg) (a: aval) := Definition make_cast16unsigned (r: reg) (a: aval) := if vincl a (Uns Ptop 16) then (Omove, r :: nil) else (Ocast16unsigned, 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/x86/ConstpropOpproof.v b/x86/ConstpropOpproof.v index 4f582f86..5eb46e34 100644 --- a/x86/ConstpropOpproof.v +++ b/x86/ConstpropOpproof.v @@ -85,7 +85,7 @@ Lemma eval_Olea_ptr: forall a el, eval_operation ge (Vptr sp Ptrofs.zero) (Olea_ptr a) el m = eval_addressing ge (Vptr sp Ptrofs.zero) a el. Proof. - unfold Olea_ptr, eval_addressing; intros. destruct Archi.ptr64; auto. + unfold Olea_ptr, eval_addressing; intros. destruct Archi.ptr64; auto. Qed. Lemma const_for_result_correct: @@ -112,12 +112,12 @@ Proof. exists (Genv.symbol_address ge id Ptrofs.zero); auto. * inv H2. exists (Genv.symbol_address ge id ofs); split. rewrite eval_Olea_ptr. apply eval_addressing_Aglobal. - auto. + auto. + (* stack *) inv H2. exists (Vptr sp ofs); split. - rewrite eval_Olea_ptr. rewrite eval_addressing_Ainstack. + rewrite eval_Olea_ptr. rewrite eval_addressing_Ainstack. simpl. rewrite Ptrofs.add_zero_l; auto. - auto. + auto. Qed. Lemma cond_strength_reduction_correct: @@ -152,8 +152,8 @@ Local Opaque Val.add. assert (B: forall x y z, Int.repr (Int.signed x * y + z) = Int.add (Int.mul x (Int.repr y)) (Int.repr z)). { intros; apply Int.eqm_samerepr; apply Int.eqm_add; auto with ints. unfold Int.mul; auto using Int.eqm_signed_unsigned with ints. } - intros until res; intros VL EA. - unfold addr_strength_reduction_32_generic; destruct (addr_strength_reduction_32_generic_match addr args vl); + intros until res; intros VL EA. + unfold addr_strength_reduction_32_generic; destruct (addr_strength_reduction_32_generic_match addr args vl); simpl in *; InvApproxRegs; SimplVM; try (inv EA). - econstructor; split; eauto. rewrite A, Val.add_assoc, Val.add_permut. auto. - econstructor; split; eauto. rewrite A, Val.add_assoc. auto. @@ -178,19 +178,19 @@ Proof. Val.add (Genv.symbol_address ge symb ofs) (Vint (Int.repr n))). { intros. rewrite <- A. apply Genv.shift_symbol_address_32; auto. } Local Opaque Val.add. - destruct (addr_strength_reduction_32_match addr args vl); + destruct (addr_strength_reduction_32_match addr args vl); simpl in *; InvApproxRegs; SimplVM; FuncInv; subst; rewrite ?SF. - econstructor; split; eauto. rewrite B. apply Val.add_lessdef; auto. - econstructor; split; eauto. rewrite Ptrofs.add_zero_l. Local Transparent Val.add. inv H0; auto. rewrite H2. simpl; rewrite SF, A. auto. -- econstructor; split; eauto. - unfold Ptrofs.add at 2. rewrite B. +- econstructor; split; eauto. + unfold Ptrofs.add at 2. rewrite B. fold (Ptrofs.add n1 (Ptrofs.of_int n2)). rewrite Genv.shift_symbol_address_32 by auto. rewrite ! Val.add_assoc. apply Val.add_lessdef; auto. - econstructor; split; eauto. - unfold Ptrofs.add at 2. rewrite B. + unfold Ptrofs.add at 2. rewrite B. fold (Ptrofs.add n2 (Ptrofs.of_int n1)). rewrite Genv.shift_symbol_address_32 by auto. rewrite ! Val.add_assoc. rewrite Val.add_permut. apply Val.add_lessdef; auto. @@ -203,7 +203,7 @@ Local Transparent Val.add. apply Val.lessdef_same; do 3 f_equal. auto with ptrofs. - econstructor; split; eauto. rewrite B. rewrite ! Val.add_assoc. rewrite (Val.add_commut (Vint (Int.repr ofs))). apply Val.add_lessdef; auto. -- econstructor; split; eauto. rewrite B. rewrite (Val.add_commut e#r1). rewrite ! Val.add_assoc. +- econstructor; split; eauto. rewrite B. rewrite (Val.add_commut e#r1). rewrite ! Val.add_assoc. rewrite (Val.add_commut (Vint (Int.repr ofs))). apply Val.add_lessdef; auto. - econstructor; split; eauto. rewrite B. rewrite Genv.shift_symbol_address_32 by auto. rewrite ! Val.add_assoc. apply Val.add_lessdef; auto. @@ -229,8 +229,8 @@ Local Opaque Val.addl. assert (B: forall x y z, Int64.repr (Int64.signed x * y + z) = Int64.add (Int64.mul x (Int64.repr y)) (Int64.repr z)). { intros; apply Int64.eqm_samerepr; apply Int64.eqm_add; auto with ints. unfold Int64.mul; auto using Int64.eqm_signed_unsigned with ints. } - intros until res; intros VL EA. - unfold addr_strength_reduction_64_generic; destruct (addr_strength_reduction_64_generic_match addr args vl); + intros until res; intros VL EA. + unfold addr_strength_reduction_64_generic; destruct (addr_strength_reduction_64_generic_match addr args vl); simpl in *; InvApproxRegs; SimplVM; try (inv EA). - econstructor; split; eauto. rewrite A, Val.addl_assoc, Val.addl_permut. auto. - econstructor; split; eauto. rewrite A, Val.addl_assoc. auto. @@ -256,19 +256,19 @@ Proof. Val.addl (Genv.symbol_address ge symb ofs) (Vlong (Int64.repr n))). { intros. rewrite <- A. apply Genv.shift_symbol_address_64; auto. } Local Opaque Val.addl. - destruct (addr_strength_reduction_64_match addr args vl); + destruct (addr_strength_reduction_64_match addr args vl); simpl in *; InvApproxRegs; SimplVM; FuncInv; subst; rewrite ?SF. - econstructor; split; eauto. rewrite B. apply Val.addl_lessdef; auto. - econstructor; split; eauto. rewrite Ptrofs.add_zero_l. Local Transparent Val.addl. inv H0; auto. rewrite H2. simpl; rewrite SF, A. auto. -- econstructor; split; eauto. - unfold Ptrofs.add at 2. rewrite B. +- econstructor; split; eauto. + unfold Ptrofs.add at 2. rewrite B. fold (Ptrofs.add n1 (Ptrofs.of_int64 n2)). rewrite Genv.shift_symbol_address_64 by auto. rewrite ! Val.addl_assoc. apply Val.addl_lessdef; auto. - econstructor; split; eauto. - unfold Ptrofs.add at 2. rewrite B. + unfold Ptrofs.add at 2. rewrite B. fold (Ptrofs.add n2 (Ptrofs.of_int64 n1)). rewrite Genv.shift_symbol_address_64 by auto. rewrite ! Val.addl_assoc. rewrite Val.addl_permut. apply Val.addl_lessdef; auto. @@ -350,8 +350,8 @@ Proof. intros. unfold make_addimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. exists (e#r); split; auto. - destruct (e#r); simpl; auto; rewrite ?Int.add_zero, ?Ptrofs.add_zero; auto. - exists (Val.add e#r (Vint n)); split; auto. simpl. rewrite Int.repr_signed; auto. + destruct (e#r); simpl; auto; rewrite ?Int.add_zero, ?Ptrofs.add_zero; auto. + exists (Val.add e#r (Vint n)); split; auto. simpl. rewrite Int.repr_signed; auto. Qed. Lemma make_shlimm_correct: @@ -514,7 +514,7 @@ Proof. predSpec Int64.eq Int64.eq_spec n Int64.zero; intros. subst. exists (e#r); split; auto. destruct (e#r); simpl; auto; rewrite ? Int64.add_zero, ? Ptrofs.add_zero; auto. - exists (Val.addl e#r (Vlong n)); split; auto. simpl. rewrite Int64.repr_signed; auto. + exists (Val.addl e#r (Vlong n)); split; auto. simpl. rewrite Int64.repr_signed; auto. Qed. Lemma make_shllimm_correct: @@ -606,8 +606,8 @@ Proof. econstructor; split. simpl; eauto. rewrite H0 in H. destruct (e#r1); inv H. destruct (Int64.eq n Int64.zero); inv H2. simpl. - erewrite Int64.is_power2'_range by eauto. - erewrite Int64.divu_pow2' by eauto. auto. + erewrite Int64.is_power2'_range by eauto. + erewrite Int64.divu_pow2' by eauto. auto. exists v; auto. Qed. @@ -621,7 +621,7 @@ Proof. intros; unfold make_modluimm. destruct (Int64.is_power2 n) eqn:?. exists v; split; auto. simpl. decEq. - rewrite H0 in H. destruct (e#r1); inv H. destruct (Int64.eq n Int64.zero); inv H2. + rewrite H0 in H. destruct (e#r1); inv H. destruct (Int64.eq n Int64.zero); inv H2. simpl. erewrite Int64.modu_and by eauto. auto. exists v; auto. Qed. @@ -830,7 +830,7 @@ Proof. InvApproxRegs; SimplVM; inv H0. replace (Val.subl e#r1 (Vlong n2)) with (Val.addl e#r1 (Vlong (Int64.neg n2))). apply make_addlimm_correct; auto. - unfold Val.addl, Val.subl. destruct Archi.ptr64 eqn:SF, e#r1; auto. + unfold Val.addl, Val.subl. destruct Archi.ptr64 eqn:SF, e#r1; auto. rewrite Int64.sub_add_opp; auto. rewrite Ptrofs.sub_add_opp. do 2 f_equal. auto with ptrofs. rewrite Int64.sub_add_opp; auto. diff --git a/x86/Conventions1.v b/x86/Conventions1.v index dbc8b064..ecfb85bf 100644 --- a/x86/Conventions1.v +++ b/x86/Conventions1.v @@ -63,6 +63,8 @@ Definition destroyed_at_call := Definition dummy_int_reg := AX. (**r Used in [Regalloc]. *) Definition dummy_float_reg := X0. (**r Used in [Regalloc]. *) +Definition callee_save_type := mreg_type. + Definition is_float_reg (r: mreg) := match r with | AX | BX | CX | DX | SI | DI | BP @@ -146,11 +148,11 @@ Lemma loc_result_pair: | 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 + /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true + /\ Archi.ptr64 = false end. Proof. - intros. change Archi.splitlong with (negb Archi.ptr64). + intros. unfold loc_result, loc_result_32, loc_result_64, mreg_type; destruct Archi.ptr64; destruct (sig_res sg) as [[]|]; auto. split; auto. congruence. @@ -162,7 +164,7 @@ Lemma loc_result_exten: forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2. Proof. intros. unfold loc_result, loc_result_32, loc_result_64. - destruct Archi.ptr64; rewrite H; auto. + destruct Archi.ptr64; rewrite H; auto. Qed. (** ** Location of function arguments *) @@ -310,7 +312,7 @@ Opaque list_nth_z. { intros. destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H1. subst. left. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. - subst. split. omega. assumption. + subst. split. omega. assumption. eapply Y; eauto. omega. } assert (B: forall ty, In p match list_nth_z float_param_regs fr with @@ -321,7 +323,7 @@ Opaque list_nth_z. { intros. destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H1. subst. right. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. - subst. split. omega. assumption. + subst. split. omega. assumption. eapply Y; eauto. omega. } destruct a; eauto. Qed. @@ -337,15 +339,15 @@ Proof. assert (X: forall l, loc_argument_64_charact 0 l -> loc_argument_acceptable l). { unfold loc_argument_64_charact, loc_argument_acceptable. destruct l as [r | [] ofs ty]; auto. intros [C|C]; auto. - intros [C D]. split; auto. apply Zdivide_trans with 2; auto. + intros [C D]. split; auto. apply Zdivide_trans with 2; auto. exists (2 / typealign ty); destruct ty; reflexivity. } - exploit loc_arguments_64_charact; eauto using Zdivide_0. + exploit loc_arguments_64_charact; eauto using Zdivide_0. unfold forall_rpair; destruct p; intuition auto. - (* 32 bits *) assert (X: forall l, loc_argument_32_charact 0 l -> loc_argument_acceptable l). { destruct l as [r | [] ofs ty]; simpl; intuition auto. rewrite H2; apply Z.divide_1_l. } - exploit loc_arguments_32_charact; eauto. + exploit loc_arguments_32_charact; eauto. unfold forall_rpair; destruct p; intuition auto. Qed. @@ -373,14 +375,14 @@ Proof. | Some _ => size_arguments_64 tyl (ir + 1) fr ofs0 | None => size_arguments_64 tyl ir fr (ofs0 + 2) end). - { destruct (list_nth_z int_param_regs ir); eauto. + { destruct (list_nth_z int_param_regs ir); eauto. apply Zle_trans with (ofs0 + 2); auto. omega. } assert (B: ofs0 <= match list_nth_z float_param_regs fr with | Some _ => size_arguments_64 tyl ir (fr + 1) ofs0 | None => size_arguments_64 tyl ir fr (ofs0 + 2) end). - { destruct (list_nth_z float_param_regs fr); eauto. + { destruct (list_nth_z float_param_regs fr); eauto. apply Zle_trans with (ofs0 + 2); auto. omega. } destruct a; auto. Qed. @@ -420,7 +422,7 @@ Proof. contradiction. assert (T: forall ty0, typesize ty0 <= 2). { destruct ty0; simpl; omega. } - assert (A: forall ty0, + assert (A: forall ty0, In (S Outgoing ofs ty) (regs_of_rpairs match list_nth_z int_param_regs ir with | Some ireg => @@ -435,9 +437,9 @@ Proof. { intros. destruct (list_nth_z int_param_regs ir); simpl in H0; destruct H0. - discriminate. - eapply IHtyl; eauto. - - inv H0. apply Zle_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above. + - inv H0. apply Zle_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above. - eapply IHtyl; eauto. } - assert (B: forall ty0, + assert (B: forall ty0, In (S Outgoing ofs ty) (regs_of_rpairs match list_nth_z float_param_regs fr with | Some ireg => @@ -452,7 +454,7 @@ Proof. { intros. destruct (list_nth_z float_param_regs fr); simpl in H0; destruct H0. - discriminate. - eapply IHtyl; eauto. - - inv H0. apply Zle_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above. + - inv H0. apply Zle_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above. - eapply IHtyl; eauto. } destruct a; eauto. Qed. diff --git a/x86/Machregs.v b/x86/Machregs.v index 04be0cd6..ffaf2531 100644 --- a/x86/Machregs.v +++ b/x86/Machregs.v @@ -58,7 +58,7 @@ Proof. Qed. Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. - + Instance Finite_mreg : Finite mreg := { Finite_elements := all_mregs; Finite_elements_spec := all_mregs_complete @@ -151,7 +151,7 @@ Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mre match chunk with | Mint8signed | Mint8unsigned => if Archi.ptr64 then nil else AX :: CX :: nil | _ => nil - end. + end. Definition destroyed_by_cond (cond: condition): list mreg := nil. diff --git a/x86/NeedOp.v b/x86/NeedOp.v index 09013cdd..68ecc745 100644 --- a/x86/NeedOp.v +++ b/x86/NeedOp.v @@ -225,7 +225,7 @@ Proof. - eapply needs_of_addressing_32_sound; eauto. - change (eval_addressing64 ge (Vptr sp Ptrofs.zero) a args') with (eval_operation ge (Vptr sp Ptrofs.zero) (Oleal a) args' m'). - eapply default_needs_of_operation_sound; eauto. + eapply default_needs_of_operation_sound; eauto. destruct a; simpl in H0; auto. - destruct (eval_condition cond args m) as [b|] eqn:EC; simpl in H2. erewrite needs_of_condition_sound by eauto. @@ -393,14 +393,14 @@ Remark eval_addressing_Aglobal: forall (F V: Type) (genv: Genv.t F V) sp id ofs, eval_addressing genv sp (Aglobal id ofs) nil = Some (Genv.symbol_address genv id ofs). Proof. - intros. unfold eval_addressing, eval_addressing32, eval_addressing64; destruct Archi.ptr64; auto. + intros. unfold eval_addressing, eval_addressing32, eval_addressing64; destruct Archi.ptr64; auto. Qed. Remark eval_addressing_Ainstack: forall (F V: Type) (genv: Genv.t F V) sp ofs, eval_addressing genv sp (Ainstack ofs) nil = Some (Val.offset_ptr sp ofs). Proof. - intros. unfold eval_addressing, eval_addressing32, eval_addressing64; destruct Archi.ptr64; auto. + intros. unfold eval_addressing, eval_addressing32, eval_addressing64; destruct Archi.ptr64; auto. Qed. Remark eval_addressing_Ainstack_inv: @@ -605,7 +605,7 @@ Corollary type_of_addressing_sound: eval_addressing genv sp addr vl = Some v -> Val.has_type v Tptr. Proof. - unfold eval_addressing, Tptr; intros. + unfold eval_addressing, Tptr; intros. destruct Archi.ptr64; eauto using type_of_addressing64_sound, type_of_addressing32_sound. Qed. @@ -815,7 +815,7 @@ Lemma eval_shift_stack_addressing32: eval_addressing32 ge (Vptr sp Ptrofs.zero) (shift_stack_addressing delta addr) vl = eval_addressing32 ge (Vptr sp (Ptrofs.repr delta)) addr vl. Proof. - intros. + intros. assert (A: forall i, Ptrofs.add Ptrofs.zero (Ptrofs.add i (Ptrofs.repr delta)) = Ptrofs.add (Ptrofs.repr delta) i). { intros. rewrite Ptrofs.add_zero_l. apply Ptrofs.add_commut. } destruct addr; simpl; rewrite ?A; reflexivity. @@ -826,7 +826,7 @@ Lemma eval_shift_stack_addressing64: eval_addressing64 ge (Vptr sp Ptrofs.zero) (shift_stack_addressing delta addr) vl = eval_addressing64 ge (Vptr sp (Ptrofs.repr delta)) addr vl. Proof. - intros. + intros. assert (A: forall i, Ptrofs.add Ptrofs.zero (Ptrofs.add i (Ptrofs.repr delta)) = Ptrofs.add (Ptrofs.repr delta) i). { intros. rewrite Ptrofs.add_zero_l. apply Ptrofs.add_commut. } destruct addr; simpl; rewrite ?A; reflexivity. @@ -837,7 +837,7 @@ Lemma eval_shift_stack_addressing: eval_addressing ge (Vptr sp Ptrofs.zero) (shift_stack_addressing delta addr) vl = eval_addressing ge (Vptr sp (Ptrofs.repr delta)) addr vl. Proof. - intros. unfold eval_addressing. + intros. unfold eval_addressing. destruct Archi.ptr64; auto using eval_shift_stack_addressing32, eval_shift_stack_addressing64. Qed. @@ -1234,7 +1234,7 @@ Proof. inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto. inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto. - inv H4; simpl in H1; try discriminate. simpl. destruct (Int.ltu n (Int.repr 63)); inv H1. TrivialExists. + inv H4; simpl in H1; try discriminate. simpl. destruct (Int.ltu n (Int.repr 63)); inv H1. TrivialExists. inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto. inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto. inv H4; simpl; auto. @@ -1426,7 +1426,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: @@ -1446,7 +1446,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/x86/SelectLongproof.v b/x86/SelectLongproof.v index 2262a70b..3bef632d 100644 --- a/x86/SelectLongproof.v +++ b/x86/SelectLongproof.v @@ -399,7 +399,7 @@ Theorem eval_mullimm: forall n, unary_constructor_sound (mullimm n) (fun v => Va Proof. unfold mullimm. intros; red; intros. destruct Archi.splitlong eqn:SL. - eapply SplitLongproof.eval_mullimm; eauto. + eapply SplitLongproof.eval_mullimm; eauto. predSpec Int64.eq Int64.eq_spec n Int64.zero. exists (Vlong Int64.zero); split. apply eval_longconst. destruct x; simpl; auto. subst n; rewrite Int64.mul_zero; auto. @@ -426,14 +426,14 @@ Proof. - TrivialExists. Qed. -Theorem eval_mullhu: +Theorem eval_mullhu: forall n, unary_constructor_sound (fun a => mullhu a n) (fun v => Val.mullhu v (Vlong n)). Proof. unfold mullhu; intros. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_mullhu; auto. red; intros. TrivialExists. constructor. eauto. constructor. apply eval_longconst. constructor. auto. Qed. -Theorem eval_mullhs: +Theorem eval_mullhs: forall n, unary_constructor_sound (fun a => mullhs a n) (fun v => Val.mullhs v (Vlong n)). Proof. unfold mullhs; intros. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_mullhs; auto. diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp index 2037760f..1200c3d7 100644 --- a/x86/SelectOp.vp +++ b/x86/SelectOp.vp @@ -369,14 +369,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 | Ceq, Eop (Oandimm n1) (t1 ::: Enil) => if Int.eq_dec n2 Int.zero then @@ -420,7 +420,7 @@ Definition compfs (c: comparison) (e1: expr) (e2: expr) := (** ** Integer conversions *) -Nondetfunction cast8unsigned (e: expr) := +Nondetfunction cast8unsigned (e: expr) := match e with | Eop (Ointconst n) Enil => Eop (Ointconst (Int.zero_ext 8 n)) Enil @@ -438,7 +438,7 @@ Nondetfunction cast8signed (e: expr) := Eop Ocast8signed (e ::: Enil) end. -Nondetfunction cast16unsigned (e: expr) := +Nondetfunction cast16unsigned (e: expr) := match e with | Eop (Ointconst n) Enil => Eop (Ointconst (Int.zero_ext 16 n)) Enil diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v index 1728c39d..e2e0b830 100644 --- a/x86/SelectOpproof.v +++ b/x86/SelectOpproof.v @@ -115,7 +115,7 @@ Lemma eval_Olea_ptr: forall a el m, eval_operation ge sp (Olea_ptr a) el m = eval_addressing ge sp a el. Proof. - unfold Olea_ptr, eval_addressing; intros. destruct Archi.ptr64; auto. + unfold Olea_ptr, eval_addressing; intros. destruct Archi.ptr64; auto. Qed. Theorem eval_addrsymbol: @@ -162,7 +162,7 @@ Proof. + TrivialExists; simpl. rewrite Int.add_commut. auto. + inv H0. simpl in H6. TrivialExists. simpl. erewrite eval_offset_addressing_total_32 by eauto. rewrite Int.repr_signed; auto. -+ TrivialExists. simpl. rewrite Int.repr_signed; auto. ++ TrivialExists. simpl. rewrite Int.repr_signed; auto. Qed. Theorem eval_add: binary_constructor_sound add Val.add. @@ -172,7 +172,7 @@ Proof. assert (B: forall id ofs n, Archi.ptr64 = false -> Genv.symbol_address ge id (Ptrofs.add ofs (Ptrofs.repr n)) = Val.add (Genv.symbol_address ge id ofs) (Vint (Int.repr n))). - { intros. replace (Ptrofs.repr n) with (Ptrofs.of_int (Int.repr n)) by auto with ptrofs. + { intros. replace (Ptrofs.repr n) with (Ptrofs.of_int (Int.repr n)) by auto with ptrofs. apply Genv.shift_symbol_address_32; auto. } red; intros until y. unfold add; case (add_match a b); intros; InvEval. @@ -193,7 +193,7 @@ Proof. - TrivialExists. - TrivialExists. simpl. repeat rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut. - TrivialExists. simpl. rewrite Val.add_assoc; auto. -- TrivialExists. simpl. +- TrivialExists. simpl. unfold Val.add; destruct Archi.ptr64, x, y; auto. + rewrite Int.add_zero; auto. + rewrite Int.add_zero; auto. @@ -324,7 +324,7 @@ Proof. exploit (eval_shlimm j (x :: le) (Eletvar 0) x). constructor; auto. intros [v2 [A2 B2]]. exploit eval_add. eexact A1. eexact A2. intros [v3 [A3 B3]]. exists v3; split. econstructor; eauto. - rewrite D; simpl; rewrite Int.add_zero. + rewrite D; simpl; rewrite Int.add_zero. replace (Vint (Int.add (Int.shl Int.one i) (Int.shl Int.one j))) with (Val.add (Val.shl Vone (Vint i)) (Val.shl Vone (Vint j))). rewrite Val.mul_add_distr_r. @@ -936,12 +936,12 @@ Proof. /\ eval_addressing ge sp (Aindexed 0) vl = Some v). { intros. exists (v :: nil); split. constructor; auto. constructor. auto. } unfold addressing; case (addressing_match a); intros. -- destruct (negb Archi.ptr64 && addressing_valid addr) eqn:E. -+ inv H. InvBooleans. apply negb_true_iff in H. unfold eval_addressing; rewrite H. +- destruct (negb Archi.ptr64 && addressing_valid addr) eqn:E. ++ inv H. InvBooleans. apply negb_true_iff in H. unfold eval_addressing; rewrite H. exists vl; auto. + apply D; auto. -- destruct (Archi.ptr64 && addressing_valid addr) eqn:E. -+ inv H. InvBooleans. unfold eval_addressing; rewrite H. +- destruct (Archi.ptr64 && addressing_valid addr) eqn:E. ++ inv H. InvBooleans. unfold eval_addressing; rewrite H. exists vl; auto. + apply D; auto. - apply D; auto. diff --git a/x86/Stacklayout.v b/x86/Stacklayout.v index 44fd43b2..22c68099 100644 --- a/x86/Stacklayout.v +++ b/x86/Stacklayout.v @@ -72,7 +72,7 @@ Local Opaque Z.add Z.mul sepconj range. assert (0 <= 4 * b.(bound_outgoing)) by omega. assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega). assert (olink + w <= ocs) by (unfold ocs; omega). - assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). + assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega). assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega). assert (ostkdata + bound_stack_data b <= oretaddr) by (apply align_le; omega). @@ -88,13 +88,13 @@ Local Opaque Z.add Z.mul sepconj range. rewrite sep_swap34. (* Apply range_split and range_split2 repeatedly *) unfold fe_ofs_arg. - apply range_split_2. fold olink. omega. omega. + apply range_split_2. fold olink. omega. omega. apply range_split. omega. apply range_split_2. fold ol. omega. omega. apply range_drop_right with ostkdata. omega. rewrite sep_swap. apply range_drop_left with (ostkdata + bound_stack_data b). omega. - rewrite sep_swap. + rewrite sep_swap. exact H. Qed. @@ -115,11 +115,11 @@ Proof. assert (0 <= 4 * b.(bound_outgoing)) by omega. assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega). assert (olink + w <= ocs) by (unfold ocs; omega). - assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). + assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega). assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega). assert (ostkdata + bound_stack_data b <= oretaddr) by (apply align_le; omega). - split. omega. omega. + split. omega. omega. Qed. Lemma frame_env_aligned: |