diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-30 00:28:22 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-30 00:28:22 +0200 |
commit | 8528ade84279dc8fa399cad8f0b8467ed454cbf7 (patch) | |
tree | f394fde20691e1c093ac56578f3ed88df8fe9c83 | |
parent | 01ebfe059727d6d91cee184f3856fa84133cd100 (diff) | |
parent | cea008aa07715cf7abbc88f7573050f5a05f58d7 (diff) | |
download | compcert-kvx-8528ade84279dc8fa399cad8f0b8467ed454cbf7.tar.gz compcert-kvx-8528ade84279dc8fa399cad8f0b8467ed454cbf7.zip |
Merge remote-tracking branch 'origin/mppa-work' into mppa-cos
-rw-r--r-- | driver/Clflags.ml | 3 | ||||
-rw-r--r-- | driver/Compopts.v | 9 | ||||
-rw-r--r-- | driver/Driver.ml | 3 | ||||
-rw-r--r-- | extraction/extraction.v | 10 | ||||
-rw-r--r-- | mppa_k1c/Asm.v | 24 | ||||
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 14 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgen.v | 42 | ||||
-rw-r--r-- | mppa_k1c/Asmvliw.v | 28 | ||||
-rw-r--r-- | mppa_k1c/ConstpropOp.vp | 2 | ||||
-rw-r--r-- | mppa_k1c/ExtValues.v | 94 | ||||
-rw-r--r-- | mppa_k1c/Machregs.v | 4 | ||||
-rw-r--r-- | mppa_k1c/NeedOp.v | 45 | ||||
-rw-r--r-- | mppa_k1c/Op.v | 134 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 43 | ||||
-rw-r--r-- | mppa_k1c/SelectLong.vp | 32 | ||||
-rw-r--r-- | mppa_k1c/SelectLongproof.v | 150 | ||||
-rw-r--r-- | mppa_k1c/SelectOp.vp | 42 | ||||
-rw-r--r-- | mppa_k1c/SelectOpproof.v | 153 | ||||
-rw-r--r-- | mppa_k1c/TargetPrinter.ml | 52 | ||||
-rw-r--r-- | mppa_k1c/ValueAOp.v | 56 | ||||
-rw-r--r-- | test/monniaux/bitsliced-aes/bs.c | 4 |
21 files changed, 891 insertions, 53 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml index b1afab6f..651d644e 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -70,4 +70,5 @@ let use_standard_headers = ref Configuration.has_standard_headers let option_fglobaladdrtmp = ref false let option_fglobaladdroffset = ref false let option_fxsaddr = ref true -let option_coalesce_mem = ref true +let option_faddx = ref false +let option_fcoalesce_mem = ref true diff --git a/driver/Compopts.v b/driver/Compopts.v index f7de596c..9c6448b7 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -43,17 +43,20 @@ Parameter optim_redundancy: unit -> bool. Parameter optim_postpass: unit -> bool. (** FIXME TEMPORARY Flag -fglobaladdrtmp. Use a temporary register for loading the address of global variables (default false) *) -Parameter optim_fglobaladdrtmp: unit -> bool. +Parameter optim_globaladdrtmp: unit -> bool. (** FIXME TEMPORARY Flag -fglobaladdroffset. Fold offsets into global addresses (default false) *) -Parameter optim_fglobaladdroffset: unit -> bool. +Parameter optim_globaladdroffset: unit -> bool. (** FIXME TEMPORARY Flag -fxsaddr. Use .xs addressing mode (default true) *) -Parameter optim_fxsaddr: unit -> bool. +Parameter optim_xsaddr: unit -> bool. (** FIXME TEMPORARY Flag -fcoaelesce-mem. Fuse (default true) *) Parameter optim_coalesce_mem: unit -> bool. +(** FIXME TEMPORARY Flag -faddx. Fuse (default false) *) +Parameter optim_addx: unit -> bool. + (** Flag -fthumb. For the ARM back-end. *) Parameter thumb: unit -> bool. diff --git a/driver/Driver.ml b/driver/Driver.ml index cfafcaa3..74e7ae77 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -375,7 +375,8 @@ let cmdline_actions = @ f_opt "globaladdrtmp" option_fglobaladdrtmp @ f_opt "globaladdroffset" option_fglobaladdroffset @ f_opt "xsaddr" option_fxsaddr - @ f_opt "coalesce-mem" option_coalesce_mem + @ f_opt "addx" option_faddx + @ f_opt "coalesce-mem" option_fcoalesce_mem (* Code generation options *) @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) diff --git a/extraction/extraction.v b/extraction/extraction.v index 979e1d49..e2ffd65d 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -117,14 +117,16 @@ Extract Constant Compopts.thumb => "fun _ -> !Clflags.option_mthumb". Extract Constant Compopts.debug => "fun _ -> !Clflags.option_g". -Extract Constant Compopts.optim_fglobaladdrtmp => +Extract Constant Compopts.optim_globaladdrtmp => "fun _ -> !Clflags.option_fglobaladdrtmp". -Extract Constant Compopts.optim_fglobaladdroffset => +Extract Constant Compopts.optim_globaladdroffset => "fun _ -> !Clflags.option_fglobaladdroffset". -Extract Constant Compopts.optim_fxsaddr => +Extract Constant Compopts.optim_xsaddr => "fun _ -> !Clflags.option_fxsaddr". +Extract Constant Compopts.optim_addx => + "fun _ -> !Clflags.option_faddx". Extract Constant Compopts.optim_coalesce_mem => - "fun _ -> !Clflags.option_coalesce_mem". + "fun _ -> !Clflags.option_fcoalesce_mem". (* Compiler *) Extract Constant Compiler.print_Clight => "PrintClight.print_if". diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 1774b102..e5f81fbb 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -182,7 +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 : shift1_4) (rd rs1 rs2: ireg) (**r add word *)
| Psubw (rd rs1 rs2: ireg) (**r sub word *)
+ | Prevsubxw (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 *)
@@ -197,9 +199,12 @@ Inductive instruction : Type := | Psrlw (rd rs1 rs2: ireg) (**r shift right logical word *)
| Psllw (rd rs1 rs2: ireg) (**r shift left logical word *)
| Pmaddw (rd rs1 rs2: ireg) (**r multiply-add words *)
+ | Pmsubw (rd rs1 rs2: ireg) (**r multiply-add words *)
| Paddl (rd rs1 rs2: ireg) (**r add long *)
+ | Paddxl (shift : shift1_4) (rd rs1 rs2: ireg) (**r add long shift *)
| Psubl (rd rs1 rs2: ireg) (**r sub long *)
+ | Prevsubxl (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 *)
@@ -214,6 +219,7 @@ Inductive instruction : Type := | Psral (rd rs1 rs2: ireg) (**r shift right arithmetic long *)
| Psrxl (rd rs1 rs2: ireg) (**r shift right arithmetic long round to 0*)
| Pmaddl (rd rs1 rs2: ireg) (**r multiply-add long *)
+ | Pmsubl (rd rs1 rs2: ireg) (**r multiply-add long *)
| Pfaddd (rd rs1 rs2: ireg) (**r Float addition double *)
| Pfaddw (rd rs1 rs2: ireg) (**r Float addition word *)
@@ -226,6 +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 : shift1_4) (rd rs: ireg) (imm: int) (**r add imm word *)
+ | Prevsubiw (rd rs: ireg) (imm: int) (**r subtract imm word *)
+ | Prevsubxiw (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 *)
@@ -249,6 +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 : shift1_4) (rd rs: ireg) (imm: int64) (**r add immediate long *)
+ | Prevsubil (rd rs: ireg) (imm: int64) (**r subtract imm long *)
+ | Prevsubxil (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 *)
@@ -338,7 +350,9 @@ Definition basic_to_instruction (b: basic) := | PArithRRR (Asmvliw.Pfcompw ft) rd rs1 rs2 => Pfcompw ft rd rs1 rs2
| PArithRRR (Asmvliw.Pfcompl ft) rd rs1 rs2 => Pfcompl ft rd rs1 rs2
| PArithRRR Asmvliw.Paddw rd rs1 rs2 => Paddw rd rs1 rs2
+ | PArithRRR (Asmvliw.Paddxw shift) rd rs1 rs2 => Paddxw shift rd rs1 rs2
| PArithRRR Asmvliw.Psubw rd rs1 rs2 => Psubw rd rs1 rs2
+ | PArithRRR (Asmvliw.Prevsubxw shift) rd rs1 rs2 => Prevsubxw shift rd rs1 rs2
| PArithRRR Asmvliw.Pmulw rd rs1 rs2 => Pmulw rd rs1 rs2
| PArithRRR Asmvliw.Pandw rd rs1 rs2 => Pandw rd rs1 rs2
| PArithRRR Asmvliw.Pnandw rd rs1 rs2 => Pnandw rd rs1 rs2
@@ -354,7 +368,9 @@ Definition basic_to_instruction (b: basic) := | PArithRRR Asmvliw.Psllw rd rs1 rs2 => Psllw rd rs1 rs2
| PArithRRR Asmvliw.Paddl rd rs1 rs2 => Paddl rd rs1 rs2
+ | PArithRRR (Asmvliw.Paddxl shift) rd rs1 rs2 => Paddxl shift rd rs1 rs2
| PArithRRR Asmvliw.Psubl rd rs1 rs2 => Psubl rd rs1 rs2
+ | PArithRRR (Asmvliw.Prevsubxl shift) rd rs1 rs2 => Prevsubxl shift rd rs1 rs2
| PArithRRR Asmvliw.Pandl rd rs1 rs2 => Pandl rd rs1 rs2
| PArithRRR Asmvliw.Pnandl rd rs1 rs2 => Pnandl rd rs1 rs2
| PArithRRR Asmvliw.Porl rd rs1 rs2 => Porl rd rs1 rs2
@@ -379,6 +395,9 @@ Definition basic_to_instruction (b: basic) := (* RRI32 *)
| PArithRRI32 (Asmvliw.Pcompiw it) rd rs imm => Pcompiw it rd rs imm
| PArithRRI32 Asmvliw.Paddiw rd rs imm => Paddiw rd rs imm
+ | PArithRRI32 (Asmvliw.Paddxiw shift) rd rs imm => Paddxiw shift rd rs imm
+ | PArithRRI32 Asmvliw.Prevsubiw rd rs imm => Prevsubiw rd rs imm
+ | PArithRRI32 (Asmvliw.Prevsubxiw shift) rd rs imm => Prevsubxiw shift rd rs imm
| PArithRRI32 Asmvliw.Pmuliw rd rs imm => Pmuliw rd rs imm
| PArithRRI32 Asmvliw.Pandiw rd rs imm => Pandiw rd rs imm
| PArithRRI32 Asmvliw.Pnandiw rd rs imm => Pnandiw rd rs imm
@@ -401,6 +420,9 @@ Definition basic_to_instruction (b: basic) := (* RRI64 *)
| PArithRRI64 (Asmvliw.Pcompil it) rd rs imm => Pcompil it rd rs imm
| PArithRRI64 Asmvliw.Paddil rd rs imm => Paddil rd rs imm
+ | PArithRRI64 (Asmvliw.Paddxil shift) rd rs imm => Paddxil shift rd rs imm
+ | PArithRRI64 Asmvliw.Prevsubil rd rs imm => Prevsubil rd rs imm
+ | PArithRRI64 (Asmvliw.Prevsubxil shift) rd rs imm => Prevsubxil shift rd rs imm
| PArithRRI64 Asmvliw.Pmulil rd rs imm => Pmulil rd rs imm
| PArithRRI64 Asmvliw.Pandil rd rs imm => Pandil rd rs imm
| PArithRRI64 Asmvliw.Pnandil rd rs imm => Pnandil rd rs imm
@@ -414,6 +436,8 @@ Definition basic_to_instruction (b: basic) := (** ARRR *)
| PArithARRR Asmvliw.Pmaddw rd rs1 rs2 => Pmaddw rd rs1 rs2
| PArithARRR Asmvliw.Pmaddl rd rs1 rs2 => Pmaddl rd rs1 rs2
+ | PArithARRR Asmvliw.Pmsubw rd rs1 rs2 => Pmsubw rd rs1 rs2
+ | PArithARRR Asmvliw.Pmsubl rd rs1 rs2 => Pmsubl rd rs1 rs2
| PArithARRR (Asmvliw.Pcmove cond) rd rs1 rs2=> Pcmove cond rd rs1 rs2
| PArithARRR (Asmvliw.Pcmoveu cond) rd rs1 rs2=> Pcmoveu cond rd rs1 rs2
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index eb3900d5..616ec6db 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1405,12 +1405,14 @@ Definition string_of_name_rf64 (n: arith_name_rf64): pstring := Definition string_of_name_rrr (n: arith_name_rrr): pstring := match n with - Pcompw _ => "Pcompw" + | Pcompw _ => "Pcompw" | Pcompl _ => "Pcompl" | Pfcompw _ => "Pfcompw" | Pfcompl _ => "Pfcompl" | Paddw => "Paddw" + | Paddxw _ => "Paddxw" | Psubw => "Psubw" + | Prevsubxw _ => "Prevsubxw" | Pmulw => "Pmulw" | Pandw => "Pandw" | Pnandw => "Pnandw" @@ -1425,7 +1427,9 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring := | Psrxw => "Psrxw" | Psllw => "Psllw" | Paddl => "Paddl" + | Paddxl _ => "Paddxl" | Psubl => "Psubl" + | Prevsubxl _ => "Prevsubxl" | Pandl => "Pandl" | Pnandl => "Pnandl" | Porl => "Porl" @@ -1451,6 +1455,9 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring := match n with Pcompiw _ => "Pcompiw" | Paddiw => "Paddiw" + | Paddxiw _ => "Paddxiw" + | Prevsubiw => "Prevsubiw" + | Prevsubxiw _ => "Prevsubxiw" | Pmuliw => "Pmuliw" | Pandiw => "Pandiw" | Pnandiw => "Pnandiw" @@ -1475,6 +1482,9 @@ Definition string_of_name_rri64 (n: arith_name_rri64): pstring := match n with Pcompil _ => "Pcompil" | Paddil => "Paddil" + | Prevsubil => "Prevsubil" + | Paddxil _ => "Paddxil" + | Prevsubxil _ => "Prevsubxil" | Pmulil => "Pmulil" | Pandil => "Pandil" | Pnandil => "Pnandil" @@ -1490,6 +1500,8 @@ Definition string_of_name_arrr (n: arith_name_arrr): pstring := match n with | Pmaddw => "Pmaddw" | Pmaddl => "Pmaddl" + | Pmsubw => "Pmsubw" + | Pmsubl => "Pmsubl" | Pcmove _ => "Pcmove" | Pcmoveu _ => "Pcmoveu" end. diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index a4364051..941796cd 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -443,12 +443,33 @@ Definition transl_op | Oaddimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (addimm32 rd rs n ::i k) + | Oaddx shift, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Paddxw shift rd rs1 rs2 ::i k) + | Oaddximm shift n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Paddxiw shift rd rs n ::i k) + | Oaddxl shift, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Paddxl shift rd rs1 rs2 ::i k) + | Oaddxlimm shift n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Paddxil shift rd rs n ::i k) | Oneg, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Pnegw rd rs ::i k) | Osub, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Psubw rd rs1 rs2 ::i k) + | Orevsubimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Prevsubiw rd rs n ::i k) + | Orevsubx shift, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Prevsubxw shift rd rs1 rs2 ::i k) + | Orevsubximm shift n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Prevsubxiw shift rd rs n ::i k) | Omul, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pmulw rd rs1 rs2 ::i k) @@ -543,6 +564,12 @@ Definition transl_op do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pmaddiw r1 r2 n ::i k) + | Omsub, a1 :: a2 :: a3 :: nil => + assertion (mreg_eq a1 res); + do r1 <- ireg_of a1; + do r2 <- ireg_of a2; + do r3 <- ireg_of a3; + OK (Pmsubw r1 r2 r3 ::i k) (* [Omakelong], [Ohighlong] should not occur *) | Olowlong, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; @@ -567,6 +594,15 @@ Definition transl_op | Osubl, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Psubl rd rs1 rs2 ::i k) + | Orevsubxl shift, a1 :: a2 :: nil => + do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; + OK (Prevsubxl shift rd rs1 rs2 ::i k) + | Orevsublimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Prevsubil rd rs n ::i k) + | Orevsubxlimm shift n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Prevsubxil shift rd rs n ::i k) | Omull, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pmull rd rs1 rs2 ::i k) @@ -662,6 +698,12 @@ Definition transl_op do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pmaddil r1 r2 n ::i k) + | Omsubl, a1 :: a2 :: a3 :: nil => + assertion (mreg_eq a1 res); + do r1 <- ireg_of a1; + do r2 <- ireg_of a2; + do r3 <- ireg_of a3; + OK (Pmsubl r1 r2 r3 ::i k) | Oabsf, a1 :: nil => do rd <- freg_of res; do rs <- freg_of a1; OK (Pfabsd rd rs ::i k) diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index 3bef1a5c..886228ad 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -429,7 +429,9 @@ Inductive arith_name_rrr : Type := | Pfcompl (ft: ftest) (**r comparison float64 *) | Paddw (**r add word *) - | Psubw (**r sub word *) + | Paddxw (shift : shift1_4) (**r add shift *) + | Psubw (**r sub word word *) + | Prevsubxw (shift : shift1_4) (**r sub shift word *) | Pmulw (**r mul word *) | Pandw (**r and word *) | Pnandw (**r nand word *) @@ -445,7 +447,9 @@ Inductive arith_name_rrr : Type := | Psllw (**r shift left logical word *) | Paddl (**r add long *) + | Paddxl (shift : shift1_4) (**r add shift long *) | Psubl (**r sub long *) + | Prevsubxl (shift : shift1_4) (**r sub shift long *) | Pandl (**r and long *) | Pnandl (**r nand long *) | Porl (**r or long *) @@ -472,6 +476,9 @@ Inductive arith_name_rri32 : Type := | Pcompiw (it: itest) (**r comparison imm word *) | Paddiw (**r add imm word *) + | Paddxiw (shift : shift1_4) + | Prevsubiw (**r add imm word *) + | Prevsubxiw (shift : shift1_4) | Pmuliw (**r add imm word *) | Pandiw (**r and imm word *) | Pnandiw (**r nand imm word *) @@ -495,6 +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 : shift1_4) + | Prevsubil + | Prevsubxil (shift : shift1_4) | Pmulil (**r mul immediate long *) | Pandil (**r and immediate long *) | Pnandil (**r nand immediate long *) @@ -509,6 +519,8 @@ Inductive arith_name_rri64 : Type := Inductive arith_name_arrr : Type := | Pmaddw (**r multiply add word *) | Pmaddl (**r multiply add long *) + | Pmsubw (**r multiply subtract word *) + | Pmsubl (**r multiply subtract long *) | Pcmove (bt: btest) (**r conditional move *) | Pcmoveu (bt: btest) (**r conditional move, test on unsigned semantics *) . @@ -1055,12 +1067,19 @@ Definition arith_eval_rrr n v1 v2 := | Pfsbfw => Val.subfs v1 v2 | Pfmuld => Val.mulf v1 v2 | Pfmulw => Val.mulfs v1 v2 + + | Paddxw shift => ExtValues.addx (int_of_shift1_4 shift) v1 v2 + | Paddxl shift => ExtValues.addxl (int_of_shift1_4 shift) v1 v2 + + | Prevsubxw shift => ExtValues.revsubx (int_of_shift1_4 shift) v1 v2 + | Prevsubxl shift => ExtValues.revsubxl (int_of_shift1_4 shift) v1 v2 end. Definition arith_eval_rri32 n v i := match n with | Pcompiw c => compare_int c v (Vint i) | Paddiw => Val.add v (Vint i) + | Prevsubiw => Val.sub (Vint i) v | Pmuliw => Val.mul v (Vint i) | Pandiw => Val.and v (Vint i) | Pnandiw => Val.notint (Val.and v (Vint i)) @@ -1079,12 +1098,15 @@ 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 => ExtValues.addx (int_of_shift1_4 shift) v (Vint i) + | Prevsubxiw shift => ExtValues.revsubx (int_of_shift1_4 shift) v (Vint i) end. Definition arith_eval_rri64 n v i := match n with | Pcompil c => compare_long c v (Vlong i) | Paddil => Val.addl v (Vlong i) + | Prevsubil => Val.subl (Vlong i) v | Pmulil => Val.mull v (Vlong i) | Pandil => Val.andl v (Vlong i) | Pnandil => Val.notl (Val.andl v (Vlong i)) @@ -1094,12 +1116,16 @@ 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 => ExtValues.addxl (int_of_shift1_4 shift) v (Vlong i) + | Prevsubxil shift => ExtValues.revsubxl (int_of_shift1_4 shift) v (Vlong i) end. Definition arith_eval_arrr n v1 v2 v3 := match n with | Pmaddw => Val.add v1 (Val.mul v2 v3) | Pmaddl => Val.addl v1 (Val.mull v2 v3) + | Pmsubw => Val.sub v1 (Val.mul v2 v3) + | Pmsubl => Val.subl v1 (Val.mull v2 v3) | Pcmove bt => match cmp_for_btest bt with | (Some c, Int) => diff --git a/mppa_k1c/ConstpropOp.vp b/mppa_k1c/ConstpropOp.vp index b5128357..7ee3dfe8 100644 --- a/mppa_k1c/ConstpropOp.vp +++ b/mppa_k1c/ConstpropOp.vp @@ -298,7 +298,7 @@ Nondetfunction addr_strength_reduction (addr: addressing) (args: list reg) (vl: list aval) := match addr, args, vl with | Aindexed n, r1 :: nil, Ptr(Gl symb n1) :: nil => - if (orb (Archi.pic_code tt) (negb (Compopts.optim_fglobaladdrtmp tt))) + if (orb (Archi.pic_code tt) (negb (Compopts.optim_globaladdrtmp tt))) then (addr, args) else (Aglobal symb (Ptrofs.add n1 n), nil) | Aindexed n, r1 :: nil, Ptr(Stk n1) :: nil => diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v index 980e18f8..155afa83 100644 --- a/mppa_k1c/ExtValues.v +++ b/mppa_k1c/ExtValues.v @@ -2,6 +2,42 @@ 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 shift1_4_of_z (x : Z) := + if Z.eq_dec x 1 then Some SHIFT1 + else if Z.eq_dec x 2 then Some SHIFT2 + else if Z.eq_dec x 3 then Some SHIFT3 + else if Z.eq_dec x 4 then Some SHIFT4 + else None. + +Lemma shift1_4_of_z_correct : + forall z, + match shift1_4_of_z z with + | Some x => z_of_shift1_4 x = z + | None => True + end. +Proof. + intro. unfold shift1_4_of_z. + destruct (Z.eq_dec _ _); simpl; try congruence. + destruct (Z.eq_dec _ _); simpl; try congruence. + destruct (Z.eq_dec _ _); simpl; try congruence. + destruct (Z.eq_dec _ _); simpl; try congruence. + trivial. +Qed. + +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) @@ -577,3 +613,61 @@ Proof. } } Qed. + +Lemma sub_add_neg : + forall x y, Val.sub x y = Val.add x (Val.neg y). +Proof. + destruct x; destruct y; simpl; trivial. + f_equal. + apply Int.sub_add_opp. +Qed. + +Lemma neg_mul_distr_r : + forall x y, Val.neg (Val.mul x y) = Val.mul x (Val.neg y). +Proof. + destruct x; destruct y; simpl; trivial. + f_equal. + apply Int.neg_mul_distr_r. +Qed. + +(* pointer diff +Lemma sub_addl_negl : + forall x y, Val.subl x y = Val.addl x (Val.negl y). +Proof. + destruct x; destruct y; simpl; trivial. + + f_equal. apply Int64.sub_add_opp. + + destruct (Archi.ptr64) eqn:ARCHI64; trivial. + f_equal. rewrite Ptrofs.sub_add_opp. + pose (Ptrofs.agree64_neg ARCHI64 (Ptrofs.of_int64 i0) i0) as Hagree. + unfold Ptrofs.agree64 in Hagree. + unfold Ptrofs.add. + f_equal. f_equal. + rewrite Hagree. + pose (Ptrofs.agree64_of_int ARCHI64 (Int64.neg i0)) as Hagree2. + rewrite Hagree2. + reflexivity. + exact (Ptrofs.agree64_of_int ARCHI64 i0). + + destruct (Archi.ptr64) eqn:ARCHI64; simpl; trivial. + destruct (eq_block _ _); simpl; trivial. +Qed. + *) + +Lemma negl_mull_distr_r : + forall x y, Val.negl (Val.mull x y) = Val.mull x (Val.negl y). +Proof. + destruct x; destruct y; simpl; trivial. + f_equal. + apply Int64.neg_mul_distr_r. +Qed. + +Definition addx sh v1 v2 := + Val.add v2 (Val.shl v1 (Vint sh)). + +Definition addxl sh v1 v2 := + Val.addl v2 (Val.shll v1 (Vint sh)). + +Definition revsubx sh v1 v2 := + Val.sub v2 (Val.shl v1 (Vint sh)). + +Definition revsubxl sh v1 v2 := + Val.subl v2 (Val.shll v1 (Vint sh)). diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index cd8c6606..db3dfe64 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -213,7 +213,9 @@ Global Opaque Definition two_address_op (op: operation) : bool := match op with - | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ + | Omadd | Omaddimm _ + | Omaddl | Omaddlimm _ + | Omsub | Omsubl | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _ | Oinsf _ _ | Oinsfl _ _ => true | _ => false diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index c10f5c56..5ba9851f 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -42,8 +42,13 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Ocast16signed => op1 (sign_ext 16 nv) | Oadd => op2 (modarith nv) | Oaddimm n => op1 (modarith nv) + | Oaddx _ => op2 (default nv) + | Oaddximm _ _ => op1 (default nv) | Oneg => op1 (modarith nv) | Osub => op2 (default nv) + | Orevsubimm _ => op1 (default nv) + | Orevsubx _ => op2 (default nv) + | Orevsubximm _ _ => op1 (default nv) | Omul => op2 (modarith nv) | Omulimm _ => op1 (modarith nv) | Omulhs | Omulhu | Odiv | Odivu | Omod | Omodu => op2 (default nv) @@ -72,12 +77,18 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Oshrximm n => op1 (default nv) | Omadd => op3 (modarith nv) | Omaddimm n => op2 (modarith nv) + | Omsub => op3 (modarith nv) | Omakelong => op2 (default nv) | Olowlong | Ohighlong => op1 (default nv) | Ocast32signed => op1 (default nv) | Ocast32unsigned => op1 (default nv) | Oaddl => op2 (default nv) | Oaddlimm n => op1 (default nv) + | Oaddxl _ => op2 (default nv) + | Oaddxlimm _ _ => op1 (default nv) + | Orevsublimm _ => op1 (default nv) + | Orevsubxl _ => op2 (default nv) + | Orevsubxlimm _ _ => op1 (default nv) | Onegl => op1 (default nv) | Osubl => op2 (default nv) | Omull => op2 (default nv) @@ -107,6 +118,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Oshrxlimm n => op1 (default nv) | Omaddl => op3 (default nv) | Omaddlimm n => op2 (default nv) + | Omsubl => op3 (default nv) | Onegf | Oabsf => op1 (default nv) | Oaddf | Osubf | Omulf | Odivf => op2 (default nv) | Onegfs | Oabsfs => op1 (default nv) @@ -229,6 +241,26 @@ Proof. - apply Val.addl_lessdef; trivial. Qed. +Lemma subl_lessdef: + forall v1 v1' v2 v2', + Val.lessdef v1 v1' -> Val.lessdef v2 v2' -> Val.lessdef (Val.subl v1 v2) (Val.subl v1' v2'). +Proof. + intros. inv H. inv H0. auto. destruct v1'; simpl; auto. simpl; auto. +Qed. + +Lemma subl_sound: + forall v1 w1 v2 w2 x, + vagree v1 w1 (default x) -> vagree v2 w2 (default x) -> + vagree (Val.subl v1 v2) (Val.subl w1 w2) x. +Proof. + unfold default; intros. + destruct x; simpl in *; trivial. + - unfold Val.subl. + destruct v1; destruct v2; trivial; destruct Archi.ptr64; simpl; trivial. + destruct (eq_block _ _) ; simpl; trivial. + - apply subl_lessdef; trivial. +Qed. + Lemma mull_sound: forall v1 w1 v2 w2 x, @@ -423,7 +455,7 @@ Remark default_idem: forall nv, default (default nv) = default nv. Proof. destruct nv; simpl; trivial. Qed. - + Lemma needs_of_operation_sound: forall op args v nv args', eval_operation ge (Vptr sp Ptrofs.zero) op args m1 = Some v -> @@ -466,11 +498,22 @@ Proof. (* madd *) - apply add_sound; try apply mul_sound; auto with na; rewrite modarith_idem; assumption. - apply add_sound; try apply mul_sound; auto with na; rewrite modarith_idem; assumption. +- repeat rewrite ExtValues.sub_add_neg. + apply add_sound; trivial. + apply neg_sound; trivial. + rewrite modarith_idem. + apply mul_sound; + rewrite modarith_idem; trivial. (* maddl *) - apply addl_sound; trivial. apply mull_sound; trivial. rewrite default_idem; trivial. rewrite default_idem; trivial. + (* msubl *) +- apply subl_sound; trivial. + apply mull_sound; trivial. + rewrite default_idem; trivial. + rewrite default_idem; trivial. (* select *) - apply select_sound; trivial. (* selectl *) diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 5e80589b..4df157b0 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -79,8 +79,13 @@ Inductive operation : Type := | Ocast16signed (**r [rd] is 16-bit sign extension of [r1] *) | Oadd (**r [rd = r1 + r2] *) | Oaddimm (n: int) (**r [rd = r1 + n] *) + | Oaddx (shift: shift1_4) (**r [rd = r1 << shift + r2] *) + | Oaddximm (shift: shift1_4) (n: int) (**r [rd = r1 << shift + n] *) | Oneg (**r [rd = - r1] *) | Osub (**r [rd = r1 - r2] *) + | Orevsubimm (n: int) (**r [rd = n - r1] *) + | Orevsubx (shift: shift1_4) (**r [rd = r2 -r1 << shift] *) + | Orevsubximm (shift: shift1_4) (n: int) (**r [rd = n -r1 << shift] *) | Omul (**r [rd = r1 * r2] *) | Omulimm (n: int) (**r [rd = r1 * n] *) | Omulhs (**r [rd = high part of r1 * r2, signed] *) @@ -116,6 +121,7 @@ Inductive operation : Type := | Ororimm (n: int) (**r rotate right immediate *) | Omadd (**r [rd = rd + r1 * r2] *) | Omaddimm (n: int) (**r [rd = rd + r1 * imm] *) + | Omsub (**r [rd = rd - r1 * r2] *) (*c 64-bit integer arithmetic: *) | Omakelong (**r [rd = r1 << 32 | r2] *) | Olowlong (**r [rd = low-word(r1)] *) @@ -124,6 +130,11 @@ Inductive operation : Type := | Ocast32unsigned (**r [rd] is 32-bit zero extension of [r1] *) | Oaddl (**r [rd = r1 + r2] *) | Oaddlimm (n: int64) (**r [rd = r1 + n] *) + | Oaddxl (shift: shift1_4) (**r [rd = r1 << shift + r2] *) + | Oaddxlimm (shift: shift1_4) (n: int64) (**r [rd = r1 << shift + n] *) + | Orevsublimm (n: int64) (**r [rd = n - r1] *) + | Orevsubxl (shift: shift1_4) (**r [rd = r2 -r1 << shift] *) + | Orevsubxlimm (shift: shift1_4) (n: int64) (**r [rd = n -r1 << shift] *) | Onegl (**r [rd = - r1] *) | Osubl (**r [rd = r1 - r2] *) | Omull (**r [rd = r1 * r2] *) @@ -160,6 +171,7 @@ Inductive operation : Type := | Oshrxlimm (n: int) (**r [rd = r1 / 2^n] (signed) *) | Omaddl (**r [rd = rd + r1 * r2] *) | Omaddlimm (n: int64) (**r [rd = rd + r1 * imm] *) + | Omsubl (**r [rd = rd - r1 * r2] *) (*c Floating-point arithmetic: *) | Onegf (**r [rd = - r1] *) | Oabsf (**r [rd = abs(r1)] *) @@ -235,9 +247,14 @@ Proof. decide equality. Defined. +Definition eq_shift1_4 (x y : shift1_4): {x=y} + {x<>y}. +Proof. + decide equality. +Defined. + Definition eq_operation: forall (x y: operation), {x=y} + {x<>y}. Proof. - generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition eq_condition0 Z.eq_dec; intros. + generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition eq_condition0 Z.eq_dec eq_shift1_4; intros. decide equality. Defined. @@ -386,8 +403,13 @@ Definition eval_operation | Ocast16signed, v1 :: nil => Some (Val.sign_ext 16 v1) | Oadd, v1 :: v2 :: nil => Some (Val.add v1 v2) | Oaddimm n, v1 :: nil => Some (Val.add v1 (Vint n)) + | Oaddx s14, v1 :: v2 :: nil => Some (addx (int_of_shift1_4 s14) v1 v2) + | Oaddximm s14 n, v1 :: nil => Some (addx (int_of_shift1_4 s14) v1 (Vint n)) | Oneg, v1 :: nil => Some (Val.neg v1) | Osub, v1 :: v2 :: nil => Some (Val.sub v1 v2) + | Orevsubimm n, v1 :: nil => Some (Val.sub (Vint n) v1) + | Orevsubx shift, v1 :: v2 :: nil => Some (ExtValues.revsubx (int_of_shift1_4 shift) v1 v2) + | Orevsubximm shift n, v1 :: nil => Some (ExtValues.revsubx (int_of_shift1_4 shift) v1 (Vint n)) | Omul, v1 :: v2 :: nil => Some (Val.mul v1 v2) | Omulimm n, v1 :: nil => Some (Val.mul v1 (Vint n)) | Omulhs, v1::v2::nil => Some (Val.mulhs v1 v2) @@ -423,6 +445,7 @@ Definition eval_operation | Oshrximm n, v1::nil => Val.shrx v1 (Vint n) | Omadd, v1::v2::v3::nil => Some (Val.add v1 (Val.mul v2 v3)) | (Omaddimm n), v1::v2::nil => Some (Val.add v1 (Val.mul v2 (Vint n))) + | Omsub, v1::v2::v3::nil => Some (Val.sub v1 (Val.mul v2 v3)) | Omakelong, v1::v2::nil => Some (Val.longofwords v1 v2) | Olowlong, v1::nil => Some (Val.loword v1) @@ -431,8 +454,13 @@ Definition eval_operation | Ocast32unsigned, v1 :: nil => Some (Val.longofintu v1) | Oaddl, v1 :: v2 :: nil => Some (Val.addl v1 v2) | Oaddlimm n, v1::nil => Some (Val.addl v1 (Vlong n)) + | Oaddxl s14, v1 :: v2 :: nil => Some (addxl (int_of_shift1_4 s14) v1 v2) + | Oaddxlimm s14 n, v1 :: nil => Some (addxl (int_of_shift1_4 s14) v1 (Vlong n)) | Onegl, v1::nil => Some (Val.negl v1) | Osubl, v1::v2::nil => Some (Val.subl v1 v2) + | Orevsublimm n, v1 :: nil => Some (Val.subl (Vlong n) v1) + | Orevsubxl shift, v1 :: v2 :: nil => Some (ExtValues.revsubxl (int_of_shift1_4 shift) v1 v2) + | Orevsubxlimm shift n, v1 :: nil => Some (ExtValues.revsubxl (int_of_shift1_4 shift) v1 (Vlong n)) | Omull, v1::v2::nil => Some (Val.mull v1 v2) | Omullimm n, v1::nil => Some (Val.mull v1 (Vlong n)) | Omullhs, v1::v2::nil => Some (Val.mullhs v1 v2) @@ -467,6 +495,7 @@ Definition eval_operation | Oshrxlimm n, v1::nil => Val.shrxl v1 (Vint n) | Omaddl, v1::v2::v3::nil => Some (Val.addl v1 (Val.mull v2 v3)) | (Omaddlimm n), v1::v2::nil => Some (Val.addl v1 (Val.mull v2 (Vlong n))) + | Omsubl, v1::v2::v3::nil => Some (Val.subl v1 (Val.mull v2 v3)) | Onegf, v1::nil => Some (Val.negf v1) | Oabsf, v1::nil => Some (Val.absf v1) @@ -583,8 +612,13 @@ Definition type_of_operation (op: operation) : list typ * typ := | Ocast16signed => (Tint :: nil, Tint) | Oadd => (Tint :: Tint :: nil, Tint) | Oaddimm _ => (Tint :: nil, Tint) + | Oaddx _ => (Tint :: Tint :: nil, Tint) + | Oaddximm _ _ => (Tint :: nil, Tint) | Oneg => (Tint :: nil, Tint) | Osub => (Tint :: Tint :: nil, Tint) + | Orevsubimm _ => (Tint :: nil, Tint) + | Orevsubx _ => (Tint :: Tint :: nil, Tint) + | Orevsubximm _ _ => (Tint :: nil, Tint) | Omul => (Tint :: Tint :: nil, Tint) | Omulimm _ => (Tint :: nil, Tint) | Omulhs => (Tint :: Tint :: nil, Tint) @@ -620,6 +654,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Ororimm _ => (Tint :: nil, Tint) | Omadd => (Tint :: Tint :: Tint :: nil, Tint) | Omaddimm _ => (Tint :: Tint :: nil, Tint) + | Omsub => (Tint :: Tint :: Tint :: nil, Tint) | Omakelong => (Tint :: Tint :: nil, Tlong) | Olowlong => (Tlong :: nil, Tint) @@ -628,6 +663,11 @@ Definition type_of_operation (op: operation) : list typ * typ := | Ocast32unsigned => (Tint :: nil, Tlong) | Oaddl => (Tlong :: Tlong :: nil, Tlong) | Oaddlimm _ => (Tlong :: nil, Tlong) + | Oaddxl _ => (Tlong :: Tlong :: nil, Tlong) + | Oaddxlimm _ _ => (Tlong :: nil, Tlong) + | Orevsublimm _ => (Tlong :: nil, Tlong) + | Orevsubxl _ => (Tlong :: Tlong :: nil, Tlong) + | Orevsubxlimm _ _ => (Tlong :: nil, Tlong) | Onegl => (Tlong :: nil, Tlong) | Osubl => (Tlong :: Tlong :: nil, Tlong) | Omull => (Tlong :: Tlong :: nil, Tlong) @@ -664,6 +704,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oshrxlimm _ => (Tlong :: nil, Tlong) | Omaddl => (Tlong :: Tlong :: Tlong :: nil, Tlong) | Omaddlimm _ => (Tlong :: Tlong :: nil, Tlong) + | Omsubl => (Tlong :: Tlong :: Tlong :: nil, Tlong) | Onegf => (Tfloat :: nil, Tfloat) | Oabsf => (Tfloat :: nil, Tfloat) @@ -736,6 +777,32 @@ Proof. intros. unfold Val.has_type, Val.addl. destruct Archi.ptr64, v1, v2; auto. Qed. +Remark type_sub: + forall v1 v2, Val.has_type (Val.sub v1 v2) Tint. +Proof. + intros. unfold Val.has_type, Val.sub. destruct Archi.ptr64, v1, v2; simpl; auto. + destruct (eq_block _ _); auto. +Qed. + +Remark type_subl: + forall v1 v2, Val.has_type (Val.subl v1 v2) Tlong. +Proof. + intros. unfold Val.has_type, Val.subl. destruct Archi.ptr64, v1, v2; simpl; auto. + destruct (eq_block _ _); auto. +Qed. + +Remark type_shl: + forall v1 v2, Val.has_type (Val.shl v1 v2) Tint. +Proof. + destruct v1, v2; simpl; trivial; destruct (Int.ltu _ _); simpl; trivial. +Qed. + +Remark type_shll: + forall v1 v2, Val.has_type (Val.shll v1 v2) Tlong. +Proof. + destruct v1, v2; simpl; trivial; destruct (Int.ltu _ _); simpl; trivial. +Qed. + Lemma type_of_operation_sound: forall op vl sp v m, op <> Omove -> @@ -761,9 +828,18 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* add, addimm *) - apply type_add. - apply type_add. + (* addx, addximm *) + - apply type_add. + - destruct v0; simpl; trivial. + destruct (Int.ltu _ _); simpl; trivial. (* neg, sub *) - destruct v0... - - unfold Val.sub. destruct v0; destruct v1... + - apply type_sub. + (* revsubimm, revsubx, revsubximm *) + - destruct v0... + - apply type_sub. + - destruct v0; simpl; trivial. + destruct (Int.ltu _ _); simpl; trivial. (* mul, mulimm, mulhs, mulhu *) - destruct v0; destruct v1... - destruct v0... @@ -819,8 +895,10 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* shrimm *) - destruct v0; simpl... (* madd *) - - destruct v0; destruct v1; destruct v2... - - destruct v0; destruct v1... + - apply type_add. + - apply type_add. + (* msub *) + - apply type_sub. (* makelong, lowlong, highlong *) - destruct v0; destruct v1... - destruct v0... @@ -831,11 +909,17 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* addl, addlimm *) - apply type_addl. - apply type_addl. + (* addxl addxlimm *) + - apply type_addl. + - destruct v0; simpl; trivial. + destruct (Int.ltu _ _); simpl; trivial. (* negl, subl *) - destruct v0... - - unfold Val.subl. destruct v0; destruct v1... - unfold Val.has_type; destruct Archi.ptr64... - destruct (eq_block b b0)... + - apply type_subl. + - destruct v0; simpl; trivial. + destruct (Int.ltu _ _); simpl; trivial. + - destruct v0... + - apply type_subl. (* mull, mullhs, mullhu *) - destruct v0; destruct v1... - destruct v0... @@ -889,10 +973,10 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* shrxl *) - destruct v0; simpl in H0; try discriminate. destruct (Int.ltu n (Int.repr 63)); inv H0... (* maddl, maddlim *) - - destruct v0; destruct v1; destruct v2; simpl; trivial. - destruct Archi.ptr64; simpl; trivial. - - destruct v0; destruct v1; simpl; trivial. - destruct Archi.ptr64; simpl; trivial. + - apply type_addl. + - apply type_addl. + (* msubl *) + - apply type_subl. (* negf, absf *) - destruct v0... - destruct v0... @@ -1359,9 +1443,19 @@ Proof. (* add, addimm *) - apply Val.add_inject; auto. - apply Val.add_inject; auto. + (* addx, addximm *) + - apply Val.add_inject; trivial. + inv H4; inv H2; simpl; try destruct (Int.ltu _ _); simpl; auto. + - inv H4; simpl; trivial. + destruct (Int.ltu _ _); simpl; trivial. (* neg, sub *) - inv H4; simpl; auto. - apply Val.sub_inject; auto. + (* revsubimm, revsubx, revsubximm *) + - inv H4; simpl; trivial. + - apply Val.sub_inject; trivial. + inv H4; inv H2; simpl; try destruct (Int.ltu _ _); simpl; auto. + - inv H4; simpl; try destruct (Int.ltu _ _); simpl; auto. (* mul, mulimm, mulhs, mulhu *) - inv H4; inv H2; simpl; auto. - inv H4; simpl; auto. @@ -1424,6 +1518,9 @@ Proof. (* madd, maddim *) - inv H2; inv H3; inv H4; simpl; auto. - inv H2; inv H4; simpl; auto. + (* msub *) + - apply Val.sub_inject; auto. + inv H3; inv H2; simpl; auto. (* makelong, highlong, lowlong *) - inv H4; inv H2; simpl; auto. - inv H4; simpl; auto. @@ -1434,9 +1531,21 @@ Proof. (* addl, addlimm *) - apply Val.addl_inject; auto. - apply Val.addl_inject; auto. + (* addxl, addxlimm *) + - apply Val.addl_inject; auto. + inv H4; simpl; trivial. + destruct (Int.ltu _ _); simpl; trivial. + - inv H4; simpl; trivial. + destruct (Int.ltu _ _); simpl; trivial. (* negl, subl *) - inv H4; simpl; auto. - apply Val.subl_inject; auto. + inv H4; inv H2; simpl; trivial; + destruct (Int.ltu _ _); simpl; trivial. + - inv H4; simpl; trivial; + destruct (Int.ltu _ _); simpl; trivial. + - inv H4; simpl; auto. + - apply Val.subl_inject; auto. (* mull, mullhs, mullhu *) - inv H4; inv H2; simpl; auto. - inv H4; simpl; auto. @@ -1500,6 +1609,9 @@ Proof. inv H2; inv H3; inv H4; simpl; auto. - apply Val.addl_inject; auto. inv H4; inv H2; simpl; auto. + (* msubl, msublimm *) + - apply Val.subl_inject; auto. + inv H2; inv H3; inv H4; simpl; auto. (* negf, absf *) - inv H4; simpl; auto. diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 7015fd5f..af1e8f85 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -61,7 +61,9 @@ let arith_rrr_str = function | Pfcompw ft -> "Pfcompw" | Pfcompl ft -> "Pfcompl" | Paddw -> "Paddw" + | Paddxw _ -> "Paddxw" | Psubw -> "Psubw" + | Prevsubxw _ -> "Psubxw" | Pmulw -> "Pmulw" | Pandw -> "Pandw" | Pnandw -> "Pnandw" @@ -76,7 +78,9 @@ let arith_rrr_str = function | Psrxw -> "Psrxw" | Psllw -> "Psllw" | Paddl -> "Paddl" + | Paddxl _ -> "Paddxl" | Psubl -> "Psubl" + | Prevsubxl _ -> "Psubxl" | Pandl -> "Pandl" | Pnandl -> "Pnandl" | Porl -> "Porl" @@ -100,6 +104,9 @@ let arith_rrr_str = function let arith_rri32_str = function | Pcompiw it -> "Pcompiw" | Paddiw -> "Paddiw" + | Paddxiw _ -> "Paddxiw" + | Prevsubiw -> "Psubiw" + | Prevsubxiw _ -> "Psubxiw" | Pmuliw -> "Pmuliw" | Pandiw -> "Pandiw" | Pnandiw -> "Pnandiw" @@ -122,6 +129,9 @@ let arith_rri32_str = function let arith_rri64_str = function | Pcompil it -> "Pcompil" | Paddil -> "Paddil" + | Prevsubil -> "Psubil" + | Paddxil _ -> "Paddxil" + | Prevsubxil _ -> "Psubxil" | Pmulil -> "Pmulil" | Pandil -> "Pandil" | Pnandil -> "Pnandil" @@ -140,6 +150,8 @@ let arith_arr_str = function let arith_arrr_str = function | Pmaddw -> "Pmaddw" | Pmaddl -> "Pmaddl" + | Pmsubw -> "Pmsubw" + | Pmsubl -> "Pmsubl" | Pcmove _ -> "Pcmove" | Pcmoveu _ -> "Pcmoveu" @@ -393,6 +405,10 @@ let alu_lite_x : int array = let resmap = fun r -> match r with | "ISSUE" -> 2 | "TINY" -> 1 | "LITE" -> 1 | _ -> 0 in Array.of_list (List.map resmap resource_names) +let alu_lite_y : int array = let resmap = fun r -> match r with + | "ISSUE" -> 3 | "TINY" -> 1 | "LITE" -> 1 | _ -> 0 + in Array.of_list (List.map resmap resource_names) + let alu_full : int array = let resmap = fun r -> match r with | "ISSUE" -> 1 | "TINY" -> 1 | "LITE" -> 1 | "ALU" -> 1 | _ -> 0 in Array.of_list (List.map resmap resource_names) @@ -452,8 +468,9 @@ type real_instruction = | Addw | Andw | Compw | Mulw | Orw | Sbfw | Sraw | Srlw | Sllw | Srsw | Rorw | Xorw | Addd | Andd | Compd | Muld | Ord | Sbfd | Srad | Srld | Slld | Srsd | Xord | Nandw | Norw | Nxorw | Nandd | Nord | Nxord | Andnw | Ornw | Andnd | Ornd - | Maddw | Maddd | Cmoved + | Maddw | Maddd | Msbfw | Msbfd | Cmoved | Make | Nop | Extfz | Extfs | Insf + | Addxw | Addxd (* LSU *) | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq | Lo | Sb | Sh | Sw | Sd | Sq | So @@ -467,6 +484,8 @@ type real_instruction = let ab_inst_to_real = function | "Paddw" | "Paddiw" | "Pcvtl2w" -> Addw + | "Paddxw" | "Paddxiw" -> Addxw + | "Paddxl" | "Paddxil" -> Addxd | "Paddl" | "Paddil" | "Pmv" | "Pmvw2l" -> Addd | "Pandw" | "Pandiw" -> Andw | "Pnandw" | "Pnandiw" -> Nandw @@ -493,6 +512,7 @@ let ab_inst_to_real = function | "Psllw" | "Pslliw" -> Sllw | "Proriw" -> Rorw | "Pmaddw" | "Pmaddiw" -> Maddw + | "Pmsubw" | "Pmsubiw" -> Msbfw | "Pslll" | "Psllil" -> Slld | "Pxorw" | "Pxoriw" -> Xorw | "Pnxorw" | "Pnxoriw" -> Nxorw @@ -502,7 +522,8 @@ let ab_inst_to_real = function | "Pnxorl" | "Pnxoril" -> Nxord | "Pandnl" | "Pandnil" -> Andnd | "Pornl" | "Pornil" -> Ornd - | "Pmaddl" -> Maddd + | "Pmaddl" | "Pmaddil" -> Maddd + | "Pmsubl" | "Pmsubil" -> Msbfd | "Pmake" | "Pmakel" | "Pmakefs" | "Pmakef" | "Ploadsymbol" -> Make | "Pnop" | "Pcvtw2l" -> Nop | "Pextfz" | "Pextfzl" | "Pzxwd" -> Extfz @@ -571,7 +592,7 @@ let rec_to_usage r = and real_inst = ab_inst_to_real r.inst in match real_inst with | Addw | Andw | Nandw | Orw | Norw | Sbfw | Xorw - | Nxorw | Andnw | Ornw -> + | Nxorw | Andnw | Ornw -> (match encoding with None | Some U6 | Some S10 -> alu_tiny | Some U27L5 | Some U27L10 -> alu_tiny_x | _ -> raise InvalidEncoding) @@ -580,6 +601,14 @@ let rec_to_usage r = (match encoding with None | Some U6 | Some S10 -> alu_tiny | Some U27L5 | Some U27L10 -> alu_tiny_x | Some E27U27L10 -> alu_tiny_y) + | Addxw -> + (match encoding with None | Some U6 | Some S10 -> alu_lite + | Some U27L5 | Some U27L10 -> alu_lite_x + | _ -> raise InvalidEncoding) + | Addxd -> + (match encoding with None | Some U6 | Some S10 -> alu_lite + | Some U27L5 | Some U27L10 -> alu_lite_x + | Some E27U27L10 -> alu_lite_y) | Compw -> (match encoding with None -> alu_tiny | Some U6 | Some S10 | Some U27L5 -> alu_tiny_x | _ -> raise InvalidEncoding) @@ -596,10 +625,10 @@ let rec_to_usage r = | Some U27L5 | Some U27L10 -> alu_tiny_x | Some E27U27L10 -> alu_tiny_y | _ -> raise InvalidEncoding) - | Mulw| Maddw -> (match encoding with None -> mau + | Mulw| Maddw | Msbfw -> (match encoding with None -> mau | Some U6 | Some S10 | Some U27L5 -> mau_x | _ -> raise InvalidEncoding) - | Muld | Maddd -> (match encoding with None | Some U6 | Some S10 -> mau + | Muld | Maddd | Msbfd -> (match encoding with None | Some U6 | Some S10 -> mau | Some U27L5 | Some U27L10 -> mau_x | Some E27U27L10 -> mau_y) | Nop -> alu_nop @@ -629,10 +658,10 @@ let real_inst_to_latency = function | Rorw | Nandw | Norw | Nxorw | Ornw | Andnw | Nandd | Nord | Nxord | Ornd | Andnd | Addd | Andd | Compd | Ord | Sbfd | Srad | Srsd | Srld | Slld | Xord | Make - | Extfs | Extfz | Insf | Fcompw | Fcompd | Cmoved + | Extfs | Extfz | Insf | Fcompw | Fcompd | Cmoved | Addxw | Addxd -> 1 | Floatwz | Floatuwz | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4 - | Mulw | Muld | Maddw | Maddd -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *) + | Mulw | Muld | Maddw | Maddd | Msbfw | Msbfd -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *) | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq | Lo -> 3 | Sb | Sh | Sw | Sd | Sq | So -> 1 (* See k1c-Optimization.pdf page 19 *) | Get -> 1 diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index 717b0120..4e369e11 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -66,19 +66,39 @@ Definition longofintu (e: expr) := (** ** Integer addition and pointer addition *) +Definition addlimm_shllimm sh k2 e1 := + if Compopts.optim_addx tt + then + match shift1_4_of_z (Int.unsigned sh) with + | Some s14 => Eop (Oaddxlimm s14 k2) (e1:::Enil) + | None => Eop (Oaddlimm k2) ((Eop (Oshllimm sh) (e1:::Enil)):::Enil) + end + else Eop (Oaddlimm k2) ((Eop (Oshllimm sh) (e1:::Enil)):::Enil). + Nondetfunction addlimm (n: int64) (e: expr) := if Int64.eq n Int64.zero then e else match e with | Eop (Olongconst m) Enil => longconst (Int64.add n m) | Eop (Oaddrsymbol s m) Enil => - (if Compopts.optim_fglobaladdroffset tt + (if Compopts.optim_globaladdroffset tt then Eop (Oaddrsymbol s (Ptrofs.add (Ptrofs.of_int64 n) m)) Enil else Eop (Oaddlimm n) (e ::: Enil)) | Eop (Oaddrstack m) Enil => Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int64 n) m)) Enil | Eop (Oaddlimm m) (t ::: Enil) => Eop (Oaddlimm(Int64.add n m)) (t ::: Enil) + | Eop (Oaddxlimm sh m) (t ::: Enil) => Eop (Oaddxlimm sh (Int64.add n m)) (t ::: Enil) + | Eop (Oshllimm sh) (t1:::Enil) => addlimm_shllimm sh n t1 | _ => Eop (Oaddlimm n) (e ::: Enil) end. +Definition addl_shllimm n e1 e2 := + if Compopts.optim_addx tt + then + match shift1_4_of_z (Int.unsigned n) with + | Some s14 => Eop (Oaddxl s14) (e1:::e2:::Enil) + | None => Eop Oaddl (e2:::(Eop (Oshllimm n) (e1:::Enil)):::Enil) + end + else Eop Oaddl (e2:::(Eop (Oshllimm n) (e1:::Enil)):::Enil). + Nondetfunction addl (e1: expr) (e2: expr) := if Archi.splitlong then SplitLong.addl e1 e2 else match e1, e2 with @@ -102,6 +122,10 @@ Nondetfunction addl (e1: expr) (e2: expr) := Eop (Omaddlimm n) (t1:::t2:::Enil) | (Eop (Omullimm n) (t2:::Enil)), t1 => Eop (Omaddlimm n) (t1:::t2:::Enil) + | (Eop (Oshllimm n) (t1:::Enil)), t2 => + addl_shllimm n t1 t2 + | t2, (Eop (Oshllimm n) (t1:::Enil)) => + addl_shllimm n t1 t2 | _, _ => Eop Oaddl (e1:::e2:::Enil) end. @@ -118,6 +142,10 @@ Nondetfunction subl (e1: expr) (e2: expr) := addlimm n1 (Eop Osubl (t1:::t2:::Enil)) | t1, Eop (Oaddlimm n2) (t2:::Enil) => addlimm (Int64.neg n2) (Eop Osubl (t1:::t2:::Enil)) + | t1, (Eop Omull (t2:::t3:::Enil)) => + Eop Omsubl (t1:::t2:::t3:::Enil) + | t1, (Eop (Omullimm n) (t2:::Enil)) => + Eop (Omaddlimm (Int64.neg n)) (t1:::t2:::Enil) | _, _ => Eop Osubl (e1:::e2:::Enil) end. @@ -225,7 +253,7 @@ Definition mullimm_base (n1: int64) (e2: expr) := | i :: j :: nil => Elet e2 (addl (shllimm (Eletvar 0) i) (shllimm (Eletvar 0) j)) | _ => - Eop Omull (e2 ::: longconst n1 ::: Enil) + Eop (Omullimm n1) (e2 ::: Enil) end. Nondetfunction mullimm (n1: int64) (e2: expr) := diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 3b724c01..78a2bb31 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -119,6 +119,76 @@ Proof. - TrivialExists. Qed. + +Theorem eval_addlimm_shllimm: + forall sh k2, unary_constructor_sound (addlimm_shllimm sh k2) (fun x => ExtValues.addxl sh x (Vlong k2)). +Proof. + red; unfold addlimm_shllimm; intros. + destruct (Compopts.optim_addx tt). + { + destruct (shift1_4_of_z (Int.unsigned sh)) as [s14 |] eqn:SHIFT. + - TrivialExists. simpl. + f_equal. + unfold shift1_4_of_z, int_of_shift1_4, z_of_shift1_4 in *. + destruct (Z.eq_dec _ _) as [e1|]. + { replace s14 with SHIFT1 by congruence. + destruct x; simpl; trivial. + replace (Int.ltu _ _) with true by reflexivity. + unfold Int.ltu. + rewrite e1. + replace (if zlt _ _ then true else false) with true by reflexivity. + rewrite <- e1. + rewrite Int.repr_unsigned. + reflexivity. + } + destruct (Z.eq_dec _ _) as [e2|]. + { replace s14 with SHIFT2 by congruence. + destruct x; simpl; trivial. + replace (Int.ltu _ _) with true by reflexivity. + unfold Int.ltu. + rewrite e2. + replace (if zlt _ _ then true else false) with true by reflexivity. + rewrite <- e2. + rewrite Int.repr_unsigned. + reflexivity. + } + destruct (Z.eq_dec _ _) as [e3|]. + { replace s14 with SHIFT3 by congruence. + destruct x; simpl; trivial. + replace (Int.ltu _ _) with true by reflexivity. + unfold Int.ltu. + rewrite e3. + replace (if zlt _ _ then true else false) with true by reflexivity. + rewrite <- e3. + rewrite Int.repr_unsigned. + reflexivity. + } + destruct (Z.eq_dec _ _) as [e4|]. + { replace s14 with SHIFT4 by congruence. + destruct x; simpl; trivial. + replace (Int.ltu _ _) with true by reflexivity. + unfold Int.ltu. + rewrite e4. + replace (if zlt _ _ then true else false) with true by reflexivity. + rewrite <- e4. + rewrite Int.repr_unsigned. + reflexivity. + } + discriminate. + - unfold addxl. rewrite Val.addl_commut. + TrivialExists. + repeat (try eassumption; try econstructor). + simpl. + reflexivity. + } + { unfold addxl. rewrite Val.addl_commut. + TrivialExists. + repeat (try eassumption; try econstructor). + simpl. + reflexivity. + } +Qed. + Theorem eval_addlimm: forall n, unary_constructor_sound (addlimm n) (fun v => Val.addl v (Vlong n)). Proof. unfold addlimm; intros; red; intros. @@ -127,7 +197,7 @@ Proof. destruct x; simpl; rewrite ?Int64.add_zero, ?Ptrofs.add_zero; auto. destruct (addlimm_match a); InvEval. - econstructor; split. apply eval_longconst. rewrite Int64.add_commut; auto. -- destruct (Compopts.optim_fglobaladdroffset _). +- destruct (Compopts.optim_globaladdroffset _). + econstructor; split. EvalOp. simpl; eauto. unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. destruct Archi.ptr64; auto. rewrite Ptrofs.add_commut; auto. @@ -136,9 +206,58 @@ Proof. destruct sp; simpl; auto. destruct Archi.ptr64; auto. rewrite Ptrofs.add_assoc, (Ptrofs.add_commut m0). auto. - subst x. rewrite Val.addl_assoc. rewrite Int64.add_commut. TrivialExists. +- TrivialExists; simpl. subst x. + destruct v1; simpl; trivial. + destruct (Int.ltu _ _); simpl; trivial. + rewrite Int64.add_assoc. rewrite Int64.add_commut. + reflexivity. +- pose proof eval_addlimm_shllimm as ADDXL. + unfold unary_constructor_sound in ADDXL. + unfold addxl in ADDXL. + rewrite Val.addl_commut. + subst x. + apply ADDXL; assumption. - TrivialExists. Qed. +Lemma eval_addxl: forall n, binary_constructor_sound (addl_shllimm n) (ExtValues.addxl n). +Proof. + red. + intros. + unfold addl_shllimm. + destruct (Compopts.optim_addx tt). + { + destruct (shift1_4_of_z (Int.unsigned n)) as [s14 |] eqn:SHIFT. + - TrivialExists. + simpl. + f_equal. f_equal. + unfold shift1_4_of_z, int_of_shift1_4, z_of_shift1_4 in *. + destruct (Z.eq_dec _ _) as [e1|]. + { replace s14 with SHIFT1 by congruence. + rewrite <- e1. + apply Int.repr_unsigned. } + destruct (Z.eq_dec _ _) as [e2|]. + { replace s14 with SHIFT2 by congruence. + rewrite <- e2. + apply Int.repr_unsigned. } + destruct (Z.eq_dec _ _) as [e3|]. + { replace s14 with SHIFT3 by congruence. + rewrite <- e3. + apply Int.repr_unsigned. } + destruct (Z.eq_dec _ _) as [e4|]. + { replace s14 with SHIFT4 by congruence. + rewrite <- e4. + apply Int.repr_unsigned. } + discriminate. + (* Oaddxl *) + - TrivialExists; + repeat econstructor; eassumption. + } + { TrivialExists; + repeat econstructor; eassumption. + } +Qed. + Theorem eval_addl: binary_constructor_sound addl Val.addl. Proof. unfold addl. destruct Archi.splitlong eqn:SL. @@ -193,6 +312,14 @@ Proof. - subst. rewrite Val.addl_commut. TrivialExists. - subst. TrivialExists. - subst. rewrite Val.addl_commut. TrivialExists. + - subst. pose proof eval_addxl as ADDXL. + unfold binary_constructor_sound in ADDXL. + rewrite Val.addl_commut. + apply ADDXL; assumption. + (* Oaddxl *) + - subst. pose proof eval_addxl as ADDXL. + unfold binary_constructor_sound in ADDXL. + apply ADDXL; assumption. - TrivialExists. Qed. @@ -208,6 +335,23 @@ Proof. - subst. rewrite Val.subl_addl_l. apply eval_addlimm; EvalOp. - subst. rewrite Val.subl_addl_r. apply eval_addlimm; EvalOp. +- TrivialExists. simpl. subst. reflexivity. +- TrivialExists. simpl. subst. + destruct v1; destruct x; simpl; trivial. + + f_equal. f_equal. + rewrite <- Int64.neg_mul_distr_r. + rewrite Int64.sub_add_opp. + reflexivity. + + destruct (Archi.ptr64) eqn:ARCHI64; simpl; trivial. + f_equal. f_equal. + rewrite <- Int64.neg_mul_distr_r. + rewrite Ptrofs.sub_add_opp. + unfold Ptrofs.add. + f_equal. f_equal. + rewrite (Ptrofs.agree64_neg ARCHI64 (Ptrofs.of_int64 (Int64.mul i n)) (Int64.mul i n)). + rewrite (Ptrofs.agree64_of_int ARCHI64 (Int64.neg (Int64.mul i n))). + reflexivity. + apply (Ptrofs.agree64_of_int ARCHI64). - TrivialExists. Qed. @@ -371,7 +515,7 @@ Proof. auto. } generalize (Int64.one_bits'_decomp n); intros D. destruct (Int64.one_bits' n) as [ | i [ | j [ | ? ? ]]] eqn:B. -- apply DEFAULT. +- TrivialExists. - replace (Val.mull x (Vlong n)) with (Val.shll x (Vint i)). apply eval_shllimm; auto. simpl in D. rewrite D, Int64.add_zero. destruct x; simpl; auto. @@ -389,7 +533,7 @@ Proof. rewrite (Int64.one_bits'_range n) in B2 by (rewrite B; auto with coqlib). inv B1; inv B2. simpl in B3; inv B3. rewrite Int64.mul_add_distr_r. rewrite <- ! Int64.shl'_mul. auto. -- apply DEFAULT. +- TrivialExists. Qed. Theorem eval_mullimm: forall n, unary_constructor_sound (mullimm n) (fun v => Val.mull v (Vlong n)). diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index aac3010e..23d234aa 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -104,6 +104,15 @@ Definition addrstack (ofs: ptrofs) := (** ** Integer addition and pointer addition *) +Definition addimm_shlimm sh k2 e1 := + if Compopts.optim_addx tt + then + match shift1_4_of_z (Int.unsigned sh) with + | Some s14 => Eop (Oaddximm s14 k2) (e1:::Enil) + | None => Eop (Oaddimm k2) ((Eop (Oshlimm sh) (e1:::Enil)):::Enil) + end + else Eop (Oaddimm k2) ((Eop (Oshlimm sh) (e1:::Enil)):::Enil). + Nondetfunction addimm (n: int) (e: expr) := if Int.eq n Int.zero then e else match e with @@ -111,9 +120,20 @@ Nondetfunction addimm (n: int) (e: expr) := | Eop (Oaddrsymbol s m) Enil => Eop (Oaddrsymbol s (Ptrofs.add (Ptrofs.of_int n) m)) Enil | Eop (Oaddrstack m) Enil => Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n) m)) Enil | Eop (Oaddimm m) (t ::: Enil) => Eop (Oaddimm(Int.add n m)) (t ::: Enil) + | Eop (Oaddximm sh m) (t ::: Enil) => Eop (Oaddximm sh (Int.add n m)) (t ::: Enil) + | Eop (Oshlimm sh) (t1:::Enil) => addimm_shlimm sh n t1 | _ => Eop (Oaddimm n) (e ::: Enil) end. +Definition add_shlimm n e1 e2 := + if Compopts.optim_addx tt + then + match shift1_4_of_z (Int.unsigned n) with + | Some s14 => Eop (Oaddx s14) (e1:::e2:::Enil) + | None => Eop Oadd (e2:::(Eop (Oshlimm n) (e1:::Enil)):::Enil) + end + else Eop Oadd (e2:::(Eop (Oshlimm n) (e1:::Enil)):::Enil). + Nondetfunction add (e1: expr) (e2: expr) := match e1, e2 with | Eop (Ointconst n1) Enil, t2 => addimm n1 t2 @@ -135,7 +155,11 @@ Nondetfunction add (e1: expr) (e2: expr) := | t1, (Eop (Omulimm n) (t2:::Enil)) => Eop (Omaddimm n) (t1:::t2:::Enil) | (Eop (Omulimm n) (t2:::Enil)), t1 => - Eop (Omaddimm n) (t1:::t2:::Enil) + Eop (Omaddimm n) (t1:::t2:::Enil) + | (Eop (Oshlimm n) (t1:::Enil)), t2 => + add_shlimm n t1 t2 + | t2, (Eop (Oshlimm n) (t1:::Enil)) => + add_shlimm n t1 t2 | _, _ => Eop Oadd (e1:::e2:::Enil) end. @@ -151,6 +175,10 @@ Nondetfunction sub (e1: expr) (e2: expr) := addimm n1 (Eop Osub (t1:::t2:::Enil)) | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil)) + | t1, (Eop Omul (t2:::t3:::Enil)) => + Eop Omsub (t1:::t2:::t3:::Enil) + | t1, (Eop (Omulimm n) (t2:::Enil)) => + Eop (Omaddimm (Int.neg n)) (t1:::t2:::Enil) | _, _ => Eop Osub (e1:::e2:::Enil) end. @@ -592,18 +620,26 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) := match e with | Eop (Oaddrstack n) Enil => (Ainstack n, Enil) | Eop (Oaddrsymbol id ofs) Enil => - (if (orb (Archi.pic_code tt) (negb (Compopts.optim_fglobaladdrtmp tt))) + (if (orb (Archi.pic_code tt) (negb (Compopts.optim_globaladdrtmp tt))) then (Aindexed Ptrofs.zero, e:::Enil) else (Aglobal id ofs, Enil)) | Eop (Oaddimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int n), e1:::Enil) | Eop (Oaddlimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int64 n), e1:::Enil) | Eop Oaddl (e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil) => - (if Compopts.optim_fxsaddr tt + (if Compopts.optim_xsaddr tt then let zscale := Int.unsigned scale in if Z.eq_dec zscale (zscale_of_chunk chunk) then (Aindexed2XS zscale, e1:::e2:::Enil) else (Aindexed2, e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil) else (Aindexed2, e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil)) + | Eop (Oaddxl sh) (e1:::e2:::Enil) => + let zscale := ExtValues.z_of_shift1_4 sh in + let scale := Int.repr zscale in + (if Compopts.optim_xsaddr tt + then if Z.eq_dec zscale (zscale_of_chunk chunk) + then (Aindexed2XS zscale, e2:::e1:::Enil) + else (Aindexed2, e2:::(Eop (Oshllimm scale) (e1:::Enil)):::Enil) + else (Aindexed2, e2:::(Eop (Oshllimm scale) (e1:::Enil)):::Enil)) | Eop Oaddl (e1:::e2:::Enil) => (Aindexed2, e1:::e2:::Enil) | _ => (Aindexed Ptrofs.zero, e:::Enil) end. diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index d22725d5..a5154611 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -183,6 +183,75 @@ Proof. auto. Qed. +Theorem eval_addimm_shlimm: + forall sh k2, unary_constructor_sound (addimm_shlimm sh k2) (fun x => ExtValues.addx sh x (Vint k2)). +Proof. + red; unfold addimm_shlimm; intros. + destruct (Compopts.optim_addx tt). + { + destruct (shift1_4_of_z (Int.unsigned sh)) as [s14 |] eqn:SHIFT. + - TrivialExists. simpl. + f_equal. + unfold shift1_4_of_z, int_of_shift1_4, z_of_shift1_4 in *. + destruct (Z.eq_dec _ _) as [e1|]. + { replace s14 with SHIFT1 by congruence. + destruct x; simpl; trivial. + replace (Int.ltu _ _) with true by reflexivity. + unfold Int.ltu. + rewrite e1. + replace (if zlt _ _ then true else false) with true by reflexivity. + rewrite <- e1. + rewrite Int.repr_unsigned. + reflexivity. + } + destruct (Z.eq_dec _ _) as [e2|]. + { replace s14 with SHIFT2 by congruence. + destruct x; simpl; trivial. + replace (Int.ltu _ _) with true by reflexivity. + unfold Int.ltu. + rewrite e2. + replace (if zlt _ _ then true else false) with true by reflexivity. + rewrite <- e2. + rewrite Int.repr_unsigned. + reflexivity. + } + destruct (Z.eq_dec _ _) as [e3|]. + { replace s14 with SHIFT3 by congruence. + destruct x; simpl; trivial. + replace (Int.ltu _ _) with true by reflexivity. + unfold Int.ltu. + rewrite e3. + replace (if zlt _ _ then true else false) with true by reflexivity. + rewrite <- e3. + rewrite Int.repr_unsigned. + reflexivity. + } + destruct (Z.eq_dec _ _) as [e4|]. + { replace s14 with SHIFT4 by congruence. + destruct x; simpl; trivial. + replace (Int.ltu _ _) with true by reflexivity. + unfold Int.ltu. + rewrite e4. + replace (if zlt _ _ then true else false) with true by reflexivity. + rewrite <- e4. + rewrite Int.repr_unsigned. + reflexivity. + } + discriminate. + - unfold addx. rewrite Val.add_commut. + TrivialExists. + repeat (try eassumption; try econstructor). + simpl. + reflexivity. + } + { unfold addx. rewrite Val.add_commut. + TrivialExists. + repeat (try eassumption; try econstructor). + simpl. + reflexivity. + } +Qed. + Theorem eval_addimm: forall n, unary_constructor_sound (addimm n) (fun x => Val.add x (Vint n)). Proof. @@ -198,9 +267,57 @@ Proof. + econstructor; split. EvalOp. simpl; eauto. destruct sp; simpl; auto. + TrivialExists; simpl. subst x. rewrite Val.add_assoc. rewrite Int.add_commut. auto. + + TrivialExists; simpl. subst x. + destruct v1; simpl; trivial. + destruct (Int.ltu _ _); simpl; trivial. + rewrite Int.add_assoc. rewrite Int.add_commut. + reflexivity. + + pose proof eval_addimm_shlimm as ADDX. + unfold unary_constructor_sound in ADDX. + unfold addx in ADDX. + rewrite Val.add_commut. + subst x. + apply ADDX; assumption. + TrivialExists. Qed. +Lemma eval_addx: forall n, binary_constructor_sound (add_shlimm n) (ExtValues.addx n). +Proof. + red. + intros. + unfold add_shlimm. + destruct (Compopts.optim_addx tt). + { + destruct (shift1_4_of_z (Int.unsigned n)) as [s14 |] eqn:SHIFT. + - TrivialExists. + simpl. + f_equal. f_equal. + unfold shift1_4_of_z, int_of_shift1_4, z_of_shift1_4 in *. + destruct (Z.eq_dec _ _) as [e1|]. + { replace s14 with SHIFT1 by congruence. + rewrite <- e1. + apply Int.repr_unsigned. } + destruct (Z.eq_dec _ _) as [e2|]. + { replace s14 with SHIFT2 by congruence. + rewrite <- e2. + apply Int.repr_unsigned. } + destruct (Z.eq_dec _ _) as [e3|]. + { replace s14 with SHIFT3 by congruence. + rewrite <- e3. + apply Int.repr_unsigned. } + destruct (Z.eq_dec _ _) as [e4|]. + { replace s14 with SHIFT4 by congruence. + rewrite <- e4. + apply Int.repr_unsigned. } + discriminate. + - TrivialExists; + repeat econstructor; eassumption. + } + { TrivialExists; + repeat econstructor; eassumption. + } +Qed. + Theorem eval_add: binary_constructor_sound add Val.add. Proof. red; intros until y. @@ -238,6 +355,15 @@ Proof. subst. TrivialExists. - (* Omaddimm rev *) subst. rewrite Val.add_commut. TrivialExists. + (* Oaddx *) + - subst. pose proof eval_addx as ADDX. + unfold binary_constructor_sound in ADDX. + rewrite Val.add_commut. + apply ADDX; assumption. + (* Oaddx *) + - subst. pose proof eval_addx as ADDX. + unfold binary_constructor_sound in ADDX. + apply ADDX; assumption. - TrivialExists. Qed. @@ -251,6 +377,12 @@ Proof. apply eval_addimm; EvalOp. - subst. rewrite Val.sub_add_l. apply eval_addimm; EvalOp. - subst. rewrite Val.sub_add_r. apply eval_addimm; EvalOp. + - TrivialExists. simpl. subst. reflexivity. + - TrivialExists. simpl. subst. + rewrite sub_add_neg. + rewrite neg_mul_distr_r. + unfold Val.neg. + reflexivity. - TrivialExists. Qed. @@ -1297,7 +1429,7 @@ Proof. - exists (v1 :: nil); split. eauto with evalexpr. simpl. destruct v1; simpl in H; try discriminate. destruct Archi.ptr64 eqn:SF; inv H. simpl. auto. - - destruct (Compopts.optim_fxsaddr tt). + - destruct (Compopts.optim_xsaddr tt). + destruct (Z.eq_dec _ _). * exists (v1 :: v2 :: nil); split. repeat (constructor; auto). simpl. rewrite Int.repr_unsigned. destruct v2; simpl in *; congruence. @@ -1309,6 +1441,25 @@ Proof. repeat (constructor; auto). econstructor. repeat (constructor; auto). eassumption. simpl. congruence. simpl. congruence. + - unfold addxl in *. + destruct (Compopts.optim_xsaddr tt). + + unfold int_of_shift1_4 in *. + destruct (Z.eq_dec _ _). + * exists (v0 :: v1 :: nil); split. + repeat (constructor; auto). simpl. + congruence. + * eexists; split. + repeat (constructor; auto). eassumption. + econstructor. + repeat (constructor; auto). eassumption. simpl. + reflexivity. + simpl. congruence. + + eexists; split. + repeat (constructor; auto). eassumption. + econstructor. + repeat (constructor; auto). eassumption. simpl. + reflexivity. + simpl. unfold int_of_shift1_4 in *. congruence. - exists (v1 :: v0 :: nil); split. repeat (constructor; auto). simpl. congruence. - exists (v :: nil); split. eauto with evalexpr. subst. simpl. rewrite Ptrofs.add_zero; auto. Qed. diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 96779517..34765726 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -145,6 +145,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 @@ -528,8 +534,14 @@ module Target (*: TARGET*) = | Paddw (rd, rs1, rs2) -> fprintf oc " addw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + | 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 + | Prevsubxw (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 | Pandw (rd, rs1, rs2) -> @@ -558,22 +570,30 @@ module Target (*: TARGET*) = fprintf oc " sllw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Pmaddw (rd, rs1, rs2) -> fprintf oc " maddw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + | Pmsubw (rd, rs1, rs2) -> + fprintf oc " msbfw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 - | Paddl (rd, rs1, rs2) -> assert Archi.ptr64; + | Paddl (rd, rs1, rs2) -> fprintf oc " addd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + | 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 - | Pandl (rd, rs1, rs2) -> assert Archi.ptr64; + | Prevsubxl (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 - | Pnandl (rd, rs1, rs2) -> assert Archi.ptr64; + | Pnandl (rd, rs1, rs2) -> fprintf oc " nandd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 - | Porl (rd, rs1, rs2) -> assert Archi.ptr64; + | Porl (rd, rs1, rs2) -> fprintf oc " ord %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 - | Pnorl (rd, rs1, rs2) -> assert Archi.ptr64; + | Pnorl (rd, rs1, rs2) -> fprintf oc " nord %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 - | Pxorl (rd, rs1, rs2) -> assert Archi.ptr64; + | Pxorl (rd, rs1, rs2) -> fprintf oc " xord %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 - | Pnxorl (rd, rs1, rs2) -> assert Archi.ptr64; + | Pnxorl (rd, rs1, rs2) -> fprintf oc " nxord %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Pandnl (rd, rs1, rs2) -> fprintf oc " andnd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 @@ -591,6 +611,8 @@ module Target (*: TARGET*) = fprintf oc " srad %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Pmaddl (rd, rs1, rs2) -> fprintf oc " maddd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + | Pmsubl (rd, rs1, rs2) -> + fprintf oc " msbfd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Pfaddd (rd, rs1, rs2) -> fprintf oc " faddd %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 @@ -610,6 +632,14 @@ 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 (s14, rd, rs, imm) -> + fprintf oc " addx%dw %a = %a, %a\n" (scale_of_shift1_4 s14) + ireg rd ireg rs coqint imm + | Prevsubiw (rd, rs, imm) -> + fprintf oc " sbfw %a = %a, %a\n" ireg rd ireg rs coqint imm + | Prevsubxiw (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 | Pandiw (rd, rs, imm) -> @@ -655,6 +685,14 @@ 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 (s14, rd, rs, imm) -> + fprintf oc " addx%dd %a = %a, %a\n" (scale_of_shift1_4 s14) + ireg rd ireg rs coqint imm + | Prevsubil (rd, rs, imm) -> + fprintf oc " sbfd %a = %a, %a\n" ireg rd ireg rs coqint64 imm + | Prevsubxil (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 | Pandil (rd, rs, imm) -> assert Archi.ptr64; diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index 643cca0c..f41dae63 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -161,8 +161,13 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Ocast16signed, v1 :: nil => sign_ext 16 v1 | Oadd, v1::v2::nil => add v1 v2 | Oaddimm n, v1::nil => add v1 (I n) + | Oaddx shift, v1::v2::nil => add v2 (shl v1 (I (int_of_shift1_4 shift))) + | Oaddximm shift n, v1::nil => add (I n) (shl v1 (I (int_of_shift1_4 shift))) | Oneg, v1::nil => neg v1 | Osub, v1::v2::nil => sub v1 v2 + | Orevsubx shift, v1::v2::nil => sub v2 (shl v1 (I (int_of_shift1_4 shift))) + | Orevsubimm n, v1::nil => sub (I n) v1 + | Orevsubximm shift n, v1::nil => sub (I n) (shl v1 (I (int_of_shift1_4 shift))) | Omul, v1::v2::nil => mul v1 v2 | Omulimm n, v1::nil => mul v1 (I n) | Omulhs, v1::v2::nil => mulhs v1 v2 @@ -198,6 +203,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Oshrximm n, v1::nil => shrx v1 (I n) | Omadd, v1::v2::v3::nil => add v1 (mul v2 v3) | Omaddimm n, v1::v2::nil => add v1 (mul v2 (I n)) + | Omsub, v1::v2::v3::nil => sub v1 (mul v2 v3) | Omakelong, v1::v2::nil => longofwords v1 v2 | Olowlong, v1::nil => loword v1 | Ohighlong, v1::nil => hiword v1 @@ -205,8 +211,13 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Ocast32unsigned, v1::nil => longofintu v1 | Oaddl, v1::v2::nil => addl v1 v2 | Oaddlimm n, v1::nil => addl v1 (L n) + | Oaddxl shift, v1::v2::nil => addl v2 (shll v1 (I (int_of_shift1_4 shift))) + | Oaddxlimm shift n, v1::nil => addl (L n) (shll v1 (I (int_of_shift1_4 shift))) | Onegl, v1::nil => negl v1 | Osubl, v1::v2::nil => subl v1 v2 + | Orevsubxl shift, v1::v2::nil => subl v2 (shll v1 (I (int_of_shift1_4 shift))) + | Orevsublimm n, v1::nil => subl (L n) v1 + | Orevsubxlimm shift n, v1::nil => subl (L n) (shll v1 (I (int_of_shift1_4 shift))) | Omull, v1::v2::nil => mull v1 v2 | Omullimm n, v1::nil => mull v1 (L n) | Omullhs, v1::v2::nil => mullhs v1 v2 @@ -241,6 +252,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Oshrxlimm n, v1::nil => shrxl v1 (I n) | Omaddl, v1::v2::v3::nil => addl v1 (mull v2 v3) | Omaddlimm n, v1::v2::nil => addl v1 (mull v2 (L n)) + | Omsubl, v1::v2::v3::nil => subl v1 (mull v2 v3) | Onegf, v1::nil => negf v1 | Oabsf, v1::nil => absf v1 | Oaddf, v1::v2::nil => addf v1 v2 @@ -359,12 +371,46 @@ Theorem eval_static_operation_sound: list_forall2 (vmatch bc) vargs aargs -> vmatch bc vres (eval_static_operation op aargs). Proof. - unfold eval_operation, eval_static_operation, eval_static_select, eval_static_selectl, eval_static_selectf, eval_static_selectfs; intros; + unfold eval_operation, eval_static_operation, eval_static_select, eval_static_selectl, eval_static_selectf, eval_static_selectfs, addx, revsubx, addxl, revsubxl; intros. destruct op; InvHyps; eauto with va. - destruct (propagate_float_constants tt); constructor. - destruct (propagate_float_constants tt); constructor. - rewrite Ptrofs.add_zero_l; eauto with va. - apply of_optbool_sound. eapply eval_static_condition_sound; eauto. + - destruct (propagate_float_constants tt); constructor. + - destruct (propagate_float_constants tt); constructor. + - rewrite Ptrofs.add_zero_l; eauto with va. + - replace(match Val.shl a1 (Vint (int_of_shift1_4 shift)) with + | Vint n2 => Vint (Int.add n n2) + | Vptr b2 ofs2 => + if Archi.ptr64 + then Vundef + else Vptr b2 (Ptrofs.add ofs2 (Ptrofs.of_int n)) + | _ => Vundef + end) with (Val.add (Vint n) (Val.shl a1 (Vint (int_of_shift1_4 shift)))). + + eauto with va. + + destruct a1; destruct shift; reflexivity. + - (*revsubimm*) inv H1; constructor. + - replace (match Val.shl a1 (Vint (int_of_shift1_4 shift)) with + | Vint n2 => Vint (Int.sub n n2) + | _ => Vundef + end) with (Val.sub (Vint n) (Val.shl a1 (Vint (int_of_shift1_4 shift)))). + + eauto with va. + + destruct n; destruct shift; reflexivity. + - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with + | Vlong n2 => Vlong (Int64.add n n2) + | Vptr b2 ofs2 => + if Archi.ptr64 + then Vptr b2 (Ptrofs.add ofs2 (Ptrofs.of_int64 n)) + else Vundef + | _ => Vundef + end) with (Val.addl (Vlong n) (Val.shll a1 (Vint (int_of_shift1_4 shift)))). + + eauto with va. + + destruct a1; destruct shift; reflexivity. + - inv H1; constructor. + - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with + | Vlong n2 => Vlong (Int64.sub n n2) + | _ => Vundef + end) with (Val.subl (Vlong n) (Val.shll a1 (Vint (int_of_shift1_4 shift)))). + + eauto with va. + + destruct a1; destruct shift; reflexivity. + - apply of_optbool_sound. eapply eval_static_condition_sound; eauto. (* select *) - assert (Hcond : (cmatch (eval_condition0 cond a2 m) (eval_static_condition0 cond b2))) by (apply eval_static_condition0_sound; assumption). rewrite eval_select_to2. diff --git a/test/monniaux/bitsliced-aes/bs.c b/test/monniaux/bitsliced-aes/bs.c index 083a8fc5..3132e1d9 100644 --- a/test/monniaux/bitsliced-aes/bs.c +++ b/test/monniaux/bitsliced-aes/bs.c @@ -3,7 +3,11 @@ #include "bs.h" #include "../ternary.h" +/* TEMPORARY */ +#define TERNARY(x, v0, v1) ((x) ? (v0) : (v1)) +/* #define TERNARY(x, v0, v1) TERNARY64(x, v1, v0) +*/ #if (defined(__BYTE_ORDER__) && __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__) ||\ defined(__amd64__) || defined(__amd32__)|| defined(__amd16__) |