From a15858a0a8fcea82db02fe8c9bd2ed912210419f Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 18 Aug 2010 09:06:55 +0000 Subject: Merge of branches/full-expr-4: - Csyntax, Csem: source C language has side-effects within expressions, performs implicit casts, and has nondeterministic reduction semantics for expressions - Cstrategy: deterministic red. sem. for the above - Clight: the previous source C language, with pure expressions. Added: temporary variables + implicit casts. - New pass SimplExpr to pull side-effects out of expressions (previously done in untrusted Caml code in cparser/) - Csharpminor: added temporary variables to match Clight. - Cminorgen: adapted, removed cast optimization (moved to back-end) - CastOptim: RTL-level optimization of casts - cparser: transformations Bitfields, StructByValue and StructAssign now work on non-simplified expressions - Added pretty-printers for several intermediate languages, and matching -dxxx command-line flags. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1467 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cshmgenproof.v | 1869 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1869 insertions(+) create mode 100644 cfrontend/Cshmgenproof.v (limited to 'cfrontend/Cshmgenproof.v') diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v new file mode 100644 index 0000000..02fab6f --- /dev/null +++ b/cfrontend/Cshmgenproof.v @@ -0,0 +1,1869 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** * 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 Csyntax. +Require Import Csem. +Require Import Clight. +Require Import Cminor. +Require Import Csharpminor. +Require Import Cshmgen. + +(** * Properties of operations over types *) + +Remark type_of_chunk_of_type: + forall ty chunk, + chunk_of_type ty = OK chunk -> + type_of_chunk chunk = typ_of_type ty. +Proof. + intros. unfold chunk_of_type in H. destruct ty; simpl in H; try monadInv H. + destruct i; destruct s; monadInv H; reflexivity. + destruct f; monadInv H; reflexivity. + reflexivity. reflexivity. +Qed. + +Remark transl_params_types: + forall p tp, + transl_params p = OK tp -> + map type_of_chunk (map param_chunk tp) = typlist_of_typelist (type_of_params p). +Proof. + induction p; simpl; intros. + inv H. auto. + destruct a as [id ty]. generalize H; clear H. case_eq (chunk_of_type ty); intros. + monadInv H0. simpl. f_equal; auto. apply type_of_chunk_of_type; auto. + inv H0. +Qed. + +Lemma transl_fundef_sig1: + forall f tf args res, + transl_fundef f = OK tf -> + classify_fun (type_of_fundef f) = fun_case_f args res -> + funsig tf = signature_of_type args res. +Proof. + intros. destruct f; simpl in *. + monadInv H. monadInv EQ. simpl. inversion H0. + unfold fn_sig; simpl. unfold signature_of_type. f_equal. + apply transl_params_types; auto. + destruct (list_typ_eq (sig_args (ef_sig e)) (typlist_of_typelist t)); simpl in H. + destruct (opt_typ_eq (sig_res (ef_sig e)) (opttyp_of_type t0)); simpl in H. + inv H. simpl. destruct (ef_sig e); simpl in *. inv H0. + unfold signature_of_type. auto. + congruence. + congruence. +Qed. + +Lemma transl_fundef_sig2: + forall f tf args res, + transl_fundef f = OK tf -> + type_of_fundef f = Tfunction args res -> + funsig tf = signature_of_type args res. +Proof. + intros. eapply transl_fundef_sig1; eauto. + rewrite H0; reflexivity. +Qed. + +Lemma var_kind_by_value: + forall ty chunk, + access_mode ty = By_value chunk -> + var_kind_of_type ty = OK(Vscalar chunk). +Proof. + intros ty chunk; destruct ty; simpl; try congruence. + destruct i; try congruence; destruct s; congruence. + destruct f; congruence. +Qed. + +Lemma sizeof_var_kind_of_type: + forall ty vk, + var_kind_of_type ty = OK vk -> + Csharpminor.sizeof vk = Csyntax.sizeof ty. +Proof. + intros ty vk. + assert (sizeof (Varray (Csyntax.sizeof ty)) = Csyntax.sizeof ty). + simpl. rewrite Zmax_spec. apply zlt_false. + generalize (Csyntax.sizeof_pos ty). omega. + destruct ty; try (destruct i; try destruct s); try (destruct f); + simpl; intro EQ; inversion EQ; subst vk; auto. +Qed. + +Remark cast_int_int_normalized: + forall sz si chunk n, + access_mode (Tint sz si) = By_value chunk -> + val_normalized (Vint (cast_int_int sz si n)) chunk. +Proof. + unfold access_mode, cast_int_int, val_normalized; intros. destruct sz. + destruct si; inv H; simpl. + rewrite Int.sign_ext_idem; auto. compute; auto. + rewrite Int.zero_ext_idem; auto. compute; auto. + destruct si; inv H; simpl. + rewrite Int.sign_ext_idem; auto. compute; auto. + rewrite Int.zero_ext_idem; auto. compute; auto. + inv H. auto. +Qed. + +Remark cast_float_float_normalized: + forall sz chunk n, + access_mode (Tfloat sz) = By_value chunk -> + val_normalized (Vfloat (cast_float_float sz n)) chunk. +Proof. + unfold access_mode, cast_float_float, val_normalized; intros. + destruct sz; inv H; simpl. + rewrite Float.singleoffloat_idem. auto. + auto. +Qed. + +Remark neutral_for_cast_chunk: + forall ty chunk, + neutral_for_cast ty -> access_mode ty = By_value chunk -> chunk = Mint32. +Proof. + induction 1; simpl; intros; inv H; auto. +Qed. + +Lemma cast_result_normalized: + forall chunk v1 ty1 ty2 v2, + cast v1 ty1 ty2 v2 -> + access_mode ty2 = By_value chunk -> + val_normalized v2 chunk. +Proof. + induction 1; intros; simpl. + apply cast_int_int_normalized; auto. + apply cast_int_int_normalized; auto. + apply cast_float_float_normalized; auto. + apply cast_float_float_normalized; auto. + rewrite (neutral_for_cast_chunk _ _ H0 H1). red; auto. + rewrite (neutral_for_cast_chunk _ _ H0 H1). red; auto. +Qed. + +Definition val_casted (v: val) (ty: type) : Prop := + exists v0, exists ty0, cast v0 ty0 ty v. + +Lemma val_casted_normalized: + forall v ty chunk, + val_casted v ty -> access_mode ty = By_value chunk -> val_normalized v chunk. +Proof. + intros. destruct H as [v0 [ty0 CAST]]. eapply cast_result_normalized; eauto. +Qed. + +Fixpoint val_casted_list (vl: list val) (tyl: typelist) {struct vl}: Prop := + match vl, tyl with + | nil, Tnil => True + | v1 :: vl', Tcons ty1 tyl' => val_casted v1 ty1 /\ val_casted_list vl' tyl' + | _, _ => False + end. + +Lemma eval_exprlist_casted: + forall ge e le m al tyl vl, + Clight.eval_exprlist ge e le m al tyl vl -> + val_casted_list vl tyl. +Proof. + induction 1; simpl. + auto. + split. exists v1; exists (typeof a); auto. eauto. +Qed. + +(** * Properties of the translation functions *) + +Lemma map_partial_names: + forall (A B: Type) (f: A -> res B) + (l: list (ident * A)) (tl: list (ident * B)), + map_partial prefix_var_name f l = OK tl -> + List.map (@fst ident B) tl = List.map (@fst ident A) l. +Proof. + induction l; simpl. + intros. inversion H. reflexivity. + intro tl. destruct a as [id x]. destruct (f x); try congruence. + caseEq (map_partial prefix_var_name f l); simpl; intros; try congruence. + inv H0. simpl. decEq. auto. +Qed. + +Lemma map_partial_append: + forall (A B: Type) (f: A -> res B) + (l1 l2: list (ident * A)) (tl1 tl2: list (ident * B)), + map_partial prefix_var_name f l1 = OK tl1 -> + map_partial prefix_var_name f l2 = OK tl2 -> + map_partial prefix_var_name f (l1 ++ l2) = OK (tl1 ++ tl2). +Proof. + induction l1; intros until tl2; simpl. + intros. inversion H. simpl; auto. + destruct a as [id x]. destruct (f x); try congruence. + caseEq (map_partial prefix_var_name f l1); simpl; intros; try congruence. + inv H0. rewrite (IHl1 _ _ _ H H1). auto. +Qed. + +Lemma transl_params_names: + forall vars tvars, + transl_params vars = OK tvars -> + List.map param_name tvars = var_names vars. +Proof. + exact (map_partial_names _ _ chunk_of_type). +Qed. + +Lemma transl_vars_names: + forall vars tvars, + transl_vars vars = OK tvars -> + List.map variable_name tvars = var_names vars. +Proof. + exact (map_partial_names _ _ var_kind_of_type). +Qed. + +Lemma transl_names_norepet: + forall params vars sg tparams tvars temps body, + list_norepet (var_names params ++ var_names vars) -> + transl_params params = OK tparams -> + transl_vars vars = OK tvars -> + let f := Csharpminor.mkfunction sg tparams tvars temps body in + list_norepet (fn_params_names f ++ fn_vars_names f). +Proof. + intros. unfold fn_params_names, fn_vars_names, f. simpl. + rewrite (transl_params_names _ _ H0). + rewrite (transl_vars_names _ _ H1). + auto. +Qed. + +Lemma transl_vars_append: + forall l1 l2 tl1 tl2, + transl_vars l1 = OK tl1 -> transl_vars l2 = OK tl2 -> + transl_vars (l1 ++ l2) = OK (tl1 ++ tl2). +Proof. + exact (map_partial_append _ _ var_kind_of_type). +Qed. + +Lemma transl_params_vars: + forall params tparams, + transl_params params = OK tparams -> + transl_vars params = + OK (List.map (fun id_chunk => (fst id_chunk, Vscalar (snd id_chunk))) tparams). +Proof. + induction params; intro tparams; simpl. + intros. inversion H. reflexivity. + destruct a as [id x]. + unfold chunk_of_type. caseEq (access_mode x); try congruence. + intros chunk AM. + caseEq (transl_params params); simpl; intros; try congruence. + inv H0. + rewrite (var_kind_by_value _ _ AM). + rewrite (IHparams _ H). reflexivity. +Qed. + +Lemma transl_fn_variables: + forall params vars sg tparams tvars temps body, + transl_params params = OK tparams -> + transl_vars vars = OK tvars -> + let f := Csharpminor.mkfunction sg tparams tvars temps body in + transl_vars (params ++ vars) = OK (fn_variables f). +Proof. + intros. + generalize (transl_params_vars _ _ H); intro. + rewrite (transl_vars_append _ _ _ _ H1 H0). + reflexivity. +Qed. + +(** Transformation of expressions and statements. *) + +Lemma is_variable_correct: + forall a id, + is_variable a = Some id -> + a = Clight.Evar id (typeof a). +Proof. + intros until id. unfold is_variable; destruct a; intros; try discriminate. + simpl. congruence. +Qed. + +Lemma transl_expr_lvalue: + forall ge e le m a loc ofs ta, + Clight.eval_lvalue ge e le m a loc ofs -> + transl_expr a = OK ta -> + (exists id, exists ty, a = Clight.Evar id ty /\ var_get id ty = OK ta) \/ + (exists tb, transl_lvalue a = OK tb /\ + make_load tb (typeof a) = OK ta). +Proof. + intros. inversion H; subst; clear H; simpl in H0. + left; exists id; exists ty; auto. + left; exists id; exists ty; auto. + monadInv H0. right. exists x; split; auto. + rewrite H2 in H0. monadInv H0. right. + exists (Ebinop Oadd x (make_intconst (Int.repr x0))). split; auto. + simpl. rewrite H2. rewrite EQ. rewrite EQ1. auto. + rewrite H2 in H0. monadInv H0. right. + exists x; split; auto. + simpl. rewrite H2. auto. +Qed. + +(** Properties of labeled statements *) + +Lemma transl_lbl_stmt_1: + forall tyret nbrk ncnt n sl tsl, + transl_lbl_stmt tyret nbrk ncnt sl = OK tsl -> + transl_lbl_stmt tyret nbrk ncnt (Clight.select_switch n sl) = OK (select_switch n tsl). +Proof. + induction sl; intros. + monadInv H. simpl. rewrite EQ. auto. + generalize H; intro TR. monadInv TR. simpl. + destruct (Int.eq i n). auto. auto. +Qed. + +Lemma transl_lbl_stmt_2: + forall tyret nbrk ncnt sl tsl, + transl_lbl_stmt tyret nbrk ncnt sl = OK tsl -> + transl_statement tyret nbrk ncnt (seq_of_labeled_statement sl) = OK (seq_of_lbl_stmt tsl). +Proof. + induction sl; intros. + monadInv H. simpl. auto. + monadInv H. simpl. rewrite EQ; simpl. rewrite (IHsl _ EQ1). simpl. auto. +Qed. + +(** * Correctness of Csharpminor construction functions *) + +Section CONSTRUCTORS. + +Variable ge: genv. + +Lemma make_intconst_correct: + forall n e le m, + eval_expr ge e le m (make_intconst n) (Vint n). +Proof. + intros. unfold make_intconst. econstructor. reflexivity. +Qed. + +Lemma make_floatconst_correct: + forall n e le m, + eval_expr ge e le m (make_floatconst n) (Vfloat n). +Proof. + intros. unfold make_floatconst. econstructor. reflexivity. +Qed. + +Lemma make_floatofint_correct: + forall a n sg e le m, + eval_expr ge e le m a (Vint n) -> + eval_expr ge e le m (make_floatofint a sg) (Vfloat(cast_int_float sg n)). +Proof. + intros. unfold make_floatofint, cast_int_float. + destruct sg; econstructor; eauto. +Qed. + +Hint Resolve make_intconst_correct make_floatconst_correct + make_floatofint_correct + eval_Eunop eval_Ebinop: cshm. +Hint Extern 2 (@eq trace _ _) => traceEq: cshm. + +Remark Vtrue_is_true: Val.is_true Vtrue. +Proof. + simpl. apply Int.one_not_zero. +Qed. + +Remark Vfalse_is_false: Val.is_false Vfalse. +Proof. + simpl. auto. +Qed. + +Lemma make_boolean_correct_true: + forall e le m a v ty, + eval_expr ge e le m a v -> + is_true v ty -> + exists vb, + eval_expr ge e le m (make_boolean a ty) vb + /\ Val.is_true vb. +Proof. + intros until ty; intros EXEC VTRUE. + destruct ty; simpl; + try (exists v; intuition; inversion VTRUE; simpl; auto; fail). + exists Vtrue; split. + eapply eval_Ebinop; eauto with cshm. + inversion VTRUE; simpl. + rewrite Float.cmp_ne_eq. rewrite H1. auto. + apply Vtrue_is_true. +Qed. + +Lemma make_boolean_correct_false: + forall e le m a v ty, + eval_expr ge e le m a v -> + is_false v ty -> + exists vb, + eval_expr ge e le m (make_boolean a ty) vb + /\ Val.is_false vb. +Proof. + intros until ty; intros EXEC VFALSE. + destruct ty; simpl; + try (exists v; intuition; inversion VFALSE; simpl; auto; fail). + exists Vfalse; split. + eapply eval_Ebinop; eauto with cshm. + inversion VFALSE; simpl. + rewrite Float.cmp_ne_eq. rewrite H1. auto. + apply Vfalse_is_false. +Qed. + +Lemma make_neg_correct: + forall a tya c va v e le m, + sem_neg va tya = Some v -> + make_neg a tya = OK c -> + eval_expr ge e le m a va -> + eval_expr ge e le m c v. +Proof. + intros until m; intro SEM. unfold make_neg. + functional inversion SEM; intros. + rewrite H0 in H4. inv H4. eapply eval_Eunop; eauto with cshm. + rewrite H0 in H4. inv H4. eauto with cshm. +Qed. + +Lemma make_notbool_correct: + forall a tya c va v e le m, + sem_notbool va tya = Some v -> + make_notbool a tya = OK c -> + eval_expr ge e le m a va -> + eval_expr ge e le m c v. +Proof. + intros until m; intro SEM. unfold make_notbool. + functional inversion SEM; intros; rewrite H0 in H4; inversion H4; simpl; + eauto with cshm. +Qed. + +Lemma make_notint_correct: + forall a tya c va v e le m, + sem_notint va tya = Some v -> + make_notint a tya = c -> + eval_expr ge e le m a va -> + eval_expr ge e le m c v. +Proof. + intros until m; intro SEM. unfold make_notint. + functional inversion SEM; intros. subst. eauto with cshm. +Qed. + +Definition binary_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 -> + 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 binary_constructor_correct' + (make: expr -> type -> expr -> type -> res expr) + (sem: val -> val -> option val): Prop := + forall a tya b tyb c va vb v e le m, + sem va vb = 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. +*) + +Lemma make_add_correct: binary_constructor_correct make_add sem_add. +Proof. + red; intros until m. intro SEM. unfold make_add. + functional inversion SEM; rewrite H0; intros; + inversion H7; eauto with cshm. + eapply eval_Ebinop. eauto. + eapply eval_Ebinop. eauto with cshm. eauto. + simpl. reflexivity. reflexivity. + eapply eval_Ebinop. eauto. + eapply eval_Ebinop. eauto with cshm. eauto. + simpl. reflexivity. simpl. reflexivity. +Qed. + +Lemma make_sub_correct: binary_constructor_correct make_sub sem_sub. +Proof. + red; intros until m. intro SEM. unfold make_sub. + functional inversion SEM; rewrite H0; intros; + inversion H7; eauto with cshm. + eapply eval_Ebinop. eauto. + eapply eval_Ebinop. eauto with cshm. eauto. + simpl. reflexivity. reflexivity. + inversion H9. eapply eval_Ebinop. + eapply eval_Ebinop; eauto. + simpl. unfold eq_block; rewrite H3. reflexivity. + eauto with cshm. simpl. rewrite H8. reflexivity. +Qed. + +Lemma make_mul_correct: binary_constructor_correct make_mul sem_mul. +Proof. + red; intros until m. intro SEM. unfold make_mul. + functional inversion SEM; rewrite H0; intros; + inversion H7; eauto with cshm. +Qed. + +Lemma make_div_correct: binary_constructor_correct make_div sem_div. +Proof. + red; intros until m. intro SEM. unfold make_div. + functional inversion SEM; rewrite H0; intros. + inversion H8. eapply eval_Ebinop; eauto with cshm. + simpl. rewrite H7; auto. + inversion H8. eapply eval_Ebinop; eauto with cshm. + simpl. rewrite H7; auto. + inversion H7; eauto with cshm. + inversion H7; eauto with cshm. + inversion H7; eauto with cshm. +Qed. + +Lemma make_mod_correct: binary_constructor_correct make_mod sem_mod. + red; intros until m. intro SEM. unfold make_mod. + functional inversion SEM; rewrite H0; intros. + inversion H8. eapply eval_Ebinop; eauto with cshm. + simpl. rewrite H7; auto. + inversion H8. eapply eval_Ebinop; eauto with cshm. + simpl. rewrite H7; auto. +Qed. + +Lemma make_and_correct: binary_constructor_correct make_and sem_and. +Proof. + red; intros until m. intro SEM. unfold make_and. + functional inversion SEM. intros. inversion H7. + eauto with cshm. +Qed. + +Lemma make_or_correct: binary_constructor_correct make_or sem_or. +Proof. + red; intros until m. intro SEM. unfold make_or. + functional inversion SEM. intros. inversion H7. + eauto with cshm. +Qed. + +Lemma make_xor_correct: binary_constructor_correct make_xor sem_xor. +Proof. + red; intros until m. intro SEM. unfold make_xor. + functional inversion SEM. intros. inversion H7. + eauto with cshm. +Qed. + +Lemma make_shl_correct: binary_constructor_correct make_shl sem_shl. +Proof. + red; intros until m. intro SEM. unfold make_shl. + functional inversion SEM. intros. inversion H8. + eapply eval_Ebinop; eauto with cshm. + simpl. rewrite H7. auto. +Qed. + +Lemma make_shr_correct: binary_constructor_correct make_shr sem_shr. +Proof. + red; intros until m. intro SEM. unfold make_shr. + functional inversion SEM; intros; rewrite H0 in H8; inversion H8. + eapply eval_Ebinop; eauto with cshm. + simpl; rewrite H7; auto. + eapply eval_Ebinop; eauto with cshm. + simpl; rewrite H7; 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. +Proof. + intros until m. intro SEM. unfold make_cmp. + functional inversion SEM; rewrite H0; intros. + (* iiu *) + inversion H8. eauto with cshm. + (* ipip int int *) + inversion H8. eauto with cshm. + (* ipip ptr ptr *) + inversion H10. eapply eval_Ebinop; eauto with cshm. + simpl. rewrite H3. unfold eq_block. rewrite H9. auto. + inversion H10. eapply eval_Ebinop; eauto with cshm. + simpl. rewrite H3. unfold eq_block. rewrite H9. auto. + (* ipip ptr int *) + inversion H9. eapply eval_Ebinop; eauto with cshm. + simpl. unfold eval_compare_null. rewrite H8. auto. + (* ipip int ptr *) + inversion H9. eapply eval_Ebinop; eauto with cshm. + simpl. unfold eval_compare_null. rewrite H8. auto. + (* ff *) + inversion H8. eauto with cshm. + (* if *) + inversion H8. eauto with cshm. + (* fi *) + inversion H8. eauto with cshm. +Qed. + +Lemma transl_unop_correct: + forall op a tya c va v e le m, + transl_unop op a tya = OK c -> + sem_unary_operation op va tya = Some v -> + eval_expr ge e le m a va -> + eval_expr ge e le m c v. +Proof. + intros. destruct op; simpl in *. + eapply make_notbool_correct; eauto. + eapply make_notint_correct with (tya := tya); eauto. congruence. + eapply make_neg_correct; eauto. +Qed. + +Lemma transl_binop_correct: + forall op a tya b tyb c va vb v e le m, + transl_binop op a tya b tyb = OK c -> + sem_binary_operation 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. +Proof. + intros. destruct op; simpl in *. + eapply make_add_correct; eauto. + eapply make_sub_correct; eauto. + eapply make_mul_correct; eauto. + eapply make_div_correct; eauto. + eapply make_mod_correct; eauto. + eapply make_and_correct; eauto. + eapply make_or_correct; eauto. + eapply make_xor_correct; eauto. + eapply make_shl_correct; eauto. + eapply make_shr_correct; eauto. + eapply make_cmp_correct; eauto. + eapply make_cmp_correct; eauto. + eapply make_cmp_correct; eauto. + eapply make_cmp_correct; eauto. + eapply make_cmp_correct; eauto. + eapply make_cmp_correct; eauto. +Qed. + +Lemma make_cast_correct: + forall e le m a v ty1 ty2 v', + eval_expr ge e le m a v -> + cast v ty1 ty2 v' -> + eval_expr ge e le m (make_cast ty1 ty2 a) v'. +Proof. + unfold make_cast, make_cast1, make_cast2. + intros until v'; intros EVAL CAST. + inversion CAST; clear CAST; subst. + (* cast_int_int *) + destruct sz2; destruct si2; repeat econstructor; eauto with cshm. + (* cast_float_int *) + destruct sz2; destruct si2; unfold make_intoffloat; repeat econstructor; eauto with cshm; simpl; auto. + (* cast_int_float *) + destruct sz2; destruct si1; unfold make_floatofint; repeat econstructor; eauto with cshm; simpl; auto. + (* cast_float_float *) + destruct sz2; repeat econstructor; eauto with cshm. + (* neutral, ptr *) + inversion H0; auto; inversion H; auto. + (* neutral, int *) + inversion H0; auto; inversion H; auto. +Qed. + +Lemma make_load_correct: + forall addr ty code b ofs v e le m, + make_load addr ty = OK code -> + eval_expr ge e le m addr (Vptr b ofs) -> + load_value_of_type ty m b ofs = Some v -> + eval_expr ge e le m code v. +Proof. + unfold make_load, load_value_of_type. + intros until m; intros MKLOAD EVEXP LDVAL. + destruct (access_mode ty); inversion MKLOAD. + (* access_mode ty = By_value m *) + apply eval_Eload with (Vptr b ofs); auto. + (* access_mode ty = By_reference *) + subst code. inversion LDVAL. auto. +Qed. + +Lemma make_store_correct: + forall addr ty rhs code e le m b ofs v m' f k, + make_store addr ty rhs = OK code -> + eval_expr ge e le m addr (Vptr b ofs) -> + eval_expr ge e le m rhs v -> + store_value_of_type ty m b ofs v = Some m' -> + step ge (State f code k e le m) E0 (State f Sskip k e le m'). +Proof. + unfold make_store, store_value_of_type. + intros until k; intros MKSTORE EV1 EV2 STVAL. + destruct (access_mode ty); inversion MKSTORE. + (* access_mode ty = By_value m *) + eapply step_store; eauto. +Qed. + +End CONSTRUCTORS. + +(** * Basic preservation invariants *) + +Section CORRECTNESS. + +Variable prog: Clight.program. +Variable tprog: Csharpminor.program. +Hypothesis TRANSL: transl_program prog = OK tprog. + +Let ge := Genv.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 transl_globvar _ 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 f = OK tf. +Proof (Genv.find_funct_transf_partial2 transl_fundef 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 f = OK tf. +Proof (Genv.find_funct_ptr_transf_partial2 transl_fundef transl_globvar _ TRANSL). + +Lemma var_info_translated: + forall b v, + Genv.find_var_info ge b = Some v -> + exists tv, Genv.find_var_info tge b = Some tv /\ transf_globvar transl_globvar v = OK tv. +Proof (Genv.find_var_info_transf_partial2 transl_fundef transl_globvar _ TRANSL). + +(** * Matching between environments *) + +(** In this section, we define a matching relation between + a Clight local environment and a Csharpminor local environment. *) + +Record match_env (e: Clight.env) (te: Csharpminor.env) : Prop := + mk_match_env { + me_local: + forall id b ty, + e!id = Some (b, ty) -> + exists vk, var_kind_of_type ty = OK vk /\ te!id = Some (b, vk); + me_local_inv: + forall id b vk, + te!id = Some (b, vk) -> exists ty, e!id = Some(b, ty) + }. + +Lemma match_env_globals: + forall e te id l ty, + match_env e te -> + e!id = None -> + Genv.find_symbol ge id = Some l -> + type_of_global ge l = Some ty -> + te!id = None /\ + (forall chunk, access_mode ty = By_value chunk -> + exists gv, Genv.find_var_info tge l = Some gv /\ gvar_info gv = Vscalar chunk). +Proof. + intros. + case_eq (te!id). intros [b' vk] EQ. + exploit me_local_inv; eauto. intros [ty' EQ']. congruence. + intros. split; auto; intros. + revert H2; unfold type_of_global. + case_eq (Genv.find_var_info ge l). intros. inv H5. + exploit var_info_translated; eauto. intros [gv [A B]]. monadInv B. unfold transl_globvar in EQ. + econstructor; split. eauto. simpl. + exploit var_kind_by_value; eauto. congruence. + intros. destruct (Genv.find_funct_ptr ge l); intros; inv H5. + destruct f; simpl in H4; discriminate. +Qed. + +Lemma match_env_same_blocks: + forall e te, + match_env e te -> + blocks_of_env te = Csem.blocks_of_env e. +Proof. + intros. + set (R := fun (x: (block * type)) (y: (block * var_kind)) => + match x, y with + | (b1, ty), (b2, vk) => b2 = b1 /\ var_kind_of_type ty = OK vk + 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. exploit me_local; eauto. intros [vk [A B]]. + exists (b, vk); split; auto. red. auto. + intros id [b vk] GET. + exploit me_local_inv; eauto. intros [ty A]. + exploit me_local; eauto. intros [vk' [B C]]. + assert (vk' = vk) by congruence. subst vk'. + exists (b, ty); split; auto. red. auto. + + unfold blocks_of_env, Csem.blocks_of_env. + generalize H0. induction 1. auto. + simpl. f_equal; auto. + unfold block_of_binding, Csem.block_of_binding. + destruct a1 as [id1 [blk1 ty1]]. destruct b1 as [id2 [blk2 vk2]]. + simpl in *. destruct H1 as [A [B C]]. subst blk2 id2. f_equal. + apply sizeof_var_kind_of_type. auto. +Qed. + +Lemma match_env_free_blocks: + forall e te m m', + match_env e te -> + Mem.free_list m (Csem.blocks_of_env e) = Some m' -> + Mem.free_list m (blocks_of_env te) = Some m'. +Proof. + intros. rewrite (match_env_same_blocks _ _ H). auto. +Qed. + +Lemma match_env_empty: + match_env Clight.empty_env Csharpminor.empty_env. +Proof. + unfold Clight.empty_env, Csharpminor.empty_env. + constructor. + intros until b. repeat rewrite PTree.gempty. congruence. + intros until vk. rewrite PTree.gempty. congruence. +Qed. + +(** The following lemmas establish the [match_env] invariant at + the beginning of a function invocation, after allocation of + local variables and initialization of the parameters. *) + +Lemma match_env_alloc_variables: + forall e1 m1 vars e2 m2, + Csem.alloc_variables e1 m1 vars e2 m2 -> + forall te1 tvars, + match_env e1 te1 -> + transl_vars vars = OK tvars -> + exists te2, + Csharpminor.alloc_variables te1 m1 tvars te2 m2 + /\ match_env e2 te2. +Proof. + induction 1; intros. + monadInv H0. + exists te1; split. constructor. auto. + generalize H2. simpl. + caseEq (var_kind_of_type ty); simpl; [intros vk VK | congruence]. + caseEq (transl_vars vars); simpl; [intros tvrs TVARS | congruence]. + intro EQ; inversion EQ; subst tvars; clear EQ. + set (te2 := PTree.set id (b1, vk) te1). + assert (match_env (PTree.set id (b1, ty) e) te2). + inversion H1. unfold te2. constructor. + (* me_local *) + intros until ty0. simpl. repeat rewrite PTree.gsspec. + destruct (peq id0 id); intros. + inv H3. exists vk; intuition. + auto. + (* me_local_inv *) + intros until vk0. repeat rewrite PTree.gsspec. + destruct (peq id0 id); intros. exists ty; congruence. eauto. + destruct (IHalloc_variables _ _ H3 TVARS) as [te3 [ALLOC MENV]]. + exists te3; split. + econstructor; eauto. + rewrite (sizeof_var_kind_of_type _ _ VK). eauto. + auto. +Qed. + +Lemma bind_parameters_match: + forall e m1 vars vals m2, + Csem.bind_parameters e m1 vars vals m2 -> + forall te tvars, + val_casted_list vals (type_of_params vars) -> + match_env e te -> + transl_params vars = OK tvars -> + Csharpminor.bind_parameters te m1 tvars vals m2. +Proof. + induction 1; intros. +(* base case *) + monadInv H1. constructor. +(* inductive case *) + simpl in H2. destruct H2. + revert H4; simpl. + caseEq (chunk_of_type ty); simpl; [intros chunk CHK | congruence]. + caseEq (transl_params params); simpl; [intros tparams TPARAMS | congruence]. + intro EQ; inversion EQ; clear EQ; subst tvars. + generalize CHK. unfold chunk_of_type. + caseEq (access_mode ty); intros; try discriminate. + inversion CHK0; clear CHK0; subst m0. + unfold store_value_of_type in H0. rewrite H4 in H0. + apply bind_parameters_cons with b m1. + exploit me_local; eauto. intros [vk [A B]]. + exploit var_kind_by_value; eauto. congruence. + eapply val_casted_normalized; eauto. + assumption. + apply IHbind_parameters; auto. +Qed. + +(* ** Correctness of variable accessors *) + +(** Correctness of the code generated by [var_get]. *) + +Lemma var_get_correct: + forall e le m id ty loc ofs v code te, + Clight.eval_lvalue ge e le m (Clight.Evar id ty) loc ofs -> + load_value_of_type ty m loc ofs = Some v -> + var_get id ty = OK code -> + match_env e te -> + eval_expr tge te le m code v. +Proof. + intros. revert H0 H1. unfold load_value_of_type, var_get. + case_eq (access_mode ty). + (* access mode By_value *) + intros chunk ACC LOAD EQ. inv EQ. + inv H. + (* local variable *) + exploit me_local; eauto. intros [vk [A B]]. + assert (vk = Vscalar chunk). + exploit var_kind_by_value; eauto. congruence. + subst vk. + eapply eval_Evar. + eapply eval_var_ref_local. eauto. assumption. + (* global variable *) + exploit match_env_globals; eauto. intros [A B]. + exploit B; eauto. intros [gv [C D]]. + eapply eval_Evar. + eapply eval_var_ref_global. auto. + rewrite symbols_preserved. eauto. + eauto. eauto. + assumption. + (* access mode By_reference *) + intros ACC EQ1 EQ2. inv EQ1; inv EQ2; inv H. + (* local variable *) + exploit me_local; eauto. intros [vk [A B]]. + eapply eval_Eaddrof. + eapply eval_var_addr_local. eauto. + (* global variable *) + exploit match_env_globals; eauto. intros [A B]. + eapply eval_Eaddrof. + eapply eval_var_addr_global. auto. + rewrite symbols_preserved. eauto. + (* access mode By_nothing *) + congruence. +Qed. + +(** Correctness of the code generated by [var_set]. *) + +Lemma var_set_correct: + forall e le m id ty loc ofs v m' code te rhs f k, + Clight.eval_lvalue ge e le m (Clight.Evar id ty) loc ofs -> + val_casted v ty -> + store_value_of_type ty m loc ofs v = Some m' -> + var_set id ty rhs = OK code -> + match_env e te -> + eval_expr tge te le m rhs v -> + step tge (State f code k te le m) E0 (State f Sskip k te le m'). +Proof. + intros. revert H1 H2. unfold store_value_of_type, var_set. + caseEq (access_mode ty). + (* access mode By_value *) + intros chunk ACC STORE EQ. inv EQ. + inv H. + (* local variable *) + exploit me_local; eauto. intros [vk [A B]]. + assert (vk = Vscalar chunk). + exploit var_kind_by_value; eauto. congruence. + subst vk. + eapply step_assign. eauto. + econstructor. eapply eval_var_ref_local. eauto. + eapply val_casted_normalized; eauto. assumption. + (* global variable *) + exploit match_env_globals; eauto. intros [A B]. + exploit B; eauto. intros [gv [C D]]. + eapply step_assign. eauto. + econstructor. eapply eval_var_ref_global. auto. + rewrite symbols_preserved. eauto. + eauto. eauto. + eapply val_casted_normalized; eauto. assumption. + (* access mode By_reference *) + congruence. + (* access mode By_nothing *) + congruence. +Qed. + +(**************************** +Lemma call_dest_correct: + forall e m lhs loc ofs optid te, + Csem.eval_lvalue ge e m lhs loc ofs -> + transl_lhs_call (Some lhs) = OK optid -> + match_env e te -> + exists id, + optid = Some id + /\ ofs = Int.zero + /\ match access_mode (typeof lhs) with + | By_value chunk => eval_var_ref tge te id loc chunk + | _ => True + end. +Proof. + intros. revert H0. simpl. caseEq (is_variable lhs); try congruence. + intros id ISV EQ. inv EQ. + exploit is_variable_correct; eauto. intro EQ. + rewrite EQ in H. clear EQ. + exists id. split; auto. + inv H. +(* local variable *) + split. auto. + exploit me_local; eauto. intros [vk [A B]]. + case_eq (access_mode (typeof lhs)); intros; auto. + assert (vk = Vscalar m0). + exploit var_kind_by_value; eauto. congruence. + subst vk. apply eval_var_ref_local; auto. +(* global variable *) + split. auto. + exploit match_env_globals; eauto. intros [A B]. + case_eq (access_mode (typeof lhs)); intros; auto. + exploit B; eauto. intros [gv [C D]]. + eapply eval_var_ref_global; eauto. + rewrite symbols_preserved. auto. +Qed. + +Lemma set_call_dest_correct: + forall ty m loc v m' e te id, + store_value_of_type ty m loc Int.zero v = Some m' -> + match access_mode ty with + | By_value chunk => eval_var_ref tge te id loc chunk + | _ => True + end -> + match_env e te -> + exec_opt_assign tge te m (Some id) v m'. +Proof. + intros. generalize H. unfold store_value_of_type. case_eq (access_mode ty); intros; try congruence. + rewrite H2 in H0. + constructor. econstructor. eauto. auto. +Qed. +**************************) + +(** * Proof of semantic preservation *) + +(** ** Semantic preservation for expressions *) + +(** The proof of semantic preservation for the translation of expressions + relies on simulation diagrams of the following form: +<< + e, le, m, a ------------------- te, le, m, ta + | | + | | + | | + v v + e, le, m, v ------------------- te, le, m, v +>> + Left: evaluation of r-value expression [a] in Clight. + Right: evaluation of its translation [ta] in Csharpminor. + Top (precondition): matching between environments [e], [te], + plus well-typedness of expression [a]. + Bottom (postcondition): the result values [v] + are identical in both evaluations. + + We state these diagrams as the following properties, parameterized + by the Clight evaluation. *) + +Section EXPR. + +Variable e: Clight.env. +Variable le: temp_env. +Variable m: mem. +Variable te: Csharpminor.env. +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 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 a = OK ta), + Csharpminor.eval_expr tge te le m ta (Vptr b ofs)). +Proof. + apply eval_expr_lvalue_ind; intros; try (monadInv TR). +(* const int *) + apply make_intconst_correct. +(* const float *) + apply make_floatconst_correct. +(* temp var *) + constructor; auto. +(* addrof *) + simpl in TR. auto. +(* sizeof *) + constructor; auto. +(* unop *) + eapply transl_unop_correct; eauto. +(* binop *) + eapply transl_binop_correct; eauto. +(* condition true *) + exploit make_boolean_correct_true. eapply H0; eauto. eauto. + intros [vb [EVAL ISTRUE]]. + eapply eval_Econdition; eauto. apply Val.bool_of_true_val; eauto. + simpl. eauto. +(* condition false *) + exploit make_boolean_correct_false. eapply H0; eauto. eauto. + intros [vb [EVAL ISFALSE]]. + eapply eval_Econdition; eauto. apply Val.bool_of_false_val; eauto. + simpl. eauto. +(* cast *) + eapply make_cast_correct; eauto. +(* rvalue out of lvalue *) + exploit transl_expr_lvalue; eauto. + intros [[id [ty [EQ VARGET]]] | [tb [TRLVAL MKLOAD]]]. + (* Case a is a variable *) + subst a. eapply var_get_correct; eauto. + (* Case a is another lvalue *) + eapply make_load_correct; eauto. +(* var local *) + exploit (me_local _ _ MENV); eauto. + intros [vk [A B]]. + econstructor. eapply eval_var_addr_local. eauto. +(* var global *) + exploit match_env_globals; eauto. intros [A B]. + econstructor. eapply eval_var_addr_global. eauto. + rewrite symbols_preserved. auto. +(* deref *) + simpl in TR. eauto. +(* field struct *) + simpl in TR. rewrite H1 in TR. monadInv TR. + eapply eval_Ebinop; eauto. + apply make_intconst_correct. + simpl. congruence. +(* field union *) + simpl in TR. rewrite H1 in TR. eauto. +Qed. + +Lemma transl_expr_correct: + forall a v, + Clight.eval_expr ge e le m a v -> + forall ta, transl_expr 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 a = OK ta -> + Csharpminor.eval_expr tge te le m ta (Vptr b ofs). +Proof (proj2 transl_expr_lvalue_correct). + +Lemma transl_exprlist_correct: + forall al tyl vl, + Clight.eval_exprlist ge e le m al tyl vl -> + forall tal, transl_exprlist al tyl = OK tal -> + Csharpminor.eval_exprlist tge te le m tal vl. +Proof. + induction 1; intros. + monadInv H. constructor. + monadInv H2. constructor. + eapply make_cast_correct. eapply transl_expr_correct; eauto. auto. + eauto. +Qed. + +End EXPR. + +Lemma exit_if_false_true: + forall a ts e le m v te f tk, + exit_if_false a = OK ts -> + Clight.eval_expr ge e le m a v -> + is_true v (typeof a) -> + match_env e te -> + step tge (State f ts tk te le m) E0 (State f Sskip tk te le m). +Proof. + intros. monadInv H. + exploit make_boolean_correct_true. + eapply (transl_expr_correct _ _ _ _ H2 _ _ H0); eauto. + eauto. + intros [vb [EVAL ISTRUE]]. + change Sskip with (if true then Sskip else Sexit 0). + eapply step_ifthenelse; eauto. + apply Val.bool_of_true_val; eauto. +Qed. + +Lemma exit_if_false_false: + forall a ts e le m v te f tk, + exit_if_false a = OK ts -> + Clight.eval_expr ge e le m a v -> + is_false v (typeof a) -> + match_env e te -> + step tge (State f ts tk te le m) E0 (State f (Sexit 0) tk te le m). +Proof. + intros. monadInv H. + exploit make_boolean_correct_false. + eapply (transl_expr_correct _ _ _ _ H2 _ _ H0); eauto. + eauto. + intros [vb [EVAL ISFALSE]]. + change (Sexit 0) with (if false then Sskip else Sexit 0). + eapply step_ifthenelse; eauto. + apply Val.bool_of_false_val; eauto. +Qed. + +(** ** Semantic preservation for statements *) + +(** The simulation diagram for the translation of statements and functions + is a "plus" diagram of the form +<< + I + S1 ------- R1 + | | + t | + | t + v v + S2 ------- R2 + I I +>> + +The invariant [I] is the [match_states] predicate that we now define. +*) + +Inductive match_transl: stmt -> cont -> stmt -> cont -> Prop := + | match_transl_0: forall ts tk, + match_transl ts tk ts tk + | match_transl_1: forall ts tk, + match_transl (Sblock ts) tk ts (Kblock tk). + +Lemma match_transl_step: + forall ts tk ts' tk' f te le m, + match_transl (Sblock ts) tk ts' tk' -> + star step tge (State f ts' tk' te le m) E0 (State f ts (Kblock tk) te le m). +Proof. + intros. inv H. + apply star_one. constructor. + 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 tyret nbrk ncnt s = OK ts -> + match_cont tyret nbrk ncnt k tk -> + match_cont tyret nbrk ncnt + (Clight.Kseq s k) + (Kseq ts tk) + | match_Kwhile: forall tyret nbrk ncnt a s k ta ts tk, + exit_if_false a = OK ta -> + transl_statement tyret 1%nat 0%nat s = OK ts -> + match_cont tyret nbrk ncnt k tk -> + match_cont tyret 1%nat 0%nat + (Clight.Kwhile a s k) + (Kblock (Kseq (Sloop (Sseq ta (Sblock ts))) (Kblock tk))) + | match_Kdowhile: forall tyret nbrk ncnt a s k ta ts tk, + exit_if_false a = OK ta -> + transl_statement tyret 1%nat 0%nat s = OK ts -> + match_cont tyret nbrk ncnt k tk -> + match_cont tyret 1%nat 0%nat + (Clight.Kdowhile a s k) + (Kblock (Kseq ta (Kseq (Sloop (Sseq (Sblock ts) ta)) (Kblock tk)))) + | match_Kfor2: forall tyret nbrk ncnt a2 a3 s k ta2 ta3 ts tk, + exit_if_false a2 = OK ta2 -> + transl_statement tyret 0%nat (S ncnt) a3 = OK ta3 -> + transl_statement tyret 1%nat 0%nat s = OK ts -> + match_cont tyret nbrk ncnt k tk -> + match_cont tyret 1%nat 0%nat + (Clight.Kfor2 a2 a3 s k) + (Kblock (Kseq ta3 (Kseq (Sloop (Sseq ta2 (Sseq (Sblock ts) ta3))) (Kblock tk)))) + | match_Kfor3: forall tyret nbrk ncnt a2 a3 s k ta2 ta3 ts tk, + exit_if_false a2 = OK ta2 -> + transl_statement tyret 0%nat (S ncnt) a3 = OK ta3 -> + transl_statement tyret 1%nat 0%nat s = OK ts -> + match_cont tyret nbrk ncnt k tk -> + match_cont tyret 0%nat (S ncnt) + (Clight.Kfor3 a2 a3 s k) + (Kseq (Sloop (Sseq ta2 (Sseq (Sblock ts) ta3))) (Kblock tk)) + | match_Kswitch: forall tyret nbrk ncnt k tk, + match_cont tyret nbrk ncnt k tk -> + match_cont 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 f = OK tf -> + match_env e te -> + match_cont (Clight.fn_return f) nbrk' ncnt' k tk -> + match_cont 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 f = OK tf) + (TR: transl_statement (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), + 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 + (TR: transl_fundef fd = OK tfd) + (MK: match_cont Tvoid 0%nat 0%nat k tk) + (ISCC: Clight.is_call_cont k) + (TY: type_of_fundef fd = Tfunction targs tres) + (VCAST: val_casted_list args targs), + 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), + 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 f = OK tf -> + match_env e te -> + match_cont (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. +Qed. + +(** Commutation between label resolution and compilation *) + +Section FIND_LABEL. +Variable lbl: label. +Variable tyret: type. + +Remark exit_if_false_no_label: + forall a s, exit_if_false a = OK s -> forall k, find_label lbl s k = None. +Proof. + intros. unfold exit_if_false in H. monadInv H. simpl. auto. +Qed. + +Lemma transl_find_label: + forall s nbrk ncnt k ts tk + (TR: transl_statement tyret nbrk ncnt s = OK ts) + (MC: match_cont 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 tyret nbrk' ncnt' s' = OK ts' + /\ match_cont tyret nbrk' ncnt' k' tk' + end + +with transl_find_label_ls: + forall ls nbrk ncnt k tls tk + (TR: transl_lbl_stmt tyret nbrk ncnt ls = OK tls) + (MC: match_cont 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 tyret nbrk' ncnt' s' = OK ts' + /\ match_cont tyret nbrk' ncnt' k' tk' + end. + +Proof. + intro s; case s; intros; try (monadInv TR); simpl. +(* skip *) + auto. +(* assign *) + simpl in TR. destruct (is_variable e); monadInv TR. + unfold var_set in EQ0. destruct (access_mode (typeof e)); inv EQ0. auto. + unfold make_store in EQ2. destruct (access_mode (typeof e)); inv EQ2. auto. +(* set *) + auto. +(* call *) + simpl in TR. destruct (classify_fun (typeof e)); monadInv TR. auto. +(* 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 *) + 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. +(* while *) + rewrite (exit_if_false_no_label _ _ EQ). + eapply transl_find_label; eauto. econstructor; eauto. +(* dowhile *) + exploit (transl_find_label s0 1%nat 0%nat (Clight.Kdowhile e s0 k)); eauto. econstructor; eauto. + destruct (Clight.find_label lbl s0 (Kdowhile e 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 exit_if_false_no_label; eauto. +(* for *) + rewrite (exit_if_false_no_label _ _ EQ). + exploit (transl_find_label s1 1%nat 0%nat (Kfor2 e s0 s1 k)); eauto. econstructor; eauto. + destruct (Clight.find_label lbl s1 (Kfor2 e 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 *) + auto. +(* continue *) + auto. +(* return *) + simpl in TR. destruct o; monadInv TR. auto. auto. +(* switch *) + eapply transl_find_label_ls with (k := Clight.Kswitch k); eauto. econstructor; eauto. +(* label *) + destruct (ident_eq lbl l). + exists x; exists tk; exists nbrk; exists ncnt; auto. + eapply transl_find_label; eauto. +(* goto *) + auto. + + intro ls; case ls; intros; monadInv TR; simpl. +(* default *) + eapply transl_find_label; eauto. +(* case *) + 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'] | ]. + 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_ls; eauto. +Qed. + +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). +Proof. + induction 1; simpl; auto. + constructor. + econstructor; eauto. +Qed. + +Lemma match_cont_is_call_cont: + forall tyret nbrk ncnt k tk tyret' nbrk' ncnt', + match_cont tyret nbrk ncnt k tk -> + Clight.is_call_cont k -> + match_cont tyret' nbrk' ncnt' k tk /\ is_call_cont tk. +Proof. + intros. inv H; simpl in H0; try contradiction; simpl. + split; auto; constructor. + split; auto; econstructor; eauto. +Qed. + +(** The simulation proof *) + +Lemma transl_step: + forall S1 t S2, Clight.step ge S1 t S2 -> + forall T1, match_states S1 T1 -> + exists T2, plus step tge T1 t T2 /\ match_states S2 T2. +Proof. + induction 1; intros T1 MST; inv MST. + +(* assign *) + revert TR. simpl. case_eq (is_variable a1); intros; monadInv TR. + exploit is_variable_correct; eauto. intro EQ1. rewrite EQ1 in H. + assert (ts' = ts /\ tk' = tk). + inversion MTR. auto. + subst ts. unfold var_set in EQ0. destruct (access_mode (typeof a1)); congruence. + destruct H4; subst ts' tk'. + econstructor; split. + apply plus_one. eapply var_set_correct; eauto. exists v2; exists (typeof a2); auto. + eapply make_cast_correct; eauto. eapply transl_expr_correct; eauto. + eapply match_states_skip; eauto. + + assert (ts' = ts /\ tk' = tk). + inversion MTR. auto. + subst ts. unfold make_store in EQ2. destruct (access_mode (typeof a1)); congruence. + destruct H4; subst ts' tk'. + econstructor; split. + apply plus_one. eapply make_store_correct; eauto. + exploit transl_lvalue_correct; eauto. + eapply make_cast_correct; eauto. eapply transl_expr_correct; eauto. + eapply match_states_skip; eauto. + +(* set *) + monadInv TR. inv MTR. econstructor; split. + apply plus_one. econstructor. eapply transl_expr_correct; eauto. + eapply match_states_skip; eauto. + +(* call *) + revert TR. simpl. case_eq (classify_fun (typeof a)); try congruence. + intros targs tres CF TR. monadInv TR. inv MTR. + exploit functions_translated; eauto. intros [tfd [FIND TFD]]. + rewrite H in CF. simpl in CF. inv CF. + econstructor; split. + apply plus_one. econstructor; eauto. + exploit transl_expr_correct; eauto. + exploit transl_exprlist_correct; eauto. + eapply transl_fundef_sig1; eauto. + rewrite H3. rewrite H. auto. + econstructor; eauto. + econstructor; eauto. + simpl. auto. + rewrite H3; rewrite H; eauto. + eapply eval_exprlist_casted; eauto. + +(* seq *) + monadInv TR. inv MTR. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. constructor. + econstructor; eauto. + +(* skip seq *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + apply plus_one. apply step_skip_seq. + econstructor; eauto. constructor. + +(* continue seq *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. simpl. reflexivity. constructor. + +(* break seq *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. simpl. reflexivity. constructor. + +(* ifthenelse true *) + monadInv TR. inv MTR. + exploit make_boolean_correct_true; eauto. + exploit transl_expr_correct; eauto. + intros [v [A B]]. + econstructor; split. + apply plus_one. apply step_ifthenelse with (v := v) (b := true). + auto. apply Val.bool_of_true_val. auto. + econstructor; eauto. constructor. + +(* ifthenelse false *) + monadInv TR. inv MTR. + exploit make_boolean_correct_false; eauto. + exploit transl_expr_correct; eauto. + intros [v [A B]]. + econstructor; split. + apply plus_one. apply step_ifthenelse with (v := v) (b := false). + auto. apply Val.bool_of_false_val. auto. + econstructor; eauto. constructor. + +(* while false *) + monadInv TR. + econstructor; split. + eapply star_plus_trans. eapply match_transl_step; eauto. + eapply plus_left. constructor. + eapply star_left. constructor. + eapply star_left. eapply exit_if_false_false; eauto. + eapply star_left. constructor. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. traceEq. + eapply match_states_skip; eauto. + +(* while true *) + monadInv TR. + econstructor; split. + eapply star_plus_trans. eapply match_transl_step; eauto. + eapply plus_left. constructor. + eapply star_left. constructor. + eapply star_left. eapply exit_if_false_true; eauto. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. reflexivity. reflexivity. reflexivity. traceEq. + econstructor; eauto. constructor. + econstructor; eauto. + +(* skip or continue while *) + assert ((ts' = Sskip \/ ts' = Sexit ncnt) /\ tk' = tk). + destruct H; subst x; monadInv TR; inv MTR; auto. + destruct H0. inv MK. + econstructor; split. + eapply plus_left. + destruct H0; subst ts'; constructor. + apply star_one. constructor. traceEq. + econstructor; eauto. + simpl. rewrite H8; simpl. rewrite H10; simpl. reflexivity. + constructor. + +(* break while *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + eapply plus_left. constructor. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. traceEq. + eapply match_states_skip; eauto. + +(* dowhile *) + monadInv TR. + econstructor; split. + eapply star_plus_trans. eapply match_transl_step; eauto. + eapply plus_left. constructor. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. reflexivity. traceEq. + econstructor; eauto. constructor. + econstructor; eauto. + +(* skip or continue dowhile false *) + assert ((ts' = Sskip \/ ts' = Sexit ncnt) /\ tk' = tk). + destruct H; subst x; monadInv TR; inv MTR; auto. + destruct H2. inv MK. + econstructor; split. + eapply plus_left. destruct H2; subst ts'; constructor. + eapply star_left. constructor. + eapply star_left. eapply exit_if_false_false; eauto. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. reflexivity. reflexivity. traceEq. + eapply match_states_skip; eauto. + +(* skip or continue dowhile true *) + assert ((ts' = Sskip \/ ts' = Sexit ncnt) /\ tk' = tk). + destruct H; subst x; monadInv TR; inv MTR; auto. + destruct H2. inv MK. + econstructor; split. + eapply plus_left. destruct H2; subst ts'; constructor. + eapply star_left. constructor. + eapply star_left. eapply exit_if_false_true; eauto. + apply star_one. constructor. + reflexivity. reflexivity. traceEq. + econstructor; eauto. + simpl. rewrite H10; simpl. rewrite H12; simpl. reflexivity. constructor. + +(* break dowhile *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + eapply plus_left. constructor. + eapply star_left. constructor. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. reflexivity. traceEq. + eapply match_states_skip; eauto. + +(* for false *) + monadInv TR. + econstructor; split. + eapply star_plus_trans. eapply match_transl_step; eauto. + eapply plus_left. constructor. + eapply star_left. constructor. + eapply star_left. eapply exit_if_false_false; eauto. + eapply star_left. constructor. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. + eapply match_states_skip; eauto. + +(* for true *) + monadInv TR. + econstructor; split. + eapply star_plus_trans. eapply match_transl_step; eauto. + eapply plus_left. constructor. + eapply star_left. constructor. + eapply star_left. eapply exit_if_false_true; eauto. + eapply star_left. constructor. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. + econstructor; eauto. constructor. + econstructor; eauto. + +(* skip or continue for2 *) + assert ((ts' = Sskip \/ ts' = Sexit ncnt) /\ tk' = tk). + destruct H; subst x; monadInv TR; inv MTR; auto. + destruct H0. inv MK. + econstructor; split. + eapply plus_left. destruct H0; subst ts'; constructor. + apply star_one. constructor. reflexivity. + econstructor; eauto. constructor. + econstructor; eauto. + +(* break for2 *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + eapply plus_left. constructor. + eapply star_left. constructor. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. reflexivity. traceEq. + eapply match_states_skip; eauto. + +(* skip for3 *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. + simpl. rewrite H6; simpl. rewrite H8; simpl. rewrite H9; simpl. reflexivity. + constructor. + +(* break for3 *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + eapply plus_left. constructor. apply star_one. constructor. + econstructor; eauto. + eapply match_states_skip; eauto. + +(* return none *) + monadInv TR. inv MTR. + econstructor; split. + apply plus_one. constructor. monadInv TRF. simpl. rewrite H. auto. + eapply match_env_free_blocks; eauto. + econstructor; eauto. + eapply match_cont_call_cont. eauto. + +(* return some *) + monadInv TR. inv MTR. + econstructor; split. + apply plus_one. constructor. monadInv TRF. simpl. + unfold opttyp_of_type. destruct (Clight.fn_return f); try congruence. + inv H0. inv H3. inv H3. + eapply make_cast_correct. eapply transl_expr_correct; eauto. eauto. + eapply match_env_free_blocks; eauto. + econstructor; eauto. + eapply match_cont_call_cont. eauto. + +(* 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. + monadInv TRF. simpl. rewrite H0. auto. + eapply match_env_free_blocks; eauto. + constructor. eauto. + +(* switch *) + monadInv TR. + exploit transl_expr_correct; eauto. intro EV. + econstructor; split. + eapply star_plus_trans. eapply match_transl_step; eauto. + apply plus_one. econstructor. eauto. traceEq. + econstructor; eauto. + apply transl_lbl_stmt_2. apply transl_lbl_stmt_1. eauto. + constructor. + econstructor. eauto. + +(* 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. + econstructor; split. + apply plus_one. destruct H0; subst ts'; constructor. + eapply match_states_skip; eauto. + + +(* continue switch *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. simpl. reflexivity. constructor. + +(* label *) + monadInv TR. inv MTR. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. constructor. + +(* goto *) + monadInv TR. inv MTR. + generalize TRF. unfold transl_function. intro TRF'. monadInv TRF'. + exploit (transl_find_label lbl). eexact EQ0. 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 *) + monadInv TR. monadInv EQ. + exploit match_cont_is_call_cont; eauto. intros [A B]. + exploit match_env_alloc_variables; eauto. + apply match_env_empty. + apply transl_fn_variables. eauto. eauto. + intros [te1 [C D]]. + econstructor; split. + apply plus_one. econstructor. + eapply transl_names_norepet; eauto. + eexact C. eapply bind_parameters_match; eauto. + simpl in TY. unfold type_of_function in TY. congruence. + econstructor; eauto. + unfold transl_function. rewrite EQ0; simpl. rewrite EQ; simpl. rewrite EQ1; auto. + constructor. + +(* external function *) + simpl in TR. + destruct (list_typ_eq (sig_args (ef_sig ef)) (typlist_of_typelist targs) && + opt_typ_eq (sig_res (ef_sig ef)) (opttyp_of_type tres)); + monadInv TR. + exploit match_cont_is_call_cont; eauto. intros [A B]. + econstructor; split. + apply plus_one. constructor. eauto. + eapply external_call_symbols_preserved_2; eauto. + exact symbols_preserved. + eexact (Genv.find_var_info_transf_partial2 transl_fundef transl_globvar _ TRANSL). + eexact (Genv.find_var_info_rev_transf_partial2 transl_fundef transl_globvar _ TRANSL). + econstructor; eauto. + +(* returnstate *) + inv MK. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. simpl; reflexivity. constructor. + inv MK. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. simpl; reflexivity. constructor. +Qed. + +Lemma transl_initial_states: + forall S t S', Clight.initial_state prog S -> Clight.step ge S t S' -> + 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 (prog_main tprog) = Some b). + rewrite symbols_preserved. replace (prog_main tprog) with (prog_main prog). + exact H2. symmetry. unfold transl_program in TRANSL. + eapply transform_partial_program2_main; eauto. + assert (funsig tf = signature_of_type Tnil (Tint I32 Signed)). + eapply transl_fundef_sig2; eauto. + econstructor; split. + econstructor; eauto. eapply Genv.init_mem_transf_partial2; eauto. + econstructor; eauto. constructor; auto. exact I. red; auto. +Qed. + +Lemma transl_final_states: + forall S R r, + match_states S R -> Clight.final_state S r -> final_state R r. +Proof. + intros. inv H0. inv H. inv MK. constructor. +Qed. + +Theorem transl_program_correct: + forall (beh: program_behavior), + not_wrong beh -> Clight.exec_program prog beh -> + Csharpminor.exec_program tprog beh. +Proof. + set (order := fun (S1 S2: Clight.state) => False). + assert (WF: well_founded order). + unfold order; red. intros. constructor; intros. contradiction. + assert (transl_step': + forall S1 t S2, Clight.step ge S1 t S2 -> + forall T1, match_states S1 T1 -> + exists T2, + (plus step tge T1 t T2 \/ star step tge T1 t T2 /\ order S2 S1) + /\ match_states S2 T2). + intros. exploit transl_step; eauto. intros [T2 [A B]]. + exists T2; split. auto. auto. + intros. inv H0. +(* Terminates *) + assert (exists t1, exists s1, Clight.step (Genv.globalenv prog) s t1 s1). + inv H3. inv H2. inv H1. exists t1; exists s2; auto. + destruct H0 as [t1 [s1 ST]]. + exploit transl_initial_states; eauto. intros [R [A B]]. + exploit simulation_star_star; eauto. intros [R' [C D]]. + econstructor; eauto. eapply transl_final_states; eauto. +(* Diverges *) + assert (exists t1, exists s1, Clight.step (Genv.globalenv prog) s t1 s1). + inv H2. inv H3. exists E0; exists s2; auto. exists t1; exists s2; auto. + destruct H0 as [t1 [s1 ST]]. + exploit transl_initial_states; eauto. intros [R [A B]]. + exploit simulation_star_star; eauto. intros [R' [C D]]. + econstructor; eauto. eapply simulation_star_forever_silent; eauto. +(* Reacts *) + assert (exists t1, exists s1, Clight.step (Genv.globalenv prog) s t1 s1). + inv H2. inv H0. congruence. exists t1; exists s0; auto. + destruct H0 as [t1 [s1 ST]]. + exploit transl_initial_states; eauto. intros [R [A B]]. + exploit simulation_star_forever_reactive; eauto. + intro C. + econstructor; eauto. +(* Goes wrong *) + contradiction. contradiction. +Qed. + +End CORRECTNESS. -- cgit v1.2.3