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/Constpropproof.v | 29 ++++++++++++++++------------- 1 file changed, 16 insertions(+), 13 deletions(-) (limited to 'backend/Constpropproof.v') diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 82284934..f14e87af 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -37,7 +37,7 @@ Variable prog: program. Let tprog := transf_program prog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. -Let gapp := make_global_approx (PTree.empty _) prog.(prog_vars). +Let gapp := make_global_approx (PTree.empty _) prog.(prog_defs). (** * Correctness of the static analysis *) @@ -279,31 +279,34 @@ Definition global_approx_charact (g: genv) (ga: global_approx) : Prop := Genv.find_var_info g b = Some (mkglobvar tt il true false). Lemma make_global_approx_correct: - forall vl g ga, + forall gdl g ga, global_approx_charact g ga -> - global_approx_charact (Genv.add_variables g vl) (make_global_approx ga vl). + global_approx_charact (Genv.add_globals g gdl) (make_global_approx ga gdl). Proof. - induction vl; simpl; intros. + induction gdl; simpl; intros. auto. - destruct a as [id gv]. apply IHvl. + destruct a as [id gd]. apply IHgdl. red; intros. - assert (EITHER: id0 = id /\ gv = mkglobvar tt il true false + assert (EITHER: id0 = id /\ gd = Gvar(mkglobvar tt il true false) \/ id0 <> id /\ ga!id0 = Some il). - destruct (gvar_readonly gv && negb (gvar_volatile gv)) as []_eqn. + destruct gd. + rewrite PTree.grspec in H0. destruct (PTree.elt_eq id0 id); [discriminate|auto]. + destruct (gvar_readonly v && negb (gvar_volatile v)) as []_eqn. rewrite PTree.gsspec in H0. destruct (peq id0 id). inv H0. left. split; auto. - destruct gv; simpl in *. + destruct v; simpl in *. destruct gvar_readonly; try discriminate. destruct gvar_volatile; try discriminate. destruct gvar_info. auto. - right; auto. - rewrite PTree.grspec in H0. destruct (PTree.elt_eq id0 id); try discriminate. - right; auto. - unfold Genv.add_variable, Genv.find_symbol, Genv.find_var_info in *; + auto. + rewrite PTree.grspec in H0. destruct (PTree.elt_eq id0 id); [discriminate|auto]. + + unfold Genv.add_global, Genv.find_symbol, Genv.find_var_info in *; simpl in *. destruct EITHER as [[A B] | [A B]]. subst id0. rewrite PTree.gss in H1. inv H1. rewrite ZMap.gss. auto. - rewrite PTree.gso in H1; auto. rewrite ZMap.gso. eapply H. eauto. auto. + rewrite PTree.gso in H1; auto. destruct gd. eapply H; eauto. + rewrite ZMap.gso. eapply H; eauto. exploit Genv.genv_symb_range; eauto. unfold ZIndexed.t. omega. Qed. -- cgit