aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--debug/CtoDwarf.ml46
-rw-r--r--debug/Debug.ml61
-rw-r--r--debug/Debug.mli23
-rw-r--r--debug/DebugInformation.ml58
-rw-r--r--driver/Driver.ml1
5 files changed, 177 insertions, 12 deletions
diff --git a/debug/CtoDwarf.ml b/debug/CtoDwarf.ml
index dce8d81e..3a325665 100644
--- a/debug/CtoDwarf.ml
+++ b/debug/CtoDwarf.ml
@@ -19,9 +19,8 @@ open DwarfTypes
open DwarfUtil
open Env
open Set
-open DebugInformation
-(* Functions to translate a C Ast into Dwarf 2 debugging information *)
+(* Functions to translate a C Ast into Dwarf 2 debugging information *)
(* Hashtable from type name to entry id *)
let type_table: (string, int) Hashtbl.t = Hashtbl.create 7
@@ -40,6 +39,49 @@ module IntSet = Set.Make(struct type t = int let compare = compare end)
(* Set of all declared composite_types *)
let composite_defined: IntSet.t ref = ref IntSet.empty
+(* Helper functions for the attributes *)
+let strip_attributes typ =
+ 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)
+ | TFloat (k,at) -> TFloat(k,strip at)
+ | TPtr (t,at) -> TPtr(t,strip at)
+ | TArray (t,s,at) -> TArray(t,s,strip at)
+ | TFun (t,arg,v,at) -> TFun(t,arg,v,strip at)
+ | TNamed (n,at) -> TNamed(n,strip at)
+ | TStruct (n,at) -> TStruct(n,strip at)
+ | TUnion (n,at) -> TUnion(n,strip at)
+ | TEnum (n,at) -> TEnum(n,strip at)
+
+let strip_last_attribute typ =
+ let rec hd_opt l = match l with
+ [] -> None,[]
+ | AConst::rest -> Some AConst,rest
+ | AVolatile::rest -> Some AVolatile,rest
+ | _::rest -> hd_opt rest in
+ match typ with
+ | TVoid at -> let l,r = hd_opt at in
+ l,TVoid r
+ | TInt (k,at) -> let l,r = hd_opt at in
+ l,TInt (k,r)
+ | TFloat (k,at) -> let l,r = hd_opt at in
+ l,TFloat (k,r)
+ | TPtr (t,at) -> let l,r = hd_opt at in
+ l,TPtr(t,r)
+ | TArray (t,s,at) -> let l,r = hd_opt at in
+ l,TArray(t,s,r)
+ | TFun (t,arg,v,at) -> let l,r = hd_opt at in
+ l,TFun(t,arg,v,r)
+ | TNamed (n,at) -> let l,r = hd_opt at in
+ l,TNamed(n,r)
+ | TStruct (n,at) -> let l,r = hd_opt at in
+ l,TStruct(n,r)
+ | TUnion (n,at) -> let l,r = hd_opt at in
+ l,TUnion(n,r)
+ | TEnum (n,at) -> let l,r = hd_opt at in
+ l,TEnum(n,r)
+
(* Get the type id of a composite_type *)
let get_composite_type (name: int): int =
try
diff --git a/debug/Debug.ml b/debug/Debug.ml
new file mode 100644
index 00000000..eb195b33
--- /dev/null
+++ b/debug/Debug.ml
@@ -0,0 +1,61 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *)
+(* *)
+(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *)
+(* is distributed under the terms of the INRIA Non-Commercial *)
+(* License Agreement. *)
+(* *)
+(* *********************************************************************)
+
+open C
+open Camlcoq
+
+(* Interface for generating and printing debug information *)
+
+(* Record used for stroring references to the actual implementation functions *)
+type implem =
+ {
+ mutable init: string -> unit;
+ mutable atom_function: ident -> atom -> unit;
+ mutable atom_global_variable: ident -> atom -> unit;
+ mutable set_composite_size: ident -> struct_or_union -> int -> unit;
+ mutable set_member_offset: ident -> string -> int -> int -> unit;
+ mutable insert_declaration: globdecl -> Env.t -> unit;
+ }
+
+let implem =
+ {
+ init = (fun _ -> ());
+ atom_function = (fun _ _ -> ());
+ atom_global_variable = (fun _ _ -> ());
+ set_composite_size = (fun _ _ _ -> ());
+ set_member_offset = (fun _ _ _ _ -> ());
+ insert_declaration = (fun _ _ -> ());
+ }
+
+let init () =
+ if !Clflags.option_g then begin
+ implem.init <- DebugInformation.init;
+ implem.atom_function <- DebugInformation.atom_function;
+ implem.atom_global_variable <- DebugInformation.atom_global_variable;
+ implem.set_composite_size <- DebugInformation.set_composite_size;
+ implem.set_member_offset <- DebugInformation.set_member_offset;
+ implem.insert_declaration <- DebugInformation.insert_declaration;
+ end else begin
+ implem.init <- (fun _ -> ());
+ implem.atom_function <- (fun _ _ -> ());
+ implem.atom_global_variable <- (fun _ _ -> ());
+ implem.set_composite_size <- (fun _ _ _ -> ());
+ implem.set_member_offset <- (fun _ _ _ _ -> ());
+ implem.insert_declaration <- (fun _ _ -> ())
+ end
+
+let init_compile_unit name = implem.init name
+let atom_function id atom = implem.atom_function id atom
+let atom_global_variable id atom = implem.atom_global_variable id atom
+let set_composite_size id sou size = implem.set_composite_size id sou size
+let set_member_offset id field off size = implem.set_member_offset id field off size
+let insert_declaration dec env = implem.insert_declaration dec env
diff --git a/debug/Debug.mli b/debug/Debug.mli
new file mode 100644
index 00000000..ea72aeb4
--- /dev/null
+++ b/debug/Debug.mli
@@ -0,0 +1,23 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *)
+(* *)
+(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *)
+(* is distributed under the terms of the INRIA Non-Commercial *)
+(* License Agreement. *)
+(* *)
+(* *********************************************************************)
+
+open C
+open Camlcoq
+
+
+val init: unit -> unit
+val init_compile_unit: string -> unit
+val atom_function: ident -> atom -> unit
+val atom_global_variable: ident -> atom -> unit
+val set_composite_size: ident -> struct_or_union -> int -> unit
+val set_member_offset: ident -> string -> int -> int -> unit
+val insert_declaration: globdecl -> Env.t -> unit
diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml
index 166a81e8..30d026c7 100644
--- a/debug/DebugInformation.ml
+++ b/debug/DebugInformation.ml
@@ -27,6 +27,9 @@ let next_id () =
let reset_id () =
id := 0
+(* The name of the current compilation unit *)
+let file_name: string ref = ref ""
+
(* Types for the information of type info *)
type composite_field =
@@ -117,7 +120,7 @@ type debug_types =
| Void
(* All types encountered *)
-let all_types: (int,debug_types) Hashtbl.t = Hashtbl.create 7
+let types: (int,debug_types) Hashtbl.t = Hashtbl.create 7
(* Lookup table for types *)
let lookup_types: (string, int) Hashtbl.t = Hashtbl.create 7
@@ -193,7 +196,7 @@ 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 types id d_ty;
Hashtbl.add lookup_types name id;
id in
(* We are only interrested in Const and Volatile *)
@@ -291,26 +294,26 @@ let insert_type (ty: typ) =
(* Replace the composite information *)
let replace_composite id f =
- let str = Hashtbl.find all_types id in
+ let str = Hashtbl.find types id in
match str with
| CompositeType comp -> let comp' = f comp in
- if comp <> comp' then Hashtbl.replace all_types id (CompositeType comp')
+ if comp <> comp' then Hashtbl.replace types id (CompositeType comp')
| _ -> assert false (* This should never happen *)
(* Replace the enum information *)
let replace_enum id f =
- let str = Hashtbl.find all_types id in
+ let str = Hashtbl.find types id in
match str with
| EnumType comp -> let comp' = f comp in
- if comp <> comp' then Hashtbl.replace all_types id (EnumType comp')
+ if comp <> comp' then Hashtbl.replace types id (EnumType comp')
| _ -> assert false (* This should never happen *)
(* Replace the typdef information *)
let replace_typedef id f =
- let typdef = Hashtbl.find all_types id in
+ let typdef = Hashtbl.find types id in
match typdef with
| Typedef typ -> let typ' = f typ in
- if typ <> typ' then Hashtbl.replace all_types id (Typedef typ')
+ if typ <> typ' then Hashtbl.replace types id (Typedef typ')
| _ -> assert false (* This should never happen *)
(* Types for global definitions *)
@@ -353,6 +356,9 @@ 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
+(* Mapping from atom to debug id *)
+let atom_to_definition: (atom, 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
@@ -360,10 +366,22 @@ let find_var_stamp id =
| GlobalVariable var -> id,var
| _ -> assert false
+let find_fun_stamp id =
+ let id = (Hashtbl.find stamp_to_definition id) in
+ let f = Hashtbl.find definitions id in
+ match f with
+ | Function f -> id,f
+ | _ -> assert false
+
+
let replace_var id var =
let var = GlobalVariable var in
Hashtbl.replace definitions id var
+let replace_fun id f =
+ let f = Function f in
+ Hashtbl.replace definitions id f
+
let gen_comp_typ sou id at =
if sou = Struct then
TStruct (id,at)
@@ -463,7 +481,7 @@ let insert_declaration dec env =
{en with enum_file_loc = Some dec.gloc; enum_enumerators = enumerator;})
| Gpragma _ -> ()
-let set_offset str field (offset,byte_size) =
+let set_member_offset str field offset byte_size =
let id = find_type (TStruct (str,[])) in
replace_composite id (fun comp ->
let name f = f.cfd_name = field || match f.cfd_bitfield with Some n -> n = field | _ -> false in
@@ -472,6 +490,26 @@ let set_offset str field (offset,byte_size) =
else a) comp.ct_members in
{comp with ct_members = members;})
-let set_size comp sou size =
+let set_composite_size comp sou size =
let id = find_type (gen_comp_typ sou comp []) in
replace_composite id (fun comp -> {comp with ct_sizeof = Some size;})
+
+let atom_global_variable id atom =
+ let id,var = find_var_stamp id.stamp in
+ replace_var id ({var with gvar_atom = Some atom;});
+ Hashtbl.add atom_to_definition atom id
+
+let atom_function id atom =
+ let id,f = find_fun_stamp id.stamp in
+ replace_fun id ({f with fun_atom = Some atom;});
+ Hashtbl.add atom_to_definition atom id
+
+let init name =
+ id := 0;
+ file_name := name;
+ Hashtbl.reset types;
+ Hashtbl.reset lookup_types;
+ Hashtbl.reset definitions;
+ Hashtbl.reset stamp_to_definition;
+ Hashtbl.reset atom_to_definition
+
diff --git a/driver/Driver.ml b/driver/Driver.ml
index f53de821..04acf902 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -682,6 +682,7 @@ let _ =
Builtins.set C2C.builtins;
CPragmas.initialize();
parse_cmdline cmdline_actions;
+ Debug.init (); (* Initialize the debug functions *)
let nolink = !option_c || !option_S || !option_E || !option_interp in
if nolink && !option_o <> None && !num_source_files >= 2 then begin
eprintf "Ambiguous '-o' option (multiple source files)\n";
generated by cgit (git 2.34.1) at 2024-06-12 00:10:05 +0000