From 4f187fdafdac0cf4a8b83964c89d79741dbd813e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 21 Aug 2015 17:53:44 +0200 Subject: Adapt the PowerPC port to the new builtin representation. __builtin_get_spr() and __builtin_set_spr() work, but horrible error message if the SPR argument is not a constant. powerpc/AsmToJSON.ml needs updating. --- powerpc/TargetPrinter.ml | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) (limited to 'powerpc/TargetPrinter.ml') diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 8610f750..5431d88d 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -599,6 +599,10 @@ module Target (System : SYSTEM):TARGET = fprintf oc " mtctr %a\n" ireg r1 | Pmtlr(r1) -> fprintf oc " mtlr %a\n" ireg r1 + | Pmfspr(rd, spr) -> + fprintf oc " mfspr %a, %ld\n" ireg rd (camlint_of_coqint spr) + | Pmtspr(spr, rs) -> + fprintf oc " mtspr %ld, %a\n" (camlint_of_coqint spr) ireg rs | Pmulli(r1, r2, c) -> fprintf oc " mulli %a, %a, %a\n" ireg r1 ireg r2 constant c | Pmullw(r1, r2, r3) -> @@ -693,6 +697,8 @@ module Target (System : SYSTEM):TARGET = fprintf oc "%a:\n" label (transl_label lbl) | Pbuiltin(ef, args, res) -> begin match ef with + | EF_annot(txt, targs) -> + print_annot_stmt oc (extern_atom txt) targs args | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; print_inline_asm preg oc (extern_atom txt) sg args res; @@ -700,13 +706,6 @@ module Target (System : SYSTEM):TARGET = | _ -> assert false end - | Pannot(ef, args) -> - begin match ef with - | EF_annot(txt, targs) -> - print_annot_stmt oc (extern_atom txt) targs args - | _ -> - assert false - end | Pcfi_adjust n -> cfi_adjust oc (camlint_of_coqint n) | Pcfi_rel_offset n -> @@ -731,8 +730,8 @@ module Target (System : SYSTEM):TARGET = | Plfi(r1, c) -> 2 | Plfis(r1, c) -> 2 | Plabel lbl -> 0 - | Pbuiltin(ef, args, res) -> 0 - | Pannot(ef, args) -> 0 + | Pbuiltin((EF_annot _ | EF_debug _), args, res) -> 0 + | Pbuiltin(ef, args, res) -> 3 | Pcfi_adjust _ | Pcfi_rel_offset _ -> 0 | _ -> 1 -- cgit From 33dfbe7601ad16fcea5377563fa7ceb4053cb85a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 22 Aug 2015 09:46:37 +0200 Subject: Renaming {BA,BR}_longofwords -> {BA,BR}_splitlong. Use EF_debug instead of EF_annot for line number annotations. Introduce PrintAsmaux.print_debug_info (very incomplete). powerpc/Asmexpand: revise expand_memcpy_small. --- powerpc/TargetPrinter.ml | 17 +++++------------ 1 file changed, 5 insertions(+), 12 deletions(-) (limited to 'powerpc/TargetPrinter.ml') diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 5431d88d..ced26783 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -358,17 +358,6 @@ module Target (System : SYSTEM):TARGET = assert (!count = 2 || (!count = 0 && !last)); (!mb, !me-1) - (* Handling of annotations *) - - let print_annot_stmt oc txt targs args = - if Str.string_match re_file_line txt 0 then begin - print_file_line oc (Str.matched_group 1 txt) - (int_of_string (Str.matched_group 2 txt)) - end else begin - fprintf oc "%s annotation: " comment; - print_annot_stmt preg_annot "R1" oc txt targs args - end - (* Determine if the displacement of a conditional branch fits the short form *) let short_cond_branch tbl pc lbl_dest = @@ -698,7 +687,11 @@ module Target (System : SYSTEM):TARGET = | Pbuiltin(ef, args, res) -> begin match ef with | EF_annot(txt, targs) -> - print_annot_stmt oc (extern_atom txt) targs args + fprintf oc "%s annotation: " comment; + print_annot_text preg_annot "r1" oc (extern_atom txt) args + | EF_debug(kind, txt, targs) -> + print_debug_info comment print_file_line preg_annot "r1" oc + (P.to_int kind) (extern_atom txt) args | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; print_inline_asm preg oc (extern_atom txt) sg args res; -- cgit From 75d50c12ee220fecf955b1626c78b78636cbca92 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 1 Sep 2015 16:44:29 +0200 Subject: Added the gcc builtin prefetch. This commit implements the gcc __builtin_prefetch in a form with all arguments for the powerpc architecture. The resulting instructions are the dcbt and dcbtst instructions in Server Category. --- powerpc/TargetPrinter.ml | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'powerpc/TargetPrinter.ml') diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index ced26783..b0f296ef 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -462,6 +462,10 @@ module Target (System : SYSTEM):TARGET = fprintf oc " dcbf %a, %a\n" ireg r1 ireg r2 | Pdcbi (r1,r2) -> fprintf oc " dcbi %a, %a\n" ireg r1 ireg r2 + | Pdcbt (c,r1) -> + fprintf oc " dcbt %a, %a, %s\n" ireg GPR0 ireg r1 (Z.to_string c) + | Pdcbtst (c,r1) -> + fprintf oc " dcbtst %a, %a, %s\n" ireg GPR0 ireg r1 (Z.to_string c) | Pdivw(r1, r2, r3) -> fprintf oc " divw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pdivwu(r1, r2, r3) -> -- cgit From db8e35c6abf58c82853b94f416aa76b33efc1f65 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 2 Sep 2015 13:50:24 +0200 Subject: Added builtin for dcbtls THis commit adds a builtin function for the dcbtls instruction. Additionaly it changes the printing of the dcbt and dcbtst instruction to embedded mode and adds support for different address variants. --- powerpc/TargetPrinter.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'powerpc/TargetPrinter.ml') diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index b0f296ef..b5fa50dc 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -463,9 +463,11 @@ module Target (System : SYSTEM):TARGET = | Pdcbi (r1,r2) -> fprintf oc " dcbi %a, %a\n" ireg r1 ireg r2 | Pdcbt (c,r1) -> - fprintf oc " dcbt %a, %a, %s\n" ireg GPR0 ireg r1 (Z.to_string c) + fprintf oc " dcbt %s, %a, %a\n" (Z.to_string c) ireg GPR0 ireg r1 | Pdcbtst (c,r1) -> - fprintf oc " dcbtst %a, %a, %s\n" ireg GPR0 ireg r1 (Z.to_string c) + fprintf oc " dcbtst %s, %a, %a\n" (Z.to_string c) ireg GPR0 ireg r1 + | Pdcbtls (c,r1) -> + fprintf oc " dcbtls %s, %a, %a\n" (Z.to_string c) ireg GPR0 ireg r1 | Pdivw(r1, r2, r3) -> fprintf oc " divw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pdivwu(r1, r2, r3) -> -- cgit From 30ebbcd0731f680d1d283afb99318fb9d6e9cead Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 2 Sep 2015 15:56:42 +0200 Subject: Allow only CT values of 0 and 2 in dcbtls instruction. The dcbtls instruction allows only the values 0 and 2 according to the PPC Isa. --- powerpc/TargetPrinter.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'powerpc/TargetPrinter.ml') diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index b5fa50dc..764ad8a3 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -463,11 +463,11 @@ module Target (System : SYSTEM):TARGET = | Pdcbi (r1,r2) -> fprintf oc " dcbi %a, %a\n" ireg r1 ireg r2 | Pdcbt (c,r1) -> - fprintf oc " dcbt %s, %a, %a\n" (Z.to_string c) ireg GPR0 ireg r1 + fprintf oc " dcbt %ld, %a, %a\n" (camlint_of_coqint c) ireg GPR0 ireg r1 | Pdcbtst (c,r1) -> - fprintf oc " dcbtst %s, %a, %a\n" (Z.to_string c) ireg GPR0 ireg r1 + fprintf oc " dcbtst %ld, %a, %a\n" (camlint_of_coqint c) ireg GPR0 ireg r1 | Pdcbtls (c,r1) -> - fprintf oc " dcbtls %s, %a, %a\n" (Z.to_string c) ireg GPR0 ireg r1 + fprintf oc " dcbtls %ld, %a, %a\n" (camlint_of_coqint c) ireg GPR0 ireg r1 | Pdivw(r1, r2, r3) -> fprintf oc " divw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pdivwu(r1, r2, r3) -> -- cgit From cfee340dc514e2cfbc5df910f7aa687e78a54d41 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 2 Sep 2015 17:17:00 +0200 Subject: Added builtin for the icbtls instruction. This commit adds a builtin for the icbtls instruction. --- powerpc/TargetPrinter.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'powerpc/TargetPrinter.ml') diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 764ad8a3..6a583cca 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -536,6 +536,8 @@ module Target (System : SYSTEM):TARGET = fprintf oc " fsel %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 | Picbi (r1,r2) -> fprintf oc " icbi %a,%a\n" ireg r1 ireg r2 + | Picbtls (n,r1) -> + fprintf oc " icbtls %ld, %a, %a\n" (camlint_of_coqint n) ireg GPR0 ireg r1 | Pisync -> fprintf oc " isync\n" | Plwsync -> -- cgit From 38959ad2b2d35a7d1b3479ef4298a5d754350cd8 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 3 Sep 2015 11:08:25 +0200 Subject: New builtin for dcbz instruction. This commit adds a builtin for the dcbz instructions. Additionally the dcbt,dcbtst,dcbtls and icbtls instruction are changed to their actually form all taking one additional register in Asm.v. --- powerpc/TargetPrinter.ml | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) (limited to 'powerpc/TargetPrinter.ml') diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 6a583cca..ffd01b69 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -462,12 +462,14 @@ module Target (System : SYSTEM):TARGET = fprintf oc " dcbf %a, %a\n" ireg r1 ireg r2 | Pdcbi (r1,r2) -> fprintf oc " dcbi %a, %a\n" ireg r1 ireg r2 - | Pdcbt (c,r1) -> - fprintf oc " dcbt %ld, %a, %a\n" (camlint_of_coqint c) ireg GPR0 ireg r1 - | Pdcbtst (c,r1) -> - fprintf oc " dcbtst %ld, %a, %a\n" (camlint_of_coqint c) ireg GPR0 ireg r1 - | Pdcbtls (c,r1) -> - fprintf oc " dcbtls %ld, %a, %a\n" (camlint_of_coqint c) ireg GPR0 ireg r1 + | Pdcbt (c,r1,r2) -> + fprintf oc " dcbt %ld, %a, %a\n" (camlint_of_coqint c) ireg r1 ireg r2 + | Pdcbtst (c,r1,r2) -> + fprintf oc " dcbtst %ld, %a, %a\n" (camlint_of_coqint c) ireg r1 ireg r2 + | Pdcbtls (c,r1,r2) -> + fprintf oc " dcbtls %ld, %a, %a\n" (camlint_of_coqint c) ireg r1 ireg r2 + | Pdcbz (r1,r2) -> + fprintf oc " dcbz %a, %a\n" ireg r1 ireg r2 | Pdivw(r1, r2, r3) -> fprintf oc " divw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pdivwu(r1, r2, r3) -> @@ -536,8 +538,8 @@ module Target (System : SYSTEM):TARGET = fprintf oc " fsel %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 | Picbi (r1,r2) -> fprintf oc " icbi %a,%a\n" ireg r1 ireg r2 - | Picbtls (n,r1) -> - fprintf oc " icbtls %ld, %a, %a\n" (camlint_of_coqint n) ireg GPR0 ireg r1 + | Picbtls (n,r1,r2) -> + fprintf oc " icbtls %ld, %a, %a\n" (camlint_of_coqint n) ireg r1 ireg r2 | Pisync -> fprintf oc " isync\n" | Plwsync -> -- cgit From c74211d87eb53cb310703dec2c504b26d7f24bdf Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 3 Sep 2015 13:22:28 +0200 Subject: Added builtin for mbar instruction. This commit adds a builtin function for the mbar instruction. --- powerpc/TargetPrinter.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'powerpc/TargetPrinter.ml') diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index ffd01b69..af5dafed 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -586,6 +586,8 @@ module Target (System : SYSTEM):TARGET = fprintf oc " lwzu %a, %a(%a)\n" ireg r1 constant c ireg r2 | Plwzx(r1, r2, r3) | Plwzx_a(r1, r2, r3) -> fprintf oc " lwzx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pmbar mo -> + fprintf oc " mbar %ld\n" (camlint_of_coqint mo) | Pmfcr(r1) -> fprintf oc " mfcr %a\n" ireg r1 | Pmfcrbit(r1, bit) -> -- cgit