Refactoring: move symbol_offset into Genv.

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

7 files changed, 61 insertions, 100 deletions

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.