diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-09-21 14:45:28 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-09-21 14:45:28 +0200 |
commit | d8aac95c8d1767bf3b10990599b0f32687994182 (patch) | |
tree | 1d883ab45812c372b6651423b43b9fd67b77e2fb | |
parent | 9147350fdb47f3471ce6d9202b7c996f79ffab2d (diff) | |
download | compcert-d8aac95c8d1767bf3b10990599b0f32687994182.tar.gz compcert-d8aac95c8d1767bf3b10990599b0f32687994182.zip |
Continuing experiment: track the scopes of local variables via __builtin_debug
As observed by B. Schommer, it is not enough to track scopes for every source line, as blocks can occur on a single line (think macros). Hence:
- Revert debug annotations of kind 1 to contain only line number info.
Generate them only when the line number changes.
- Use debug annotations of kind 6 to record the list of active scopes
(as BA_int integer arguments to __builtin_annot). Generate them
before every nontrivial statement, even if on the same line as others.
- Remove the generation of "variable x is declared in scope N" debug
annotations. This can be tracked separately and more efficiently.
-rw-r--r-- | backend/PrintAsmaux.ml | 8 | ||||
-rw-r--r-- | cparser/Unblock.ml | 62 |
2 files changed, 31 insertions, 39 deletions
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 13daa644..a67c85d2 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -269,8 +269,6 @@ let print_debug_info comment print_line print_preg sp_name oc kind txt args = args in match kind with | 1 -> (* line number *) - fprintf oc "%s debug: current scopes%a\n" - comment print_debug_args args; if Str.string_match re_file_line txt 0 then print_line oc (Str.matched_group 1 txt) (int_of_string (Str.matched_group 2 txt)) @@ -285,9 +283,9 @@ let print_debug_info comment print_line print_preg sp_name oc kind txt args = | 5 -> (* local variable preallocated in stack *) fprintf oc "%s debug: %s resides at%a\n" comment txt print_debug_args args - | 6 -> (* declaration of a local variable *) - fprintf oc "%s debug: %s declared in scope%a\n" - comment txt print_debug_args args + | 6 -> (* scope annotations *) + fprintf oc "%s debug: current scopes%a\n" + comment print_debug_args args; | _ -> () diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index b5f945d4..bad5002b 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -199,40 +199,34 @@ let integer_const n = intconst (Int64.of_int n) IInt (* Line number annotation: - __builtin_debug(1, "#line:filename:lineno", scope1, ..., scopeN) *) + __builtin_debug(1, "#line:filename:lineno") *) (* TODO: consider - __builtin_debug(1, "filename", lineno, scope1, ..., scopeN) + __builtin_debug(1, "filename", lineno) instead. *) -let debug_lineno ctx (filename, lineno) = +let debug_lineno (filename, lineno) = debug_annot 1L - (string_const (Printf.sprintf "#line:%s:%d" filename lineno) :: - List.rev_map integer_const ctx) + [string_const (Printf.sprintf "#line:%s:%d" filename lineno)] -let add_lineno ctx prev_loc this_loc s = - if !Clflags.option_g && this_loc <> prev_loc && this_loc <> no_loc - then sseq no_loc (debug_lineno ctx this_loc) s - else s +(* Scope annotation: + __builtin_debug(6, "", scope1, scope2, ..., scopeN) +*) -(* Variable declaration annotation: - __builtin_debug(6, var, scope) *) +let empty_string = string_const "" -let debug_var_decl ctx id ty = - let scope = match ctx with [] -> 0 | sc :: _ -> sc in - debug_annot 6L - [ {edesc = EVar id; etyp = ty}; integer_const scope ] +let debug_scope ctx = + debug_annot 6L (empty_string :: List.rev_map integer_const ctx) -let add_var_decl ctx id ty s = - if !Clflags.option_g - then sseq no_loc (debug_var_decl ctx id ty) s - else s +(* Add line number debug annotation if the line number changes. + Add scope debug annotation regardless. *) -let add_param_decls params body = +let add_lineno ctx prev_loc this_loc s = if !Clflags.option_g then - List.fold_right - (fun (id, ty) s -> sseq no_loc (debug_var_decl [] id ty) s) - params body - else body + 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 *) @@ -255,14 +249,14 @@ let new_scope_id () = 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; - add_var_decl ctx id ty - (match optinit with - | None -> - k - | Some init -> - let init' = expand_init true env init in - let l = local_initializer env { edesc = EVar id; etyp = ty' } init' [] in - add_inits_stmt loc l k) + (* TODO: register the fact that id is declared in scope ctx *) + match optinit with + | None -> + k + | Some init -> + let init' = expand_init true env init in + let l = local_initializer env { edesc = EVar id; etyp = ty' } init' [] in + add_inits_stmt loc l k (* Simplification of blocks within a statement *) @@ -342,8 +336,8 @@ and unblock_block env ctx ploc = function let unblock_fundef env f = local_variables := []; next_scope_id := 0; - let body = - add_param_decls f.fd_params (unblock_stmt env [] no_loc f.fd_body) in + (* 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 } |