From 3fa79790e617d87584598746296e626e0ce3b256 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 24 May 2014 09:46:07 +0000
Subject: Refactoring: move symbol_offset into Genv.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2503 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 arm/Asm.v                  | 14 ++++----------
 arm/Asmgenproof.v          |  8 ++++----
 arm/ConstpropOpproof.v     |  4 ++--
 arm/Op.v                   | 20 +++++++-------------
 arm/SelectOpproof.v        |  4 ++--
 arm/ValueAOp.v             |  2 +-
 backend/Constpropproof.v   |  6 +++---
 backend/Selectionproof.v   |  2 +-
 backend/ValueDomain.v      | 11 ++++-------
 common/Globalenvs.v        | 17 +++++++++++++++++
 ia32/Asm.v                 | 16 +++++-----------
 ia32/Asmgenproof.v         |  8 ++++----
 ia32/Asmgenproof1.v        |  4 ++--
 ia32/ConstpropOpproof.v    | 31 ++++++++++++------------------
 ia32/Op.v                  | 44 +++++++++++++++++++------------------------
 ia32/SelectOpproof.v       | 20 +++++++-------------
 ia32/ValueAOp.v            |  2 +-
 powerpc/Asm.v              | 26 ++++++++++---------------
 powerpc/Asmgenproof.v      |  8 ++++----
 powerpc/Asmgenproof1.v     | 47 +++++++++++++++++-----------------------------
 powerpc/ConstpropOpproof.v | 19 ++++++-------------
 powerpc/Op.v               | 36 +++++++++++++++--------------------
 powerpc/SelectOpproof.v    | 23 ++++++++---------------
 powerpc/ValueAOp.v         |  2 +-
 24 files changed, 156 insertions(+), 218 deletions(-)

diff --git a/arm/Asm.v b/arm/Asm.v
index 69f6319..9d3ba5b 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -493,12 +493,6 @@ Definition eval_testcond (c: testcond) (rs: regset) : option bool :=
     must survive the execution of the pseudo-instruction.
 *)
 
-Definition symbol_offset (id: ident) (ofs: int) : val :=
-  match Genv.find_symbol ge id with
-  | Some b => Vptr b ofs
-  | None => Vundef
-  end.
-
 Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : outcome :=
   match i with
   | Padd r1 r2 so => 
@@ -514,11 +508,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       | None => Stuck
       end
   | Pbsymb id sg =>                  
-      Next (rs#PC <- (symbol_offset id Int.zero)) m
+      Next (rs#PC <- (Genv.symbol_address ge id Int.zero)) m
   | Pbreg r sg =>                    
       Next (rs#PC <- (rs#r)) m
   | Pblsymb id sg =>                 
-      Next (rs#IR14 <- (Val.add rs#PC Vone) #PC <- (symbol_offset id Int.zero)) m
+      Next (rs#IR14 <- (Val.add rs#PC Vone) #PC <- (Genv.symbol_address ge id Int.zero)) m
   | Pblreg r sg =>                   
       Next (rs#IR14 <- (Val.add rs#PC Vone) #PC <- (rs#r)) m
   | Pbic r1 r2 so => 
@@ -649,7 +643,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Plabel lbl =>
       Next (nextinstr rs) m
   | Ploadsymbol r1 lbl ofs =>
-      Next (nextinstr (rs#r1 <- (symbol_offset lbl ofs))) m
+      Next (nextinstr (rs#r1 <- (Genv.symbol_address ge lbl ofs))) m
   | Pbtbl r tbl =>
       match rs#r with
       | Vint n => 
@@ -763,7 +757,7 @@ Inductive initial_state (p: program): state -> Prop :=
       let ge := Genv.globalenv p in
       let rs0 :=
         (Pregmap.init Vundef)
-        # PC <- (symbol_offset ge p.(prog_main) Int.zero)
+        # PC <- (Genv.symbol_address ge p.(prog_main) Int.zero)
         # IR14 <- Vzero
         # IR13 <- Vzero in
       Genv.init_mem p = Some m0 ->
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index 19f5687..cfe4f54 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -662,7 +662,7 @@ Opaque loadind.
   left; econstructor; split.
   apply plus_one. eapply exec_step_internal. eauto.
   eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
-  simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite H. eauto.
+  simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. eauto.
   econstructor; eauto. 
   econstructor; eauto.
   eapply agree_sp_def; eauto.
@@ -730,7 +730,7 @@ Opaque loadind.
   eapply plus_right'. eapply exec_straight_exec; eauto. 
   econstructor. eauto. eapply functions_transl; eauto. 
   eapply find_instr_tail; eauto. 
-  simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite H. reflexivity. 
+  simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. reflexivity. 
   traceEq.
   econstructor; eauto.
   split. Simpl. eapply parent_sp_def; eauto. 
@@ -944,13 +944,13 @@ Proof.
   econstructor; split.
   econstructor.
   eapply Genv.init_mem_transf_partial; eauto.
-  replace (symbol_offset (Genv.globalenv tprog) (prog_main tprog) Int.zero)
+  replace (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Int.zero)
      with (Vptr fb Int.zero).
   econstructor; eauto.
   constructor.
   apply Mem.extends_refl.
   split. auto. simpl. unfold Vzero; congruence. intros. rewrite Regmap.gi. auto. 
-  unfold symbol_offset. 
+  unfold Genv.symbol_address. 
   rewrite (transform_partial_program_main _ _ TRANSF).
   rewrite symbols_preserved. 
   unfold ge; rewrite H1. auto.
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index 7cf5879..00ea8bc 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -49,7 +49,7 @@ Hypothesis MATCH: ematch bc rs ae.
 
 Lemma match_G:
   forall r id ofs,
-  AE.get r ae = Ptr(Gl id ofs) -> Val.lessdef rs#r (symbol_address ge id ofs).
+  AE.get r ae = Ptr(Gl id ofs) -> Val.lessdef rs#r (Genv.symbol_address ge id ofs).
 Proof.
   intros. apply vmatch_ptr_gl with bc; auto. rewrite <- H. apply MATCH. 
 Qed.
@@ -82,7 +82,7 @@ Ltac SimplVM :=
       rewrite E in *; clear H; SimplVM
   | [ H: vmatch _ ?v (Ptr(Gl ?id ?ofs)) |- _ ] =>
       let E := fresh in
-      assert (E: Val.lessdef v (Op.symbol_address ge id ofs)) by (eapply vmatch_ptr_gl; eauto); 
+      assert (E: Val.lessdef v (Genv.symbol_address ge id ofs)) by (eapply vmatch_ptr_gl; eauto); 
       clear H; SimplVM
   | [ H: vmatch _ ?v (Ptr(Stk ?ofs)) |- _ ] =>
       let E := fresh in
diff --git a/arm/Op.v b/arm/Op.v
index 7323abc..b50a7b0 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -177,12 +177,6 @@ Global Opaque eq_shift eq_condition eq_operation eq_addressing.
 
 (** * Evaluation functions *)
 
-Definition symbol_address (F V: Type) (genv: Genv.t F V) (id: ident) (ofs: int) : val :=
-  match Genv.find_symbol genv id with
-  | Some b => Vptr b ofs
-  | None => Vundef
-  end.
-
 (** Evaluation of conditions, operators and addressing modes applied
   to lists of values.  Return [None] when the computation can trigger an
   error, e.g. integer division by zero.  [eval_condition] returns a boolean,
@@ -219,7 +213,7 @@ Definition eval_operation
   | Omove, v1::nil => Some v1
   | Ointconst n, nil => Some (Vint n)
   | Ofloatconst n, nil => Some (Vfloat n)
-  | Oaddrsymbol s ofs, nil => Some (symbol_address genv s ofs)
+  | Oaddrsymbol s ofs, nil => Some (Genv.symbol_address genv s ofs)
   | Oaddrstack ofs, nil => Some (Val.add sp (Vint ofs))
   | Ocast8signed, v1::nil => Some (Val.sign_ext 8 v1)
   | Ocast16signed, v1::nil => Some (Val.sign_ext 16 v1)
@@ -397,7 +391,7 @@ Proof with (try exact I).
   destruct op; simpl; simpl in H0; FuncInv; try subst v...
   congruence.
   destruct (Float.is_single_dec f); red; auto. 
-  unfold symbol_address. destruct (Genv.find_symbol genv i)...
+  unfold Genv.symbol_address. destruct (Genv.find_symbol genv i)...
   destruct sp...
   destruct v0...
   destruct v0...
@@ -714,7 +708,7 @@ Lemma eval_operation_preserved:
 Proof.
   intros.
   unfold eval_operation; destruct op; auto. 
-  unfold symbol_address. rewrite agree_on_symbols; auto.
+  unfold Genv.symbol_address. rewrite agree_on_symbols; auto.
 Qed.
 
 Lemma eval_addressing_preserved:
@@ -739,7 +733,7 @@ Variable f: meminj.
 
 Hypothesis symbol_address_inj: 
   forall id ofs,
-  val_inject f (symbol_address genv id ofs) (symbol_address genv id ofs).
+  val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs).
 
 Variable m1: mem.
 Variable m2: mem.
@@ -902,7 +896,7 @@ Lemma eval_addressing_inj:
   exists v2, eval_addressing genv sp2 addr vl2 = Some v2 /\ val_inject f v1 v2.
 Proof.
   assert (UNUSED: forall id ofs,
-            val_inject f (symbol_address genv id ofs) (symbol_address genv id ofs)).
+            val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs)).
   exact symbol_address_inj.
   intros. destruct addr; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
   apply Values.val_add_inject; auto.
@@ -1032,9 +1026,9 @@ Variable delta: Z.
 Hypothesis sp_inj: f sp1 = Some(sp2, delta).
 
 Remark symbol_address_inject:
-  forall id ofs, val_inject f (symbol_address genv id ofs) (symbol_address genv id ofs).
+  forall id ofs, val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs).
 Proof.
-  intros. unfold symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto.
+  intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto.
   exploit (proj1 globals); eauto. intros. 
   econstructor; eauto. rewrite Int.add_zero; auto.
 Qed.
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index d10e7fc..4b89119 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -114,7 +114,7 @@ Definition binary_constructor_sound (cstr: expr -> expr -> expr) (sem: val -> va
 
 Theorem eval_addrsymbol:
   forall le id ofs,
-  exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (symbol_address ge id ofs) v.
+  exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (Genv.symbol_address ge id ofs) v.
 Proof.
   intros. unfold addrsymbol. econstructor; split. 
   EvalOp. simpl; eauto. 
@@ -150,7 +150,7 @@ Proof.
   destruct x; simpl; auto. rewrite Int.add_zero. auto. rewrite Int.add_zero. auto.
   case (addimm_match a); intros; InvEval; simpl; TrivialExists; simpl.
   rewrite Int.add_commut. auto.
-  unfold symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. rewrite Int.add_commut; auto.
+  unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. rewrite Int.add_commut; auto.
   rewrite Val.add_assoc. rewrite Int.add_commut. auto.
   subst x. rewrite Val.add_assoc. rewrite Int.add_commut. auto.
 Qed. 
diff --git a/arm/ValueAOp.v b/arm/ValueAOp.v
index 037b22e..b312361 100644
--- a/arm/ValueAOp.v
+++ b/arm/ValueAOp.v
@@ -149,7 +149,7 @@ Qed.
 
 Lemma symbol_address_sound:
   forall id ofs,
-  vmatch bc (symbol_address ge id ofs) (Ptr (Gl id ofs)).
+  vmatch bc (Genv.symbol_address ge id ofs) (Ptr (Gl id ofs)).
 Proof.
   intros; apply symbol_address_sound; apply GENV.
 Qed.
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index d88d6e4..ecae5dc 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -133,7 +133,7 @@ Proof.
   destruct (areg ae r); auto. destruct p; auto. 
   predSpec Int.eq Int.eq_spec ofs Int.zero; intros; auto. 
   subst ofs. exploit vmatch_ptr_gl; eauto. intros LD'. inv LD'; try discriminate.
-  rewrite H1 in FF. unfold symbol_address in FF. 
+  rewrite H1 in FF. unfold Genv.symbol_address in FF. 
   simpl. rewrite symbols_preserved.
   destruct (Genv.find_symbol ge id) as [b|]; try discriminate.
   simpl in FF. rewrite dec_eq_true in FF.
@@ -162,8 +162,8 @@ Proof.
 - (* pointer *)
   destruct p; try discriminate.
   + (* global *)
-    inv H. exists (symbol_address ge id ofs); split.
-    unfold symbol_address. rewrite <- symbols_preserved. reflexivity.
+    inv H. exists (Genv.symbol_address ge id ofs); split.
+    unfold Genv.symbol_address. rewrite <- symbols_preserved. reflexivity.
     eapply vmatch_ptr_gl; eauto. 
   + (* stack *)
     inv H. exists (Vptr sp ofs); split. 
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index c292b49..175b025 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -380,7 +380,7 @@ Proof.
   exists (Val.longofwords (Vint (Int64.hiword i)) (Vint (Int64.loword i))); split.
   eapply eval_Eop. constructor. EvalOp. simpl; eauto. constructor. EvalOp. simpl; eauto. constructor. auto.
   simpl. rewrite Int64.ofwords_recompose. auto.
-  rewrite <- symbols_preserved. fold (symbol_address tge i i0). apply eval_addrsymbol.
+  rewrite <- symbols_preserved. fold (Genv.symbol_address tge i i0). apply eval_addrsymbol.
   apply eval_addrstack.
   (* Eunop *)
   exploit IHeval_expr; eauto. intros [v1' [A B]].
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 2ece8cd..c8431bb 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -1075,15 +1075,12 @@ Definition genv_match (ge: genv) : Prop :=
   (forall id b, Genv.find_symbol ge id = Some b <-> bc b = BCglob id)
 /\(forall b, Plt b (Genv.genv_next ge) -> bc b <> BCinvalid /\ bc b <> BCstack).
 
-Definition symbol_address (ge: genv) (id: ident) (ofs: int) : val :=
-  match Genv.find_symbol ge id with Some b => Vptr b ofs | None => Vundef end.
-
 Lemma symbol_address_sound:
   forall ge id ofs,
   genv_match ge ->
-  vmatch (symbol_address ge id ofs) (Ptr (Gl id ofs)).
+  vmatch (Genv.symbol_address ge id ofs) (Ptr (Gl id ofs)).
 Proof.
-  intros. unfold symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:F. 
+  intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:F. 
   constructor. constructor. apply H; auto. 
   constructor.
 Qed.
@@ -1092,9 +1089,9 @@ Lemma vmatch_ptr_gl:
   forall ge v id ofs,
   genv_match ge ->
   vmatch v (Ptr (Gl id ofs)) ->
-  Val.lessdef v (symbol_address ge id ofs).
+  Val.lessdef v (Genv.symbol_address ge id ofs).
 Proof.
-  intros. unfold symbol_address. inv H0. 
+  intros. unfold Genv.symbol_address. inv H0. 
 - inv H3. replace (Genv.find_symbol ge id) with (Some b). constructor. 
   symmetry. apply H; auto.
 - constructor.
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index 4e155e3..3b077e0 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -102,6 +102,16 @@ Record t: Type := mkgenv {
 Definition find_symbol (ge: t) (id: ident) : option block :=
   PTree.get id ge.(genv_symb).
 
+(** [symbol_address ge id ofs] returns a pointer into the block associated
+  with [id], at byte offset [ofs].  [Vundef] is returned if no block is associated
+  to [id]. *)
+
+Definition symbol_address (ge: t) (id: ident) (ofs: int) : val :=
+  match find_symbol ge id with
+  | Some b => Vptr b ofs
+  | None => Vundef
+  end.
+
 (** [find_funct_ptr ge b] returns the function description associated with
     the given address. *)
 
@@ -267,6 +277,13 @@ End GLOBALENV_PRINCIPLES.
 
 (** ** Properties of the operations over global environments *)
 
+Theorem shift_symbol_address:
+  forall ge id ofs n,
+  symbol_address ge id (Int.add ofs n) = Val.add (symbol_address ge id ofs) (Vint n).
+Proof.
+  intros. unfold symbol_address. destruct (find_symbol ge id); auto. 
+Qed.
+
 Theorem find_funct_inv:
   forall ge v f,
   find_funct ge v = Some f -> exists b, v = Vptr b Int.zero.
diff --git a/ia32/Asm.v b/ia32/Asm.v
index f03ea75..2e5b8b9 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -275,12 +275,6 @@ Fixpoint label_pos (lbl: label) (pos: Z) (c: code) {struct c} : option Z :=
 
 Variable ge: genv.
 
-Definition symbol_offset (id: ident) (ofs: int) : val :=
-  match Genv.find_symbol ge id with
-  | Some b => Vptr b ofs
-  | None => Vundef
-  end.
-
 (** Evaluating an addressing mode *)
 
 Definition eval_addrmode (a: addrmode) (rs: regset) : val :=
@@ -296,7 +290,7 @@ Definition eval_addrmode (a: addrmode) (rs: regset) : val :=
               end)
              (match const with
               | inl ofs => Vint ofs
-              | inr(id, ofs) => symbol_offset id ofs
+              | inr(id, ofs) => Genv.symbol_address ge id ofs
               end))
   end.
 
@@ -477,7 +471,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pmov_ri rd n =>
       Next (nextinstr_nf (rs#rd <- (Vint n))) m
   | Pmov_ra rd id =>
-      Next (nextinstr_nf (rs#rd <- (symbol_offset id Int.zero))) m
+      Next (nextinstr_nf (rs#rd <- (Genv.symbol_address ge id Int.zero))) m
   | Pmov_rm rd a =>
       exec_load Mint32 m a rs rd
   | Pmov_mr a r1 =>
@@ -631,7 +625,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pjmp_l lbl =>
       goto_label f lbl rs m
   | Pjmp_s id sg =>
-      Next (rs#PC <- (symbol_offset id Int.zero)) m
+      Next (rs#PC <- (Genv.symbol_address ge id Int.zero)) m
   | Pjmp_r r sg =>
       Next (rs#PC <- (rs r)) m
   | Pjcc cond lbl =>
@@ -656,7 +650,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       | _ => Stuck
       end
   | Pcall_s id sg =>
-      Next (rs#RA <- (Val.add rs#PC Vone) #PC <- (symbol_offset id Int.zero)) m
+      Next (rs#RA <- (Val.add rs#PC Vone) #PC <- (Genv.symbol_address ge id Int.zero)) m
   | Pcall_r r sg =>
       Next (rs#RA <- (Val.add rs#PC Vone) #PC <- (rs r)) m
   | Pret =>
@@ -806,7 +800,7 @@ Inductive initial_state (p: program): state -> Prop :=
       let ge := Genv.globalenv p in
       let rs0 :=
         (Pregmap.init Vundef)
-        # PC <- (symbol_offset ge p.(prog_main) Int.zero)
+        # PC <- (Genv.symbol_address ge p.(prog_main) Int.zero)
         # RA <- Vzero
         # ESP <- Vzero in
       initial_state p (State rs0 m0).
diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v
index fa8ce6c..881375f 100644
--- a/ia32/Asmgenproof.v
+++ b/ia32/Asmgenproof.v
@@ -613,7 +613,7 @@ Opaque loadind.
   left; econstructor; split.
   apply plus_one. eapply exec_step_internal. eauto.
   eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
-  simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite H. eauto.
+  simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. eauto.
   econstructor; eauto. 
   econstructor; eauto.
   eapply agree_sp_def; eauto.
@@ -665,7 +665,7 @@ Opaque loadind.
   econstructor; eauto.
   apply agree_set_other; auto. apply agree_nextinstr. apply agree_set_other; auto.
   eapply agree_change_sp; eauto. eapply parent_sp_def; eauto.
-  rewrite Pregmap.gss. unfold symbol_offset. rewrite symbols_preserved. rewrite H. auto.
+  rewrite Pregmap.gss. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. auto.
 
 - (* Mbuiltin *)
   inv AT. monadInv H3. 
@@ -900,13 +900,13 @@ Proof.
   econstructor; split.
   econstructor.
   eapply Genv.init_mem_transf_partial; eauto.
-  replace (symbol_offset (Genv.globalenv tprog) (prog_main tprog) Int.zero)
+  replace (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Int.zero)
      with (Vptr fb Int.zero).
   econstructor; eauto.
   constructor.
   apply Mem.extends_refl.
   split. auto. simpl. unfold Vzero; congruence. intros. rewrite Regmap.gi. auto. 
-  unfold symbol_offset. 
+  unfold Genv.symbol_address.
   rewrite (transform_partial_program_main _ _ TRANSF).
   rewrite symbols_preserved. 
   unfold ge; rewrite H1. auto.
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index 6f2aee5..b3c815b 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -381,11 +381,11 @@ Proof.
   monadInv H. rewrite (ireg_of_eq _ _ EQ); rewrite (ireg_of_eq _ _ EQ1); simpl.
   apply Val.add_lessdef; auto. apply Val.add_lessdef; auto. 
 (* global *)
-  inv H. simpl. unfold symbol_address, symbol_offset.
+  inv H. simpl. unfold Genv.symbol_address.
   destruct (Genv.find_symbol ge i); simpl; auto. repeat rewrite Int.add_zero. auto.
 (* based *)
   monadInv H. rewrite (ireg_of_eq _ _ EQ). simpl.
-  unfold symbol_address, symbol_offset. destruct (Genv.find_symbol ge i); simpl; auto.
+  unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); simpl; auto.
   rewrite Int.add_zero. rewrite Val.add_commut. auto. 
 (* basedscaled *)
   monadInv H. rewrite (ireg_of_eq _ _ EQ). unfold eval_addrmode. 
diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v
index 8a05534..d9eea2b 100644
--- a/ia32/ConstpropOpproof.v
+++ b/ia32/ConstpropOpproof.v
@@ -46,7 +46,7 @@ Hypothesis MATCH: ematch bc e ae.
 
 Lemma match_G:
   forall r id ofs,
-  AE.get r ae = Ptr(Gl id ofs) -> Val.lessdef e#r (symbol_address ge id ofs).
+  AE.get r ae = Ptr(Gl id ofs) -> Val.lessdef e#r (Genv.symbol_address ge id ofs).
 Proof.
   intros. apply vmatch_ptr_gl with bc; auto. rewrite <- H. apply MATCH. 
 Qed.
@@ -79,7 +79,7 @@ Ltac SimplVM :=
       rewrite E in *; clear H; SimplVM
   | [ H: vmatch _ ?v (Ptr(Gl ?id ?ofs)) |- _ ] =>
       let E := fresh in
-      assert (E: Val.lessdef v (Op.symbol_address ge id ofs)) by (eapply vmatch_ptr_gl; eauto); 
+      assert (E: Val.lessdef v (Genv.symbol_address ge id ofs)) by (eapply vmatch_ptr_gl; eauto); 
       clear H; SimplVM
   | [ H: vmatch _ ?v (Ptr(Stk ?ofs)) |- _ ] =>
       let E := fresh in
@@ -103,13 +103,6 @@ Proof.
 - auto.
 Qed.
 
-Remark shift_symbol_address:
-  forall symb ofs n,
-  Op.symbol_address ge symb (Int.add ofs n) = Val.add (Op.symbol_address ge symb ofs) (Vint n).
-Proof.
-  unfold Op.symbol_address; intros. destruct (Genv.find_symbol ge symb); auto. 
-Qed.
-
 Lemma addr_strength_reduction_correct:
   forall addr args vl res,
   vl = map (fun r => AE.get r ae) args ->
@@ -120,15 +113,15 @@ Proof.
   intros until res. unfold addr_strength_reduction.
   destruct (addr_strength_reduction_match addr args vl); simpl;
   intros VL EA; InvApproxRegs; SimplVM; try (inv EA).
-- rewrite shift_symbol_address. econstructor; split. eauto. apply Val.add_lessdef; auto.
+- rewrite Genv.shift_symbol_address. econstructor; split. eauto. apply Val.add_lessdef; auto.
 - econstructor; split; eauto. rewrite Int.add_zero_l.
   change (Vptr sp (Int.add n ofs)) with (Val.add (Vptr sp n) (Vint ofs)). apply Val.add_lessdef; auto.
-- econstructor; split; eauto. rewrite Int.add_assoc. rewrite shift_symbol_address. 
+- econstructor; split; eauto. rewrite Int.add_assoc. rewrite Genv.shift_symbol_address. 
   rewrite Val.add_assoc. apply Val.add_lessdef; auto.
 - econstructor; split; eauto.
   fold (Val.add (Vint n1) e#r2). rewrite (Val.add_commut (Vint n1)).
-  rewrite shift_symbol_address. apply Val.add_lessdef; auto.
-  rewrite Int.add_commut. rewrite shift_symbol_address. apply Val.add_lessdef; auto. 
+  rewrite Genv.shift_symbol_address. apply Val.add_lessdef; auto.
+  rewrite Int.add_commut. rewrite Genv.shift_symbol_address. apply Val.add_lessdef; auto. 
 - econstructor; split; eauto. rewrite Int.add_zero_l. rewrite Int.add_assoc. 
   change (Vptr sp (Int.add n1 (Int.add n2 ofs)))
     with (Val.add (Vptr sp n1) (Vint (Int.add n2 ofs))).
@@ -138,10 +131,10 @@ Proof.
   change (Vptr sp (Int.add (Int.add n2 n1) ofs))
     with (Val.add (Val.add (Vint n1) (Vptr sp n2)) (Vint ofs)).
   apply Val.add_lessdef; auto. apply Val.add_lessdef; auto. 
-- econstructor; split; eauto. rewrite shift_symbol_address. 
+- econstructor; split; eauto. rewrite Genv.shift_symbol_address. 
   rewrite ! Val.add_assoc. apply Val.add_lessdef; auto. 
   rewrite Val.add_commut. apply Val.add_lessdef; auto. 
-- econstructor; split; eauto. rewrite shift_symbol_address.
+- econstructor; split; eauto. rewrite Genv.shift_symbol_address.
   rewrite (Val.add_commut e#r1). rewrite ! Val.add_assoc.
   apply Val.add_lessdef; auto. rewrite Val.add_commut. apply Val.add_lessdef; auto.
 - fold (Val.add (Vint n1) e#r2). econstructor; split; eauto. 
@@ -150,13 +143,13 @@ Proof.
 - econstructor; split; eauto.  rewrite ! Val.add_assoc.
   apply Val.add_lessdef; eauto. 
 - econstructor; split; eauto. rewrite Int.add_assoc. 
-  rewrite shift_symbol_address. apply Val.add_lessdef; auto. 
+  rewrite Genv.shift_symbol_address. apply Val.add_lessdef; auto. 
 - econstructor; split; eauto. 
-  rewrite shift_symbol_address. rewrite ! Val.add_assoc. apply Val.add_lessdef; auto.
+  rewrite Genv.shift_symbol_address. rewrite ! Val.add_assoc. apply Val.add_lessdef; auto.
   rewrite Val.add_commut; auto.
 - econstructor; split; eauto.
-- econstructor; split; eauto. rewrite shift_symbol_address. auto.
-- econstructor; split; eauto. rewrite shift_symbol_address. rewrite Int.mul_commut; auto.
+- econstructor; split; eauto. rewrite Genv.shift_symbol_address. auto.
+- econstructor; split; eauto. rewrite Genv.shift_symbol_address. rewrite Int.mul_commut; auto.
 - econstructor; eauto.
 Qed.
 
diff --git a/ia32/Op.v b/ia32/Op.v
index 5420607..e46c740 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -156,12 +156,6 @@ Global Opaque eq_condition eq_addressing eq_operation.
 
 (** * Evaluation functions *)
 
-Definition symbol_address (F V: Type) (genv: Genv.t F V) (id: ident) (ofs: int) : val :=
-  match Genv.find_symbol genv id with
-  | Some b => Vptr b ofs
-  | None => Vundef
-  end.
-
 (** Evaluation of conditions, operators and addressing modes applied
   to lists of values.  Return [None] when the computation can trigger an
   error, e.g. integer division by zero.  [eval_condition] returns a boolean,
@@ -193,11 +187,11 @@ Definition eval_addressing
   | Aindexed2scaled sc ofs, v1::v2::nil =>
       Some(Val.add v1 (Val.add (Val.mul v2 (Vint sc)) (Vint ofs)))
   | Aglobal s ofs, nil =>
-      Some (symbol_address genv s ofs)
+      Some (Genv.symbol_address genv s ofs)
   | Abased s ofs, v1::nil =>
-      Some (Val.add (symbol_address genv s ofs) v1)
+      Some (Val.add (Genv.symbol_address genv s ofs) v1)
   | Abasedscaled sc s ofs, v1::nil =>
-      Some (Val.add (symbol_address genv s ofs) (Val.mul v1 (Vint sc)))
+      Some (Val.add (Genv.symbol_address genv s ofs) (Val.mul v1 (Vint sc)))
   | Ainstack ofs, nil =>
       Some(Val.add sp (Vint ofs))
   | _, _ => None
@@ -210,7 +204,7 @@ Definition eval_operation
   | Omove, v1::nil => Some v1
   | Ointconst n, nil => Some (Vint n)
   | Ofloatconst n, nil => Some (Vfloat n)
-  | Oindirectsymbol id, nil => Some (symbol_address genv id Int.zero)
+  | Oindirectsymbol id, nil => Some (Genv.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)
@@ -368,11 +362,11 @@ Proof with (try exact I).
   destruct v0... destruct v1... destruct v1...
   destruct v0...
   destruct v0... destruct v1... destruct v1...
-  unfold symbol_address; destruct (Genv.find_symbol genv i)...
-  unfold symbol_address; destruct (Genv.find_symbol genv i)...
-  unfold symbol_address; destruct (Genv.find_symbol genv i)... destruct v0...
+  unfold Genv.symbol_address; destruct (Genv.find_symbol genv i)...
+  unfold Genv.symbol_address; destruct (Genv.find_symbol genv i)...
+  unfold Genv.symbol_address; destruct (Genv.find_symbol genv i)... destruct v0...
   destruct v0...
-  unfold symbol_address; destruct (Genv.find_symbol genv i0)... destruct v0...
+  unfold Genv.symbol_address; destruct (Genv.find_symbol genv i0)... destruct v0...
   destruct sp...
 Qed.
 
@@ -387,7 +381,7 @@ Proof with (try exact I).
   congruence.
   exact I.
   destruct (Float.is_single_dec f); auto. 
-  unfold symbol_address; destruct (Genv.find_symbol genv i)...
+  unfold Genv.symbol_address; destruct (Genv.find_symbol genv i)...
   destruct v0...
   destruct v0...
   destruct v0...
@@ -568,10 +562,10 @@ Proof.
   rewrite !Val.add_assoc; auto.
   rewrite !Val.add_assoc; auto.
   rewrite !Val.add_assoc; auto.
-  unfold symbol_address. destruct (Genv.find_symbol ge i); auto. 
-  unfold symbol_address. destruct (Genv.find_symbol ge i); auto.
+  unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto. 
+  unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto.
   rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_commut. auto. 
-  unfold symbol_address. destruct (Genv.find_symbol ge i0); auto.
+  unfold Genv.symbol_address. destruct (Genv.find_symbol ge i0); auto.
   rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_commut. auto. 
   rewrite Val.add_assoc. auto. 
 Qed.
@@ -645,7 +639,7 @@ Proof.
   destruct v; simpl in *; inv H1; inv H2.
   right. apply Int.no_overlap_sound; auto. 
 (* Aglobal *)
-  unfold symbol_address in *. 
+  unfold Genv.symbol_address in *. 
   destruct (Genv.find_symbol ge i1) eqn:?; inv H2.
   destruct (Genv.find_symbol ge i) eqn:?; inv H1.
   destruct (ident_eq i i1). subst.
@@ -656,7 +650,7 @@ Proof.
   rewrite Int.add_commut; rewrite Int.add_zero; auto.
   left. red; intros; elim n. subst. eapply Genv.genv_vars_inj; eauto.
 (* Abased *)
-  unfold symbol_address in *. 
+  unfold Genv.symbol_address in *. 
   destruct (Genv.find_symbol ge i1) eqn:?; simpl in *; try discriminate.
   destruct v; inv H2.
   destruct (Genv.find_symbol ge i) eqn:?; inv H1.
@@ -689,7 +683,7 @@ Lemma eval_addressing_preserved:
   eval_addressing ge2 sp addr vl = eval_addressing ge1 sp addr vl.
 Proof.
   intros.
-  unfold eval_addressing, symbol_address; destruct addr; try rewrite agree_on_symbols;
+  unfold eval_addressing, Genv.symbol_address; destruct addr; try rewrite agree_on_symbols;
   reflexivity.
 Qed.
 
@@ -699,7 +693,7 @@ Lemma eval_operation_preserved:
 Proof.
   intros.
   unfold eval_operation; destruct op; auto.
-  unfold symbol_address. rewrite agree_on_symbols. auto.
+  unfold Genv.symbol_address. rewrite agree_on_symbols. auto.
   apply eval_addressing_preserved.
 Qed.
 
@@ -715,7 +709,7 @@ Variable f: meminj.
 
 Hypothesis symbol_address_inj: 
   forall id ofs,
-  val_inject f (symbol_address genv id ofs) (symbol_address genv id ofs).
+  val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs).
 
 Variable m1: mem.
 Variable m2: mem.
@@ -992,9 +986,9 @@ Variable delta: Z.
 Hypothesis sp_inj: f sp1 = Some(sp2, delta).
 
 Remark symbol_address_inject:
-  forall id ofs, val_inject f (symbol_address genv id ofs) (symbol_address genv id ofs).
+  forall id ofs, val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs).
 Proof.
-  intros. unfold symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto.
+  intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto.
   exploit (proj1 globals); eauto. intros. 
   econstructor; eauto. rewrite Int.add_zero; auto.
 Qed.
diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v
index b528a72..0fd6f7b 100644
--- a/ia32/SelectOpproof.v
+++ b/ia32/SelectOpproof.v
@@ -113,14 +113,14 @@ Definition binary_constructor_sound (cstr: expr -> expr -> expr) (sem: val -> va
 
 Theorem eval_addrsymbol:
   forall le id ofs,
-  exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (symbol_address ge id ofs) v.
+  exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (Genv.symbol_address ge id ofs) v.
 Proof.
-  intros. unfold addrsymbol. exists (symbol_address ge id ofs); split; auto.
+  intros. unfold addrsymbol. exists (Genv.symbol_address ge id ofs); split; auto.
   destruct (symbol_is_external id).
   predSpec Int.eq Int.eq_spec ofs Int.zero.
   subst. EvalOp.
   EvalOp. econstructor. EvalOp. simpl; eauto. econstructor. simpl. 
-  unfold symbol_address. destruct (Genv.find_symbol ge id); auto. 
+  unfold Genv.symbol_address. destruct (Genv.find_symbol ge id); auto. 
   simpl. rewrite Int.add_commut. rewrite Int.add_zero. auto. 
   EvalOp.
 Qed.
@@ -142,12 +142,6 @@ Proof.
   TrivialExists.
 Qed.
 
-Lemma shift_symbol_address:
-  forall id ofs n, symbol_address ge id (Int.add ofs n) = Val.add (symbol_address ge id ofs) (Vint n).
-Proof.
-  intros. unfold symbol_address. destruct (Genv.find_symbol); auto. 
-Qed.
-
 Theorem eval_addimm:
   forall n, unary_constructor_sound (addimm n) (fun x => Val.add x (Vint n)).
 Proof.
@@ -170,13 +164,13 @@ Proof.
   subst. TrivialExists. simpl. rewrite Val.add_permut_4. auto.
   subst. TrivialExists. simpl. rewrite Val.add_assoc. decEq; decEq. rewrite Val.add_permut. auto.
   subst. TrivialExists. simpl. rewrite Val.add_permut_4. rewrite <- Val.add_permut. rewrite <- Val.add_assoc. auto.
-  subst. TrivialExists. simpl. rewrite shift_symbol_address. 
+  subst. TrivialExists. simpl. rewrite Genv.shift_symbol_address. 
     rewrite Val.add_commut. rewrite Val.add_assoc. decEq. decEq. apply Val.add_commut.
-  subst. TrivialExists. simpl. rewrite shift_symbol_address. rewrite Val.add_assoc.
+  subst. TrivialExists. simpl. rewrite Genv.shift_symbol_address. rewrite Val.add_assoc.
     decEq; decEq. apply Val.add_commut.
-  subst. TrivialExists. simpl. rewrite shift_symbol_address. rewrite Val.add_commut. 
+  subst. TrivialExists. simpl. rewrite Genv.shift_symbol_address. rewrite Val.add_commut. 
     rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut.
-  subst. TrivialExists. simpl. rewrite shift_symbol_address.
+  subst. TrivialExists. simpl. rewrite Genv.shift_symbol_address.
     rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut.
   subst. TrivialExists. simpl. rewrite Val.add_permut. rewrite Val.add_assoc.
     decEq; decEq. apply Val.add_commut.
diff --git a/ia32/ValueAOp.v b/ia32/ValueAOp.v
index f3e2194..58b945f 100644
--- a/ia32/ValueAOp.v
+++ b/ia32/ValueAOp.v
@@ -128,7 +128,7 @@ Qed.
 
 Lemma symbol_address_sound:
   forall id ofs,
-  vmatch bc (symbol_address ge id ofs) (Ptr (Gl id ofs)).
+  vmatch bc (Genv.symbol_address ge id ofs) (Ptr (Gl id ofs)).
 Proof.
   intros; apply symbol_address_sound; apply GENV.
 Qed.
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 7a75d8f..aba78d4 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -376,12 +376,6 @@ Definition gpr_or_zero (rs: regset) (r: ireg) :=
 
 Variable ge: genv.
 
-Definition symbol_offset (id: ident) (ofs: int) : val :=
-  match Genv.find_symbol ge id with
-  | Some b => Vptr b ofs
-  | None => Vundef
-  end.
-
 (** The two functions below axiomatize how the linker processes
   symbolic references [symbol + offset] and splits their
   actual values into two 16-bit halves. *)
@@ -395,8 +389,8 @@ Parameter high_half: val -> val.
 
 Axiom low_high_half:
   forall id ofs,
-  Val.add (low_half (symbol_offset id ofs)) (high_half (symbol_offset id ofs))
-  = symbol_offset id ofs.
+  Val.add (low_half (Genv.symbol_address ge id ofs)) (high_half (Genv.symbol_address ge id ofs))
+  = Genv.symbol_address ge id ofs.
 
 (** The other axioms we take is that the results of
   the [low_half] and [high_half] functions are of type [Tint],
@@ -421,7 +415,7 @@ Parameter small_data_area_offset: genv -> ident -> int -> val.
 Axiom small_data_area_addressing:
   forall id ofs,
   symbol_is_small_data id ofs = true ->
-  small_data_area_offset ge id ofs = symbol_offset id ofs.
+  small_data_area_offset ge id ofs = Genv.symbol_address ge id ofs.
 
 Parameter symbol_is_rel_data: ident -> int -> bool.
 
@@ -436,10 +430,10 @@ Parameter symbol_is_rel_data: ident -> int -> bool.
 Definition const_low (c: constant) :=
   match c with
   | Cint n => Vint n
-  | Csymbol_low id ofs => low_half (symbol_offset id ofs)
+  | Csymbol_low id ofs => low_half (Genv.symbol_address ge id ofs)
   | Csymbol_high id ofs => Vundef
   | Csymbol_sda id ofs => small_data_area_offset ge id ofs
-  | Csymbol_rel_low id ofs => low_half (symbol_offset id ofs)
+  | Csymbol_rel_low id ofs => low_half (Genv.symbol_address ge id ofs)
   | Csymbol_rel_high id ofs => Vundef
   end.
 
@@ -447,10 +441,10 @@ Definition const_high (c: constant) :=
   match c with
   | Cint n => Vint (Int.shl n (Int.repr 16))
   | Csymbol_low id ofs => Vundef
-  | Csymbol_high id ofs => high_half (symbol_offset id ofs)
+  | Csymbol_high id ofs => high_half (Genv.symbol_address ge id ofs)
   | Csymbol_sda id ofs => Vundef
   | Csymbol_rel_low id ofs => Vundef
-  | Csymbol_rel_high id ofs => high_half (symbol_offset id ofs)
+  | Csymbol_rel_high id ofs => high_half (Genv.symbol_address ge id ofs)
   end.
 
 (** The semantics is purely small-step and defined as a function
@@ -597,9 +591,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       | _ => Stuck
       end
   | Pbl ident sg =>
-      Next (rs#LR <- (Val.add rs#PC Vone) #PC <- (symbol_offset ident Int.zero)) m
+      Next (rs#LR <- (Val.add rs#PC Vone) #PC <- (Genv.symbol_address ge ident Int.zero)) m
   | Pbs ident sg =>
-      Next (rs#PC <- (symbol_offset ident Int.zero)) m
+      Next (rs#PC <- (Genv.symbol_address ge ident Int.zero)) m
   | Pblr =>
       Next (rs#PC <- (rs#LR)) m
   | Pbt bit lbl =>
@@ -900,7 +894,7 @@ Inductive initial_state (p: program): state -> Prop :=
       let ge := Genv.globalenv p in
       let rs0 :=
         (Pregmap.init Vundef)
-        # PC <- (symbol_offset ge p.(prog_main) Int.zero)
+        # PC <- (Genv.symbol_address ge p.(prog_main) Int.zero)
         # LR <- Vzero
         # GPR1 <- Vzero in
       initial_state p (State rs0 m0).
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 5c99231..879d752 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -642,7 +642,7 @@ Opaque loadind.
   left; econstructor; split.
   apply plus_one. eapply exec_step_internal. eauto.
   eapply functions_transl; eauto. eapply find_instr_tail; eauto. 
-  simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite H. eauto.
+  simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. eauto.
   econstructor; eauto. 
   econstructor; eauto.
   eapply agree_sp_def; eauto.
@@ -733,7 +733,7 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen.
   eapply functions_transl; eauto. 
   eapply find_instr_tail.
   repeat (eapply code_tail_next_int; auto). eauto. 
-  simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite H. auto. traceEq.
+  simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. auto. traceEq.
   (* match states *)
   econstructor; eauto.
   assert (AG3: agree rs (Vptr stk soff) rs3).
@@ -972,13 +972,13 @@ Proof.
   econstructor; split.
   econstructor.
   eapply Genv.init_mem_transf_partial; eauto.
-  replace (symbol_offset (Genv.globalenv tprog) (prog_main tprog) Int.zero)
+  replace (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Int.zero)
      with (Vptr fb Int.zero).
   econstructor; eauto.
   constructor.
   apply Mem.extends_refl.
   split. auto. simpl. unfold Vzero; congruence. intros. rewrite Regmap.gi. auto. 
-  unfold symbol_offset. 
+  unfold Genv.symbol_address. 
   rewrite (transform_partial_program_main _ _ TRANSF).
   rewrite symbols_preserved. 
   unfold ge; rewrite H1. auto.
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 2436e2f..cfeb823 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -103,42 +103,30 @@ Proof.
   rewrite Int.sub_idem. apply Int.add_zero.
 Qed.
 
-Lemma add_zero_symbol_offset:
-  forall ge id ofs,
-  Val.add Vzero (symbol_offset ge id ofs) = symbol_offset ge id ofs.
+Lemma add_zero_symbol_address:
+  forall (ge: genv) id ofs,
+  Val.add Vzero (Genv.symbol_address ge id ofs) = Genv.symbol_address ge id ofs.
 Proof.
-  unfold symbol_offset; intros. destruct (Genv.find_symbol ge id); auto. 
+  unfold Genv.symbol_address; intros. destruct (Genv.find_symbol ge id); auto. 
   simpl. rewrite Int.add_zero; auto.
 Qed.
 
 Lemma csymbol_high_low:
-  forall ge id ofs,
-  Val.add (high_half (symbol_offset ge id ofs)) (low_half (symbol_offset ge id ofs))
-  = symbol_offset ge id ofs.
+  forall (ge: genv) id ofs,
+  Val.add (high_half (Genv.symbol_address ge id ofs)) (low_half (Genv.symbol_address ge id ofs))
+  = Genv.symbol_address ge id ofs.
 Proof.
   intros. rewrite Val.add_commut. apply low_high_half.
 Qed.
 
 Lemma csymbol_high_low_2:
-  forall ge id ofs rel,
+  forall (ge: genv) id ofs rel,
   Val.add (const_high ge (csymbol_high id ofs rel))
-          (const_low ge (csymbol_low id ofs rel)) = symbol_offset ge id ofs.
+          (const_low ge (csymbol_low id ofs rel)) = Genv.symbol_address ge id ofs.
 Proof.
   intros. destruct rel; apply csymbol_high_low. 
 Qed.
 
-(*
-Lemma csymbol_sda_eq:
-  forall ge id ofs,
-  symbol_is_small_data id ofs = true ->
-  Val.add Vzero (const_low ge (Csymbol_sda id ofs)) = symbol_offset ge id ofs.
-Proof.
-  intros. unfold const_low. rewrite small_data_area_addressing by auto. 
-  unfold symbol_offset. 
-  destruct (Genv.find_symbol ge id); simpl; auto. rewrite Int.add_zero; auto.
-Qed.
-*)
-
 (** Useful properties of the GPR0 registers. *)
 
 Lemma gpr_or_zero_not_zero:
@@ -859,18 +847,17 @@ Opaque Int.eq.
   destruct (loadimm_correct x i k rs m) as [rs' [A [B C]]]. 
   exists rs'. auto with asmgen. 
   (* Oaddrsymbol *)
-  change (symbol_address ge i i0) with (symbol_offset ge i i0).
-  set (v' := symbol_offset ge i i0).
+  set (v' := Genv.symbol_address ge i i0).
   destruct (symbol_is_small_data i i0) eqn:SD.
   (* small data *)
 Opaque Val.add.
   econstructor; split. apply exec_straight_one; simpl; reflexivity.
-  split. Simpl. rewrite small_data_area_addressing by auto. apply add_zero_symbol_offset.
+  split. Simpl. rewrite small_data_area_addressing by auto. apply add_zero_symbol_address.
   intros; Simpl.
   (* not small data *)
   econstructor; split. eapply exec_straight_two; simpl; reflexivity.
   split. Simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. Simpl.
-  rewrite Val.add_assoc. rewrite csymbol_high_low_2. apply add_zero_symbol_offset. 
+  rewrite Val.add_assoc. rewrite csymbol_high_low_2. apply add_zero_symbol_address. 
   intros; Simpl. 
   (* Oaddrstack *)
   destruct (addimm_correct x GPR1 i k rs m) as [rs' [EX [RES OTH]]]; eauto with asmgen.
@@ -883,14 +870,14 @@ Opaque Val.add.
   (* small data *)
   econstructor; split. eapply exec_straight_two; simpl; reflexivity. 
   split. Simpl. rewrite (Val.add_commut (rs x)). f_equal.
-  rewrite small_data_area_addressing by auto. apply add_zero_symbol_offset.
+  rewrite small_data_area_addressing by auto. apply add_zero_symbol_address.
   intros; Simpl.
   destruct (symbol_is_rel_data i i0).
   (* relative data *)
   econstructor; split. eapply exec_straight_three; simpl; reflexivity. 
   split. Simpl. rewrite gpr_or_zero_zero. rewrite gpr_or_zero_not_zero by (eauto with asmgen).
   Simpl. rewrite Val.add_assoc. rewrite (Val.add_commut (rs x)). f_equal. 
-  rewrite Val.add_assoc. rewrite csymbol_high_low. apply add_zero_symbol_offset.
+  rewrite Val.add_assoc. rewrite csymbol_high_low. apply add_zero_symbol_address.
   intros; Simpl.
   (* absolute data *)
   econstructor; split. eapply exec_straight_two; simpl; reflexivity.
@@ -1023,7 +1010,7 @@ Transparent Val.add.
   destruct (symbol_is_small_data i i0) eqn:SISD; inv TR.
   (* Aglobal from small data *)
   apply MK1. unfold const_low. rewrite small_data_area_addressing by auto. 
-  apply add_zero_symbol_offset.
+  apply add_zero_symbol_address.
   auto.
   (* Aglobal general case *)
   set (rel := symbol_is_rel_data i i0).
@@ -1042,7 +1029,7 @@ Transparent Val.add.
   (* Abased *)
   destruct (symbol_is_small_data i i0) eqn:SISD.
   (* Abased from small data *)
-  set (rs1 := nextinstr (rs#GPR0 <- (symbol_offset ge i i0))).
+  set (rs1 := nextinstr (rs#GPR0 <- (Genv.symbol_address ge i i0))).
   exploit (MK2 x GPR0 rs1 k).
     unfold rs1; Simpl. apply Val.add_commut.
     intros. unfold rs1; Simpl.
@@ -1050,7 +1037,7 @@ Transparent Val.add.
   exists rs'; split. apply exec_straight_step with rs1 m. 
   unfold exec_instr. rewrite gpr_or_zero_zero. f_equal. unfold rs1. f_equal. f_equal. 
   unfold const_low. rewrite small_data_area_addressing; auto.
-  apply add_zero_symbol_offset.
+  apply add_zero_symbol_address.
   reflexivity.
   assumption. assumption.
   destruct (symbol_is_rel_data i i0).
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index a28d908..584865a 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -49,7 +49,7 @@ Hypothesis MATCH: ematch bc rs ae.
 
 Lemma match_G:
   forall r id ofs,
-  AE.get r ae = Ptr(Gl id ofs) -> Val.lessdef rs#r (symbol_address ge id ofs).
+  AE.get r ae = Ptr(Gl id ofs) -> Val.lessdef rs#r (Genv.symbol_address ge id ofs).
 Proof.
   intros. apply vmatch_ptr_gl with bc; auto. rewrite <- H. apply MATCH. 
 Qed.
@@ -82,7 +82,7 @@ Ltac SimplVM :=
       rewrite E in *; clear H; SimplVM
   | [ H: vmatch _ ?v (Ptr(Gl ?id ?ofs)) |- _ ] =>
       let E := fresh in
-      assert (E: Val.lessdef v (Op.symbol_address ge id ofs)) by (eapply vmatch_ptr_gl; eauto); 
+      assert (E: Val.lessdef v (Genv.symbol_address ge id ofs)) by (eapply vmatch_ptr_gl; eauto); 
       clear H; SimplVM
   | [ H: vmatch _ ?v (Ptr(Stk ?ofs)) |- _ ] =>
       let E := fresh in
@@ -436,13 +436,6 @@ Proof.
   exists v; auto.
 Qed.
 
-Remark shift_symbol_address:
-  forall symb ofs n,
-  Op.symbol_address ge symb (Int.add ofs n) = Val.add (Op.symbol_address ge symb ofs) (Vint n).
-Proof.
-  unfold Op.symbol_address; intros. destruct (Genv.find_symbol ge symb); auto. 
-Qed.
-
 Lemma addr_strength_reduction_correct:
   forall addr args vl res,
   vl = map (fun r => AE.get r ae) args ->
@@ -453,8 +446,8 @@ Proof.
   intros until res. unfold addr_strength_reduction.
   destruct (addr_strength_reduction_match addr args vl); simpl;
   intros VL EA; InvApproxRegs; SimplVM; try (inv EA).
-- rewrite shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto. 
-- fold (Val.add (Vint n1) rs#r2). rewrite Int.add_commut. rewrite shift_symbol_address. rewrite Val.add_commut.
+- rewrite Genv.shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto. 
+- fold (Val.add (Vint n1) rs#r2). rewrite Int.add_commut. rewrite Genv.shift_symbol_address. rewrite Val.add_commut.
   econstructor; split; eauto. apply Val.add_lessdef; auto.
 - rewrite Int.add_zero_l. 
   change (Vptr sp (Int.add n1 n2)) with (Val.add (Vptr sp n1) (Vint n2)).
@@ -467,8 +460,8 @@ Proof.
 - fold (Val.add (Vint n1) rs#r2).
   rewrite Val.add_commut. econstructor; split; eauto.
 - econstructor; split; eauto.
-- rewrite shift_symbol_address. econstructor; split; eauto. 
-- rewrite shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto. 
+- rewrite Genv.shift_symbol_address. econstructor; split; eauto. 
+- rewrite Genv.shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto. 
 - rewrite Int.add_zero_l.  
   change (Vptr sp (Int.add n1 n)) with (Val.add (Vptr sp n1) (Vint n)).
   econstructor; split; eauto. apply Val.add_lessdef; auto.
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 3545b18..17cf072 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -147,12 +147,6 @@ Global Opaque eq_condition eq_addressing eq_operation.
 
 (** * Evaluation functions *)
 
-Definition symbol_address (F V: Type) (genv: Genv.t F V) (id: ident) (ofs: int) : val :=
-  match Genv.find_symbol genv id with
-  | Some b => Vptr b ofs
-  | None => Vundef
-  end.
-
 (** Evaluation of conditions, operators and addressing modes applied
   to lists of values.  Return [None] when the computation can trigger an
   error, e.g. integer division by zero.  [eval_condition] returns a boolean,
@@ -178,13 +172,13 @@ Definition eval_operation
   | Omove, v1::nil => Some v1
   | Ointconst n, nil => Some (Vint n)
   | Ofloatconst n, nil => Some (Vfloat n)
-  | Oaddrsymbol s ofs, nil => Some (symbol_address genv s ofs) 
+  | Oaddrsymbol s ofs, nil => Some (Genv.symbol_address genv s ofs) 
   | Oaddrstack ofs, nil => Some (Val.add sp (Vint ofs))
   | Ocast8signed, v1::nil => Some (Val.sign_ext 8 v1)
   | Ocast16signed, v1::nil => Some (Val.sign_ext 16 v1)
   | Oadd, v1::v2::nil => Some (Val.add v1 v2)
   | Oaddimm n, v1::nil => Some (Val.add v1 (Vint n))
-  | Oaddsymbol s ofs, v1::nil => Some (Val.add (symbol_address genv s ofs) v1)
+  | Oaddsymbol s ofs, v1::nil => Some (Val.add (Genv.symbol_address genv s ofs) v1)
   | Osub, v1::v2::nil => Some (Val.sub v1 v2)
   | Osubimm n, v1::nil => Some (Val.sub (Vint n) v1)
   | Omul, v1::v2::nil => Some (Val.mul v1 v2)
@@ -235,8 +229,8 @@ Definition eval_addressing
   match addr, vl with
   | Aindexed n, v1::nil => Some (Val.add v1 (Vint n))
   | Aindexed2, v1::v2::nil => Some (Val.add v1 v2)
-  | Aglobal s ofs, nil => Some (symbol_address genv s ofs)
-  | Abased s ofs, v1::nil => Some (Val.add (symbol_address genv s ofs) v1)
+  | Aglobal s ofs, nil => Some (Genv.symbol_address genv s ofs)
+  | Abased s ofs, v1::nil => Some (Val.add (Genv.symbol_address genv s ofs) v1)
   | Ainstack ofs, nil => Some(Val.add sp (Vint ofs))
   | _, _ => None
   end.
@@ -350,13 +344,13 @@ Proof with (try exact I).
   congruence.
   exact I.
   destruct (Float.is_single_dec f); auto. 
-  unfold symbol_address. destruct (Genv.find_symbol genv i)...
+  unfold Genv.symbol_address. destruct (Genv.find_symbol genv i)...
   destruct sp...
   destruct v0...
   destruct v0...
   destruct v0; destruct v1...
   destruct v0...
-  unfold symbol_address. destruct (Genv.find_symbol genv i)... destruct v0...
+  unfold Genv.symbol_address. destruct (Genv.find_symbol genv i)... destruct v0...
   destruct v0; destruct v1... simpl. destruct (eq_block b b0)...
   destruct v0...
   destruct v0; destruct v1...
@@ -521,8 +515,8 @@ Lemma eval_offset_addressing:
 Proof.
   intros. destruct addr; simpl in H; inv H; simpl in *; FuncInv; subst.
   rewrite Val.add_assoc; auto.
-  unfold symbol_address. destruct (Genv.find_symbol ge i); auto. 
-  unfold symbol_address. destruct (Genv.find_symbol ge i); auto.
+  unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto. 
+  unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto.
   rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_commut. auto. 
   rewrite Val.add_assoc. auto. 
 Qed.
@@ -615,7 +609,7 @@ Proof.
   destruct v; simpl in *; inv H1; inv H2.
   right. apply Int.no_overlap_sound; auto. 
 (* Aglobal *)
-  unfold symbol_address in *. 
+  unfold Genv.symbol_address in *. 
   destruct (Genv.find_symbol ge i1) eqn:?; inv H2.
   destruct (Genv.find_symbol ge i) eqn:?; inv H1.
   destruct (ident_eq i i1). subst.
@@ -626,7 +620,7 @@ Proof.
   rewrite Int.add_commut; rewrite Int.add_zero; auto.
   left. red; intros; elim n. subst. eapply Genv.genv_vars_inj; eauto.
 (* Abased *)
-  unfold symbol_address in *. 
+  unfold Genv.symbol_address in *. 
   destruct (Genv.find_symbol ge i1) eqn:?; simpl in *; try discriminate.
   destruct v; inv H2.
   destruct (Genv.find_symbol ge i) eqn:?; inv H1.
@@ -655,9 +649,9 @@ Hypothesis agree_on_symbols:
   forall (s: ident), Genv.find_symbol ge2 s = Genv.find_symbol ge1 s.
 
 Remark symbol_address_preserved:
-  forall s ofs, symbol_address ge2 s ofs = symbol_address ge1 s ofs.
+  forall s ofs, Genv.symbol_address ge2 s ofs = Genv.symbol_address ge1 s ofs.
 Proof.
-  unfold symbol_address; intros. rewrite agree_on_symbols; auto.
+  unfold Genv.symbol_address; intros. rewrite agree_on_symbols; auto.
 Qed.
  
 Lemma eval_operation_preserved:
@@ -686,7 +680,7 @@ Variable f: meminj.
 
 Hypothesis symbol_address_inj: 
   forall id ofs,
-  val_inject f (symbol_address genv id ofs) (symbol_address genv id ofs).
+  val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs).
 
 Variable m1: mem.
 Variable m2: mem.
@@ -956,9 +950,9 @@ Variable delta: Z.
 Hypothesis sp_inj: f sp1 = Some(sp2, delta).
 
 Remark symbol_address_inject:
-  forall id ofs, val_inject f (symbol_address genv id ofs) (symbol_address genv id ofs).
+  forall id ofs, val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs).
 Proof.
-  intros. unfold symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto.
+  intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto.
   exploit (proj1 globals); eauto. intros. 
   econstructor; eauto. rewrite Int.add_zero; auto.
 Qed.
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 1aa889b..cb48d51 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -115,7 +115,7 @@ Definition binary_constructor_sound (cstr: expr -> expr -> expr) (sem: val -> va
 
 Theorem eval_addrsymbol:
   forall le id ofs,
-  exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (symbol_address ge id ofs) v.
+  exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (Genv.symbol_address ge id ofs) v.
 Proof.
   intros. unfold addrsymbol. econstructor; split. 
   EvalOp. simpl; eauto. 
@@ -154,13 +154,6 @@ Proof.
   TrivialExists. 
 Qed.
 
-Remark symbol_address_shift:
-  forall s ofs n,
-  symbol_address ge s (Int.add ofs n) = Val.add (symbol_address ge s ofs) (Vint n).
-Proof.
-  unfold symbol_address; intros. destruct (Genv.find_symbol ge s); auto. 
-Qed.
-
 Theorem eval_addimm:
   forall n, unary_constructor_sound (addimm n) (fun x => Val.add x (Vint n)).
 Proof.
@@ -170,19 +163,19 @@ Proof.
   destruct x; simpl; auto. rewrite Int.add_zero. auto. rewrite Int.add_zero. auto.
   case (addimm_match a); intros; InvEval; simpl; TrivialExists; simpl.
   rewrite Int.add_commut. auto.
-  unfold symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. rewrite Int.add_commut; auto.
+  unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. rewrite Int.add_commut; auto.
   rewrite Val.add_assoc. rewrite Int.add_commut. auto.
   subst. rewrite Val.add_assoc. rewrite Int.add_commut. auto.
-  subst. rewrite Int.add_commut. rewrite symbol_address_shift. rewrite ! Val.add_assoc. f_equal. f_equal. apply Val.add_commut.
+  subst. rewrite Int.add_commut. rewrite Genv.shift_symbol_address. rewrite ! Val.add_assoc. f_equal. f_equal. apply Val.add_commut.
 Qed. 
 
 Theorem eval_addsymbol:
-  forall s ofs, unary_constructor_sound (addsymbol s ofs) (Val.add (symbol_address ge s ofs)).
+  forall s ofs, unary_constructor_sound (addsymbol s ofs) (Val.add (Genv.symbol_address ge s ofs)).
 Proof.
   red; unfold addsymbol; intros until x.
   case (addsymbol_match a); intros; InvEval; simpl; TrivialExists; simpl.
-  rewrite symbol_address_shift. auto. 
-  rewrite symbol_address_shift. subst x. rewrite Val.add_assoc. f_equal. f_equal. 
+  rewrite Genv.shift_symbol_address. auto. 
+  rewrite Genv.shift_symbol_address. subst x. rewrite Val.add_assoc. f_equal. f_equal. 
   apply Val.add_commut.
 Qed.
 
@@ -209,9 +202,9 @@ Proof.
     simpl. repeat rewrite Val.add_assoc. decEq; decEq.
     rewrite Val.add_commut. rewrite Val.add_permut. auto.
 - replace (Val.add x y) with
-    (Val.add (symbol_address ge s (Int.add ofs n)) (Val.add v1 v0)).
+    (Val.add (Genv.symbol_address ge s (Int.add ofs n)) (Val.add v1 v0)).
   apply eval_addsymbol; auto. EvalOp. 
-  subst. rewrite symbol_address_shift. rewrite ! Val.add_assoc. f_equal. 
+  subst. rewrite Genv.shift_symbol_address. rewrite ! Val.add_assoc. f_equal. 
   rewrite Val.add_permut. f_equal. apply Val.add_commut.
 - subst. rewrite Val.add_assoc. apply eval_addsymbol. EvalOp. 
 - subst. rewrite <- Val.add_assoc. apply eval_addimm. EvalOp.
diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v
index 7f16bb3..77463f4 100644
--- a/powerpc/ValueAOp.v
+++ b/powerpc/ValueAOp.v
@@ -127,7 +127,7 @@ Qed.
 
 Lemma symbol_address_sound:
   forall id ofs,
-  vmatch bc (symbol_address ge id ofs) (Ptr (Gl id ofs)).
+  vmatch bc (Genv.symbol_address ge id ofs) (Ptr (Gl id ofs)).
 Proof.
   intros; apply symbol_address_sound; apply GENV.
 Qed.
-- 
cgit v1.2.3