From eb814730ba3bc29ab7db69a5d6f46f172aff0152 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 18 Mar 2019 15:15:16 +0100
Subject: begin implementing multiply-add

---
 mppa_k1c/Asm.v            |  6 +++++-
 mppa_k1c/TargetPrinter.ml | 12 ++++++++++--
 2 files changed, 15 insertions(+), 3 deletions(-)

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 8486e25d..55143e4f 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -148,6 +148,7 @@ Inductive instruction : Type :=
   | Psraw               (rd rs1 rs2: ireg)          (**r shift right arithmetic word *)
   | 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 *)
 
   | Paddl               (rd rs1 rs2: ireg)          (**r add long *)
   | Psubl               (rd rs1 rs2: ireg)          (**r sub long *)
@@ -163,6 +164,7 @@ Inductive instruction : Type :=
   | Pslll               (rd rs1 rs2: ireg)          (**r shift left logical long *)
   | Psrll               (rd rs1 rs2: ireg)          (**r shift right logical long *)
   | Psral               (rd rs1 rs2: ireg)          (**r shift right arithmetic long *)
+  | Pmaddl              (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 *)
@@ -187,6 +189,7 @@ Inductive instruction : Type :=
   | Psrliw              (rd rs: ireg) (imm: int)    (**r shift right logical imm word *)
   | Pslliw              (rd rs: ireg) (imm: int)    (**r shift left logical imm word *)
   | Proriw              (rd rs: ireg) (imm: int)    (**r rotate right imm word *) 
+  | Pmaddiw             (rd rs: ireg) (imm: int)    (**r multiply add imm word *)
   | Psllil              (rd rs: ireg) (imm: int)    (**r shift left logical immediate long *)
   | Psrlil              (rd rs: ireg) (imm: int)    (**r shift right logical immediate long *)
   | Psrail              (rd rs: ireg) (imm: int)    (**r shift right arithmetic immediate long *)
@@ -202,7 +205,8 @@ Inductive instruction : Type :=
   | Pnxoril             (rd rs: ireg) (imm: int64)  (**r xor immediate long *)
   | Pandnil             (rd rs: ireg) (imm: int64)  (**r andn long *)
   | Pornil              (rd rs: ireg) (imm: int64)  (**r orn long *)
-  .
+  | Pmaddil             (rd rs: ireg) (imm: int64)  (**r multiply add imm long *)
+.
 
 (** Correspondance between Asmblock and Asm *)
 
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index c3de5206..5c5d6c79 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -390,6 +390,8 @@ module Target (*: TARGET*) =
          fprintf oc "	srlw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Psllw (rd, rs1, rs2) ->
          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
 
       | Paddl (rd, rs1, rs2) -> assert Archi.ptr64;
          fprintf oc "	addd	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
@@ -419,6 +421,8 @@ module Target (*: TARGET*) =
          fprintf oc "	srld	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Psral   (rd, rs1, rs2) ->
          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
 
       | Pfaddd (rd, rs1, rs2) ->
          fprintf oc "	faddd	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
@@ -462,6 +466,8 @@ module Target (*: TARGET*) =
          fprintf oc "	sllw	%a = %a, %a\n" ireg rd ireg rs coqint imm
       | Proriw (rd, rs, imm) ->
          fprintf oc "	rorw	%a = %a, %a\n" ireg rd ireg rs coqint imm
+      | Pmaddiw (rd, rs, imm) ->
+         fprintf oc "	maddw	%a = %a, %a\n" ireg rd ireg rs coqint imm
 
       | Psllil (rd, rs, imm) ->
          fprintf oc "	slld	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
@@ -488,9 +494,11 @@ module Target (*: TARGET*) =
       | Pnxoril (rd, rs, imm) -> assert Archi.ptr64;
          fprintf oc "	nxord	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
       | Pandnil (rd, rs, imm) -> 
-         fprintf oc "	andnd	%a = %a, %a\n" ireg rd ireg rs coqint imm
+         fprintf oc "	andnd	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
       | Pornil (rd, rs, imm) -> 
-         fprintf oc "	ornd	%a = %a, %a\n" ireg rd ireg rs coqint imm
+         fprintf oc "	ornd	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
+      | Pmaddil (rd, rs, imm) ->
+         fprintf oc "	maddd	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
 
     let get_section_names name =
       let (text, lit) =
-- 
cgit 


From 652a59174685ef4d4333a56812e2c30041828c16 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 18 Mar 2019 18:35:31 +0100
Subject: ça passe mais pas encore l'oracle
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 mppa_k1c/Asm.v          | 10 ++++++++++
 mppa_k1c/Asmblock.v     | 38 ++++++++++++++++++++++++++++++++++++
 mppa_k1c/Asmblockdeps.v | 51 ++++++++++++++++++++++++++++++++++++++++++++++++-
 3 files changed, 98 insertions(+), 1 deletion(-)

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 55143e4f..1a57e554 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -347,6 +347,16 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRRI64 Asmblock.Pandnil rd rs imm      => Pandnil rd rs imm
   | PArithRRI64 Asmblock.Pornil rd rs imm       => Pornil rd rs imm
 
+  (** ARRR *)
+  | PArithARRR Asmblock.Pmaddw rd rs1 rs2       => Pmaddw rd rs1 rs2
+  | PArithARRR Asmblock.Pmaddl rd rs1 rs2       => Pmaddl rd rs1 rs2
+
+  (** ARRI32 *)
+  | PArithARRI32 Asmblock.Pmaddiw rd rs1 imm    => Pmaddiw rd rs1 imm
+
+  (** ARRI64 *)
+  | PArithARRI64 Asmblock.Pmaddil rd rs1 imm    => Pmaddil rd rs1 imm
+                                                          
   (** Load *)
   | PLoadRRO Asmblock.Plb rd ra ofs   => Plb rd ra ofs
   | PLoadRRO Asmblock.Plbu rd ra ofs  => Plbu rd ra ofs
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index cdbe4eb3..9b51ea33 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -406,6 +406,19 @@ Inductive arith_name_rri64 : Type :=
   | Pornil                                          (**r orn immediate long *)
 .
 
+Inductive arith_name_arrr : Type :=
+  | Pmaddw                                           (**r multiply add word *)
+  | Pmaddl                                           (**r multiply add long *)
+.
+
+Inductive arith_name_arri32 : Type :=
+  | Pmaddiw                                           (**r multiply add word *)
+.
+
+Inductive arith_name_arri64 : Type :=
+  | Pmaddil                                           (**r multiply add long *)
+.
+
 Inductive ar_instruction : Type :=
   | PArithR     (i: arith_name_r)     (rd: ireg)
   | PArithRR    (i: arith_name_rr)    (rd rs: ireg)
@@ -416,6 +429,9 @@ Inductive ar_instruction : Type :=
   | PArithRRR   (i: arith_name_rrr)   (rd rs1 rs2: ireg)
   | PArithRRI32 (i: arith_name_rri32) (rd rs: ireg) (imm: int)
   | PArithRRI64 (i: arith_name_rri64) (rd rs: ireg) (imm: int64)
+  | PArithARRR   (i: arith_name_arrr)   (rd rs1 rs2: ireg)
+  | PArithARRI32 (i: arith_name_arri32) (rd rs: ireg) (imm: int)
+  | PArithARRI64 (i: arith_name_arri64) (rd rs: ireg) (imm: int64)
 .
 
 Coercion PArithR:       arith_name_r        >-> Funclass.
@@ -1180,6 +1196,22 @@ Definition arith_eval_rri64 n v i :=
   | Pornil  => Val.orl (Val.notl 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)
+  end.                    
+
+Definition arith_eval_arri32 n v1 v2 v3 :=
+  match n with
+  | Pmaddiw => Val.add v1 (Val.mul v2 (Vint v3))
+  end.                    
+
+Definition arith_eval_arri64 n v1 v2 v3 :=
+  match n with
+  | Pmaddil => Val.addl v1 (Val.mull v2 (Vlong v3))
+  end.                    
+
 Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   match ai with
   | PArithR n d => rs#d <- (arith_eval_r n)
@@ -1196,6 +1228,12 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
   | PArithRRI32 n d s i => rs#d <- (arith_eval_rri32 n rs#s i)
 
   | PArithRRI64 n d s i => rs#d <- (arith_eval_rri64 n rs#s i)
+
+  | PArithARRR n d s1 s2 => rs#d <- (arith_eval_arrr n rs#d rs#s1 rs#s2)
+
+  | PArithARRI32 n d s i => rs#d <- (arith_eval_arri32 n rs#d rs#s i)
+
+  | PArithARRI64 n d s i => rs#d <- (arith_eval_arri64 n rs#d rs#s i)
   end.
 
 (** * load/store *)
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index d69903b4..5a138d00 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -52,6 +52,9 @@ Inductive arith_op :=
   | OArithRRR (n: arith_name_rrr)
   | OArithRRI32 (n: arith_name_rri32) (imm: int)
   | OArithRRI64 (n: arith_name_rri64) (imm: int64)
+  | OArithARRR (n: arith_name_arrr)
+  | OArithARRI32 (n: arith_name_arri32) (imm: int)
+  | OArithARRI64 (n: arith_name_arri64) (imm: int64)
 .
 
 Coercion OArithR: arith_name_r >-> arith_op.
@@ -109,10 +112,13 @@ Definition arith_eval (ao: arith_op) (l: list value) :=
   | OArithRF64 n i, [] => Some (Val (arith_eval_rf64 n i))
 
   | OArithRRR n, [Val v1; Val v2] => Some (Val (arith_eval_rrr n v1 v2))
-
   | OArithRRI32 n i, [Val v] => Some (Val (arith_eval_rri32 n v i))
   | OArithRRI64 n i, [Val v] => Some (Val (arith_eval_rri64 n v i))
 
+  | OArithARRR n, [Val v1; Val v2; Val v3] => Some (Val (arith_eval_arrr n v1 v2 v3))
+  | OArithARRI32 n i, [Val v1; Val v2] => Some (Val (arith_eval_arri32 n v1 v2 i))
+  | OArithARRI64 n i, [Val v1; Val v2] => Some (Val (arith_eval_arri64 n v1 v2 i))
+
   | _, _ => None
   end.
 
@@ -525,6 +531,9 @@ Definition trans_arith (ai: ar_instruction) : macro :=
   | PArithRRR n d s1 s2 => [(#d, Op (Arith (OArithRRR n)) (Name (#s1) @ Name (#s2) @ Enil))]
   | PArithRRI32 n d s i => [(#d, Op (Arith (OArithRRI32 n i)) (Name (#s) @ Enil))]
   | PArithRRI64 n d s i => [(#d, Op (Arith (OArithRRI64 n i)) (Name (#s) @ Enil))]
+  | PArithARRR n d s1 s2 => [(#d, Op (Arith (OArithARRR n)) (Name(#d) @ Name (#s1) @ Name (#s2) @ Enil))]
+  | PArithARRI32 n d s i => [(#d, Op (Arith (OArithARRI32 n i)) (Name(#d) @ Name (#s) @ Enil))]
+  | PArithARRI64 n d s i => [(#d, Op (Arith (OArithARRI64 n i)) (Name(#d) @ Name (#s) @ Enil))]
   end.
 
 
@@ -711,6 +720,27 @@ Proof.
     * Simpl.
     * intros rr; destruct rr; Simpl.
       destruct (ireg_eq g rd); subst; Simpl.
+(* PArithARRR *)
+  - inv H; inv H0;
+    eexists; split; try split.
+    * simpl. pose (H1 rd); rewrite e. pose (H1 rs1); rewrite e0. pose (H1 rs2); rewrite e1. reflexivity.
+    * Simpl.
+    * intros rr; destruct rr; Simpl.
+      destruct (ireg_eq g rd); subst; Simpl.
+(* PArithARRI32 *)
+  - inv H; inv H0;
+    eexists; split; try split.
+    * simpl. pose (H1 rd); rewrite e. pose (H1 rs0); rewrite e0. reflexivity.
+    * Simpl.
+    * intros rr; destruct rr; Simpl.
+      destruct (ireg_eq g rd); subst; Simpl.
+(* PArithARRI64 *)
+  - inv H; inv H0;
+    eexists; split; try split.
+    * simpl. pose (H1 rd); rewrite e. pose (H1 rs0); rewrite e0. reflexivity.
+    * Simpl.
+    * intros rr; destruct rr; Simpl.
+      destruct (ireg_eq g rd); subst; Simpl.
 Qed.
 
 Lemma forward_simu_basic:
@@ -1367,6 +1397,22 @@ Definition string_of_name_rri64 (n: arith_name_rri64): pstring :=
   | Pornil => "Pornil"
   end.
 
+Definition string_of_name_arrr (n: arith_name_arrr): pstring :=
+  match n with
+  | Pmaddw  => "Pmaddw"
+  | Pmaddl  => "Pmaddl"
+  end.
+
+Definition string_of_name_arri32 (n: arith_name_arri32): pstring :=
+  match n with
+  | Pmaddiw => "Pmaddw"
+  end.
+
+Definition string_of_name_arri64 (n: arith_name_arri64): pstring :=
+  match n with
+  | Pmaddil => "Pmaddl"
+  end.
+
 Definition string_of_arith (op: arith_op): pstring :=
   match op with
   | OArithR n => string_of_name_r n
@@ -1378,6 +1424,9 @@ Definition string_of_arith (op: arith_op): pstring :=
   | OArithRRR n => string_of_name_rrr n
   | OArithRRI32 n _ => string_of_name_rri32 n
   | OArithRRI64 n _ => string_of_name_rri64 n
+  | OArithARRR n => string_of_name_arrr n
+  | OArithARRI32 n _ => string_of_name_arri32 n
+  | OArithARRI64 n _ => string_of_name_arri64 n
   end.
 
 Definition string_of_name_lrro (n: load_name_rro) : pstring :=
-- 
cgit 


From fe4318192bb29fa25dc163004701a45879c41ec0 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 18 Mar 2019 18:57:08 +0100
Subject: maddw exists now in postpass scheduler

---
 mppa_k1c/PostpassSchedulingOracle.ml | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index ce2fb2ae..22833dfd 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -123,6 +123,10 @@ let arith_rri64_str = function
   | Pandnil -> "Pandnil"
   | Pornil -> "Pornil"
 
+let arith_arrr_str = function
+  | Pmaddw -> "Pmaddw"
+  | Pmaddl -> "Pmaddl"
+            
 let arith_ri32_str = "Pmake"
 
 let arith_ri64_str = "Pmakel"
@@ -162,6 +166,12 @@ let arith_rri64_rec i rd rs imm64 = { inst = arith_rri64_str i; write_locs = [Re
 
 let arith_rrr_rec i rd rs1 rs2 = { inst = arith_rrr_str i; write_locs = [Reg rd]; read_locs = [Reg rs1; Reg rs2]; imm = None; is_control = false}
 
+let arith_arri32_rec i rd rs imm32 = { inst = "Pmaddiw"; write_locs = [Reg rd]; read_locs = [Reg rd; Reg rs]; imm = imm32; is_control = false }
+
+let arith_arri64_rec i rd rs imm64 = { inst = "Pmaddil"; write_locs = [Reg rd]; read_locs = [Reg rd; Reg rs]; imm = imm64; is_control = false }
+
+let arith_arrr_rec i rd rs1 rs2 = { inst = arith_arrr_str i; write_locs = [Reg rd]; read_locs = [Reg rd; Reg rs1; Reg rs2]; imm = None; is_control = false}
+
 let arith_rr_rec i rd rs = { inst = arith_rr_str i; write_locs = [Reg rd]; read_locs = [Reg rs]; imm = None; is_control = false}
 
 let arith_r_rec i rd = match i with
@@ -173,6 +183,10 @@ let arith_rec i =
   | PArithRRI32 (i, rd, rs, imm32) -> arith_rri32_rec i (IR rd) (IR rs) (Some (I32 imm32))
   | PArithRRI64 (i, rd, rs, imm64) -> arith_rri64_rec i (IR rd) (IR rs) (Some (I64 imm64))
   | PArithRRR (i, rd, rs1, rs2) -> arith_rrr_rec i (IR rd) (IR rs1) (IR rs2)
+  (* Seems like single constant constructor types are elided *)
+  | PArithARRI32 ((* i,*) rd, rs, imm32) -> arith_arri32_rec () (IR rd) (IR rs) (Some (I32 imm32))
+  | PArithARRI64 ((* i,*) rd, rs, imm64) -> arith_arri64_rec () (IR rd) (IR rs) (Some (I64 imm64))
+  | PArithARRR (i, rd, rs1, rs2) -> arith_arrr_rec i (IR rd) (IR rs1) (IR rs2)
   | PArithRI32 (rd, imm32) -> { inst = arith_ri32_str; write_locs = [Reg (IR rd)]; read_locs = []; imm = (Some (I32 imm32)) ; is_control = false}
   | PArithRI64 (rd, imm64) -> { inst = arith_ri64_str; write_locs = [Reg (IR rd)]; read_locs = []; imm = (Some (I64 imm64)) ; is_control = false}
   | PArithRF32 (rd, f) -> { inst = arith_rf32_str; write_locs = [Reg (IR rd)]; read_locs = [];
-- 
cgit 


From ea12bb63c4ff63c12a383b8b66dff11fc5dc6e65 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 18 Mar 2019 20:50:02 +0100
Subject: plus d'infrastructure pour madd

---
 mppa_k1c/NeedOp.v   |  6 ++++++
 mppa_k1c/Op.v       | 41 +++++++++++++++++++++++++++++++++++++++++
 mppa_k1c/ValueAOp.v |  2 ++
 3 files changed, 49 insertions(+)

diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index 12d7a4f7..801a520e 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -25,6 +25,7 @@ Require Import NeedDomain.
 
 Definition op1 (nv: nval) := nv :: nil.
 Definition op2 (nv: nval) := nv :: nv :: nil.
+Definition op3 (nv: nval) := nv :: nv :: nv :: nil.
 
 Definition needs_of_condition (cond: condition): list nval := nil.
 
@@ -68,6 +69,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Ororimm n => op1 (ror nv n)
   | Oshruimm n => op1 (shruimm nv n)
   | Oshrximm n => op1 (default nv)
+  | Omadd => op3 (modarith nv)
+  | Omaddimm n => op2 (modarith nv)
   | Omakelong => op2 (default nv)
   | Olowlong | Ohighlong => op1 (default nv)
   | Ocast32signed => op1 (default nv)
@@ -189,6 +192,9 @@ Proof.
 - apply shrimm_sound; auto.
 - apply shruimm_sound; auto.
 - apply ror_sound; auto.
+  (* 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.
 Qed.
 
 Lemma operation_is_redundant_sound:
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 04ea8945..c56a9649 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -101,6 +101,8 @@ Inductive operation : Type :=
   | Oshruimm (n: int)        (**r [rd = r1 >> n] (unsigned) *)
   | Oshrximm (n: int)        (**r [rd = r1 / 2^n] (signed) *)
   | Ororimm (n: int)         (**r rotate right immediate *)
+  | Omadd                    (**r [rd = rd + r1 * r2] *)
+  | Omaddimm (n: int)        (**r [rd = rd + r1 * imm] *)
 (*c 64-bit integer arithmetic: *)
   | Omakelong                (**r [rd = r1 << 32 | r2] *)
   | Olowlong                 (**r [rd = low-word(r1)] *)
@@ -142,6 +144,10 @@ Inductive operation : Type :=
   | Oshrlu                   (**r [rd = r1 >> r2] (unsigned) *)
   | Oshrluimm (n: int)       (**r [rd = r1 >> n] (unsigned) *)
   | Oshrxlimm (n: int)       (**r [rd = r1 / 2^n] (signed) *)
+              (* FIXME
+  | Omaddl                   (**r [rd = rd + r1 * r2] *)
+  | Omaddlimm (n: int64)     (**r [rd = rd + r1 * imm] *)
+*)
 (*c Floating-point arithmetic: *)
   | Onegf                    (**r [rd = - r1] *)
   | Oabsf                    (**r [rd = abs(r1)] *)
@@ -293,6 +299,9 @@ Definition eval_operation
   | Oshru, v1 :: v2 :: nil => Some (Val.shru v1 v2)
   | Oshruimm n, v1 :: nil => Some (Val.shru v1 (Vint n))
   | 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)))
+                                     
   | Omakelong, v1::v2::nil => Some (Val.longofwords v1 v2)
   | Olowlong, v1::nil => Some (Val.loword v1)
   | Ohighlong, v1::nil => Some (Val.hiword v1)
@@ -333,6 +342,12 @@ Definition eval_operation
   | Oshrlu, v1::v2::nil => Some (Val.shrlu v1 v2)
   | Oshrluimm n, v1::nil => Some (Val.shrlu v1 (Vint n))
   | 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)))
+                                       *)
+                                      
   | Onegf, v1::nil => Some (Val.negf v1)
   | Oabsf, v1::nil => Some (Val.absf v1)
   | Oaddf, v1::v2::nil => Some (Val.addf v1 v2)
@@ -472,6 +487,9 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Oshruimm _ => (Tint :: nil, Tint)
   | Oshrximm _ => (Tint :: nil, Tint)
   | Ororimm _ => (Tint :: nil, Tint)
+  | Omadd => (Tint :: Tint :: Tint :: nil, Tint)
+  | Omaddimm _ => (Tint :: Tint :: nil, Tint)
+                   
   | Omakelong => (Tint :: Tint :: nil, Tlong)
   | Olowlong => (Tlong :: nil, Tint)
   | Ohighlong => (Tlong :: nil, Tint)
@@ -512,6 +530,10 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Oshrlu => (Tlong :: Tint :: nil, Tlong)
   | Oshrluimm _ => (Tlong :: nil, Tlong)
   | Oshrxlimm _ => (Tlong :: nil, Tlong)
+                     (* FIXME
+  | Omaddl => (Tlong :: Tlong :: Tlong :: nil, Tlong)
+  | Omaddlimm _ => (Tlong :: Tlong :: nil, Tlong)
+*)
   | Onegf => (Tfloat :: nil, Tfloat)
   | Oabsf => (Tfloat :: nil, Tfloat)
   | Oaddf => (Tfloat :: Tfloat :: nil, Tfloat)
@@ -654,6 +676,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - destruct v0; simpl in H0; try discriminate. destruct (Int.ltu n (Int.repr 31)); inv H0...
   (* shrimm *)
   - destruct v0; simpl...   
+  (* madd *)
+  - destruct v0; destruct v1; destruct v2...   
+  - destruct v0; destruct v1...
   (* makelong, lowlong, highlong *)
   - destruct v0; destruct v1...
   - destruct v0...
@@ -720,6 +745,10 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')...
   (* shrxl *)
   - destruct v0; simpl in H0; try discriminate. destruct (Int.ltu n (Int.repr 63)); inv H0...
+    (* FIXME
+  (* maddl, maddlim *)
+  - destruct v0; destruct v1; destruct v2...
+  - destruct v0; destruct v1... *)
   (* negf, absf *)
   - destruct v0...
   - destruct v0...
@@ -1153,6 +1182,9 @@ Proof.
     destruct (Int.ltu n (Int.repr 31)); inv H1. TrivialExists.
   (* rorimm *)
   - inv H4; simpl; auto.
+  (* madd, maddim *)
+  - inv H2; inv H3; inv H4; simpl; auto.
+  - inv H2; inv H4; simpl; auto.
   (* makelong, highlong, lowlong *)
   - inv H4; inv H2; simpl; auto.
   - inv H4; simpl; auto.
@@ -1222,6 +1254,15 @@ Proof.
   (* shrx *)
   - inv H4; simpl in H1; try discriminate. simpl.
     destruct (Int.ltu n (Int.repr 63)); inv H1. TrivialExists.
+
+  (*
+  (* maddl, maddlim *)
+  - inv H2; inv H3; inv H4; simpl; auto; simpl.
+    destruct Archi.ptr64; trivial.
+    s
+  - inv H2; inv H4; simpl; auto.
+   *)
+    
   (* negf, absf *)
   - inv H4; simpl; auto.
   - inv H4; simpl; auto.
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index 57676b35..a92358ca 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -88,6 +88,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Oshru, v1::v2::nil => shru v1 v2
   | Oshruimm n, v1::nil => shru v1 (I n)
   | 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))
   | Omakelong, v1::v2::nil => longofwords v1 v2
   | Olowlong, v1::nil => loword v1
   | Ohighlong, v1::nil => hiword v1
-- 
cgit 


From ddbe4221279f9e75b4ed075156420e62a92f28d9 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 18 Mar 2019 22:08:45 +0100
Subject: maddw dans la génération
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 mppa_k1c/Asmblock.v    | 3 +++
 mppa_k1c/Asmblockgen.v | 7 ++++++-
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 9b51ea33..b3e1532d 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -443,6 +443,9 @@ Coercion PArithRF64:    arith_name_rf64     >-> Funclass.
 Coercion PArithRRR:     arith_name_rrr      >-> Funclass.
 Coercion PArithRRI32:   arith_name_rri32    >-> Funclass.
 Coercion PArithRRI64:   arith_name_rri64    >-> Funclass.
+Coercion PArithARRR:     arith_name_arrr      >-> Funclass.
+Coercion PArithARRI32:   arith_name_arri32    >-> Funclass.
+Coercion PArithARRI64:   arith_name_arri64    >-> Funclass.
 
 Inductive basic : Type :=
   | PArith          (i: ar_instruction)
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 87df237c..1646ff94 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -513,7 +513,12 @@ Definition transl_op
   | Ororimm n, a1 :: nil =>
     do rd <- ireg_of res; do rs <- ireg_of a1;
       OK (Proriw rd rs n ::i k)
-         
+  | Omadd, 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 (Pmaddw r1 r2 r3 ::i k)
   (* [Omakelong], [Ohighlong]  should not occur *)
   | Olowlong, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
-- 
cgit 


From a34c36161ac7bd43e128a39aaf52c15c5f923400 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 18 Mar 2019 23:25:04 +0100
Subject: mandw mais ça coince
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 mppa_k1c/PostpassSchedulingOracle.ml | 11 ++++++++---
 mppa_k1c/SelectOp.vp                 |  2 ++
 mppa_k1c/SelectOpproof.v             |  2 ++
 3 files changed, 12 insertions(+), 3 deletions(-)

diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 22833dfd..b02bc6ca 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -413,6 +413,7 @@ type real_instruction =
   | Addw | Andw | Compw | Mulw | Orw | Sbfw | Sraw | Srlw | Sllw | Rorw | Xorw
   | Addd | Andd | Compd | Muld | Ord | Sbfd | Srad | Srld | Slld | Xord
   | Nandw | Norw | Nxorw | Nandd | Nord | Nxord | Andnw | Ornw | Andnd | Ornd
+  | Maddw | Maddd
   | Make | Nop  | Sxwd  | Zxwd
   (* LSU *)
   | Lbs | Lbz | Lhs | Lhz | Lws | Ld
@@ -450,6 +451,7 @@ let ab_inst_to_real = function
   | "Psrll" | "Psrlil" -> Srld
   | "Psllw" | "Pslliw" -> Sllw
   | "Proriw" -> Rorw
+  | "Pmaddw" -> Maddw
   | "Pslll" | "Psllil" -> Slld
   | "Pxorw" | "Pxoriw" -> Xorw
   | "Pnxorw" | "Pnxoriw" -> Nxorw
@@ -459,6 +461,7 @@ let ab_inst_to_real = function
   | "Pnxorl" | "Pnxoril" -> Nxord
   | "Pandnl" | "Pandnil" -> Andnd
   | "Pornl" | "Pornil" -> Ornd
+  | "Pmaddl" -> Maddd
   | "Pmake" | "Pmakel" | "Pmakefs" | "Pmakef" | "Ploadsymbol" -> Make
   | "Pnop" | "Pcvtw2l" -> Nop
   | "Psxwd" -> Sxwd
@@ -520,11 +523,13 @@ let rec_to_usage r =
                                   (* I do not know yet in which context Ofslow can be used by CompCert *)
   and real_inst = ab_inst_to_real r.inst
   in match real_inst with
-  | Addw | Andw | Nandw | Orw | Norw | Sbfw | Xorw | Nxorw | Andnw | Ornw -> 
+  | Addw | Andw | Nandw | Orw | Norw | Sbfw | Xorw
+  | Nxorw | Andnw | Ornw | Maddw -> 
       (match encoding with None | Some U6 | Some S10 -> alu_tiny 
                           | Some U27L5 | Some U27L10 -> alu_tiny_x
                           | _ -> raise InvalidEncoding)
-  | Addd | Andd | Nandd | Ord | Nord | Sbfd | Xord | Nxord | Andnd | Ornd -> 
+  | Addd | Andd | Nandd | Ord | Nord | Sbfd | Xord
+  | Nxord | Andnd | Ornd | Maddd -> 
       (match encoding with None | Some U6 | Some S10 -> alu_tiny 
                           | Some U27L5 | Some U27L10 -> alu_tiny_x
                           | Some E27U27L10 -> alu_tiny_y)
@@ -580,7 +585,7 @@ let real_inst_to_latency = function
   | Sxwd | Zxwd | Fcompw | Fcompd
         -> 1
   | Floatwz | Floatuwz | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4
-  | Mulw | Muld -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *)
+  | Mulw | Muld | Maddw | Maddd -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *)
   | Lbs | Lbz | Lhs | Lhz | Lws | Ld -> 3
   | Sb | Sh | Sw | Sd -> 1 (* See k1c-Optimization.pdf page 19 *)
   | Get -> 1
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 7ec694e2..e34e7c32 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -86,6 +86,8 @@ Nondetfunction add (e1: expr) (e2: expr) :=
       addimm n1 (Eop Oadd (t1:::t2:::Enil))
   | t1, Eop (Oaddimm n2) (t2:::Enil) =>
       addimm n2 (Eop Oadd (t1:::t2:::Enil))
+  | t1, (Eop Omul (t2:::t3:::Enil)) =>
+      Eop Omadd (t1:::t2:::t3:::Enil)
   | _, _ => Eop Oadd (e1:::e2:::Enil)
   end.
 
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index 57cd3d58..d7ae92dc 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -182,6 +182,8 @@ Proof.
        with (Val.add (Val.add x v1) (Vint n2)).
     apply eval_addimm. EvalOp.
     repeat rewrite Val.add_assoc. reflexivity.
+  - (* Omadd *)
+    subst. TrivialExists.
   - TrivialExists.
 Qed.
 
-- 
cgit 


From fdb8d0c7b5a8be87a64cb995f3abf5bc60f07bfd Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 19 Mar 2019 07:07:46 +0100
Subject: implemented -fno-postpass normally

---
 mppa_k1c/Asmgen.v      |  5 ++++-
 mppa_k1c/Asmgenproof.v | 52 +++++++++++++++++++++++++++++++++-----------------
 mppa_k1c/SelectOp.v    |  6 ++++++
 3 files changed, 45 insertions(+), 18 deletions(-)

diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index 58e80be1..46714496 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -19,13 +19,16 @@ Require Import Integers.
 Require Import Mach Asm Asmblock Asmblockgen Machblockgen.
 Require Import PostpassScheduling.
 Require Import Errors.
+Require Import Compopts.
 
 Local Open Scope error_monad_scope.
 
 Definition transf_program (p: Mach.program) : res Asm.program :=
   let mbp := Machblockgen.transf_program p in
   do abp <- Asmblockgen.transf_program mbp;
-  do abp' <- PostpassScheduling.transf_program abp;
+    do abp' <- if Compopts.optim_postpass tt
+               then PostpassScheduling.transf_program abp
+               else OK abp;
   OK (Asm.transf_program abp').
 
 Definition transf_function (f: Mach.function) : res Asm.function :=
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index 588019a2..918403cd 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -17,15 +17,18 @@ Require Import Integers Floats AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Op Locations Mach Conventions Asm Asmgen Machblockgen Asmblockgen.
 Require Import Machblockgenproof Asmblockgenproof PostpassSchedulingproof.
+Require Import Compopts.
 
 Local Open Scope linking_scope.
 
 Definition block_passes :=
       mkpass Machblockgenproof.match_prog
   ::: mkpass Asmblockgenproof.match_prog
-  ::: mkpass PostpassSchedulingproof.match_prog
-  ::: mkpass Asm.match_prog
-  ::: pass_nil _.
+  ::: if Compopts.optim_postpass tt
+      then mkpass PostpassSchedulingproof.match_prog
+           ::: mkpass Asm.match_prog
+           ::: pass_nil _
+      else mkpass Asm.match_prog ::: pass_nil _.
 
 Definition match_prog := pass_match (compose_passes block_passes).
 
@@ -36,11 +39,16 @@ Proof.
   unfold Asmgen.transf_program in H. apply bind_inversion in H. destruct H.
   inversion_clear H. apply bind_inversion in H1. destruct H1.
   inversion_clear H. inversion H2. remember (Machblockgen.transf_program p) as mbp.
-  unfold match_prog; simpl.
-  exists mbp; split. apply Machblockgenproof.transf_program_match; auto.
-  exists x; split. apply Asmblockgenproof.transf_program_match; auto.
-  exists x0; split. apply PostpassSchedulingproof.transf_program_match; auto.
-  exists tp; split. apply Asm.transf_program_match; auto. auto.
+  unfold match_prog. simpl.
+  destruct (optim_postpass tt); simpl.
+  - exists mbp; split. apply Machblockgenproof.transf_program_match; auto.
+    exists x; split. apply Asmblockgenproof.transf_program_match; auto.
+    exists x0; split. apply PostpassSchedulingproof.transf_program_match; auto.
+    exists tp; split. apply Asm.transf_program_match; auto. auto.
+  - exists mbp; split. apply Machblockgenproof.transf_program_match; auto.
+    exists x0; split. apply Asmblockgenproof.transf_program_match; auto.
+    congruence.
+    exists tp; split. apply Asm.transf_program_match; auto. auto.
 Qed.
 
 (** Return Address Offset *)
@@ -149,15 +157,25 @@ Let tge := Genv.globalenv tprog.
 Theorem transf_program_correct:
   forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog).
 Proof.
-  unfold match_prog in TRANSF. simpl in TRANSF.
-  inv TRANSF. inv H. inv H1. inv H. inv H2. inv H. inv H3. inv H.
-  eapply compose_forward_simulations. 
-  exploit Machblockgenproof.transf_program_correct; eauto.
-  unfold Machblockgenproof.inv_trans_rao. 
-  intros X; apply X.
-  eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto.
-  eapply compose_forward_simulations. apply PostpassSchedulingproof.transf_program_correct; eauto.
-  apply Asm.transf_program_correct. eauto.
+  unfold match_prog in TRANSF.
+  simpl in TRANSF.
+  inv TRANSF.
+  destruct (optim_postpass tt) in *.
+  - inv H. inv H1. inv H. inv H2. inv H. inv H3. inv H. inv H4.
+    eapply compose_forward_simulations. 
+    exploit Machblockgenproof.transf_program_correct; eauto.
+    unfold Machblockgenproof.inv_trans_rao. 
+    intros X; apply X.
+    eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto.
+    eapply compose_forward_simulations. apply PostpassSchedulingproof.transf_program_correct; eauto.
+    apply Asm.transf_program_correct; eauto.
+  - inv H. inv H1. inv H. inv H2. inv H. inv H3.
+    eapply compose_forward_simulations. 
+    exploit Machblockgenproof.transf_program_correct; eauto.
+    unfold Machblockgenproof.inv_trans_rao. 
+    intros X; apply X.
+    eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto.
+    apply Asm.transf_program_correct ; eauto.
 Qed.
 
 End PRESERVATION.
diff --git a/mppa_k1c/SelectOp.v b/mppa_k1c/SelectOp.v
index edb07e5f..66615f1d 100644
--- a/mppa_k1c/SelectOp.v
+++ b/mppa_k1c/SelectOp.v
@@ -123,6 +123,8 @@ Nondetfunction add (e1: expr) (e2: expr) :=
       addimm n1 (Eop Oadd (t1:::t2:::Enil))
   | t1, Eop (Oaddimm n2) (t2:::Enil) =>
       addimm n2 (Eop Oadd (t1:::t2:::Enil))
+  | t1, (Eop Omul (t2:::t3:::Enil)) =>
+      Eop Omadd (t1:::t2:::t3:::Enil)
   | _, _ => Eop Oadd (e1:::e2:::Enil)
   end.
 >>
@@ -136,6 +138,7 @@ Inductive add_cases: forall (e1: expr) (e2: expr), Type :=
   | add_case5: forall n1 n2 t2, add_cases (Eop (Oaddrstack n1) Enil) (Eop (Oaddimm n2) (t2:::Enil))
   | add_case6: forall n1 t1 t2, add_cases (Eop (Oaddimm n1) (t1:::Enil)) (t2)
   | add_case7: forall t1 n2 t2, add_cases (t1) (Eop (Oaddimm n2) (t2:::Enil))
+  | add_case8: forall t1 t2 t3, add_cases (t1) ((Eop Omul (t2:::t3:::Enil)))
   | add_default: forall (e1: expr) (e2: expr), add_cases e1 e2.
 
 Definition add_match (e1: expr) (e2: expr) :=
@@ -147,6 +150,7 @@ Definition add_match (e1: expr) (e2: expr) :=
   | Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) => add_case5 n1 n2 t2
   | Eop (Oaddimm n1) (t1:::Enil), t2 => add_case6 n1 t1 t2
   | t1, Eop (Oaddimm n2) (t2:::Enil) => add_case7 t1 n2 t2
+  | t1, (Eop Omul (t2:::t3:::Enil)) => add_case8 t1 t2 t3
   | e1, e2 => add_default e1 e2
   end.
 
@@ -166,6 +170,8 @@ Definition add (e1: expr) (e2: expr) :=
       addimm n1 (Eop Oadd (t1:::t2:::Enil))
   | add_case7 t1 n2 t2 => (* t1, Eop (Oaddimm n2) (t2:::Enil) *) 
       addimm n2 (Eop Oadd (t1:::t2:::Enil))
+  | add_case8 t1 t2 t3 => (* t1, (Eop Omul (t2:::t3:::Enil)) *) 
+      Eop Omadd (t1:::t2:::t3:::Enil)
   | add_default e1 e2 =>
       Eop Oadd (e1:::e2:::Enil)
   end.
-- 
cgit 


From bcfcbcb78d5aae904cac23d3e0a055c4d8cc8509 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 19 Mar 2019 07:23:15 +0100
Subject: test for madd

---
 test/monniaux/madd/madd_run.c | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 test/monniaux/madd/madd_run.c

diff --git a/test/monniaux/madd/madd_run.c b/test/monniaux/madd/madd_run.c
new file mode 100644
index 00000000..d4238c53
--- /dev/null
+++ b/test/monniaux/madd/madd_run.c
@@ -0,0 +1,9 @@
+#include <stdio.h>
+
+extern unsigned madd(unsigned a, unsigned b, unsigned c);
+
+int main() {
+  unsigned a = 7, b = 3, c = 4;
+  printf("res = %u\n", madd(a, b, c));
+  return 0;
+}
-- 
cgit 


From 6d2c27127fd67b6ad5499c7d3f4be537333ac356 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 19 Mar 2019 13:31:57 +0100
Subject: Revert "implemented -fno-postpass normally"

This reverts commit fdb8d0c7b5a8be87a64cb995f3abf5bc60f07bfd.
---
 mppa_k1c/Asmgen.v      |  5 +----
 mppa_k1c/Asmgenproof.v | 52 +++++++++++++++++---------------------------------
 mppa_k1c/SelectOp.v    |  6 ------
 3 files changed, 18 insertions(+), 45 deletions(-)

diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index 46714496..58e80be1 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -19,16 +19,13 @@ Require Import Integers.
 Require Import Mach Asm Asmblock Asmblockgen Machblockgen.
 Require Import PostpassScheduling.
 Require Import Errors.
-Require Import Compopts.
 
 Local Open Scope error_monad_scope.
 
 Definition transf_program (p: Mach.program) : res Asm.program :=
   let mbp := Machblockgen.transf_program p in
   do abp <- Asmblockgen.transf_program mbp;
-    do abp' <- if Compopts.optim_postpass tt
-               then PostpassScheduling.transf_program abp
-               else OK abp;
+  do abp' <- PostpassScheduling.transf_program abp;
   OK (Asm.transf_program abp').
 
 Definition transf_function (f: Mach.function) : res Asm.function :=
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index 918403cd..588019a2 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -17,18 +17,15 @@ Require Import Integers Floats AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Op Locations Mach Conventions Asm Asmgen Machblockgen Asmblockgen.
 Require Import Machblockgenproof Asmblockgenproof PostpassSchedulingproof.
-Require Import Compopts.
 
 Local Open Scope linking_scope.
 
 Definition block_passes :=
       mkpass Machblockgenproof.match_prog
   ::: mkpass Asmblockgenproof.match_prog
-  ::: if Compopts.optim_postpass tt
-      then mkpass PostpassSchedulingproof.match_prog
-           ::: mkpass Asm.match_prog
-           ::: pass_nil _
-      else mkpass Asm.match_prog ::: pass_nil _.
+  ::: mkpass PostpassSchedulingproof.match_prog
+  ::: mkpass Asm.match_prog
+  ::: pass_nil _.
 
 Definition match_prog := pass_match (compose_passes block_passes).
 
@@ -39,16 +36,11 @@ Proof.
   unfold Asmgen.transf_program in H. apply bind_inversion in H. destruct H.
   inversion_clear H. apply bind_inversion in H1. destruct H1.
   inversion_clear H. inversion H2. remember (Machblockgen.transf_program p) as mbp.
-  unfold match_prog. simpl.
-  destruct (optim_postpass tt); simpl.
-  - exists mbp; split. apply Machblockgenproof.transf_program_match; auto.
-    exists x; split. apply Asmblockgenproof.transf_program_match; auto.
-    exists x0; split. apply PostpassSchedulingproof.transf_program_match; auto.
-    exists tp; split. apply Asm.transf_program_match; auto. auto.
-  - exists mbp; split. apply Machblockgenproof.transf_program_match; auto.
-    exists x0; split. apply Asmblockgenproof.transf_program_match; auto.
-    congruence.
-    exists tp; split. apply Asm.transf_program_match; auto. auto.
+  unfold match_prog; simpl.
+  exists mbp; split. apply Machblockgenproof.transf_program_match; auto.
+  exists x; split. apply Asmblockgenproof.transf_program_match; auto.
+  exists x0; split. apply PostpassSchedulingproof.transf_program_match; auto.
+  exists tp; split. apply Asm.transf_program_match; auto. auto.
 Qed.
 
 (** Return Address Offset *)
@@ -157,25 +149,15 @@ Let tge := Genv.globalenv tprog.
 Theorem transf_program_correct:
   forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog).
 Proof.
-  unfold match_prog in TRANSF.
-  simpl in TRANSF.
-  inv TRANSF.
-  destruct (optim_postpass tt) in *.
-  - inv H. inv H1. inv H. inv H2. inv H. inv H3. inv H. inv H4.
-    eapply compose_forward_simulations. 
-    exploit Machblockgenproof.transf_program_correct; eauto.
-    unfold Machblockgenproof.inv_trans_rao. 
-    intros X; apply X.
-    eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto.
-    eapply compose_forward_simulations. apply PostpassSchedulingproof.transf_program_correct; eauto.
-    apply Asm.transf_program_correct; eauto.
-  - inv H. inv H1. inv H. inv H2. inv H. inv H3.
-    eapply compose_forward_simulations. 
-    exploit Machblockgenproof.transf_program_correct; eauto.
-    unfold Machblockgenproof.inv_trans_rao. 
-    intros X; apply X.
-    eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto.
-    apply Asm.transf_program_correct ; eauto.
+  unfold match_prog in TRANSF. simpl in TRANSF.
+  inv TRANSF. inv H. inv H1. inv H. inv H2. inv H. inv H3. inv H.
+  eapply compose_forward_simulations. 
+  exploit Machblockgenproof.transf_program_correct; eauto.
+  unfold Machblockgenproof.inv_trans_rao. 
+  intros X; apply X.
+  eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto.
+  eapply compose_forward_simulations. apply PostpassSchedulingproof.transf_program_correct; eauto.
+  apply Asm.transf_program_correct. eauto.
 Qed.
 
 End PRESERVATION.
diff --git a/mppa_k1c/SelectOp.v b/mppa_k1c/SelectOp.v
index 66615f1d..edb07e5f 100644
--- a/mppa_k1c/SelectOp.v
+++ b/mppa_k1c/SelectOp.v
@@ -123,8 +123,6 @@ Nondetfunction add (e1: expr) (e2: expr) :=
       addimm n1 (Eop Oadd (t1:::t2:::Enil))
   | t1, Eop (Oaddimm n2) (t2:::Enil) =>
       addimm n2 (Eop Oadd (t1:::t2:::Enil))
-  | t1, (Eop Omul (t2:::t3:::Enil)) =>
-      Eop Omadd (t1:::t2:::t3:::Enil)
   | _, _ => Eop Oadd (e1:::e2:::Enil)
   end.
 >>
@@ -138,7 +136,6 @@ Inductive add_cases: forall (e1: expr) (e2: expr), Type :=
   | add_case5: forall n1 n2 t2, add_cases (Eop (Oaddrstack n1) Enil) (Eop (Oaddimm n2) (t2:::Enil))
   | add_case6: forall n1 t1 t2, add_cases (Eop (Oaddimm n1) (t1:::Enil)) (t2)
   | add_case7: forall t1 n2 t2, add_cases (t1) (Eop (Oaddimm n2) (t2:::Enil))
-  | add_case8: forall t1 t2 t3, add_cases (t1) ((Eop Omul (t2:::t3:::Enil)))
   | add_default: forall (e1: expr) (e2: expr), add_cases e1 e2.
 
 Definition add_match (e1: expr) (e2: expr) :=
@@ -150,7 +147,6 @@ Definition add_match (e1: expr) (e2: expr) :=
   | Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) => add_case5 n1 n2 t2
   | Eop (Oaddimm n1) (t1:::Enil), t2 => add_case6 n1 t1 t2
   | t1, Eop (Oaddimm n2) (t2:::Enil) => add_case7 t1 n2 t2
-  | t1, (Eop Omul (t2:::t3:::Enil)) => add_case8 t1 t2 t3
   | e1, e2 => add_default e1 e2
   end.
 
@@ -170,8 +166,6 @@ Definition add (e1: expr) (e2: expr) :=
       addimm n1 (Eop Oadd (t1:::t2:::Enil))
   | add_case7 t1 n2 t2 => (* t1, Eop (Oaddimm n2) (t2:::Enil) *) 
       addimm n2 (Eop Oadd (t1:::t2:::Enil))
-  | add_case8 t1 t2 t3 => (* t1, (Eop Omul (t2:::t3:::Enil)) *) 
-      Eop Omadd (t1:::t2:::t3:::Enil)
   | add_default e1 e2 =>
       Eop Oadd (e1:::e2:::Enil)
   end.
-- 
cgit 


From 08136431cae04e29491c22be1a45c3b7171c232b Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 19 Mar 2019 14:14:49 +0100
Subject: specify instructions that write to first operand (madd)

---
 mppa_k1c/Machregs.v |    2 +-
 mppa_k1c/SelectOp.v | 1323 ---------------------------------------------------
 2 files changed, 1 insertion(+), 1324 deletions(-)
 delete mode 100644 mppa_k1c/SelectOp.v

diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v
index 1c1930da..9f0f6a4d 100644
--- a/mppa_k1c/Machregs.v
+++ b/mppa_k1c/Machregs.v
@@ -210,7 +210,7 @@ Global Opaque
 
 Definition two_address_op (op: operation) : bool :=
   match op with
-  | Ocast32unsigned => true
+  | Ocast32unsigned | Omadd | Omaddimm _ => true
   | _ => false
   end.
 
diff --git a/mppa_k1c/SelectOp.v b/mppa_k1c/SelectOp.v
deleted file mode 100644
index edb07e5f..00000000
--- a/mppa_k1c/SelectOp.v
+++ /dev/null
@@ -1,1323 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*           Prashanth Mundkur, SRI International                      *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(*  The contributions by Prashanth Mundkur are reused and adapted      *)
-(*  under the terms of a Contributor License Agreement between         *)
-(*  SRI International and INRIA.                                       *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Instruction selection for operators *)
-
-(** The instruction selection pass recognizes opportunities for using
-  combined arithmetic and logical operations and addressing modes
-  offered by the target processor.  For instance, the expression [x + 1]
-  can take advantage of the "immediate add" instruction of the processor,
-  and on the PowerPC, the expression [(x >> 6) & 0xFF] can be turned
-  into a "rotate and mask" instruction.
-
-  This file defines functions for building CminorSel expressions and
-  statements, especially expressions consisting of operator
-  applications.  These functions examine their arguments to choose
-  cheaper forms of operators whenever possible.
-
-  For instance, [add e1 e2] will return a CminorSel expression semantically
-  equivalent to [Eop Oadd (e1 ::: e2 ::: Enil)], but will use a
-  [Oaddimm] operator if one of the arguments is an integer constant,
-  or suppress the addition altogether if one of the arguments is the
-  null integer.  In passing, we perform operator reassociation
-  ([(e + c1) * c2] becomes [(e * c2) + (c1 * c2)]) and a small amount
-  of constant propagation.
-
-  On top of the "smart constructor" functions defined below,
-  module [Selection] implements the actual instruction selection pass.
-*)
-
-Require Archi.
-Require Import Coqlib.
-Require Import Compopts.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Op.
-Require Import CminorSel.
-
-Local Open Scope cminorsel_scope.
-
-(** ** Constants **)
-
-Definition addrsymbol (id: ident) (ofs: ptrofs) :=
-  Eop (Oaddrsymbol id ofs) Enil.
-
-Definition addrstack (ofs: ptrofs) :=
-  Eop (Oaddrstack ofs) Enil.
-
-(** ** Integer addition and pointer addition *)
-
-(** Original definition:
-<<
-Nondetfunction addimm (n: int) (e: expr) :=
-  if Int.eq n Int.zero then e else
-  match e with
-  | Eop (Ointconst m) Enil => Eop (Ointconst (Int.add n m)) Enil
-  | 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 (Oaddimm n) (e ::: Enil)
-  end.
->>
-*)
-
-Inductive addimm_cases: forall (e: expr), Type :=
-  | addimm_case1: forall m, addimm_cases (Eop (Ointconst m) Enil)
-  | addimm_case2: forall s m, addimm_cases (Eop (Oaddrsymbol s m) Enil)
-  | addimm_case3: forall m, addimm_cases (Eop (Oaddrstack m) Enil)
-  | addimm_case4: forall m t, addimm_cases (Eop (Oaddimm m) (t ::: Enil))
-  | addimm_default: forall (e: expr), addimm_cases e.
-
-Definition addimm_match (e: expr) :=
-  match e as zz1 return addimm_cases zz1 with
-  | Eop (Ointconst m) Enil => addimm_case1 m
-  | Eop (Oaddrsymbol s m) Enil => addimm_case2 s m
-  | Eop (Oaddrstack m) Enil => addimm_case3 m
-  | Eop (Oaddimm m) (t ::: Enil) => addimm_case4 m t
-  | e => addimm_default e
-  end.
-
-Definition addimm (n: int) (e: expr) :=
- if Int.eq n Int.zero then e else match addimm_match e with
-  | addimm_case1 m => (* Eop (Ointconst m) Enil *) 
-      Eop (Ointconst (Int.add n m)) Enil
-  | addimm_case2 s m => (* Eop (Oaddrsymbol s m) Enil *) 
-      Eop (Oaddrsymbol s (Ptrofs.add (Ptrofs.of_int n) m)) Enil
-  | addimm_case3 m => (* Eop (Oaddrstack m) Enil *) 
-      Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n) m)) Enil
-  | addimm_case4 m t => (* Eop (Oaddimm m) (t ::: Enil) *) 
-      Eop (Oaddimm(Int.add n m)) (t ::: Enil)
-  | addimm_default e =>
-      Eop (Oaddimm n) (e ::: Enil)
-  end.
-
-
-(** Original definition:
-<<
-Nondetfunction add (e1: expr) (e2: expr) :=
-  match e1, e2 with
-  | Eop (Ointconst n1) Enil, t2 => addimm n1 t2
-  | t1, Eop (Ointconst n2) Enil => addimm n2 t1
-  | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) =>
-      addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil))
-  | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddrstack n2) Enil =>
-      Eop Oadd (Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n1) n2)) Enil ::: t1 ::: Enil)
-  | Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) =>
-      Eop Oadd (Eop (Oaddrstack (Ptrofs.add n1 (Ptrofs.of_int n2))) Enil ::: t2 ::: Enil)
-  | Eop (Oaddimm n1) (t1:::Enil), t2 =>
-      addimm n1 (Eop Oadd (t1:::t2:::Enil))
-  | t1, Eop (Oaddimm n2) (t2:::Enil) =>
-      addimm n2 (Eop Oadd (t1:::t2:::Enil))
-  | _, _ => Eop Oadd (e1:::e2:::Enil)
-  end.
->>
-*)
-
-Inductive add_cases: forall (e1: expr) (e2: expr), Type :=
-  | add_case1: forall n1 t2, add_cases (Eop (Ointconst n1) Enil) (t2)
-  | add_case2: forall t1 n2, add_cases (t1) (Eop (Ointconst n2) Enil)
-  | add_case3: forall n1 t1 n2 t2, add_cases (Eop (Oaddimm n1) (t1:::Enil)) (Eop (Oaddimm n2) (t2:::Enil))
-  | add_case4: forall n1 t1 n2, add_cases (Eop (Oaddimm n1) (t1:::Enil)) (Eop (Oaddrstack n2) Enil)
-  | add_case5: forall n1 n2 t2, add_cases (Eop (Oaddrstack n1) Enil) (Eop (Oaddimm n2) (t2:::Enil))
-  | add_case6: forall n1 t1 t2, add_cases (Eop (Oaddimm n1) (t1:::Enil)) (t2)
-  | add_case7: forall t1 n2 t2, add_cases (t1) (Eop (Oaddimm n2) (t2:::Enil))
-  | add_default: forall (e1: expr) (e2: expr), add_cases e1 e2.
-
-Definition add_match (e1: expr) (e2: expr) :=
-  match e1 as zz1, e2 as zz2 return add_cases zz1 zz2 with
-  | Eop (Ointconst n1) Enil, t2 => add_case1 n1 t2
-  | t1, Eop (Ointconst n2) Enil => add_case2 t1 n2
-  | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => add_case3 n1 t1 n2 t2
-  | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddrstack n2) Enil => add_case4 n1 t1 n2
-  | Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) => add_case5 n1 n2 t2
-  | Eop (Oaddimm n1) (t1:::Enil), t2 => add_case6 n1 t1 t2
-  | t1, Eop (Oaddimm n2) (t2:::Enil) => add_case7 t1 n2 t2
-  | e1, e2 => add_default e1 e2
-  end.
-
-Definition add (e1: expr) (e2: expr) :=
-  match add_match e1 e2 with
-  | add_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) 
-      addimm n1 t2
-  | add_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) 
-      addimm n2 t1
-  | add_case3 n1 t1 n2 t2 => (* Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) *) 
-      addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil))
-  | add_case4 n1 t1 n2 => (* Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddrstack n2) Enil *) 
-      Eop Oadd (Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n1) n2)) Enil ::: t1 ::: Enil)
-  | add_case5 n1 n2 t2 => (* Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) *) 
-      Eop Oadd (Eop (Oaddrstack (Ptrofs.add n1 (Ptrofs.of_int n2))) Enil ::: t2 ::: Enil)
-  | add_case6 n1 t1 t2 => (* Eop (Oaddimm n1) (t1:::Enil), t2 *) 
-      addimm n1 (Eop Oadd (t1:::t2:::Enil))
-  | add_case7 t1 n2 t2 => (* t1, Eop (Oaddimm n2) (t2:::Enil) *) 
-      addimm n2 (Eop Oadd (t1:::t2:::Enil))
-  | add_default e1 e2 =>
-      Eop Oadd (e1:::e2:::Enil)
-  end.
-
-
-(** ** Integer and pointer subtraction *)
-
-(** Original definition:
-<<
-Nondetfunction sub (e1: expr) (e2: expr) :=
-  match e1, e2 with
-  | t1, Eop (Ointconst n2) Enil =>
-      addimm (Int.neg n2) t1
-  | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) =>
-      addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil))
-  | Eop (Oaddimm n1) (t1:::Enil), t2 =>
-      addimm n1 (Eop Osub (t1:::t2:::Enil))
-  | t1, Eop (Oaddimm n2) (t2:::Enil) =>
-      addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil))
-  | _, _ => Eop Osub (e1:::e2:::Enil)
-  end.
->>
-*)
-
-Inductive sub_cases: forall (e1: expr) (e2: expr), Type :=
-  | sub_case1: forall t1 n2, sub_cases (t1) (Eop (Ointconst n2) Enil)
-  | sub_case2: forall n1 t1 n2 t2, sub_cases (Eop (Oaddimm n1) (t1:::Enil)) (Eop (Oaddimm n2) (t2:::Enil))
-  | sub_case3: forall n1 t1 t2, sub_cases (Eop (Oaddimm n1) (t1:::Enil)) (t2)
-  | sub_case4: forall t1 n2 t2, sub_cases (t1) (Eop (Oaddimm n2) (t2:::Enil))
-  | sub_default: forall (e1: expr) (e2: expr), sub_cases e1 e2.
-
-Definition sub_match (e1: expr) (e2: expr) :=
-  match e1 as zz1, e2 as zz2 return sub_cases zz1 zz2 with
-  | t1, Eop (Ointconst n2) Enil => sub_case1 t1 n2
-  | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => sub_case2 n1 t1 n2 t2
-  | Eop (Oaddimm n1) (t1:::Enil), t2 => sub_case3 n1 t1 t2
-  | t1, Eop (Oaddimm n2) (t2:::Enil) => sub_case4 t1 n2 t2
-  | e1, e2 => sub_default e1 e2
-  end.
-
-Definition sub (e1: expr) (e2: expr) :=
-  match sub_match e1 e2 with
-  | sub_case1 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) 
-      addimm (Int.neg n2) t1
-  | sub_case2 n1 t1 n2 t2 => (* Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) *) 
-      addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil))
-  | sub_case3 n1 t1 t2 => (* Eop (Oaddimm n1) (t1:::Enil), t2 *) 
-      addimm n1 (Eop Osub (t1:::t2:::Enil))
-  | sub_case4 t1 n2 t2 => (* t1, Eop (Oaddimm n2) (t2:::Enil) *) 
-      addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil))
-  | sub_default e1 e2 =>
-      Eop Osub (e1:::e2:::Enil)
-  end.
-
-
-(** Original definition:
-<<
-Nondetfunction negint (e: expr) :=
-  match e with
-  | Eop (Ointconst n) Enil => Eop (Ointconst (Int.neg n)) Enil
-  | _ => Eop Oneg (e ::: Enil)
-  end.
->>
-*)
-
-Inductive negint_cases: forall (e: expr), Type :=
-  | negint_case1: forall n, negint_cases (Eop (Ointconst n) Enil)
-  | negint_default: forall (e: expr), negint_cases e.
-
-Definition negint_match (e: expr) :=
-  match e as zz1 return negint_cases zz1 with
-  | Eop (Ointconst n) Enil => negint_case1 n
-  | e => negint_default e
-  end.
-
-Definition negint (e: expr) :=
-  match negint_match e with
-  | negint_case1 n => (* Eop (Ointconst n) Enil *) 
-      Eop (Ointconst (Int.neg n)) Enil
-  | negint_default e =>
-      Eop Oneg (e ::: Enil)
-  end.
-
-
-(** ** Immediate shifts *)
-
-(** Original definition:
-<<
-Nondetfunction shlimm (e1: expr) (n: int) :=
-  if Int.eq n Int.zero then
-    e1
-  else if negb (Int.ltu n Int.iwordsize) then
-    Eop Oshl (e1 ::: Eop (Ointconst n) Enil ::: Enil)
-  else match e1 with
-    | Eop (Ointconst n1) Enil =>
-        Eop (Ointconst (Int.shl n1 n)) Enil
-    | Eop (Oshlimm n1) (t1:::Enil) =>
-        if Int.ltu (Int.add n n1) Int.iwordsize
-        then Eop (Oshlimm (Int.add n n1)) (t1:::Enil)
-        else Eop (Oshlimm n) (e1:::Enil)
-    | _ =>
-        Eop (Oshlimm n) (e1:::Enil)
-  end.
->>
-*)
-
-Inductive shlimm_cases: forall (e1: expr) , Type :=
-  | shlimm_case1: forall n1, shlimm_cases (Eop (Ointconst n1) Enil)
-  | shlimm_case2: forall n1 t1, shlimm_cases (Eop (Oshlimm n1) (t1:::Enil))
-  | shlimm_default: forall (e1: expr) , shlimm_cases e1.
-
-Definition shlimm_match (e1: expr)  :=
-  match e1 as zz1 return shlimm_cases zz1 with
-  | Eop (Ointconst n1) Enil => shlimm_case1 n1
-  | Eop (Oshlimm n1) (t1:::Enil) => shlimm_case2 n1 t1
-  | e1 => shlimm_default e1
-  end.
-
-Definition shlimm (e1: expr) (n: int) :=
- if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int.iwordsize) then Eop Oshl (e1 ::: Eop (Ointconst n) Enil ::: Enil) else match shlimm_match e1 with
-  | shlimm_case1 n1 => (* Eop (Ointconst n1) Enil *) 
-      Eop (Ointconst (Int.shl n1 n)) Enil
-  | shlimm_case2 n1 t1 => (* Eop (Oshlimm n1) (t1:::Enil) *) 
-      if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshlimm (Int.add n n1)) (t1:::Enil) else Eop (Oshlimm n) (e1:::Enil)
-  | shlimm_default e1 =>
-      Eop (Oshlimm n) (e1:::Enil)
-  end.
-
-
-(** Original definition:
-<<
-Nondetfunction shruimm (e1: expr) (n: int) :=
-  if Int.eq n Int.zero then
-    e1
-  else if negb (Int.ltu n Int.iwordsize) then
-    Eop Oshru (e1 ::: Eop (Ointconst n) Enil ::: Enil)
-  else match e1 with
-    | Eop (Ointconst n1) Enil =>
-        Eop (Ointconst (Int.shru n1 n)) Enil
-    | Eop (Oshruimm n1) (t1:::Enil) =>
-        if Int.ltu (Int.add n n1) Int.iwordsize
-        then Eop (Oshruimm (Int.add n n1)) (t1:::Enil)
-        else Eop (Oshruimm n) (e1:::Enil)
-    | _ =>
-        Eop (Oshruimm n) (e1:::Enil)
-    end.
->>
-*)
-
-Inductive shruimm_cases: forall (e1: expr) , Type :=
-  | shruimm_case1: forall n1, shruimm_cases (Eop (Ointconst n1) Enil)
-  | shruimm_case2: forall n1 t1, shruimm_cases (Eop (Oshruimm n1) (t1:::Enil))
-  | shruimm_default: forall (e1: expr) , shruimm_cases e1.
-
-Definition shruimm_match (e1: expr)  :=
-  match e1 as zz1 return shruimm_cases zz1 with
-  | Eop (Ointconst n1) Enil => shruimm_case1 n1
-  | Eop (Oshruimm n1) (t1:::Enil) => shruimm_case2 n1 t1
-  | e1 => shruimm_default e1
-  end.
-
-Definition shruimm (e1: expr) (n: int) :=
- if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int.iwordsize) then Eop Oshru (e1 ::: Eop (Ointconst n) Enil ::: Enil) else match shruimm_match e1 with
-  | shruimm_case1 n1 => (* Eop (Ointconst n1) Enil *) 
-      Eop (Ointconst (Int.shru n1 n)) Enil
-  | shruimm_case2 n1 t1 => (* Eop (Oshruimm n1) (t1:::Enil) *) 
-      if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshruimm (Int.add n n1)) (t1:::Enil) else Eop (Oshruimm n) (e1:::Enil)
-  | shruimm_default e1 =>
-      Eop (Oshruimm n) (e1:::Enil)
-  end.
-
-
-(** Original definition:
-<<
-Nondetfunction shrimm (e1: expr) (n: int) :=
-  if Int.eq n Int.zero then
-    e1
-  else if negb (Int.ltu n Int.iwordsize) then
-    Eop Oshr (e1 ::: Eop (Ointconst n) Enil ::: Enil)
-  else match e1 with
-    | Eop (Ointconst n1) Enil =>
-        Eop (Ointconst (Int.shr n1 n)) Enil
-    | Eop (Oshrimm n1) (t1:::Enil) =>
-        if Int.ltu (Int.add n n1) Int.iwordsize
-        then Eop (Oshrimm (Int.add n n1)) (t1:::Enil)
-        else Eop (Oshrimm n) (e1:::Enil)
-    | _ =>
-        Eop (Oshrimm n) (e1:::Enil)
-    end.
->>
-*)
-
-Inductive shrimm_cases: forall (e1: expr) , Type :=
-  | shrimm_case1: forall n1, shrimm_cases (Eop (Ointconst n1) Enil)
-  | shrimm_case2: forall n1 t1, shrimm_cases (Eop (Oshrimm n1) (t1:::Enil))
-  | shrimm_default: forall (e1: expr) , shrimm_cases e1.
-
-Definition shrimm_match (e1: expr)  :=
-  match e1 as zz1 return shrimm_cases zz1 with
-  | Eop (Ointconst n1) Enil => shrimm_case1 n1
-  | Eop (Oshrimm n1) (t1:::Enil) => shrimm_case2 n1 t1
-  | e1 => shrimm_default e1
-  end.
-
-Definition shrimm (e1: expr) (n: int) :=
- if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int.iwordsize) then Eop Oshr (e1 ::: Eop (Ointconst n) Enil ::: Enil) else match shrimm_match e1 with
-  | shrimm_case1 n1 => (* Eop (Ointconst n1) Enil *) 
-      Eop (Ointconst (Int.shr n1 n)) Enil
-  | shrimm_case2 n1 t1 => (* Eop (Oshrimm n1) (t1:::Enil) *) 
-      if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshrimm (Int.add n n1)) (t1:::Enil) else Eop (Oshrimm n) (e1:::Enil)
-  | shrimm_default e1 =>
-      Eop (Oshrimm n) (e1:::Enil)
-  end.
-
-
-(** ** Integer multiply *)
-
-Definition mulimm_base (n1: int) (e2: expr) :=
-  match Int.one_bits n1 with
-  | i :: nil =>
-      shlimm e2 i
-  | i :: j :: nil =>
-      Elet e2 (add (shlimm (Eletvar 0) i) (shlimm (Eletvar 0) j))
-  | _ =>
-      Eop Omul (Eop (Ointconst n1) Enil ::: e2 ::: Enil)
-  end.
-
-(** Original definition:
-<<
-Nondetfunction mulimm (n1: int) (e2: expr) :=
-  if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil
-  else if Int.eq n1 Int.one then e2
-  else match e2 with
-  | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.mul n1 n2)) Enil
-  | Eop (Oaddimm n2) (t2:::Enil) => addimm (Int.mul n1 n2) (mulimm_base n1 t2)
-  | _ => mulimm_base n1 e2
-  end.
->>
-*)
-
-Inductive mulimm_cases: forall (e2: expr), Type :=
-  | mulimm_case1: forall n2, mulimm_cases (Eop (Ointconst n2) Enil)
-  | mulimm_case2: forall n2 t2, mulimm_cases (Eop (Oaddimm n2) (t2:::Enil))
-  | mulimm_default: forall (e2: expr), mulimm_cases e2.
-
-Definition mulimm_match (e2: expr) :=
-  match e2 as zz1 return mulimm_cases zz1 with
-  | Eop (Ointconst n2) Enil => mulimm_case1 n2
-  | Eop (Oaddimm n2) (t2:::Enil) => mulimm_case2 n2 t2
-  | e2 => mulimm_default e2
-  end.
-
-Definition mulimm (n1: int) (e2: expr) :=
- if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else if Int.eq n1 Int.one then e2 else match mulimm_match e2 with
-  | mulimm_case1 n2 => (* Eop (Ointconst n2) Enil *) 
-      Eop (Ointconst (Int.mul n1 n2)) Enil
-  | mulimm_case2 n2 t2 => (* Eop (Oaddimm n2) (t2:::Enil) *) 
-      addimm (Int.mul n1 n2) (mulimm_base n1 t2)
-  | mulimm_default e2 =>
-      mulimm_base n1 e2
-  end.
-
-
-(** Original definition:
-<<
-Nondetfunction mul (e1: expr) (e2: expr) :=
-  match e1, e2 with
-  | Eop (Ointconst n1) Enil, t2 => mulimm n1 t2
-  | t1, Eop (Ointconst n2) Enil => mulimm n2 t1
-  | _, _ => Eop Omul (e1:::e2:::Enil)
-  end.
->>
-*)
-
-Inductive mul_cases: forall (e1: expr) (e2: expr), Type :=
-  | mul_case1: forall n1 t2, mul_cases (Eop (Ointconst n1) Enil) (t2)
-  | mul_case2: forall t1 n2, mul_cases (t1) (Eop (Ointconst n2) Enil)
-  | mul_default: forall (e1: expr) (e2: expr), mul_cases e1 e2.
-
-Definition mul_match (e1: expr) (e2: expr) :=
-  match e1 as zz1, e2 as zz2 return mul_cases zz1 zz2 with
-  | Eop (Ointconst n1) Enil, t2 => mul_case1 n1 t2
-  | t1, Eop (Ointconst n2) Enil => mul_case2 t1 n2
-  | e1, e2 => mul_default e1 e2
-  end.
-
-Definition mul (e1: expr) (e2: expr) :=
-  match mul_match e1 e2 with
-  | mul_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) 
-      mulimm n1 t2
-  | mul_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) 
-      mulimm n2 t1
-  | mul_default e1 e2 =>
-      Eop Omul (e1:::e2:::Enil)
-  end.
-
-
-Definition mulhs (e1: expr) (e2: expr) :=
-  if Archi.ptr64 then
-    Eop Olowlong
-      (Eop (Oshrlimm (Int.repr 32))
-         (Eop Omull (Eop Ocast32signed (e1 ::: Enil) :::
-                     Eop Ocast32signed (e2 ::: Enil) ::: Enil) ::: Enil)
-          ::: Enil)
-  else
-    Eop Omulhs (e1 ::: e2 ::: Enil).
-
-Definition mulhu (e1: expr) (e2: expr) :=
-  if Archi.ptr64 then
-    Eop Olowlong
-      (Eop (Oshrluimm (Int.repr 32))
-         (Eop Omull (Eop Ocast32unsigned (e1 ::: Enil) :::
-                     Eop Ocast32unsigned (e2 ::: Enil) ::: Enil) ::: Enil)
-          ::: Enil)
-  else
-    Eop Omulhu (e1 ::: e2 ::: Enil).
-
-(** ** Bitwise and, or, xor *)
-
-(** Original definition:
-<<
-Nondetfunction andimm (n1: int) (e2: expr) :=
-  if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil
-  else if Int.eq n1 Int.mone then e2
-  else match e2 with
-  | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.and n1 n2)) Enil
-  | Eop (Oandimm n2) (t2:::Enil) => Eop (Oandimm (Int.and n1 n2)) (t2:::Enil)
-  | Eop Onot (t2:::Enil) => Eop (Oandnimm n1) (t2:::Enil)
-  | _ => Eop (Oandimm n1) (e2:::Enil)
-  end.
->>
-*)
-
-Inductive andimm_cases: forall (e2: expr), Type :=
-  | andimm_case1: forall n2, andimm_cases (Eop (Ointconst n2) Enil)
-  | andimm_case2: forall n2 t2, andimm_cases (Eop (Oandimm n2) (t2:::Enil))
-  | andimm_case3: forall t2, andimm_cases (Eop Onot (t2:::Enil))
-  | andimm_default: forall (e2: expr), andimm_cases e2.
-
-Definition andimm_match (e2: expr) :=
-  match e2 as zz1 return andimm_cases zz1 with
-  | Eop (Ointconst n2) Enil => andimm_case1 n2
-  | Eop (Oandimm n2) (t2:::Enil) => andimm_case2 n2 t2
-  | Eop Onot (t2:::Enil) => andimm_case3 t2
-  | e2 => andimm_default e2
-  end.
-
-Definition andimm (n1: int) (e2: expr) :=
- if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else if Int.eq n1 Int.mone then e2 else match andimm_match e2 with
-  | andimm_case1 n2 => (* Eop (Ointconst n2) Enil *) 
-      Eop (Ointconst (Int.and n1 n2)) Enil
-  | andimm_case2 n2 t2 => (* Eop (Oandimm n2) (t2:::Enil) *) 
-      Eop (Oandimm (Int.and n1 n2)) (t2:::Enil)
-  | andimm_case3 t2 => (* Eop Onot (t2:::Enil) *) 
-      Eop (Oandnimm n1) (t2:::Enil)
-  | andimm_default e2 =>
-      Eop (Oandimm n1) (e2:::Enil)
-  end.
-
-
-(** Original definition:
-<<
-Nondetfunction and (e1: expr) (e2: expr) :=
-  match e1, e2 with
-  | Eop (Ointconst n1) Enil, t2 => andimm n1 t2
-  | t1, Eop (Ointconst n2) Enil => andimm n2 t1
-  | (Eop Onot (t1:::Enil)), t2 => Eop Oandn (t1:::t2:::Enil) 
-  | t1, (Eop Onot (t2:::Enil)) => Eop Oandn (t2:::t1:::Enil) 
-  | _, _ => Eop Oand (e1:::e2:::Enil)
-  end.
->>
-*)
-
-Inductive and_cases: forall (e1: expr) (e2: expr), Type :=
-  | and_case1: forall n1 t2, and_cases (Eop (Ointconst n1) Enil) (t2)
-  | and_case2: forall t1 n2, and_cases (t1) (Eop (Ointconst n2) Enil)
-  | and_case3: forall t1 t2, and_cases ((Eop Onot (t1:::Enil))) (t2)
-  | and_case4: forall t1 t2, and_cases (t1) ((Eop Onot (t2:::Enil)))
-  | and_default: forall (e1: expr) (e2: expr), and_cases e1 e2.
-
-Definition and_match (e1: expr) (e2: expr) :=
-  match e1 as zz1, e2 as zz2 return and_cases zz1 zz2 with
-  | Eop (Ointconst n1) Enil, t2 => and_case1 n1 t2
-  | t1, Eop (Ointconst n2) Enil => and_case2 t1 n2
-  | (Eop Onot (t1:::Enil)), t2 => and_case3 t1 t2
-  | t1, (Eop Onot (t2:::Enil)) => and_case4 t1 t2
-  | e1, e2 => and_default e1 e2
-  end.
-
-Definition and (e1: expr) (e2: expr) :=
-  match and_match e1 e2 with
-  | and_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) 
-      andimm n1 t2
-  | and_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) 
-      andimm n2 t1
-  | and_case3 t1 t2 => (* (Eop Onot (t1:::Enil)), t2 *) 
-      Eop Oandn (t1:::t2:::Enil)
-  | and_case4 t1 t2 => (* t1, (Eop Onot (t2:::Enil)) *) 
-      Eop Oandn (t2:::t1:::Enil)
-  | and_default e1 e2 =>
-      Eop Oand (e1:::e2:::Enil)
-  end.
-
-
-(** Original definition:
-<<
-Nondetfunction orimm (n1: int) (e2: expr) :=
-  if Int.eq n1 Int.zero then e2
-  else if Int.eq n1 Int.mone then Eop (Ointconst Int.mone) Enil
-  else match e2 with
-       | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.or n1 n2)) Enil
-       | Eop (Oorimm n2) (t2:::Enil) => Eop (Oorimm (Int.or n1 n2)) (t2:::Enil)
-       | Eop Onot (t2:::Enil) => Eop (Oornimm n1) (t2:::Enil)
-       | _ => Eop (Oorimm n1) (e2:::Enil)
-  end.
->>
-*)
-
-Inductive orimm_cases: forall (e2: expr), Type :=
-  | orimm_case1: forall n2, orimm_cases (Eop (Ointconst n2) Enil)
-  | orimm_case2: forall n2 t2, orimm_cases (Eop (Oorimm n2) (t2:::Enil))
-  | orimm_case3: forall t2, orimm_cases (Eop Onot (t2:::Enil))
-  | orimm_default: forall (e2: expr), orimm_cases e2.
-
-Definition orimm_match (e2: expr) :=
-  match e2 as zz1 return orimm_cases zz1 with
-  | Eop (Ointconst n2) Enil => orimm_case1 n2
-  | Eop (Oorimm n2) (t2:::Enil) => orimm_case2 n2 t2
-  | Eop Onot (t2:::Enil) => orimm_case3 t2
-  | e2 => orimm_default e2
-  end.
-
-Definition orimm (n1: int) (e2: expr) :=
- if Int.eq n1 Int.zero then e2 else if Int.eq n1 Int.mone then Eop (Ointconst Int.mone) Enil else match orimm_match e2 with
-  | orimm_case1 n2 => (* Eop (Ointconst n2) Enil *) 
-      Eop (Ointconst (Int.or n1 n2)) Enil
-  | orimm_case2 n2 t2 => (* Eop (Oorimm n2) (t2:::Enil) *) 
-      Eop (Oorimm (Int.or n1 n2)) (t2:::Enil)
-  | orimm_case3 t2 => (* Eop Onot (t2:::Enil) *) 
-      Eop (Oornimm n1) (t2:::Enil)
-  | orimm_default e2 =>
-      Eop (Oorimm n1) (e2:::Enil)
-  end.
-
-
-Definition same_expr_pure (e1 e2: expr) :=
-  match e1, e2 with
-  | Evar v1, Evar v2 => if ident_eq v1 v2 then true else false
-  | _, _ => false
-  end.
-
-(** Original definition:
-<<
-Nondetfunction or (e1: expr) (e2: expr) :=
-  match e1, e2 with
-  | Eop (Ointconst n1) Enil, t2 => orimm n1 t2
-  | t1, Eop (Ointconst n2) Enil => orimm n2 t1
-  | Eop (Oshlimm n1) (t1:::Enil), Eop (Oshruimm n2) (t2:::Enil) =>
-      if Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2
-      then Eop (Ororimm n2) (t1:::Enil)
-      else Eop Oor (e1:::e2:::Enil)
-  | Eop (Oshruimm n2) (t2:::Enil), Eop (Oshlimm n1) (t1:::Enil) =>
-      if Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2
-      then Eop (Ororimm n2) (t1:::Enil)
-      else Eop Oor (e1:::e2:::Enil)
-  | (Eop Onot (t1:::Enil)), t2 => Eop Oorn (t1:::t2:::Enil) 
-  | t1, (Eop Onot (t2:::Enil))  => Eop Oorn (t2:::t1:::Enil) 
-  | _, _ => Eop Oor (e1:::e2:::Enil)
-  end.
->>
-*)
-
-Inductive or_cases: forall (e1: expr) (e2: expr), Type :=
-  | or_case1: forall n1 t2, or_cases (Eop (Ointconst n1) Enil) (t2)
-  | or_case2: forall t1 n2, or_cases (t1) (Eop (Ointconst n2) Enil)
-  | or_case3: forall n1 t1 n2 t2, or_cases (Eop (Oshlimm n1) (t1:::Enil)) (Eop (Oshruimm n2) (t2:::Enil))
-  | or_case4: forall n2 t2 n1 t1, or_cases (Eop (Oshruimm n2) (t2:::Enil)) (Eop (Oshlimm n1) (t1:::Enil))
-  | or_case5: forall t1 t2, or_cases ((Eop Onot (t1:::Enil))) (t2)
-  | or_case6: forall t1 t2, or_cases (t1) ((Eop Onot (t2:::Enil)))
-  | or_default: forall (e1: expr) (e2: expr), or_cases e1 e2.
-
-Definition or_match (e1: expr) (e2: expr) :=
-  match e1 as zz1, e2 as zz2 return or_cases zz1 zz2 with
-  | Eop (Ointconst n1) Enil, t2 => or_case1 n1 t2
-  | t1, Eop (Ointconst n2) Enil => or_case2 t1 n2
-  | Eop (Oshlimm n1) (t1:::Enil), Eop (Oshruimm n2) (t2:::Enil) => or_case3 n1 t1 n2 t2
-  | Eop (Oshruimm n2) (t2:::Enil), Eop (Oshlimm n1) (t1:::Enil) => or_case4 n2 t2 n1 t1
-  | (Eop Onot (t1:::Enil)), t2 => or_case5 t1 t2
-  | t1, (Eop Onot (t2:::Enil)) => or_case6 t1 t2
-  | e1, e2 => or_default e1 e2
-  end.
-
-Definition or (e1: expr) (e2: expr) :=
-  match or_match e1 e2 with
-  | or_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) 
-      orimm n1 t2
-  | or_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) 
-      orimm n2 t1
-  | or_case3 n1 t1 n2 t2 => (* Eop (Oshlimm n1) (t1:::Enil), Eop (Oshruimm n2) (t2:::Enil) *) 
-      if Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2 then Eop (Ororimm n2) (t1:::Enil) else Eop Oor (e1:::e2:::Enil)
-  | or_case4 n2 t2 n1 t1 => (* Eop (Oshruimm n2) (t2:::Enil), Eop (Oshlimm n1) (t1:::Enil) *) 
-      if Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2 then Eop (Ororimm n2) (t1:::Enil) else Eop Oor (e1:::e2:::Enil)
-  | or_case5 t1 t2 => (* (Eop Onot (t1:::Enil)), t2 *) 
-      Eop Oorn (t1:::t2:::Enil)
-  | or_case6 t1 t2 => (* t1, (Eop Onot (t2:::Enil)) *) 
-      Eop Oorn (t2:::t1:::Enil)
-  | or_default e1 e2 =>
-      Eop Oor (e1:::e2:::Enil)
-  end.
-
-
-(** Original definition:
-<<
-Nondetfunction xorimm (n1: int) (e2: expr) :=
-  if Int.eq n1 Int.zero then e2 else
-  match e2 with
-  | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.xor n1 n2)) Enil
-  | Eop (Oxorimm n2) (t2:::Enil) =>
-      let n := Int.xor n1 n2 in
-      if Int.eq n Int.zero then t2 else Eop (Oxorimm n) (t2:::Enil)
-  | _ => Eop (Oxorimm n1) (e2:::Enil)
-  end.
->>
-*)
-
-Inductive xorimm_cases: forall (e2: expr), Type :=
-  | xorimm_case1: forall n2, xorimm_cases (Eop (Ointconst n2) Enil)
-  | xorimm_case2: forall n2 t2, xorimm_cases (Eop (Oxorimm n2) (t2:::Enil))
-  | xorimm_default: forall (e2: expr), xorimm_cases e2.
-
-Definition xorimm_match (e2: expr) :=
-  match e2 as zz1 return xorimm_cases zz1 with
-  | Eop (Ointconst n2) Enil => xorimm_case1 n2
-  | Eop (Oxorimm n2) (t2:::Enil) => xorimm_case2 n2 t2
-  | e2 => xorimm_default e2
-  end.
-
-Definition xorimm (n1: int) (e2: expr) :=
- if Int.eq n1 Int.zero then e2 else match xorimm_match e2 with
-  | xorimm_case1 n2 => (* Eop (Ointconst n2) Enil *) 
-      Eop (Ointconst (Int.xor n1 n2)) Enil
-  | xorimm_case2 n2 t2 => (* Eop (Oxorimm n2) (t2:::Enil) *) 
-      let n := Int.xor n1 n2 in if Int.eq n Int.zero then t2 else Eop (Oxorimm n) (t2:::Enil)
-  | xorimm_default e2 =>
-      Eop (Oxorimm n1) (e2:::Enil)
-  end.
-
-
-(** Original definition:
-<<
-Nondetfunction xor (e1: expr) (e2: expr) :=
-  match e1, e2 with
-  | Eop (Ointconst n1) Enil, t2 => xorimm n1 t2
-  | t1, Eop (Ointconst n2) Enil => xorimm n2 t1
-  | _, _ => Eop Oxor (e1:::e2:::Enil)
-  end.
->>
-*)
-
-Inductive xor_cases: forall (e1: expr) (e2: expr), Type :=
-  | xor_case1: forall n1 t2, xor_cases (Eop (Ointconst n1) Enil) (t2)
-  | xor_case2: forall t1 n2, xor_cases (t1) (Eop (Ointconst n2) Enil)
-  | xor_default: forall (e1: expr) (e2: expr), xor_cases e1 e2.
-
-Definition xor_match (e1: expr) (e2: expr) :=
-  match e1 as zz1, e2 as zz2 return xor_cases zz1 zz2 with
-  | Eop (Ointconst n1) Enil, t2 => xor_case1 n1 t2
-  | t1, Eop (Ointconst n2) Enil => xor_case2 t1 n2
-  | e1, e2 => xor_default e1 e2
-  end.
-
-Definition xor (e1: expr) (e2: expr) :=
-  match xor_match e1 e2 with
-  | xor_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) 
-      xorimm n1 t2
-  | xor_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) 
-      xorimm n2 t1
-  | xor_default e1 e2 =>
-      Eop Oxor (e1:::e2:::Enil)
-  end.
-
-
-(** ** Integer logical negation *)
-
-(** Original definition:
-<<
-Nondetfunction notint (e: expr) :=
-  match e with
-  | Eop Oand (e1:::e2:::Enil) => Eop Onand (e1:::e2:::Enil)
-  | Eop (Oandimm n) (e1:::Enil) => Eop (Onandimm n) (e1:::Enil)
-  | Eop Oor (e1:::e2:::Enil) => Eop Onor (e1:::e2:::Enil)
-  | Eop (Oorimm n) (e1:::Enil) => Eop (Onorimm n) (e1:::Enil)
-  | Eop Oxor (e1:::e2:::Enil) => Eop Onxor (e1:::e2:::Enil)
-  | Eop (Oxorimm n) (e1:::Enil) => Eop (Onxorimm n) (e1:::Enil)
-  | _ => Eop Onot (e:::Enil)
-  end.
->>
-*)
-
-Inductive notint_cases: forall (e: expr), Type :=
-  | notint_case1: forall e1 e2, notint_cases (Eop Oand (e1:::e2:::Enil))
-  | notint_case2: forall n e1, notint_cases (Eop (Oandimm n) (e1:::Enil))
-  | notint_case3: forall e1 e2, notint_cases (Eop Oor (e1:::e2:::Enil))
-  | notint_case4: forall n e1, notint_cases (Eop (Oorimm n) (e1:::Enil))
-  | notint_case5: forall e1 e2, notint_cases (Eop Oxor (e1:::e2:::Enil))
-  | notint_case6: forall n e1, notint_cases (Eop (Oxorimm n) (e1:::Enil))
-  | notint_default: forall (e: expr), notint_cases e.
-
-Definition notint_match (e: expr) :=
-  match e as zz1 return notint_cases zz1 with
-  | Eop Oand (e1:::e2:::Enil) => notint_case1 e1 e2
-  | Eop (Oandimm n) (e1:::Enil) => notint_case2 n e1
-  | Eop Oor (e1:::e2:::Enil) => notint_case3 e1 e2
-  | Eop (Oorimm n) (e1:::Enil) => notint_case4 n e1
-  | Eop Oxor (e1:::e2:::Enil) => notint_case5 e1 e2
-  | Eop (Oxorimm n) (e1:::Enil) => notint_case6 n e1
-  | e => notint_default e
-  end.
-
-Definition notint (e: expr) :=
-  match notint_match e with
-  | notint_case1 e1 e2 => (* Eop Oand (e1:::e2:::Enil) *) 
-      Eop Onand (e1:::e2:::Enil)
-  | notint_case2 n e1 => (* Eop (Oandimm n) (e1:::Enil) *) 
-      Eop (Onandimm n) (e1:::Enil)
-  | notint_case3 e1 e2 => (* Eop Oor (e1:::e2:::Enil) *) 
-      Eop Onor (e1:::e2:::Enil)
-  | notint_case4 n e1 => (* Eop (Oorimm n) (e1:::Enil) *) 
-      Eop (Onorimm n) (e1:::Enil)
-  | notint_case5 e1 e2 => (* Eop Oxor (e1:::e2:::Enil) *) 
-      Eop Onxor (e1:::e2:::Enil)
-  | notint_case6 n e1 => (* Eop (Oxorimm n) (e1:::Enil) *) 
-      Eop (Onxorimm n) (e1:::Enil)
-  | notint_default e =>
-      Eop Onot (e:::Enil)
-  end.
-
-
-(** ** Integer division and modulus *)
-
-Definition divs_base (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
-Definition mods_base (e1: expr) (e2: expr) := Eop Omod (e1:::e2:::Enil).
-Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil).
-Definition modu_base (e1: expr) (e2: expr) := Eop Omodu (e1:::e2:::Enil).
-
-Definition shrximm (e1: expr) (n2: int) :=
-  if Int.eq n2 Int.zero then e1 else Eop (Oshrximm n2) (e1:::Enil).
-
-(* Alternate definition, not convenient for strength reduction during constant propagation *)
-(*
-(* n2 will be less than 31. *)
-
-Definition shrximm_inner (e1: expr) (n2: int) :=
-  Eop (Oshruimm (Int.sub Int.iwordsize n2))
-      ((Eop (Oshrimm (Int.repr (Int.zwordsize - 1)))
-            (e1 ::: Enil))
-         ::: Enil).
-
-Definition shrximm (e1: expr) (n2: int) :=
-  if Int.eq n2 Int.zero then e1
-  else Eop (Oshrimm n2)
-           ((Eop Oadd (e1 ::: shrximm_inner e1 n2 ::: Enil))
-              ::: Enil).
-*)
-
-(** ** General shifts *)
-
-(** Original definition:
-<<
-Nondetfunction shl (e1: expr) (e2: expr) :=
-  match e2 with
-  | Eop (Ointconst n2) Enil => shlimm e1 n2
-  | _ => Eop Oshl (e1:::e2:::Enil)
-  end.
->>
-*)
-
-Inductive shl_cases: forall (e2: expr), Type :=
-  | shl_case1: forall n2, shl_cases (Eop (Ointconst n2) Enil)
-  | shl_default: forall (e2: expr), shl_cases e2.
-
-Definition shl_match (e2: expr) :=
-  match e2 as zz1 return shl_cases zz1 with
-  | Eop (Ointconst n2) Enil => shl_case1 n2
-  | e2 => shl_default e2
-  end.
-
-Definition shl (e1: expr) (e2: expr) :=
-  match shl_match e2 with
-  | shl_case1 n2 => (* Eop (Ointconst n2) Enil *) 
-      shlimm e1 n2
-  | shl_default e2 =>
-      Eop Oshl (e1:::e2:::Enil)
-  end.
-
-
-(** Original definition:
-<<
-Nondetfunction shr (e1: expr) (e2: expr) :=
-  match e2 with
-  | Eop (Ointconst n2) Enil => shrimm e1 n2
-  | _ => Eop Oshr (e1:::e2:::Enil)
-  end.
->>
-*)
-
-Inductive shr_cases: forall (e2: expr), Type :=
-  | shr_case1: forall n2, shr_cases (Eop (Ointconst n2) Enil)
-  | shr_default: forall (e2: expr), shr_cases e2.
-
-Definition shr_match (e2: expr) :=
-  match e2 as zz1 return shr_cases zz1 with
-  | Eop (Ointconst n2) Enil => shr_case1 n2
-  | e2 => shr_default e2
-  end.
-
-Definition shr (e1: expr) (e2: expr) :=
-  match shr_match e2 with
-  | shr_case1 n2 => (* Eop (Ointconst n2) Enil *) 
-      shrimm e1 n2
-  | shr_default e2 =>
-      Eop Oshr (e1:::e2:::Enil)
-  end.
-
-
-(** Original definition:
-<<
-Nondetfunction shru (e1: expr) (e2: expr) :=
-  match e2 with
-  | Eop (Ointconst n2) Enil => shruimm e1 n2
-  | _ => Eop Oshru (e1:::e2:::Enil)
-  end.
->>
-*)
-
-Inductive shru_cases: forall (e2: expr), Type :=
-  | shru_case1: forall n2, shru_cases (Eop (Ointconst n2) Enil)
-  | shru_default: forall (e2: expr), shru_cases e2.
-
-Definition shru_match (e2: expr) :=
-  match e2 as zz1 return shru_cases zz1 with
-  | Eop (Ointconst n2) Enil => shru_case1 n2
-  | e2 => shru_default e2
-  end.
-
-Definition shru (e1: expr) (e2: expr) :=
-  match shru_match e2 with
-  | shru_case1 n2 => (* Eop (Ointconst n2) Enil *) 
-      shruimm e1 n2
-  | shru_default e2 =>
-      Eop Oshru (e1:::e2:::Enil)
-  end.
-
-
-(** ** Floating-point arithmetic *)
-
-Definition negf (e: expr) :=  Eop Onegf (e ::: Enil).
-Definition absf (e: expr) :=  Eop Oabsf (e ::: Enil).
-Definition addf (e1 e2: expr) :=  Eop Oaddf (e1 ::: e2 ::: Enil).
-Definition subf (e1 e2: expr) :=  Eop Osubf (e1 ::: e2 ::: Enil).
-Definition mulf (e1 e2: expr) :=  Eop Omulf (e1 ::: e2 ::: Enil).
-
-Definition negfs (e: expr) :=  Eop Onegfs (e ::: Enil).
-Definition absfs (e: expr) :=  Eop Oabsfs (e ::: Enil).
-Definition addfs (e1 e2: expr) :=  Eop Oaddfs (e1 ::: e2 ::: Enil).
-Definition subfs (e1 e2: expr) :=  Eop Osubfs (e1 ::: e2 ::: Enil).
-Definition mulfs (e1 e2: expr) :=  Eop Omulfs (e1 ::: e2 ::: Enil).
-
-(** ** Comparisons *)
-
-(** Original definition:
-<<
-Nondetfunction compimm (default: comparison -> int -> condition)
-                       (sem: comparison -> int -> int -> bool)
-                       (c: comparison) (e1: expr) (n2: int) :=
-  match c, e1 with
-  | c, Eop (Ointconst n1) Enil =>
-      Eop (Ointconst (if sem c n1 n2 then Int.one else Int.zero)) Enil
-  | Ceq, Eop (Ocmp c) el =>
-      if Int.eq_dec n2 Int.zero then
-        Eop (Ocmp (negate_condition c)) el
-      else if Int.eq_dec n2 Int.one then
-        Eop (Ocmp c) el
-      else
-        Eop (Ointconst Int.zero) Enil
-  | Cne, Eop (Ocmp c) el =>
-      if Int.eq_dec n2 Int.zero then
-        Eop (Ocmp c) el
-      else if Int.eq_dec n2 Int.one then
-        Eop (Ocmp (negate_condition c)) el
-      else
-        Eop (Ointconst Int.one) Enil
-  | _, _ =>
-       Eop (Ocmp (default c n2)) (e1 ::: Enil)
-  end.
->>
-*)
-
-Inductive compimm_cases: forall (c: comparison) (e1: expr) , Type :=
-  | compimm_case1: forall c n1, compimm_cases (c) (Eop (Ointconst n1) Enil)
-  | compimm_case2: forall c el, compimm_cases (Ceq) (Eop (Ocmp c) el)
-  | compimm_case3: forall c el, compimm_cases (Cne) (Eop (Ocmp c) el)
-  | compimm_default: forall (c: comparison) (e1: expr) , compimm_cases c e1.
-
-Definition compimm_match (c: comparison) (e1: expr)  :=
-  match c as zz1, e1 as zz2 return compimm_cases zz1 zz2 with
-  | c, Eop (Ointconst n1) Enil => compimm_case1 c n1
-  | Ceq, Eop (Ocmp c) el => compimm_case2 c el
-  | Cne, Eop (Ocmp c) el => compimm_case3 c el
-  | c, e1 => compimm_default c e1
-  end.
-
-Definition compimm (default: comparison -> int -> condition) (sem: comparison -> int -> int -> bool) (c: comparison) (e1: expr) (n2: int) :=
-  match compimm_match c e1 with
-  | compimm_case1 c n1 => (* c, Eop (Ointconst n1) Enil *) 
-      Eop (Ointconst (if sem c n1 n2 then Int.one else Int.zero)) Enil
-  | compimm_case2 c el => (* Ceq, Eop (Ocmp c) el *) 
-      if Int.eq_dec n2 Int.zero then Eop (Ocmp (negate_condition c)) el else if Int.eq_dec n2 Int.one then Eop (Ocmp c) el else Eop (Ointconst Int.zero) Enil
-  | compimm_case3 c el => (* Cne, Eop (Ocmp c) el *) 
-      if Int.eq_dec n2 Int.zero then Eop (Ocmp c) el else if Int.eq_dec n2 Int.one then Eop (Ocmp (negate_condition c)) el else Eop (Ointconst Int.one) Enil
-  | compimm_default c e1 =>
-      Eop (Ocmp (default c n2)) (e1 ::: Enil)
-  end.
-
-
-(** Original definition:
-<<
-Nondetfunction comp (c: comparison) (e1: expr) (e2: expr) :=
-  match e1, e2 with
-  | Eop (Ointconst n1) Enil, t2 =>
-      compimm Ccompimm Int.cmp (swap_comparison c) t2 n1
-  | t1, Eop (Ointconst n2) Enil =>
-      compimm Ccompimm Int.cmp c t1 n2
-  | _, _ =>
-      Eop (Ocmp (Ccomp c)) (e1 ::: e2 ::: Enil)
-  end.
->>
-*)
-
-Inductive comp_cases: forall (e1: expr) (e2: expr), Type :=
-  | comp_case1: forall n1 t2, comp_cases (Eop (Ointconst n1) Enil) (t2)
-  | comp_case2: forall t1 n2, comp_cases (t1) (Eop (Ointconst n2) Enil)
-  | comp_default: forall (e1: expr) (e2: expr), comp_cases e1 e2.
-
-Definition comp_match (e1: expr) (e2: expr) :=
-  match e1 as zz1, e2 as zz2 return comp_cases zz1 zz2 with
-  | Eop (Ointconst n1) Enil, t2 => comp_case1 n1 t2
-  | t1, Eop (Ointconst n2) Enil => comp_case2 t1 n2
-  | e1, e2 => comp_default e1 e2
-  end.
-
-Definition comp (c: comparison) (e1: expr) (e2: expr) :=
-  match comp_match e1 e2 with
-  | comp_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) 
-      compimm Ccompimm Int.cmp (swap_comparison c) t2 n1
-  | comp_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) 
-      compimm Ccompimm Int.cmp c t1 n2
-  | comp_default e1 e2 =>
-      Eop (Ocmp (Ccomp c)) (e1 ::: e2 ::: Enil)
-  end.
-
-
-(** Original definition:
-<<
-Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) :=
-  match e1, e2 with
-  | Eop (Ointconst n1) Enil, t2 =>
-      compimm Ccompuimm Int.cmpu (swap_comparison c) t2 n1
-  | t1, Eop (Ointconst n2) Enil =>
-      compimm Ccompuimm Int.cmpu c t1 n2
-  | _, _ =>
-      Eop (Ocmp (Ccompu c)) (e1 ::: e2 ::: Enil)
-  end.
->>
-*)
-
-Inductive compu_cases: forall (e1: expr) (e2: expr), Type :=
-  | compu_case1: forall n1 t2, compu_cases (Eop (Ointconst n1) Enil) (t2)
-  | compu_case2: forall t1 n2, compu_cases (t1) (Eop (Ointconst n2) Enil)
-  | compu_default: forall (e1: expr) (e2: expr), compu_cases e1 e2.
-
-Definition compu_match (e1: expr) (e2: expr) :=
-  match e1 as zz1, e2 as zz2 return compu_cases zz1 zz2 with
-  | Eop (Ointconst n1) Enil, t2 => compu_case1 n1 t2
-  | t1, Eop (Ointconst n2) Enil => compu_case2 t1 n2
-  | e1, e2 => compu_default e1 e2
-  end.
-
-Definition compu (c: comparison) (e1: expr) (e2: expr) :=
-  match compu_match e1 e2 with
-  | compu_case1 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) 
-      compimm Ccompuimm Int.cmpu (swap_comparison c) t2 n1
-  | compu_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) 
-      compimm Ccompuimm Int.cmpu c t1 n2
-  | compu_default e1 e2 =>
-      Eop (Ocmp (Ccompu c)) (e1 ::: e2 ::: Enil)
-  end.
-
-
-Definition compf (c: comparison) (e1: expr) (e2: expr) :=
-  Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil).
-
-Definition compfs (c: comparison) (e1: expr) (e2: expr) :=
-  Eop (Ocmp (Ccompfs c)) (e1 ::: e2 ::: Enil).
-
-(** ** Integer conversions *)
-
-Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e.
-
-(** Original definition:
-<<
-Nondetfunction cast8signed (e: expr) :=
-  match e with
-  | Eop (Ointconst n) Enil => Eop (Ointconst (Int.sign_ext 8 n)) Enil
-  | _ =>  Eop Ocast8signed (e ::: Enil)
-  end.
->>
-*)
-
-Inductive cast8signed_cases: forall (e: expr), Type :=
-  | cast8signed_case1: forall n, cast8signed_cases (Eop (Ointconst n) Enil)
-  | cast8signed_default: forall (e: expr), cast8signed_cases e.
-
-Definition cast8signed_match (e: expr) :=
-  match e as zz1 return cast8signed_cases zz1 with
-  | Eop (Ointconst n) Enil => cast8signed_case1 n
-  | e => cast8signed_default e
-  end.
-
-Definition cast8signed (e: expr) :=
-  match cast8signed_match e with
-  | cast8signed_case1 n => (* Eop (Ointconst n) Enil *) 
-      Eop (Ointconst (Int.sign_ext 8 n)) Enil
-  | cast8signed_default e =>
-      Eop Ocast8signed (e ::: Enil)
-  end.
-
-
-Definition cast16unsigned (e: expr) := andimm (Int.repr 65535) e.
-
-(** Original definition:
-<<
-Nondetfunction cast16signed (e: expr) :=
-  match e with
-  | Eop (Ointconst n) Enil => Eop (Ointconst (Int.sign_ext 16 n)) Enil
-  | _ => Eop Ocast16signed (e ::: Enil)
-  end.
->>
-*)
-
-Inductive cast16signed_cases: forall (e: expr), Type :=
-  | cast16signed_case1: forall n, cast16signed_cases (Eop (Ointconst n) Enil)
-  | cast16signed_default: forall (e: expr), cast16signed_cases e.
-
-Definition cast16signed_match (e: expr) :=
-  match e as zz1 return cast16signed_cases zz1 with
-  | Eop (Ointconst n) Enil => cast16signed_case1 n
-  | e => cast16signed_default e
-  end.
-
-Definition cast16signed (e: expr) :=
-  match cast16signed_match e with
-  | cast16signed_case1 n => (* Eop (Ointconst n) Enil *) 
-      Eop (Ointconst (Int.sign_ext 16 n)) Enil
-  | cast16signed_default e =>
-      Eop Ocast16signed (e ::: Enil)
-  end.
-
-
-(** ** Floating-point conversions *)
-
-Definition intoffloat  (e: expr) := Eop Ointoffloat (e ::: Enil).
-Definition intuoffloat (e: expr) := Eop Ointuoffloat (e ::: Enil).
-
-(** Original definition:
-<<
-Nondetfunction floatofintu (e: expr) :=
-  match e with
-  | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_intu n)) Enil
-  | _ => Eop Ofloatofintu (e ::: Enil)
-  end.
->>
-*)
-
-Inductive floatofintu_cases: forall (e: expr), Type :=
-  | floatofintu_case1: forall n, floatofintu_cases (Eop (Ointconst n) Enil)
-  | floatofintu_default: forall (e: expr), floatofintu_cases e.
-
-Definition floatofintu_match (e: expr) :=
-  match e as zz1 return floatofintu_cases zz1 with
-  | Eop (Ointconst n) Enil => floatofintu_case1 n
-  | e => floatofintu_default e
-  end.
-
-Definition floatofintu (e: expr) :=
-  match floatofintu_match e with
-  | floatofintu_case1 n => (* Eop (Ointconst n) Enil *) 
-      Eop (Ofloatconst (Float.of_intu n)) Enil
-  | floatofintu_default e =>
-      Eop Ofloatofintu (e ::: Enil)
-  end.
-
-
-(** Original definition:
-<<
-Nondetfunction floatofint (e: expr) :=
-  match e with
-  | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_int n)) Enil
-  | _ => Eop Ofloatofint (e ::: Enil)
-  end.
->>
-*)
-
-Inductive floatofint_cases: forall (e: expr), Type :=
-  | floatofint_case1: forall n, floatofint_cases (Eop (Ointconst n) Enil)
-  | floatofint_default: forall (e: expr), floatofint_cases e.
-
-Definition floatofint_match (e: expr) :=
-  match e as zz1 return floatofint_cases zz1 with
-  | Eop (Ointconst n) Enil => floatofint_case1 n
-  | e => floatofint_default e
-  end.
-
-Definition floatofint (e: expr) :=
-  match floatofint_match e with
-  | floatofint_case1 n => (* Eop (Ointconst n) Enil *) 
-      Eop (Ofloatconst (Float.of_int n)) Enil
-  | floatofint_default e =>
-      Eop Ofloatofint (e ::: Enil)
-  end.
-
-
-Definition intofsingle (e: expr) := Eop Ointofsingle (e ::: Enil).
-Definition singleofint (e: expr) := Eop Osingleofint (e ::: Enil).
-
-Definition intuofsingle (e: expr) := Eop Ointuofsingle (e ::: Enil).
-Definition singleofintu (e: expr) := Eop Osingleofintu (e ::: Enil).
-
-Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil).
-Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil).
-
-(** ** Recognition of addressing modes for load and store operations *)
-
-(** Original definition:
-<<
-Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
-  match e with
-  | Eop (Oaddrstack n) Enil => (Ainstack n, Enil)
-  | Eop (Oaddrsymbol id ofs) Enil => if Archi.pic_code 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)
-  | _ => (Aindexed Ptrofs.zero, e:::Enil)
-  end.
->>
-*)
-
-Inductive addressing_cases: forall (e: expr), Type :=
-  | addressing_case1: forall n, addressing_cases (Eop (Oaddrstack n) Enil)
-  | addressing_case2: forall id ofs, addressing_cases (Eop (Oaddrsymbol id ofs) Enil)
-  | addressing_case3: forall n e1, addressing_cases (Eop (Oaddimm n) (e1:::Enil))
-  | addressing_case4: forall n e1, addressing_cases (Eop (Oaddlimm n) (e1:::Enil))
-  | addressing_default: forall (e: expr), addressing_cases e.
-
-Definition addressing_match (e: expr) :=
-  match e as zz1 return addressing_cases zz1 with
-  | Eop (Oaddrstack n) Enil => addressing_case1 n
-  | Eop (Oaddrsymbol id ofs) Enil => addressing_case2 id ofs
-  | Eop (Oaddimm n) (e1:::Enil) => addressing_case3 n e1
-  | Eop (Oaddlimm n) (e1:::Enil) => addressing_case4 n e1
-  | e => addressing_default e
-  end.
-
-Definition addressing (chunk: memory_chunk) (e: expr) :=
-  match addressing_match e with
-  | addressing_case1 n => (* Eop (Oaddrstack n) Enil *) 
-      (Ainstack n, Enil)
-  | addressing_case2 id ofs => (* Eop (Oaddrsymbol id ofs) Enil *) 
-      if Archi.pic_code tt then (Aindexed Ptrofs.zero, e:::Enil) else (Aglobal id ofs, Enil)
-  | addressing_case3 n e1 => (* Eop (Oaddimm n) (e1:::Enil) *) 
-      (Aindexed (Ptrofs.of_int n), e1:::Enil)
-  | addressing_case4 n e1 => (* Eop (Oaddlimm n) (e1:::Enil) *) 
-      (Aindexed (Ptrofs.of_int64 n), e1:::Enil)
-  | addressing_default e =>
-      (Aindexed Ptrofs.zero, e:::Enil)
-  end.
-
-
-(** ** Arguments of builtins *)
-
-(** Original definition:
-<<
-Nondetfunction builtin_arg (e: expr) :=
-  match e with
-  | Eop (Ointconst n) Enil => BA_int n
-  | Eop (Oaddrsymbol id ofs) Enil => BA_addrglobal id ofs
-  | Eop (Oaddrstack ofs) Enil => BA_addrstack ofs
-  | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) =>
-        BA_long (Int64.ofwords h l)
-  | Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l)
-  | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs
-  | Eop (Oaddimm n) (e1:::Enil) =>
-      if Archi.ptr64 then BA e else BA_addptr (BA e1) (BA_int n)
-  | Eop (Oaddlimm n) (e1:::Enil) =>
-      if Archi.ptr64 then BA_addptr (BA e1) (BA_long n) else BA e
-  | _ => BA e
-  end.
->>
-*)
-
-Inductive builtin_arg_cases: forall (e: expr), Type :=
-  | builtin_arg_case1: forall n, builtin_arg_cases (Eop (Ointconst n) Enil)
-  | builtin_arg_case2: forall id ofs, builtin_arg_cases (Eop (Oaddrsymbol id ofs) Enil)
-  | builtin_arg_case3: forall ofs, builtin_arg_cases (Eop (Oaddrstack ofs) Enil)
-  | builtin_arg_case4: forall h l, builtin_arg_cases (Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil))
-  | builtin_arg_case5: forall h l, builtin_arg_cases (Eop Omakelong (h ::: l ::: Enil))
-  | builtin_arg_case6: forall chunk ofs, builtin_arg_cases (Eload chunk (Ainstack ofs) Enil)
-  | builtin_arg_case7: forall n e1, builtin_arg_cases (Eop (Oaddimm n) (e1:::Enil))
-  | builtin_arg_case8: forall n e1, builtin_arg_cases (Eop (Oaddlimm n) (e1:::Enil))
-  | builtin_arg_default: forall (e: expr), builtin_arg_cases e.
-
-Definition builtin_arg_match (e: expr) :=
-  match e as zz1 return builtin_arg_cases zz1 with
-  | Eop (Ointconst n) Enil => builtin_arg_case1 n
-  | Eop (Oaddrsymbol id ofs) Enil => builtin_arg_case2 id ofs
-  | Eop (Oaddrstack ofs) Enil => builtin_arg_case3 ofs
-  | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => builtin_arg_case4 h l
-  | Eop Omakelong (h ::: l ::: Enil) => builtin_arg_case5 h l
-  | Eload chunk (Ainstack ofs) Enil => builtin_arg_case6 chunk ofs
-  | Eop (Oaddimm n) (e1:::Enil) => builtin_arg_case7 n e1
-  | Eop (Oaddlimm n) (e1:::Enil) => builtin_arg_case8 n e1
-  | e => builtin_arg_default e
-  end.
-
-Definition builtin_arg (e: expr) :=
-  match builtin_arg_match e with
-  | builtin_arg_case1 n => (* Eop (Ointconst n) Enil *) 
-      BA_int n
-  | builtin_arg_case2 id ofs => (* Eop (Oaddrsymbol id ofs) Enil *) 
-      BA_addrglobal id ofs
-  | builtin_arg_case3 ofs => (* Eop (Oaddrstack ofs) Enil *) 
-      BA_addrstack ofs
-  | builtin_arg_case4 h l => (* Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) *) 
-      BA_long (Int64.ofwords h l)
-  | builtin_arg_case5 h l => (* Eop Omakelong (h ::: l ::: Enil) *) 
-      BA_splitlong (BA h) (BA l)
-  | builtin_arg_case6 chunk ofs => (* Eload chunk (Ainstack ofs) Enil *) 
-      BA_loadstack chunk ofs
-  | builtin_arg_case7 n e1 => (* Eop (Oaddimm n) (e1:::Enil) *) 
-      if Archi.ptr64 then BA e else BA_addptr (BA e1) (BA_int n)
-  | builtin_arg_case8 n e1 => (* Eop (Oaddlimm n) (e1:::Enil) *) 
-      if Archi.ptr64 then BA_addptr (BA e1) (BA_long n) else BA e
-  | builtin_arg_default e =>
-      BA e
-  end.
-
-- 
cgit 


From 3125e65d78c9f06514574650648b3d5b5adaacbd Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Tue, 19 Mar 2019 17:36:36 +0100
Subject: remove a FAILWITH that forbids some debugging information to be
 printed

---
 mppa_k1c/abstractbb/ImpDep.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/mppa_k1c/abstractbb/ImpDep.v b/mppa_k1c/abstractbb/ImpDep.v
index 0cce7ce3..9051f6ad 100644
--- a/mppa_k1c/abstractbb/ImpDep.v
+++ b/mppa_k1c/abstractbb/ImpDep.v
@@ -386,7 +386,7 @@ Variable print_error_end: hdeps -> hdeps -> ?? unit.
 Variable print_error: pstring -> ?? unit.
 
 Program Definition g_bblock_eq_test (p1 p2: bblock): ?? bool :=
-  DO r <~ (TRY 
+  DO r <~ (TRY
     DO d1 <~ hbblock_deps (hC hco_tree) (hC hco_list) dbg1 log1 p1 ;;
     DO d2 <~ hbblock_deps (hC_known hco_tree) (hC_known hco_list) dbg2 log2 p2 ;;
     DO b <~ Dict.eq_test d1 d2 ;;
@@ -395,7 +395,7 @@ Program Definition g_bblock_eq_test (p1 p2: bblock): ?? bool :=
       print_error_end d1 d2 ;;
       RET false
     )
-  CATCH_FAIL s, _ => 
+  CATCH_FAIL s, _ =>
     print_error s;;
     RET false
   ENSURE (fun b => b=true -> forall ge, bblock_equiv ge p1 p2));;
@@ -633,7 +633,7 @@ Definition print_witness ext exl cr msg :=
      println(r);;
      println("=> encoded on " +; msg +; " graph as: ");;
      print_raw_hlist pl
-  | _ => FAILWITH "No witness info"
+  | _ => println "Unexpected failure: no witness info (hint: hash-consing bug ?)"
   end.
 
 
-- 
cgit 


From 6ae5c96b2905220cc31535fb93a2e853249adae7 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Tue, 19 Mar 2019 17:39:26 +0100
Subject: fix missing case in Asmblockdeps.arith_op_eq

---
 mppa_k1c/Asmblockdeps.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 5a138d00..f28e660c 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -286,6 +286,7 @@ Definition arith_op_eq (o1 o2: arith_op): ?? bool :=
   | OArithRRR n1, OArithRRR n2 => phys_eq n1 n2
   | OArithRRI32 n1 i1, OArithRRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2)
   | OArithRRI64 n1 i1, OArithRRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2)
+  | OArithARRR n1, OArithARRR n2 => phys_eq n1 n2
   | _, _ => RET false
   end.
 
@@ -381,13 +382,12 @@ Qed.
 
 (* Definition op_eq (o1 o2: op): ?? bool := struct_eq o1 o2. 
 
-
 Theorem op_eq_correct o1 o2: 
  WHEN op_eq o1 o2 ~> b THEN b=true -> o1 = o2.
 Proof.
   wlp_simplify.
 Qed.
- *)
+*)
 
 End IMPPARAM.
 
-- 
cgit 


From d1dfa934a33da18eab0424012cf4dd2b602c21a5 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Tue, 19 Mar 2019 18:05:49 +0100
Subject: improve robustness of Asmblockdeps.arith_op_eq.

---
 mppa_k1c/Asmblockdeps.v | 42 +++++++++++++++++++++++++++++-------------
 1 file changed, 29 insertions(+), 13 deletions(-)

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index f28e660c..e05f92a7 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -276,18 +276,31 @@ Definition iandb (ib1 ib2: ?? bool): ?? bool :=
   RET (andb b1 b2).
 
 Definition arith_op_eq (o1 o2: arith_op): ?? bool :=
-  match o1, o2 with
-  | OArithR n1, OArithR n2 => struct_eq n1 n2
-  | OArithRR n1, OArithRR n2 => phys_eq n1 n2
-  | OArithRI32 n1 i1, OArithRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2)
-  | OArithRI64 n1 i1, OArithRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2)
-  | OArithRF32 n1 i1, OArithRF32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2)
-  | OArithRF64 n1 i1, OArithRF64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2)
-  | OArithRRR n1, OArithRRR n2 => phys_eq n1 n2
-  | OArithRRI32 n1 i1, OArithRRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2)
-  | OArithRRI64 n1 i1, OArithRRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2)
-  | OArithARRR n1, OArithARRR n2 => phys_eq n1 n2
-  | _, _ => RET false
+  match o1 with
+  | OArithR n1 =>
+     match o2 with OArithR n2 => struct_eq n1 n2 | _ => RET false end
+  | OArithRR n1 => 
+     match o2 with OArithRR n2 => phys_eq n1 n2 | _ => RET false end
+  | OArithRI32 n1 i1 =>
+     match o2 with OArithRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end
+  | OArithRI64 n1 i1 =>
+     match o2 with OArithRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end
+  | OArithRF32 n1 i1 =>
+     match o2 with OArithRF32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end
+  | OArithRF64 n1 i1 =>
+     match o2 with OArithRF64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end
+  | OArithRRR n1 =>
+     match o2 with OArithRRR n2 => phys_eq n1 n2 | _ => RET false end
+  | OArithRRI32 n1 i1 =>
+     match o2 with OArithRRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end
+  | OArithRRI64 n1 i1 =>
+     match o2 with OArithRRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end
+  | OArithARRR n1 =>
+     match o2 with OArithARRR n2 => phys_eq n1 n2 | _ => RET false end
+  | OArithARRI32 n1 i1 =>
+     match o2 with OArithARRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end
+  | OArithARRI64 n1 i1 =>
+     match o2 with OArithARRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end
   end.
 
 Lemma arith_op_eq_correct o1 o2:
@@ -324,7 +337,8 @@ Proof.
   apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence.
 Qed.
 
-
+(* TODO: rewrite control_op_eq in a robust style against the miss of a case
+   cf. arith_op_eq above *)
 Definition control_op_eq (c1 c2: control_op): ?? bool :=
   match c1, c2 with
   | Oj_l l1, Oj_l l2 => phys_eq l1 l2
@@ -346,6 +360,8 @@ Proof.
 Qed.
 
 
+(* TODO: rewrite op_eq in a robust style against the miss of a case
+   cf. arith_op_eq above *)
 Definition op_eq (o1 o2: op): ?? bool :=
   match o1, o2 with
   | Arith i1, Arith i2 => arith_op_eq i1 i2
-- 
cgit 


From 196dbf8e545e0bed39696434c0425806b00da6e8 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 19 Mar 2019 19:35:30 +0100
Subject: seems to work

---
 test/monniaux/madd/madd.c | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test/monniaux/madd/madd.c

diff --git a/test/monniaux/madd/madd.c b/test/monniaux/madd/madd.c
new file mode 100644
index 00000000..e1e5eeb7
--- /dev/null
+++ b/test/monniaux/madd/madd.c
@@ -0,0 +1,7 @@
+unsigned madd(unsigned a, unsigned b, unsigned c) {
+  return a + b*c;
+}
+
+unsigned madd2(unsigned a, unsigned b, unsigned c) {
+  return c + b*a;
+}
-- 
cgit 


From 4833f4a05023b57cba859a652924d1cd058efcea Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 19 Mar 2019 19:42:03 +0100
Subject: reverse madd

---
 mppa_k1c/SelectOp.vp     | 2 ++
 mppa_k1c/SelectOpproof.v | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index e34e7c32..22211167 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -88,6 +88,8 @@ Nondetfunction add (e1: expr) (e2: expr) :=
       addimm n2 (Eop Oadd (t1:::t2:::Enil))
   | t1, (Eop Omul (t2:::t3:::Enil)) =>
       Eop Omadd (t1:::t2:::t3:::Enil)
+  | (Eop Omul (t2:::t3:::Enil)), t1 =>
+      Eop Omadd (t1:::t2:::t3:::Enil)
   | _, _ => Eop Oadd (e1:::e2:::Enil)
   end.
 
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index d7ae92dc..fe678383 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -184,6 +184,8 @@ Proof.
     repeat rewrite Val.add_assoc. reflexivity.
   - (* Omadd *)
     subst. TrivialExists.
+  - (* Omadd *)
+    subst. rewrite Val.add_commut. TrivialExists.
   - TrivialExists.
 Qed.
 
-- 
cgit 


From f2e7e95f6e113edbcb80618a0f3b4c15caa6f5cd Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 19 Mar 2019 19:52:01 +0100
Subject: fix classes for madd

---
 mppa_k1c/PostpassSchedulingOracle.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index b02bc6ca..f7702a9d 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -524,12 +524,12 @@ 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 | Maddw -> 
+  | Nxorw | Andnw | Ornw  -> 
       (match encoding with None | Some U6 | Some S10 -> alu_tiny 
                           | Some U27L5 | Some U27L10 -> alu_tiny_x
                           | _ -> raise InvalidEncoding)
   | Addd | Andd | Nandd | Ord | Nord | Sbfd | Xord
-  | Nxord | Andnd | Ornd | Maddd -> 
+  | Nxord | Andnd | Ornd -> 
       (match encoding with None | Some U6 | Some S10 -> alu_tiny 
                           | Some U27L5 | Some U27L10 -> alu_tiny_x
                           | Some E27U27L10 -> alu_tiny_y)
@@ -549,10 +549,10 @@ let rec_to_usage r =
                           | Some U27L5 | Some U27L10 -> alu_tiny_x 
                           | Some E27U27L10 -> alu_tiny_y 
                           | _ -> raise InvalidEncoding)
-  | Mulw -> (match encoding with None -> mau
+  | Mulw| Maddw -> (match encoding with None -> mau
                                 | Some U6 | Some S10 | Some U27L5 -> mau_x
                                 | _ -> raise InvalidEncoding)
-  | Muld -> (match encoding with None | Some U6 | Some S10 -> mau
+  | Muld | Maddd -> (match encoding with None | Some U6 | Some S10 -> mau
                                 | Some U27L5 | Some U27L10 -> mau_x
                                 | Some E27U27L10 -> mau_y)
   | Nop -> alu_nop
-- 
cgit 


From ae571e2467e977f03044d750568f6528d8d64e43 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 19 Mar 2019 20:41:23 +0100
Subject: mul immediate begin

---
 mppa_k1c/Asm.v                       | 4 ++++
 mppa_k1c/Asmblock.v                  | 4 ++++
 mppa_k1c/Asmblockdeps.v              | 2 ++
 mppa_k1c/NeedOp.v                    | 2 ++
 mppa_k1c/Op.v                        | 9 +++++++--
 mppa_k1c/PostpassSchedulingOracle.ml | 6 ++++--
 mppa_k1c/TargetPrinter.ml            | 4 ++++
 mppa_k1c/ValueAOp.v                  | 1 +
 test/monniaux/madd/madd.c            | 4 ++++
 9 files changed, 32 insertions(+), 4 deletions(-)

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 1a57e554..0ca554ab 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -177,6 +177,7 @@ 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 *)
+  | 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 *)
   | Poriw               (rd rs: ireg) (imm: int)    (**r or imm word *)
@@ -197,6 +198,7 @@ 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 *) 
+  | 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 *) 
   | Poril               (rd rs: ireg) (imm: int64)  (**r or immediate long *) 
@@ -319,6 +321,7 @@ Definition basic_to_instruction (b: basic) :=
   (* RRI32 *)
   | PArithRRI32 (Asmblock.Pcompiw it) rd rs imm => Pcompiw it rd rs imm
   | PArithRRI32 Asmblock.Paddiw rd rs imm       => Paddiw rd rs imm
+  | PArithRRI32 Asmblock.Pmuliw rd rs imm       => Pmuliw rd rs imm
   | PArithRRI32 Asmblock.Pandiw rd rs imm       => Pandiw rd rs imm
   | PArithRRI32 Asmblock.Pnandiw rd rs imm      => Pnandiw rd rs imm
   | PArithRRI32 Asmblock.Poriw rd rs imm        => Poriw rd rs imm
@@ -338,6 +341,7 @@ Definition basic_to_instruction (b: basic) :=
   (* RRI64 *)
   | PArithRRI64 (Asmblock.Pcompil it) rd rs imm => Pcompil it rd rs imm
   | PArithRRI64 Asmblock.Paddil rd rs imm       => Paddil rd rs imm
+  | PArithRRI64 Asmblock.Pmulil rd rs imm       => Pmulil rd rs imm
   | PArithRRI64 Asmblock.Pandil rd rs imm       => Pandil rd rs imm
   | PArithRRI64 Asmblock.Pnandil rd rs imm      => Pnandil rd rs imm
   | PArithRRI64 Asmblock.Poril rd rs imm        => Poril rd rs imm
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index b3e1532d..386106d6 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -376,6 +376,7 @@ Inductive arith_name_rri32 : Type :=
   | Pcompiw (it: itest)                             (**r comparison imm word *)
 
   | Paddiw                                          (**r add imm word *)
+  | Pmuliw                                          (**r add imm word *)
   | Pandiw                                          (**r and imm word *)
   | Pnandiw                                         (**r nand imm word *)
   | Poriw                                           (**r or imm word *)
@@ -396,6 +397,7 @@ Inductive arith_name_rri32 : Type :=
 Inductive arith_name_rri64 : Type :=
   | Pcompil (it: itest)                             (**r comparison imm long *)
   | Paddil                                          (**r add immediate long *) 
+  | Pmulil                                          (**r mul immediate long *) 
   | Pandil                                          (**r and immediate long *) 
   | Pnandil                                         (**r nand immediate long *) 
   | Poril                                           (**r or immediate long *) 
@@ -1168,6 +1170,7 @@ Definition arith_eval_rri32 n v i :=
   match n with
   | Pcompiw c => compare_int c v (Vint i)
   | Paddiw  => Val.add   v (Vint i)
+  | Pmuliw  => Val.mul   v (Vint i)
   | Pandiw  => Val.and   v (Vint i)
   | Pnandiw => Val.notint (Val.and  v (Vint i))
   | Poriw   => Val.or    v (Vint i)
@@ -1189,6 +1192,7 @@ Definition arith_eval_rri64 n v i :=
   match n with
   | Pcompil c => compare_long c v (Vlong i)
   | Paddil  => Val.addl v (Vlong i)
+  | Pmulil  => Val.mull v (Vlong i)
   | Pandil  => Val.andl v (Vlong i)
   | Pnandil  => Val.notl (Val.andl v (Vlong i))
   | Poril   => Val.orl  v (Vlong i)
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index e05f92a7..f50b7d4a 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1382,6 +1382,7 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring :=
   match n with
     Pcompiw _ => "Pcompiw"
   | Paddiw => "Paddiw"
+  | Pmuliw => "Pmuliw"
   | Pandiw => "Pandiw"
   | Pnandiw => "Pnandiw"
   | Poriw => "Poriw"
@@ -1403,6 +1404,7 @@ Definition string_of_name_rri64 (n: arith_name_rri64): pstring :=
   match n with
     Pcompil _ => "Pcompil"
   | Paddil => "Paddil"
+  | Pmulil => "Pmulil"
   | Pandil => "Pandil"
   | Pnandil => "Pnandil"
   | Poril => "Poril"
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index 801a520e..c7b59a34 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -45,6 +45,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Oneg => op1 (modarith nv)
   | Osub => op2 (default nv)
   | Omul => op2 (modarith nv)
+  | Omulimm _ => op1 (modarith nv)
   | Omulhs | Omulhu | Odiv | Odivu | Omod | Omodu => op2 (default nv)
   | Oand => op2 (bitwise nv)
   | Oandimm n => op1 (andimm nv n)
@@ -171,6 +172,7 @@ Proof.
 - apply add_sound; auto with na.
 - apply neg_sound; auto.
 - apply mul_sound; auto.
+- apply mul_sound; auto with na.
 - apply and_sound; auto.
 - apply andimm_sound; auto.
 - apply notint_sound; apply and_sound; auto.
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index c56a9649..04081158 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -70,6 +70,7 @@ Inductive operation : Type :=
   | Oneg                     (**r [rd = - r1]   *)                     
   | Osub                     (**r [rd = r1 - r2] *)
   | Omul                     (**r [rd = r1 * r2] *)
+  | Omulimm (n: int)         (**r [rd = r1 * n] *)
   | Omulhs                   (**r [rd = high part of r1 * r2, signed] *)
   | Omulhu                   (**r [rd = high part of r1 * r2, unsigned] *)
   | Odiv                     (**r [rd = r1 / r2] (signed) *)
@@ -268,6 +269,7 @@ Definition eval_operation
   | Oneg, v1 :: nil => Some (Val.neg v1)
   | Osub, v1 :: v2 :: nil => Some (Val.sub v1 v2)
   | 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)
   | Omulhu, v1::v2::nil => Some (Val.mulhu v1 v2)
   | Odiv, v1 :: v2 :: nil => Val.divs v1 v2
@@ -456,6 +458,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Oneg => (Tint :: nil, Tint)
   | Osub => (Tint :: Tint :: nil, Tint)
   | Omul => (Tint :: Tint :: nil, Tint)
+  | Omulimm _ => (Tint :: nil, Tint)
   | Omulhs => (Tint :: Tint :: nil, Tint)
   | Omulhu => (Tint :: Tint :: nil, Tint)
   | Odiv => (Tint :: Tint :: nil, Tint)
@@ -623,8 +626,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* neg, sub *)
   - destruct v0...
   - unfold Val.sub. destruct v0; destruct v1... 
-  (* mul, mulhs, mulhu *)
+  (* mul, mulimm, mulhs, mulhu *)
   - destruct v0; destruct v1...
+  - destruct v0...
   - destruct v0; destruct v1...
   - destruct v0; destruct v1...
   (* div, divu *)
@@ -1124,8 +1128,9 @@ Proof.
   (* neg, sub *)
   - inv H4; simpl; auto.
   - apply Val.sub_inject; auto.
-  (* mul, mulhs, mulhu *)
+  (* mul, mulimm, mulhs, mulhu *)
   - inv H4; inv H2; simpl; auto.
+  - inv H4; simpl; auto.
   - inv H4; inv H2; simpl; auto.
   - inv H4; inv H2; simpl; auto.
   (* div, divu *)
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index f7702a9d..e1948a03 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -95,6 +95,7 @@ let arith_rrr_str = function
 let arith_rri32_str = function
   | Pcompiw it -> "Pcompiw"
   | Paddiw -> "Paddiw"
+  | Pmuliw -> "Pmuliw"
   | Pandiw -> "Pandiw"
   | Pnandiw -> "Pnandiw"
   | Poriw -> "Poriw"
@@ -114,6 +115,7 @@ let arith_rri32_str = function
 let arith_rri64_str = function
   | Pcompil it -> "Pcompil"
   | Paddil -> "Paddil"
+  | Pmulil -> "Pmulil"
   | Pandil -> "Pandil"
   | Pnandil -> "Pnandil"
   | Poril -> "Poril"
@@ -437,8 +439,8 @@ let ab_inst_to_real = function
   | "Pcompl" | "Pcompil" -> Compd
   | "Pfcompw" -> Fcompw
   | "Pfcompl" -> Fcompd
-  | "Pmulw" -> Mulw
-  | "Pmull" -> Muld
+  | "Pmulw" | "Pmuliw" -> Mulw
+  | "Pmull" | "Pmulil" -> Muld
   | "Porw" | "Poriw" -> Orw
   | "Pnorw" | "Pnoriw" -> Norw
   | "Porl" | "Poril" -> Ord
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 5c5d6c79..69824852 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -442,6 +442,8 @@ 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
+      | Pmuliw (rd, rs, imm) ->
+         fprintf oc "	mulw	%a = %a, %a\n" ireg rd ireg rs coqint imm
       | Pandiw (rd, rs, imm) ->
          fprintf oc "	andw	%a = %a, %a\n" ireg rd ireg rs coqint imm
       | Pnandiw (rd, rs, imm) ->
@@ -481,6 +483,8 @@ 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
+      | 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;
          fprintf oc "	andd	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
       | Pnandil (rd, rs, imm) -> assert Archi.ptr64;
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index a92358ca..3bb25807 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -57,6 +57,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Oneg, v1::nil => neg v1
   | Osub, v1::v2::nil => sub v1 v2
   | Omul, v1::v2::nil => mul v1 v2
+  | Omulimm n, v1::nil => mul v1 (I n)
   | Omulhs, v1::v2::nil => mulhs v1 v2
   | Omulhu, v1::v2::nil => mulhu v1 v2
   | Odiv, v1::v2::nil => divs v1 v2
diff --git a/test/monniaux/madd/madd.c b/test/monniaux/madd/madd.c
index e1e5eeb7..f847edf3 100644
--- a/test/monniaux/madd/madd.c
+++ b/test/monniaux/madd/madd.c
@@ -2,6 +2,10 @@ unsigned madd(unsigned a, unsigned b, unsigned c) {
   return a + b*c;
 }
 
+unsigned maddimm(unsigned a, unsigned b) {
+  return a + b*17113;
+}
+
 unsigned madd2(unsigned a, unsigned b, unsigned c) {
   return c + b*a;
 }
-- 
cgit 


From 9adb576998f3b2017db5c062b459449e1721579a Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 19 Mar 2019 21:31:20 +0100
Subject: mul immediate

---
 mppa_k1c/Asmblockgen.v   | 8 ++++++++
 mppa_k1c/NeedOp.v        | 1 +
 mppa_k1c/Op.v            | 5 +++++
 mppa_k1c/SelectOp.vp     | 2 +-
 mppa_k1c/SelectOpproof.v | 4 ++--
 mppa_k1c/ValueAOp.v      | 1 +
 6 files changed, 18 insertions(+), 3 deletions(-)

diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 1646ff94..ba01883d 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -85,6 +85,7 @@ Definition opimm32 (op: arith_name_rrr)
   end.
 
 Definition addimm32 := opimm32 Paddw Paddiw.
+Definition mulimm32 := opimm32 Pmulw Pmuliw.
 Definition andimm32 := opimm32 Pandw Pandiw.
 Definition nandimm32 := opimm32 Pnandw Pnandiw.
 Definition orimm32  := opimm32 Porw Poriw.
@@ -109,6 +110,7 @@ Definition opimm64 (op: arith_name_rrr)
 end.
 
 Definition addimm64 := opimm64 Paddl Paddil.
+Definition mulimm64 := opimm64 Pmull Pmulil.
 Definition orimm64  := opimm64 Porl  Poril.
 Definition andimm64 := opimm64 Pandl Pandil.
 Definition xorimm64 := opimm64 Pxorl  Pxoril.
@@ -420,6 +422,9 @@ Definition transl_op
   | 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)
+  | Omulimm n, a1 :: nil =>
+      do rd <- ireg_of res; do rs1 <- ireg_of a1;
+      OK (mulimm32 rd rs1 n ::i k)
   | Omulhs, _ => Error(msg "Asmblockgen.transl_op: Omulhs") (* Normalement pas émis *)
   | Omulhu, _ => Error(msg "Asmblockgen.transl_op: Omulhu") (* Normalement pas émis *)
   | Odiv, a1 :: a2 :: nil => Error(msg "Asmblockgen.transl_op: Odiv: 32-bits division not supported yet. Please use 64-bits.")
@@ -546,6 +551,9 @@ Definition transl_op
   | 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)
+  | Omullimm n, a1 :: nil =>
+      do rd <- ireg_of res; do rs1 <- ireg_of a1;
+      OK (mulimm64 rd rs1 n ::i k)
   | Omullhs, _ => Error (msg "Asmblockgen.transl_op: Omullhs") (* Normalement pas émis *)
   | Omullhu, _ => Error (msg "Asmblockgen.transl_op: Omullhu") (* Normalement pas émis *)
   | Odivl, _ => Error (msg "Asmblockgen.transl_op: Odivl") (* Géré par fonction externe *)
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index c7b59a34..68f43894 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -81,6 +81,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Onegl => op1 (default nv)
   | Osubl => op2 (default nv)
   | Omull => op2 (default nv)
+  | Omullimm _ => op1 (default nv)
   | Omullhs | Omullhu | Odivl | Odivlu | Omodl | Omodlu => op2 (default nv)
   | Oandl => op2 (default nv)
   | Oandlimm n => op1 (default nv)
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 04081158..0e9a7af9 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -115,6 +115,7 @@ Inductive operation : Type :=
   | Onegl                    (**r [rd = - r1] *)
   | Osubl                    (**r [rd = r1 - r2] *)
   | Omull                    (**r [rd = r1 * r2] *)
+  | Omullimm (n: int64)      (**r [rd = r1 * n] *)
   | Omullhs                  (**r [rd = high part of r1 * r2, signed] *)
   | Omullhu                  (**r [rd = high part of r1 * r2, unsigned] *)
   | Odivl                    (**r [rd = r1 / r2] (signed) *)
@@ -314,6 +315,7 @@ Definition eval_operation
   | Onegl, v1::nil => Some (Val.negl v1)
   | Osubl, v1::v2::nil => Some (Val.subl v1 v2)
   | 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)
   | Omullhu, v1::v2::nil => Some (Val.mullhu v1 v2)
   | Odivl, v1::v2::nil => Val.divls v1 v2
@@ -503,6 +505,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Onegl => (Tlong :: nil, Tlong)
   | Osubl => (Tlong :: Tlong :: nil, Tlong)
   | Omull => (Tlong :: Tlong :: nil, Tlong)
+  | Omullimm _ => (Tlong :: nil, Tlong)
   | Omullhs => (Tlong :: Tlong :: nil, Tlong)
   | Omullhu => (Tlong :: Tlong :: nil, Tlong)
   | Odivl => (Tlong :: Tlong :: nil, Tlong)
@@ -700,6 +703,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
     destruct (eq_block b b0)...
   (* mull, mullhs, mullhu *)
   - destruct v0; destruct v1...
+  - destruct v0...
   - destruct v0; destruct v1...
   - destruct v0; destruct v1...
   (* divl, divlu *)
@@ -1205,6 +1209,7 @@ Proof.
   - apply Val.subl_inject; auto.
   (* mull, mullhs, mullhu *)
   - inv H4; inv H2; simpl; auto.
+  - inv H4; simpl; auto.
   - inv H4; inv H2; simpl; auto.
   - inv H4; inv H2; simpl; auto.
   (* divl, divlu *)
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 22211167..d87c837e 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -173,7 +173,7 @@ Definition mulimm_base (n1: int) (e2: expr) :=
   | i :: j :: nil =>
       Elet e2 (add (shlimm (Eletvar 0) i) (shlimm (Eletvar 0) j))
   | _ =>
-      Eop Omul (Eop (Ointconst n1) Enil ::: e2 ::: Enil)
+      Eop (Omulimm n1) (e2 ::: Enil)
   end.
 
 Nondetfunction mulimm (n1: int) (e2: expr) :=
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index fe678383..a8889430 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -301,7 +301,7 @@ Proof.
   generalize (Int.one_bits_decomp n).
   generalize (Int.one_bits_range n).
   destruct (Int.one_bits n).
-  - intros. auto.
+  - intros. TrivialExists.
   - destruct l.
     + intros. rewrite H1. simpl.
       rewrite Int.add_zero.
@@ -319,7 +319,7 @@ Proof.
       rewrite Val.mul_add_distr_r.
       repeat rewrite Val.shl_mul. eapply Val.lessdef_trans. 2: eauto. apply Val.add_lessdef; auto.
       simpl. repeat rewrite H0; auto with coqlib.
-      intros. auto.
+      intros. TrivialExists.
 Qed.
 
 Theorem eval_mulimm:
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index 3bb25807..b43c4d78 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -101,6 +101,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Onegl, v1::nil => negl v1
   | Osubl, v1::v2::nil => subl v1 v2
   | Omull, v1::v2::nil => mull v1 v2
+  | Omullimm n, v1::nil => mull v1 (L n)
   | Omullhs, v1::v2::nil => mullhs v1 v2
   | Omullhu, v1::v2::nil => mullhu v1 v2
   | Odivl, v1::v2::nil => divls v1 v2
-- 
cgit 


From 2af07d6a328f73a32bc2c768e3108dd3db393ed1 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 19 Mar 2019 21:50:25 +0100
Subject: mul+madd immediate

---
 mppa_k1c/Asmblockgen.v               | 19 ++++++++++++++++++-
 mppa_k1c/PostpassSchedulingOracle.ml |  2 +-
 mppa_k1c/SelectOp.vp                 |  4 ++++
 mppa_k1c/SelectOpproof.v             |  6 +++++-
 4 files changed, 28 insertions(+), 3 deletions(-)

diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index ba01883d..80b712e3 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -524,6 +524,11 @@ Definition transl_op
       do r2 <- ireg_of a2;
       do r3 <- ireg_of a3;
         OK (Pmaddw r1 r2 r3 ::i k)
+  | Omaddimm n, a1 :: a2 :: nil =>
+    assertion (mreg_eq a1 res);
+      do r1 <- ireg_of a1;
+      do r2 <- ireg_of a2;
+        OK (Pmaddiw r1 r2 n ::i k)
   (* [Omakelong], [Ohighlong]  should not occur *)
   | Olowlong, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
@@ -636,7 +641,19 @@ Definition transl_op
           Psrlil RTMP RTMP (Int.sub Int64.iwordsize' n) ::i
           Paddl RTMP rs RTMP ::i
           Psrail rd RTMP n ::i k)
-
+         (* FIXME
+  | Omaddl, 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 (Pmaddl r1 r2 r3 ::i k)
+  | Omaddlimm n, a1 :: a2 :: nil =>
+    assertion (mreg_eq a1 res);
+      do r1 <- ireg_of a1;
+      do r2 <- ireg_of a2;
+        OK (Pmaddil r1 r2 n ::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/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index e1948a03..f4732ee4 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -453,7 +453,7 @@ let ab_inst_to_real = function
   | "Psrll" | "Psrlil" -> Srld
   | "Psllw" | "Pslliw" -> Sllw
   | "Proriw" -> Rorw
-  | "Pmaddw" -> Maddw
+  | "Pmaddw" | "Pmaddiw" -> Maddw
   | "Pslll" | "Psllil" -> Slld
   | "Pxorw" | "Pxoriw" -> Xorw
   | "Pnxorw" | "Pnxoriw" -> Nxorw
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index d87c837e..e4d65ced 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -90,6 +90,10 @@ Nondetfunction add (e1: expr) (e2: expr) :=
       Eop Omadd (t1:::t2:::t3:::Enil)
   | (Eop Omul (t2:::t3:::Enil)), t1 =>
       Eop Omadd (t1:::t2:::t3:::Enil)
+  | 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 Oadd (e1:::e2:::Enil)
   end.
 
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index a8889430..94d162a2 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -184,7 +184,11 @@ Proof.
     repeat rewrite Val.add_assoc. reflexivity.
   - (* Omadd *)
     subst. TrivialExists.
-  - (* Omadd *)
+  - (* Omadd rev *)
+    subst. rewrite Val.add_commut. TrivialExists.
+  - (* Omaddimm *)
+    subst. TrivialExists.
+  - (* Omaddimm rev *)
     subst. rewrite Val.add_commut. TrivialExists.
   - TrivialExists.
 Qed.
-- 
cgit