k1c -> kvx changes

1 files changed, 715 insertions, 0 deletions

diff --git a/kvx/SelectOp.vp b/kvx/SelectOp.vp
new file mode 100644
index 00000000..9e5d45a0
--- /dev/null
+++ b/kvx/SelectOp.vp
@@ -0,0 +1,715 @@
+(* *************************************************************)
+(*                                                             *)
+(*             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}.
+
+Nondetfunction cond_to_condition0 (cond : condition) (args : exprlist) :=
+  match cond, args with
+  | (Ccompimm c x), (e1 ::: Enil) =>
+    if Int.eq_dec x Int.zero
+    then Some ((Ccomp0 c), e1)
+    else None
+           
+  | (Ccompuimm c x), (e1 ::: Enil) =>
+    if Int.eq_dec x Int.zero
+    then Some ((Ccompu0 c), e1)
+    else None
+
+  | (Ccomplimm c x), (e1 ::: Enil) =>
+    if Int64.eq_dec x Int64.zero
+    then Some ((Ccompl0 c), e1)
+    else None
+           
+  | (Ccompluimm c x), (e1 ::: Enil) =>
+    if Int64.eq_dec x Int64.zero
+    then Some ((Ccomplu0 c), e1)
+    else None
+           
+  | _, _ => None
+  end.
+  
+(** 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 select (ty : typ) (cond : condition) (args : exprlist) (e1 e2: expr)  : option expr :=
+  Some(
+  match cond_to_condition0 cond args with
+  | None => select0 ty (Ccomp0 Cne) e1 e2 (Eop (Ocmp cond) args)
+  | Some(cond0, ec) => select0 ty cond0 e1 e2 ec
+  end).
+
+				      
+(** ** Constants **)
+
+Definition addrsymbol (id: ident) (ofs: ptrofs) :=
+  Eop (Oaddrsymbol id ofs) Enil.
+
+Definition addrstack (ofs: ptrofs) :=
+  Eop (Oaddrstack ofs) Enil.
+
+(** ** Integer addition and pointer addition *)
+
+Definition addimm_shlimm sh k2 e1 :=
+  if Compopts.optim_addx tt
+  then
+    match shift1_4_of_z (Int.unsigned sh) with
+    | Some s14 => Eop (Oaddximm s14 k2) (e1:::Enil)
+    | None => Eop (Oaddimm k2) ((Eop (Oshlimm sh) (e1:::Enil)):::Enil)
+    end
+  else Eop (Oaddimm k2) ((Eop (Oshlimm sh) (e1:::Enil)):::Enil).
+
+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.
+
+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.
+
+Nondetfunction or (e1: expr) (e2: expr) :=
+  match e1, e2 with
+  | Eop (Ointconst n1) Enil, t2 => orimm n1 t2
+  | t1, Eop (Ointconst n2) Enil => orimm n2 t1
+  | Eop (Oshlimm n1) (t1:::Enil), Eop (Oshruimm n2) (t2:::Enil) =>
+      if Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2
+      then Eop (Ororimm n2) (t1:::Enil)
+      else Eop Oor (e1:::e2:::Enil)
+  | Eop (Oshruimm n2) (t2:::Enil), Eop (Oshlimm n1) (t1:::Enil) =>
+      if Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2
+      then Eop (Ororimm n2) (t1:::Enil)
+      else Eop Oor (e1:::e2:::Enil)
+  | (Eop Onot (t1:::Enil)), t2 => Eop Oorn (t1:::t2:::Enil) 
+  | t1, (Eop Onot (t2:::Enil))  => Eop Oorn (t2:::t1:::Enil)
+  | (Eop (Oandimm nmask) (prev:::Enil)),
+    (Eop (Oandimm mask)
+      ((Eop (Oshlimm start) (fld:::Enil)):::Enil)) =>
+      let zstart := Int.unsigned start in
+      let zstop := int_highest_bit mask in
+      if is_bitfield zstop zstart
+      then
+        let mask' := Int.repr (zbitfield_mask zstop zstart) in
+          if and_dec (Int.eq_dec mask mask')
+                     (Int.eq_dec nmask (Int.not mask'))
+          then Eop (Oinsf zstop zstart) (prev:::fld:::Enil)
+          else Eop Oor (e1:::e2:::Enil)
+      else Eop Oor (e1:::e2:::Enil)
+  | (Eop (Oandimm nmask) (prev:::Enil)),
+    (Eop (Oandimm mask) (fld:::Enil)) =>
+      let zstart := 0 in
+      let zstop := int_highest_bit mask in
+      if is_bitfield zstop zstart
+      then
+        let mask' := Int.repr (zbitfield_mask zstop zstart) in
+          if and_dec (Int.eq_dec mask mask')
+                     (Int.eq_dec nmask (Int.not mask'))
+          then Eop (Oinsf zstop zstart) (prev:::fld:::Enil)
+          else Eop Oor (e1:::e2:::Enil)
+      else Eop Oor (e1:::e2:::Enil)
+  | _, _ => Eop Oor (e1:::e2:::Enil)
+  end.
+
+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 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_fabsf => Some (Eop Oabsfs args)
+  | BI_fma => gen_fma args
+  | BI_fmaf => gen_fmaf args
+  end.
+End SELECT.
+
+(* Local Variables: *)
+(* mode: coq *)
+(* End: *)