diff options
Diffstat (limited to 'debug/DebugInformation.ml')
| -rw-r--r-- | debug/DebugInformation.ml | 219 |
1 files changed, 206 insertions, 13 deletions
diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml index e84172e6..42c229fa 100644 --- a/debug/DebugInformation.ml +++ b/debug/DebugInformation.ml @@ -11,6 +11,8 @@ (* *********************************************************************) open C +open Camlcoq +open Cutil (* This implements an interface for the collection of debugging information. *) @@ -66,7 +68,7 @@ type array_type = { type typedef = { typedef_name: string; - typ: int; + typ: int option; } type enumerator = { @@ -75,7 +77,7 @@ type enumerator = { enumerator_const: int; } -type emum_type = { +type enum_type = { enum_name: string; enum_byte_size: int option; enum_file_loc: location option; @@ -97,7 +99,7 @@ type parameter_type = { type function_type = { fun_return_type: int; - fun_prototyped: int; + fun_prototyped: bool; fun_params: parameter_type list; } @@ -108,6 +110,7 @@ type debug_types = | ArrayType of array_type | StructType of composite_type | UnionType of composite_type + | EnumType of enum_type | FunctionType of function_type | Typedef of typedef | ConstType of const_type @@ -133,7 +136,7 @@ let typ_to_string (ty: typ) = (* Helper functions for the attributes *) let strip_attributes typ = - let strip = List.filter (fun a -> a = AConst || a = AVolatile) in + let strip = List.filter (fun a -> a = AConst || a = AVolatile) in match typ with | TVoid at -> TVoid (strip at) | TInt (k,at) -> TInt (k,strip at) @@ -187,17 +190,207 @@ let find_type (ty: typ) = Hashtbl.find lookup_types (typ_to_string ty) (* Add type and information *) -let insert_type (ty: typ) = +let insert_type (ty: typ) = + let insert d_ty ty = + let id = next_id () + and name = typ_to_string ty in + Hashtbl.add all_types id d_ty; + Hashtbl.add lookup_types name id; + id in (* We are only interrested in Const and Volatile *) let ty = strip_attributes ty in - if not (exist_type ty) then - begin - let rec typ_aux ty = () - and attr_aux ty = + let rec typ_aux ty = + try find_type ty with + | Not_found -> + let d_ty = + match ty with + | TVoid _ -> Void + | TInt (k,_) -> + IntegerType ({int_kind = k }) + | TFloat (k,_) -> + FloatType ({float_kind = k}) + | TPtr (t,_) -> + let id = attr_aux t in + PointerType ({pts = id}) + | TArray (t,s,_) -> + let id = attr_aux t in + let arr = { + arr_type = id; + arr_size= s; + } in + ArrayType arr + | TFun (t,param,va,_) -> + let param,prot = (match param with + | None -> [],false + | Some p -> List.map (fun (i,t) -> let t = attr_aux t in + { + param_type = t; + param_name = i.name; + }) p,true) in + let ret = attr_aux t in + let ftype = { + fun_return_type = ret; + fun_prototyped = prot; + fun_params = param; + } in + FunctionType ftype + | TNamed (id,_) -> + let t = { + typedef_name = id.name; + typ = None; + } in + Typedef t + | TStruct (id,_) -> + let str = + { + ct_name = id.name; + ct_file_loc = None; + ct_members = []; + ct_alignof = None; + ct_sizeof = None; + } in + StructType str + | TUnion (id,_) -> + let union = + { + ct_name = id.name; + ct_file_loc = None; + ct_members = []; + ct_alignof = None; + ct_sizeof = None; + } in + UnionType union + | TEnum (id,_) -> + let enum = + { + enum_name = id.name; + enum_byte_size = None; + enum_file_loc = None; + enum_enumerators = []; + } in + EnumType enum in + insert d_ty ty + and attr_aux ty = + try + find_type ty + with + Not_found -> match strip_last_attribute ty with | Some AConst,t -> - () + let id = attr_aux t in + let const = { const_type = id} in + insert (ConstType const) ty + | Some AVolatile,t -> + let id = attr_aux t in + let volatile = {volatile_type = id} in + insert (VolatileType volatile) ty + | Some (ARestrict|AAlignas _| Attr(_,_)),t -> + attr_aux t | None,t -> typ_aux t - in - attr_aux ty - end + in + attr_aux ty + +(* Replace the struct information *) +let replace_struct id f = + let str = Hashtbl.find all_types id in + match str with + | StructType comp -> let comp' = f comp in + if comp <> comp' then Hashtbl.replace all_types id (StructType comp') + | _ -> assert false (* This should never happen *) + +(* Replace the union information *) +let replace_union id f = + let union = Hashtbl.find all_types id in + match union with + | UnionType comp -> let comp' = f comp in + if comp <> comp' then Hashtbl.replace all_types id (UnionType comp') + | _ -> assert false (* This should never happen *) + +(* Replace the typdef information *) +let replace_typedef id f = + let typdef = Hashtbl.find all_types id in + match typdef with + | Typedef typ -> let typ' = f typ in + if typ <> typ' then Hashtbl.replace all_types id (Typedef typ') + | _ -> assert false (* This should never happen *) + +(* Types for global definitions *) + +(* Information for a global variable *) +type global_variable = { + gvar_name: string; + gvar_atom: atom option; + gvar_file_loc: location; + gvar_declaration: bool; + gvar_external: bool; + gvar_type: int; + } + +type definition_type = + | GlobalVariable of global_variable + +(* All definitions encountered *) +let definitions: (int,definition_type) Hashtbl.t = Hashtbl.create 7 + +(* Mapping from stamp to debug id *) +let stamp_to_definition: (int,int) Hashtbl.t = Hashtbl.create 7 + +let find_var_stamp id = + let id = (Hashtbl.find stamp_to_definition id) in + let var = Hashtbl.find definitions id in + match var with + | GlobalVariable var -> id,var + +let replace_var id var = + let var = GlobalVariable var in + Hashtbl.replace definitions id var + +let insert_declaration dec env = + let insert d_dec stamp = + let id = next_id () in + Hashtbl.add definitions id d_dec; + Hashtbl.add stamp_to_definition stamp id + in + match dec.gdesc with + | Gdecl (sto,id,ty,init) -> + if not (is_function_type env ty) then begin + if not (Hashtbl.mem stamp_to_definition id.stamp) then begin + let at_decl,ext = (match sto with + | Storage_extern -> init = None,true + | Storage_static -> false,false + | _ -> false,true) in + let ty = insert_type ty in + let decl = { + gvar_name = id.name; + gvar_atom = None; + gvar_file_loc = dec.gloc; + gvar_declaration = at_decl; + gvar_external = ext; + gvar_type = ty; + } in + insert (GlobalVariable decl) id.stamp + end else if init <> None || sto <> Storage_extern then begin (* It is a definition *) + let id,var = find_var_stamp id.stamp in + replace_var id ({var with gvar_declaration = false;}) + end + end + | Gfundef _ -> () + | Gcompositedecl (Struct,id,at) -> + ignore (insert_type (TStruct (id,at))); + let id = find_type (TStruct (id,[])) in + replace_struct id (fun comp -> if comp.ct_file_loc = None then + {comp with ct_file_loc = Some (dec.gloc);} + else comp) + | Gcompositedecl (Union,id,at) -> + ignore (insert_type (TUnion (id,at))); + let id = find_type (TUnion (id,[])) in + replace_union id (fun comp -> if comp.ct_file_loc = None then + {comp with ct_file_loc = Some (dec.gloc);} + else comp) + | Gcompositedef _ -> () + | Gtypedef (id,t) -> + let id = insert_type (TNamed (id,[])) in + let tid = insert_type t in + replace_typedef id (fun typ -> {typ with typ = Some tid;}); + | Genumdef _ -> () + | Gpragma _ -> () |