Module SelectLong


Instruction selection for 64-bit integer operations

Require Import Coqlib.
Require Import Compopts.
Require Import AST Integers Floats.
Require Import Op CminorSel.
Require Import OpHelpers.
Require Import SelectOp SplitLong.
Require Import ExtValues.
Require Import DecBoolOps.
Require FPExtra.

Local Open Scope cminorsel_scope.
Local Open Scope string_scope.

Section SELECT.

Context {hf: helper_functions}.

Definition longconst (n: int64) : expr :=
  if Archi.splitlong then SplitLong.longconst n else Eop (Olongconst n) Enil.

Definition is_longconst (e: expr) :=
  if Archi.splitlong then SplitLong.is_longconst e else
  match e with
  | Eop (Olongconst n) Enil => Some n
  | _ => None
  end.

Definition intoflong (e: expr) :=
  if Archi.splitlong then SplitLong.intoflong e else
  match is_longconst e with
  | Some n => Eop (Ointconst (Int.repr (Int64.unsigned n))) Enil
  | None => Eop Olowlong (e ::: Enil)
  end.

Definition longofint (e: expr) :=
  if Archi.splitlong then SplitLong.longofint e else
  match is_intconst e with
  | Some n => longconst (Int64.repr (Int.signed n))
  | None => Eop Ocast32signed (e ::: Enil)
  end.

Definition longofintu (e: expr) :=
  if Archi.splitlong then SplitLong.longofintu e else
  match is_intconst e with
  | Some n => longconst (Int64.repr (Int.unsigned n))
  | None => Eop Ocast32unsigned (e ::: Enil)
  end.

Integer addition and pointer addition


Definition addlimm_shllimm sh k2 e1 :=
  if Compopts.optim_addx tt
  then
    match shift1_4_of_z (Int.unsigned sh) with
    | Some s14 => Eop (Oaddxlimm s14 k2) (e1:::Enil)
    | None => Eop (Oaddlimm k2) ((Eop (Oshllimm sh) (e1:::Enil)):::Enil)
    end
  else Eop (Oaddlimm k2) ((Eop (Oshllimm sh) (e1:::Enil)):::Enil).

Original definition: 
Nondetfunction addlimm (n: int64) (e: expr) :=
  if Int64.eq n Int64.zero then e else
  match e with
  | Eop (Olongconst m) Enil => longconst (Int64.add n m)
  | Eop (Oaddrsymbol s m) Enil   =>
    (if Compopts.optim_globaladdroffset tt
     then Eop (Oaddrsymbol s (Ptrofs.add (Ptrofs.of_int64 n) m)) Enil
     else Eop (Oaddlimm n) (e ::: Enil))
  | Eop (Oaddrstack m) Enil      => Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int64 n) m)) Enil
  | Eop (Oaddlimm m) (t ::: Enil) => Eop (Oaddlimm(Int64.add n m)) (t ::: Enil)
  | Eop (Oaddxlimm sh m) (t ::: Enil) => Eop (Oaddxlimm sh (Int64.add n m)) (t ::: Enil)
  | Eop (Oshllimm sh) (t1:::Enil) => addlimm_shllimm sh n t1
  | _ => Eop (Oaddlimm n) (e ::: Enil)
  end.

Inductive addlimm_cases: forall (e: expr), Type :=
  | addlimm_case1: forall m, addlimm_cases (Eop (Olongconst m) Enil)
  | addlimm_case2: forall s m, addlimm_cases (Eop (Oaddrsymbol s m) Enil)
  | addlimm_case3: forall m, addlimm_cases (Eop (Oaddrstack m) Enil)
  | addlimm_case4: forall m t, addlimm_cases (Eop (Oaddlimm m) (t ::: Enil))
  | addlimm_case5: forall sh m t, addlimm_cases (Eop (Oaddxlimm sh m) (t ::: Enil))
  | addlimm_case6: forall sh t1, addlimm_cases (Eop (Oshllimm sh) (t1:::Enil))
  | addlimm_default: forall (e: expr), addlimm_cases e.

Definition addlimm_match (e: expr) :=
  match e as zz1 return addlimm_cases zz1 with
  | Eop (Olongconst m) Enil => addlimm_case1 m
  | Eop (Oaddrsymbol s m) Enil => addlimm_case2 s m
  | Eop (Oaddrstack m) Enil => addlimm_case3 m
  | Eop (Oaddlimm m) (t ::: Enil) => addlimm_case4 m t
  | Eop (Oaddxlimm sh m) (t ::: Enil) => addlimm_case5 sh m t
  | Eop (Oshllimm sh) (t1:::Enil) => addlimm_case6 sh t1
  | e => addlimm_default e
  end.

Definition addlimm (n: int64) (e: expr) :=
 if Int64.eq n Int64.zero then e else match addlimm_match e with
  | addlimm_case1 m =>
      longconst (Int64.add n m)
  | addlimm_case2 s m =>
      (if Compopts.optim_globaladdroffset tt then Eop (Oaddrsymbol s (Ptrofs.add (Ptrofs.of_int64 n) m)) Enil else Eop (Oaddlimm n) (e ::: Enil))
  | addlimm_case3 m =>
      Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int64 n) m)) Enil
  | addlimm_case4 m t =>
      Eop (Oaddlimm(Int64.add n m)) (t ::: Enil)
  | addlimm_case5 sh m t =>
      Eop (Oaddxlimm sh (Int64.add n m)) (t ::: Enil)
  | addlimm_case6 sh t1 =>
      addlimm_shllimm sh n t1
  | addlimm_default e =>
      Eop (Oaddlimm n) (e ::: Enil)
  end.


Definition addl_shllimm n e1 e2 :=
  if Compopts.optim_addx tt
  then
    match shift1_4_of_z (Int.unsigned n) with
    | Some s14 => Eop (Oaddxl s14) (e1:::e2:::Enil)
    | None => Eop Oaddl (e2:::(Eop (Oshllimm n) (e1:::Enil)):::Enil)
    end
  else Eop Oaddl (e2:::(Eop (Oshllimm n) (e1:::Enil)):::Enil).

Original definition: 
Nondetfunction addl (e1: expr) (e2: expr) :=
  if Archi.splitlong then SplitLong.addl e1 e2 else
  match e1, e2 with
  | Eop (Olongconst n1) Enil, t2 => addlimm n1 t2
  | t1, Eop (Olongconst n2) Enil => addlimm n2 t1
  | Eop (Oaddlimm n1) (t1:::Enil), Eop (Oaddlimm n2) (t2:::Enil) =>
      addlimm (Int64.add n1 n2) (Eop Oaddl (t1:::t2:::Enil))
  | Eop (Oaddlimm n1) (t1:::Enil), Eop (Oaddrstack n2) Enil =>
      Eop Oaddl (Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int64 n1) n2)) Enil ::: t1 ::: Enil)
  | Eop (Oaddrstack n1) Enil, Eop (Oaddlimm n2) (t2:::Enil) =>
      Eop Oaddl (Eop (Oaddrstack (Ptrofs.add n1 (Ptrofs.of_int64 n2))) Enil ::: t2 ::: Enil)
  | Eop (Oaddlimm n1) (t1:::Enil), t2 =>
      addlimm n1 (Eop Oaddl (t1:::t2:::Enil))
  | t1, Eop (Oaddlimm n2) (t2:::Enil) =>
      addlimm n2 (Eop Oaddl (t1:::t2:::Enil))
  | t1, (Eop Omull (t2:::t3:::Enil)) =>
      Eop Omaddl (t1:::t2:::t3:::Enil)
  | (Eop Omull (t2:::t3:::Enil)), t1 =>
      Eop Omaddl (t1:::t2:::t3:::Enil)
  | t1, (Eop (Omullimm n) (t2:::Enil)) =>
      Eop (Omaddlimm n) (t1:::t2:::Enil)
  | (Eop (Omullimm n) (t2:::Enil)), t1 =>
      Eop (Omaddlimm n) (t1:::t2:::Enil)
  | (Eop (Oshllimm n) (t1:::Enil)), t2 =>
    addl_shllimm n t1 t2
  | t2, (Eop (Oshllimm n) (t1:::Enil)) =>
    addl_shllimm n t1 t2
  | _, _ => Eop Oaddl (e1:::e2:::Enil)
  end.

Inductive addl_cases: forall (e1: expr) (e2: expr), Type :=
  | addl_case1: forall n1 t2, addl_cases (Eop (Olongconst n1) Enil) (t2)
  | addl_case2: forall t1 n2, addl_cases (t1) (Eop (Olongconst n2) Enil)
  | addl_case3: forall n1 t1 n2 t2, addl_cases (Eop (Oaddlimm n1) (t1:::Enil)) (Eop (Oaddlimm n2) (t2:::Enil))
  | addl_case4: forall n1 t1 n2, addl_cases (Eop (Oaddlimm n1) (t1:::Enil)) (Eop (Oaddrstack n2) Enil)
  | addl_case5: forall n1 n2 t2, addl_cases (Eop (Oaddrstack n1) Enil) (Eop (Oaddlimm n2) (t2:::Enil))
  | addl_case6: forall n1 t1 t2, addl_cases (Eop (Oaddlimm n1) (t1:::Enil)) (t2)
  | addl_case7: forall t1 n2 t2, addl_cases (t1) (Eop (Oaddlimm n2) (t2:::Enil))
  | addl_case8: forall t1 t2 t3, addl_cases (t1) ((Eop Omull (t2:::t3:::Enil)))
  | addl_case9: forall t2 t3 t1, addl_cases ((Eop Omull (t2:::t3:::Enil))) (t1)
  | addl_case10: forall t1 n t2, addl_cases (t1) ((Eop (Omullimm n) (t2:::Enil)))
  | addl_case11: forall n t2 t1, addl_cases ((Eop (Omullimm n) (t2:::Enil))) (t1)
  | addl_case12: forall n t1 t2, addl_cases ((Eop (Oshllimm n) (t1:::Enil))) (t2)
  | addl_case13: forall t2 n t1, addl_cases (t2) ((Eop (Oshllimm n) (t1:::Enil)))
  | addl_default: forall (e1: expr) (e2: expr), addl_cases e1 e2.

Definition addl_match (e1: expr) (e2: expr) :=
  match e1 as zz1, e2 as zz2 return addl_cases zz1 zz2 with
  | Eop (Olongconst n1) Enil, t2 => addl_case1 n1 t2
  | t1, Eop (Olongconst n2) Enil => addl_case2 t1 n2
  | Eop (Oaddlimm n1) (t1:::Enil), Eop (Oaddlimm n2) (t2:::Enil) => addl_case3 n1 t1 n2 t2
  | Eop (Oaddlimm n1) (t1:::Enil), Eop (Oaddrstack n2) Enil => addl_case4 n1 t1 n2
  | Eop (Oaddrstack n1) Enil, Eop (Oaddlimm n2) (t2:::Enil) => addl_case5 n1 n2 t2
  | Eop (Oaddlimm n1) (t1:::Enil), t2 => addl_case6 n1 t1 t2
  | t1, Eop (Oaddlimm n2) (t2:::Enil) => addl_case7 t1 n2 t2
  | t1, (Eop Omull (t2:::t3:::Enil)) => addl_case8 t1 t2 t3
  | (Eop Omull (t2:::t3:::Enil)), t1 => addl_case9 t2 t3 t1
  | t1, (Eop (Omullimm n) (t2:::Enil)) => addl_case10 t1 n t2
  | (Eop (Omullimm n) (t2:::Enil)), t1 => addl_case11 n t2 t1
  | (Eop (Oshllimm n) (t1:::Enil)), t2 => addl_case12 n t1 t2
  | t2, (Eop (Oshllimm n) (t1:::Enil)) => addl_case13 t2 n t1
  | e1, e2 => addl_default e1 e2
  end.

Definition addl (e1: expr) (e2: expr) :=
 if Archi.splitlong then SplitLong.addl e1 e2 else match addl_match e1 e2 with
  | addl_case1 n1 t2 =>
      addlimm n1 t2
  | addl_case2 t1 n2 =>
      addlimm n2 t1
  | addl_case3 n1 t1 n2 t2 =>
      addlimm (Int64.add n1 n2) (Eop Oaddl (t1:::t2:::Enil))
  | addl_case4 n1 t1 n2 =>
      Eop Oaddl (Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int64 n1) n2)) Enil ::: t1 ::: Enil)
  | addl_case5 n1 n2 t2 =>
      Eop Oaddl (Eop (Oaddrstack (Ptrofs.add n1 (Ptrofs.of_int64 n2))) Enil ::: t2 ::: Enil)
  | addl_case6 n1 t1 t2 =>
      addlimm n1 (Eop Oaddl (t1:::t2:::Enil))
  | addl_case7 t1 n2 t2 =>
      addlimm n2 (Eop Oaddl (t1:::t2:::Enil))
  | addl_case8 t1 t2 t3 =>
      Eop Omaddl (t1:::t2:::t3:::Enil)
  | addl_case9 t2 t3 t1 =>
      Eop Omaddl (t1:::t2:::t3:::Enil)
  | addl_case10 t1 n t2 =>
      Eop (Omaddlimm n) (t1:::t2:::Enil)
  | addl_case11 n t2 t1 =>
      Eop (Omaddlimm n) (t1:::t2:::Enil)
  | addl_case12 n t1 t2 =>
      addl_shllimm n t1 t2
  | addl_case13 t2 n t1 =>
      addl_shllimm n t1 t2
  | addl_default e1 e2 =>
      Eop Oaddl (e1:::e2:::Enil)
  end.


Integer and pointer subtraction


Original definition: 
Nondetfunction subl (e1: expr) (e2: expr) :=
  if Archi.splitlong then SplitLong.subl e1 e2 else
  match e1, e2 with
  | t1, Eop (Olongconst n2) Enil =>
      addlimm (Int64.neg n2) t1
  | Eop (Oaddlimm n1) (t1:::Enil), Eop (Oaddlimm n2) (t2:::Enil) =>
      addlimm (Int64.sub n1 n2) (Eop Osubl (t1:::t2:::Enil))
  | Eop (Oaddlimm n1) (t1:::Enil), t2 =>
      addlimm n1 (Eop Osubl (t1:::t2:::Enil))
  | t1, Eop (Oaddlimm n2) (t2:::Enil) =>
      addlimm (Int64.neg n2) (Eop Osubl (t1:::t2:::Enil))
  | t1, (Eop Omull (t2:::t3:::Enil)) =>
      Eop Omsubl (t1:::t2:::t3:::Enil)
  | t1, (Eop (Omullimm n) (t2:::Enil)) =>
      Eop (Omaddlimm (Int64.neg n)) (t1:::t2:::Enil)
  | _, _ => Eop Osubl (e1:::e2:::Enil)
  end.

Inductive subl_cases: forall (e1: expr) (e2: expr), Type :=
  | subl_case1: forall t1 n2, subl_cases (t1) (Eop (Olongconst n2) Enil)
  | subl_case2: forall n1 t1 n2 t2, subl_cases (Eop (Oaddlimm n1) (t1:::Enil)) (Eop (Oaddlimm n2) (t2:::Enil))
  | subl_case3: forall n1 t1 t2, subl_cases (Eop (Oaddlimm n1) (t1:::Enil)) (t2)
  | subl_case4: forall t1 n2 t2, subl_cases (t1) (Eop (Oaddlimm n2) (t2:::Enil))
  | subl_case5: forall t1 t2 t3, subl_cases (t1) ((Eop Omull (t2:::t3:::Enil)))
  | subl_case6: forall t1 n t2, subl_cases (t1) ((Eop (Omullimm n) (t2:::Enil)))
  | subl_default: forall (e1: expr) (e2: expr), subl_cases e1 e2.

Definition subl_match (e1: expr) (e2: expr) :=
  match e1 as zz1, e2 as zz2 return subl_cases zz1 zz2 with
  | t1, Eop (Olongconst n2) Enil => subl_case1 t1 n2
  | Eop (Oaddlimm n1) (t1:::Enil), Eop (Oaddlimm n2) (t2:::Enil) => subl_case2 n1 t1 n2 t2
  | Eop (Oaddlimm n1) (t1:::Enil), t2 => subl_case3 n1 t1 t2
  | t1, Eop (Oaddlimm n2) (t2:::Enil) => subl_case4 t1 n2 t2
  | t1, (Eop Omull (t2:::t3:::Enil)) => subl_case5 t1 t2 t3
  | t1, (Eop (Omullimm n) (t2:::Enil)) => subl_case6 t1 n t2
  | e1, e2 => subl_default e1 e2
  end.

Definition subl (e1: expr) (e2: expr) :=
 if Archi.splitlong then SplitLong.subl e1 e2 else match subl_match e1 e2 with
  | subl_case1 t1 n2 =>
      addlimm (Int64.neg n2) t1
  | subl_case2 n1 t1 n2 t2 =>
      addlimm (Int64.sub n1 n2) (Eop Osubl (t1:::t2:::Enil))
  | subl_case3 n1 t1 t2 =>
      addlimm n1 (Eop Osubl (t1:::t2:::Enil))
  | subl_case4 t1 n2 t2 =>
      addlimm (Int64.neg n2) (Eop Osubl (t1:::t2:::Enil))
  | subl_case5 t1 t2 t3 =>
      Eop Omsubl (t1:::t2:::t3:::Enil)
  | subl_case6 t1 n t2 =>
      Eop (Omaddlimm (Int64.neg n)) (t1:::t2:::Enil)
  | subl_default e1 e2 =>
      Eop Osubl (e1:::e2:::Enil)
  end.


Definition negl (e: expr) :=
  if Archi.splitlong then SplitLong.negl e else
  match is_longconst e with
  | Some n => longconst (Int64.neg n)
  | None => Eop Onegl (e ::: Enil)
  end.

Immediate shifts


Original definition: 
Nondetfunction shllimm (e1: expr) (n: int) :=
  if Archi.splitlong then SplitLong.shllimm e1 n else
  if Int.eq n Int.zero then
    e1
  else if negb (Int.ltu n Int64.iwordsize') then
    Eop Oshll (e1 ::: Eop (Ointconst n) Enil ::: Enil)
  else match e1 with
    | Eop (Olongconst n1) Enil =>
        longconst (Int64.shl' n1 n)
    | Eop (Oshllimm n1) (t1:::Enil) =>
        if Int.ltu (Int.add n n1) Int64.iwordsize'
        then Eop (Oshllimm (Int.add n n1)) (t1:::Enil)
        else Eop (Oshllimm n) (e1:::Enil)
    | _ =>
        Eop (Oshllimm n) (e1:::Enil)
  end.

Inductive shllimm_cases: forall (e1: expr) , Type :=
  | shllimm_case1: forall n1, shllimm_cases (Eop (Olongconst n1) Enil)
  | shllimm_case2: forall n1 t1, shllimm_cases (Eop (Oshllimm n1) (t1:::Enil))
  | shllimm_default: forall (e1: expr) , shllimm_cases e1.

Definition shllimm_match (e1: expr) :=
  match e1 as zz1 return shllimm_cases zz1 with
  | Eop (Olongconst n1) Enil => shllimm_case1 n1
  | Eop (Oshllimm n1) (t1:::Enil) => shllimm_case2 n1 t1
  | e1 => shllimm_default e1
  end.

Definition shllimm (e1: expr) (n: int) :=
 if Archi.splitlong then SplitLong.shllimm e1 n else if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int64.iwordsize') then Eop Oshll (e1 ::: Eop (Ointconst n) Enil ::: Enil) else match shllimm_match e1 with
  | shllimm_case1 n1 =>
      longconst (Int64.shl' n1 n)
  | shllimm_case2 n1 t1 =>
      if Int.ltu (Int.add n n1) Int64.iwordsize' then Eop (Oshllimm (Int.add n n1)) (t1:::Enil) else Eop (Oshllimm n) (e1:::Enil)
  | shllimm_default e1 =>
      Eop (Oshllimm n) (e1:::Enil)
  end.


Original definition: 
Nondetfunction shrluimm (e1: expr) (n: int) :=
  if Archi.splitlong then SplitLong.shrluimm e1 n else
  if Int.eq n Int.zero then e1 else
  if negb (Int.ltu n Int64.iwordsize') then
    Eop Oshrlu (e1:::Eop (Ointconst n) Enil:::Enil)
  else
    match e1 with
    | Eop (Olongconst n1) Enil =>
        longconst (Int64.shru' n1 n)
    | Eop (Oshrluimm n1) (t1:::Enil) =>
        if Int.ltu (Int.add n n1) Int64.iwordsize'
        then Eop (Oshrluimm (Int.add n n1)) (t1:::Enil)
        else Eop (Oshrluimm n) (e1:::Enil)
    | Eop (Oshllimm n1) (t1:::Enil) =>
        let stop := Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one) in
	let start := Z.sub (Z.add (Z.add (Int.unsigned n) stop) Z.one) Int64.zwordsize in
	if is_bitfieldl stop start
        then Eop (Oextfzl stop start) (t1:::Enil)
	else Eop (Oshrluimm n) (e1:::Enil)
    | _ =>
        Eop (Oshrluimm n) (e1:::Enil)
    end.

Inductive shrluimm_cases: forall (e1: expr) , Type :=
  | shrluimm_case1: forall n1, shrluimm_cases (Eop (Olongconst n1) Enil)
  | shrluimm_case2: forall n1 t1, shrluimm_cases (Eop (Oshrluimm n1) (t1:::Enil))
  | shrluimm_case3: forall n1 t1, shrluimm_cases (Eop (Oshllimm n1) (t1:::Enil))
  | shrluimm_default: forall (e1: expr) , shrluimm_cases e1.

Definition shrluimm_match (e1: expr) :=
  match e1 as zz1 return shrluimm_cases zz1 with
  | Eop (Olongconst n1) Enil => shrluimm_case1 n1
  | Eop (Oshrluimm n1) (t1:::Enil) => shrluimm_case2 n1 t1
  | Eop (Oshllimm n1) (t1:::Enil) => shrluimm_case3 n1 t1
  | e1 => shrluimm_default e1
  end.

Definition shrluimm (e1: expr) (n: int) :=
 if Archi.splitlong then SplitLong.shrluimm e1 n else if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int64.iwordsize') then Eop Oshrlu (e1:::Eop (Ointconst n) Enil:::Enil) else match shrluimm_match e1 with
  | shrluimm_case1 n1 =>
      longconst (Int64.shru' n1 n)
  | shrluimm_case2 n1 t1 =>
      if Int.ltu (Int.add n n1) Int64.iwordsize' then Eop (Oshrluimm (Int.add n n1)) (t1:::Enil) else Eop (Oshrluimm n) (e1:::Enil)
  | shrluimm_case3 n1 t1 =>
      let stop := Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one) in let start := Z.sub (Z.add (Z.add (Int.unsigned n) stop) Z.one) Int64.zwordsize in if is_bitfieldl stop start then Eop (Oextfzl stop start) (t1:::Enil) else Eop (Oshrluimm n) (e1:::Enil)
  | shrluimm_default e1 =>
      Eop (Oshrluimm n) (e1:::Enil)
  end.


Original definition: 
Nondetfunction shrlimm (e1: expr) (n: int) :=
  if Archi.splitlong then SplitLong.shrlimm e1 n else
  if Int.eq n Int.zero then e1 else
  if negb (Int.ltu n Int64.iwordsize') then
    Eop Oshrl (e1:::Eop (Ointconst n) Enil:::Enil)
  else
  match e1 with
  | Eop (Olongconst n1) Enil =>
      longconst (Int64.shr' n1 n)
  | Eop (Oshrlimm n1) (t1:::Enil) =>
      if Int.ltu (Int.add n n1) Int64.iwordsize'
      then Eop (Oshrlimm (Int.add n n1)) (t1:::Enil)
      else Eop (Oshrlimm n) (e1:::Enil)
  | Eop (Oshllimm n1) (t1:::Enil) =>
        let stop := Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one) in
	let start := Z.sub (Z.add (Z.add (Int.unsigned n) stop) Z.one) Int64.zwordsize in
	if is_bitfieldl stop start
        then Eop (Oextfsl stop start) (t1:::Enil)
	else Eop (Oshrlimm n) (e1:::Enil)
  | _ =>
      Eop (Oshrlimm n) (e1:::Enil)
  end.

Inductive shrlimm_cases: forall (e1: expr) , Type :=
  | shrlimm_case1: forall n1, shrlimm_cases (Eop (Olongconst n1) Enil)
  | shrlimm_case2: forall n1 t1, shrlimm_cases (Eop (Oshrlimm n1) (t1:::Enil))
  | shrlimm_case3: forall n1 t1, shrlimm_cases (Eop (Oshllimm n1) (t1:::Enil))
  | shrlimm_default: forall (e1: expr) , shrlimm_cases e1.

Definition shrlimm_match (e1: expr) :=
  match e1 as zz1 return shrlimm_cases zz1 with
  | Eop (Olongconst n1) Enil => shrlimm_case1 n1
  | Eop (Oshrlimm n1) (t1:::Enil) => shrlimm_case2 n1 t1
  | Eop (Oshllimm n1) (t1:::Enil) => shrlimm_case3 n1 t1
  | e1 => shrlimm_default e1
  end.

Definition shrlimm (e1: expr) (n: int) :=
 if Archi.splitlong then SplitLong.shrlimm e1 n else if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int64.iwordsize') then Eop Oshrl (e1:::Eop (Ointconst n) Enil:::Enil) else match shrlimm_match e1 with
  | shrlimm_case1 n1 =>
      longconst (Int64.shr' n1 n)
  | shrlimm_case2 n1 t1 =>
      if Int.ltu (Int.add n n1) Int64.iwordsize' then Eop (Oshrlimm (Int.add n n1)) (t1:::Enil) else Eop (Oshrlimm n) (e1:::Enil)
  | shrlimm_case3 n1 t1 =>
      let stop := Z.sub Int64.zwordsize (Z.add (Int.unsigned n1) Z.one) in let start := Z.sub (Z.add (Z.add (Int.unsigned n) stop) Z.one) Int64.zwordsize in if is_bitfieldl stop start then Eop (Oextfsl stop start) (t1:::Enil) else Eop (Oshrlimm n) (e1:::Enil)
  | shrlimm_default e1 =>
      Eop (Oshrlimm n) (e1:::Enil)
  end.


General shifts


Definition shll (e1: expr) (e2: expr) :=
  if Archi.splitlong then SplitLong.shll e1 e2 else
  match is_intconst e2 with
  | Some n2 => shllimm e1 n2
  | None => Eop Oshll (e1:::e2:::Enil)
  end.

Definition shrl (e1: expr) (e2: expr) :=
  if Archi.splitlong then SplitLong.shrl e1 e2 else
  match is_intconst e2 with
  | Some n2 => shrlimm e1 n2
  | None => Eop Oshrl (e1:::e2:::Enil)
  end.

Definition shrlu (e1: expr) (e2: expr) :=
  if Archi.splitlong then SplitLong.shrlu e1 e2 else
  match is_intconst e2 with
  | Some n2 => shrluimm e1 n2
  | _ => Eop Oshrlu (e1:::e2:::Enil)
  end.

Integer multiply


Definition mullimm_base (n1: int64) (e2: expr) :=
  match Int64.one_bits' n1 with
  | i :: nil =>
      shllimm e2 i
  | i :: j :: nil =>
      Elet e2 (addl (shllimm (Eletvar 0) i) (shllimm (Eletvar 0) j))
  | _ =>
      Eop (Omullimm n1) (e2 ::: Enil)
  end.

Original definition: 
Nondetfunction mullimm (n1: int64) (e2: expr) :=
  if Archi.splitlong then SplitLong.mullimm n1 e2
  else if Int64.eq n1 Int64.zero then longconst Int64.zero
  else if Int64.eq n1 Int64.one then e2
  else match e2 with
  | Eop (Olongconst n2) Enil => longconst (Int64.mul n1 n2)
  | Eop (Oaddlimm n2) (t2:::Enil) => addlimm (Int64.mul n1 n2) (mullimm_base n1 t2)
  | _ => mullimm_base n1 e2
  end.

Inductive mullimm_cases: forall (e2: expr), Type :=
  | mullimm_case1: forall n2, mullimm_cases (Eop (Olongconst n2) Enil)
  | mullimm_case2: forall n2 t2, mullimm_cases (Eop (Oaddlimm n2) (t2:::Enil))
  | mullimm_default: forall (e2: expr), mullimm_cases e2.

Definition mullimm_match (e2: expr) :=
  match e2 as zz1 return mullimm_cases zz1 with
  | Eop (Olongconst n2) Enil => mullimm_case1 n2
  | Eop (Oaddlimm n2) (t2:::Enil) => mullimm_case2 n2 t2
  | e2 => mullimm_default e2
  end.

Definition mullimm (n1: int64) (e2: expr) :=
 if Archi.splitlong then SplitLong.mullimm n1 e2 else if Int64.eq n1 Int64.zero then longconst Int64.zero else if Int64.eq n1 Int64.one then e2 else match mullimm_match e2 with
  | mullimm_case1 n2 =>
      longconst (Int64.mul n1 n2)
  | mullimm_case2 n2 t2 =>
      addlimm (Int64.mul n1 n2) (mullimm_base n1 t2)
  | mullimm_default e2 =>
      mullimm_base n1 e2
  end.


Original definition: 
Nondetfunction mull (e1: expr) (e2: expr) :=
  if Archi.splitlong then SplitLong.mull e1 e2 else
  match e1, e2 with
  | Eop (Olongconst n1) Enil, t2 => mullimm n1 t2
  | t1, Eop (Olongconst n2) Enil => mullimm n2 t1
  | _, _ => Eop Omull (e1:::e2:::Enil)
  end.

Inductive mull_cases: forall (e1: expr) (e2: expr), Type :=
  | mull_case1: forall n1 t2, mull_cases (Eop (Olongconst n1) Enil) (t2)
  | mull_case2: forall t1 n2, mull_cases (t1) (Eop (Olongconst n2) Enil)
  | mull_default: forall (e1: expr) (e2: expr), mull_cases e1 e2.

Definition mull_match (e1: expr) (e2: expr) :=
  match e1 as zz1, e2 as zz2 return mull_cases zz1 zz2 with
  | Eop (Olongconst n1) Enil, t2 => mull_case1 n1 t2
  | t1, Eop (Olongconst n2) Enil => mull_case2 t1 n2
  | e1, e2 => mull_default e1 e2
  end.

Definition mull (e1: expr) (e2: expr) :=
 if Archi.splitlong then SplitLong.mull e1 e2 else match mull_match e1 e2 with
  | mull_case1 n1 t2 =>
      mullimm n1 t2
  | mull_case2 t1 n2 =>
      mullimm n2 t1
  | mull_default e1 e2 =>
      Eop Omull (e1:::e2:::Enil)
  end.


Definition mullhu (e1: expr) (n2: int64) :=
  if Archi.splitlong then SplitLong.mullhu e1 n2 else
  Eop Omullhu (e1 ::: longconst n2 ::: Enil).

Definition mullhs (e1: expr) (n2: int64) :=
  if Archi.splitlong then SplitLong.mullhs e1 n2 else
  Eop Omullhs (e1 ::: longconst n2 ::: Enil).

Bitwise and, or, xor


Original definition: 
Nondetfunction andlimm (n1: int64) (e2: expr) := 
  if Int64.eq n1 Int64.zero then longconst Int64.zero else
  if Int64.eq n1 Int64.mone then e2 else
  match e2 with
  | Eop (Olongconst n2) Enil =>
      longconst (Int64.and n1 n2)
  | Eop (Oandlimm n2) (t2:::Enil) =>
      Eop (Oandlimm (Int64.and n1 n2)) (t2:::Enil)
  | Eop Onotl (t2:::Enil) => Eop (Oandnlimm n1) (t2:::Enil)
  | _ =>
      Eop (Oandlimm n1) (e2:::Enil)
  end.

Inductive andlimm_cases: forall (e2: expr), Type :=
  | andlimm_case1: forall n2, andlimm_cases (Eop (Olongconst n2) Enil)
  | andlimm_case2: forall n2 t2, andlimm_cases (Eop (Oandlimm n2) (t2:::Enil))
  | andlimm_case3: forall t2, andlimm_cases (Eop Onotl (t2:::Enil))
  | andlimm_default: forall (e2: expr), andlimm_cases e2.

Definition andlimm_match (e2: expr) :=
  match e2 as zz1 return andlimm_cases zz1 with
  | Eop (Olongconst n2) Enil => andlimm_case1 n2
  | Eop (Oandlimm n2) (t2:::Enil) => andlimm_case2 n2 t2
  | Eop Onotl (t2:::Enil) => andlimm_case3 t2
  | e2 => andlimm_default e2
  end.

Definition andlimm (n1: int64) (e2: expr) :=
 if Int64.eq n1 Int64.zero then longconst Int64.zero else if Int64.eq n1 Int64.mone then e2 else match andlimm_match e2 with
  | andlimm_case1 n2 =>
      longconst (Int64.and n1 n2)
  | andlimm_case2 n2 t2 =>
      Eop (Oandlimm (Int64.and n1 n2)) (t2:::Enil)
  | andlimm_case3 t2 =>
      Eop (Oandnlimm n1) (t2:::Enil)
  | andlimm_default e2 =>
      Eop (Oandlimm n1) (e2:::Enil)
  end.


Original definition: 
Nondetfunction andl (e1: expr) (e2: expr) :=
  if Archi.splitlong then SplitLong.andl e1 e2 else
  match e1, e2 with
  | Eop (Olongconst n1) Enil, t2 => andlimm n1 t2
  | t1, Eop (Olongconst n2) Enil => andlimm n2 t1
  | (Eop Onotl (t1:::Enil)), t2 => Eop Oandnl (t1:::t2:::Enil) 
  | t1, (Eop Onotl (t2:::Enil)) => Eop Oandnl (t2:::t1:::Enil)
  | _, _ => Eop Oandl (e1:::e2:::Enil)
  end.

Inductive andl_cases: forall (e1: expr) (e2: expr), Type :=
  | andl_case1: forall n1 t2, andl_cases (Eop (Olongconst n1) Enil) (t2)
  | andl_case2: forall t1 n2, andl_cases (t1) (Eop (Olongconst n2) Enil)
  | andl_case3: forall t1 t2, andl_cases ((Eop Onotl (t1:::Enil))) (t2)
  | andl_case4: forall t1 t2, andl_cases (t1) ((Eop Onotl (t2:::Enil)))
  | andl_default: forall (e1: expr) (e2: expr), andl_cases e1 e2.

Definition andl_match (e1: expr) (e2: expr) :=
  match e1 as zz1, e2 as zz2 return andl_cases zz1 zz2 with
  | Eop (Olongconst n1) Enil, t2 => andl_case1 n1 t2
  | t1, Eop (Olongconst n2) Enil => andl_case2 t1 n2
  | (Eop Onotl (t1:::Enil)), t2 => andl_case3 t1 t2
  | t1, (Eop Onotl (t2:::Enil)) => andl_case4 t1 t2
  | e1, e2 => andl_default e1 e2
  end.

Definition andl (e1: expr) (e2: expr) :=
 if Archi.splitlong then SplitLong.andl e1 e2 else match andl_match e1 e2 with
  | andl_case1 n1 t2 =>
      andlimm n1 t2
  | andl_case2 t1 n2 =>
      andlimm n2 t1
  | andl_case3 t1 t2 =>
      Eop Oandnl (t1:::t2:::Enil)
  | andl_case4 t1 t2 =>
      Eop Oandnl (t2:::t1:::Enil)
  | andl_default e1 e2 =>
      Eop Oandl (e1:::e2:::Enil)
  end.


Original definition: 
Nondetfunction orlimm (n1: int64) (e2: expr) :=
  if Int64.eq n1 Int64.zero then e2 else
  if Int64.eq n1 Int64.mone then longconst Int64.mone else
  match e2 with
  | Eop (Olongconst n2) Enil => longconst (Int64.or n1 n2)
  | Eop (Oorlimm n2) (t2:::Enil) => Eop (Oorlimm (Int64.or n1 n2)) (t2:::Enil)
  | Eop Onotl (t2:::Enil) => Eop (Oornlimm n1) (t2:::Enil)
  | _ => Eop (Oorlimm n1) (e2:::Enil)
  end.

Inductive orlimm_cases: forall (e2: expr), Type :=
  | orlimm_case1: forall n2, orlimm_cases (Eop (Olongconst n2) Enil)
  | orlimm_case2: forall n2 t2, orlimm_cases (Eop (Oorlimm n2) (t2:::Enil))
  | orlimm_case3: forall t2, orlimm_cases (Eop Onotl (t2:::Enil))
  | orlimm_default: forall (e2: expr), orlimm_cases e2.

Definition orlimm_match (e2: expr) :=
  match e2 as zz1 return orlimm_cases zz1 with
  | Eop (Olongconst n2) Enil => orlimm_case1 n2
  | Eop (Oorlimm n2) (t2:::Enil) => orlimm_case2 n2 t2
  | Eop Onotl (t2:::Enil) => orlimm_case3 t2
  | e2 => orlimm_default e2
  end.

Definition orlimm (n1: int64) (e2: expr) :=
 if Int64.eq n1 Int64.zero then e2 else if Int64.eq n1 Int64.mone then longconst Int64.mone else match orlimm_match e2 with
  | orlimm_case1 n2 =>
      longconst (Int64.or n1 n2)
  | orlimm_case2 n2 t2 =>
      Eop (Oorlimm (Int64.or n1 n2)) (t2:::Enil)
  | orlimm_case3 t2 =>
      Eop (Oornlimm n1) (t2:::Enil)
  | orlimm_default e2 =>
      Eop (Oorlimm n1) (e2:::Enil)
  end.


Original definition: 
Nondetfunction orl (e1: expr) (e2: expr) :=
  if Archi.splitlong then SplitLong.orl e1 e2 else
  match e1, e2 with
  | Eop (Olongconst n1) Enil, t2 => orlimm n1 t2
  | t1, Eop (Olongconst n2) Enil => orlimm n2 t1
  | (Eop Onotl (t1:::Enil)), t2 => Eop Oornl (t1:::t2:::Enil) 
  | t1, (Eop Onotl (t2:::Enil))  => Eop Oornl (t2:::t1:::Enil)
  | (Eop (Oandlimm nmask) (prev:::Enil)),
    (Eop (Oandlimm mask)
      ((Eop (Oshllimm start) (fld:::Enil)):::Enil)) =>
      let zstart := Int.unsigned start in
      let zstop := int64_highest_bit mask in
      if is_bitfieldl zstop zstart
      then
        let mask' := Int64.repr (zbitfield_mask zstop zstart) in
          if and_dec (Int64.eq_dec mask mask')
                     (Int64.eq_dec nmask (Int64.not mask'))
          then Eop (Oinsfl zstop zstart) (prev:::fld:::Enil)
          else Eop Oorl (e1:::e2:::Enil)
      else Eop Oorl (e1:::e2:::Enil)
  | (Eop (Oandlimm nmask) (prev:::Enil)),
    (Eop (Oandlimm mask) (fld:::Enil)) =>
      let zstart := 0 in
      let zstop := int64_highest_bit mask in
      if is_bitfieldl zstop zstart
      then
        let mask' := Int64.repr (zbitfield_mask zstop zstart) in
          if and_dec (Int64.eq_dec mask mask')
                     (Int64.eq_dec nmask (Int64.not mask'))
          then Eop (Oinsfl zstop zstart) (prev:::fld:::Enil)
          else Eop Oorl (e1:::e2:::Enil)
      else Eop Oorl (e1:::e2:::Enil)
  | _, _ => Eop Oorl (e1:::e2:::Enil)
  end.

Inductive orl_cases: forall (e1: expr) (e2: expr), Type :=
  | orl_case1: forall n1 t2, orl_cases (Eop (Olongconst n1) Enil) (t2)
  | orl_case2: forall t1 n2, orl_cases (t1) (Eop (Olongconst n2) Enil)
  | orl_case3: forall t1 t2, orl_cases ((Eop Onotl (t1:::Enil))) (t2)
  | orl_case4: forall t1 t2, orl_cases (t1) ((Eop Onotl (t2:::Enil)))
  | orl_case5: forall nmask prev mask start fld, orl_cases ((Eop (Oandlimm nmask) (prev:::Enil))) ((Eop (Oandlimm mask) ((Eop (Oshllimm start) (fld:::Enil)):::Enil)))
  | orl_case6: forall nmask prev mask fld, orl_cases ((Eop (Oandlimm nmask) (prev:::Enil))) ((Eop (Oandlimm mask) (fld:::Enil)))
  | orl_default: forall (e1: expr) (e2: expr), orl_cases e1 e2.

Definition orl_match (e1: expr) (e2: expr) :=
  match e1 as zz1, e2 as zz2 return orl_cases zz1 zz2 with
  | Eop (Olongconst n1) Enil, t2 => orl_case1 n1 t2
  | t1, Eop (Olongconst n2) Enil => orl_case2 t1 n2
  | (Eop Onotl (t1:::Enil)), t2 => orl_case3 t1 t2
  | t1, (Eop Onotl (t2:::Enil)) => orl_case4 t1 t2
  | (Eop (Oandlimm nmask) (prev:::Enil)), (Eop (Oandlimm mask) ((Eop (Oshllimm start) (fld:::Enil)):::Enil)) => orl_case5 nmask prev mask start fld
  | (Eop (Oandlimm nmask) (prev:::Enil)), (Eop (Oandlimm mask) (fld:::Enil)) => orl_case6 nmask prev mask fld
  | e1, e2 => orl_default e1 e2
  end.

Definition orl (e1: expr) (e2: expr) :=
 if Archi.splitlong then SplitLong.orl e1 e2 else match orl_match e1 e2 with
  | orl_case1 n1 t2 =>
      orlimm n1 t2
  | orl_case2 t1 n2 =>
      orlimm n2 t1
  | orl_case3 t1 t2 =>
      Eop Oornl (t1:::t2:::Enil)
  | orl_case4 t1 t2 =>
      Eop Oornl (t2:::t1:::Enil)
  | orl_case5 nmask prev mask start fld =>
      let zstart := Int.unsigned start in let zstop := int64_highest_bit mask in if is_bitfieldl zstop zstart then let mask' := Int64.repr (zbitfield_mask zstop zstart) in if and_dec (Int64.eq_dec mask mask') (Int64.eq_dec nmask (Int64.not mask')) then Eop (Oinsfl zstop zstart) (prev:::fld:::Enil) else Eop Oorl (e1:::e2:::Enil) else Eop Oorl (e1:::e2:::Enil)
  | orl_case6 nmask prev mask fld =>
      let zstart := 0 in let zstop := int64_highest_bit mask in if is_bitfieldl zstop zstart then let mask' := Int64.repr (zbitfield_mask zstop zstart) in if and_dec (Int64.eq_dec mask mask') (Int64.eq_dec nmask (Int64.not mask')) then Eop (Oinsfl zstop zstart) (prev:::fld:::Enil) else Eop Oorl (e1:::e2:::Enil) else Eop Oorl (e1:::e2:::Enil)
  | orl_default e1 e2 =>
      Eop Oorl (e1:::e2:::Enil)
  end.


Original definition: 
Nondetfunction xorlimm (n1: int64) (e2: expr) :=
  if Int64.eq n1 Int64.zero then e2 else
  if Int64.eq n1 Int64.mone
  then Eop Onotl (e2:::Enil)
  else
  match e2 with
  | Eop (Olongconst n2) Enil => longconst (Int64.xor n1 n2)
  | Eop (Oxorlimm n2) (t2:::Enil) =>
      let n := Int64.xor n1 n2 in
      if Int64.eq n Int64.zero then t2 else Eop (Oxorlimm n) (t2:::Enil)
  | _ => Eop (Oxorlimm n1) (e2:::Enil)
  end.

Inductive xorlimm_cases: forall (e2: expr), Type :=
  | xorlimm_case1: forall n2, xorlimm_cases (Eop (Olongconst n2) Enil)
  | xorlimm_case2: forall n2 t2, xorlimm_cases (Eop (Oxorlimm n2) (t2:::Enil))
  | xorlimm_default: forall (e2: expr), xorlimm_cases e2.

Definition xorlimm_match (e2: expr) :=
  match e2 as zz1 return xorlimm_cases zz1 with
  | Eop (Olongconst n2) Enil => xorlimm_case1 n2
  | Eop (Oxorlimm n2) (t2:::Enil) => xorlimm_case2 n2 t2
  | e2 => xorlimm_default e2
  end.

Definition xorlimm (n1: int64) (e2: expr) :=
 if Int64.eq n1 Int64.zero then e2 else if Int64.eq n1 Int64.mone then Eop Onotl (e2:::Enil) else match xorlimm_match e2 with
  | xorlimm_case1 n2 =>
      longconst (Int64.xor n1 n2)
  | xorlimm_case2 n2 t2 =>
      let n := Int64.xor n1 n2 in if Int64.eq n Int64.zero then t2 else Eop (Oxorlimm n) (t2:::Enil)
  | xorlimm_default e2 =>
      Eop (Oxorlimm n1) (e2:::Enil)
  end.


Original definition: 
Nondetfunction xorl (e1: expr) (e2: expr) :=
  if Archi.splitlong then SplitLong.xorl e1 e2 else
  match e1, e2 with
  | Eop (Olongconst n1) Enil, t2 => xorlimm n1 t2
  | t1, Eop (Olongconst n2) Enil => xorlimm n2 t1
  | _, _ => Eop Oxorl (e1:::e2:::Enil)
  end.

Inductive xorl_cases: forall (e1: expr) (e2: expr), Type :=
  | xorl_case1: forall n1 t2, xorl_cases (Eop (Olongconst n1) Enil) (t2)
  | xorl_case2: forall t1 n2, xorl_cases (t1) (Eop (Olongconst n2) Enil)
  | xorl_default: forall (e1: expr) (e2: expr), xorl_cases e1 e2.

Definition xorl_match (e1: expr) (e2: expr) :=
  match e1 as zz1, e2 as zz2 return xorl_cases zz1 zz2 with
  | Eop (Olongconst n1) Enil, t2 => xorl_case1 n1 t2
  | t1, Eop (Olongconst n2) Enil => xorl_case2 t1 n2
  | e1, e2 => xorl_default e1 e2
  end.

Definition xorl (e1: expr) (e2: expr) :=
 if Archi.splitlong then SplitLong.xorl e1 e2 else match xorl_match e1 e2 with
  | xorl_case1 n1 t2 =>
      xorlimm n1 t2
  | xorl_case2 t1 n2 =>
      xorlimm n2 t1
  | xorl_default e1 e2 =>
      Eop Oxorl (e1:::e2:::Enil)
  end.


Integer logical negation


Original definition: 
Nondetfunction notl (e: expr) :=
  match e with
  | Eop Oandl (e1:::e2:::Enil) => Eop Onandl (e1:::e2:::Enil)
  | Eop (Oandlimm n) (e1:::Enil) => Eop (Onandlimm n) (e1:::Enil)
  | Eop Oorl (e1:::e2:::Enil) => Eop Onorl (e1:::e2:::Enil)
  | Eop (Oorlimm n) (e1:::Enil) => Eop (Onorlimm n) (e1:::Enil)
  | Eop Oxorl (e1:::e2:::Enil) => Eop Onxorl (e1:::e2:::Enil)
  | Eop (Oxorlimm n) (e1:::Enil) => Eop (Onxorlimm n) (e1:::Enil)
  | Eop Onandl (e1:::e2:::Enil) => Eop Oandl (e1:::e2:::Enil)
  | Eop (Onandlimm n) (e1:::Enil) => Eop (Oandlimm n) (e1:::Enil)
  | Eop Onorl (e1:::e2:::Enil) => Eop Oorl (e1:::e2:::Enil)
  | Eop (Onorlimm n) (e1:::Enil) => Eop (Oorlimm n) (e1:::Enil)
  | Eop Onxorl (e1:::e2:::Enil) => Eop Oxorl (e1:::e2:::Enil)
  | Eop (Onxorlimm n) (e1:::Enil) => Eop (Oxorlimm n) (e1:::Enil)
  | Eop Oandnl (e1:::e2:::Enil) => Eop Oornl (e2:::e1:::Enil)
  | Eop (Oandnlimm n) (e1:::Enil) => Eop (Oorlimm (Int64.not n)) (e1:::Enil)
  | Eop Oornl (e1:::e2:::Enil) => Eop Oandnl (e2:::e1:::Enil)
  | Eop (Oornlimm n) (e1:::Enil) => Eop (Oandlimm (Int64.not n)) (e1:::Enil)
  | Eop Onotl (e1:::Enil) => e1
  | Eop (Olongconst k) Enil => Eop (Olongconst (Int64.not k)) Enil
  | _ => Eop Onotl (e:::Enil) 
  end.

Inductive notl_cases: forall (e: expr), Type :=
  | notl_case1: forall e1 e2, notl_cases (Eop Oandl (e1:::e2:::Enil))
  | notl_case2: forall n e1, notl_cases (Eop (Oandlimm n) (e1:::Enil))
  | notl_case3: forall e1 e2, notl_cases (Eop Oorl (e1:::e2:::Enil))
  | notl_case4: forall n e1, notl_cases (Eop (Oorlimm n) (e1:::Enil))
  | notl_case5: forall e1 e2, notl_cases (Eop Oxorl (e1:::e2:::Enil))
  | notl_case6: forall n e1, notl_cases (Eop (Oxorlimm n) (e1:::Enil))
  | notl_case7: forall e1 e2, notl_cases (Eop Onandl (e1:::e2:::Enil))
  | notl_case8: forall n e1, notl_cases (Eop (Onandlimm n) (e1:::Enil))
  | notl_case9: forall e1 e2, notl_cases (Eop Onorl (e1:::e2:::Enil))
  | notl_case10: forall n e1, notl_cases (Eop (Onorlimm n) (e1:::Enil))
  | notl_case11: forall e1 e2, notl_cases (Eop Onxorl (e1:::e2:::Enil))
  | notl_case12: forall n e1, notl_cases (Eop (Onxorlimm n) (e1:::Enil))
  | notl_case13: forall e1 e2, notl_cases (Eop Oandnl (e1:::e2:::Enil))
  | notl_case14: forall n e1, notl_cases (Eop (Oandnlimm n) (e1:::Enil))
  | notl_case15: forall e1 e2, notl_cases (Eop Oornl (e1:::e2:::Enil))
  | notl_case16: forall n e1, notl_cases (Eop (Oornlimm n) (e1:::Enil))
  | notl_case17: forall e1, notl_cases (Eop Onotl (e1:::Enil))
  | notl_case18: forall k, notl_cases (Eop (Olongconst k) Enil)
  | notl_default: forall (e: expr), notl_cases e.

Definition notl_match (e: expr) :=
  match e as zz1 return notl_cases zz1 with
  | Eop Oandl (e1:::e2:::Enil) => notl_case1 e1 e2
  | Eop (Oandlimm n) (e1:::Enil) => notl_case2 n e1
  | Eop Oorl (e1:::e2:::Enil) => notl_case3 e1 e2
  | Eop (Oorlimm n) (e1:::Enil) => notl_case4 n e1
  | Eop Oxorl (e1:::e2:::Enil) => notl_case5 e1 e2
  | Eop (Oxorlimm n) (e1:::Enil) => notl_case6 n e1
  | Eop Onandl (e1:::e2:::Enil) => notl_case7 e1 e2
  | Eop (Onandlimm n) (e1:::Enil) => notl_case8 n e1
  | Eop Onorl (e1:::e2:::Enil) => notl_case9 e1 e2
  | Eop (Onorlimm n) (e1:::Enil) => notl_case10 n e1
  | Eop Onxorl (e1:::e2:::Enil) => notl_case11 e1 e2
  | Eop (Onxorlimm n) (e1:::Enil) => notl_case12 n e1
  | Eop Oandnl (e1:::e2:::Enil) => notl_case13 e1 e2
  | Eop (Oandnlimm n) (e1:::Enil) => notl_case14 n e1
  | Eop Oornl (e1:::e2:::Enil) => notl_case15 e1 e2
  | Eop (Oornlimm n) (e1:::Enil) => notl_case16 n e1
  | Eop Onotl (e1:::Enil) => notl_case17 e1
  | Eop (Olongconst k) Enil => notl_case18 k
  | e => notl_default e
  end.

Definition notl (e: expr) :=
  match notl_match e with
  | notl_case1 e1 e2 =>
      Eop Onandl (e1:::e2:::Enil)
  | notl_case2 n e1 =>
      Eop (Onandlimm n) (e1:::Enil)
  | notl_case3 e1 e2 =>
      Eop Onorl (e1:::e2:::Enil)
  | notl_case4 n e1 =>
      Eop (Onorlimm n) (e1:::Enil)
  | notl_case5 e1 e2 =>
      Eop Onxorl (e1:::e2:::Enil)
  | notl_case6 n e1 =>
      Eop (Onxorlimm n) (e1:::Enil)
  | notl_case7 e1 e2 =>
      Eop Oandl (e1:::e2:::Enil)
  | notl_case8 n e1 =>
      Eop (Oandlimm n) (e1:::Enil)
  | notl_case9 e1 e2 =>
      Eop Oorl (e1:::e2:::Enil)
  | notl_case10 n e1 =>
      Eop (Oorlimm n) (e1:::Enil)
  | notl_case11 e1 e2 =>
      Eop Oxorl (e1:::e2:::Enil)
  | notl_case12 n e1 =>
      Eop (Oxorlimm n) (e1:::Enil)
  | notl_case13 e1 e2 =>
      Eop Oornl (e2:::e1:::Enil)
  | notl_case14 n e1 =>
      Eop (Oorlimm (Int64.not n)) (e1:::Enil)
  | notl_case15 e1 e2 =>
      Eop Oandnl (e2:::e1:::Enil)
  | notl_case16 n e1 =>
      Eop (Oandlimm (Int64.not n)) (e1:::Enil)
  | notl_case17 e1 =>
      e1
  | notl_case18 k =>
      Eop (Olongconst (Int64.not k)) Enil
  | notl_default e =>
      Eop Onotl (e:::Enil)
  end.


Integer division and modulus


Require FPDivision64.

Definition divls_base (e1: expr) (e2: expr) :=
  if Compopts.inline_fp_div64 tt
  then FPDivision64.fp_divs64 e1 e2
  else SplitLong.divls_base e1 e2.
  
Definition modls_base (e1: expr) (e2: expr) :=
  if Compopts.inline_fp_div64 tt
  then FPDivision64.fp_mods64 e1 e2
  else SplitLong.modls_base e1 e2.

Definition divlu_base (e1: expr) (e2: expr) :=
  if Compopts.inline_fp_div64 tt
  then FPDivision64.fp_divu64 e1 e2
  else SplitLong.divlu_base e1 e2.
  
Definition modlu_base (e1: expr) (e2: expr) :=
  if Compopts.inline_fp_div64 tt
  then FPDivision64.fp_modu64 e1 e2
  else SplitLong.modlu_base e1 e2.

Definition shrxlimm (e: expr) (n: int) :=
  if Archi.splitlong then SplitLong.shrxlimm e n else
  if Int.eq n Int.zero then e else Eop (Oshrxlimm n) (e ::: Enil).

Comparisons


Definition cmplu (c: comparison) (e1 e2: expr) :=
  if Archi.splitlong then SplitLong.cmplu c e1 e2 else
  match is_longconst e1, is_longconst e2 with
  | Some n1, Some n2 =>
      Eop (Ointconst (if Int64.cmpu c n1 n2 then Int.one else Int.zero)) Enil
  | Some n1, None => Eop (Ocmp (Ccompluimm (swap_comparison c) n1)) (e2:::Enil)
  | None, Some n2 => Eop (Ocmp (Ccompluimm c n2)) (e1:::Enil)
  | None, None => Eop (Ocmp (Ccomplu c)) (e1:::e2:::Enil)
  end.

Definition cmpl (c: comparison) (e1 e2: expr) :=
  if Archi.splitlong then SplitLong.cmpl c e1 e2 else
  match is_longconst e1, is_longconst e2 with
  | Some n1, Some n2 =>
      Eop (Ointconst (if Int64.cmp c n1 n2 then Int.one else Int.zero)) Enil
  | Some n1, None => Eop (Ocmp (Ccomplimm (swap_comparison c) n1)) (e2:::Enil)
  | None, Some n2 => Eop (Ocmp (Ccomplimm c n2)) (e1:::Enil)
  | None, None => Eop (Ocmp (Ccompl c)) (e1:::e2:::Enil)
  end.

Floating-point conversions


Definition longoffloat (e: expr) :=
  Eop Olongoffloat (e:::Enil).

Definition longuoffloat (e: expr) :=
  Eop Olonguoffloat (e:::Enil).

Definition floatoflong (e: expr) :=
  Eop Ofloatoflong (e:::Enil).

Definition floatoflongu (e: expr) :=
  Eop Ofloatoflongu (e:::Enil).

Definition longofsingle (e: expr) := longoffloat (floatofsingle e).

Definition longuofsingle (e: expr) := longuoffloat (floatofsingle e).

Definition use_inlined_fp_conversions := true.
Opaque use_inlined_fp_conversions.

Definition singleoflong (e: expr) :=
  if use_inlined_fp_conversions
  then FPExtra.e_single_of_long e
  else SplitLong.singleoflong e.

Definition singleoflongu (e: expr) :=
  if use_inlined_fp_conversions
  then FPExtra.e_single_of_longu e
  else SplitLong.singleoflongu e.

End SELECT.

Generated by coq2html