SelectOp.vp

(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*                 Xavier Leroy, INRIA Paris                           *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  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 Import Coqlib.
Require Import Compopts.
Require Import AST Integers Floats.
Require Import Op CminorSel.

Local Open Scope cminorsel_scope.

(** ** Constants **)

(** External oracle to determine whether a symbol should be addressed
  through [Oindirectsymbol] or can be addressed via [Oleal Aglobal].
  This is to accommodate MacOS X's limitations on references to data
  symbols imported from shared libraries.  It can also help with PIC
  code under ELF. *)

Parameter symbol_is_external: ident -> bool.

Definition Olea_ptr (a: addressing) := if Archi.ptr64 then Oleal a else Olea a.

Definition addrsymbol (id: ident) (ofs: ptrofs) :=
  if symbol_is_external id then
    if Ptrofs.eq ofs Ptrofs.zero
    then Eop (Oindirectsymbol id) Enil
    else Eop (Olea_ptr (Aindexed (Ptrofs.unsigned ofs))) (Eop (Oindirectsymbol id) Enil ::: Enil)
  else
    Eop (Olea_ptr (Aglobal id ofs)) Enil.

Definition addrstack (ofs: ptrofs) :=
  Eop (Olea_ptr (Ainstack ofs)) Enil.

(** ** Integer logical negation *)

Nondetfunction notint (e: expr) :=
  match e with
  | Eop (Ointconst n) Enil => Eop (Ointconst (Int.not n)) Enil
  | Eop (Oxorimm n) (e1 ::: Enil) => Eop (Oxorimm (Int.not n)) (e1 ::: Enil)
  | _ => Eop Onot (e ::: Enil)
  end.

(** ** Integer addition and pointer addition *)

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 (Olea addr) args   => Eop (Olea (offset_addressing_total addr (Int.signed n))) args
  | _                      => Eop (Olea (Aindexed (Int.signed n))) (e ::: Enil)
  end.

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 (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Aindexed n2)) (t2:::Enil) =>
      Eop (Olea (Aindexed2 (n1 + n2))) (t1:::t2:::Enil)
  | Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Ascaled sc n2)) (t2:::Enil) =>
      Eop (Olea (Aindexed2scaled sc (n1 + n2))) (t1:::t2:::Enil)
  | Eop (Olea (Ascaled sc n1)) (t1:::Enil), Eop (Olea (Aindexed n2)) (t2:::Enil) =>
      Eop (Olea (Aindexed2scaled sc (n1 + n2))) (t2:::t1:::Enil)
  | Eop (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Aglobal id ofs)) Enil =>
      Eop (Olea (Abased id (Ptrofs.add ofs (Ptrofs.repr n1)))) (t1:::Enil)
  | Eop (Olea (Aglobal id ofs)) Enil, Eop (Olea (Aindexed n2)) (t2:::Enil) =>
      Eop (Olea (Abased id (Ptrofs.add ofs (Ptrofs.repr n2)))) (t2:::Enil)
  | Eop (Olea (Ascaled sc n1)) (t1:::Enil), Eop (Olea (Aglobal id ofs)) Enil =>
      Eop (Olea (Abasedscaled sc id (Ptrofs.add ofs (Ptrofs.repr n1)))) (t1:::Enil)
  | Eop (Olea (Aglobal id ofs)) Enil, Eop (Olea (Ascaled sc n2)) (t2:::Enil) =>
      Eop (Olea (Abasedscaled sc id (Ptrofs.add ofs (Ptrofs.repr n2)))) (t2:::Enil)
  | Eop (Olea (Ascaled sc n)) (t1:::Enil), t2 =>
      Eop (Olea (Aindexed2scaled sc n)) (t2:::t1:::Enil)
  | t1, Eop (Olea (Ascaled sc n)) (t2:::Enil) =>
      Eop (Olea (Aindexed2scaled sc n)) (t1:::t2:::Enil)
  | Eop (Olea (Aindexed n)) (t1:::Enil), t2 =>
      Eop (Olea (Aindexed2 n)) (t1:::t2:::Enil)
  | t1, Eop (Olea (Aindexed n)) (t2:::Enil) =>
      Eop (Olea (Aindexed2 n)) (t1:::t2:::Enil)
  | _, _ =>
      Eop (Olea (Aindexed2 0)) (e1:::e2:::Enil)
  end.

(** ** Opposite *)

Nondetfunction negint (e: expr) :=
  match e with
  | Eop (Ointconst n) Enil => Eop (Ointconst (Int.neg n)) Enil
  | _ =>  Eop Oneg (e ::: 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 (Olea (Aindexed n1)) (t1:::Enil), Eop (Olea (Aindexed n2)) (t2:::Enil) =>
      addimm (Int.repr (n1 - n2)) (Eop Osub (t1:::t2:::Enil))
  | Eop (Olea (Aindexed n1)) (t1:::Enil), t2 =>
      addimm (Int.repr n1) (Eop Osub (t1:::t2:::Enil))
  | t1, Eop (Olea (Aindexed n2)) (t2:::Enil) =>
      addimm (Int.repr (-n2)) (Eop Osub (t1:::t2:::Enil))
  | _, _ =>
      Eop Osub (e1:::e2:::Enil)
  end.

(** ** Immediate shifts *)

Definition shift_is_scale (n: int) : bool :=
  Int.eq n (Int.repr 1) || Int.eq n (Int.repr 2) || Int.eq n (Int.repr 3).

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 (Olea (Aindexed n1)) (t1:::Enil) =>
        if shift_is_scale n
        then Eop (Olea (Ascaled (Int.unsigned (Int.shl Int.one n))
                                (Int.unsigned (Int.shl (Int.repr n1) n)))) (t1:::Enil)
        else Eop (Oshlimm n) (e1:::Enil)
    | _ =>
        if shift_is_scale n
        then Eop (Olea (Ascaled (Int.unsigned (Int.shl Int.one n)) 0)) (e1:::Enil)
        else 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 (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 (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 (Olea (Aindexed n2)) (t2:::Enil) => addimm (Int.mul n1 (Int.repr 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) := Eop Omulhs (e1 ::: e2 ::: Enil).
Definition mulhu (e1: expr) (e2: expr) := 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 Ocast8unsigned (t2:::Enil) =>
     Eop (Oandimm (Int.and n1 (Int.repr 255))) (t2:::Enil)
  | Eop Ocast16unsigned (t2:::Enil) =>
     Eop (Oandimm (Int.and n1 (Int.repr 65535))) (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 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 (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 then
        if same_expr_pure t1 t2
        then Eop (Ororimm n2) (t1:::Enil)
        else Eop (Oshldimm n1) (t1:::t2:::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 then
        if same_expr_pure t1 t2
        then Eop (Ororimm n2) (t1:::Enil)
        else Eop (Oshldimm n1) (t1:::t2:::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 match e2 with
  | Eop (Ointconst n2) Enil =>
      Eop (Ointconst (Int.xor n1 n2)) Enil
  | Eop (Oxorimm n2) (t2:::Enil) =>
     Eop (Oxorimm (Int.xor n1 n2)) (t2:::Enil)
  | Eop Onot (t2:::Enil) =>
     Eop (Oxorimm (Int.not n1)) (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 division and modulus *)

Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil).
Definition modu_base (e1: expr) (e2: expr) := Eop Omodu (e1:::e2:::Enil).
Definition divs_base (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
Definition mods_base (e1: expr) (e2: expr) := Eop Omod (e1:::e2:::Enil).

Definition shrximm (e1: expr) (n2: int) :=
  if Int.eq n2 Int.zero then e1 else Eop (Oshrximm n2) (e1:::Enil).

(** ** General shifts *)

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
  | Ceq, Eop (Oandimm n1) (t1 ::: Enil) =>
      if Int.eq_dec n2 Int.zero then
        Eop (Ocmp (Cmaskzero n1)) (t1 ::: Enil)
      else
        Eop (Ocmp (default c n2)) (e1 ::: Enil)
  | Cne, Eop (Oandimm n1) (t1 ::: Enil) =>
      if Int.eq_dec n2 Int.zero then
        Eop (Ocmp (Cmasknotzero n1)) (t1 ::: Enil)
      else
        Eop (Ocmp (default c n2)) (e1 ::: 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 *)

Nondetfunction cast8unsigned (e: expr) :=
  match e with
  | Eop (Ointconst n) Enil =>
      Eop (Ointconst (Int.zero_ext 8 n)) Enil
  | Eop (Oandimm n) (t:::Enil) =>
      andimm (Int.and (Int.repr 255) n) t
  | _ =>
      Eop Ocast8unsigned (e:::Enil)
  end.

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

Nondetfunction cast16unsigned (e: expr) :=
  match e with
  | Eop (Ointconst n) Enil =>
      Eop (Ointconst (Int.zero_ext 16 n)) Enil
  | Eop (Oandimm n) (t:::Enil) =>
      andimm (Int.and (Int.repr 65535) n) t
  | _ =>
      Eop Ocast16unsigned (e:::Enil)
  end.

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 singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil).
Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil).

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

Nondetfunction floatofint (e: expr) :=
  match e with
  | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_int n)) Enil
  | _ => Eop Ofloatofint (e ::: Enil)
  end.

Definition intuoffloat (e: expr) :=
  Elet e
    (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil)
      (Econdition (CEcond (Ccompf Clt) (Eletvar 1 ::: Eletvar 0 ::: Enil))
        (intoffloat (Eletvar 1))
        (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar 1) (Eletvar 0))))))%nat.

Nondetfunction floatofintu (e: expr) :=
  match e with
  | Eop (Ointconst n) Enil => Eop (Ofloatconst (Float.of_intu n)) Enil
  | _ =>
    let f := Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil in
    Elet e
      (Econdition (CEcond (Ccompuimm Clt Float.ox8000_0000) (Eletvar O ::: Enil))
        (floatofint (Eletvar O))
        (addf (floatofint (addimm (Int.neg Float.ox8000_0000) (Eletvar O))) f))
  end.

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

Nondetfunction singleofint (e: expr) :=
  match e with
  | Eop (Ointconst n) Enil => Eop (Osingleconst (Float32.of_int n)) Enil
  | _ => Eop Osingleofint (e ::: Enil)
  end.

Definition intuofsingle (e: expr) := intuoffloat (floatofsingle e).

Nondetfunction singleofintu (e: expr) :=
  match e with
  | Eop (Ointconst n) Enil => Eop (Osingleconst (Float32.of_intu n)) Enil
  | _ => singleoffloat (floatofintu e)
  end.

(** ** Addressing modes *)

Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
  match e with
  | Eop (Olea addr) args =>
      if (negb Archi.ptr64) && addressing_valid addr then (addr, args) else (Aindexed 0, e:::Enil)
  | Eop (Oleal addr) args =>
      if Archi.ptr64 && addressing_valid addr then (addr, args) else (Aindexed 0, e:::Enil)
  | _ => (Aindexed 0, e:::Enil)
  end.

(** ** Arguments of builtins *)

Nondetfunction builtin_arg_addr (addr: Op.addressing) (el: exprlist) :=
  match addr, el with
  | Aindexed n, e1 ::: Enil =>
      BA_addptr (BA e1) (if Archi.ptr64 then BA_long (Int64.repr n) else BA_int (Int.repr n))
  | Aglobal id ofs, Enil => BA_addrglobal id ofs
  | Ainstack ofs, Enil => BA_addrstack ofs
  | _, _ => BA (Eop (Olea_ptr addr) el)
  end.

Nondetfunction builtin_arg (e: expr) :=
  match e with
  | Eop (Ointconst n) Enil => BA_int n
  | Eop (Olongconst n) Enil => BA_long n
  | Eop (Olea addr) el =>
      if Archi.ptr64 then BA e else builtin_arg_addr addr el
  | Eop (Oleal addr) el =>
      if Archi.ptr64 then builtin_arg_addr addr el else BA e
  | 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 (Aglobal id ofs) Enil => BA_loadglobal chunk id ofs
  | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs
  | _ => BA e
  end.