From 2ca1282f84c5da41328b1251ac7bbcfa417b9be6 Mon Sep 17 00:00:00 2001 From: François Pottier Date: Tue, 3 Nov 2015 10:32:55 +0100 Subject: When printing a fragment of source text as part of an error message, compress multiple whitespace characters into just one space character. This is done before the call to [sanitize], which replaces special characters with a dot. This produces more a readable result when the error spans multiple lines. --- cparser/ErrorReports.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/cparser/ErrorReports.ml b/cparser/ErrorReports.ml index 4bbf3ded..a8976e42 100644 --- a/cparser/ErrorReports.ml +++ b/cparser/ErrorReports.ml @@ -92,6 +92,14 @@ let extract text (pos1, pos2) : string = (* -------------------------------------------------------------------------- *) +(* [compress text] replaces every run of at least one whitespace character + with exactly one space character. *) + +let compress text = + Str.global_replace (Str.regexp "[ \t\n\r]+") " " text + +(* -------------------------------------------------------------------------- *) + (* [sanitize text] eliminates any special characters from the text [text]. They are (arbitrarily) replaced with a single dot character. *) @@ -182,7 +190,7 @@ let range text (e : element) : string = (* Get the underlying source text fragment. *) let fragment = extract text (pos1, pos2) in (* Sanitize it and limit its length. Enclose it in single quotes. *) - "'" ^ shorten width (sanitize fragment) ^ "'" + "'" ^ shorten width (sanitize (compress fragment)) ^ "'" (* -------------------------------------------------------------------------- *) -- cgit From d10d384f4ce0c1081497cf0657ea3580779d7330 Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Wed, 4 Nov 2015 17:12:24 +0100 Subject: bug 17567, typos --- debug/Debug.ml | 2 +- debug/Debug.mli | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/debug/Debug.ml b/debug/Debug.ml index 87d04ad7..789ecb70 100644 --- a/debug/Debug.ml +++ b/debug/Debug.ml @@ -20,7 +20,7 @@ open Sections (* Interface for generating and printing debug information *) -(* Record used for stroring references to the actual implementation functions *) +(* Record used for storing references to the actual implementation functions *) type implem = { init: string -> unit; diff --git a/debug/Debug.mli b/debug/Debug.mli index 1585e7e4..614fe84b 100644 --- a/debug/Debug.mli +++ b/debug/Debug.mli @@ -18,7 +18,7 @@ open BinNums open Sections -(* Record used for stroring references to the actual implementation functions *) +(* Record used for storing references to the actual implementation functions *) type implem = { init: string -> unit; -- cgit From 738c07062ea0708fc9208318933fda16fd696cc0 Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Wed, 4 Nov 2015 17:29:22 +0100 Subject: bug 17567, typos --- debug/DwarfUtil.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/debug/DwarfUtil.ml b/debug/DwarfUtil.ml index 3e252dd2..8db80fca 100644 --- a/debug/DwarfUtil.ml +++ b/debug/DwarfUtil.ml @@ -10,7 +10,7 @@ (* *) (* *********************************************************************) -(* Utility functions for the dwarf debuging type *) +(* Utility functions for the dwarf debugging type *) open DwarfTypes @@ -22,12 +22,12 @@ let new_entry id tag = id = id; } -(* Add an entry as child to another entry *) +(* Add an entry as child to another entry *) let add_child entry child = {entry with children = child::entry.children;} -(* Add entries as children to another entry *) +(* Add entries as children to another entry *) let add_children entry children = {entry with children = entry.children@children;} -- cgit From cbff6d5b0f84090e2ff7f74bfb6eb7f3e3a29ef9 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 4 Nov 2015 18:21:19 +0100 Subject: New option to control the debug information build. The new option -gonly-global allows the generation of debuging information for global variables only. Bug 17566. --- debug/DwarfPrinter.ml | 6 ++++-- debug/Dwarfgen.ml | 11 ++++++++--- driver/Clflags.ml | 1 + driver/Driver.ml | 2 ++ 4 files changed, 15 insertions(+), 5 deletions(-) diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml index 3e85ecfc..7469c4af 100644 --- a/debug/DwarfPrinter.ml +++ b/debug/DwarfPrinter.ml @@ -623,8 +623,10 @@ module DwarfPrinter(Target: DWARF_TARGET): let name = if e.section_name <> ".text" then Some e.section_name else None in section oc (Section_debug_info name); print_debug_info oc e.start_label e.line_label e.entry) entries; - section oc Section_debug_loc; - List.iter (fun e -> print_location_list oc e.locs) entries + if List.exists (fun e -> match e.locs with _,[] -> false | _,_ -> true) entries then begin + section oc Section_debug_loc; + List.iter (fun e -> print_location_list oc e.locs) entries + end let print_ranges oc r = section oc Section_debug_ranges; diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml index 56a318fe..d198a92f 100644 --- a/debug/Dwarfgen.ml +++ b/debug/Dwarfgen.ml @@ -475,9 +475,14 @@ module Dwarfgenaux (Target: TARGET) = let f_id = get_opt_val f.fun_atom in let acc = match f.fun_return_type with Some s -> acc =<< s | None -> acc in let f_entry = new_entry id (DW_TAG_subprogram f_tag) in - let params,acc = mmap (function_parameter_to_entry f_id) acc f.fun_parameter in - let vars,acc = fun_scope_to_entries f_id acc f.fun_scope in - add_children f_entry (params@vars),acc + let children,acc = + if not !Clflags.option_gglobal then + let params,acc = mmap (function_parameter_to_entry f_id) acc f.fun_parameter in + let vars,acc = fun_scope_to_entries f_id acc f.fun_scope in + params@vars,acc + else + [],acc in + add_children f_entry (children),acc let definition_to_entry acc id t = match t with diff --git a/driver/Clflags.ml b/driver/Clflags.ml index b0c24f08..1eaa5449 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -47,6 +47,7 @@ let option_dasm = ref false let option_sdump = ref false let option_g = ref false let option_gdwarf = ref 2 +let option_gglobal = ref false let option_o = ref (None: string option) let option_E = ref false let option_S = ref false diff --git a/driver/Driver.ml b/driver/Driver.ml index a0d742c2..59e3fa3b 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -435,6 +435,7 @@ Language support options (use -fno- to turn off -f) : Debugging options: -g Generate debugging information -gdwarf- (GCC only) Generate debug information in DWARF v2 or DWARF v3 + -gonly-global Generate debugging information only for globals -frename-static Rename static functions and declarations Optimization options: (use -fno- to turn off -f) -O Optimize the compiled code [on by default] @@ -547,6 +548,7 @@ let cmdline_actions = Exact "-gdwarf-3", Self (fun s -> option_g := true; option_gdwarf := 3); Exact "-frename-static", Self (fun s -> option_rename_static:= true); + Exact "-gonly-global", Self (fun s -> option_gglobal := true); (* Code generation options -- more below *) Exact "-O0", Self (fun _ -> unset_all optimization_options); Exact "-O", Self (fun _ -> set_all optimization_options); -- cgit From c1829348282418e42d2c94bb2f761a63d5a06ab4 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 6 Nov 2015 13:04:54 +0100 Subject: Do not print parameter names in function types. For function types used by function pointers we do not need to print the name of the paraments. Also switch the logic in case of prototyped/unprototyped. Fix 17579. --- debug/Dwarfgen.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml index d198a92f..8a72a865 100644 --- a/debug/Dwarfgen.ml +++ b/debug/Dwarfgen.ml @@ -186,7 +186,7 @@ module Dwarfgenaux (Target: TARGET) = add_children enum child let fun_type_to_entry id f = - let children = if f.fun_prototyped then + let children = if not f.fun_prototyped then let u = { unspecified_parameter_artificial = None; } in @@ -195,7 +195,7 @@ module Dwarfgenaux (Target: TARGET) = List.map (fun p -> let fp = { formal_parameter_artificial = None; - formal_parameter_name = name_opt p.param_name; + formal_parameter_name = None; formal_parameter_type = p.param_type; formal_parameter_variable_parameter = None; formal_parameter_location = None; -- cgit From 31fcfe29ebf1ef6eea487e8ce18eb5e11fb60b67 Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Fri, 6 Nov 2015 13:04:58 +0100 Subject: bug 17567, typos --- debug/DebugInformation.ml | 14 +++++++------- debug/DebugTypes.mli | 2 +- debug/DwarfTypes.mli | 2 +- debug/Dwarfgen.ml | 4 ++-- 4 files changed, 11 insertions(+), 11 deletions(-) diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml index 51fbfde9..ed00ea0d 100644 --- a/debug/DebugInformation.ml +++ b/debug/DebugInformation.ml @@ -65,7 +65,7 @@ let strip_attributes typ = strip_attributes_type typ [AConst; AVolatile] (* Find the type id to an type *) let find_type (ty: typ) = - (* We are only interrested in Const and Volatile *) + (* We are only interested in Const and Volatile *) let ty = strip_attributes ty in Hashtbl.find lookup_types (typ_to_string ty) @@ -77,7 +77,7 @@ let insert_type (ty: typ) = Hashtbl.add types id d_ty; Hashtbl.add lookup_types name id; id in - (* We are only interrested in Const and Volatile *) + (* We are only interested in Const and Volatile *) let ty = strip_attributes ty in let rec typ_aux ty = try find_type ty with @@ -255,14 +255,14 @@ let replace_fun id f = (* All local variables *) let local_variables: (int, local_information) Hashtbl.t = Hashtbl.create 7 -(* Mapping from stampt to the debug id of the local variable *) +(* Mapping from stamp to the debug id of the local variable *) let stamp_to_local: (int,int) Hashtbl.t = Hashtbl.create 7 -(* Map from scope id + function id to debug id *) +(* Map from function id + scope id to debug id *) let scope_to_local: (int * int,int) Hashtbl.t = Hashtbl.create 7 -(* Map from scope id + function atom to debug id *) -let atom_to_scope: (atom * int, int) Hashtbl.t = Hashtbl.create 7 +(* Map from function atom + scope id atom to debug id *) +let atom_to_scope: (atom * int,int) Hashtbl.t = Hashtbl.create 7 let find_lvar_stamp id = let id = (Hashtbl.find stamp_to_local id) in @@ -299,7 +299,7 @@ let remove_unused id = Hashtbl.remove stamp_to_definition id.stamp with Not_found -> () -let insert_global_declaration env dec= +let insert_global_declaration env dec = add_file (fst dec.gloc); let insert d_dec stamp = let id = next_id () in diff --git a/debug/DebugTypes.mli b/debug/DebugTypes.mli index b2f19f7a..e885fc59 100644 --- a/debug/DebugTypes.mli +++ b/debug/DebugTypes.mli @@ -147,7 +147,7 @@ type local_variable_information = { lvar_atom: atom option; lvar_file_loc:location; lvar_type: int; - lvar_static: bool; (* Static variable are mapped to symbols *) + lvar_static: bool; (* Static variables are mapped to symbols *) } type scope_information = diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli index a4c75201..2af64c0b 100644 --- a/debug/DwarfTypes.mli +++ b/debug/DwarfTypes.mli @@ -297,7 +297,7 @@ type debug_entries = | Gnu of gnu_entries (* The target specific functions for printing the debug information *) -module type DWARF_TARGET= +module type DWARF_TARGET = sig val label: out_channel -> int -> unit val section: out_channel -> section_name -> unit diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml index d198a92f..9baf6d70 100644 --- a/debug/Dwarfgen.ml +++ b/debug/Dwarfgen.ml @@ -182,8 +182,8 @@ module Dwarfgenaux (Target: TARGET) = enumeration_name = string_entry e.enum_name; } in let enum = new_entry id (DW_TAG_enumeration_type enum) in - let child = List.map enumerator_to_entry e.enum_enumerators in - add_children enum child + let children = List.map enumerator_to_entry e.enum_enumerators in + add_children enum children let fun_type_to_entry id f = let children = if f.fun_prototyped then -- cgit From 76cb39f790fc3bf4d1e2fae99cda7eeae8bbbbf2 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 6 Nov 2015 13:26:11 +0100 Subject: Added printing functions for debug annotations. Instead of printing we now print the debug annotations. Fix 17581. --- cfrontend/PrintCsyntax.ml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 4f2a8d0c..bb6576aa 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -266,6 +266,9 @@ let rec expr p (prec, e) = fprintf p "%s@[(%a)@]" (camlstring_of_coqstring id) exprlist (true, args) | Ebuiltin(EF_inline_asm(txt, sg, clob), _, args, _) -> extended_asm p txt None args clob + | Ebuiltin(EF_debug(kind,txt,_),_,args,_) -> + fprintf p "__builtin_debug@[(%d,%S%a)@]" + (P.to_int kind) (extern_atom txt) exprlist (false,args) | Ebuiltin(_, _, args, _) -> fprintf p "@[(%a)@]" exprlist (true, args) | Eparen(a1, tycast, ty) -> -- cgit From d9584e32f6b6f3a44d54615c97a5998c0ba6dfd5 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 6 Nov 2015 14:18:31 +0100 Subject: Remove debug stmts during grouping of switch. Debug statements introduced during the translation result in warnings when they are introduced at the head of the switch. Since they are not used and the warning is not necessary we can remove them before. Fix 17580. --- cfrontend/C2C.ml | 8 +++++--- cparser/Cutil.ml | 16 ++++++++++++---- cparser/Cutil.mli | 2 ++ 3 files changed, 19 insertions(+), 7 deletions(-) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index a2db0915..913b2874 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -918,8 +918,11 @@ let rec groupSwitch = function let (fst, cases) = groupSwitch rem in (Cutil.sskip, (case, fst) :: cases) | Stmt s :: rem -> - let (fst, cases) = groupSwitch rem in - (Cutil.sseq s.sloc s fst, cases) + if Cutil.is_debug_stmt s then + groupSwitch rem + else + let (fst, cases) = groupSwitch rem in + (Cutil.sseq s.sloc s fst, cases) (* Test whether the statement contains case and give an *) let rec contains_case s = @@ -1313,4 +1316,3 @@ let convertProgram p = if Cerrors.check_errors () then None else Some p' with Env.Error msg -> error (Env.error_message msg); None - diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index a86c779f..1b0bf65d 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -880,6 +880,18 @@ let is_literal_0 e = | EConst(CInt(0L, _, _)) -> true | _ -> false +(* Check that a C statement is a debug annotation *) + +let is_debug_stmt s = + let is_debug_call = function + | (ECall ({edesc = EVar id; _},_)) -> id.name = "__builtin_debug" + | _ -> false in + match s.sdesc with + | Sdo {edesc = e;_} -> + is_debug_call e + | _ -> false + + (* Assignment compatibility check over attributes. Standard attributes ("const", "volatile", "restrict") can safely be added (to the rhs type to get the lhs type) but must not be dropped. @@ -1099,7 +1111,3 @@ let rec subst_stmt phi s = List.map subst_asm_operand inputs, clob) } - - - - diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 8b6c609b..b353cba3 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -187,6 +187,8 @@ val type_of_member : Env.t -> field -> typ (* Return the type of accessing the given field [fld]. Normally it's [fld.fld_type] but there is a special case for small unsigned bitfields. *) +val is_debug_stmt : stmt -> bool + (* Is the given statement a call to debug builtin? *) val is_literal_0 : exp -> bool (* Is the given expression the integer literal "0"? *) val is_lvalue : exp -> bool -- cgit From d0049e3b6bafb3aa88e173c10183b564918de115 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 6 Nov 2015 14:38:07 +0100 Subject: Fix for switch was to eager. We should not remove any debug stmt inside of the cases. We should just not warn in the case that init is only debugcalls. Bug 17850 --- cfrontend/C2C.ml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 913b2874..6b3426b2 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -918,11 +918,8 @@ let rec groupSwitch = function let (fst, cases) = groupSwitch rem in (Cutil.sskip, (case, fst) :: cases) | Stmt s :: rem -> - if Cutil.is_debug_stmt s then - groupSwitch rem - else - let (fst, cases) = groupSwitch rem in - (Cutil.sseq s.sloc s fst, cases) + let (fst, cases) = groupSwitch rem in + (Cutil.sseq s.sloc s fst, cases) (* Test whether the statement contains case and give an *) let rec contains_case s = @@ -986,7 +983,12 @@ let rec convertStmt env s = Scontinue | C.Sswitch(e, s1) -> let (init, cases) = groupSwitch (flattenSwitch s1) in - if init.sdesc <> C.Sskip then + let rec init_debug s = + match s.sdesc with + | Sseq (a,b) -> init_debug a && init_debug b + | C.Sskip -> true + | _ -> Cutil.is_debug_stmt s in + if init.sdesc <> C.Sskip && not (init_debug init) then begin warning "ignored code at beginning of 'switch'"; contains_case init -- cgit