Added support for the locations of stack allocated local variables.

This commit adds furher support for location information for local
variables and starts with the implementation of the debug_loc section.

16 files changed, 318 insertions, 98 deletions

diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 5f16fc9e..30166215 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -153,6 +153,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
           sprintf ".section	\"%s\",\"a%s%s\",%%progbits"
             s (if wr then "w" else "") (if ex then "x" else "")
       | Section_debug_info
+      | Section_debug_loc
       | Section_debug_abbrev -> "" (* Dummy value *)
             
     let section oc sec =
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index 9ffe3aa5..104440c6 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -66,7 +66,9 @@ module Printer(Target:TARGET) =
       print_debug_label oc e;
       Target.print_fun_info oc name;
       Target.emit_constants oc lit;
-      Target.print_jumptable oc jmptbl
+      Target.print_jumptable oc jmptbl;
+      if !Clflags.option_g then
+        Hashtbl.iter (fun p i -> Debug.add_label name p i) current_function_labels
     
     let print_init_data oc name id =
       if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0
@@ -141,6 +143,6 @@ let print_program oc p db =
     begin
       match Debug.generate_debug_info () with
       | None -> ()
-      | Some db ->
-          Printer.DebugPrinter.print_debug oc db
+      | Some (db,loc) ->
+          Printer.DebugPrinter.print_debug oc db loc
     end
diff --git a/common/Sections.ml b/common/Sections.ml
index c0c95848..8e569389 100644
--- a/common/Sections.ml
+++ b/common/Sections.ml
@@ -29,6 +29,7 @@ type section_name =
   | Section_user of string * bool (*writable*) * bool (*executable*)
   | Section_debug_info
   | Section_debug_abbrev
+  | Section_debug_loc
 
 type access_mode =
   | Access_default
diff --git a/common/Sections.mli b/common/Sections.mli
index e878b9e5..eca9a993 100644
--- a/common/Sections.mli
+++ b/common/Sections.mli
@@ -28,6 +28,7 @@ type section_name =
   | Section_user of string * bool (*writable*) * bool (*executable*)
   | Section_debug_info
   | Section_debug_abbrev
+  | Section_debug_loc
 
 type access_mode =
   | Access_default
diff --git a/debug/Debug.ml b/debug/Debug.ml
index fba921e1..7155ae0f 100644
--- a/debug/Debug.ml
+++ b/debug/Debug.ml
@@ -30,7 +30,7 @@ type implem =
      mutable set_bitfield_offset: ident -> string -> int -> string -> int -> unit;
      mutable insert_global_declaration: Env.t -> globdecl -> unit;
      mutable add_fun_addr: atom -> (int * int) -> unit;
-     mutable generate_debug_info: unit -> dw_entry option;
+     mutable generate_debug_info: unit -> (dw_entry * dw_locations) option;
      mutable all_files_iter: (string -> unit) -> unit;
      mutable insert_local_declaration:  storage -> ident -> typ -> location -> unit;
      mutable atom_local_variable: ident -> atom -> unit;
@@ -39,9 +39,11 @@ type implem =
      mutable add_lvar_scope: int -> ident -> int -> unit;
      mutable open_scope: atom -> int -> positive -> unit;
      mutable close_scope: atom -> int -> positive -> unit;
-     mutable start_live_range: atom -> positive -> string builtin_arg -> unit;
+     mutable start_live_range: atom -> positive -> int * int builtin_arg -> unit;
      mutable end_live_range: atom -> positive -> unit;
-     mutable stack_variable: atom -> string builtin_arg -> unit
+     mutable stack_variable: atom -> int * int builtin_arg -> unit;
+     mutable function_end: atom -> positive -> unit;
+     mutable add_label: atom -> positive -> int -> unit;
    }
 
 let implem =
@@ -66,6 +68,8 @@ let implem =
    start_live_range = (fun _ _ _ -> ());
    end_live_range = (fun _ _ -> ());
    stack_variable = (fun _ _ -> ());
+   function_end = (fun _ _ -> ());
+   add_label = (fun _ _ _ -> ());
 }
 
 let init () =
@@ -90,6 +94,8 @@ let init () =
     implem.start_live_range <- DebugInformation.start_live_range;
     implem.end_live_range <- DebugInformation.end_live_range;
     implem.stack_variable <- DebugInformation.stack_variable;
+    implem.function_end <- DebugInformation.function_end;
+    implem.add_label <- DebugInformation.add_label;
   end else begin
     implem.init <- (fun _ -> ());
     implem.atom_function <- (fun _ _ -> ());
@@ -111,6 +117,8 @@ let init () =
     implem.start_live_range <- (fun _ _ _ -> ());
     implem.end_live_range <- (fun _ _ -> ());
     implem.stack_variable <- (fun _ _ -> ());
+    implem.function_end <- (fun _ _ -> ());
+    implem.add_label <- (fun _ _ _ -> ());
   end
 
 let init_compile_unit name = implem.init name
@@ -133,3 +141,5 @@ let close_scope atom id lbl = implem.close_scope atom id lbl
 let start_live_range atom lbl loc = implem.start_live_range atom lbl loc
 let end_live_range atom lbl = implem.end_live_range atom lbl
 let stack_variable atom loc = implem.stack_variable atom loc
+let function_end atom loc = implem.function_end atom loc
+let add_label atom p lbl = implem.add_label atom p lbl
diff --git a/debug/Debug.mli b/debug/Debug.mli
index 42a0cee7..2954c300 100644
--- a/debug/Debug.mli
+++ b/debug/Debug.mli
@@ -26,7 +26,6 @@ val set_member_offset: ident -> string -> int -> unit
 val set_bitfield_offset: ident -> string -> int -> string -> int -> unit
 val insert_global_declaration:  Env.t -> globdecl -> unit
 val add_fun_addr: atom -> (int * int) -> unit
-val generate_debug_info: unit -> dw_entry option
 val all_files_iter: (string -> unit) -> unit
 val insert_local_declaration: storage -> ident -> typ -> location -> unit
 val atom_local_variable: ident -> atom -> unit
@@ -35,6 +34,9 @@ val enter_function_scope: int -> int -> unit
 val add_lvar_scope: int -> ident -> int -> unit
 val open_scope: atom -> int -> positive -> unit
 val close_scope: atom -> int -> positive -> unit
-val start_live_range: atom -> positive -> string builtin_arg -> unit
+val start_live_range: atom -> positive -> (int * int builtin_arg) -> unit
 val end_live_range: atom -> positive -> unit
-val stack_variable: atom -> string builtin_arg -> unit
+val stack_variable: atom -> int * int builtin_arg -> unit
+val function_end: atom -> positive -> unit
+val add_label: atom -> positive -> int -> unit
+val generate_debug_info: unit -> (dw_entry * dw_locations) option
diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml
index f12853c9..459c4e9d 100644
--- a/debug/DebugInformation.ml
+++ b/debug/DebugInformation.ml
@@ -10,6 +10,8 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+open AST
+open BinNums
 open C
 open Camlcoq
 open Cutil
@@ -659,20 +661,94 @@ let enter_scope f_id p_id id =
     replace_scope p_id' ({scope_variables = id'::scope.scope_variables;})
   with Not_found  -> ()
 
+
+type scope_range =
+    {
+     start_addr: positive option;
+     end_addr: positive option;
+   }
+
+type var_range =
+    {
+     range_start: positive option;
+     range_end:   positive option;
+     var_loc:     int * int builtin_arg;
+   }
+
+type var_location =
+  | RangeLoc of var_range list
+  | FunctionLoc of  int * int builtin_arg (* Stack allocated variables *)
+
+let var_locations: (atom,var_location) Hashtbl.t = Hashtbl.create 7
+
+let scope_ranges: (int,scope_range list) Hashtbl.t = Hashtbl.create 7
+
+let label_translation: (atom * positive, int) Hashtbl.t = Hashtbl.create 7
+
+let add_label atom p i =
+  Hashtbl.add label_translation (atom,p) i
+
+(* Auxiliary data structures and functions *)
+module IntSet = Set.Make(struct
+  type t = int
+  let compare (x:int) (y:int) = compare x y
+end)
+
+let open_scopes: IntSet.t ref = ref IntSet.empty
+
 let open_scope atom s_id lbl =
-  ()
+  try
+    let s_id = Hashtbl.find atom_to_scope (atom,s_id) in
+    let old_r = try Hashtbl.find scope_ranges s_id with Not_found -> [] in
+    let n_scop = { start_addr = Some lbl; end_addr = None;} in
+    open_scopes := IntSet.add s_id !open_scopes;
+    Hashtbl.replace scope_ranges s_id (n_scop::old_r)
+  with Not_found -> ()
 
 let close_scope atom s_id lbl =
-  ()
+  try
+    let s_id = Hashtbl.find atom_to_scope (atom,s_id) in
+    let old_r = try Hashtbl.find scope_ranges s_id with Not_found -> [] in
+    let last_r,rest = 
+      begin
+        match old_r with
+        | a::rest -> a,rest
+        | _ -> assert false (* We must have an opening scope *)
+      end in
+    let new_r = ({last_r with end_addr = Some lbl;})::rest in
+    open_scopes := IntSet.remove s_id !open_scopes;
+    Hashtbl.replace scope_ranges s_id new_r
+  with Not_found -> ()
 
 let start_live_range atom lbl loc =
-  ()
+  try
+    let old_r = Hashtbl.find var_locations atom in
+    match old_r with
+    | RangeLoc old_r ->
+        let n_r = { range_start = Some lbl; range_end = None; var_loc = loc } in
+        Hashtbl.replace var_locations atom (RangeLoc (n_r::old_r))
+    | _ -> assert false
+  with Not_found -> ()
+
 
 let end_live_range atom lbl =
-  ()
+  try
+    let old_r = Hashtbl.find var_locations atom in
+    match old_r with
+    | RangeLoc (n_r::old_r) ->
+        let n_r = {n_r with  range_end = Some lbl} in
+        Hashtbl.replace var_locations atom (RangeLoc (n_r::old_r))
+    | _ -> assert false
+  with Not_found -> ()
+  
+
+let stack_variable atom (sp,loc) =
+  Hashtbl.add var_locations atom (FunctionLoc (sp,loc))
+
+let function_end atom loc =
+  IntSet.iter (fun id -> close_scope atom id loc) !open_scopes;
+  open_scopes := IntSet.empty
 
-let stack_variable atom loc =
-  ()
 
 let init name =
   id := 0;
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
index f3cfdc6e..5f459a57 100644
--- a/debug/DwarfPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -21,7 +21,7 @@ open Sections
 (* The printer is parameterized over target specific functions and a set of dwarf type constants *)
 module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
     sig
-      val print_debug: out_channel -> dw_entry -> unit
+      val print_debug: out_channel -> dw_entry -> dw_locations -> unit
     end =
   struct
 
@@ -36,6 +36,10 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
     let print_label oc lbl =
       fprintf oc "%a:\n" label lbl
 
+    (* Print a positive label *)
+    let print_plabel oc lbl =
+      print_label oc (transl_label lbl)
+
     (* Helper functions for abbreviation printing *)
     let add_byte buf value =
       Buffer.add_string buf (string_of_byte value)
@@ -69,9 +73,10 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
     let add_location loc buf =
       match loc with
       | None -> ()
-      | Some (LocSymbol _) ->add_abbr_entry (0x2,location_block_type_abbr) buf
-      | Some (LocConst _) -> add_abbr_entry (0x2,location_const_type_abbr) buf
-      | Some (LocBlock _) -> add_abbr_entry (0x2,location_block_type_abbr) buf
+      | Some (LocRef _) -> add_abbr_entry (0x2,location_ref_type_abbr) buf
+      | Some (LocList _ )
+      | Some (LocSymbol _)
+      | Some (LocSimple _) -> add_abbr_entry (0x2,location_block_type_abbr) buf
 
     (* Dwarf entity to string function *)
     let abbrev_string_of_entity entity has_sibling =
@@ -101,8 +106,8 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
       | DW_TAG_compile_unit e ->
           prologue 0x11;
           add_abbr_entry (0x1b,comp_dir_type_abbr) buf;
-          add_high_pc buf;
           add_low_pc buf;
+          add_high_pc buf;
           add_abbr_entry (0x13,language_type_abbr) buf;
           add_name buf;
           add_abbr_entry (0x25,producer_type_abbr) buf;
@@ -288,20 +293,43 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
     let print_byte oc b =
       fprintf oc "	.byte		0x%X\n" b
 
+
+    let size_of_loc_expr = function
+      | DW_OP_bregx _ -> 3
+      | DW_OP_plus_uconst _ -> 2
+      | DW_OP_piece _ -> 2
+        
+    let print_loc_expr oc = function
+      | DW_OP_bregx (a,b) ->
+          print_byte oc dw_op_bregx;
+          print_uleb128 oc a;
+          fprintf oc "	.sleb128	%ld\n" b
+      | DW_OP_plus_uconst i ->
+          print_byte oc dw_op_plus_uconst;
+          print_byte oc i
+      | DW_OP_piece i ->
+          print_byte oc dw_op_piece;
+          print_uleb128 oc i
+        
     let print_loc oc loc =
       match loc with
       | LocSymbol s ->
-          fprintf oc "	.sleb128	5\n";
-          fprintf oc "	.byte		3\n";
+          print_sleb128 oc 5;
+          print_byte oc dw_op_addr;
           fprintf oc "	.4byte		%a\n" symbol s
+      | LocSimple e ->
+          print_sleb128 oc (size_of_loc_expr e);
+          print_loc_expr oc e
+      | LocList e ->
+          let size = List.fold_left (fun acc a -> acc + size_of_loc_expr a) 0 e in
+          print_sleb128 oc size;
+          List.iter (print_loc_expr oc) e
       | _ ->   ()
 
     let print_data_location oc dl =
       match dl with
-      | DataLocBlock [DW_OP_plus_uconst i] ->
-          fprintf oc "	.sleb128	2\n";
-          fprintf oc "	.byte		0x23\n";
-          fprintf oc "	.byte		%d\n" i
+      | DataLocBlock e ->
+          print_loc_expr oc e
       | _ -> ()
 
     let print_ref oc r =
@@ -340,8 +368,8 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
     let print_compilation_unit oc tag =
       let prod_name = sprintf "AbsInt Angewandte Informatik GmbH:CompCert Version %s:%s" Version.version Configuration.arch in
       print_string oc (Sys.getcwd ());
-      print_addr oc (get_end_addr ());
       print_addr oc (get_start_addr ());
+      print_addr oc (get_end_addr ());
       print_uleb128 oc 1;
       print_string oc tag.compile_unit_name;
       print_string oc prod_name;
@@ -372,9 +400,10 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
       print_ref oc tl.label_low_pc;
       print_string oc tl.label_name
 
+
     let print_lexical_block oc lb =
-      print_opt_value oc lb.lexical_block_high_pc print_ref;
-      print_opt_value oc lb.lexical_block_low_pc print_ref
+      print_opt_value oc lb.lexical_block_high_pc print_addr;
+      print_opt_value oc lb.lexical_block_low_pc print_addr
 
     let print_member oc mb =
       print_file_loc oc mb.member_file_loc;
@@ -504,10 +533,24 @@ module DwarfPrinter(Target: DWARF_TARGET)(DwarfAbbrevs:DWARF_ABBREVS):
       print_sleb128 oc 0;
       print_label oc debug_end (* End of the debug section *)
 
+    let print_location_entry oc l =
+      let c_low = get_start_addr () in
+      print_label oc (entry_to_label l.loc_id);
+      List.iter (fun (b,e,loc) ->
+        fprintf oc "	.4byte		%a-%a\n" label b label c_low;
+        fprintf oc "	.4byte		%a-%a\n" label e label c_low;
+        print_loc oc loc) l.loc;
+      fprintf oc "	.4byte	0\n";
+      fprintf oc "	.4byte	0\n"
+
+    let print_location_list oc l =
+      List.iter (print_location_entry oc) l
 
     (* Print the debug info and abbrev section *)
-    let print_debug oc entry =
+    let print_debug oc entry loc =
       print_debug_abbrev oc entry;
-      print_debug_info oc entry
+      print_debug_info oc entry;
+      print_location_list oc loc
+
 
   end
diff --git a/debug/DwarfPrinter.mli b/debug/DwarfPrinter.mli
index 9e0e6693..ab9ab264 100644
--- a/debug/DwarfPrinter.mli
+++ b/debug/DwarfPrinter.mli
@@ -14,5 +14,5 @@ open DwarfTypes
 
 module DwarfPrinter: functor (Target: DWARF_TARGET) -> functor (DwarfAbbrevs: DWARF_ABBREVS) ->
   sig
-    val print_debug: out_channel -> dw_entry -> unit
+    val print_debug: out_channel -> dw_entry -> dw_locations -> unit
   end
diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli
index 1d41403b..f01e550a 100644
--- a/debug/DwarfTypes.mli
+++ b/debug/DwarfTypes.mli
@@ -12,8 +12,9 @@
 
 (* Types used for writing dwarf debug information *)
 
-open Sections
+open BinNums
 open Camlcoq
+open Sections
 
 (* Basic types for the value of attributes *)
 
@@ -39,16 +40,17 @@ type block = string
 
 type location_expression =
   | DW_OP_plus_uconst of constant
-  | DW_OP
-
+  | DW_OP_bregx of int * int32
+  | DW_OP_piece of int
 
 type location_value =
   | LocSymbol of atom
-  | LocConst of constant
-  | LocBlock of block
-
+  | LocRef of address
+  | LocSimple of location_expression
+  | LocList of location_expression list
+        
 type data_location_value =
-  | DataLocBlock of location_expression list
+  | DataLocBlock of location_expression
   | DataLocRef of reference
 
 type bound_value =
@@ -233,6 +235,14 @@ type dw_entry =
      id:       reference;
    }
 
+(* The type for the location list. *)
+type location_entry =
+    {
+     loc:     (int * int * location_value) list;
+     loc_id:  reference;
+   }
+type dw_locations = location_entry list
+
 (* Module type for a matching from type to dwarf encoding *)
 module type DWARF_ABBREVS =
   sig
@@ -257,7 +267,7 @@ module type DWARF_ABBREVS =
     val artificial_type_abbr: int
     val variable_parameter_type_abbr: int
     val bit_size_type_abbr: int
-    val location_const_type_abbr: int
+    val location_ref_type_abbr: int
     val location_block_type_abbr: int
     val data_location_block_type_abbr: int
     val data_location_ref_type_abbr: int
diff --git a/debug/DwarfUtil.ml b/debug/DwarfUtil.ml
index 4cd838b6..954324f1 100644
--- a/debug/DwarfUtil.ml
+++ b/debug/DwarfUtil.ml
@@ -76,6 +76,13 @@ let dw_form_ref8     = 0x14
 let dw_ref_udata     = 0x15
 let dw_ref_indirect  = 0x16
 
+(* Operation encoding *)
+let dw_op_addr = 0x3
+let dw_op_plus_uconst = 0x23
+let dw_op_bregx = 0x92
+let dw_op_piece = 0x93
+
+
 (* Default corresponding encoding for the different abbreviations *)
 module DefaultAbbrevs =
   struct
@@ -100,7 +107,7 @@ module DefaultAbbrevs =
     let artificial_type_abbr = dw_form_flag
     let variable_parameter_type_abbr = dw_form_flag
     let bit_size_type_abbr = dw_form_data1
-    let location_const_type_abbr = dw_form_data4
+    let location_ref_type_abbr = dw_form_data4
     let location_block_type_abbr = dw_form_block
     let data_location_block_type_abbr = dw_form_block
     let data_location_ref_type_abbr = dw_form_ref4
diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml
index 6c10b362..7b155419 100644
--- a/debug/Dwarfgen.ml
+++ b/debug/Dwarfgen.ml
@@ -10,7 +10,9 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+open AST
 open C
+open Camlcoq
 open Cutil
 open DebugInformation
 open DwarfTypes
@@ -162,7 +164,7 @@ let member_to_entry mem =
     member_data_member_location =
     (match mem.cfd_byte_offset with 
     | None -> None 
-    | Some s -> Some (DataLocBlock [DW_OP_plus_uconst s]));
+    | Some s -> Some (DataLocBlock (DW_OP_plus_uconst s)));
     member_declaration = None;
     member_name = Some (mem.cfd_name);
     member_type = mem.cfd_typ;
@@ -280,38 +282,66 @@ let function_parameter_to_entry acc p =
   } in
   new_entry (next_id ()) (DW_TAG_formal_parameter p),IntSet.add p.formal_parameter_type acc
 
-let rec local_variable_to_entry acc v id =
+let rec local_variable_to_entry f_id acc v id =
+  let loc = try
+    begin 
+      match (Hashtbl.find var_locations (get_opt_val v.lvar_atom)) with
+      | FunctionLoc (a,BA_addrstack (ofs)) ->
+          let ofs = camlint_of_coqint ofs in
+          Some (LocSimple (DW_OP_bregx (a,ofs)))
+      | FunctionLoc (a,BA_splitlong ((BA_addrstack hi),(BA_addrstack lo))) ->
+          let hi = camlint_of_coqint hi 
+          and lo = camlint_of_coqint lo in
+          if lo = Int32.add hi 4l then
+            Some (LocSimple (DW_OP_bregx (a,hi)))
+          else
+            Some (LocList [DW_OP_bregx (a,hi);DW_OP_piece 4;DW_OP_bregx (a,lo);DW_OP_piece 4])
+      | _ -> None
+    end
+  with Not_found -> None in
   let var = {
     variable_file_loc = v.lvar_file_loc;
     variable_declaration = None;
     variable_external = None;
     variable_name = v.lvar_name;
     variable_type = v.lvar_type;
-    variable_location = None;
+    variable_location = loc;
   } in
   new_entry id (DW_TAG_variable var),IntSet.add v.lvar_type acc
 
-and scope_to_entry acc sc id =
+and scope_to_entry f_id acc sc id =
+  let l_pc,h_pc = try
+    let r = Hashtbl.find scope_ranges id in
+    let lbl l = match l with 
+    | Some l -> Some (Hashtbl.find label_translation (f_id,l)) 
+    | None -> None in
+    begin
+      match r with
+      | [] -> None,None
+      | [a] -> lbl a.start_addr, lbl a.end_addr
+      | a::rest -> lbl (List.hd (List.rev rest)).start_addr,lbl a.end_addr
+    end
+  with Not_found -> None,None in
   let scope = {
-    lexical_block_high_pc = None;
-    lexical_block_low_pc = None;
+    lexical_block_high_pc = h_pc;
+    lexical_block_low_pc = l_pc;
   } in
-  let vars,acc = mmap local_to_entry acc sc.scope_variables in
+  let vars,acc = mmap (local_to_entry f_id) acc sc.scope_variables in
   let entry = new_entry id (DW_TAG_lexical_block scope) in
   add_children entry vars,acc
 
-and local_to_entry acc id =
+and local_to_entry f_id acc id =
   match Hashtbl.find local_variables id with
-  | LocalVariable v -> local_variable_to_entry acc v id
-  | Scope v -> scope_to_entry acc v id
+  | LocalVariable v -> local_variable_to_entry f_id acc v id
+  | Scope v -> scope_to_entry f_id acc v id
 
-let fun_scope_to_entries acc id =
+let fun_scope_to_entries f_id acc id =
   match id with
   | None -> [],acc
   | Some id ->
       let sc = Hashtbl.find local_variables id in
       (match sc with
-      | Scope sc ->mmap local_to_entry acc sc.scope_variables
+      | Scope sc ->mmap (local_to_entry f_id) acc sc.scope_variables
       | _ -> assert false)
 
 let function_to_entry acc id f =
@@ -324,10 +354,11 @@ let function_to_entry acc id f =
     subprogram_high_pc = f.fun_high_pc;
     subprogram_low_pc = f.fun_low_pc;
   } in
+  let f_id = get_opt_val f.fun_atom in
   let acc = match f.fun_return_type with Some s -> IntSet.add s acc | None -> acc in
   let f_entry =  new_entry id (DW_TAG_subprogram f_tag) in
   let params,acc = mmap function_parameter_to_entry acc f.fun_parameter in
-  let vars,acc = fun_scope_to_entries acc f.fun_scope in
+  let vars,acc = fun_scope_to_entries f_id acc f.fun_scope in
   add_children f_entry (params@vars),acc
      
 let definition_to_entry acc id t =
@@ -340,10 +371,10 @@ let gen_defs () =
   t::acc,bcc) definitions ([],IntSet.empty) in
   List.rev defs,typ
 
-let gen_debug_info () =
+let gen_debug_info () : dw_entry * dw_locations=
   let cp =  {
     compile_unit_name = !file_name;
   } in
   let cp = new_entry (next_id ()) (DW_TAG_compile_unit cp) in
   let defs,ty = gen_defs () in
-  add_children cp ((gen_types ty) @ defs)
+  add_children cp ((gen_types ty) @ defs),[]
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index b06f6f97..215eb4b8 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -102,6 +102,7 @@ module Cygwin_System : SYSTEM =
           sprintf ".section	\"%s\", \"%s\"\n"
             s (if ex then "xr" else if wr then "d" else "dr")
       | Section_debug_info
+      | Section_debug_loc
       | Section_debug_abbrev -> "" (* Dummy value *)
 
     let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *)
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index a7e66701..136c9e41 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -331,7 +331,8 @@ let p_section oc = function
   | Section_jumptable -> fprintf oc "{\"Section Name\":\"Jumptable\"}"
   | Section_user (s,w,e) -> fprintf oc "{\"Section Name\":%s,\"Writable\":%B,\"Executable\":%B}" s w e
   | Section_debug_info 
-  | Section_debug_abbrev -> () (* There should be no info in the debug sections *)
+  | Section_debug_abbrev 
+  | Section_debug_loc -> () (* There should be no info in the debug sections *)
 
 let p_int_opt oc = function
   | None -> fprintf oc "0"
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index d4675e5f..d44f709e 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -586,36 +586,57 @@ let expand_instruction_simple instr =
   | _ ->
       emit instr
 
-let preg_to_string p =
-  ""
-
-let rec translate_annot a =
-  match a with
-  | BA x -> BA (preg_to_string x)
-  | BA_int n -> BA_int n
-  | BA_long n -> BA_long n
-  | BA_float n -> BA_float n
-  | BA_single n -> BA_single n
-  | BA_loadstack (chunk,ofs) -> BA_loadstack (chunk,ofs)
-  | BA_addrstack ofs -> BA_addrstack ofs
-  | BA_loadglobal (chunk,id,ofs) -> BA_loadglobal (chunk,id,ofs) 
-  | BA_addrglobal (id,ofs) -> BA_addrglobal  (id,ofs)
-  | BA_splitlong (hi,lo) -> BA_splitlong (translate_annot hi,translate_annot lo)
-
-let expand_stack_loc txt = function
-  | [a] -> Debug.stack_variable txt (translate_annot a)
-  | _ -> assert false
-
-let expand_start_live_range txt lbl = function
-  | [a] -> Debug.start_live_range txt lbl (translate_annot a)
-  | _ -> assert false
-
-let expand_end_live_range =
-  Debug.end_live_range
+(* Translate to the integer identifier of the register as
+   the EABI specifies *)
+
+let int_reg_to_dwarf = function
+   | GPR0 -> 0  | GPR1 -> 1  | GPR2 -> 2  | GPR3 -> 3
+   | GPR4 -> 4  | GPR5 -> 5  | GPR6 -> 6  | GPR7 -> 7
+   | GPR8 -> 8  | GPR9 -> 9  | GPR10 -> 10 | GPR11 -> 11
+   | GPR12 -> 12 | GPR13 -> 13 | GPR14 -> 14 | GPR15 -> 15
+   | GPR16 -> 16 | GPR17 -> 17 | GPR18 -> 18 | GPR19 -> 19
+   | GPR20 -> 20 | GPR21 -> 21 | GPR22 -> 22 | GPR23 -> 23
+   | GPR24 -> 24 | GPR25 -> 25 | GPR26 -> 26 | GPR27 -> 27
+   | GPR28 -> 28 | GPR29 -> 29 | GPR30 -> 30 | GPR31 -> 31
+
+let float_reg_to_dwarf = function
+   | FPR0 -> 32  | FPR1 -> 33  | FPR2 -> 34  | FPR3 -> 35
+   | FPR4 -> 36  | FPR5 -> 37  | FPR6 -> 38  | FPR7 -> 39
+   | FPR8 -> 40  | FPR9 -> 41  | FPR10 -> 42 | FPR11 -> 43
+   | FPR12 -> 44 | FPR13 -> 45 | FPR14 -> 46 | FPR15 -> 47
+   | FPR16 -> 48 | FPR17 -> 49 | FPR18 -> 50 | FPR19 -> 51
+   | FPR20 -> 52 | FPR21 -> 53 | FPR22 -> 54| FPR23 -> 55
+   | FPR24 -> 56 | FPR25 -> 57 | FPR26 -> 58 | FPR27 -> 59
+   | FPR28 -> 60 | FPR29 -> 61 | FPR30 -> 62 | FPR31 -> 63
+
+let preg_to_dwarf_int = function
+   | IR r -> int_reg_to_dwarf r
+   | FR r -> float_reg_to_dwarf r
+   | _ -> assert false
+
+
+let translate_annot a =
+  let rec aux = function
+    | BA x -> Some (BA (preg_to_dwarf_int x))
+    | BA_int _
+    | BA_long _
+    | BA_float _
+    | BA_single _
+    | BA_loadglobal _
+    | BA_addrglobal _
+    | BA_loadstack _ -> None
+    | BA_addrstack ofs -> Some (BA_addrstack ofs)
+    | BA_splitlong (hi,lo) -> 
+        begin
+          match (aux hi,aux lo) with
+          | Some hi ,Some lo -> Some (BA_splitlong (hi,lo))
+          | _,_ -> None
+        end in
+  aux (List.hd a)
 
 let expand_scope id lbl oldscopes newscopes =
-  let opening = List.filter (fun a -> List.mem a oldscopes) newscopes
-  and closing = List.filter (fun a -> List.mem a newscopes) oldscopes in
+  let opening = List.filter (fun a -> not (List.mem a oldscopes)) newscopes
+  and closing = List.filter (fun a -> not (List.mem a newscopes)) oldscopes in
   List.iter (fun i -> Debug.open_scope id i lbl) opening;
   List.iter (fun i -> Debug.close_scope id i lbl) closing
 
@@ -627,31 +648,42 @@ let expand_instruction id l =
         lbl
     | Some lbl -> lbl in
   let rec aux lbl scopes = function
-    | [] -> ()
+    | [] -> let lbl = get_lbl lbl in
+      Debug.function_end id lbl
     | (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i)::rest ->
         let kind = (P.to_int kind) in
         begin
           match kind with
-          | 1 -> 
-              emit i; aux lbl scopes rest
+          | 1-> 
+              aux lbl scopes rest
           | 2 ->
               aux  lbl scopes rest
           | 3 ->
-              let lbl = get_lbl lbl in
-              expand_start_live_range txt lbl args;
-              aux (Some lbl) scopes rest
+             begin 
+               match translate_annot args with
+               | Some a ->
+                   let lbl = get_lbl lbl in
+                   Debug.start_live_range txt lbl (1,a);
+                   aux (Some lbl) scopes rest
+               | None -> aux lbl scopes rest
+             end
           | 4 ->
               let lbl = get_lbl lbl in
-              expand_end_live_range txt lbl;
+              Debug.end_live_range txt lbl;
               aux (Some lbl) scopes rest
-          | 5 -> 
-              expand_stack_loc txt args;
-              aux lbl scopes rest
-          | 6 ->
+          | 5 ->
+              begin
+                match translate_annot args with
+                | Some a->
+                    Debug.stack_variable txt (1,a);
+                    aux lbl scopes rest
+                | _ -> aux lbl scopes rest
+              end
+          | 6  ->
               let lbl = get_lbl lbl in
               let scopes' = List.map (function BA_int x -> Int32.to_int (camlint_of_coqint x) | _ -> assert false) args in
               expand_scope id lbl scopes scopes';
-              aux (Some lbl) scopes' rest
+              emit i;aux (Some lbl) scopes' rest
           | _ ->
               emit i; aux None scopes rest
         end
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 21181215..e53f56a9 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -133,7 +133,8 @@ module Linux_System : SYSTEM =
             s (if wr then "w" else "") (if ex then "x" else "")
       | Section_debug_info -> ".debug_info,\"\",@progbits"
       | Section_debug_abbrev -> ".debug_abbrev,\"\",@progbits"
-    
+      | Section_debug_loc -> ".debug_loc,\"\",@progbits"
+            
     let section oc sec =
       let name = name_of_section sec in
       assert (name <> "COMM");
@@ -211,6 +212,7 @@ module Diab_System : SYSTEM =
             | false, false -> 'r')              (* const *)
       | Section_debug_info -> ".debug_info,,n"
       | Section_debug_abbrev -> ".debug_abbrev,,n"
+      | Section_debug_loc -> ".debug_loc,,n"
 
     let section oc sec =
       let name = name_of_section sec in