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.

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