diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-07-06 12:51:42 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-07-06 12:51:42 +0200 |
commit | e30aa60a06817ed67c14a80430a7275defc41e76 (patch) | |
tree | b4bb512416a40578db1f32eb3a7836ddb6f8582d /powerpc | |
parent | aa780c7145a418b4a7264e828258034fc4629313 (diff) | |
parent | 2f31c1867b75040067a1ef74ae32f197e8d296c1 (diff) | |
download | compcert-e30aa60a06817ed67c14a80430a7275defc41e76.tar.gz compcert-e30aa60a06817ed67c14a80430a7275defc41e76.zip |
Merge branch 'master' into json_export
Conflicts:
driver/Driver.ml
Diffstat (limited to 'powerpc')
-rw-r--r-- | powerpc/Asm.v | 4 | ||||
-rw-r--r-- | powerpc/AsmToJSON.ml | 2 | ||||
-rw-r--r-- | powerpc/Asmexpand.ml | 2 | ||||
-rw-r--r-- | powerpc/TargetPrinter.ml | 61 |
4 files changed, 54 insertions, 15 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 3fa7af31..a1d8338a 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -161,7 +161,7 @@ Inductive instruction : Type := | Pcmplwi: ireg -> constant -> instruction (**r same, with immediate argument *) | Pcmpw: ireg -> ireg -> instruction (**r signed integer comparison *) | Pcmpwi: ireg -> constant -> instruction (**r same, with immediate argument *) - | Pcntlz: ireg -> ireg -> instruction (**r count leading zeros *) + | Pcntlzw: ireg -> ireg -> instruction (**r count leading zeros *) | Pcreqv: crbit -> crbit -> crbit -> instruction (**r not-xor between condition bits *) | Pcror: crbit -> crbit -> crbit -> instruction (**r or between condition bits *) | Pcrxor: crbit -> crbit -> crbit -> instruction (**r xor between condition bits *) @@ -853,7 +853,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out (** The following instructions and directives are not generated directly by Asmgen, so we do not model them. *) | Pbdnz _ - | Pcntlz _ _ + | Pcntlzw _ _ | Pcreqv _ _ _ | Pcrxor _ _ _ | Peieio diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 4c3f9d97..36960821 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -171,7 +171,7 @@ let p_instruction oc ic = | Pcmplwi (ir,c) -> fprintf oc "{\"Instruction Name\":\"Pcmplwi\",\"Args\":[%a,%a]}" p_ireg ir p_constant c | Pcmpw (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pcmpw\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Pcmpwi (ir,c) -> fprintf oc "{\"Instruction Name\":\"Pcmpwi\",\"Args\":[%a,%a]}" p_ireg ir p_constant c - | Pcntlz (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pcntlz\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 + | Pcntlzw (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pcntlzw\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2 | Pcreqv (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcreqv\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3 | Pcror (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcror\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3 | Pcrxor (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcrxor\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3 diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 699c841f..3f4dc94b 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -343,7 +343,7 @@ let expand_builtin_inline name args res = | "__builtin_mulhwu", [IR a1; IR a2], [IR res] -> emit (Pmulhwu(res, a1, a2)) | "__builtin_clz", [IR a1], [IR res] -> - emit (Pcntlz(res, a1)) + emit (Pcntlzw(res, a1)) | ("__builtin_bswap" | "__builtin_bswap32"), [IR a1], [IR res] -> emit (Pstwu(a1, Cint _m8, GPR1)); emit (Pcfi_adjust _8); diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 2d47acb0..1cd7fe37 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -30,8 +30,8 @@ module type SYSTEM = val constant: out_channel -> constant -> unit val ireg: out_channel -> ireg -> unit val freg: out_channel -> freg -> unit - val creg: out_channel -> int -> unit val name_of_section: section_name -> string + val creg: out_channel -> int -> unit val print_file_line: out_channel -> string -> int -> unit val cfi_startproc: out_channel -> unit val cfi_endproc: out_channel -> unit @@ -40,6 +40,8 @@ module type SYSTEM = val print_prologue: out_channel -> unit val print_epilogue: out_channel -> unit val print_file_loc: out_channel -> DwarfTypes.file_loc -> unit + val section: out_channel -> section_name -> unit + val debug_section: out_channel -> section_name -> unit end let symbol = elf_symbol @@ -129,6 +131,11 @@ module Linux_System : SYSTEM = s (if wr then "w" else "") (if ex then "x" else "") | Section_debug_info -> ".debug_info,\"\",@progbits" | Section_debug_abbrev -> ".debug_abbrev,\"\",@progbits" + + let section oc sec = + let name = name_of_section sec in + assert (name <> "COMM"); + fprintf oc " %s\n" name let print_file_line oc file line = @@ -148,7 +155,8 @@ module Linux_System : SYSTEM = let print_epilogue oc = () let print_file_loc _ _ = () - + + let debug_section _ _ = () end module Diab_System : SYSTEM = @@ -202,6 +210,12 @@ module Diab_System : SYSTEM = | Section_debug_info -> ".debug_info,,n" | Section_debug_abbrev -> ".debug_abbrev,,n" + let section oc sec = + let name = name_of_section sec in + assert (name <> "COMM"); + fprintf oc " %s\n" name + + let print_file_line oc file line = print_file_line_d2 oc comment file line @@ -232,6 +246,9 @@ module Diab_System : SYSTEM = let filenum : (string,int) Hashtbl.t = Hashtbl.create 7 + let additional_debug_sections: StringSet.t ref = ref StringSet.empty + + let print_epilogue oc = if !Clflags.option_g then begin @@ -244,12 +261,35 @@ module Diab_System : SYSTEM = 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" + 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 print_file_loc oc (file,col) = fprintf oc " .4byte %a\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 + () + + end module Target (System : SYSTEM):TARGET = @@ -296,11 +336,6 @@ module Target (System : SYSTEM):TARGET = | FR r -> fprintf oc "f%s" (float_reg_name r) | _ -> assert false - let section oc sec = - let name = name_of_section sec in - assert (name <> "COMM"); - fprintf oc " %s\n" name - let print_location oc loc = if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc) @@ -426,8 +461,8 @@ module Target (System : SYSTEM):TARGET = fprintf oc " cmpw %a, %a, %a\n" creg 0 ireg r1 ireg r2 | Pcmpwi(r1, c) -> fprintf oc " cmpwi %a, %a, %a\n" creg 0 ireg r1 constant c - | Pcntlz(r1, r2) -> - fprintf oc " cntlz %a, %a\n" ireg r1 ireg r2 + | Pcntlzw(r1, r2) -> + fprintf oc " cntlzw %a, %a\n" ireg r1 ireg r2 | Pcreqv(c1, c2, c3) -> fprintf oc " creqv %a, %a, %a\n" crbit c1 crbit c2 crbit c3 | Pcror(c1, c2, c3) -> @@ -806,7 +841,11 @@ module Target (System : SYSTEM):TARGET = module DwarfAbbrevs = DwarfUtil.DefaultAbbrevs - let new_label = new_label + let new_label = new_label + + let section oc sec = + section oc sec; + debug_section oc sec end |