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 Archi.
Require Import Coqlib.
Require Import Compopts.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import CminorSel.
Require Import OpHelpers.
Require Import ExtValues ExtFloats.
Require Import DecBoolOps.
Require Import Chunks.
Require Import Builtins.
Require Compopts.

Local Open Scope cminorsel_scope.

Local Open Scope string_scope.
Local Open Scope error_monad_scope.

Section SELECT.

Context {hf: helper_functions}.

Original definition:
Nondetfunction cond_to_condition0 (cond : condition) (args : exprlist) :=
  match cond, args with
  | (Ccompimm c x), (e1 ::: Enil) =>
    if Int.eq_dec x Int.zero
    then Some ((Ccomp0 c), e1)
    else None
           
  | (Ccompuimm c x), (e1 ::: Enil) =>
    if Int.eq_dec x Int.zero
    then Some ((Ccompu0 c), e1)
    else None

  | (Ccomplimm c x), (e1 ::: Enil) =>
    if Int64.eq_dec x Int64.zero
    then Some ((Ccompl0 c), e1)
    else None
           
  | (Ccompluimm c x), (e1 ::: Enil) =>
    if Int64.eq_dec x Int64.zero
    then Some ((Ccomplu0 c), e1)
    else None
           
  | _, _ => None
  end.

Inductive cond_to_condition0_cases: forall (cond : condition) (args : exprlist), Type :=
  | cond_to_condition0_case1: forall c x e1, cond_to_condition0_cases ((Ccompimm c x)) ((e1 ::: Enil))
  | cond_to_condition0_case2: forall c x e1, cond_to_condition0_cases ((Ccompuimm c x)) ((e1 ::: Enil))
  | cond_to_condition0_case3: forall c x e1, cond_to_condition0_cases ((Ccomplimm c x)) ((e1 ::: Enil))
  | cond_to_condition0_case4: forall c x e1, cond_to_condition0_cases ((Ccompluimm c x)) ((e1 ::: Enil))
  | cond_to_condition0_default: forall (cond : condition) (args : exprlist), cond_to_condition0_cases cond args.

Definition cond_to_condition0_match (cond : condition) (args : exprlist) :=
  match cond as zz1, args as zz2 return cond_to_condition0_cases zz1 zz2 with
  | (Ccompimm c x), (e1 ::: Enil) => cond_to_condition0_case1 c x e1
  | (Ccompuimm c x), (e1 ::: Enil) => cond_to_condition0_case2 c x e1
  | (Ccomplimm c x), (e1 ::: Enil) => cond_to_condition0_case3 c x e1
  | (Ccompluimm c x), (e1 ::: Enil) => cond_to_condition0_case4 c x e1
  | cond, args => cond_to_condition0_default cond args
  end.

Definition cond_to_condition0 (cond : condition) (args : exprlist) :=
  match cond_to_condition0_match cond args with
  | cond_to_condition0_case1 c x e1 =>
      if Int.eq_dec x Int.zero then Some ((Ccomp0 c), e1) else None
  | cond_to_condition0_case2 c x e1 =>
      if Int.eq_dec x Int.zero then Some ((Ccompu0 c), e1) else None
  | cond_to_condition0_case3 c x e1 =>
      if Int64.eq_dec x Int64.zero then Some ((Ccompl0 c), e1) else None
  | cond_to_condition0_case4 c x e1 =>
      if Int64.eq_dec x Int64.zero then Some ((Ccomplu0 c), e1) else None
  | cond_to_condition0_default cond args =>
      None
  end.

  
Ternary operator
Original definition:
Nondetfunction select0 (ty : typ) (cond0 : condition0) (e1 e2 e3: expr) :=
  match ty, cond0, e1, e2, e3 with
  | Tint, cond0, e1, (Eop (Ointconst imm) Enil), e3 =>
    (Eop (Oselimm cond0 imm) (e1 ::: e3 ::: Enil))
  | Tint, cond0, (Eop (Ointconst imm) Enil), e2, e3 =>
    (Eop (Oselimm (negate_condition0 cond0) imm) (e2 ::: e3 ::: Enil))
  | Tlong, cond0, e1, (Eop (Olongconst imm) Enil), e3 =>
    (Eop (Osellimm cond0 imm) (e1 ::: e3 ::: Enil))
  | Tlong, cond0, (Eop (Olongconst imm) Enil), e2, e3 =>
    (Eop (Osellimm (negate_condition0 cond0) imm) (e2 ::: e3 ::: Enil))
  | _, _, _ => (Eop (Osel cond0 ty) (e1 ::: e2 ::: e3 ::: Enil))
  end.

Inductive select0_cases: forall (ty : typ) (cond0 : condition0) (e1 e2 e3: expr), Type :=
  | select0_case1: forall cond0 e1 imm e3, select0_cases (Tint) (cond0) (e1) ((Eop (Ointconst imm) Enil)) (e3)
  | select0_case2: forall cond0 imm e2 e3, select0_cases (Tint) (cond0) ((Eop (Ointconst imm) Enil)) (e2) (e3)
  | select0_case3: forall cond0 e1 imm e3, select0_cases (Tlong) (cond0) (e1) ((Eop (Olongconst imm) Enil)) (e3)
  | select0_case4: forall cond0 imm e2 e3, select0_cases (Tlong) (cond0) ((Eop (Olongconst imm) Enil)) (e2) (e3)
  | select0_default: forall (ty : typ) (cond0 : condition0) (e1 e2 e3: expr), select0_cases ty cond0 e1 e2 e3.

Definition select0_match (ty : typ) (cond0 : condition0) (e1 e2 e3: expr) :=
  match ty as zz1, cond0 as zz2, e1 as zz3, e2 as zz4, e3 as zz5 return select0_cases zz1 zz2 zz3 zz4 zz5 with
  | Tint, cond0, e1, (Eop (Ointconst imm) Enil), e3 => select0_case1 cond0 e1 imm e3
  | Tint, cond0, (Eop (Ointconst imm) Enil), e2, e3 => select0_case2 cond0 imm e2 e3
  | Tlong, cond0, e1, (Eop (Olongconst imm) Enil), e3 => select0_case3 cond0 e1 imm e3
  | Tlong, cond0, (Eop (Olongconst imm) Enil), e2, e3 => select0_case4 cond0 imm e2 e3
  | ty, cond0, e1, e2, e3 => select0_default ty cond0 e1 e2 e3
  end.

Definition select0 (ty : typ) (cond0 : condition0) (e1 e2 e3: expr) :=
  match select0_match ty cond0 e1 e2 e3 with
  | select0_case1 cond0 e1 imm e3 =>
      (Eop (Oselimm cond0 imm) (e1 ::: e3 ::: Enil))
  | select0_case2 cond0 imm e2 e3 =>
      (Eop (Oselimm (negate_condition0 cond0) imm) (e2 ::: e3 ::: Enil))
  | select0_case3 cond0 e1 imm e3 =>
      (Eop (Osellimm cond0 imm) (e1 ::: e3 ::: Enil))
  | select0_case4 cond0 imm e2 e3 =>
      (Eop (Osellimm (negate_condition0 cond0) imm) (e2 ::: e3 ::: Enil))
  | select0_default ty cond0 e1 e2 e3 =>
      (Eop (Osel cond0 ty) (e1 ::: e2 ::: e3 ::: 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.

Definition select (ty : typ) (cond : condition) (args : exprlist) (e1 e2: expr) : option expr :=
  Some (if same_expr_pure e1 e2 then e1 else
  match cond_to_condition0 cond args with
  | None => select0 ty (Ccomp0 Cne) e1 e2 (Eop (Ocmp cond) args)
  | Some(cond0, ec) => select0 ty cond0 e1 e2 ec
  end).

          

Constants *


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

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

Integer addition and pointer addition


Definition addimm_shlimm sh k2 e1 :=
  if Compopts.optim_addx tt
  then
    match shift1_4_of_z (Int.unsigned sh) with
    | Some s14 => Eop (Oaddximm s14 k2) (e1:::Enil)
    | None => Eop (Oaddimm k2) ((Eop (Oshlimm sh) (e1:::Enil)):::Enil)
    end
  else Eop (Oaddimm k2) ((Eop (Oshlimm sh) (e1:::Enil)):::Enil).

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 (Oaddximm sh m) (t ::: Enil) => Eop (Oaddximm sh (Int.add n m)) (t ::: Enil)
  | Eop (Oshlimm sh) (t1:::Enil) => addimm_shlimm sh n t1
  | _ => 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 sh m t, addimm_cases (Eop (Oaddximm sh m) (t ::: Enil))
  | addimm_case6: forall sh t1, addimm_cases (Eop (Oshlimm sh) (t1:::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 (Oaddximm sh m) (t ::: Enil) => addimm_case5 sh m t
  | Eop (Oshlimm sh) (t1:::Enil) => addimm_case6 sh t1
  | 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 sh m t =>
      Eop (Oaddximm sh (Int.add n m)) (t ::: Enil)
  | addimm_case6 sh t1 =>
      addimm_shlimm sh n t1
  | addimm_default e =>
      Eop (Oaddimm n) (e ::: Enil)
  end.


Definition add_shlimm n e1 e2 :=
  if Compopts.optim_addx tt
  then
    match shift1_4_of_z (Int.unsigned n) with
    | Some s14 => Eop (Oaddx s14) (e1:::e2:::Enil)
    | None => Eop Oadd (e2:::(Eop (Oshlimm n) (e1:::Enil)):::Enil)
    end
  else Eop Oadd (e2:::(Eop (Oshlimm n) (e1:::Enil)):::Enil).

Original definition:
Nondetfunction add (e1: expr) (e2: expr) :=
  match e1, e2 with
  | Eop (Ointconst n1) Enil, t2 => addimm n1 t2
  | t1, Eop (Ointconst n2) Enil => addimm n2 t1
  | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) =>
      addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil))
  | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddrstack n2) Enil =>
      Eop Oadd (Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n1) n2)) Enil ::: t1 ::: Enil)
  | Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) =>
      Eop Oadd (Eop (Oaddrstack (Ptrofs.add n1 (Ptrofs.of_int n2))) Enil ::: t2 ::: Enil)
  | Eop (Oaddimm n1) (t1:::Enil), t2 =>
      addimm n1 (Eop Oadd (t1:::t2:::Enil))
  | t1, Eop (Oaddimm n2) (t2:::Enil) =>
      addimm n2 (Eop Oadd (t1:::t2:::Enil))
  | t1, (Eop Omul (t2:::t3:::Enil)) =>
    if Compopts.optim_madd tt
    then Eop Omadd (t1:::t2:::t3:::Enil)
    else Eop Oadd (e1:::e2:::Enil)
  | (Eop Omul (t2:::t3:::Enil)), t1 =>
    if Compopts.optim_madd tt
    then Eop Omadd (t1:::t2:::t3:::Enil)
    else Eop Oadd (e1:::e2:::Enil)
  | t1, (Eop (Omulimm n) (t2:::Enil)) =>
    if Compopts.optim_madd tt
    then Eop (Omaddimm n) (t1:::t2:::Enil)
    else Eop Oadd (e1:::e2:::Enil)
  | (Eop (Omulimm n) (t2:::Enil)), t1 =>
    if Compopts.optim_madd tt
    then Eop (Omaddimm n) (t1:::t2:::Enil)
    else Eop Oadd (e1:::e2:::Enil)
  | (Eop (Oshlimm n) (t1:::Enil)), t2 =>
    add_shlimm n t1 t2
  | t2, (Eop (Oshlimm n) (t1:::Enil)) =>
    add_shlimm n t1 t2
  | _, _ => Eop Oadd (e1:::e2:::Enil)
  end.

Inductive add_cases: forall (e1: expr) (e2: expr), Type :=
  | add_case1: forall n1 t2, add_cases (Eop (Ointconst n1) Enil) (t2)
  | add_case2: forall t1 n2, add_cases (t1) (Eop (Ointconst n2) Enil)
  | add_case3: forall n1 t1 n2 t2, add_cases (Eop (Oaddimm n1) (t1:::Enil)) (Eop (Oaddimm n2) (t2:::Enil))
  | add_case4: forall n1 t1 n2, add_cases (Eop (Oaddimm n1) (t1:::Enil)) (Eop (Oaddrstack n2) Enil)
  | add_case5: forall n1 n2 t2, add_cases (Eop (Oaddrstack n1) Enil) (Eop (Oaddimm n2) (t2:::Enil))
  | add_case6: forall n1 t1 t2, add_cases (Eop (Oaddimm n1) (t1:::Enil)) (t2)
  | add_case7: forall t1 n2 t2, add_cases (t1) (Eop (Oaddimm n2) (t2:::Enil))
  | add_case8: forall t1 t2 t3, add_cases (t1) ((Eop Omul (t2:::t3:::Enil)))
  | add_case9: forall t2 t3 t1, add_cases ((Eop Omul (t2:::t3:::Enil))) (t1)
  | add_case10: forall t1 n t2, add_cases (t1) ((Eop (Omulimm n) (t2:::Enil)))
  | add_case11: forall n t2 t1, add_cases ((Eop (Omulimm n) (t2:::Enil))) (t1)
  | add_case12: forall n t1 t2, add_cases ((Eop (Oshlimm n) (t1:::Enil))) (t2)
  | add_case13: forall t2 n t1, add_cases (t2) ((Eop (Oshlimm n) (t1:::Enil)))
  | add_default: forall (e1: expr) (e2: expr), add_cases e1 e2.

Definition add_match (e1: expr) (e2: expr) :=
  match e1 as zz1, e2 as zz2 return add_cases zz1 zz2 with
  | Eop (Ointconst n1) Enil, t2 => add_case1 n1 t2
  | t1, Eop (Ointconst n2) Enil => add_case2 t1 n2
  | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => add_case3 n1 t1 n2 t2
  | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddrstack n2) Enil => add_case4 n1 t1 n2
  | Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) => add_case5 n1 n2 t2
  | Eop (Oaddimm n1) (t1:::Enil), t2 => add_case6 n1 t1 t2
  | t1, Eop (Oaddimm n2) (t2:::Enil) => add_case7 t1 n2 t2
  | t1, (Eop Omul (t2:::t3:::Enil)) => add_case8 t1 t2 t3
  | (Eop Omul (t2:::t3:::Enil)), t1 => add_case9 t2 t3 t1
  | t1, (Eop (Omulimm n) (t2:::Enil)) => add_case10 t1 n t2
  | (Eop (Omulimm n) (t2:::Enil)), t1 => add_case11 n t2 t1
  | (Eop (Oshlimm n) (t1:::Enil)), t2 => add_case12 n t1 t2
  | t2, (Eop (Oshlimm n) (t1:::Enil)) => add_case13 t2 n t1
  | 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 n1 t1 n2 t2 =>
      addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil))
  | add_case4 n1 t1 n2 =>
      Eop Oadd (Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n1) n2)) Enil ::: t1 ::: Enil)
  | add_case5 n1 n2 t2 =>
      Eop Oadd (Eop (Oaddrstack (Ptrofs.add n1 (Ptrofs.of_int n2))) Enil ::: t2 ::: Enil)
  | add_case6 n1 t1 t2 =>
      addimm n1 (Eop Oadd (t1:::t2:::Enil))
  | add_case7 t1 n2 t2 =>
      addimm n2 (Eop Oadd (t1:::t2:::Enil))
  | add_case8 t1 t2 t3 =>
      if Compopts.optim_madd tt then Eop Omadd (t1:::t2:::t3:::Enil) else Eop Oadd (e1:::e2:::Enil)
  | add_case9 t2 t3 t1 =>
      if Compopts.optim_madd tt then Eop Omadd (t1:::t2:::t3:::Enil) else Eop Oadd (e1:::e2:::Enil)
  | add_case10 t1 n t2 =>
      if Compopts.optim_madd tt then Eop (Omaddimm n) (t1:::t2:::Enil) else Eop Oadd (e1:::e2:::Enil)
  | add_case11 n t2 t1 =>
      if Compopts.optim_madd tt then Eop (Omaddimm n) (t1:::t2:::Enil) else Eop Oadd (e1:::e2:::Enil)
  | add_case12 n t1 t2 =>
      add_shlimm n t1 t2
  | add_case13 t2 n t1 =>
      add_shlimm n t1 t2
  | 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))
  | t1, (Eop Omul (t2:::t3:::Enil)) =>
      Eop Omsub (t1:::t2:::t3:::Enil)
  | t1, (Eop (Omulimm n) (t2:::Enil)) =>
    if Compopts.optim_madd tt
    then Eop (Omaddimm (Int.neg n)) (t1:::t2:::Enil)
    else Eop Osub (e1:::e2:::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 t1 t2 t3, sub_cases (t1) ((Eop Omul (t2:::t3:::Enil)))
  | sub_case6: forall t1 n t2, sub_cases (t1) ((Eop (Omulimm n) (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
  | t1, (Eop Omul (t2:::t3:::Enil)) => sub_case5 t1 t2 t3
  | t1, (Eop (Omulimm n) (t2:::Enil)) => sub_case6 t1 n 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 t1 n2 t2 =>
      addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil))
  | sub_case3 n1 t1 t2 =>
      addimm n1 (Eop Osub (t1:::t2:::Enil))
  | sub_case4 t1 n2 t2 =>
      addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil))
  | sub_case5 t1 t2 t3 =>
      Eop Omsub (t1:::t2:::t3:::Enil)
  | sub_case6 t1 n t2 =>
      if Compopts.optim_madd tt then Eop (Omaddimm (Int.neg n)) (t1:::t2:::Enil) else Eop Osub (e1:::e2:::Enil)
  | sub_default e1 e2 =>
      Eop Osub (e1:::e2:::Enil)
  end.


Original definition:
Nondetfunction negint (e: expr) :=
  match e with
  | Eop (Ointconst n) Enil => Eop (Ointconst (Int.neg n)) Enil
  | _ => Eop Oneg (e ::: Enil)
  end.

Inductive negint_cases: forall (e: expr), Type :=
  | negint_case1: forall n, negint_cases (Eop (Ointconst n) Enil)
  | negint_default: forall (e: expr), negint_cases e.

Definition negint_match (e: expr) :=
  match e as zz1 return negint_cases zz1 with
  | Eop (Ointconst n) Enil => negint_case1 n
  | e => negint_default e
  end.

Definition negint (e: expr) :=
  match negint_match e with
  | negint_case1 n =>
      Eop (Ointconst (Int.neg n)) Enil
  | negint_default e =>
      Eop Oneg (e ::: Enil)
  end.


Immediate shifts


Original definition:
Nondetfunction shlimm (e1: expr) (n: int) :=
  if Int.eq n Int.zero then
    e1
  else if negb (Int.ltu n Int.iwordsize) then
    Eop Oshl (e1 ::: Eop (Ointconst n) Enil ::: Enil)
  else match e1 with
    | Eop (Ointconst n1) Enil =>
        Eop (Ointconst (Int.shl n1 n)) Enil
    | Eop (Oshlimm n1) (t1:::Enil) =>
        if Int.ltu (Int.add n n1) Int.iwordsize
        then Eop (Oshlimm (Int.add n n1)) (t1:::Enil)
        else Eop (Oshlimm n) (e1:::Enil)
    | _ =>
        Eop (Oshlimm n) (e1:::Enil)
  end.

Inductive shlimm_cases: forall (e1: expr) , Type :=
  | shlimm_case1: forall n1, shlimm_cases (Eop (Ointconst n1) Enil)
  | shlimm_case2: forall n1 t1, shlimm_cases (Eop (Oshlimm n1) (t1:::Enil))
  | shlimm_default: forall (e1: expr) , shlimm_cases e1.

Definition shlimm_match (e1: expr) :=
  match e1 as zz1 return shlimm_cases zz1 with
  | Eop (Ointconst n1) Enil => shlimm_case1 n1
  | Eop (Oshlimm n1) (t1:::Enil) => shlimm_case2 n1 t1
  | e1 => shlimm_default e1
  end.

Definition shlimm (e1: expr) (n: int) :=
 if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int.iwordsize) then Eop Oshl (e1 ::: Eop (Ointconst n) Enil ::: Enil) else match shlimm_match e1 with
  | shlimm_case1 n1 =>
      Eop (Ointconst (Int.shl n1 n)) Enil
  | shlimm_case2 n1 t1 =>
      if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshlimm (Int.add n n1)) (t1:::Enil) else Eop (Oshlimm n) (e1:::Enil)
  | shlimm_default e1 =>
      Eop (Oshlimm n) (e1:::Enil)
  end.


Original definition:
Nondetfunction shruimm (e1: expr) (n: int) :=
  if Int.eq n Int.zero then
    e1
  else if negb (Int.ltu n Int.iwordsize) then
    Eop Oshru (e1 ::: Eop (Ointconst n) Enil ::: Enil)
  else match e1 with
    | Eop (Ointconst n1) Enil =>
        Eop (Ointconst (Int.shru n1 n)) Enil
    | Eop (Oshruimm n1) (t1:::Enil) =>
        if Int.ltu (Int.add n n1) Int.iwordsize
        then Eop (Oshruimm (Int.add n n1)) (t1:::Enil)
        else Eop (Oshruimm n) (e1:::Enil)
    | Eop (Oshlimm n1) (t1:::Enil) =>
        let stop := Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one) in
	let start := Z.sub (Z.add (Z.add (Int.unsigned n) stop) Z.one) Int.zwordsize in
	if is_bitfield stop start
        then Eop (Oextfz stop start) (t1:::Enil)
	else Eop (Oshruimm n) (e1:::Enil)
    | _ =>
        Eop (Oshruimm n) (e1:::Enil)
    end.

Inductive shruimm_cases: forall (e1: expr) , Type :=
  | shruimm_case1: forall n1, shruimm_cases (Eop (Ointconst n1) Enil)
  | shruimm_case2: forall n1 t1, shruimm_cases (Eop (Oshruimm n1) (t1:::Enil))
  | shruimm_case3: forall n1 t1, shruimm_cases (Eop (Oshlimm n1) (t1:::Enil))
  | shruimm_default: forall (e1: expr) , shruimm_cases e1.

Definition shruimm_match (e1: expr) :=
  match e1 as zz1 return shruimm_cases zz1 with
  | Eop (Ointconst n1) Enil => shruimm_case1 n1
  | Eop (Oshruimm n1) (t1:::Enil) => shruimm_case2 n1 t1
  | Eop (Oshlimm n1) (t1:::Enil) => shruimm_case3 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 (Int.shru n1 n)) Enil
  | shruimm_case2 n1 t1 =>
      if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshruimm (Int.add n n1)) (t1:::Enil) else Eop (Oshruimm n) (e1:::Enil)
  | shruimm_case3 n1 t1 =>
      let stop := Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one) in let start := Z.sub (Z.add (Z.add (Int.unsigned n) stop) Z.one) Int.zwordsize in if is_bitfield stop start then Eop (Oextfz stop start) (t1:::Enil) else Eop (Oshruimm n) (e1:::Enil)
  | shruimm_default e1 =>
      Eop (Oshruimm n) (e1:::Enil)
  end.


Original definition:
Nondetfunction shrimm (e1: expr) (n: int) :=
  if Int.eq n Int.zero then
    e1
  else if negb (Int.ltu n Int.iwordsize) then
    Eop Oshr (e1 ::: Eop (Ointconst n) Enil ::: Enil)
  else match e1 with
    | Eop (Ointconst n1) Enil =>
        Eop (Ointconst (Int.shr n1 n)) Enil
    | Eop (Oshrimm n1) (t1:::Enil) =>
        if Int.ltu (Int.add n n1) Int.iwordsize
        then Eop (Oshrimm (Int.add n n1)) (t1:::Enil)
        else Eop (Oshrimm n) (e1:::Enil)
    | Eop (Oshlimm n1) (t1:::Enil) =>
        let stop := Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one) in
	let start := Z.sub (Z.add (Z.add (Int.unsigned n) stop) Z.one) Int.zwordsize in
	if is_bitfield stop start
        then Eop (Oextfs stop start) (t1:::Enil)
	else Eop (Oshrimm n) (e1:::Enil)
    | _ =>
        Eop (Oshrimm n) (e1:::Enil)
    end.

Inductive shrimm_cases: forall (e1: expr) , Type :=
  | shrimm_case1: forall n1, shrimm_cases (Eop (Ointconst n1) Enil)
  | shrimm_case2: forall n1 t1, shrimm_cases (Eop (Oshrimm n1) (t1:::Enil))
  | shrimm_case3: forall n1 t1, shrimm_cases (Eop (Oshlimm n1) (t1:::Enil))
  | shrimm_default: forall (e1: expr) , shrimm_cases e1.

Definition shrimm_match (e1: expr) :=
  match e1 as zz1 return shrimm_cases zz1 with
  | Eop (Ointconst n1) Enil => shrimm_case1 n1
  | Eop (Oshrimm n1) (t1:::Enil) => shrimm_case2 n1 t1
  | Eop (Oshlimm n1) (t1:::Enil) => shrimm_case3 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 (Int.shr n1 n)) Enil
  | shrimm_case2 n1 t1 =>
      if Int.ltu (Int.add n n1) Int.iwordsize then Eop (Oshrimm (Int.add n n1)) (t1:::Enil) else Eop (Oshrimm n) (e1:::Enil)
  | shrimm_case3 n1 t1 =>
      let stop := Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one) in let start := Z.sub (Z.add (Z.add (Int.unsigned n) stop) Z.one) Int.zwordsize in if is_bitfield stop start then Eop (Oextfs stop start) (t1:::Enil) else Eop (Oshrimm n) (e1:::Enil)
  | shrimm_default e1 =>
      Eop (Oshrimm n) (e1:::Enil)
  end.


Integer multiply


Definition mulimm_base (n1: int) (e2: expr) :=
  match Int.one_bits n1 with
  | i :: nil =>
      shlimm e2 i
  | i :: j :: nil =>
      Elet e2 (add (shlimm (Eletvar 0) i) (shlimm (Eletvar 0) j))
  | _ =>
      Eop (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) :=
  if Archi.ptr64 then
    Eop Olowlong
      (Eop (Oshrlimm (Int.repr 32))
         (Eop Omull (Eop Ocast32signed (e1 ::: Enil) :::
                     Eop Ocast32signed (e2 ::: Enil) ::: Enil) ::: Enil)
          ::: Enil)
  else
    Eop Omulhs (e1 ::: e2 ::: Enil).

Definition mulhu (e1: expr) (e2: expr) :=
  if Archi.ptr64 then
    Eop Olowlong
      (Eop (Oshrluimm (Int.repr 32))
         (Eop Omull (Eop Ocast32unsigned (e1 ::: Enil) :::
                     Eop Ocast32unsigned (e2 ::: Enil) ::: Enil) ::: Enil)
          ::: Enil)
  else
    Eop Omulhu (e1 ::: e2 ::: Enil).

Bitwise and, or, xor


Original definition:
Nondetfunction andimm (n1: int) (e2: expr) :=
  if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil
  else if Int.eq n1 Int.mone then e2
  else match e2 with
  | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.and n1 n2)) Enil
  | Eop (Oandimm n2) (t2:::Enil) => Eop (Oandimm (Int.and n1 n2)) (t2:::Enil)
  | Eop Onot (t2:::Enil) => Eop (Oandnimm n1) (t2:::Enil)
  | _ => Eop (Oandimm n1) (e2:::Enil)
  end.

Inductive andimm_cases: forall (e2: expr), Type :=
  | andimm_case1: forall n2, andimm_cases (Eop (Ointconst n2) Enil)
  | andimm_case2: forall n2 t2, andimm_cases (Eop (Oandimm n2) (t2:::Enil))
  | andimm_case3: forall t2, andimm_cases (Eop Onot (t2:::Enil))
  | andimm_default: forall (e2: expr), andimm_cases e2.

Definition andimm_match (e2: expr) :=
  match e2 as zz1 return andimm_cases zz1 with
  | Eop (Ointconst n2) Enil => andimm_case1 n2
  | Eop (Oandimm n2) (t2:::Enil) => andimm_case2 n2 t2
  | Eop Onot (t2:::Enil) => andimm_case3 t2
  | e2 => andimm_default e2
  end.

Definition andimm (n1: int) (e2: expr) :=
 if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else if Int.eq n1 Int.mone then e2 else match andimm_match e2 with
  | andimm_case1 n2 =>
      Eop (Ointconst (Int.and n1 n2)) Enil
  | andimm_case2 n2 t2 =>
      Eop (Oandimm (Int.and n1 n2)) (t2:::Enil)
  | andimm_case3 t2 =>
      Eop (Oandnimm n1) (t2:::Enil)
  | andimm_default e2 =>
      Eop (Oandimm n1) (e2:::Enil)
  end.


Original definition:
Nondetfunction and (e1: expr) (e2: expr) :=
  match e1, e2 with
  | Eop (Ointconst n1) Enil, t2 => andimm n1 t2
  | t1, Eop (Ointconst n2) Enil => andimm n2 t1
  | (Eop Onot (t1:::Enil)), t2 => Eop Oandn (t1:::t2:::Enil) 
  | t1, (Eop Onot (t2:::Enil)) => Eop Oandn (t2:::t1:::Enil) 
  | _, _ => Eop Oand (e1:::e2:::Enil)
  end.

Inductive and_cases: forall (e1: expr) (e2: expr), Type :=
  | and_case1: forall n1 t2, and_cases (Eop (Ointconst n1) Enil) (t2)
  | and_case2: forall t1 n2, and_cases (t1) (Eop (Ointconst n2) Enil)
  | and_case3: forall t1 t2, and_cases ((Eop Onot (t1:::Enil))) (t2)
  | and_case4: forall t1 t2, and_cases (t1) ((Eop Onot (t2:::Enil)))
  | and_default: forall (e1: expr) (e2: expr), and_cases e1 e2.

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

Definition and (e1: expr) (e2: expr) :=
  match and_match e1 e2 with
  | and_case1 n1 t2 =>
      andimm n1 t2
  | and_case2 t1 n2 =>
      andimm n2 t1
  | and_case3 t1 t2 =>
      Eop Oandn (t1:::t2:::Enil)
  | and_case4 t1 t2 =>
      Eop Oandn (t2:::t1:::Enil)
  | and_default e1 e2 =>
      Eop Oand (e1:::e2:::Enil)
  end.


Original definition:
Nondetfunction orimm (n1: int) (e2: expr) :=
  if Int.eq n1 Int.zero then e2
  else if Int.eq n1 Int.mone then Eop (Ointconst Int.mone) Enil
  else match e2 with
       | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.or n1 n2)) Enil
       | Eop (Oorimm n2) (t2:::Enil) => Eop (Oorimm (Int.or n1 n2)) (t2:::Enil)
       | Eop Onot (t2:::Enil) => Eop (Oornimm n1) (t2:::Enil)
       | _ => Eop (Oorimm n1) (e2:::Enil)
  end.

Inductive orimm_cases: forall (e2: expr), Type :=
  | orimm_case1: forall n2, orimm_cases (Eop (Ointconst n2) Enil)
  | orimm_case2: forall n2 t2, orimm_cases (Eop (Oorimm n2) (t2:::Enil))
  | orimm_case3: forall t2, orimm_cases (Eop Onot (t2:::Enil))
  | orimm_default: forall (e2: expr), orimm_cases e2.

Definition orimm_match (e2: expr) :=
  match e2 as zz1 return orimm_cases zz1 with
  | Eop (Ointconst n2) Enil => orimm_case1 n2
  | Eop (Oorimm n2) (t2:::Enil) => orimm_case2 n2 t2
  | Eop Onot (t2:::Enil) => orimm_case3 t2
  | e2 => orimm_default e2
  end.

Definition orimm (n1: int) (e2: expr) :=
 if Int.eq n1 Int.zero then e2 else if Int.eq n1 Int.mone then Eop (Ointconst Int.mone) Enil else match orimm_match e2 with
  | orimm_case1 n2 =>
      Eop (Ointconst (Int.or n1 n2)) Enil
  | orimm_case2 n2 t2 =>
      Eop (Oorimm (Int.or n1 n2)) (t2:::Enil)
  | orimm_case3 t2 =>
      Eop (Oornimm n1) (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 (Oshlimm n1) (t1:::Enil), Eop (Oshruimm n2) (t2:::Enil) =>
      if Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2
      then Eop (Ororimm n2) (t1:::Enil)
      else Eop Oor (e1:::e2:::Enil)
  | Eop (Oshruimm n2) (t2:::Enil), Eop (Oshlimm n1) (t1:::Enil) =>
      if Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2
      then Eop (Ororimm n2) (t1:::Enil)
      else Eop Oor (e1:::e2:::Enil)
  | (Eop Onot (t1:::Enil)), t2 => Eop Oorn (t1:::t2:::Enil) 
  | t1, (Eop Onot (t2:::Enil))  => Eop Oorn (t2:::t1:::Enil)
  | (Eop (Oandimm nmask) (prev:::Enil)),
    (Eop (Oandimm mask)
      ((Eop (Oshlimm start) (fld:::Enil)):::Enil)) =>
      let zstart := Int.unsigned start in
      let zstop := int_highest_bit mask in
      if is_bitfield zstop zstart
      then
        let mask' := Int.repr (zbitfield_mask zstop zstart) in
          if and_dec (Int.eq_dec mask mask')
                     (Int.eq_dec nmask (Int.not mask'))
          then Eop (Oinsf zstop zstart) (prev:::fld:::Enil)
          else Eop Oor (e1:::e2:::Enil)
      else Eop Oor (e1:::e2:::Enil)
  | (Eop (Oandimm nmask) (prev:::Enil)),
    (Eop (Oandimm mask) (fld:::Enil)) =>
      let zstart := 0 in
      let zstop := int_highest_bit mask in
      if is_bitfield zstop zstart
      then
        let mask' := Int.repr (zbitfield_mask zstop zstart) in
          if and_dec (Int.eq_dec mask mask')
                     (Int.eq_dec nmask (Int.not mask'))
          then Eop (Oinsf zstop zstart) (prev:::fld:::Enil)
          else Eop Oor (e1:::e2:::Enil)
      else Eop Oor (e1:::e2:::Enil)
  | _, _ => Eop Oor (e1:::e2:::Enil)
  end.

Inductive or_cases: forall (e1: expr) (e2: expr), Type :=
  | or_case1: forall n1 t2, or_cases (Eop (Ointconst n1) Enil) (t2)
  | or_case2: forall t1 n2, or_cases (t1) (Eop (Ointconst n2) Enil)
  | or_case3: forall n1 t1 n2 t2, or_cases (Eop (Oshlimm n1) (t1:::Enil)) (Eop (Oshruimm n2) (t2:::Enil))
  | or_case4: forall n2 t2 n1 t1, or_cases (Eop (Oshruimm n2) (t2:::Enil)) (Eop (Oshlimm n1) (t1:::Enil))
  | or_case5: forall t1 t2, or_cases ((Eop Onot (t1:::Enil))) (t2)
  | or_case6: forall t1 t2, or_cases (t1) ((Eop Onot (t2:::Enil)))
  | or_case7: forall nmask prev mask start fld, or_cases ((Eop (Oandimm nmask) (prev:::Enil))) ((Eop (Oandimm mask) ((Eop (Oshlimm start) (fld:::Enil)):::Enil)))
  | or_case8: forall nmask prev mask fld, or_cases ((Eop (Oandimm nmask) (prev:::Enil))) ((Eop (Oandimm mask) (fld:::Enil)))
  | or_default: forall (e1: expr) (e2: expr), or_cases e1 e2.

Definition or_match (e1: expr) (e2: expr) :=
  match e1 as zz1, e2 as zz2 return or_cases zz1 zz2 with
  | Eop (Ointconst n1) Enil, t2 => or_case1 n1 t2
  | t1, Eop (Ointconst n2) Enil => or_case2 t1 n2
  | Eop (Oshlimm n1) (t1:::Enil), Eop (Oshruimm n2) (t2:::Enil) => or_case3 n1 t1 n2 t2
  | Eop (Oshruimm n2) (t2:::Enil), Eop (Oshlimm n1) (t1:::Enil) => or_case4 n2 t2 n1 t1
  | (Eop Onot (t1:::Enil)), t2 => or_case5 t1 t2
  | t1, (Eop Onot (t2:::Enil)) => or_case6 t1 t2
  | (Eop (Oandimm nmask) (prev:::Enil)), (Eop (Oandimm mask) ((Eop (Oshlimm start) (fld:::Enil)):::Enil)) => or_case7 nmask prev mask start fld
  | (Eop (Oandimm nmask) (prev:::Enil)), (Eop (Oandimm mask) (fld:::Enil)) => or_case8 nmask prev mask fld
  | e1, e2 => or_default e1 e2
  end.

Definition or (e1: expr) (e2: expr) :=
  match or_match e1 e2 with
  | or_case1 n1 t2 =>
      orimm n1 t2
  | or_case2 t1 n2 =>
      orimm n2 t1
  | or_case3 n1 t1 n2 t2 =>
      if Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2 then Eop (Ororimm n2) (t1:::Enil) else Eop Oor (e1:::e2:::Enil)
  | or_case4 n2 t2 n1 t1 =>
      if Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2 then Eop (Ororimm n2) (t1:::Enil) else Eop Oor (e1:::e2:::Enil)
  | or_case5 t1 t2 =>
      Eop Oorn (t1:::t2:::Enil)
  | or_case6 t1 t2 =>
      Eop Oorn (t2:::t1:::Enil)
  | or_case7 nmask prev mask start fld =>
      let zstart := Int.unsigned start in let zstop := int_highest_bit mask in if is_bitfield zstop zstart then let mask' := Int.repr (zbitfield_mask zstop zstart) in if and_dec (Int.eq_dec mask mask') (Int.eq_dec nmask (Int.not mask')) then Eop (Oinsf zstop zstart) (prev:::fld:::Enil) else Eop Oor (e1:::e2:::Enil) else Eop Oor (e1:::e2:::Enil)
  | or_case8 nmask prev mask fld =>
      let zstart := 0 in let zstop := int_highest_bit mask in if is_bitfield zstop zstart then let mask' := Int.repr (zbitfield_mask zstop zstart) in if and_dec (Int.eq_dec mask mask') (Int.eq_dec nmask (Int.not mask')) then Eop (Oinsf zstop zstart) (prev:::fld:::Enil) else Eop Oor (e1:::e2:::Enil) else Eop Oor (e1:::e2:::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 Eop Onot (e2:::Enil)
  else
  match e2 with
  | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.xor n1 n2)) Enil
  | Eop (Oxorimm n2) (t2:::Enil) =>
      let n := Int.xor n1 n2 in
      if Int.eq n Int.zero then t2 else Eop (Oxorimm n) (t2:::Enil)
  | _ => Eop (Oxorimm n1) (e2:::Enil)
  end.

Inductive xorimm_cases: forall (e2: expr), Type :=
  | xorimm_case1: forall n2, xorimm_cases (Eop (Ointconst n2) Enil)
  | xorimm_case2: forall n2 t2, xorimm_cases (Eop (Oxorimm n2) (t2:::Enil))
  | xorimm_default: forall (e2: expr), xorimm_cases e2.

Definition xorimm_match (e2: expr) :=
  match e2 as zz1 return xorimm_cases zz1 with
  | Eop (Ointconst n2) Enil => xorimm_case1 n2
  | Eop (Oxorimm n2) (t2:::Enil) => xorimm_case2 n2 t2
  | e2 => xorimm_default e2
  end.

Definition xorimm (n1: int) (e2: expr) :=
 if Int.eq n1 Int.zero then e2 else if Int.eq n1 Int.mone then Eop Onot (e2:::Enil) else match xorimm_match e2 with
  | xorimm_case1 n2 =>
      Eop (Ointconst (Int.xor n1 n2)) Enil
  | xorimm_case2 n2 t2 =>
      let n := Int.xor n1 n2 in if Int.eq n Int.zero then t2 else Eop (Oxorimm n) (t2:::Enil)
  | xorimm_default e2 =>
      Eop (Oxorimm n1) (e2:::Enil)
  end.


Original definition:
Nondetfunction xor (e1: expr) (e2: expr) :=
  match e1, e2 with
  | Eop (Ointconst n1) Enil, t2 => xorimm n1 t2
  | t1, Eop (Ointconst n2) Enil => xorimm n2 t1
  | _, _ => Eop Oxor (e1:::e2:::Enil)
  end.

Inductive xor_cases: forall (e1: expr) (e2: expr), Type :=
  | xor_case1: forall n1 t2, xor_cases (Eop (Ointconst n1) Enil) (t2)
  | xor_case2: forall t1 n2, xor_cases (t1) (Eop (Ointconst n2) Enil)
  | xor_default: forall (e1: expr) (e2: expr), xor_cases e1 e2.

Definition xor_match (e1: expr) (e2: expr) :=
  match e1 as zz1, e2 as zz2 return xor_cases zz1 zz2 with
  | Eop (Ointconst n1) Enil, t2 => xor_case1 n1 t2
  | t1, Eop (Ointconst n2) Enil => xor_case2 t1 n2
  | e1, e2 => xor_default e1 e2
  end.

Definition xor (e1: expr) (e2: expr) :=
  match xor_match e1 e2 with
  | xor_case1 n1 t2 =>
      xorimm n1 t2
  | xor_case2 t1 n2 =>
      xorimm n2 t1
  | xor_default e1 e2 =>
      Eop Oxor (e1:::e2:::Enil)
  end.


Integer logical negation


Original definition:
Nondetfunction notint (e: expr) :=
  match e with
  | Eop Oand (e1:::e2:::Enil) => Eop Onand (e1:::e2:::Enil)
  | Eop (Oandimm n) (e1:::Enil) => Eop (Onandimm n) (e1:::Enil)
  | Eop Oor (e1:::e2:::Enil) => Eop Onor (e1:::e2:::Enil)
  | Eop (Oorimm n) (e1:::Enil) => Eop (Onorimm n) (e1:::Enil)
  | Eop Oxor (e1:::e2:::Enil) => Eop Onxor (e1:::e2:::Enil)
  | Eop (Oxorimm n) (e1:::Enil) => Eop (Onxorimm n) (e1:::Enil)
  | Eop Onand (e1:::e2:::Enil) => Eop Oand (e1:::e2:::Enil)
  | Eop (Onandimm n) (e1:::Enil) => Eop (Oandimm n) (e1:::Enil)
  | Eop Onor (e1:::e2:::Enil) => Eop Oor (e1:::e2:::Enil)
  | Eop (Onorimm n) (e1:::Enil) => Eop (Oorimm n) (e1:::Enil)
  | Eop Onxor (e1:::e2:::Enil) => Eop Oxor (e1:::e2:::Enil)
  | Eop (Onxorimm n) (e1:::Enil) => Eop (Oxorimm n) (e1:::Enil)
  | Eop Oandn (e1:::e2:::Enil) => Eop Oorn (e2:::e1:::Enil)
  | Eop (Oandnimm n) (e1:::Enil) => Eop (Oorimm (Int.not n)) (e1:::Enil)
  | Eop Oorn (e1:::e2:::Enil) => Eop Oandn (e2:::e1:::Enil)
  | Eop (Oornimm n) (e1:::Enil) => Eop (Oandimm (Int.not n)) (e1:::Enil)
  | Eop Onot (e1:::Enil) => e1
  | Eop (Ointconst k) Enil => Eop (Ointconst (Int.not k)) Enil
  | _ => Eop Onot (e:::Enil)
  end.

Inductive notint_cases: forall (e: expr), Type :=
  | notint_case1: forall e1 e2, notint_cases (Eop Oand (e1:::e2:::Enil))
  | notint_case2: forall n e1, notint_cases (Eop (Oandimm n) (e1:::Enil))
  | notint_case3: forall e1 e2, notint_cases (Eop Oor (e1:::e2:::Enil))
  | notint_case4: forall n e1, notint_cases (Eop (Oorimm n) (e1:::Enil))
  | notint_case5: forall e1 e2, notint_cases (Eop Oxor (e1:::e2:::Enil))
  | notint_case6: forall n e1, notint_cases (Eop (Oxorimm n) (e1:::Enil))
  | notint_case7: forall e1 e2, notint_cases (Eop Onand (e1:::e2:::Enil))
  | notint_case8: forall n e1, notint_cases (Eop (Onandimm n) (e1:::Enil))
  | notint_case9: forall e1 e2, notint_cases (Eop Onor (e1:::e2:::Enil))
  | notint_case10: forall n e1, notint_cases (Eop (Onorimm n) (e1:::Enil))
  | notint_case11: forall e1 e2, notint_cases (Eop Onxor (e1:::e2:::Enil))
  | notint_case12: forall n e1, notint_cases (Eop (Onxorimm n) (e1:::Enil))
  | notint_case13: forall e1 e2, notint_cases (Eop Oandn (e1:::e2:::Enil))
  | notint_case14: forall n e1, notint_cases (Eop (Oandnimm n) (e1:::Enil))
  | notint_case15: forall e1 e2, notint_cases (Eop Oorn (e1:::e2:::Enil))
  | notint_case16: forall n e1, notint_cases (Eop (Oornimm n) (e1:::Enil))
  | notint_case17: forall e1, notint_cases (Eop Onot (e1:::Enil))
  | notint_case18: forall k, notint_cases (Eop (Ointconst k) Enil)
  | notint_default: forall (e: expr), notint_cases e.

Definition notint_match (e: expr) :=
  match e as zz1 return notint_cases zz1 with
  | Eop Oand (e1:::e2:::Enil) => notint_case1 e1 e2
  | Eop (Oandimm n) (e1:::Enil) => notint_case2 n e1
  | Eop Oor (e1:::e2:::Enil) => notint_case3 e1 e2
  | Eop (Oorimm n) (e1:::Enil) => notint_case4 n e1
  | Eop Oxor (e1:::e2:::Enil) => notint_case5 e1 e2
  | Eop (Oxorimm n) (e1:::Enil) => notint_case6 n e1
  | Eop Onand (e1:::e2:::Enil) => notint_case7 e1 e2
  | Eop (Onandimm n) (e1:::Enil) => notint_case8 n e1
  | Eop Onor (e1:::e2:::Enil) => notint_case9 e1 e2
  | Eop (Onorimm n) (e1:::Enil) => notint_case10 n e1
  | Eop Onxor (e1:::e2:::Enil) => notint_case11 e1 e2
  | Eop (Onxorimm n) (e1:::Enil) => notint_case12 n e1
  | Eop Oandn (e1:::e2:::Enil) => notint_case13 e1 e2
  | Eop (Oandnimm n) (e1:::Enil) => notint_case14 n e1
  | Eop Oorn (e1:::e2:::Enil) => notint_case15 e1 e2
  | Eop (Oornimm n) (e1:::Enil) => notint_case16 n e1
  | Eop Onot (e1:::Enil) => notint_case17 e1
  | Eop (Ointconst k) Enil => notint_case18 k
  | e => notint_default e
  end.

Definition notint (e: expr) :=
  match notint_match e with
  | notint_case1 e1 e2 =>
      Eop Onand (e1:::e2:::Enil)
  | notint_case2 n e1 =>
      Eop (Onandimm n) (e1:::Enil)
  | notint_case3 e1 e2 =>
      Eop Onor (e1:::e2:::Enil)
  | notint_case4 n e1 =>
      Eop (Onorimm n) (e1:::Enil)
  | notint_case5 e1 e2 =>
      Eop Onxor (e1:::e2:::Enil)
  | notint_case6 n e1 =>
      Eop (Onxorimm n) (e1:::Enil)
  | notint_case7 e1 e2 =>
      Eop Oand (e1:::e2:::Enil)
  | notint_case8 n e1 =>
      Eop (Oandimm n) (e1:::Enil)
  | notint_case9 e1 e2 =>
      Eop Oor (e1:::e2:::Enil)
  | notint_case10 n e1 =>
      Eop (Oorimm n) (e1:::Enil)
  | notint_case11 e1 e2 =>
      Eop Oxor (e1:::e2:::Enil)
  | notint_case12 n e1 =>
      Eop (Oxorimm n) (e1:::Enil)
  | notint_case13 e1 e2 =>
      Eop Oorn (e2:::e1:::Enil)
  | notint_case14 n e1 =>
      Eop (Oorimm (Int.not n)) (e1:::Enil)
  | notint_case15 e1 e2 =>
      Eop Oandn (e2:::e1:::Enil)
  | notint_case16 n e1 =>
      Eop (Oandimm (Int.not n)) (e1:::Enil)
  | notint_case17 e1 =>
      e1
  | notint_case18 k =>
      Eop (Ointconst (Int.not k)) Enil
  | notint_default e =>
      Eop Onot (e:::Enil)
  end.


Integer division and modulus


Definition divs_base (e1: expr) (e2: expr) :=
  Eexternal i32_sdiv sig_ii_i (e1 ::: e2 ::: Enil).
  
Definition mods_base (e1: expr) (e2: expr) :=
  Eexternal i32_smod sig_ii_i (e1 ::: e2 ::: Enil).

Definition divu_base (e1: expr) (e2: expr) :=
  Eexternal i32_udiv sig_ii_i (e1 ::: e2 ::: Enil).
  
Definition modu_base (e1: expr) (e2: expr) :=
  Eexternal i32_umod sig_ii_i (e1 ::: e2 ::: Enil).

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
  | _, _ =>
       Eop (Ocmp (default c n2)) (e1 ::: Enil)
  end.

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

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

Definition compimm (default: comparison -> int -> condition) (sem: comparison -> int -> int -> bool) (c: comparison) (e1: expr) (n2: int) :=
  match compimm_match c e1 with
  | compimm_case1 c n1 =>
      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_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 (Ccompfs c)) (e1 ::: e2 ::: Enil).

Integer conversions


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

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

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

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

Definition cast8signed (e: expr) :=
  match cast8signed_match e with
  | cast8signed_case1 n =>
      Eop (Ointconst (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) := Eop Ointuoffloat (e ::: Enil).

Original definition:
Nondetfunction floatofintu (e: expr) :=
  match e with
  | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_intu n)) Enil
  | _ => Eop Ofloatoflongu ((Eop Ocast32unsigned (e ::: Enil)) ::: 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 =>
      Eop Ofloatoflongu ((Eop Ocast32unsigned (e ::: Enil)) ::: Enil)
  end.


Original definition:
Nondetfunction floatofint (e: expr) :=
  match e with
  | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_int n)) Enil
  | _ => Eop Ofloatoflong ((Eop Ocast32signed (e ::: Enil)) ::: 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 =>
      Eop Ofloatoflong ((Eop Ocast32signed (e ::: Enil)) ::: Enil)
  end.


Definition intofsingle (e: expr) := Eop Ointofsingle (e ::: Enil).
Definition singleofint (e: expr) := Eop Osingleofint (e ::: Enil).

Definition intuofsingle (e: expr) := Eop Ointuofsingle (e ::: Enil).
Definition singleofintu (e: expr) := Eop Osingleofintu (e ::: Enil).

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

Recognition of addressing modes for load and store operations


Original definition:
Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
  match e with
  | Eop (Oaddrstack n) Enil => (Ainstack n, Enil)
  | Eop (Oaddrsymbol id ofs) Enil =>
    (if (orb (Archi.pic_code tt) (negb (Compopts.optim_globaladdrtmp tt)))
     then (Aindexed Ptrofs.zero, e:::Enil)
     else (Aglobal id ofs, Enil))
  | Eop (Oaddimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int n), e1:::Enil)
  | Eop (Oaddlimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int64 n), e1:::Enil)
  | Eop Oaddl (e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil) =>
    (if Compopts.optim_xsaddr tt
     then let zscale := Int.unsigned scale in
          if Z.eq_dec zscale (zscale_of_chunk chunk)
          then (Aindexed2XS zscale, e1:::e2:::Enil) 
          else (Aindexed2, e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil)
     else (Aindexed2, e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil))
  | Eop (Oaddxl sh) (e1:::e2:::Enil) =>
    let zscale := ExtValues.z_of_shift1_4 sh in
    let scale := Int.repr zscale in
    (if Compopts.optim_xsaddr tt
     then if Z.eq_dec zscale (zscale_of_chunk chunk)
          then (Aindexed2XS zscale, e2:::e1:::Enil) 
          else (Aindexed2, e2:::(Eop (Oshllimm scale) (e1:::Enil)):::Enil)
     else (Aindexed2, e2:::(Eop (Oshllimm scale) (e1:::Enil)):::Enil))
  | Eop Oaddl (e1:::e2:::Enil) => (Aindexed2, e1:::e2:::Enil) 
  | _ => (Aindexed Ptrofs.zero, e:::Enil)
  end.

Inductive addressing_cases: forall (e: expr), Type :=
  | addressing_case1: forall n, addressing_cases (Eop (Oaddrstack n) Enil)
  | addressing_case2: forall id ofs, addressing_cases (Eop (Oaddrsymbol id ofs) Enil)
  | addressing_case3: forall n e1, addressing_cases (Eop (Oaddimm n) (e1:::Enil))
  | addressing_case4: forall n e1, addressing_cases (Eop (Oaddlimm n) (e1:::Enil))
  | addressing_case5: forall e1 scale e2, addressing_cases (Eop Oaddl (e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil))
  | addressing_case6: forall sh e1 e2, addressing_cases (Eop (Oaddxl sh) (e1:::e2:::Enil))
  | addressing_case7: forall e1 e2, addressing_cases (Eop Oaddl (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 (Oaddrsymbol id ofs) Enil => addressing_case2 id ofs
  | Eop (Oaddimm n) (e1:::Enil) => addressing_case3 n e1
  | Eop (Oaddlimm n) (e1:::Enil) => addressing_case4 n e1
  | Eop Oaddl (e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil) => addressing_case5 e1 scale e2
  | Eop (Oaddxl sh) (e1:::e2:::Enil) => addressing_case6 sh e1 e2
  | Eop Oaddl (e1:::e2:::Enil) => addressing_case7 e1 e2
  | e => addressing_default e
  end.

Definition addressing (chunk: memory_chunk) (e: expr) :=
  match addressing_match e with
  | addressing_case1 n =>
      (Ainstack n, Enil)
  | addressing_case2 id ofs =>
      (if (orb (Archi.pic_code tt) (negb (Compopts.optim_globaladdrtmp tt))) then (Aindexed Ptrofs.zero, e:::Enil) else (Aglobal id ofs, Enil))
  | addressing_case3 n e1 =>
      (Aindexed (Ptrofs.of_int n), e1:::Enil)
  | addressing_case4 n e1 =>
      (Aindexed (Ptrofs.of_int64 n), e1:::Enil)
  | addressing_case5 e1 scale e2 =>
      (if Compopts.optim_xsaddr tt then let zscale := Int.unsigned scale in if Z.eq_dec zscale (zscale_of_chunk chunk) then (Aindexed2XS zscale, e1:::e2:::Enil) else (Aindexed2, e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil) else (Aindexed2, e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil))
  | addressing_case6 sh e1 e2 =>
      let zscale := ExtValues.z_of_shift1_4 sh in let scale := Int.repr zscale in (if Compopts.optim_xsaddr tt then if Z.eq_dec zscale (zscale_of_chunk chunk) then (Aindexed2XS zscale, e2:::e1:::Enil) else (Aindexed2, e2:::(Eop (Oshllimm scale) (e1:::Enil)):::Enil) else (Aindexed2, e2:::(Eop (Oshllimm scale) (e1:::Enil)):::Enil))
  | addressing_case7 e1 e2 =>
      (Aindexed2, e1:::e2:::Enil)
  | addressing_default e =>
      (Aindexed Ptrofs.zero, e:::Enil)
  end.


Arguments of builtins


Original definition:
Nondetfunction builtin_arg (e: expr) :=
  match e with
  | Eop (Ointconst n) Enil => BA_int n
  | Eop (Oaddrsymbol id ofs) Enil => BA_addrglobal id ofs
  | Eop (Oaddrstack ofs) Enil => BA_addrstack ofs
  | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) =>
        BA_long (Int64.ofwords h l)
  | Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l)
  | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs
  | Eop (Oaddimm n) (e1:::Enil) =>
      if Archi.ptr64 then BA e else BA_addptr (BA e1) (BA_int n)
  | Eop (Oaddlimm n) (e1:::Enil) =>
      if Archi.ptr64 then BA_addptr (BA e1) (BA_long n) else BA e
  | _ => BA e
  end.

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

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

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



Definition divf_base (e1: expr) (e2: expr) :=
  Eexternal f64_div sig_ff_f (e1 ::: e2 ::: Enil).

Definition divfs_base1 (e2 : expr) :=
  Eop Oinvfs (e2 ::: Enil).
Definition divfs_baseX (e1 : expr) (e2 : expr) :=
  Eexternal f32_div sig_ss_s (e1 ::: e2 ::: Enil).

Original definition:
Nondetfunction divfs_base (e1: expr) :=
  match e1 with
  | Eop (Osingleconst f) Enil =>
    (if Float32.eq_dec f ExtFloat32.one
     then divfs_base1
     else divfs_baseX e1)
  | _ => divfs_baseX e1
  end.

Inductive divfs_base_cases: forall (e1: expr), Type :=
  | divfs_base_case1: forall f, divfs_base_cases (Eop (Osingleconst f) Enil)
  | divfs_base_default: forall (e1: expr), divfs_base_cases e1.

Definition divfs_base_match (e1: expr) :=
  match e1 as zz1 return divfs_base_cases zz1 with
  | Eop (Osingleconst f) Enil => divfs_base_case1 f
  | e1 => divfs_base_default e1
  end.

Definition divfs_base (e1: expr) :=
  match divfs_base_match e1 with
  | divfs_base_case1 f =>
      (if Float32.eq_dec f ExtFloat32.one then divfs_base1 else divfs_baseX e1)
  | divfs_base_default e1 =>
      divfs_baseX e1
  end.


Original definition:
Nondetfunction gen_fma args :=
  match args with
  | (Eop Onegf (e1:::Enil)):::e2:::e3:::Enil => Some (Eop Ofmsubf (e3:::e1:::e2:::Enil))
  | e1:::e2:::e3:::Enil => Some (Eop Ofmaddf (e3:::e1:::e2:::Enil))
  | _ => None
  end.

Inductive gen_fma_cases: forall args, Type :=
  | gen_fma_case1: forall e1 e2 e3, gen_fma_cases ((Eop Onegf (e1:::Enil)):::e2:::e3:::Enil)
  | gen_fma_case2: forall e1 e2 e3, gen_fma_cases (e1:::e2:::e3:::Enil)
  | gen_fma_default: forall args, gen_fma_cases args.

Definition gen_fma_match args :=
  match args as zz1 return gen_fma_cases zz1 with
  | (Eop Onegf (e1:::Enil)):::e2:::e3:::Enil => gen_fma_case1 e1 e2 e3
  | e1:::e2:::e3:::Enil => gen_fma_case2 e1 e2 e3
  | args => gen_fma_default args
  end.

Definition gen_fma args :=
  match gen_fma_match args with
  | gen_fma_case1 e1 e2 e3 =>
      Some (Eop Ofmsubf (e3:::e1:::e2:::Enil))
  | gen_fma_case2 e1 e2 e3 =>
      Some (Eop Ofmaddf (e3:::e1:::e2:::Enil))
  | gen_fma_default args =>
      None
  end.


Original definition:
Nondetfunction gen_fmaf args :=
  match args with
  | (Eop Onegfs (e1:::Enil)):::e2:::e3:::Enil => Some (Eop Ofmsubfs (e3:::e1:::e2:::Enil))
  | e1:::e2:::e3:::Enil => Some (Eop Ofmaddfs (e3:::e1:::e2:::Enil))
  | _ => None
  end.

Inductive gen_fmaf_cases: forall args, Type :=
  | gen_fmaf_case1: forall e1 e2 e3, gen_fmaf_cases ((Eop Onegfs (e1:::Enil)):::e2:::e3:::Enil)
  | gen_fmaf_case2: forall e1 e2 e3, gen_fmaf_cases (e1:::e2:::e3:::Enil)
  | gen_fmaf_default: forall args, gen_fmaf_cases args.

Definition gen_fmaf_match args :=
  match args as zz1 return gen_fmaf_cases zz1 with
  | (Eop Onegfs (e1:::Enil)):::e2:::e3:::Enil => gen_fmaf_case1 e1 e2 e3
  | e1:::e2:::e3:::Enil => gen_fmaf_case2 e1 e2 e3
  | args => gen_fmaf_default args
  end.

Definition gen_fmaf args :=
  match gen_fmaf_match args with
  | gen_fmaf_case1 e1 e2 e3 =>
      Some (Eop Ofmsubfs (e3:::e1:::e2:::Enil))
  | gen_fmaf_case2 e1 e2 e3 =>
      Some (Eop Ofmaddfs (e3:::e1:::e2:::Enil))
  | gen_fmaf_default args =>
      None
  end.


Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
  match b with
  | BI_fmin => Some (Eop Ominf args)
  | BI_fmax => Some (Eop Omaxf args)
  | BI_fminf => Some (Eop Ominfs args)
  | BI_fmaxf => Some (Eop Omaxfs args)
  | BI_fma => gen_fma args
  | BI_fmaf => gen_fmaf args
  end.
End SELECT.