diff options
Diffstat (limited to 'powerpc')
-rw-r--r-- | powerpc/AsmToJSON.ml | 5 | ||||
-rw-r--r-- | powerpc/Asmexpand.ml | 150 | ||||
-rw-r--r-- | powerpc/TargetPrinter.ml | 114 |
3 files changed, 201 insertions, 68 deletions
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index a7e66701..5764aa8f 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -330,8 +330,9 @@ let p_section oc = function | Section_literal -> fprintf oc "{\"Section Name\":\"Literal\"}" | Section_jumptable -> fprintf oc "{\"Section Name\":\"Jumptable\"}" | Section_user (s,w,e) -> fprintf oc "{\"Section Name\":%s,\"Writable\":%B,\"Executable\":%B}" s w e - | Section_debug_info - | Section_debug_abbrev -> () (* There should be no info in the debug sections *) + | Section_debug_info _ + | Section_debug_abbrev + | Section_debug_loc -> () (* There should be no info in the debug sections *) let p_int_opt oc = function | None -> fprintf oc "0" diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index fc0fc44e..5a365123 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -563,7 +563,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 @@ -637,22 +637,160 @@ let expand_instruction instr = | _ -> emit instr -let expand_function fn = +(* Translate to the integer identifier of the register as + the EABI specifies *) + +let int_reg_to_dwarf = function + | GPR0 -> 0 | GPR1 -> 1 | GPR2 -> 2 | GPR3 -> 3 + | GPR4 -> 4 | GPR5 -> 5 | GPR6 -> 6 | GPR7 -> 7 + | GPR8 -> 8 | GPR9 -> 9 | GPR10 -> 10 | GPR11 -> 11 + | GPR12 -> 12 | GPR13 -> 13 | GPR14 -> 14 | GPR15 -> 15 + | GPR16 -> 16 | GPR17 -> 17 | GPR18 -> 18 | GPR19 -> 19 + | GPR20 -> 20 | GPR21 -> 21 | GPR22 -> 22 | GPR23 -> 23 + | GPR24 -> 24 | GPR25 -> 25 | GPR26 -> 26 | GPR27 -> 27 + | GPR28 -> 28 | GPR29 -> 29 | GPR30 -> 30 | GPR31 -> 31 + +let float_reg_to_dwarf = function + | FPR0 -> 32 | FPR1 -> 33 | FPR2 -> 34 | FPR3 -> 35 + | FPR4 -> 36 | FPR5 -> 37 | FPR6 -> 38 | FPR7 -> 39 + | FPR8 -> 40 | FPR9 -> 41 | FPR10 -> 42 | FPR11 -> 43 + | FPR12 -> 44 | FPR13 -> 45 | FPR14 -> 46 | FPR15 -> 47 + | FPR16 -> 48 | FPR17 -> 49 | FPR18 -> 50 | FPR19 -> 51 + | FPR20 -> 52 | FPR21 -> 53 | FPR22 -> 54| FPR23 -> 55 + | FPR24 -> 56 | FPR25 -> 57 | FPR26 -> 58 | FPR27 -> 59 + | FPR28 -> 60 | FPR29 -> 61 | FPR30 -> 62 | FPR31 -> 63 + +let preg_to_dwarf_int = function + | IR r -> int_reg_to_dwarf r + | FR r -> float_reg_to_dwarf r + | _ -> assert false + + +let translate_annot annot = + let rec aux = function + | BA x -> Some (BA (preg_to_dwarf_int x)) + | BA_int _ + | BA_long _ + | BA_float _ + | BA_single _ + | BA_loadglobal _ + | BA_addrglobal _ + | BA_loadstack _ -> None + | BA_addrstack ofs -> Some (BA_addrstack ofs) + | BA_splitlong (hi,lo) -> + begin + match (aux hi,aux lo) with + | Some hi ,Some lo -> Some (BA_splitlong (hi,lo)) + | _,_ -> None + end in + (match annot with + | [] -> None + | a::_ -> aux a) + +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 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 + | [] -> let lbl = get_lbl lbl in + Debug.function_end id lbl + | (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i)::rest -> + let kind = (P.to_int kind) in + emit i; + begin + match kind with + | 1-> + aux lbl scopes rest + | 2 -> + aux lbl scopes rest + | 3 -> + begin + match translate_annot args with + | Some a -> + let lbl = get_lbl lbl in + Debug.start_live_range txt lbl (1,a); + aux (Some lbl) scopes rest + | None -> aux lbl scopes rest + end + | 4 -> + let lbl = get_lbl lbl in + Debug.end_live_range txt lbl; + aux (Some lbl) scopes rest + | 5 -> + begin + match translate_annot args with + | Some a-> + Debug.stack_variable txt (1,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 + | i::rest -> expand_instruction_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 = function + | (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i)::rest -> + move_debug (i::acc) rest (* Move the debug annotations forward *) + | b::rest -> List.rev (b::(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)) + + +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 diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index eca7a1b8..3c73f22d 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -78,6 +78,8 @@ let end_addr = ref (-1) let stmt_list_addr = ref (-1) +let debug_start_addr = ref (-1) + let label = elf_label module Linux_System : SYSTEM = @@ -129,9 +131,10 @@ module Linux_System : SYSTEM = | Section_user(s, wr, ex) -> sprintf ".section \"%s\",\"a%s%s\",@progbits" s (if wr then "w" else "") (if ex then "x" else "") - | Section_debug_info -> ".debug_info,\"\",@progbits" + | Section_debug_info _ -> ".debug_info,\"\",@progbits" | Section_debug_abbrev -> ".debug_abbrev,\"\",@progbits" - + | Section_debug_loc -> ".debug_loc,\"\",@progbits" + let section oc sec = let name = name_of_section sec in assert (name <> "COMM"); @@ -207,14 +210,20 @@ module Diab_System : SYSTEM = | true, false -> 'd' (* data *) | false, true -> 'c' (* text *) | false, false -> 'r') (* const *) - | Section_debug_info -> ".debug_info,,n" - | Section_debug_abbrev -> ".debug_abbrev,,n" + | Section_debug_info s -> sprintf ".section .debug_info%s,,n" (if s <> ".text" then s else "") + | Section_debug_abbrev -> ".section .debug_abbrev,,n" + | Section_debug_loc -> ".section .debug_loc,,n" let section oc sec = let name = name_of_section sec in assert (name <> "COMM"); - fprintf oc " %s\n" name - + match sec with + | Section_debug_info s -> + fprintf oc " %s\n" name; + if s <> ".text" then + fprintf oc " .sectionlink .debug_info\n" + | _ -> + fprintf oc " %s\n" name let print_file_line oc file line = print_file_line_d2 oc comment file line @@ -229,65 +238,51 @@ module Diab_System : SYSTEM = let cfi_rel_offset oc reg ofs = () let print_prologue oc = - fprintf oc " .xopt align-fill-text=0x60000000\n"; - if !Clflags.option_g then - begin - fprintf oc " .text\n"; - fprintf oc " .section .debug_line,,n\n"; - let label_line_start = new_label () in - stmt_list_addr := label_line_start; - fprintf oc "%a:\n" label label_line_start; - fprintf oc " .text\n"; - let label_start = new_label () in - start_addr := label_start; - fprintf oc "%a:\n" label label_start; - fprintf oc " .d2_line_start .debug_line\n"; - end - - let filenum : (string,int) Hashtbl.t = Hashtbl.create 7 - - let additional_debug_sections: StringSet.t ref = ref StringSet.empty - + fprintf oc " .xopt align-fill-text=0x60000000\n" let print_epilogue oc = - if !Clflags.option_g then - begin - fprintf oc "\n"; - let label_end = new_label () in - end_addr := label_end; - fprintf oc "%a:\n" label label_end; - fprintf oc " .text\n"; - StringSet.iter (fun file -> - let label = new_label () in - Hashtbl.add filenum file label; - fprintf oc ".L%d: .d2filenum \"%s\"\n" label file) !all_files; - fprintf oc " .d2_line_end\n"; - StringSet.iter (fun s -> - fprintf oc " %s\n" s; - fprintf oc " .d2_line_end\n") !additional_debug_sections - end + let end_label sec = + fprintf oc "\n"; + fprintf oc " %s\n" sec; + let label_end = new_label () in + fprintf oc "%a:\n" label label_end; + label_end + and entry_label f = + let label = new_label () in + fprintf oc ".L%d: .d2filenum \"%s\"\n" label f; + label + and end_line () = fprintf oc " .d2_line_end\n" in + Debug.compute_file_enum end_label entry_label end_line let print_file_loc oc (file,col) = - fprintf oc " .4byte %a\n" label (Hashtbl.find filenum file); + fprintf oc " .4byte 1\n";(* label (Hashtbl.find filenum file);*) fprintf oc " .uleb128 %d\n" col let debug_section oc sec = - if !Clflags.option_g && Configuration.advanced_debug then - match sec with - | Section_user (name,_,_) -> - let sec_name = name_of_section sec in - if not (StringSet.mem sec_name !additional_debug_sections) then - begin - let name = ".debug_line"^name in - additional_debug_sections := StringSet.add sec_name !additional_debug_sections; - fprintf oc " .section %s,,n\n" name; - fprintf oc " .sectionlink .debug_line\n"; - section oc sec; - fprintf oc " .d2_line_start %s\n" name - end - | _ -> () (* Only the case of a user section is interresting *) - else - () + match sec with + | Section_debug_abbrev + | Section_debug_info _ + | Section_debug_loc -> () + | sec -> + let name = match sec with + | Section_user (name,_,_) -> name + | _ -> name_of_section sec in + if not (Debug.exists_section name) then + let line_start = new_label () + and low_pc = new_label () + and debug_info = new_label () in + Debug.add_compilation_section_start name (line_start,low_pc,debug_info,name_of_section sec); + let line_name = ".debug_line" ^(if name <> ".text" then name else "") in + fprintf oc " .section %s,,n\n" line_name; + if name <> ".text" then + fprintf oc " .sectionlink .debug_line\n"; + fprintf oc "%a:\n" label line_start; + section oc sec; + fprintf oc "%a:\n" label low_pc; + fprintf oc " .0byte %a\n" label debug_info; + fprintf oc " .d2_line_start %s\n" line_name + else + () end @@ -855,14 +850,13 @@ module Target (System : SYSTEM):TARGET = let get_stmt_list_addr () = !stmt_list_addr - module DwarfAbbrevs = DwarfUtil.DefaultAbbrevs + let get_debug_start_addr () = !debug_start_addr let new_label = new_label let section oc sec = section oc sec; debug_section oc sec - end let sel_target () = |