(* *************************************************************)
(*                                                             *)
(*             The Compcert verified compiler                  *)
(*                                                             *)
(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
(*           Xavier Leroy       INRIA Paris-Rocquencourt       *)
(*           David Monniaux     CNRS, VERIMAG                  *)
(*           Cyril Six          Kalray                         *)
(*                                                             *)
(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
(*  This file is distributed under the terms of the INRIA      *)
(*  Non-Commercial License Agreement.                          *)
(*                                                             *)
(* *************************************************************)


(** Instruction selection for operators *)

(** The instruction selection pass recognizes opportunities for using
  combined arithmetic and logical operations and addressing modes
  offered by the target processor.  For instance, the expression [x + 1]
  can take advantage of the "immediate add" instruction of the processor,
  and on the PowerPC, the expression [(x >> 6) & 0xFF] can be turned
  into a "rotate and mask" instruction.

  This file defines functions for building CminorSel expressions and
  statements, especially expressions consisting of operator
  applications.  These functions examine their arguments to choose
  cheaper forms of operators whenever possible.

  For instance, [add e1 e2] will return a CminorSel expression semantically
  equivalent to [Eop Oadd (e1 ::: e2 ::: Enil)], but will use a
  [Oaddimm] operator if one of the arguments is an integer constant,
  or suppress the addition altogether if one of the arguments is the
  null integer.  In passing, we perform operator reassociation
  ([(e + c1) * c2] becomes [(e * c2) + (c1 * c2)]) and a small amount
  of constant propagation.

  On top of the "smart constructor" functions defined below,
  module [Selection] implements the actual instruction selection pass.
*)

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

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 Cond0_some (Ccomp0 c) e1
    else Cond0_none
           
  | (Ccompuimm c x), (e1 ::: Enil) =>
    if Int.eq_dec x Int.zero
    then compu0 c e1
    else Cond0_none

  | (Ccomplimm c x), (e1 ::: Enil) =>
    if Int64.eq_dec x Int64.zero
    then Cond0_some (Ccompl0 c) e1
    else Cond0_none
           
  | (Ccompluimm c x), (e1 ::: Enil) =>
    if Int64.eq_dec x Int64.zero
    then complu0 c e1
    else Cond0_none
           
  | _, _ => Cond0_none
  end.
  
(** Ternary operator *)
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.

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

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.

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

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.

(** ** Integer and pointer subtraction *)

Nondetfunction sub (e1: expr) (e2: expr) :=
  match e1, e2 with
  | t1, Eop (Ointconst n2) Enil =>
      addimm (Int.neg n2) t1
  | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) =>
      addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil))
  | Eop (Oaddimm n1) (t1:::Enil), t2 =>
      addimm n1 (Eop Osub (t1:::t2:::Enil))
  | t1, Eop (Oaddimm n2) (t2:::Enil) =>
      addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil))
  | 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.

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

(** ** Immediate shifts *)

Nondetfunction shlimm (e1: expr) (n: int) :=
  if Int.eq n Int.zero then
    e1
  else if negb (Int.ltu n Int.iwordsize) then
    Eop Oshl (e1 ::: Eop (Ointconst n) Enil ::: Enil)
  else match e1 with
    | Eop (Ointconst n1) Enil =>
        Eop (Ointconst (Int.shl n1 n)) Enil
    | Eop (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.

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.

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.

(** ** 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.

Nondetfunction mulimm (n1: int) (e2: expr) :=
  if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil
  else if Int.eq n1 Int.one then e2
  else match e2 with
  | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.mul n1 n2)) Enil
  | Eop (Oaddimm n2) (t2:::Enil) => addimm (Int.mul n1 n2) (mulimm_base n1 t2)
  | _ => mulimm_base n1 e2
  end.

Nondetfunction mul (e1: expr) (e2: expr) :=
  match e1, e2 with
  | Eop (Ointconst n1) Enil, t2 => mulimm n1 t2
  | t1, Eop (Ointconst n2) Enil => mulimm n2 t1
  | _, _ => Eop Omul (e1:::e2:::Enil)
  end.

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

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.

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.

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.

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 mask)
         ((Eop (Oshlimm start) (fld:::Enil)):::Enil)),
    (Eop (Oandimm nmask) (prev:::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 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)
  | _, _ => Eop Oor (e1:::e2:::Enil)
  end.

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.

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.

(** ** Integer logical negation *)

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.

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

(* Alternate definition, not convenient for strength reduction during constant propagation *)
(*
(* n2 will be less than 31. *)

Definition shrximm_inner (e1: expr) (n2: int) :=
  Eop (Oshruimm (Int.sub Int.iwordsize n2))
      ((Eop (Oshrimm (Int.repr (Int.zwordsize - 1)))
            (e1 ::: Enil))
         ::: Enil).

Definition shrximm (e1: expr) (n2: int) :=
  if Int.eq n2 Int.zero then e1
  else Eop (Oshrimm n2)
           ((Eop Oadd (e1 ::: shrximm_inner e1 n2 ::: Enil))
              ::: Enil).
*)

(** ** General shifts *)

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

Nondetfunction shr (e1: expr) (e2: expr) :=
  match e2 with
  | Eop (Ointconst n2) Enil => shrimm e1 n2
  | _ => Eop Oshr (e1:::e2:::Enil)
  end.

Nondetfunction shru (e1: expr) (e2: expr) :=
  match e2 with
  | Eop (Ointconst n2) Enil => shruimm e1 n2
  | _ => Eop Oshru (e1:::e2:::Enil)
  end.

(** ** Floating-point arithmetic *)

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

Definition 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 *)

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.

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.

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.

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.

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

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

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

(** ** Floating-point conversions *)

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

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.

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.

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

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.

(** ** Arguments of builtins *)

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.

(* float division *)

Definition divf_base (e1: expr) (e2: expr) :=
  (* Eop Odivf (e1 ::: e2 ::: Enil). *)
  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) :=
  (* Eop Odivf (e1 ::: e2 ::: Enil). *)
  Eexternal f32_div sig_ss_s (e1 ::: e2 ::: Enil).

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.

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.

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.

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.

Require FPDivision32 FPDivision64.

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.

(* Local Variables: *)
(* mode: coq *)
(* End: *)