diff options
| -rw-r--r-- | powerpc/Asm.v | 4 | ||||
| -rw-r--r-- | powerpc/AsmToJSON.ml | 1 | ||||
| -rw-r--r-- | powerpc/TargetPrinter.ml | 5 |
3 files changed, 8 insertions, 2 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 228977c2..a9b60fbd 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -259,6 +259,7 @@ Inductive instruction : Type := | Pori: ireg -> ireg -> constant -> instruction (**r or with immediate *) | Poris: ireg -> ireg -> constant -> instruction (**r or with immediate high *) | Prldicl: ireg -> ireg -> int -> int -> instruction (**r rotate and mask left (PPC64) *) + | Prldicr: ireg -> ireg -> int -> int -> instruction (**r rotate and mask right (PPC64) *) | Prlwinm: ireg -> ireg -> int -> int -> instruction (**r rotate and mask *) | Prlwimi: ireg -> ireg -> int -> int -> instruction (**r rotate and insert *) | Pslw: ireg -> ireg -> ireg -> instruction (**r shift left *) @@ -267,7 +268,7 @@ Inductive instruction : Type := | Psrw: ireg -> ireg -> ireg -> instruction (**r shift right unsigned *) | Pstb: ireg -> constant -> ireg -> instruction (**r store 8-bit int *) | Pstbx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) - | Pstdu: ireg -> constant -> ireg -> instruction (**r store 64-bit integer with update (PPC64) *) + | Pstdu: ireg -> constant -> ireg -> instruction (**r store 64-bit integer with update (PPC64) *) | Pstfd: freg -> constant -> ireg -> instruction (**r store 64-bit float *) | Pstfdu: freg -> constant -> ireg -> instruction (**r store 64-bit float with update *) | Pstfdx: freg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) @@ -925,6 +926,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pmfspr _ _ | Pmtspr _ _ | Prldicl _ _ _ _ + | Prldicr _ _ _ _ | Pstdu _ _ _ | Pstwbrx _ _ _ | Pstwcx_ _ _ _ diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 02d2dc84..42ad4f97 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -287,6 +287,7 @@ let p_instruction oc ic = | Pori (ir1,ir2,c) -> instruction "Pori" [Ireg ir1; Ireg ir2; Constant c] | Poris (ir1,ir2,c) -> instruction "Poris" [Ireg ir1; Ireg ir2; Constant c] | Prldicl (ir1,ir2,ic1,ic2) -> instruction "Prldicl" [Ireg ir1; Ireg ir2; Constant (Cint ic1); Constant (Cint ic2)] + | Prldicr (ir1,ir2,ic1,ic2) -> instruction "Prldicr" [Ireg ir1; Ireg ir2; Constant (Cint ic1); Constant (Cint ic2)] | Prlwinm (ir1,ir2,ic1,ic2) -> instruction "Prlwinm" [Ireg ir1; Ireg ir2; Constant (Cint ic1); Constant (Cint ic2)] | Prlwimi (ir1,ir2,ic1,ic2) ->instruction "Prlwimi" [Ireg ir1; Ireg ir2; Constant (Cint ic1); Constant (Cint ic2)] | Pslw (ir1,ir2,ir3) -> instruction "Pslw" [Ireg ir1; Ireg ir2; Ireg ir3] diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 73cb12f5..24511887 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -647,6 +647,9 @@ module Target (System : SYSTEM):TARGET = | Prldicl(r1, r2, c1, c2) -> fprintf oc " rldicl %a, %a, %ld, %ld\n" ireg r1 ireg r2 (camlint_of_coqint c1) (camlint_of_coqint c2) + | Prldicr(r1, r2, c1, c2) -> + fprintf oc " rldicr %a, %a, %ld, %ld\n" + ireg r1 ireg r2 (camlint_of_coqint c1) (camlint_of_coqint c2) | Prlwinm(r1, r2, c1, c2) -> let (mb, me) = rolm_mask (camlint_of_coqint c2) in fprintf oc " rlwinm %a, %a, %ld, %d, %d %s 0x%lx\n" @@ -789,7 +792,7 @@ module Target (System : SYSTEM):TARGET = let nlo = Int64.to_int32 n and nhi = Int64.to_int32(Int64.shift_right_logical n 32) in fprintf oc "%a: .long 0x%lx, 0x%lx\n" label lbl nhi nlo - + let print_literal32 oc (lbl, n) = fprintf oc "%a: .long 0x%lx\n" label lbl n |