(* *********************************************************************) (* *) (* 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 Errors Maps Integers Floats. Require Import AST Linking. Require Import Values Events Memory Globalenvs Smallstep. Require Import Ctypes Ctyping 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: forall params, map typ_of_type (map snd params) = typlist_of_typelist (type_of_params params). Proof. induction params; simpl. auto. destruct a as [id ty]; simpl. f_equal; auto. Qed. Lemma transl_fundef_sig1: forall ce f tf args res cc, 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. inv H. - monadInv H1. simpl. inversion H0. unfold signature_of_function, signature_of_type. f_equal. apply transl_params_types. - simpl in H0. unfold funsig. congruence. Qed. Lemma transl_fundef_sig2: forall ce f tf args res cc, match_fundef ce f tf -> type_of_fundef f = Tfunction args res cc -> funsig tf = signature_of_type args res cc. Proof. intros. eapply transl_fundef_sig1; eauto. 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 union_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 /\ union_field_offset prog.(prog_comp_env) f (co_members co) = union_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. apply Ctypes.union_field_offset_stable; eauto using co_consistent_complete. 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. apply Ctypes.field_offset_stable; eauto using co_consistent_complete. Qed. (** * Properties of the translation functions *) (** Properties of labeled statements *) Lemma transl_lbl_stmt_1: forall ce tyret nbrk ncnt n sl tsl, transl_lbl_stmt ce tyret nbrk ncnt sl = OK tsl -> transl_lbl_stmt ce tyret nbrk ncnt (Clight.select_switch n sl) = OK (select_switch n tsl). Proof. intros until n. assert (DFL: forall sl tsl, transl_lbl_stmt ce tyret nbrk ncnt sl = OK tsl -> transl_lbl_stmt ce tyret nbrk ncnt (Clight.select_switch_default sl) = OK (select_switch_default tsl)). { induction sl; simpl; intros. inv H; auto. monadInv H. simpl. destruct o; eauto. simpl; rewrite EQ; simpl; rewrite EQ1; auto. } assert (CASE: forall sl tsl, transl_lbl_stmt ce tyret nbrk ncnt sl = OK tsl -> match Clight.select_switch_case n sl with | None => select_switch_case n tsl = None | Some sl' => exists tsl', select_switch_case n tsl = Some tsl' /\ transl_lbl_stmt ce tyret nbrk ncnt sl' = OK tsl' end). { induction sl; simpl; intros. inv H; auto. monadInv H; simpl. destruct o. destruct (zeq z n). econstructor; split; eauto. simpl; rewrite EQ; simpl; rewrite EQ1; auto. apply IHsl; auto. apply IHsl; auto. } intros. specialize (CASE _ _ H). unfold Clight.select_switch, select_switch. destruct (Clight.select_switch_case n sl) as [sl'|]. destruct CASE as [tsl' [P Q]]. rewrite P, Q. auto. rewrite CASE. auto. Qed. Lemma transl_lbl_stmt_2: forall ce tyret nbrk ncnt sl tsl, transl_lbl_stmt ce tyret nbrk ncnt sl = OK tsl -> transl_statement ce tyret nbrk ncnt (seq_of_labeled_statement sl) = OK (seq_of_lbl_stmt tsl). Proof. induction sl; intros. monadInv H. auto. monadInv H. simpl. rewrite EQ; simpl. rewrite (IHsl _ EQ1). simpl. auto. Qed. (** * Correctness of Csharpminor construction functions *) Section CONSTRUCTORS. Variables cunit prog: Clight.program. Hypothesis LINK: linkorder cunit prog. 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_singleconst_correct: forall n e le m, eval_expr ge e le m (make_singleconst n) (Vsingle n). Proof. intros. unfold make_singleconst. econstructor. reflexivity. Qed. Lemma make_longconst_correct: forall n e le m, eval_expr ge e le m (make_longconst n) (Vlong n). Proof. intros. unfold make_floatconst. econstructor. reflexivity. Qed. Lemma make_ptrofsconst_correct: forall n e le m, eval_expr ge e le m (make_ptrofsconst n) (Vptrofs (Ptrofs.repr n)). Proof. intros. unfold Vptrofs, make_ptrofsconst. destruct Archi.ptr64 eqn:SF. - replace (Ptrofs.to_int64 (Ptrofs.repr n)) with (Int64.repr n). apply make_longconst_correct. symmetry; auto with ptrofs. - replace (Ptrofs.to_int (Ptrofs.repr n)) with (Int.repr n). apply make_intconst_correct. symmetry; auto with ptrofs. Qed. Lemma make_singleoffloat_correct: forall a n e le m, eval_expr ge e le m a (Vfloat n) -> eval_expr ge e le m (make_singleoffloat a) (Vsingle (Float.to_single n)). Proof. intros. econstructor. eauto. auto. Qed. Lemma make_floatofsingle_correct: forall a n e le m, eval_expr ge e le m a (Vsingle n) -> eval_expr ge e le m (make_floatofsingle a) (Vfloat (Float.of_single n)). Proof. intros. econstructor. eauto. auto. 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_longconst_correct make_singleconst_correct make_singleoffloat_correct make_floatofsingle_correct make_floatofint_correct: cshm. Hint Constructors eval_expr eval_exprlist: cshm. Hint Extern 2 (@eq trace _ _) => traceEq: cshm. Lemma make_cmpu_ne_zero_correct: forall e le m a n, eval_expr ge e le m a (Vint n) -> eval_expr ge e le m (make_cmpu_ne_zero a) (Vint (if Int.eq n Int.zero then Int.zero else Int.one)). Proof. intros. assert (DEFAULT: eval_expr ge e le m (Ebinop (Ocmpu Cne) a (make_intconst Int.zero)) (Vint (if Int.eq n Int.zero then Int.zero else Int.one))). { econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool. unfold Int.cmpu. destruct (Int.eq n Int.zero); auto. } assert (CMP: forall ob, Val.of_optbool ob = Vint n -> n = (if Int.eq n Int.zero then Int.zero else Int.one)). { intros. destruct ob; simpl in H0; inv H0. destruct b; inv H2. rewrite Int.eq_false. auto. apply Int.one_not_zero. rewrite Int.eq_true. auto. } destruct a; simpl; auto. destruct b; auto. - inv H. econstructor; eauto. rewrite H6. decEq. decEq. simpl in H6. inv H6. eauto. - inv H. econstructor; eauto. rewrite H6. decEq. decEq. simpl in H6. inv H6. eauto. - inv H. econstructor; eauto. rewrite H6. decEq. decEq. simpl in H6. inv H6. eauto. - inv H. econstructor; eauto. rewrite H6. decEq. decEq. simpl in H6. inv H6. eauto. - inv H. econstructor; eauto. rewrite H6. decEq. decEq. simpl in H6. unfold Val.cmpl in H6. destruct (Val.cmpl_bool c v1 v2) as [[]|]; inv H6; reflexivity. - inv H. econstructor; eauto. rewrite H6. decEq. decEq. simpl in H6. unfold Val.cmplu in H6. destruct (Val.cmplu_bool (Mem.valid_pointer m) c v1 v2) as [[]|]; inv H6; reflexivity. Qed. Lemma make_cmpu_ne_zero_correct_ptr: forall e le m a b i, eval_expr ge e le m a (Vptr b i) -> Archi.ptr64 = false -> Mem.weak_valid_pointer m b (Ptrofs.unsigned i) = true -> eval_expr ge e le m (make_cmpu_ne_zero a) Vone. Proof. intros. assert (DEFAULT: eval_expr ge e le m (Ebinop (Ocmpu Cne) a (make_intconst Int.zero)) Vone). { econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool. unfold Mem.weak_valid_pointer in H1. rewrite H0, H1. rewrite Int.eq_true; auto. } assert (OF_OPTBOOL: forall ob, Some (Val.of_optbool ob) <> Some (Vptr b i)). { intros. destruct ob as [[]|]; discriminate. } assert (OF_BOOL: forall ob, option_map Val.of_bool ob <> Some (Vptr b i)). { intros. destruct ob as [[]|]; discriminate. } destruct a; simpl; auto. destruct b0; auto. - inv H; eelim OF_OPTBOOL; eauto. - inv H; eelim OF_OPTBOOL; eauto. - inv H; eelim OF_OPTBOOL; eauto. - inv H; eelim OF_OPTBOOL; eauto. - inv H; eelim OF_BOOL; eauto. - inv H; eelim OF_BOOL; eauto. Qed. Lemma make_cast_int_correct: forall e le m a n sz si, eval_expr ge e le m a (Vint n) -> eval_expr ge e le m (make_cast_int a sz si) (Vint (cast_int_int sz si n)). Proof. intros. unfold make_cast_int, cast_int_int. destruct sz. destruct si; eauto with cshm. destruct si; eauto with cshm. auto. apply make_cmpu_ne_zero_correct; auto. Qed. Lemma make_longofint_correct: forall e le m a n si, eval_expr ge e le m a (Vint n) -> eval_expr ge e le m (make_longofint a si) (Vlong (cast_int_long si n)). Proof. intros. unfold make_longofint, cast_int_long. destruct si; eauto with cshm. Qed. Hint Resolve make_cast_int_correct make_longofint_correct: cshm. Ltac InvEval := match goal with | [ H: None = Some _ |- _ ] => discriminate | [ H: Some _ = Some _ |- _ ] => inv H; InvEval | [ H: match ?x with Some _ => _ | None => _ end = Some _ |- _ ] => destruct x eqn:?; InvEval | [ H: match ?x with true => _ | false => _ end = Some _ |- _ ] => destruct x eqn:?; InvEval | _ => idtac end. 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 m = Some v' -> eval_expr ge e le m b v'. Proof. intros. unfold make_cast, sem_cast in *; destruct (classify_cast ty1 ty2); inv H; destruct v; InvEval; eauto with cshm. - (* single -> int *) unfold make_singleofint, cast_int_float. destruct si1; eauto with cshm. - (* float -> int *) apply make_cast_int_correct. unfold cast_float_int in Heqo. unfold make_intoffloat. destruct si2; econstructor; eauto; simpl; rewrite Heqo; auto. - (* single -> int *) apply make_cast_int_correct. unfold cast_single_int in Heqo. unfold make_intofsingle. destruct si2; econstructor; eauto with cshm; simpl; rewrite Heqo; auto. - (* long -> float *) unfold make_floatoflong, cast_long_float. destruct si1; eauto with cshm. - (* long -> single *) unfold make_singleoflong, cast_long_single. destruct si1; eauto with cshm. - (* float -> long *) unfold cast_float_long in Heqo. unfold make_longoffloat. destruct si2; econstructor; eauto; simpl; rewrite Heqo; auto. - (* single -> long *) unfold cast_single_long in Heqo. unfold make_longofsingle. destruct si2; econstructor; eauto with cshm; simpl; rewrite Heqo; auto. - (* int -> bool *) apply make_cmpu_ne_zero_correct; auto. - (* pointer (32 bits) -> bool *) eapply make_cmpu_ne_zero_correct_ptr; eauto. - (* long -> bool *) econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool, Int64.cmpu. destruct (Int64.eq i Int64.zero); auto. - (* pointer (64 bits) -> bool *) econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool. unfold Mem.weak_valid_pointer in Heqb1. rewrite Heqb0, Heqb1. rewrite Int64.eq_true. reflexivity. - (* float -> bool *) econstructor; eauto with cshm. simpl. unfold Val.cmpf, Val.cmpf_bool. rewrite Float.cmp_ne_eq. destruct (Float.cmp Ceq f Float.zero); auto. - (* single -> bool *) econstructor; eauto with cshm. simpl. unfold Val.cmpfs, Val.cmpfs_bool. rewrite Float32.cmp_ne_eq. destruct (Float32.cmp Ceq f Float32.zero); auto. - (* struct *) destruct (ident_eq id1 id2); inv H1; auto. - (* union *) destruct (ident_eq id1 id2); inv H1; auto. Qed. Lemma make_boolean_correct: forall e le m a v ty b, eval_expr ge e le m a v -> bool_val v ty m = Some b -> exists vb, eval_expr ge e le m (make_boolean a ty) vb /\ Val.bool_of_val vb b. Proof. intros. unfold make_boolean. unfold bool_val in H0. destruct (classify_bool ty); destruct v; InvEval. - (* int *) econstructor; split. apply make_cmpu_ne_zero_correct with (n := i); auto. destruct (Int.eq i Int.zero); simpl; constructor. - (* ptr 32 bits *) exists Vone; split. eapply make_cmpu_ne_zero_correct_ptr; eauto. constructor. - (* long *) econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmplu. simpl. eauto. destruct (Int64.eq i Int64.zero); simpl; constructor. - (* ptr 64 bits *) exists Vone; split. econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool. unfold Mem.weak_valid_pointer in Heqb0. rewrite Heqb0, Heqb1, Int64.eq_true. reflexivity. constructor. - (* float *) econstructor; split. econstructor; eauto with cshm. simpl. eauto. unfold Val.cmpf, Val.cmpf_bool. simpl. rewrite <- Float.cmp_ne_eq. destruct (Float.cmp Cne f Float.zero); constructor. - (* single *) econstructor; split. econstructor; eauto with cshm. simpl. eauto. unfold Val.cmpfs, Val.cmpfs_bool. simpl. rewrite <- Float32.cmp_ne_eq. destruct (Float32.cmp Cne f Float32.zero); constructor. 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. unfold sem_neg, make_neg; intros until m; intros SEM MAKE EV1; destruct (classify_neg tya); inv MAKE; destruct va; inv SEM; eauto with cshm. Qed. Lemma make_absfloat_correct: forall a tya c va v e le m, sem_absfloat va tya = Some v -> make_absfloat a tya = OK c -> eval_expr ge e le m a va -> eval_expr ge e le m c v. Proof. unfold sem_absfloat, make_absfloat; intros until m; intros SEM MAKE EV1; destruct (classify_neg tya); inv MAKE; destruct va; inv SEM; eauto with cshm. unfold make_floatoflong, cast_long_float. destruct s. econstructor. econstructor; simpl; eauto. simpl; eauto. simpl; eauto. econstructor. econstructor; simpl; eauto. simpl; eauto. simpl; eauto. Qed. Lemma make_notbool_correct: forall a tya c va v e le m, sem_notbool va tya m = 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. unfold sem_notbool, bool_val, make_notbool; intros until m; intros SEM MAKE EV1. destruct (classify_bool tya); inv MAKE; destruct va; simpl in SEM; InvEval. - econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu. destruct (Int.eq i Int.zero); auto. - destruct Archi.ptr64 eqn:SF; inv SEM. destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)) eqn:V; simpl in H0; inv H0. econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool. unfold Mem.weak_valid_pointer in V. rewrite SF, V, Int.eq_true. auto. - econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool, Int64.cmpu. destruct (Int64.eq i Int64.zero); auto. - destruct Archi.ptr64 eqn:SF; inv SEM. destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)) eqn:V; simpl in H0; inv H0. econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool. unfold Mem.weak_valid_pointer in V. rewrite SF, V, Int64.eq_true. auto. - econstructor; eauto with cshm. simpl. unfold Val.cmpf, Val.cmpf_bool. destruct (Float.cmp Ceq f Float.zero); auto. - econstructor; eauto with cshm. simpl. unfold Val.cmpfs, Val.cmpfs_bool. destruct (Float32.cmp Ceq f Float32.zero); auto. Qed. Lemma make_notint_correct: forall a tya c va v e le m, sem_notint va tya = Some v -> make_notint a tya = OK c -> eval_expr ge e le m a va -> eval_expr ge e le m c v. Proof. unfold sem_notint, make_notint; intros until m; intros SEM MAKE EV1; destruct (classify_notint tya); inv MAKE; destruct va; inv SEM; eauto with cshm. 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 -> 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. Section MAKE_BIN. Variable sem_int: signedness -> int -> int -> option val. Variable sem_long: signedness -> int64 -> int64 -> option val. Variable sem_float: float -> float -> option val. Variable sem_single: float32 -> float32 -> option val. Variables iop iopu fop sop lop lopu: binary_operation. Hypothesis iop_ok: forall x y m, eval_binop iop (Vint x) (Vint y) m = sem_int Signed x y. Hypothesis iopu_ok: forall x y m, eval_binop iopu (Vint x) (Vint y) m = sem_int Unsigned x y. Hypothesis lop_ok: forall x y m, eval_binop lop (Vlong x) (Vlong y) m = sem_long Signed x y. Hypothesis lopu_ok: forall x y m, eval_binop lopu (Vlong x) (Vlong y) m = sem_long Unsigned x y. Hypothesis fop_ok: forall x y m, eval_binop fop (Vfloat x) (Vfloat y) m = sem_float x y. Hypothesis sop_ok: forall x y m, eval_binop sop (Vsingle x) (Vsingle y) m = sem_single x y. Lemma make_binarith_correct: binary_constructor_correct (make_binarith iop iopu fop sop lop lopu) (sem_binarith sem_int sem_long sem_float sem_single). Proof. red; unfold make_binarith, sem_binarith; intros until m; intros SEM MAKE EV1 EV2. set (cls := classify_binarith tya tyb) in *. set (ty := binarith_type cls) in *. monadInv MAKE. 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. - destruct s; inv H0; econstructor; eauto with cshm. rewrite iop_ok; auto. rewrite iopu_ok; auto. - destruct s; inv H0; econstructor; eauto with cshm. rewrite lop_ok; auto. rewrite lopu_ok; auto. - erewrite <- fop_ok in SEM; eauto with cshm. - erewrite <- sop_ok in SEM; eauto with cshm. Qed. Lemma make_binarith_int_correct: binary_constructor_correct (make_binarith_int iop iopu lop lopu) (sem_binarith sem_int sem_long (fun x y => None) (fun x y => None)). Proof. red; unfold make_binarith_int, sem_binarith; intros until m; intros SEM MAKE EV1 EV2. set (cls := classify_binarith tya tyb) in *. set (ty := binarith_type cls) in *. monadInv MAKE. 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. - destruct s; inv H0; econstructor; eauto with cshm. rewrite iop_ok; auto. rewrite iopu_ok; auto. - destruct s; inv H0; econstructor; eauto with cshm. rewrite lop_ok; auto. rewrite lopu_ok; auto. Qed. End MAKE_BIN. Hint Extern 2 (@eq (option val) _ _) => (simpl; reflexivity) : cshm. Lemma make_expect_correct: binary_constructor_correct make_expect sem_expect. Proof. apply make_binarith_correct; intros; auto. Qed. Lemma make_add_correct: binary_constructor_correct (make_add cunit.(prog_comp_env)) (sem_add prog.(prog_comp_env)). Proof. assert (A: forall ty si a b c e le m va vb v, make_add_ptr_int cunit.(prog_comp_env) ty si a b = OK c -> eval_expr ge e le m a va -> eval_expr ge e le m b vb -> sem_add_ptr_int (prog_comp_env prog) ty si va vb = Some v -> eval_expr ge e le m c v). { unfold make_add_ptr_int, sem_add_ptr_int; intros until v; intros MAKE EV1 EV2 SEM; monadInv MAKE. destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ). - destruct va; InvEval; destruct vb; inv SEM. + eauto with cshm. + econstructor; eauto with cshm. simpl. rewrite SF. f_equal. f_equal. f_equal. assert (Ptrofs.agree64 (ptrofs_of_int si i0) (cast_int_long si i0)). { destruct si; simpl; apply Ptrofs.agree64_repr; auto. } auto with ptrofs. - destruct va; InvEval; destruct vb; inv SEM. + eauto with cshm. + econstructor; eauto with cshm. simpl. rewrite SF. f_equal. f_equal. f_equal. assert (Ptrofs.agree32 (ptrofs_of_int si i0) i0) by (destruct si; simpl; auto with ptrofs). auto with ptrofs. } assert (B: forall ty a b c e le m va vb v, make_add_ptr_long cunit.(prog_comp_env) ty a b = OK c -> eval_expr ge e le m a va -> eval_expr ge e le m b vb -> sem_add_ptr_long (prog_comp_env prog) ty va vb = Some v -> eval_expr ge e le m c v). { unfold make_add_ptr_long, sem_add_ptr_long; intros until v; intros MAKE EV1 EV2 SEM; monadInv MAKE. destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ). - destruct va; InvEval; destruct vb; inv SEM. + eauto with cshm. + econstructor; eauto with cshm. simpl. rewrite SF. f_equal. f_equal. f_equal. auto with ptrofs. - destruct va; InvEval; destruct vb; inv SEM. + eauto with cshm. + econstructor; eauto with cshm. simpl. rewrite SF. f_equal. f_equal. f_equal. assert (Ptrofs.agree32 (Ptrofs.of_int64 i0) (Int64.loword i0)) by (apply Ptrofs.agree32_repr; auto). auto with ptrofs. } red; unfold make_add, sem_add; intros until m; intros SEM MAKE EV1 EV2; destruct (classify_add tya tyb); eauto. - eapply make_binarith_correct; eauto; intros; auto. Qed. 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); try (monadInv MAKE). - destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ). + destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. econstructor; eauto with cshm. simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. assert (Ptrofs.agree64 (ptrofs_of_int si i0) (cast_int_long si i0)). { destruct si; simpl; apply Ptrofs.agree64_repr; auto. } auto with ptrofs. + destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. econstructor; eauto with cshm. simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. assert (Ptrofs.agree32 (ptrofs_of_int si i0) i0) by (destruct si; simpl; auto with ptrofs). auto with ptrofs. - rewrite (transl_sizeof _ _ _ _ LINK EQ) in EQ0. clear EQ. set (sz := Ctypes.sizeof (prog_comp_env prog) ty) in *. destruct va; InvEval; destruct vb; InvEval. destruct (eq_block b0 b1); try discriminate. destruct (zlt 0 sz); try discriminate. destruct (zle sz Ptrofs.max_signed); simpl in SEM; inv SEM. assert (E1: Ptrofs.signed (Ptrofs.repr sz) = sz). { apply Ptrofs.signed_repr. generalize Ptrofs.min_signed_neg; lia. } destruct Archi.ptr64 eqn:SF; inversion EQ0; clear EQ0; subst c. + assert (E: Int64.signed (Int64.repr sz) = sz). { apply Int64.signed_repr. replace Int64.max_signed with Ptrofs.max_signed. generalize Int64.min_signed_neg; lia. unfold Ptrofs.max_signed, Ptrofs.half_modulus; rewrite Ptrofs.modulus_eq64 by auto. reflexivity. } econstructor; eauto with cshm. rewrite SF, dec_eq_true. simpl. predSpec Int64.eq Int64.eq_spec (Int64.repr sz) Int64.zero. rewrite H in E; rewrite Int64.signed_zero in E; extlia. predSpec Int64.eq Int64.eq_spec (Int64.repr sz) Int64.mone. rewrite H0 in E; rewrite Int64.signed_mone in E; extlia. rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. apply f_equal. apply f_equal. symmetry. auto with ptrofs. + assert (E: Int.signed (Int.repr sz) = sz). { apply Int.signed_repr. replace Int.max_signed with Ptrofs.max_signed. generalize Int.min_signed_neg; lia. unfold Ptrofs.max_signed, Ptrofs.half_modulus, Ptrofs.modulus, Ptrofs.wordsize, Wordsize_Ptrofs.wordsize. rewrite SF. reflexivity. } econstructor; eauto with cshm. rewrite SF, dec_eq_true. simpl. predSpec Int.eq Int.eq_spec (Int.repr sz) Int.zero. rewrite H in E; rewrite Int.signed_zero in E; extlia. predSpec Int.eq Int.eq_spec (Int.repr sz) Int.mone. rewrite H0 in E; rewrite Int.signed_mone in E; extlia. rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. apply f_equal. apply f_equal. symmetry. auto with ptrofs. - destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ). + destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. econstructor; eauto with cshm. simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. auto with ptrofs. + destruct va; InvEval; destruct vb; inv SEM; eauto with cshm. econstructor; eauto with cshm. simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. assert (Ptrofs.agree32 (Ptrofs.of_int64 i0) (Int64.loword i0)) by (apply Ptrofs.agree32_repr; auto). auto with ptrofs. - eapply make_binarith_correct; eauto; intros; auto. Qed. Lemma make_mul_correct: binary_constructor_correct make_mul sem_mul. Proof. apply make_binarith_correct; intros; auto. Qed. Lemma make_div_correct: binary_constructor_correct make_div sem_div. Proof. apply make_binarith_correct; intros; auto. Qed. Lemma make_mod_correct: binary_constructor_correct make_mod sem_mod. Proof. apply make_binarith_int_correct; intros; auto. Qed. Lemma make_and_correct: binary_constructor_correct make_and sem_and. Proof. apply make_binarith_int_correct; intros; auto. Qed. Lemma make_or_correct: binary_constructor_correct make_or sem_or. Proof. apply make_binarith_int_correct; intros; auto. Qed. Lemma make_xor_correct: binary_constructor_correct make_xor sem_xor. Proof. apply make_binarith_int_correct; intros; auto. Qed. Ltac comput val := let x := fresh in set val as x in *; vm_compute in x; subst x. Remark small_shift_amount_1: forall i, Int64.ltu i Int64.iwordsize = true -> Int.ltu (Int64.loword i) Int64.iwordsize' = true /\ Int64.unsigned i = Int.unsigned (Int64.loword i). Proof. intros. apply Int64.ltu_inv in H. comput (Int64.unsigned Int64.iwordsize). assert (Int64.unsigned i = Int.unsigned (Int64.loword i)). { unfold Int64.loword. rewrite Int.unsigned_repr; auto. comput Int.max_unsigned; lia. } split; auto. unfold Int.ltu. apply zlt_true. rewrite <- H0. tauto. Qed. Remark small_shift_amount_2: forall i, Int64.ltu i (Int64.repr 32) = true -> Int.ltu (Int64.loword i) Int.iwordsize = true. Proof. intros. apply Int64.ltu_inv in H. comput (Int64.unsigned (Int64.repr 32)). assert (Int64.unsigned i = Int.unsigned (Int64.loword i)). { unfold Int64.loword. rewrite Int.unsigned_repr; auto. comput Int.max_unsigned; lia. } unfold Int.ltu. apply zlt_true. rewrite <- H0. tauto. Qed. Lemma small_shift_amount_3: forall i, Int.ltu i Int64.iwordsize' = true -> Int64.unsigned (Int64.repr (Int.unsigned i)) = Int.unsigned i. Proof. intros. apply Int.ltu_inv in H. comput (Int.unsigned Int64.iwordsize'). apply Int64.unsigned_repr. comput Int64.max_unsigned; lia. Qed. 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; destruct (classify_shift tya tyb); inv MAKE; destruct va; try discriminate; destruct vb; try discriminate. - destruct (Int.ltu i0 Int.iwordsize) eqn:E; inv SEM. econstructor; eauto. simpl; rewrite E; auto. - destruct (Int64.ltu i0 Int64.iwordsize) eqn:E; inv SEM. exploit small_shift_amount_1; eauto. intros [A B]. econstructor; eauto with cshm. simpl. rewrite A. f_equal; f_equal. unfold Int64.shl', Int64.shl. rewrite B; auto. - destruct (Int64.ltu i0 (Int64.repr 32)) eqn:E; inv SEM. econstructor; eauto with cshm. simpl. rewrite small_shift_amount_2; auto. - destruct (Int.ltu i0 Int64.iwordsize') eqn:E; inv SEM. econstructor; eauto with cshm. simpl. rewrite E. unfold Int64.shl', Int64.shl. rewrite small_shift_amount_3; auto. Qed. 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; destruct (classify_shift tya tyb); inv MAKE; destruct va; try discriminate; destruct vb; try discriminate. - destruct (Int.ltu i0 Int.iwordsize) eqn:E; inv SEM. destruct s; inv H0; econstructor; eauto; simpl; rewrite E; auto. - destruct (Int64.ltu i0 Int64.iwordsize) eqn:E; inv SEM. exploit small_shift_amount_1; eauto. intros [A B]. destruct s; inv H0; econstructor; eauto with cshm; simpl; rewrite A; f_equal; f_equal. unfold Int64.shr', Int64.shr; rewrite B; auto. unfold Int64.shru', Int64.shru; rewrite B; auto. - destruct (Int64.ltu i0 (Int64.repr 32)) eqn:E; inv SEM. destruct s; inv H0; econstructor; eauto with cshm; simpl; rewrite small_shift_amount_2; auto. - destruct (Int.ltu i0 Int64.iwordsize') eqn:E; inv SEM. destruct s; inv H0; econstructor; eauto with cshm; simpl; rewrite E. unfold Int64.shr', Int64.shr; rewrite small_shift_amount_3; auto. unfold Int64.shru', Int64.shru; rewrite small_shift_amount_3; auto. Qed. Lemma make_cmp_ptr_correct: forall cmp e le m a va b vb v, cmp_ptr m cmp va vb = Some v -> eval_expr ge e le m a va -> eval_expr ge e le m b vb -> eval_expr ge e le m (make_cmp_ptr cmp a b) v. Proof. unfold cmp_ptr, make_cmp_ptr; intros. destruct Archi.ptr64. - econstructor; eauto. - econstructor; eauto. simpl. unfold Val.cmpu. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bo|]; inv H. auto. Qed. Remark make_ptrofs_of_int_correct: forall e le m a i si, eval_expr ge e le m a (Vint i) -> eval_expr ge e le m (if Archi.ptr64 then make_longofint a si else a) (Vptrofs (ptrofs_of_int si i)). Proof. intros. unfold Vptrofs, ptrofs_of_int. destruct Archi.ptr64 eqn:SF. - unfold make_longofint. destruct si. + replace (Ptrofs.to_int64 (Ptrofs.of_ints i)) with (Int64.repr (Int.signed i)). eauto with cshm. apply Int64.eqm_samerepr. rewrite Ptrofs.eqm64 by auto. apply Ptrofs.eqm_unsigned_repr. + replace (Ptrofs.to_int64 (Ptrofs.of_intu i)) with (Int64.repr (Int.unsigned i)). eauto with cshm. apply Int64.eqm_samerepr. rewrite Ptrofs.eqm64 by auto. apply Ptrofs.eqm_unsigned_repr. - destruct si. + replace (Ptrofs.to_int (Ptrofs.of_ints i)) with i. auto. symmetry. auto with ptrofs. + replace (Ptrofs.to_int (Ptrofs.of_intu i)) with i. auto. symmetry. auto with ptrofs. Qed. Remark make_ptrofs_of_int64_correct: forall e le m a i, eval_expr ge e le m a (Vlong i) -> eval_expr ge e le m (if Archi.ptr64 then a else Eunop Ointoflong a) (Vptrofs (Ptrofs.of_int64 i)). Proof. intros. unfold Vptrofs. destruct Archi.ptr64 eqn:SF. - replace (Ptrofs.to_int64 (Ptrofs.of_int64 i)) with i. auto. symmetry. auto with ptrofs. - econstructor; eauto. simpl. apply f_equal. apply f_equal. apply Int.eqm_samerepr. rewrite Ptrofs.eqm32 by auto. apply Ptrofs.eqm_unsigned_repr. Qed. Lemma make_cmp_correct: forall cmp, binary_constructor_correct (make_cmp cmp) (sem_cmp cmp). Proof. red; unfold sem_cmp, make_cmp; intros until m; intros SEM MAKE EV1 EV2; destruct (classify_cmp tya tyb). - inv MAKE. eapply make_cmp_ptr_correct; eauto. - inv MAKE. destruct vb; InvEval; eauto using make_cmp_ptr_correct, make_ptrofs_of_int_correct. - inv MAKE. destruct va; InvEval; eauto using make_cmp_ptr_correct, make_ptrofs_of_int_correct. - inv MAKE. destruct vb; InvEval; eauto using make_cmp_ptr_correct, make_ptrofs_of_int64_correct. - inv MAKE. destruct va; InvEval; eauto using make_cmp_ptr_correct, make_ptrofs_of_int64_correct. - eapply make_binarith_correct; eauto; intros; auto. 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 m = 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; eauto. eapply make_neg_correct; eauto. eapply make_absfloat_correct; eauto. Qed. Lemma transl_binop_correct: forall op a tya b tyb c va vb v e le m, 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. Proof. intros. destruct op; simpl in *. - eapply make_expect_correct; eauto. - 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. Remark int_ltu_true: forall x, 0 <= x < Int.zwordsize -> Int.ltu (Int.repr x) Int.iwordsize = true. Proof. intros. unfold Int.ltu. rewrite Int.unsigned_repr_wordsize, Int.unsigned_repr, zlt_true by (generalize Int.wordsize_max_unsigned; lia). auto. Qed. Remark first_bit_range: forall sz pos width, 0 <= pos -> 0 < width -> pos + width <= bitsize_carrier sz -> 0 <= first_bit sz pos width < Int.zwordsize /\ 0 <= Int.zwordsize - first_bit sz pos width - width < Int.zwordsize. Proof. intros. assert (bitsize_carrier sz <= Int.zwordsize) by (destruct sz; compute; congruence). unfold first_bit; destruct Archi.big_endian; lia. Qed. Lemma make_load_correct: forall addr ty bf code b ofs v e le m, make_load addr ty bf = OK code -> eval_expr ge e le m addr (Vptr b ofs) -> deref_loc ty m b ofs bf v -> eval_expr ge e le m code v. Proof. unfold make_load; intros until m; intros MKLOAD EVEXP DEREF. inv DEREF. - (* scalar *) rewrite H in MKLOAD. inv MKLOAD. apply eval_Eload with (Vptr b ofs); auto. - (* by reference *) rewrite H in MKLOAD. inv MKLOAD. auto. - (* by copy *) rewrite H in MKLOAD. inv MKLOAD. auto. - (* by bitfield *) inv H. unfold make_extract_bitfield in MKLOAD. unfold bitfield_extract. exploit (first_bit_range sz pos width); eauto. lia. intros [A1 A2]. set (amount1 := Int.repr (Int.zwordsize - first_bit sz pos width - width)) in MKLOAD. set (amount2 := Int.repr (Int.zwordsize - width)) in MKLOAD. destruct (zle 0 pos && zlt 0 width && zle (pos + width) (bitsize_carrier sz)); inv MKLOAD. set (e1 := Eload (chunk_for_carrier sz) addr). assert (E1: eval_expr ge e le m e1 (Vint c)) by (econstructor; eauto). set (e2 := Ebinop Oshl e1 (make_intconst amount1)). assert (E2: eval_expr ge e le m e2 (Vint (Int.shl c amount1))). { econstructor; eauto using make_intconst_correct. cbn. unfold amount1 at 1; rewrite int_ltu_true by lia. auto. } econstructor; eauto using make_intconst_correct. destruct (Ctypes.intsize_eq sz IBool || Ctypes.signedness_eq sg Unsigned); cbn. + unfold amount2 at 1; rewrite int_ltu_true by lia. rewrite Int.unsigned_bitfield_extract_by_shifts by lia. auto. + unfold amount2 at 1; rewrite int_ltu_true by lia. rewrite Int.signed_bitfield_extract_by_shifts by lia. auto. Qed. Lemma make_store_bitfield_correct: forall f sz sg pos width 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 prog.(prog_comp_env) ty m b ofs (Bits sz sg pos width) v m' -> make_store_bitfield sz sg pos width dst src = OK s -> step ge (State f s k e le m) E0 (State f Sskip k e le m'). Proof. intros until s; intros DST SRC ASG MK. inv ASG. inv H5. unfold make_store_bitfield in MK. destruct (zle 0 pos && zlt 0 width && zle (pos + width) (bitsize_carrier sz)); inv MK. econstructor; eauto. exploit (first_bit_range sz pos width); eauto. lia. intros [A1 A2]. rewrite Int.bitfield_insert_alternative by lia. set (amount := first_bit sz pos width). set (mask := Int.shl (Int.repr (two_p width - 1)) (Int.repr amount)). repeat econstructor; eauto. cbn. rewrite int_ltu_true by lia. auto. Qed. Lemma make_memcpy_correct: 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 prog.(prog_comp_env) ty m b ofs Full v m' -> access_mode ty = By_copy -> 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. 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. apply alignof_blockcopy_1248. apply sizeof_pos. apply sizeof_alignof_blockcopy_compat. Qed. Lemma make_store_correct: forall addr ty bf rhs code e le m b ofs v m' f k, make_store cunit.(prog_comp_env) addr ty bf rhs = OK code -> eval_expr ge e le m addr (Vptr b ofs) -> eval_expr ge e le m rhs v -> assign_loc prog.(prog_comp_env) ty m b ofs bf 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. inversion ASSIGN; subst. - (* nonvolatile scalar *) rewrite H in MKSTORE; inv MKSTORE. econstructor; eauto. - (* by copy *) rewrite H in MKSTORE. eapply make_memcpy_correct with (b := b) (v := Vptr b' ofs'); eauto. - (* bitfield *) eapply make_store_bitfield_correct; eauto. Qed. Lemma make_normalization_correct: forall e le m a v t, eval_expr ge e le m a v -> wt_val v t -> eval_expr ge e le m (make_normalization t a) v. Proof. intros. destruct t; simpl; auto. inv H0. - destruct i; simpl in H3. + destruct s; econstructor; eauto; simpl; congruence. + destruct s; econstructor; eauto; simpl; congruence. + auto. + econstructor; eauto; simpl; congruence. - auto. - destruct i. + destruct s; econstructor; eauto. + destruct s; econstructor; eauto. + auto. + econstructor; eauto. Qed. End CONSTRUCTORS. (** * Basic preservation invariants *) Section CORRECTNESS. Variable prog: Clight.program. Variable tprog: Csharpminor.program. 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_match 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 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 *) (** 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) -> 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) }. Lemma match_env_globals: forall e te id, match_env e te -> e!id = None -> te!id = None. Proof. intros. destruct (te!id) as [[b sz] | ] eqn:?; auto. exploit me_local_inv; eauto. intros [ty EQ]. congruence. Qed. Lemma match_env_same_blocks: forall e te, match_env e te -> blocks_of_env te = Clight.blocks_of_env ge e. Proof. intros. set (R := fun (x: (block * type)) (y: (block * Z)) => match x, y with | (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, 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. unfold blocks_of_env, Clight.blocks_of_env. generalize H0. induction 1. auto. simpl. f_equal; auto. unfold block_of_binding, Clight.block_of_binding. destruct a1 as [id1 [blk1 ty1]]. destruct b1 as [id2 [blk2 sz2]]. simpl in *. destruct H1 as [A [B C]]. congruence. Qed. Lemma match_env_free_blocks: forall e te m m', match_env e te -> Mem.free_list m (Clight.blocks_of_env ge 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 ty. repeat rewrite PTree.gempty. congruence. intros until sz. 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 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 tvars te2 m2 /\ match_env e2 te2. Proof. 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. destruct (peq id0 id); intros. congruence. eapply me_local; eauto. (* me_local_inv *) intros until sz. repeat rewrite PTree.gsspec. destruct (peq id0 id); intros. exists ty; congruence. eapply me_local_inv; eauto. intros [te2 [ALLOC MENV]]. exists te2; split. econstructor; eauto. auto. Qed. Lemma create_undef_temps_match: forall temps, create_undef_temps (map fst temps) = Clight.create_undef_temps temps. Proof. induction temps; simpl. auto. destruct a as [id ty]. simpl. decEq. auto. Qed. Lemma bind_parameter_temps_match: forall vars vals le1 le2, Clight.bind_parameter_temps vars vals le1 = Some le2 -> bind_parameters (map fst vars) vals le1 = Some le2. Proof. induction vars; simpl; intros. destruct vals; inv H. auto. 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 *) (** 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 cunit: Clight.program. Hypothesis LINK: linkorder cunit prog. 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: forall a loc ofs bf ta, Clight.eval_lvalue ge e le m a loc ofs bf -> transl_expr cunit.(prog_comp_env) a = OK ta -> exists tb, transl_lvalue cunit.(prog_comp_env) a = OK (tb, bf) /\ make_load tb (typeof a) bf = OK ta. Proof. intros until ta; intros EVAL TR. inv EVAL; simpl in TR. - (* var local *) exists (Eaddrof id); auto. - (* var global *) exists (Eaddrof id); auto. - (* deref *) monadInv TR. cbn; rewrite EQ. exists x; auto. - (* field struct *) monadInv TR. assert (x1 = bf). { rewrite H0 in EQ1. unfold make_field_access in EQ1. destruct ((prog_comp_env cunit)!id) as [co'|] eqn:E; try discriminate. monadInv EQ1. exploit field_offset_stable. eexact LINK. eauto. instantiate (1 := i). intros [A B]. simpl in H1, H2. congruence. } subst x1. exists x0; split; auto. simpl; rewrite EQ; auto. - (* field union *) monadInv TR. assert (x1 = bf). { rewrite H0 in EQ1. unfold make_field_access in EQ1. destruct ((prog_comp_env cunit)!id) as [co'|] eqn:E; try discriminate. monadInv EQ1. exploit union_field_offset_stable. eexact LINK. eauto. instantiate (1 := i). intros [A B]. simpl in H1, H2. congruence. } subst x1. exists x0; split; auto. simpl; rewrite EQ; auto. Qed. Lemma transl_expr_lvalue_correct: (forall a v, Clight.eval_expr ge e le m a v -> 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 bf, Clight.eval_lvalue ge e le m a b ofs bf -> forall ta bf' (TR: transl_lvalue cunit.(prog_comp_env) a = OK (ta, bf')), bf = bf' /\ 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. - (* const single *) apply make_singleconst_correct. - (* const long *) apply make_longconst_correct. - (* temp var *) constructor; auto. - (* addrof *) destruct x0; inv EQ0. apply H0 in EQ. destruct EQ. auto. - (* unop *) eapply transl_unop_correct; eauto. - (* binop *) eapply transl_binop_correct; eauto. - (* cast *) eapply make_cast_correct; eauto. - (* sizeof *) rewrite (transl_sizeof _ _ _ _ LINK EQ). apply make_ptrofsconst_correct. - (* alignof *) rewrite (transl_alignof _ _ _ _ LINK EQ). apply make_ptrofsconst_correct. - (* rvalue out of lvalue *) exploit transl_expr_lvalue; eauto. intros [tb [TRLVAL MKLOAD]]. apply H0 in TRLVAL; destruct TRLVAL. eapply make_load_correct; eauto. - (* var local *) exploit (me_local _ _ MENV); eauto. intros EQ. split; auto. econstructor. eapply eval_var_addr_local. eauto. - (* var global *) split; auto. econstructor. eapply eval_var_addr_global. eapply match_env_globals; eauto. rewrite symbols_preserved. auto. - (* deref *) eauto. - (* field struct *) unfold make_field_access in EQ0. rewrite H1 in EQ0. destruct (prog_comp_env cunit)!id as [co'|] eqn:CO; try discriminate; monadInv EQ0. exploit field_offset_stable. eexact LINK. eauto. instantiate (1 := i). intros [A B]. rewrite <- B in EQ1. assert (x0 = delta) by (unfold ge in *; simpl in *; congruence). assert (bf' = bf) by (unfold ge in *; simpl in *; congruence). subst x0 bf'. split; auto. destruct Archi.ptr64 eqn:SF. + eapply eval_Ebinop; eauto using make_longconst_correct. simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. auto with ptrofs. + eapply eval_Ebinop; eauto using make_intconst_correct. simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. auto with ptrofs. - (* field union *) unfold make_field_access in EQ0. rewrite H1 in EQ0. destruct (prog_comp_env cunit)!id as [co'|] eqn:CO; try discriminate; monadInv EQ0. exploit union_field_offset_stable. eexact LINK. eauto. instantiate (1 := i). intros [A B]. rewrite <- B in EQ1. assert (x0 = delta) by (unfold ge in *; simpl in *; congruence). assert (bf' = bf) by (unfold ge in *; simpl in *; congruence). subst x0 bf'. split; auto. destruct Archi.ptr64 eqn:SF. + eapply eval_Ebinop; eauto using make_longconst_correct. simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. auto with ptrofs. + eapply eval_Ebinop; eauto using make_intconst_correct. simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. auto with ptrofs. Qed. Lemma transl_expr_correct: forall a v, Clight.eval_expr ge e le m a v -> 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 bf, Clight.eval_lvalue ge e le m a b ofs bf -> forall ta bf', transl_lvalue cunit.(prog_comp_env) a = OK (ta, bf') -> bf = bf' /\ 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 cunit.(prog_comp_env) 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; eauto. eapply transl_expr_correct; eauto. auto. Qed. Lemma typlist_of_arglist_eq: forall al tyl vl, Clight.eval_exprlist ge e le m al tyl vl -> typlist_of_arglist al tyl = typlist_of_typelist tyl. Proof. induction 1; simpl. auto. f_equal; auto. Qed. End EXPR. (** ** 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: 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 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 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 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: 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 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) | match_Kcall_normalize: forall ce tyret nbrk ncnt nbrk' ncnt' f e k id a tf te le tk cu, linkorder cu prog -> transl_function cu.(prog_comp_env) f = OK tf -> match_env e te -> match_cont cu.(prog_comp_env) (Clight.fn_return f) nbrk' ncnt' k tk -> (forall v e le m, wt_val v tyret -> le!id = Some v -> eval_expr tge e le m a v) -> match_cont ce tyret nbrk ncnt (Clight.Kcall (Some id) f e le k) (Kcall (Some id) tf te le (Kseq (Sset id a) 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' 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 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 cu ce (LINK: linkorder cu prog) (TR: match_fundef cu fd tfd) (MK: match_cont ce tres 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 tres k m tk ce (MK: match_cont ce tres 0%nat 0%nat k tk) (WT: wt_val res tres), 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 cu, linkorder cu prog -> transl_function cu.(prog_comp_env) f = OK tf -> match_env e te -> 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. 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 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 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 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 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 *) auto. - (* assign *) unfold make_store, make_memcpy in EQ3. destruct x0. destruct (access_mode (typeof e)); monadInv EQ3; auto. unfold make_store_bitfield in EQ3. destruct (zle 0 pos && zlt 0 width && zle (pos + width) (bitsize_carrier sz)); monadInv EQ3; auto. - (* set *) auto. - (* call *) simpl in TR. destruct (classify_fun (typeof e)); monadInv TR. unfold make_funcall. destruct o; auto; destruct Conventions1.return_value_needs_normalization; auto. - (* builtin *) 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. - (* 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 *) auto. - (* continue *) auto. - (* return *) simpl in TR. destruct o; monadInv TR. auto. auto. - (* 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 *) 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. - (* nil *) auto. - (* 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'] | ]. 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 ce' 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. - apply match_Kstop. - eapply match_Kcall; eauto. - eapply match_Kcall_normalize; eauto. Qed. Lemma match_cont_is_call_cont: forall ce tyret nbrk ncnt k tk ce' nbrk' ncnt', match_cont ce tyret nbrk ncnt k tk -> Clight.is_call_cont k -> match_cont ce' tyret nbrk' ncnt' k tk /\ is_call_cont tk. Proof. intros. inv H; simpl in H0; try contradiction; simpl. split; auto; apply match_Kstop. split; auto; eapply match_Kcall; eauto. split; auto; eapply match_Kcall_normalize; eauto. Qed. (** The simulation proof *) Lemma transl_step: forall S1 t S2, Clight.step2 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 *) monadInv TR. assert (SAME: ts' = ts /\ tk' = tk). { inversion MTR. auto. subst ts. unfold make_store, make_memcpy in EQ3. destruct x0. destruct (access_mode (typeof a1)); monadInv EQ3; auto. unfold make_store_bitfield in EQ3. destruct (zle 0 pos && zlt 0 width && zle (pos + width) (bitsize_carrier sz)); monadInv EQ3; auto. } destruct SAME; subst ts' tk'. exploit transl_lvalue_correct; eauto. intros [A B]; subst x0. econstructor; split. apply plus_one. eapply make_store_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 cc CF TR. monadInv TR. exploit functions_translated; eauto. intros (cu' & tfd & FIND & TFD & LINK'). rewrite H in CF. simpl in CF. inv CF. set (sg := {| sig_args := typlist_of_arglist al targs; sig_res := rettype_of_type tres; sig_cc := cc |}) in *. assert (SIG: funsig tfd = sg). { unfold sg; erewrite typlist_of_arglist_eq by eauto. eapply transl_fundef_sig1; eauto. rewrite H3; auto. } assert (EITHER: tk' = tk /\ ts' = Scall optid sg x x0 \/ exists id, optid = Some id /\ tk' = tk /\ ts' = Sseq (Scall optid sg x x0) (Sset id (make_normalization tres (Evar id)))). { unfold make_funcall in MTR. destruct optid. destruct Conventions1.return_value_needs_normalization. inv MTR. right; exists i; auto. inv MTR; auto. inv MTR; auto. } destruct EITHER as [(EK & ES) | (id & EI & EK & ES)]; rewrite EK, ES. + (* without normalization of return value *) econstructor; split. apply plus_one. eapply step_call; eauto. eapply transl_expr_correct with (cunit := cu); eauto. eapply transl_arglist_correct with (cunit := cu); eauto. econstructor; eauto. eapply match_Kcall with (ce := prog_comp_env cu') (cu := cu); eauto. exact I. + (* with normalization of return value *) subst optid. econstructor; split. eapply plus_two. apply step_seq. eapply step_call; eauto. eapply transl_expr_correct with (cunit := cu); eauto. eapply transl_arglist_correct with (cunit := cu); eauto. traceEq. econstructor; eauto. eapply match_Kcall_normalize with (ce := prog_comp_env cu') (cu := cu); eauto. intros. eapply make_normalization_correct; eauto. constructor; eauto. exact I. - (* builtin *) monadInv TR. inv MTR. econstructor; split. apply plus_one. econstructor. eapply transl_arglist_correct; eauto. eapply external_call_symbols_preserved with (ge1 := ge). apply senv_preserved. eauto. eapply match_states_skip; 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 *) monadInv TR. inv MTR. exploit make_boolean_correct; eauto. exploit transl_expr_correct; eauto. intros [v [A B]]. econstructor; split. apply plus_one. apply step_ifthenelse with (v := v) (b := b); auto. destruct b; econstructor; eauto; constructor. - (* loop *) 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 loop *) 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'. 2:constructor. constructor. apply star_one. constructor. traceEq. econstructor; eauto. constructor. econstructor; eauto. - (* break loop1 *) 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 loop2 *) monadInv TR. inv MTR. inv MK. econstructor; split. apply plus_one. constructor. econstructor; eauto. simpl. rewrite H6; simpl. rewrite H8; simpl. eauto. constructor. - (* break loop2 *) monadInv TR. inv MTR. inv MK. econstructor; split. eapply plus_left. constructor. apply star_one. constructor. traceEq. eapply match_states_skip; eauto. - (* return none *) monadInv TR. inv MTR. econstructor; split. apply plus_one. constructor. eapply match_env_free_blocks; eauto. eapply match_returnstate with (ce := prog_comp_env cu); eauto. eapply match_cont_call_cont. eauto. constructor. - (* 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. eapply match_returnstate with (ce := prog_comp_env cu); eauto. eapply match_cont_call_cont. eauto. apply wt_val_casted. eapply cast_val_is_casted; 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. eapply match_env_free_blocks; eauto. eapply match_returnstate with (ce := prog_comp_env cu); eauto. constructor. - (* 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. destruct (classify_switch (typeof a)); inv EQ2; econstructor; split; eauto; destruct v; inv H0; constructor. } destruct E as (b & A & B). subst ts. 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'. 2:constructor. 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 (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. 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. 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 EQ; simpl. rewrite EQ1; simpl. auto. constructor. replace (fn_return f) with tres. eassumption. simpl in TY. unfold type_of_function in TY. congruence. - (* external function *) inv TR. exploit match_cont_is_call_cont; eauto. intros [A B]. econstructor; split. apply plus_one. constructor. eapply external_call_symbols_preserved; eauto. apply senv_preserved. eapply match_returnstate with (ce := ce); eauto. apply has_rettype_wt_val. replace (rettype_of_type tres0) with (sig_res (ef_sig ef)). eapply external_call_well_typed_gen; eauto. rewrite H5. simpl. simpl in TY. congruence. - (* returnstate *) inv MK. + (* without normalization *) econstructor; split. apply plus_one. constructor. econstructor; eauto. simpl; reflexivity. constructor. + (* with normalization *) econstructor; split. eapply plus_three. econstructor. econstructor. constructor. simpl. apply H13. eauto. apply PTree.gss. traceEq. simpl. rewrite PTree.set2. econstructor; eauto. simpl; reflexivity. constructor. Qed. Lemma transl_initial_states: forall S, Clight.initial_state prog S -> exists R, initial_state tprog R /\ match_states S R. Proof. intros. inv H. 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. apply (Genv.init_mem_match TRANSL). eauto. econstructor; eauto. instantiate (1 := prog_comp_env cu). constructor; auto. exact I. 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: forward_simulation (Clight.semantics2 prog) (Csharpminor.semantics tprog). Proof. eapply forward_simulation_plus. apply senv_preserved. eexact transl_initial_states. eexact transl_final_states. eexact transl_step. Qed. End CORRECTNESS. (** ** Commutation with linking *) Global 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.