diff options
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/C2C.ml | 2 | ||||
| -rw-r--r-- | cfrontend/Cexec.v | 5 | ||||
| -rw-r--r-- | cfrontend/Clight.v | 46 | ||||
| -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/Csyntax.v | 62 | ||||
| -rw-r--r-- | cfrontend/Ctypes.v | 529 | ||||
| -rw-r--r-- | cfrontend/Ctyping.v | 80 | ||||
| -rw-r--r-- | cfrontend/Initializersproof.v | 4 | ||||
| -rw-r--r-- | cfrontend/PrintClight.ml | 2 | ||||
| -rw-r--r-- | cfrontend/PrintCsyntax.ml | 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 |
18 files changed, 1093 insertions, 649 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index e4001e6b..418fa702 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -1090,6 +1090,7 @@ let convertFundef loc env fd = (** External function declaration *) let re_builtin = Str.regexp "__builtin_" +let re_runtime = Str.regexp "__i64_" let convertFundecl env (sto, id, ty, optinit) = let (args, res, cconv) = @@ -1102,6 +1103,7 @@ let convertFundecl env (sto, id, ty, optinit) = let ef = if id.name = "malloc" then EF_malloc else if id.name = "free" then EF_free else + if Str.string_match re_runtime id.name 0 then EF_runtime(id'', sg) else if Str.string_match re_builtin id.name 0 && List.mem_assoc id.name builtins.functions then EF_builtin(id'', sg) diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 00d77b00..bf88e033 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -536,6 +536,7 @@ Definition do_external (ef: external_function): match ef with | EF_external name sg => do_external_function name sg ge | EF_builtin name sg => do_external_function name sg ge + | EF_runtime name sg => do_external_function name sg ge | EF_vload chunk => do_ef_volatile_load chunk | EF_vstore chunk => do_ef_volatile_store chunk | EF_malloc => do_ef_malloc @@ -558,6 +559,8 @@ Proof with try congruence. eapply do_external_function_sound; eauto. (* EF_builtin *) eapply do_external_function_sound; eauto. +(* EF_runtime *) + eapply do_external_function_sound; eauto. (* EF_vload *) unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs... mydestr. destruct p as [[w'' t''] v]; mydestr. @@ -604,6 +607,8 @@ Proof. eapply do_external_function_complete; eauto. (* EF_builtin *) eapply do_external_function_complete; eauto. +(* EF_runtime *) + eapply do_external_function_complete; eauto. (* EF_vload *) inv H; unfold do_ef_volatile_load. exploit do_volatile_load_complete; eauto. intros EQ; rewrite EQ; auto. diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index 086f4654..e6426fb8 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -146,9 +146,7 @@ Definition var_names (vars: list(ident * type)) : list ident := (** Functions can either be defined ([Internal]) or declared as external functions ([External]). *) -Inductive fundef : Type := - | Internal: function -> fundef - | External: external_function -> typelist -> type -> calling_convention -> fundef. +Definition fundef := Ctypes.fundef function. (** The type of a function definition. *) @@ -163,45 +161,16 @@ Definition type_of_fundef (f: fundef) : type := (** ** Programs *) -(** A program is composed of: +(** As defined in module [Ctypes], a program, or compilation unit, is + composed of: - a list of definitions of functions and global variables; - the names of functions and global variables that are public (not static); - the name of the function that acts as entry point ("main" function). -- a list of definitions for structure and union names; -- the corresponding composite environment; -*) - -Record program : Type := { - prog_defs: list (ident * globdef fundef type); - prog_public: list ident; - prog_main: ident; - prog_types: list composite_definition; - prog_comp_env: composite_env; - prog_comp_env_eq: build_composite_env prog_types = OK prog_comp_env -}. +- a list of definitions for structure and union names +- the corresponding composite environment +- a proof that this environment is consistent with the definitions. *) -Definition program_of_program (p: program) : AST.program fundef type := - {| AST.prog_defs := p.(prog_defs); - AST.prog_public := p.(prog_public); - AST.prog_main := p.(prog_main) |}. - -Coercion program_of_program: program >-> AST.program. - -Program Definition make_program (types: list composite_definition) - (defs: list (ident * globdef fundef type)) - (public: list ident) - (main: ident): res program := - match build_composite_env types with - | OK env => - OK {| prog_defs := defs; - prog_public := public; - prog_main := main; - prog_types := types; - prog_comp_env := env; - prog_comp_env_eq := _ |} - | Error msg => - Error msg - end. +Definition program := Ctypes.program function. (** * Operational semantics *) @@ -774,4 +743,3 @@ Proof. eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. Qed. - 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 4f067fad..8bc97b99 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: @@ -487,27 +561,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. @@ -519,7 +599,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. @@ -673,8 +754,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. @@ -716,15 +797,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. @@ -735,10 +819,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. @@ -747,8 +831,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. @@ -759,34 +843,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 *) @@ -797,7 +877,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) @@ -821,13 +901,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. @@ -863,17 +943,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. @@ -903,6 +987,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 *) @@ -929,6 +1023,8 @@ Qed. Section EXPR. +Variable cunit: Clight.program. +Hypothesis LINK: linkorder cunit prog. Variable e: Clight.env. Variable le: temp_env. Variable m: mem. @@ -938,11 +1034,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). @@ -965,9 +1061,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. @@ -981,11 +1077,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. @@ -994,21 +1092,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. @@ -1062,71 +1160,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. @@ -1135,89 +1237,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'] | ]. @@ -1232,9 +1335,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. @@ -1242,10 +1345,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. @@ -1261,11 +1364,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. @@ -1273,62 +1377,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. @@ -1337,7 +1440,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. @@ -1347,9 +1450,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. @@ -1357,7 +1460,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. @@ -1367,16 +1470,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. @@ -1384,32 +1486,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. @@ -1425,7 +1527,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. @@ -1433,57 +1535,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. @@ -1495,17 +1594,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: @@ -1519,10 +1615,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/Csyntax.v b/cfrontend/Csyntax.v index 89d0b2bf..fd7a6b96 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -15,14 +15,9 @@ (** Abstract syntax for the Compcert C language *) -Require Import Coqlib. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import AST. -Require Import Errors. -Require Import Ctypes. -Require Import Cop. +Require Import Coqlib Maps Integers Floats Errors. +Require Import AST Linking Values. +Require Import Ctypes Cop. (** ** Expressions *) @@ -191,9 +186,7 @@ Definition var_names (vars: list(ident * type)) : list ident := (** Functions can either be defined ([Internal]) or declared as external functions ([External]). *) -Inductive fundef : Type := - | Internal: function -> fundef - | External: external_function -> typelist -> type -> calling_convention -> fundef. +Definition fundef := Ctypes.fundef function. (** The type of a function definition. *) @@ -206,50 +199,15 @@ Definition type_of_fundef (f: fundef) : type := | External id args res cc => Tfunction args res cc end. -(** ** Programs *) +(** ** Programs and compilation units *) -(** A "pre-program", as produced by the elaborator is composed of: +(** As defined in module [Ctypes], a program, or compilation unit, is + composed of: - a list of definitions of functions and global variables; - the names of functions and global variables that are public (not static); - the name of the function that acts as entry point ("main" function). - a list of definitions for structure and union names +- the corresponding composite environment +- a proof that this environment is consistent with the definitions. *) -A program is composed of the same information, plus the corresponding -composite environment, and a proof that this environment is consistent -with the composite definitions. *) - -Record pre_program : Type := { - pprog_defs: list (ident * globdef fundef type); - pprog_public: list ident; - pprog_main: ident; - pprog_types: list composite_definition -}. - -Record program : Type := { - prog_defs: list (ident * globdef fundef type); - prog_public: list ident; - prog_main: ident; - prog_types: list composite_definition; - prog_comp_env: composite_env; - prog_comp_env_eq: build_composite_env prog_types = OK prog_comp_env -}. - -Definition program_of_program (p: program) : AST.program fundef type := - {| AST.prog_defs := p.(prog_defs); - AST.prog_public := p.(prog_public); - AST.prog_main := p.(prog_main) |}. - -Coercion program_of_program: program >-> AST.program. - -Program Definition program_of_pre_program (p: pre_program) : res program := - match build_composite_env p.(pprog_types) with - | Error e => Error e - | OK ce => - OK {| prog_defs := p.(pprog_defs); - prog_public := p.(pprog_public); - prog_main := p.(pprog_main); - prog_types := p.(pprog_types); - prog_comp_env := ce; - prog_comp_env_eq := _ |} - end. - +Definition program := Ctypes.program function. diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 78345b42..9faa6d40 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -15,10 +15,8 @@ (** Type expressions for the Compcert C and Clight languages *) -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Errors. +Require Import Axioms Coqlib Maps Errors. +Require Import AST Linking. Require Archi. (** * Syntax of types *) @@ -157,6 +155,20 @@ Definition members : Type := list (ident * type). Inductive composite_definition : Type := Composite (id: ident) (su: struct_or_union) (m: members) (a: attr). +Definition name_composite_def (c: composite_definition) : ident := + match c with Composite id su m a => id end. + +Definition composite_def_eq (x y: composite_definition): {x=y} + {x<>y}. +Proof. + decide equality. +- decide equality. decide equality. apply N.eq_dec. apply bool_dec. +- apply list_eq_dec. decide equality. apply type_eq. apply ident_eq. +- decide equality. +- apply ident_eq. +Defined. + +Global Opaque composite_def_eq. + (** For type-checking, compilation and semantics purposes, the composite definitions are collected in the following [composite_env] environment. The [composite] record contains additional information compared with @@ -960,6 +972,29 @@ Record composite_consistent (env: composite_env) (co: composite) : Prop := { Definition composite_env_consistent (env: composite_env) : Prop := forall id co, env!id = Some co -> composite_consistent env co. +Lemma composite_consistent_stable: + forall (env env': composite_env) + (EXTENDS: forall id co, env!id = Some co -> env'!id = Some co) + co, + composite_consistent env co -> composite_consistent env' co. +Proof. + intros. destruct H as [A B C D]. constructor. + eapply complete_members_stable; eauto. + symmetry; rewrite B. f_equal. apply alignof_composite_stable; auto. + symmetry; rewrite C. f_equal. apply sizeof_composite_stable; auto. + symmetry; rewrite D. apply rank_members_stable; auto. +Qed. + +Lemma composite_of_def_consistent: + forall env id su m a co, + composite_of_def env id su m a = OK co -> + composite_consistent env co. +Proof. + unfold composite_of_def; intros. + destruct (env!id); try discriminate. destruct (complete_members env m) eqn:C; inv H. + constructor; auto. +Qed. + Theorem build_composite_env_consistent: forall defs env, build_composite_env defs = OK env -> composite_env_consistent env. Proof. @@ -973,28 +1008,15 @@ Proof. - destruct d1; monadInv H. eapply IHdefs; eauto. set (env1 := PTree.set id x env0) in *. - unfold composite_of_def in EQ. - destruct (env0!id) eqn:E; try discriminate. - destruct (complete_members env0 m) eqn:C; inversion EQ; clear EQ. + assert (env0!id = None). + { unfold composite_of_def in EQ. destruct (env0!id). discriminate. auto. } assert (forall id1 co1, env0!id1 = Some co1 -> env1!id1 = Some co1). { intros. unfold env1. rewrite PTree.gso; auto. congruence. } - red; intros. unfold env1 in H2; rewrite PTree.gsspec in H2; destruct (peq id0 id). + red; intros. apply composite_consistent_stable with env0; auto. + unfold env1 in H2; rewrite PTree.gsspec in H2; destruct (peq id0 id). + subst id0. inversion H2; clear H2. subst co. -(* - assert (A: alignof_composite env1 m = alignof_composite env0 m) - by (apply alignof_composite_stable; assumption). -*) - rewrite <- H1; constructor; simpl. -* eapply complete_members_stable; eauto. -* f_equal. symmetry. apply alignof_composite_stable; auto. -* f_equal. symmetry. apply sizeof_composite_stable; auto. -* symmetry. apply rank_members_stable; auto. -+ exploit H0; eauto. intros [P Q R S]. - constructor; intros. -* eapply complete_members_stable; eauto. -* rewrite Q. f_equal. symmetry. apply alignof_composite_stable; auto. -* rewrite R. f_equal. symmetry. apply sizeof_composite_stable; auto. -* rewrite S. symmetry; apply rank_members_stable; auto. + eapply composite_of_def_consistent; eauto. ++ eapply H0; eauto. Qed. (** Moreover, every composite definition is reflected in the composite environment. *) @@ -1018,6 +1040,29 @@ Proof. subst x; auto. Qed. +Theorem build_composite_env_domain: + forall env defs id co, + build_composite_env defs = OK env -> + env!id = Some co -> + In (Composite id (co_su co) (co_members co) (co_attr co)) defs. +Proof. + intros env0 defs0 id co. + assert (REC: forall l env env', + add_composite_definitions env l = OK env' -> + env'!id = Some co -> + env!id = Some co \/ In (Composite id (co_su co) (co_members co) (co_attr co)) l). + { induction l; simpl; intros. + - inv H; auto. + - destruct a; monadInv H. exploit IHl; eauto. + unfold composite_of_def in EQ. destruct (env!id0) eqn:E; try discriminate. + destruct (complete_members env m) eqn:C; simplify_eq EQ. clear EQ; intros EQ. + rewrite PTree.gsspec. intros [A|A]; auto. + destruct (peq id id0); auto. + inv A. rewrite <- H1; auto. + } + intros. exploit REC; eauto. rewrite PTree.gempty. intuition congruence. +Qed. + (** As a corollay, in a consistent environment, the rank of a composite type is strictly greater than the ranks of its member types. *) @@ -1054,3 +1099,441 @@ Proof. exploit (rank_type_members ce); eauto. omega. Qed. + +(** * Programs and compilation units *) + +(** The definitions in this section are parameterized over a type [F] of + internal function definitions, so that they apply both to CompCert C and to Clight. *) + +Set Implicit Arguments. + +Section PROGRAMS. + +Variable F: Type. + +(** Functions can either be defined ([Internal]) or declared as + external functions ([External]). *) + +Inductive fundef : Type := + | Internal: F -> fundef + | External: external_function -> typelist -> type -> calling_convention -> fundef. + +(** A program, or compilation unit, is composed of: +- a list of definitions of functions and global variables; +- the names of functions and global variables that are public (not static); +- the name of the function that acts as entry point ("main" function). +- a list of definitions for structure and union names +- the corresponding composite environment +- a proof that this environment is consistent with the definitions. *) + +Record program : Type := { + prog_defs: list (ident * globdef fundef type); + prog_public: list ident; + prog_main: ident; + prog_types: list composite_definition; + prog_comp_env: composite_env; + prog_comp_env_eq: build_composite_env prog_types = OK prog_comp_env +}. + +Definition program_of_program (p: program) : AST.program fundef type := + {| AST.prog_defs := p.(prog_defs); + AST.prog_public := p.(prog_public); + AST.prog_main := p.(prog_main) |}. + +Coercion program_of_program: program >-> AST.program. + +Program Definition make_program (types: list composite_definition) + (defs: list (ident * globdef fundef type)) + (public: list ident) + (main: ident) : res program := + match build_composite_env types with + | Error e => Error e + | OK ce => + OK {| prog_defs := defs; + prog_public := public; + prog_main := main; + prog_types := types; + prog_comp_env := ce; + prog_comp_env_eq := _ |} + end. + +End PROGRAMS. + +Arguments External {F} _ _ _ _. + +Unset Implicit Arguments. + +(** * Separate compilation and linking *) + +(** ** Linking types *) + +Instance Linker_types : Linker type := { + link := fun t1 t2 => if type_eq t1 t2 then Some t1 else None; + linkorder := fun t1 t2 => t1 = t2 +}. +Proof. + auto. + intros; congruence. + intros. destruct (type_eq x y); inv H. auto. +Defined. + +Global Opaque Linker_types. + +(** ** Linking composite definitions *) + +Definition check_compat_composite (l: list composite_definition) (cd: composite_definition) : bool := + List.forallb + (fun cd' => + if ident_eq (name_composite_def cd') (name_composite_def cd) then composite_def_eq cd cd' else true) + l. + +Definition filter_redefs (l1 l2: list composite_definition) := + let names1 := map name_composite_def l1 in + List.filter (fun cd => negb (In_dec ident_eq (name_composite_def cd) names1)) l2. + +Definition link_composite_defs (l1 l2: list composite_definition): option (list composite_definition) := + if List.forallb (check_compat_composite l2) l1 + then Some (l1 ++ filter_redefs l1 l2) + else None. + +Lemma link_composite_def_inv: + forall l1 l2 l, + link_composite_defs l1 l2 = Some l -> + (forall cd1 cd2, In cd1 l1 -> In cd2 l2 -> name_composite_def cd2 = name_composite_def cd1 -> cd2 = cd1) + /\ l = l1 ++ filter_redefs l1 l2 + /\ (forall x, In x l <-> In x l1 \/ In x l2). +Proof. + unfold link_composite_defs; intros. + destruct (forallb (check_compat_composite l2) l1) eqn:C; inv H. + assert (A: + forall cd1 cd2, In cd1 l1 -> In cd2 l2 -> name_composite_def cd2 = name_composite_def cd1 -> cd2 = cd1). + { rewrite forallb_forall in C. intros. + apply C in H. unfold check_compat_composite in H. rewrite forallb_forall in H. + apply H in H0. rewrite H1, dec_eq_true in H0. symmetry; eapply proj_sumbool_true; eauto. } + split. auto. split. auto. + unfold filter_redefs; intros. + rewrite in_app_iff. rewrite filter_In. intuition auto. + destruct (in_dec ident_eq (name_composite_def x) (map name_composite_def l1)); simpl; auto. + exploit list_in_map_inv; eauto. intros (y & P & Q). + assert (x = y) by eauto. subst y. auto. +Qed. + +Instance Linker_composite_defs : Linker (list composite_definition) := { + link := link_composite_defs; + linkorder := @List.incl composite_definition +}. +Proof. +- intros; apply incl_refl. +- intros; red; intros; eauto. +- intros. apply link_composite_def_inv in H; destruct H as (A & B & C). + split; red; intros; apply C; auto. +Defined. + +(** Connections with [build_composite_env]. *) + +Lemma add_composite_definitions_append: + forall l1 l2 env env'', + add_composite_definitions env (l1 ++ l2) = OK env'' <-> + exists env', add_composite_definitions env l1 = OK env' /\ add_composite_definitions env' l2 = OK env''. +Proof. + induction l1; simpl; intros. +- split; intros. exists env; auto. destruct H as (env' & A & B). congruence. +- destruct a; simpl. destruct (composite_of_def env id su m a); simpl. + apply IHl1. + split; intros. discriminate. destruct H as (env' & A & B); discriminate. +Qed. + +Lemma composite_eq: + forall su1 m1 a1 sz1 al1 r1 pos1 al2p1 szal1 + su2 m2 a2 sz2 al2 r2 pos2 al2p2 szal2, + su1 = su2 -> m1 = m2 -> a1 = a2 -> sz1 = sz2 -> al1 = al2 -> r1 = r2 -> + Build_composite su1 m1 a1 sz1 al1 r1 pos1 al2p1 szal1 = Build_composite su2 m2 a2 sz2 al2 r2 pos2 al2p2 szal2. +Proof. + intros. subst. + assert (pos1 = pos2) by apply proof_irr. + assert (al2p1 = al2p2) by apply proof_irr. + assert (szal1 = szal2) by apply proof_irr. + subst. reflexivity. +Qed. + +Lemma composite_of_def_eq: + forall env id co, + composite_consistent env co -> + env!id = None -> + composite_of_def env id (co_su co) (co_members co) (co_attr co) = OK co. +Proof. + intros. destruct H as [A B C D]. unfold composite_of_def. rewrite H0, A. + destruct co; simpl in *. f_equal. apply composite_eq; auto. rewrite C, B; auto. +Qed. + +Lemma composite_consistent_unique: + forall env co1 co2, + composite_consistent env co1 -> + composite_consistent env co2 -> + co_su co1 = co_su co2 -> + co_members co1 = co_members co2 -> + co_attr co1 = co_attr co2 -> + co1 = co2. +Proof. + intros. destruct H, H0. destruct co1, co2; simpl in *. apply composite_eq; congruence. +Qed. + +Lemma composite_of_def_stable: + forall (env env': composite_env) + (EXTENDS: forall id co, env!id = Some co -> env'!id = Some co) + id su m a co, + env'!id = None -> + composite_of_def env id su m a = OK co -> + composite_of_def env' id su m a = OK co. +Proof. + intros. + unfold composite_of_def in H0. + destruct (env!id) eqn:E; try discriminate. + destruct (complete_members env m) eqn:CM; try discriminate. + transitivity (composite_of_def env' id (co_su co) (co_members co) (co_attr co)). + inv H0; auto. + apply composite_of_def_eq; auto. + apply composite_consistent_stable with env; auto. + inv H0; constructor; auto. +Qed. + +Lemma link_add_composite_definitions: + forall l0 env0, + build_composite_env l0 = OK env0 -> + forall l env1 env1' env2, + add_composite_definitions env1 l = OK env1' -> + (forall id co, env1!id = Some co -> env2!id = Some co) -> + (forall id co, env0!id = Some co -> env2!id = Some co) -> + (forall id, env2!id = if In_dec ident_eq id (map name_composite_def l0) then env0!id else env1!id) -> + ((forall cd1 cd2, In cd1 l0 -> In cd2 l -> name_composite_def cd2 = name_composite_def cd1 -> cd2 = cd1)) -> + { env2' | + add_composite_definitions env2 (filter_redefs l0 l) = OK env2' + /\ (forall id co, env1'!id = Some co -> env2'!id = Some co) + /\ (forall id co, env0!id = Some co -> env2'!id = Some co) }. +Proof. + induction l; simpl; intros until env2; intros ACD AGREE1 AGREE0 AGREE2 UNIQUE. +- inv ACD. exists env2; auto. +- destruct a. destruct (composite_of_def env1 id su m a) as [x|e] eqn:EQ; try discriminate. + simpl in ACD. + generalize EQ. unfold composite_of_def at 1. + destruct (env1!id) eqn:E1; try congruence. + destruct (complete_members env1 m) eqn:CM1; try congruence. + intros EQ1. + simpl. destruct (in_dec ident_eq id (map name_composite_def l0)); simpl. ++ eapply IHl; eauto. +* intros. rewrite PTree.gsspec in H0. destruct (peq id0 id); auto. + inv H0. + exploit list_in_map_inv; eauto. intros ([id' su' m' a'] & P & Q). + assert (X: Composite id su m a = Composite id' su' m' a'). + { eapply UNIQUE. auto. auto. rewrite <- P; auto. } + inv X. + exploit build_composite_env_charact; eauto. intros (co' & U & V & W & X). + assert (co' = co). + { apply composite_consistent_unique with env2. + apply composite_consistent_stable with env0; auto. + eapply build_composite_env_consistent; eauto. + apply composite_consistent_stable with env1; auto. + inversion EQ1; constructor; auto. + inversion EQ1; auto. + inversion EQ1; auto. + inversion EQ1; auto. } + subst co'. apply AGREE0; auto. +* intros. rewrite AGREE2. destruct (in_dec ident_eq id0 (map name_composite_def l0)); auto. + rewrite PTree.gsspec. destruct (peq id0 id); auto. subst id0. contradiction. ++ assert (E2: env2!id = None). + { rewrite AGREE2. rewrite pred_dec_false by auto. auto. } + assert (E3: composite_of_def env2 id su m a = OK x). + { eapply composite_of_def_stable. eexact AGREE1. eauto. eauto. } + rewrite E3. simpl. eapply IHl; eauto. +* intros until co; rewrite ! PTree.gsspec. destruct (peq id0 id); auto. +* intros until co; rewrite ! PTree.gsspec. intros. destruct (peq id0 id); auto. + subst id0. apply AGREE0 in H0. congruence. +* intros. rewrite ! PTree.gsspec. destruct (peq id0 id); auto. subst id0. + rewrite pred_dec_false by auto. auto. +Qed. + +Theorem link_build_composite_env: + forall l1 l2 l env1 env2, + build_composite_env l1 = OK env1 -> + build_composite_env l2 = OK env2 -> + link l1 l2 = Some l -> + { env | + build_composite_env l = OK env + /\ (forall id co, env1!id = Some co -> env!id = Some co) + /\ (forall id co, env2!id = Some co -> env!id = Some co) }. +Proof. + intros. edestruct link_composite_def_inv as (A & B & C); eauto. + edestruct link_add_composite_definitions as (env & P & Q & R). + eexact H. + eexact H0. + instantiate (1 := env1). intros. rewrite PTree.gempty in H2; discriminate. + auto. + intros. destruct (in_dec ident_eq id (map name_composite_def l1)); auto. + rewrite PTree.gempty. destruct (env1!id) eqn:E1; auto. + exploit build_composite_env_domain. eexact H. eauto. + intros. apply (in_map name_composite_def) in H2. elim n; auto. + auto. + exists env; split; auto. subst l. apply add_composite_definitions_append. exists env1; auto. +Qed. + +(** ** Linking function definitions *) + +Definition link_fundef {F: Type} (fd1 fd2: fundef F) := + match fd1, fd2 with + | Internal _, Internal _ => None + | External ef1 targs1 tres1 cc1, External ef2 targs2 tres2 cc2 => + if external_function_eq ef1 ef2 + && typelist_eq targs1 targs2 + && type_eq tres1 tres2 + && calling_convention_eq cc1 cc2 + then Some (External ef1 targs1 tres1 cc1) + else None + | Internal f, External ef targs tres cc => + match ef with EF_external id sg => Some (Internal f) | _ => None end + | External ef targs tres cc, Internal f => + match ef with EF_external id sg => Some (Internal f) | _ => None end + end. + +Inductive linkorder_fundef {F: Type}: fundef F -> fundef F -> Prop := + | linkorder_fundef_refl: forall fd, + linkorder_fundef fd fd + | linkorder_fundef_ext_int: forall f id sg targs tres cc, + linkorder_fundef (External (EF_external id sg) targs tres cc) (Internal f). + +Instance Linker_fundef (F: Type): Linker (fundef F) := { + link := link_fundef; + linkorder := linkorder_fundef +}. +Proof. +- intros; constructor. +- intros. inv H; inv H0; constructor. +- intros x y z EQ. destruct x, y; simpl in EQ. ++ discriminate. ++ destruct e; inv EQ. split; constructor. ++ destruct e; inv EQ. split; constructor. ++ destruct (external_function_eq e e0 && typelist_eq t t1 && type_eq t0 t2 && calling_convention_eq c c0) eqn:A; inv EQ. + InvBooleans. subst. split; constructor. +Defined. + +Remark link_fundef_either: + forall (F: Type) (f1 f2 f: fundef F), link f1 f2 = Some f -> f = f1 \/ f = f2. +Proof. + simpl; intros. unfold link_fundef in H. destruct f1, f2; try discriminate. +- destruct e; inv H. auto. +- destruct e; inv H. auto. +- destruct (external_function_eq e e0 && typelist_eq t t1 && type_eq t0 t2 && calling_convention_eq c c0); inv H; auto. +Qed. + +Global Opaque Linker_fundef. + +(** ** Linking programs *) + +Definition lift_option {A: Type} (opt: option A) : { x | opt = Some x } + { opt = None }. +Proof. + destruct opt. left; exists a; auto. right; auto. +Defined. + +Definition link_program {F:Type} (p1 p2: program F): option (program F) := + match link (program_of_program p1) (program_of_program p2) with + | None => None + | Some p => + match lift_option (link p1.(prog_types) p2.(prog_types)) with + | inright _ => None + | inleft (exist typs EQ) => + match link_build_composite_env + p1.(prog_types) p2.(prog_types) typs + p1.(prog_comp_env) p2.(prog_comp_env) + p1.(prog_comp_env_eq) p2.(prog_comp_env_eq) EQ with + | exist env (conj P Q) => + Some {| prog_defs := p.(AST.prog_defs); + prog_public := p.(AST.prog_public); + prog_main := p.(AST.prog_main); + prog_types := typs; + prog_comp_env := env; + prog_comp_env_eq := P |} + end + end + end. + +Definition linkorder_program {F: Type} (p1 p2: program F) : Prop := + linkorder (program_of_program p1) (program_of_program p2) + /\ (forall id co, p1.(prog_comp_env)!id = Some co -> p2.(prog_comp_env)!id = Some co). + +Instance Linker_program (F: Type): Linker (program F) := { + link := link_program; + linkorder := linkorder_program +}. +Proof. +- intros; split. apply linkorder_refl. auto. +- intros. destruct H, H0. split. eapply linkorder_trans; eauto. + intros; auto. +- intros until z. unfold link_program. + destruct (link (program_of_program x) (program_of_program y)) as [p|] eqn:LP; try discriminate. + destruct (lift_option (link (prog_types x) (prog_types y))) as [[typs EQ]|EQ]; try discriminate. + destruct (link_build_composite_env (prog_types x) (prog_types y) typs + (prog_comp_env x) (prog_comp_env y) (prog_comp_env_eq x) + (prog_comp_env_eq y) EQ) as (env & P & Q & R). + destruct (link_linkorder _ _ _ LP). + intros X; inv X. + split; split; auto. +Defined. + +Global Opaque Linker_program. + +(** ** Commutation between linking and program transformations *) + +Section LINK_MATCH_PROGRAM. + +Context {F G: Type}. +Variable match_fundef: fundef F -> fundef G -> Prop. + +Hypothesis link_match_fundef: + forall f1 tf1 f2 tf2 f, + link f1 f2 = Some f -> + match_fundef f1 tf1 -> match_fundef f2 tf2 -> + exists tf, link tf1 tf2 = Some tf /\ match_fundef f tf. + +Let match_program (p: program F) (tp: program G) : Prop := + Linking.match_program (fun ctx f tf => match_fundef f tf) eq p tp + /\ prog_types tp = prog_types p. + +Theorem link_match_program: + forall p1 p2 tp1 tp2 p, + link p1 p2 = Some p -> match_program p1 tp1 -> match_program p2 tp2 -> + exists tp, link tp1 tp2 = Some tp /\ match_program p tp. +Proof. + intros. destruct H0, H1. +Local Transparent Linker_program. + simpl in H; unfold link_program in H. + destruct (link (program_of_program p1) (program_of_program p2)) as [pp|] eqn:LP; try discriminate. + assert (A: exists tpp, + link (program_of_program tp1) (program_of_program tp2) = Some tpp + /\ Linking.match_program (fun ctx f tf => match_fundef f tf) eq pp tpp). + { eapply Linking.link_match_program. + - intros. exploit link_match_fundef; eauto. intros (tf & A & B). exists tf; auto. + - intros. + Local Transparent Linker_types. + simpl in *. destruct (type_eq v1 v2); inv H4. subst v tv2. exists tv1; rewrite dec_eq_true; auto. + - eauto. + - eauto. + - eauto. + - apply (link_linkorder _ _ _ LP). + - apply (link_linkorder _ _ _ LP). } + destruct A as (tpp & TLP & MP). + simpl; unfold link_program. rewrite TLP. + destruct (lift_option (link (prog_types p1) (prog_types p2))) as [[typs EQ]|EQ]; 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). + rewrite <- H2, <- H3 in EQ. + destruct (lift_option (link (prog_types tp1) (prog_types tp2))) as [[ttyps EQ']|EQ']; try congruence. + assert (ttyps = typs) by congruence. subst ttyps. + destruct (link_build_composite_env (prog_types tp1) (prog_types tp2) typs + (prog_comp_env tp1) (prog_comp_env tp2) (prog_comp_env_eq tp1) + (prog_comp_env_eq tp2) EQ') as (tenv & R & S). + assert (tenv = env) by congruence. subst tenv. + econstructor; split; eauto. inv H. split; auto. + unfold program_of_program; simpl. destruct pp, tpp; exact MP. +Qed. + +End LINK_MATCH_PROGRAM. diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index f59fb396..440e4e84 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 *) @@ -2122,28 +2109,3 @@ Proof. Qed. End PRESERVATION. - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index e6fcad8c..d5f39d7d 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -649,7 +649,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. @@ -666,7 +666,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/PrintClight.ml b/cfrontend/PrintClight.ml index 9600b3fa..8a321757 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -258,7 +258,7 @@ let print_function p id f = let print_fundef p id fd = match fd with - | External(EF_external(_,_), args, res, cconv) -> + | External((EF_external _ | EF_runtime _), args, res, cconv) -> fprintf p "extern %s;@ @ " (name_cdecl (extern_atom id) (Tfunction(args, res, cconv))) | External(_, _, _, _) -> diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index f68f520d..d884100b 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -264,6 +264,8 @@ let rec expr p (prec, e) = (camlstring_of_coqstring txt) exprlist (false, args) | Ebuiltin(EF_external(id, sg), _, args, _) -> fprintf p "%s@[<hov 1>(%a)@]" (camlstring_of_coqstring id) exprlist (true, args) + | Ebuiltin(EF_runtime(id, sg), _, args, _) -> + fprintf p "%s@[<hov 1>(%a)@]" (camlstring_of_coqstring id) exprlist (true, args) | Ebuiltin(EF_inline_asm(txt, sg, clob), _, args, _) -> extended_asm p txt None args clob | Ebuiltin(EF_debug(kind,txt,_),_,args,_) -> @@ -427,7 +429,7 @@ let print_function p id f = let print_fundef p id fd = match fd with - | External(EF_external(_,_), args, res, cconv) -> + | External((EF_external _ | EF_runtime _), args, res, cconv) -> fprintf p "extern %s;@ @ " (name_cdecl (extern_atom id) (Tfunction(args, res, cconv))) | External(_, _, _, _) -> diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index a3af8114..bfdd8ab9 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 8baa7d46..64e52df8 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. @@ -1907,8 +1884,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. @@ -1918,8 +1894,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. @@ -2215,8 +2190,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 *) @@ -2246,15 +2220,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. @@ -2271,7 +2244,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. @@ -2279,3 +2252,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 b94465a1..453a4c9a 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. @@ -1077,8 +1068,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, @@ -1092,9 +1082,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, @@ -1117,30 +1107,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 a86e3a01..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, @@ -2073,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. @@ -2235,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. @@ -2259,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. @@ -2292,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. + |