From 295058286407ec6c4182f2b12b27608fc7d28f95 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 10 May 2019 23:53:02 +0200 Subject: use shift 1-4 in backend --- mppa_k1c/Asm.v | 16 ++++++------- mppa_k1c/Asmvliw.v | 61 ++++++++++++++--------------------------------- mppa_k1c/ExtValues.v | 14 +++++++++++ mppa_k1c/Op.v | 14 ----------- mppa_k1c/TargetPrinter.ml | 54 +++++++++++++++++------------------------ 5 files changed, 62 insertions(+), 97 deletions(-) diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 6a4095da..04f6969b 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -182,9 +182,9 @@ Inductive instruction : Type := | Pfcompl (ft: ftest) (rd rs1 rs2: ireg) (**r comparison float64 *) | Paddw (rd rs1 rs2: ireg) (**r add word *) - | Paddxw (shift : Z) (rd rs1 rs2: ireg) (**r add word *) + | Paddxw (shift : shift1_4) (rd rs1 rs2: ireg) (**r add word *) | Psubw (rd rs1 rs2: ireg) (**r sub word *) - | Psubxw (shift : Z) (rd rs1 rs2: ireg) (**r add word *) + | Psubxw (shift : shift1_4) (rd rs1 rs2: ireg) (**r add word *) | Pmulw (rd rs1 rs2: ireg) (**r mul word *) | Pandw (rd rs1 rs2: ireg) (**r and word *) | Pnandw (rd rs1 rs2: ireg) (**r nand word *) @@ -202,9 +202,9 @@ Inductive instruction : Type := | Pmsubw (rd rs1 rs2: ireg) (**r multiply-add words *) | Paddl (rd rs1 rs2: ireg) (**r add long *) - | Paddxl (shift : Z) (rd rs1 rs2: ireg) (**r add long shift *) + | Paddxl (shift : shift1_4) (rd rs1 rs2: ireg) (**r add long shift *) | Psubl (rd rs1 rs2: ireg) (**r sub long *) - | Psubxl (shift : Z) (rd rs1 rs2: ireg) (**r sub long shift *) + | Psubxl (shift : shift1_4) (rd rs1 rs2: ireg) (**r sub long shift *) | Pandl (rd rs1 rs2: ireg) (**r and long *) | Pnandl (rd rs1 rs2: ireg) (**r nand long *) | Porl (rd rs1 rs2: ireg) (**r or long *) @@ -232,9 +232,9 @@ Inductive instruction : Type := | Pcompiw (it: itest) (rd rs: ireg) (imm: int) (**r comparison imm word *) | Paddiw (rd rs: ireg) (imm: int) (**r add imm word *) - | Paddxiw (shift : Z) (rd rs: ireg) (imm: int) (**r add imm word *) + | Paddxiw (shift : shift1_4) (rd rs: ireg) (imm: int) (**r add imm word *) | Psubiw (rd rs: ireg) (imm: int) (**r subtract imm word *) - | Psubxiw (shift : Z) (rd rs: ireg) (imm: int) (**r subtract imm word *) + | Psubxiw (shift : shift1_4) (rd rs: ireg) (imm: int) (**r subtract imm word *) | Pmuliw (rd rs: ireg) (imm: int) (**r mul imm word *) | Pandiw (rd rs: ireg) (imm: int) (**r and imm word *) | Pnandiw (rd rs: ireg) (imm: int) (**r nand imm word *) @@ -258,9 +258,9 @@ Inductive instruction : Type := (** Arith RRI64 *) | Pcompil (it: itest) (rd rs: ireg) (imm: int64) (**r comparison imm long *) | Paddil (rd rs: ireg) (imm: int64) (**r add immediate long *) - | Paddxil (shift : Z) (rd rs: ireg) (imm: int64) (**r add immediate long *) + | Paddxil (shift : shift1_4) (rd rs: ireg) (imm: int64) (**r add immediate long *) | Psubil (rd rs: ireg) (imm: int64) (**r subtract imm long *) - | Psubxil (shift : Z) (rd rs: ireg) (imm: int64) (**r subtract imm long *) + | Psubxil (shift : shift1_4) (rd rs: ireg) (imm: int64) (**r subtract imm long *) | Pmulil (rd rs: ireg) (imm: int64) (**r add immediate long *) | Pandil (rd rs: ireg) (imm: int64) (**r and immediate long *) | Pnandil (rd rs: ireg) (imm: int64) (**r and immediate long *) diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index e8ea4318..e332cedc 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -429,9 +429,9 @@ Inductive arith_name_rrr : Type := | Pfcompl (ft: ftest) (**r comparison float64 *) | Paddw (**r add word *) - | Paddxw (shift : Z) (**r add shift *) + | Paddxw (shift : shift1_4) (**r add shift *) | Psubw (**r sub word word *) - | Psubxw (shift : Z) (**r sub shift word *) + | Psubxw (shift : shift1_4) (**r sub shift word *) | Pmulw (**r mul word *) | Pandw (**r and word *) | Pnandw (**r nand word *) @@ -447,9 +447,9 @@ Inductive arith_name_rrr : Type := | Psllw (**r shift left logical word *) | Paddl (**r add long *) - | Paddxl (shift : Z) (**r add shift long *) + | Paddxl (shift : shift1_4) (**r add shift long *) | Psubl (**r sub long *) - | Psubxl (shift : Z) (**r sub shift long *) + | Psubxl (shift : shift1_4) (**r sub shift long *) | Pandl (**r and long *) | Pnandl (**r nand long *) | Porl (**r or long *) @@ -476,9 +476,9 @@ Inductive arith_name_rri32 : Type := | Pcompiw (it: itest) (**r comparison imm word *) | Paddiw (**r add imm word *) - | Paddxiw (shift : Z) + | Paddxiw (shift : shift1_4) | Psubiw (**r add imm word *) - | Psubxiw (shift : Z) + | Psubxiw (shift : shift1_4) | Pmuliw (**r add imm word *) | Pandiw (**r and imm word *) | Pnandiw (**r nand imm word *) @@ -502,9 +502,9 @@ Inductive arith_name_rri32 : Type := Inductive arith_name_rri64 : Type := | Pcompil (it: itest) (**r comparison imm long *) | Paddil (**r add immediate long *) - | Paddxil (shift : Z) + | Paddxil (shift : shift1_4) | Psubil - | Psubxil (shift : Z) + | Psubxil (shift : shift1_4) | Pmulil (**r mul immediate long *) | Pandil (**r and immediate long *) | Pnandil (**r nand immediate long *) @@ -1068,25 +1068,12 @@ Definition arith_eval_rrr n v1 v2 := | Pfmuld => Val.mulf v1 v2 | Pfmulw => Val.mulfs v1 v2 - | Paddxw shift => - if Z.leb shift 4 && Z.leb 1 shift - then Val.add v1 (Val.shl v2 (Vint (Int.repr shift))) - else Vundef - - | Paddxl shift => - if Z.leb shift 4 && Z.leb 1 shift - then Val.addl v1 (Val.shll v2 (Vint (Int.repr shift))) - else Vundef - - | Psubxw shift => - if Z.leb shift 4 && Z.leb 1 shift - then Val.sub v1 (Val.shl v2 (Vint (Int.repr shift))) - else Vundef - - | Psubxl shift => - if Z.leb shift 4 && Z.leb 1 shift - then Val.subl v1 (Val.shll v2 (Vint (Int.repr shift))) - else Vundef + | Paddxw shift => Val.add v1 (Val.shl v2 (Vint (int_of_shift1_4 shift))) + | Paddxl shift => Val.addl v1 (Val.shll v2 (Vint (int_of_shift1_4 shift))) + + | Psubxw shift => Val.sub v1 (Val.shl v2 (Vint (int_of_shift1_4 shift))) + + | Psubxl shift => Val.subl v1 (Val.shll v2 (Vint (int_of_shift1_4 shift))) end. Definition arith_eval_rri32 n v i := @@ -1112,14 +1099,8 @@ Definition arith_eval_rri32 n v i := | Psrxil => ExtValues.val_shrxl v (Vint i) | Psrlil => Val.shrlu v (Vint i) | Psrail => Val.shrl v (Vint i) - | Paddxiw shift => - if Z.leb shift 4 && Z.leb 1 shift - then Val.add (Vint i) (Val.shl v (Vint (Int.repr shift))) - else Vundef - | Psubxiw shift => - if Z.leb shift 4 && Z.leb 1 shift - then Val.sub (Vint i) (Val.shl v (Vint (Int.repr shift))) - else Vundef + | Paddxiw shift => Val.add (Vint i) (Val.shl v (Vint (int_of_shift1_4 shift))) + | Psubxiw shift => Val.sub (Vint i) (Val.shl v (Vint (int_of_shift1_4 shift))) end. Definition arith_eval_rri64 n v i := @@ -1136,14 +1117,8 @@ Definition arith_eval_rri64 n v i := | Pnxoril => Val.notl (Val.xorl v (Vlong i)) | Pandnil => Val.andl (Val.notl v) (Vlong i) | Pornil => Val.orl (Val.notl v) (Vlong i) - | Paddxil shift => - if Z.leb shift 4 && Z.leb 1 shift - then Val.addl (Vlong i) (Val.shll v (Vint (Int.repr shift))) - else Vundef - | Psubxil shift => - if Z.leb shift 4 && Z.leb 1 shift - then Val.subl (Vlong i) (Val.shll v (Vint (Int.repr shift))) - else Vundef + | Paddxil shift => Val.addl (Vlong i) (Val.shll v (Vint (int_of_shift1_4 shift))) + | Psubxil shift => Val.subl (Vlong i) (Val.shll v (Vint (int_of_shift1_4 shift))) end. Definition arith_eval_arrr n v1 v2 v3 := diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v index 5d16b79c..1aa17458 100644 --- a/mppa_k1c/ExtValues.v +++ b/mppa_k1c/ExtValues.v @@ -2,6 +2,20 @@ Require Import Coqlib. Require Import Integers. Require Import Values. +Inductive shift1_4 : Type := +| SHIFT1 | SHIFT2 | SHIFT3 | SHIFT4. + +Definition z_of_shift1_4 (x : shift1_4) := + match x with + | SHIFT1 => 1 + | SHIFT2 => 2 + | SHIFT3 => 3 + | SHIFT4 => 4 + end. + +Definition int_of_shift1_4 (x : shift1_4) := + Int.repr (z_of_shift1_4 x). + Definition is_bitfield stop start := (Z.leb start stop) && (Z.geb start Z.zero) diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index b93a9fc3..4abd104e 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -66,20 +66,6 @@ Definition arg_type_of_condition0 (cond: condition0) := (** Arithmetic and logical operations. In the descriptions, [rd] is the result of the operation and [r1], [r2], etc, are the arguments. *) -Inductive shift1_4 : Type := -| SHIFT1 | SHIFT2 | SHIFT3 | SHIFT4. - -Definition z_of_shift1_4 (x : shift1_4) := - match x with - | SHIFT1 => 1 - | SHIFT2 => 2 - | SHIFT3 => 3 - | SHIFT4 => 4 - end. - -Definition int_of_shift1_4 (x : shift1_4) := - Int.repr (z_of_shift1_4 x). - Inductive operation : Type := | Omove (**r [rd = r1] *) | Ointconst (n: int) (**r [rd] is set to the given integer constant *) diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 83d12da7..6a21e63d 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -130,6 +130,12 @@ module Target (*: TARGET*) = | RA -> "$ra" | _ -> assert false + let scale_of_shift1_4 = let open ExtValues in function + | SHIFT1 -> 2 + | SHIFT2 -> 4 + | SHIFT3 -> 8 + | SHIFT4 -> 16;; + (* Names of sections *) let name_of_section = function @@ -513,17 +519,13 @@ module Target (*: TARGET*) = | Paddw (rd, rs1, rs2) -> fprintf oc " addw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 - | Paddxw (zshift, rd, rs1, rs2) -> - let shift = camlint_of_coqint zshift in - assert(shift >= 1l && shift <= 4l); - fprintf oc " addx%dw %a = %a, %a\n" (1 lsl (Int32.to_int shift)) + | Paddxw (s14, rd, rs1, rs2) -> + fprintf oc " addx%dw %a = %a, %a\n" (scale_of_shift1_4 s14) ireg rd ireg rs1 ireg rs2 | Psubw (rd, rs1, rs2) -> fprintf oc " sbfw %a = %a, %a\n" ireg rd ireg rs2 ireg rs1 - | Psubxw (zshift, rd, rs1, rs2) -> - let shift = camlint_of_coqint zshift in - assert(shift >= 1l && shift <= 4l); - fprintf oc " subx%dw %a = %a, %a\n" (1 lsl (Int32.to_int shift)) + | Psubxw (s14, rd, rs1, rs2) -> + fprintf oc " subx%dw %a = %a, %a\n" (scale_of_shift1_4 s14) ireg rd ireg rs1 ireg rs2 | Pmulw (rd, rs1, rs2) -> fprintf oc " mulw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 @@ -558,17 +560,13 @@ module Target (*: TARGET*) = | Paddl (rd, rs1, rs2) -> fprintf oc " addd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 - | Paddxl (zshift, rd, rs1, rs2) -> - let shift = camlint_of_coqint zshift in - assert(shift >= 1l && shift <= 4l); - fprintf oc " addx%dd %a = %a, %a\n" (1 lsl (Int32.to_int shift)) + | Paddxl (s14, rd, rs1, rs2) -> + fprintf oc " addx%dd %a = %a, %a\n" (scale_of_shift1_4 s14) ireg rd ireg rs1 ireg rs2 | Psubl (rd, rs1, rs2) -> fprintf oc " sbfd %a = %a, %a\n" ireg rd ireg rs2 ireg rs1 - | Psubxl (zshift, rd, rs1, rs2) -> - let shift = camlint_of_coqint zshift in - assert(shift >= 1l && shift <= 4l); - fprintf oc " sbfx%dd %a = %a, %a\n" (1 lsl (Int32.to_int shift)) + | Psubxl (s14, rd, rs1, rs2) -> + fprintf oc " sbfx%dd %a = %a, %a\n" (scale_of_shift1_4 s14) ireg rd ireg rs1 ireg rs2 | Pandl (rd, rs1, rs2) -> fprintf oc " andd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 @@ -619,17 +617,13 @@ module Target (*: TARGET*) = fprintf oc " compw.%a %a = %a, %a\n" icond it ireg rd ireg rs coqint imm | Paddiw (rd, rs, imm) -> fprintf oc " addw %a = %a, %a\n" ireg rd ireg rs coqint imm - | Paddxiw (zshift, rd, rs, imm) -> - let shift = camlint_of_coqint zshift in - assert(shift >= 1l && shift <= 4l); - fprintf oc " addx%dw %a = %a, %a\n" (1 lsl (Int32.to_int shift)) + | Paddxiw (s14, rd, rs, imm) -> + fprintf oc " addx%dw %a = %a, %a\n" (scale_of_shift1_4 s14) ireg rd ireg rs coqint imm | Psubiw (rd, rs, imm) -> fprintf oc " sbfw %a = %a, %a\n" ireg rd ireg rs coqint imm - | Psubxiw (zshift, rd, rs, imm) -> - let shift = camlint_of_coqint zshift in - assert(shift >= 1l && shift <= 4l); - fprintf oc " sbfx%dw %a = %a, %a\n" (1 lsl (Int32.to_int shift)) + | Psubxiw (s14, rd, rs, imm) -> + fprintf oc " sbfx%dw %a = %a, %a\n" (scale_of_shift1_4 s14) ireg rd ireg rs coqint imm | Pmuliw (rd, rs, imm) -> fprintf oc " mulw %a = %a, %a\n" ireg rd ireg rs coqint imm @@ -676,17 +670,13 @@ module Target (*: TARGET*) = fprintf oc " compd.%a %a = %a, %a\n" icond it ireg rd ireg rs coqint64 imm | Paddil (rd, rs, imm) -> assert Archi.ptr64; fprintf oc " addd %a = %a, %a\n" ireg rd ireg rs coqint64 imm - | Paddxil (zshift, rd, rs, imm) -> - let shift = camlint_of_coqint zshift in - assert(shift >= 1l && shift <= 4l); - fprintf oc " addx%dd %a = %a, %a\n" (1 lsl (Int32.to_int shift)) + | Paddxil (s14, rd, rs, imm) -> + fprintf oc " addx%dd %a = %a, %a\n" (scale_of_shift1_4 s14) ireg rd ireg rs coqint imm | Psubil (rd, rs, imm) -> fprintf oc " sbfd %a = %a, %a\n" ireg rd ireg rs coqint64 imm - | Psubxil (zshift, rd, rs, imm) -> - let shift = camlint_of_coqint zshift in - assert(shift >= 1l && shift <= 4l); - fprintf oc " sbfx%dd %a = %a, %a\n" (1 lsl (Int32.to_int shift)) + | Psubxil (s14, rd, rs, imm) -> + fprintf oc " sbfx%dd %a = %a, %a\n" (scale_of_shift1_4 s14) ireg rd ireg rs coqint64 imm | Pmulil (rd, rs, imm) -> assert Archi.ptr64; fprintf oc " muld %a = %a, %a\n" ireg rd ireg rs coqint64 imm -- cgit