diff options
Diffstat (limited to 'cfrontend/SimplLocalsproof.v')
| -rw-r--r-- | cfrontend/SimplLocalsproof.v | 208 |
1 files changed, 51 insertions, 157 deletions
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index a47036bf..2cd82d8f 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -13,80 +13,58 @@ (** Semantic preservation for the SimplLocals pass. *) Require Import FSets. -Require FSetAVL. -Require Import Coqlib. -Require Import Errors. -Require Import Ordered. -Require Import AST. -Require Import Maps. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Events. -Require Import Smallstep. -Require Import Ctypes. -Require Import Cop. -Require Import Clight. -Require Import SimplLocals. +Require Import Coqlib Errors Ordered Maps Integers Floats. +Require Import AST Linking. +Require Import Values Memory Globalenvs Events Smallstep. +Require Import Ctypes Cop Clight SimplLocals. Module VSF := FSetFacts.Facts(VSet). Module VSP := FSetProperties.Properties(VSet). +Definition match_prog (p tp: program) : Prop := + match_program (fun ctx f tf => transf_fundef f = OK tf) eq p tp + /\ prog_types tp = prog_types p. + +Lemma match_transf_program: + forall p tp, transf_program p = OK tp -> match_prog p tp. +Proof. + unfold transf_program; intros. monadInv H. + split; auto. apply match_transform_partial_program. rewrite EQ. destruct x; auto. +Qed. + Section PRESERVATION. Variable prog: program. Variable tprog: program. -Hypothesis TRANSF: transf_program prog = OK tprog. +Hypothesis TRANSF: match_prog prog tprog. Let ge := globalenv prog. Let tge := globalenv tprog. Lemma comp_env_preserved: genv_cenv tge = genv_cenv ge. Proof. - monadInv TRANSF. unfold tge; rewrite <- H0; auto. -Qed. - -Lemma transf_programs: - AST.transform_partial_program transf_fundef (program_of_program prog) = OK (program_of_program tprog). -Proof. - monadInv TRANSF. rewrite EQ. destruct x; reflexivity. + unfold tge, ge. destruct prog, tprog; simpl. destruct TRANSF as [_ EQ]. simpl in EQ. congruence. Qed. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof. - exact (Genv.find_symbol_transf_partial _ _ transf_programs). -Qed. +Proof (Genv.find_symbol_match (proj1 TRANSF)). -Lemma public_preserved: - forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. -Proof. - exact (Genv.public_symbol_transf_partial _ _ transf_programs). -Qed. - -Lemma varinfo_preserved: - forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. -Proof. - exact (Genv.find_var_info_transf_partial _ _ transf_programs). -Qed. +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_match (proj1 TRANSF)). Lemma functions_translated: forall (v: val) (f: fundef), Genv.find_funct ge v = Some f -> exists tf, Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf. -Proof. - exact (Genv.find_funct_transf_partial _ _ transf_programs). -Qed. +Proof (Genv.find_funct_transf_partial (proj1 TRANSF)). Lemma function_ptr_translated: forall (b: block) (f: fundef), Genv.find_funct_ptr ge b = Some f -> exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf. -Proof. - exact (Genv.find_funct_ptr_transf_partial _ _ transf_programs). -Qed. +Proof (Genv.find_funct_ptr_transf_partial (proj1 TRANSF)). Lemma type_of_fundef_preserved: forall fd tfd, @@ -201,97 +179,7 @@ Proof. xomegaContradiction. Qed. -(** Properties of values obtained by casting to a given type. *) - -Inductive val_casted: val -> type -> Prop := - | val_casted_int: forall sz si attr n, - cast_int_int sz si n = n -> - val_casted (Vint n) (Tint sz si attr) - | val_casted_float: forall attr n, - val_casted (Vfloat n) (Tfloat F64 attr) - | val_casted_single: forall attr n, - val_casted (Vsingle n) (Tfloat F32 attr) - | val_casted_long: forall si attr n, - val_casted (Vlong n) (Tlong si attr) - | val_casted_ptr_ptr: forall b ofs ty attr, - val_casted (Vptr b ofs) (Tpointer ty attr) - | val_casted_int_ptr: forall n ty attr, - val_casted (Vint n) (Tpointer ty attr) - | val_casted_ptr_int: forall b ofs si attr, - val_casted (Vptr b ofs) (Tint I32 si attr) - | val_casted_struct: forall id attr b ofs, - val_casted (Vptr b ofs) (Tstruct id attr) - | val_casted_union: forall id attr b ofs, - val_casted (Vptr b ofs) (Tunion id attr) - | val_casted_void: forall v, - val_casted v Tvoid. - -Remark cast_int_int_idem: - forall sz sg i, cast_int_int sz sg (cast_int_int sz sg i) = cast_int_int sz sg i. -Proof. - intros. destruct sz; simpl; auto. - destruct sg; [apply Int.sign_ext_idem|apply Int.zero_ext_idem]; compute; intuition congruence. - destruct sg; [apply Int.sign_ext_idem|apply Int.zero_ext_idem]; compute; intuition congruence. - destruct (Int.eq i Int.zero); auto. -Qed. - -Lemma cast_val_is_casted: - forall v ty ty' v', sem_cast v ty ty' = Some v' -> val_casted v' ty'. -Proof. - unfold sem_cast; intros. destruct ty'; simpl in *. -(* void *) - constructor. -(* int *) - destruct i; destruct ty; simpl in H; try (destruct f); try discriminate; destruct v; inv H. - constructor. apply (cast_int_int_idem I8 s). - constructor. apply (cast_int_int_idem I8 s). - destruct (cast_single_int s f); inv H1. constructor. apply (cast_int_int_idem I8 s). - destruct (cast_float_int s f); inv H1. constructor. apply (cast_int_int_idem I8 s). - constructor. apply (cast_int_int_idem I16 s). - constructor. apply (cast_int_int_idem I16 s). - destruct (cast_single_int s f); inv H1. constructor. apply (cast_int_int_idem I16 s). - destruct (cast_float_int s f); inv H1. constructor. apply (cast_int_int_idem I16 s). - constructor. auto. - constructor. - constructor. auto. - destruct (cast_single_int s f); inv H1. constructor. auto. - destruct (cast_float_int s f); inv H1. constructor; auto. - constructor; auto. - constructor. - constructor; auto. - constructor. - constructor; auto. - constructor. - constructor. simpl. destruct (Int.eq i0 Int.zero); auto. - constructor. simpl. destruct (Int64.eq i Int64.zero); auto. - constructor. simpl. destruct (Float32.cmp Ceq f Float32.zero); auto. - constructor. simpl. destruct (Float.cmp Ceq f Float.zero); auto. - constructor. simpl. destruct (Int.eq i Int.zero); auto. - constructor. simpl. destruct (Int.eq i Int.zero); auto. - constructor. simpl. destruct (Int.eq i Int.zero); auto. -(* long *) - destruct ty; try (destruct f); try discriminate. - destruct v; inv H. constructor. - destruct v; inv H. constructor. - destruct v; try discriminate. destruct (cast_single_long s f); inv H. constructor. - destruct v; try discriminate. destruct (cast_float_long s f); inv H. constructor. - destruct v; inv H. constructor. - destruct v; inv H. constructor. - destruct v; inv H. constructor. -(* float *) - destruct f; destruct ty; simpl in H; try (destruct f); try discriminate; destruct v; inv H; constructor. -(* pointer *) - destruct ty; simpl in H; try discriminate; destruct v; inv H; try constructor. -(* impossible cases *) - discriminate. - discriminate. -(* structs *) - destruct ty; try discriminate; destruct v; try discriminate. - destruct (ident_eq i0 i); inv H; constructor. -(* unions *) - destruct ty; try discriminate; destruct v; try discriminate. - destruct (ident_eq i0 i); inv H; constructor. -Qed. +(** Properties of values resulting from a cast *) Lemma val_casted_load_result: forall v ty chunk, @@ -316,15 +204,6 @@ Proof. discriminate. Qed. -Lemma cast_val_casted: - forall v ty, val_casted v ty -> sem_cast v ty ty = Some v. -Proof. - intros. inversion H; clear H; subst v ty; unfold sem_cast; simpl; auto. - destruct sz; congruence. - unfold proj_sumbool; repeat rewrite dec_eq_true; auto. - unfold proj_sumbool; repeat rewrite dec_eq_true; auto. -Qed. - Lemma val_casted_inject: forall f v v' ty, Val.inject f v v' -> val_casted v ty -> val_casted v' ty. @@ -363,7 +242,7 @@ Qed. Lemma make_cast_correct: forall e le m a v1 tto v2, eval_expr tge e le m a v1 -> - sem_cast v1 (typeof a) tto = Some v2 -> + sem_cast v1 (typeof a) tto m = Some v2 -> eval_expr tge e le m (make_cast a tto) v2. Proof. intros. @@ -386,9 +265,9 @@ Qed. (** Debug annotations. *) Lemma cast_typeconv: - forall v ty, + forall v ty m, val_casted v ty -> - sem_cast v ty (typeconv ty) = Some v. + sem_cast v ty (typeconv ty) m = Some v. Proof. induction 1; simpl; auto. - destruct sz; auto. @@ -423,7 +302,7 @@ Qed. Lemma step_Sset_debug: forall f id ty a k e le m v v', eval_expr tge e le m a v -> - sem_cast v (typeof a) ty = Some v' -> + sem_cast v (typeof a) ty m = Some v' -> plus step2 tge (State f (Sset_debug id ty a) k e le m) E0 (State f Sskip k e (PTree.set id v' le) m). Proof. @@ -2172,8 +2051,7 @@ Proof. exploit external_call_mem_inject; eauto. apply match_globalenvs_preserves_globals; eauto with compat. intros [j' [tvres [tm' [P [Q [R [S [T [U V]]]]]]]]]. econstructor; split. - apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved. econstructor; eauto with compat. eapply match_envs_set_opttemp; eauto. eapply match_envs_extcall; eauto. @@ -2334,8 +2212,7 @@ Proof. eapply match_cont_globalenv. eexact (MCONT VSet.empty). intros [j' [tvres [tm' [P [Q [R [S [T [U V]]]]]]]]]. econstructor; split. - apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved. econstructor; eauto. intros. apply match_cont_incr_bounds with (Mem.nextblock m) (Mem.nextblock tm). eapply match_cont_extcall; eauto. xomega. xomega. @@ -2358,10 +2235,10 @@ Proof. exploit function_ptr_translated; eauto. intros [tf [A B]]. econstructor; split. econstructor. - eapply Genv.init_mem_transf_partial. eexact transf_programs. eauto. - change (prog_main tprog) with (AST.prog_main tprog). - rewrite (transform_partial_program_main _ _ transf_programs). + eapply (Genv.init_mem_transf_partial (proj1 TRANSF)). eauto. + replace (prog_main tprog) with (prog_main prog). instantiate (1 := b). rewrite <- H1. apply symbols_preserved. + generalize (match_program_main (proj1 TRANSF)). simpl; auto. eauto. rewrite <- H3; apply type_of_fundef_preserved; auto. econstructor; eauto. @@ -2391,10 +2268,27 @@ Theorem transf_program_correct: forward_simulation (semantics1 prog) (semantics2 tprog). Proof. eapply forward_simulation_plus. - eexact public_preserved. + apply senv_preserved. eexact initial_states_simulation. eexact final_states_simulation. eexact step_simulation. Qed. End PRESERVATION. + +(** ** Commutation with linking *) + +Instance TransfSimplLocalsLink : TransfLink match_prog. +Proof. + red; intros. eapply Ctypes.link_match_program; eauto. +- intros. +Local Transparent Linker_fundef. + simpl in *; unfold link_fundef in *. + destruct f1; monadInv H3; destruct f2; monadInv H4; try discriminate. + destruct e; inv H2. exists (Internal x); split; auto. simpl; rewrite EQ; auto. + destruct e; inv H2. exists (Internal x); split; auto. simpl; rewrite EQ; auto. + destruct (external_function_eq e e0 && typelist_eq t t1 && + type_eq t0 t2 && calling_convention_eq c c0); inv H2. + econstructor; split; eauto. +Qed. + |