From 378ac3925503e6efd24cc34796e85d95c031e72d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 13 Sep 2015 11:44:32 +0200 Subject: Use PowerPC 64 bits instructions (when available) for int<->FP conversions. Also: implement __builtin_isel on non-EREF platforms with a branch-free instruction sequence. Also: extend ./configure so that it recognizes "ppc64-" and "e5500-" platforms in addition to "ppc-". --- powerpc/TargetPrinter.ml | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'powerpc/TargetPrinter.ml') diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index eca7a1b8..bc990de5 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -484,6 +484,8 @@ module Target (System : SYSTEM):TARGET = fprintf oc " extsb %a, %a\n" ireg r1 ireg r2 | Pextsh(r1, r2) -> fprintf oc " extsh %a, %a\n" ireg r1 ireg r2 + | Pextsw(r1, r2) -> + fprintf oc " extsw %a, %a\n" ireg r1 ireg r2 | Pfreeframe(sz, ofs) -> assert false | Pfabs(r1, r2) | Pfabss(r1, r2) -> @@ -494,8 +496,18 @@ module Target (System : SYSTEM):TARGET = fprintf oc " fadds %a, %a, %a\n" freg r1 freg r2 freg r3 | Pfcmpu(r1, r2) -> fprintf oc " fcmpu %a, %a, %a\n" creg 0 freg r1 freg r2 + | Pfcfi(r1, r2) -> + assert false + | Pfcfid(r1, r2) -> + fprintf oc " fcfid %a, %a\n" freg r1 freg r2 + | Pfcfiu(r1, r2) -> + assert false | Pfcti(r1, r2) -> assert false + | Pfctidz(r1, r2) -> + fprintf oc " fctidz %a, %a\n" freg r1 freg r2 + | Pfctiu(r1, r2) -> + assert false | Pfctiw(r1, r2) -> fprintf oc " fctiw %a, %a\n" freg r1 freg r2 | Pfctiwz(r1, r2) -> @@ -628,6 +640,9 @@ module Target (System : SYSTEM):TARGET = fprintf oc " ori %a, %a, %a\n" ireg r1 ireg r2 constant c | Poris(r1, r2, c) -> fprintf oc " oris %a, %a, %a\n" ireg r1 ireg r2 constant c + | Prldicl(r1, r2, c1, c2) -> + fprintf oc " rldicl %a, %a, %ld, %ld\n" + ireg r1 ireg r2 (camlint_of_coqint c1) (camlint_of_coqint c2) | Prlwinm(r1, r2, c1, c2) -> let (mb, me) = rolm_mask (camlint_of_coqint c2) in fprintf oc " rlwinm %a, %a, %ld, %d, %d %s 0x%lx\n" @@ -650,6 +665,8 @@ module Target (System : SYSTEM):TARGET = fprintf oc " stb %a, %a(%a)\n" ireg r1 constant c ireg r2 | Pstbx(r1, r2, r3) -> fprintf oc " stbx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pstdu(r1, c, r2) -> + fprintf oc " stdu %a, %a(%a)\n" ireg r1 constant c ireg r2 | Pstfd(r1, c, r2) | Pstfd_a(r1, c, r2) -> fprintf oc " stfd %a, %a(%a)\n" freg r1 constant c ireg r2 | Pstfdu(r1, c, r2) -> -- cgit From 16315711d815580afa77f93424cc49c7362ab5b8 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 13 Oct 2015 14:57:31 +0200 Subject: Implement the usage of the debug_str section for the gcc backend. GCC prints all string larger than 3 characters in the debug_str section which reduces the size of the debug information since entries containing the same string now map to the same string in the debug_str sections. Bug 17392. --- powerpc/TargetPrinter.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'powerpc/TargetPrinter.ml') diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 250686be..61ac5e42 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -126,7 +126,8 @@ module Linux_System : SYSTEM = | Section_debug_info _ -> ".section .debug_info,\"\",@progbits" | Section_debug_abbrev -> ".section .debug_abbrev,\"\",@progbits" | Section_debug_loc -> ".section .debug_loc,\"\",@progbits" - | Section_debug_line _ -> ".section .debug_line,\"\",@progbits\n" + | Section_debug_line _ -> ".section .debug_line,\"\",@progbits" + | Section_debug_str -> ".section .debug_str,\"MS\",@progbits,1" let section oc sec = @@ -221,6 +222,7 @@ module Diab_System : SYSTEM = | Section_debug_abbrev -> ".section .debug_abbrev,,n" | Section_debug_loc -> ".section .debug_loc,,n" | Section_debug_line s -> sprintf ".section .debug_line.%s,,n\n" s + | Section_debug_str -> assert false (* Should not be used *) let section oc sec = let name = name_of_section sec in -- cgit From a479c280441b91007c379b0b63b907926d54f930 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 13 Oct 2015 16:23:20 +0200 Subject: Changed the type of the debug sections with additional string. Instead of using a string they now take an optional string, which should be none if the backend is not the diab backend and the corresponding section is the text section and Some s with s being the custom section name else. Bug 17392. --- powerpc/TargetPrinter.ml | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) (limited to 'powerpc/TargetPrinter.ml') diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 61ac5e42..a596e587 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -218,20 +218,25 @@ module Diab_System : SYSTEM = | true, false -> 'd' (* data *) | false, true -> 'c' (* text *) | false, false -> 'r') (* const *) - | Section_debug_info s -> sprintf ".section .debug_info%s,,n" (if s <> ".text" then s else "") + | Section_debug_info (Some s) -> + sprintf ".section .debug_info%s,,n" s + | Section_debug_info None -> + sprintf ".section .debug_info,,n" | Section_debug_abbrev -> ".section .debug_abbrev,,n" | Section_debug_loc -> ".section .debug_loc,,n" - | Section_debug_line s -> sprintf ".section .debug_line.%s,,n\n" s + | Section_debug_line (Some s) -> + sprintf ".section .debug_line.%s,,n\n" s + | Section_debug_line None -> + sprintf ".section .debug_line,,n\n" | Section_debug_str -> assert false (* Should not be used *) let section oc sec = let name = name_of_section sec in assert (name <> "COMM"); match sec with - | Section_debug_info s -> + | Section_debug_info (Some s) -> fprintf oc " %s\n" name; - if s <> ".text" then - fprintf oc " .sectionlink .debug_info\n" + fprintf oc " .sectionlink .debug_info\n" | _ -> fprintf oc " %s\n" name @@ -263,6 +268,7 @@ module Diab_System : SYSTEM = Debug.add_diab_info name (line_start,debug_info,name_of_section sec); Debug.add_compilation_section_start name low_pc; let line_name = ".debug_line" ^(if name <> ".text" then name else "") in + section oc (Section_debug_line (if name <> ".text" then Some name else None)); fprintf oc " .section %s,,n\n" line_name; if name <> ".text" then fprintf oc " .sectionlink .debug_line\n"; -- cgit From 60ab550a952c3d9719b2a91ec90c9b58769f6717 Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Wed, 14 Oct 2015 15:07:48 +0200 Subject: bug 17392: remove trailing whitespace in source files --- powerpc/TargetPrinter.ml | 70 ++++++++++++++++++++++++------------------------ 1 file changed, 35 insertions(+), 35 deletions(-) (limited to 'powerpc/TargetPrinter.ml') diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index a596e587..10d89d54 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -103,15 +103,15 @@ module Linux_System : SYSTEM = let freg oc r = output_string oc (float_reg_name r) - - let creg oc r = + + let creg oc r = fprintf oc "%d" r - + let name_of_section = function | Section_text -> ".text" | Section_data i -> if i then ".data" else "COMM" - | Section_small_data i -> + | Section_small_data i -> if i then ".section .sdata,\"aw\",@progbits" else "COMM" | Section_const i -> if i then ".rodata" else "COMM" @@ -138,17 +138,17 @@ module Linux_System : SYSTEM = let print_file_line oc file line = print_file_line oc comment file line - - (* Emit .cfi directives *) + + (* Emit .cfi directives *) let cfi_startproc = cfi_startproc let cfi_endproc = cfi_endproc - + let cfi_adjust = cfi_adjust - + let cfi_rel_offset = cfi_rel_offset - let print_prologue oc = + let print_prologue oc = if !Clflags.option_g then begin section oc Section_text; let low_pc = new_label () in @@ -169,7 +169,7 @@ module Linux_System : SYSTEM = let debug_section _ _ = () end - + module Diab_System : SYSTEM = struct @@ -189,7 +189,7 @@ module Diab_System : SYSTEM = symbol_fragment oc s n "@sdax@l" | Csymbol_rel_high(s, n) -> symbol_fragment oc s n "@sdarx@ha" - + let ireg oc r = output_char oc 'r'; output_string oc (int_reg_name r) @@ -197,10 +197,10 @@ module Diab_System : SYSTEM = let freg oc r = output_char oc 'f'; output_string oc (float_reg_name r) - + let creg oc r = fprintf oc "cr%d" r - + let name_of_section = function | Section_text -> ".text" | Section_data i -> if i then ".data" else "COMM" @@ -254,20 +254,20 @@ module Diab_System : SYSTEM = let debug_section oc sec = match sec with - | Section_debug_abbrev + | Section_debug_abbrev | Section_debug_info _ | Section_debug_loc -> () | sec -> let name = match sec with | Section_user (name,_,_) -> name | _ -> name_of_section sec in - if not (Debug.exists_section name) then + if not (Debug.exists_section name) then let line_start = new_label () and low_pc = new_label () and debug_info = new_label () in Debug.add_diab_info name (line_start,debug_info,name_of_section sec); Debug.add_compilation_section_start name low_pc; - let line_name = ".debug_line" ^(if name <> ".text" then name else "") in + let line_name = ".debug_line" ^(if name <> ".text" then name else "") in section oc (Section_debug_line (if name <> ".text" then Some name else None)); fprintf oc " .section %s,,n\n" line_name; if name <> ".text" then @@ -279,18 +279,18 @@ module Diab_System : SYSTEM = fprintf oc " .d2_line_start %s\n" line_name else () - + let print_prologue oc = fprintf oc " .xopt align-fill-text=0x60000000\n"; debug_section oc Section_text let print_epilogue oc = - let end_label sec = + let end_label sec = fprintf oc "\n"; fprintf oc " %s\n" sec; let label_end = new_label () in fprintf oc "%a:\n" label label_end; - label_end + label_end and entry_label f = let label = new_label () in fprintf oc ".L%d: .d2filenum \"%s\"\n" label f; @@ -306,7 +306,7 @@ module Target (System : SYSTEM):TARGET = (* Basic printing functions *) let symbol = symbol - + let raw_symbol oc s = fprintf oc "%s" s @@ -371,7 +371,7 @@ module Target (System : SYSTEM):TARGET = let short_cond_branch tbl pc lbl_dest = match PTree.get lbl_dest tbl with | None -> assert false - | Some pc_dest -> + | Some pc_dest -> let disp = pc_dest - pc in -0x2000 <= disp && disp < 0x2000 (* Printing of instructions *) @@ -551,11 +551,11 @@ module Target (System : SYSTEM):TARGET = | Pfnmsub(r1, r2, r3, r4) -> fprintf oc " fnmsub %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 | Pfsqrt(r1, r2) -> - fprintf oc " fsqrt %a, %a\n" freg r1 freg r2 + fprintf oc " fsqrt %a, %a\n" freg r1 freg r2 | Pfrsqrte(r1, r2) -> - fprintf oc " frsqrte %a, %a\n" freg r1 freg r2 + fprintf oc " frsqrte %a, %a\n" freg r1 freg r2 | Pfres(r1, r2) -> - fprintf oc " fres %a, %a\n" freg r1 freg r2 + fprintf oc " fres %a, %a\n" freg r1 freg r2 | Pfsel(r1, r2, r3, r4) -> fprintf oc " fsel %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 | Pisel (r1,r2,r3,cr) -> @@ -793,7 +793,7 @@ module Target (System : SYSTEM):TARGET = let nlo = Int64.to_int32 n and nhi = Int64.to_int32(Int64.shift_right_logical n 32) in fprintf oc "%a: .long 0x%lx, 0x%lx\n" label lbl nhi nlo - + let print_literal32 oc (lbl, n) = fprintf oc "%a: .long 0x%lx\n" label lbl n @@ -823,10 +823,10 @@ module Target (System : SYSTEM):TARGET = if Z.gt n Z.zero then fprintf oc " .space %s\n" (Z.to_string n) | Init_addrof(symb, ofs) -> - fprintf oc " .long %a\n" + fprintf oc " .long %a\n" symbol_offset (symb, ofs) - + let print_fun_info = elf_print_fun_info let emit_constants oc lit = @@ -840,26 +840,26 @@ module Target (System : SYSTEM):TARGET = let print_optional_fun_info _ = () - let get_section_names name = + let get_section_names name = match C2C.atom_sections name with | [t;l;j] -> (t, l, j) | _ -> (Section_text, Section_literal, Section_jumptable) - + let reset_constants = reset_constants - + let print_var_info = elf_print_var_info - let print_comm_symb oc sz name align = + let print_comm_symb oc sz name align = fprintf oc " %s %a, %s, %d\n" (if C2C.atom_is_static name then ".lcomm" else ".comm") symbol name (Z.to_string sz) align - + let print_align oc align = fprintf oc " .balign %d\n" align - let print_jumptable oc jmptbl = + let print_jumptable oc jmptbl = let print_jumptable oc (lbl, tbl) = fprintf oc "%a:" label lbl; List.iter @@ -874,7 +874,7 @@ module Target (System : SYSTEM):TARGET = let default_falignment = 4 - let new_label = new_label + let new_label = new_label let section oc sec = section oc sec; @@ -882,7 +882,7 @@ module Target (System : SYSTEM):TARGET = end let sel_target () = - let module S = (val + let module S = (val (match Configuration.system with | "linux" -> (module Linux_System:SYSTEM) | "diab" -> (module Diab_System:SYSTEM) -- cgit From ccfc5ced6a09ce2c8a1ebce81050c328c17c9bec Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 14 Oct 2015 10:10:19 +0200 Subject: Reworked the section interface for the debug information. Instead of pushing strings around use the actual section. However the string is still used in the Hashtbl. Bug 17392. --- powerpc/TargetPrinter.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'powerpc/TargetPrinter.ml') diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 10d89d54..aed6e2bf 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -152,7 +152,7 @@ module Linux_System : SYSTEM = if !Clflags.option_g then begin section oc Section_text; let low_pc = new_label () in - Debug.add_compilation_section_start ".text" low_pc; + Debug.add_compilation_section_start Section_text low_pc; fprintf oc "%a:\n" label low_pc; fprintf oc " .cfi_sections .debug_frame\n" end @@ -161,7 +161,7 @@ module Linux_System : SYSTEM = if !Clflags.option_g then begin let high_pc = new_label () in - Debug.add_compilation_section_end ".text" high_pc; + Debug.add_compilation_section_end Section_text high_pc; Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f)); section oc Section_text; fprintf oc "%a:\n" label high_pc @@ -256,17 +256,18 @@ module Diab_System : SYSTEM = match sec with | Section_debug_abbrev | Section_debug_info _ + | Section_debug_str | Section_debug_loc -> () | sec -> let name = match sec with | Section_user (name,_,_) -> name | _ -> name_of_section sec in - if not (Debug.exists_section name) then + if not (Debug.exists_section sec) then let line_start = new_label () and low_pc = new_label () and debug_info = new_label () in - Debug.add_diab_info name (line_start,debug_info,name_of_section sec); - Debug.add_compilation_section_start name low_pc; + Debug.add_diab_info sec line_start debug_info; + Debug.add_compilation_section_start sec low_pc; let line_name = ".debug_line" ^(if name <> ".text" then name else "") in section oc (Section_debug_line (if name <> ".text" then Some name else None)); fprintf oc " .section %s,,n\n" line_name; @@ -287,7 +288,7 @@ module Diab_System : SYSTEM = let print_epilogue oc = let end_label sec = fprintf oc "\n"; - fprintf oc " %s\n" sec; + section oc sec; let label_end = new_label () in fprintf oc "%a:\n" label label_end; label_end -- cgit From 1e52bb2001964d87086cea00d0cb779e270b99ce Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 15 Oct 2015 13:15:28 +0200 Subject: First step to implemente address ranges for the gnu backend. In contrast to the dcc, the gcc uses address ranges to express non-contiguous range of addresses. As a first step we set the start and end addresses for the different address ranges for the compilation unit by using the start and end addresses of functions. Bug 17392. --- powerpc/TargetPrinter.ml | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) (limited to 'powerpc/TargetPrinter.ml') diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index aed6e2bf..54a2868a 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -151,20 +151,14 @@ module Linux_System : SYSTEM = let print_prologue oc = if !Clflags.option_g then begin section oc Section_text; - let low_pc = new_label () in - Debug.add_compilation_section_start Section_text low_pc; - fprintf oc "%a:\n" label low_pc; fprintf oc " .cfi_sections .debug_frame\n" end let print_epilogue oc = if !Clflags.option_g then begin - let high_pc = new_label () in - Debug.add_compilation_section_end Section_text high_pc; Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f)); section oc Section_text; - fprintf oc "%a:\n" label high_pc end let debug_section _ _ = () @@ -266,8 +260,7 @@ module Diab_System : SYSTEM = let line_start = new_label () and low_pc = new_label () and debug_info = new_label () in - Debug.add_diab_info sec line_start debug_info; - Debug.add_compilation_section_start sec low_pc; + Debug.add_diab_info sec line_start debug_info low_pc; let line_name = ".debug_line" ^(if name <> ".text" then name else "") in section oc (Section_debug_line (if name <> ".text" then Some name else None)); fprintf oc " .section %s,,n\n" line_name; -- cgit From 24b4159b6a29328c529e0e59405e03ea192aa99e Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 16 Oct 2015 13:06:09 +0200 Subject: Implemented the usage of DW_AT_ranges for non-contiguous address ranges. The gcc produces DW_AT_ranges for non-contiguous address ranges, like compilation units containing functions which are placed in different ELF-sections or lexical scopes that are split up. With this commit CompCert also uses this DWARF v3 feature for gnu backend based targets. In order to ensure backward compability a flag is added which avoids this and produces debug info in DWARF v2 format. Bug 17392. --- powerpc/TargetPrinter.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'powerpc/TargetPrinter.ml') diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 54a2868a..709a0d7c 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -127,6 +127,7 @@ module Linux_System : SYSTEM = | Section_debug_abbrev -> ".section .debug_abbrev,\"\",@progbits" | Section_debug_loc -> ".section .debug_loc,\"\",@progbits" | Section_debug_line _ -> ".section .debug_line,\"\",@progbits" + | Section_debug_ranges -> ".section .debug_ranges,\"\",@progbits" | Section_debug_str -> ".section .debug_str,\"MS\",@progbits,1" @@ -222,6 +223,7 @@ module Diab_System : SYSTEM = sprintf ".section .debug_line.%s,,n\n" s | Section_debug_line None -> sprintf ".section .debug_line,,n\n" + | Section_debug_ranges | Section_debug_str -> assert false (* Should not be used *) let section oc sec = -- cgit