aboutsummaryrefslogtreecommitdiffstats
path: root/debug
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-09-16 11:10:28 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-09-16 11:10:28 +0200
commit3344bcf59acb1ae8d43a0d15acb4b824689e706d (patch)
treea5621a5d30ee7e39e2e6d2a95e02ab018e8ef846 /debug
parent36fe88d4cc2022947474a2fcc0b650e22f41ee3e (diff)
downloadcompcert-kvx-3344bcf59acb1ae8d43a0d15acb4b824689e706d.tar.gz
compcert-kvx-3344bcf59acb1ae8d43a0d15acb4b824689e706d.zip
Add the debug interface file.
The new file Debug.ml contains the interface for generating and printing debug information. In order to generate debug information the init function initializes the necessary functions depending on the -g flag. If the -g is not there all functions are dummy functions which do nothing.
Diffstat (limited to 'debug')
-rw-r--r--debug/CtoDwarf.ml46
-rw-r--r--debug/Debug.ml61
-rw-r--r--debug/Debug.mli23
-rw-r--r--debug/DebugInformation.ml58
4 files changed, 176 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
+