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. --- arm/TargetPrinter.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'arm/TargetPrinter.ml') diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 2e676090..b988f10f 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -157,7 +157,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | Section_debug_loc -> ".section .debug_loc,\"\",%progbits" | Section_debug_abbrev -> ".section .debug_abbrev,\"\",%progbits" | Section_debug_line _ -> ".section .debug_line,\"\",%progbits" - + | Section_debug_str -> ".section .debug_str,\"MS\",%progbits,1" let section oc sec = fprintf oc " %s\n" (name_of_section sec) -- 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 --- arm/TargetPrinter.ml | 94 ++++++++++++++++++++++++++-------------------------- 1 file changed, 47 insertions(+), 47 deletions(-) (limited to 'arm/TargetPrinter.ml') diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index b988f10f..4961f897 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -40,13 +40,13 @@ module type PRINTER_OPTIONS = module Target (Opt: PRINTER_OPTIONS) : TARGET = struct (* Code generation options. *) - + let literals_in_code = ref true (* to be turned into a proper option *) - + (* Basic printing functions *) - + let print_label oc lbl = elf_label oc (transl_label lbl) - + let comment = "@" let symbol = elf_symbol @@ -61,34 +61,34 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | IR4 -> "r4" | IR5 -> "r5" | IR6 -> "r6" | IR7 -> "r7" | IR8 -> "r8" | IR9 -> "r9" | IR10 -> "r10" | IR11 -> "r11" | IR12 -> "r12" | IR13 -> "sp" | IR14 -> "lr" - + let float_reg_name = function | FR0 -> "d0" | FR1 -> "d1" | FR2 -> "d2" | FR3 -> "d3" | FR4 -> "d4" | FR5 -> "d5" | FR6 -> "d6" | FR7 -> "d7" | FR8 -> "d8" | FR9 -> "d9" | FR10 -> "d10" | FR11 -> "d11" | FR12 -> "d12" | FR13 -> "d13" | FR14 -> "d14" | FR15 -> "d15" - + let single_float_reg_index = function | FR0 -> 0 | FR1 -> 2 | FR2 -> 4 | FR3 -> 6 | FR4 -> 8 | FR5 -> 10 | FR6 -> 12 | FR7 -> 14 | FR8 -> 16 | FR9 -> 18 | FR10 -> 20 | FR11 -> 22 | FR12 -> 24 | FR13 -> 26 | FR14 -> 28 | FR15 -> 30 - + let single_float_reg_name = function | FR0 -> "s0" | FR1 -> "s2" | FR2 -> "s4" | FR3 -> "s6" | FR4 -> "s8" | FR5 -> "s10" | FR6 -> "s12" | FR7 -> "s14" | FR8 -> "s16" | FR9 -> "s18" | FR10 -> "s20" | FR11 -> "s22" | FR12 -> "s24" | FR13 -> "s26" | FR14 -> "s28" | FR15 -> "s30" - + let ireg oc r = output_string oc (int_reg_name r) let freg oc r = output_string oc (float_reg_name r) let freg_single oc r = output_string oc (single_float_reg_name r) - + let preg oc = function | IR r -> ireg oc r | FR r -> freg oc r | _ -> assert false - + let condition_name = function | TCeq -> "eq" | TCne -> "ne" @@ -102,7 +102,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | TClt -> "lt" | TCgt -> "gt" | TCle -> "le" - + let neg_condition_name = function | TCeq -> "ne" | TCne -> "eq" @@ -116,7 +116,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | TClt -> "ge" | TCgt -> "le" | TCle -> "gt" - + (* In Thumb2 mode, some arithmetic instructions have shorter encodings if they carry the "S" flag (update condition flags): add (but not sp + imm) @@ -158,27 +158,27 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | Section_debug_abbrev -> ".section .debug_abbrev,\"\",%progbits" | Section_debug_line _ -> ".section .debug_line,\"\",%progbits" | Section_debug_str -> ".section .debug_str,\"MS\",%progbits,1" - + let section oc sec = fprintf oc " %s\n" (name_of_section sec) - + (* Record current code position and latest position at which to emit float and symbol constants. *) - + let currpos = ref 0 let size_constants = ref 0 let max_pos_constants = ref max_int - + let distance_to_emit_constants () = if !literals_in_code then !max_pos_constants - (!currpos + !size_constants) else max_int - + (* Associate labels to floating-point constants and to symbols *) - + let float_labels = (Hashtbl.create 39 : (int64, int) Hashtbl.t) let float32_labels = (Hashtbl.create 39 : (int32, int) Hashtbl.t) - + let label_float bf = try Hashtbl.find float_labels bf @@ -188,7 +188,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = size_constants := !size_constants + 8; max_pos_constants := min !max_pos_constants (!currpos + 1024); lbl' - + let label_float32 bf = try Hashtbl.find float32_labels bf @@ -198,10 +198,10 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = size_constants := !size_constants + 4; max_pos_constants := min !max_pos_constants (!currpos + 1024); lbl' - + let symbol_labels = (Hashtbl.create 39 : (ident * Integers.Int.int, int) Hashtbl.t) - + let label_symbol id ofs = try Hashtbl.find symbol_labels (id, ofs) @@ -211,14 +211,14 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = size_constants := !size_constants + 4; max_pos_constants := min !max_pos_constants (!currpos + 4096); lbl' - + let reset_constants () = Hashtbl.clear float_labels; Hashtbl.clear float32_labels; Hashtbl.clear symbol_labels; size_constants := 0; max_pos_constants := max_int - + let emit_constants oc = fprintf oc " .balign 4\n"; Hashtbl.iter @@ -238,9 +238,9 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = lbl symbol_offset (id, ofs)) symbol_labels; reset_constants () - + (* Generate code to load the address of id + ofs in register r *) - + let loadsymbol oc r id ofs = if !Clflags.option_mthumb then begin fprintf oc " movw %a, #:lower16:%a\n" @@ -249,13 +249,13 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = ireg r symbol_offset (id, ofs); 2 end else begin let lbl = label_symbol id ofs in - fprintf oc " ldr %a, .L%d @ %a\n" + fprintf oc " ldr %a, .L%d @ %a\n" ireg r lbl symbol_offset (id, ofs); 1 end - + (* Emit instruction sequences that set or offset a register by a constant. *) (* No S suffix because they are applied to SP most of the time. *) - + let movimm oc dst n = match Asmgen.decompose_int n with | [] -> assert false @@ -265,7 +265,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = (fun n -> fprintf oc " orr %s, %s, #%a\n" dst dst coqint n) tl; List.length l - + let addimm oc dst src n = match Asmgen.decompose_int n with | [] -> assert false @@ -275,7 +275,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = (fun n -> fprintf oc " add %s, %s, #%a\n" dst dst coqint n) tl; List.length l - + let subimm oc dst src n = match Asmgen.decompose_int n with | [] -> assert false @@ -285,27 +285,27 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = (fun n -> fprintf oc " sub %s, %s, #%a\n" dst dst coqint n) tl; List.length l - + (* Recognition of float constants appropriate for VMOV. a normalized binary floating point encoding with 1 sign bit, 4 bits of fraction and a 3-bit exponent *) - + let is_immediate_float64 bits = let exp = (Int64.(to_int (shift_right_logical bits 52)) land 0x7FF) - 1023 in let mant = Int64.logand bits 0xF_FFFF_FFFF_FFFFL in exp >= -3 && exp <= 4 && Int64.logand mant 0xF_0000_0000_0000L = mant - + let is_immediate_float32 bits = let exp = (Int32.(to_int (shift_right_logical bits 23)) land 0xFF) - 127 in let mant = Int32.logand bits 0x7F_FFFFl in exp >= -3 && exp <= 4 && Int32.logand mant 0x78_0000l = mant - + (* Emit .file / .loc debugging directives *) - + let print_file_line oc file line = print_file_line oc comment file line - + let print_location oc loc = if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc) @@ -456,7 +456,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = match Opt.float_abi with | Soft -> (FixupEABI.fixup_arguments, FixupEABI.fixup_result) | Hard -> (FixupHF.fixup_arguments, FixupHF.fixup_result) - + (* Printing of instructions *) let shift_op oc = function @@ -494,7 +494,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = fprintf oc " b %a\n" symbol id; n + 1 | Pbreg(r, sg) -> - let n = + let n = if r = IR14 then fixup_result oc Outgoing sg else fixup_arguments oc Outgoing sg in @@ -886,7 +886,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = fprintf oc " .space %s\n" (Z.to_string n) | Init_addrof(symb, ofs) -> fprintf oc " .word %a\n" symbol_offset (symb, ofs) - + let print_prologue oc = fprintf oc " .syntax unified\n"; fprintf oc " .arch %s\n" @@ -908,7 +908,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = end - let print_epilogue oc = + let print_epilogue oc = if !Clflags.option_g then begin let high_pc = new_label () in Debug.add_compilation_section_end ".text" high_pc; @@ -919,22 +919,22 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = let default_falignment = 4 - + let label = elf_label - + let new_label = new_label end -let sel_target () = +let sel_target () = let module S : PRINTER_OPTIONS = struct - + let vfpv3 = Configuration.model >= "armv7" - + let float_abi = match Configuration.abi with | "eabi" -> Soft | "hardfloat" -> Hard | _ -> assert false - + let hardware_idiv = match Configuration.model with | "armv7r" | "armv7m" -> !Clflags.option_mthumb -- cgit From 44845982f412810b0c18067987f2780ef6245fbb Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 15 Oct 2015 09:10:22 +0200 Subject: Use section type also for other targets. Bug 17392. --- arm/TargetPrinter.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'arm/TargetPrinter.ml') diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 4961f897..3bffe59b 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -902,7 +902,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = 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" elf_label low_pc; fprintf oc " .cfi_sections .debug_frame\n" end @@ -911,7 +911,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = let print_epilogue oc = 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" elf_label high_pc -- 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. --- arm/TargetPrinter.ml | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) (limited to 'arm/TargetPrinter.ml') diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 3bffe59b..151326bb 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -901,21 +901,15 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = fprintf oc " .%s\n" (if !Clflags.option_mthumb then "thumb" else "arm"); 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" elf_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" elf_label high_pc - end + end let default_falignment = 4 -- 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. --- arm/TargetPrinter.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'arm/TargetPrinter.ml') diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 151326bb..9f435cee 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -157,6 +157,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | Section_debug_loc -> ".section .debug_loc,\"\",%progbits" | Section_debug_abbrev -> ".section .debug_abbrev,\"\",%progbits" | Section_debug_line _ -> ".section .debug_line,\"\",%progbits" + | Section_debug_line -> ".section .debug_ranges,\"\",%progbits" | Section_debug_str -> ".section .debug_str,\"MS\",%progbits,1" let section oc sec = -- cgit From 32ab0017ba80baafd03230960beaf3e256637369 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 16 Oct 2015 13:14:15 +0200 Subject: Fixed typos in the arm and ia32 section printing. Bug 17392 --- arm/TargetPrinter.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'arm/TargetPrinter.ml') diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 9f435cee..3b920ce0 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -157,7 +157,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | Section_debug_loc -> ".section .debug_loc,\"\",%progbits" | Section_debug_abbrev -> ".section .debug_abbrev,\"\",%progbits" | Section_debug_line _ -> ".section .debug_line,\"\",%progbits" - | Section_debug_line -> ".section .debug_ranges,\"\",%progbits" + | Section_debug_ranges -> ".section .debug_ranges,\"\",%progbits" | Section_debug_str -> ".section .debug_str,\"MS\",%progbits,1" let section oc sec = -- cgit