begin generating Prevsub etc. from Oxxx to Pxxx

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;