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 0ffd562ae1941e37471ac0c2b8f93bed1de26441 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 9 Oct 2015 11:06:24 +0200 Subject: Filled in the rest of the funciton needed for thte debug info under arm. The name_of_section function no returns the correct name for the debug sections, the prologue and epilogue directives are added and the labels for the live ranges are introduced in the Asmexpand pass. --- powerpc/TargetPrinter.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'powerpc/TargetPrinter.ml') diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 530e269d..0f0ed357 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -126,7 +126,9 @@ 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" + + let section oc sec = let name = name_of_section sec in assert (name <> "COMM"); @@ -146,9 +148,7 @@ module Linux_System : SYSTEM = let cfi_rel_offset = cfi_rel_offset let print_prologue oc = - if !Clflags.option_g then - begin - (* TODO print file *) + if !Clflags.option_g then begin section oc Section_text; let low_pc = new_label () in Debug.add_compilation_section_start ".text" low_pc; @@ -220,6 +220,7 @@ module Diab_System : SYSTEM = | Section_debug_info s -> sprintf ".section .debug_info%s,,n" (if s <> ".text" then s else "") | 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; let section oc sec = let name = name_of_section sec in -- cgit From 6a2cfdb1bc410532a23c58206cd00b39bc7ccba3 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 9 Oct 2015 12:10:30 +0200 Subject: Fixed syntax error and added Section_debug_line to the Json serializer. --- powerpc/TargetPrinter.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'powerpc/TargetPrinter.ml') diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 0f0ed357..e65a8934 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -220,7 +220,7 @@ module Diab_System : SYSTEM = | Section_debug_info s -> sprintf ".section .debug_info%s,,n" (if s <> ".text" then s else "") | 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 s -> sprintf ".section .debug_line.%s,,n\n" s let section oc sec = let name = name_of_section sec in -- cgit From 7a6bb90048db7a254e959b1e3c308bac5fe6c418 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 11 Oct 2015 17:43:59 +0200 Subject: Use Coq strings instead of idents to name external and builtin functions. The AST.ident type represents source-level identifiers as unique positive numbers. However, the mapping identifiers <-> AST.ident differs between runs of CompCert on different source files. This is problematic when we need to produce or recognize external functions and builtin functions with fixed names, for example: * in $ARCH/Machregs.v to define the register conventions for builtin functions; * in the VST program logic from Princeton to treat thread primitives specially. So far, we used AST.ident_of_string to recover the ident associated with a string. However, this function is defined in OCaml and doesn't execute within Coq. This is a problem both for VST and for future executability of CompCert within Coq. This commit replaces "ident" by "string" in the arguments of EF_external, EF_builtin, EF_inline_asm, EF_annot, and EF_annot_val. This provides stable names for externals and builtins, as needed. For inline asm and annotations, it's a matter of taste, but using strings feels more natural. EF_debug keeps using idents, since some kinds of EF_debug annotations talk about program variables. --- powerpc/TargetPrinter.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'powerpc/TargetPrinter.ml') diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index e65a8934..7dbc2cf5 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -704,13 +704,13 @@ module Target (System : SYSTEM):TARGET = begin match ef with | EF_annot(txt, targs) -> fprintf oc "%s annotation: " comment; - print_annot_text preg_annot "r1" oc (extern_atom txt) args + print_annot_text preg_annot "r1" oc (camlstring_of_coqstring txt) args | EF_debug(kind, txt, targs) -> print_debug_info comment print_file_line preg_annot "r1" oc (P.to_int kind) (extern_atom txt) args | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; - print_inline_asm preg oc (extern_atom txt) sg args res; + print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res; fprintf oc "%s end inline assembly\n" comment | _ -> assert false -- 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 From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- 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 7dbc2cf5..74eb8776 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" @@ -137,17 +137,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 @@ -168,7 +168,7 @@ module Linux_System : SYSTEM = let debug_section _ _ = () end - + module Diab_System : SYSTEM = struct @@ -188,7 +188,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) @@ -196,10 +196,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" @@ -247,20 +247,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 fprintf oc " .section %s,,n\n" line_name; if name <> ".text" then fprintf oc " .sectionlink .debug_line\n"; @@ -271,18 +271,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; @@ -298,7 +298,7 @@ module Target (System : SYSTEM):TARGET = (* Basic printing functions *) let symbol = symbol - + let raw_symbol oc s = fprintf oc "%s" s @@ -363,7 +363,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 *) @@ -531,11 +531,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) -> @@ -768,7 +768,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 @@ -798,10 +798,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 = @@ -815,26 +815,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 @@ -849,7 +849,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; @@ -857,7 +857,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