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

1 files changed, 6 insertions, 1 deletions

diff --git a/ia32/Op.v b/ia32/Op.v
index 9fdafe1..a5568c7 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -69,6 +69,7 @@ Inductive operation : Type :=
   | Omove: operation                    (**r [rd = r1] *)
   | Ointconst: int -> operation         (**r [rd] is set to the given integer constant *)
   | Ofloatconst: float -> operation     (**r [rd] is set to the given float constant *)
+  | Oaddrsymbol: ident -> operation     (**r [rd] is set to the address of the symbol *)
 (*c Integer arithmetic: *)
   | Ocast8signed: operation             (**r [rd] is 8-bit sign extension of [r1] *)
   | Ocast8unsigned: operation           (**r [rd] is 8-bit zero extension of [r1] *)
@@ -113,7 +114,6 @@ Inductive operation : Type :=
 
 (** Derived operators. *)
 
-Definition Oaddrsymbol (id: ident) (ofs: int) : operation := Olea (Aglobal id ofs).
 Definition Oaddrstack (ofs: int) : operation := Olea (Ainstack ofs).
 Definition Oaddimm (n: int) : operation := Olea (Aindexed n).
 
@@ -193,6 +193,7 @@ Definition eval_operation
   | Omove, v1::nil => Some v1
   | Ointconst n, nil => Some (Vint n)
   | Ofloatconst n, nil => Some (Vfloat n)
+  | Oaddrsymbol id, nil => Some (symbol_address genv id Int.zero)
   | Ocast8signed, v1 :: nil => Some (Val.sign_ext 8 v1)
   | Ocast8unsigned, v1 :: nil => Some (Val.zero_ext 8 v1)
   | Ocast16signed, v1 :: nil => Some (Val.sign_ext 16 v1)
@@ -276,6 +277,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Omove => (nil, Tint)   (* treated specially *)
   | Ointconst _ => (nil, Tint)
   | Ofloatconst _ => (nil, Tfloat)
+  | Oaddrsymbol _ => (nil, Tint)
   | Ocast8signed => (Tint :: nil, Tint)
   | Ocast8unsigned => (Tint :: nil, Tint)
   | Ocast16signed => (Tint :: nil, Tint)
@@ -353,6 +355,7 @@ Proof with (try exact I).
   congruence.
   exact I.
   exact I.
+  unfold symbol_address; destruct (Genv.find_symbol genv i)...
   destruct v0...
   destruct v0...
   destruct v0...
@@ -539,6 +542,7 @@ Definition two_address_op (op: operation) : bool :=
   | Omove => false
   | Ointconst _ => false
   | Ofloatconst _ => false
+  | Oaddrsymbol _ => false
   | Ocast8signed => false
   | Ocast8unsigned => false
   | Ocast16signed => false
@@ -691,6 +695,7 @@ Lemma eval_operation_preserved:
 Proof.
   intros.
   unfold eval_operation; destruct op; auto.
+  unfold symbol_address. rewrite agree_on_symbols. auto.
   apply eval_addressing_preserved.
 Qed.