diff options
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/C2C.ml | 6 | ||||
-rw-r--r-- | cfrontend/Cexec.v | 63 | ||||
-rw-r--r-- | cfrontend/Clight.v | 54 | ||||
-rw-r--r-- | cfrontend/ClightBigstep.v | 8 | ||||
-rw-r--r-- | cfrontend/Cminorgen.v | 17 | ||||
-rw-r--r-- | cfrontend/Cminorgenproof.v | 63 | ||||
-rw-r--r-- | cfrontend/Cop.v | 253 | ||||
-rw-r--r-- | cfrontend/Csem.v | 37 | ||||
-rw-r--r-- | cfrontend/Cshmgen.v | 72 | ||||
-rw-r--r-- | cfrontend/Cshmgenproof.v | 600 | ||||
-rw-r--r-- | cfrontend/Cstrategy.v | 80 | ||||
-rw-r--r-- | cfrontend/Csyntax.v | 62 | ||||
-rw-r--r-- | cfrontend/Ctypes.v | 529 | ||||
-rw-r--r-- | cfrontend/Ctyping.v | 97 | ||||
-rw-r--r-- | cfrontend/Initializers.v | 2 | ||||
-rw-r--r-- | cfrontend/Initializersproof.v | 28 | ||||
-rw-r--r-- | cfrontend/PrintClight.ml | 8 | ||||
-rw-r--r-- | cfrontend/PrintCsyntax.ml | 16 | ||||
-rw-r--r-- | cfrontend/SimplExpr.v | 26 | ||||
-rw-r--r-- | cfrontend/SimplExprproof.v | 167 | ||||
-rw-r--r-- | cfrontend/SimplExprspec.v | 76 | ||||
-rw-r--r-- | cfrontend/SimplLocals.v | 10 | ||||
-rw-r--r-- | cfrontend/SimplLocalsproof.v | 208 |
23 files changed, 1493 insertions, 989 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 6eabfbf4..16e8a80d 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -1078,7 +1078,7 @@ let convertFundef loc env fd = a_access = Sections.Access_default; a_inline = fd.fd_inline && not fd.fd_vararg; (* PR#15 *) a_loc = loc }; - (id', Gfun(Csyntax.Internal + (id', Gfun(Ctypes.Internal {fn_return = ret; fn_callconv = convertCallconv fd.fd_vararg false fd.fd_attrib; fn_params = params; @@ -1088,6 +1088,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) = @@ -1100,11 +1101,12 @@ 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) else EF_external(id'', sg) in - (id', Gfun(Csyntax.External(ef, args, res, cconv))) + (id', Gfun(Ctypes.External(ef, args, res, cconv))) (** Initializers *) diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 7e966ffe..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. @@ -645,11 +650,11 @@ Section EXPRS. Variable e: env. Variable w: world. -Fixpoint sem_cast_arguments (vtl: list (val * type)) (tl: typelist) : option (list val) := +Fixpoint sem_cast_arguments (vtl: list (val * type)) (tl: typelist) (m: mem) : option (list val) := match vtl, tl with | nil, Tnil => Some nil | (v1,t1)::vtl, Tcons t1' tl => - do v <- sem_cast v1 t1 t1'; do vl <- sem_cast_arguments vtl tl; Some(v::vl) + do v <- sem_cast v1 t1 t1' m; do vl <- sem_cast_arguments vtl tl m; Some(v::vl) | _, _ => None end. @@ -772,7 +777,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | RV, Ecast r1 ty => match is_val r1 with | Some(v1, ty1) => - do v <- sem_cast v1 ty1 ty; + do v <- sem_cast v1 ty1 ty m; topred (Rred "red_cast" (Eval v ty) m E0) | None => incontext (fun x => Ecast x ty) (step_expr RV r1 m) @@ -811,7 +816,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match is_loc l1, is_val r2 with | Some(b, ofs, ty1), Some(v2, ty2) => check type_eq ty1 ty; - do v <- sem_cast v2 ty2 ty1; + do v <- sem_cast v2 ty2 ty1 m; do w',t,m' <- do_assign_loc w ty1 m b ofs v; topred (Rred "red_assign" (Eval v ty) m' t) | _, _ => @@ -856,7 +861,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | RV, Eparen r1 tycast ty => match is_val r1 with | Some (v1, ty1) => - do v <- sem_cast v1 ty1 tycast; + do v <- sem_cast v1 ty1 tycast m; topred (Rred "red_paren" (Eval v ty) m E0) | None => incontext (fun x => Eparen x tycast ty) (step_expr RV r1 m) @@ -867,7 +872,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match classify_fun tyf with | fun_case_f tyargs tyres cconv => do fd <- Genv.find_funct ge vf; - do vargs <- sem_cast_arguments vtl tyargs; + do vargs <- sem_cast_arguments vtl tyargs m; check type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv); topred (Callred "red_call" fd vargs ty m) | _ => stuck @@ -879,7 +884,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | RV, Ebuiltin ef tyargs rargs ty => match is_val_list rargs with | Some vtl => - do vargs <- sem_cast_arguments vtl tyargs; + do vargs <- sem_cast_arguments vtl tyargs m; match do_external ef w vargs m with | None => stuck | Some(w',t,v,m') => topred (Rred "red_builtin" (Eval v ty) m' t) @@ -915,7 +920,7 @@ Inductive imm_safe_t: kind -> expr -> mem -> Prop := context RV to C -> imm_safe_t to (C r) m | imm_safe_t_callred: forall to C r m fd args ty, - callred ge r fd args ty -> + callred ge r m fd args ty -> context RV to C -> imm_safe_t to (C r) m. @@ -961,7 +966,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty => exists v, sem_binary_operation ge op v1 ty1 v2 ty2 m = Some v | Ecast (Eval v1 ty1) ty => - exists v, sem_cast v1 ty1 ty = Some v + exists v, sem_cast v1 ty1 ty m = Some v | Eseqand (Eval v1 ty1) r2 ty => exists b, bool_val v1 ty1 m = Some b | Eseqor (Eval v1 ty1) r2 ty => @@ -970,7 +975,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := exists b, bool_val v1 ty1 m = Some b | Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty => exists v, exists m', exists t, exists w', - ty = ty1 /\ sem_cast v2 ty2 ty1 = Some v /\ assign_loc ge ty1 m b ofs v t m' /\ possible_trace w t w' + ty = ty1 /\ sem_cast v2 ty2 ty1 m = Some v /\ assign_loc ge ty1 m b ofs v t m' /\ possible_trace w t w' | Eassignop op (Eloc b ofs ty1) (Eval v2 ty2) tyres ty => exists t, exists v1, exists w', ty = ty1 /\ deref_loc ge ty1 m b ofs t v1 /\ possible_trace w t w' @@ -980,18 +985,18 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := | Ecomma (Eval v ty1) r2 ty => typeof r2 = ty | Eparen (Eval v1 ty1) tycast ty => - exists v, sem_cast v1 ty1 tycast = Some v + exists v, sem_cast v1 ty1 tycast m = Some v | Ecall (Eval vf tyf) rargs ty => exprlist_all_values rargs -> exists tyargs tyres cconv fd vl, classify_fun tyf = fun_case_f tyargs tyres cconv /\ Genv.find_funct ge vf = Some fd - /\ cast_arguments rargs tyargs vl + /\ cast_arguments m rargs tyargs vl /\ type_of_fundef fd = Tfunction tyargs tyres cconv | Ebuiltin ef tyargs rargs ty => exprlist_all_values rargs -> exists vargs t vres m' w', - cast_arguments rargs tyargs vargs + cast_arguments m rargs tyargs vargs /\ external_call ef ge vargs m t vres m' /\ possible_trace w t w' | _ => True @@ -1028,7 +1033,7 @@ Qed. Lemma callred_invert: forall r fd args ty m, - callred ge r fd args ty -> + callred ge r m fd args ty -> invert_expr_prop r m. Proof. intros. inv H. simpl. @@ -1124,7 +1129,7 @@ Definition reduction_ok (k: kind) (a: expr) (m: mem) (rd: reduction) : Prop := match k, rd with | LV, Lred _ l' m' => lred ge e a m l' m' | RV, Rred _ r' m' t => rred ge a m t r' m' /\ exists w', possible_trace w t w' - | RV, Callred _ fd args tyres m' => callred ge a fd args tyres /\ m' = m + | RV, Callred _ fd args tyres m' => callred ge a m fd args tyres /\ m' = m | LV, Stuckred => ~imm_safe_t k a m | RV, Stuckred => ~imm_safe_t k a m | _, _ => False @@ -1152,10 +1157,10 @@ Ltac monadInv := end. Lemma sem_cast_arguments_sound: - forall rargs vtl tyargs vargs, + forall m rargs vtl tyargs vargs, is_val_list rargs = Some vtl -> - sem_cast_arguments vtl tyargs = Some vargs -> - cast_arguments rargs tyargs vargs. + sem_cast_arguments vtl tyargs m = Some vargs -> + cast_arguments m rargs tyargs vargs. Proof. induction rargs; simpl; intros. inv H. destruct tyargs; simpl in H0; inv H0. constructor. @@ -1164,9 +1169,9 @@ Proof. Qed. Lemma sem_cast_arguments_complete: - forall al tyl vl, - cast_arguments al tyl vl -> - exists vtl, is_val_list al = Some vtl /\ sem_cast_arguments vtl tyl = Some vl. + forall m al tyl vl, + cast_arguments m al tyl vl -> + exists vtl, is_val_list al = Some vtl /\ sem_cast_arguments vtl tyl m = Some vl. Proof. induction 1. exists (@nil (val * type)); auto. @@ -1396,7 +1401,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* cast *) destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) - destruct (sem_cast v ty' ty) as [v'|] eqn:?... + destruct (sem_cast v ty' ty m) as [v'|] eqn:?... apply topred_ok; auto. split. apply red_cast; auto. exists w; constructor. (* depth *) eapply incontext_ok; eauto. @@ -1433,7 +1438,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; rewrite (is_loc_inv _ _ _ _ Heqo). rewrite (is_val_inv _ _ _ Heqo0). (* top *) destruct (type_eq ty1 ty)... subst ty1. - destruct (sem_cast v2 ty2 ty) as [v|] eqn:?... + destruct (sem_cast v2 ty2 ty m) as [v|] eqn:?... destruct (do_assign_loc w ty m b ofs v) as [[[w' t] m']|] eqn:?. exploit do_assign_loc_sound; eauto. intros [P Q]. apply topred_ok; auto. split. apply red_assign; auto. exists w'; auto. @@ -1478,7 +1483,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* top *) destruct (classify_fun tyf) as [tyargs tyres cconv|] eqn:?... destruct (Genv.find_funct ge vf) as [fd|] eqn:?... - destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?... + destruct (sem_cast_arguments vtl tyargs m) as [vargs|] eqn:?... destruct (type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv))... apply topred_ok; auto. red. split; auto. eapply red_call; eauto. eapply sem_cast_arguments_sound; eauto. @@ -1494,7 +1499,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; destruct (is_val_list rargs) as [vtl | ] eqn:?. exploit is_val_list_all_values; eauto. intros ALLVAL. (* top *) - destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?... + destruct (sem_cast_arguments vtl tyargs m) as [vargs|] eqn:?... destruct (do_external ef w vargs m) as [[[[? ?] v] m'] | ] eqn:?... exploit do_ef_external_sound; eauto. intros [EC PT]. apply topred_ok; auto. red. split; auto. eapply red_builtin; eauto. @@ -1514,7 +1519,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; (* paren *) destruct (is_val a) as [[v ty'] | ] eqn:?. rewrite (is_val_inv _ _ _ Heqo). (* top *) - destruct (sem_cast v ty' tycast) as [v'|] eqn:?... + destruct (sem_cast v ty' tycast m) as [v'|] eqn:?... apply topred_ok; auto. split. apply red_paren; auto. exists w; constructor. (* depth *) eapply incontext_ok; eauto. @@ -1607,7 +1612,7 @@ Qed. Lemma callred_topred: forall a fd args ty m, - callred ge a fd args ty -> + callred ge a m fd args ty -> exists rule, step_expr RV a m = topred (Callred rule fd args ty m). Proof. induction 1; simpl. @@ -1961,7 +1966,7 @@ Definition do_step (w: world) (s: state) : list transition := then ret "step_for_true" (State f s (Kfor3 a2 a3 s k) e m) else ret "step_for_false" (State f Sskip k e m) | Kreturn k => - do v' <- sem_cast v ty f.(fn_return); + do v' <- sem_cast v ty f.(fn_return) m; do m' <- Mem.free_list m (blocks_of_env ge e); ret "step_return_2" (Returnstate v' (call_cont k) m') | Kswitch1 sl k => @@ -2165,7 +2170,7 @@ Proof with (unfold ret; eauto with coqlib). apply extensionality; auto. (* callred *) unfold do_step; rewrite NOTVAL. - exploit callred_topred; eauto. instantiate (1 := m). instantiate (1 := w). instantiate (1 := e). + exploit callred_topred; eauto. instantiate (1 := w). instantiate (1 := e). intros (rule & STEP). exists rule. change (TR rule E0 (Callstate fd vargs (Kcall f e C ty k) m)) with (expr_final_state f k e (C, Callred rule fd vargs ty m)). apply in_map. diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index 8722da69..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 *) @@ -412,7 +381,7 @@ Inductive eval_expr: expr -> val -> Prop := eval_expr (Ebinop op a1 a2 ty) v | eval_Ecast: forall a ty v1 v, eval_expr a v1 -> - sem_cast v1 (typeof a) ty = Some v -> + sem_cast v1 (typeof a) ty m = Some v -> eval_expr (Ecast a ty) v | eval_Esizeof: forall ty1 ty, eval_expr (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1))) @@ -464,7 +433,7 @@ Inductive eval_exprlist: list expr -> typelist -> list val -> Prop := eval_exprlist nil Tnil nil | eval_Econs: forall a bl ty tyl v1 v2 vl, eval_expr a v1 -> - sem_cast v1 (typeof a) ty = Some v2 -> + sem_cast v1 (typeof a) ty m = Some v2 -> eval_exprlist bl tyl vl -> eval_exprlist (a :: bl) (Tcons ty tyl) (v2 :: vl). @@ -580,7 +549,7 @@ Inductive step: state -> trace -> state -> Prop := | step_assign: forall f a1 a2 k e le m loc ofs v2 v m', eval_lvalue e le m a1 loc ofs -> eval_expr e le m a2 v2 -> - sem_cast v2 (typeof a2) (typeof a1) = Some v -> + sem_cast v2 (typeof a2) (typeof a1) m = Some v -> assign_loc ge (typeof a1) m loc ofs v m' -> step (State f (Sassign a1 a2) k e le m) E0 (State f Sskip k e le m') @@ -647,7 +616,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (Returnstate Vundef (call_cont k) m') | step_return_1: forall f a k e le m v v' m', eval_expr e le m a v -> - sem_cast v (typeof a) f.(fn_return) = Some v' -> + sem_cast v (typeof a) f.(fn_return) m = Some v' -> Mem.free_list m (blocks_of_env e) = Some m' -> step (State f (Sreturn (Some a)) k e le m) E0 (Returnstate v' (call_cont k) m') @@ -774,4 +743,3 @@ Proof. eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. Qed. - diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v index ee653d50..92457586 100644 --- a/cfrontend/ClightBigstep.v +++ b/cfrontend/ClightBigstep.v @@ -60,11 +60,11 @@ Definition outcome_switch (out: outcome) : outcome := | o => o end. -Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop := +Definition outcome_result_value (out: outcome) (t: type) (v: val) (m: mem): Prop := match out, t with | Out_normal, Tvoid => v = Vundef | Out_return None, Tvoid => v = Vundef - | Out_return (Some (v',t')), ty => ty <> Tvoid /\ sem_cast v' t' t = Some v + | Out_return (Some (v',t')), ty => ty <> Tvoid /\ sem_cast v' t' t m = Some v | _, _ => False end. @@ -81,7 +81,7 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env -> | exec_Sassign: forall e le m a1 a2 loc ofs v2 v m', eval_lvalue ge e le m a1 loc ofs -> eval_expr ge e le m a2 v2 -> - sem_cast v2 (typeof a2) (typeof a1) = Some v -> + sem_cast v2 (typeof a2) (typeof a1) m = Some v -> assign_loc ge (typeof a1) m loc ofs v m' -> exec_stmt e le m (Sassign a1 a2) E0 le m' Out_normal @@ -168,7 +168,7 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) -> bind_parameters ge e m1 f.(fn_params) vargs m2 -> exec_stmt e (create_undef_temps f.(fn_temps)) m2 f.(fn_body) t le m3 out -> - outcome_result_value out f.(fn_return) vres -> + outcome_result_value out f.(fn_return) vres m3 -> Mem.free_list m3 (blocks_of_env ge e) = Some m4 -> eval_funcall m (Internal f) vargs t m4 vres | eval_funcall_external: forall m ef targs tres cconv vargs t vres m', 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/Cop.v b/cfrontend/Cop.v index b4784028..4ac56b04 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -130,7 +130,7 @@ Definition classify_cast (tfrom tto: type) : classify_cast_cases := | _, _ => cast_case_default end. -(** Semantics of casts. [sem_cast v1 t1 t2 = Some v2] if value [v1], +(** Semantics of casts. [sem_cast v1 t1 t2 m = Some v2] if value [v1], viewed with static type [t1], can be converted to type [t2], resulting in value [v2]. *) @@ -198,7 +198,7 @@ Definition cast_single_long (si : signedness) (f: float32) : option int64 := | Unsigned => Float32.to_longu f end. -Definition sem_cast (v: val) (t1 t2: type) : option val := +Definition sem_cast (v: val) (t1 t2: type) (m: mem): option val := match classify_cast t1 t2 with | cast_case_neutral => match v with @@ -273,6 +273,7 @@ Definition sem_cast (v: val) (t1 t2: type) : option val := | cast_case_p2bool => match v with | Vint i => Some (Vint (cast_int_int IBool Signed i)) + | Vptr b ofs => if Mem.weak_valid_pointer m b (Int.unsigned ofs) then Some Vone else None | _ => None end | cast_case_l2l => @@ -586,13 +587,13 @@ Definition sem_binarith (sem_long: signedness -> int64 -> int64 -> option val) (sem_float: float -> float -> option val) (sem_single: float32 -> float32 -> option val) - (v1: val) (t1: type) (v2: val) (t2: type) : option val := + (v1: val) (t1: type) (v2: val) (t2: type) (m: mem): option val := let c := classify_binarith t1 t2 in let t := binarith_type c in - match sem_cast v1 t1 t with + match sem_cast v1 t1 t m with | None => None | Some v1' => - match sem_cast v2 t2 t with + match sem_cast v2 t2 t m with | None => None | Some v2' => match c with @@ -637,18 +638,22 @@ Definition classify_add (ty1: type) (ty2: type) := | _, _ => add_default end. -Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) : option val := +Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) (m: mem): option val := match classify_add t1 t2 with | add_case_pi ty => (**r pointer plus integer *) match v1,v2 with | Vptr b1 ofs1, Vint n2 => Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) + | Vint n1, Vint n2 => + Some (Vint (Int.add n1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) | _, _ => None end | add_case_ip ty => (**r integer plus pointer *) match v1,v2 with | Vint n1, Vptr b2 ofs2 => Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof cenv ty)) n1))) + | Vint n1, Vint n2 => + Some (Vint (Int.add n2 (Int.mul (Int.repr (sizeof cenv ty)) n1))) | _, _ => None end | add_case_pl ty => (**r pointer plus long *) @@ -656,6 +661,9 @@ Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) | Vptr b1 ofs1, Vlong n2 => let n2 := Int.repr (Int64.unsigned n2) in Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) + | Vint n1, Vlong n2 => + let n2 := Int.repr (Int64.unsigned n2) in + Some (Vint (Int.add n1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) | _, _ => None end | add_case_lp ty => (**r long plus pointer *) @@ -663,6 +671,9 @@ Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) | Vlong n1, Vptr b2 ofs2 => let n1 := Int.repr (Int64.unsigned n1) in Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof cenv ty)) n1))) + | Vlong n1, Vint n2 => + let n1 := Int.repr (Int64.unsigned n1) in + Some (Vint (Int.add n2 (Int.mul (Int.repr (sizeof cenv ty)) n1))) | _, _ => None end | add_default => @@ -671,7 +682,7 @@ Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) (fun sg n1 n2 => Some(Vlong(Int64.add n1 n2))) (fun n1 n2 => Some(Vfloat(Float.add n1 n2))) (fun n1 n2 => Some(Vsingle(Float32.add n1 n2))) - v1 t1 v2 t2 + v1 t1 v2 t2 m end. (** *** Subtraction *) @@ -690,12 +701,14 @@ Definition classify_sub (ty1: type) (ty2: type) := | _, _ => sub_default end. -Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) : option val := +Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) (m:mem): option val := match classify_sub t1 t2 with | sub_case_pi ty => (**r pointer minus integer *) match v1,v2 with | Vptr b1 ofs1, Vint n2 => Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) + | Vint n1, Vint n2 => + Some (Vint (Int.sub n1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) | _, _ => None end | sub_case_pl ty => (**r pointer minus long *) @@ -703,6 +716,9 @@ Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) | Vptr b1 ofs1, Vlong n2 => let n2 := Int.repr (Int64.unsigned n2) in Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) + | Vint n1, Vlong n2 => + let n2 := Int.repr (Int64.unsigned n2) in + Some (Vint (Int.sub n1 (Int.mul (Int.repr (sizeof cenv ty)) n2))) | _, _ => None end | sub_case_pp ty => (**r pointer minus pointer *) @@ -722,20 +738,20 @@ Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) (fun sg n1 n2 => Some(Vlong(Int64.sub n1 n2))) (fun n1 n2 => Some(Vfloat(Float.sub n1 n2))) (fun n1 n2 => Some(Vsingle(Float32.sub n1 n2))) - v1 t1 v2 t2 + v1 t1 v2 t2 m end. (** *** Multiplication, division, modulus *) -Definition sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val := +Definition sem_mul (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val := sem_binarith (fun sg n1 n2 => Some(Vint(Int.mul n1 n2))) (fun sg n1 n2 => Some(Vlong(Int64.mul n1 n2))) (fun n1 n2 => Some(Vfloat(Float.mul n1 n2))) (fun n1 n2 => Some(Vsingle(Float32.mul n1 n2))) - v1 t1 v2 t2. + v1 t1 v2 t2 m. -Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val := +Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val := sem_binarith (fun sg n1 n2 => match sg with @@ -759,9 +775,9 @@ Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val := end) (fun n1 n2 => Some(Vfloat(Float.div n1 n2))) (fun n1 n2 => Some(Vsingle(Float32.div n1 n2))) - v1 t1 v2 t2. + v1 t1 v2 t2 m. -Definition sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val := +Definition sem_mod (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val := sem_binarith (fun sg n1 n2 => match sg with @@ -785,31 +801,31 @@ Definition sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val := end) (fun n1 n2 => None) (fun n1 n2 => None) - v1 t1 v2 t2. + v1 t1 v2 t2 m. -Definition sem_and (v1:val) (t1:type) (v2: val) (t2:type) : option val := +Definition sem_and (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val := sem_binarith (fun sg n1 n2 => Some(Vint(Int.and n1 n2))) (fun sg n1 n2 => Some(Vlong(Int64.and n1 n2))) (fun n1 n2 => None) (fun n1 n2 => None) - v1 t1 v2 t2. + v1 t1 v2 t2 m. -Definition sem_or (v1:val) (t1:type) (v2: val) (t2:type) : option val := +Definition sem_or (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val := sem_binarith (fun sg n1 n2 => Some(Vint(Int.or n1 n2))) (fun sg n1 n2 => Some(Vlong(Int64.or n1 n2))) (fun n1 n2 => None) (fun n1 n2 => None) - v1 t1 v2 t2. + v1 t1 v2 t2 m. -Definition sem_xor (v1:val) (t1:type) (v2: val) (t2:type) : option val := +Definition sem_xor (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val := sem_binarith (fun sg n1 n2 => Some(Vint(Int.xor n1 n2))) (fun sg n1 n2 => Some(Vlong(Int64.xor n1 n2))) (fun n1 n2 => None) (fun n1 n2 => None) - v1 t1 v2 t2. + v1 t1 v2 t2 m. (** *** Shifts *) @@ -931,7 +947,7 @@ Definition sem_cmp (c:comparison) Some(Val.of_bool(Float.cmp c n1 n2))) (fun n1 n2 => Some(Val.of_bool(Float32.cmp c n1 n2))) - v1 t1 v2 t2 + v1 t1 v2 t2 m end. (** ** Function applications *) @@ -988,14 +1004,14 @@ Definition sem_binary_operation (v1: val) (t1: type) (v2: val) (t2:type) (m: mem): option val := match op with - | Oadd => sem_add cenv v1 t1 v2 t2 - | Osub => sem_sub cenv v1 t1 v2 t2 - | Omul => sem_mul v1 t1 v2 t2 - | Omod => sem_mod v1 t1 v2 t2 - | Odiv => sem_div v1 t1 v2 t2 - | Oand => sem_and v1 t1 v2 t2 - | Oor => sem_or v1 t1 v2 t2 - | Oxor => sem_xor v1 t1 v2 t2 + | Oadd => sem_add cenv v1 t1 v2 t2 m + | Osub => sem_sub cenv v1 t1 v2 t2 m + | Omul => sem_mul v1 t1 v2 t2 m + | Omod => sem_mod v1 t1 v2 t2 m + | Odiv => sem_div v1 t1 v2 t2 m + | Oand => sem_and v1 t1 v2 t2 m + | Oor => sem_or v1 t1 v2 t2 m + | Oxor => sem_xor v1 t1 v2 t2 m | Oshl => sem_shl v1 t1 v2 t2 | Oshr => sem_shr v1 t1 v2 t2 | Oeq => sem_cmp Ceq v1 t1 v2 t2 m @@ -1006,10 +1022,10 @@ Definition sem_binary_operation | Oge => sem_cmp Cge v1 t1 v2 t2 m end. -Definition sem_incrdecr (cenv: composite_env) (id: incr_or_decr) (v: val) (ty: type) := +Definition sem_incrdecr (cenv: composite_env) (id: incr_or_decr) (v: val) (ty: type) (m: mem) := match id with - | Incr => sem_add cenv v ty (Vint Int.one) type_int32s - | Decr => sem_sub cenv v ty (Vint Int.one) type_int32s + | Incr => sem_add cenv v ty (Vint Int.one) type_int32s m + | Decr => sem_sub cenv v ty (Vint Int.one) type_int32s m end. Definition incrdecr_type (ty: type) := @@ -1074,11 +1090,11 @@ Ltac TrivialInject := | _ => idtac end. -Lemma sem_cast_inject: +Lemma sem_cast_inj: forall v1 ty1 ty v tv1, - sem_cast v1 ty1 ty = Some v -> + sem_cast v1 ty1 ty m = Some v -> Val.inject f v1 tv1 -> - exists tv, sem_cast tv1 ty1 ty = Some tv /\ Val.inject f v tv. + exists tv, sem_cast tv1 ty1 ty m'= Some tv /\ Val.inject f v tv. Proof. unfold sem_cast; intros; destruct (classify_cast ty1 ty); inv H0; inv H; TrivialInject. @@ -1087,6 +1103,8 @@ Proof. - destruct (cast_single_int si2 f0); inv H1; TrivialInject. - destruct (cast_float_long si2 f0); inv H1; TrivialInject. - destruct (cast_single_long si2 f0); inv H1; TrivialInject. +- destruct (Mem.weak_valid_pointer m b1 (Int.unsigned ofs1)) eqn:VALID; inv H2. + erewrite weak_valid_pointer_inj by eauto. TrivialInject. - destruct (ident_eq id1 id2); inv H2; TrivialInject. econstructor; eauto. - destruct (ident_eq id1 id2); inv H2; TrivialInject. econstructor; eauto. - econstructor; eauto. @@ -1119,13 +1137,13 @@ Definition optval_self_injects (ov: option val) : Prop := Remark sem_binarith_inject: forall sem_int sem_long sem_float sem_single v1 t1 v2 t2 v v1' v2', - sem_binarith sem_int sem_long sem_float sem_single v1 t1 v2 t2 = Some v -> + sem_binarith sem_int sem_long sem_float sem_single v1 t1 v2 t2 m = Some v -> Val.inject f v1 v1' -> Val.inject f v2 v2' -> (forall sg n1 n2, optval_self_injects (sem_int sg n1 n2)) -> (forall sg n1 n2, optval_self_injects (sem_long sg n1 n2)) -> (forall n1 n2, optval_self_injects (sem_float n1 n2)) -> (forall n1 n2, optval_self_injects (sem_single n1 n2)) -> - exists v', sem_binarith sem_int sem_long sem_float sem_single v1' t1 v2' t2 = Some v' /\ Val.inject f v v'. + exists v', sem_binarith sem_int sem_long sem_float sem_single v1' t1 v2' t2 m' = Some v' /\ Val.inject f v v'. Proof. intros. assert (SELF: forall ov v, ov = Some v -> optval_self_injects ov -> Val.inject f v v). @@ -1135,10 +1153,10 @@ Proof. unfold sem_binarith in *. set (c := classify_binarith t1 t2) in *. set (t := binarith_type c) in *. - destruct (sem_cast v1 t1 t) as [w1|] eqn:C1; try discriminate. - destruct (sem_cast v2 t2 t) as [w2|] eqn:C2; try discriminate. - exploit (sem_cast_inject v1); eauto. intros (w1' & C1' & INJ1). - exploit (sem_cast_inject v2); eauto. intros (w2' & C2' & INJ2). + destruct (sem_cast v1 t1 t m) as [w1|] eqn:C1; try discriminate. + destruct (sem_cast v2 t2 t m) as [w2|] eqn:C2; try discriminate. + exploit (sem_cast_inj v1); eauto. intros (w1' & C1' & INJ1). + exploit (sem_cast_inj v2); eauto. intros (w2' & C2' & INJ2). rewrite C1'; rewrite C2'. destruct c; inv INJ1; inv INJ2; discriminate || eauto. Qed. @@ -1202,25 +1220,25 @@ Proof. unfold sem_binary_operation; intros; destruct op. - (* add *) unfold sem_add in *; destruct (classify_add ty1 ty2). - + inv H0; inv H1; inv H. TrivialInject. + + inv H0; inv H1; inv H. TrivialInject. TrivialInject. econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - + inv H0; inv H1; inv H. TrivialInject. + + inv H0; inv H1; inv H. TrivialInject. TrivialInject. econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - + inv H0; inv H1; inv H. TrivialInject. + + inv H0; inv H1; inv H. TrivialInject. TrivialInject. econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - + inv H0; inv H1; inv H. TrivialInject. + + inv H0; inv H1; inv H. TrivialInject. TrivialInject. econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + eapply sem_binarith_inject; eauto; intros; exact I. - (* sub *) unfold sem_sub in *; destruct (classify_sub ty1 ty2). - + inv H0; inv H1; inv H. TrivialInject. + + inv H0; inv H1; inv H. TrivialInject. TrivialInject. econstructor. eauto. rewrite Int.sub_add_l. auto. + inv H0; inv H1; inv H. TrivialInject. destruct (eq_block b1 b0); try discriminate. subst b1. rewrite H0 in H2; inv H2. rewrite dec_eq_true. destruct (zlt 0 (sizeof cenv ty) && zle (sizeof cenv ty) Int.max_signed); inv H3. rewrite Int.sub_shifted. TrivialInject. - + inv H0; inv H1; inv H. TrivialInject. + + inv H0; inv H1; inv H. TrivialInject. TrivialInject. econstructor. eauto. rewrite Int.sub_add_l. auto. + eapply sem_binarith_inject; eauto; intros; exact I. - (* mul *) @@ -1282,6 +1300,17 @@ Qed. End GENERIC_INJECTION. +Lemma sem_cast_inject: + forall f v1 ty1 ty m v tv1 tm, + sem_cast v1 ty1 ty m = Some v -> + Val.inject f v1 tv1 -> + Mem.inject f m tm -> + exists tv, sem_cast tv1 ty1 ty tm = Some tv /\ Val.inject f v tv. +Proof. + intros. eapply sem_cast_inj; eauto. + intros; eapply Mem.weak_valid_pointer_inject_val; eauto. +Qed. + Lemma sem_unary_operation_inject: forall f m m' op v1 ty1 v tv1, sem_unary_operation op v1 ty1 m = Some v -> @@ -1321,20 +1350,16 @@ Qed. (** * Some properties of operator semantics *) (** This section collects some common-sense properties about the type - classification and semantic functions above. These properties are - not used in the CompCert semantics preservation proofs, but increase + classification and semantic functions above. Some properties are used + in the CompCert semantics preservation proofs. Others are not, but increase confidence in the specification and its relation with the ISO C99 standard. *) (** Relation between Boolean value and casting to [_Bool] type. *) Lemma cast_bool_bool_val: forall v t m, - match sem_cast v t (Tint IBool Signed noattr), bool_val v t m with - | Some v', Some b => v' = Val.of_bool b - | Some v', None => False - | None, _ => True - end. -Proof. + sem_cast v t (Tint IBool Signed noattr) m = + match bool_val v t m with None => None | Some b => Some(Val.of_bool b) end. intros. assert (A: classify_bool t = match t with @@ -1360,8 +1385,11 @@ Proof. destruct (Float32.cmp Ceq f0 Float32.zero); auto. destruct f; auto. destruct (Int.eq i Int.zero); auto. + destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto. destruct (Int.eq i Int.zero); auto. + destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto. destruct (Int.eq i Int.zero); auto. + destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto. Qed. (** Relation between Boolean value and Boolean negation. *) @@ -1376,6 +1404,119 @@ Proof. destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); auto. Qed. +(** Properties of values obtained by casting to a given type. *) + +Inductive val_casted: val -> type -> Prop := + | val_casted_int: forall sz si attr n, + cast_int_int sz si n = n -> + val_casted (Vint n) (Tint sz si attr) + | val_casted_float: forall attr n, + val_casted (Vfloat n) (Tfloat F64 attr) + | val_casted_single: forall attr n, + val_casted (Vsingle n) (Tfloat F32 attr) + | val_casted_long: forall si attr n, + val_casted (Vlong n) (Tlong si attr) + | val_casted_ptr_ptr: forall b ofs ty attr, + val_casted (Vptr b ofs) (Tpointer ty attr) + | val_casted_int_ptr: forall n ty attr, + val_casted (Vint n) (Tpointer ty attr) + | val_casted_ptr_int: forall b ofs si attr, + val_casted (Vptr b ofs) (Tint I32 si attr) + | val_casted_struct: forall id attr b ofs, + val_casted (Vptr b ofs) (Tstruct id attr) + | val_casted_union: forall id attr b ofs, + val_casted (Vptr b ofs) (Tunion id attr) + | val_casted_void: forall v, + val_casted v Tvoid. + +Remark cast_int_int_idem: + forall sz sg i, cast_int_int sz sg (cast_int_int sz sg i) = cast_int_int sz sg i. +Proof. + intros. destruct sz; simpl; auto. + destruct sg; [apply Int.sign_ext_idem|apply Int.zero_ext_idem]; compute; intuition congruence. + destruct sg; [apply Int.sign_ext_idem|apply Int.zero_ext_idem]; compute; intuition congruence. + destruct (Int.eq i Int.zero); auto. +Qed. + +Lemma cast_val_is_casted: + forall v ty ty' v' m, sem_cast v ty ty' m = Some v' -> val_casted v' ty'. +Proof. + unfold sem_cast; intros. destruct ty'; simpl in *. +- (* void *) + constructor. +- (* int *) + destruct i; destruct ty; simpl in H; try (destruct f); try discriminate; destruct v; inv H. + constructor. apply (cast_int_int_idem I8 s). + constructor. apply (cast_int_int_idem I8 s). + destruct (cast_single_int s f); inv H1. constructor. apply (cast_int_int_idem I8 s). + destruct (cast_float_int s f); inv H1. constructor. apply (cast_int_int_idem I8 s). + constructor. apply (cast_int_int_idem I16 s). + constructor. apply (cast_int_int_idem I16 s). + destruct (cast_single_int s f); inv H1. constructor. apply (cast_int_int_idem I16 s). + destruct (cast_float_int s f); inv H1. constructor. apply (cast_int_int_idem I16 s). + constructor. auto. + constructor. + constructor. auto. + destruct (cast_single_int s f); inv H1. constructor. auto. + destruct (cast_float_int s f); inv H1. constructor; auto. + constructor; auto. + constructor. + constructor; auto. + constructor. + constructor; auto. + constructor. + constructor. simpl. destruct (Int.eq i0 Int.zero); auto. + constructor. simpl. destruct (Int64.eq i Int64.zero); auto. + constructor. simpl. destruct (Float32.cmp Ceq f Float32.zero); auto. + constructor. simpl. destruct (Float.cmp Ceq f Float.zero); auto. + constructor. simpl. destruct (Int.eq i Int.zero); auto. + destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); inv H1. constructor; auto. + constructor. simpl. destruct (Int.eq i Int.zero); auto. + destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); inv H1. constructor; auto. + constructor. simpl. destruct (Int.eq i Int.zero); auto. + destruct (Mem.weak_valid_pointer m b (Int.unsigned i)); inv H1. constructor; auto. +- (* long *) + destruct ty; try (destruct f); try discriminate. + destruct v; inv H. constructor. + destruct v; inv H. constructor. + destruct v; try discriminate. destruct (cast_single_long s f); inv H. constructor. + destruct v; try discriminate. destruct (cast_float_long s f); inv H. constructor. + destruct v; inv H. constructor. + destruct v; inv H. constructor. + destruct v; inv H. constructor. +- (* float *) + destruct f; destruct ty; simpl in H; try (destruct f); try discriminate; destruct v; inv H; constructor. +- (* pointer *) + destruct ty; simpl in H; try discriminate; destruct v; inv H; try constructor. +- (* array (impossible case) *) + discriminate. +- (* function (impossible case) *) + discriminate. +- (* structs *) + destruct ty; try discriminate; destruct v; try discriminate. + destruct (ident_eq i0 i); inv H; constructor. +- (* unions *) + destruct ty; try discriminate; destruct v; try discriminate. + destruct (ident_eq i0 i); inv H; constructor. +Qed. + +(** As a consequence, casting twice is equivalent to casting once. *) + +Lemma cast_val_casted: + forall v ty m, val_casted v ty -> sem_cast v ty ty m = Some v. +Proof. + intros. inversion H; clear H; subst v ty; unfold sem_cast; simpl; auto. + destruct sz; congruence. + unfold proj_sumbool; repeat rewrite dec_eq_true; auto. + unfold proj_sumbool; repeat rewrite dec_eq_true; auto. +Qed. + +Lemma cast_idempotent: + forall v ty ty' v' m, sem_cast v ty ty' m = Some v' -> sem_cast v' ty' ty' m = Some v'. +Proof. + intros. apply cast_val_casted. eapply cast_val_is_casted; eauto. +Qed. + (** Relation with the arithmetic conversions of ISO C99, section 6.3.1 *) Module ArithConv. diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 539b6826..30e6200d 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -187,12 +187,12 @@ Fixpoint seq_of_labeled_statement (sl: labeled_statements) : statement := (** Extract the values from a list of function arguments *) -Inductive cast_arguments: exprlist -> typelist -> list val -> Prop := +Inductive cast_arguments (m: mem): exprlist -> typelist -> list val -> Prop := | cast_args_nil: - cast_arguments Enil Tnil nil + cast_arguments m Enil Tnil nil | cast_args_cons: forall v ty el targ1 targs v1 vl, - sem_cast v ty targ1 = Some v1 -> cast_arguments el targs vl -> - cast_arguments (Econs (Eval v ty) el) (Tcons targ1 targs) (v1 :: vl). + sem_cast v ty targ1 m = Some v1 -> cast_arguments m el targs vl -> + cast_arguments m (Econs (Eval v ty) el) (Tcons targ1 targs) (v1 :: vl). (** ** Reduction semantics for expressions *) @@ -249,7 +249,7 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := rred (Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty) m E0 (Eval v ty) m | red_cast: forall ty v1 ty1 m v, - sem_cast v1 ty1 ty = Some v -> + sem_cast v1 ty1 ty m = Some v -> rred (Ecast (Eval v1 ty1) ty) m E0 (Eval v ty) m | red_seqand_true: forall v1 ty1 r2 ty m, @@ -279,7 +279,7 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := rred (Ealignof ty1 ty) m E0 (Eval (Vint (Int.repr (alignof ge ty1))) ty) m | red_assign: forall b ofs ty1 v2 ty2 m v t m', - sem_cast v2 ty2 ty1 = Some v -> + sem_cast v2 ty2 ty1 m = Some v -> assign_loc ty1 m b ofs v t m' -> rred (Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty1) m t (Eval v ty1) m' @@ -303,11 +303,11 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := rred (Ecomma (Eval v ty1) r2 ty) m E0 r2 m | red_paren: forall v1 ty1 ty2 ty m v, - sem_cast v1 ty1 ty2 = Some v -> + sem_cast v1 ty1 ty2 m = Some v -> rred (Eparen (Eval v1 ty1) ty2 ty) m E0 (Eval v ty) m | red_builtin: forall ef tyargs el ty m vargs t vres m', - cast_arguments el tyargs vargs -> + cast_arguments m el tyargs vargs -> external_call ef ge vargs m t vres m' -> rred (Ebuiltin ef tyargs el ty) m t (Eval vres ty) m'. @@ -316,13 +316,13 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := (** Head reduction for function calls. (More exactly, identification of function calls that can reduce.) *) -Inductive callred: expr -> fundef -> list val -> type -> Prop := - | red_call: forall vf tyf tyargs tyres cconv el ty fd vargs, +Inductive callred: expr -> mem -> fundef -> list val -> type -> Prop := + | red_call: forall vf tyf m tyargs tyres cconv el ty fd vargs, Genv.find_funct ge vf = Some fd -> - cast_arguments el tyargs vargs -> + cast_arguments m el tyargs vargs -> type_of_fundef fd = Tfunction tyargs tyres cconv -> classify_fun tyf = fun_case_f tyargs tyres cconv -> - callred (Ecall (Eval vf tyf) el ty) + callred (Ecall (Eval vf tyf) el ty) m fd vargs ty. (** Reduction contexts. In accordance with C's nondeterministic semantics, @@ -429,17 +429,14 @@ Inductive imm_safe: kind -> expr -> mem -> Prop := context RV to C -> imm_safe to (C e) m | imm_safe_callred: forall to C e m fd args ty, - callred e fd args ty -> + callred e m fd args ty -> context RV to C -> imm_safe to (C e) m. -(* An expression is not stuck if none of the potential redexes contained within - is immediately stuck. *) -(* Definition not_stuck (e: expr) (m: mem) : Prop := forall k C e' , - context k RV C -> e = C e' -> not_imm_stuck k e' m. -*) + context k RV C -> e = C e' -> imm_safe k e' m. + End EXPR. (** ** Transition semantics. *) @@ -597,7 +594,7 @@ Inductive estep: state -> trace -> state -> Prop := t (ExprState f (C a') k e m') | step_call: forall C f a k e m fd vargs ty, - callred a fd vargs ty -> + callred a m fd vargs ty -> context RV RV C -> estep (ExprState f (C a) k e m) E0 (Callstate fd vargs (Kcall f e C ty k) m) @@ -709,7 +706,7 @@ Inductive sstep: state -> trace -> state -> Prop := sstep (State f (Sreturn (Some x)) k e m) E0 (ExprState f x (Kreturn k) e m) | step_return_2: forall f v1 ty k e m v2 m', - sem_cast v1 ty f.(fn_return) = Some v2 -> + sem_cast v1 ty f.(fn_return) m = Some v2 -> Mem.free_list m (blocks_of_env e) = Some m' -> sstep (ExprState f (Eval v1 ty) (Kreturn k) e m) E0 (Returnstate v2 (call_cont k) m') diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 825a563c..40b51bd3 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -20,17 +20,9 @@ Csharpminor's simpler control structures. *) -Require Import Coqlib. -Require Import Maps. -Require Import Errors. -Require Import Integers. -Require Import Floats. -Require Import AST. -Require Import Ctypes. -Require Import Cop. -Require Import Clight. -Require Import Cminor. -Require Import Csharpminor. +Require Import Coqlib Maps Errors Integers Floats. +Require Import AST Linking. +Require Import Ctypes Cop Clight Cminor Csharpminor. Open Local Scope string_scope. Open Local Scope error_monad_scope. @@ -125,6 +117,18 @@ Definition make_cmp_ne_zero (e: expr) := | _ => Ebinop (Ocmp Cne) e (make_intconst Int.zero) end. +(** Variants of [sizeof] and [alignof] that check that the given type is complete. *) + +Definition sizeof (ce: composite_env) (t: type) : res Z := + if complete_type ce t + then OK (Ctypes.sizeof ce t) + else Error (msg "incomplete type"). + +Definition alignof (ce: composite_env) (t: type) : res Z := + if complete_type ce t + then OK (Ctypes.alignof ce t) + else Error (msg "incomplete type"). + (** [make_cast from to e] applies to [e] the numeric conversions needed to transform a result of type [from] to a result of type [to]. *) @@ -238,16 +242,20 @@ Definition make_binarith (iop iopu fop sop lop lopu: binary_operation) Definition make_add (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_add ty1 ty2 with | add_case_pi ty => - let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in + do sz <- sizeof ce ty; + let n := make_intconst (Int.repr sz) in OK (Ebinop Oadd e1 (Ebinop Omul n e2)) | add_case_ip ty => - let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in + do sz <- sizeof ce ty; + let n := make_intconst (Int.repr sz) in OK (Ebinop Oadd e2 (Ebinop Omul n e1)) | add_case_pl ty => - let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in + do sz <- sizeof ce ty; + let n := make_intconst (Int.repr sz) in OK (Ebinop Oadd e1 (Ebinop Omul n (Eunop Ointoflong e2))) | add_case_lp ty => - let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in + do sz <- sizeof ce ty; + let n := make_intconst (Int.repr sz) in OK (Ebinop Oadd e2 (Ebinop Omul n (Eunop Ointoflong e1))) | add_default => make_binarith Oadd Oadd Oaddf Oaddfs Oaddl Oaddl e1 ty1 e2 ty2 @@ -256,13 +264,16 @@ Definition make_add (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: Definition make_sub (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_sub ty1 ty2 with | sub_case_pi ty => - let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in + do sz <- sizeof ce ty; + let n := make_intconst (Int.repr sz) in OK (Ebinop Osub e1 (Ebinop Omul n e2)) | sub_case_pp ty => - let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in + do sz <- sizeof ce ty; + let n := make_intconst (Int.repr sz) in OK (Ebinop Odiv (Ebinop Osub e1 e2) n) | sub_case_pl ty => - let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in + do sz <- sizeof ce ty; + let n := make_intconst (Int.repr sz) in OK (Ebinop Osub e1 (Ebinop Omul n (Eunop Ointoflong e2))) | sub_default => make_binarith Osub Osub Osubf Osubfs Osubl Osubl e1 ty1 e2 ty2 @@ -351,8 +362,9 @@ Definition make_load (addr: expr) (ty_res: type) := by-copy assignment of a value of Clight type [ty]. *) Definition make_memcpy (ce: composite_env) (dst src: expr) (ty: type) := - Sbuiltin None (EF_memcpy (Ctypes.sizeof ce ty) (Ctypes.alignof_blockcopy ce ty)) - (dst :: src :: nil). + do sz <- sizeof ce ty; + OK (Sbuiltin None (EF_memcpy sz (Ctypes.alignof_blockcopy ce ty)) + (dst :: src :: nil)). (** [make_store addr ty rhs] stores the value of the Csharpminor expression [rhs] into the memory location denoted by the @@ -362,7 +374,7 @@ Definition make_memcpy (ce: composite_env) (dst src: expr) (ty: type) := Definition make_store (ce: composite_env) (addr: expr) (ty: type) (rhs: expr) := match access_mode ty with | By_value chunk => OK (Sstore chunk addr rhs) - | By_copy => OK (make_memcpy ce addr rhs ty) + | By_copy => make_memcpy ce addr rhs ty | _ => Error (msg "Cshmgen.make_store") end. @@ -457,9 +469,9 @@ Fixpoint transl_expr (ce: composite_env) (a: Clight.expr) {struct a} : res expr do addr <- make_field_access ce (typeof b) i tb; make_load addr ty | Clight.Esizeof ty' ty => - OK(make_intconst (Int.repr (sizeof ce ty'))) + do sz <- sizeof ce ty'; OK(make_intconst (Int.repr sz)) | Clight.Ealignof ty' ty => - OK(make_intconst (Int.repr (alignof ce ty'))) + do al <- alignof ce ty'; OK(make_intconst (Int.repr al)) end (** [transl_lvalue a] returns the Csharpminor code that evaluates @@ -621,7 +633,8 @@ with transl_lbl_stmt (ce: composite_env) (tyret: type) (nbrk ncnt: nat) (*** Translation of functions *) -Definition transl_var (ce: composite_env) (v: ident * type) := (fst v, sizeof ce (snd v)). +Definition transl_var (ce: composite_env) (v: ident * type) := + do sz <- sizeof ce (snd v); OK (fst v, sz). Definition signature_of_function (f: Clight.function) := {| sig_args := map typ_of_type (map snd (Clight.fn_params f)); @@ -630,18 +643,19 @@ Definition signature_of_function (f: Clight.function) := Definition transl_function (ce: composite_env) (f: Clight.function) : res function := do tbody <- transl_statement ce f.(Clight.fn_return) 1%nat 0%nat (Clight.fn_body f); + do tvars <- mmap (transl_var ce) (Clight.fn_vars f); OK (mkfunction (signature_of_function f) (map fst (Clight.fn_params f)) - (map (transl_var ce) (Clight.fn_vars f)) + tvars (map fst (Clight.fn_temps f)) tbody). -Definition transl_fundef (ce: composite_env) (f: Clight.fundef) : res fundef := +Definition transl_fundef (ce: composite_env) (id: ident) (f: Clight.fundef) : res fundef := match f with - | Clight.Internal g => + | Internal g => do tg <- transl_function ce g; OK(AST.Internal tg) - | Clight.External ef args res cconv => + | External ef args res cconv => if signature_eq (ef_sig ef) (signature_of_type args res cconv) then OK(AST.External ef) else Error(msg "Cshmgen.transl_fundef: wrong external signature") @@ -649,7 +663,7 @@ Definition transl_fundef (ce: composite_env) (f: Clight.fundef) : res fundef := (** ** Translation of programs *) -Definition transl_globvar (ty: type) := OK tt. +Definition transl_globvar (id: ident) (ty: type) := OK tt. Definition transl_program (p: Clight.program) : res program := transform_partial_program2 (transl_fundef p.(prog_comp_env)) transl_globvar p. diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index e25e21c9..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: @@ -255,7 +329,7 @@ Lemma make_cast_correct: forall e le m a b v ty1 ty2 v', make_cast ty1 ty2 a = OK b -> eval_expr ge e le m a v -> - sem_cast v ty1 ty2 = Some v' -> + sem_cast v ty1 ty2 m = Some v' -> eval_expr ge e le m b v'. Proof. intros. unfold make_cast, sem_cast in *; @@ -302,6 +376,12 @@ Proof. econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu. destruct (Int.eq i Int.zero); auto. + (* pointer -> bool *) + destruct (Mem.weak_valid_pointer m b (Int.unsigned i)) eqn:VALID; inv H2. + econstructor; eauto with cshm. + simpl. unfold Val.cmpu. simpl. rewrite Int.eq_true. + unfold Mem.weak_valid_pointer in VALID; rewrite VALID. + auto. (* struct *) destruct (ident_eq id1 id2); inv H2; auto. (* union *) @@ -394,6 +474,16 @@ Qed. Definition binary_constructor_correct (make: expr -> type -> expr -> type -> res expr) + (sem: val -> type -> val -> type -> mem -> option val): Prop := + forall a tya b tyb c va vb v e le m, + sem va tya vb tyb m = Some v -> + make a tya b tyb = OK c -> + eval_expr ge e le m a va -> + eval_expr ge e le m b vb -> + eval_expr ge e le m c v. + +Definition shift_constructor_correct + (make: expr -> type -> expr -> type -> res expr) (sem: val -> type -> val -> type -> option val): Prop := forall a tya b tyb c va vb v e le m, sem va tya vb tyb = Some v -> @@ -433,8 +523,8 @@ Proof. set (cls := classify_binarith tya tyb) in *. set (ty := binarith_type cls) in *. monadInv MAKE. - destruct (sem_cast va tya ty) as [va'|] eqn:Ca; try discriminate. - destruct (sem_cast vb tyb ty) as [vb'|] eqn:Cb; try discriminate. + destruct (sem_cast va tya ty m) as [va'|] eqn:Ca; try discriminate. + destruct (sem_cast vb tyb ty m) as [vb'|] eqn:Cb; try discriminate. exploit make_cast_correct. eexact EQ. eauto. eauto. intros EV1'. exploit make_cast_correct. eexact EQ1. eauto. eauto. intros EV2'. destruct cls; inv EQ2; destruct va'; try discriminate; destruct vb'; try discriminate. @@ -456,8 +546,8 @@ Proof. set (cls := classify_binarith tya tyb) in *. set (ty := binarith_type cls) in *. monadInv MAKE. - destruct (sem_cast va tya ty) as [va'|] eqn:Ca; try discriminate. - destruct (sem_cast vb tyb ty) as [vb'|] eqn:Cb; try discriminate. + destruct (sem_cast va tya ty m) as [va'|] eqn:Ca; try discriminate. + destruct (sem_cast vb tyb ty m) as [vb'|] eqn:Cb; try discriminate. exploit make_cast_correct. eexact EQ. eauto. eauto. intros EV1'. exploit make_cast_correct. eexact EQ1. eauto. eauto. intros EV2'. destruct cls; inv EQ2; destruct va'; try discriminate; destruct vb'; try discriminate. @@ -471,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. @@ -503,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. @@ -578,7 +675,7 @@ Proof. apply Int64.unsigned_repr. comput Int64.max_unsigned; omega. Qed. -Lemma make_shl_correct: binary_constructor_correct make_shl sem_shl. +Lemma make_shl_correct: shift_constructor_correct make_shl sem_shl. Proof. red; unfold make_shl, sem_shl, sem_shift; intros until m; intros SEM MAKE EV1 EV2; @@ -597,7 +694,7 @@ Proof. unfold Int64.shl', Int64.shl. rewrite small_shift_amount_3; auto. Qed. -Lemma make_shr_correct: binary_constructor_correct make_shr sem_shr. +Lemma make_shr_correct: shift_constructor_correct make_shr sem_shr. Proof. red; unfold make_shr, sem_shr, sem_shift; intros until m; intros SEM MAKE EV1 EV2; @@ -619,15 +716,9 @@ Proof. unfold Int64.shru', Int64.shru; rewrite small_shift_amount_3; auto. Qed. -Lemma make_cmp_correct: - forall cmp a tya b tyb c va vb v e le m, - sem_cmp cmp va tya vb tyb m = Some v -> - make_cmp cmp a tya b tyb = OK c -> - eval_expr ge e le m a va -> - eval_expr ge e le m b vb -> - eval_expr ge e le m c v. +Lemma make_cmp_correct: forall cmp, binary_constructor_correct (make_cmp cmp) (sem_cmp cmp). Proof. - unfold sem_cmp, make_cmp; intros until m; intros SEM MAKE EV1 EV2; + red; unfold sem_cmp, make_cmp; intros until m; intros SEM MAKE EV1 EV2; destruct (classify_cmp tya tyb). - inv MAKE. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E; simpl in SEM; inv SEM. @@ -663,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. @@ -706,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. @@ -725,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. @@ -737,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. @@ -749,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 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 senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_match TRANSL). + +Lemma function_ptr_translated: + forall v f, + Genv.find_funct_ptr ge v = Some f -> + exists cu tf, Genv.find_funct_ptr tge v = Some tf /\ match_fundef cu f tf /\ linkorder cu prog. +Proof (Genv.find_funct_ptr_match TRANSL). Lemma functions_translated: forall v f, Genv.find_funct ge v = Some f -> - exists tf, Genv.find_funct tge v = Some tf /\ transl_fundef ge f = OK tf. -Proof (Genv.find_funct_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL). - -Lemma function_ptr_translated: - forall b f, - Genv.find_funct_ptr ge b = Some f -> - exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef ge f = OK tf. -Proof (Genv.find_funct_ptr_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL). - -Lemma block_is_volatile_preserved: - forall b, Genv.block_is_volatile tge b = Genv.block_is_volatile ge b. -Proof (Genv.block_is_volatile_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL). + exists cu tf, Genv.find_funct tge v = Some tf /\ match_fundef cu f tf /\ linkorder cu prog. +Proof (Genv.find_funct_match TRANSL). (** * Matching between environments *) @@ -787,7 +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) @@ -811,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. @@ -853,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. @@ -893,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 *) @@ -919,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. @@ -928,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). @@ -955,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. @@ -971,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. @@ -984,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. @@ -1052,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. @@ -1125,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'] | ]. @@ -1222,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. @@ -1232,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. @@ -1251,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. @@ -1263,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. @@ -1327,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. @@ -1337,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. @@ -1347,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. @@ -1357,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. @@ -1374,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. @@ -1415,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. @@ -1423,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. @@ -1485,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: @@ -1509,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/Cstrategy.v b/cfrontend/Cstrategy.v index b3cbacca..2650e0a8 100644 --- a/cfrontend/Cstrategy.v +++ b/cfrontend/Cstrategy.v @@ -130,7 +130,7 @@ with eval_simple_rvalue: expr -> val -> Prop := eval_simple_rvalue (Ebinop op r1 r2 ty) v | esr_cast: forall ty r1 v1 v, eval_simple_rvalue r1 v1 -> - sem_cast v1 (typeof r1) ty = Some v -> + sem_cast v1 (typeof r1) ty m = Some v -> eval_simple_rvalue (Ecast r1 ty) v | esr_sizeof: forall ty1 ty, eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1))) @@ -141,7 +141,7 @@ Inductive eval_simple_list: exprlist -> typelist -> list val -> Prop := | esrl_nil: eval_simple_list Enil Tnil nil | esrl_cons: forall r rl ty tyl v vl v', - eval_simple_rvalue r v' -> sem_cast v' (typeof r) ty = Some v -> + eval_simple_rvalue r v' -> sem_cast v' (typeof r) ty m = Some v -> eval_simple_list rl tyl vl -> eval_simple_list (Econs r rl) (Tcons ty tyl) (v :: vl). @@ -283,7 +283,7 @@ Inductive estep: state -> trace -> state -> Prop := leftcontext RV RV C -> eval_simple_lvalue e m l b ofs -> eval_simple_rvalue e m r v -> - sem_cast v (typeof r) (typeof l) = Some v' -> + sem_cast v (typeof r) (typeof l) m = Some v' -> assign_loc ge (typeof l) m b ofs v' t m' -> ty = typeof l -> estep (ExprState f (C (Eassign l r ty)) k e m) @@ -295,7 +295,7 @@ Inductive estep: state -> trace -> state -> Prop := deref_loc ge (typeof l) m b ofs t1 v1 -> eval_simple_rvalue e m r v2 -> sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m = Some v3 -> - sem_cast v3 tyres (typeof l) = Some v4 -> + sem_cast v3 tyres (typeof l) m = Some v4 -> assign_loc ge (typeof l) m b ofs v4 t2 m' -> ty = typeof l -> t = t1 ** t2 -> @@ -310,7 +310,7 @@ Inductive estep: state -> trace -> state -> Prop := match sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m with | None => True | Some v3 => - match sem_cast v3 tyres (typeof l) with + match sem_cast v3 tyres (typeof l) m with | None => True | Some v4 => forall t2 m', ~(assign_loc ge (typeof l) m b ofs v4 t2 m') end @@ -323,8 +323,8 @@ Inductive estep: state -> trace -> state -> Prop := leftcontext RV RV C -> eval_simple_lvalue e m l b ofs -> deref_loc ge ty m b ofs t1 v1 -> - sem_incrdecr ge id v1 ty = Some v2 -> - sem_cast v2 (incrdecr_type ty) ty = Some v3 -> + sem_incrdecr ge id v1 ty m = Some v2 -> + sem_cast v2 (incrdecr_type ty) ty m = Some v3 -> assign_loc ge ty m b ofs v3 t2 m' -> ty = typeof l -> t = t1 ** t2 -> @@ -335,10 +335,10 @@ Inductive estep: state -> trace -> state -> Prop := leftcontext RV RV C -> eval_simple_lvalue e m l b ofs -> deref_loc ge ty m b ofs t v1 -> - match sem_incrdecr ge id v1 ty with + match sem_incrdecr ge id v1 ty m with | None => True | Some v2 => - match sem_cast v2 (incrdecr_type ty) ty with + match sem_cast v2 (incrdecr_type ty) ty m with | None => True | Some v3 => forall t2 m', ~(assign_loc ge (typeof l) m b ofs v3 t2 m') end @@ -357,7 +357,7 @@ Inductive estep: state -> trace -> state -> Prop := | step_paren: forall f C r tycast ty k e m v1 v, leftcontext RV RV C -> eval_simple_rvalue e m r v1 -> - sem_cast v1 (typeof r) tycast = Some v -> + sem_cast v1 (typeof r) tycast m = Some v -> estep (ExprState f (C (Eparen r tycast ty)) k e m) E0 (ExprState f (C (Eval v ty)) k e m) @@ -472,7 +472,7 @@ Proof. Qed. Lemma callred_kind: - forall a fd args ty, callred ge a fd args ty -> expr_kind a = RV. + forall a m fd args ty, callred ge a m fd args ty -> expr_kind a = RV. Proof. induction 1; auto. Qed. @@ -540,7 +540,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty => exists v, sem_binary_operation ge op v1 ty1 v2 ty2 m = Some v | Ecast (Eval v1 ty1) ty => - exists v, sem_cast v1 ty1 ty = Some v + exists v, sem_cast v1 ty1 ty m = Some v | Eseqand (Eval v1 ty1) r2 ty => exists b, bool_val v1 ty1 m = Some b | Eseqor (Eval v1 ty1) r2 ty => @@ -549,7 +549,7 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := exists b, bool_val v1 ty1 m = Some b | Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty => exists v, exists m', exists t, - ty = ty1 /\ sem_cast v2 ty2 ty1 = Some v /\ assign_loc ge ty1 m b ofs v t m' + ty = ty1 /\ sem_cast v2 ty2 ty1 m = Some v /\ assign_loc ge ty1 m b ofs v t m' | Eassignop op (Eloc b ofs ty1) (Eval v2 ty2) tyres ty => exists t, exists v1, ty = ty1 @@ -561,18 +561,18 @@ Definition invert_expr_prop (a: expr) (m: mem) : Prop := | Ecomma (Eval v ty1) r2 ty => typeof r2 = ty | Eparen (Eval v1 ty1) ty2 ty => - exists v, sem_cast v1 ty1 ty2 = Some v + exists v, sem_cast v1 ty1 ty2 m = Some v | Ecall (Eval vf tyf) rargs ty => exprlist_all_values rargs -> exists tyargs tyres cconv fd vl, classify_fun tyf = fun_case_f tyargs tyres cconv /\ Genv.find_funct ge vf = Some fd - /\ cast_arguments rargs tyargs vl + /\ cast_arguments m rargs tyargs vl /\ type_of_fundef fd = Tfunction tyargs tyres cconv | Ebuiltin ef tyargs rargs ty => exprlist_all_values rargs -> exists vargs, exists t, exists vres, exists m', - cast_arguments rargs tyargs vargs + cast_arguments m rargs tyargs vargs /\ external_call ef ge vargs m t vres m' | _ => True end. @@ -608,7 +608,7 @@ Qed. Lemma callred_invert: forall r fd args ty m, - callred ge r fd args ty -> + callred ge r m fd args ty -> invert_expr_prop r m. Proof. intros. inv H. simpl. @@ -893,7 +893,7 @@ Inductive eval_simple_list': exprlist -> list val -> Prop := Lemma eval_simple_list_implies: forall rl tyl vl, eval_simple_list e m rl tyl vl -> - exists vl', cast_arguments (rval_list vl' rl) tyl vl /\ eval_simple_list' rl vl'. + exists vl', cast_arguments m (rval_list vl' rl) tyl vl /\ eval_simple_list' rl vl'. Proof. induction 1. exists (@nil val); split. constructor. constructor. @@ -905,7 +905,7 @@ Lemma can_eval_simple_list: forall rl vl, eval_simple_list' rl vl -> forall tyl vl', - cast_arguments (rval_list vl rl) tyl vl' -> + cast_arguments m (rval_list vl rl) tyl vl' -> eval_simple_list e m rl tyl vl'. Proof. induction 1; simpl; intros. @@ -1234,9 +1234,9 @@ Proof. left; apply step_rred; auto. econstructor; eauto. set (op := match id with Incr => Oadd | Decr => Osub end). assert (SEM: sem_binary_operation ge op v1 (typeof l) (Vint Int.one) type_int32s m = - sem_incrdecr ge id v1 (typeof l)). + sem_incrdecr ge id v1 (typeof l) m). destruct id; auto. - destruct (sem_incrdecr ge id v1 (typeof l)) as [v2|]. + destruct (sem_incrdecr ge id v1 (typeof l) m) as [v2|]. eapply star_left. left; apply step_rred with (C := fun x => C (Ecomma (Eassign (Eloc b ofs (typeof l)) x (typeof l)) (Eval v1 (typeof l)) (typeof l))); eauto. econstructor; eauto. @@ -1329,7 +1329,7 @@ Proof. intros [v [E2 S2]]. exploit safe_inv. eexact S2. eauto. simpl. intros [t1 [v1 [A B]]]. destruct (sem_binary_operation ge op v1 (typeof b1) v (typeof b2) m) as [v3|] eqn:?. - destruct (sem_cast v3 tyres (typeof b1)) as [v4|] eqn:?. + destruct (sem_cast v3 tyres (typeof b1) m) as [v4|] eqn:?. destruct (classic (exists t2, exists m', assign_loc ge (typeof b1) m b ofs v4 t2 m')). destruct H2 as [t2 [m' D]]. econstructor; econstructor; eapply step_assignop; eauto. @@ -1343,8 +1343,8 @@ Proof. exploit (simple_can_eval_lval f k e m b (fun x => C(Epostincr id x ty))); eauto. intros [b1 [ofs [E1 S1]]]. exploit safe_inv. eexact S1. eauto. simpl. intros [t [v1 [A B]]]. - destruct (sem_incrdecr ge id v1 ty) as [v2|] eqn:?. - destruct (sem_cast v2 (incrdecr_type ty) ty) as [v3|] eqn:?. + destruct (sem_incrdecr ge id v1 ty m) as [v2|] eqn:?. + destruct (sem_cast v2 (incrdecr_type ty) ty m) as [v3|] eqn:?. destruct (classic (exists t2, exists m', assign_loc ge ty m b1 ofs v3 t2 m')). destruct H0 as [t2 [m' D]]. econstructor; econstructor; eapply step_postincr; eauto. @@ -1498,7 +1498,7 @@ Proof. econstructor; econstructor; eauto. inv H10. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0. destruct (sem_binary_operation ge op v1' (typeof l) v2 (typeof r) m) as [v3'|] eqn:?. - destruct (sem_cast v3' tyres (typeof l)) as [v4'|] eqn:?. + destruct (sem_cast v3' tyres (typeof l) m) as [v4'|] eqn:?. destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v4' t2' m'')). destruct H1 as [t2' [m'' P]]. econstructor; econstructor. left; eapply step_assignop with (v1 := v1'); eauto. simpl; reflexivity. @@ -1511,7 +1511,7 @@ Proof. (* assignop stuck *) exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1. destruct (sem_binary_operation ge op v1' (typeof l) v2 (typeof r) m) as [v3'|] eqn:?. - destruct (sem_cast v3' tyres (typeof l)) as [v4'|] eqn:?. + destruct (sem_cast v3' tyres (typeof l) m) as [v4'|] eqn:?. destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v4' t2' m'')). destruct H1 as [t2' [m'' P]]. econstructor; econstructor. left; eapply step_assignop with (v1 := v1'); eauto. simpl; reflexivity. @@ -1526,8 +1526,8 @@ Proof. subst t2. exploit assign_loc_receptive; eauto. intros EQ; rewrite EQ in H. econstructor; econstructor; eauto. inv H9. exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t0. - destruct (sem_incrdecr ge id v1' (typeof l)) as [v2'|] eqn:?. - destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l)) as [v3'|] eqn:?. + destruct (sem_incrdecr ge id v1' (typeof l) m) as [v2'|] eqn:?. + destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l) m) as [v3'|] eqn:?. destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v3' t2' m'')). destruct H1 as [t2' [m'' P]]. econstructor; econstructor. left; eapply step_postincr with (v1 := v1'); eauto. simpl; reflexivity. @@ -1539,8 +1539,8 @@ Proof. rewrite Heqo; auto. (* postincr stuck *) exploit deref_loc_receptive; eauto. intros [EQ [v1' A]]. subst t1. - destruct (sem_incrdecr ge id v1' (typeof l)) as [v2'|] eqn:?. - destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l)) as [v3'|] eqn:?. + destruct (sem_incrdecr ge id v1' (typeof l) m) as [v2'|] eqn:?. + destruct (sem_cast v2' (incrdecr_type (typeof l)) (typeof l) m) as [v3'|] eqn:?. destruct (classic (exists t2', exists m'', assign_loc ge (typeof l) m b ofs v3' t2' m'')). destruct H1 as [t2' [m'' P]]. econstructor; econstructor. left; eapply step_postincr with (v1 := v1'); eauto. simpl; reflexivity. @@ -1641,11 +1641,11 @@ Definition outcome_switch (out: outcome) : outcome := | o => o end. -Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop := +Definition outcome_result_value (out: outcome) (t: type) (v: val) (m: mem) : Prop := match out, t with | Out_normal, Tvoid => v = Vundef | Out_return None, Tvoid => v = Vundef - | Out_return (Some (v', ty')), ty => ty <> Tvoid /\ sem_cast v' ty' ty = Some v + | Out_return (Some (v', ty')), ty => ty <> Tvoid /\ sem_cast v' ty' ty m = Some v | _, _ => False end. @@ -1697,7 +1697,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> bool_val v1 (typeof a1) m' = Some true -> eval_expr e m' RV a2 t2 m'' a2' -> eval_simple_rvalue ge e m'' a2' v2 -> - sem_cast v2 (typeof a2) type_bool = Some v -> + sem_cast v2 (typeof a2) type_bool m'' = Some v -> eval_expr e m RV (Eseqand a1 a2 ty) (t1**t2) m'' (Eval v ty) | eval_seqand_false: forall e m a1 a2 ty t1 m' a1' v1, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> @@ -1707,7 +1707,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> bool_val v1 (typeof a1) m' = Some false -> eval_expr e m' RV a2 t2 m'' a2' -> eval_simple_rvalue ge e m'' a2' v2 -> - sem_cast v2 (typeof a2) type_bool = Some v -> + sem_cast v2 (typeof a2) type_bool m'' = Some v -> eval_expr e m RV (Eseqor a1 a2 ty) (t1**t2) m'' (Eval v ty) | eval_seqor_true: forall e m a1 a2 ty t1 m' a1' v1, eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> @@ -1717,7 +1717,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> bool_val v1 (typeof a1) m' = Some b -> eval_expr e m' RV (if b then a2 else a3) t2 m'' a' -> eval_simple_rvalue ge e m'' a' v' -> - sem_cast v' (typeof (if b then a2 else a3)) ty = Some v -> + sem_cast v' (typeof (if b then a2 else a3)) ty m'' = Some v -> eval_expr e m RV (Econdition a1 a2 a3 ty) (t1**t2) m'' (Eval v ty) | eval_sizeof: forall e m ty' ty, eval_expr e m RV (Esizeof ty' ty) E0 m (Esizeof ty' ty) @@ -1727,7 +1727,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := eval_expr e m LV l t1 m1 l' -> eval_expr e m1 RV r t2 m2 r' -> eval_simple_lvalue ge e m2 l' b ofs -> eval_simple_rvalue ge e m2 r' v -> - sem_cast v (typeof r) (typeof l) = Some v' -> + sem_cast v (typeof r) (typeof l) m2 = Some v' -> assign_loc ge (typeof l) m2 b ofs v' t3 m3 -> ty = typeof l -> eval_expr e m RV (Eassign l r ty) (t1**t2**t3) m3 (Eval v' ty) @@ -1738,7 +1738,7 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := deref_loc ge (typeof l) m2 b ofs t3 v1 -> eval_simple_rvalue ge e m2 r' v2 -> sem_binary_operation ge op v1 (typeof l) v2 (typeof r) m2 = Some v3 -> - sem_cast v3 tyres (typeof l) = Some v4 -> + sem_cast v3 tyres (typeof l) m2 = Some v4 -> assign_loc ge (typeof l) m2 b ofs v4 t4 m3 -> ty = typeof l -> eval_expr e m RV (Eassignop op l r tyres ty) (t1**t2**t3**t4) m3 (Eval v4 ty) @@ -1746,8 +1746,8 @@ with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := eval_expr e m LV l t1 m1 l' -> eval_simple_lvalue ge e m1 l' b ofs -> deref_loc ge ty m1 b ofs t2 v1 -> - sem_incrdecr ge id v1 ty = Some v2 -> - sem_cast v2 (incrdecr_type ty) ty = Some v3 -> + sem_incrdecr ge id v1 ty m1 = Some v2 -> + sem_cast v2 (incrdecr_type ty) ty m1 = Some v3 -> assign_loc ge ty m1 b ofs v3 t3 m2 -> ty = typeof l -> eval_expr e m RV (Epostincr id l ty) (t1**t2**t3) m2 (Eval v1 ty) @@ -1901,7 +1901,7 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := alloc_variables ge empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> bind_parameters ge e m1 f.(fn_params) vargs m2 -> exec_stmt e m2 f.(fn_body) t m3 out -> - outcome_result_value out f.(fn_return) vres -> + outcome_result_value out f.(fn_return) vres m3 -> Mem.free_list m3 (blocks_of_env ge e) = Some m4 -> eval_funcall m (Internal f) vargs t m4 vres | eval_funcall_external: forall m ef targs tres cconv vargs t vres m', 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 aa320f20..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 *) @@ -1370,7 +1357,7 @@ Qed. Hint Resolve pres_cast_int_int: ty. Lemma pres_sem_cast: - forall v2 ty2 v1 ty1, wt_val v1 ty1 -> sem_cast v1 ty1 ty2 = Some v2 -> wt_val v2 ty2. + forall m v2 ty2 v1 ty1, wt_val v1 ty1 -> sem_cast v1 ty1 ty2 m = Some v2 -> wt_val v2 ty2. Proof. unfold sem_cast, classify_cast; induction 1; simpl; intros; DestructCases; auto with ty. - constructor. apply (pres_cast_int_int I8 s). @@ -1385,7 +1372,10 @@ Proof. - constructor. apply (pres_cast_int_int I8 s). - constructor. apply (pres_cast_int_int I16 s). - destruct (Float32.cmp Ceq f Float32.zero); auto with ty. +- constructor. reflexivity. - destruct (Int.eq n Int.zero); auto with ty. +- constructor. reflexivity. +- constructor. reflexivity. Qed. Lemma pres_sem_binarith: @@ -1394,7 +1384,7 @@ Lemma pres_sem_binarith: (sem_long: signedness -> int64 -> int64 -> option val) (sem_float: float -> float -> option val) (sem_single: float32 -> float32 -> option val) - v1 ty1 v2 ty2 v ty msg, + v1 ty1 v2 ty2 m v ty msg, (forall sg n1 n2, match sem_int sg n1 n2 with None | Some (Vint _) | Some Vundef => True | _ => False end) -> (forall sg n1 n2, @@ -1403,14 +1393,14 @@ Lemma pres_sem_binarith: match sem_float n1 n2 with None | Some (Vfloat _) | Some Vundef => True | _ => False end) -> (forall n1 n2, match sem_single n1 n2 with None | Some (Vsingle _) | Some Vundef => True | _ => False end) -> - sem_binarith sem_int sem_long sem_float sem_single v1 ty1 v2 ty2 = Some v -> + sem_binarith sem_int sem_long sem_float sem_single v1 ty1 v2 ty2 m = Some v -> binarith_type ty1 ty2 msg = OK ty -> wt_val v ty. Proof with (try discriminate). intros. unfold sem_binarith, binarith_type in *. set (ty' := Cop.binarith_type (classify_binarith ty1 ty2)) in *. - destruct (sem_cast v1 ty1 ty') as [v1'|] eqn:CAST1... - destruct (sem_cast v2 ty2 ty') as [v2'|] eqn:CAST2... + destruct (sem_cast v1 ty1 ty' m) as [v1'|] eqn:CAST1... + destruct (sem_cast v2 ty2 ty' m) as [v2'|] eqn:CAST2... DestructCases. - specialize (H s i i0). rewrite H3 in H. destruct v; auto with ty; contradiction. @@ -1426,12 +1416,12 @@ Lemma pres_sem_binarith_int: forall (sem_int: signedness -> int -> int -> option val) (sem_long: signedness -> int64 -> int64 -> option val) - v1 ty1 v2 ty2 v ty msg, + v1 ty1 v2 ty2 m v ty msg, (forall sg n1 n2, match sem_int sg n1 n2 with None | Some (Vint _) | Some Vundef => True | _ => False end) -> (forall sg n1 n2, match sem_long sg n1 n2 with None | Some (Vlong _) | Some Vundef => True | _ => False end) -> - sem_binarith sem_int sem_long (fun n1 n2 => None) (fun n1 n2 => None) v1 ty1 v2 ty2 = Some v -> + sem_binarith sem_int sem_long (fun n1 n2 => None) (fun n1 n2 => None) v1 ty1 v2 ty2 m = Some v -> binarith_int_type ty1 ty2 msg = OK ty -> wt_val v ty. Proof. @@ -2119,28 +2109,3 @@ Proof. Qed. End PRESERVATION. - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index b1a39c64..7228cd75 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -47,7 +47,7 @@ If [a] is a l-value, the returned value denotes: *) Definition do_cast (v: val) (t1 t2: type) : res val := - match sem_cast v t1 t2 with + match sem_cast v t1 t2 Mem.empty with | Some v' => OK v' | None => Error(msg "undefined cast") end. diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 9c662f5e..d5f39d7d 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -120,7 +120,7 @@ with eval_simple_rvalue: expr -> val -> Prop := eval_simple_rvalue (Ebinop op r1 r2 ty) v | esr_cast: forall ty r1 v1 v, eval_simple_rvalue r1 v1 -> - sem_cast v1 (typeof r1) ty = Some v -> + sem_cast v1 (typeof r1) ty m = Some v -> eval_simple_rvalue (Ecast r1 ty) v | esr_sizeof: forall ty1 ty, eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1))) @@ -129,7 +129,7 @@ with eval_simple_rvalue: expr -> val -> Prop := | esr_seqand_true: forall r1 r2 ty v1 v2 v3, eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some true -> eval_simple_rvalue r2 v2 -> - sem_cast v2 (typeof r2) type_bool = Some v3 -> + sem_cast v2 (typeof r2) type_bool m = Some v3 -> eval_simple_rvalue (Eseqand r1 r2 ty) v3 | esr_seqand_false: forall r1 r2 ty v1, eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some false -> @@ -137,7 +137,7 @@ with eval_simple_rvalue: expr -> val -> Prop := | esr_seqor_false: forall r1 r2 ty v1 v2 v3, eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some false -> eval_simple_rvalue r2 v2 -> - sem_cast v2 (typeof r2) type_bool = Some v3 -> + sem_cast v2 (typeof r2) type_bool m = Some v3 -> eval_simple_rvalue (Eseqor r1 r2 ty) v3 | esr_seqor_true: forall r1 r2 ty v1, eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some true -> @@ -145,13 +145,13 @@ with eval_simple_rvalue: expr -> val -> Prop := | esr_condition: forall r1 r2 r3 ty v v1 b v', eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some b -> eval_simple_rvalue (if b then r2 else r3) v' -> - sem_cast v' (typeof (if b then r2 else r3)) ty = Some v -> + sem_cast v' (typeof (if b then r2 else r3)) ty m = Some v -> eval_simple_rvalue (Econdition r1 r2 r3 ty) v | esr_comma: forall r1 r2 ty v1 v, eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v -> eval_simple_rvalue (Ecomma r1 r2 ty) v | esr_paren: forall r tycast ty v v', - eval_simple_rvalue r v -> sem_cast v (typeof r) tycast = Some v' -> + eval_simple_rvalue r v -> sem_cast v (typeof r) tycast m = Some v' -> eval_simple_rvalue (Eparen r tycast ty) v'. End SIMPLE_EXPRS. @@ -355,14 +355,16 @@ Proof. Qed. Lemma sem_cast_match: - forall v1 ty1 ty2 v2 v1' v2', - sem_cast v1 ty1 ty2 = Some v2 -> + forall v1 ty1 ty2 m v2 v1' v2', + sem_cast v1 ty1 ty2 m = Some v2 -> do_cast v1' ty1 ty2 = OK v2' -> Val.inject inj v1' v1 -> Val.inject inj v2' v2. Proof. - intros. unfold do_cast in H0. destruct (sem_cast v1' ty1 ty2) as [v2''|] eqn:E; inv H0. - exploit sem_cast_inject. eexact E. eauto. + intros. unfold do_cast in H0. destruct (sem_cast v1' ty1 ty2 Mem.empty) as [v2''|] eqn:E; inv H0. + exploit (sem_cast_inj inj Mem.empty m). + intros. rewrite mem_empty_not_weak_valid_pointer in H2. discriminate. + eexact E. eauto. intros [v' [A B]]. congruence. Qed. @@ -605,7 +607,7 @@ Theorem transl_init_single_steps: forall ty a data f m v1 ty1 m' v chunk b ofs m'', transl_init_single ge ty a = OK data -> star step ge (ExprState f a Kstop empty_env m) E0 (ExprState f (Eval v1 ty1) Kstop empty_env m') -> - sem_cast v1 ty1 ty = Some v -> + sem_cast v1 ty1 ty m' = Some v -> access_mode ty = By_value chunk -> Mem.store chunk m' b ofs v = Some m'' -> Genv.store_init_data ge m b ofs data = Some m''. @@ -647,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. @@ -664,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. @@ -760,7 +762,7 @@ Inductive exec_init: mem -> block -> Z -> type -> initializer -> mem -> Prop := | exec_init_single: forall m b ofs ty a v1 ty1 chunk m' v m'', star step ge (ExprState dummy_function a Kstop empty_env m) E0 (ExprState dummy_function (Eval v1 ty1) Kstop empty_env m') -> - sem_cast v1 ty1 ty = Some v -> + sem_cast v1 ty1 ty m' = Some v -> access_mode ty = By_value chunk -> Mem.store chunk m' b ofs v = Some m'' -> exec_init m b ofs ty (Init_single a) m'' diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index b8a2cb8d..e08411a5 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -80,9 +80,9 @@ let rec expr p (prec, e) = | Econst_int(n, _) -> fprintf p "%ld" (camlint_of_coqint n) | Econst_float(f, _) -> - fprintf p "%F" (camlfloat_of_coqfloat f) + fprintf p "%.15F" (camlfloat_of_coqfloat f) | Econst_single(f, _) -> - fprintf p "%Ff" (camlfloat_of_coqfloat32 f) + fprintf p "%.15Ff" (camlfloat_of_coqfloat32 f) | Econst_long(n, Tlong(Unsigned, _)) -> fprintf p "%LuLLU" (camlint64_of_coqint n) | Econst_long(n, _) -> @@ -254,10 +254,10 @@ let print_function p id f = let print_fundef p id fd = match fd with - | Clight.External(EF_external(_,_), args, res, cconv) -> + | Ctypes.External((EF_external _ | EF_runtime _), args, res, cconv) -> fprintf p "extern %s;@ @ " (name_cdecl (extern_atom id) (Tfunction(args, res, cconv))) - | Clight.External(_, _, _, _) -> + | Ctypes.External(_, _, _, _) -> () | Internal f -> print_function p id f diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index d518d6bb..4287f7f9 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -179,9 +179,9 @@ let print_typed_value p v ty = | Vint n, _ -> fprintf p "%ld" (camlint_of_coqint n) | Vfloat f, _ -> - fprintf p "%F" (camlfloat_of_coqfloat f) + fprintf p "%.15F" (camlfloat_of_coqfloat f) | Vsingle f, _ -> - fprintf p "%Ff" (camlfloat_of_coqfloat32 f) + fprintf p "%.15Ff" (camlfloat_of_coqfloat32 f) | Vlong n, Tlong(Unsigned, _) -> fprintf p "%LuLLU" (camlint64_of_coqint n) | Vlong n, _ -> @@ -261,6 +261,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,_) -> @@ -424,12 +426,12 @@ let print_function p id f = let print_fundef p id fd = match fd with - | Csyntax.External(EF_external(_,_), args, res, cconv) -> + | Ctypes.External((EF_external _ | EF_runtime _), args, res, cconv) -> fprintf p "extern %s;@ @ " (name_cdecl (extern_atom id) (Tfunction(args, res, cconv))) - | Csyntax.External(_, _, _, _) -> + | Ctypes.External(_, _, _, _) -> () - | Csyntax.Internal f -> + | Ctypes.Internal f -> print_function p id f let string_of_init id = @@ -454,8 +456,8 @@ let print_init p = function | Init_int16 n -> fprintf p "%ld" (camlint_of_coqint n) | Init_int32 n -> fprintf p "%ld" (camlint_of_coqint n) | Init_int64 n -> fprintf p "%LdLL" (camlint64_of_coqint n) - | Init_float32 n -> fprintf p "%F" (camlfloat_of_coqfloat n) - | Init_float64 n -> fprintf p "%F" (camlfloat_of_coqfloat n) + | Init_float32 n -> fprintf p "%.15F" (camlfloat_of_coqfloat n) + | Init_float64 n -> fprintf p "%.15F" (camlfloat_of_coqfloat n) | Init_space n -> fprintf p "/* skip %ld */@ " (camlint_of_coqint n) | Init_addrof(symb, ofs) -> let ofs = camlint_of_coqint ofs in diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index a5a6ad66..bfdd8ab9 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -114,7 +114,7 @@ Fixpoint eval_simpl_expr (a: expr) : option val := | Ecast b ty => match eval_simpl_expr b with | None => None - | Some v => sem_cast v (typeof b) ty + | Some v => sem_cast v (typeof b) ty Mem.empty end | _ => None end. @@ -327,10 +327,10 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement let ty2 := Csyntax.typeof r2 in match dst with | For_val | For_set _ => - do t <- gensym ty2; + do t <- gensym ty1; ret (finish dst - (sl1 ++ sl2 ++ Sset t a2 :: make_assign a1 (Etempvar t ty2) :: nil) - (Ecast (Etempvar t ty2) ty1)) + (sl1 ++ sl2 ++ Sset t (Ecast a2 ty1) :: make_assign a1 (Etempvar t ty1) :: nil) + (Etempvar t ty1)) | For_effects => ret (sl1 ++ sl2 ++ make_assign a1 a2 :: nil, dummy_expr) @@ -342,12 +342,12 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement do (sl3, a3) <- transl_valof ty1 a1; match dst with | For_val | For_set _ => - do t <- gensym tyres; + do t <- gensym ty1; ret (finish dst (sl1 ++ sl2 ++ sl3 ++ - Sset t (Ebinop op a3 a2 tyres) :: - make_assign a1 (Etempvar t tyres) :: nil) - (Ecast (Etempvar t tyres) ty1)) + Sset t (Ecast (Ebinop op a3 a2 tyres) ty1) :: + make_assign a1 (Etempvar t ty1) :: nil) + (Etempvar t ty1)) | For_effects => ret (sl1 ++ sl2 ++ sl3 ++ make_assign a1 (Ebinop op a3 a2 tyres) :: nil, dummy_expr) @@ -512,9 +512,9 @@ Local Open Scope error_monad_scope. Definition transl_fundef (fd: Csyntax.fundef) : res fundef := match fd with - | Csyntax.Internal f => + | Internal f => do tf <- transl_function f; OK (Internal tf) - | Csyntax.External ef targs tres cc => + | External ef targs tres cc => OK (External ef targs tres cc) end. @@ -523,6 +523,6 @@ Definition transl_program (p: Csyntax.program) : res program := OK {| prog_defs := AST.prog_defs p1; prog_public := AST.prog_public p1; prog_main := AST.prog_main p1; - prog_types := Csyntax.prog_types p; - prog_comp_env := Csyntax.prog_comp_env p; - prog_comp_env_eq := Csyntax.prog_comp_env_eq p |}. + prog_types := prog_types p; + prog_comp_env := prog_comp_env p; + prog_comp_env_eq := prog_comp_env_eq p |}. diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 0c7c9ce7..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. @@ -752,12 +729,27 @@ Qed. (** Semantics of smart constructors *) +Remark sem_cast_deterministic: + forall v ty ty' m1 v1 m2 v2, + sem_cast v ty ty' m1 = Some v1 -> + sem_cast v ty ty' m2 = Some v2 -> + v1 = v2. +Proof. + unfold sem_cast; intros. destruct (classify_cast ty ty'); try congruence. + destruct v; try congruence. + destruct (Mem.weak_valid_pointer m1 b (Int.unsigned i)); inv H. + destruct (Mem.weak_valid_pointer m2 b (Int.unsigned i)); inv H0. + auto. +Qed. + Lemma eval_simpl_expr_sound: forall e le m a v, eval_expr tge e le m a v -> match eval_simpl_expr a with Some v' => v' = v | None => True end. Proof. induction 1; simpl; auto. - destruct (eval_simpl_expr a); auto. subst. rewrite H0. auto. + destruct (eval_simpl_expr a); auto. subst. + destruct (sem_cast v1 (typeof a) ty Mem.empty) as [v'|] eqn:C; auto. + eapply sem_cast_deterministic; eauto. inv H; simpl; auto. Qed. @@ -811,7 +803,7 @@ Lemma step_make_assign: Csem.assign_loc ge ty m b ofs v t m' -> eval_lvalue tge e le m a1 b ofs -> eval_expr tge e le m a2 v2 -> - sem_cast v2 (typeof a2) ty = Some v -> + sem_cast v2 (typeof a2) ty m = Some v -> typeof a1 = ty -> step1 tge (State f (make_assign a1 a2) k e le m) t (State f Sskip k e le m'). @@ -1649,18 +1641,19 @@ Proof. (* for value *) exploit tr_simple_rvalue; eauto. intros [SL2 [TY2 EV2]]. exploit tr_simple_lvalue. eauto. - eapply tr_expr_invariant with (le' := PTree.set t0 v le). eauto. + eapply tr_expr_invariant with (le' := PTree.set t0 v' le). eauto. intros. apply PTree.gso. intuition congruence. intros [SL1 [TY1 EV1]]. subst; simpl Kseqlist. econstructor; split. left. eapply plus_left. constructor. - eapply star_left. constructor. eauto. + eapply star_left. constructor. econstructor. eauto. rewrite <- TY2; eauto. eapply star_left. constructor. apply star_one. eapply step_make_assign; eauto. - constructor. apply PTree.gss. reflexivity. reflexivity. traceEq. + constructor. apply PTree.gss. simpl. eapply cast_idempotent; eauto. + reflexivity. reflexivity. traceEq. econstructor. auto. apply S. - apply tr_val_gen. auto. intros. econstructor; eauto. constructor. + apply tr_val_gen. auto. intros. constructor. rewrite H4; auto. apply PTree.gss. intros. apply PTree.gso. intuition congruence. auto. auto. @@ -1692,7 +1685,7 @@ Proof. exploit tr_simple_rvalue. eauto. eapply tr_expr_invariant with (le := le) (le' := le'). eauto. intros. apply INV. NOTIN. simpl. intros [SL2 [TY2 EV2]]. exploit tr_simple_lvalue. eauto. - eapply tr_expr_invariant with (le := le) (le' := PTree.set t v3 le'). eauto. + eapply tr_expr_invariant with (le := le) (le' := PTree.set t v4 le'). eauto. intros. rewrite PTree.gso. apply INV. NOTIN. intuition congruence. intros [? [? EV1'']]. subst; simpl Kseqlist. @@ -1700,13 +1693,14 @@ Proof. left. rewrite app_ass. rewrite Kseqlist_app. eapply star_plus_trans. eexact EXEC. simpl. eapply plus_four. econstructor. econstructor. - econstructor. eexact EV3. eexact EV2. + econstructor. econstructor. eexact EV3. eexact EV2. rewrite TY3; rewrite <- TY1; rewrite <- TY2; rewrite comp_env_preserved; eauto. + eassumption. econstructor. eapply step_make_assign; eauto. - constructor. apply PTree.gss. + constructor. apply PTree.gss. simpl. eapply cast_idempotent; eauto. reflexivity. traceEq. econstructor. auto. apply S. - apply tr_val_gen. auto. intros. econstructor; eauto. constructor. + apply tr_val_gen. auto. intros. constructor. rewrite H10; auto. apply PTree.gss. intros. rewrite PTree.gso. apply INV. red; intros; elim H10; auto. @@ -1890,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. @@ -1901,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. @@ -2198,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 *) @@ -2229,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. @@ -2254,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. @@ -2262,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 4077d7df..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. @@ -222,10 +213,10 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement -> ty2 = Csyntax.typeof e2 -> tr_expr le dst (Csyntax.Eassign e1 e2 ty) (sl1 ++ sl2 ++ - Sset t a2 :: - make_assign a1 (Etempvar t ty2) :: - final dst (Ecast (Etempvar t ty2) ty1)) - (Ecast (Etempvar t ty2) ty1) tmp + Sset t (Ecast a2 ty1) :: + make_assign a1 (Etempvar t ty1) :: + final dst (Etempvar t ty1)) + (Etempvar t ty1) tmp | tr_assignop_effects: forall le op e1 e2 tyres ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> tr_expr le For_val e2 sl2 a2 tmp2 -> @@ -246,10 +237,10 @@ Inductive tr_expr: temp_env -> destination -> Csyntax.expr -> list statement -> ty1 = Csyntax.typeof e1 -> tr_expr le dst (Csyntax.Eassignop op e1 e2 tyres ty) (sl1 ++ sl2 ++ sl3 ++ - Sset t (Ebinop op a3 a2 tyres) :: - make_assign a1 (Etempvar t tyres) :: - final dst (Ecast (Etempvar t tyres) ty1)) - (Ecast (Etempvar t tyres) ty1) tmp + Sset t (Ecast (Ebinop op a3 a2 tyres) ty1) :: + make_assign a1 (Etempvar t ty1) :: + final dst (Etempvar t ty1)) + (Etempvar t ty1) tmp | tr_postincr_effects: forall le id e1 ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 any tmp, tr_expr le For_val e1 sl1 a1 tmp1 -> tr_rvalof ty1 a1 sl2 a2 tmp2 -> @@ -375,8 +366,7 @@ Qed. between Csyntax values and Cminor expressions: in the case of [tr_expr], the Cminor expression must not depend on memory, while in the case of [tr_top] it can depend on the current memory - state. This special case is extended to values occurring under - one or several [Csyntax.Eparen]. *) + state. *) Section TR_TOP. @@ -389,19 +379,9 @@ Inductive tr_top: destination -> Csyntax.expr -> list statement -> expr -> list | tr_top_val_val: forall v ty a tmp, typeof a = ty -> eval_expr ge e le m a v -> tr_top For_val (Csyntax.Eval v ty) nil a tmp -(* - | tr_top_val_set: forall t tyl v ty a any tmp, - typeof a = ty -> eval_expr ge e le m a v -> - tr_top (For_set tyl t) (Csyntax.Eval v ty) (Sset t (fold_left Ecast tyl a) :: nil) any tmp -*) | tr_top_base: forall dst r sl a tmp, tr_expr le dst r sl a tmp -> tr_top dst r sl a tmp. -(* - | tr_top_paren_test: forall tyl t r ty sl a tmp, - tr_top (For_set (ty :: tyl) t) r sl a tmp -> - tr_top (For_set tyl t) (Csyntax.Eparen r ty) sl a tmp. -*) End TR_TOP. @@ -1088,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, @@ -1103,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, @@ -1128,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 a47036bf..2cd82d8f 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -13,80 +13,58 @@ (** Semantic preservation for the SimplLocals pass. *) Require Import FSets. -Require FSetAVL. -Require Import Coqlib. -Require Import Errors. -Require Import Ordered. -Require Import AST. -Require Import Maps. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Events. -Require Import Smallstep. -Require Import Ctypes. -Require Import Cop. -Require Import Clight. -Require Import SimplLocals. +Require Import Coqlib Errors Ordered Maps Integers Floats. +Require Import AST Linking. +Require Import Values Memory Globalenvs Events Smallstep. +Require Import Ctypes Cop Clight SimplLocals. Module VSF := FSetFacts.Facts(VSet). Module VSP := FSetProperties.Properties(VSet). +Definition match_prog (p tp: program) : Prop := + match_program (fun ctx f tf => transf_fundef f = OK tf) eq p tp + /\ prog_types tp = prog_types p. + +Lemma match_transf_program: + forall p tp, transf_program p = OK tp -> match_prog p tp. +Proof. + unfold transf_program; intros. monadInv H. + split; auto. apply match_transform_partial_program. rewrite EQ. destruct x; auto. +Qed. + Section PRESERVATION. Variable prog: program. Variable tprog: program. -Hypothesis TRANSF: transf_program prog = OK tprog. +Hypothesis TRANSF: match_prog prog tprog. Let ge := globalenv prog. Let tge := globalenv tprog. Lemma comp_env_preserved: genv_cenv tge = genv_cenv ge. Proof. - monadInv TRANSF. unfold tge; rewrite <- H0; auto. -Qed. - -Lemma transf_programs: - AST.transform_partial_program transf_fundef (program_of_program prog) = OK (program_of_program tprog). -Proof. - monadInv TRANSF. rewrite EQ. destruct x; reflexivity. + unfold tge, ge. destruct prog, tprog; simpl. destruct TRANSF as [_ EQ]. simpl in EQ. congruence. Qed. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof. - exact (Genv.find_symbol_transf_partial _ _ transf_programs). -Qed. +Proof (Genv.find_symbol_match (proj1 TRANSF)). -Lemma public_preserved: - forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. -Proof. - exact (Genv.public_symbol_transf_partial _ _ transf_programs). -Qed. - -Lemma varinfo_preserved: - forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. -Proof. - exact (Genv.find_var_info_transf_partial _ _ transf_programs). -Qed. +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_match (proj1 TRANSF)). Lemma functions_translated: forall (v: val) (f: fundef), Genv.find_funct ge v = Some f -> exists tf, Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf. -Proof. - exact (Genv.find_funct_transf_partial _ _ transf_programs). -Qed. +Proof (Genv.find_funct_transf_partial (proj1 TRANSF)). Lemma function_ptr_translated: forall (b: block) (f: fundef), Genv.find_funct_ptr ge b = Some f -> exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf. -Proof. - exact (Genv.find_funct_ptr_transf_partial _ _ transf_programs). -Qed. +Proof (Genv.find_funct_ptr_transf_partial (proj1 TRANSF)). Lemma type_of_fundef_preserved: forall fd tfd, @@ -201,97 +179,7 @@ Proof. xomegaContradiction. Qed. -(** Properties of values obtained by casting to a given type. *) - -Inductive val_casted: val -> type -> Prop := - | val_casted_int: forall sz si attr n, - cast_int_int sz si n = n -> - val_casted (Vint n) (Tint sz si attr) - | val_casted_float: forall attr n, - val_casted (Vfloat n) (Tfloat F64 attr) - | val_casted_single: forall attr n, - val_casted (Vsingle n) (Tfloat F32 attr) - | val_casted_long: forall si attr n, - val_casted (Vlong n) (Tlong si attr) - | val_casted_ptr_ptr: forall b ofs ty attr, - val_casted (Vptr b ofs) (Tpointer ty attr) - | val_casted_int_ptr: forall n ty attr, - val_casted (Vint n) (Tpointer ty attr) - | val_casted_ptr_int: forall b ofs si attr, - val_casted (Vptr b ofs) (Tint I32 si attr) - | val_casted_struct: forall id attr b ofs, - val_casted (Vptr b ofs) (Tstruct id attr) - | val_casted_union: forall id attr b ofs, - val_casted (Vptr b ofs) (Tunion id attr) - | val_casted_void: forall v, - val_casted v Tvoid. - -Remark cast_int_int_idem: - forall sz sg i, cast_int_int sz sg (cast_int_int sz sg i) = cast_int_int sz sg i. -Proof. - intros. destruct sz; simpl; auto. - destruct sg; [apply Int.sign_ext_idem|apply Int.zero_ext_idem]; compute; intuition congruence. - destruct sg; [apply Int.sign_ext_idem|apply Int.zero_ext_idem]; compute; intuition congruence. - destruct (Int.eq i Int.zero); auto. -Qed. - -Lemma cast_val_is_casted: - forall v ty ty' v', sem_cast v ty ty' = Some v' -> val_casted v' ty'. -Proof. - unfold sem_cast; intros. destruct ty'; simpl in *. -(* void *) - constructor. -(* int *) - destruct i; destruct ty; simpl in H; try (destruct f); try discriminate; destruct v; inv H. - constructor. apply (cast_int_int_idem I8 s). - constructor. apply (cast_int_int_idem I8 s). - destruct (cast_single_int s f); inv H1. constructor. apply (cast_int_int_idem I8 s). - destruct (cast_float_int s f); inv H1. constructor. apply (cast_int_int_idem I8 s). - constructor. apply (cast_int_int_idem I16 s). - constructor. apply (cast_int_int_idem I16 s). - destruct (cast_single_int s f); inv H1. constructor. apply (cast_int_int_idem I16 s). - destruct (cast_float_int s f); inv H1. constructor. apply (cast_int_int_idem I16 s). - constructor. auto. - constructor. - constructor. auto. - destruct (cast_single_int s f); inv H1. constructor. auto. - destruct (cast_float_int s f); inv H1. constructor; auto. - constructor; auto. - constructor. - constructor; auto. - constructor. - constructor; auto. - constructor. - constructor. simpl. destruct (Int.eq i0 Int.zero); auto. - constructor. simpl. destruct (Int64.eq i Int64.zero); auto. - constructor. simpl. destruct (Float32.cmp Ceq f Float32.zero); auto. - constructor. simpl. destruct (Float.cmp Ceq f Float.zero); auto. - constructor. simpl. destruct (Int.eq i Int.zero); auto. - constructor. simpl. destruct (Int.eq i Int.zero); auto. - constructor. simpl. destruct (Int.eq i Int.zero); auto. -(* long *) - destruct ty; try (destruct f); try discriminate. - destruct v; inv H. constructor. - destruct v; inv H. constructor. - destruct v; try discriminate. destruct (cast_single_long s f); inv H. constructor. - destruct v; try discriminate. destruct (cast_float_long s f); inv H. constructor. - destruct v; inv H. constructor. - destruct v; inv H. constructor. - destruct v; inv H. constructor. -(* float *) - destruct f; destruct ty; simpl in H; try (destruct f); try discriminate; destruct v; inv H; constructor. -(* pointer *) - destruct ty; simpl in H; try discriminate; destruct v; inv H; try constructor. -(* impossible cases *) - discriminate. - discriminate. -(* structs *) - destruct ty; try discriminate; destruct v; try discriminate. - destruct (ident_eq i0 i); inv H; constructor. -(* unions *) - destruct ty; try discriminate; destruct v; try discriminate. - destruct (ident_eq i0 i); inv H; constructor. -Qed. +(** Properties of values resulting from a cast *) Lemma val_casted_load_result: forall v ty chunk, @@ -316,15 +204,6 @@ Proof. discriminate. Qed. -Lemma cast_val_casted: - forall v ty, val_casted v ty -> sem_cast v ty ty = Some v. -Proof. - intros. inversion H; clear H; subst v ty; unfold sem_cast; simpl; auto. - destruct sz; congruence. - unfold proj_sumbool; repeat rewrite dec_eq_true; auto. - unfold proj_sumbool; repeat rewrite dec_eq_true; auto. -Qed. - Lemma val_casted_inject: forall f v v' ty, Val.inject f v v' -> val_casted v ty -> val_casted v' ty. @@ -363,7 +242,7 @@ Qed. Lemma make_cast_correct: forall e le m a v1 tto v2, eval_expr tge e le m a v1 -> - sem_cast v1 (typeof a) tto = Some v2 -> + sem_cast v1 (typeof a) tto m = Some v2 -> eval_expr tge e le m (make_cast a tto) v2. Proof. intros. @@ -386,9 +265,9 @@ Qed. (** Debug annotations. *) Lemma cast_typeconv: - forall v ty, + forall v ty m, val_casted v ty -> - sem_cast v ty (typeconv ty) = Some v. + sem_cast v ty (typeconv ty) m = Some v. Proof. induction 1; simpl; auto. - destruct sz; auto. @@ -423,7 +302,7 @@ Qed. Lemma step_Sset_debug: forall f id ty a k e le m v v', eval_expr tge e le m a v -> - sem_cast v (typeof a) ty = Some v' -> + sem_cast v (typeof a) ty m = Some v' -> plus step2 tge (State f (Sset_debug id ty a) k e le m) E0 (State f Sskip k e (PTree.set id v' le) m). Proof. @@ -2172,8 +2051,7 @@ Proof. exploit external_call_mem_inject; eauto. apply match_globalenvs_preserves_globals; eauto with compat. intros [j' [tvres [tm' [P [Q [R [S [T [U V]]]]]]]]]. econstructor; split. - apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved. econstructor; eauto with compat. eapply match_envs_set_opttemp; eauto. eapply match_envs_extcall; eauto. @@ -2334,8 +2212,7 @@ Proof. eapply match_cont_globalenv. eexact (MCONT VSet.empty). intros [j' [tvres [tm' [P [Q [R [S [T [U V]]]]]]]]]. econstructor; split. - apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved. econstructor; eauto. intros. apply match_cont_incr_bounds with (Mem.nextblock m) (Mem.nextblock tm). eapply match_cont_extcall; eauto. xomega. xomega. @@ -2358,10 +2235,10 @@ Proof. exploit function_ptr_translated; eauto. intros [tf [A B]]. econstructor; split. econstructor. - eapply Genv.init_mem_transf_partial. eexact transf_programs. eauto. - change (prog_main tprog) with (AST.prog_main tprog). - rewrite (transform_partial_program_main _ _ transf_programs). + eapply (Genv.init_mem_transf_partial (proj1 TRANSF)). eauto. + replace (prog_main tprog) with (prog_main prog). instantiate (1 := b). rewrite <- H1. apply symbols_preserved. + generalize (match_program_main (proj1 TRANSF)). simpl; auto. eauto. rewrite <- H3; apply type_of_fundef_preserved; auto. econstructor; eauto. @@ -2391,10 +2268,27 @@ Theorem transf_program_correct: forward_simulation (semantics1 prog) (semantics2 tprog). Proof. eapply forward_simulation_plus. - eexact public_preserved. + apply senv_preserved. eexact initial_states_simulation. eexact final_states_simulation. eexact step_simulation. Qed. End PRESERVATION. + +(** ** Commutation with linking *) + +Instance TransfSimplLocalsLink : TransfLink match_prog. +Proof. + red; intros. eapply Ctypes.link_match_program; eauto. +- intros. +Local Transparent Linker_fundef. + simpl in *; unfold link_fundef in *. + destruct f1; monadInv H3; destruct f2; monadInv H4; try discriminate. + destruct e; inv H2. exists (Internal x); split; auto. simpl; rewrite EQ; auto. + destruct e; inv H2. exists (Internal x); split; auto. simpl; rewrite EQ; auto. + destruct (external_function_eq e e0 && typelist_eq t t1 && + type_eq t0 t2 && calling_convention_eq c c0); inv H2. + econstructor; split; eauto. +Qed. + |