From 64bacbbc939551a47bb03371d0f1a065af1e278c Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 6 Dec 2007 14:17:23 +0000 Subject: Ajout find_symbol_not_nullptr; nettoyages git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@455 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Globalenvs.v | 110 +++++++++++++++++++++++++++++++++------------------- 1 file changed, 71 insertions(+), 39 deletions(-) (limited to 'common/Globalenvs.v') diff --git a/common/Globalenvs.v b/common/Globalenvs.v index 66140d16..7ace0cf1 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -114,6 +114,9 @@ Module Type GENV. Hypothesis find_symbol_not_fresh: forall (F V: Set) (p: program F V) (id: ident) (b: block), find_symbol (globalenv p) id = Some b -> b < nextblock (init_mem p). + Hypothesis find_symbol_not_nullptr: + forall (F V: Set) (p: program F V) (id: ident) (b: block), + find_symbol (globalenv p) id = Some b -> b <> nullptr. Hypothesis global_addresses_distinct: forall (F V: Set) (p: program F V) id1 id2 b1 b2, id1<>id2 -> @@ -458,30 +461,30 @@ Proof. intros. eauto. Qed. -Remark find_symbol_add_functs_neg: +Remark find_symbol_add_functs_negative: forall (fns: list (ident * F)) s b, - find_symbol (add_functs empty fns) s = Some b -> - b < 0. + (symbols (add_functs empty fns)) ! s = Some b -> b < 0. Proof. - unfold find_symbol. induction fns; simpl; intros until b. + induction fns; simpl; intros until b. rewrite PTree.gempty. congruence. rewrite PTree.gsspec. destruct a; simpl. case (peq s i); intro. intro EQ; inversion EQ. apply nextfunction_add_functs_neg. eauto. Qed. -Remark find_symbol_add_globals_not_fresh: - forall (fns: list (ident * F)) (vars: list (ident * list init_data * V)) g m s b, +Remark find_symbol_add_symbols_not_fresh: + forall fns vars g m s b, add_globals (add_functs empty fns, Mem.empty) vars = (g, m) -> (symbols g)!s = Some b -> b < nextblock m. Proof. induction vars; simpl; intros until b. - intros. inv H. simpl. generalize (find_symbol_add_functs_neg _ _ H0). omega. + intros. inversion H. subst g m. simpl. + generalize (find_symbol_add_functs_negative fns s H0). omega. + Transparent alloc_init_data. destruct a as [[id1 init1] info1]. caseEq (add_globals (add_functs empty fns, Mem.empty) vars). - Transparent alloc_init_data. unfold alloc_init_data. - intros g1 m1 ADG EQ. inv EQ. + intros g1 m1 ADG EQ. inversion EQ; subst g m; clear EQ. unfold add_symbol; simpl. rewrite PTree.gsspec. case (peq s id1); intro. intro EQ; inversion EQ. omega. intro. generalize (IHvars _ _ _ _ ADG H). omega. @@ -494,22 +497,18 @@ Proof. intros until b. unfold find_symbol, globalenv, init_mem, globalenv_initmem; simpl. caseEq (add_globals (add_functs empty (prog_funct p), Mem.empty) (prog_vars p)); intros g m EQ. - simpl; intros. eapply find_symbol_add_globals_not_fresh; eauto. + simpl; intros. eapply find_symbol_add_symbols_not_fresh; eauto. Qed. -End GENV. - -(* Invariants on functions *) - Lemma find_symbol_exists: - forall (F V: Set) (p: program F V) + forall (p: program F V) (id: ident) (init: list init_data) (v: V), In (id, init, v) (prog_vars p) -> exists b, find_symbol (globalenv p) id = Some b. Proof. intros until v. assert (forall initm vl, In (id, init, v) vl -> - exists b, PTree.get id (@symbols F (fst (add_globals initm vl))) = Some b). + exists b, PTree.get id (symbols (fst (add_globals initm vl))) = Some b). induction vl; simpl; intros. elim H. destruct a as [[id0 init0] v0]. @@ -520,8 +519,8 @@ Proof. Qed. Remark find_symbol_above_nextfunction: - forall (F: Set) (id: ident) (b: block) (fns: list (ident * F)), - let g := add_functs (empty F) fns in + forall (id: ident) (b: block) (fns: list (ident * F)), + let g := add_functs empty fns in PTree.get id g.(symbols) = Some b -> b > g.(nextfunction). Proof. @@ -533,7 +532,7 @@ Proof. Qed. Remark find_symbol_add_globals: - forall (F V: Set) (id: ident) (ge_m: t F * mem) (vars: list (ident * list init_data * V)), + forall (id: ident) (ge_m: t * mem) (vars: list (ident * list init_data * V)), ~In id (map (fun x: ident * list init_data * V => fst(fst x)) vars) -> find_symbol (fst (add_globals ge_m vars)) id = find_symbol (fst ge_m) id. @@ -547,7 +546,7 @@ Proof. Qed. Lemma find_funct_ptr_exists: - forall (F V: Set) (p: program F V) (id: ident) (f: F), + forall (p: program F V) (id: ident) (f: F), list_norepet (prog_funct_names p) -> list_disjoint (prog_funct_names p) (prog_var_names p) -> In (id, f) (prog_funct p) -> @@ -558,8 +557,8 @@ Proof. assert (forall (fns: list (ident * F)), list_norepet (map (@fst ident F) fns) -> In (id, f) fns -> - exists b, find_symbol (add_functs (empty F) fns) id = Some b - /\ find_funct_ptr (add_functs (empty F) fns) b = Some f). + exists b, find_symbol (add_functs empty fns) id = Some b + /\ find_funct_ptr (add_functs empty fns) b = Some f). unfold find_symbol, find_funct_ptr. induction fns; intros. elim H0. destruct a as [id0 f0]; simpl in *. inv H. @@ -585,25 +584,25 @@ Proof. Qed. Lemma find_funct_ptr_inversion: - forall (F V: Set) (P: F -> Prop) (p: program F V) (b: block) (f: F), + forall (P: F -> Prop) (p: program F V) (b: block) (f: F), find_funct_ptr (globalenv p) b = Some f -> exists id, In (id, f) (prog_funct p). Proof. intros until f. assert (forall fns: list (ident * F), - find_funct_ptr (add_functs (empty F) fns) b = Some f -> + find_funct_ptr (add_functs empty fns) b = Some f -> exists id, In (id, f) fns). unfold find_funct_ptr. induction fns; simpl. rewrite ZMap.gi. congruence. destruct a as [id0 f0]; simpl. - rewrite ZMap.gsspec. destruct (ZIndexed.eq b (nextfunction (add_functs (empty F) fns))). + rewrite ZMap.gsspec. destruct (ZIndexed.eq b (nextfunction (add_functs empty fns))). intro. inv H. exists id0; auto. intro. exploit IHfns; eauto. intros [id A]. exists id; auto. unfold find_funct_ptr; rewrite functions_globalenv. intros; apply H; auto. Qed. Lemma find_funct_ptr_prop: - forall (F V: Set) (P: F -> Prop) (p: program F V) (b: block) (f: F), + forall (P: F -> Prop) (p: program F V) (b: block) (f: F), (forall id f, In (id, f) (prog_funct p) -> P f) -> find_funct_ptr (globalenv p) b = Some f -> P f. @@ -612,7 +611,7 @@ Proof. Qed. Lemma find_funct_inversion: - forall (F V: Set) (P: F -> Prop) (p: program F V) (v: val) (f: F), + forall (P: F -> Prop) (p: program F V) (v: val) (f: F), find_funct (globalenv p) v = Some f -> exists id, In (id, f) (prog_funct p). Proof. @@ -622,7 +621,7 @@ Proof. Qed. Lemma find_funct_prop: - forall (F V: Set) (P: F -> Prop) (p: program F V) (v: val) (f: F), + forall (P: F -> Prop) (p: program F V) (v: val) (f: F), (forall id f, In (id, f) (prog_funct p) -> P f) -> find_funct (globalenv p) v = Some f -> P f. @@ -631,20 +630,20 @@ Proof. Qed. Lemma find_funct_ptr_symbol_inversion: - forall (F V: Set) (p: program F V) (id: ident) (b: block) (f: F), + forall (p: program F V) (id: ident) (b: block) (f: F), find_symbol (globalenv p) id = Some b -> find_funct_ptr (globalenv p) b = Some f -> In (id, f) p.(prog_funct). Proof. intros until f. assert (forall fns, - let g := add_functs (empty F) fns in + let g := add_functs empty fns in PTree.get id g.(symbols) = Some b -> ZMap.get b g.(functions) = Some f -> In (id, f) fns). induction fns; simpl. rewrite ZMap.gi. congruence. - set (g := add_functs (empty F) fns). + set (g := add_functs empty fns). rewrite PTree.gsspec. rewrite ZMap.gsspec. case (peq id (fst a)); intro. intro EQ. inversion EQ. unfold ZIndexed.eq. rewrite zeq_true. @@ -653,7 +652,7 @@ Proof. generalize (find_symbol_above_nextfunction _ _ H). fold g. unfold block. omega. assert (forall g0 m0, b < 0 -> forall vars g m, - @add_globals F V (g0, m0) vars = (g, m) -> + add_globals (g0, m0) vars = (g, m) -> PTree.get id g.(symbols) = Some b -> PTree.get id g0.(symbols) = Some b). induction vars; simpl. @@ -667,15 +666,46 @@ Proof. eauto. intros. generalize (find_funct_ptr_negative _ _ H2). intro. - pose (g := add_functs (empty F) (prog_funct p)). + pose (g := add_functs empty (prog_funct p)). apply H. apply H0 with Mem.empty (prog_vars p) (globalenv p) (init_mem p). auto. unfold globalenv, init_mem. rewrite <- surjective_pairing. reflexivity. assumption. rewrite <- functions_globalenv. assumption. Qed. +Theorem find_symbol_not_nullptr: + forall (p: program F V) (id: ident) (b: block), + find_symbol (globalenv p) id = Some b -> b <> nullptr. +Proof. + intros until b. + assert (forall fns, + find_symbol (add_functs empty fns) id = Some b -> + b <> nullptr). + unfold find_symbol; induction fns; simpl. + rewrite PTree.gempty. congruence. + destruct a as [id1 f1]. simpl. rewrite PTree.gsspec. + destruct (peq id id1); intros. + inversion H. generalize (nextfunction_add_functs_neg fns). + unfold block, nullptr; omega. + auto. + set (g0 := add_functs empty p.(prog_funct)). + assert (forall vars g m, + add_globals (g0, Mem.empty) vars = (g, m) -> + find_symbol g id = Some b -> + b <> nullptr). + induction vars; simpl; intros until m. + intros. inversion H0. subst g. apply H with (prog_funct p). auto. + destruct a as [[id1 init1] info1]. + caseEq (add_globals (g0, Mem.empty) vars); intros g1 m1 EQ1 EQ2. + inv EQ2. unfold find_symbol, add_symbol; simpl. rewrite PTree.gsspec. + destruct (peq id id1); intros. + inv H0. generalize (nextblock_pos m1). unfold nullptr, block; omega. + eauto. + intros. eapply H0 with (vars := prog_vars p). apply surjective_pairing. auto. +Qed. + Theorem global_addresses_distinct: - forall (F V: Set) (p: program F V) id1 id2 b1 b2, + forall (p: program F V) id1 id2 b1 b2, id1<>id2 -> find_symbol (globalenv p) id1 = Some b1 -> find_symbol (globalenv p) id2 = Some b2 -> @@ -683,8 +713,8 @@ Theorem global_addresses_distinct: Proof. intros. assert (forall fns, - find_symbol (add_functs (empty F) fns) id1 = Some b1 -> - find_symbol (add_functs (empty F) fns) id2 = Some b2 -> + find_symbol (add_functs empty fns) id1 = Some b1 -> + find_symbol (add_functs empty fns) id2 = Some b2 -> b1 <> b2). unfold find_symbol. induction fns; simpl; intros. rewrite PTree.gempty in H2. discriminate. @@ -697,7 +727,7 @@ Proof. destruct (peq id2 id). subst id. inv H3. generalize (find_symbol_above_nextfunction _ _ H2). unfold block. omega. eauto. - set (ge0 := add_functs (empty F) p.(prog_funct)). + set (ge0 := add_functs empty p.(prog_funct)). assert (forall (vars: list (ident * list init_data * V)) ge m, add_globals (ge0, Mem.empty) vars = (ge, m) -> find_symbol ge id1 = Some b1 -> @@ -710,15 +740,17 @@ Proof. unfold add_symbol. simpl. intros. rewrite PTree.gsspec in H3; destruct (peq id1 id). subst id. inv H3. rewrite PTree.gso in H4; auto. - generalize (find_symbol_add_globals_not_fresh _ _ _ A H4). unfold block; omega. + generalize (find_symbol_add_symbols_not_fresh _ _ _ A H4). unfold block; omega. rewrite PTree.gsspec in H4; destruct (peq id2 id). subst id. inv H4. - generalize (find_symbol_add_globals_not_fresh _ _ _ A H3). unfold block; omega. + generalize (find_symbol_add_symbols_not_fresh _ _ _ A H3). unfold block; omega. eauto. set (ge_m := add_globals (ge0, Mem.empty) p.(prog_vars)). apply H3 with (p.(prog_vars)) (fst ge_m) (snd ge_m). fold ge_m. apply surjective_pairing. auto. auto. Qed. +End GENV. + (* Global environments and program transformations. *) Section MATCH_PROGRAM. -- cgit