From 513489eb97c2b99f5ad901a0f26b493e99bbec1a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 2 Mar 2016 10:35:21 +0100 Subject: Make casts of pointers to _Bool semantically well defined (again). In compCert 2.5 the semantics of pointer comparisons against the NULL pointer was made more accurate by making it undefined if the pointer is invalid (outside bounds). Technical difficulties prevented this change from being propagated to the semantics of casts from pointer types to the _Bool type, which involves an implicit pointer comparison against NULL. Hence, this kind of casts was temporarily given undefined semantics. This commit makes pointer-to-_Bool casts semantically defined (again), provided the pointer is valid. This reinstates the equivalence between casts to _Bool and comparisons != 0. The technical difficulties mentioned above came from the translation of assignments in a value context in the SimplExpr pass. The pass was lightly modified to work around the issue. --- cfrontend/SimplExprproof.v | 37 +++++++++++++++++++++++++++---------- 1 file changed, 27 insertions(+), 10 deletions(-) (limited to 'cfrontend/SimplExprproof.v') diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 0c7c9ce7..8baa7d46 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -752,12 +752,27 @@ Qed. (** Semantics of smart constructors *) +Remark sem_cast_deterministic: + forall v ty ty' m1 v1 m2 v2, + sem_cast v ty ty' m1 = Some v1 -> + sem_cast v ty ty' m2 = Some v2 -> + v1 = v2. +Proof. + unfold sem_cast; intros. destruct (classify_cast ty ty'); try congruence. + destruct v; try congruence. + destruct (Mem.weak_valid_pointer m1 b (Int.unsigned i)); inv H. + destruct (Mem.weak_valid_pointer m2 b (Int.unsigned i)); inv H0. + auto. +Qed. + Lemma eval_simpl_expr_sound: forall e le m a v, eval_expr tge e le m a v -> match eval_simpl_expr a with Some v' => v' = v | None => True end. Proof. induction 1; simpl; auto. - destruct (eval_simpl_expr a); auto. subst. rewrite H0. auto. + destruct (eval_simpl_expr a); auto. subst. + destruct (sem_cast v1 (typeof a) ty Mem.empty) as [v'|] eqn:C; auto. + eapply sem_cast_deterministic; eauto. inv H; simpl; auto. Qed. @@ -811,7 +826,7 @@ Lemma step_make_assign: Csem.assign_loc ge ty m b ofs v t m' -> eval_lvalue tge e le m a1 b ofs -> eval_expr tge e le m a2 v2 -> - sem_cast v2 (typeof a2) ty = Some v -> + sem_cast v2 (typeof a2) ty m = Some v -> typeof a1 = ty -> step1 tge (State f (make_assign a1 a2) k e le m) t (State f Sskip k e le m'). @@ -1649,18 +1664,19 @@ Proof. (* for value *) exploit tr_simple_rvalue; eauto. intros [SL2 [TY2 EV2]]. exploit tr_simple_lvalue. eauto. - eapply tr_expr_invariant with (le' := PTree.set t0 v le). eauto. + eapply tr_expr_invariant with (le' := PTree.set t0 v' le). eauto. intros. apply PTree.gso. intuition congruence. intros [SL1 [TY1 EV1]]. subst; simpl Kseqlist. econstructor; split. left. eapply plus_left. constructor. - eapply star_left. constructor. eauto. + eapply star_left. constructor. econstructor. eauto. rewrite <- TY2; eauto. eapply star_left. constructor. apply star_one. eapply step_make_assign; eauto. - constructor. apply PTree.gss. reflexivity. reflexivity. traceEq. + constructor. apply PTree.gss. simpl. eapply cast_idempotent; eauto. + reflexivity. reflexivity. traceEq. econstructor. auto. apply S. - apply tr_val_gen. auto. intros. econstructor; eauto. constructor. + apply tr_val_gen. auto. intros. constructor. rewrite H4; auto. apply PTree.gss. intros. apply PTree.gso. intuition congruence. auto. auto. @@ -1692,7 +1708,7 @@ Proof. exploit tr_simple_rvalue. eauto. eapply tr_expr_invariant with (le := le) (le' := le'). eauto. intros. apply INV. NOTIN. simpl. intros [SL2 [TY2 EV2]]. exploit tr_simple_lvalue. eauto. - eapply tr_expr_invariant with (le := le) (le' := PTree.set t v3 le'). eauto. + eapply tr_expr_invariant with (le := le) (le' := PTree.set t v4 le'). eauto. intros. rewrite PTree.gso. apply INV. NOTIN. intuition congruence. intros [? [? EV1'']]. subst; simpl Kseqlist. @@ -1700,13 +1716,14 @@ Proof. left. rewrite app_ass. rewrite Kseqlist_app. eapply star_plus_trans. eexact EXEC. simpl. eapply plus_four. econstructor. econstructor. - econstructor. eexact EV3. eexact EV2. + econstructor. econstructor. eexact EV3. eexact EV2. rewrite TY3; rewrite <- TY1; rewrite <- TY2; rewrite comp_env_preserved; eauto. + eassumption. econstructor. eapply step_make_assign; eauto. - constructor. apply PTree.gss. + constructor. apply PTree.gss. simpl. eapply cast_idempotent; eauto. reflexivity. traceEq. econstructor. auto. apply S. - apply tr_val_gen. auto. intros. econstructor; eauto. constructor. + apply tr_val_gen. auto. intros. constructor. rewrite H10; auto. apply PTree.gss. intros. rewrite PTree.gso. apply INV. red; intros; elim H10; auto. -- cgit From 21613d7ad098ce4a080963aa4210ce208d24e9b3 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 6 Mar 2016 10:33:19 +0100 Subject: Update the proofs of the C front-end to the new linking framework. --- cfrontend/SimplExprproof.v | 130 ++++++++++++++++++++------------------------- 1 file changed, 59 insertions(+), 71 deletions(-) (limited to 'cfrontend/SimplExprproof.v') diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 0c7c9ce7..c6e0a44b 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -12,30 +12,34 @@ (** Correctness proof for expression simplification. *) -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Errors. -Require Import Integers. -Require Import Values. -Require Import Memory. -Require Import Events. -Require Import Smallstep. -Require Import Globalenvs. -Require Import Ctypes. -Require Import Cop. -Require Import Csyntax. -Require Import Csem. -Require Import Cstrategy. -Require Import Clight. -Require Import SimplExpr. -Require Import SimplExprspec. +Require Import Coqlib Maps Errors Integers. +Require Import AST Linking. +Require Import Values Memory Events Globalenvs Smallstep. +Require Import Ctypes Cop Csyntax Csem Cstrategy Clight. +Require Import SimplExpr SimplExprspec. + +(** ** Relational specification of the translation. *) + +Definition match_prog (p: Csyntax.program) (tp: Clight.program) := + match_program (fun ctx f tf => tr_fundef f tf) eq p tp + /\ prog_types tp = prog_types p. + +Lemma transf_program_match: + forall p tp, transl_program p = OK tp -> match_prog p tp. +Proof. + unfold transl_program; intros. monadInv H. split; auto. + unfold program_of_program; simpl. destruct x; simpl. + eapply match_transform_partial_program_contextual. eexact EQ. + intros. apply transl_fundef_spec; auto. +Qed. + +(** ** Semantic preservation *) Section PRESERVATION. Variable prog: Csyntax.program. Variable tprog: Clight.program. -Hypothesis TRANSL: transl_program prog = OK tprog. +Hypothesis TRANSL: match_prog prog tprog. Let ge := Csem.globalenv prog. Let tge := Clight.globalenv tprog. @@ -45,22 +49,17 @@ Let tge := Clight.globalenv tprog. Lemma comp_env_preserved: Clight.genv_cenv tge = Csem.genv_cenv ge. Proof. - monadInv TRANSL. unfold tge; rewrite <- H0; auto. + simpl. destruct TRANSL. generalize (prog_comp_env_eq tprog) (prog_comp_env_eq prog). + congruence. Qed. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof. - intros. eapply Genv.find_symbol_match. eapply transl_program_spec; eauto. - simpl. tauto. -Qed. +Proof (Genv.find_symbol_match (proj1 TRANSL)). -Lemma public_preserved: - forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. -Proof. - intros. eapply Genv.public_symbol_match. eapply transl_program_spec; eauto. - simpl. tauto. -Qed. +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_match (proj1 TRANSL)). Lemma function_ptr_translated: forall b f, @@ -68,9 +67,8 @@ Lemma function_ptr_translated: exists tf, Genv.find_funct_ptr tge b = Some tf /\ tr_fundef f tf. Proof. - intros. eapply Genv.find_funct_ptr_match. - eapply transl_program_spec; eauto. - assumption. + intros. + edestruct (Genv.find_funct_ptr_match (proj1 TRANSL)) as (ctx & tf & A & B & C); eauto. Qed. Lemma functions_translated: @@ -79,27 +77,8 @@ Lemma functions_translated: exists tf, Genv.find_funct tge v = Some tf /\ tr_fundef f tf. Proof. - intros. eapply Genv.find_funct_match. - eapply transl_program_spec; eauto. - assumption. -Qed. - -Lemma varinfo_preserved: - forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. -Proof. - intros. destruct (Genv.find_var_info ge b) as [v|] eqn:V. -- exploit Genv.find_var_info_match. eapply transl_program_spec; eauto. eassumption. - intros [tv [A B]]. inv B. assumption. -- destruct (Genv.find_var_info tge b) as [v'|] eqn:V'; auto. - exploit Genv.find_var_info_rev_match. eapply transl_program_spec; eauto. eassumption. - simpl. destruct (plt b (Genv.genv_next (Genv.globalenv prog))); try tauto. - intros [v [A B]]. inv B. change (Genv.globalenv prog) with (Csem.genv_genv ge) in A. congruence. -Qed. - -Lemma block_is_volatile_preserved: - forall b, Genv.block_is_volatile tge b = Genv.block_is_volatile ge b. -Proof. - intros. unfold Genv.block_is_volatile. rewrite varinfo_preserved. auto. + intros. + edestruct (Genv.find_funct_match (proj1 TRANSL)) as (ctx & tf & A & B & C); eauto. Qed. Lemma type_of_fundef_preserved: @@ -167,8 +146,7 @@ Proof. (* By_value, not volatile *) rewrite H1. split; auto. eapply deref_loc_value; eauto. (* By_value, volatile *) - rewrite H0; rewrite H1. eapply volatile_load_preserved with (ge1 := ge); auto. - exact symbols_preserved. exact public_preserved. exact block_is_volatile_preserved. + rewrite H0; rewrite H1. eapply volatile_load_preserved with (ge1 := ge); auto. apply senv_preserved. (* By reference *) rewrite H0. destruct (type_is_volatile ty); split; auto; eapply deref_loc_reference; eauto. (* By copy *) @@ -187,8 +165,7 @@ Proof. (* By_value, not volatile *) rewrite H1. split; auto. eapply assign_loc_value; eauto. (* By_value, volatile *) - rewrite H0; rewrite H1. eapply volatile_store_preserved with (ge1 := ge); auto. - exact symbols_preserved. exact public_preserved. exact block_is_volatile_preserved. + rewrite H0; rewrite H1. eapply volatile_store_preserved with (ge1 := ge); auto. apply senv_preserved. (* By copy *) rewrite H0. rewrite <- comp_env_preserved in *. destruct (type_is_volatile ty); split; auto; eapply assign_loc_copy; eauto. @@ -1890,8 +1867,7 @@ Proof. econstructor; split. left. eapply plus_left. constructor. apply star_one. econstructor; eauto. - eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. traceEq. econstructor; eauto. change sl2 with (nil ++ sl2). apply S. constructor. simpl; auto. auto. @@ -1901,8 +1877,7 @@ Proof. econstructor; split. left. eapply plus_left. constructor. apply star_one. econstructor; eauto. - eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. traceEq. econstructor; eauto. change sl2 with (nil ++ sl2). apply S. @@ -2198,8 +2173,7 @@ Proof. inv H5. econstructor; split. left; apply plus_one. econstructor; eauto. - eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. constructor; auto. (* return *) @@ -2229,15 +2203,14 @@ Lemma transl_initial_states: Csem.initial_state prog S -> exists S', Clight.initial_state tprog S' /\ match_states S S'. Proof. - intros. inv H. generalize TRANSL; intros TR; monadInv TR. rewrite H4. - exploit transl_program_spec; eauto. intros MP. + intros. inv H. exploit function_ptr_translated; eauto. intros [tf [FIND TR]]. econstructor; split. econstructor. - exploit Genv.init_mem_match; eauto. - change (Genv.globalenv tprog) with (genv_genv tge). - rewrite symbols_preserved. rewrite <- H4; simpl. - rewrite (transform_partial_program_main _ _ EQ). eauto. + eapply (Genv.init_mem_match (proj1 TRANSL)); eauto. + replace (prog_main tprog) with (prog_main prog). + rewrite symbols_preserved. eauto. + destruct TRANSL. destruct H as (A & B & C). simpl in B. auto. eexact FIND. rewrite <- H3. apply type_of_fundef_preserved. auto. constructor. auto. constructor. @@ -2254,7 +2227,7 @@ Theorem transl_program_correct: forward_simulation (Cstrategy.semantics prog) (Clight.semantics1 tprog). Proof. eapply forward_simulation_star_wf with (order := ltof _ measure). - eexact public_preserved. + eapply senv_preserved. eexact transl_initial_states. eexact transl_final_states. apply well_founded_ltof. @@ -2262,3 +2235,18 @@ Proof. Qed. End PRESERVATION. + +(** ** Commutation with linking *) + +Instance TransfSimplExprLink : TransfLink match_prog. +Proof. + red; intros. eapply Ctypes.link_match_program; eauto. +- intros. +Local Transparent Linker_fundef. + simpl in *; unfold link_fundef in *. inv H3; inv H4; try discriminate. + destruct ef; inv H2. exists (Internal tf); split; auto. constructor; auto. + destruct ef; inv H2. exists (Internal tf); split; auto. constructor; auto. + destruct (external_function_eq ef ef0 && typelist_eq targs targs0 && + type_eq tres tres0 && calling_convention_eq cconv cconv0); inv H2. + exists (External ef targs tres cconv); split; auto. constructor. +Qed. -- cgit