aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
diff options
context:
space:
mode:
Diffstat (limited to 'cparser')
-rw-r--r--cparser/Bitfields.ml1
-rw-r--r--cparser/Cleanup.ml7
-rw-r--r--cparser/Cprint.ml6
-rw-r--r--cparser/Cprint.mli1
-rw-r--r--cparser/Cutil.ml21
-rw-r--r--cparser/Cutil.mli2
-rw-r--r--cparser/Elab.ml32
-rw-r--r--cparser/Parse.ml13
-rw-r--r--cparser/Parse.mli2
-rw-r--r--cparser/Unblock.ml161
10 files changed, 192 insertions, 54 deletions
diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
index fbf57082..d064f4b1 100644
--- a/cparser/Bitfields.ml
+++ b/cparser/Bitfields.ml
@@ -134,6 +134,7 @@ let rec transf_struct_members env id count = function
if !config.bitfields_msb_first
then sizeof_ikind carrier_ikind * 8 - pos - sz
else pos in
+ Debug.set_bitfield_offset id name pos carrier (sizeof_ikind carrier_ikind);
Hashtbl.add bitfield_table
(id, name)
{bf_carrier = carrier; bf_carrier_typ = carrier_typ;
diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml
index 254f6fed..c81fd498 100644
--- a/cparser/Cleanup.ml
+++ b/cparser/Cleanup.ml
@@ -184,6 +184,11 @@ let saturate p =
(* Remove unreferenced definitions *)
+let remove_unused_debug = function
+ | Gdecl (_,id,_,_) -> Debug.remove_unused id
+ | Gfundef f -> Debug.remove_unused f.fd_name
+ | _ -> ()
+
let rec simpl_globdecls accu = function
| [] -> accu
| g :: rem ->
@@ -199,7 +204,7 @@ let rec simpl_globdecls accu = function
| Gpragma s -> true in
if need
then simpl_globdecls (g :: accu) rem
- else simpl_globdecls accu rem
+ else begin remove_unused_debug g.gdesc; simpl_globdecls accu rem end
let program p =
referenced := IdentSet.empty;
diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml
index 4ceaa016..1af5af1e 100644
--- a/cparser/Cprint.ml
+++ b/cparser/Cprint.ml
@@ -20,6 +20,8 @@ open C
let print_idents_in_full = ref false
+let print_debug_idents = ref false
+
let print_line_numbers = ref false
let location pp (file, lineno) =
@@ -27,7 +29,9 @@ let location pp (file, lineno) =
fprintf pp "# %d \"%s\"@ " lineno file
let ident pp i =
- if !print_idents_in_full
+ if !print_debug_idents
+ then fprintf pp "$%d" i.stamp
+ else if !print_idents_in_full
then fprintf pp "%s$%d" i.name i.stamp
else fprintf pp "%s" i.name
diff --git a/cparser/Cprint.mli b/cparser/Cprint.mli
index d63e341c..349b5f9a 100644
--- a/cparser/Cprint.mli
+++ b/cparser/Cprint.mli
@@ -15,6 +15,7 @@
val print_idents_in_full : bool ref
val print_line_numbers : bool ref
+val print_debug_idents : bool ref
val location : Format.formatter -> C.location -> unit
val attributes : Format.formatter -> C.attributes -> unit
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index a3c05c34..90bbfe5a 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -427,7 +427,6 @@ let sizeof_union env members =
We lay out fields consecutively, inserting padding to preserve
their alignment.
Not done here but in composite_info_decl: rounding size to alignment. *)
-
let sizeof_struct env members =
let rec sizeof_rec ofs = function
| [] ->
@@ -449,6 +448,26 @@ let sizeof_struct env members =
end
in sizeof_rec 0 members
+(* Simplified version to compute offsets on structs without bitfields *)
+let struct_layout env members =
+ let rec struct_layout_rec mem ofs = function
+ | [] ->
+ mem
+ | [ { fld_typ = TArray(_, None, _) } as m ] ->
+ (* C99: ty[] allowed as last field *)
+ begin match alignof env m.fld_typ with
+ | Some a -> ( m.fld_name,align ofs a)::mem
+ | None -> []
+ end
+ | m :: rem ->
+ match alignof env m.fld_typ, sizeof env m.fld_typ with
+ | Some a, Some s ->
+ let offset = align ofs a in
+ struct_layout_rec ((m.fld_name,offset)::mem) (offset + s) rem
+ | _, _ -> []
+ in struct_layout_rec [] 0 members
+
+
(* Determine whether a type is incomplete *)
let incomplete_type env t =
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index b1f77944..b9879339 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -105,6 +105,8 @@ val composite_info_decl:
Env.t -> struct_or_union -> attributes -> Env.composite_info
val composite_info_def:
Env.t -> struct_or_union -> attributes -> field list -> Env.composite_info
+val struct_layout:
+ Env.t -> field list -> (string * int) list
(* Type classification functions *)
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 6a238572..e81e6139 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -56,9 +56,11 @@ let elab_loc l = (l.filename, l.lineno)
let top_declarations = ref ([] : globdecl list)
-let emit_elab loc td =
+let emit_elab ?(enter:bool=true) env loc td =
let loc = elab_loc loc in
- top_declarations := { gdesc = td; gloc = loc } :: !top_declarations
+ let dec ={ gdesc = td; gloc = loc } in
+ if enter then Debug.insert_global_declaration env dec;
+ top_declarations := dec :: !top_declarations
let reset() = top_declarations := []
@@ -730,7 +732,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env =
(* finishing the definition of an incomplete struct or union *)
let (ci', env') = elab_struct_or_union_info kind loc env members attrs in
(* Emit a global definition for it *)
- emit_elab loc (Gcompositedef(kind, tag', attrs, ci'.ci_members));
+ emit_elab env' loc (Gcompositedef(kind, tag', attrs, ci'.ci_members));
(* Replace infos but keep same ident *)
(tag', Env.add_composite env' tag' ci')
| Some(tag', {ci_sizeof = Some _}), Some _
@@ -745,7 +747,7 @@ and elab_struct_or_union only kind loc tag optmembers attrs env =
(* enter it with a new name *)
let (tag', env') = Env.enter_composite env tag ci in
(* emit it *)
- emit_elab loc (Gcompositedecl(kind, tag', attrs));
+ emit_elab env' loc (Gcompositedecl(kind, tag', attrs));
(tag', env')
| _, Some members ->
(* definition of a complete struct or union *)
@@ -753,12 +755,12 @@ and elab_struct_or_union only kind loc tag optmembers attrs env =
(* enter it, incomplete, with a new name *)
let (tag', env') = Env.enter_composite env tag ci1 in
(* emit a declaration so that inner structs and unions can refer to it *)
- emit_elab loc (Gcompositedecl(kind, tag', attrs));
+ emit_elab env' loc (Gcompositedecl(kind, tag', attrs));
(* elaborate the members *)
let (ci2, env'') =
elab_struct_or_union_info kind loc env' members attrs in
(* emit a definition *)
- emit_elab loc (Gcompositedef(kind, tag', attrs, ci2.ci_members));
+ emit_elab env'' loc (Gcompositedef(kind, tag', attrs, ci2.ci_members));
(* Replace infos but keep same ident *)
(tag', Env.add_composite env'' tag' ci2)
@@ -809,7 +811,7 @@ and elab_enum only loc tag optmembers attrs env =
let (dcls, env') = elab_members env 0L members in
let info = { ei_members = dcls; ei_attr = attrs } in
let (tag', env'') = Env.enter_enum env' tag info in
- emit_elab loc (Genumdef(tag', attrs, dcls));
+ emit_elab env' loc (Genumdef(tag', attrs, dcls));
(tag', env'')
(* Elaboration of a naked type, e.g. in a cast *)
@@ -1312,7 +1314,7 @@ let elab_expr loc env a =
let ty = TFun(TInt(IInt, []), None, false, []) in
(* Emit an extern declaration for it *)
let id = Env.fresh_ident n in
- emit_elab loc (Gdecl(Storage_extern, id, ty, None));
+ emit_elab env loc (Gdecl(Storage_extern, id, ty, None));
{ edesc = EVar id; etyp = ty }
| _ -> elab a1 in
let bl = List.map elab al in
@@ -1789,7 +1791,7 @@ let enter_typedefs loc env sto dl =
if redef Env.lookup_ident env s then
error loc "redefinition of identifier '%s' as different kind of symbol" s;
let (id, env') = Env.enter_typedef env s ty in
- emit_elab loc (Gtypedef(id, ty));
+ emit_elab env loc (Gtypedef(id, ty));
env') env dl
let enter_or_refine_ident local loc env s sto ty =
@@ -1865,7 +1867,7 @@ let enter_decdefs local loc env sto dl =
((sto', id, ty', init') :: decls, env2)
else begin
(* Global definition *)
- emit_elab loc (Gdecl(sto', id, ty', init'));
+ emit_elab env2 loc (Gdecl(sto', id, ty', init'));
(decls, env2)
end in
let (decls, env') = List.fold_left enter_decdef ([], env) dl in
@@ -1899,7 +1901,7 @@ let elab_fundef env spec name body loc =
let (func_ty, func_init) = __func__type_and_init s in
let (func_id, _, env3,func_ty) =
enter_or_refine_ident true loc env2 "__func__" Storage_static func_ty in
- emit_elab loc (Gdecl(Storage_static, func_id, func_ty, Some func_init));
+ emit_elab ~enter:false env3 loc (Gdecl(Storage_static, func_id, func_ty, Some func_init));
(* Elaborate function body *)
let body' = !elab_funbody_f ty_ret env3 body in
(* Special treatment of the "main" function *)
@@ -1925,7 +1927,7 @@ let elab_fundef env spec name body loc =
fd_vararg = vararg;
fd_locals = [];
fd_body = body'' } in
- emit_elab loc (Gfundef fn);
+ emit_elab env1 loc (Gfundef fn);
env1
let elab_kr_fundef env spec name params defs body loc =
@@ -1997,7 +1999,7 @@ let rec elab_definition (local: bool) (env: Env.t) (def: Cabs.definition)
(* pragma *)
| PRAGMA(s, loc) ->
- emit_elab loc (Gpragma s);
+ emit_elab env loc (Gpragma s);
([], env)
and elab_definitions local env = function
@@ -2224,7 +2226,9 @@ and elab_block_body env ctx sl =
| DEFINITION def :: sl1 ->
let (dcl, env') = elab_definition true env def in
let loc = elab_loc (get_definitionloc def) in
- List.map (fun d -> {sdesc = Sdecl d; sloc = loc}) dcl
+ List.map (fun ((sto,id,ty,_) as d) ->
+ Debug.insert_local_declaration sto id ty loc;
+ {sdesc = Sdecl d; sloc = loc}) dcl
@ elab_block_body env' ctx sl1
| s :: sl1 ->
let s' = elab_stmt env ctx s in
diff --git a/cparser/Parse.ml b/cparser/Parse.ml
index 47698f8d..cfa95688 100644
--- a/cparser/Parse.ml
+++ b/cparser/Parse.ml
@@ -24,12 +24,7 @@ let transform_program t p name =
(run_pass Unblock.program 'b'
(run_pass Bitfields.program 'f'
p)))) in
- let debug =
- if !Clflags.option_g && Configuration.advanced_debug then
- Some (CtoDwarf.program_to_dwarf p p1 name)
- else
- None in
- (Rename.program p1 (Filename.chop_suffix name ".c")),debug
+ (Rename.program p1 (Filename.chop_suffix name ".c"))
let parse_transformations s =
let t = ref CharSet.empty in
@@ -46,7 +41,7 @@ let parse_transformations s =
let preprocessed_file transfs name sourcefile =
Cerrors.reset();
let ic = open_in sourcefile in
- let p,d =
+ let p =
try
let t = parse_transformations transfs in
let rec inf = Datatypes.S inf in
@@ -69,6 +64,6 @@ let preprocessed_file transfs name sourcefile =
Timing.time2 "Emulations" transform_program t p1 name
with
| Cerrors.Abort ->
- [],None in
+ [] in
close_in ic;
- if Cerrors.check_errors() then None,None else Some p,d
+ if Cerrors.check_errors() then None else Some p
diff --git a/cparser/Parse.mli b/cparser/Parse.mli
index ac8feb70..58c3cfb9 100644
--- a/cparser/Parse.mli
+++ b/cparser/Parse.mli
@@ -15,7 +15,7 @@
(* Entry point for the library: parse, elaborate, and transform *)
-val preprocessed_file: string -> string -> string -> C.program option * DwarfTypes.dw_entry option
+val preprocessed_file: string -> string -> string -> C.program option
(* first arg: desired transformations
second arg: source file name before preprocessing
diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
index 91f50552..c6646b5c 100644
--- a/cparser/Unblock.ml
+++ b/cparser/Unblock.ml
@@ -177,16 +177,89 @@ and expand_init islocal env i =
in
expand i
+(* Insertion of debug annotation, for -g mode *)
+
+let debug_id = Env.fresh_ident "__builtin_debug"
+let debug_ty =
+ TFun(TVoid [], Some [Env.fresh_ident "kind", TInt(IInt, [])], true, [])
+
+let debug_annot kind args =
+ { sloc = no_loc;
+ sdesc = Sdo {
+ etyp = TVoid [];
+ edesc = ECall({edesc = EVar debug_id; etyp = debug_ty},
+ intconst kind IInt :: args)
+ }
+ }
+
+let string_const str =
+ let c = CStr str in { edesc = EConst c; etyp = type_of_constant c }
+
+let integer_const n =
+ intconst (Int64.of_int n) IInt
+
+(* Line number annotation:
+ __builtin_debug(1, "#line:filename:lineno") *)
+(* TODO: consider
+ __builtin_debug(1, "filename", lineno)
+ instead. *)
+
+let debug_lineno (filename, lineno) =
+ debug_annot 1L
+ [string_const (Printf.sprintf "#line:%s:%d" filename lineno)]
+
+(* Scope annotation:
+ __builtin_debug(6, "", scope1, scope2, ..., scopeN)
+*)
+
+let empty_string = string_const ""
+
+let curr_fun_id = ref 0
+
+let debug_var_decl ctx id =
+ Debug.add_lvar_scope !curr_fun_id id (List.hd ctx)
+
+let debug_scope ctx =
+ debug_annot 6L (empty_string :: List.rev_map integer_const ctx)
+
+(* Add line number debug annotation if the line number changes.
+ Add scope debug annotation regardless. *)
+
+
+let add_lineno ctx prev_loc this_loc s =
+ if !Clflags.option_g then
+ sseq no_loc (debug_scope ctx)
+ (if this_loc <> prev_loc && this_loc <> no_loc
+ then sseq no_loc (debug_lineno this_loc) s
+ else s)
+ else s
+
+(* Generate fresh scope identifiers, for blocks that contain at least
+ one declaration *)
+
+let block_contains_decl sl =
+ List.exists
+ (function {sdesc = Sdecl _} -> true | _ -> false)
+ sl
+
+let next_scope_id = ref 0
+
+let new_scope_id () =
+ incr next_scope_id; !next_scope_id
+
(* Process a block-scoped variable declaration.
The variable is entered in [local_variables].
The initializer, if any, is converted into assignments and
prepended to [k]. *)
-let process_decl loc env (sto, id, ty, optinit) k =
+let process_decl loc env ctx (sto, id, ty, optinit) k =
let ty' = remove_const env ty in
local_variables := (sto, id, ty', None) :: !local_variables;
+ debug_var_decl ctx id;
+ (* TODO: register the fact that id is declared in scope ctx *)
match optinit with
- | None -> k
+ | None ->
+ k
| Some init ->
let init' = expand_init true env init in
let l = local_initializer env { edesc = EVar id; etyp = ty' } init' [] in
@@ -194,57 +267,90 @@ let process_decl loc env (sto, id, ty, optinit) k =
(* Simplification of blocks within a statement *)
-let rec unblock_stmt env s =
+let rec unblock_stmt env ctx ploc s =
match s.sdesc with
| Sskip -> s
| Sdo e ->
- {s with sdesc = Sdo(expand_expr true env e)}
+ add_lineno ctx ploc s.sloc
+ {s with sdesc = Sdo(expand_expr true env e)}
| Sseq(s1, s2) ->
- {s with sdesc = Sseq(unblock_stmt env s1, unblock_stmt env s2)}
+ {s with sdesc = Sseq(unblock_stmt env ctx ploc s1,
+ unblock_stmt env ctx s1.sloc s2)}
| Sif(e, s1, s2) ->
- {s with sdesc = Sif(expand_expr true env e,
- unblock_stmt env s1, unblock_stmt env s2)}
+ add_lineno ctx ploc s.sloc
+ {s with sdesc = Sif(expand_expr true env e,
+ unblock_stmt env ctx s.sloc s1,
+ unblock_stmt env ctx s.sloc s2)}
| Swhile(e, s1) ->
- {s with sdesc = Swhile(expand_expr true env e, unblock_stmt env s1)}
+ add_lineno ctx ploc s.sloc
+ {s with sdesc = Swhile(expand_expr true env e,
+ unblock_stmt env ctx s.sloc s1)}
| Sdowhile(s1, e) ->
- {s with sdesc = Sdowhile(unblock_stmt env s1, expand_expr true env e)}
+ add_lineno ctx ploc s.sloc
+ {s with sdesc = Sdowhile(unblock_stmt env ctx s.sloc s1,
+ expand_expr true env e)}
| Sfor(s1, e, s2, s3) ->
- {s with sdesc = Sfor(unblock_stmt env s1,
- expand_expr true env e,
- unblock_stmt env s2,
- unblock_stmt env s3)}
+ add_lineno ctx ploc s.sloc
+ {s with sdesc = Sfor(unblock_stmt env ctx s.sloc s1,
+ expand_expr true env e,
+ unblock_stmt env ctx s.sloc s2,
+ unblock_stmt env ctx s.sloc s3)}
| Sbreak -> s
| Scontinue -> s
| Sswitch(e, s1) ->
- {s with sdesc = Sswitch(expand_expr true env e, unblock_stmt env s1)}
+ add_lineno ctx ploc s.sloc
+ {s with sdesc = Sswitch(expand_expr true env e,
+ unblock_stmt env ctx s.sloc s1)}
| Slabeled(lbl, s1) ->
- {s with sdesc = Slabeled(lbl, unblock_stmt env s1)}
- | Sgoto lbl -> s
- | Sreturn None -> s
+ add_lineno ctx ploc s.sloc
+ {s with sdesc = Slabeled(lbl, unblock_stmt env ctx s.sloc s1)}
+ | Sgoto lbl ->
+ add_lineno ctx ploc s.sloc s
+ | Sreturn None ->
+ add_lineno ctx ploc s.sloc s
| Sreturn (Some e) ->
- {s with sdesc = Sreturn(Some (expand_expr true env e))}
- | Sblock sl -> unblock_block env sl
- | Sdecl d -> assert false
+ add_lineno ctx ploc s.sloc
+ {s with sdesc = Sreturn(Some (expand_expr true env e))}
+ | Sblock sl ->
+ let ctx' =
+ if block_contains_decl sl
+ then
+ let id = new_scope_id () in
+ (match ctx with
+ | [] -> Debug.enter_function_scope !curr_fun_id id
+ | a::_ -> Debug.enter_scope !curr_fun_id a id);
+ id:: ctx
+ else ctx in
+ unblock_block env ctx' ploc sl
+ | Sdecl d ->
+ assert false
| Sasm(attr, template, outputs, inputs, clob) ->
let expand_asm_operand (lbl, cstr, e) =
(lbl, cstr, expand_expr true env e) in
- {s with sdesc = Sasm(attr, template,
- List.map expand_asm_operand outputs,
- List.map expand_asm_operand inputs, clob)}
+ add_lineno ctx ploc s.sloc
+ {s with sdesc = Sasm(attr, template,
+ List.map expand_asm_operand outputs,
+ List.map expand_asm_operand inputs, clob)}
-and unblock_block env = function
+and unblock_block env ctx ploc = function
| [] -> sskip
| {sdesc = Sdecl d; sloc = loc} :: sl ->
- process_decl loc env d (unblock_block env sl)
+ add_lineno ctx ploc loc
+ (process_decl loc env ctx d
+ (unblock_block env ctx loc sl))
| s :: sl ->
- sseq s.sloc (unblock_stmt env s) (unblock_block env sl)
+ sseq s.sloc (unblock_stmt env ctx ploc s)
+ (unblock_block env ctx s.sloc sl)
(* Simplification of blocks and compound literals within a function *)
let unblock_fundef env f =
local_variables := [];
- let body = unblock_stmt env f.fd_body in
+ next_scope_id := 0;
+ curr_fun_id:= f.fd_name.stamp;
+ (* TODO: register the parameters as being declared in function scope *)
+ let body = unblock_stmt env [] no_loc f.fd_body in
let decls = !local_variables in
local_variables := [];
{ f with fd_locals = f.fd_locals @ decls; fd_body = body }
@@ -299,4 +405,5 @@ let rec unblock_glob env accu = function
(* Entry point *)
let program p =
+ {gloc = no_loc; gdesc = Gdecl(Storage_extern, debug_id, debug_ty, None)} ::
unblock_glob (Builtins.environment()) [] p