diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-05-24 09:46:07 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-05-24 09:46:07 +0000 |
| commit | 3fa79790e617d87584598746296e626e0ce3b256 (patch) | |
| tree | dcdc926130d9ed8d302eedf8215d065c0e787eed /backend | |
| parent | 285d908c5dbd90bff7f03618c7a9e0fa5e287c94 (diff) | |
Refactoring: move symbol_offset into Genv.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2503 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Constpropproof.v | 6 | ||||
| -rw-r--r-- | backend/Selectionproof.v | 2 | ||||
| -rw-r--r-- | backend/ValueDomain.v | 11 |
3 files changed, 8 insertions, 11 deletions
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. |