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.

8 files changed, 232 insertions, 53 deletions

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),[]