From 48b839d15e69c3c9995ca3c25e6a7c4730224292 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 13 Jul 2012 15:01:51 +0000 Subject: 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 --- ia32/SelectOp.vp | 21 +++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) (limited to 'ia32/SelectOp.vp') diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp index 62de4ce..19e64cc 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 -- cgit v1.2.3