From b4a08d0815342b6238d307864f0823d0f07bb691 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 26 May 2020 22:04:20 +0200 Subject: k1c -> kvx changes --- kvx/SelectOp.vp | 715 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 715 insertions(+) create mode 100644 kvx/SelectOp.vp (limited to 'kvx/SelectOp.vp') 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: *) -- cgit