From c4877832826fa26aea9c236f16bdc2de16c98150 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 15 Jan 2012 08:57:09 +0000 Subject: Added volatile_read_global and volatile_store_global builtins. Finished updating IA32 and ARM ports. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1792 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/SelectOp.vp | 444 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 444 insertions(+) create mode 100644 arm/SelectOp.vp (limited to 'arm/SelectOp.vp') diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp new file mode 100644 index 00000000..432db948 --- /dev/null +++ b/arm/SelectOp.vp @@ -0,0 +1,444 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* 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 Maps. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Memory. +Require Import Globalenvs. +Require Cminor. +Require Import Op. +Require Import CminorSel. + +Open Local Scope cminorsel_scope. + +(** ** Constants **) + +Definition addrsymbol (id: ident) (ofs: int) := + Eop (Oaddrsymbol id ofs) Enil. + +Definition addrstack (ofs: int) := + Eop (Oaddrstack ofs) Enil. + +(** ** Integer logical negation *) + +Nondetfunction notint (e: expr) := + match e with + | Eop (Oshift s) (t1:::Enil) => Eop (Onotshift s) (t1:::Enil) + | Eop Onot (t1:::Enil) => t1 + | Eop (Onotshift s) (t1:::Enil) => Eop (Oshift s) (t1:::Enil) + | _ => Eop Onot (e:::Enil) + end. + +(** ** Boolean negation *) + +Fixpoint notbool (e: expr) {struct e} : expr := + let default := Eop (Ocmp (Ccompuimm Ceq Int.zero)) (e ::: Enil) in + match e with + | Eop (Ointconst n) Enil => + Eop (Ointconst (if Int.eq n Int.zero then Int.one else Int.zero)) Enil + | Eop (Ocmp cond) args => + Eop (Ocmp (negate_condition cond)) args + | Econdition e1 e2 e3 => + Econdition e1 (notbool e2) (notbool e3) + | _ => + default + 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 (Oaddrsymbol s m) Enil => Eop (Oaddrsymbol s (Int.add n m)) Enil + | Eop (Oaddrstack m) Enil => Eop (Oaddrstack (Int.add n m)) Enil + | Eop (Oaddimm m) (t ::: Enil) => Eop (Oaddimm(Int.add n m)) (t ::: Enil) + | _ => Eop (Oaddimm n) (e ::: Enil) + end. + +Nondetfunction add (e1: expr) (e2: expr) := + match e1, e2 with + | Eop (Ointconst n1) Enil, t2 => addimm n1 t2 + | 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), t2 => addimm n1 (Eop Oadd (t1:::t2:::Enil)) + | t1, Eop (Ointconst n2) Enil => addimm n2 t1 + | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil)) + | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oaddshift s) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oaddshift s) (t1:::t2:::Enil) + | _, _ => 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)) + | Eop (Ointconst n1) Enil, t2 => Eop (Orsubimm n1) (t2:::Enil) + | Eop (Oshift s) (t1:::Enil), t2 => Eop (Orsubshift s) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => Eop (Osubshift s) (t1:::t2:::Enil) + | _, _ => Eop Osub (e1:::e2:::Enil) + end. + +Definition negint (e: expr) := Eop (Orsubimm Int.zero) (e ::: Enil). + +(** ** 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 (Oshift (Slsl n1)) (t1:::Enil) => + if Int.ltu (Int.add n n1) Int.iwordsize + then Eop (Oshift (Slsl (mk_shift_amount(Int.add n n1)))) (t1:::Enil) + else Eop (Oshift (Slsl (mk_shift_amount n))) (e1:::Enil) + | _ => Eop (Oshift (Slsl (mk_shift_amount 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 (Oshift (Slsr n1)) (t1:::Enil) => + if Int.ltu (Int.add n n1) Int.iwordsize + then Eop (Oshift (Slsr (mk_shift_amount (Int.add n n1)))) (t1:::Enil) + else Eop (Oshift (Slsr (mk_shift_amount n))) (e1:::Enil) + | _ => Eop (Oshift (Slsr (mk_shift_amount 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 (Oshift (Sasr n1)) (t1:::Enil) => + if Int.ltu (Int.add n n1) Int.iwordsize + then Eop (Oshift (Sasr (mk_shift_amount (Int.add n n1)))) (t1:::Enil) + else Eop (Oshift (Sasr (mk_shift_amount n))) (e1:::Enil) + | _ => Eop (Oshift (Sasr (mk_shift_amount 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 Omul (Eop (Ointconst n1) Enil ::: 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. + +(** ** Bitwise and, or, xor *) + +Nondetfunction andimm (n1: int) (e2: expr) := + if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil 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 (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 (Oshift s) (t1:::Enil), t2 => Eop (Oandshift s) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oandshift s) (t1:::t2:::Enil) + | Eop (Onotshift s) (t1:::Enil), t2 => Eop (Obicshift s) (t2:::t1:::Enil) + | t1, Eop (Onotshift s) (t2:::Enil) => Eop (Obicshift s) (t1:::t2:::Enil) + | Eop Onot (t1:::Enil), t2 => Eop Obic (t2:::t1:::Enil) + | t1, Eop Onot (t2:::Enil) => Eop Obic (t1:::t2:::Enil) + | _, _ => Eop Oand (e1:::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 orimm (n1: int) (e2: expr) := + if Int.eq n1 Int.zero then e2 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. + +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 (Oshift (Slsl n1)) (t1:::Enil), Eop (Oshift (Slsr n2)) (t2:::Enil) => + if Int.eq (Int.add n1 n2) Int.iwordsize + && same_expr_pure t1 t2 + then Eop (Oshift (Sror n2)) (t1:::Enil) + else Eop (Oorshift (Slsr n2)) (e1:::t2:::Enil) + | Eop (Oshift (Slsr n1)) (t1:::Enil), Eop (Oshift (Slsl n2)) (t2:::Enil) => + if Int.eq (Int.add n2 n1) Int.iwordsize + && same_expr_pure t1 t2 + then Eop (Oshift (Sror n1)) (t1:::Enil) + else Eop (Oorshift (Slsl n2)) (e1:::t2:::Enil) + | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oorshift s) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oorshift s) (t1:::t2:::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 (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 (Oshift s) (t1:::Enil), t2 => Eop (Oxorshift s) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oxorshift s) (t1:::t2:::Enil) + | _, _ => Eop Oxor (e1:::e2:::Enil) + end. + +(** ** Integer division and modulus *) + +Definition mod_aux (divop: operation) (e1 e2: expr) := + Elet e1 + (Elet (lift e2) + (Eop Osub (Eletvar 1 ::: + Eop Omul (Eop divop (Eletvar 1 ::: Eletvar 0 ::: Enil) ::: + Eletvar 0 ::: + Enil) ::: + Enil))). + +Definition divs (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil). + +Definition mods := mod_aux Odiv. + +Definition divuimm (e: expr) (n: int) := + match Int.is_power2 n with + | Some l => shruimm e l + | None => Eop Odivu (e ::: Eop (Ointconst n) Enil ::: Enil) + end. + +Nondetfunction divu (e1: expr) (e2: expr) := + match e2 with + | Eop (Ointconst n2) Enil => divuimm e1 n2 + | _ => Eop Odivu (e1:::e2:::Enil) + end. + +Definition moduimm (e: expr) (n: int) := + match Int.is_power2 n with + | Some l => Eop (Oandimm (Int.sub n Int.one)) (e ::: Enil) + | None => mod_aux Odivu e (Eop (Ointconst n) Enil) + end. + +Nondetfunction modu (e1: expr) (e2: expr) := + match e2 with + | Eop (Ointconst n2) Enil => moduimm e1 n2 + | _ => mod_aux Odivu e1 e2 + end. + +(** ** 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 divf (e1 e2: expr) := Eop Odivf (e1 ::: e2 ::: Enil). + +(** ** Comparisons *) + +Nondetfunction comp (c: comparison) (e1: expr) (e2: expr) := + match e1, e2 with + | Eop (Ointconst n1) Enil, t2 => + Eop (Ocmp (Ccompimm (swap_comparison c) n1)) (t2:::Enil) + | t1, Eop (Ointconst n2) Enil => + Eop (Ocmp (Ccompimm c n2)) (t1:::Enil) + | Eop (Oshift s) (t1:::Enil), t2 => + Eop (Ocmp (Ccompshift (swap_comparison c) s)) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => + Eop (Ocmp (Ccompshift c s)) (t1:::t2:::Enil) + | _, _ => + 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 => + Eop (Ocmp (Ccompuimm (swap_comparison c) n1)) (t2:::Enil) + | t1, Eop (Ointconst n2) Enil => + Eop (Ocmp (Ccompuimm c n2)) (t1:::Enil) + | Eop (Oshift s) (t1:::Enil), t2 => + Eop (Ocmp (Ccompushift (swap_comparison c) s)) (t2:::t1:::Enil) + | t1, Eop (Oshift s) (t2:::Enil) => + Eop (Ocmp (Ccompushift c s)) (t1:::t2:::Enil) + | _, _ => + Eop (Ocmp (Ccompu c)) (e1:::e2:::Enil) + end. + +Definition compf (c: comparison) (e1: expr) (e2: expr) := + Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil). + +(** ** Integer conversions *) + +Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e. + +Definition cast8signed (e: expr) := shrimm (shlimm e (Int.repr 24)) (Int.repr 24). + +Definition cast16unsigned (e: expr) := andimm (Int.repr 65535) e. + +Definition cast16signed (e: expr) := shrimm (shlimm e (Int.repr 16)) (Int.repr 16). + +(** ** Floating-point conversions *) + +Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil). +Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). +Definition intuoffloat (e: expr) := Eop Ointuoffloat (e ::: Enil). +Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil). +Definition floatofintu (e: expr) := Eop Ofloatofintu (e ::: Enil). + +(** ** Recognition of addressing modes for load and store operations *) + +(** We do not recognize the [Aindexed2] and [Aindexed2shift] modes + for floating-point accesses, since these are not supported + by the hardware and emulated inefficiently in [Asmgen]. + Likewise, [Aindexed2shift] are not supported for halfword + and signed byte accesses. *) + +Definition can_use_Aindexed2 (chunk: memory_chunk): bool := + match chunk with + | Mint8signed => true + | Mint8unsigned => true + | Mint16signed => true + | Mint16unsigned => true + | Mint32 => true + | Mfloat32 => false + | Mfloat64 => false + end. + +Definition can_use_Aindexed2shift (chunk: memory_chunk): bool := + match chunk with + | Mint8signed => false + | Mint8unsigned => true + | Mint16signed => false + | Mint16unsigned => false + | Mint32 => true + | Mfloat32 => false + | Mfloat64 => false + end. + +Nondetfunction addressing (chunk: memory_chunk) (e: expr) := + match e with + | Eop (Oaddrstack n) Enil => (Ainstack n, Enil) + | Eop (Oaddimm n) (e1:::Enil) => (Aindexed n, e1:::Enil) + | Eop (Oaddshift s) (e1:::e2:::Enil) => + if can_use_Aindexed2shift chunk + then (Aindexed2shift s, e1:::e2:::Enil) + else (Aindexed Int.zero, Eop (Oaddshift s) (e1:::e2:::Enil) ::: Enil) + | Eop Oadd (e1:::e2:::Enil) => + if can_use_Aindexed2 chunk + then (Aindexed2, e1:::e2:::Enil) + else (Aindexed Int.zero, Eop Oadd (e1:::e2:::Enil) ::: Enil) + | _ => (Aindexed Int.zero, e:::Enil) + end. + + -- cgit