diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-08-23 14:28:29 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-08-23 14:28:29 +0200 |
| commit | 095ec29088ede2c5ca7db813d56001efb63aa97e (patch) | |
| tree | 12783d01cde7b851812ade989b0f37d50bee0227 /backend/PrintAsmaux.ml | |
| parent | 33dfbe7601ad16fcea5377563fa7ceb4053cb85a (diff) | |
| download | compcert-kvx-095ec29088ede2c5ca7db813d56001efb63aa97e.tar.gz compcert-kvx-095ec29088ede2c5ca7db813d56001efb63aa97e.zip | |
Track the locations of local variables using EF_debug annotations.
SimplLocals:
- record locations of stack-allocated variables with annotations
(of kind 5) at the beginning of the function;
- mark every assignment to non-stack-allocated variables with an
annotation of kind 2.
Debugvar: (new pass!)
- perform availability analysis for debug annotations of kind 2
- insert "start of live range" and "end of live range" annotations
(kind 3 and 4) to delimit intervals of PCs where the location
of a local variable is known.
Diffstat (limited to 'backend/PrintAsmaux.ml')
| -rw-r--r-- | backend/PrintAsmaux.ml | 28 |
1 files changed, 20 insertions, 8 deletions
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 883b5477..67e53aea 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -263,16 +263,28 @@ let print_annot_text print_preg sp_reg_name oc txt args = let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$" let print_debug_info comment print_line print_preg sp_name oc kind txt args = - if kind = 1 && Str.string_match re_file_line txt 0 then begin - print_line oc (Str.matched_group 1 txt) - (int_of_string (Str.matched_group 2 txt)) - end else begin - fprintf oc "%s debug%d: %s" comment kind txt; + let print_debug_args oc args = List.iter (fun a -> fprintf oc " %a" (print_annot print_preg sp_name) a) - args; - fprintf oc "\n" - end + args in + match kind with + | 1 -> (* line number *) + 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)) + | 2 -> (* assignment to local variable, not useful *) + () + | 3 -> (* beginning of live range for local variable *) + fprintf oc "%s debug: start live range %s =%a\n" + comment txt print_debug_args args + | 4 -> (* end of live range for local variable *) + fprintf oc "%s debug: end live range %s\n" + comment txt + | 5 -> (* local variable preallocated in stack *) + fprintf oc "%s debug: %s resides at%a\n" + comment txt print_debug_args args + | _ -> + () (** Inline assembly *) |