diff options
author | Xavier Leroy <xavier.leroy@gmail.com> | 2015-09-20 15:23:38 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@gmail.com> | 2015-09-20 15:23:38 +0200 |
commit | 9147350fdb47f3471ce6d9202b7c996f79ffab2d (patch) | |
tree | f47977b33fa0975d614cc9bc2e4a22c996a96401 | |
parent | db0a62a01bbf90617701b68917319767159bf039 (diff) | |
download | compcert-9147350fdb47f3471ce6d9202b7c996f79ffab2d.tar.gz compcert-9147350fdb47f3471ce6d9202b7c996f79ffab2d.zip |
Experiment: track the scopes of local variables via __builtin_debug.
C2C: the code that insert debug builtins with the line numbers is now
in Unblock. Handle calls to __builtin_debug.
Unblock: generate __builtin_debug(1) for line numbers, carrying
the list of active scopes as extra arguments.
Generate __builtin_debug(6) for local variable declarations,
carrying the corresponding scope number as extra argument.
Constprop: avoid duplicating debug arguments that are constants already.
PrintAsmaux: show this extra debug info as comments.
-rw-r--r-- | backend/Constprop.v | 6 | ||||
-rw-r--r-- | backend/Constpropproof.v | 6 | ||||
-rw-r--r-- | backend/PrintAsmaux.ml | 5 | ||||
-rw-r--r-- | cfrontend/C2C.ml | 74 | ||||
-rw-r--r-- | cparser/Unblock.ml | 164 |
5 files changed, 181 insertions, 74 deletions
diff --git a/backend/Constprop.v b/backend/Constprop.v index cd844d30..8f4cb76d 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -144,9 +144,9 @@ Fixpoint debug_strength_reduction (ae: AE.t) (al: list (builtin_arg reg)) := | a :: al => let a' := builtin_arg_reduction ae a in let al' := a :: debug_strength_reduction ae al in - match a' with - | BA_int _ | BA_long _ | BA_float _ | BA_single _ => a' :: al' - | _ => al' + match a, a' with + | BA _, (BA_int _ | BA_long _ | BA_float _ | BA_single _) => a' :: al' + | _, _ => al' end end. diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index d9005f5e..eafefed5 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -243,7 +243,11 @@ Proof. induction 2; simpl. - exists (@nil val); constructor. - destruct IHlist_forall2 as (vl' & A). - destruct (builtin_arg_reduction ae a1); repeat (eauto; econstructor). + assert (eval_builtin_args ge (fun r => rs#r) sp m + (a1 :: debug_strength_reduction ae al) (b1 :: vl')) + by (constructor; eauto). + destruct a1; try (econstructor; eassumption). + destruct (builtin_arg_reduction ae (BA x)); repeat (eauto; econstructor). Qed. Lemma builtin_strength_reduction_correct: diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 67e53aea..13daa644 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -269,6 +269,8 @@ 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)) @@ -283,6 +285,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 | _ -> () diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 5cd5997d..f5e550f3 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -741,6 +741,22 @@ let rec convertExpr env e = | C.ECompound(ty1, ie) -> unsupported "compound literals"; ezero + | C.ECall({edesc = C.EVar {name = "__builtin_debug"}}, args) -> + let (kind, args1) = + match args with + | {edesc = C.EConst(CInt(n,_,_))} :: args1 -> (n, args1) + | _ -> error "ill_formed __builtin_debug"; (0L, args) in + let (text, args2) = + match args1 with + | {edesc = C.EConst(CStr(txt))} :: args2 -> (txt, args2) + | {edesc = C.EVar id} :: args2 -> (id.name, args2) + | _ -> error "ill_formed __builtin_debug"; ("", args1) in + let targs2 = convertTypArgs env [] args2 in + Ebuiltin( + EF_debug(P.of_int64 kind, intern_string text, + typlist_of_typelist targs2), + targs2, convertExprList env args2, convertTyp env e.etyp) + | C.ECall({edesc = C.EVar {name = "__builtin_annot"}}, args) -> begin match args with | {edesc = C.EConst(CStr txt)} :: args1 -> @@ -922,16 +938,6 @@ let rec contains_case s = (** Annotations for line numbers *) -let add_lineno prev_loc this_loc s = - if !Clflags.option_g && prev_loc <> this_loc && this_loc <> Cutil.no_loc - then begin - let txt = sprintf "#line:%s:%d" (fst this_loc) (snd this_loc) in - Ssequence(Sdo(Ebuiltin(EF_debug(P.one, intern_string txt, []), - Tnil, Enil, Tvoid)), - s) - end else - s - (** Statements *) let swrap = function @@ -939,36 +945,31 @@ let swrap = function | Errors.Error msg -> error ("retyping error: " ^ string_of_errmsg msg); Sskip -let rec convertStmt ploc env s = +let rec convertStmt env s = updateLoc s.sloc; match s.sdesc with | C.Sskip -> Sskip | C.Sdo e -> - add_lineno ploc s.sloc (swrap (Ctyping.sdo (convertExpr env e))) + swrap (Ctyping.sdo (convertExpr env e)) | C.Sseq(s1, s2) -> - let s1' = convertStmt ploc env s1 in - let s2' = convertStmt s1.sloc env s2 in + let s1' = convertStmt env s1 in + let s2' = convertStmt env s2 in Ssequence(s1', s2') | C.Sif(e, s1, s2) -> let te = convertExpr env e in - add_lineno ploc s.sloc - (swrap (Ctyping.sifthenelse te - (convertStmt s.sloc env s1) (convertStmt s.sloc env s2))) + swrap (Ctyping.sifthenelse te (convertStmt env s1) (convertStmt env s2)) | C.Swhile(e, s1) -> let te = convertExpr env e in - add_lineno ploc s.sloc - (swrap (Ctyping.swhile te (convertStmt s.sloc env s1))) + swrap (Ctyping.swhile te (convertStmt env s1)) | C.Sdowhile(s1, e) -> let te = convertExpr env e in - add_lineno ploc s.sloc - (swrap (Ctyping.sdowhile te (convertStmt s.sloc env s1))) + swrap (Ctyping.sdowhile te (convertStmt env s1)) | C.Sfor(s1, e, s2, s3) -> let te = convertExpr env e in - add_lineno ploc s.sloc - (swrap (Ctyping.sfor - (convertStmt s.sloc env s1) te - (convertStmt s.sloc env s2) (convertStmt s.sloc env s3))) + swrap (Ctyping.sfor + (convertStmt env s1) te + (convertStmt env s2) (convertStmt env s3)) | C.Sbreak -> Sbreak | C.Scontinue -> @@ -981,22 +982,20 @@ let rec convertStmt ploc env s = contains_case init end; let te = convertExpr env e in - add_lineno ploc s.sloc - (swrap (Ctyping.sswitch te - (convertSwitch s.sloc env (is_longlong env e.etyp) cases))) + swrap (Ctyping.sswitch te + (convertSwitch env (is_longlong env e.etyp) cases)) | C.Slabeled(C.Slabel lbl, s1) -> - add_lineno ploc s.sloc - (Slabel(intern_string lbl, convertStmt s.sloc env s1)) + Slabel(intern_string lbl, convertStmt env s1) | C.Slabeled(C.Scase _, _) -> unsupported "'case' outside of 'switch'"; Sskip | C.Slabeled(C.Sdefault, _) -> unsupported "'default' outside of 'switch'"; Sskip | C.Sgoto lbl -> - add_lineno ploc s.sloc (Sgoto(intern_string lbl)) + Sgoto(intern_string lbl) | C.Sreturn None -> - add_lineno ploc s.sloc (Sreturn None) + Sreturn None | C.Sreturn(Some e) -> - add_lineno ploc s.sloc (Sreturn(Some(convertExpr env e))) + Sreturn(Some(convertExpr env e)) | C.Sblock _ -> unsupported "nested blocks"; Sskip | C.Sdecl _ -> @@ -1004,10 +1003,9 @@ let rec convertStmt ploc env s = | C.Sasm(attrs, txt, outputs, inputs, clobber) -> if not !Clflags.option_finline_asm then unsupported "inline 'asm' statement (consider adding option -finline-asm)"; - add_lineno ploc s.sloc - (Sdo (convertAsm s.sloc env txt outputs inputs clobber)) + Sdo (convertAsm s.sloc env txt outputs inputs clobber) -and convertSwitch ploc env is_64 = function +and convertSwitch env is_64 = function | [] -> LSnil | (lbl, s) :: rem -> @@ -1024,7 +1022,7 @@ and convertSwitch ploc env is_64 = function then Z.of_uint64 v else Z.of_uint32 (Int64.to_int32 v)) in - LScons(lbl', convertStmt ploc env s, convertSwitch s.sloc env is_64 rem) + LScons(lbl', convertStmt env s, convertSwitch env is_64 rem) (** Function definitions *) @@ -1049,7 +1047,7 @@ let convertFundef loc env fd = unsupported "initialized local variable"; (intern_string id.name, convertTyp env ty)) fd.fd_locals in - let body' = convertStmt loc env fd.fd_body in + let body' = convertStmt env fd.fd_body in let id' = intern_string fd.fd_name.name in Hashtbl.add decl_atom id' { a_storage = fd.fd_storage; diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index 91f50552..b5f945d4 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -177,74 +177,173 @@ 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", scope1, ..., scopeN) *) +(* TODO: consider + __builtin_debug(1, "filename", lineno, scope1, ..., scopeN) + instead. *) + +let debug_lineno ctx (filename, lineno) = + debug_annot 1L + (string_const (Printf.sprintf "#line:%s:%d" filename lineno) :: + List.rev_map integer_const ctx) + +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 + +(* Variable declaration annotation: + __builtin_debug(6, var, scope) *) + +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 add_var_decl ctx id ty s = + if !Clflags.option_g + then sseq no_loc (debug_var_decl ctx id ty) s + else s + +let add_param_decls params body = + 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 + +(* 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; - 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 + 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) (* 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 new_scope_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; + let body = + add_param_decls f.fd_params (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 +398,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 |