diff options
| -rw-r--r-- | debug/Debug.ml | 27 | ||||
| -rw-r--r-- | debug/Debug.mli | 7 | ||||
| -rw-r--r-- | debug/DebugInformation.ml | 17 | ||||
| -rw-r--r-- | debug/Dwarfgen.ml | 1 | ||||
| -rw-r--r-- | powerpc/Asmexpand.ml | 109 |
5 files changed, 152 insertions, 9 deletions
diff --git a/debug/Debug.ml b/debug/Debug.ml index c2b48618..fba921e1 100644 --- a/debug/Debug.ml +++ b/debug/Debug.ml @@ -10,6 +10,8 @@ (* *) (* *********************************************************************) +open AST +open BinNums open C open Camlcoq open Dwarfgen @@ -35,6 +37,11 @@ type implem = mutable enter_scope: int -> int -> int -> unit; mutable enter_function_scope: int -> int -> unit; 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 end_live_range: atom -> positive -> unit; + mutable stack_variable: atom -> string builtin_arg -> unit } let implem = @@ -54,6 +61,11 @@ let implem = enter_scope = (fun _ _ _ -> ()); enter_function_scope = (fun _ _ -> ()); add_lvar_scope = (fun _ _ _ -> ()); + open_scope = (fun _ _ _ -> ()); + close_scope = (fun _ _ _ -> ()); + start_live_range = (fun _ _ _ -> ()); + end_live_range = (fun _ _ -> ()); + stack_variable = (fun _ _ -> ()); } let init () = @@ -73,6 +85,11 @@ let init () = implem.enter_scope <- DebugInformation.enter_scope; implem.enter_function_scope <- DebugInformation.enter_function_scope; implem.add_lvar_scope <- DebugInformation.add_lvar_scope; + implem.open_scope <- DebugInformation.open_scope; + implem.close_scope <- DebugInformation.close_scope; + implem.start_live_range <- DebugInformation.start_live_range; + implem.end_live_range <- DebugInformation.end_live_range; + implem.stack_variable <- DebugInformation.stack_variable; end else begin implem.init <- (fun _ -> ()); implem.atom_function <- (fun _ _ -> ()); @@ -89,6 +106,11 @@ let init () = implem.enter_scope <- (fun _ _ _ -> ()); implem.enter_function_scope <- (fun _ _ -> ()); implem.add_lvar_scope <- (fun _ _ _ -> ()); + implem.open_scope <- (fun _ _ _ -> ()); + implem.close_scope <- (fun _ _ _ -> ()); + implem.start_live_range <- (fun _ _ _ -> ()); + implem.end_live_range <- (fun _ _ -> ()); + implem.stack_variable <- (fun _ _ -> ()); end let init_compile_unit name = implem.init name @@ -106,3 +128,8 @@ let atom_local_variable id atom = implem.atom_local_variable id atom let enter_scope p_id id = implem.enter_scope p_id id let enter_function_scope fun_id sc_id = implem.enter_function_scope fun_id sc_id let add_lvar_scope fun_id var_id s_id = implem.add_lvar_scope fun_id var_id s_id +let open_scope atom id lbl = implem.open_scope atom id lbl +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 diff --git a/debug/Debug.mli b/debug/Debug.mli index 1fabb943..42a0cee7 100644 --- a/debug/Debug.mli +++ b/debug/Debug.mli @@ -10,9 +10,11 @@ (* *) (* *********************************************************************) +open AST open C open Camlcoq open DwarfTypes +open BinNums val init: unit -> unit @@ -31,3 +33,8 @@ val atom_local_variable: ident -> atom -> unit val enter_scope: int -> int -> int -> unit 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 end_live_range: atom -> positive -> unit +val stack_variable: atom -> string builtin_arg -> unit diff --git a/debug/DebugInformation.ml b/debug/DebugInformation.ml index 80d71dfd..f12853c9 100644 --- a/debug/DebugInformation.ml +++ b/debug/DebugInformation.ml @@ -478,7 +478,6 @@ let insert_global_declaration env dec= in match dec.gdesc with | Gdecl (sto,id,ty,init) -> - Printf.printf "Entering information for %s\n" id.name; 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 @@ -660,6 +659,21 @@ let enter_scope f_id p_id id = replace_scope p_id' ({scope_variables = id'::scope.scope_variables;}) with Not_found -> () +let open_scope atom s_id lbl = + () + +let close_scope atom s_id lbl = + () + +let start_live_range atom lbl loc = + () + +let end_live_range atom lbl = + () + +let stack_variable atom loc = + () + let init name = id := 0; file_name := name; @@ -672,4 +686,3 @@ let init name = Hashtbl.reset stamp_to_local; Hashtbl.reset atom_to_local; Hashtbl.reset scope_to_local; - diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml index 15c63b66..6c10b362 100644 --- a/debug/Dwarfgen.ml +++ b/debug/Dwarfgen.ml @@ -315,7 +315,6 @@ let fun_scope_to_entries acc id = | _ -> assert false) let function_to_entry acc id f = - Printf.printf "Generating information for %s with id %d\n" f.fun_name id; let f_tag = { subprogram_file_loc = f.fun_file_loc; subprogram_external = Some f.fun_external; diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index b9fe1d7f..d4675e5f 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -512,7 +512,7 @@ let num_crbit = function | CRbit_3 -> 3 | CRbit_6 -> 6 -let expand_instruction instr = +let expand_instruction_simple instr = match instr with | Pallocframe(sz, ofs,retofs) -> let variadic = (!current_function).fn_sig.sig_cc.cc_vararg in @@ -586,22 +586,119 @@ let expand_instruction instr = | _ -> emit instr -let expand_function fn = +let preg_to_string p = + "" + +let rec translate_annot a = + match a with + | BA x -> BA (preg_to_string x) + | BA_int n -> BA_int n + | BA_long n -> BA_long n + | BA_float n -> BA_float n + | BA_single n -> BA_single n + | BA_loadstack (chunk,ofs) -> BA_loadstack (chunk,ofs) + | BA_addrstack ofs -> BA_addrstack ofs + | BA_loadglobal (chunk,id,ofs) -> BA_loadglobal (chunk,id,ofs) + | BA_addrglobal (id,ofs) -> BA_addrglobal (id,ofs) + | BA_splitlong (hi,lo) -> BA_splitlong (translate_annot hi,translate_annot lo) + +let expand_stack_loc txt = function + | [a] -> Debug.stack_variable txt (translate_annot a) + | _ -> assert false + +let expand_start_live_range txt lbl = function + | [a] -> Debug.start_live_range txt lbl (translate_annot a) + | _ -> assert false + +let expand_end_live_range = + Debug.end_live_range + +let expand_scope id lbl oldscopes newscopes = + let opening = List.filter (fun a -> List.mem a oldscopes) newscopes + and closing = List.filter (fun a -> List.mem a newscopes) oldscopes in + List.iter (fun i -> Debug.open_scope id i lbl) opening; + List.iter (fun i -> Debug.close_scope id i lbl) closing + +let expand_instruction id l = + let get_lbl = function + | None -> + let lbl = new_label () in + emit (Plabel lbl); + lbl + | Some lbl -> lbl in + let rec aux lbl scopes = function + | [] -> () + | (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i)::rest -> + let kind = (P.to_int kind) in + begin + match kind with + | 1 -> + emit i; aux lbl scopes rest + | 2 -> + aux lbl scopes rest + | 3 -> + let lbl = get_lbl lbl in + expand_start_live_range txt lbl args; + aux (Some lbl) scopes rest + | 4 -> + let lbl = get_lbl lbl in + expand_end_live_range txt lbl; + aux (Some lbl) scopes rest + | 5 -> + expand_stack_loc txt args; + aux lbl scopes rest + | 6 -> + let lbl = get_lbl lbl in + let scopes' = List.map (function BA_int x -> Int32.to_int (camlint_of_coqint x) | _ -> assert false) args in + expand_scope id lbl scopes scopes'; + aux (Some lbl) scopes' rest + | _ -> + emit i; aux None scopes rest + end + | i::rest -> expand_instruction_simple i; aux None scopes rest in + aux None [] l + + +let expand_function id fn = try set_current_function fn; - List.iter expand_instruction fn.fn_code; + if !Clflags.option_g then + expand_instruction id fn.fn_code + else + List.iter expand_instruction_simple fn.fn_code; Errors.OK (get_current_function ()) with Error s -> Errors.Error (Errors.msg (coqstring_of_camlstring s)) -let expand_fundef = function +let expand_fundef id = function | Internal f -> - begin match expand_function f with + begin match expand_function id f with | Errors.OK tf -> Errors.OK (Internal tf) | Errors.Error msg -> Errors.Error msg end | External ef -> Errors.OK (External ef) +let rec transform_partial_prog transfun p = + match p with + | [] -> Errors.OK [] + | (id,Gvar v)::l -> + (match transform_partial_prog transfun l with + | Errors.OK x -> Errors.OK ((id,Gvar v)::x) + | Errors.Error msg -> Errors.Error msg) + | (id,Gfun f)::l -> + (match transfun id f with + | Errors.OK tf -> + (match transform_partial_prog transfun l with + | Errors.OK x -> Errors.OK ((id,Gfun tf)::x) + | Errors.Error msg -> Errors.Error msg) + | Errors.Error msg -> + Errors.Error ((Errors.MSG (coqstring_of_camlstring "In function"))::((Errors.CTX + id) :: (Errors.MSG (coqstring_of_camlstring ": ") :: msg)))) + let expand_program (p: Asm.program) : Asm.program Errors.res = - AST.transform_partial_program expand_fundef p + match transform_partial_prog expand_fundef p.prog_defs with + | Errors.OK x-> + Errors.OK { prog_defs = x; prog_public = p.prog_public; prog_main = + p.prog_main } + | Errors.Error msg -> Errors.Error msg |