Added volatile_read_global and volatile_store_global builtins.

Finished updating IA32 and ARM ports.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1792 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

6 files changed, 759 insertions, 1973 deletions

diff --git a/arm/ConstpropOp.v b/arm/ConstpropOp.v
deleted file mode 100644
index 9e51e25..0000000
--- a/arm/ConstpropOp.v
+++ /dev/null
@@ -1,800 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  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.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Static analysis and strength reduction for operators 
-  and conditions.  This is the machine-dependent part of [Constprop]. *)
-
-Require Import Coqlib.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Op.
-Require Import Registers.
-
-(** * Static analysis *)
-
-(** To each pseudo-register at each program point, the static analysis 
-  associates a compile-time approximation taken from the following set. *)
-
-Inductive approx : Type :=
-  | Novalue: approx      (** No value possible, code is unreachable. *)
-  | Unknown: approx      (** All values are possible,
-                             no compile-time information is available. *)
-  | I: int -> approx     (** A known integer value. *)
-  | F: float -> approx   (** A known floating-point value. *)
-  | G: ident -> int -> approx
-                         (** The value is the address of the given global
-                             symbol plus the given integer offset. *)
-  | S: int -> approx.    (** The value is the stack pointer plus the offset. *)
-
-
-(** We now define the abstract interpretations of conditions and operators
-  over this set of approximations.  For instance, the abstract interpretation
-  of the operator [Oaddf] applied to two expressions [a] and [b] is
-  [F(Float.add f g)] if [a] and [b] have static approximations [F f]
-  and [F g] respectively, and [Unknown] otherwise.
-
-  The static approximations are defined by large pattern-matchings over
-  the approximations of the results.  We write these matchings in the
-  indirect style described in file [SelectOp] to avoid excessive
-  duplication of cases in proofs. *)
-
-Definition eval_static_shift (s: shift) (n: int) : int :=
-  match s with
-  | Slsl x => Int.shl n x
-  | Slsr x => Int.shru n x
-  | Sasr x => Int.shr n x
-  | Sror x => Int.ror n x
-  end.
-
-(** Original definition:
-<<
-Nondetfunction eval_static_condition (cond: condition) (vl: list approx) :=
-  match cond, vl with
-  | Ccomp c, I n1 :: I n2 :: nil => Some(Int.cmp c n1 n2)
-  | Ccompu c, I n1 :: I n2 :: nil => Some(Int.cmpu c n1 n2)
-  | Ccompshift c s, I n1 :: I n2 :: nil => Some(Int.cmp c n1 (eval_static_shift s n2))
-  | Ccompushift c s, I n1 :: I n2 :: nil => Some(Int.cmpu c n1 (eval_static_shift s n2))
-  | Ccompimm c n, I n1 :: nil => Some(Int.cmp c n1 n)
-  | Ccompuimm c n, I n1 :: nil => Some(Int.cmpu c n1 n)
-  | Ccompf c, F n1 :: F n2 :: nil => Some(Float.cmp c n1 n2)
-  | Cnotcompf c, F n1 :: F n2 :: nil => Some(negb(Float.cmp c n1 n2))
-  | _, _ => None
-  end.
->>
-*)
-
-Inductive eval_static_condition_cases: forall (cond: condition) (vl: list approx), Type :=
-  | eval_static_condition_case1: forall c n1 n2, eval_static_condition_cases (Ccomp c) (I n1 :: I n2 :: nil)
-  | eval_static_condition_case2: forall c n1 n2, eval_static_condition_cases (Ccompu c) (I n1 :: I n2 :: nil)
-  | eval_static_condition_case3: forall c s n1 n2, eval_static_condition_cases (Ccompshift c s) (I n1 :: I n2 :: nil)
-  | eval_static_condition_case4: forall c s n1 n2, eval_static_condition_cases (Ccompushift c s) (I n1 :: I n2 :: nil)
-  | eval_static_condition_case5: forall c n n1, eval_static_condition_cases (Ccompimm c n) (I n1 :: nil)
-  | eval_static_condition_case6: forall c n n1, eval_static_condition_cases (Ccompuimm c n) (I n1 :: nil)
-  | eval_static_condition_case7: forall c n1 n2, eval_static_condition_cases (Ccompf c) (F n1 :: F n2 :: nil)
-  | eval_static_condition_case8: forall c n1 n2, eval_static_condition_cases (Cnotcompf c) (F n1 :: F n2 :: nil)
-  | eval_static_condition_default: forall (cond: condition) (vl: list approx), eval_static_condition_cases cond vl.
-
-Definition eval_static_condition_match (cond: condition) (vl: list approx) :=
-  match cond as zz1, vl as zz2 return eval_static_condition_cases zz1 zz2 with
-  | Ccomp c, I n1 :: I n2 :: nil => eval_static_condition_case1 c n1 n2
-  | Ccompu c, I n1 :: I n2 :: nil => eval_static_condition_case2 c n1 n2
-  | Ccompshift c s, I n1 :: I n2 :: nil => eval_static_condition_case3 c s n1 n2
-  | Ccompushift c s, I n1 :: I n2 :: nil => eval_static_condition_case4 c s n1 n2
-  | Ccompimm c n, I n1 :: nil => eval_static_condition_case5 c n n1
-  | Ccompuimm c n, I n1 :: nil => eval_static_condition_case6 c n n1
-  | Ccompf c, F n1 :: F n2 :: nil => eval_static_condition_case7 c n1 n2
-  | Cnotcompf c, F n1 :: F n2 :: nil => eval_static_condition_case8 c n1 n2
-  | cond, vl => eval_static_condition_default cond vl
-  end.
-
-Definition eval_static_condition (cond: condition) (vl: list approx) :=
-  match eval_static_condition_match cond vl with
-  | eval_static_condition_case1 c n1 n2 => (* Ccomp c, I n1 :: I n2 :: nil *) 
-      Some(Int.cmp c n1 n2)
-  | eval_static_condition_case2 c n1 n2 => (* Ccompu c, I n1 :: I n2 :: nil *) 
-      Some(Int.cmpu c n1 n2)
-  | eval_static_condition_case3 c s n1 n2 => (* Ccompshift c s, I n1 :: I n2 :: nil *) 
-      Some(Int.cmp c n1 (eval_static_shift s n2))
-  | eval_static_condition_case4 c s n1 n2 => (* Ccompushift c s, I n1 :: I n2 :: nil *) 
-      Some(Int.cmpu c n1 (eval_static_shift s n2))
-  | eval_static_condition_case5 c n n1 => (* Ccompimm c n, I n1 :: nil *) 
-      Some(Int.cmp c n1 n)
-  | eval_static_condition_case6 c n n1 => (* Ccompuimm c n, I n1 :: nil *) 
-      Some(Int.cmpu c n1 n)
-  | eval_static_condition_case7 c n1 n2 => (* Ccompf c, F n1 :: F n2 :: nil *) 
-      Some(Float.cmp c n1 n2)
-  | eval_static_condition_case8 c n1 n2 => (* Cnotcompf c, F n1 :: F n2 :: nil *) 
-      Some(negb(Float.cmp c n1 n2))
-  | eval_static_condition_default cond vl =>
-      None
-  end.
-
-
-Definition eval_static_condition_val (cond: condition) (vl: list approx) :=
-  match eval_static_condition cond vl with
-  | None => Unknown
-  | Some b => I(if b then Int.one else Int.zero)
-  end.
-
-Definition eval_static_intoffloat (f: float) :=
-  match Float.intoffloat f with Some x => I x | None => Unknown end.
-
-Definition eval_static_intuoffloat (f: float) :=
-  match Float.intuoffloat f with Some x => I x | None => Unknown end.
-
-(** Original definition:
-<<
-Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
-  match op, vl with
-  | Omove, v1::nil => v1
-  | Ointconst n, nil => I n
-  | Ofloatconst n, nil => F n
-  | Oaddrsymbol s n, nil => G s n
-  | Oaddrstack n, nil => S n
-  | Oadd, I n1 :: I n2 :: nil => I(Int.add n1 n2)
-  | Oaddshift s, I n1 :: I n2 :: nil => I(Int.add n1 (eval_static_shift s n2))
-  | Oadd, G s1 n1 :: I n2 :: nil => G s1 (Int.add n1 n2)
-  | Oaddshift s, G s1 n1 :: I n2 :: nil => G s1 (Int.add n1 (eval_static_shift s n2))
-  | Oadd, S n1 :: I n2 :: nil => S (Int.add n1 n2)
-  | Oaddshift s, S n1 :: I n2 :: nil => S (Int.add n1 (eval_static_shift s n2))
-  | Oadd, I n1 :: G s2 n2 :: nil => G s2 (Int.add n1 n2)
-  | Oadd, I n1 :: S n2 :: nil => S (Int.add n1 n2)
-  | Oaddimm n, I n1 :: nil => I (Int.add n1 n)
-  | Oaddimm n, G s1 n1 :: nil => G s1 (Int.add n1 n)
-  | Oaddimm n, S n1 :: nil => S (Int.add n1 n)
-  | Osub, I n1 :: I n2 :: nil => I(Int.sub n1 n2)
-  | Osubshift s, I n1 :: I n2 :: nil => I(Int.sub n1 (eval_static_shift s n2))
-  | Osub, G s1 n1 :: I n2 :: nil => G s1 (Int.sub n1 n2)
-  | Osub, S n1 :: I n2 :: nil => S (Int.sub n1 n2)
-  | Osubshift s, G s1 n1 :: I n2 :: nil => G s1 (Int.sub n1 (eval_static_shift s n2))
-  | Orsubshift s, I n1 :: I n2 :: nil => I(Int.sub (eval_static_shift s n2) n1)
-  | Orsubimm n, I n1 :: nil => I (Int.sub n n1)
-  | Omul, I n1 :: I n2 :: nil => I(Int.mul n1 n2)
-  | Odiv, I n1 :: I n2 :: nil => if Int.eq n2 Int.zero then Unknown else I(Int.divs n1 n2)
-  | Odivu, I n1 :: I n2 :: nil => if Int.eq n2 Int.zero then Unknown else I(Int.divu n1 n2)
-  | Oand, I n1 :: I n2 :: nil => I(Int.and n1 n2)
-  | Oandshift s, I n1 :: I n2 :: nil => I(Int.and n1 (eval_static_shift s n2))
-  | Oandimm n, I n1 :: nil => I(Int.and n1 n)
-  | Oor, I n1 :: I n2 :: nil => I(Int.or n1 n2)
-  | Oorshift s, I n1 :: I n2 :: nil => I(Int.or n1 (eval_static_shift s n2))
-  | Oorimm n, I n1 :: nil => I(Int.or n1 n)
-  | Oxor, I n1 :: I n2 :: nil => I(Int.xor n1 n2)
-  | Oxorshift s, I n1 :: I n2 :: nil => I(Int.xor n1 (eval_static_shift s n2))
-  | Oxorimm n, I n1 :: nil => I(Int.xor n1 n)
-  | Obic, I n1 :: I n2 :: nil => I(Int.and n1 (Int.not n2))
-  | Obicshift s, I n1 :: I n2 :: nil => I(Int.and n1 (Int.not (eval_static_shift s n2)))
-  | Onot, I n1 :: nil => I(Int.not n1)
-  | Onotshift s, I n1 :: nil => I(Int.not (eval_static_shift s n1))
-  | Oshl, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shl n1 n2) else Unknown
-  | Oshr, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shr n1 n2) else Unknown
-  | Oshru, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shru n1 n2) else Unknown
-  | Oshift s, I n1 :: nil => I(eval_static_shift s n1)
-  | Onegf, F n1 :: nil => F(Float.neg n1)
-  | Oabsf, F n1 :: nil => F(Float.abs n1)
-  | Oaddf, F n1 :: F n2 :: nil => F(Float.add n1 n2)
-  | Osubf, F n1 :: F n2 :: nil => F(Float.sub n1 n2)
-  | Omulf, F n1 :: F n2 :: nil => F(Float.mul n1 n2)
-  | Odivf, F n1 :: F n2 :: nil => F(Float.div n1 n2)
-  | Osingleoffloat, F n1 :: nil => F(Float.singleoffloat n1)
-  | Ointoffloat, F n1 :: nil => eval_static_intoffloat n1
-  | Ointuoffloat, F n1 :: nil => eval_static_intuoffloat n1
-  | Ofloatofint, I n1 :: nil => F(Float.floatofint n1)
-  | Ofloatofintu, I n1 :: nil => F(Float.floatofintu n1)
-  | Ocmp c, vl => eval_static_condition_val c vl
-  | _, _ => Unknown
-  end.
->>
-*)
-
-Inductive eval_static_operation_cases: forall (op: operation) (vl: list approx), Type :=
-  | eval_static_operation_case1: forall v1, eval_static_operation_cases (Omove) (v1::nil)
-  | eval_static_operation_case2: forall n, eval_static_operation_cases (Ointconst n) (nil)
-  | eval_static_operation_case3: forall n, eval_static_operation_cases (Ofloatconst n) (nil)
-  | eval_static_operation_case4: forall s n, eval_static_operation_cases (Oaddrsymbol s n) (nil)
-  | eval_static_operation_case5: forall n, eval_static_operation_cases (Oaddrstack n) (nil)
-  | eval_static_operation_case6: forall n1 n2, eval_static_operation_cases (Oadd) (I n1 :: I n2 :: nil)
-  | eval_static_operation_case7: forall s n1 n2, eval_static_operation_cases (Oaddshift s) (I n1 :: I n2 :: nil)
-  | eval_static_operation_case8: forall s1 n1 n2, eval_static_operation_cases (Oadd) (G s1 n1 :: I n2 :: nil)
-  | eval_static_operation_case9: forall s s1 n1 n2, eval_static_operation_cases (Oaddshift s) (G s1 n1 :: I n2 :: nil)
-  | eval_static_operation_case10: forall n1 n2, eval_static_operation_cases (Oadd) (S n1 :: I n2 :: nil)
-  | eval_static_operation_case11: forall s n1 n2, eval_static_operation_cases (Oaddshift s) (S n1 :: I n2 :: nil)
-  | eval_static_operation_case12: forall n1 s2 n2, eval_static_operation_cases (Oadd) (I n1 :: G s2 n2 :: nil)
-  | eval_static_operation_case13: forall n1 n2, eval_static_operation_cases (Oadd) (I n1 :: S n2 :: nil)
-  | eval_static_operation_case14: forall n n1, eval_static_operation_cases (Oaddimm n) (I n1 :: nil)
-  | eval_static_operation_case15: forall n s1 n1, eval_static_operation_cases (Oaddimm n) (G s1 n1 :: nil)
-  | eval_static_operation_case16: forall n n1, eval_static_operation_cases (Oaddimm n) (S n1 :: nil)
-  | eval_static_operation_case17: forall n1 n2, eval_static_operation_cases (Osub) (I n1 :: I n2 :: nil)
-  | eval_static_operation_case18: forall s n1 n2, eval_static_operation_cases (Osubshift s) (I n1 :: I n2 :: nil)
-  | eval_static_operation_case19: forall s1 n1 n2, eval_static_operation_cases (Osub) (G s1 n1 :: I n2 :: nil)
-  | eval_static_operation_case20: forall n1 n2, eval_static_operation_cases (Osub) (S n1 :: I n2 :: nil)
-  | eval_static_operation_case21: forall s s1 n1 n2, eval_static_operation_cases (Osubshift s) (G s1 n1 :: I n2 :: nil)
-  | eval_static_operation_case22: forall s n1 n2, eval_static_operation_cases (Orsubshift s) (I n1 :: I n2 :: nil)
-  | eval_static_operation_case23: forall n n1, eval_static_operation_cases (Orsubimm n) (I n1 :: nil)
-  | eval_static_operation_case24: forall n1 n2, eval_static_operation_cases (Omul) (I n1 :: I n2 :: nil)
-  | eval_static_operation_case25: forall n1 n2, eval_static_operation_cases (Odiv) (I n1 :: I n2 :: nil)
-  | eval_static_operation_case26: forall n1 n2, eval_static_operation_cases (Odivu) (I n1 :: I n2 :: nil)
-  | eval_static_operation_case27: forall n1 n2, eval_static_operation_cases (Oand) (I n1 :: I n2 :: nil)
-  | eval_static_operation_case28: forall s n1 n2, eval_static_operation_cases (Oandshift s) (I n1 :: I n2 :: nil)
-  | eval_static_operation_case29: forall n n1, eval_static_operation_cases (Oandimm n) (I n1 :: nil)
-  | eval_static_operation_case30: forall n1 n2, eval_static_operation_cases (Oor) (I n1 :: I n2 :: nil)
-  | eval_static_operation_case31: forall s n1 n2, eval_static_operation_cases (Oorshift s) (I n1 :: I n2 :: nil)
-  | eval_static_operation_case32: forall n n1, eval_static_operation_cases (Oorimm n) (I n1 :: nil)
-  | eval_static_operation_case33: forall n1 n2, eval_static_operation_cases (Oxor) (I n1 :: I n2 :: nil)
-  | eval_static_operation_case34: forall s n1 n2, eval_static_operation_cases (Oxorshift s) (I n1 :: I n2 :: nil)
-  | eval_static_operation_case35: forall n n1, eval_static_operation_cases (Oxorimm n) (I n1 :: nil)
-  | eval_static_operation_case36: forall n1 n2, eval_static_operation_cases (Obic) (I n1 :: I n2 :: nil)
-  | eval_static_operation_case37: forall s n1 n2, eval_static_operation_cases (Obicshift s) (I n1 :: I n2 :: nil)
-  | eval_static_operation_case38: forall n1, eval_static_operation_cases (Onot) (I n1 :: nil)
-  | eval_static_operation_case39: forall s n1, eval_static_operation_cases (Onotshift s) (I n1 :: nil)
-  | eval_static_operation_case40: forall n1 n2, eval_static_operation_cases (Oshl) (I n1 :: I n2 :: nil)
-  | eval_static_operation_case41: forall n1 n2, eval_static_operation_cases (Oshr) (I n1 :: I n2 :: nil)
-  | eval_static_operation_case42: forall n1 n2, eval_static_operation_cases (Oshru) (I n1 :: I n2 :: nil)
-  | eval_static_operation_case43: forall s n1, eval_static_operation_cases (Oshift s) (I n1 :: nil)
-  | eval_static_operation_case44: forall n1, eval_static_operation_cases (Onegf) (F n1 :: nil)
-  | eval_static_operation_case45: forall n1, eval_static_operation_cases (Oabsf) (F n1 :: nil)
-  | eval_static_operation_case46: forall n1 n2, eval_static_operation_cases (Oaddf) (F n1 :: F n2 :: nil)
-  | eval_static_operation_case47: forall n1 n2, eval_static_operation_cases (Osubf) (F n1 :: F n2 :: nil)
-  | eval_static_operation_case48: forall n1 n2, eval_static_operation_cases (Omulf) (F n1 :: F n2 :: nil)
-  | eval_static_operation_case49: forall n1 n2, eval_static_operation_cases (Odivf) (F n1 :: F n2 :: nil)
-  | eval_static_operation_case50: forall n1, eval_static_operation_cases (Osingleoffloat) (F n1 :: nil)
-  | eval_static_operation_case51: forall n1, eval_static_operation_cases (Ointoffloat) (F n1 :: nil)
-  | eval_static_operation_case52: forall n1, eval_static_operation_cases (Ointuoffloat) (F n1 :: nil)
-  | eval_static_operation_case53: forall n1, eval_static_operation_cases (Ofloatofint) (I n1 :: nil)
-  | eval_static_operation_case54: forall n1, eval_static_operation_cases (Ofloatofintu) (I n1 :: nil)
-  | eval_static_operation_case55: forall c vl, eval_static_operation_cases (Ocmp c) (vl)
-  | eval_static_operation_default: forall (op: operation) (vl: list approx), eval_static_operation_cases op vl.
-
-Definition eval_static_operation_match (op: operation) (vl: list approx) :=
-  match op as zz1, vl as zz2 return eval_static_operation_cases zz1 zz2 with
-  | Omove, v1::nil => eval_static_operation_case1 v1
-  | Ointconst n, nil => eval_static_operation_case2 n
-  | Ofloatconst n, nil => eval_static_operation_case3 n
-  | Oaddrsymbol s n, nil => eval_static_operation_case4 s n
-  | Oaddrstack n, nil => eval_static_operation_case5 n
-  | Oadd, I n1 :: I n2 :: nil => eval_static_operation_case6 n1 n2
-  | Oaddshift s, I n1 :: I n2 :: nil => eval_static_operation_case7 s n1 n2
-  | Oadd, G s1 n1 :: I n2 :: nil => eval_static_operation_case8 s1 n1 n2
-  | Oaddshift s, G s1 n1 :: I n2 :: nil => eval_static_operation_case9 s s1 n1 n2
-  | Oadd, S n1 :: I n2 :: nil => eval_static_operation_case10 n1 n2
-  | Oaddshift s, S n1 :: I n2 :: nil => eval_static_operation_case11 s n1 n2
-  | Oadd, I n1 :: G s2 n2 :: nil => eval_static_operation_case12 n1 s2 n2
-  | Oadd, I n1 :: S n2 :: nil => eval_static_operation_case13 n1 n2
-  | Oaddimm n, I n1 :: nil => eval_static_operation_case14 n n1
-  | Oaddimm n, G s1 n1 :: nil => eval_static_operation_case15 n s1 n1
-  | Oaddimm n, S n1 :: nil => eval_static_operation_case16 n n1
-  | Osub, I n1 :: I n2 :: nil => eval_static_operation_case17 n1 n2
-  | Osubshift s, I n1 :: I n2 :: nil => eval_static_operation_case18 s n1 n2
-  | Osub, G s1 n1 :: I n2 :: nil => eval_static_operation_case19 s1 n1 n2
-  | Osub, S n1 :: I n2 :: nil => eval_static_operation_case20 n1 n2
-  | Osubshift s, G s1 n1 :: I n2 :: nil => eval_static_operation_case21 s s1 n1 n2
-  | Orsubshift s, I n1 :: I n2 :: nil => eval_static_operation_case22 s n1 n2
-  | Orsubimm n, I n1 :: nil => eval_static_operation_case23 n n1
-  | Omul, I n1 :: I n2 :: nil => eval_static_operation_case24 n1 n2
-  | Odiv, I n1 :: I n2 :: nil => eval_static_operation_case25 n1 n2
-  | Odivu, I n1 :: I n2 :: nil => eval_static_operation_case26 n1 n2
-  | Oand, I n1 :: I n2 :: nil => eval_static_operation_case27 n1 n2
-  | Oandshift s, I n1 :: I n2 :: nil => eval_static_operation_case28 s n1 n2
-  | Oandimm n, I n1 :: nil => eval_static_operation_case29 n n1
-  | Oor, I n1 :: I n2 :: nil => eval_static_operation_case30 n1 n2
-  | Oorshift s, I n1 :: I n2 :: nil => eval_static_operation_case31 s n1 n2
-  | Oorimm n, I n1 :: nil => eval_static_operation_case32 n n1
-  | Oxor, I n1 :: I n2 :: nil => eval_static_operation_case33 n1 n2
-  | Oxorshift s, I n1 :: I n2 :: nil => eval_static_operation_case34 s n1 n2
-  | Oxorimm n, I n1 :: nil => eval_static_operation_case35 n n1
-  | Obic, I n1 :: I n2 :: nil => eval_static_operation_case36 n1 n2
-  | Obicshift s, I n1 :: I n2 :: nil => eval_static_operation_case37 s n1 n2
-  | Onot, I n1 :: nil => eval_static_operation_case38 n1
-  | Onotshift s, I n1 :: nil => eval_static_operation_case39 s n1
-  | Oshl, I n1 :: I n2 :: nil => eval_static_operation_case40 n1 n2
-  | Oshr, I n1 :: I n2 :: nil => eval_static_operation_case41 n1 n2
-  | Oshru, I n1 :: I n2 :: nil => eval_static_operation_case42 n1 n2
-  | Oshift s, I n1 :: nil => eval_static_operation_case43 s n1
-  | Onegf, F n1 :: nil => eval_static_operation_case44 n1
-  | Oabsf, F n1 :: nil => eval_static_operation_case45 n1
-  | Oaddf, F n1 :: F n2 :: nil => eval_static_operation_case46 n1 n2
-  | Osubf, F n1 :: F n2 :: nil => eval_static_operation_case47 n1 n2
-  | Omulf, F n1 :: F n2 :: nil => eval_static_operation_case48 n1 n2
-  | Odivf, F n1 :: F n2 :: nil => eval_static_operation_case49 n1 n2
-  | Osingleoffloat, F n1 :: nil => eval_static_operation_case50 n1
-  | Ointoffloat, F n1 :: nil => eval_static_operation_case51 n1
-  | Ointuoffloat, F n1 :: nil => eval_static_operation_case52 n1
-  | Ofloatofint, I n1 :: nil => eval_static_operation_case53 n1
-  | Ofloatofintu, I n1 :: nil => eval_static_operation_case54 n1
-  | Ocmp c, vl => eval_static_operation_case55 c vl
-  | op, vl => eval_static_operation_default op vl
-  end.
-
-Definition eval_static_operation (op: operation) (vl: list approx) :=
-  match eval_static_operation_match op vl with
-  | eval_static_operation_case1 v1 => (* Omove, v1::nil *) 
-      v1
-  | eval_static_operation_case2 n => (* Ointconst n, nil *) 
-      I n
-  | eval_static_operation_case3 n => (* Ofloatconst n, nil *) 
-      F n
-  | eval_static_operation_case4 s n => (* Oaddrsymbol s n, nil *) 
-      G s n
-  | eval_static_operation_case5 n => (* Oaddrstack n, nil *) 
-      S n
-  | eval_static_operation_case6 n1 n2 => (* Oadd, I n1 :: I n2 :: nil *) 
-      I(Int.add n1 n2)
-  | eval_static_operation_case7 s n1 n2 => (* Oaddshift s, I n1 :: I n2 :: nil *) 
-      I(Int.add n1 (eval_static_shift s n2))
-  | eval_static_operation_case8 s1 n1 n2 => (* Oadd, G s1 n1 :: I n2 :: nil *) 
-      G s1 (Int.add n1 n2)
-  | eval_static_operation_case9 s s1 n1 n2 => (* Oaddshift s, G s1 n1 :: I n2 :: nil *) 
-      G s1 (Int.add n1 (eval_static_shift s n2))
-  | eval_static_operation_case10 n1 n2 => (* Oadd, S n1 :: I n2 :: nil *) 
-      S (Int.add n1 n2)
-  | eval_static_operation_case11 s n1 n2 => (* Oaddshift s, S n1 :: I n2 :: nil *) 
-      S (Int.add n1 (eval_static_shift s n2))
-  | eval_static_operation_case12 n1 s2 n2 => (* Oadd, I n1 :: G s2 n2 :: nil *) 
-      G s2 (Int.add n1 n2)
-  | eval_static_operation_case13 n1 n2 => (* Oadd, I n1 :: S n2 :: nil *) 
-      S (Int.add n1 n2)
-  | eval_static_operation_case14 n n1 => (* Oaddimm n, I n1 :: nil *) 
-      I (Int.add n1 n)
-  | eval_static_operation_case15 n s1 n1 => (* Oaddimm n, G s1 n1 :: nil *) 
-      G s1 (Int.add n1 n)
-  | eval_static_operation_case16 n n1 => (* Oaddimm n, S n1 :: nil *) 
-      S (Int.add n1 n)
-  | eval_static_operation_case17 n1 n2 => (* Osub, I n1 :: I n2 :: nil *) 
-      I(Int.sub n1 n2)
-  | eval_static_operation_case18 s n1 n2 => (* Osubshift s, I n1 :: I n2 :: nil *) 
-      I(Int.sub n1 (eval_static_shift s n2))
-  | eval_static_operation_case19 s1 n1 n2 => (* Osub, G s1 n1 :: I n2 :: nil *) 
-      G s1 (Int.sub n1 n2)
-  | eval_static_operation_case20 n1 n2 => (* Osub, S n1 :: I n2 :: nil *) 
-      S (Int.sub n1 n2)
-  | eval_static_operation_case21 s s1 n1 n2 => (* Osubshift s, G s1 n1 :: I n2 :: nil *) 
-      G s1 (Int.sub n1 (eval_static_shift s n2))
-  | eval_static_operation_case22 s n1 n2 => (* Orsubshift s, I n1 :: I n2 :: nil *) 
-      I(Int.sub (eval_static_shift s n2) n1)
-  | eval_static_operation_case23 n n1 => (* Orsubimm n, I n1 :: nil *) 
-      I (Int.sub n n1)
-  | eval_static_operation_case24 n1 n2 => (* Omul, I n1 :: I n2 :: nil *) 
-      I(Int.mul n1 n2)
-  | eval_static_operation_case25 n1 n2 => (* Odiv, I n1 :: I n2 :: nil *) 
-      if Int.eq n2 Int.zero then Unknown else I(Int.divs n1 n2)
-  | eval_static_operation_case26 n1 n2 => (* Odivu, I n1 :: I n2 :: nil *) 
-      if Int.eq n2 Int.zero then Unknown else I(Int.divu n1 n2)
-  | eval_static_operation_case27 n1 n2 => (* Oand, I n1 :: I n2 :: nil *) 
-      I(Int.and n1 n2)
-  | eval_static_operation_case28 s n1 n2 => (* Oandshift s, I n1 :: I n2 :: nil *) 
-      I(Int.and n1 (eval_static_shift s n2))
-  | eval_static_operation_case29 n n1 => (* Oandimm n, I n1 :: nil *) 
-      I(Int.and n1 n)
-  | eval_static_operation_case30 n1 n2 => (* Oor, I n1 :: I n2 :: nil *) 
-      I(Int.or n1 n2)
-  | eval_static_operation_case31 s n1 n2 => (* Oorshift s, I n1 :: I n2 :: nil *) 
-      I(Int.or n1 (eval_static_shift s n2))
-  | eval_static_operation_case32 n n1 => (* Oorimm n, I n1 :: nil *) 
-      I(Int.or n1 n)
-  | eval_static_operation_case33 n1 n2 => (* Oxor, I n1 :: I n2 :: nil *) 
-      I(Int.xor n1 n2)
-  | eval_static_operation_case34 s n1 n2 => (* Oxorshift s, I n1 :: I n2 :: nil *) 
-      I(Int.xor n1 (eval_static_shift s n2))
-  | eval_static_operation_case35 n n1 => (* Oxorimm n, I n1 :: nil *) 
-      I(Int.xor n1 n)
-  | eval_static_operation_case36 n1 n2 => (* Obic, I n1 :: I n2 :: nil *) 
-      I(Int.and n1 (Int.not n2))
-  | eval_static_operation_case37 s n1 n2 => (* Obicshift s, I n1 :: I n2 :: nil *) 
-      I(Int.and n1 (Int.not (eval_static_shift s n2)))
-  | eval_static_operation_case38 n1 => (* Onot, I n1 :: nil *) 
-      I(Int.not n1)
-  | eval_static_operation_case39 s n1 => (* Onotshift s, I n1 :: nil *) 
-      I(Int.not (eval_static_shift s n1))
-  | eval_static_operation_case40 n1 n2 => (* Oshl, I n1 :: I n2 :: nil *) 
-      if Int.ltu n2 Int.iwordsize then I(Int.shl n1 n2) else Unknown
-  | eval_static_operation_case41 n1 n2 => (* Oshr, I n1 :: I n2 :: nil *) 
-      if Int.ltu n2 Int.iwordsize then I(Int.shr n1 n2) else Unknown
-  | eval_static_operation_case42 n1 n2 => (* Oshru, I n1 :: I n2 :: nil *) 
-      if Int.ltu n2 Int.iwordsize then I(Int.shru n1 n2) else Unknown
-  | eval_static_operation_case43 s n1 => (* Oshift s, I n1 :: nil *) 
-      I(eval_static_shift s n1)
-  | eval_static_operation_case44 n1 => (* Onegf, F n1 :: nil *) 
-      F(Float.neg n1)
-  | eval_static_operation_case45 n1 => (* Oabsf, F n1 :: nil *) 
-      F(Float.abs n1)
-  | eval_static_operation_case46 n1 n2 => (* Oaddf, F n1 :: F n2 :: nil *) 
-      F(Float.add n1 n2)
-  | eval_static_operation_case47 n1 n2 => (* Osubf, F n1 :: F n2 :: nil *) 
-      F(Float.sub n1 n2)
-  | eval_static_operation_case48 n1 n2 => (* Omulf, F n1 :: F n2 :: nil *) 
-      F(Float.mul n1 n2)
-  | eval_static_operation_case49 n1 n2 => (* Odivf, F n1 :: F n2 :: nil *) 
-      F(Float.div n1 n2)
-  | eval_static_operation_case50 n1 => (* Osingleoffloat, F n1 :: nil *) 
-      F(Float.singleoffloat n1)
-  | eval_static_operation_case51 n1 => (* Ointoffloat, F n1 :: nil *) 
-      eval_static_intoffloat n1
-  | eval_static_operation_case52 n1 => (* Ointuoffloat, F n1 :: nil *) 
-      eval_static_intuoffloat n1
-  | eval_static_operation_case53 n1 => (* Ofloatofint, I n1 :: nil *) 
-      F(Float.floatofint n1)
-  | eval_static_operation_case54 n1 => (* Ofloatofintu, I n1 :: nil *) 
-      F(Float.floatofintu n1)
-  | eval_static_operation_case55 c vl => (* Ocmp c, vl *) 
-      eval_static_condition_val c vl
-  | eval_static_operation_default op vl =>
-      Unknown
-  end.
-
-
-(** * Operator strength reduction *)
-
-(** We now define auxiliary functions for strength reduction of
-  operators and addressing modes: replacing an operator with a cheaper
-  one if some of its arguments are statically known.  These are again
-  large pattern-matchings expressed in indirect style. *)
-
-Section STRENGTH_REDUCTION.
-
-(** Original definition:
-<<
-Nondetfunction cond_strength_reduction 
-              (cond: condition) (args: list reg) (vl: list approx) :=
-  match cond, args, vl with
-  | Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil =>
-      (Ccompimm (swap_comparison c) n1, r2 :: nil)
-  | Ccomp c, r1 :: r2 :: nil, v1 :: I n2 :: nil =>
-      (Ccompimm c n2, r1 :: nil)
-  | Ccompu c, r1 :: r2 :: nil, I n1 :: v2 :: nil =>
-      (Ccompuimm (swap_comparison c) n1, r2 :: nil)
-  | Ccompu c, r1 :: r2 :: nil, v1 :: I n2 :: nil =>
-      (Ccompuimm c n2, r1 :: nil)
-  | Ccompshift c s, r1 :: r2 :: nil, v1 :: I n2 :: nil =>
-      (Ccompimm c (eval_static_shift s n2), r1 :: nil)
-  | Ccompushift c s, r1 :: r2 :: nil, v1 :: I n2 :: nil =>
-      (Ccompuimm c (eval_static_shift s n2), r1 :: nil)
-  | _, _, _ => 
-      (cond, args)
-  end.
->>
-*)
-
-Inductive cond_strength_reduction_cases: forall (cond: condition) (args: list reg) (vl: list approx), Type :=
-  | cond_strength_reduction_case1: forall c r1 r2 n1 v2, cond_strength_reduction_cases (Ccomp c) (r1 :: r2 :: nil) (I n1 :: v2 :: nil)
-  | cond_strength_reduction_case2: forall c r1 r2 v1 n2, cond_strength_reduction_cases (Ccomp c) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | cond_strength_reduction_case3: forall c r1 r2 n1 v2, cond_strength_reduction_cases (Ccompu c) (r1 :: r2 :: nil) (I n1 :: v2 :: nil)
-  | cond_strength_reduction_case4: forall c r1 r2 v1 n2, cond_strength_reduction_cases (Ccompu c) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | cond_strength_reduction_case5: forall c s r1 r2 v1 n2, cond_strength_reduction_cases (Ccompshift c s) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | cond_strength_reduction_case6: forall c s r1 r2 v1 n2, cond_strength_reduction_cases (Ccompushift c s) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | cond_strength_reduction_default: forall (cond: condition) (args: list reg) (vl: list approx), cond_strength_reduction_cases cond args vl.
-
-Definition cond_strength_reduction_match (cond: condition) (args: list reg) (vl: list approx) :=
-  match cond as zz1, args as zz2, vl as zz3 return cond_strength_reduction_cases zz1 zz2 zz3 with
-  | Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil => cond_strength_reduction_case1 c r1 r2 n1 v2
-  | Ccomp c, r1 :: r2 :: nil, v1 :: I n2 :: nil => cond_strength_reduction_case2 c r1 r2 v1 n2
-  | Ccompu c, r1 :: r2 :: nil, I n1 :: v2 :: nil => cond_strength_reduction_case3 c r1 r2 n1 v2
-  | Ccompu c, r1 :: r2 :: nil, v1 :: I n2 :: nil => cond_strength_reduction_case4 c r1 r2 v1 n2
-  | Ccompshift c s, r1 :: r2 :: nil, v1 :: I n2 :: nil => cond_strength_reduction_case5 c s r1 r2 v1 n2
-  | Ccompushift c s, r1 :: r2 :: nil, v1 :: I n2 :: nil => cond_strength_reduction_case6 c s r1 r2 v1 n2
-  | cond, args, vl => cond_strength_reduction_default cond args vl
-  end.
-
-Definition cond_strength_reduction (cond: condition) (args: list reg) (vl: list approx) :=
-  match cond_strength_reduction_match cond args vl with
-  | cond_strength_reduction_case1 c r1 r2 n1 v2 => (* Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil *) 
-      (Ccompimm (swap_comparison c) n1, r2 :: nil)
-  | cond_strength_reduction_case2 c r1 r2 v1 n2 => (* Ccomp c, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      (Ccompimm c n2, r1 :: nil)
-  | cond_strength_reduction_case3 c r1 r2 n1 v2 => (* Ccompu c, r1 :: r2 :: nil, I n1 :: v2 :: nil *) 
-      (Ccompuimm (swap_comparison c) n1, r2 :: nil)
-  | cond_strength_reduction_case4 c r1 r2 v1 n2 => (* Ccompu c, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      (Ccompuimm c n2, r1 :: nil)
-  | cond_strength_reduction_case5 c s r1 r2 v1 n2 => (* Ccompshift c s, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      (Ccompimm c (eval_static_shift s n2), r1 :: nil)
-  | cond_strength_reduction_case6 c s r1 r2 v1 n2 => (* Ccompushift c s, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      (Ccompuimm c (eval_static_shift s n2), r1 :: nil)
-  | cond_strength_reduction_default cond args vl =>
-      (cond, args)
-  end.
-
-
-Definition make_addimm (n: int) (r: reg) :=
-  if Int.eq n Int.zero
-  then (Omove, r :: nil)
-  else (Oaddimm n, r :: nil).
-
-Definition make_shlimm (n: int) (r1 r2: reg) :=
-  if Int.eq n Int.zero then
-    (Omove, r1 :: nil)
-  else if Int.ltu n Int.iwordsize then
-    (Oshift (Slsl (mk_shift_amount n)), r1 :: nil)
-  else
-    (Oshl, r1 :: r2 :: nil).
-
-Definition make_shrimm (n: int) (r1 r2: reg) :=
-  if Int.eq n Int.zero then
-    (Omove, r1 :: nil)
-  else if Int.ltu n Int.iwordsize then
-    (Oshift (Sasr (mk_shift_amount n)), r1 :: nil)
-  else
-    (Oshr, r1 :: r2 :: nil).
-
-Definition make_shruimm (n: int) (r1 r2: reg) :=
-  if Int.eq n Int.zero then
-    (Omove, r1 :: nil)
-  else if Int.ltu n Int.iwordsize then
-    (Oshift (Slsr (mk_shift_amount n)), r1 :: nil)
-  else
-    (Oshru, r1 :: r2 :: nil).
-
-Definition make_mulimm (n: int) (r1 r2: reg) :=
-  if Int.eq n Int.zero then
-    (Ointconst Int.zero, nil)
-  else if Int.eq n Int.one then
-    (Omove, r1 :: nil)
-  else
-    match Int.is_power2 n with
-    | Some l => (Oshift (Slsl (mk_shift_amount l)), r1 :: nil)
-    | None => (Omul, r1 :: r2 :: nil)
-    end.
-
-Definition make_divimm (n: int) (r1 r2: reg) :=
-  match Int.is_power2 n with
-  | Some l => if Int.ltu l (Int.repr 31)
-              then (Oshrximm l, r1 :: nil)
-              else (Odiv, r1 :: r2 :: nil)
-  | None   => (Odiv, r1 :: r2 :: nil)
-  end.
-
-Definition make_divuimm (n: int) (r1 r2: reg) :=
-  match Int.is_power2 n with
-  | Some l => (Oshift (Slsr (mk_shift_amount l)), r1 :: nil)
-  | None   => (Odivu, r1 :: r2 :: nil)
-  end.
-
-Definition make_andimm (n: int) (r: reg) :=
-  if Int.eq n Int.zero then (Ointconst Int.zero, nil)
-  else if Int.eq n Int.mone then (Omove, r :: nil)
-  else (Oandimm n, r :: nil).
-
-Definition make_orimm (n: int) (r: reg) :=
-  if Int.eq n Int.zero then (Omove, r :: nil)
-  else if Int.eq n Int.mone then (Ointconst Int.mone, nil)
-  else (Oorimm n, r :: nil).
-
-Definition make_xorimm (n: int) (r: reg) :=
-  if Int.eq n Int.zero then (Omove, r :: nil)
-  else if Int.eq n Int.mone then (Onot, r :: nil)
-  else (Oxorimm n, r :: nil).
-
-(** Original definition:
-<<
-Nondetfunction op_strength_reduction 
-              (op: operation) (args: list reg) (vl: list approx) :=
-  match op, args, vl with
-  | Oadd, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_addimm n1 r2
-  | Oadd, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_addimm n2 r1
-  | Oaddshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_addimm (eval_static_shift s n2) r1
-  | Osub, r1 :: r2 :: nil, I n1 :: v2 :: nil => (Orsubimm n1, r2 :: nil)
-  | Osub, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_addimm (Int.neg n2) r1
-  | Osubshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_addimm (Int.neg (eval_static_shift s n2)) r1
-  | Orsubshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => (Orsubimm (eval_static_shift s n2), r1 :: nil)
-  | Omul, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_mulimm n1 r2 r1
-  | Omul, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_mulimm n2 r1 r2
-  | Odiv, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_divimm n2 r1 r2
-  | Odivu, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_divuimm n2 r1 r2
-  | Oand, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_andimm n1 r2
-  | Oand, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm n2 r1
-  | Oandshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm (eval_static_shift s n2) r1
-  | Oor, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_orimm n1 r2
-  | Oor, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_orimm n2 r1
-  | Oorshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_orimm (eval_static_shift s n2) r1
-  | Oxor, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_xorimm n1 r2
-  | Oxor, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_xorimm n2 r1
-  | Oxorshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_xorimm (eval_static_shift s n2) r1
-  | Obic, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm (Int.not n2) r1
-  | Obicshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm (Int.not (eval_static_shift s n2)) r1
-  | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shlimm n2 r1 r2
-  | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrimm n2 r1 r2
-  | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1 r2
-  | Ocmp c, args, vl =>
-      let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args')
-  | _, _, _ => (op, args)
-  end.
->>
-*)
-
-Inductive op_strength_reduction_cases: forall (op: operation) (args: list reg) (vl: list approx), Type :=
-  | op_strength_reduction_case1: forall r1 r2 n1 v2, op_strength_reduction_cases (Oadd) (r1 :: r2 :: nil) (I n1 :: v2 :: nil)
-  | op_strength_reduction_case2: forall r1 r2 v1 n2, op_strength_reduction_cases (Oadd) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | op_strength_reduction_case3: forall s r1 r2 v1 n2, op_strength_reduction_cases (Oaddshift s) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | op_strength_reduction_case4: forall r1 r2 n1 v2, op_strength_reduction_cases (Osub) (r1 :: r2 :: nil) (I n1 :: v2 :: nil)
-  | op_strength_reduction_case5: forall r1 r2 v1 n2, op_strength_reduction_cases (Osub) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | op_strength_reduction_case6: forall s r1 r2 v1 n2, op_strength_reduction_cases (Osubshift s) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | op_strength_reduction_case7: forall s r1 r2 v1 n2, op_strength_reduction_cases (Orsubshift s) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | op_strength_reduction_case8: forall r1 r2 n1 v2, op_strength_reduction_cases (Omul) (r1 :: r2 :: nil) (I n1 :: v2 :: nil)
-  | op_strength_reduction_case9: forall r1 r2 v1 n2, op_strength_reduction_cases (Omul) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | op_strength_reduction_case10: forall r1 r2 v1 n2, op_strength_reduction_cases (Odiv) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | op_strength_reduction_case11: forall r1 r2 v1 n2, op_strength_reduction_cases (Odivu) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | op_strength_reduction_case12: forall r1 r2 n1 v2, op_strength_reduction_cases (Oand) (r1 :: r2 :: nil) (I n1 :: v2 :: nil)
-  | op_strength_reduction_case13: forall r1 r2 v1 n2, op_strength_reduction_cases (Oand) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | op_strength_reduction_case14: forall s r1 r2 v1 n2, op_strength_reduction_cases (Oandshift s) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | op_strength_reduction_case15: forall r1 r2 n1 v2, op_strength_reduction_cases (Oor) (r1 :: r2 :: nil) (I n1 :: v2 :: nil)
-  | op_strength_reduction_case16: forall r1 r2 v1 n2, op_strength_reduction_cases (Oor) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | op_strength_reduction_case17: forall s r1 r2 v1 n2, op_strength_reduction_cases (Oorshift s) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | op_strength_reduction_case18: forall r1 r2 n1 v2, op_strength_reduction_cases (Oxor) (r1 :: r2 :: nil) (I n1 :: v2 :: nil)
-  | op_strength_reduction_case19: forall r1 r2 v1 n2, op_strength_reduction_cases (Oxor) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | op_strength_reduction_case20: forall s r1 r2 v1 n2, op_strength_reduction_cases (Oxorshift s) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | op_strength_reduction_case21: forall r1 r2 v1 n2, op_strength_reduction_cases (Obic) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | op_strength_reduction_case22: forall s r1 r2 v1 n2, op_strength_reduction_cases (Obicshift s) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | op_strength_reduction_case23: forall r1 r2 v1 n2, op_strength_reduction_cases (Oshl) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | op_strength_reduction_case24: forall r1 r2 v1 n2, op_strength_reduction_cases (Oshr) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | op_strength_reduction_case25: forall r1 r2 v1 n2, op_strength_reduction_cases (Oshru) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | op_strength_reduction_case26: forall c args vl, op_strength_reduction_cases (Ocmp c) (args) (vl)
-  | op_strength_reduction_default: forall (op: operation) (args: list reg) (vl: list approx), op_strength_reduction_cases op args vl.
-
-Definition op_strength_reduction_match (op: operation) (args: list reg) (vl: list approx) :=
-  match op as zz1, args as zz2, vl as zz3 return op_strength_reduction_cases zz1 zz2 zz3 with
-  | Oadd, r1 :: r2 :: nil, I n1 :: v2 :: nil => op_strength_reduction_case1 r1 r2 n1 v2
-  | Oadd, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case2 r1 r2 v1 n2
-  | Oaddshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case3 s r1 r2 v1 n2
-  | Osub, r1 :: r2 :: nil, I n1 :: v2 :: nil => op_strength_reduction_case4 r1 r2 n1 v2
-  | Osub, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case5 r1 r2 v1 n2
-  | Osubshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case6 s r1 r2 v1 n2
-  | Orsubshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case7 s r1 r2 v1 n2
-  | Omul, r1 :: r2 :: nil, I n1 :: v2 :: nil => op_strength_reduction_case8 r1 r2 n1 v2
-  | Omul, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case9 r1 r2 v1 n2
-  | Odiv, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case10 r1 r2 v1 n2
-  | Odivu, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case11 r1 r2 v1 n2
-  | Oand, r1 :: r2 :: nil, I n1 :: v2 :: nil => op_strength_reduction_case12 r1 r2 n1 v2
-  | Oand, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case13 r1 r2 v1 n2
-  | Oandshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case14 s r1 r2 v1 n2
-  | Oor, r1 :: r2 :: nil, I n1 :: v2 :: nil => op_strength_reduction_case15 r1 r2 n1 v2
-  | Oor, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case16 r1 r2 v1 n2
-  | Oorshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case17 s r1 r2 v1 n2
-  | Oxor, r1 :: r2 :: nil, I n1 :: v2 :: nil => op_strength_reduction_case18 r1 r2 n1 v2
-  | Oxor, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case19 r1 r2 v1 n2
-  | Oxorshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case20 s r1 r2 v1 n2
-  | Obic, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case21 r1 r2 v1 n2
-  | Obicshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case22 s r1 r2 v1 n2
-  | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case23 r1 r2 v1 n2
-  | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case24 r1 r2 v1 n2
-  | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => op_strength_reduction_case25 r1 r2 v1 n2
-  | Ocmp c, args, vl => op_strength_reduction_case26 c args vl
-  | op, args, vl => op_strength_reduction_default op args vl
-  end.
-
-Definition op_strength_reduction (op: operation) (args: list reg) (vl: list approx) :=
-  match op_strength_reduction_match op args vl with
-  | op_strength_reduction_case1 r1 r2 n1 v2 => (* Oadd, r1 :: r2 :: nil, I n1 :: v2 :: nil *) 
-      make_addimm n1 r2
-  | op_strength_reduction_case2 r1 r2 v1 n2 => (* Oadd, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      make_addimm n2 r1
-  | op_strength_reduction_case3 s r1 r2 v1 n2 => (* Oaddshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      make_addimm (eval_static_shift s n2) r1
-  | op_strength_reduction_case4 r1 r2 n1 v2 => (* Osub, r1 :: r2 :: nil, I n1 :: v2 :: nil *) 
-      (Orsubimm n1, r2 :: nil)
-  | op_strength_reduction_case5 r1 r2 v1 n2 => (* Osub, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      make_addimm (Int.neg n2) r1
-  | op_strength_reduction_case6 s r1 r2 v1 n2 => (* Osubshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      make_addimm (Int.neg (eval_static_shift s n2)) r1
-  | op_strength_reduction_case7 s r1 r2 v1 n2 => (* Orsubshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      (Orsubimm (eval_static_shift s n2), r1 :: nil)
-  | op_strength_reduction_case8 r1 r2 n1 v2 => (* Omul, r1 :: r2 :: nil, I n1 :: v2 :: nil *) 
-      make_mulimm n1 r2 r1
-  | op_strength_reduction_case9 r1 r2 v1 n2 => (* Omul, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      make_mulimm n2 r1 r2
-  | op_strength_reduction_case10 r1 r2 v1 n2 => (* Odiv, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      make_divimm n2 r1 r2
-  | op_strength_reduction_case11 r1 r2 v1 n2 => (* Odivu, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      make_divuimm n2 r1 r2
-  | op_strength_reduction_case12 r1 r2 n1 v2 => (* Oand, r1 :: r2 :: nil, I n1 :: v2 :: nil *) 
-      make_andimm n1 r2
-  | op_strength_reduction_case13 r1 r2 v1 n2 => (* Oand, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      make_andimm n2 r1
-  | op_strength_reduction_case14 s r1 r2 v1 n2 => (* Oandshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      make_andimm (eval_static_shift s n2) r1
-  | op_strength_reduction_case15 r1 r2 n1 v2 => (* Oor, r1 :: r2 :: nil, I n1 :: v2 :: nil *) 
-      make_orimm n1 r2
-  | op_strength_reduction_case16 r1 r2 v1 n2 => (* Oor, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      make_orimm n2 r1
-  | op_strength_reduction_case17 s r1 r2 v1 n2 => (* Oorshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      make_orimm (eval_static_shift s n2) r1
-  | op_strength_reduction_case18 r1 r2 n1 v2 => (* Oxor, r1 :: r2 :: nil, I n1 :: v2 :: nil *) 
-      make_xorimm n1 r2
-  | op_strength_reduction_case19 r1 r2 v1 n2 => (* Oxor, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      make_xorimm n2 r1
-  | op_strength_reduction_case20 s r1 r2 v1 n2 => (* Oxorshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      make_xorimm (eval_static_shift s n2) r1
-  | op_strength_reduction_case21 r1 r2 v1 n2 => (* Obic, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      make_andimm (Int.not n2) r1
-  | op_strength_reduction_case22 s r1 r2 v1 n2 => (* Obicshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      make_andimm (Int.not (eval_static_shift s n2)) r1
-  | op_strength_reduction_case23 r1 r2 v1 n2 => (* Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      make_shlimm n2 r1 r2
-  | op_strength_reduction_case24 r1 r2 v1 n2 => (* Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      make_shrimm n2 r1 r2
-  | op_strength_reduction_case25 r1 r2 v1 n2 => (* Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      make_shruimm n2 r1 r2
-  | op_strength_reduction_case26 c args vl => (* Ocmp c, args, vl *) 
-      let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args')
-  | op_strength_reduction_default op args vl =>
-      (op, args)
-  end.
-
-
-
-(** Original definition:
-<<
-Nondetfunction addr_strength_reduction
-                (addr: addressing) (args: list reg) (vl: list approx) :=
-  match addr, args, vl with
-  | Aindexed2, r1 :: r2 :: nil, S n1 :: I n2 :: nil =>
-      (Ainstack (Int.add n1 n2), nil)
-  | Aindexed2, r1 :: r2 :: nil, I n1 :: S n2 :: nil =>
-      (Ainstack (Int.add n1 n2), nil)
-  | Aindexed2, r1 :: r2 :: nil, I n1 :: v2 :: nil =>
-      (Aindexed n1, r2 :: nil)
-  | Aindexed2, r1 :: r2 :: nil, v1 :: I n2 :: nil =>
-      (Aindexed n2, r1 :: nil)
-  | Aindexed2shift s, r1 :: r2 :: nil, S n1 :: I n2 :: nil =>
-      (Ainstack (Int.add n1 (eval_static_shift s n2)), nil)
-  | Aindexed2shift s, r1 :: r2 :: nil, v1 :: I n2 :: nil =>
-      (Aindexed (eval_static_shift s n2), r1 :: nil)
-  | Aindexed n, r1 :: nil, S n1 :: nil =>
-      (Ainstack (Int.add n1 n), nil)
-  | _, _, _ =>
-      (addr, args)
-  end.
->>
-*)
-
-Inductive addr_strength_reduction_cases: forall (addr: addressing) (args: list reg) (vl: list approx), Type :=
-  | addr_strength_reduction_case1: forall r1 r2 n1 n2, addr_strength_reduction_cases (Aindexed2) (r1 :: r2 :: nil) (S n1 :: I n2 :: nil)
-  | addr_strength_reduction_case2: forall r1 r2 n1 n2, addr_strength_reduction_cases (Aindexed2) (r1 :: r2 :: nil) (I n1 :: S n2 :: nil)
-  | addr_strength_reduction_case3: forall r1 r2 n1 v2, addr_strength_reduction_cases (Aindexed2) (r1 :: r2 :: nil) (I n1 :: v2 :: nil)
-  | addr_strength_reduction_case4: forall r1 r2 v1 n2, addr_strength_reduction_cases (Aindexed2) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | addr_strength_reduction_case5: forall s r1 r2 n1 n2, addr_strength_reduction_cases (Aindexed2shift s) (r1 :: r2 :: nil) (S n1 :: I n2 :: nil)
-  | addr_strength_reduction_case6: forall s r1 r2 v1 n2, addr_strength_reduction_cases (Aindexed2shift s) (r1 :: r2 :: nil) (v1 :: I n2 :: nil)
-  | addr_strength_reduction_case7: forall n r1 n1, addr_strength_reduction_cases (Aindexed n) (r1 :: nil) (S n1 :: nil)
-  | addr_strength_reduction_default: forall (addr: addressing) (args: list reg) (vl: list approx), addr_strength_reduction_cases addr args vl.
-
-Definition addr_strength_reduction_match (addr: addressing) (args: list reg) (vl: list approx) :=
-  match addr as zz1, args as zz2, vl as zz3 return addr_strength_reduction_cases zz1 zz2 zz3 with
-  | Aindexed2, r1 :: r2 :: nil, S n1 :: I n2 :: nil => addr_strength_reduction_case1 r1 r2 n1 n2
-  | Aindexed2, r1 :: r2 :: nil, I n1 :: S n2 :: nil => addr_strength_reduction_case2 r1 r2 n1 n2
-  | Aindexed2, r1 :: r2 :: nil, I n1 :: v2 :: nil => addr_strength_reduction_case3 r1 r2 n1 v2
-  | Aindexed2, r1 :: r2 :: nil, v1 :: I n2 :: nil => addr_strength_reduction_case4 r1 r2 v1 n2
-  | Aindexed2shift s, r1 :: r2 :: nil, S n1 :: I n2 :: nil => addr_strength_reduction_case5 s r1 r2 n1 n2
-  | Aindexed2shift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => addr_strength_reduction_case6 s r1 r2 v1 n2
-  | Aindexed n, r1 :: nil, S n1 :: nil => addr_strength_reduction_case7 n r1 n1
-  | addr, args, vl => addr_strength_reduction_default addr args vl
-  end.
-
-Definition addr_strength_reduction (addr: addressing) (args: list reg) (vl: list approx) :=
-  match addr_strength_reduction_match addr args vl with
-  | addr_strength_reduction_case1 r1 r2 n1 n2 => (* Aindexed2, r1 :: r2 :: nil, S n1 :: I n2 :: nil *) 
-      (Ainstack (Int.add n1 n2), nil)
-  | addr_strength_reduction_case2 r1 r2 n1 n2 => (* Aindexed2, r1 :: r2 :: nil, I n1 :: S n2 :: nil *) 
-      (Ainstack (Int.add n1 n2), nil)
-  | addr_strength_reduction_case3 r1 r2 n1 v2 => (* Aindexed2, r1 :: r2 :: nil, I n1 :: v2 :: nil *) 
-      (Aindexed n1, r2 :: nil)
-  | addr_strength_reduction_case4 r1 r2 v1 n2 => (* Aindexed2, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      (Aindexed n2, r1 :: nil)
-  | addr_strength_reduction_case5 s r1 r2 n1 n2 => (* Aindexed2shift s, r1 :: r2 :: nil, S n1 :: I n2 :: nil *) 
-      (Ainstack (Int.add n1 (eval_static_shift s n2)), nil)
-  | addr_strength_reduction_case6 s r1 r2 v1 n2 => (* Aindexed2shift s, r1 :: r2 :: nil, v1 :: I n2 :: nil *) 
-      (Aindexed (eval_static_shift s n2), r1 :: nil)
-  | addr_strength_reduction_case7 n r1 n1 => (* Aindexed n, r1 :: nil, S n1 :: nil *) 
-      (Ainstack (Int.add n1 n), nil)
-  | addr_strength_reduction_default addr args vl =>
-      (addr, args)
-  end.
-
-
-End STRENGTH_REDUCTION.
diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp
new file mode 100644
index 0000000..031ec32
--- /dev/null
+++ b/arm/ConstpropOp.vp
@@ -0,0 +1,301 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Static analysis and strength reduction for operators 
+  and conditions.  This is the machine-dependent part of [Constprop]. *)
+
+Require Import Coqlib.
+Require Import AST.
+Require Import Integers.
+Require Import Floats.
+Require Import Values.
+Require Import Op.
+Require Import Registers.
+
+(** * Static analysis *)
+
+(** To each pseudo-register at each program point, the static analysis 
+  associates a compile-time approximation taken from the following set. *)
+
+Inductive approx : Type :=
+  | Novalue: approx      (** No value possible, code is unreachable. *)
+  | Unknown: approx      (** All values are possible,
+                             no compile-time information is available. *)
+  | I: int -> approx     (** A known integer value. *)
+  | F: float -> approx   (** A known floating-point value. *)
+  | G: ident -> int -> approx
+                         (** The value is the address of the given global
+                             symbol plus the given integer offset. *)
+  | S: int -> approx.    (** The value is the stack pointer plus the offset. *)
+
+
+(** We now define the abstract interpretations of conditions and operators
+  over this set of approximations.  For instance, the abstract interpretation
+  of the operator [Oaddf] applied to two expressions [a] and [b] is
+  [F(Float.add f g)] if [a] and [b] have static approximations [F f]
+  and [F g] respectively, and [Unknown] otherwise.
+
+  The static approximations are defined by large pattern-matchings over
+  the approximations of the results.  We write these matchings in the
+  indirect style described in file [SelectOp] to avoid excessive
+  duplication of cases in proofs. *)
+
+Definition eval_static_shift (s: shift) (n: int) : int :=
+  match s with
+  | Slsl x => Int.shl n x
+  | Slsr x => Int.shru n x
+  | Sasr x => Int.shr n x
+  | Sror x => Int.ror n x
+  end.
+
+Nondetfunction eval_static_condition (cond: condition) (vl: list approx) :=
+  match cond, vl with
+  | Ccomp c, I n1 :: I n2 :: nil => Some(Int.cmp c n1 n2)
+  | Ccompu c, I n1 :: I n2 :: nil => Some(Int.cmpu c n1 n2)
+  | Ccompshift c s, I n1 :: I n2 :: nil => Some(Int.cmp c n1 (eval_static_shift s n2))
+  | Ccompushift c s, I n1 :: I n2 :: nil => Some(Int.cmpu c n1 (eval_static_shift s n2))
+  | Ccompimm c n, I n1 :: nil => Some(Int.cmp c n1 n)
+  | Ccompuimm c n, I n1 :: nil => Some(Int.cmpu c n1 n)
+  | Ccompf c, F n1 :: F n2 :: nil => Some(Float.cmp c n1 n2)
+  | Cnotcompf c, F n1 :: F n2 :: nil => Some(negb(Float.cmp c n1 n2))
+  | _, _ => None
+  end.
+
+Definition eval_static_condition_val (cond: condition) (vl: list approx) :=
+  match eval_static_condition cond vl with
+  | None => Unknown
+  | Some b => I(if b then Int.one else Int.zero)
+  end.
+
+Definition eval_static_intoffloat (f: float) :=
+  match Float.intoffloat f with Some x => I x | None => Unknown end.
+
+Definition eval_static_intuoffloat (f: float) :=
+  match Float.intuoffloat f with Some x => I x | None => Unknown end.
+
+Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
+  match op, vl with
+  | Omove, v1::nil => v1
+  | Ointconst n, nil => I n
+  | Ofloatconst n, nil => F n
+  | Oaddrsymbol s n, nil => G s n
+  | Oaddrstack n, nil => S n
+  | Oadd, I n1 :: I n2 :: nil => I(Int.add n1 n2)
+  | Oaddshift s, I n1 :: I n2 :: nil => I(Int.add n1 (eval_static_shift s n2))
+  | Oadd, G s1 n1 :: I n2 :: nil => G s1 (Int.add n1 n2)
+  | Oaddshift s, G s1 n1 :: I n2 :: nil => G s1 (Int.add n1 (eval_static_shift s n2))
+  | Oadd, S n1 :: I n2 :: nil => S (Int.add n1 n2)
+  | Oaddshift s, S n1 :: I n2 :: nil => S (Int.add n1 (eval_static_shift s n2))
+  | Oadd, I n1 :: G s2 n2 :: nil => G s2 (Int.add n1 n2)
+  | Oadd, I n1 :: S n2 :: nil => S (Int.add n1 n2)
+  | Oaddimm n, I n1 :: nil => I (Int.add n1 n)
+  | Oaddimm n, G s1 n1 :: nil => G s1 (Int.add n1 n)
+  | Oaddimm n, S n1 :: nil => S (Int.add n1 n)
+  | Osub, I n1 :: I n2 :: nil => I(Int.sub n1 n2)
+  | Osubshift s, I n1 :: I n2 :: nil => I(Int.sub n1 (eval_static_shift s n2))
+  | Osub, G s1 n1 :: I n2 :: nil => G s1 (Int.sub n1 n2)
+  | Osub, S n1 :: I n2 :: nil => S (Int.sub n1 n2)
+  | Osubshift s, G s1 n1 :: I n2 :: nil => G s1 (Int.sub n1 (eval_static_shift s n2))
+  | Orsubshift s, I n1 :: I n2 :: nil => I(Int.sub (eval_static_shift s n2) n1)
+  | Orsubimm n, I n1 :: nil => I (Int.sub n n1)
+  | Omul, I n1 :: I n2 :: nil => I(Int.mul n1 n2)
+  | Odiv, I n1 :: I n2 :: nil => if Int.eq n2 Int.zero then Unknown else I(Int.divs n1 n2)
+  | Odivu, I n1 :: I n2 :: nil => if Int.eq n2 Int.zero then Unknown else I(Int.divu n1 n2)
+  | Oand, I n1 :: I n2 :: nil => I(Int.and n1 n2)
+  | Oandshift s, I n1 :: I n2 :: nil => I(Int.and n1 (eval_static_shift s n2))
+  | Oandimm n, I n1 :: nil => I(Int.and n1 n)
+  | Oor, I n1 :: I n2 :: nil => I(Int.or n1 n2)
+  | Oorshift s, I n1 :: I n2 :: nil => I(Int.or n1 (eval_static_shift s n2))
+  | Oorimm n, I n1 :: nil => I(Int.or n1 n)
+  | Oxor, I n1 :: I n2 :: nil => I(Int.xor n1 n2)
+  | Oxorshift s, I n1 :: I n2 :: nil => I(Int.xor n1 (eval_static_shift s n2))
+  | Oxorimm n, I n1 :: nil => I(Int.xor n1 n)
+  | Obic, I n1 :: I n2 :: nil => I(Int.and n1 (Int.not n2))
+  | Obicshift s, I n1 :: I n2 :: nil => I(Int.and n1 (Int.not (eval_static_shift s n2)))
+  | Onot, I n1 :: nil => I(Int.not n1)
+  | Onotshift s, I n1 :: nil => I(Int.not (eval_static_shift s n1))
+  | Oshl, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shl n1 n2) else Unknown
+  | Oshr, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shr n1 n2) else Unknown
+  | Oshru, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shru n1 n2) else Unknown
+  | Oshift s, I n1 :: nil => I(eval_static_shift s n1)
+  | Onegf, F n1 :: nil => F(Float.neg n1)
+  | Oabsf, F n1 :: nil => F(Float.abs n1)
+  | Oaddf, F n1 :: F n2 :: nil => F(Float.add n1 n2)
+  | Osubf, F n1 :: F n2 :: nil => F(Float.sub n1 n2)
+  | Omulf, F n1 :: F n2 :: nil => F(Float.mul n1 n2)
+  | Odivf, F n1 :: F n2 :: nil => F(Float.div n1 n2)
+  | Osingleoffloat, F n1 :: nil => F(Float.singleoffloat n1)
+  | Ointoffloat, F n1 :: nil => eval_static_intoffloat n1
+  | Ointuoffloat, F n1 :: nil => eval_static_intuoffloat n1
+  | Ofloatofint, I n1 :: nil => F(Float.floatofint n1)
+  | Ofloatofintu, I n1 :: nil => F(Float.floatofintu n1)
+  | Ocmp c, vl => eval_static_condition_val c vl
+  | _, _ => Unknown
+  end.
+
+(** * Operator strength reduction *)
+
+(** We now define auxiliary functions for strength reduction of
+  operators and addressing modes: replacing an operator with a cheaper
+  one if some of its arguments are statically known.  These are again
+  large pattern-matchings expressed in indirect style. *)
+
+Section STRENGTH_REDUCTION.
+
+Nondetfunction cond_strength_reduction 
+              (cond: condition) (args: list reg) (vl: list approx) :=
+  match cond, args, vl with
+  | Ccomp c, r1 :: r2 :: nil, I n1 :: v2 :: nil =>
+      (Ccompimm (swap_comparison c) n1, r2 :: nil)
+  | Ccomp c, r1 :: r2 :: nil, v1 :: I n2 :: nil =>
+      (Ccompimm c n2, r1 :: nil)
+  | Ccompu c, r1 :: r2 :: nil, I n1 :: v2 :: nil =>
+      (Ccompuimm (swap_comparison c) n1, r2 :: nil)
+  | Ccompu c, r1 :: r2 :: nil, v1 :: I n2 :: nil =>
+      (Ccompuimm c n2, r1 :: nil)
+  | Ccompshift c s, r1 :: r2 :: nil, v1 :: I n2 :: nil =>
+      (Ccompimm c (eval_static_shift s n2), r1 :: nil)
+  | Ccompushift c s, r1 :: r2 :: nil, v1 :: I n2 :: nil =>
+      (Ccompuimm c (eval_static_shift s n2), r1 :: nil)
+  | _, _, _ => 
+      (cond, args)
+  end.
+
+Definition make_addimm (n: int) (r: reg) :=
+  if Int.eq n Int.zero
+  then (Omove, r :: nil)
+  else (Oaddimm n, r :: nil).
+
+Definition make_shlimm (n: int) (r1 r2: reg) :=
+  if Int.eq n Int.zero then
+    (Omove, r1 :: nil)
+  else if Int.ltu n Int.iwordsize then
+    (Oshift (Slsl (mk_shift_amount n)), r1 :: nil)
+  else
+    (Oshl, r1 :: r2 :: nil).
+
+Definition make_shrimm (n: int) (r1 r2: reg) :=
+  if Int.eq n Int.zero then
+    (Omove, r1 :: nil)
+  else if Int.ltu n Int.iwordsize then
+    (Oshift (Sasr (mk_shift_amount n)), r1 :: nil)
+  else
+    (Oshr, r1 :: r2 :: nil).
+
+Definition make_shruimm (n: int) (r1 r2: reg) :=
+  if Int.eq n Int.zero then
+    (Omove, r1 :: nil)
+  else if Int.ltu n Int.iwordsize then
+    (Oshift (Slsr (mk_shift_amount n)), r1 :: nil)
+  else
+    (Oshru, r1 :: r2 :: nil).
+
+Definition make_mulimm (n: int) (r1 r2: reg) :=
+  if Int.eq n Int.zero then
+    (Ointconst Int.zero, nil)
+  else if Int.eq n Int.one then
+    (Omove, r1 :: nil)
+  else
+    match Int.is_power2 n with
+    | Some l => (Oshift (Slsl (mk_shift_amount l)), r1 :: nil)
+    | None => (Omul, r1 :: r2 :: nil)
+    end.
+
+Definition make_divimm (n: int) (r1 r2: reg) :=
+  match Int.is_power2 n with
+  | Some l => if Int.ltu l (Int.repr 31)
+              then (Oshrximm l, r1 :: nil)
+              else (Odiv, r1 :: r2 :: nil)
+  | None   => (Odiv, r1 :: r2 :: nil)
+  end.
+
+Definition make_divuimm (n: int) (r1 r2: reg) :=
+  match Int.is_power2 n with
+  | Some l => (Oshift (Slsr (mk_shift_amount l)), r1 :: nil)
+  | None   => (Odivu, r1 :: r2 :: nil)
+  end.
+
+Definition make_andimm (n: int) (r: reg) :=
+  if Int.eq n Int.zero then (Ointconst Int.zero, nil)
+  else if Int.eq n Int.mone then (Omove, r :: nil)
+  else (Oandimm n, r :: nil).
+
+Definition make_orimm (n: int) (r: reg) :=
+  if Int.eq n Int.zero then (Omove, r :: nil)
+  else if Int.eq n Int.mone then (Ointconst Int.mone, nil)
+  else (Oorimm n, r :: nil).
+
+Definition make_xorimm (n: int) (r: reg) :=
+  if Int.eq n Int.zero then (Omove, r :: nil)
+  else if Int.eq n Int.mone then (Onot, r :: nil)
+  else (Oxorimm n, r :: nil).
+
+Nondetfunction op_strength_reduction 
+              (op: operation) (args: list reg) (vl: list approx) :=
+  match op, args, vl with
+  | Oadd, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_addimm n1 r2
+  | Oadd, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_addimm n2 r1
+  | Oaddshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_addimm (eval_static_shift s n2) r1
+  | Osub, r1 :: r2 :: nil, I n1 :: v2 :: nil => (Orsubimm n1, r2 :: nil)
+  | Osub, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_addimm (Int.neg n2) r1
+  | Osubshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_addimm (Int.neg (eval_static_shift s n2)) r1
+  | Orsubshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => (Orsubimm (eval_static_shift s n2), r1 :: nil)
+  | Omul, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_mulimm n1 r2 r1
+  | Omul, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_mulimm n2 r1 r2
+  | Odiv, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_divimm n2 r1 r2
+  | Odivu, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_divuimm n2 r1 r2
+  | Oand, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_andimm n1 r2
+  | Oand, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm n2 r1
+  | Oandshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm (eval_static_shift s n2) r1
+  | Oor, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_orimm n1 r2
+  | Oor, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_orimm n2 r1
+  | Oorshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_orimm (eval_static_shift s n2) r1
+  | Oxor, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_xorimm n1 r2
+  | Oxor, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_xorimm n2 r1
+  | Oxorshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_xorimm (eval_static_shift s n2) r1
+  | Obic, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm (Int.not n2) r1
+  | Obicshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm (Int.not (eval_static_shift s n2)) r1
+  | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shlimm n2 r1 r2
+  | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrimm n2 r1 r2
+  | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1 r2
+  | Ocmp c, args, vl =>
+      let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args')
+  | _, _, _ => (op, args)
+  end.
+
+
+Nondetfunction addr_strength_reduction
+                (addr: addressing) (args: list reg) (vl: list approx) :=
+  match addr, args, vl with
+  | Aindexed2, r1 :: r2 :: nil, S n1 :: I n2 :: nil =>
+      (Ainstack (Int.add n1 n2), nil)
+  | Aindexed2, r1 :: r2 :: nil, I n1 :: S n2 :: nil =>
+      (Ainstack (Int.add n1 n2), nil)
+  | Aindexed2, r1 :: r2 :: nil, I n1 :: v2 :: nil =>
+      (Aindexed n1, r2 :: nil)
+  | Aindexed2, r1 :: r2 :: nil, v1 :: I n2 :: nil =>
+      (Aindexed n2, r1 :: nil)
+  | Aindexed2shift s, r1 :: r2 :: nil, S n1 :: I n2 :: nil =>
+      (Ainstack (Int.add n1 (eval_static_shift s n2)), nil)
+  | Aindexed2shift s, r1 :: r2 :: nil, v1 :: I n2 :: nil =>
+      (Aindexed (eval_static_shift s n2), r1 :: nil)
+  | Aindexed n, r1 :: nil, S n1 :: nil =>
+      (Ainstack (Int.add n1 n), nil)
+  | _, _, _ =>
+      (addr, args)
+  end.
+
+Definition builtin_strength_reduction
+               (ef: external_function) (args: list reg) (vl: list approx) :=
+  (ef, args).
+
+End STRENGTH_REDUCTION.
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index 0e60796..711bb33 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -19,6 +19,7 @@ Require Import Floats.
 Require Import Values.
 Require Import Memory.
 Require Import Globalenvs.
+Require Import Events.
 Require Import Op.
 Require Import Registers.
 Require Import RTL.
@@ -417,6 +418,19 @@ Proof.
   auto.
 Qed.
 
+Lemma builtin_strength_reduction_correct:
+  forall ef args vl m t vres m',
+  vl = approx_regs app args ->
+  external_call ef ge rs##args m t vres m' ->
+  let (ef', args') := builtin_strength_reduction ef args vl in
+  external_call ef' ge rs##args' m t vres m'.
+Proof.
+  (* force MATCH to be used *)
+  assert (val_match_approx (approx_reg app 1%positive) rs#(1%positive))
+    by (apply MATCH).
+  unfold builtin_strength_reduction; intros; simpl; auto.
+Qed.
+
 End STRENGTH_REDUCTION.
 
 End ANALYSIS.
diff --git a/arm/PrintOp.ml b/arm/PrintOp.ml
index dff4e4f..9ebce97 100644
--- a/arm/PrintOp.ml
+++ b/arm/PrintOp.ml
@@ -59,10 +59,6 @@ let print_operation reg pp = function
       fprintf pp "\"%s\" + %ld" (extern_atom id) (camlint_of_coqint ofs)
   | Oaddrstack ofs, [] ->
       fprintf pp "stack(%ld)" (camlint_of_coqint ofs)
-  | Ocast8signed, [r1] -> fprintf pp "int8signed(%a)" reg r1
-  | Ocast8unsigned, [r1] -> fprintf pp "int8unsigned(%a)" reg r1
-  | Ocast16signed, [r1] -> fprintf pp "int16signed(%a)" reg r1
-  | Ocast16unsigned, [r1] -> fprintf pp "int16unsigned(%a)" reg r1
   | Oadd, [r1;r2] -> fprintf pp "%a + %a" reg r1 reg r2
   | Oaddshift s, [r1;r2] -> fprintf pp "%a + %a %a" reg r1 reg r2 shift s
   | Oaddimm n, [r1] -> fprintf pp "%a + %ld" reg r1 (camlint_of_coqint n)
diff --git a/arm/SelectOp.v b/arm/SelectOp.v
deleted file mode 100644
index 64d15cb..0000000
--- a/arm/SelectOp.v
+++ /dev/null
@@ -1,1169 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  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.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** 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 Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Globalenvs.
-Require Cminor.
-Require Import Op.
-Require Import CminorSel.
-
-Open Local Scope cminorsel_scope.
-
-(** ** Constants **)
-
-Definition addrsymbol (id: ident) (ofs: int) :=
-  Eop (Oaddrsymbol id ofs) Enil.
-
-Definition addrstack (ofs: int) :=
-  Eop (Oaddrstack ofs) Enil.
-
-(** ** Integer logical negation *)
-
-(** Original definition:
-<<
-Nondetfunction notint (e: expr) :=
-  match e with
-  | Eop (Oshift s) (t1:::Enil) => Eop (Onotshift s) (t1:::Enil)
-  | Eop Onot (t1:::Enil) => t1
-  | Eop (Onotshift s) (t1:::Enil) => Eop (Oshift s) (t1:::Enil)
-  | _ => Eop Onot (e:::Enil)
-  end.
->>
-*)
-
-Inductive notint_cases: forall (e: expr), Type :=
-  | notint_case1: forall s t1, notint_cases (Eop (Oshift s) (t1:::Enil))
-  | notint_case2: forall t1, notint_cases (Eop Onot (t1:::Enil))
-  | notint_case3: forall s t1, notint_cases (Eop (Onotshift s) (t1:::Enil))
-  | notint_default: forall (e: expr), notint_cases e.
-
-Definition notint_match (e: expr) :=
-  match e as zz1 return notint_cases zz1 with
-  | Eop (Oshift s) (t1:::Enil) => notint_case1 s t1
-  | Eop Onot (t1:::Enil) => notint_case2 t1
-  | Eop (Onotshift s) (t1:::Enil) => notint_case3 s t1
-  | e => notint_default e
-  end.
-
-Definition notint (e: expr) :=
-  match notint_match e with
-  | notint_case1 s t1 => (* Eop (Oshift s) (t1:::Enil) *) 
-      Eop (Onotshift s) (t1:::Enil)
-  | notint_case2 t1 => (* Eop Onot (t1:::Enil) *) 
-      t1
-  | notint_case3 s t1 => (* Eop (Onotshift s) (t1:::Enil) *) 
-      Eop (Oshift s) (t1:::Enil)
-  | notint_default e =>
-      Eop Onot (e:::Enil)
-  end.
-
-
-(** ** Boolean negation *)
-
-Fixpoint notbool (e: expr) {struct e} : expr :=
-  let default := Eop (Ocmp (Ccompuimm Ceq Int.zero)) (e ::: Enil) in
-  match e with
-  | Eop (Ointconst n) Enil =>
-      Eop (Ointconst (if Int.eq n Int.zero then Int.one else Int.zero)) Enil
-  | Eop (Ocmp cond) args =>
-      Eop (Ocmp (negate_condition cond)) args
-  | Econdition e1 e2 e3 =>
-      Econdition e1 (notbool e2) (notbool e3)
-  | _ =>
-      default
-  end.
-
-(** ** 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 (Int.add n m)) Enil
-  | Eop (Oaddrstack m) Enil      => Eop (Oaddrstack (Int.add 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 (Int.add n m)) Enil
-  | addimm_case3 m => (* Eop (Oaddrstack m) Enil *) 
-      Eop (Oaddrstack (Int.add 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
-  | 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), t2 => addimm n1 (Eop Oadd (t1:::t2:::Enil))
-  | t1, Eop (Ointconst n2) Enil => addimm n2 t1
-  | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil))
-  | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oaddshift s) (t2:::t1:::Enil)
-  | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oaddshift s) (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 n1 t1 n2 t2, add_cases (Eop (Oaddimm n1) (t1:::Enil)) (Eop (Oaddimm n2) (t2:::Enil))
-  | add_case3: forall n1 t1 t2, add_cases (Eop(Oaddimm n1) (t1:::Enil)) (t2)
-  | add_case4: forall t1 n2, add_cases (t1) (Eop (Ointconst n2) Enil)
-  | add_case5: forall t1 n2 t2, add_cases (t1) (Eop (Oaddimm n2) (t2:::Enil))
-  | add_case6: forall s t1 t2, add_cases (Eop (Oshift s) (t1:::Enil)) (t2)
-  | add_case7: forall t1 s t2, add_cases (t1) (Eop (Oshift s) (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
-  | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => add_case2 n1 t1 n2 t2
-  | Eop(Oaddimm n1) (t1:::Enil), t2 => add_case3 n1 t1 t2
-  | t1, Eop (Ointconst n2) Enil => add_case4 t1 n2
-  | t1, Eop (Oaddimm n2) (t2:::Enil) => add_case5 t1 n2 t2
-  | Eop (Oshift s) (t1:::Enil), t2 => add_case6 s t1 t2
-  | t1, Eop (Oshift s) (t2:::Enil) => add_case7 t1 s 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 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_case3 n1 t1 t2 => (* Eop(Oaddimm n1) (t1:::Enil), t2 *) 
-      addimm n1 (Eop Oadd (t1:::t2:::Enil))
-  | add_case4 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) 
-      addimm n2 t1
-  | add_case5 t1 n2 t2 => (* t1, Eop (Oaddimm n2) (t2:::Enil) *) 
-      addimm n2 (Eop Oadd (t1:::t2:::Enil))
-  | add_case6 s t1 t2 => (* Eop (Oshift s) (t1:::Enil), t2 *) 
-      Eop (Oaddshift s) (t2:::t1:::Enil)
-  | add_case7 t1 s t2 => (* t1, Eop (Oshift s) (t2:::Enil) *) 
-      Eop (Oaddshift s) (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 (Ointconst n1) Enil, t2 => Eop (Orsubimm n1) (t2:::Enil)
-  | Eop (Oshift s) (t1:::Enil), t2 => Eop (Orsubshift s) (t2:::t1:::Enil)
-  | t1, Eop (Oshift s) (t2:::Enil) => Eop (Osubshift s) (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_case5: forall n1 t2, sub_cases (Eop (Ointconst n1) Enil) (t2)
-  | sub_case6: forall s t1 t2, sub_cases (Eop (Oshift s) (t1:::Enil)) (t2)
-  | sub_case7: forall t1 s t2, sub_cases (t1) (Eop (Oshift s) (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
-  | Eop (Ointconst n1) Enil, t2 => sub_case5 n1 t2
-  | Eop (Oshift s) (t1:::Enil), t2 => sub_case6 s t1 t2
-  | t1, Eop (Oshift s) (t2:::Enil) => sub_case7 t1 s 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_case5 n1 t2 => (* Eop (Ointconst n1) Enil, t2 *) 
-      Eop (Orsubimm n1) (t2:::Enil)
-  | sub_case6 s t1 t2 => (* Eop (Oshift s) (t1:::Enil), t2 *) 
-      Eop (Orsubshift s) (t2:::t1:::Enil)
-  | sub_case7 t1 s t2 => (* t1, Eop (Oshift s) (t2:::Enil) *) 
-      Eop (Osubshift s) (t1:::t2:::Enil)
-  | sub_default e1 e2 =>
-      Eop Osub (e1:::e2:::Enil)
-  end.
-
-
-Definition negint (e: expr) := Eop (Orsubimm Int.zero) (e ::: Enil).
-
-(** ** 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 (Oshift (Slsl n1)) (t1:::Enil) =>
-        if Int.ltu (Int.add n n1) Int.iwordsize
-        then Eop (Oshift (Slsl (mk_shift_amount(Int.add n n1)))) (t1:::Enil)
-        else Eop (Oshift (Slsl (mk_shift_amount n))) (e1:::Enil)
-    | _ => Eop (Oshift (Slsl (mk_shift_amount 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 (Oshift (Slsl 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 (Oshift (Slsl 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 (Oshift (Slsl n1)) (t1:::Enil) *) 
-      if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshift (Slsl (mk_shift_amount(Int.add n n1)))) (t1:::Enil) else Eop (Oshift (Slsl (mk_shift_amount n))) (e1:::Enil)
-  | shlimm_default e1 =>
-      Eop (Oshift (Slsl (mk_shift_amount 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 (Oshift (Slsr n1)) (t1:::Enil) =>
-        if Int.ltu (Int.add n n1) Int.iwordsize
-        then Eop (Oshift (Slsr (mk_shift_amount (Int.add n n1)))) (t1:::Enil)
-        else Eop (Oshift (Slsr (mk_shift_amount n))) (e1:::Enil)
-    | _ => Eop (Oshift (Slsr (mk_shift_amount 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 (Oshift (Slsr 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 (Oshift (Slsr 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 (Oshift (Slsr n1)) (t1:::Enil) *) 
-      if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshift (Slsr (mk_shift_amount (Int.add n n1)))) (t1:::Enil) else Eop (Oshift (Slsr (mk_shift_amount n))) (e1:::Enil)
-  | shruimm_default e1 =>
-      Eop (Oshift (Slsr (mk_shift_amount 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 (Oshift (Sasr n1)) (t1:::Enil) =>
-        if Int.ltu (Int.add n n1) Int.iwordsize
-        then Eop (Oshift (Sasr (mk_shift_amount (Int.add n n1)))) (t1:::Enil)
-        else Eop (Oshift (Sasr (mk_shift_amount n))) (e1:::Enil)
-    | _ => Eop (Oshift (Sasr (mk_shift_amount 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 (Oshift (Sasr 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 (Oshift (Sasr 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 (Oshift (Sasr n1)) (t1:::Enil) *) 
-      if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshift (Sasr (mk_shift_amount (Int.add n n1)))) (t1:::Enil) else Eop (Oshift (Sasr (mk_shift_amount n))) (e1:::Enil)
-  | shrimm_default e1 =>
-      Eop (Oshift (Sasr (mk_shift_amount 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.
-
-
-(** ** 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
-  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 (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_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
-  | e2 => andimm_default e2
-  end.
-
-Definition andimm (n1: int) (e2: expr) :=
- if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil 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_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 (Oshift s) (t1:::Enil), t2 => Eop (Oandshift s) (t2:::t1:::Enil)
-  | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oandshift s) (t1:::t2:::Enil)
-  | Eop (Onotshift s) (t1:::Enil), t2 => Eop (Obicshift s) (t2:::t1:::Enil)
-  | t1, Eop (Onotshift s) (t2:::Enil) => Eop (Obicshift s) (t1:::t2:::Enil)
-  | Eop Onot (t1:::Enil), t2 => Eop Obic (t2:::t1:::Enil)
-  | t1, Eop Onot (t2:::Enil) => Eop Obic (t1:::t2:::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 s t1 t2, and_cases (Eop (Oshift s) (t1:::Enil)) (t2)
-  | and_case4: forall t1 s t2, and_cases (t1) (Eop (Oshift s) (t2:::Enil))
-  | and_case5: forall s t1 t2, and_cases (Eop (Onotshift s) (t1:::Enil)) (t2)
-  | and_case6: forall t1 s t2, and_cases (t1) (Eop (Onotshift s) (t2:::Enil))
-  | and_case7: forall t1 t2, and_cases (Eop Onot (t1:::Enil)) (t2)
-  | and_case8: 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 (Oshift s) (t1:::Enil), t2 => and_case3 s t1 t2
-  | t1, Eop (Oshift s) (t2:::Enil) => and_case4 t1 s t2
-  | Eop (Onotshift s) (t1:::Enil), t2 => and_case5 s t1 t2
-  | t1, Eop (Onotshift s) (t2:::Enil) => and_case6 t1 s t2
-  | Eop Onot (t1:::Enil), t2 => and_case7 t1 t2
-  | t1, Eop Onot (t2:::Enil) => and_case8 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 s t1 t2 => (* Eop (Oshift s) (t1:::Enil), t2 *) 
-      Eop (Oandshift s) (t2:::t1:::Enil)
-  | and_case4 t1 s t2 => (* t1, Eop (Oshift s) (t2:::Enil) *) 
-      Eop (Oandshift s) (t1:::t2:::Enil)
-  | and_case5 s t1 t2 => (* Eop (Onotshift s) (t1:::Enil), t2 *) 
-      Eop (Obicshift s) (t2:::t1:::Enil)
-  | and_case6 t1 s t2 => (* t1, Eop (Onotshift s) (t2:::Enil) *) 
-      Eop (Obicshift s) (t1:::t2:::Enil)
-  | and_case7 t1 t2 => (* Eop Onot (t1:::Enil), t2 *) 
-      Eop Obic (t2:::t1:::Enil)
-  | and_case8 t1 t2 => (* t1, Eop Onot (t2:::Enil) *) 
-      Eop Obic (t1:::t2:::Enil)
-  | and_default e1 e2 =>
-      Eop Oand (e1:::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 orimm (n1: int) (e2: expr) :=
-  if Int.eq n1 Int.zero then e2 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 (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_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
-  | e2 => orimm_default e2
-  end.
-
-Definition orimm (n1: int) (e2: expr) :=
- if Int.eq n1 Int.zero then e2 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_default e2 =>
-      Eop (Oorimm n1) (e2:::Enil)
-  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 (Oshift (Slsl n1)) (t1:::Enil), Eop (Oshift (Slsr n2)) (t2:::Enil) =>
-      if Int.eq (Int.add n1 n2) Int.iwordsize
-      && same_expr_pure t1 t2
-      then Eop (Oshift (Sror n2)) (t1:::Enil)
-      else Eop (Oorshift (Slsr n2)) (e1:::t2:::Enil)
-  | Eop (Oshift (Slsr n1)) (t1:::Enil), Eop (Oshift (Slsl n2)) (t2:::Enil) =>
-      if Int.eq (Int.add n2 n1) Int.iwordsize
-      && same_expr_pure t1 t2
-      then Eop (Oshift (Sror n1)) (t1:::Enil)
-      else Eop (Oorshift (Slsl n2)) (e1:::t2:::Enil)
-  | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oorshift s) (t2:::t1:::Enil)
-  | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oorshift s) (t1:::t2:::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 (Oshift (Slsl n1)) (t1:::Enil)) (Eop (Oshift (Slsr n2)) (t2:::Enil))
-  | or_case4: forall n1 t1 n2 t2, or_cases (Eop (Oshift (Slsr n1)) (t1:::Enil)) (Eop (Oshift (Slsl n2)) (t2:::Enil))
-  | or_case5: forall s t1 t2, or_cases (Eop (Oshift s) (t1:::Enil)) (t2)
-  | or_case6: forall t1 s t2, or_cases (t1) (Eop (Oshift s) (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 (Oshift (Slsl n1)) (t1:::Enil), Eop (Oshift (Slsr n2)) (t2:::Enil) => or_case3 n1 t1 n2 t2
-  | Eop (Oshift (Slsr n1)) (t1:::Enil), Eop (Oshift (Slsl n2)) (t2:::Enil) => or_case4 n1 t1 n2 t2
-  | Eop (Oshift s) (t1:::Enil), t2 => or_case5 s t1 t2
-  | t1, Eop (Oshift s) (t2:::Enil) => or_case6 t1 s 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 (Oshift (Slsl n1)) (t1:::Enil), Eop (Oshift (Slsr n2)) (t2:::Enil) *) 
-      if Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2 then Eop (Oshift (Sror n2)) (t1:::Enil) else Eop (Oorshift (Slsr n2)) (e1:::t2:::Enil)
-  | or_case4 n1 t1 n2 t2 => (* Eop (Oshift (Slsr n1)) (t1:::Enil), Eop (Oshift (Slsl n2)) (t2:::Enil) *) 
-      if Int.eq (Int.add n2 n1) Int.iwordsize && same_expr_pure t1 t2 then Eop (Oshift (Sror n1)) (t1:::Enil) else Eop (Oorshift (Slsl n2)) (e1:::t2:::Enil)
-  | or_case5 s t1 t2 => (* Eop (Oshift s) (t1:::Enil), t2 *) 
-      Eop (Oorshift s) (t2:::t1:::Enil)
-  | or_case6 t1 s t2 => (* t1, Eop (Oshift s) (t2:::Enil) *) 
-      Eop (Oorshift s) (t1:::t2:::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) => Eop (Oxorimm (Int.xor n1 n2)) (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) *) 
-      Eop (Oxorimm (Int.xor n1 n2)) (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 (Oshift s) (t1:::Enil), t2 => Eop (Oxorshift s) (t2:::t1:::Enil)
-  | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oxorshift s) (t1:::t2:::Enil)
-  | _, _ => 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_case3: forall s t1 t2, xor_cases (Eop (Oshift s) (t1:::Enil)) (t2)
-  | xor_case4: forall t1 s t2, xor_cases (t1) (Eop (Oshift s) (t2:::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
-  | Eop (Oshift s) (t1:::Enil), t2 => xor_case3 s t1 t2
-  | t1, Eop (Oshift s) (t2:::Enil) => xor_case4 t1 s t2
-  | 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_case3 s t1 t2 => (* Eop (Oshift s) (t1:::Enil), t2 *) 
-      Eop (Oxorshift s) (t2:::t1:::Enil)
-  | xor_case4 t1 s t2 => (* t1, Eop (Oshift s) (t2:::Enil) *) 
-      Eop (Oxorshift s) (t1:::t2:::Enil)
-  | xor_default e1 e2 =>
-      Eop Oxor (e1:::e2:::Enil)
-  end.
-
-
-(** ** Integer division and modulus *)
-
-Definition mod_aux (divop: operation) (e1 e2: expr) :=
-  Elet e1
-    (Elet (lift e2)
-      (Eop Osub (Eletvar 1 :::
-                 Eop Omul (Eop divop (Eletvar 1 ::: Eletvar 0 ::: Enil) :::
-                           Eletvar 0 :::
-                           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.
-
-(** Original definition:
-<<
-Nondetfunction divu (e1: expr) (e2: expr) :=
-  match e2 with
-  | Eop (Ointconst n2) Enil => divuimm e1 n2
-  | _ => Eop Odivu (e1:::e2:::Enil)
-  end.
->>
-*)
-
-Inductive divu_cases: forall (e2: expr), Type :=
-  | divu_case1: forall n2, divu_cases (Eop (Ointconst n2) Enil)
-  | divu_default: forall (e2: expr), divu_cases e2.
-
-Definition divu_match (e2: expr) :=
-  match e2 as zz1 return divu_cases zz1 with
-  | Eop (Ointconst n2) Enil => divu_case1 n2
-  | e2 => divu_default e2
-  end.
-
-Definition divu (e1: expr) (e2: expr) :=
-  match divu_match e2 with
-  | divu_case1 n2 => (* Eop (Ointconst n2) Enil *) 
-      divuimm e1 n2
-  | divu_default e2 =>
-      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.
-
-(** Original definition:
-<<
-Nondetfunction modu (e1: expr) (e2: expr) :=
-  match e2 with
-  | Eop (Ointconst n2) Enil => moduimm e1 n2
-  | _ => mod_aux Odivu e1 e2
-  end.
->>
-*)
-
-Inductive modu_cases: forall (e2: expr), Type :=
-  | modu_case1: forall n2, modu_cases (Eop (Ointconst n2) Enil)
-  | modu_default: forall (e2: expr), modu_cases e2.
-
-Definition modu_match (e2: expr) :=
-  match e2 as zz1 return modu_cases zz1 with
-  | Eop (Ointconst n2) Enil => modu_case1 n2
-  | e2 => modu_default e2
-  end.
-
-Definition modu (e1: expr) (e2: expr) :=
-  match modu_match e2 with
-  | modu_case1 n2 => (* Eop (Ointconst n2) Enil *) 
-      moduimm e1 n2
-  | modu_default e2 =>
-      mod_aux Odivu e1 e2
-  end.
-
-
-(** ** 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 divf (e1 e2: expr) :=  Eop Odivf (e1 ::: e2 ::: Enil).
-
-(** ** Comparisons *)
-
-(** Original definition:
-<<
-Nondetfunction comp (c: comparison) (e1: expr) (e2: expr) :=
-  match e1, e2 with
-  | Eop (Ointconst n1) Enil, t2 =>
-      Eop (Ocmp (Ccompimm (swap_comparison c) n1)) (t2:::Enil)
-  | t1, Eop (Ointconst n2) Enil =>
-      Eop (Ocmp (Ccompimm c n2)) (t1:::Enil)
-  | Eop (Oshift s) (t1:::Enil), t2 =>
-      Eop (Ocmp (Ccompshift (swap_comparison c) s)) (t2:::t1:::Enil)
-  | t1, Eop (Oshift s) (t2:::Enil) =>
-      Eop (Ocmp (Ccompshift c s)) (t1:::t2:::Enil)
-  | _, _ =>
-      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_case3: forall s t1 t2, comp_cases (Eop (Oshift s) (t1:::Enil)) (t2)
-  | comp_case4: forall t1 s t2, comp_cases (t1) (Eop (Oshift s) (t2:::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
-  | Eop (Oshift s) (t1:::Enil), t2 => comp_case3 s t1 t2
-  | t1, Eop (Oshift s) (t2:::Enil) => comp_case4 t1 s t2
-  | 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 *) 
-      Eop (Ocmp (Ccompimm (swap_comparison c) n1)) (t2:::Enil)
-  | comp_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) 
-      Eop (Ocmp (Ccompimm c n2)) (t1:::Enil)
-  | comp_case3 s t1 t2 => (* Eop (Oshift s) (t1:::Enil), t2 *) 
-      Eop (Ocmp (Ccompshift (swap_comparison c) s)) (t2:::t1:::Enil)
-  | comp_case4 t1 s t2 => (* t1, Eop (Oshift s) (t2:::Enil) *) 
-      Eop (Ocmp (Ccompshift c s)) (t1:::t2:::Enil)
-  | 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 =>
-      Eop (Ocmp (Ccompuimm (swap_comparison c) n1)) (t2:::Enil)
-  | t1, Eop (Ointconst n2) Enil =>
-      Eop (Ocmp (Ccompuimm c n2)) (t1:::Enil)
-  | Eop (Oshift s) (t1:::Enil), t2 =>
-      Eop (Ocmp (Ccompushift (swap_comparison c) s)) (t2:::t1:::Enil)
-  | t1, Eop (Oshift s) (t2:::Enil) =>
-      Eop (Ocmp (Ccompushift c s)) (t1:::t2:::Enil)
-  | _, _ =>
-      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_case3: forall s t1 t2, compu_cases (Eop (Oshift s) (t1:::Enil)) (t2)
-  | compu_case4: forall t1 s t2, compu_cases (t1) (Eop (Oshift s) (t2:::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
-  | Eop (Oshift s) (t1:::Enil), t2 => compu_case3 s t1 t2
-  | t1, Eop (Oshift s) (t2:::Enil) => compu_case4 t1 s t2
-  | 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 *) 
-      Eop (Ocmp (Ccompuimm (swap_comparison c) n1)) (t2:::Enil)
-  | compu_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) 
-      Eop (Ocmp (Ccompuimm c n2)) (t1:::Enil)
-  | compu_case3 s t1 t2 => (* Eop (Oshift s) (t1:::Enil), t2 *) 
-      Eop (Ocmp (Ccompushift (swap_comparison c) s)) (t2:::t1:::Enil)
-  | compu_case4 t1 s t2 => (* t1, Eop (Oshift s) (t2:::Enil) *) 
-      Eop (Ocmp (Ccompushift c s)) (t1:::t2:::Enil)
-  | 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).
-
-(** ** Integer conversions *)
-
-Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e.
-
-Definition cast8signed (e: expr) := shrimm (shlimm e (Int.repr 24)) (Int.repr 24).
-
-Definition cast16unsigned (e: expr) := andimm (Int.repr 65535) e.
-
-Definition cast16signed (e: expr) := shrimm (shlimm e (Int.repr 16)) (Int.repr 16).
-
-(** ** Floating-point conversions *)
-
-Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil).
-Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil).
-Definition intuoffloat (e: expr) := Eop Ointuoffloat (e ::: Enil).
-Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil).
-Definition floatofintu (e: expr) := Eop Ofloatofintu (e ::: Enil).
-
-(** ** Recognition of addressing modes for load and store operations *)
-
-(** We do not recognize the [Aindexed2] and [Aindexed2shift] modes
-    for floating-point accesses, since these are not supported
-    by the hardware and emulated inefficiently in [Asmgen].
-    Likewise, [Aindexed2shift] are not supported for halfword
-    and signed byte accesses. *)
-
-Definition can_use_Aindexed2 (chunk: memory_chunk): bool :=
-  match chunk with
-  | Mint8signed => true
-  | Mint8unsigned => true
-  | Mint16signed => true
-  | Mint16unsigned => true
-  | Mint32 => true
-  | Mfloat32 => false
-  | Mfloat64 => false
-  end.
-
-Definition can_use_Aindexed2shift (chunk: memory_chunk): bool :=
-  match chunk with
-  | Mint8signed => false
-  | Mint8unsigned => true
-  | Mint16signed => false
-  | Mint16unsigned => false
-  | Mint32 => true
-  | Mfloat32 => false
-  | Mfloat64 => false
-  end.
-
-(** Original definition:
-<<
-Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
-  match e with
-  | Eop (Oaddrstack n) Enil => (Ainstack n, Enil)
-  | Eop (Oaddimm n) (e1:::Enil) => (Aindexed n, e1:::Enil)
-  | Eop (Oaddshift s) (e1:::e2:::Enil) =>
-      if can_use_Aindexed2shift chunk
-      then (Aindexed2shift s, e1:::e2:::Enil)
-      else (Aindexed Int.zero, Eop (Oaddshift s) (e1:::e2:::Enil) ::: Enil)
-  | Eop Oadd (e1:::e2:::Enil) =>
-      if can_use_Aindexed2 chunk
-      then (Aindexed2, e1:::e2:::Enil)
-      else (Aindexed Int.zero, Eop Oadd (e1:::e2:::Enil) ::: Enil)
-  | _ => (Aindexed Int.zero, e:::Enil)
-  end.
->>
-*)
-
-Inductive addressing_cases: forall (e: expr), Type :=
-  | addressing_case1: forall n, addressing_cases (Eop (Oaddrstack n) Enil)
-  | addressing_case2: forall n e1, addressing_cases (Eop (Oaddimm n) (e1:::Enil))
-  | addressing_case3: forall s e1 e2, addressing_cases (Eop (Oaddshift s) (e1:::e2:::Enil))
-  | addressing_case4: forall e1 e2, addressing_cases (Eop Oadd (e1:::e2:::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 (Oaddimm n) (e1:::Enil) => addressing_case2 n e1
-  | Eop (Oaddshift s) (e1:::e2:::Enil) => addressing_case3 s e1 e2
-  | Eop Oadd (e1:::e2:::Enil) => addressing_case4 e1 e2
-  | 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 n e1 => (* Eop (Oaddimm n) (e1:::Enil) *) 
-      (Aindexed n, e1:::Enil)
-  | addressing_case3 s e1 e2 => (* Eop (Oaddshift s) (e1:::e2:::Enil) *) 
-      if can_use_Aindexed2shift chunk then (Aindexed2shift s, e1:::e2:::Enil) else (Aindexed Int.zero, Eop (Oaddshift s) (e1:::e2:::Enil) ::: Enil)
-  | addressing_case4 e1 e2 => (* Eop Oadd (e1:::e2:::Enil) *) 
-      if can_use_Aindexed2 chunk then (Aindexed2, e1:::e2:::Enil) else (Aindexed Int.zero, Eop Oadd (e1:::e2:::Enil) ::: Enil)
-  | addressing_default e =>
-      (Aindexed Int.zero, e:::Enil)
-  end.
-
-
-
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
new file mode 100644
index 0000000..432db94
--- /dev/null
+++ b/arm/SelectOp.vp
@@ -0,0 +1,444 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** 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 Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Floats.
+Require Import Values.
+Require Import Memory.
+Require Import Globalenvs.
+Require Cminor.
+Require Import Op.
+Require Import CminorSel.
+
+Open Local Scope cminorsel_scope.
+
+(** ** Constants **)
+
+Definition addrsymbol (id: ident) (ofs: int) :=
+  Eop (Oaddrsymbol id ofs) Enil.
+
+Definition addrstack (ofs: int) :=
+  Eop (Oaddrstack ofs) Enil.
+
+(** ** Integer logical negation *)
+
+Nondetfunction notint (e: expr) :=
+  match e with
+  | Eop (Oshift s) (t1:::Enil) => Eop (Onotshift s) (t1:::Enil)
+  | Eop Onot (t1:::Enil) => t1
+  | Eop (Onotshift s) (t1:::Enil) => Eop (Oshift s) (t1:::Enil)
+  | _ => Eop Onot (e:::Enil)
+  end.
+
+(** ** Boolean negation *)
+
+Fixpoint notbool (e: expr) {struct e} : expr :=
+  let default := Eop (Ocmp (Ccompuimm Ceq Int.zero)) (e ::: Enil) in
+  match e with
+  | Eop (Ointconst n) Enil =>
+      Eop (Ointconst (if Int.eq n Int.zero then Int.one else Int.zero)) Enil
+  | Eop (Ocmp cond) args =>
+      Eop (Ocmp (negate_condition cond)) args
+  | Econdition e1 e2 e3 =>
+      Econdition e1 (notbool e2) (notbool e3)
+  | _ =>
+      default
+  end.
+
+(** ** Integer addition and pointer addition *)
+
+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 (Int.add n m)) Enil
+  | Eop (Oaddrstack m) Enil      => Eop (Oaddrstack (Int.add n m)) Enil
+  | Eop (Oaddimm m) (t ::: Enil) => Eop (Oaddimm(Int.add n m)) (t ::: Enil)
+  | _                            => Eop (Oaddimm n) (e ::: Enil)
+  end.
+
+Nondetfunction add (e1: expr) (e2: expr) :=
+  match e1, e2 with
+  | Eop (Ointconst n1) Enil, t2 => addimm n1 t2
+  | 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), t2 => addimm n1 (Eop Oadd (t1:::t2:::Enil))
+  | t1, Eop (Ointconst n2) Enil => addimm n2 t1
+  | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil))
+  | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oaddshift s) (t2:::t1:::Enil)
+  | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oaddshift s) (t1:::t2:::Enil)
+  | _, _ => Eop Oadd (e1:::e2:::Enil)
+  end.
+
+(** ** Integer and pointer subtraction *)
+
+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 (Ointconst n1) Enil, t2 => Eop (Orsubimm n1) (t2:::Enil)
+  | Eop (Oshift s) (t1:::Enil), t2 => Eop (Orsubshift s) (t2:::t1:::Enil)
+  | t1, Eop (Oshift s) (t2:::Enil) => Eop (Osubshift s) (t1:::t2:::Enil)
+  | _, _ => Eop Osub (e1:::e2:::Enil)
+  end.
+
+Definition negint (e: expr) := Eop (Orsubimm Int.zero) (e ::: Enil).
+
+(** ** Immediate shifts *)
+
+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 (Oshift (Slsl n1)) (t1:::Enil) =>
+        if Int.ltu (Int.add n n1) Int.iwordsize
+        then Eop (Oshift (Slsl (mk_shift_amount(Int.add n n1)))) (t1:::Enil)
+        else Eop (Oshift (Slsl (mk_shift_amount n))) (e1:::Enil)
+    | _ => Eop (Oshift (Slsl (mk_shift_amount n))) (e1:::Enil)
+    end.
+
+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 (Oshift (Slsr n1)) (t1:::Enil) =>
+        if Int.ltu (Int.add n n1) Int.iwordsize
+        then Eop (Oshift (Slsr (mk_shift_amount (Int.add n n1)))) (t1:::Enil)
+        else Eop (Oshift (Slsr (mk_shift_amount n))) (e1:::Enil)
+    | _ => Eop (Oshift (Slsr (mk_shift_amount n))) (e1:::Enil)
+    end.
+
+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 (Oshift (Sasr n1)) (t1:::Enil) =>
+        if Int.ltu (Int.add n n1) Int.iwordsize
+        then Eop (Oshift (Sasr (mk_shift_amount (Int.add n n1)))) (t1:::Enil)
+        else Eop (Oshift (Sasr (mk_shift_amount n))) (e1:::Enil)
+    | _ => Eop (Oshift (Sasr (mk_shift_amount 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.
+
+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.
+
+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.
+
+(** ** Bitwise and, or, xor *)
+
+Nondetfunction andimm (n1: int) (e2: expr) := 
+  if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil 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 (Oandimm n1) (e2:::Enil)
+  end.
+
+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 (Oshift s) (t1:::Enil), t2 => Eop (Oandshift s) (t2:::t1:::Enil)
+  | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oandshift s) (t1:::t2:::Enil)
+  | Eop (Onotshift s) (t1:::Enil), t2 => Eop (Obicshift s) (t2:::t1:::Enil)
+  | t1, Eop (Onotshift s) (t2:::Enil) => Eop (Obicshift s) (t1:::t2:::Enil)
+  | Eop Onot (t1:::Enil), t2 => Eop Obic (t2:::t1:::Enil)
+  | t1, Eop Onot (t2:::Enil) => Eop Obic (t1:::t2:::Enil)
+  | _, _ => Eop Oand (e1:::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.
+
+Nondetfunction orimm (n1: int) (e2: expr) :=
+  if Int.eq n1 Int.zero then e2 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 (Oorimm n1) (e2:::Enil)
+  end.
+
+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 (Oshift (Slsl n1)) (t1:::Enil), Eop (Oshift (Slsr n2)) (t2:::Enil) =>
+      if Int.eq (Int.add n1 n2) Int.iwordsize
+      && same_expr_pure t1 t2
+      then Eop (Oshift (Sror n2)) (t1:::Enil)
+      else Eop (Oorshift (Slsr n2)) (e1:::t2:::Enil)
+  | Eop (Oshift (Slsr n1)) (t1:::Enil), Eop (Oshift (Slsl n2)) (t2:::Enil) =>
+      if Int.eq (Int.add n2 n1) Int.iwordsize
+      && same_expr_pure t1 t2
+      then Eop (Oshift (Sror n1)) (t1:::Enil)
+      else Eop (Oorshift (Slsl n2)) (e1:::t2:::Enil)
+  | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oorshift s) (t2:::t1:::Enil)
+  | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oorshift s) (t1:::t2:::Enil)
+  | _, _ => Eop Oor (e1:::e2:::Enil)
+  end.
+
+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) => Eop (Oxorimm (Int.xor n1 n2)) (t2:::Enil)
+  | _ => Eop (Oxorimm n1) (e2:::Enil)
+  end.
+
+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 (Oshift s) (t1:::Enil), t2 => Eop (Oxorshift s) (t2:::t1:::Enil)
+  | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oxorshift s) (t1:::t2:::Enil)
+  | _, _ => Eop Oxor (e1:::e2:::Enil)
+  end.
+
+(** ** Integer division and modulus *)
+
+Definition mod_aux (divop: operation) (e1 e2: expr) :=
+  Elet e1
+    (Elet (lift e2)
+      (Eop Osub (Eletvar 1 :::
+                 Eop Omul (Eop divop (Eletvar 1 ::: Eletvar 0 ::: Enil) :::
+                           Eletvar 0 :::
+                           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.
+
+(** ** General shifts *)
+
+Nondetfunction shl (e1: expr) (e2: expr) :=
+  match e2 with
+  | Eop (Ointconst n2) Enil => shlimm e1 n2
+  | _ => Eop Oshl (e1:::e2:::Enil)
+  end.
+
+Nondetfunction shr (e1: expr) (e2: expr) :=
+  match e2 with
+  | Eop (Ointconst n2) Enil => shrimm e1 n2
+  | _ => Eop Oshr (e1:::e2:::Enil)
+  end.
+
+Nondetfunction shru (e1: expr) (e2: expr) :=
+  match e2 with
+  | Eop (Ointconst n2) Enil => shruimm e1 n2
+  | _ => 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 divf (e1 e2: expr) :=  Eop Odivf (e1 ::: e2 ::: Enil).
+
+(** ** Comparisons *)
+
+Nondetfunction comp (c: comparison) (e1: expr) (e2: expr) :=
+  match e1, e2 with
+  | Eop (Ointconst n1) Enil, t2 =>
+      Eop (Ocmp (Ccompimm (swap_comparison c) n1)) (t2:::Enil)
+  | t1, Eop (Ointconst n2) Enil =>
+      Eop (Ocmp (Ccompimm c n2)) (t1:::Enil)
+  | Eop (Oshift s) (t1:::Enil), t2 =>
+      Eop (Ocmp (Ccompshift (swap_comparison c) s)) (t2:::t1:::Enil)
+  | t1, Eop (Oshift s) (t2:::Enil) =>
+      Eop (Ocmp (Ccompshift c s)) (t1:::t2:::Enil)
+  | _, _ =>
+      Eop (Ocmp (Ccomp c)) (e1:::e2:::Enil)
+  end.
+
+Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) :=
+  match e1, e2 with
+  | Eop (Ointconst n1) Enil, t2 =>
+      Eop (Ocmp (Ccompuimm (swap_comparison c) n1)) (t2:::Enil)
+  | t1, Eop (Ointconst n2) Enil =>
+      Eop (Ocmp (Ccompuimm c n2)) (t1:::Enil)
+  | Eop (Oshift s) (t1:::Enil), t2 =>
+      Eop (Ocmp (Ccompushift (swap_comparison c) s)) (t2:::t1:::Enil)
+  | t1, Eop (Oshift s) (t2:::Enil) =>
+      Eop (Ocmp (Ccompushift c s)) (t1:::t2:::Enil)
+  | _, _ =>
+      Eop (Ocmp (Ccompu c)) (e1:::e2:::Enil)
+  end.
+
+Definition compf (c: comparison) (e1: expr) (e2: expr) :=
+  Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil).
+
+(** ** Integer conversions *)
+
+Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e.
+
+Definition cast8signed (e: expr) := shrimm (shlimm e (Int.repr 24)) (Int.repr 24).
+
+Definition cast16unsigned (e: expr) := andimm (Int.repr 65535) e.
+
+Definition cast16signed (e: expr) := shrimm (shlimm e (Int.repr 16)) (Int.repr 16).
+
+(** ** Floating-point conversions *)
+
+Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil).
+Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil).
+Definition intuoffloat (e: expr) := Eop Ointuoffloat (e ::: Enil).
+Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil).
+Definition floatofintu (e: expr) := Eop Ofloatofintu (e ::: Enil).
+
+(** ** Recognition of addressing modes for load and store operations *)
+
+(** We do not recognize the [Aindexed2] and [Aindexed2shift] modes
+    for floating-point accesses, since these are not supported
+    by the hardware and emulated inefficiently in [Asmgen].
+    Likewise, [Aindexed2shift] are not supported for halfword
+    and signed byte accesses. *)
+
+Definition can_use_Aindexed2 (chunk: memory_chunk): bool :=
+  match chunk with
+  | Mint8signed => true
+  | Mint8unsigned => true
+  | Mint16signed => true
+  | Mint16unsigned => true
+  | Mint32 => true
+  | Mfloat32 => false
+  | Mfloat64 => false
+  end.
+
+Definition can_use_Aindexed2shift (chunk: memory_chunk): bool :=
+  match chunk with
+  | Mint8signed => false
+  | Mint8unsigned => true
+  | Mint16signed => false
+  | Mint16unsigned => false
+  | Mint32 => true
+  | Mfloat32 => false
+  | Mfloat64 => false
+  end.
+
+Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
+  match e with
+  | Eop (Oaddrstack n) Enil => (Ainstack n, Enil)
+  | Eop (Oaddimm n) (e1:::Enil) => (Aindexed n, e1:::Enil)
+  | Eop (Oaddshift s) (e1:::e2:::Enil) =>
+      if can_use_Aindexed2shift chunk
+      then (Aindexed2shift s, e1:::e2:::Enil)
+      else (Aindexed Int.zero, Eop (Oaddshift s) (e1:::e2:::Enil) ::: Enil)
+  | Eop Oadd (e1:::e2:::Enil) =>
+      if can_use_Aindexed2 chunk
+      then (Aindexed2, e1:::e2:::Enil)
+      else (Aindexed Int.zero, Eop Oadd (e1:::e2:::Enil) ::: Enil)
+  | _ => (Aindexed Int.zero, e:::Enil)
+  end.
+
+