diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-07-13 15:01:51 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-07-13 15:01:51 +0000 |
commit | 48b839d15e69c3c9995ca3c25e6a7c4730224292 (patch) | |
tree | 2394d10bcb90b36617bfd79f32aa5e04492a860a /ia32/SelectOp.vp | |
parent | 926bf226e89e0a4935da8815852af76c8d2b3cdf (diff) | |
download | compcert-48b839d15e69c3c9995ca3c25e6a7c4730224292.tar.gz compcert-48b839d15e69c3c9995ca3c25e6a7c4730224292.zip |
Support for MacOS X's indirect symbols. (first try)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1978 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'ia32/SelectOp.vp')
-rw-r--r-- | ia32/SelectOp.vp | 21 |
1 files changed, 17 insertions, 4 deletions
diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp index 62de4ce1..19e64cc3 100644 --- a/ia32/SelectOp.vp +++ b/ia32/SelectOp.vp @@ -52,8 +52,20 @@ Open Local Scope cminorsel_scope. (** ** Constants **) +(** External oracle to determine whether a symbol is external and must + be addressed through [Oaddrsymbol], or is local and can be addressed + through [Olea Aglobal]. This is to accommodate MacOS X's limitations + on references to data symbols imported from shared libraries. *) + +Parameter symbol_is_external: ident -> bool. + Definition addrsymbol (id: ident) (ofs: int) := - Eop (Olea (Aglobal id ofs)) Enil. + if symbol_is_external id then + if Int.eq ofs Int.zero + then Eop (Oaddrsymbol id) Enil + else Eop (Olea (Aindexed ofs)) (Eop (Oaddrsymbol id) Enil ::: Enil) + else + Eop (Olea (Aglobal id ofs)) Enil. Definition addrstack (ofs: int) := Eop (Olea (Ainstack ofs)) Enil. @@ -410,9 +422,10 @@ Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil). Definition intuoffloat (e: expr) := let f := Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil in Elet e - (Econdition (CEcond (Ccompf Clt) (Eletvar O ::: f ::: Enil)) - (intoffloat (Eletvar O)) - (addimm Float.ox8000_0000 (intoffloat (subf (Eletvar O) f)))). + (Elet (Eop (Ofloatconst (Float.floatofintu 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. Definition floatofintu (e: expr) := let f := Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil in |