Support for indirect symbols under MacOS X (final).

Remove stdio hack in runtime/


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1979 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

6 files changed, 12 insertions, 24 deletions

diff --git a/ia32/Asm.v b/ia32/Asm.v
index a6a03ed..6210286 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -108,7 +108,7 @@ Inductive instruction: Type :=
   (** Moves *)
   | Pmov_rr (rd: ireg) (r1: ireg)       (**r [mov] (32-bit int) *)
   | Pmov_ri (rd: ireg) (n: int)
-  | Pmov_raddr (rd: ireg) (id: ident)
+  | Pmov_ra (rd: ireg) (id: ident)
   | Pmov_rm (rd: ireg) (a: addrmode)
   | Pmov_mr (a: addrmode) (rs: ireg)
   | Pmovd_fr (rd: freg) (r1: ireg)      (**r [movd] (32-bit int) *)
@@ -459,7 +459,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       Next (nextinstr (rs#rd <- (rs r1))) m
   | Pmov_ri rd n =>
       Next (nextinstr_nf (rs#rd <- (Vint n))) m
-  | Pmov_raddr rd id =>
+  | Pmov_ra rd id =>
       Next (nextinstr_nf (rs#rd <- (symbol_offset id Int.zero))) m
   | Pmov_rm rd a =>
       exec_load Mint32 m a rs rd
diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v
index 5603d85..3fc3efb 100644
--- a/ia32/Asmgen.v
+++ b/ia32/Asmgen.v
@@ -322,9 +322,9 @@ Definition transl_op
   | Ofloatconst f, nil =>
       do r <- freg_of res; 
       OK ((if Float.eq_dec f Float.zero then Pxorpd_f r else Pmovsd_fi r f) :: k)
-  | Oaddrsymbol id, nil =>
+  | Oindirectsymbol id, nil =>
       do r <- ireg_of res;
-      OK (Pmov_raddr r id :: k)
+      OK (Pmov_ra r id :: k)
   | Ocast8signed, a1 :: nil =>
       do r1 <- ireg_of a1; do r <- ireg_of res; mk_intconv Pmovsb_rr r r1 k
   | Ocast8unsigned, a1 :: nil =>
diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp
index 0643296..ff5044f 100644
--- a/ia32/ConstpropOp.vp
+++ b/ia32/ConstpropOp.vp
@@ -145,19 +145,6 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
   | _, _ => Unknown
   end.
 
-(** * Generation of constants *)
-
-Parameter generate_float_constants : unit -> bool.
-
-Definition const_for_result (a: approx) : option operation :=
-  match a with
-  | I n => Some(Ointconst n)
-  | F n => if generate_float_constants tt then Some(Ofloatconst n) else None
-  | G symb ofs => Some(Olea (Aglobal symb ofs))
-  | S ofs => Some(Olea (Ainstack ofs))
-  | _ => None
-  end.
-
 (** * Operator strength reduction *)
 
 (** We now define auxiliary functions for strength reduction of
diff --git a/ia32/Op.v b/ia32/Op.v
index a5568c7..c32de67 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -69,7 +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 *)
+  | Oindirectsymbol: 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] *)
@@ -114,6 +114,7 @@ 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,7 +194,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)
+  | Oindirectsymbol 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)
@@ -277,7 +278,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Omove => (nil, Tint)   (* treated specially *)
   | Ointconst _ => (nil, Tint)
   | Ofloatconst _ => (nil, Tfloat)
-  | Oaddrsymbol _ => (nil, Tint)
+  | Oindirectsymbol _ => (nil, Tint)
   | Ocast8signed => (Tint :: nil, Tint)
   | Ocast8unsigned => (Tint :: nil, Tint)
   | Ocast16signed => (Tint :: nil, Tint)
@@ -542,7 +543,7 @@ Definition two_address_op (op: operation) : bool :=
   | Omove => false
   | Ointconst _ => false
   | Ofloatconst _ => false
-  | Oaddrsymbol _ => false
+  | Oindirectsymbol _ => false
   | Ocast8signed => false
   | Ocast8unsigned => false
   | Ocast16signed => false
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index ec3cf2a..8b795ee 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -511,7 +511,7 @@ let print_instruction oc = function
       fprintf oc "	movl	%a, %a\n" ireg r1 ireg rd
   | Pmov_ri(rd, n) ->
       fprintf oc "	movl	$%ld, %a\n" (camlint_of_coqint n) ireg rd
-  | Pmov_raddr(rd, id) ->
+  | Pmov_ra(rd, id) ->
       if target = MacOS then begin
         let id = extern_atom id in
         indirect_symbols := StringSet.add id !indirect_symbols;
diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp
index 19e64cc..6d44cf5 100644
--- a/ia32/SelectOp.vp
+++ b/ia32/SelectOp.vp
@@ -62,8 +62,8 @@ Parameter symbol_is_external: ident -> bool.
 Definition addrsymbol (id: ident) (ofs: int) :=
   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)
+    then Eop (Oindirectsymbol id) Enil
+    else Eop (Olea (Aindexed ofs)) (Eop (Oindirectsymbol id) Enil ::: Enil)
   else
     Eop (Olea (Aglobal id ofs)) Enil.