diff options
Diffstat (limited to 'verilog')
| -rw-r--r-- | verilog/Asm.v | 2 | ||||
| -rw-r--r-- | verilog/Asmexpand.ml | 99 | ||||
| -rw-r--r-- | verilog/Asmgenproof.v | 10 | ||||
| -rw-r--r-- | verilog/ConstpropOpproof.v | 2 | ||||
| -rw-r--r-- | verilog/Conventions1.v | 23 | ||||
| -rw-r--r-- | verilog/NeedOp.v | 12 | ||||
| -rw-r--r-- | verilog/SelectOpproof.v | 10 | ||||
| -rw-r--r-- | verilog/Stacklayout.v | 50 | ||||
| -rw-r--r-- | verilog/TargetPrinter.ml | 80 |
9 files changed, 134 insertions, 154 deletions
diff --git a/verilog/Asm.v b/verilog/Asm.v index 58e28c40..64ae1c32 100644 --- a/verilog/Asm.v +++ b/verilog/Asm.v @@ -1191,7 +1191,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/verilog/Asmexpand.ml b/verilog/Asmexpand.ml index caa9775a..1b3961e0 100644 --- a/verilog/Asmexpand.ml +++ b/verilog/Asmexpand.ml @@ -39,12 +39,7 @@ 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 *) +(* SP adjustment to allocate or free a stack frame. *) let align n a = if n >= 0 then (n + a - 1) land (-a) else n land (-a) @@ -56,7 +51,7 @@ let sp_adjustment_32 sz = (* The top 4 bytes have already been allocated by the "call" instruction. *) sz - 4 -let sp_adjustment_64 sz = +let sp_adjustment_elf64 sz = let sz = Z.to_int sz in if is_current_function_variadic() then begin (* If variadic, add room for register save area, which must be 16-aligned *) @@ -73,6 +68,13 @@ let sp_adjustment_64 sz = (sz - 8, -1) end +let sp_adjustment_win64 sz = + let sz = Z.to_int sz in + (* Preserve proper alignment of the stack *) + let sz = align sz 16 in + (* The top 8 bytes have already been allocated by the "call" instruction. *) + sz - 8 + (* Built-ins. They come in two flavors: - annotation statements: take their arguments in registers or stack locations; generate no code; @@ -102,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 @@ -143,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; @@ -256,7 +273,7 @@ let expand_builtin_va_start_32 r = emit (Pleal (RAX, linear_addr RSP (Z.of_uint32 ofs))); emit (Pmovl_mr (linear_addr r _0z, RAX)) -let expand_builtin_va_start_64 r = +let expand_builtin_va_start_elf64 r = if not (is_current_function_variadic ()) then invalid_arg "Fatal error: va_start used in non-vararg function"; let (ir, fr, ofs) = @@ -282,11 +299,22 @@ let expand_builtin_va_start_64 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 = + if not (is_current_function_variadic ()) then + invalid_arg "Fatal error: va_start used in non-vararg function"; + let num_args = + List.length (get_current_function_args()) in + let ofs = + Int64.(add !current_function_stacksize + (mul 8L (of_int num_args))) in + emit_leaq RAX (linear_addr RSP (Z.of_uint64 ofs)); + emit (Pmovq_mr (linear_addr r _0z, RAX)) + (* FMA operations *) (* vfmadd<i><j><k> r1, r2, r3 performs r1 := ri * rj + rk @@ -463,44 +491,63 @@ let expand_builtin_inline name args res = (* Vararg stuff *) | "__builtin_va_start", [BA(IR a)], _ -> assert (a = RDX); - if Archi.ptr64 - then expand_builtin_va_start_64 a + if Archi.ptr64 then expand_builtin_va_start_elf64 a else expand_builtin_va_start_32 a (* Synchronization *) | "__builtin_membar", [], _ -> () - (* no operation *) + (* No operation *) | "__builtin_nop", [], _ -> emit Pnop + (* Optimization hint *) + | "__builtin_unreachable", [], _ -> + () (* Catch-all *) | _ -> raise (Error ("unrecognized builtin " ^ name)) -(* Calls to variadic functions for x86-64: register AL must contain +(* Calls to variadic functions for x86-64 ELF: register AL must contain the number of XMM registers used for parameter passing. To be on - the safe side. do the same if the called function is + the safe side, do the same if the called function is unprototyped. *) -let set_al sg = - if Archi.ptr64 && (sg.sig_cc.cc_vararg || sg.sig_cc.cc_unproto) then begin +let fixup_funcall_elf64 sg = + 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 +(* Calls to variadic functions for x86-64 Windows: + FP arguments passed in FP registers must also be passed in integer + registers. +*) + +let copy_fregs_to_iregs args fr ir = + () + +let fixup_funcall_win64 sg = + 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 = + if Archi.ptr64 then + fixup_funcall_elf64 sg + else () + (* Expansion of instructions *) let expand_instruction instr = match instr with | Pallocframe (sz, ofs_ra, ofs_link) -> - if Archi.ptr64 then begin - let (sz, save_regs) = sp_adjustment_64 sz in + if Archi.ptr64 then begin + let (sz, save_regs) = sp_adjustment_elf64 sz in (* Allocate frame *) let sz' = Z.of_uint sz in emit (Psubq_ri (RSP, sz')); 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; @@ -508,7 +555,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 @@ -525,15 +572,15 @@ let expand_instruction instr = PrintAsmaux.current_function_stacksize := Int32.of_int sz end | Pfreeframe(sz, ofs_ra, ofs_link) -> - if Archi.ptr64 then begin - let (sz, _) = sp_adjustment_64 sz in + if Archi.ptr64 then begin + let (sz, _) = sp_adjustment_elf64 sz in emit (Paddq_ri (RSP, Z.of_uint sz)) end else begin let sz = sp_adjustment_32 sz in emit (Paddl_ri (RSP, Z.of_uint sz)) end | Pjmp_s(_, sg) | Pjmp_r(_, sg) | Pcall_s(_, sg) | Pcall_r(_, sg) -> - set_al sg; + fixup_funcall sg; emit instr | Pbuiltin (ef,args, res) -> begin diff --git a/verilog/Asmgenproof.v b/verilog/Asmgenproof.v index f1fd41e3..67c42b2b 100644 --- a/verilog/Asmgenproof.v +++ b/verilog/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/verilog/ConstpropOpproof.v b/verilog/ConstpropOpproof.v index 6d2df9c1..c0bdaa76 100644 --- a/verilog/ConstpropOpproof.v +++ b/verilog/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/verilog/Conventions1.v b/verilog/Conventions1.v index fdd94239..592acd72 100644 --- a/verilog/Conventions1.v +++ b/verilog/Conventions1.v @@ -248,14 +248,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_64_charact: @@ -263,7 +263,7 @@ Remark loc_arguments_64_charact: In p (loc_arguments_64 tyl ir fr ofs) -> (2 | ofs) -> forall_rpair (loc_argument_64_charact ofs) p. Proof. assert (X: forall ofs1 ofs2 l, loc_argument_64_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_64_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_64_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_64_charact ofs1) p). { destruct p; simpl; intuition eauto. } assert (Z: forall ofs, (2 | ofs) -> (2 | ofs + 2)). @@ -280,8 +280,8 @@ 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. - 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 fr with | Some ireg => One (R ireg) :: loc_arguments_64 tyl ir (fr + 1) ofs @@ -291,8 +291,8 @@ 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. - eapply Y; eauto. omega. } + subst. split. lia. assumption. + eapply Y; eauto. lia. } destruct a; eauto. Qed. @@ -340,3 +340,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/verilog/NeedOp.v b/verilog/NeedOp.v index d9a58fbb..775a23db 100644 --- a/verilog/NeedOp.v +++ b/verilog/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/verilog/SelectOpproof.v b/verilog/SelectOpproof.v index 961f602c..d8ab32a4 100644 --- a/verilog/SelectOpproof.v +++ b/verilog/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/verilog/Stacklayout.v b/verilog/Stacklayout.v index d375febf..de2a6f10 100644 --- a/verilog/Stacklayout.v +++ b/verilog/Stacklayout.v @@ -67,15 +67,15 @@ 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 <= 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 (0 <= 4 * b.(bound_outgoing)) by lia. + assert (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 @@ -88,12 +88,12 @@ 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. omega. - apply range_split_2. fold ol. omega. omega. - apply range_drop_right with ostkdata. omega. + 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. @@ -110,16 +110,16 @@ 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 <= 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 (0 <= 4 * b.(bound_outgoing)) by lia. + assert (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: @@ -138,11 +138,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. apply Z.divide_0_r. - 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/verilog/TargetPrinter.ml b/verilog/TargetPrinter.ml index f0a54506..8950b8ca 100644 --- a/verilog/TargetPrinter.ml +++ b/verilog/TargetPrinter.ml @@ -131,25 +131,7 @@ module ELF_System : SYSTEM = let label = elf_label - let name_of_section = function - | Section_text -> ".text" - | Section_data i | Section_small_data i -> - if i then ".data" else common_section () - | Section_const i | Section_small_const i -> - if i || (not !Clflags.option_fcommon) then ".section .rodata" else "COMM" - | Section_string -> ".section .rodata" - | Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8" - | Section_jumptable -> ".text" - | Section_user(s, wr, ex) -> - sprintf ".section \"%s\",\"a%s%s\",@progbits" - s (if wr then "w" else "") (if ex then "x" else "") - | Section_debug_info _ -> ".section .debug_info,\"\",@progbits" - | Section_debug_loc -> ".section .debug_loc,\"\",@progbits" - | Section_debug_line _ -> ".section .debug_line,\"\",@progbits" - | Section_debug_abbrev -> ".section .debug_abbrev,\"\",@progbits" - | Section_debug_ranges -> ".section .debug_ranges,\"\",@progbits" - | Section_debug_str -> ".section .debug_str,\"MS\",@progbits,1" - | Section_ais_annotation -> sprintf ".section \"__compcert_ais_annotations\",\"\",@note" + let name_of_section = fun _ -> assert false let stack_alignment = 16 @@ -189,26 +171,7 @@ module MacOS_System : SYSTEM = let label oc lbl = fprintf oc "L%d" lbl - 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" - | Section_const i | Section_small_const i -> - if i || (not !Clflags.option_fcommon) then ".const" else "COMM" - | Section_string -> ".const" - | Section_literal -> ".literal8" - | Section_jumptable -> ".text" - | Section_user(s, wr, ex) -> - sprintf ".section \"%s\", %s, %s" - (if wr then "__DATA" else "__TEXT") s - (if ex then "regular, pure_instructions" else "regular") - | Section_debug_info _ -> ".section __DWARF,__debug_info,regular,debug" - | Section_debug_loc -> ".section __DWARF,__debug_loc,regular,debug" - | Section_debug_line _ -> ".section __DWARF,__debug_line,regular,debug" - | Section_debug_str -> ".section __DWARF,__debug_str,regular,debug" - | Section_debug_ranges -> ".section __DWARF,__debug_ranges,regular,debug" - | Section_debug_abbrev -> ".section __DWARF,__debug_abbrev,regular,debug" - | Section_ais_annotation -> assert false (* Not supported under MacOS *) + let name_of_section = fun _ -> assert false let stack_alignment = 16 (* mandatory *) @@ -248,25 +211,7 @@ module Cygwin_System : SYSTEM = let label oc lbl = fprintf oc "L%d" lbl - let name_of_section = function - | Section_text -> ".text" - | Section_data i | Section_small_data i -> - if i then ".data" else common_section () - | Section_const i | Section_small_const i -> - if i || (not !Clflags.option_fcommon) then ".section .rdata,\"dr\"" else "COMM" - | Section_string -> ".section .rdata,\"dr\"" - | Section_literal -> ".section .rdata,\"dr\"" - | Section_jumptable -> ".text" - | Section_user(s, wr, ex) -> - sprintf ".section %s, \"%s\"\n" - s (if ex then "xr" else if wr then "d" else "dr") - | Section_debug_info _ -> ".section .debug_info,\"dr\"" - | Section_debug_loc -> ".section .debug_loc,\"dr\"" - | Section_debug_line _ -> ".section .debug_line,\"dr\"" - | Section_debug_abbrev -> ".section .debug_abbrev,\"dr\"" - | Section_debug_ranges -> ".section .debug_ranges,\"dr\"" - | Section_debug_str-> assert false (* Should not be used *) - | Section_ais_annotation -> assert false (* Not supported for coff binaries *) + let name_of_section = fun _ -> assert false let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) @@ -887,24 +832,7 @@ module Target(System: SYSTEM):TARGET = end let print_epilogue oc = - if !need_masks then begin - section oc (Section_const true); - (* not Section_literal because not 8-bytes *) - print_align oc 16; - fprintf oc "%a: .quad 0x8000000000000000, 0\n" - raw_symbol "__negd_mask"; - fprintf oc "%a: .quad 0x7FFFFFFFFFFFFFFF, 0xFFFFFFFFFFFFFFFF\n" - raw_symbol "__absd_mask"; - fprintf oc "%a: .long 0x80000000, 0, 0, 0\n" - raw_symbol "__negs_mask"; - fprintf oc "%a: .long 0x7FFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF\n" - raw_symbol "__abss_mask" - end; - System.print_epilogue oc; - if !Clflags.option_g then begin - Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f)); - section oc Section_text; - end + assert false let comment = comment |