diff options
Diffstat (limited to 'x86')
| -rw-r--r-- | x86/Asm.v | 2 | ||||
| -rw-r--r-- | x86/Asmexpand.ml | 45 | ||||
| -rw-r--r-- | x86/Asmgenproof.v | 10 | ||||
| -rw-r--r-- | x86/Builtins1.v | 9 | ||||
| -rw-r--r-- | x86/CBuiltins.ml | 9 | ||||
| -rw-r--r-- | x86/ConstpropOpproof.v | 2 | ||||
| -rw-r--r-- | x86/Conventions1.v | 37 | ||||
| -rw-r--r-- | x86/NeedOp.v | 12 | ||||
| -rw-r--r-- | x86/SelectOpproof.v | 10 | ||||
| -rw-r--r-- | x86/Stacklayout.v | 56 | ||||
| -rw-r--r-- | x86/TargetPrinter.ml | 35 | ||||
| -rw-r--r-- | x86/extractionMachdep.v | 11 |
12 files changed, 133 insertions, 105 deletions
@@ -1193,7 +1193,7 @@ Ltac Equalities := split. auto. intros. destruct B; auto. subst. auto. - (* trace length *) red; intros; inv H; simpl. - omega. + lia. eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. - (* initial states *) diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml index 73efc3c5..a1c24f2d 100644 --- a/x86/Asmexpand.ml +++ b/x86/Asmexpand.ml @@ -39,11 +39,6 @@ let _16z = Z.of_sint 16 let stack_alignment () = 16 -(* Pseudo instructions for 32/64 bit compatibility *) - -let _Plea (r, addr) = - if Archi.ptr64 then Pleaq (r, addr) else Pleal (r, addr) - (* SP adjustment to allocate or free a stack frame. *) let align n a = @@ -109,6 +104,21 @@ let offset_addressing (Addrmode(base, ofs, cst)) delta = let linear_addr reg ofs = Addrmode(Some reg, None, Coq_inl ofs) let global_addr id ofs = Addrmode(None, None, Coq_inr(id, ofs)) +(* A "leaq" instruction that does not overflow *) + +let emit_leaq r addr = + match Asmgen.normalize_addrmode_64 addr with + | (addr, None) -> + emit (Pleaq (r, addr)) + | (addr, Some delta) -> + emit (Pleaq (r, addr)); + emit (Paddq_ri (r, delta)) + +(* Pseudo "lea" instruction for 32/64 bit compatibility *) + +let emit_lea r addr = + if Archi.ptr64 then emit_leaq r addr else emit (Pleal (r, addr)) + (* Translate a builtin argument into an addressing mode *) let addressing_of_builtin_arg = function @@ -150,8 +160,8 @@ let expand_builtin_memcpy_small sz al src dst = copy (addressing_of_builtin_arg src) (addressing_of_builtin_arg dst) sz let expand_builtin_memcpy_big sz al src dst = - if src <> BA (IR RSI) then emit (_Plea (RSI, addressing_of_builtin_arg src)); - if dst <> BA (IR RDI) then emit (_Plea (RDI, addressing_of_builtin_arg dst)); + if src <> BA (IR RSI) then emit_lea RSI (addressing_of_builtin_arg src); + if dst <> BA (IR RDI) then emit_lea RDI (addressing_of_builtin_arg dst); (* TODO: movsq? *) emit (Pmovl_ri (RCX,coqint_of_camlint (Int32.of_int (sz / 4)))); emit Prep_movsl; @@ -289,9 +299,9 @@ let expand_builtin_va_start_elf64 r = emit (Pmovl_mr (linear_addr r _0z, RAX)); emit (Pmovl_ri (RAX, coqint_of_camlint fp_offset)); emit (Pmovl_mr (linear_addr r _4z, RAX)); - emit (Pleaq (RAX, linear_addr RSP (Z.of_uint64 overflow_arg_area))); + emit_leaq RAX (linear_addr RSP (Z.of_uint64 overflow_arg_area)); emit (Pmovq_mr (linear_addr r _8z, RAX)); - emit (Pleaq (RAX, linear_addr RSP (Z.of_uint64 reg_save_area))); + emit_leaq RAX (linear_addr RSP (Z.of_uint64 reg_save_area)); emit (Pmovq_mr (linear_addr r _16z, RAX)) let expand_builtin_va_start_win64 r = @@ -302,7 +312,7 @@ let expand_builtin_va_start_win64 r = let ofs = Int64.(add !current_function_stacksize (mul 8L (of_int num_args))) in - emit (Pleaq (RAX, linear_addr RSP (Z.of_uint64 ofs))); + emit_leaq RAX (linear_addr RSP (Z.of_uint64 ofs)); emit (Pmovq_mr (linear_addr r _0z, RAX)) (* FMA operations *) @@ -487,9 +497,12 @@ let expand_builtin_inline name args res = (* Synchronization *) | "__builtin_membar", [], _ -> () - (* no operation *) + (* No operation *) | "__builtin_nop", [], _ -> emit Pnop + (* Optimization hint *) + | "__builtin_unreachable", [], _ -> + () (* Catch-all *) | _ -> raise (Error ("unrecognized builtin " ^ name)) @@ -500,7 +513,7 @@ let expand_builtin_inline name args res = unprototyped. *) let fixup_funcall_elf64 sg = - if sg.sig_cc.cc_vararg || sg.sig_cc.cc_unproto then begin + if sg.sig_cc.cc_vararg <> None || sg.sig_cc.cc_unproto then begin let (ir, fr, ofs) = next_arg_locations 0 0 0 sg.sig_args in emit (Pmovl_ri (RAX, coqint_of_camlint (Int32.of_int fr))) end @@ -521,7 +534,7 @@ let rec copy_fregs_to_iregs args fr ir = () let fixup_funcall_win64 sg = - if sg.sig_cc.cc_vararg then + if sg.sig_cc.cc_vararg <> None then copy_fregs_to_iregs sg.sig_args [XMM0; XMM1; XMM2; XMM3] [RCX; RDX; R8; R9] let fixup_funcall sg = @@ -549,7 +562,7 @@ let expand_instruction instr = (* Stack chaining *) let addr1 = linear_addr RSP (Z.of_uint (sz + 8)) in let addr2 = linear_addr RSP ofs_link in - emit (Pleaq (RAX,addr1)); + emit_leaq RAX addr1; emit (Pmovq_mr (addr2, RAX)); current_function_stacksize := Int64.of_int (sz + 8) end else if Archi.ptr64 then begin @@ -560,7 +573,7 @@ let expand_instruction instr = emit (Pcfi_adjust sz'); if save_regs >= 0 then begin (* Save the registers *) - emit (Pleaq (R10, linear_addr RSP (Z.of_uint save_regs))); + emit_leaq R10 (linear_addr RSP (Z.of_uint save_regs)); emit (Pcall_s (intern_string "__compcert_va_saveregs", {sig_args = []; sig_res = Tvoid; sig_cc = cc_default})) end; @@ -568,7 +581,7 @@ let expand_instruction instr = let fullsz = sz + 8 in let addr1 = linear_addr RSP (Z.of_uint fullsz) in let addr2 = linear_addr RSP ofs_link in - emit (Pleaq (RAX, addr1)); + emit_leaq RAX addr1; emit (Pmovq_mr (addr2, RAX)); current_function_stacksize := Int64.of_int fullsz end else begin diff --git a/x86/Asmgenproof.v b/x86/Asmgenproof.v index f1fd41e3..67c42b2b 100644 --- a/x86/Asmgenproof.v +++ b/x86/Asmgenproof.v @@ -67,7 +67,7 @@ Lemma transf_function_no_overflow: transf_function f = OK tf -> list_length_z (fn_code tf) <= Ptrofs.max_unsigned. Proof. intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x))); monadInv EQ0. - omega. + lia. Qed. Lemma exec_straight_exec: @@ -332,8 +332,8 @@ Proof. split. unfold goto_label. rewrite P. rewrite H1. auto. split. rewrite Pregmap.gss. constructor; auto. rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q. - auto. omega. - generalize (transf_function_no_overflow _ _ H0). omega. + auto. lia. + generalize (transf_function_no_overflow _ _ H0). lia. intros. apply Pregmap.gso; auto. Qed. @@ -852,7 +852,7 @@ Transparent destroyed_by_jumptable. econstructor; eauto. unfold nextinstr. rewrite Pregmap.gss. repeat rewrite Pregmap.gso; auto with asmgen. rewrite ATPC. simpl. constructor; eauto. - unfold fn_code. eapply code_tail_next_int. simpl in g. omega. + unfold fn_code. eapply code_tail_next_int. simpl in g. lia. constructor. apply agree_nextinstr. eapply agree_change_sp; eauto. Transparent destroyed_at_function_entry. @@ -877,7 +877,7 @@ Transparent destroyed_at_function_entry. - (* return *) inv STACKS. simpl in *. - right. split. omega. split. auto. + right. split. lia. split. auto. econstructor; eauto. rewrite ATPC; eauto. congruence. Qed. diff --git a/x86/Builtins1.v b/x86/Builtins1.v index f1d60961..e5233ff5 100644 --- a/x86/Builtins1.v +++ b/x86/Builtins1.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/x86/CBuiltins.ml b/x86/CBuiltins.ml index a16f3ef7..a549cd25 100644 --- a/x86/CBuiltins.ml +++ b/x86/CBuiltins.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) diff --git a/x86/ConstpropOpproof.v b/x86/ConstpropOpproof.v index 82179fa4..09c6e91b 100644 --- a/x86/ConstpropOpproof.v +++ b/x86/ConstpropOpproof.v @@ -532,7 +532,7 @@ Proof. Int.bit_solve. destruct (zlt i0 n0). replace (Int.testbit n i0) with (negb (Int.testbit Int.zero i0)). rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto. - rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto. + rewrite <- EQ. rewrite Int.bits_zero_ext by lia. rewrite zlt_true by auto. rewrite Int.bits_not by auto. apply negb_involutive. rewrite H6 by auto. auto. econstructor; split; eauto. auto. diff --git a/x86/Conventions1.v b/x86/Conventions1.v index 645aae90..a4e3b970 100644 --- a/x86/Conventions1.v +++ b/x86/Conventions1.v @@ -302,14 +302,14 @@ Remark loc_arguments_32_charact: In p (loc_arguments_32 tyl ofs) -> forall_rpair (loc_argument_32_charact ofs) p. Proof. assert (X: forall ofs1 ofs2 l, loc_argument_32_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_32_charact ofs1 l). - { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. } + { destruct l; simpl; intros; auto. destruct sl; auto. intuition lia. } induction tyl as [ | ty tyl]; simpl loc_arguments_32; intros. - contradiction. - destruct H. -+ destruct ty; subst p; simpl; omega. ++ destruct ty; subst p; simpl; lia. + apply IHtyl in H. generalize (typesize_pos ty); intros. destruct p; simpl in *. -* eapply X; eauto; omega. -* destruct H; split; eapply X; eauto; omega. +* eapply X; eauto; lia. +* destruct H; split; eapply X; eauto; lia. Qed. Remark loc_arguments_elf64_charact: @@ -317,7 +317,7 @@ Remark loc_arguments_elf64_charact: In p (loc_arguments_elf64 tyl ir fr ofs) -> (2 | ofs) -> forall_rpair (loc_argument_elf64_charact ofs) p. Proof. assert (X: forall ofs1 ofs2 l, loc_argument_elf64_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_elf64_charact ofs1 l). - { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. } + { destruct l; simpl; intros; auto. destruct sl; auto. intuition lia. } assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_elf64_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_elf64_charact ofs1) p). { destruct p; simpl; intuition eauto. } assert (Z: forall ofs, (2 | ofs) -> (2 | ofs + 2)). @@ -334,8 +334,8 @@ Opaque list_nth_z. { intros. destruct (list_nth_z int_param_regs_elf64 ir) as [r|] eqn:E; destruct H1. subst. left. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. - subst. split. omega. assumption. - eapply Y; eauto. omega. } + subst. split. lia. assumption. + eapply Y; eauto. lia. } assert (B: forall ty, In p match list_nth_z float_param_regs_elf64 fr with | Some ireg => One (R ireg) :: loc_arguments_elf64 tyl ir (fr + 1) ofs @@ -345,8 +345,8 @@ Opaque list_nth_z. { intros. destruct (list_nth_z float_param_regs_elf64 fr) as [r|] eqn:E; destruct H1. subst. right. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. - subst. split. omega. assumption. - eapply Y; eauto. omega. } + subst. split. lia. assumption. + eapply Y; eauto. lia. } destruct a; eauto. Qed. @@ -355,7 +355,7 @@ Remark loc_arguments_win64_charact: In p (loc_arguments_win64 tyl r ofs) -> (2 | ofs) -> forall_rpair (loc_argument_win64_charact ofs) p. Proof. assert (X: forall ofs1 ofs2 l, loc_argument_win64_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_win64_charact ofs1 l). - { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. } + { destruct l; simpl; intros; auto. destruct sl; auto. intuition lia. } assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_win64_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_win64_charact ofs1) p). { destruct p; simpl; intuition eauto. } assert (Z: forall ofs, (2 | ofs) -> (2 | ofs + 2)). @@ -372,8 +372,8 @@ Opaque list_nth_z. { intros. destruct (list_nth_z int_param_regs_win64 r) as [r'|] eqn:E; destruct H1. subst. left. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. - subst. split. omega. assumption. - eapply Y; eauto. omega. } + subst. split. lia. assumption. + eapply Y; eauto. lia. } assert (B: forall ty, In p match list_nth_z float_param_regs_win64 r with | Some ireg => One (R ireg) :: loc_arguments_win64 tyl (r + 1) ofs @@ -383,8 +383,8 @@ Opaque list_nth_z. { intros. destruct (list_nth_z float_param_regs_win64 r) as [r'|] eqn:E; destruct H1. subst. right. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. - subst. split. omega. assumption. - eapply Y; eauto. omega. } + subst. split. lia. assumption. + eapply Y; eauto. lia. } destruct a; eauto. Qed. @@ -423,7 +423,7 @@ Proof. unfold forall_rpair; destruct p; intuition auto. Qed. -Hint Resolve loc_arguments_acceptable: locs. +Global Hint Resolve loc_arguments_acceptable: locs. Lemma loc_arguments_main: loc_arguments signature_main = nil. @@ -431,7 +431,7 @@ Proof. unfold loc_arguments; destruct Archi.ptr64; auto; destruct Archi.win64; auto. Qed. -(** ** Normalization of function results *) +(** ** Normalization of function results and parameters *) (** In the x86 ABI, a return value of type "char" is returned in register AL, leaving the top 24 bits of EAX unspecified. @@ -444,3 +444,8 @@ Definition return_value_needs_normalization (t: rettype) : bool := | Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => true | _ => false end. + +(** Function parameters are passed in normalized form and do not need + to be re-normalized at function entry. *) + +Definition parameter_needs_normalization (t: rettype) := false. diff --git a/x86/NeedOp.v b/x86/NeedOp.v index d9a58fbb..775a23db 100644 --- a/x86/NeedOp.v +++ b/x86/NeedOp.v @@ -206,9 +206,9 @@ Proof. unfold needs_of_operation; intros; destruct op; try (eapply default_needs_of_operation_sound; eauto; fail); simpl in *; FuncInv; InvAgree; TrivialExists. - apply sign_ext_sound; auto. compute; auto. -- apply zero_ext_sound; auto. omega. +- apply zero_ext_sound; auto. lia. - apply sign_ext_sound; auto. compute; auto. -- apply zero_ext_sound; auto. omega. +- apply zero_ext_sound; auto. lia. - apply neg_sound; auto. - apply mul_sound; auto. - apply mul_sound; auto with na. @@ -246,10 +246,10 @@ Lemma operation_is_redundant_sound: vagree v arg1' nv. Proof. intros. destruct op; simpl in *; try discriminate; inv H1; FuncInv; subst. -- apply sign_ext_redundant_sound; auto. omega. -- apply zero_ext_redundant_sound; auto. omega. -- apply sign_ext_redundant_sound; auto. omega. -- apply zero_ext_redundant_sound; auto. omega. +- apply sign_ext_redundant_sound; auto. lia. +- apply zero_ext_redundant_sound; auto. lia. +- apply sign_ext_redundant_sound; auto. lia. +- apply zero_ext_redundant_sound; auto. lia. - apply andimm_redundant_sound; auto. - apply orimm_redundant_sound; auto. Qed. diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v index 961f602c..d8ab32a4 100644 --- a/x86/SelectOpproof.v +++ b/x86/SelectOpproof.v @@ -381,9 +381,9 @@ Proof. - TrivialExists. simpl. rewrite Int.and_commut; auto. - TrivialExists. simpl. rewrite Val.and_assoc. rewrite Int.and_commut. auto. - rewrite Val.zero_ext_and. TrivialExists. rewrite Val.and_assoc. - rewrite Int.and_commut. auto. omega. + rewrite Int.and_commut. auto. lia. - rewrite Val.zero_ext_and. TrivialExists. rewrite Val.and_assoc. - rewrite Int.and_commut. auto. omega. + rewrite Int.and_commut. auto. lia. - TrivialExists. Qed. @@ -743,7 +743,7 @@ Proof. red; intros until x. unfold cast8unsigned. destruct (cast8unsigned_match a); intros; InvEval. TrivialExists. subst. rewrite Val.zero_ext_and. rewrite Val.and_assoc. - rewrite Int.and_commut. apply eval_andimm; auto. omega. + rewrite Int.and_commut. apply eval_andimm; auto. lia. TrivialExists. Qed. @@ -759,7 +759,7 @@ Proof. red; intros until x. unfold cast16unsigned. destruct (cast16unsigned_match a); intros; InvEval. TrivialExists. subst. rewrite Val.zero_ext_and. rewrite Val.and_assoc. - rewrite Int.and_commut. apply eval_andimm; auto. omega. + rewrite Int.and_commut. apply eval_andimm; auto. lia. TrivialExists. Qed. @@ -860,7 +860,7 @@ Proof. simpl. rewrite Heqo; reflexivity. simpl. unfold Int64.loword. rewrite Int64.unsigned_repr, Int.repr_unsigned; auto. assert (Int.modulus < Int64.max_unsigned) by reflexivity. - generalize (Int.unsigned_range n); omega. + generalize (Int.unsigned_range n); lia. Qed. Theorem eval_floatofintu: diff --git a/x86/Stacklayout.v b/x86/Stacklayout.v index 4f68cf26..002b86bf 100644 --- a/x86/Stacklayout.v +++ b/x86/Stacklayout.v @@ -69,16 +69,16 @@ Local Opaque Z.add Z.mul sepconj range. set (ostkdata := align (ol + 4 * b.(bound_local)) 8). set (oretaddr := align (ostkdata + b.(bound_stack_data)) w). replace (size_chunk Mptr) with w by (rewrite size_chunk_Mptr; auto). - assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). + assert (0 < w) by (unfold w; destruct Archi.ptr64; lia). generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. - assert (0 <= fe_ofs_arg) by (unfold fe_ofs_arg; destruct Archi.win64; omega). - assert (0 <= 4 * b.(bound_outgoing)) by omega. - assert (fe_ofs_arg + 4 * b.(bound_outgoing) <= olink) by (apply align_le; omega). - assert (olink + w <= ocs) by (unfold ocs; omega). + assert (0 <= fe_ofs_arg) by (unfold fe_ofs_arg; destruct Archi.win64; lia). + assert (0 <= 4 * b.(bound_outgoing)) by lia. + assert (fe_ofs_arg + 4 * b.(bound_outgoing) <= olink) by (apply align_le; lia). + assert (olink + w <= ocs) by (unfold ocs; lia). 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). + assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia). + assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; lia). + assert (ostkdata + bound_stack_data b <= oretaddr) by (apply align_le; lia). (* Reorder as: outgoing back link @@ -90,13 +90,13 @@ Local Opaque Z.add Z.mul sepconj range. rewrite sep_swap45. rewrite sep_swap34. (* Apply range_split and range_split2 repeatedly *) - apply range_drop_left with 0. 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. + apply range_drop_left with 0. lia. + apply range_split_2. fold olink. lia. lia. + apply range_split. lia. + apply range_split_2. fold ol. lia. lia. + apply range_drop_right with ostkdata. lia. rewrite sep_swap. - apply range_drop_left with (ostkdata + bound_stack_data b). omega. + apply range_drop_left with (ostkdata + bound_stack_data b). lia. rewrite sep_swap. exact H. Qed. @@ -113,17 +113,17 @@ Proof. set (ol := align (size_callee_save_area b ocs) 8). set (ostkdata := align (ol + 4 * b.(bound_local)) 8). set (oretaddr := align (ostkdata + b.(bound_stack_data)) w). - assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). + assert (0 < w) by (unfold w; destruct Archi.ptr64; lia). generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. - assert (0 <= fe_ofs_arg) by (unfold fe_ofs_arg; destruct Archi.win64; omega). - assert (0 <= 4 * b.(bound_outgoing)) by omega. - assert (fe_ofs_arg + 4 * b.(bound_outgoing) <= olink) by (apply align_le; omega). - assert (olink + w <= ocs) by (unfold ocs; omega). + assert (0 <= fe_ofs_arg) by (unfold fe_ofs_arg; destruct Archi.win64; lia). + assert (0 <= 4 * b.(bound_outgoing)) by lia. + assert (fe_ofs_arg + 4 * b.(bound_outgoing) <= olink) by (apply align_le; lia). + assert (olink + w <= ocs) by (unfold ocs; lia). 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. + assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia). + assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; lia). + assert (ostkdata + bound_stack_data b <= oretaddr) by (apply align_le; lia). + split. lia. lia. Qed. Lemma frame_env_aligned: @@ -142,11 +142,11 @@ Proof. set (ol := align (size_callee_save_area b ocs) 8). set (ostkdata := align (ol + 4 * b.(bound_local)) 8). set (oretaddr := align (ostkdata + b.(bound_stack_data)) w). - assert (0 < w) by (unfold w; destruct Archi.ptr64; omega). + assert (0 < w) by (unfold w; destruct Archi.ptr64; lia). replace (align_chunk Mptr) with w by (rewrite align_chunk_Mptr; auto). split. exists (fe_ofs_arg / 8). unfold fe_ofs_arg; destruct Archi.win64; reflexivity. - split. apply align_divides; omega. - split. apply align_divides; omega. - split. apply align_divides; omega. - apply align_divides; omega. + split. apply align_divides; lia. + split. apply align_divides; lia. + split. apply align_divides; lia. + apply align_divides; lia. Qed. diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml index 481b09b9..5bc2be1c 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -95,9 +95,6 @@ let z oc n = output_string oc (Z.to_string n) let data_pointer = if Archi.ptr64 then ".quad" else ".long" -(* The comment deliminiter *) -let comment = "#" - (* Base-2 log of a Caml integer *) let rec log2 n = assert (n > 0); @@ -106,6 +103,7 @@ let rec log2 n = (* System dependent printer functions *) module type SYSTEM = sig + val comment: string val raw_symbol: out_channel -> string -> unit val symbol: out_channel -> P.t -> unit val label: out_channel -> int -> unit @@ -124,6 +122,9 @@ module type SYSTEM = module ELF_System : SYSTEM = struct + (* The comment delimiter *) + let comment = "#" + let raw_symbol oc s = fprintf oc "%s" s @@ -134,9 +135,9 @@ module ELF_System : SYSTEM = let name_of_section = function | Section_text -> ".text" | Section_data i | Section_small_data i -> - if i then ".data" else common_section () + variable_section ~sec:".data" ~bss:".bss" i | Section_const i | Section_small_const i -> - if i || (not !Clflags.option_fcommon) then ".section .rodata" else "COMM" + variable_section ~sec:".section .rodata" i | Section_string -> ".section .rodata" | Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8" | Section_jumptable -> ".text" @@ -180,6 +181,10 @@ module ELF_System : SYSTEM = module MacOS_System : SYSTEM = struct + (* The comment delimiter. + `##` instead of `#` to please the Clang assembler. *) + let comment = "##" + let raw_symbol oc s = fprintf oc "_%s" s @@ -192,11 +197,11 @@ module MacOS_System : SYSTEM = let name_of_section = function | Section_text -> ".text" | Section_data i | Section_small_data i -> - if i || (not !Clflags.option_fcommon) then ".data" else "COMM" + variable_section ~sec:".data" i | Section_const i | Section_small_const i -> - if i || (not !Clflags.option_fcommon) then ".const" else "COMM" + variable_section ~sec:".const" ~reloc:".const_data" i | Section_string -> ".const" - | Section_literal -> ".literal8" + | Section_literal -> ".const" | Section_jumptable -> ".text" | Section_user(s, wr, ex) -> sprintf ".section \"%s\", %s, %s" @@ -239,6 +244,9 @@ module MacOS_System : SYSTEM = module Cygwin_System : SYSTEM = struct + (* The comment delimiter *) + let comment = "#" + let symbol_prefix = if Archi.ptr64 then "" else "_" @@ -254,9 +262,9 @@ module Cygwin_System : SYSTEM = let name_of_section = function | Section_text -> ".text" | Section_data i | Section_small_data i -> - if i then ".data" else common_section () + variable_section ~sec:".data" ~bss:".bss" i | Section_const i | Section_small_const i -> - if i || (not !Clflags.option_fcommon) then ".section .rdata,\"dr\"" else "COMM" + variable_section ~sec:".section .rdata,\"dr\"" i | Section_string -> ".section .rdata,\"dr\"" | Section_literal -> ".section .rdata,\"dr\"" | Section_jumptable -> ".text" @@ -733,7 +741,7 @@ module Target(System: SYSTEM):TARGET = | Pret -> if (not Archi.ptr64) && (!current_function_sig).sig_cc.cc_structret then begin - fprintf oc " movl 0(%%esp), %%eax\n"; + fprintf oc " movl 4(%%esp), %%eax\n"; fprintf oc " ret $4\n" end else begin fprintf oc " ret\n" @@ -914,8 +922,7 @@ module Target(System: SYSTEM):TARGET = let print_epilogue oc = if !need_masks then begin - section oc (Section_const true); - (* not Section_literal because not 8-bytes *) + section oc Section_literal; print_align oc 16; fprintf oc "%a: .quad 0x8000000000000000, 0\n" raw_symbol "__negd_mask"; @@ -945,7 +952,7 @@ end let sel_target () = let module S = (val (match Configuration.system with | "linux" | "bsd" -> (module ELF_System:SYSTEM) - | "macosx" -> (module MacOS_System:SYSTEM) + | "macos" -> (module MacOS_System:SYSTEM) | "cygwin" -> (module Cygwin_System:SYSTEM) | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported") ):SYSTEM) in (module Target(S):TARGET) diff --git a/x86/extractionMachdep.v b/x86/extractionMachdep.v index 20c6a521..26a3f0a7 100644 --- a/x86/extractionMachdep.v +++ b/x86/extractionMachdep.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -28,6 +29,6 @@ Extract Constant Archi.win64 => Extract Constant SelectOp.symbol_is_external => "match Configuration.system with - | ""macosx"" -> C2C.atom_is_extern + | ""macos"" -> C2C.atom_is_extern | ""cygwin"" when Archi.ptr64 -> C2C.atom_is_extern | _ -> (fun _ -> false)". |