Module SelectOp

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}.

Inductive to_cond0 :=
| Cond0_some : condition0 -> expr -> to_cond0
| Cond0_none : to_cond0
| Cond0_true : to_cond0
| Cond0_false : to_cond0.

Definition compu0 c e1 :=
  match c with
  | Clt => Cond0_false
  | Cge => Cond0_true
  | _ => Cond0_some (Ccompu0 c) e1
  end.

Definition complu0 c e1 :=
  match c with
  | Clt => Cond0_false
  | Cge => Cond0_true
  | _ => Cond0_some (Ccomplu0 c) e1
  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 Cond0_some (Ccomp0 c) e1 else Cond0_none
  | cond_to_condition0_case2 c x e1 =>
      if Int.eq_dec x Int.zero then compu0 c e1 else Cond0_none
  | cond_to_condition0_case3 c x e1 =>
      if Int64.eq_dec x Int64.zero then Cond0_some (Ccompl0 c) e1 else Cond0_none
  | cond_to_condition0_case4 c x e1 =>
      if Int64.eq_dec x Int64.zero then complu0 c e1 else Cond0_none
  | cond_to_condition0_default cond args =>
      Cond0_none
  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
  | Cond0_none => select0 ty (Ccomp0 Cne) e1 e2 (Eop (Ocmp cond) args)
  | Cond0_some cond0 ec => select0 ty cond0 e1 e2 ec
  | Cond0_true => e1
  | Cond0_false => e2
  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).


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).


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

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.



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

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.



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.



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.


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.



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

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.



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.



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.



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 mask start fld nmask prev, or_cases ((Eop (Oandimm mask) ((Eop (Oshlimm start) (fld:::Enil)):::Enil))) ((Eop (Oandimm nmask) (prev:::Enil)))
  | or_case9: 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 mask) ((Eop (Oshlimm start) (fld:::Enil)):::Enil)), (Eop (Oandimm nmask) (prev:::Enil)) => or_case8 mask start fld nmask prev
  | (Eop (Oandimm nmask) (prev:::Enil)), (Eop (Oandimm mask) (fld:::Enil)) => or_case9 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 mask start fld nmask prev =>
      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_case9 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 let zstart := 0 in let zstop := int_highest_bit nmask in if is_bitfield zstop zstart then let mask' := Int.repr (zbitfield_mask zstop zstart) in if and_dec (Int.eq_dec nmask mask') (Int.eq_dec mask (Int.not mask')) then Eop (Oinsf zstop zstart) (fld:::prev:::Enil) else Eop Oor (e1:::e2:::Enil) else Eop Oor (e1:::e2:::Enil) else Eop Oor (e1:::e2:::Enil)
  | or_default e1 e2 =>
      Eop Oor (e1:::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.



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

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

Require FPDivision32 FPDivision64.

Definition divs_base (e1: expr) (e2: expr) :=
  if Compopts.inline_fp_div32 tt
  then FPDivision32.fp_divs32 e1 e2
  else Eexternal i32_sdiv sig_ii_i (e1 ::: e2 ::: Enil).
  
Definition mods_base (e1: expr) (e2: expr) :=
  if Compopts.inline_fp_div32 tt
  then FPDivision32.fp_mods32 e1 e2
  else Eexternal i32_smod sig_ii_i (e1 ::: e2 ::: Enil).

Definition divu_base (e1: expr) (e2: expr) :=
  if Compopts.inline_fp_div32 tt
  then FPDivision32.fp_divu32 e1 e2
  else Eexternal i32_udiv sig_ii_i (e1 ::: e2 ::: Enil).
  
Definition modu_base (e1: expr) (e2: expr) :=
  if Compopts.inline_fp_div32 tt
  then FPDivision32.fp_modu32 e1 e2
  else 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

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.



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.



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

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.



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.



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.


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.


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).


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.



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

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

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).


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.



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.



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 select_abs (e1 : expr) :=
  Eop (Oabsdiffimm Int.zero) (e1 ::: Enil).

Definition select_absl (e1 : expr) :=
  Eop (Oabsdifflimm Int64.zero) (e1 ::: Enil).
  
Definition gen_abs args :=
  match args with
  | e1:::Enil => Some (select_abs e1)
  | _ => None
  end.

Definition gen_absl args :=
  match args with
  | e1:::Enil => Some (select_absl e1)
  | _ => 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
  | BI_lround_ne => Some (Eop Olongoffloat_ne args)
  | BI_luround_ne => Some (Eop Olonguoffloat_ne args)
  | BI_fp_udiv32 => (match args with
                     | a:::b:::Enil => Some (FPDivision32.fp_divu32 a b)
                     | _ => None
                     end)
  | BI_fp_udiv64 => (match args with
                     | a:::b:::Enil => Some (FPDivision64.fp_divu64 a b)
                     | _ => None
                     end)
  | BI_fp_umod32 => (match args with
                     | a:::b:::Enil => Some (FPDivision32.fp_modu32 a b)
                     | _ => None
                     end)
  | BI_fp_umod64 => (match args with
                     | a:::b:::Enil => Some (FPDivision64.fp_modu64 a b)
                     | _ => None
                     end)
  | BI_fp_sdiv32 => (match args with
                     | a:::b:::Enil => Some (FPDivision32.fp_divs32 a b)
                     | _ => None
                     end)
  | BI_fp_sdiv64 => (match args with
                     | a:::b:::Enil => Some (FPDivision64.fp_divs64 a b)
                     | _ => None
                     end)
  | BI_fp_smod32 => (match args with
                     | a:::b:::Enil => Some (FPDivision32.fp_mods32 a b)
                     | _ => None
                     end)
  | BI_fp_smod64 => (match args with
                     | a:::b:::Enil => Some (FPDivision64.fp_mods64 a b)
                     | _ => None
                     end)
  | BI_abs => gen_abs args
  | BI_absl => gen_absl args
  end.
End SELECT.