1 files changed, 14 insertions, 27 deletions
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index d81328b..4cd09d1 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -272,33 +272,20 @@ Definition mod_aux (divop: operation) (e1 e2: expr) :=
                            Enil) :::
                  Enil))).
 
-Definition divs (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
-
-Definition mods := mod_aux Odiv.
-
-Definition divuimm (e: expr) (n: int) :=
-  match Int.is_power2 n with
-  | Some l => shruimm e l
-  | None   => Eop Odivu (e ::: Eop (Ointconst n) Enil ::: Enil)
-  end.
-
-Nondetfunction divu (e1: expr) (e2: expr) :=
-  match e2 with
-  | Eop (Ointconst n2) Enil => divuimm e1 n2
-  | _ => Eop Odivu (e1:::e2:::Enil)
-  end.
-
-Definition moduimm (e: expr) (n: int) :=
-  match Int.is_power2 n with
-  | Some l => Eop (Oandimm (Int.sub n Int.one)) (e ::: Enil)
-  | None   => mod_aux Odivu e (Eop (Ointconst n) Enil)
-  end.
-
-Nondetfunction modu (e1: expr) (e2: expr) :=
-  match e2 with
-  | Eop (Ointconst n2) Enil => moduimm e1 n2
-  | _ => mod_aux Odivu e1 e2
-  end.
+Definition divs_base (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
+Definition mods_base := mod_aux Odiv.
+Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil).
+Definition modu_base := mod_aux Odivu.
+
+Definition shrximm (e1: expr) (n2: int) :=
+  if Int.eq n2 Int.zero
+  then e1
+  else Elet e1
+         (shrimm
+             (add (Eletvar O)
+                  (shruimm (shrimm (Eletvar O) (Int.repr 31))
+                           (Int.sub Int.iwordsize n2)))
+             n2).
 
 (** ** General shifts *)