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, 50 insertions, 75 deletions

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.