diff options
| -rw-r--r-- | cfrontend/Cminorgen.v | 17 | ||||
| -rw-r--r-- | cfrontend/Cminorgenproof.v | 63 | ||||
| -rw-r--r-- | cfrontend/Cshmgen.v | 72 | ||||
| -rw-r--r-- | cfrontend/Cshmgenproof.v | 560 | ||||
| -rw-r--r-- | cfrontend/Ctyping.v | 80 | ||||
| -rw-r--r-- | cfrontend/Initializersproof.v | 4 | ||||
| -rw-r--r-- | cfrontend/SimplExpr.v | 10 | ||||
| -rw-r--r-- | cfrontend/SimplExprproof.v | 130 | ||||
| -rw-r--r-- | cfrontend/SimplExprspec.v | 47 | ||||
| -rw-r--r-- | cfrontend/SimplLocals.v | 10 | ||||
| -rw-r--r-- | cfrontend/SimplLocalsproof.v | 99 |
11 files changed, 559 insertions, 533 deletions
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index c2b59fbe..b9a28ee1 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -12,19 +12,10 @@ (** Translation from Csharpminor to Cminor. *) -Require Import FSets. -Require FSetAVL. -Require Import Orders. -Require Mergesort. -Require Import Coqlib. -Require Import Errors. -Require Import Maps. -Require Import Ordered. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Csharpminor. -Require Import Cminor. +Require Import FSets FSetAVL Orders Mergesort. +Require Import Coqlib Maps Ordered Errors Integers Floats. +Require Import AST Linking. +Require Import Csharpminor Cminor. Local Open Scope string_scope. Local Open Scope error_monad_scope. diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 7a5d882e..2f551d68 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -12,61 +12,54 @@ (** Correctness proof for Cminor generation. *) -Require Import Coq.Program.Equality. -Require Import FSets. -Require Import Permutation. -Require Import Coqlib. +Require Import Coq.Program.Equality FSets Permutation. +Require Import FSets FSetAVL Orders Mergesort. +Require Import Coqlib Maps Ordered Errors Integers Floats. Require Intv. -Require Import Errors. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Events. -Require Import Globalenvs. -Require Import Smallstep. -Require Import Switch. -Require Import Csharpminor. -Require Import Cminor. -Require Import Cminorgen. +Require Import AST Linking. +Require Import Values Memory Events Globalenvs Smallstep. +Require Import Csharpminor Switch Cminor Cminorgen. Open Local Scope error_monad_scope. +Definition match_prog (p: Csharpminor.program) (tp: Cminor.program) := + match_program (fun cu f tf => transl_fundef f = OK tf) eq p tp. + +Lemma transf_program_match: + forall p tp, transl_program p = OK tp -> match_prog p tp. +Proof. + intros. apply match_transform_partial_program; auto. +Qed. + Section TRANSLATION. Variable prog: Csharpminor.program. Variable tprog: program. -Hypothesis TRANSL: transl_program prog = OK tprog. +Hypothesis TRANSL: match_prog prog tprog. Let ge : Csharpminor.genv := Genv.globalenv prog. Let tge: genv := Genv.globalenv tprog. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof (Genv.find_symbol_transf_partial transl_fundef _ TRANSL). +Proof (Genv.find_symbol_transf_partial TRANSL). -Lemma public_preserved: - forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. -Proof (Genv.public_symbol_transf_partial transl_fundef _ TRANSL). +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_transf_partial TRANSL). Lemma function_ptr_translated: forall (b: block) (f: Csharpminor.fundef), Genv.find_funct_ptr ge b = Some f -> exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf. -Proof (Genv.find_funct_ptr_transf_partial transl_fundef _ TRANSL). +Proof (Genv.find_funct_ptr_transf_partial TRANSL). Lemma functions_translated: forall (v: val) (f: Csharpminor.fundef), Genv.find_funct ge v = Some f -> exists tf, Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf. -Proof (Genv.find_funct_transf_partial transl_fundef _ TRANSL). - -Lemma varinfo_preserved: - forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. -Proof (Genv.find_var_info_transf_partial transl_fundef _ TRANSL). +Proof (Genv.find_funct_transf_partial TRANSL). Lemma sig_preserved_body: forall f tf cenv size, @@ -2029,8 +2022,7 @@ Proof. intros [f' [vres' [tm' [EC [VINJ [MINJ' [UNMAPPED [OUTOFREACH [INCR SEPARATED]]]]]]]]]. left; econstructor; split. apply plus_one. econstructor. eauto. - eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. eexact varinfo_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. assert (MCS': match_callstack f' m' tm' (Frame cenv tfn e le te sp lo hi :: cs) (Mem.nextblock m') (Mem.nextblock tm')). @@ -2184,8 +2176,7 @@ Opaque PTree.set. intros [f' [vres' [tm' [EC [VINJ [MINJ' [UNMAPPED [OUTOFREACH [INCR SEPARATED]]]]]]]]]. left; econstructor; split. apply plus_one. econstructor. - eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. eexact varinfo_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. econstructor; eauto. apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm). eapply match_callstack_external_call; eauto. @@ -2224,11 +2215,11 @@ Proof. exploit function_ptr_translated; eauto. intros [tf [FIND TR]]. econstructor; split. econstructor. - apply (Genv.init_mem_transf_partial _ _ TRANSL). eauto. + apply (Genv.init_mem_transf_partial TRANSL). eauto. simpl. fold tge. rewrite symbols_preserved. replace (prog_main tprog) with (prog_main prog). eexact H0. symmetry. unfold transl_program in TRANSL. - eapply transform_partial_program_main; eauto. + eapply match_program_main; eauto. eexact FIND. rewrite <- H2. apply sig_preserved; auto. eapply match_callstate with (f := Mem.flat_inj (Mem.nextblock m0)) (cs := @nil frame) (cenv := PTree.empty Z). @@ -2250,7 +2241,7 @@ Theorem transl_program_correct: forward_simulation (Csharpminor.semantics prog) (Cminor.semantics tprog). Proof. eapply forward_simulation_star; eauto. - eexact public_preserved. + apply senv_preserved. eexact transl_initial_states. eexact transl_final_states. eexact transl_step_correct. diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 825a563c..40b51bd3 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -20,17 +20,9 @@ Csharpminor's simpler control structures. *) -Require Import Coqlib. -Require Import Maps. -Require Import Errors. -Require Import Integers. -Require Import Floats. -Require Import AST. -Require Import Ctypes. -Require Import Cop. -Require Import Clight. -Require Import Cminor. -Require Import Csharpminor. +Require Import Coqlib Maps Errors Integers Floats. +Require Import AST Linking. +Require Import Ctypes Cop Clight Cminor Csharpminor. Open Local Scope string_scope. Open Local Scope error_monad_scope. @@ -125,6 +117,18 @@ Definition make_cmp_ne_zero (e: expr) := | _ => Ebinop (Ocmp Cne) e (make_intconst Int.zero) end. +(** Variants of [sizeof] and [alignof] that check that the given type is complete. *) + +Definition sizeof (ce: composite_env) (t: type) : res Z := + if complete_type ce t + then OK (Ctypes.sizeof ce t) + else Error (msg "incomplete type"). + +Definition alignof (ce: composite_env) (t: type) : res Z := + if complete_type ce t + then OK (Ctypes.alignof ce t) + else Error (msg "incomplete type"). + (** [make_cast from to e] applies to [e] the numeric conversions needed to transform a result of type [from] to a result of type [to]. *) @@ -238,16 +242,20 @@ Definition make_binarith (iop iopu fop sop lop lopu: binary_operation) Definition make_add (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_add ty1 ty2 with | add_case_pi ty => - let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in + do sz <- sizeof ce ty; + let n := make_intconst (Int.repr sz) in OK (Ebinop Oadd e1 (Ebinop Omul n e2)) | add_case_ip ty => - let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in + do sz <- sizeof ce ty; + let n := make_intconst (Int.repr sz) in OK (Ebinop Oadd e2 (Ebinop Omul n e1)) | add_case_pl ty => - let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in + do sz <- sizeof ce ty; + let n := make_intconst (Int.repr sz) in OK (Ebinop Oadd e1 (Ebinop Omul n (Eunop Ointoflong e2))) | add_case_lp ty => - let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in + do sz <- sizeof ce ty; + let n := make_intconst (Int.repr sz) in OK (Ebinop Oadd e2 (Ebinop Omul n (Eunop Ointoflong e1))) | add_default => make_binarith Oadd Oadd Oaddf Oaddfs Oaddl Oaddl e1 ty1 e2 ty2 @@ -256,13 +264,16 @@ Definition make_add (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: Definition make_sub (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_sub ty1 ty2 with | sub_case_pi ty => - let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in + do sz <- sizeof ce ty; + let n := make_intconst (Int.repr sz) in OK (Ebinop Osub e1 (Ebinop Omul n e2)) | sub_case_pp ty => - let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in + do sz <- sizeof ce ty; + let n := make_intconst (Int.repr sz) in OK (Ebinop Odiv (Ebinop Osub e1 e2) n) | sub_case_pl ty => - let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in + do sz <- sizeof ce ty; + let n := make_intconst (Int.repr sz) in OK (Ebinop Osub e1 (Ebinop Omul n (Eunop Ointoflong e2))) | sub_default => make_binarith Osub Osub Osubf Osubfs Osubl Osubl e1 ty1 e2 ty2 @@ -351,8 +362,9 @@ Definition make_load (addr: expr) (ty_res: type) := by-copy assignment of a value of Clight type [ty]. *) Definition make_memcpy (ce: composite_env) (dst src: expr) (ty: type) := - Sbuiltin None (EF_memcpy (Ctypes.sizeof ce ty) (Ctypes.alignof_blockcopy ce ty)) - (dst :: src :: nil). + do sz <- sizeof ce ty; + OK (Sbuiltin None (EF_memcpy sz (Ctypes.alignof_blockcopy ce ty)) + (dst :: src :: nil)). (** [make_store addr ty rhs] stores the value of the Csharpminor expression [rhs] into the memory location denoted by the @@ -362,7 +374,7 @@ Definition make_memcpy (ce: composite_env) (dst src: expr) (ty: type) := Definition make_store (ce: composite_env) (addr: expr) (ty: type) (rhs: expr) := match access_mode ty with | By_value chunk => OK (Sstore chunk addr rhs) - | By_copy => OK (make_memcpy ce addr rhs ty) + | By_copy => make_memcpy ce addr rhs ty | _ => Error (msg "Cshmgen.make_store") end. @@ -457,9 +469,9 @@ Fixpoint transl_expr (ce: composite_env) (a: Clight.expr) {struct a} : res expr do addr <- make_field_access ce (typeof b) i tb; make_load addr ty | Clight.Esizeof ty' ty => - OK(make_intconst (Int.repr (sizeof ce ty'))) + do sz <- sizeof ce ty'; OK(make_intconst (Int.repr sz)) | Clight.Ealignof ty' ty => - OK(make_intconst (Int.repr (alignof ce ty'))) + do al <- alignof ce ty'; OK(make_intconst (Int.repr al)) end (** [transl_lvalue a] returns the Csharpminor code that evaluates @@ -621,7 +633,8 @@ with transl_lbl_stmt (ce: composite_env) (tyret: type) (nbrk ncnt: nat) (*** Translation of functions *) -Definition transl_var (ce: composite_env) (v: ident * type) := (fst v, sizeof ce (snd v)). +Definition transl_var (ce: composite_env) (v: ident * type) := + do sz <- sizeof ce (snd v); OK (fst v, sz). Definition signature_of_function (f: Clight.function) := {| sig_args := map typ_of_type (map snd (Clight.fn_params f)); @@ -630,18 +643,19 @@ Definition signature_of_function (f: Clight.function) := Definition transl_function (ce: composite_env) (f: Clight.function) : res function := do tbody <- transl_statement ce f.(Clight.fn_return) 1%nat 0%nat (Clight.fn_body f); + do tvars <- mmap (transl_var ce) (Clight.fn_vars f); OK (mkfunction (signature_of_function f) (map fst (Clight.fn_params f)) - (map (transl_var ce) (Clight.fn_vars f)) + tvars (map fst (Clight.fn_temps f)) tbody). -Definition transl_fundef (ce: composite_env) (f: Clight.fundef) : res fundef := +Definition transl_fundef (ce: composite_env) (id: ident) (f: Clight.fundef) : res fundef := match f with - | Clight.Internal g => + | Internal g => do tg <- transl_function ce g; OK(AST.Internal tg) - | Clight.External ef args res cconv => + | External ef args res cconv => if signature_eq (ef_sig ef) (signature_of_type args res cconv) then OK(AST.External ef) else Error(msg "Cshmgen.transl_fundef: wrong external signature") @@ -649,7 +663,7 @@ Definition transl_fundef (ce: composite_env) (f: Clight.fundef) : res fundef := (** ** Translation of programs *) -Definition transl_globvar (ty: type) := OK tt. +Definition transl_globvar (id: ident) (ty: type) := OK tt. Definition transl_program (p: Clight.program) : res program := transform_partial_program2 (transl_fundef p.(prog_comp_env)) transl_globvar p. diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index e25e21c9..dfd3ceb4 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -12,24 +12,40 @@ (** * Correctness of the translation from Clight to C#minor. *) -Require Import Coqlib. -Require Import Errors. -Require Import Maps. -Require Import Integers. -Require Import Floats. -Require Import AST. -Require Import Values. -Require Import Events. -Require Import Memory. -Require Import Globalenvs. -Require Import Smallstep. -Require Import Ctypes. -Require Import Cop. -Require Import Clight. -Require Import Cminor. -Require Import Csharpminor. +Require Import Coqlib Errors Maps Integers Floats. +Require Import AST Linking. +Require Import Values Events Memory Globalenvs Smallstep. +Require Import Ctypes Cop Clight Cminor Csharpminor. Require Import Cshmgen. +(** * Relational specification of the transformation *) + +Inductive match_fundef (p: Clight.program) : Clight.fundef -> Csharpminor.fundef -> Prop := + | match_fundef_internal: forall f tf, + transl_function p.(prog_comp_env) f = OK tf -> + match_fundef p (Ctypes.Internal f) (AST.Internal tf) + | match_fundef_external: forall ef args res cc, + ef_sig ef = signature_of_type args res cc -> + match_fundef p (Ctypes.External ef args res cc) (AST.External ef). + +Definition match_varinfo (v: type) (tv: unit) := True. + +Definition match_prog (p: Clight.program) (tp: Csharpminor.program) : Prop := + match_program_gen match_fundef match_varinfo p p tp. + +Lemma transf_program_match: + forall p tp, transl_program p = OK tp -> match_prog p tp. +Proof. + unfold transl_program; intros. + eapply match_transform_partial_program2. + eexact H. +- intros. destruct f; simpl in H0. ++ monadInv H0. constructor; auto. ++ destruct (signature_eq (ef_sig e) (signature_of_type t t0 c)); inv H0. + constructor; auto. +- intros; red; auto. +Qed. + (** * Properties of operations over types *) Remark transl_params_types: @@ -41,21 +57,20 @@ Qed. Lemma transl_fundef_sig1: forall ce f tf args res cc, - transl_fundef ce f = OK tf -> + match_fundef ce f tf -> classify_fun (type_of_fundef f) = fun_case_f args res cc -> funsig tf = signature_of_type args res cc. Proof. - intros. destruct f; simpl in *. - monadInv H. monadInv EQ. simpl. inversion H0. + intros. inv H. +- monadInv H1. simpl. inversion H0. unfold signature_of_function, signature_of_type. f_equal. apply transl_params_types. - destruct (signature_eq (ef_sig e) (signature_of_type t t0 c)); inv H. - simpl. congruence. +- simpl in H0. unfold funsig. congruence. Qed. Lemma transl_fundef_sig2: forall ce f tf args res cc, - transl_fundef ce f = OK tf -> + match_fundef ce f tf -> type_of_fundef f = Tfunction args res cc -> funsig tf = signature_of_type args res cc. Proof. @@ -63,15 +78,73 @@ Proof. rewrite H0; reflexivity. Qed. +Lemma transl_sizeof: + forall (cunit prog: Clight.program) t sz, + linkorder cunit prog -> + sizeof cunit.(prog_comp_env) t = OK sz -> + sz = Ctypes.sizeof prog.(prog_comp_env) t. +Proof. + intros. destruct H. + unfold sizeof in H0. destruct (complete_type (prog_comp_env cunit) t) eqn:C; inv H0. + symmetry. apply Ctypes.sizeof_stable; auto. +Qed. + +Lemma transl_alignof: + forall (cunit prog: Clight.program) t al, + linkorder cunit prog -> + alignof cunit.(prog_comp_env) t = OK al -> + al = Ctypes.alignof prog.(prog_comp_env) t. +Proof. + intros. destruct H. + unfold alignof in H0. destruct (complete_type (prog_comp_env cunit) t) eqn:C; inv H0. + symmetry. apply Ctypes.alignof_stable; auto. +Qed. + +Lemma transl_alignof_blockcopy: + forall (cunit prog: Clight.program) t sz, + linkorder cunit prog -> + sizeof cunit.(prog_comp_env) t = OK sz -> + sz = Ctypes.sizeof prog.(prog_comp_env) t /\ + alignof_blockcopy cunit.(prog_comp_env) t = alignof_blockcopy prog.(prog_comp_env) t. +Proof. + intros. destruct H. + unfold sizeof in H0. destruct (complete_type (prog_comp_env cunit) t) eqn:C; inv H0. + split. +- symmetry. apply Ctypes.sizeof_stable; auto. +- revert C. induction t; simpl; auto; + destruct (prog_comp_env cunit)!i as [co|] eqn:X; try discriminate; erewrite H1 by eauto; auto. +Qed. + +Lemma field_offset_stable: + forall (cunit prog: Clight.program) id co f, + linkorder cunit prog -> + cunit.(prog_comp_env)!id = Some co -> + prog.(prog_comp_env)!id = Some co /\ + field_offset prog.(prog_comp_env) f (co_members co) = field_offset cunit.(prog_comp_env) f (co_members co). +Proof. + intros. + assert (C: composite_consistent cunit.(prog_comp_env) co). + { apply build_composite_env_consistent with cunit.(prog_types) id; auto. + apply prog_comp_env_eq. } + destruct H as [_ A]. + split. auto. generalize (co_consistent_complete _ _ C). + unfold field_offset. generalize 0. induction (co_members co) as [ | [f1 t1] m]; simpl; intros. +- auto. +- InvBooleans. + rewrite ! (alignof_stable _ _ A) by auto. + rewrite ! (sizeof_stable _ _ A) by auto. + destruct (ident_eq f f1); eauto. +Qed. + (** * Properties of the translation functions *) (** Transformation of expressions and statements. *) Lemma transl_expr_lvalue: - forall ge e le m a loc ofs ta, + forall ge e le m a loc ofs ce ta, Clight.eval_lvalue ge e le m a loc ofs -> - transl_expr ge a = OK ta -> - (exists tb, transl_lvalue ge a = OK tb /\ make_load tb (typeof a) = OK ta). + transl_expr ce a = OK ta -> + (exists tb, transl_lvalue ce a = OK tb /\ make_load tb (typeof a) = OK ta). Proof. intros until ta; intros EVAL TR. inv EVAL; simpl in TR. (* var local *) @@ -140,7 +213,8 @@ Qed. Section CONSTRUCTORS. -Variable ce: composite_env. +Variables cunit prog: Clight.program. +Hypothesis LINK: linkorder cunit prog. Variable ge: genv. Lemma make_intconst_correct: @@ -471,27 +545,33 @@ End MAKE_BIN. Hint Extern 2 (@eq (option val) _ _) => (simpl; reflexivity) : cshm. -Lemma make_add_correct: binary_constructor_correct (make_add ce) (sem_add ce). +Lemma make_add_correct: binary_constructor_correct (make_add cunit.(prog_comp_env)) (sem_add prog.(prog_comp_env)). Proof. red; unfold make_add, sem_add; intros until m; intros SEM MAKE EV1 EV2; - destruct (classify_add tya tyb); inv MAKE. -- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. -- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. -- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. -- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. + destruct (classify_add tya tyb); try (monadInv MAKE). +- rewrite (transl_sizeof _ _ _ _ LINK EQ). + destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. +- rewrite (transl_sizeof _ _ _ _ LINK EQ). + destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. +- rewrite (transl_sizeof _ _ _ _ LINK EQ). + destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. +- rewrite (transl_sizeof _ _ _ _ LINK EQ). + destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. - eapply make_binarith_correct; eauto; intros; auto. Qed. -Lemma make_sub_correct: binary_constructor_correct (make_sub ce) (sem_sub ce). +Lemma make_sub_correct: binary_constructor_correct (make_sub cunit.(prog_comp_env)) (sem_sub prog.(prog_comp_env)). Proof. red; unfold make_sub, sem_sub; intros until m; intros SEM MAKE EV1 EV2; - destruct (classify_sub tya tyb); inv MAKE. -- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. -- destruct va; try discriminate; destruct vb; inv SEM. + destruct (classify_sub tya tyb); try (monadInv MAKE). +- rewrite (transl_sizeof _ _ _ _ LINK EQ). + destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. +- rewrite (transl_sizeof _ _ _ _ LINK EQ). + destruct va; try discriminate; destruct vb; inv SEM. destruct (eq_block b0 b1); try discriminate. - set (sz := sizeof ce ty) in *. + set (sz := Ctypes.sizeof (prog_comp_env prog) ty) in *. destruct (zlt 0 sz); try discriminate. destruct (zle sz Int.max_signed); simpl in H0; inv H0. econstructor; eauto with cshm. @@ -503,7 +583,8 @@ Proof. predSpec Int.eq Int.eq_spec (Int.repr sz) Int.mone. rewrite H0 in E; rewrite Int.signed_mone in E; omegaContradiction. rewrite andb_false_r; auto. -- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. +- rewrite (transl_sizeof _ _ _ _ LINK EQ). + destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm. - eapply make_binarith_correct; eauto; intros; auto. Qed. @@ -663,8 +744,8 @@ Qed. Lemma transl_binop_correct: forall op a tya b tyb c va vb v e le m, - transl_binop ce op a tya b tyb = OK c -> - sem_binary_operation ce op va tya vb tyb m = Some v -> + transl_binop cunit.(prog_comp_env) op a tya b tyb = OK c -> + sem_binary_operation prog.(prog_comp_env) op va tya vb tyb m = Some v -> eval_expr ge e le m a va -> eval_expr ge e le m b vb -> eval_expr ge e le m c v. @@ -706,15 +787,18 @@ Proof. Qed. Lemma make_memcpy_correct: - forall ce f dst src ty k e le m b ofs v m', + forall f dst src ty k e le m b ofs v m' s, eval_expr ge e le m dst (Vptr b ofs) -> eval_expr ge e le m src v -> - assign_loc ce ty m b ofs v m' -> + assign_loc prog.(prog_comp_env) ty m b ofs v m' -> access_mode ty = By_copy -> - step ge (State f (make_memcpy ce dst src ty) k e le m) E0 (State f Sskip k e le m'). + make_memcpy cunit.(prog_comp_env) dst src ty = OK s -> + step ge (State f s k e le m) E0 (State f Sskip k e le m'). Proof. intros. inv H1; try congruence. - unfold make_memcpy. change le with (set_optvar None Vundef le) at 2. + monadInv H3. + exploit transl_alignof_blockcopy. eexact LINK. eauto. intros [A B]. rewrite A, B. + change le with (set_optvar None Vundef le) at 2. econstructor. econstructor. eauto. econstructor. eauto. constructor. econstructor; eauto. @@ -725,10 +809,10 @@ Qed. Lemma make_store_correct: forall addr ty rhs code e le m b ofs v m' f k, - make_store ce addr ty rhs = OK code -> + make_store cunit.(prog_comp_env) addr ty rhs = OK code -> eval_expr ge e le m addr (Vptr b ofs) -> eval_expr ge e le m rhs v -> - assign_loc ce ty m b ofs v m' -> + assign_loc prog.(prog_comp_env) ty m b ofs v m' -> step ge (State f code k e le m) E0 (State f Sskip k e le m'). Proof. unfold make_store. intros until k; intros MKSTORE EV1 EV2 ASSIGN. @@ -737,8 +821,8 @@ Proof. rewrite H in MKSTORE; inv MKSTORE. econstructor; eauto. (* by copy *) - rewrite H in MKSTORE; inv MKSTORE. - eapply make_memcpy_correct; eauto. + rewrite H in MKSTORE. + eapply make_memcpy_correct with (b := b) (v := Vptr b' ofs'); eauto. Qed. End CONSTRUCTORS. @@ -749,34 +833,30 @@ Section CORRECTNESS. Variable prog: Clight.program. Variable tprog: Csharpminor.program. -Hypothesis TRANSL: transl_program prog = OK tprog. +Hypothesis TRANSL: match_prog prog tprog. Let ge := globalenv prog. Let tge := Genv.globalenv tprog. Lemma symbols_preserved: forall s, Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof (Genv.find_symbol_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL). +Proof (Genv.find_symbol_match TRANSL). + +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_match TRANSL). -Lemma public_preserved: - forall s, Genv.public_symbol tge s = Genv.public_symbol ge s. -Proof (Genv.public_symbol_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL). +Lemma function_ptr_translated: + forall v f, + Genv.find_funct_ptr ge v = Some f -> + exists cu tf, Genv.find_funct_ptr tge v = Some tf /\ match_fundef cu f tf /\ linkorder cu prog. +Proof (Genv.find_funct_ptr_match TRANSL). Lemma functions_translated: forall v f, Genv.find_funct ge v = Some f -> - exists tf, Genv.find_funct tge v = Some tf /\ transl_fundef ge f = OK tf. -Proof (Genv.find_funct_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL). - -Lemma function_ptr_translated: - forall b f, - Genv.find_funct_ptr ge b = Some f -> - exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef ge f = OK tf. -Proof (Genv.find_funct_ptr_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL). - -Lemma block_is_volatile_preserved: - forall b, Genv.block_is_volatile tge b = Genv.block_is_volatile ge b. -Proof (Genv.block_is_volatile_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL). + exists cu tf, Genv.find_funct tge v = Some tf /\ match_fundef cu f tf /\ linkorder cu prog. +Proof (Genv.find_funct_match TRANSL). (** * Matching between environments *) @@ -787,7 +867,7 @@ Record match_env (e: Clight.env) (te: Csharpminor.env) : Prop := mk_match_env { me_local: forall id b ty, - e!id = Some (b, ty) -> te!id = Some(b, sizeof ge ty); + e!id = Some (b, ty) -> te!id = Some(b, Ctypes.sizeof ge ty); me_local_inv: forall id b sz, te!id = Some (b, sz) -> exists ty, e!id = Some(b, ty) @@ -811,13 +891,13 @@ Proof. intros. set (R := fun (x: (block * type)) (y: (block * Z)) => match x, y with - | (b1, ty), (b2, sz) => b2 = b1 /\ sz = sizeof ge ty + | (b1, ty), (b2, sz) => b2 = b1 /\ sz = Ctypes.sizeof ge ty end). assert (list_forall2 (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y)) (PTree.elements e) (PTree.elements te)). apply PTree.elements_canonical_order. - intros id [b ty] GET. exists (b, sizeof ge ty); split. eapply me_local; eauto. red; auto. + intros id [b ty] GET. exists (b, Ctypes.sizeof ge ty); split. eapply me_local; eauto. red; auto. intros id [b sz] GET. exploit me_local_inv; eauto. intros [ty EQ]. exploit me_local; eauto. intros EQ1. exists (b, ty); split. auto. red; split; congruence. @@ -853,17 +933,21 @@ Qed. local variables and initialization of the parameters. *) Lemma match_env_alloc_variables: - forall e1 m1 vars e2 m2, - Clight.alloc_variables ge e1 m1 vars e2 m2 -> - forall te1, + forall cunit, linkorder cunit prog -> + forall e1 m1 vars e2 m2, Clight.alloc_variables ge e1 m1 vars e2 m2 -> + forall tvars te1, + mmap (transl_var cunit.(prog_comp_env)) vars = OK tvars -> match_env e1 te1 -> exists te2, - Csharpminor.alloc_variables te1 m1 (map (transl_var ge) vars) te2 m2 + Csharpminor.alloc_variables te1 m1 tvars te2 m2 /\ match_env e2 te2. Proof. - induction 1; intros; simpl. - exists te1; split. constructor. auto. - exploit (IHalloc_variables (PTree.set id (b1, sizeof ge ty) te1)). + induction 2; simpl; intros. +- inv H0. exists te1; split. constructor. auto. +- monadInv H2. monadInv EQ. simpl in *. + exploit transl_sizeof. eexact H. eauto. intros SZ; rewrite SZ. + exploit (IHalloc_variables x0 (PTree.set id (b1, Ctypes.sizeof ge ty) te1)). + auto. constructor. (* me_local *) intros until ty0. repeat rewrite PTree.gsspec. @@ -893,6 +977,16 @@ Proof. destruct a as [id ty]. destruct vals; try discriminate. auto. Qed. +Lemma transl_vars_names: + forall ce vars tvars, + mmap (transl_var ce) vars = OK tvars -> + map fst tvars = var_names vars. +Proof. + intros. exploit mmap_inversion; eauto. generalize vars tvars. induction 1; simpl. +- auto. +- monadInv H0. simpl; congruence. +Qed. + (** * Proof of semantic preservation *) (** ** Semantic preservation for expressions *) @@ -919,6 +1013,8 @@ Qed. Section EXPR. +Variable cunit: Clight.program. +Hypothesis LINK: linkorder cunit prog. Variable e: Clight.env. Variable le: temp_env. Variable m: mem. @@ -928,11 +1024,11 @@ Hypothesis MENV: match_env e te. Lemma transl_expr_lvalue_correct: (forall a v, Clight.eval_expr ge e le m a v -> - forall ta (TR: transl_expr ge a = OK ta) , + forall ta (TR: transl_expr cunit.(prog_comp_env) a = OK ta) , Csharpminor.eval_expr tge te le m ta v) /\(forall a b ofs, Clight.eval_lvalue ge e le m a b ofs -> - forall ta (TR: transl_lvalue ge a = OK ta), + forall ta (TR: transl_lvalue cunit.(prog_comp_env) a = OK ta), Csharpminor.eval_expr tge te le m ta (Vptr b ofs)). Proof. apply eval_expr_lvalue_ind; intros; try (monadInv TR). @@ -955,9 +1051,9 @@ Proof. (* cast *) eapply make_cast_correct; eauto. (* sizeof *) - apply make_intconst_correct. + rewrite (transl_sizeof _ _ _ _ LINK EQ). apply make_intconst_correct. (* alignof *) - apply make_intconst_correct. + rewrite (transl_alignof _ _ _ _ LINK EQ). apply make_intconst_correct. (* rvalue out of lvalue *) exploit transl_expr_lvalue; eauto. intros [tb [TRLVAL MKLOAD]]. eapply make_load_correct; eauto. @@ -971,11 +1067,13 @@ Proof. (* deref *) simpl in TR. eauto. (* field struct *) - change (prog_comp_env prog) with (genv_cenv ge) in EQ0. - unfold make_field_access in EQ0; rewrite H1, H2 in EQ0; monadInv EQ0. + unfold make_field_access in EQ0. rewrite H1 in EQ0. + destruct (prog_comp_env cunit)!id as [co'|] eqn:CO; monadInv EQ0. + exploit field_offset_stable. eexact LINK. eauto. instantiate (1 := i). intros [A B]. + rewrite <- B in EQ1. eapply eval_Ebinop; eauto. apply make_intconst_correct. - simpl. congruence. + simpl. unfold ge in *; simpl in *. congruence. (* field union *) unfold make_field_access in EQ0; rewrite H1 in EQ0; monadInv EQ0. auto. @@ -984,21 +1082,21 @@ Qed. Lemma transl_expr_correct: forall a v, Clight.eval_expr ge e le m a v -> - forall ta, transl_expr ge a = OK ta -> + forall ta, transl_expr cunit.(prog_comp_env) a = OK ta -> Csharpminor.eval_expr tge te le m ta v. Proof (proj1 transl_expr_lvalue_correct). Lemma transl_lvalue_correct: forall a b ofs, Clight.eval_lvalue ge e le m a b ofs -> - forall ta, transl_lvalue ge a = OK ta -> + forall ta, transl_lvalue cunit.(prog_comp_env) a = OK ta -> Csharpminor.eval_expr tge te le m ta (Vptr b ofs). Proof (proj2 transl_expr_lvalue_correct). Lemma transl_arglist_correct: forall al tyl vl, Clight.eval_exprlist ge e le m al tyl vl -> - forall tal, transl_arglist ge al tyl = OK tal -> + forall tal, transl_arglist cunit.(prog_comp_env) al tyl = OK tal -> Csharpminor.eval_exprlist tge te le m tal vl. Proof. induction 1; intros. @@ -1052,71 +1150,75 @@ Proof. apply star_refl. Qed. -Inductive match_cont: type -> nat -> nat -> Clight.cont -> Csharpminor.cont -> Prop := - | match_Kstop: forall tyret nbrk ncnt, - match_cont tyret nbrk ncnt Clight.Kstop Kstop - | match_Kseq: forall tyret nbrk ncnt s k ts tk, - transl_statement ge tyret nbrk ncnt s = OK ts -> - match_cont tyret nbrk ncnt k tk -> - match_cont tyret nbrk ncnt +Inductive match_cont: composite_env -> type -> nat -> nat -> Clight.cont -> Csharpminor.cont -> Prop := + | match_Kstop: forall ce tyret nbrk ncnt, + match_cont tyret ce nbrk ncnt Clight.Kstop Kstop + | match_Kseq: forall ce tyret nbrk ncnt s k ts tk, + transl_statement ce tyret nbrk ncnt s = OK ts -> + match_cont ce tyret nbrk ncnt k tk -> + match_cont ce tyret nbrk ncnt (Clight.Kseq s k) (Kseq ts tk) - | match_Kloop1: forall tyret s1 s2 k ts1 ts2 nbrk ncnt tk, - transl_statement ge tyret 1%nat 0%nat s1 = OK ts1 -> - transl_statement ge tyret 0%nat (S ncnt) s2 = OK ts2 -> - match_cont tyret nbrk ncnt k tk -> - match_cont tyret 1%nat 0%nat + | match_Kloop1: forall ce tyret s1 s2 k ts1 ts2 nbrk ncnt tk, + transl_statement ce tyret 1%nat 0%nat s1 = OK ts1 -> + transl_statement ce tyret 0%nat (S ncnt) s2 = OK ts2 -> + match_cont ce tyret nbrk ncnt k tk -> + match_cont ce tyret 1%nat 0%nat (Clight.Kloop1 s1 s2 k) (Kblock (Kseq ts2 (Kseq (Sloop (Sseq (Sblock ts1) ts2)) (Kblock tk)))) - | match_Kloop2: forall tyret s1 s2 k ts1 ts2 nbrk ncnt tk, - transl_statement ge tyret 1%nat 0%nat s1 = OK ts1 -> - transl_statement ge tyret 0%nat (S ncnt) s2 = OK ts2 -> - match_cont tyret nbrk ncnt k tk -> - match_cont tyret 0%nat (S ncnt) + | match_Kloop2: forall ce tyret s1 s2 k ts1 ts2 nbrk ncnt tk, + transl_statement ce tyret 1%nat 0%nat s1 = OK ts1 -> + transl_statement ce tyret 0%nat (S ncnt) s2 = OK ts2 -> + match_cont ce tyret nbrk ncnt k tk -> + match_cont ce tyret 0%nat (S ncnt) (Clight.Kloop2 s1 s2 k) (Kseq (Sloop (Sseq (Sblock ts1) ts2)) (Kblock tk)) - | match_Kswitch: forall tyret nbrk ncnt k tk, - match_cont tyret nbrk ncnt k tk -> - match_cont tyret 0%nat (S ncnt) + | match_Kswitch: forall ce tyret nbrk ncnt k tk, + match_cont ce tyret nbrk ncnt k tk -> + match_cont ce tyret 0%nat (S ncnt) (Clight.Kswitch k) (Kblock tk) - | match_Kcall_some: forall tyret nbrk ncnt nbrk' ncnt' f e k id tf te le tk, - transl_function ge f = OK tf -> + | match_Kcall: forall ce tyret nbrk ncnt nbrk' ncnt' f e k id tf te le tk cu, + linkorder cu prog -> + transl_function cu.(prog_comp_env) f = OK tf -> match_env e te -> - match_cont (Clight.fn_return f) nbrk' ncnt' k tk -> - match_cont tyret nbrk ncnt + match_cont cu.(prog_comp_env) (Clight.fn_return f) nbrk' ncnt' k tk -> + match_cont ce tyret nbrk ncnt (Clight.Kcall id f e le k) (Kcall id tf te le tk). Inductive match_states: Clight.state -> Csharpminor.state -> Prop := | match_state: - forall f nbrk ncnt s k e le m tf ts tk te ts' tk' - (TRF: transl_function ge f = OK tf) - (TR: transl_statement ge (Clight.fn_return f) nbrk ncnt s = OK ts) + forall f nbrk ncnt s k e le m tf ts tk te ts' tk' cu + (LINK: linkorder cu prog) + (TRF: transl_function cu.(prog_comp_env) f = OK tf) + (TR: transl_statement cu.(prog_comp_env) (Clight.fn_return f) nbrk ncnt s = OK ts) (MTR: match_transl ts tk ts' tk') (MENV: match_env e te) - (MK: match_cont (Clight.fn_return f) nbrk ncnt k tk), + (MK: match_cont cu.(prog_comp_env) (Clight.fn_return f) nbrk ncnt k tk), match_states (Clight.State f s k e le m) (State tf ts' tk' te le m) | match_callstate: - forall fd args k m tfd tk targs tres cconv - (TR: transl_fundef ge fd = OK tfd) - (MK: match_cont Tvoid 0%nat 0%nat k tk) + forall fd args k m tfd tk targs tres cconv cu ce + (LINK: linkorder cu prog) + (TR: match_fundef cu fd tfd) + (MK: match_cont ce Tvoid 0%nat 0%nat k tk) (ISCC: Clight.is_call_cont k) (TY: type_of_fundef fd = Tfunction targs tres cconv), match_states (Clight.Callstate fd args k m) (Callstate tfd args tk m) | match_returnstate: - forall res k m tk - (MK: match_cont Tvoid 0%nat 0%nat k tk), + forall res k m tk ce + (MK: match_cont ce Tvoid 0%nat 0%nat k tk), match_states (Clight.Returnstate res k m) (Returnstate res tk m). Remark match_states_skip: - forall f e le te nbrk ncnt k tf tk m, - transl_function ge f = OK tf -> + forall f e le te nbrk ncnt k tf tk m cu, + linkorder cu prog -> + transl_function cu.(prog_comp_env) f = OK tf -> match_env e te -> - match_cont (Clight.fn_return f) nbrk ncnt k tk -> + match_cont cu.(prog_comp_env) (Clight.fn_return f) nbrk ncnt k tk -> match_states (Clight.State f Clight.Sskip k e le m) (State tf Sskip tk te le m). Proof. intros. econstructor; eauto. simpl; reflexivity. constructor. @@ -1125,89 +1227,90 @@ Qed. (** Commutation between label resolution and compilation *) Section FIND_LABEL. +Variable ce: composite_env. Variable lbl: label. Variable tyret: type. Lemma transl_find_label: forall s nbrk ncnt k ts tk - (TR: transl_statement ge tyret nbrk ncnt s = OK ts) - (MC: match_cont tyret nbrk ncnt k tk), + (TR: transl_statement ce tyret nbrk ncnt s = OK ts) + (MC: match_cont ce tyret nbrk ncnt k tk), match Clight.find_label lbl s k with | None => find_label lbl ts tk = None | Some (s', k') => exists ts', exists tk', exists nbrk', exists ncnt', find_label lbl ts tk = Some (ts', tk') - /\ transl_statement ge tyret nbrk' ncnt' s' = OK ts' - /\ match_cont tyret nbrk' ncnt' k' tk' + /\ transl_statement ce tyret nbrk' ncnt' s' = OK ts' + /\ match_cont ce tyret nbrk' ncnt' k' tk' end with transl_find_label_ls: forall ls nbrk ncnt k tls tk - (TR: transl_lbl_stmt ge tyret nbrk ncnt ls = OK tls) - (MC: match_cont tyret nbrk ncnt k tk), + (TR: transl_lbl_stmt ce tyret nbrk ncnt ls = OK tls) + (MC: match_cont ce tyret nbrk ncnt k tk), match Clight.find_label_ls lbl ls k with | None => find_label_ls lbl tls tk = None | Some (s', k') => exists ts', exists tk', exists nbrk', exists ncnt', find_label_ls lbl tls tk = Some (ts', tk') - /\ transl_statement ge tyret nbrk' ncnt' s' = OK ts' - /\ match_cont tyret nbrk' ncnt' k' tk' + /\ transl_statement ce tyret nbrk' ncnt' s' = OK ts' + /\ match_cont ce tyret nbrk' ncnt' k' tk' end. Proof. - intro s; case s; intros; try (monadInv TR); simpl. -(* skip *) +* intro s; case s; intros; try (monadInv TR); simpl. +- (* skip *) auto. -(* assign *) +- (* assign *) unfold make_store, make_memcpy in EQ3. - destruct (access_mode (typeof e)); inv EQ3; auto. -(* set *) + destruct (access_mode (typeof e)); monadInv EQ3; auto. +- (* set *) auto. -(* call *) +- (* call *) simpl in TR. destruct (classify_fun (typeof e)); monadInv TR. auto. -(* builtin *) +- (* builtin *) auto. -(* seq *) +- (* seq *) exploit (transl_find_label s0 nbrk ncnt (Clight.Kseq s1 k)); eauto. constructor; eauto. destruct (Clight.find_label lbl s0 (Clight.Kseq s1 k)) as [[s' k'] | ]. intros [ts' [tk' [nbrk' [ncnt' [A [B C]]]]]]. rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. intro. rewrite H. eapply transl_find_label; eauto. -(* ifthenelse *) +- (* ifthenelse *) exploit (transl_find_label s0); eauto. destruct (Clight.find_label lbl s0 k) as [[s' k'] | ]. intros [ts' [tk' [nbrk' [ncnt' [A [B C]]]]]]. rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. intro. rewrite H. eapply transl_find_label; eauto. -(* loop *) +- (* loop *) exploit (transl_find_label s0 1%nat 0%nat (Kloop1 s0 s1 k)); eauto. econstructor; eauto. destruct (Clight.find_label lbl s0 (Kloop1 s0 s1 k)) as [[s' k'] | ]. intros [ts' [tk' [nbrk' [ncnt' [A [B C]]]]]]. rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. intro. rewrite H. eapply transl_find_label; eauto. econstructor; eauto. -(* break *) +- (* break *) auto. -(* continue *) +- (* continue *) auto. -(* return *) +- (* return *) simpl in TR. destruct o; monadInv TR. auto. auto. -(* switch *) +- (* switch *) assert (exists b, ts = Sblock (Sswitch b x x0)). { destruct (classify_switch (typeof e)); inv EQ2; econstructor; eauto. } destruct H as [b EQ3]; rewrite EQ3; simpl. eapply transl_find_label_ls with (k := Clight.Kswitch k); eauto. econstructor; eauto. -(* label *) +- (* label *) destruct (ident_eq lbl l). exists x; exists tk; exists nbrk; exists ncnt; auto. eapply transl_find_label; eauto. -(* goto *) +- (* goto *) auto. - intro ls; case ls; intros; monadInv TR; simpl. -(* nil *) +* intro ls; case ls; intros; monadInv TR; simpl. +- (* nil *) auto. -(* cons *) +- (* cons *) exploit (transl_find_label s nbrk ncnt (Clight.Kseq (seq_of_labeled_statement l) k)); eauto. econstructor; eauto. apply transl_lbl_stmt_2; eauto. destruct (Clight.find_label lbl s (Clight.Kseq (seq_of_labeled_statement l) k)) as [[s' k'] | ]. @@ -1222,9 +1325,9 @@ End FIND_LABEL. (** Properties of call continuations *) Lemma match_cont_call_cont: - forall tyret' nbrk' ncnt' tyret nbrk ncnt k tk, - match_cont tyret nbrk ncnt k tk -> - match_cont tyret' nbrk' ncnt' (Clight.call_cont k) (call_cont tk). + forall ce' tyret' nbrk' ncnt' ce tyret nbrk ncnt k tk, + match_cont ce tyret nbrk ncnt k tk -> + match_cont ce' tyret' nbrk' ncnt' (Clight.call_cont k) (call_cont tk). Proof. induction 1; simpl; auto. constructor. @@ -1232,10 +1335,10 @@ Proof. Qed. Lemma match_cont_is_call_cont: - forall tyret nbrk ncnt k tk tyret' nbrk' ncnt', - match_cont tyret nbrk ncnt k tk -> + forall ce tyret nbrk ncnt k tk ce' tyret' nbrk' ncnt', + match_cont ce tyret nbrk ncnt k tk -> Clight.is_call_cont k -> - match_cont tyret' nbrk' ncnt' k tk /\ is_call_cont tk. + match_cont ce' tyret' nbrk' ncnt' k tk /\ is_call_cont tk. Proof. intros. inv H; simpl in H0; try contradiction; simpl. split; auto; constructor. @@ -1251,11 +1354,12 @@ Lemma transl_step: Proof. induction 1; intros T1 MST; inv MST. -(* assign *) +- (* assign *) monadInv TR. assert (SAME: ts' = ts /\ tk' = tk). - inversion MTR. auto. - subst ts. unfold make_store, make_memcpy in EQ3. destruct (access_mode (typeof a1)); congruence. + { inversion MTR. auto. + subst ts. unfold make_store, make_memcpy in EQ3. + destruct (access_mode (typeof a1)); monadInv EQ3; auto. } destruct SAME; subst ts' tk'. econstructor; split. apply plus_one. eapply make_store_correct; eauto. @@ -1263,62 +1367,61 @@ Proof. eapply transl_expr_correct; eauto. eapply match_states_skip; eauto. -(* set *) +- (* set *) monadInv TR. inv MTR. econstructor; split. apply plus_one. econstructor. eapply transl_expr_correct; eauto. eapply match_states_skip; eauto. -(* call *) +- (* call *) revert TR. simpl. case_eq (classify_fun (typeof a)); try congruence. intros targs tres cc CF TR. monadInv TR. inv MTR. - exploit functions_translated; eauto. intros [tfd [FIND TFD]]. + exploit functions_translated; eauto. intros (cu' & tfd & FIND & TFD & LINK'). rewrite H in CF. simpl in CF. inv CF. econstructor; split. apply plus_one. econstructor; eauto. - exploit transl_expr_correct; eauto. - exploit transl_arglist_correct; eauto. + eapply transl_expr_correct with (cunit := cu); eauto. + eapply transl_arglist_correct with (cunit := cu); eauto. erewrite typlist_of_arglist_eq by eauto. eapply transl_fundef_sig1; eauto. rewrite H3. auto. econstructor; eauto. - econstructor; eauto. + eapply match_Kcall with (ce := prog_comp_env cu') (cu := cu); eauto. simpl. auto. -(* builtin *) +- (* builtin *) monadInv TR. inv MTR. econstructor; split. apply plus_one. econstructor. eapply transl_arglist_correct; eauto. - eapply external_call_symbols_preserved_gen with (ge1 := ge). - exact symbols_preserved. exact public_preserved. exact block_is_volatile_preserved. eauto. + eapply external_call_symbols_preserved with (ge1 := ge). apply senv_preserved. eauto. eapply match_states_skip; eauto. -(* seq *) +- (* seq *) monadInv TR. inv MTR. econstructor; split. apply plus_one. constructor. econstructor; eauto. constructor. econstructor; eauto. -(* skip seq *) +- (* skip seq *) monadInv TR. inv MTR. inv MK. econstructor; split. apply plus_one. apply step_skip_seq. econstructor; eauto. constructor. -(* continue seq *) +- (* continue seq *) monadInv TR. inv MTR. inv MK. econstructor; split. apply plus_one. constructor. econstructor; eauto. simpl. reflexivity. constructor. -(* break seq *) +- (* break seq *) monadInv TR. inv MTR. inv MK. econstructor; split. apply plus_one. constructor. econstructor; eauto. simpl. reflexivity. constructor. -(* ifthenelse *) +- (* ifthenelse *) monadInv TR. inv MTR. exploit make_boolean_correct; eauto. exploit transl_expr_correct; eauto. @@ -1327,7 +1430,7 @@ Proof. apply plus_one. apply step_ifthenelse with (v := v) (b := b); auto. destruct b; econstructor; eauto; constructor. -(* loop *) +- (* loop *) monadInv TR. econstructor; split. eapply star_plus_trans. eapply match_transl_step; eauto. @@ -1337,9 +1440,9 @@ Proof. reflexivity. reflexivity. traceEq. econstructor; eauto. constructor. econstructor; eauto. -(* skip-or-continue loop *) +- (* skip-or-continue loop *) assert ((ts' = Sskip \/ ts' = Sexit ncnt) /\ tk' = tk). - destruct H; subst x; monadInv TR; inv MTR; auto. + { destruct H; subst x; monadInv TR; inv MTR; auto. } destruct H0. inv MK. econstructor; split. eapply plus_left. @@ -1347,7 +1450,7 @@ Proof. apply star_one. constructor. traceEq. econstructor; eauto. constructor. econstructor; eauto. -(* break loop1 *) +- (* break loop1 *) monadInv TR. inv MTR. inv MK. econstructor; split. eapply plus_left. constructor. @@ -1357,16 +1460,15 @@ Proof. reflexivity. reflexivity. traceEq. eapply match_states_skip; eauto. -(* skip loop2 *) +- (* skip loop2 *) monadInv TR. inv MTR. inv MK. econstructor; split. apply plus_one. constructor. econstructor; eauto. -Local Opaque ge. - simpl. rewrite H5; simpl. rewrite H7; simpl. eauto. + simpl. rewrite H6; simpl. rewrite H8; simpl. eauto. constructor. -(* break loop2 *) +- (* break loop2 *) monadInv TR. inv MTR. inv MK. econstructor; split. eapply plus_left. constructor. @@ -1374,32 +1476,32 @@ Local Opaque ge. traceEq. eapply match_states_skip; eauto. -(* return none *) +- (* return none *) monadInv TR. inv MTR. econstructor; split. apply plus_one. constructor. eapply match_env_free_blocks; eauto. - econstructor; eauto. + eapply match_returnstate with (ce := prog_comp_env cu); eauto. eapply match_cont_call_cont. eauto. -(* return some *) +- (* return some *) monadInv TR. inv MTR. econstructor; split. apply plus_one. constructor. eapply make_cast_correct; eauto. eapply transl_expr_correct; eauto. eapply match_env_free_blocks; eauto. - econstructor; eauto. + eapply match_returnstate with (ce := prog_comp_env cu); eauto. eapply match_cont_call_cont. eauto. -(* skip call *) +- (* skip call *) monadInv TR. inv MTR. exploit match_cont_is_call_cont; eauto. intros [A B]. econstructor; split. apply plus_one. apply step_skip_call. auto. eapply match_env_free_blocks; eauto. - constructor. eauto. + eapply match_returnstate with (ce := prog_comp_env cu); eauto. -(* switch *) +- (* switch *) monadInv TR. assert (E: exists b, ts = Sblock (Sswitch b x x0) /\ Switch.switch_argument b v n). { unfold sem_switch_arg in H0. @@ -1415,7 +1517,7 @@ Local Opaque ge. constructor. econstructor. eauto. -(* skip or break switch *) +- (* skip or break switch *) assert ((ts' = Sskip \/ ts' = Sexit nbrk) /\ tk' = tk). destruct H; subst x; monadInv TR; inv MTR; auto. destruct H0. inv MK. @@ -1423,57 +1525,54 @@ Local Opaque ge. apply plus_one. destruct H0; subst ts'. 2:constructor. constructor. eapply match_states_skip; eauto. - -(* continue switch *) +- (* continue switch *) monadInv TR. inv MTR. inv MK. econstructor; split. apply plus_one. constructor. econstructor; eauto. simpl. reflexivity. constructor. -(* label *) +- (* label *) monadInv TR. inv MTR. econstructor; split. apply plus_one. constructor. econstructor; eauto. constructor. -(* goto *) +- (* goto *) monadInv TR. inv MTR. generalize TRF. unfold transl_function. intro TRF'. monadInv TRF'. - exploit (transl_find_label lbl). eexact EQ. eapply match_cont_call_cont. eauto. + exploit (transl_find_label (prog_comp_env cu) lbl). eexact EQ. eapply match_cont_call_cont. eauto. rewrite H. intros [ts' [tk'' [nbrk' [ncnt' [A [B C]]]]]]. econstructor; split. apply plus_one. constructor. simpl. eexact A. econstructor; eauto. constructor. -(* internal function *) - inv H. monadInv TR. monadInv EQ. +- (* internal function *) + inv H. inv TR. monadInv H5. exploit match_cont_is_call_cont; eauto. intros [A B]. exploit match_env_alloc_variables; eauto. apply match_env_empty. intros [te1 [C D]]. econstructor; split. apply plus_one. eapply step_internal_function. - simpl. rewrite list_map_compose. simpl. assumption. - simpl. auto. - simpl. auto. - simpl. eauto. + simpl. erewrite transl_vars_names by eauto. assumption. + simpl. assumption. + simpl. assumption. + simpl; eauto. simpl. rewrite create_undef_temps_match. eapply bind_parameter_temps_match; eauto. simpl. econstructor; eauto. - unfold transl_function. rewrite EQ0; simpl. auto. + unfold transl_function. rewrite EQ; simpl. rewrite EQ1; simpl. auto. constructor. -(* external function *) - simpl in TR. - destruct (signature_eq (ef_sig ef) (signature_of_type targs tres cconv)); inv TR. +- (* external function *) + inv TR. exploit match_cont_is_call_cont; eauto. intros [A B]. econstructor; split. apply plus_one. constructor. eauto. - eapply external_call_symbols_preserved_gen with (ge1 := ge). - exact symbols_preserved. exact public_preserved. exact block_is_volatile_preserved. eauto. - econstructor; eauto. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + eapply match_returnstate with (ce := ce); eauto. -(* returnstate *) +- (* returnstate *) inv MK. econstructor; split. apply plus_one. constructor. @@ -1485,17 +1584,14 @@ Lemma transl_initial_states: exists R, initial_state tprog R /\ match_states S R. Proof. intros. inv H. - exploit function_ptr_translated; eauto. intros [tf [A B]]. - assert (C: Genv.find_symbol tge (AST.prog_main tprog) = Some b). - rewrite symbols_preserved. replace (AST.prog_main tprog) with (prog_main prog). - auto. symmetry. unfold transl_program in TRANSL. - change (prog_main prog) with (AST.prog_main (program_of_program prog)). - eapply transform_partial_program2_main; eauto. - assert (funsig tf = signature_of_type Tnil type_int32s cc_default). - eapply transl_fundef_sig2; eauto. + exploit function_ptr_translated; eauto. intros (cu & tf & A & B & C). + assert (D: Genv.find_symbol tge (AST.prog_main tprog) = Some b). + { destruct TRANSL as (P & Q & R). rewrite Q. rewrite symbols_preserved. auto. } + assert (E: funsig tf = signature_of_type Tnil type_int32s cc_default). + { eapply transl_fundef_sig2; eauto. } econstructor; split. - econstructor; eauto. eapply Genv.init_mem_transf_partial2; eauto. - econstructor; eauto. constructor; auto. exact I. + econstructor; eauto. apply (Genv.init_mem_match TRANSL). eauto. + econstructor; eauto. instantiate (1 := prog_comp_env cu). constructor; auto. exact I. Qed. Lemma transl_final_states: @@ -1509,10 +1605,40 @@ Theorem transl_program_correct: forward_simulation (Clight.semantics2 prog) (Csharpminor.semantics tprog). Proof. eapply forward_simulation_plus. - eexact public_preserved. + apply senv_preserved. eexact transl_initial_states. eexact transl_final_states. eexact transl_step. Qed. End CORRECTNESS. + +(** ** Commutation with linking *) + +Instance TransfCshmgenLink : TransfLink match_prog. +Proof. + red; intros. destruct (link_linkorder _ _ _ H) as (LO1 & LO2). + generalize H. +Local Transparent Ctypes.Linker_program. + simpl; unfold link_program. + destruct (link (program_of_program p1) (program_of_program p2)) as [pp|] eqn:LP; try discriminate. + destruct (lift_option (link (prog_types p1) (prog_types p2))) as [[typs EQ]|P]; try discriminate. + destruct (link_build_composite_env (prog_types p1) (prog_types p2) typs + (prog_comp_env p1) (prog_comp_env p2) (prog_comp_env_eq p1) + (prog_comp_env_eq p2) EQ) as (env & P & Q). + intros E. + eapply Linking.link_match_program; eauto. +- intros. +Local Transparent Linker_fundef Linking.Linker_fundef. + inv H3; inv H4; simpl in H2. ++ discriminate. ++ destruct ef; inv H2. econstructor; split. simpl; eauto. left; constructor; auto. ++ destruct ef; inv H2. econstructor; split. simpl; eauto. right; constructor; auto. ++ destruct (external_function_eq ef ef0 && typelist_eq args args0 && + type_eq res res0 && calling_convention_eq cc cc0) eqn:E'; inv H2. + InvBooleans. subst ef0. econstructor; split. + simpl; rewrite dec_eq_true; eauto. + left; constructor. congruence. +- intros. exists tt. auto. +- replace (program_of_program p) with pp. auto. inv E; destruct pp; auto. +Qed. diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index aa320f20..6e2749bd 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -15,21 +15,11 @@ (** Typing rules and type-checking for the Compcert C language *) -Require Import Coqlib. Require Import String. -Require Import Maps. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Events. -Require Import AST. -Require Import Ctypes. -Require Import Cop. -Require Import Csyntax. -Require Import Csem. -Require Import Errors. +Require Import Coqlib Maps Integers Floats Errors. +Require Import AST Linking. +Require Import Values Memory Globalenvs Events. +Require Import Ctypes Cop Csyntax Csem. Local Open Scope error_monad_scope. @@ -911,8 +901,8 @@ Definition retype_fundef (ce: composite_env) (e: typenv) (fd: fundef) : res fund Definition typecheck_program (p: program) : res program := let e := bind_globdef (PTree.empty _) p.(prog_defs) in let ce := p.(prog_comp_env) in - do defs <- transf_globdefs (retype_fundef ce e) (fun v => OK v) p.(prog_defs); - OK {| prog_defs := defs; + do tp <- transform_partial_program (retype_fundef ce e) p; + OK {| prog_defs := tp.(AST.prog_defs); prog_public := p.(prog_public); prog_main := p.(prog_main); prog_types := p.(prog_types); @@ -1325,32 +1315,29 @@ Theorem typecheck_program_sound: forall p p', typecheck_program p = OK p' -> wt_program p'. Proof. unfold typecheck_program; intros. monadInv H. - rename x into defs. + rename x into tp. constructor; simpl. set (ce := prog_comp_env p) in *. set (e := bind_globdef (PTree.empty type) (prog_defs p)) in *. - set (e' := bind_globdef (PTree.empty type) defs) in *. - assert (MATCH: - list_forall2 (match_globdef (fun f tf => retype_fundef ce e f = OK tf) (fun v tv => tv = v)) (prog_defs p) defs). - { - revert EQ; generalize (prog_defs p) defs. - induction l as [ | [id gd] l ]; intros l'; simpl; intros. - inv EQ. constructor. - destruct gd as [f | v]. - destruct (retype_fundef ce e f) as [tf|msg] eqn:R; monadInv EQ. - constructor; auto. constructor; auto. - monadInv EQ. constructor; auto. destruct v; constructor; auto. } + set (e' := bind_globdef (PTree.empty type) (AST.prog_defs tp)) in *. + assert (M: match_program (fun ctx f tf => retype_fundef ce e f = OK tf) eq p tp) + by (eapply match_transform_partial_program; eauto). + destruct M as (MATCH & _). simpl in MATCH. assert (ENVS: e' = e). - { unfold e, e'. revert MATCH; generalize (prog_defs p) defs (PTree.empty type). + { unfold e, e'. revert MATCH; generalize (prog_defs p) (AST.prog_defs tp) (PTree.empty type). induction l as [ | [id gd] l ]; intros l' t M; inv M. - auto. inv H1; simpl; auto. replace (type_of_fundef f2) with (type_of_fundef f1); auto. - unfold retype_fundef in H4. destruct f1; monadInv H4; auto. monadInv EQ0; auto. + auto. + destruct b1 as [id' gd']; destruct H1; simpl in *. inv H0; simpl. + replace (type_of_fundef f2) with (type_of_fundef f1); auto. + unfold retype_fundef in H2. destruct f1; monadInv H2; auto. monadInv EQ0; auto. + inv H1. simpl. auto. } rewrite ENVS. - intros id f. revert MATCH; generalize (prog_defs p) defs. induction 1; simpl; intros. + intros id f. revert MATCH; generalize (prog_defs p) (AST.prog_defs tp). + induction 1; simpl; intros. contradiction. - destruct H0; auto. subst b1; inv H. destruct f1; simpl in H2. - monadInv H2. eapply retype_function_sound; eauto. congruence. + destruct H0; auto. subst b1; inv H. simpl in H1. inv H1. + destruct f1; monadInv H4. eapply retype_function_sound; eauto. Qed. (** * Subject reduction *) @@ -2119,28 +2106,3 @@ Proof. Qed. End PRESERVATION. - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 9c662f5e..945f0465 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -647,7 +647,7 @@ Qed. Lemma transl_init_single_size: forall ty a data, transl_init_single ge ty a = OK data -> - Genv.init_data_size data = sizeof ge ty. + init_data_size data = sizeof ge ty. Proof. intros. monadInv H. destruct x0. - monadInv EQ2. @@ -664,7 +664,7 @@ Proof. inv EQ2; auto. Qed. -Notation idlsize := Genv.init_data_list_size. +Notation idlsize := init_data_list_size. Remark padding_size: forall frm to, frm <= to -> idlsize (tr_padding frm to) = to - frm. diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index a5a6ad66..c88c4db5 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -512,9 +512,9 @@ Local Open Scope error_monad_scope. Definition transl_fundef (fd: Csyntax.fundef) : res fundef := match fd with - | Csyntax.Internal f => + | Internal f => do tf <- transl_function f; OK (Internal tf) - | Csyntax.External ef targs tres cc => + | External ef targs tres cc => OK (External ef targs tres cc) end. @@ -523,6 +523,6 @@ Definition transl_program (p: Csyntax.program) : res program := OK {| prog_defs := AST.prog_defs p1; prog_public := AST.prog_public p1; prog_main := AST.prog_main p1; - prog_types := Csyntax.prog_types p; - prog_comp_env := Csyntax.prog_comp_env p; - prog_comp_env_eq := Csyntax.prog_comp_env_eq p |}. + prog_types := prog_types p; + prog_comp_env := prog_comp_env p; + prog_comp_env_eq := prog_comp_env_eq p |}. 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. diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index 4077d7df..e3dfe896 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -12,18 +12,9 @@ (** Relational specification of expression simplification. *) -Require Import Coqlib. -Require Import Errors. -Require Import Maps. -Require Import Integers. -Require Import Floats. -Require Import Memory. -Require Import AST. -Require Import Ctypes. -Require Import Cop. -Require Import Csyntax. -Require Import Clight. -Require Import SimplExpr. +Require Import Coqlib Maps Errors Integers Floats. +Require Import AST Linking Memory. +Require Import Ctypes Cop Csyntax Clight SimplExpr. Section SPEC. @@ -1088,8 +1079,7 @@ Opaque transl_expression transl_expr_stmt. monadInv TR; constructor; eauto. Qed. -(** Relational presentation for the transformation of functions, fundefs, and va -riables. *) +(** Relational presentation for the transformation of functions, fundefs, and variables. *) Inductive tr_function: Csyntax.function -> Clight.function -> Prop := | tr_function_intro: forall f tf, @@ -1103,9 +1093,9 @@ Inductive tr_function: Csyntax.function -> Clight.function -> Prop := Inductive tr_fundef: Csyntax.fundef -> Clight.fundef -> Prop := | tr_internal: forall f tf, tr_function f tf -> - tr_fundef (Csyntax.Internal f) (Clight.Internal tf) + tr_fundef (Internal f) (Internal tf) | tr_external: forall ef targs tres cconv, - tr_fundef (Csyntax.External ef targs tres cconv) (External ef targs tres cconv). + tr_fundef (External ef targs tres cconv) (External ef targs tres cconv). Lemma transl_function_spec: forall f tf, @@ -1128,30 +1118,5 @@ Proof. + constructor. Qed. -Lemma transl_globdefs_spec: - forall l l', - transf_globdefs transl_fundef (fun v : type => OK v) l = OK l' -> - list_forall2 (match_globdef tr_fundef (fun v1 v2 => v1 = v2)) l l'. -Proof. - induction l; simpl; intros. -- inv H. constructor. -- destruct a as [id gd]. destruct gd. - + destruct (transl_fundef f) as [tf | ?] eqn:E1; Errors.monadInv H. - constructor; eauto. constructor. eapply transl_fundef_spec; eauto. - + Errors.monadInv H. - constructor; eauto. destruct v; constructor; auto. -Qed. - -Theorem transl_program_spec: - forall p tp, - transl_program p = OK tp -> - match_program tr_fundef (fun v1 v2 => v1 = v2) nil (Csyntax.prog_main p) p tp. -Proof. - unfold transl_program, transform_partial_program; intros. Errors.monadInv H. Errors.monadInv EQ; simpl. - split; auto. exists x0; split. - eapply transl_globdefs_spec; eauto. - rewrite <- app_nil_end; auto. -Qed. - End SPEC. diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v index c4b1054d..580f02c2 100644 --- a/cfrontend/SimplLocals.v +++ b/cfrontend/SimplLocals.v @@ -15,13 +15,9 @@ Require Import FSets. Require FSetAVL. -Require Import Coqlib. -Require Import Ordered. -Require Import Errors. -Require Import AST. -Require Import Ctypes. -Require Import Cop. -Require Import Clight. +Require Import Coqlib Ordered Errors. +Require Import AST Linking. +Require Import Ctypes Cop Clight. Require Compopts. Open Scope error_monad_scope. diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index a47036bf..e8b1203c 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, @@ -2172,8 +2150,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 +2311,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 +2334,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 +2367,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. + |