Refactoring: move symbol_offset into Genv.

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

6 files changed, 20 insertions, 32 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.