diff options
Diffstat (limited to 'backend/Asmexpandaux.ml')
-rw-r--r-- | backend/Asmexpandaux.ml | 98 |
1 files changed, 94 insertions, 4 deletions
diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml index 6ce6c005..3d1dd754 100644 --- a/backend/Asmexpandaux.ml +++ b/backend/Asmexpandaux.ml @@ -11,13 +11,13 @@ (* *) (* *********************************************************************) -(* Util functions used for the expansion of built-ins and some +(* Util functions used for the expansion of built-ins and some pseudo-instructions *) open Asm open AST open Camlcoq - + (* Buffering the expanded code *) let current_code = ref ([]: instruction list) @@ -25,7 +25,7 @@ let current_code = ref ([]: instruction list) let emit i = current_code := i :: !current_code (* Generation of fresh labels *) - + let dummy_function = { fn_code = []; fn_sig = signature_main } let current_function = ref dummy_function let next_label = ref (None: label option) @@ -46,7 +46,7 @@ let new_label () = next_label := Some (P.succ lbl); lbl - + let set_current_function f = current_function := f; next_label := None; current_code := [] @@ -55,3 +55,93 @@ let get_current_function () = let fn = !current_function in set_current_function dummy_function; {fn with fn_code = c} + +(* Expand function for debug information *) + +let expand_scope id lbl oldscopes newscopes = + let opening = List.filter (fun a -> not (List.mem a oldscopes)) newscopes + and closing = List.filter (fun a -> not (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 translate_annot sp preg_to_dwarf annot = + let rec aux = function + | BA x -> Some (sp,BA (preg_to_dwarf x)) + | BA_int _ + | BA_long _ + | BA_float _ + | BA_single _ + | BA_loadglobal _ + | BA_addrglobal _ + | BA_loadstack _ -> None + | BA_addrstack ofs -> Some (sp,BA_addrstack ofs) + | BA_splitlong (hi,lo) -> + begin + match (aux hi,aux lo) with + | Some (_,hi) ,Some (_,lo) -> Some (sp,BA_splitlong (hi,lo)) + | _,_ -> None + end in + (match annot with + | [] -> None + | a::_ -> aux a) + + +let expand_debug id sp preg simple 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 -> + begin + match translate_annot sp preg args with + | Some a -> + let lbl = get_lbl lbl in + Debug.start_live_range (id,txt) lbl a; + aux (Some lbl) scopes rest + | None -> aux lbl scopes rest + end + | 4 -> + let lbl = get_lbl lbl in + Debug.end_live_range (id,txt) lbl; + aux (Some lbl) scopes rest + | 5 -> + begin + match translate_annot sp preg args with + | Some a-> + Debug.stack_variable (id,txt) a; + aux lbl scopes rest + | _ -> aux lbl scopes rest + end + | 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 + | _ -> + aux None scopes rest + end + | (Plabel lbl)::rest -> simple (Plabel lbl); aux (Some lbl) scopes rest + | i::rest -> simple i; aux None scopes rest in + (* We need to move all closing debug annotations before the last real statement *) + let rec move_debug acc bcc = function + | (Pbuiltin(EF_debug (kind,_,_),_,_) as i)::rest -> + let kind = (P.to_int kind) in + if kind = 1 then + move_debug acc (i::bcc) rest (* Do not move debug line *) + else + move_debug (i::acc) bcc rest (* Move the debug annotations forward *) + | b::rest -> List.rev ((List.rev (b::bcc)@List.rev acc)@rest) (* We found the first non debug location *) + | [] -> List.rev acc (* This actually can never happen *) in + aux None [] (move_debug [] [] (List.rev l)) |