more integer Op

4 files changed, 245 insertions, 17 deletions

diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v
index cd8c6606..6e0efe28 100644
--- a/mppa_k1c/Machregs.v
+++ b/mppa_k1c/Machregs.v
@@ -213,7 +213,10 @@ Global Opaque
 
 Definition two_address_op (op: operation) : bool :=
   match op with
-  | Omadd | Omaddimm _ | Omaddl | Omaddlimm _
+  | Omadd | Omaddimm _
+  | Omaddl | Omaddlimm _
+  | Omsub | Omsubimm _
+  | Omsubl | Omsublimm _
   | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _
   | Oinsf _ _ | Oinsfl _ _ => true
   | _ => false
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index c10f5c56..ced31758 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -42,8 +42,13 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Ocast16signed => op1 (sign_ext 16 nv)
   | Oadd => op2 (modarith nv)
   | Oaddimm n => op1 (modarith nv)
+  | Oaddx _ => op2 (default nv)
+  | Oaddximm _ _ => op1 (default nv)
   | Oneg => op1 (modarith nv)
   | Osub => op2 (default nv)
+  | Orevsubimm _ => op1 (default nv)
+  | Orevsubx _ => op2 (default nv)
+  | Orevsubximm _ _ => op1 (default nv)
   | Omul => op2 (modarith nv)
   | Omulimm _ => op1 (modarith nv)
   | Omulhs | Omulhu | Odiv | Odivu | Omod | Omodu => op2 (default nv)
@@ -72,12 +77,19 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Oshrximm n => op1 (default nv)
   | Omadd => op3 (modarith nv)
   | Omaddimm n => op2 (modarith nv)
+  | Omsub => op3 (modarith nv)
+  | Omsubimm n => op2 (modarith nv)
   | Omakelong => op2 (default nv)
   | Olowlong | Ohighlong => op1 (default nv)
   | Ocast32signed => op1 (default nv)
   | Ocast32unsigned => op1 (default nv)
   | Oaddl => op2 (default nv)
   | Oaddlimm n => op1 (default nv)
+  | Oaddxl _ => op2 (default nv)
+  | Oaddxlimm _ _ => op1 (default nv)
+  | Orevsublimm _ => op1 (default nv)
+  | Orevsubxl _ => op2 (default nv)
+  | Orevsubxlimm _ _ => op1 (default nv)
   | Onegl => op1 (default nv)
   | Osubl => op2 (default nv)
   | Omull => op2 (default nv)
@@ -107,6 +119,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Oshrxlimm n => op1 (default nv)
   | Omaddl => op3 (default nv)
   | Omaddlimm n => op2 (default nv)
+  | Omsubl => op3 (default nv)
+  | Omsublimm n => op2 (default nv)
   | Onegf | Oabsf => op1 (default nv)
   | Oaddf | Osubf | Omulf | Odivf => op2 (default nv)
   | Onegfs | Oabsfs => op1 (default nv)
@@ -229,6 +243,26 @@ Proof.
   - apply Val.addl_lessdef; trivial.
 Qed.
 
+Lemma subl_lessdef:
+  forall v1 v1' v2 v2',
+  Val.lessdef v1 v1' -> Val.lessdef v2 v2' -> Val.lessdef (Val.subl v1 v2) (Val.subl v1' v2').
+Proof.
+  intros. inv H. inv H0. auto. destruct v1'; simpl; auto. simpl; auto.
+Qed.
+
+Lemma subl_sound:
+  forall v1 w1 v2 w2 x,
+  vagree v1 w1 (default x) -> vagree v2 w2 (default x) ->
+  vagree (Val.subl v1 v2) (Val.subl w1 w2) x.
+Proof.
+  unfold default; intros.
+  destruct x; simpl in *; trivial.
+  - unfold Val.subl.
+    destruct v1; destruct v2; trivial; destruct Archi.ptr64; simpl; trivial.
+    destruct (eq_block _ _) ; simpl; trivial.
+  - apply subl_lessdef; trivial.
+Qed.
+
 
 Lemma mull_sound:
   forall v1 w1 v2 w2 x,
@@ -424,6 +458,14 @@ Proof.
   destruct nv; simpl; trivial.
 Qed.
 
+Remark sub_add_neg :
+  forall x y, Val.sub x y = Val.add x (Val.neg y).
+Proof.
+  destruct x; destruct y; simpl; trivial.
+  f_equal.
+  apply Int.sub_add_opp.
+Qed.
+  
 Lemma needs_of_operation_sound:
   forall op args v nv args',
   eval_operation ge (Vptr sp Ptrofs.zero) op args m1 = Some v ->
@@ -466,11 +508,29 @@ Proof.
   (* madd *)
 - apply add_sound; try apply mul_sound; auto with na; rewrite modarith_idem; assumption.
 - apply add_sound; try apply mul_sound; auto with na; rewrite modarith_idem; assumption.
+- repeat rewrite sub_add_neg.
+  apply add_sound; trivial.
+  apply neg_sound; trivial.
+  rewrite modarith_idem.
+  apply mul_sound;
+  rewrite modarith_idem; trivial.
+- repeat rewrite sub_add_neg.
+  apply add_sound; trivial.
+  apply neg_sound; trivial.
+  rewrite modarith_idem.
+  apply mul_sound;
+  rewrite modarith_idem; trivial.
+  apply vagree_same.
   (* maddl *)
 - apply addl_sound; trivial.
   apply mull_sound; trivial.
   rewrite default_idem; trivial.
   rewrite default_idem; trivial.
+  (* msubl *)
+- apply subl_sound; trivial.
+  apply mull_sound; trivial.
+  rewrite default_idem; trivial.
+  rewrite default_idem; trivial.
   (* select *)
 - apply select_sound; trivial.
   (* selectl *)
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 5e80589b..b93a9fc3 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -66,6 +66,20 @@ Definition arg_type_of_condition0 (cond: condition0) :=
 (** Arithmetic and logical operations.  In the descriptions, [rd] is the
   result of the operation and [r1], [r2], etc, are the arguments. *)
 
+Inductive shift1_4 : Type :=
+| SHIFT1 | SHIFT2 | SHIFT3 | SHIFT4.
+
+Definition z_of_shift1_4 (x : shift1_4) :=
+  match x with
+  | SHIFT1 => 1
+  | SHIFT2 => 2
+  | SHIFT3 => 3
+  | SHIFT4 => 4
+  end.
+
+Definition int_of_shift1_4 (x : shift1_4) :=
+  Int.repr (z_of_shift1_4 x).
+
 Inductive operation : Type :=
   | Omove                    (**r [rd = r1] *)
   | Ointconst (n: int)       (**r [rd] is set to the given integer constant *)
@@ -79,8 +93,13 @@ Inductive operation : Type :=
   | Ocast16signed            (**r [rd] is 16-bit sign extension of [r1] *)
   | Oadd                     (**r [rd = r1 + r2] *)
   | Oaddimm (n: int)         (**r [rd = r1 + n] *)
+  | Oaddx (shift: shift1_4)         (**r [rd = r1 << shift + r2] *)
+  | Oaddximm (shift: shift1_4) (n: int) (**r [rd = r1 << shift + n] *)
   | Oneg                     (**r [rd = - r1]   *)                     
   | Osub                     (**r [rd = r1 - r2] *)
+  | Orevsubimm (n: int)      (**r [rd = n - r1] *)
+  | Orevsubx (shift: shift1_4)         (**r [rd = r2 -r1 << shift] *)
+  | Orevsubximm (shift: shift1_4) (n: int) (**r [rd = n -r1 << shift] *)
   | Omul                     (**r [rd = r1 * r2] *)
   | Omulimm (n: int)         (**r [rd = r1 * n] *)
   | Omulhs                   (**r [rd = high part of r1 * r2, signed] *)
@@ -116,6 +135,8 @@ Inductive operation : Type :=
   | Ororimm (n: int)         (**r rotate right immediate *)
   | Omadd                    (**r [rd = rd + r1 * r2] *)
   | Omaddimm (n: int)        (**r [rd = rd + r1 * imm] *)
+  | Omsub                    (**r [rd = rd - r1 * r2] *)
+  | Omsubimm (n: int)        (**r [rd = rd - r1 * imm] *)
 (*c 64-bit integer arithmetic: *)
   | Omakelong                (**r [rd = r1 << 32 | r2] *)
   | Olowlong                 (**r [rd = low-word(r1)] *)
@@ -124,6 +145,11 @@ Inductive operation : Type :=
   | Ocast32unsigned          (**r [rd] is 32-bit zero extension of [r1] *)
   | Oaddl                    (**r [rd = r1 + r2] *)
   | Oaddlimm (n: int64)      (**r [rd = r1 + n] *)
+  | Oaddxl (shift: shift1_4)         (**r [rd = r1 << shift + r2] *)
+  | Oaddxlimm (shift: shift1_4) (n: int64) (**r [rd = r1 << shift + n] *)
+  | Orevsublimm (n: int64)      (**r [rd = n - r1] *)
+  | Orevsubxl (shift: shift1_4)         (**r [rd = r2 -r1 << shift] *)
+  | Orevsubxlimm (shift: shift1_4) (n: int64) (**r [rd = n -r1 << shift] *)
   | Onegl                    (**r [rd = - r1] *)
   | Osubl                    (**r [rd = r1 - r2] *)
   | Omull                    (**r [rd = r1 * r2] *)
@@ -160,6 +186,8 @@ Inductive operation : Type :=
   | Oshrxlimm (n: int)       (**r [rd = r1 / 2^n] (signed) *)
   | Omaddl                   (**r [rd = rd + r1 * r2] *)
   | Omaddlimm (n: int64)     (**r [rd = rd + r1 * imm] *)
+  | Omsubl                   (**r [rd = rd - r1 * r2] *)
+  | Omsublimm (n: int64)     (**r [rd = rd - r1 * imm] *)
 (*c Floating-point arithmetic: *)
   | Onegf                    (**r [rd = - r1] *)
   | Oabsf                    (**r [rd = abs(r1)] *)
@@ -235,9 +263,14 @@ Proof.
   decide equality.
 Defined.
 
+Definition eq_shift1_4 (x y : shift1_4): {x=y} + {x<>y}.
+Proof.
+  decide equality.
+Defined.
+
 Definition eq_operation: forall (x y: operation), {x=y} + {x<>y}.
 Proof.
-  generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition eq_condition0 Z.eq_dec; intros.
+  generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition eq_condition0 Z.eq_dec eq_shift1_4; intros.
   decide equality.
 Defined.
 
@@ -386,8 +419,13 @@ Definition eval_operation
   | Ocast16signed, v1 :: nil => Some (Val.sign_ext 16 v1)
   | Oadd, v1 :: v2 :: nil => Some (Val.add v1 v2)
   | Oaddimm n, v1 :: nil => Some (Val.add v1 (Vint n))
+  | Oaddx shift, v1 :: v2 :: nil => Some (Val.add (Val.shl v1 (Vint (int_of_shift1_4 shift))) v2)
+  | Oaddximm shift n, v1 :: nil => Some (Val.add (Val.shl v1 (Vint (int_of_shift1_4 shift))) (Vint n))
   | Oneg, v1 :: nil => Some (Val.neg v1)
   | Osub, v1 :: v2 :: nil => Some (Val.sub v1 v2)
+  | Orevsubimm n, v1 :: nil => Some (Val.sub (Vint n) v1)
+  | Orevsubx shift, v1 :: v2 :: nil => Some (Val.sub v2 (Val.shl v1 (Vint (int_of_shift1_4 shift))))
+  | Orevsubximm shift n, v1 :: nil => Some (Val.sub (Vint n) (Val.shl v1 (Vint (int_of_shift1_4 shift))))
   | Omul, v1 :: v2 :: nil => Some (Val.mul v1 v2)
   | Omulimm n, v1 :: nil => Some (Val.mul v1 (Vint n))
   | Omulhs, v1::v2::nil => Some (Val.mulhs v1 v2)
@@ -423,6 +461,8 @@ Definition eval_operation
   | Oshrximm n, v1::nil => Val.shrx v1 (Vint n)
   | Omadd, v1::v2::v3::nil => Some (Val.add v1 (Val.mul v2 v3))
   | (Omaddimm n), v1::v2::nil => Some (Val.add v1 (Val.mul v2 (Vint n)))
+  | Omsub, v1::v2::v3::nil => Some (Val.sub v1 (Val.mul v2 v3))
+  | (Omsubimm n), v1::v2::nil => Some (Val.sub v1 (Val.mul v2 (Vint n)))
                                      
   | Omakelong, v1::v2::nil => Some (Val.longofwords v1 v2)
   | Olowlong, v1::nil => Some (Val.loword v1)
@@ -431,8 +471,13 @@ Definition eval_operation
   | Ocast32unsigned, v1 :: nil => Some (Val.longofintu v1)
   | Oaddl, v1 :: v2 :: nil => Some (Val.addl v1 v2)
   | Oaddlimm n, v1::nil => Some (Val.addl v1 (Vlong n))
+  | Oaddxl shift, v1 :: v2 :: nil => Some (Val.addl (Val.shll v1 (Vint (int_of_shift1_4 shift))) v2)
+  | Oaddxlimm shift n, v1 :: nil => Some (Val.addl (Val.shll v1 (Vint (int_of_shift1_4 shift))) (Vlong n))
   | Onegl, v1::nil => Some (Val.negl v1)
   | Osubl, v1::v2::nil => Some (Val.subl v1 v2)
+  | Orevsublimm n, v1 :: nil => Some (Val.subl (Vlong n) v1)
+  | Orevsubxl shift, v1 :: v2 :: nil => Some (Val.subl v2 (Val.shll v1 (Vint (int_of_shift1_4 shift))))
+  | Orevsubxlimm shift n, v1 :: nil => Some (Val.subl (Vlong n) (Val.shll v1 (Vint (int_of_shift1_4 shift))))
   | Omull, v1::v2::nil => Some (Val.mull v1 v2)
   | Omullimm n, v1::nil => Some (Val.mull v1 (Vlong n))
   | Omullhs, v1::v2::nil => Some (Val.mullhs v1 v2)
@@ -467,6 +512,8 @@ Definition eval_operation
   | Oshrxlimm n, v1::nil => Val.shrxl v1 (Vint n)
   | Omaddl, v1::v2::v3::nil => Some (Val.addl v1 (Val.mull v2 v3))
   | (Omaddlimm n), v1::v2::nil => Some (Val.addl v1 (Val.mull v2 (Vlong n)))
+  | Omsubl, v1::v2::v3::nil => Some (Val.subl v1 (Val.mull v2 v3))
+  | (Omsublimm n), v1::v2::nil => Some (Val.subl v1 (Val.mull v2 (Vlong n)))
                                       
   | Onegf, v1::nil => Some (Val.negf v1)
   | Oabsf, v1::nil => Some (Val.absf v1)
@@ -583,8 +630,13 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Ocast16signed => (Tint :: nil, Tint)
   | Oadd => (Tint :: Tint :: nil, Tint)
   | Oaddimm _ => (Tint :: nil, Tint)
+  | Oaddx _ => (Tint :: Tint :: nil, Tint)
+  | Oaddximm _ _ => (Tint :: nil, Tint)
   | Oneg => (Tint :: nil, Tint)
   | Osub => (Tint :: Tint :: nil, Tint)
+  | Orevsubimm _ => (Tint :: nil, Tint)
+  | Orevsubx _ => (Tint :: Tint :: nil, Tint)
+  | Orevsubximm _ _ => (Tint :: nil, Tint)
   | Omul => (Tint :: Tint :: nil, Tint)
   | Omulimm _ => (Tint :: nil, Tint)
   | Omulhs => (Tint :: Tint :: nil, Tint)
@@ -620,6 +672,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Ororimm _ => (Tint :: nil, Tint)
   | Omadd => (Tint :: Tint :: Tint :: nil, Tint)
   | Omaddimm _ => (Tint :: Tint :: nil, Tint)
+  | Omsub => (Tint :: Tint :: Tint :: nil, Tint)
+  | Omsubimm _ => (Tint :: Tint :: nil, Tint)
                    
   | Omakelong => (Tint :: Tint :: nil, Tlong)
   | Olowlong => (Tlong :: nil, Tint)
@@ -628,6 +682,11 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Ocast32unsigned => (Tint :: nil, Tlong)
   | Oaddl => (Tlong :: Tlong :: nil, Tlong)
   | Oaddlimm _ => (Tlong :: nil, Tlong)
+  | Oaddxl _ => (Tlong :: Tlong :: nil, Tlong)
+  | Oaddxlimm _ _ => (Tlong :: nil, Tlong)
+  | Orevsublimm _ => (Tlong :: nil, Tlong)
+  | Orevsubxl _ => (Tlong :: Tlong :: nil, Tlong)
+  | Orevsubxlimm _ _ => (Tlong :: nil, Tlong)
   | Onegl => (Tlong :: nil, Tlong)
   | Osubl => (Tlong :: Tlong :: nil, Tlong)
   | Omull => (Tlong :: Tlong :: nil, Tlong)
@@ -664,6 +723,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Oshrxlimm _ => (Tlong :: nil, Tlong)
   | Omaddl => (Tlong :: Tlong :: Tlong :: nil, Tlong)
   | Omaddlimm _ => (Tlong :: Tlong :: nil, Tlong)
+  | Omsubl => (Tlong :: Tlong :: Tlong :: nil, Tlong)
+  | Omsublimm _ => (Tlong :: Tlong :: nil, Tlong)
 
   | Onegf => (Tfloat :: nil, Tfloat)
   | Oabsf => (Tfloat :: nil, Tfloat)
@@ -736,6 +797,32 @@ Proof.
   intros. unfold Val.has_type, Val.addl. destruct Archi.ptr64, v1, v2; auto.
 Qed.
 
+Remark type_sub:
+  forall v1 v2, Val.has_type (Val.sub v1 v2) Tint.
+Proof.
+  intros. unfold Val.has_type, Val.sub. destruct Archi.ptr64, v1, v2; simpl; auto.
+  destruct (eq_block _ _); auto.
+Qed.
+
+Remark type_subl:
+  forall v1 v2, Val.has_type (Val.subl v1 v2) Tlong.
+Proof.
+  intros. unfold Val.has_type, Val.subl. destruct Archi.ptr64, v1, v2; simpl; auto.
+  destruct (eq_block _ _); auto.
+Qed.
+
+Remark type_shl:
+  forall v1 v2, Val.has_type (Val.shl v1 v2) Tint.
+Proof.
+  destruct v1, v2; simpl; trivial; destruct (Int.ltu _ _); simpl; trivial.
+Qed.
+
+Remark type_shll:
+  forall v1 v2, Val.has_type (Val.shll v1 v2) Tlong.
+Proof.
+  destruct v1, v2; simpl; trivial; destruct (Int.ltu _ _); simpl; trivial.
+Qed.
+
 Lemma type_of_operation_sound:
   forall op vl sp v m,
   op <> Omove ->
@@ -761,9 +848,17 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* add, addimm *)
   - apply type_add.
   - apply type_add.
+  (* addx, addximm *)
+  - apply type_add.
+  - apply type_add.
   (* neg, sub *)
   - destruct v0...
-  - unfold Val.sub. destruct v0; destruct v1... 
+  - apply type_sub.
+  (* revsubimm, revsubx, revsubximm *)
+  - destruct v0...
+  - apply type_sub.
+  - destruct v0; simpl; trivial.
+    destruct (Int.ltu _ _); simpl; trivial.
   (* mul, mulimm, mulhs, mulhu *)
   - destruct v0; destruct v1...
   - destruct v0...
@@ -819,8 +914,11 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* shrimm *)
   - destruct v0; simpl...   
   (* madd *)
-  - destruct v0; destruct v1; destruct v2...   
-  - destruct v0; destruct v1...
+  - apply type_add.
+  - apply type_add.
+  (* msub *)
+  - apply type_sub.
+  - apply type_sub.
   (* makelong, lowlong, highlong *)
   - destruct v0; destruct v1...
   - destruct v0...
@@ -831,11 +929,16 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* addl, addlimm *)
   - apply type_addl.
   - apply type_addl.
+  (* addxl addxlimm *)
+  - apply type_addl.
+  - apply type_addl.
   (* negl, subl *)
   - destruct v0...
-  - unfold Val.subl. destruct v0; destruct v1... 
-    unfold Val.has_type; destruct Archi.ptr64...
-    destruct (eq_block b b0)...
+  - apply type_subl.
+  - destruct v0; simpl; trivial.
+    destruct (Int.ltu _ _); simpl; trivial.
+  - destruct v0...
+  - apply type_subl.
   (* mull, mullhs, mullhu *)
   - destruct v0; destruct v1...
   - destruct v0...
@@ -889,10 +992,11 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* shrxl *)
   - destruct v0; simpl in H0; try discriminate. destruct (Int.ltu n (Int.repr 63)); inv H0...
   (* maddl, maddlim *)
-  - destruct v0; destruct v1; destruct v2; simpl; trivial.
-    destruct Archi.ptr64; simpl; trivial.
-  - destruct v0; destruct v1; simpl; trivial.
-    destruct Archi.ptr64; simpl; trivial.
+  - apply type_addl.
+  - apply type_addl.
+  (* msubl, msublim *)
+  - apply type_subl.
+  - apply type_subl.
   (* negf, absf *)
   - destruct v0...
   - destruct v0...
@@ -1359,9 +1463,19 @@ Proof.
   (* add, addimm *)
   - apply Val.add_inject; auto.
   - apply Val.add_inject; auto.
+  (* addx, addximm *)
+  - apply Val.add_inject; trivial.
+    inv H4; inv H2; simpl; try destruct (Int.ltu _ _); simpl; auto.
+  - apply Val.add_inject; trivial.
+    inv H4; simpl; try destruct (Int.ltu _ _); simpl; auto.
   (* neg, sub *)
   - inv H4; simpl; auto.
   - apply Val.sub_inject; auto.
+  (* revsubimm, revsubx, revsubximm *)
+  - inv H4; simpl; trivial.
+  - apply Val.sub_inject; trivial.
+    inv H4; inv H2; simpl; try destruct (Int.ltu _ _); simpl; auto.
+  - inv H4; simpl; try destruct (Int.ltu _ _); simpl; auto.
   (* mul, mulimm, mulhs, mulhu *)
   - inv H4; inv H2; simpl; auto.
   - inv H4; simpl; auto.
@@ -1424,6 +1538,11 @@ Proof.
   (* madd, maddim *)
   - inv H2; inv H3; inv H4; simpl; auto.
   - inv H2; inv H4; simpl; auto.
+  (* msub *)
+  - apply Val.sub_inject; auto.
+    inv H3; inv H2; simpl; auto.
+  - apply Val.sub_inject; trivial.
+    inv H2; inv H4; simpl; auto.
   (* makelong, highlong, lowlong *)
   - inv H4; inv H2; simpl; auto.
   - inv H4; simpl; auto.
@@ -1434,9 +1553,22 @@ Proof.
   (* addl, addlimm *)
   - apply Val.addl_inject; auto.
   - apply Val.addl_inject; auto.
+  (* addxl, addxlimm *)
+  - apply Val.addl_inject; auto.
+    inv H4; simpl; trivial.
+    destruct (Int.ltu _ _); simpl; trivial.
+  - apply Val.addl_inject; auto.
+    inv H4; simpl; trivial.
+    destruct (Int.ltu _ _); simpl; trivial.
   (* negl, subl *)
   - inv H4; simpl; auto.
   - apply Val.subl_inject; auto.
+    inv H4; inv H2; simpl; trivial;
+    destruct (Int.ltu _ _); simpl; trivial.
+  - inv H4; simpl; trivial;
+      destruct (Int.ltu _ _); simpl; trivial.
+  - inv H4; simpl; auto.
+  - apply Val.subl_inject; auto.
   (* mull, mullhs, mullhu *)
   - inv H4; inv H2; simpl; auto.
   - inv H4; simpl; auto.
@@ -1500,6 +1632,11 @@ Proof.
     inv H2; inv H3; inv H4; simpl; auto.
   - apply Val.addl_inject; auto.
     inv H4; inv H2; simpl; auto.
+  (* msubl, msublimm *)
+  - apply Val.subl_inject; auto.
+    inv H2; inv H3; inv H4; simpl; auto.
+  - apply Val.subl_inject; auto.
+    inv H4; inv H2; simpl; auto.
     
   (* negf, absf *)
   - inv H4; simpl; auto.
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index 643cca0c..27faa33c 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -161,8 +161,13 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Ocast16signed, v1 :: nil => sign_ext 16 v1
   | Oadd, v1::v2::nil => add v1 v2
   | Oaddimm n, v1::nil => add v1 (I n)
+  | Oaddx shift, v1::v2::nil => add (shl v1 (I (int_of_shift1_4 shift))) v2
+  | Oaddximm shift n, v1::nil => add (shl v1 (I (int_of_shift1_4 shift))) (I n)
   | Oneg, v1::nil => neg v1
   | Osub, v1::v2::nil => sub v1 v2
+  | Orevsubx shift, v1::v2::nil => sub v2 (shl v1 (I (int_of_shift1_4 shift)))
+  | Orevsubimm n, v1::nil => sub (I n) v1
+  | Orevsubximm shift n, v1::nil => sub (I n) (shl v1 (I (int_of_shift1_4 shift)))
   | Omul, v1::v2::nil => mul v1 v2
   | Omulimm n, v1::nil => mul v1 (I n)
   | Omulhs, v1::v2::nil => mulhs v1 v2
@@ -198,6 +203,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Oshrximm n, v1::nil => shrx v1 (I n)
   | Omadd, v1::v2::v3::nil => add v1 (mul v2 v3)
   | Omaddimm n, v1::v2::nil => add v1 (mul v2 (I n))
+  | Omsub, v1::v2::v3::nil => sub v1 (mul v2 v3)
+  | Omsubimm n, v1::v2::nil => sub v1 (mul v2 (I n))
   | Omakelong, v1::v2::nil => longofwords v1 v2
   | Olowlong, v1::nil => loword v1
   | Ohighlong, v1::nil => hiword v1
@@ -205,8 +212,13 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Ocast32unsigned, v1::nil => longofintu v1
   | Oaddl, v1::v2::nil => addl v1 v2
   | Oaddlimm n, v1::nil => addl v1 (L n)
+  | Oaddxl shift, v1::v2::nil => addl (shll v1 (I (int_of_shift1_4 shift))) v2
+  | Oaddxlimm shift n, v1::nil => addl (shll v1 (I (int_of_shift1_4 shift))) (L n)
   | Onegl, v1::nil => negl v1
   | Osubl, v1::v2::nil => subl v1 v2
+  | Orevsubxl shift, v1::v2::nil => subl v2 (shll v1 (I (int_of_shift1_4 shift)))
+  | Orevsublimm n, v1::nil => subl (L n) v1
+  | Orevsubxlimm shift n, v1::nil => subl (L n) (shll v1 (I (int_of_shift1_4 shift)))
   | Omull, v1::v2::nil => mull v1 v2
   | Omullimm n, v1::nil => mull v1 (L n)
   | Omullhs, v1::v2::nil => mullhs v1 v2
@@ -241,6 +253,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Oshrxlimm n, v1::nil => shrxl v1 (I n)
   | Omaddl, v1::v2::v3::nil => addl v1 (mull v2 v3)
   | Omaddlimm n, v1::v2::nil => addl v1 (mull v2 (L n))
+  | Omsubl, v1::v2::v3::nil => subl v1 (mull v2 v3)
+  | Omsublimm n, v1::v2::nil => subl v1 (mull v2 (L n))
   | Onegf, v1::nil => negf v1
   | Oabsf, v1::nil => absf v1
   | Oaddf, v1::v2::nil => addf v1 v2
@@ -360,11 +374,25 @@ Theorem eval_static_operation_sound:
   vmatch bc vres (eval_static_operation op aargs).
 Proof.
   unfold eval_operation, eval_static_operation, eval_static_select, eval_static_selectl, eval_static_selectf, eval_static_selectfs; intros;
-  destruct op; InvHyps; eauto with va.
-  destruct (propagate_float_constants tt); constructor.
-  destruct (propagate_float_constants tt); constructor.
-  rewrite Ptrofs.add_zero_l; eauto with va.
-  apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
+  destruct op; try (InvHyps; eauto with va).
+  - destruct (propagate_float_constants tt); constructor.
+  - destruct (propagate_float_constants tt); constructor.
+  - rewrite Ptrofs.add_zero_l; eauto with va.
+  - (*revsubimm*) inv H1; constructor.
+  - replace (match Val.shl a1 (Vint (int_of_shift1_4 shift)) with
+    | Vint n2 => Vint (Int.sub n n2)
+    | _ => Vundef
+             end) with (Val.sub (Vint n) (Val.shl a1 (Vint (int_of_shift1_4 shift)))).
+    eauto with va.
+    destruct a1; destruct shift; reflexivity.
+  - inv H1; constructor.
+  - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with
+    | Vlong n2 => Vlong (Int64.sub n n2)
+    | _ => Vundef
+             end) with (Val.subl (Vlong n) (Val.shll a1 (Vint (int_of_shift1_4 shift)))).
+    eauto with va.
+    destruct a1; destruct shift; reflexivity.
+  - apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
   (* select *)
   - assert (Hcond : (cmatch (eval_condition0 cond a2 m) (eval_static_condition0 cond b2))) by (apply eval_static_condition0_sound; assumption).
     rewrite eval_select_to2.