Module SelectOp


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 Compopts.
Require Import AST Integers Floats Builtins.
Require Import Op CminorSel.
Require Archi.

Local Open Scope cminorsel_scope.

Constants *


Definition addrsymbol (id: ident) (ofs: ptrofs) :=
  Eop (Oaddrsymbol id ofs) Enil.

Definition addrstack (ofs: ptrofs) :=
  Eop (Oaddrstack ofs) Enil.

Integer logical negation


Original definition: 
Nondetfunction notint (e: expr) :=
  match e with
  | Eop (Ointconst n) Enil => Eop (Ointconst (Int.not n)) Enil
  | Eop Onot (t1:::Enil) => t1
  | Eop Oand (t1:::t2:::Enil) => Eop Onand (t1:::t2:::Enil)
  | Eop Oor (t1:::t2:::Enil) => Eop Onor (t1:::t2:::Enil)
  | Eop Oxor (t1:::t2:::Enil) => Eop Onxor (t1:::t2:::Enil)
  | Eop Onand (t1:::t2:::Enil) => Eop Oand (t1:::t2:::Enil)
  | Eop Onor (t1:::t2:::Enil) => Eop Oor (t1:::t2:::Enil)
  | Eop Onxor (t1:::t2:::Enil) => Eop Oxor (t1:::t2:::Enil)
  | Eop Oandc (t1:::t2:::Enil) => Eop Oorc (t2:::t1:::Enil)
  | Eop Oorc (t1:::t2:::Enil) => Eop Oandc (t2:::t1:::Enil)
  | Eop (Oxorimm n) (t1:::Enil) => Eop (Oxorimm (Int.not n)) (t1:::Enil)
  | _ => Eop Onot (e:::Enil)
  end.

Inductive notint_cases: forall (e: expr), Type :=
  | notint_case1: forall n, notint_cases (Eop (Ointconst n) Enil)
  | notint_case2: forall t1, notint_cases (Eop Onot (t1:::Enil))
  | notint_case3: forall t1 t2, notint_cases (Eop Oand (t1:::t2:::Enil))
  | notint_case4: forall t1 t2, notint_cases (Eop Oor (t1:::t2:::Enil))
  | notint_case5: forall t1 t2, notint_cases (Eop Oxor (t1:::t2:::Enil))
  | notint_case6: forall t1 t2, notint_cases (Eop Onand (t1:::t2:::Enil))
  | notint_case7: forall t1 t2, notint_cases (Eop Onor (t1:::t2:::Enil))
  | notint_case8: forall t1 t2, notint_cases (Eop Onxor (t1:::t2:::Enil))
  | notint_case9: forall t1 t2, notint_cases (Eop Oandc (t1:::t2:::Enil))
  | notint_case10: forall t1 t2, notint_cases (Eop Oorc (t1:::t2:::Enil))
  | notint_case11: forall n t1, notint_cases (Eop (Oxorimm n) (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 (Ointconst n) Enil => notint_case1 n
  | Eop Onot (t1:::Enil) => notint_case2 t1
  | Eop Oand (t1:::t2:::Enil) => notint_case3 t1 t2
  | Eop Oor (t1:::t2:::Enil) => notint_case4 t1 t2
  | Eop Oxor (t1:::t2:::Enil) => notint_case5 t1 t2
  | Eop Onand (t1:::t2:::Enil) => notint_case6 t1 t2
  | Eop Onor (t1:::t2:::Enil) => notint_case7 t1 t2
  | Eop Onxor (t1:::t2:::Enil) => notint_case8 t1 t2
  | Eop Oandc (t1:::t2:::Enil) => notint_case9 t1 t2
  | Eop Oorc (t1:::t2:::Enil) => notint_case10 t1 t2
  | Eop (Oxorimm n) (t1:::Enil) => notint_case11 n t1
  | e => notint_default e
  end.

Definition notint (e: expr) :=
  match notint_match e with
  | notint_case1 n =>
      Eop (Ointconst (Int.not n)) Enil
  | notint_case2 t1 =>
      t1
  | notint_case3 t1 t2 =>
      Eop Onand (t1:::t2:::Enil)
  | notint_case4 t1 t2 =>
      Eop Onor (t1:::t2:::Enil)
  | notint_case5 t1 t2 =>
      Eop Onxor (t1:::t2:::Enil)
  | notint_case6 t1 t2 =>
      Eop Oand (t1:::t2:::Enil)
  | notint_case7 t1 t2 =>
      Eop Oor (t1:::t2:::Enil)
  | notint_case8 t1 t2 =>
      Eop Oxor (t1:::t2:::Enil)
  | notint_case9 t1 t2 =>
      Eop Oorc (t2:::t1:::Enil)
  | notint_case10 t1 t2 =>
      Eop Oandc (t2:::t1:::Enil)
  | notint_case11 n t1 =>
      Eop (Oxorimm (Int.not n)) (t1:::Enil)
  | notint_default e =>
      Eop Onot (e:::Enil)
  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 (Ptrofs.add (Ptrofs.of_int n) m)) Enil
  | Eop (Oaddrstack m) Enil      => Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n) m)) Enil
  | Eop (Oaddimm m) (t ::: Enil) => Eop (Oaddimm(Int.add n m)) (t ::: Enil)
  | Eop (Oaddsymbol s m) (t ::: Enil) => Eop (Oaddsymbol s (Ptrofs.add (Ptrofs.of_int 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_case5: forall s m t, addimm_cases (Eop (Oaddsymbol s 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
  | Eop (Oaddsymbol s m) (t ::: Enil) => addimm_case5 s 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(Int.add n m)) Enil
  | addimm_case2 s m =>
      Eop (Oaddrsymbol s (Ptrofs.add (Ptrofs.of_int n) m)) Enil
  | addimm_case3 m =>
      Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n) m)) Enil
  | addimm_case4 m t =>
      Eop (Oaddimm(Int.add n m)) (t ::: Enil)
  | addimm_case5 s m t =>
      Eop (Oaddsymbol s (Ptrofs.add (Ptrofs.of_int n) m)) (t ::: Enil)
  | addimm_default e =>
      Eop (Oaddimm n) (e ::: Enil)
  end.


Original definition: 
Nondetfunction addsymbol (s: ident) (ofs: ptrofs) (e: expr) :=
  match e with
  | Eop (Ointconst n) Enil => Eop (Oaddrsymbol s (Ptrofs.add ofs (Ptrofs.of_int n))) Enil
  | Eop (Oaddimm n) (t ::: Enil) => Eop (Oaddsymbol s (Ptrofs.add ofs (Ptrofs.of_int n))) (t ::: Enil)
  | _ => Eop (Oaddsymbol s ofs) (e ::: Enil)
  end.

Inductive addsymbol_cases: forall (e: expr), Type :=
  | addsymbol_case1: forall n, addsymbol_cases (Eop (Ointconst n) Enil)
  | addsymbol_case2: forall n t, addsymbol_cases (Eop (Oaddimm n) (t ::: Enil))
  | addsymbol_default: forall (e: expr), addsymbol_cases e.

Definition addsymbol_match (e: expr) :=
  match e as zz1 return addsymbol_cases zz1 with
  | Eop (Ointconst n) Enil => addsymbol_case1 n
  | Eop (Oaddimm n) (t ::: Enil) => addsymbol_case2 n t
  | e => addsymbol_default e
  end.

Definition addsymbol (s: ident) (ofs: ptrofs) (e: expr) :=
  match addsymbol_match e with
  | addsymbol_case1 n =>
      Eop (Oaddrsymbol s (Ptrofs.add ofs (Ptrofs.of_int n))) Enil
  | addsymbol_case2 n t =>
      Eop (Oaddsymbol s (Ptrofs.add ofs (Ptrofs.of_int n))) (t ::: Enil)
  | addsymbol_default e =>
      Eop (Oaddsymbol s ofs) (e ::: Enil)
  end.


Original definition: 
Nondetfunction add (e1: expr) (e2: expr) :=
  match e1, e2 with
  | Eop (Ointconst n1) Enil, t2 =>
      addimm n1 t2
  | t1, Eop (Ointconst n2) Enil =>
      addimm n2 t1
  | Eop (Oaddrsymbol s ofs) Enil, t2 =>
      addsymbol s ofs t2
  | t1, Eop (Oaddrsymbol s ofs) Enil =>
      addsymbol s ofs t1
  | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) =>
      addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil))
  | Eop (Oaddimm n1) (t1:::Enil), t2 =>
      addimm n1 (Eop Oadd (t1:::t2:::Enil))
  | Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) =>
      Eop Oadd (Eop (Oaddrstack (Ptrofs.add n1 (Ptrofs.of_int n2))) Enil ::: t2 ::: Enil)
  | Eop (Oaddsymbol s ofs) (t1:::Enil), Eop (Oaddimm n) (t2:::Enil) =>
      addsymbol s (Ptrofs.add ofs (Ptrofs.of_int n)) (Eop Oadd (t1:::t2:::Enil))
  | Eop (Oaddsymbol s ofs) (t1:::Enil), t2 =>
      addsymbol s ofs (Eop Oadd (t1:::t2:::Enil))
  | t1, Eop (Oaddimm n2) (t2:::Enil) =>
      addimm n2 (Eop Oadd (t1:::t2:::Enil))
  | t1, Eop (Oaddsymbol s ofs) (t2:::Enil) =>
      addsymbol s ofs (Eop Oadd (t1:::t2:::Enil))
  | _, _ =>
      Eop Oadd (e1:::e2:::Enil)
  end.

Inductive add_cases: forall (e1: expr) (e2: expr), Type :=
  | add_case1: forall n1 t2, add_cases (Eop (Ointconst n1) Enil) (t2)
  | add_case2: forall t1 n2, add_cases (t1) (Eop (Ointconst n2) Enil)
  | add_case3: forall s ofs t2, add_cases (Eop (Oaddrsymbol s ofs) Enil) (t2)
  | add_case4: forall t1 s ofs, add_cases (t1) (Eop (Oaddrsymbol s ofs) Enil)
  | add_case5: forall n1 t1 n2 t2, add_cases (Eop (Oaddimm n1) (t1:::Enil)) (Eop (Oaddimm n2) (t2:::Enil))
  | add_case6: forall n1 t1 t2, add_cases (Eop (Oaddimm n1) (t1:::Enil)) (t2)
  | add_case7: forall n1 n2 t2, add_cases (Eop (Oaddrstack n1) Enil) (Eop (Oaddimm n2) (t2:::Enil))
  | add_case8: forall s ofs t1 n t2, add_cases (Eop (Oaddsymbol s ofs) (t1:::Enil)) (Eop (Oaddimm n) (t2:::Enil))
  | add_case9: forall s ofs t1 t2, add_cases (Eop (Oaddsymbol s ofs) (t1:::Enil)) (t2)
  | add_case10: forall t1 n2 t2, add_cases (t1) (Eop (Oaddimm n2) (t2:::Enil))
  | add_case11: forall t1 s ofs t2, add_cases (t1) (Eop (Oaddsymbol s ofs) (t2:::Enil))
  | add_default: forall (e1: expr) (e2: expr), add_cases e1 e2.

Definition add_match (e1: expr) (e2: expr) :=
  match e1 as zz1, e2 as zz2 return add_cases zz1 zz2 with
  | Eop (Ointconst n1) Enil, t2 => add_case1 n1 t2
  | t1, Eop (Ointconst n2) Enil => add_case2 t1 n2
  | Eop (Oaddrsymbol s ofs) Enil, t2 => add_case3 s ofs t2
  | t1, Eop (Oaddrsymbol s ofs) Enil => add_case4 t1 s ofs
  | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => add_case5 n1 t1 n2 t2
  | Eop (Oaddimm n1) (t1:::Enil), t2 => add_case6 n1 t1 t2
  | Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) => add_case7 n1 n2 t2
  | Eop (Oaddsymbol s ofs) (t1:::Enil), Eop (Oaddimm n) (t2:::Enil) => add_case8 s ofs t1 n t2
  | Eop (Oaddsymbol s ofs) (t1:::Enil), t2 => add_case9 s ofs t1 t2
  | t1, Eop (Oaddimm n2) (t2:::Enil) => add_case10 t1 n2 t2
  | t1, Eop (Oaddsymbol s ofs) (t2:::Enil) => add_case11 t1 s ofs t2
  | e1, e2 => add_default e1 e2
  end.

Definition add (e1: expr) (e2: expr) :=
  match add_match e1 e2 with
  | add_case1 n1 t2 =>
      addimm n1 t2
  | add_case2 t1 n2 =>
      addimm n2 t1
  | add_case3 s ofs t2 =>
      addsymbol s ofs t2
  | add_case4 t1 s ofs =>
      addsymbol s ofs t1
  | add_case5 n1 t1 n2 t2 =>
      addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil))
  | add_case6 n1 t1 t2 =>
      addimm n1 (Eop Oadd (t1:::t2:::Enil))
  | add_case7 n1 n2 t2 =>
      Eop Oadd (Eop (Oaddrstack (Ptrofs.add n1 (Ptrofs.of_int n2))) Enil ::: t2 ::: Enil)
  | add_case8 s ofs t1 n t2 =>
      addsymbol s (Ptrofs.add ofs (Ptrofs.of_int n)) (Eop Oadd (t1:::t2:::Enil))
  | add_case9 s ofs t1 t2 =>
      addsymbol s ofs (Eop Oadd (t1:::t2:::Enil))
  | add_case10 t1 n2 t2 =>
      addimm n2 (Eop Oadd (t1:::t2:::Enil))
  | add_case11 t1 s ofs t2 =>
      addsymbol s ofs (Eop Oadd (t1:::t2:::Enil))
  | add_default e1 e2 =>
      Eop Oadd (e1:::e2:::Enil)
  end.


Integer and pointer subtraction


Original definition: 
Nondetfunction subimm (n1: int) (e: expr) :=
  match e with
  | Eop (Ointconst n2) Enil =>
      Eop (Ointconst (Int.sub n1 n2)) Enil
  | Eop (Oaddimm n2) (t2:::Enil) =>
      Eop (Osubimm (Int.sub n1 n2)) (t2 ::: Enil)
  | _ =>
      Eop (Osubimm n1) (e ::: Enil)
  end.

Inductive subimm_cases: forall (e: expr), Type :=
  | subimm_case1: forall n2, subimm_cases (Eop (Ointconst n2) Enil)
  | subimm_case2: forall n2 t2, subimm_cases (Eop (Oaddimm n2) (t2:::Enil))
  | subimm_default: forall (e: expr), subimm_cases e.

Definition subimm_match (e: expr) :=
  match e as zz1 return subimm_cases zz1 with
  | Eop (Ointconst n2) Enil => subimm_case1 n2
  | Eop (Oaddimm n2) (t2:::Enil) => subimm_case2 n2 t2
  | e => subimm_default e
  end.

Definition subimm (n1: int) (e: expr) :=
  match subimm_match e with
  | subimm_case1 n2 =>
      Eop (Ointconst (Int.sub n1 n2)) Enil
  | subimm_case2 n2 t2 =>
      Eop (Osubimm (Int.sub n1 n2)) (t2 ::: Enil)
  | subimm_default e =>
      Eop (Osubimm n1) (e ::: Enil)
  end.


Original definition: 
Nondetfunction sub (e1: expr) (e2: expr) :=
  match e1, e2 with
  | t1, Eop (Ointconst n2) Enil =>
      addimm (Int.neg n2) t1
  | Eop (Ointconst n1) Enil, t2 =>
      subimm n1 t2
  | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) =>
      addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil))
  | Eop (Oaddimm n1) (t1:::Enil), t2 =>
      addimm n1 (Eop Osub (t1:::t2:::Enil))
  | t1, Eop (Oaddimm n2) (t2:::Enil) =>
      addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil))
  | _, _ =>
      Eop Osub (e1:::e2:::Enil)
  end.

Inductive sub_cases: forall (e1: expr) (e2: expr), Type :=
  | sub_case1: forall t1 n2, sub_cases (t1) (Eop (Ointconst n2) Enil)
  | sub_case2: forall n1 t2, sub_cases (Eop (Ointconst n1) Enil) (t2)
  | sub_case3: forall n1 t1 n2 t2, sub_cases (Eop (Oaddimm n1) (t1:::Enil)) (Eop (Oaddimm n2) (t2:::Enil))
  | sub_case4: forall n1 t1 t2, sub_cases (Eop (Oaddimm n1) (t1:::Enil)) (t2)
  | sub_case5: forall t1 n2 t2, sub_cases (t1) (Eop (Oaddimm n2) (t2:::Enil))
  | sub_default: forall (e1: expr) (e2: expr), sub_cases e1 e2.

Definition sub_match (e1: expr) (e2: expr) :=
  match e1 as zz1, e2 as zz2 return sub_cases zz1 zz2 with
  | t1, Eop (Ointconst n2) Enil => sub_case1 t1 n2
  | Eop (Ointconst n1) Enil, t2 => sub_case2 n1 t2
  | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => sub_case3 n1 t1 n2 t2
  | Eop (Oaddimm n1) (t1:::Enil), t2 => sub_case4 n1 t1 t2
  | t1, Eop (Oaddimm n2) (t2:::Enil) => sub_case5 t1 n2 t2
  | e1, e2 => sub_default e1 e2
  end.

Definition sub (e1: expr) (e2: expr) :=
  match sub_match e1 e2 with
  | sub_case1 t1 n2 =>
      addimm (Int.neg n2) t1
  | sub_case2 n1 t2 =>
      subimm n1 t2
  | sub_case3 n1 t1 n2 t2 =>
      addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil))
  | sub_case4 n1 t1 t2 =>
      addimm n1 (Eop Osub (t1:::t2:::Enil))
  | sub_case5 t1 n2 t2 =>
      addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil))
  | sub_default e1 e2 =>
      Eop Osub (e1:::e2:::Enil)
  end.


Definition negint (e: expr) := subimm Int.zero e.

Rotates and immediate shifts


Original definition: 
Nondetfunction rolm (e1: expr) (amount2: int) (mask2: int) :=
  match e1 with
  | Eop (Ointconst n1) Enil =>
      Eop (Ointconst(Int.and (Int.rol n1 amount2) mask2)) Enil
  | Eop (Orolm amount1 mask1) (t1:::Enil) =>
      Eop (Orolm (Int.modu (Int.add amount1 amount2) Int.iwordsize)
                 (Int.and (Int.rol mask1 amount2) mask2))
          (t1:::Enil)
  | Eop (Oandimm mask1) (t1:::Enil) =>
      Eop (Orolm (Int.modu amount2 Int.iwordsize)
                 (Int.and (Int.rol mask1 amount2) mask2))
          (t1:::Enil)
  | _ =>
      Eop (Orolm amount2 mask2) (e1:::Enil)
  end.

Inductive rolm_cases: forall (e1: expr) , Type :=
  | rolm_case1: forall n1, rolm_cases (Eop (Ointconst n1) Enil)
  | rolm_case2: forall amount1 mask1 t1, rolm_cases (Eop (Orolm amount1 mask1) (t1:::Enil))
  | rolm_case3: forall mask1 t1, rolm_cases (Eop (Oandimm mask1) (t1:::Enil))
  | rolm_default: forall (e1: expr) , rolm_cases e1.

Definition rolm_match (e1: expr) :=
  match e1 as zz1 return rolm_cases zz1 with
  | Eop (Ointconst n1) Enil => rolm_case1 n1
  | Eop (Orolm amount1 mask1) (t1:::Enil) => rolm_case2 amount1 mask1 t1
  | Eop (Oandimm mask1) (t1:::Enil) => rolm_case3 mask1 t1
  | e1 => rolm_default e1
  end.

Definition rolm (e1: expr) (amount2: int) (mask2: int) :=
  match rolm_match e1 with
  | rolm_case1 n1 =>
      Eop (Ointconst(Int.and (Int.rol n1 amount2) mask2)) Enil
  | rolm_case2 amount1 mask1 t1 =>
      Eop (Orolm (Int.modu (Int.add amount1 amount2) Int.iwordsize) (Int.and (Int.rol mask1 amount2) mask2)) (t1:::Enil)
  | rolm_case3 mask1 t1 =>
      Eop (Orolm (Int.modu amount2 Int.iwordsize) (Int.and (Int.rol mask1 amount2) mask2)) (t1:::Enil)
  | rolm_default e1 =>
      Eop (Orolm amount2 mask2) (e1:::Enil)
  end.


Definition shlimm (e1: expr) (n2: int) :=
  if Int.eq n2 Int.zero then
    e1
  else if Int.ltu n2 Int.iwordsize then
    rolm e1 n2 (Int.shl Int.mone n2)
  else
    Eop Oshl (e1:::Eop (Ointconst n2) Enil:::Enil).

Definition shruimm (e1: expr) (n2: int) :=
  if Int.eq n2 Int.zero then
    e1
  else if Int.ltu n2 Int.iwordsize then
    rolm e1 (Int.sub Int.iwordsize n2) (Int.shru Int.mone n2)
  else
    Eop Oshru (e1:::Eop (Ointconst n2) Enil:::Enil).

Original definition: 
Nondetfunction shrimm (e1: expr) (n2: int) :=
  if Int.eq n2 Int.zero then
    e1
  else if negb (Int.ltu n2 Int.iwordsize) then
    Eop Oshr (e1:::Eop (Ointconst n2) Enil:::Enil)
  else
    match e1 with
    | Eop (Ointconst n1) Enil =>
        Eop (Ointconst (Int.shr n1 n2)) Enil
    | Eop (Oandimm mask1) (t1:::Enil) =>
        if Int.lt mask1 Int.zero
        then Eop (Oshrimm n2) (e1:::Enil)
        else shruimm e1 n2
    | _ =>
        Eop (Oshrimm n2) (e1:::Enil)
    end.

Inductive shrimm_cases: forall (e1: expr) , Type :=
  | shrimm_case1: forall n1, shrimm_cases (Eop (Ointconst n1) Enil)
  | shrimm_case2: forall mask1 t1, shrimm_cases (Eop (Oandimm mask1) (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 (Oandimm mask1) (t1:::Enil) => shrimm_case2 mask1 t1
  | e1 => shrimm_default e1
  end.

Definition shrimm (e1: expr) (n2: int) :=
 if Int.eq n2 Int.zero then e1 else if negb (Int.ltu n2 Int.iwordsize) then Eop Oshr (e1:::Eop (Ointconst n2) Enil:::Enil) else match shrimm_match e1 with
  | shrimm_case1 n1 =>
      Eop (Ointconst (Int.shr n1 n2)) Enil
  | shrimm_case2 mask1 t1 =>
      if Int.lt mask1 Int.zero then Eop (Oshrimm n2) (e1:::Enil) else shruimm e1 n2
  | shrimm_default e1 =>
      Eop (Oshrimm n2) (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 =>
      if optim_for_size tt then
        Eop (Omulimm n1) (e2:::Enil)
      else
        Elet e2
          (Eop Oadd (shlimm (Eletvar 0) i :::
                     shlimm (Eletvar 0) j ::: Enil))
  | _ =>
      Eop (Omulimm n1) (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(Int.mul n1 n2)) Enil
  | mulimm_case2 n2 t2 =>
      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 =>
      mulimm n1 t2
  | mul_case2 t1 n2 =>
      mulimm n2 t1
  | mul_default e1 e2 =>
      Eop Omul (e1:::e2:::Enil)
  end.


Definition mulhs (e1: expr) (e2: expr) := Eop Omulhs (e1 ::: e2 ::: Enil).
Definition mulhu (e1: expr) (e2: expr) := Eop Omulhu (e1 ::: e2 ::: Enil).

Bitwise and, or, xor


Original definition: 
Nondetfunction andimm (n1: int) (e2: expr) :=
  if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else
  if Int.eq n1 Int.mone then e2 else
  match e2 with
  | Eop (Ointconst n2) Enil =>
      Eop (Ointconst (Int.and n1 n2)) Enil
  | Eop (Oandimm n2) (Eop (Oshrimm amount) (t2:::Enil) ::: Enil) =>
      let n := Int.and n1 n2 in
      if Int.eq (Int.shru (Int.shl n amount) amount) n
      && Int.ltu amount Int.iwordsize
      then rolm t2 (Int.sub Int.iwordsize amount)
                   (Int.and (Int.shru Int.mone amount) n)
      else Eop (Oandimm n) (Eop (Oshrimm amount) (t2:::Enil) ::: Enil)
  | Eop (Oandimm n2) (t2:::Enil) =>
      Eop (Oandimm (Int.and n1 n2)) (t2:::Enil)
  | Eop (Orolm amount2 mask2) (t2:::Enil) =>
      Eop (Orolm amount2 (Int.and n1 mask2)) (t2:::Enil)
  | Eop (Oshrimm amount) (t2:::Enil) =>
      if Int.eq (Int.shru (Int.shl n1 amount) amount) n1
      && Int.ltu amount Int.iwordsize
      then rolm t2 (Int.sub Int.iwordsize amount)
                   (Int.and (Int.shru Int.mone amount) n1)
      else Eop (Oandimm n1) (e2:::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 amount t2, andimm_cases (Eop (Oandimm n2) (Eop (Oshrimm amount) (t2:::Enil) ::: Enil))
  | andimm_case3: forall n2 t2, andimm_cases (Eop (Oandimm n2) (t2:::Enil))
  | andimm_case4: forall amount2 mask2 t2, andimm_cases (Eop (Orolm amount2 mask2) (t2:::Enil))
  | andimm_case5: forall amount t2, andimm_cases (Eop (Oshrimm amount) (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) (Eop (Oshrimm amount) (t2:::Enil) ::: Enil) => andimm_case2 n2 amount t2
  | Eop (Oandimm n2) (t2:::Enil) => andimm_case3 n2 t2
  | Eop (Orolm amount2 mask2) (t2:::Enil) => andimm_case4 amount2 mask2 t2
  | Eop (Oshrimm amount) (t2:::Enil) => andimm_case5 amount t2
  | e2 => andimm_default e2
  end.

Definition andimm (n1: int) (e2: expr) :=
 if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else if Int.eq n1 Int.mone then e2 else match andimm_match e2 with
  | andimm_case1 n2 =>
      Eop (Ointconst (Int.and n1 n2)) Enil
  | andimm_case2 n2 amount t2 =>
      let n := Int.and n1 n2 in if Int.eq (Int.shru (Int.shl n amount) amount) n && Int.ltu amount Int.iwordsize then rolm t2 (Int.sub Int.iwordsize amount) (Int.and (Int.shru Int.mone amount) n) else Eop (Oandimm n) (Eop (Oshrimm amount) (t2:::Enil) ::: Enil)
  | andimm_case3 n2 t2 =>
      Eop (Oandimm (Int.and n1 n2)) (t2:::Enil)
  | andimm_case4 amount2 mask2 t2 =>
      Eop (Orolm amount2 (Int.and n1 mask2)) (t2:::Enil)
  | andimm_case5 amount t2 =>
      if Int.eq (Int.shru (Int.shl n1 amount) amount) n1 && Int.ltu amount Int.iwordsize then rolm t2 (Int.sub Int.iwordsize amount) (Int.and (Int.shru Int.mone amount) n1) else Eop (Oandimm n1) (e2:::Enil)
  | andimm_default e2 =>
      Eop (Oandimm n1) (e2:::Enil)
  end.


Original definition: 
Nondetfunction and (e1: expr) (e2: expr) :=
  match e1, e2 with
  | Eop (Ointconst n1) Enil, t2 => andimm n1 t2
  | t1, Eop (Ointconst n2) Enil => andimm n2 t1
  | Eop Onot (t1:::Enil), t2 => Eop Oandc (t2:::t1:::Enil)
  | t1, Eop Onot (t2:::Enil) => Eop Oandc (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 t1 t2, and_cases (Eop Onot (t1:::Enil)) (t2)
  | and_case4: forall t1 t2, and_cases (t1) (Eop Onot (t2:::Enil))
  | and_default: forall (e1: expr) (e2: expr), and_cases e1 e2.

Definition and_match (e1: expr) (e2: expr) :=
  match e1 as zz1, e2 as zz2 return and_cases zz1 zz2 with
  | Eop (Ointconst n1) Enil, t2 => and_case1 n1 t2
  | t1, Eop (Ointconst n2) Enil => and_case2 t1 n2
  | Eop Onot (t1:::Enil), t2 => and_case3 t1 t2
  | t1, Eop Onot (t2:::Enil) => and_case4 t1 t2
  | e1, e2 => and_default e1 e2
  end.

Definition and (e1: expr) (e2: expr) :=
  match and_match e1 e2 with
  | and_case1 n1 t2 =>
      andimm n1 t2
  | and_case2 t1 n2 =>
      andimm n2 t1
  | and_case3 t1 t2 =>
      Eop Oandc (t2:::t1:::Enil)
  | and_case4 t1 t2 =>
      Eop Oandc (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
  if Int.eq n1 Int.mone then Eop (Ointconst Int.mone) Enil else
  match e2 with
  | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.or n1 n2)) Enil
  | Eop (Oorimm n2) (t2:::Enil) => Eop (Oorimm (Int.or n1 n2)) (t2:::Enil)
  | _ => Eop (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 if Int.eq n1 Int.mone then Eop (Ointconst Int.mone) Enil else match orimm_match e2 with
  | orimm_case1 n2 =>
      Eop (Ointconst (Int.or n1 n2)) Enil
  | orimm_case2 n2 t2 =>
      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 (Orolm amount1  mask1) (t1:::Enil), Eop (Orolm amount2 mask2) (t2:::Enil) =>
      if Int.eq amount1 amount2 && same_expr_pure t1 t2
      then Eop (Orolm amount1 (Int.or mask1 mask2)) (t1:::Enil)
      else Eop Oor (e1:::e2:::Enil)
  | Eop (Oandimm mask1) (t1:::Enil), Eop (Orolm amount2 mask2) (t2:::Enil) =>
      if Int.eq mask1 (Int.not mask2) && is_rlw_mask mask2
      then Eop (Oroli amount2 mask2) (t1:::t2:::Enil)
      else Eop Oor (e1:::e2:::Enil)
  | Eop (Orolm amount1 mask1) (t1:::Enil), Eop (Oandimm mask2) (t2:::Enil) =>
      if Int.eq mask2 (Int.not mask1) && is_rlw_mask mask1
      then Eop (Oroli amount1 mask1) (t2:::t1:::Enil)
      else Eop Oor (e1:::e2:::Enil)
  | Eop (Ointconst n1) Enil, t2 => orimm n1 t2
  | t1, Eop (Ointconst n2) Enil => orimm n2 t1
  | Eop Onot (t1:::Enil), t2 => Eop Oorc (t2:::t1:::Enil)
  | t1, Eop Onot (t2:::Enil) => Eop Oorc (t1:::t2:::Enil)
  | _, _ => Eop Oor (e1:::e2:::Enil)
  end.

Inductive or_cases: forall (e1: expr) (e2: expr), Type :=
  | or_case1: forall amount1 mask1 t1 amount2 mask2 t2, or_cases (Eop (Orolm amount1 mask1) (t1:::Enil)) (Eop (Orolm amount2 mask2) (t2:::Enil))
  | or_case2: forall mask1 t1 amount2 mask2 t2, or_cases (Eop (Oandimm mask1) (t1:::Enil)) (Eop (Orolm amount2 mask2) (t2:::Enil))
  | or_case3: forall amount1 mask1 t1 mask2 t2, or_cases (Eop (Orolm amount1 mask1) (t1:::Enil)) (Eop (Oandimm mask2) (t2:::Enil))
  | or_case4: forall n1 t2, or_cases (Eop (Ointconst n1) Enil) (t2)
  | or_case5: forall t1 n2, or_cases (t1) (Eop (Ointconst n2) Enil)
  | or_case6: forall t1 t2, or_cases (Eop Onot (t1:::Enil)) (t2)
  | or_case7: forall t1 t2, or_cases (t1) (Eop Onot (t2:::Enil))
  | or_default: forall (e1: expr) (e2: expr), or_cases e1 e2.

Definition or_match (e1: expr) (e2: expr) :=
  match e1 as zz1, e2 as zz2 return or_cases zz1 zz2 with
  | Eop (Orolm amount1 mask1) (t1:::Enil), Eop (Orolm amount2 mask2) (t2:::Enil) => or_case1 amount1 mask1 t1 amount2 mask2 t2
  | Eop (Oandimm mask1) (t1:::Enil), Eop (Orolm amount2 mask2) (t2:::Enil) => or_case2 mask1 t1 amount2 mask2 t2
  | Eop (Orolm amount1 mask1) (t1:::Enil), Eop (Oandimm mask2) (t2:::Enil) => or_case3 amount1 mask1 t1 mask2 t2
  | Eop (Ointconst n1) Enil, t2 => or_case4 n1 t2
  | t1, Eop (Ointconst n2) Enil => or_case5 t1 n2
  | Eop Onot (t1:::Enil), t2 => or_case6 t1 t2
  | t1, Eop Onot (t2:::Enil) => or_case7 t1 t2
  | e1, e2 => or_default e1 e2
  end.

Definition or (e1: expr) (e2: expr) :=
  match or_match e1 e2 with
  | or_case1 amount1 mask1 t1 amount2 mask2 t2 =>
      if Int.eq amount1 amount2 && same_expr_pure t1 t2 then Eop (Orolm amount1 (Int.or mask1 mask2)) (t1:::Enil) else Eop Oor (e1:::e2:::Enil)
  | or_case2 mask1 t1 amount2 mask2 t2 =>
      if Int.eq mask1 (Int.not mask2) && is_rlw_mask mask2 then Eop (Oroli amount2 mask2) (t1:::t2:::Enil) else Eop Oor (e1:::e2:::Enil)
  | or_case3 amount1 mask1 t1 mask2 t2 =>
      if Int.eq mask2 (Int.not mask1) && is_rlw_mask mask1 then Eop (Oroli amount1 mask1) (t2:::t1:::Enil) else Eop Oor (e1:::e2:::Enil)
  | or_case4 n1 t2 =>
      orimm n1 t2
  | or_case5 t1 n2 =>
      orimm n2 t1
  | or_case6 t1 t2 =>
      Eop Oorc (t2:::t1:::Enil)
  | or_case7 t1 t2 =>
      Eop Oorc (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
  if Int.eq n1 Int.mone then notint 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 Onot (t2:::Enil) => Eop (Oxorimm (Int.not n1)) (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_case3: forall t2, xorimm_cases (Eop Onot (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
  | Eop Onot (t2:::Enil) => xorimm_case3 t2
  | e2 => xorimm_default e2
  end.

Definition xorimm (n1: int) (e2: expr) :=
 if Int.eq n1 Int.zero then e2 else if Int.eq n1 Int.mone then notint e2 else match xorimm_match e2 with
  | xorimm_case1 n2 =>
      Eop (Ointconst (Int.xor n1 n2)) Enil
  | xorimm_case2 n2 t2 =>
      Eop (Oxorimm (Int.xor n1 n2)) (t2:::Enil)
  | xorimm_case3 t2 =>
      Eop (Oxorimm (Int.not n1)) (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 Onot (t1:::Enil), t2 => Eop Onxor (t1:::t2:::Enil)
  | t1, Eop Onot (t2:::Enil) => Eop Onxor (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 t1 t2, xor_cases (Eop Onot (t1:::Enil)) (t2)
  | xor_case4: forall t1 t2, xor_cases (t1) (Eop Onot (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 Onot (t1:::Enil), t2 => xor_case3 t1 t2
  | t1, Eop Onot (t2:::Enil) => xor_case4 t1 t2
  | e1, e2 => xor_default e1 e2
  end.

Definition xor (e1: expr) (e2: expr) :=
  match xor_match e1 e2 with
  | xor_case1 n1 t2 =>
      xorimm n1 t2
  | xor_case2 t1 n2 =>
      xorimm n2 t1
  | xor_case3 t1 t2 =>
      Eop Onxor (t1:::t2:::Enil)
  | xor_case4 t1 t2 =>
      Eop Onxor (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_base (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
Definition mods_base := mod_aux Odiv.
Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil).
Definition modu_base := mod_aux Odivu.

Definition shrximm (e1: expr) (n2: int) :=
  if Int.eq n2 Int.zero then e1 else Eop (Oshrximm n2) (e1:::Enil).

General shifts


Original definition: 
Nondetfunction shl (e1: expr) (e2: expr) :=
  match e2 with
  | Eop (Ointconst n2) Enil => shlimm e1 n2
  | _ => Eop Oshl (e1:::e2:::Enil)
  end.

Inductive shl_cases: forall (e2: expr), Type :=
  | shl_case1: forall n2, shl_cases (Eop (Ointconst n2) Enil)
  | shl_default: forall (e2: expr), shl_cases e2.

Definition shl_match (e2: expr) :=
  match e2 as zz1 return shl_cases zz1 with
  | Eop (Ointconst n2) Enil => shl_case1 n2
  | e2 => shl_default e2
  end.

Definition shl (e1: expr) (e2: expr) :=
  match shl_match e2 with
  | shl_case1 n2 =>
      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 =>
      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 =>
      shruimm e1 n2
  | shru_default e2 =>
      Eop Oshru (e1:::e2:::Enil)
  end.


Floating-point arithmetic


Definition negf (e: expr) := Eop Onegf (e ::: Enil).
Definition absf (e: expr) := Eop Oabsf (e ::: Enil).
Definition addf (e1 e2: expr) := Eop Oaddf (e1 ::: e2 ::: Enil).
Definition subf (e1 e2: expr) := Eop Osubf (e1 ::: e2 ::: Enil).
Definition mulf (e1 e2: expr) := Eop Omulf (e1 ::: e2 ::: Enil).

Definition negfs (e: expr) := Eop Onegfs (e ::: Enil).
Definition absfs (e: expr) := Eop Oabsfs (e ::: Enil).
Definition addfs (e1 e2: expr) := Eop Oaddfs (e1 ::: e2 ::: Enil).
Definition subfs (e1 e2: expr) := Eop Osubfs (e1 ::: e2 ::: Enil).
Definition mulfs (e1 e2: expr) := Eop Omulfs (e1 ::: e2 ::: Enil).

Comparisons


Original definition: 
Nondetfunction compimm (default: comparison -> int -> condition)
                       (sem: comparison -> int -> int -> bool)
                       (c: comparison) (e1: expr) (n2: int) :=
  match c, e1 with
  | c, Eop (Ointconst n1) Enil =>
      Eop (Ointconst (if sem c n1 n2 then Int.one else Int.zero)) Enil
  | Ceq, Eop (Ocmp c) el =>
      if Int.eq_dec n2 Int.zero then
        Eop (Ocmp (negate_condition c)) el
      else if Int.eq_dec n2 Int.one then
        Eop (Ocmp c) el
      else
        Eop (Ointconst Int.zero) Enil
  | Cne, Eop (Ocmp c) el =>
      if Int.eq_dec n2 Int.zero then
        Eop (Ocmp c) el
      else if Int.eq_dec n2 Int.one then
        Eop (Ocmp (negate_condition c)) el
      else
        Eop (Ointconst Int.one) Enil
  | Ceq, Eop (Oandimm n1) (t1 ::: Enil) =>
      if Int.eq_dec n2 Int.zero then
        Eop (Ocmp (Cmaskzero n1)) (t1 ::: Enil)
      else
        Eop (Ocmp (default c n2)) (e1 ::: Enil)
  | Cne, Eop (Oandimm n1) (t1 ::: Enil) =>
      if Int.eq_dec n2 Int.zero then
        Eop (Ocmp (Cmasknotzero n1)) (t1 ::: Enil)
      else
        Eop (Ocmp (default c n2)) (e1 ::: Enil)
  | _, _ =>
       Eop (Ocmp (default c n2)) (e1 ::: Enil)
  end.

Inductive compimm_cases: forall (c: comparison) (e1: expr) , Type :=
  | compimm_case1: forall c n1, compimm_cases (c) (Eop (Ointconst n1) Enil)
  | compimm_case2: forall c el, compimm_cases (Ceq) (Eop (Ocmp c) el)
  | compimm_case3: forall c el, compimm_cases (Cne) (Eop (Ocmp c) el)
  | compimm_case4: forall n1 t1, compimm_cases (Ceq) (Eop (Oandimm n1) (t1 ::: Enil))
  | compimm_case5: forall n1 t1, compimm_cases (Cne) (Eop (Oandimm n1) (t1 ::: Enil))
  | compimm_default: forall (c: comparison) (e1: expr) , compimm_cases c e1.

Definition compimm_match (c: comparison) (e1: expr) :=
  match c as zz1, e1 as zz2 return compimm_cases zz1 zz2 with
  | c, Eop (Ointconst n1) Enil => compimm_case1 c n1
  | Ceq, Eop (Ocmp c) el => compimm_case2 c el
  | Cne, Eop (Ocmp c) el => compimm_case3 c el
  | Ceq, Eop (Oandimm n1) (t1 ::: Enil) => compimm_case4 n1 t1
  | Cne, Eop (Oandimm n1) (t1 ::: Enil) => compimm_case5 n1 t1
  | c, e1 => compimm_default c e1
  end.

Definition compimm (default: comparison -> int -> condition) (sem: comparison -> int -> int -> bool) (c: comparison) (e1: expr) (n2: int) :=
  match compimm_match c e1 with
  | compimm_case1 c n1 =>
      Eop (Ointconst (if sem c n1 n2 then Int.one else Int.zero)) Enil
  | compimm_case2 c el =>
      if Int.eq_dec n2 Int.zero then Eop (Ocmp (negate_condition c)) el else if Int.eq_dec n2 Int.one then Eop (Ocmp c) el else Eop (Ointconst Int.zero) Enil
  | compimm_case3 c el =>
      if Int.eq_dec n2 Int.zero then Eop (Ocmp c) el else if Int.eq_dec n2 Int.one then Eop (Ocmp (negate_condition c)) el else Eop (Ointconst Int.one) Enil
  | compimm_case4 n1 t1 =>
      if Int.eq_dec n2 Int.zero then Eop (Ocmp (Cmaskzero n1)) (t1 ::: Enil) else Eop (Ocmp (default c n2)) (e1 ::: Enil)
  | compimm_case5 n1 t1 =>
      if Int.eq_dec n2 Int.zero then Eop (Ocmp (Cmasknotzero n1)) (t1 ::: Enil) else Eop (Ocmp (default c n2)) (e1 ::: Enil)
  | compimm_default c e1 =>
      Eop (Ocmp (default c n2)) (e1 ::: Enil)
  end.


Original definition: 
Nondetfunction comp (c: comparison) (e1: expr) (e2: expr) :=
  match e1, e2 with
  | Eop (Ointconst n1) Enil, t2 =>
      compimm Ccompimm Int.cmp (swap_comparison c) t2 n1
  | t1, Eop (Ointconst n2) Enil =>
      compimm Ccompimm Int.cmp c t1 n2
  | _, _ =>
      Eop (Ocmp (Ccomp c)) (e1 ::: e2 ::: Enil)
  end.

Inductive comp_cases: forall (e1: expr) (e2: expr), Type :=
  | comp_case1: forall n1 t2, comp_cases (Eop (Ointconst n1) Enil) (t2)
  | comp_case2: forall t1 n2, comp_cases (t1) (Eop (Ointconst n2) Enil)
  | comp_default: forall (e1: expr) (e2: expr), comp_cases e1 e2.

Definition comp_match (e1: expr) (e2: expr) :=
  match e1 as zz1, e2 as zz2 return comp_cases zz1 zz2 with
  | Eop (Ointconst n1) Enil, t2 => comp_case1 n1 t2
  | t1, Eop (Ointconst n2) Enil => comp_case2 t1 n2
  | e1, e2 => comp_default e1 e2
  end.

Definition comp (c: comparison) (e1: expr) (e2: expr) :=
  match comp_match e1 e2 with
  | comp_case1 n1 t2 =>
      compimm Ccompimm Int.cmp (swap_comparison c) t2 n1
  | comp_case2 t1 n2 =>
      compimm Ccompimm Int.cmp c t1 n2
  | comp_default e1 e2 =>
      Eop (Ocmp (Ccomp c)) (e1 ::: e2 ::: Enil)
  end.


Original definition: 
Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) :=
  match e1, e2 with
  | Eop (Ointconst n1) Enil, t2 =>
      compimm Ccompuimm Int.cmpu (swap_comparison c) t2 n1
  | t1, Eop (Ointconst n2) Enil =>
      compimm Ccompuimm Int.cmpu c t1 n2
  | _, _ =>
      Eop (Ocmp (Ccompu c)) (e1 ::: e2 ::: Enil)
  end.

Inductive compu_cases: forall (e1: expr) (e2: expr), Type :=
  | compu_case1: forall n1 t2, compu_cases (Eop (Ointconst n1) Enil) (t2)
  | compu_case2: forall t1 n2, compu_cases (t1) (Eop (Ointconst n2) Enil)
  | compu_default: forall (e1: expr) (e2: expr), compu_cases e1 e2.

Definition compu_match (e1: expr) (e2: expr) :=
  match e1 as zz1, e2 as zz2 return compu_cases zz1 zz2 with
  | Eop (Ointconst n1) Enil, t2 => compu_case1 n1 t2
  | t1, Eop (Ointconst n2) Enil => compu_case2 t1 n2
  | e1, e2 => compu_default e1 e2
  end.

Definition compu (c: comparison) (e1: expr) (e2: expr) :=
  match compu_match e1 e2 with
  | compu_case1 n1 t2 =>
      compimm Ccompuimm Int.cmpu (swap_comparison c) t2 n1
  | compu_case2 t1 n2 =>
      compimm Ccompuimm Int.cmpu c t1 n2
  | compu_default e1 e2 =>
      Eop (Ocmp (Ccompu c)) (e1 ::: e2 ::: Enil)
  end.


Definition compf (c: comparison) (e1: expr) (e2: expr) :=
  Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil).

Definition compfs (c: comparison) (e1: expr) (e2: expr) :=
  Eop (Ocmp (Ccompf c)) (Eop Ofloatofsingle (e1 ::: Enil) :::
                         Eop Ofloatofsingle (e2 ::: Enil) ::: Enil).

Integer conversions


Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e.

Original definition: 
Nondetfunction cast8signed (e: expr) :=
  match e with
  | Eop (Ointconst n) Enil => Eop (Ointconst (Int.sign_ext 8 n)) Enil
  | _ => Eop Ocast8signed (e ::: Enil)
  end.

Inductive cast8signed_cases: forall (e: expr), Type :=
  | cast8signed_case1: forall n, cast8signed_cases (Eop (Ointconst n) Enil)
  | cast8signed_default: forall (e: expr), cast8signed_cases e.

Definition cast8signed_match (e: expr) :=
  match e as zz1 return cast8signed_cases zz1 with
  | Eop (Ointconst n) Enil => cast8signed_case1 n
  | e => cast8signed_default e
  end.

Definition cast8signed (e: expr) :=
  match cast8signed_match e with
  | cast8signed_case1 n =>
      Eop (Ointconst (Int.sign_ext 8 n)) Enil
  | cast8signed_default e =>
      Eop Ocast8signed (e ::: Enil)
  end.


Definition cast16unsigned (e: expr) := andimm (Int.repr 65535) e.

Original definition: 
Nondetfunction cast16signed (e: expr) :=
  match e with
  | Eop (Ointconst n) Enil => Eop (Ointconst (Int.sign_ext 16 n)) Enil
  | _ => Eop Ocast16signed (e ::: Enil)
  end.

Inductive cast16signed_cases: forall (e: expr), Type :=
  | cast16signed_case1: forall n, cast16signed_cases (Eop (Ointconst n) Enil)
  | cast16signed_default: forall (e: expr), cast16signed_cases e.

Definition cast16signed_match (e: expr) :=
  match e as zz1 return cast16signed_cases zz1 with
  | Eop (Ointconst n) Enil => cast16signed_case1 n
  | e => cast16signed_default e
  end.

Definition cast16signed (e: expr) :=
  match cast16signed_match e with
  | cast16signed_case1 n =>
      Eop (Ointconst (Int.sign_ext 16 n)) Enil
  | cast16signed_default e =>
      Eop Ocast16signed (e ::: Enil)
  end.


Floating-point conversions


Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil).

Definition intuoffloat (e: expr) :=
  if Archi.ppc64 then
    Eop Olowlong (Eop Olongoffloat (e ::: Enil) ::: Enil)
  else
    Elet e
    (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil)
      (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil))
        (intoffloat (Eletvar 1))
        (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat.

Original definition: 
Nondetfunction floatofintu (e: expr) :=
  match e with
  | Eop (Ointconst n) Enil =>
      Eop (Ofloatconst (Float.of_intu n)) Enil
  | _ =>
      if Archi.ppc64 then
        Eop Ofloatoflong (Eop Ocast32unsigned (e ::: Enil) ::: Enil)
      else
        subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil))
             (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil)
  end.

Inductive floatofintu_cases: forall (e: expr), Type :=
  | floatofintu_case1: forall n, floatofintu_cases (Eop (Ointconst n) Enil)
  | floatofintu_default: forall (e: expr), floatofintu_cases e.

Definition floatofintu_match (e: expr) :=
  match e as zz1 return floatofintu_cases zz1 with
  | Eop (Ointconst n) Enil => floatofintu_case1 n
  | e => floatofintu_default e
  end.

Definition floatofintu (e: expr) :=
  match floatofintu_match e with
  | floatofintu_case1 n =>
      Eop (Ofloatconst (Float.of_intu n)) Enil
  | floatofintu_default e =>
      if Archi.ppc64 then Eop Ofloatoflong (Eop Ocast32unsigned (e ::: Enil) ::: Enil) else subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil)) (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil)
  end.


Original definition: 
Nondetfunction floatofint (e: expr) :=
  match e with
  | Eop (Ointconst n) Enil =>
      Eop (Ofloatconst (Float.of_int n)) Enil
  | _ =>
      if Archi.ppc64 then
        Eop Ofloatoflong (Eop Ocast32signed (e ::: Enil) ::: Enil)
      else
        subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil
                                 ::: addimm Float.ox8000_0000 e ::: Enil))
             (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil)
  end.

Inductive floatofint_cases: forall (e: expr), Type :=
  | floatofint_case1: forall n, floatofint_cases (Eop (Ointconst n) Enil)
  | floatofint_default: forall (e: expr), floatofint_cases e.

Definition floatofint_match (e: expr) :=
  match e as zz1 return floatofint_cases zz1 with
  | Eop (Ointconst n) Enil => floatofint_case1 n
  | e => floatofint_default e
  end.

Definition floatofint (e: expr) :=
  match floatofint_match e with
  | floatofint_case1 n =>
      Eop (Ofloatconst (Float.of_int n)) Enil
  | floatofint_default e =>
      if Archi.ppc64 then Eop Ofloatoflong (Eop Ocast32signed (e ::: Enil) ::: Enil) else subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: addimm Float.ox8000_0000 e ::: Enil)) (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil)
  end.


Definition intofsingle (e: expr) :=
  intoffloat (Eop Ofloatofsingle (e ::: Enil)).

Definition singleofint (e: expr) :=
  Eop Osingleoffloat (floatofint e ::: Enil).

Definition intuofsingle (e: expr) :=
  intuoffloat (Eop Ofloatofsingle (e ::: Enil)).

Definition singleofintu (e: expr) :=
  Eop Osingleoffloat (floatofintu e ::: Enil).

Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil).
Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil).

Selection


Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr) :=
  if match ty with
     | Tint => true
     | Tfloat => true
     | Tsingle => true
     | Tlong => Archi.ppc64
     | _ => false
     end
  then Some (Eop (Osel cond ty) (e1 ::: e2 ::: args))
  else None.

Recognition of addressing modes for load and store operations


Definition can_use_Aindexed2 (chunk: memory_chunk): bool :=
  match chunk with Mint64 => Archi.ppc64 | _ => true end.

Original definition: 
Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
  match e with
  | Eop (Oaddrsymbol s n) Enil => (Aglobal s n, Enil)
  | Eop (Oaddrstack n) Enil => (Ainstack n, Enil)
  | Eop (Oaddsymbol s n) (e1:::Enil) => (Abased s n, e1:::Enil)
  | Eop (Oaddimm n) (e1:::Enil) => (Aindexed n, e1:::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 s n, addressing_cases (Eop (Oaddrsymbol s n) Enil)
  | addressing_case2: forall n, addressing_cases (Eop (Oaddrstack n) Enil)
  | addressing_case3: forall s n e1, addressing_cases (Eop (Oaddsymbol s n) (e1:::Enil))
  | addressing_case4: forall n e1, addressing_cases (Eop (Oaddimm n) (e1:::Enil))
  | addressing_case5: 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 (Oaddrsymbol s n) Enil => addressing_case1 s n
  | Eop (Oaddrstack n) Enil => addressing_case2 n
  | Eop (Oaddsymbol s n) (e1:::Enil) => addressing_case3 s n e1
  | Eop (Oaddimm n) (e1:::Enil) => addressing_case4 n e1
  | Eop Oadd (e1:::e2:::Enil) => addressing_case5 e1 e2
  | e => addressing_default e
  end.

Definition addressing (chunk: memory_chunk) (e: expr) :=
  match addressing_match e with
  | addressing_case1 s n =>
      (Aglobal s n, Enil)
  | addressing_case2 n =>
      (Ainstack n, Enil)
  | addressing_case3 s n e1 =>
      (Abased s n, e1:::Enil)
  | addressing_case4 n e1 =>
      (Aindexed n, e1:::Enil)
  | addressing_case5 e1 e2 =>
      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.


Arguments of builtins


Original definition: 
Nondetfunction builtin_arg (e: expr) :=
  match e with
  | Eop (Ointconst n) Enil => BA_int n
  | Eop (Oaddrsymbol id ofs) Enil => BA_addrglobal id ofs
  | Eop (Oaddrstack ofs) Enil => BA_addrstack ofs
  | Eop (Olongconst n) Enil => BA_long n
  | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) =>
        BA_long (Int64.ofwords h l)
  | Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l)
  | Eload chunk (Aglobal id ofs) Enil => BA_loadglobal chunk id ofs
  | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs
  | Eop (Oaddimm n) (e1:::Enil) => BA_addptr (BA e1) (BA_int n)
  | Eop (Oaddsymbol id ofs) (e1:::Enil) => BA_addptr (BA_addrglobal id ofs) (BA e1)
  | Eop Oadd (e1:::e2:::Enil) => BA_addptr (BA e1) (BA e2)
  | _ => BA e
  end.

Inductive builtin_arg_cases: forall (e: expr), Type :=
  | builtin_arg_case1: forall n, builtin_arg_cases (Eop (Ointconst n) Enil)
  | builtin_arg_case2: forall id ofs, builtin_arg_cases (Eop (Oaddrsymbol id ofs) Enil)
  | builtin_arg_case3: forall ofs, builtin_arg_cases (Eop (Oaddrstack ofs) Enil)
  | builtin_arg_case4: forall n, builtin_arg_cases (Eop (Olongconst n) Enil)
  | builtin_arg_case5: forall h l, builtin_arg_cases (Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil))
  | builtin_arg_case6: forall h l, builtin_arg_cases (Eop Omakelong (h ::: l ::: Enil))
  | builtin_arg_case7: forall chunk id ofs, builtin_arg_cases (Eload chunk (Aglobal id ofs) Enil)
  | builtin_arg_case8: forall chunk ofs, builtin_arg_cases (Eload chunk (Ainstack ofs) Enil)
  | builtin_arg_case9: forall n e1, builtin_arg_cases (Eop (Oaddimm n) (e1:::Enil))
  | builtin_arg_case10: forall id ofs e1, builtin_arg_cases (Eop (Oaddsymbol id ofs) (e1:::Enil))
  | builtin_arg_case11: forall e1 e2, builtin_arg_cases (Eop Oadd (e1:::e2:::Enil))
  | builtin_arg_default: forall (e: expr), builtin_arg_cases e.

Definition builtin_arg_match (e: expr) :=
  match e as zz1 return builtin_arg_cases zz1 with
  | Eop (Ointconst n) Enil => builtin_arg_case1 n
  | Eop (Oaddrsymbol id ofs) Enil => builtin_arg_case2 id ofs
  | Eop (Oaddrstack ofs) Enil => builtin_arg_case3 ofs
  | Eop (Olongconst n) Enil => builtin_arg_case4 n
  | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => builtin_arg_case5 h l
  | Eop Omakelong (h ::: l ::: Enil) => builtin_arg_case6 h l
  | Eload chunk (Aglobal id ofs) Enil => builtin_arg_case7 chunk id ofs
  | Eload chunk (Ainstack ofs) Enil => builtin_arg_case8 chunk ofs
  | Eop (Oaddimm n) (e1:::Enil) => builtin_arg_case9 n e1
  | Eop (Oaddsymbol id ofs) (e1:::Enil) => builtin_arg_case10 id ofs e1
  | Eop Oadd (e1:::e2:::Enil) => builtin_arg_case11 e1 e2
  | e => builtin_arg_default e
  end.

Definition builtin_arg (e: expr) :=
  match builtin_arg_match e with
  | builtin_arg_case1 n =>
      BA_int n
  | builtin_arg_case2 id ofs =>
      BA_addrglobal id ofs
  | builtin_arg_case3 ofs =>
      BA_addrstack ofs
  | builtin_arg_case4 n =>
      BA_long n
  | builtin_arg_case5 h l =>
      BA_long (Int64.ofwords h l)
  | builtin_arg_case6 h l =>
      BA_splitlong (BA h) (BA l)
  | builtin_arg_case7 chunk id ofs =>
      BA_loadglobal chunk id ofs
  | builtin_arg_case8 chunk ofs =>
      BA_loadstack chunk ofs
  | builtin_arg_case9 n e1 =>
      BA_addptr (BA e1) (BA_int n)
  | builtin_arg_case10 id ofs e1 =>
      BA_addptr (BA_addrglobal id ofs) (BA e1)
  | builtin_arg_case11 e1 e2 =>
      BA_addptr (BA e1) (BA e2)
  | builtin_arg_default e =>
      BA e
  end.


Platform-specific known builtins

Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
  None.
Generated by coq2html