From ce4951549999f403446415c135ad1403a16a15c3 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 12 Nov 2012 13:42:22 +0000 Subject: Globalenvs: allocate one-byte block with permissions Nonempty for each function definition, so that comparisons between function pointers are correctly defined. AST, Globalenvs, and many other files: represent programs as a list of (function or variable) definitions instead of two lists, one for functions and the other for variables. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2067 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Stackingproof.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'backend/Stackingproof.v') diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 1cfb738..1d87ad3 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -1734,7 +1734,8 @@ Inductive match_globalenvs (j: meminj) (bound: Z) : Prop := (DOMAIN: forall b, b < bound -> j b = Some(b, 0)) (IMAGE: forall b1 b2 delta, j b1 = Some(b2, delta) -> b2 < bound -> b1 = b2) (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> b < bound) - (INFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound). + (FUNCTIONS: forall b fd, Genv.find_funct_ptr ge b = Some fd -> b < bound) + (VARINFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound). Inductive match_stacks (j: meminj) (m m': mem): list Linear.stackframe -> list stackframe -> signature -> Z -> Z -> Prop := @@ -2170,9 +2171,8 @@ Proof. exploit function_ptr_translated; eauto. intros [tf [A B]]. exists b; exists tf; split; auto. simpl. generalize (AG m0). rewrite EQ. intro INJ. inv INJ. - exploit Genv.find_funct_ptr_negative. unfold ge in FF; eexact FF. intros. - inv MG. rewrite (DOMAIN b) in H2. inv H2. auto. omega. - revert FF. case_eq (Genv.find_symbol ge i); intros; try discriminate. + inv MG. rewrite DOMAIN in H2. inv H2. simpl. auto. eapply FUNCTIONS; eauto. + destruct (Genv.find_symbol ge i) as [b|]_eqn; try discriminate. exploit function_ptr_translated; eauto. intros [tf [A B]]. exists b; exists tf; split; auto. simpl. rewrite symbols_preserved. auto. @@ -2742,6 +2742,7 @@ Proof. intros. unfold Mem.flat_inj. apply zlt_true; auto. unfold Mem.flat_inj; intros. destruct (zlt b1 (Mem.nextblock m0)); congruence. intros. change (Mem.valid_block m0 b0). eapply Genv.find_symbol_not_fresh; eauto. + intros. change (Mem.valid_block m0 b0). eapply Genv.find_funct_ptr_not_fresh; eauto. intros. change (Mem.valid_block m0 b0). eapply Genv.find_var_info_not_fresh; eauto. rewrite H3. red; intros. contradiction. eapply Genv.find_funct_ptr_prop. eexact wt_prog. -- cgit v1.2.3