Rework of struct member offsets for debug info.

The struct member byte and bit offsets are now set based upon the new
function `struct_layout` from Ctypes.v, thus using the same code to
compute as used to generate the actual struct access.

The struct offset member information is addded using the types computed
after the translation in C2C. Therefore we need to store the new internal
names of the members as well as the composites and use them
when adding the offset information.

Fixes: #445

6 files changed, 92 insertions, 41 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 65f290ba..b0dc8e8a 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -624,9 +624,10 @@ let rec convertTypAnnotArgs env = function
       Tcons(convertTyp env (Cutil.unary_conversion env e1.etyp),
             convertTypAnnotArgs env el)
 
-let convertField env f =
+let convertField env sid f =
   let id = intern_string f.fld_name
   and ty = convertTyp env ?bitwidth: f.fld_bitfield f.fld_typ in
+  Debug.set_member_atom ~str_id:sid f.fld_name ~fld_id:id;
   match f.fld_bitfield with
   | None -> Member_plain(id, ty)
   | Some w ->
@@ -639,17 +640,13 @@ let convertField env f =
 let convertCompositedef env su id attr members =
   if Cutil.find_custom_attributes ["packed";"__packed__"] attr <> [] then
     unsupported "packed struct (consider adding option [-fpacked-structs])";
-  let t = match su with
-  | C.Struct ->
-      let layout = Cutil.struct_layout env attr members in
-      List.iter (fun (a,b) -> Debug.set_member_offset id a b) layout;
-      TStruct (id,attr)
-  | C.Union -> TUnion (id,attr) in
-  Debug.set_composite_size id su (Cutil.sizeof env t);
-  Composite(intern_string id.name,
-            begin match su with C.Struct -> Ctypes.Struct | C.Union -> Ctypes.Union end,
-            List.map (convertField env) members,
-            convertAttr attr)
+  let intern_name = intern_string id.name in
+  let (t, su') = match su with
+    | C.Struct -> TStruct (id, attr), Ctypes.Struct
+    | C.Union -> TUnion (id, attr), Ctypes.Union in
+  Debug.set_composite_size id intern_name su (Cutil.sizeof env t);
+  let ms = List.map (convertField env intern_name) members in
+  Composite(intern_name, su', ms, convertAttr attr)
 
 let rec projFunType env ty =
   match Cutil.unroll env ty with
@@ -1527,6 +1524,41 @@ let public_globals gl =
     (fun accu (id, g) -> if atom_is_static id then accu else id :: accu)
     [] gl
 
+(** Complete the debug information of struct/unions *)
+
+(* [debug_set_struct_mem_ofs sid ((id,byte_ofs), bits)] sets the
+   byte and bit offset information of the member [id] of the struct
+   [sid] *)
+let debug_set_struct_mem_ofs sid ((id, byte_ofs), bits) =
+  let byte_ofs = Z.to_int byte_ofs in
+  match bits with
+  | Full ->
+    Debug.set_member_offset ~str_id:sid ~fld_id:id byte_ofs
+  | Bits (sz, sg, bit_pos, width) ->
+    let bit_pos = Z.to_int bit_pos in
+    let sz = Z.to_int (bitalignof_intsize sz) in
+    let bit_pos = if not !Machine.config.Machine.bitfields_msb_first then
+        sz - bit_pos - (Z.to_int width)
+      else
+        bit_pos in
+    let size = sz / 8 in
+    Debug.set_bitfield_offset ~str_id:sid ~fld_id:id ~bit_ofs:bit_pos ~byte_ofs:byte_ofs ~size:size
+
+(* [debug_set_struct_ofs env types] sets the missing offset information
+   of all structs in the list of composites in [types] if we compile
+   with debug information. *)
+let debug_set_struct_ofs env typs =
+  if !Clflags.option_g then
+    List.iter (function
+        | Composite (sid, Ctypes.Struct, ms, a) ->
+          let layout = Ctypes.layout_struct env ms in
+          begin match layout with
+            | Errors.OK layout ->
+              List.iter (debug_set_struct_mem_ofs sid) layout
+            | Errors.Error _ -> ()
+          end
+        | _ -> ()) typs
+
 (** Convert a [C.program] into a [Csyntax.program] *)
 
 let convertProgram p =
@@ -1555,6 +1587,7 @@ let convertProgram p =
             prog_main = intern_string !Clflags.main_function_name;
             prog_types = typs;
             prog_comp_env = ce } in
+        debug_set_struct_ofs ce typs;
         Diagnostics.check_errors ();
         p'
   with Env.Error msg ->
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index 17eb2207..0eb0feb4 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -142,8 +142,6 @@ val composite_info_decl:
   struct_or_union -> attributes -> Env.composite_info
 val composite_info_def:
   Env.t -> struct_or_union -> attributes -> field list -> Env.composite_info
-val struct_layout:
-  Env.t -> attributes -> field list -> (string * int) list
 val offsetof:
   Env.t -> typ -> field -> int
 (* Compute the offset of a struct member *)
diff --git a/debug/Debug.ml b/debug/Debug.ml
index 812f57cc..a1a68b74 100644
--- a/debug/Debug.ml
+++ b/debug/Debug.ml
@@ -23,9 +23,10 @@ type implem =
     {
       init: string -> unit;
       atom_global: ident -> atom -> unit;
-      set_composite_size: ident -> struct_or_union -> int option -> unit;
-      set_member_offset: ident -> string -> int -> unit;
-      set_bitfield_offset: ident -> string -> int -> string -> int -> unit;
+      set_composite_size: ident -> atom -> struct_or_union -> int option -> unit;
+      set_member_atom: str_id:atom -> string -> fld_id:atom -> unit;
+      set_member_offset: str_id:atom -> fld_id:atom -> int -> unit;
+      set_bitfield_offset: str_id:atom -> fld_id:atom -> bit_ofs:int -> byte_ofs:int -> size:int -> unit;
       insert_global_declaration: Env.t -> globdecl -> unit;
       add_fun_addr: atom -> section_name -> (int * int) -> unit;
       generate_debug_info: (atom -> string) -> string -> debug_entries option;
@@ -55,9 +56,10 @@ let default_implem =
   {
    init = (fun _ -> ());
    atom_global = (fun _ _ -> ());
-   set_composite_size = (fun _ _ _ -> ());
-   set_member_offset = (fun _ _  _ -> ());
-   set_bitfield_offset = (fun _ _ _ _ _ -> ());
+   set_composite_size = (fun _ _ _ _ -> ());
+   set_member_atom = (fun ~str_id _ ~fld_id -> ());
+   set_member_offset = (fun ~str_id ~fld_id  _ -> ());
+   set_bitfield_offset = (fun ~str_id ~fld_id ~bit_ofs ~byte_ofs  ~size-> ());
    insert_global_declaration = (fun _ _ -> ());
    add_fun_addr = (fun _ _ _ -> ());
    generate_debug_info = (fun _  _ -> None);
@@ -87,9 +89,11 @@ let implem = ref default_implem
 
 let init_compile_unit name = !implem.init name
 let atom_global id atom = !implem.atom_global id atom
-let set_composite_size id sou size = !implem.set_composite_size id sou size
-let set_member_offset id field off = !implem.set_member_offset id field off
-let set_bitfield_offset id field off underlying size = !implem.set_bitfield_offset id field off underlying size
+let set_composite_size id atom sou size = !implem.set_composite_size id atom sou size
+let set_member_atom ~str_id field ~fld_id = !implem.set_member_atom ~str_id:str_id field ~fld_id:fld_id
+let set_member_offset ~str_id ~fld_id off = !implem.set_member_offset ~str_id:str_id ~fld_id:fld_id off
+let set_bitfield_offset ~str_id ~fld_id ~bit_ofs ~byte_ofs ~size =
+  !implem.set_bitfield_offset ~str_id:str_id ~fld_id:fld_id ~bit_ofs:bit_ofs ~byte_ofs:byte_ofs ~size:size
 let insert_global_declaration env dec = !implem.insert_global_declaration env dec
 let add_fun_addr atom addr = !implem.add_fun_addr atom addr
 let generate_debug_info fun_s var_s = !implem.generate_debug_info fun_s var_s
diff --git a/debug/Debug.mli b/debug/Debug.mli
index 60e2f9bc..001cf0ea 100644
--- a/debug/Debug.mli
+++ b/debug/Debug.mli
@@ -22,9 +22,10 @@ type implem =
     {
      init: string -> unit;
      atom_global: ident -> atom -> unit;
-     set_composite_size: ident -> struct_or_union -> int option -> unit;
-     set_member_offset: ident -> string -> int -> unit;
-     set_bitfield_offset: ident -> string -> int -> string -> int -> unit;
+     set_composite_size: ident -> atom -> struct_or_union -> int option -> unit;
+     set_member_atom: str_id:atom -> string -> fld_id:atom -> unit;
+     set_member_offset: str_id:atom -> fld_id:atom -> int -> unit;
+     set_bitfield_offset: str_id:atom -> fld_id:atom -> bit_ofs:int -> byte_ofs:int -> size:int -> unit;
      insert_global_declaration: Env.t -> globdecl -> unit;
      add_fun_addr: atom -> section_name -> (int * int) -> unit;
      generate_debug_info: (atom -> string) -> string -> debug_entries option;
@@ -56,9 +57,10 @@ val implem: implem ref
 
 val init_compile_unit: string -> unit
 val atom_global: ident -> atom -> unit
-val set_composite_size: ident -> struct_or_union -> int option -> unit
-val set_member_offset: ident -> string -> int -> unit
-val set_bitfield_offset: ident -> string -> int -> string -> int -> unit
+val set_composite_size: ident -> atom -> struct_or_union -> int option -> unit
+val set_member_atom: str_id:atom -> string -> fld_id:atom -> unit
+val set_member_offset: str_id:atom -> fld_id:atom -> int -> unit
+val set_bitfield_offset: str_id:atom -> fld_id:atom -> bit_ofs:int -> byte_ofs:int -> size:int -> unit
 val insert_global_declaration:  Env.t -> globdecl -> unit
 val add_fun_addr: atom -> section_name -> (int * int) -> unit
 val all_files_iter: (string -> unit) -> unit
diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml
index f9684355..f6e2e271 100644
--- a/debug/DebugInformation.ml
+++ b/debug/DebugInformation.ml
@@ -396,13 +396,13 @@ let insert_global_declaration env dec =
       let fields = List.map (fun f ->
         {
          cfd_name = f.fld_name;
+         cfd_atom = None;
          cfd_anon = f.fld_anonymous;
          cfd_typ = insert_type f.fld_typ;
          cfd_bit_size = f.fld_bitfield;
          cfd_bit_offset = None;
          cfd_byte_offset = None;
          cfd_byte_size = None;
-         cfd_bitfield = None;
        }) fi in
       replace_composite id (fun comp ->
         let loc = if comp.ct_file_loc = None then Some dec.gloc else comp.ct_file_loc in
@@ -423,23 +423,36 @@ let insert_global_declaration env dec =
         {en with enum_file_loc = Some dec.gloc; enum_enumerators = enumerator;})
   | Gpragma _ -> ()
 
-let set_member_offset str field offset =
-  let id = find_type (TStruct (str,[])) in
+let atom_is_member id f =
+  match f.cfd_atom with
+  | None -> false
+  | Some f -> f = id
+
+let set_member_atom ~str_id field ~fld_id =
+  let sid = Hashtbl.find atom_to_definition str_id in
+  replace_composite sid (fun comp ->
+      let name f = f.cfd_name = field in
+      let members = list_replace name (fun a -> {a with cfd_atom = Some fld_id;}) comp.ct_members in
+      {comp with ct_members = members;})
+
+let set_member_offset ~str_id ~fld_id offset =
+  let id = Hashtbl.find atom_to_definition str_id in
   replace_composite id (fun comp ->
-    let name f = f.cfd_name = field || match f.cfd_bitfield with Some n -> n = field | _ -> false in
-    let members = list_replace name (fun a -> {a with cfd_byte_offset = Some offset;}) comp.ct_members in
+    let members = list_replace (atom_is_member fld_id) (fun a -> {a with cfd_byte_offset = Some offset;}) comp.ct_members in
     {comp with ct_members = members;})
 
-let set_composite_size comp sou size =
+let set_composite_size comp intern_name sou size =
   let id = find_type (gen_comp_typ sou comp []) in
+  Hashtbl.add atom_to_definition intern_name id;
   replace_composite id (fun comp -> {comp with ct_sizeof = size;})
 
-let set_bitfield_offset str field offset underlying size =
-  let id = find_type (TStruct (str,[])) in
+let set_bitfield_offset ~str_id ~fld_id ~bit_ofs ~byte_ofs ~size =
+  let id = Hashtbl.find atom_to_definition str_id in
   replace_composite id (fun comp ->
-    let name f = f.cfd_name = field in
-    let members = list_replace name (fun a ->
-      {a with cfd_bit_offset = Some offset; cfd_bitfield = Some underlying; cfd_byte_size = Some size})
+    let members = list_replace (atom_is_member fld_id) (fun a ->
+      {a with cfd_bit_offset = Some bit_ofs;
+              cfd_byte_size = Some size;
+              cfd_byte_offset = Some byte_ofs})
         comp.ct_members in
     {comp with ct_members = members;})
 
@@ -670,6 +683,7 @@ let default_debug =
    init = init;
    atom_global = atom_global;
    set_composite_size = set_composite_size;
+   set_member_atom = set_member_atom;
    set_member_offset = set_member_offset;
    set_bitfield_offset = set_bitfield_offset;
    insert_global_declaration = insert_global_declaration;
diff --git a/debug/DebugTypes.mli b/debug/DebugTypes.mli
index c3df6066..b3002f4c 100644
--- a/debug/DebugTypes.mli
+++ b/debug/DebugTypes.mli
@@ -19,13 +19,13 @@ open Camlcoq
 type composite_field =
     {
      cfd_name:        string;
+     cfd_atom:        atom option;
      cfd_anon:        bool;
      cfd_typ:         int;
      cfd_bit_size:    int option;
      cfd_bit_offset:  int option;
      cfd_byte_offset: int option;
      cfd_byte_size:   int option;
-     cfd_bitfield:    string option;
    }
 
 type composite_type =