Preliminary support for debugging info (-g).

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2253 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

9 files changed, 285 insertions, 49 deletions

diff --git a/Makefile b/Makefile
index 4da580c..d7a0fdd 100644
--- a/Makefile
+++ b/Makefile
@@ -208,6 +208,7 @@ driver/Configuration.ml: Makefile.config VERSION
          echo let variant = "\"$(VARIANT)\""; \
          echo let system = "\"$(SYSTEM)\""; \
          echo let has_runtime_lib = $(HAS_RUNTIME_LIB); \
+         echo let asm_supports_cfi = $(ASM_SUPPORTS_CFI); \
          version=`cat VERSION`; \
          echo let version = "\"$$version\"") \
         > driver/Configuration.ml
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 1d46416..fafd1d5 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -181,6 +181,53 @@ let emit_constants oc =
     symbol_labels;
   reset_constants ()
 
+(* Emit .file / .loc debugging directives *)
+
+let filename_num : (string, int) Hashtbl.t = Hashtbl.create 7
+
+let print_file_line oc file line =
+  if !Clflags.option_g && file <> "" then begin
+    let filenum = 
+      try
+        Hashtbl.find filename_num file
+      with Not_found ->
+        let n = Hashtbl.length filename_num + 1 in
+        Hashtbl.add filename_num file n;
+        fprintf oc "	.file	%d %S\n" n file;
+        n
+    in fprintf oc "	.loc	%d %s\n" filenum line
+  end
+
+let print_location oc loc =
+  if loc <> Cutil.no_loc then
+    print_file_line oc (fst loc) (string_of_int (snd loc))
+
+(* Emit .cfi directives *)
+
+let cfi_startproc oc =
+  if Configuration.asm_supports_cfi then
+    match config with
+    | Linux -> fprintf oc "	.cfi_startproc\n"
+    | Diab  -> assert false
+
+let cfi_endproc oc =
+  if Configuration.asm_supports_cfi then
+    match config with
+    | Linux -> fprintf oc "	.cfi_endproc\n"
+    | Diab  -> assert false
+
+let cfi_adjust oc delta =
+  if Configuration.asm_supports_cfi then
+    match config with
+    | Linux -> fprintf oc "	.cfi_adjust_cfa_offset	%ld\n" delta
+    | Diab  -> assert false
+
+let cfi_rel_offset oc reg ofs =
+  if Configuration.asm_supports_cfi then
+    match config with
+    | Linux -> fprintf oc "	.cfi_rel_offset	%s, %ld\n" reg ofs
+    | Diab  -> assert false
+
 (* Built-ins.  They come in two flavors: 
    - annotation statements: take their arguments in registers or stack
      locations; generate no code;
@@ -519,7 +566,12 @@ let print_instruction oc = function
   | Prsb(r1, r2, so) ->
       fprintf oc "	rsb	%a, %a, %a\n" ireg r1 ireg r2 shift_op so; 1
   | Pstr(r1, r2, sa) ->
-      fprintf oc "	str	%a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1
+      fprintf oc "	str	%a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa;
+      begin match r1, r2, sa with
+      | IR14, IR13, SAimm n -> cfi_rel_offset oc "lr" (camlint_of_coqint n)
+      | _ -> ()
+      end;
+      1
   | Pstrb(r1, r2, sa) ->
       fprintf oc "	strb	%a, [%a, %a]\n" ireg r1 ireg r2 shift_addr sa; 1
   | Pstrh(r1, r2, sa) ->
@@ -592,12 +644,14 @@ let print_instruction oc = function
            fprintf oc "	sub	sp, sp, #%a\n" coqint n;
            incr ninstr)
         (Asmgen.decompose_int sz);
+      cfi_adjust oc (camlint_of_coqint sz);
       fprintf oc "	str	r12, [sp, #%a]\n" coqint ofs;
       2 + !ninstr
   | Pfreeframe(sz, ofs) ->
       if Asmgen.is_immed_arith sz
       then fprintf oc "	add	sp, sp, #%a\n" coqint sz
       else fprintf oc "	ldr	sp, [sp, #%a]\n" coqint ofs;
+      cfi_adjust oc (Int32.neg (camlint_of_coqint sz));
       1
   | Plabel lbl ->
       fprintf oc "%a:\n" print_label lbl; 0
@@ -690,9 +744,12 @@ let print_function oc name fn =
   if not (C2C.atom_is_static name) then
     fprintf oc "	.global	%a\n" print_symb name;
   fprintf oc "%a:\n" print_symb name;
+  print_location oc (C2C.atom_location name);
+  cfi_startproc oc;
   ignore (fixup_arguments oc Incoming fn.fn_sig);
   print_instructions oc fn.fn_code;
   emit_constants oc;
+  cfi_endproc oc;
   fprintf oc "	.type	%a, %%function\n" print_symb name;
   fprintf oc "	.size	%a, . - %a\n" print_symb name print_symb name
 
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 34cb27a..c347aba 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -37,7 +37,8 @@ type atom_info =
     a_sections: Sections.section_name list; (* in which section to put it *)
       (* 1 section for data, 3 sections (code/lit/jumptbl) for functions *)
     a_small_data: bool;                (* data in a small data area? *)
-    a_inline: bool                     (* function declared inline? *)
+    a_inline: bool;                    (* function declared inline? *)
+    a_loc: location                    (* source location *)
 }
 
 let decl_atom : (AST.ident, atom_info) Hashtbl.t = Hashtbl.create 103
@@ -120,7 +121,8 @@ let name_for_string_literal env s =
         a_alignment = Some 1;
         a_sections = [Sections.for_stringlit()];
         a_small_data = false;
-        a_inline = false };
+        a_inline = false;
+        a_loc = Cutil.no_loc };
     Hashtbl.add stringTable s id;
     id
 
@@ -634,29 +636,44 @@ let rec groupSwitch = function
       let (fst, cases) = groupSwitch rem in
       (Cutil.sseq s.sloc s fst, cases)
 
-(* Statement *)
+(** Annotations for line numbers *)
 
-let rec convertStmt env s =
+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_annot(intern_string txt, []),
+                            Tnil, Enil, Tvoid)),
+               s)
+  end else
+    s
+
+(** Statements *)
+
+let rec convertStmt ploc env s =
   updateLoc s.sloc;
   match s.sdesc with
   | C.Sskip ->
       Sskip
   | C.Sdo e ->
-      Sdo(convertExpr env e)
+      add_lineno ploc s.sloc (Sdo(convertExpr env e))
   | C.Sseq(s1, s2) ->
-      Ssequence(convertStmt env s1, convertStmt env s2)
+      Ssequence(convertStmt ploc env s1, convertStmt s1.sloc env s2)
   | C.Sif(e, s1, s2) ->
       let te = convertExpr env e in
-      Sifthenelse(te, convertStmt env s1, convertStmt env s2)
+      add_lineno ploc s.sloc 
+        (Sifthenelse(te, convertStmt s.sloc env s1, convertStmt s.sloc env s2))
   | C.Swhile(e, s1) ->
       let te = convertExpr env e in
-      Swhile(te, convertStmt env s1)
+      add_lineno ploc s.sloc (Swhile(te, convertStmt s.sloc env s1))
   | C.Sdowhile(s1, e) ->
       let te = convertExpr env e in
-      Sdowhile(te, convertStmt env s1)
+      add_lineno ploc s.sloc (Sdowhile(te, convertStmt s.sloc env s1))
   | C.Sfor(s1, e, s2, s3) ->
       let te = convertExpr env e in
-      Sfor(convertStmt env s1, te, convertStmt env s2, convertStmt env s3)
+      add_lineno ploc s.sloc
+        (Sfor(convertStmt s.sloc env s1, te,
+              convertStmt s.sloc env s2, convertStmt s.sloc env s3))
   | C.Sbreak ->
       Sbreak
   | C.Scontinue ->
@@ -668,19 +685,20 @@ let rec convertStmt env s =
       if init.sdesc <> C.Sskip then
         warning "ignored code at beginning of 'switch'";
       let te = convertExpr env e in
-      Sswitch(te, convertSwitch env cases)
+      add_lineno ploc s.sloc (Sswitch(te, convertSwitch s.sloc env cases))
   | C.Slabeled(C.Slabel lbl, s1) ->
-      Slabel(intern_string lbl, convertStmt env s1)
+      add_lineno ploc s.sloc
+        (Slabel(intern_string lbl, convertStmt s.sloc 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 ->
-      Sgoto(intern_string lbl)
+      add_lineno ploc s.sloc (Sgoto(intern_string lbl))
   | C.Sreturn None ->
-      Sreturn None
+      add_lineno ploc s.sloc (Sreturn None)
   | C.Sreturn(Some e) ->
-      Sreturn(Some(convertExpr env e))
+      add_lineno ploc s.sloc (Sreturn(Some(convertExpr env e)))
   | C.Sblock _ ->
       unsupported "nested blocks"; Sskip
   | C.Sdecl _ ->
@@ -688,13 +706,14 @@ let rec convertStmt env s =
   | C.Sasm txt ->
       if not !Clflags.option_finline_asm then
         unsupported "inline 'asm' statement (consider adding option -finline-asm)";
-      Sdo (Ebuiltin (EF_inline_asm (intern_string txt), Tnil, Enil, Tvoid))
+      add_lineno ploc s.sloc
+        (Sdo (Ebuiltin (EF_inline_asm (intern_string txt), Tnil, Enil, Tvoid)))
 
-and convertSwitch env = function
+and convertSwitch ploc env = function
   | [] ->
       LSdefault Sskip
   | [Default, s] ->
-      LSdefault (convertStmt env s)
+      LSdefault (convertStmt ploc env s)
   | (Default, s) :: _ ->
       updateLoc s.sloc;
       unsupported "'default' case must occur last";
@@ -706,12 +725,12 @@ and convertSwitch env = function
         | None -> unsupported "'case' label is not a compile-time integer"; 0L
         | Some v -> v in
       LScase(convertInt v,
-             convertStmt env s,
-             convertSwitch env rem)
+             convertStmt ploc env s,
+             convertSwitch s.sloc env rem)
 
 (** Function definitions *)
 
-let convertFundef env fd =
+let convertFundef loc env fd =
   if Cutil.is_composite_type env fd.fd_ret then
     unsupported "function returning a struct or union";
   let ret =
@@ -730,14 +749,15 @@ let convertFundef env fd =
           unsupported "initialized local variable";
         (intern_string id.name, convertTyp env ty))
       fd.fd_locals in
-  let body' = convertStmt env fd.fd_body in
+  let body' = convertStmt loc env fd.fd_body in
   let id' = intern_string fd.fd_name.name in
   Hashtbl.add decl_atom id'
     { a_storage = fd.fd_storage;
       a_alignment = None;
       a_sections = Sections.for_function env id' fd.fd_ret;
       a_small_data = false;
-      a_inline = fd.fd_inline };
+      a_inline = fd.fd_inline;
+      a_loc = loc };
   (id', Gfun(Internal {fn_return = ret; fn_params = params;
                        fn_vars = vars; fn_body = body'}))
 
@@ -793,7 +813,7 @@ let convertInitializer env ty i =
 
 (** Global variable *)
 
-let convertGlobvar env (sto, id, ty, optinit) =
+let convertGlobvar loc env (sto, id, ty, optinit) =
   let id' = intern_string id.name in
   let ty' = convertTyp env ty in 
   let sz = Ctypes.sizeof ty' in
@@ -818,7 +838,8 @@ let convertGlobvar env (sto, id, ty, optinit) =
       a_alignment = align;
       a_sections = [section];
       a_small_data = near_access;
-      a_inline = false };
+      a_inline = false;
+      a_loc = loc };
   let volatile = List.mem C.AVolatile attr in
   let readonly = List.mem C.AConst attr && not volatile in
   (id', Gvar {gvar_info = ty'; gvar_init = init';
@@ -858,10 +879,10 @@ let rec convertGlobdecls env res gl =
           | TFun(_, _, true, _) ->
               convertGlobdecls env res gl'
           | _ ->
-              convertGlobdecls env (convertGlobvar env d :: res) gl'
+              convertGlobdecls env (convertGlobvar g.gloc env d :: res) gl'
           end
       | C.Gfundef fd ->
-          convertGlobdecls env (convertFundef env fd :: res) gl'
+          convertGlobdecls env (convertFundef g.gloc env fd :: res) gl'
       | C.Gcompositedecl _ | C.Gtypedef _ | C.Genumdef _ ->
           (* typedefs are unrolled, structs are expanded inline, and
              enum tags are folded.  So we just skip their declarations. *)
@@ -1008,3 +1029,9 @@ let atom_is_inline a =
     (Hashtbl.find decl_atom a).a_inline
   with Not_found ->
     false
+
+let atom_location a =
+  try
+    (Hashtbl.find decl_atom a).a_loc
+  with Not_found ->
+    Cutil.no_loc
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index f91dca6..897a2ee 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -242,11 +242,11 @@ let rec expr p (prec, e) =
                 (camlint_of_coqint sz) (camlint_of_coqint al)
                 exprlist (true, args)
   | Ebuiltin(EF_annot(txt, _), _, args, _) ->
-      fprintf p "__builtin_annot@[<hov 1>(%S,@ %a)@]"
-                (extern_atom txt) exprlist (true, args)
+      fprintf p "__builtin_annot@[<hov 1>(%S%a)@]"
+                (extern_atom txt) exprlist (false, args)
   | Ebuiltin(EF_annot_val(txt, _), _, args, _) ->
-      fprintf p "__builtin_annot_val@[<hov 1>(%S,@ %a)@]"
-                (extern_atom txt) exprlist (true, args)
+      fprintf p "__builtin_annot_val@[<hov 1>(%S%a)@]"
+                (extern_atom txt) exprlist (false, args)
   | Ebuiltin(_, _, args, _) ->
       fprintf p "<unknown builtin>@[<hov 1>(%a)@]" exprlist (true, args)
   | Eparen(a1, ty) ->
diff --git a/configure b/configure
index f570dcf..68b643a 100755
--- a/configure
+++ b/configure
@@ -63,6 +63,8 @@ done
 
 cchecklink=false
 has_runtime_lib=true
+casmruntime=""
+asm_supports_cfi=""
 
 case "$target" in
   powerpc-linux|ppc-linux|powerpc-eabi|ppc-eabi)
@@ -83,6 +85,7 @@ case "$target" in
     cc="${toolprefix}dcc"
     cprepro="${toolprefix}dcc -E"
     casm="${toolprefix}das"
+    asm_supports_cfi=false
     clinker="${toolprefix}dcc"
     libmath="-lm"
     cchecklink=true;;
@@ -150,6 +153,27 @@ esac
 
 if test -z "$casmruntime"; then casmruntime="$casm"; fi
 
+# Test assembler support for CFI directives
+
+if test "$target" != "manual" && test -z "$asm_supports_cfi"; then
+  echo "Testing assembler support for CFI directives..."
+  f=/tmp/compcert-configure-$$.s
+  rm -f $f
+  cat >> $f <<EOF
+testfun:
+	.file 1 "testfun.c"
+	.loc 1 1
+	.cfi_startproc
+	.cfi_adjust_cfa_offset 16
+	.cfi_endproc
+EOF
+  if $casm -o /dev/null $f 2>/dev/null
+  then asm_supports_cfi=true
+  else asm_supports_cfi=false
+  fi
+  rm -f $f
+fi
+
 # Additional packages needed for cchecklink
 
 if $cchecklink; then
@@ -183,6 +207,7 @@ CLINKER=$clinker
 LIBMATH=$libmath
 HAS_RUNTIME_LIB=$has_runtime_lib
 CCHECKLINK=$cchecklink
+ASM_SUPPORTS_CFI=$asm_supports_cfi
 EOF
 else
 cat >> Makefile.config <<'EOF'
@@ -233,7 +258,13 @@ LIBMATH=-lm
 
 # Do not change
 HAS_RUNTIME_LIB=true
+
+# Whether the assembler $(CASM) supports .cfi debug directives
+ASM_SUPPORTS_CFI=false
+#ASM_SUPPORTS_CFI=true
+
 EOF
+
 fi
 
 # Summarize configuration
@@ -259,6 +290,7 @@ CompCert configuration:
     C compiler.................... $cc
     C preprocessor................ $cprepro
     Assembler..................... $casm
+    Assembler supports CFI........ $asm_supports_cfi
     Assembler for runtime lib..... $casmruntime
     Linker........................ $clinker
     Math library.................. $libmath
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index ea8e884..d70467a 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -40,6 +40,7 @@ let option_dalloctrace = ref false
 let option_dmach = ref false
 let option_dasm = ref false
 let option_sdump = ref false
+let option_g = ref false
 let option_o = ref (None: string option)
 let option_E = ref false
 let option_S = ref false
diff --git a/driver/Driver.ml b/driver/Driver.ml
index e029aa2..3d981f0 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -396,6 +396,12 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>) :
   -falign-branch-targets <n>  Set alignment (in bytes) of branch targets
   -falign-cond-branches <n>  Set alignment (in bytes) of conditional branches
   -Wa,<opt>      Pass option <opt> to the assembler
+Debugging options:
+  -g             Generate debugging information
+Linking options:
+  -l<lib>        Link library <lib>
+  -L<dir>        Add <dir> to search path for libraries
+  -Wl,<opt>      Pass option <opt> to the linker
 Tracing options:
   -dparse        Save C file after parsing and elaboration in <file>.parse.c
   -dc            Save generated Compcert C in <file>.compcert.c
@@ -410,10 +416,6 @@ Tracing options:
   -dmach         Save generated Mach code in <file>.mach
   -dasm          Save generated assembly in <file>.s
   -sdump         Save info for post-linking validation in <file>.sdump
-Linking options:
-  -l<lib>        Link library <lib>
-  -L<dir>        Add <dir> to search path for libraries
-  -Wl,<opt>      Pass option <opt> to the linker
 General options:
   -stdlib <dir>  Set the path of the Compcert run-time library
   -v             Print external commands before invoking them
@@ -441,6 +443,12 @@ let cmdline_actions =
   "-[IDU].", Self(fun s -> prepro_options := s :: !prepro_options);
   "-[lL].", Self(fun s -> linker_options := s :: !linker_options);
   "-o$", String(fun s -> option_o := Some s);
+  "-E$", Set option_E;
+  "-S$", Set option_S;
+  "-c$", Set option_c;
+  "-v$", Set option_v;
+  "-g$", Self (fun s ->
+      option_g := true; linker_options := s :: !linker_options);
   "-stdlib$", String(fun s -> stdlib_path := s);
   "-dparse$", Set option_dparse;
   "-dc$", Set option_dcmedium;
@@ -456,10 +464,6 @@ let cmdline_actions =
   "-dmach$", Set option_dmach;
   "-dasm$", Set option_dasm;
   "-sdump$", Set option_sdump;
-  "-E$", Set option_E;
-  "-S$", Set option_S;
-  "-c$", Set option_c;
-  "-v$", Set option_v;
   "-interp$", Set option_interp;
   "-quiet$", Self (fun _ -> Interp.trace := 0);
   "-trace$", Self (fun _ -> Interp.trace := 2);
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 2d676d1..12f6691 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -221,6 +221,39 @@ let print_align oc n =
 
 let need_masks = ref false
 
+(* Emit .file / .loc debugging directives *)
+
+let filename_num : (string, int) Hashtbl.t = Hashtbl.create 7
+
+let print_file_line oc file line =
+  if !Clflags.option_g && file <> "" then begin
+    let filenum = 
+      try
+        Hashtbl.find filename_num file
+      with Not_found ->
+        let n = Hashtbl.length filename_num + 1 in
+        Hashtbl.add filename_num file n;
+        fprintf oc "	.file	%d %S\n" n file;
+        n
+    in fprintf oc "	.loc	%d %s\n" filenum line
+  end
+
+let print_location oc loc =
+  if loc <> Cutil.no_loc then
+    print_file_line oc (fst loc) (string_of_int (snd loc))
+
+(* Emit .cfi directives *)
+
+let cfi_startproc oc =
+  if Configuration.asm_supports_cfi then fprintf oc "	.cfi_startproc\n"
+
+let cfi_endproc oc =
+  if Configuration.asm_supports_cfi then fprintf oc "	.cfi_endproc\n"
+
+let cfi_adjust oc delta =
+  if Configuration.asm_supports_cfi then
+    fprintf oc "	.cfi_adjust_cfa_offset	%ld\n" delta
+
 (* Built-in functions *)
 
 (* Built-ins.  They come in two flavors: 
@@ -231,9 +264,15 @@ let need_masks = ref false
 
 (* Handling of annotations *)
 
+let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$"
+
 let print_annot_stmt oc txt targs args =
-  fprintf oc "%s annotation: " comment;
-  PrintAnnot.print_annot_stmt preg "ESP" oc txt targs args
+  if Str.string_match re_file_line txt 0 then begin
+    print_file_line oc (Str.matched_group 1 txt) (Str.matched_group 2 txt)
+  end else begin
+    fprintf oc "%s annotation: " comment;
+    PrintAnnot.print_annot_stmt preg "ESP" oc txt targs args
+  end
 
 let print_annot_val oc txt args res =
   fprintf oc "%s annotation: " comment;
@@ -509,16 +548,20 @@ let print_instruction oc = function
       fprintf oc "	movsd	%a, %a\n" freg r1 addressing a
   | Pfld_f(r1) ->
       fprintf oc "	subl	$8, %%esp\n";
+      cfi_adjust oc 8l;
       fprintf oc "	movsd	%a, 0(%%esp)\n" freg r1;
       fprintf oc "	fldl	0(%%esp)\n";
-      fprintf oc "	addl	$8, %%esp\n"
+      fprintf oc "	addl	$8, %%esp\n";
+      cfi_adjust oc (-8l)
   | Pfld_m(a) ->
       fprintf oc "	fldl	%a\n" addressing a
   | Pfstp_f(rd) ->
       fprintf oc "	subl	$8, %%esp\n";
+      cfi_adjust oc 8l;
       fprintf oc "	fstpl	0(%%esp)\n";
       fprintf oc "	movsd	0(%%esp), %a\n" freg rd;
-      fprintf oc "	addl	$8, %%esp\n"
+      fprintf oc "	addl	$8, %%esp\n";
+      cfi_adjust oc (-8l)
   | Pfstp_m(a) ->
       fprintf oc "	fstpl	%a\n" addressing a
   | Pxchg_rr(r1, r2) ->
@@ -668,11 +711,13 @@ let print_instruction oc = function
       let sz = sp_adjustment sz in
       let ofs_link = camlint_of_coqint ofs_link in
       fprintf oc "	subl	$%ld, %%esp\n" sz;
+      cfi_adjust oc sz;
       fprintf oc "	leal	%ld(%%esp), %%edx\n" (Int32.add sz 4l);
       fprintf oc "	movl	%%edx, %ld(%%esp)\n" ofs_link
   | Pfreeframe(sz, ofs_ra, ofs_link) ->
       let sz = sp_adjustment sz in
-      fprintf oc "	addl	$%ld, %%esp\n" sz
+      fprintf oc "	addl	$%ld, %%esp\n" sz;
+      cfi_adjust oc (Int32.neg sz)
   | Pbuiltin(ef, args, res) ->
       begin match ef with
       | EF_builtin(name, sg) ->
@@ -729,7 +774,10 @@ let print_function oc name code =
   if not (C2C.atom_is_static name) then
     fprintf oc "	.globl %a\n" symbol name;
   fprintf oc "%a:\n" symbol name;
+  print_location oc (C2C.atom_location name);
+  cfi_startproc oc;
   List.iter (print_instruction oc) code;
+  cfi_endproc oc;
   if target = ELF then begin
     fprintf oc "	.type	%a, @function\n" symbol name;
     fprintf oc "	.size	%a, . - %a\n" symbol name symbol name
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 21b615b..07ed87c 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -200,6 +200,58 @@ let section oc sec =
   assert (name <> "COMM");
   fprintf oc "	%s\n" name
 
+(* Emit .file / .loc debugging directives *)
+
+let file_dir =
+  match target with Linux -> ".file" | Diab -> ".d2file"
+let loc_dir =
+  match target with Linux -> ".loc"  | Diab -> ".d2line"
+
+let filename_num : (string, int) Hashtbl.t = Hashtbl.create 7
+
+let print_file_line oc file line =
+  if !Clflags.option_g && file <> "" then begin
+    let filenum = 
+      try
+        Hashtbl.find filename_num file
+      with Not_found ->
+        let n = Hashtbl.length filename_num + 1 in
+        Hashtbl.add filename_num file n;
+        fprintf oc "	%s	%d %S\n" file_dir n file;
+        n
+    in fprintf oc "	%s	%d %s\n" loc_dir filenum line
+  end
+
+let print_location oc loc =
+  if loc <> Cutil.no_loc then
+    print_file_line oc (fst loc) (string_of_int (snd loc))
+
+(* Emit .cfi directives *)
+
+let cfi_startproc oc =
+  if Configuration.asm_supports_cfi then
+    match config with
+    | Linux -> fprintf oc "	.cfi_startproc\n"
+    | Diab  -> assert false
+
+let cfi_endproc oc =
+  if Configuration.asm_supports_cfi then
+    match config with
+    | Linux -> fprintf oc "	.cfi_endproc\n"
+    | Diab  -> assert false
+
+let cfi_adjust oc delta =
+  if Configuration.asm_supports_cfi then
+    match config with
+    | Linux -> fprintf oc "	.cfi_adjust_cfa_offset	%ld\n" delta
+    | Diab  -> assert false
+
+let cfi_rel_offset oc reg ofs =
+  if Configuration.asm_supports_cfi then
+    match config with
+    | Linux -> fprintf oc "	.cfi_rel_offset	%s, %ld\n" reg ofs
+    | Diab  -> assert false
+
 (* Encoding masks for rlwinm instructions *)
 
 let rolm_mask n =
@@ -442,8 +494,10 @@ let print_builtin_inline oc name args res =
       fprintf oc "	cntlzw	%a, %a\n" ireg res ireg a1
   | ("__builtin_bswap" | "__builtin_bswap32"), [IR a1], [IR res] ->
       fprintf oc "	stwu	%a, -8(%a)\n" ireg a1 ireg GPR1;
+      cfi_adjust oc 8l;
       fprintf oc "	lwbrx	%a, %a, %a\n" ireg res ireg_or_zero GPR0 ireg GPR1;
-      fprintf oc "	addi	%a, %a, 8\n" ireg GPR1 ireg GPR1
+      fprintf oc "	addi	%a, %a, 8\n" ireg GPR1 ireg GPR1;
+      cfi_adjust oc (-8l)
   | "__builtin_bswap16", [IR a1], [IR res] ->
       fprintf oc "	rlwinm	%a, %a, 8, 16, 23\n" ireg GPR0 ireg a1;
       fprintf oc "	rlwinm	%a, %a, 24, 24, 31\n" ireg res ireg a1;
@@ -470,8 +524,10 @@ let print_builtin_inline oc name args res =
   | "__builtin_fcti", [FR a1], [IR res] ->
       fprintf oc "	fctiw	%a, %a\n" freg FPR13 freg a1;
       fprintf oc "	stfdu	%a, -8(%a)\n" freg FPR13 ireg GPR1;
+      cfi_adjust oc 8l;
       fprintf oc "	lwz	%a, 4(%a)\n" ireg res ireg GPR1;
       fprintf oc "	addi	%a, %a, 8\n" ireg GPR1 ireg GPR1
+      cfi_adjust oc (-8l)
   (* 64-bit integer arithmetic *)
   | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] ->
       if rl = ah then begin
@@ -570,7 +626,8 @@ let print_instruction oc tbl pc fallthrough = function
         fprintf oc "	addis	%a, 0, %ld\n" ireg GPR0 (Int32.shift_right_logical adj 16);
         fprintf oc "	ori	%a, %a, %ld\n" ireg GPR0 ireg GPR0 (Int32.logand adj 0xFFFFl);
         fprintf oc "	stwux	%a, %a, %a\n" ireg GPR1 ireg GPR1 ireg GPR0
-      end
+      end;
+      cfi_adjust oc sz
   | Pand_(r1, r2, r3) ->
       fprintf oc "	and.	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pandc(r1, r2, r3) ->
@@ -652,7 +709,8 @@ let print_instruction oc tbl pc fallthrough = function
       if sz < 0x8000l then
         fprintf oc "	addi	%a, %a, %ld\n" ireg GPR1 ireg GPR1 sz
       else
-        fprintf oc "	lwz	%a, %ld(%a)\n" ireg GPR1 ofs ireg GPR1
+        fprintf oc "	lwz	%a, %ld(%a)\n" ireg GPR1 ofs ireg GPR1;
+      cfi_adjust oc (Int32.neg sz)
   | Pfabs(r1, r2) ->
       fprintf oc "	fabs	%a, %a\n" freg r1 freg r2
   | Pfadd(r1, r2, r3) ->
@@ -663,8 +721,10 @@ let print_instruction oc tbl pc fallthrough = function
       fprintf oc "%s begin pseudoinstr %a = fcti(%a)\n" comment ireg r1 freg r2;
       fprintf oc "	fctiwz	%a, %a\n" freg FPR13 freg r2;
       fprintf oc "	stfdu	%a, -8(%a)\n" freg FPR13 ireg GPR1;
+      cfi_adjust oc 8l;
       fprintf oc "	lwz	%a, 4(%a)\n" ireg r1 ireg GPR1;
       fprintf oc "	addi	%a, %a, 8\n" ireg GPR1 ireg GPR1;
+      cfi_adjust oc (-8l);
       fprintf oc "%s end pseudoinstr fcti\n" comment
   | Pfdiv(r1, r2, r3) ->
       fprintf oc "	fdiv	%a, %a, %a\n" freg r1 freg r2 freg r3
@@ -672,9 +732,11 @@ let print_instruction oc tbl pc fallthrough = function
       fprintf oc "%s begin pseudoinstr %a = fmake(%a, %a)\n"
               comment freg rd ireg r1 ireg r2;
       fprintf oc "	stwu	%a, -8(%a)\n" ireg r1 ireg GPR1;
+      cfi_adjust oc 8l;
       fprintf oc "	stw	%a, 4(%a)\n" ireg r2 ireg GPR1;
       fprintf oc "	lfd	%a, 0(%a)\n" freg rd ireg GPR1;
       fprintf oc "	addi	%a, %a, 8\n" ireg GPR1 ireg GPR1;
+      cfi_adjust oc (-8l);
       fprintf oc "%s end pseudoinstr fmake\n" comment
   | Pfmr(r1, r2) ->
       fprintf oc "	fmr	%a, %a\n" freg r1 freg r2
@@ -719,7 +781,8 @@ let print_instruction oc tbl pc fallthrough = function
       fprintf oc "	mfcr	%a\n" ireg r1;
       fprintf oc "	rlwinm	%a, %a, %d, 31, 31\n" ireg r1  ireg r1 (1 + num_crbit bit)
   | Pmflr(r1) ->
-      fprintf oc "	mflr	%a\n" ireg r1
+      fprintf oc "	mflr	%a\n" ireg r1;
+      cfi_rel_offset oc "lr" 8l
   | Pmr(r1, r2) ->
       fprintf oc "	mr	%a, %a\n" ireg r1 ireg r2
   | Pmtctr(r1) ->
@@ -925,7 +988,10 @@ let print_function oc name code =
   if not (C2C.atom_is_static name) then
     fprintf oc "	.globl %a\n" symbol name;
   fprintf oc "%a:\n" symbol name;
+  print_location oc (C2C.atom_location name);
+  cfi_startproc oc;
   print_instructions oc (label_positions PTree.empty 0 code) 0 true code;
+  cfi_endproc oc;
   fprintf oc "	.type	%a, @function\n" symbol name;
   fprintf oc "	.size	%a, . - %a\n" symbol name symbol name;
   if !float_literals <> [] then begin