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
---
 backend/Constpropproof.v |  6 +++---
 backend/Selectionproof.v |  2 +-
 backend/ValueDomain.v    | 11 ++++-------
 3 files changed, 8 insertions(+), 11 deletions(-)

(limited to 'backend')

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.
-- 
cgit v1.2.3