diff options
Diffstat (limited to 'ia32/SelectOp.vp')
| -rw-r--r-- | ia32/SelectOp.vp | 530 |
1 files changed, 0 insertions, 530 deletions
diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp deleted file mode 100644 index db546d99..00000000 --- a/ia32/SelectOp.vp +++ /dev/null @@ -1,530 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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. - -Open Local 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. - -(** ** 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 (e: expr) := - match e with - | Eop (Ointconst n) Enil => BA_int n - | Eop (Olongconst n) Enil => BA_long n - | Eop (Olea (Aglobal id ofs)) Enil => if Archi.ptr64 then BA e else BA_addrglobal id ofs - | Eop (Olea (Ainstack ofs)) Enil => if Archi.ptr64 then BA e else BA_addrstack ofs - | Eop (Oleal (Aglobal id ofs)) Enil => if Archi.ptr64 then BA_addrglobal id ofs else BA e - | Eop (Oleal (Ainstack ofs)) Enil => if Archi.ptr64 then BA_addrstack ofs 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. |