From d8d22519bff9414f973a1310cb32eb60e6695796 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 11 May 2019 06:02:13 +0200 Subject: begin generating Prevsub etc. from Oxxx to Pxxx --- mppa_k1c/Asm.v | 24 +++++++++++----------- mppa_k1c/Asmblockdeps.v | 12 +++++------ mppa_k1c/Asmblockgen.v | 3 +++ mppa_k1c/Asmblockgenproof1.v | 2 +- mppa_k1c/Asmvliw.v | 24 +++++++++++----------- mppa_k1c/PostpassSchedulingOracle.ml | 12 +++++------ mppa_k1c/TargetPrinter.ml | 12 +++++------ .../lustre-convertible-en-2cgc/convertible_main.c | 2 +- 8 files changed, 47 insertions(+), 44 deletions(-) diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 04f6969b..e5f81fbb 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -184,7 +184,7 @@ Inductive instruction : Type := | 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 *) - | Psubxw (shift : shift1_4) (rd rs1 rs2: ireg) (**r add 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 *) @@ -204,7 +204,7 @@ Inductive instruction : Type := | 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 *) - | Psubxl (shift : shift1_4) (rd rs1 rs2: ireg) (**r sub long shift *) + | 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 *) @@ -233,8 +233,8 @@ Inductive instruction : Type := | Paddiw (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 : shift1_4) (rd rs: ireg) (imm: int) (**r subtract 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 *) @@ -259,8 +259,8 @@ Inductive instruction : Type := | 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 *) - | Psubil (rd rs: ireg) (imm: int64) (**r subtract imm long *) - | Psubxil (shift : shift1_4) (rd rs: ireg) (imm: int64) (**r subtract imm 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 *) @@ -352,7 +352,7 @@ Definition basic_to_instruction (b: basic) := | 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.Psubxw shift) rd rs1 rs2 => Psubxw shift 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 @@ -370,7 +370,7 @@ Definition basic_to_instruction (b: basic) := | 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.Psubxl shift) rd rs1 rs2 => Psubxl shift 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 @@ -396,8 +396,8 @@ Definition basic_to_instruction (b: basic) := | 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.Psubiw rd rs imm => Psubiw rd rs imm - | PArithRRI32 (Asmvliw.Psubxiw shift) rd rs imm => Psubxiw 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 @@ -421,8 +421,8 @@ Definition basic_to_instruction (b: basic) := | 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.Psubil rd rs imm => Psubil rd rs imm - | PArithRRI64 (Asmvliw.Psubxil shift) rd rs imm => Psubxil 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 diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 82062fab..616ec6db 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1412,7 +1412,7 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring := | Paddw => "Paddw" | Paddxw _ => "Paddxw" | Psubw => "Psubw" - | Psubxw _ => "Psubxw" + | Prevsubxw _ => "Prevsubxw" | Pmulw => "Pmulw" | Pandw => "Pandw" | Pnandw => "Pnandw" @@ -1429,7 +1429,7 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring := | Paddl => "Paddl" | Paddxl _ => "Paddxl" | Psubl => "Psubl" - | Psubxl _ => "Psubxl" + | Prevsubxl _ => "Prevsubxl" | Pandl => "Pandl" | Pnandl => "Pnandl" | Porl => "Porl" @@ -1455,9 +1455,9 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring := match n with Pcompiw _ => "Pcompiw" | Paddiw => "Paddiw" - | Psubiw => "Psubiw" | Paddxiw _ => "Paddxiw" - | Psubxiw _ => "Psubxiw" + | Prevsubiw => "Prevsubiw" + | Prevsubxiw _ => "Prevsubxiw" | Pmuliw => "Pmuliw" | Pandiw => "Pandiw" | Pnandiw => "Pnandiw" @@ -1482,9 +1482,9 @@ Definition string_of_name_rri64 (n: arith_name_rri64): pstring := match n with Pcompil _ => "Pcompil" | Paddil => "Paddil" - | Psubil => "Psubil" + | Prevsubil => "Prevsubil" | Paddxil _ => "Paddxil" - | Psubxil _ => "Psubxil" + | Prevsubxil _ => "Prevsubxil" | Pmulil => "Pmulil" | Pandil => "Pandil" | Pnandil => "Pnandil" diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index f2292f9a..839d444d 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -449,6 +449,9 @@ Definition transl_op | 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) | 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) diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 86a0ff88..1569aedf 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1693,7 +1693,7 @@ Opaque Int.eq. split; intros; Simpl. assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto. destruct (rs x0); auto; simpl. rewrite A; simpl. Simpl. unfold Val.shr. rewrite A. - apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. + apply Val.lessdef_same. f_equal. apply Int.sign_ext_shr_shl. split; reflexivity. - (* Oshrximm *) econstructor; split. + apply exec_straight_one. simpl. eauto. diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index e332cedc..2bf9115e 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -431,7 +431,7 @@ Inductive arith_name_rrr : Type := | Paddw (**r add word *) | Paddxw (shift : shift1_4) (**r add shift *) | Psubw (**r sub word word *) - | Psubxw (shift : shift1_4) (**r sub shift word *) + | Prevsubxw (shift : shift1_4) (**r sub shift word *) | Pmulw (**r mul word *) | Pandw (**r and word *) | Pnandw (**r nand word *) @@ -449,7 +449,7 @@ Inductive arith_name_rrr : Type := | Paddl (**r add long *) | Paddxl (shift : shift1_4) (**r add shift long *) | Psubl (**r sub long *) - | Psubxl (shift : shift1_4) (**r sub shift long *) + | Prevsubxl (shift : shift1_4) (**r sub shift long *) | Pandl (**r and long *) | Pnandl (**r nand long *) | Porl (**r or long *) @@ -477,8 +477,8 @@ Inductive arith_name_rri32 : Type := | Paddiw (**r add imm word *) | Paddxiw (shift : shift1_4) - | Psubiw (**r add imm word *) - | Psubxiw (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 *) @@ -503,8 +503,8 @@ Inductive arith_name_rri64 : Type := | Pcompil (it: itest) (**r comparison imm long *) | Paddil (**r add immediate long *) | Paddxil (shift : shift1_4) - | Psubil - | Psubxil (shift : shift1_4) + | Prevsubil + | Prevsubxil (shift : shift1_4) | Pmulil (**r mul immediate long *) | Pandil (**r and immediate long *) | Pnandil (**r nand immediate long *) @@ -1071,16 +1071,16 @@ Definition arith_eval_rrr n v1 v2 := | 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))) + | Prevsubxw shift => Val.sub v2 (Val.shl v1 (Vint (int_of_shift1_4 shift))) - | Psubxl shift => Val.subl v1 (Val.shll v2 (Vint (int_of_shift1_4 shift))) + | Prevsubxl shift => Val.subl v2 (Val.shll v1 (Vint (int_of_shift1_4 shift))) 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) - | Psubiw => Val.sub 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)) @@ -1100,14 +1100,14 @@ Definition arith_eval_rri32 n v i := | Psrlil => Val.shrlu v (Vint i) | Psrail => Val.shrl v (Vint i) | 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))) + | Prevsubxiw shift => Val.sub (Vint i) (Val.shl v (Vint (int_of_shift1_4 shift))) 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) - | Psubil => Val.subl 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)) @@ -1118,7 +1118,7 @@ Definition arith_eval_rri64 n v i := | Pandnil => Val.andl (Val.notl v) (Vlong i) | Pornil => Val.orl (Val.notl v) (Vlong i) | 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))) + | Prevsubxil 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/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 9b22cd01..9dc1ab44 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -63,7 +63,7 @@ let arith_rrr_str = function | Paddw -> "Paddw" | Paddxw _ -> "Paddxw" | Psubw -> "Psubw" - | Psubxw _ -> "Psubxw" + | Prevsubxw _ -> "Psubxw" | Pmulw -> "Pmulw" | Pandw -> "Pandw" | Pnandw -> "Pnandw" @@ -80,7 +80,7 @@ let arith_rrr_str = function | Paddl -> "Paddl" | Paddxl _ -> "Paddxl" | Psubl -> "Psubl" - | Psubxl _ -> "Psubxl" + | Prevsubxl _ -> "Psubxl" | Pandl -> "Pandl" | Pnandl -> "Pnandl" | Porl -> "Porl" @@ -105,8 +105,8 @@ let arith_rri32_str = function | Pcompiw it -> "Pcompiw" | Paddiw -> "Paddiw" | Paddxiw _ -> "Paddxiw" - | Psubiw -> "Psubiw" - | Psubxiw _ -> "Psubxiw" + | Prevsubiw -> "Psubiw" + | Prevsubxiw _ -> "Psubxiw" | Pmuliw -> "Pmuliw" | Pandiw -> "Pandiw" | Pnandiw -> "Pnandiw" @@ -129,9 +129,9 @@ let arith_rri32_str = function let arith_rri64_str = function | Pcompil it -> "Pcompil" | Paddil -> "Paddil" - | Psubil -> "Psubil" + | Prevsubil -> "Psubil" | Paddxil _ -> "Paddxil" - | Psubxil _ -> "Psubxil" + | Prevsubxil _ -> "Psubxil" | Pmulil -> "Pmulil" | Pandil -> "Pandil" | Pnandil -> "Pnandil" diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 6a21e63d..2d870c01 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -524,7 +524,7 @@ module Target (*: TARGET*) = ireg rd ireg rs1 ireg rs2 | Psubw (rd, rs1, rs2) -> fprintf oc " sbfw %a = %a, %a\n" ireg rd ireg rs2 ireg rs1 - | Psubxw (s14, rd, rs1, rs2) -> + | 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) -> @@ -565,7 +565,7 @@ module Target (*: TARGET*) = ireg rd ireg rs1 ireg rs2 | Psubl (rd, rs1, rs2) -> fprintf oc " sbfd %a = %a, %a\n" ireg rd ireg rs2 ireg rs1 - | Psubxl (s14, rd, rs1, rs2) -> + | 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) -> @@ -620,9 +620,9 @@ module Target (*: TARGET*) = | 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) -> + | Prevsubiw (rd, rs, imm) -> fprintf oc " sbfw %a = %a, %a\n" ireg rd ireg rs coqint imm - | Psubxiw (s14, rd, rs, 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) -> @@ -673,9 +673,9 @@ module Target (*: TARGET*) = | 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) -> + | Prevsubil (rd, rs, imm) -> fprintf oc " sbfd %a = %a, %a\n" ireg rd ireg rs coqint64 imm - | Psubxil (s14, rd, rs, 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; diff --git a/test/monniaux/lustre-convertible-en-2cgc/convertible_main.c b/test/monniaux/lustre-convertible-en-2cgc/convertible_main.c index 4dc333dd..6a4db4c3 100644 --- a/test/monniaux/lustre-convertible-en-2cgc/convertible_main.c +++ b/test/monniaux/lustre-convertible-en-2cgc/convertible_main.c @@ -58,7 +58,7 @@ DM_INLINE void Lustre_arrow_3_step(_real i1[50],_real i2[50],_real out[50]/*out* } // End of Lustre_arrow_3_step // Step function(s) for Lustre_hat_ctx -void Lustre_hat_step(_real i1,_real out[50]/*out*/){ +DM_INLINE void Lustre_hat_step(_real i1,_real out[50]/*out*/){ out[0] = i1; out[1] = i1; out[2] = i1; -- cgit