diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-28 12:57:58 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-28 12:57:58 +0000 |
commit | c48b9097201dc9a1e326acdbce491fe16cab01e6 (patch) | |
tree | 53335d9dcb4aead3ec1f42e4138e87649640edd0 /backend/Selectionproof.v | |
parent | 2b89ae94ffb6dc56fa780acced8ab7ad0afbb3b5 (diff) | |
download | compcert-c48b9097201dc9a1e326acdbce491fe16cab01e6.tar.gz compcert-c48b9097201dc9a1e326acdbce491fe16cab01e6.zip |
Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les expressions sont maintenant pures et les appels de fonctions sont des statements. Ajout de semantiques coinductives pour la divergence en Clight, C#minor, Cminor. Preuve de preservation semantique pour les programmes qui divergent.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@409 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Selectionproof.v')
-rw-r--r-- | backend/Selectionproof.v | 1105 |
1 files changed, 524 insertions, 581 deletions
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index e41765a7..177e3211 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -19,6 +19,9 @@ Open Local Scope selection_scope. Section CMCONSTR. Variable ge: genv. +Variable sp: val. +Variable e: env. +Variable m: mem. (** * Lifting of let-bound variables *) @@ -57,72 +60,34 @@ Proof. apply IHinsert_lenv. exact H0. omega. Qed. -Scheme eval_expr_ind_3 := Minimality for eval_expr Sort Prop - with eval_condexpr_ind_3 := Minimality for eval_condexpr Sort Prop - with eval_exprlist_ind_3 := Minimality for eval_exprlist Sort Prop. - -Hint Resolve eval_Evar eval_Eop eval_Eload eval_Estore - eval_Ecall eval_Econdition eval_Ealloc +Hint Resolve eval_Evar eval_Eop eval_Eload eval_Econdition eval_Elet eval_Eletvar eval_CEtrue eval_CEfalse eval_CEcond eval_CEcondition eval_Enil eval_Econs: evalexpr. -Lemma eval_list_one: - forall sp le e m1 a t m2 v, - eval_expr ge sp le e m1 a t m2 v -> - eval_exprlist ge sp le e m1 (a ::: Enil) t m2 (v :: nil). -Proof. - intros. econstructor. eauto. constructor. traceEq. -Qed. - -Lemma eval_list_two: - forall sp le e m1 a1 t1 m2 v1 a2 t2 m3 v2 t, - eval_expr ge sp le e m1 a1 t1 m2 v1 -> - eval_expr ge sp le e m2 a2 t2 m3 v2 -> - t = t1 ** t2 -> - eval_exprlist ge sp le e m1 (a1 ::: a2 ::: Enil) t m3 (v1 :: v2 :: nil). -Proof. - intros. econstructor. eauto. econstructor. eauto. constructor. - reflexivity. traceEq. -Qed. - -Lemma eval_list_three: - forall sp le e m1 a1 t1 m2 v1 a2 t2 m3 v2 a3 t3 m4 v3 t, - eval_expr ge sp le e m1 a1 t1 m2 v1 -> - eval_expr ge sp le e m2 a2 t2 m3 v2 -> - eval_expr ge sp le e m3 a3 t3 m4 v3 -> - t = t1 ** t2 ** t3 -> - eval_exprlist ge sp le e m1 (a1 ::: a2 ::: a3 ::: Enil) t m4 (v1 :: v2 :: v3 :: nil). -Proof. - intros. econstructor. eauto. econstructor. eauto. econstructor. eauto. constructor. - reflexivity. reflexivity. traceEq. -Qed. - -Hint Resolve eval_list_one eval_list_two eval_list_three: evalexpr. - Lemma eval_lift_expr: - forall w sp le e m1 a t m2 v, - eval_expr ge sp le e m1 a t m2 v -> + forall w le a v, + eval_expr ge sp e m le a v -> forall p le', insert_lenv le p w le' -> - eval_expr ge sp le' e m1 (lift_expr p a) t m2 v. + eval_expr ge sp e m le' (lift_expr p a) v. Proof. - intros w. - apply (eval_expr_ind_3 ge - (fun sp le e m1 a t m2 v => + intro w. + apply (eval_expr_ind3 ge sp e m + (fun le a v => forall p le', insert_lenv le p w le' -> - eval_expr ge sp le' e m1 (lift_expr p a) t m2 v) - (fun sp le e m1 a t m2 vb => + eval_expr ge sp e m le' (lift_expr p a) v) + (fun le a v => forall p le', insert_lenv le p w le' -> - eval_condexpr ge sp le' e m1 (lift_condexpr p a) t m2 vb) - (fun sp le e m1 al t m2 vl => + eval_condexpr ge sp e m le' (lift_condexpr p a) v) + (fun le al vl => forall p le', insert_lenv le p w le' -> - eval_exprlist ge sp le' e m1 (lift_exprlist p al) t m2 vl)); + eval_exprlist ge sp e m le' (lift_exprlist p al) vl)); simpl; intros; eauto with evalexpr. destruct v1; eapply eval_Econdition; eauto with evalexpr; simpl; eauto with evalexpr. - eapply eval_Elet. eauto. apply H2. apply insert_lenv_S; auto. auto. + eapply eval_Elet. eauto. apply H2. apply insert_lenv_S; auto. case (le_gt_dec p n); intro. apply eval_Eletvar. eapply insert_lenv_lookup2; eauto. @@ -133,13 +98,14 @@ Proof. Qed. Lemma eval_lift: - forall sp le e m1 a t m2 v w, - eval_expr ge sp le e m1 a t m2 v -> - eval_expr ge sp (w::le) e m1 (lift a) t m2 v. + forall le a v w, + eval_expr ge sp e m le a v -> + eval_expr ge sp e m (w::le) (lift a) v. Proof. intros. unfold lift. eapply eval_lift_expr. eexact H. apply insert_lenv_0. Qed. + Hint Resolve eval_lift: evalexpr. (** * Useful lemmas and tactics *) @@ -152,75 +118,37 @@ Ltac EvalOp := eapply eval_Eop; eauto with evalexpr. Ltac TrivialOp cstr := unfold cstr; intros; EvalOp. -Lemma inv_eval_Eop_0: - forall sp le e m1 op t m2 v, - eval_expr ge sp le e m1 (Eop op Enil) t m2 v -> - t = E0 /\ m2 = m1 /\ eval_operation ge sp op nil m1 = Some v. -Proof. - intros. inversion H. inversion H6. - intuition. congruence. -Qed. - -Lemma inv_eval_Eop_1: - forall sp le e m1 op t a1 m2 v, - eval_expr ge sp le e m1 (Eop op (a1 ::: Enil)) t m2 v -> - exists v1, - eval_expr ge sp le e m1 a1 t m2 v1 /\ - eval_operation ge sp op (v1 :: nil) m2 = Some v. -Proof. - intros. - inversion H. inversion H6. inversion H18. - subst. exists v1; intuition. rewrite E0_right. auto. -Qed. - -Lemma inv_eval_Eop_2: - forall sp le e m1 op a1 a2 t3 m3 v, - eval_expr ge sp le e m1 (Eop op (a1 ::: a2 ::: Enil)) t3 m3 v -> - exists t1, exists t2, exists m2, exists v1, exists v2, - eval_expr ge sp le e m1 a1 t1 m2 v1 /\ - eval_expr ge sp le e m2 a2 t2 m3 v2 /\ - t3 = t1 ** t2 /\ - eval_operation ge sp op (v1 :: v2 :: nil) m3 = Some v. -Proof. - intros. - inversion H. subst. inversion H6. subst. inversion H8. subst. - inversion H11. subst. - exists t1; exists t0; exists m0; exists v0; exists v1. - intuition. traceEq. -Qed. +Ltac InvEval1 := + match goal with + | [ H: (eval_expr _ _ _ _ _ (Eop _ Enil) _) |- _ ] => + inv H; InvEval1 + | [ H: (eval_expr _ _ _ _ _ (Eop _ (_ ::: Enil)) _) |- _ ] => + inv H; InvEval1 + | [ H: (eval_expr _ _ _ _ _ (Eop _ (_ ::: _ ::: Enil)) _) |- _ ] => + inv H; InvEval1 + | [ H: (eval_exprlist _ _ _ _ _ Enil _) |- _ ] => + inv H; InvEval1 + | [ H: (eval_exprlist _ _ _ _ _ (_ ::: _) _) |- _ ] => + inv H; InvEval1 + | _ => + idtac + end. -Ltac SimplEval := +Ltac InvEval2 := match goal with - | [ |- (eval_expr _ ?sp ?le ?e ?m1 (Eop ?op Enil) ?t ?m2 ?v) -> _] => - intro XX1; - generalize (inv_eval_Eop_0 sp le e m1 op t m2 v XX1); - clear XX1; - intros [XX1 [XX2 XX3]]; - subst t m2; simpl in XX3; - try (simplify_eq XX3; clear XX3; - let EQ := fresh "EQ" in (intro EQ; rewrite EQ)) - | [ |- (eval_expr _ ?sp ?le ?e ?m1 (Eop ?op (?a1 ::: Enil)) ?t ?m2 ?v) -> _] => - intro XX1; - generalize (inv_eval_Eop_1 sp le e m1 op t a1 m2 v XX1); - clear XX1; - let v1 := fresh "v" in let EV := fresh "EV" in - let EQ := fresh "EQ" in - (intros [v1 [EV EQ]]; simpl in EQ) - | [ |- (eval_expr _ ?sp ?le ?e ?m1 (Eop ?op (?a1 ::: ?a2 ::: Enil)) ?t ?m2 ?v) -> _] => - intro XX1; - generalize (inv_eval_Eop_2 sp le e m1 op a1 a2 t m2 v XX1); - clear XX1; - let t1 := fresh "t" in let t2 := fresh "t" in - let m := fresh "m" in - let v1 := fresh "v" in let v2 := fresh "v" in - let EV1 := fresh "EV" in let EV2 := fresh "EV" in - let EQ := fresh "EQ" in let TR := fresh "TR" in - (intros [t1 [t2 [m [v1 [v2 [EV1 [EV2 [TR EQ]]]]]]]]; simpl in EQ) - | _ => idtac + | [ H: (eval_operation _ _ _ nil _ = Some _) |- _ ] => + simpl in H; inv H + | [ H: (eval_operation _ _ _ (_ :: nil) _ = Some _) |- _ ] => + simpl in H; FuncInv + | [ H: (eval_operation _ _ _ (_ :: _ :: nil) _ = Some _) |- _ ] => + simpl in H; FuncInv + | [ H: (eval_operation _ _ _ (_ :: _ :: _ :: nil) _ = Some _) |- _ ] => + simpl in H; FuncInv + | _ => + idtac end. -Ltac InvEval H := - generalize H; SimplEval; clear H. +Ltac InvEval := InvEval1; InvEval2; InvEval2. (** * Correctness of the smart constructors *) @@ -244,31 +172,31 @@ Ltac InvEval H := by the smart constructor. *) -Lemma eval_notint: - forall sp le e m1 a t m2 x, - eval_expr ge sp le e m1 a t m2 (Vint x) -> - eval_expr ge sp le e m1 (notint a) t m2 (Vint (Int.not x)). +Theorem eval_notint: + forall le a x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (notint a) (Vint (Int.not x)). Proof. - unfold notint; intros until x; case (notint_match a); intros. - InvEval H. FuncInv. EvalOp. simpl. congruence. - InvEval H. FuncInv. EvalOp. simpl. congruence. - InvEval H. FuncInv. EvalOp. simpl. congruence. + unfold notint; intros until x; case (notint_match a); intros; InvEval. + EvalOp. simpl. congruence. + EvalOp. simpl. congruence. + EvalOp. simpl. congruence. eapply eval_Elet. eexact H. eapply eval_Eop. eapply eval_Econs. apply eval_Eletvar. simpl. reflexivity. eapply eval_Econs. apply eval_Eletvar. simpl. reflexivity. - apply eval_Enil. reflexivity. reflexivity. - simpl. rewrite Int.or_idem. auto. traceEq. + apply eval_Enil. + simpl. rewrite Int.or_idem. auto. Qed. Lemma eval_notbool_base: - forall sp le e m1 a t m2 v b, - eval_expr ge sp le e m1 a t m2 v -> + forall le a v b, + eval_expr ge sp e m le a v -> Val.bool_of_val v b -> - eval_expr ge sp le e m1 (notbool_base a) t m2 (Val.of_bool (negb b)). + eval_expr ge sp e m le (notbool_base a) (Val.of_bool (negb b)). Proof. TrivialOp notbool_base. simpl. - inversion H0. + inv H0. rewrite Int.eq_false; auto. rewrite Int.eq_true; auto. reflexivity. @@ -277,245 +205,203 @@ Qed. Hint Resolve Val.bool_of_true_val Val.bool_of_false_val Val.bool_of_true_val_inv Val.bool_of_false_val_inv: valboolof. -Lemma eval_notbool: - forall a sp le e m1 t m2 v b, - eval_expr ge sp le e m1 a t m2 v -> +Theorem eval_notbool: + forall le a v b, + eval_expr ge sp e m le a v -> Val.bool_of_val v b -> - eval_expr ge sp le e m1 (notbool a) t m2 (Val.of_bool (negb b)). + eval_expr ge sp e m le (notbool a) (Val.of_bool (negb b)). Proof. - assert (N1: forall v b, Val.is_false v -> Val.bool_of_val v b -> Val.is_true (Val.of_bool (negb b))). - intros. inversion H0; simpl; auto; subst v; simpl in H. - congruence. apply Int.one_not_zero. contradiction. - assert (N2: forall v b, Val.is_true v -> Val.bool_of_val v b -> Val.is_false (Val.of_bool (negb b))). - intros. inversion H0; simpl; auto; subst v; simpl in H. - congruence. - induction a; simpl; intros; try (eapply eval_notbool_base; eauto). destruct o; try (eapply eval_notbool_base; eauto). - destruct e. InvEval H. injection XX3; clear XX3; intro; subst v. - inversion H0. rewrite Int.eq_false; auto. + destruct e0. InvEval. + inv H0. rewrite Int.eq_false; auto. simpl; eauto with evalexpr. rewrite Int.eq_true; simpl; eauto with evalexpr. eapply eval_notbool_base; eauto. - inversion H. subst. - simpl in H11. eapply eval_Eop; eauto. - simpl. caseEq (eval_condition c vl m2); intros. - rewrite H1 in H11. - assert (b0 = b). - destruct b0; inversion H11; subst v; inversion H0; auto. - subst b0. rewrite (Op.eval_negate_condition _ _ _ H1). + inv H. eapply eval_Eop; eauto. + simpl. assert (eval_condition c vl m = Some b). + generalize H6. simpl. + case (eval_condition c vl m); intros. + destruct b0; inv H1; inversion H0; auto; congruence. + congruence. + rewrite (Op.eval_negate_condition _ _ _ H). destruct b; reflexivity. - rewrite H1 in H11; discriminate. - inversion H; eauto 10 with evalexpr valboolof. - inversion H; eauto 10 with evalexpr valboolof. - - inversion H. subst. eapply eval_Econdition with (t2 := t8). eexact H34. - destruct v4; eauto. auto. + inv H. eapply eval_Econdition; eauto. + destruct v1; eauto. Qed. -Lemma eval_addimm: - forall sp le e m1 n a t m2 x, - eval_expr ge sp le e m1 a t m2 (Vint x) -> - eval_expr ge sp le e m1 (addimm n a) t m2 (Vint (Int.add x n)). +Theorem eval_addimm: + forall le n a x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (addimm n a) (Vint (Int.add x n)). Proof. unfold addimm; intros until x. generalize (Int.eq_spec n Int.zero). case (Int.eq n Int.zero); intro. subst n. rewrite Int.add_zero. auto. - case (addimm_match a); intros. - InvEval H0. EvalOp. simpl. rewrite Int.add_commut. auto. - InvEval H0. destruct (Genv.find_symbol ge s); discriminate. - InvEval H0. - destruct sp; simpl in XX3; discriminate. - InvEval H0. FuncInv. EvalOp. simpl. subst x. - rewrite Int.add_assoc. decEq; decEq; decEq. apply Int.add_commut. - EvalOp. + case (addimm_match a); intros; InvEval; EvalOp; simpl. + rewrite Int.add_commut. auto. + destruct (Genv.find_symbol ge s); discriminate. + destruct sp; simpl in H1; discriminate. + subst x. rewrite Int.add_assoc. decEq; decEq; decEq. apply Int.add_commut. Qed. -Lemma eval_addimm_ptr: - forall sp le e m1 n t a m2 b ofs, - eval_expr ge sp le e m1 a t m2 (Vptr b ofs) -> - eval_expr ge sp le e m1 (addimm n a) t m2 (Vptr b (Int.add ofs n)). +Theorem eval_addimm_ptr: + forall le n a b ofs, + eval_expr ge sp e m le a (Vptr b ofs) -> + eval_expr ge sp e m le (addimm n a) (Vptr b (Int.add ofs n)). Proof. unfold addimm; intros until ofs. generalize (Int.eq_spec n Int.zero). case (Int.eq n Int.zero); intro. subst n. rewrite Int.add_zero. auto. - case (addimm_match a); intros. - InvEval H0. - InvEval H0. EvalOp. simpl. - destruct (Genv.find_symbol ge s). - rewrite Int.add_commut. congruence. - discriminate. - InvEval H0. destruct sp; simpl in XX3; try discriminate. - inversion XX3. EvalOp. simpl. decEq. decEq. + case (addimm_match a); intros; InvEval; EvalOp; simpl. + destruct (Genv.find_symbol ge s). + rewrite Int.add_commut. congruence. + discriminate. + destruct sp; simpl in H1; try discriminate. + inv H1. simpl. decEq. decEq. rewrite Int.add_assoc. decEq. apply Int.add_commut. - InvEval H0. FuncInv. subst b0; subst ofs. EvalOp. simpl. - rewrite (Int.add_commut n m). rewrite Int.add_assoc. auto. - EvalOp. + subst. rewrite (Int.add_commut n m0). rewrite Int.add_assoc. auto. Qed. -Lemma eval_add: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - eval_expr ge sp le e m1 (add a b) (t1**t2) m3 (Vint (Int.add x y)). +Theorem eval_add: + forall le a b x y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (add a b) (Vint (Int.add x y)). Proof. - intros until y. unfold add; case (add_match a b); intros. - InvEval H. rewrite Int.add_commut. apply eval_addimm. - rewrite E0_left; assumption. - InvEval H. FuncInv. InvEval H0. FuncInv. - replace (Int.add x y) with (Int.add (Int.add i i0) (Int.add n1 n2)). - apply eval_addimm. EvalOp. + intros until y. + unfold add; case (add_match a b); intros; InvEval. + rewrite Int.add_commut. apply eval_addimm. auto. + replace (Int.add x y) with (Int.add (Int.add i0 i) (Int.add n1 n2)). + apply eval_addimm. EvalOp. subst x; subst y. repeat rewrite Int.add_assoc. decEq. apply Int.add_permut. - InvEval H. FuncInv. - replace (Int.add x y) with (Int.add (Int.add i y) n1). + replace (Int.add x y) with (Int.add (Int.add i y) n1). apply eval_addimm. EvalOp. subst x. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - InvEval H0. FuncInv. - apply eval_addimm. rewrite E0_right. auto. - InvEval H0. FuncInv. - replace (Int.add x y) with (Int.add (Int.add x i) n2). + apply eval_addimm. auto. + replace (Int.add x y) with (Int.add (Int.add x i) n2). apply eval_addimm. EvalOp. subst y. rewrite Int.add_assoc. auto. EvalOp. Qed. -Lemma eval_add_ptr: - forall sp le e m1 a t1 m2 p x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vptr p x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - eval_expr ge sp le e m1 (add a b) (t1**t2) m3 (Vptr p (Int.add x y)). +Theorem eval_add_ptr: + forall le a b p x y, + eval_expr ge sp e m le a (Vptr p x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (add a b) (Vptr p (Int.add x y)). Proof. - intros until y. unfold add; case (add_match a b); intros. - InvEval H. - InvEval H. FuncInv. InvEval H0. FuncInv. - replace (Int.add x y) with (Int.add (Int.add i i0) (Int.add n1 n2)). + intros until y. unfold add; case (add_match a b); intros; InvEval. + replace (Int.add x y) with (Int.add (Int.add i0 i) (Int.add n1 n2)). apply eval_addimm_ptr. subst b0. EvalOp. subst x; subst y. repeat rewrite Int.add_assoc. decEq. apply Int.add_permut. - InvEval H. FuncInv. - replace (Int.add x y) with (Int.add (Int.add i y) n1). + replace (Int.add x y) with (Int.add (Int.add i y) n1). apply eval_addimm_ptr. subst b0. EvalOp. subst x. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - InvEval H0. apply eval_addimm_ptr. rewrite E0_right. auto. - InvEval H0. FuncInv. - replace (Int.add x y) with (Int.add (Int.add x i) n2). + apply eval_addimm_ptr. auto. + replace (Int.add x y) with (Int.add (Int.add x i) n2). apply eval_addimm_ptr. EvalOp. subst y. rewrite Int.add_assoc. auto. EvalOp. Qed. -Lemma eval_add_ptr_2: - forall sp le e m1 a t1 m2 p x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vptr p y) -> - eval_expr ge sp le e m1 (add a b) (t1**t2) m3 (Vptr p (Int.add y x)). +Theorem eval_add_ptr_2: + forall le a b x p y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vptr p y) -> + eval_expr ge sp e m le (add a b) (Vptr p (Int.add y x)). Proof. - intros until y. unfold add; case (add_match a b); intros. - InvEval H. - apply eval_addimm_ptr. rewrite E0_left. auto. - InvEval H. FuncInv. InvEval H0. FuncInv. - replace (Int.add y x) with (Int.add (Int.add i0 i) (Int.add n1 n2)). + intros until y. unfold add; case (add_match a b); intros; InvEval. + apply eval_addimm_ptr. auto. + replace (Int.add y x) with (Int.add (Int.add i i0) (Int.add n1 n2)). apply eval_addimm_ptr. subst b0. EvalOp. subst x; subst y. repeat rewrite Int.add_assoc. decEq. rewrite (Int.add_commut n1 n2). apply Int.add_permut. - InvEval H. FuncInv. - replace (Int.add y x) with (Int.add (Int.add y i) n1). + replace (Int.add y x) with (Int.add (Int.add y i) n1). apply eval_addimm_ptr. EvalOp. subst x. repeat rewrite Int.add_assoc. auto. - InvEval H0. - InvEval H0. FuncInv. - replace (Int.add y x) with (Int.add (Int.add i x) n2). + replace (Int.add y x) with (Int.add (Int.add i x) n2). apply eval_addimm_ptr. EvalOp. subst b0; reflexivity. subst y. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. EvalOp. Qed. -Lemma eval_sub: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - eval_expr ge sp le e m1 (sub a b) (t1**t2) m3 (Vint (Int.sub x y)). +Theorem eval_sub: + forall le a b x y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (sub a b) (Vint (Int.sub x y)). Proof. intros until y. - unfold sub; case (sub_match a b); intros. - InvEval H0. rewrite Int.sub_add_opp. - apply eval_addimm. rewrite E0_right. assumption. - InvEval H. FuncInv. InvEval H0. FuncInv. - replace (Int.sub x y) with (Int.add (Int.sub i i0) (Int.sub n1 n2)). + unfold sub; case (sub_match a b); intros; InvEval. + rewrite Int.sub_add_opp. + apply eval_addimm. assumption. + replace (Int.sub x y) with (Int.add (Int.sub i0 i) (Int.sub n1 n2)). apply eval_addimm. EvalOp. subst x; subst y. repeat rewrite Int.sub_add_opp. repeat rewrite Int.add_assoc. decEq. rewrite Int.add_permut. decEq. symmetry. apply Int.neg_add_distr. - InvEval H. FuncInv. - replace (Int.sub x y) with (Int.add (Int.sub i y) n1). + replace (Int.sub x y) with (Int.add (Int.sub i y) n1). apply eval_addimm. EvalOp. subst x. rewrite Int.sub_add_l. auto. - InvEval H0. FuncInv. - replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)). + replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)). apply eval_addimm. EvalOp. subst y. rewrite (Int.add_commut i n2). symmetry. apply Int.sub_add_r. EvalOp. Qed. -Lemma eval_sub_ptr_int: - forall sp le e m1 a t1 m2 p x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vptr p x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - eval_expr ge sp le e m1 (sub a b) (t1**t2) m3 (Vptr p (Int.sub x y)). +Theorem eval_sub_ptr_int: + forall le a b p x y, + eval_expr ge sp e m le a (Vptr p x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (sub a b) (Vptr p (Int.sub x y)). Proof. intros until y. - unfold sub; case (sub_match a b); intros. - InvEval H0. rewrite Int.sub_add_opp. - apply eval_addimm_ptr. rewrite E0_right. assumption. - InvEval H. FuncInv. InvEval H0. FuncInv. - subst b0. - replace (Int.sub x y) with (Int.add (Int.sub i i0) (Int.sub n1 n2)). + unfold sub; case (sub_match a b); intros; InvEval. + rewrite Int.sub_add_opp. + apply eval_addimm_ptr. assumption. + subst b0. replace (Int.sub x y) with (Int.add (Int.sub i0 i) (Int.sub n1 n2)). apply eval_addimm_ptr. EvalOp. subst x; subst y. repeat rewrite Int.sub_add_opp. repeat rewrite Int.add_assoc. decEq. rewrite Int.add_permut. decEq. symmetry. apply Int.neg_add_distr. - InvEval H. FuncInv. subst b0. - replace (Int.sub x y) with (Int.add (Int.sub i y) n1). + subst b0. replace (Int.sub x y) with (Int.add (Int.sub i y) n1). apply eval_addimm_ptr. EvalOp. subst x. rewrite Int.sub_add_l. auto. - InvEval H0. FuncInv. - replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)). + replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)). apply eval_addimm_ptr. EvalOp. subst y. rewrite (Int.add_commut i n2). symmetry. apply Int.sub_add_r. EvalOp. Qed. -Lemma eval_sub_ptr_ptr: - forall sp le e m1 a t1 m2 p x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vptr p x) -> - eval_expr ge sp le e m2 b t2 m3 (Vptr p y) -> - eval_expr ge sp le e m1 (sub a b) (t1**t2) m3 (Vint (Int.sub x y)). +Theorem eval_sub_ptr_ptr: + forall le a b p x y, + eval_expr ge sp e m le a (Vptr p x) -> + eval_expr ge sp e m le b (Vptr p y) -> + eval_expr ge sp e m le (sub a b) (Vint (Int.sub x y)). Proof. intros until y. - unfold sub; case (sub_match a b); intros. - InvEval H0. - InvEval H. FuncInv. InvEval H0. FuncInv. - replace (Int.sub x y) with (Int.add (Int.sub i i0) (Int.sub n1 n2)). + unfold sub; case (sub_match a b); intros; InvEval. + replace (Int.sub x y) with (Int.add (Int.sub i0 i) (Int.sub n1 n2)). apply eval_addimm. EvalOp. simpl; unfold eq_block. subst b0; subst b1; rewrite zeq_true. auto. subst x; subst y. repeat rewrite Int.sub_add_opp. repeat rewrite Int.add_assoc. decEq. rewrite Int.add_permut. decEq. symmetry. apply Int.neg_add_distr. - InvEval H. FuncInv. subst b0. - replace (Int.sub x y) with (Int.add (Int.sub i y) n1). + subst b0. replace (Int.sub x y) with (Int.add (Int.sub i y) n1). apply eval_addimm. EvalOp. simpl. unfold eq_block. rewrite zeq_true. auto. subst x. rewrite Int.sub_add_l. auto. - InvEval H0. FuncInv. subst b0. - replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)). + subst b0. replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)). apply eval_addimm. EvalOp. simpl. unfold eq_block. rewrite zeq_true. auto. subst y. rewrite (Int.add_commut i n2). symmetry. apply Int.sub_add_r. @@ -523,29 +409,29 @@ Proof. Qed. Lemma eval_rolm: - forall sp le e m1 a amount mask t m2 x, - eval_expr ge sp le e m1 a t m2 (Vint x) -> - eval_expr ge sp le e m1 (rolm a amount mask) t m2 (Vint (Int.rolm x amount mask)). + forall le a amount mask x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (rolm a amount mask) (Vint (Int.rolm x amount mask)). Proof. - intros until x. unfold rolm; case (rolm_match a); intros. - InvEval H. eauto with evalexpr. + intros until x. unfold rolm; case (rolm_match a); intros; InvEval. + eauto with evalexpr. case (Int.is_rlw_mask (Int.and (Int.rol mask1 amount) mask)). - InvEval H. FuncInv. EvalOp. simpl. subst x. + EvalOp. simpl. subst x. decEq. decEq. replace (Int.and (Int.add amount1 amount) (Int.repr 31)) with (Int.modu (Int.add amount1 amount) (Int.repr 32)). symmetry. apply Int.rolm_rolm. change (Int.repr 31) with (Int.sub (Int.repr 32) Int.one). apply Int.modu_and with (Int.repr 5). reflexivity. - EvalOp. + EvalOp. econstructor. EvalOp. simpl. rewrite H. reflexivity. constructor. auto. EvalOp. Qed. -Lemma eval_shlimm: - forall sp le e m1 a n t m2 x, - eval_expr ge sp le e m1 a t m2 (Vint x) -> +Theorem eval_shlimm: + forall le a n x, + eval_expr ge sp e m le a (Vint x) -> Int.ltu n (Int.repr 32) = true -> - eval_expr ge sp le e m1 (shlimm a n) t m2 (Vint (Int.shl x n)). + eval_expr ge sp e m le (shlimm a n) (Vint (Int.shl x n)). Proof. intros. unfold shlimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro. @@ -555,11 +441,11 @@ Proof. apply eval_rolm. auto. symmetry. apply Int.shl_rolm. exact H0. Qed. -Lemma eval_shruimm: - forall sp le e m1 a n t m2 x, - eval_expr ge sp le e m1 a t m2 (Vint x) -> +Theorem eval_shruimm: + forall le a n x, + eval_expr ge sp e m le a (Vint x) -> Int.ltu n (Int.repr 32) = true -> - eval_expr ge sp le e m1 (shruimm a n) t m2 (Vint (Int.shru x n)). + eval_expr ge sp e m le (shruimm a n) (Vint (Int.shru x n)). Proof. intros. unfold shruimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro. @@ -570,9 +456,9 @@ Proof. Qed. Lemma eval_mulimm_base: - forall sp le e m1 a t n m2 x, - eval_expr ge sp le e m1 a t m2 (Vint x) -> - eval_expr ge sp le e m1 (mulimm_base n a) t m2 (Vint (Int.mul x n)). + forall le a n x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (mulimm_base n a) (Vint (Int.mul x n)). Proof. intros; unfold mulimm_base. generalize (Int.one_bits_decomp n). @@ -585,7 +471,7 @@ Proof. rewrite Int.add_zero. rewrite <- Int.shl_mul. apply eval_shlimm. auto. auto with coqlib. destruct l. - intros. apply eval_Elet with t m2 (Vint x) E0. auto. + intros. apply eval_Elet with (Vint x). auto. rewrite H1. simpl. rewrite Int.add_zero. rewrite Int.mul_add_distr_r. rewrite <- Int.shl_mul. @@ -597,50 +483,48 @@ Proof. apply eval_shlimm. apply eval_Eletvar. simpl. reflexivity. auto with coqlib. auto with evalexpr. - reflexivity. traceEq. reflexivity. traceEq. + reflexivity. intros. EvalOp. Qed. -Lemma eval_mulimm: - forall sp le e m1 a n t m2 x, - eval_expr ge sp le e m1 a t m2 (Vint x) -> - eval_expr ge sp le e m1 (mulimm n a) t m2 (Vint (Int.mul x n)). +Theorem eval_mulimm: + forall le a n x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (mulimm n a) (Vint (Int.mul x n)). Proof. intros until x; unfold mulimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro. subst n. rewrite Int.mul_zero. - intro. eapply eval_Elet; eauto with evalexpr. traceEq. + intro. eapply eval_Elet; eauto with evalexpr. generalize (Int.eq_spec n Int.one); case (Int.eq n Int.one); intro. subst n. rewrite Int.mul_one. auto. - case (mulimm_match a); intros. - InvEval H1. EvalOp. rewrite Int.mul_commut. reflexivity. - InvEval H1. FuncInv. + case (mulimm_match a); intros; InvEval. + EvalOp. rewrite Int.mul_commut. reflexivity. replace (Int.mul x n) with (Int.add (Int.mul i n) (Int.mul n n2)). apply eval_addimm. apply eval_mulimm_base. auto. subst x. rewrite Int.mul_add_distr_l. decEq. apply Int.mul_commut. apply eval_mulimm_base. assumption. Qed. -Lemma eval_mul: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - eval_expr ge sp le e m1 (mul a b) (t1**t2) m3 (Vint (Int.mul x y)). +Theorem eval_mul: + forall le a b x y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (mul a b) (Vint (Int.mul x y)). Proof. intros until y. - unfold mul; case (mul_match a b); intros. - InvEval H. rewrite Int.mul_commut. apply eval_mulimm. - rewrite E0_left; auto. - InvEval H0. rewrite E0_right. apply eval_mulimm. auto. + unfold mul; case (mul_match a b); intros; InvEval. + rewrite Int.mul_commut. apply eval_mulimm. auto. + apply eval_mulimm. auto. EvalOp. Qed. -Lemma eval_divs: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> +Theorem eval_divs: + forall le a b x y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> y <> Int.zero -> - eval_expr ge sp le e m1 (divs a b) (t1**t2) m3 (Vint (Int.divs x y)). + eval_expr ge sp e m le (divs a b) (Vint (Int.divs x y)). Proof. TrivialOp divs. simpl. predSpec Int.eq Int.eq_spec y Int.zero. contradiction. auto. @@ -652,11 +536,11 @@ Lemma eval_mod_aux: y <> Int.zero -> eval_operation ge sp divop (Vint x :: Vint y :: nil) m = Some (Vint (semdivop x y))) -> - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> + forall le a b x y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> y <> Int.zero -> - eval_expr ge sp le e m1 (mod_aux divop a b) (t1**t2) m3 + eval_expr ge sp e m le (mod_aux divop a b) (Vint (Int.sub x (Int.mul (semdivop x y) y))). Proof. intros; unfold mod_aux. @@ -668,21 +552,20 @@ Proof. eapply eval_Econs. eapply eval_Eop. eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. - apply eval_Enil. reflexivity. reflexivity. + apply eval_Enil. apply H. assumption. eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. - apply eval_Enil. reflexivity. reflexivity. + apply eval_Enil. simpl; reflexivity. apply eval_Enil. - reflexivity. reflexivity. reflexivity. - reflexivity. traceEq. + reflexivity. Qed. -Lemma eval_mods: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> +Theorem eval_mods: + forall le a b x y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> y <> Int.zero -> - eval_expr ge sp le e m1 (mods a b) (t1**t2) m3 (Vint (Int.mods x y)). + eval_expr ge sp e m le (mods a b) (Vint (Int.mods x y)). Proof. intros; unfold mods. rewrite Int.mods_divs. @@ -692,232 +575,217 @@ Proof. Qed. Lemma eval_divu_base: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> y <> Int.zero -> - eval_expr ge sp le e m1 (Eop Odivu (a ::: b ::: Enil)) (t1**t2) m3 (Vint (Int.divu x y)). + eval_expr ge sp e m le (Eop Odivu (a ::: b ::: Enil)) (Vint (Int.divu x y)). Proof. intros. EvalOp. simpl. predSpec Int.eq Int.eq_spec y Int.zero. contradiction. auto. Qed. -Lemma eval_divu: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> +Theorem eval_divu: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> y <> Int.zero -> - eval_expr ge sp le e m1 (divu a b) (t1**t2) m3 (Vint (Int.divu x y)). + eval_expr ge sp e m le (divu a b) (Vint (Int.divu x y)). Proof. intros until y. - unfold divu; case (divu_match b); intros. - InvEval H0. caseEq (Int.is_power2 y). + unfold divu; case (divu_match b); intros; InvEval. + caseEq (Int.is_power2 y). intros. rewrite (Int.divu_pow2 x y i H0). - apply eval_shruimm. rewrite E0_right. auto. + apply eval_shruimm. auto. apply Int.is_power2_range with y. auto. - intros. subst n2. eapply eval_divu_base. eexact H. EvalOp. auto. + intros. apply eval_divu_base. auto. EvalOp. auto. eapply eval_divu_base; eauto. Qed. -Lemma eval_modu: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> +Theorem eval_modu: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> y <> Int.zero -> - eval_expr ge sp le e m1 (modu a b) (t1**t2) m3 (Vint (Int.modu x y)). + eval_expr ge sp e m le (modu a b) (Vint (Int.modu x y)). Proof. - intros until y; unfold modu; case (divu_match b); intros. - InvEval H0. caseEq (Int.is_power2 y). + intros until y; unfold modu; case (divu_match b); intros; InvEval. + caseEq (Int.is_power2 y). intros. rewrite (Int.modu_and x y i H0). - rewrite <- Int.rolm_zero. apply eval_rolm. rewrite E0_right; auto. + rewrite <- Int.rolm_zero. apply eval_rolm. auto. intro. rewrite Int.modu_divu. eapply eval_mod_aux. intros. simpl. predSpec Int.eq Int.eq_spec y0 Int.zero. contradiction. auto. - eexact H. EvalOp. auto. auto. + auto. EvalOp. auto. auto. rewrite Int.modu_divu. eapply eval_mod_aux. intros. simpl. predSpec Int.eq Int.eq_spec y0 Int.zero. - contradiction. auto. - eexact H. eexact H0. auto. auto. + contradiction. auto. auto. auto. auto. auto. Qed. -Lemma eval_andimm: - forall sp le e m1 n a t m2 x, - eval_expr ge sp le e m1 a t m2 (Vint x) -> - eval_expr ge sp le e m1 (andimm n a) t m2 (Vint (Int.and x n)). +Theorem eval_andimm: + forall le n a x, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le (andimm n a) (Vint (Int.and x n)). Proof. intros. unfold andimm. case (Int.is_rlw_mask n). rewrite <- Int.rolm_zero. apply eval_rolm; auto. EvalOp. Qed. -Lemma eval_and: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - eval_expr ge sp le e m1 (and a b) (t1**t2) m3 (Vint (Int.and x y)). +Theorem eval_and: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (and a b) (Vint (Int.and x y)). Proof. - intros until y; unfold and; case (mul_match a b); intros. - InvEval H. rewrite Int.and_commut. - rewrite E0_left; apply eval_andimm; auto. - InvEval H0. rewrite E0_right; apply eval_andimm; auto. + intros until y; unfold and; case (mul_match a b); intros; InvEval. + rewrite Int.and_commut. apply eval_andimm; auto. + apply eval_andimm; auto. EvalOp. Qed. -Remark eval_same_expr_pure: - forall a1 a2 sp le e m1 t1 m2 v1 t2 m3 v2, +Remark eval_same_expr: + forall a1 a2 le v1 v2, same_expr_pure a1 a2 = true -> - eval_expr ge sp le e m1 a1 t1 m2 v1 -> - eval_expr ge sp le e m2 a2 t2 m3 v2 -> - t1 = E0 /\ t2 = E0 /\ a2 = a1 /\ v2 = v1 /\ m2 = m1. + eval_expr ge sp e m le a1 v1 -> + eval_expr ge sp e m le a2 v2 -> + a1 = a2 /\ v1 = v2. Proof. intros until v2. destruct a1; simpl; try (intros; discriminate). destruct a2; simpl; try (intros; discriminate). case (ident_eq i i0); intros. - subst i0. inversion H0. inversion H1. - assert (v2 = v1). congruence. tauto. + subst i0. inversion H0. inversion H1. split. auto. congruence. discriminate. Qed. Lemma eval_or: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> - eval_expr ge sp le e m1 (or a b) (t1**t2) m3 (Vint (Int.or x y)). + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (or a b) (Vint (Int.or x y)). Proof. - intros until y; unfold or; case (or_match a b); intros. - generalize (Int.eq_spec amount1 amount2); case (Int.eq amount1 amount2); intro. - case (Int.is_rlw_mask (Int.or mask1 mask2)). - caseEq (same_expr_pure t0 t3); intro. - simpl. InvEval H. FuncInv. InvEval H0. FuncInv. - generalize (eval_same_expr_pure _ _ _ _ _ _ _ _ _ _ _ _ H2 EV EV0). - intros [EQ1 [EQ2 [EQ3 [EQ4 EQ5]]]]. - injection EQ4; intro EQ7. subst. - EvalOp. simpl. rewrite Int.or_rolm. auto. - simpl. EvalOp. - simpl. EvalOp. - simpl. EvalOp. + intros until y; unfold or; case (or_match a b); intros; InvEval. + caseEq (Int.eq amount1 amount2 + && Int.is_rlw_mask (Int.or mask1 mask2) + && same_expr_pure t1 t2); intro. + destruct (andb_prop _ _ H1). destruct (andb_prop _ _ H4). + generalize (Int.eq_spec amount1 amount2). rewrite H6. intro. subst amount2. + exploit eval_same_expr; eauto. intros [EQ1 EQ2]. inv EQ1. inv EQ2. + simpl. EvalOp. simpl. rewrite Int.or_rolm. auto. + simpl. apply eval_Eop with (Vint x :: Vint y :: nil). + econstructor. EvalOp. simpl. congruence. + econstructor. EvalOp. simpl. congruence. constructor. auto. EvalOp. Qed. -Lemma eval_shl: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> +Theorem eval_shl: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> Int.ltu y (Int.repr 32) = true -> - eval_expr ge sp le e m1 (shl a b) (t1**t2) m3 (Vint (Int.shl x y)). + eval_expr ge sp e m le (shl a b) (Vint (Int.shl x y)). Proof. intros until y; unfold shl; case (shift_match b); intros. - InvEval H0. rewrite E0_right. apply eval_shlimm; auto. + InvEval. apply eval_shlimm; auto. EvalOp. simpl. rewrite H1. auto. Qed. -Lemma eval_shru: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vint x) -> - eval_expr ge sp le e m2 b t2 m3 (Vint y) -> +Theorem eval_shru: + forall le a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> Int.ltu y (Int.repr 32) = true -> - eval_expr ge sp le e m1 (shru a b) (t1**t2) m3 (Vint (Int.shru x y)). + eval_expr ge sp e m le (shru a b) (Vint (Int.shru x y)). Proof. intros until y; unfold shru; case (shift_match b); intros. - InvEval H0. rewrite E0_right; apply eval_shruimm; auto. + InvEval. apply eval_shruimm; auto. EvalOp. simpl. rewrite H1. auto. Qed. -Lemma eval_addf: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vfloat x) -> - eval_expr ge sp le e m2 b t2 m3 (Vfloat y) -> - eval_expr ge sp le e m1 (addf a b) (t1**t2) m3 (Vfloat (Float.add x y)). +Theorem eval_addf: + forall le a x b y, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le b (Vfloat y) -> + eval_expr ge sp e m le (addf a b) (Vfloat (Float.add x y)). Proof. - intros until y; unfold addf; case (addf_match a b); intros. - InvEval H. FuncInv. EvalOp. - econstructor; eauto. econstructor; eauto. econstructor; eauto. constructor. - traceEq. simpl. subst x. reflexivity. - InvEval H0. FuncInv. eapply eval_Elet. eexact H. EvalOp. - econstructor; eauto with evalexpr. - econstructor; eauto with evalexpr. - econstructor. apply eval_Eletvar. simpl; reflexivity. - constructor. reflexivity. traceEq. - subst y. rewrite Float.addf_commut. reflexivity. auto. + intros until y; unfold addf; case (addf_match a b); intros; InvEval. + EvalOp. simpl. congruence. + econstructor. eauto. EvalOp. econstructor. eauto with evalexpr. + econstructor. eauto with evalexpr. econstructor. + econstructor. simpl. reflexivity. constructor. + simpl. subst y. rewrite Float.addf_commut. auto. EvalOp. Qed. -Lemma eval_subf: - forall sp le e m1 a t1 m2 x b t2 m3 y, - eval_expr ge sp le e m1 a t1 m2 (Vfloat x) -> - eval_expr ge sp le e m2 b t2 m3 (Vfloat y) -> - eval_expr ge sp le e m1 (subf a b) (t1**t2) m3 (Vfloat (Float.sub x y)). +Theorem eval_subf: + forall le a x b y, + eval_expr ge sp e m le a (Vfloat x) -> + eval_expr ge sp e m le b (Vfloat y) -> + eval_expr ge sp e m le (subf a b) (Vfloat (Float.sub x y)). Proof. intros until y; unfold subf; case (subf_match a b); intros. - InvEval H. FuncInv. EvalOp. - econstructor; eauto. econstructor; eauto. econstructor; eauto. constructor. - traceEq. subst x. reflexivity. + InvEval. EvalOp. simpl. congruence. EvalOp. Qed. -Lemma eval_cast8signed: - forall sp le e m1 a t m2 v, - eval_expr ge sp le e m1 a t m2 v -> - eval_expr ge sp le e m1 (cast8signed a) t m2 (Val.cast8signed v). +Theorem eval_cast8signed: + forall le a v, + eval_expr ge sp e m le a v -> + eval_expr ge sp e m le (cast8signed a) (Val.cast8signed v). Proof. - intros until v; unfold cast8signed; case (cast8signed_match a); intros. - replace (Val.cast8signed v) with v. auto. - InvEval H. inversion EQ. destruct v0; simpl; auto. rewrite Int.cast8_signed_idem. reflexivity. + intros until v; unfold cast8signed; case (cast8signed_match a); intros; InvEval. + EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.cast8_signed_idem. reflexivity. EvalOp. Qed. -Lemma eval_cast8unsigned: - forall sp le e m1 a t m2 v, - eval_expr ge sp le e m1 a t m2 v -> - eval_expr ge sp le e m1 (cast8unsigned a) t m2 (Val.cast8unsigned v). +Theorem eval_cast8unsigned: + forall le a v, + eval_expr ge sp e m le a v -> + eval_expr ge sp e m le (cast8unsigned a) (Val.cast8unsigned v). Proof. - intros until v; unfold cast8unsigned; case (cast8unsigned_match a); intros. - replace (Val.cast8unsigned v) with v. auto. - InvEval H. inversion EQ. destruct v0; simpl; auto. rewrite Int.cast8_unsigned_idem. reflexivity. + intros until v; unfold cast8unsigned; case (cast8unsigned_match a); intros; InvEval. + EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.cast8_unsigned_idem. reflexivity. EvalOp. Qed. -Lemma eval_cast16signed: - forall sp le e m1 a t m2 v, - eval_expr ge sp le e m1 a t m2 v -> - eval_expr ge sp le e m1 (cast16signed a) t m2 (Val.cast16signed v). +Theorem eval_cast16signed: + forall le a v, + eval_expr ge sp e m le a v -> + eval_expr ge sp e m le (cast16signed a) (Val.cast16signed v). Proof. - intros until v; unfold cast16signed; case (cast16signed_match a); intros. - replace (Val.cast16signed v) with v. auto. - InvEval H. inversion EQ. destruct v0; simpl; auto. rewrite Int.cast16_signed_idem. reflexivity. + intros until v; unfold cast16signed; case (cast16signed_match a); intros; InvEval. + EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.cast16_signed_idem. reflexivity. EvalOp. Qed. -Lemma eval_cast16unsigned: - forall sp le e m1 a t m2 v, - eval_expr ge sp le e m1 a t m2 v -> - eval_expr ge sp le e m1 (cast16unsigned a) t m2 (Val.cast16unsigned v). +Theorem eval_cast16unsigned: + forall le a v, + eval_expr ge sp e m le a v -> + eval_expr ge sp e m le (cast16unsigned a) (Val.cast16unsigned v). Proof. - intros until v; unfold cast16unsigned; case (cast16unsigned_match a); intros. - replace (Val.cast16unsigned v) with v. auto. - InvEval H. inversion EQ. destruct v0; simpl; auto. rewrite Int.cast16_unsigned_idem. reflexivity. + intros until v; unfold cast16unsigned; case (cast16unsigned_match a); intros; InvEval. + EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.cast16_unsigned_idem. reflexivity. EvalOp. Qed. -Lemma eval_singleoffloat: - forall sp le e m1 a t m2 v, - eval_expr ge sp le e m1 a t m2 v -> - eval_expr ge sp le e m1 (singleoffloat a) t m2 (Val.singleoffloat v). +Theorem eval_singleoffloat: + forall le a v, + eval_expr ge sp e m le a v -> + eval_expr ge sp e m le (singleoffloat a) (Val.singleoffloat v). Proof. - intros until v; unfold singleoffloat; case (singleoffloat_match a); intros. - replace (Val.singleoffloat v) with v. auto. - InvEval H. inversion EQ. destruct v0; simpl; auto. rewrite Float.singleoffloat_idem. reflexivity. + intros until v; unfold singleoffloat; case (singleoffloat_match a); intros; InvEval. + EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Float.singleoffloat_idem. reflexivity. EvalOp. Qed. Lemma eval_base_condition_of_expr: - forall sp le a e m1 t m2 v (b: bool), - eval_expr ge sp le e m1 a t m2 v -> + forall le a v b, + eval_expr ge sp e m le a v -> Val.bool_of_val v b -> - eval_condexpr ge sp le e m1 + eval_condexpr ge sp e m le (CEcond (Ccompimm Cne Int.zero) (a ::: Enil)) - t m2 b. + b. Proof. intros. eapply eval_CEcond. eauto with evalexpr. @@ -925,90 +793,81 @@ Proof. Qed. Lemma eval_condition_of_expr: - forall a sp le e m1 t m2 v (b: bool), - eval_expr ge sp le e m1 a t m2 v -> + forall a le v b, + eval_expr ge sp e m le a v -> Val.bool_of_val v b -> - eval_condexpr ge sp le e m1 (condexpr_of_expr a) t m2 b. + eval_condexpr ge sp e m le (condexpr_of_expr a) b. Proof. induction a; simpl; intros; try (eapply eval_base_condition_of_expr; eauto; fail). + destruct o; try (eapply eval_base_condition_of_expr; eauto; fail). - destruct e. InvEval H. inversion XX3; subst v. + destruct e0. InvEval. inversion H0. rewrite Int.eq_false; auto. constructor. subst i; rewrite Int.eq_true. constructor. eapply eval_base_condition_of_expr; eauto. - inversion H. subst. eapply eval_CEcond; eauto. simpl in H11. - destruct (eval_condition c vl); try discriminate. - destruct b0; inversion H11; subst; inversion H0; congruence. + inv H. eapply eval_CEcond; eauto. simpl in H6. + destruct (eval_condition c vl m); try discriminate. + destruct b0; inv H6; inversion H0; congruence. - inversion H. subst. - destruct v1; eauto with evalexpr. + inv H. destruct v1; eauto with evalexpr. Qed. Lemma eval_addressing: - forall sp le e m1 a t m2 v b ofs, - eval_expr ge sp le e m1 a t m2 v -> + forall le a v b ofs, + eval_expr ge sp e m le a v -> v = Vptr b ofs -> match addressing a with (mode, args) => exists vl, - eval_exprlist ge sp le e m1 args t m2 vl /\ + eval_exprlist ge sp e m le args vl /\ eval_addressing ge sp mode vl = Some v end. Proof. - intros until v. unfold addressing; case (addressing_match a); intros. - InvEval H. exists (@nil val). split. eauto with evalexpr. - simpl. auto. - InvEval H. exists (@nil val). split. eauto with evalexpr. - simpl. auto. - InvEval H. InvEval EV. rewrite E0_left in TR. subst t1. FuncInv. - congruence. - destruct (Genv.find_symbol ge s); congruence. - exists (Vint i0 :: nil). split. eauto with evalexpr. - simpl. subst v. destruct (Genv.find_symbol ge s). congruence. - discriminate. - InvEval H. FuncInv. - congruence. - exists (Vptr b0 i :: nil). split. eauto with evalexpr. + intros until v. unfold addressing; case (addressing_match a); intros; InvEval. + exists (@nil val). split. eauto with evalexpr. simpl. auto. + exists (@nil val). split. eauto with evalexpr. simpl. auto. + destruct (Genv.find_symbol ge s); congruence. + exists (Vint i0 :: nil). split. eauto with evalexpr. + simpl. destruct (Genv.find_symbol ge s). congruence. discriminate. + exists (Vptr b0 i :: nil). split. eauto with evalexpr. simpl. congruence. - InvEval H. FuncInv. - congruence. - exists (Vint i :: Vptr b0 i0 :: nil). + exists (Vint i :: Vptr b0 i0 :: nil). split. eauto with evalexpr. simpl. rewrite Int.add_commut. congruence. - exists (Vptr b0 i :: Vint i0 :: nil). + exists (Vptr b0 i :: Vint i0 :: nil). split. eauto with evalexpr. simpl. congruence. exists (v :: nil). split. eauto with evalexpr. subst v. simpl. rewrite Int.add_zero. auto. Qed. Lemma eval_load: - forall sp le e m1 a t m2 v chunk v', - eval_expr ge sp le e m1 a t m2 v -> - Mem.loadv chunk m2 v = Some v' -> - eval_expr ge sp le e m1 (load chunk a) t m2 v'. + forall le a v chunk v', + eval_expr ge sp e m le a v -> + Mem.loadv chunk m v = Some v' -> + eval_expr ge sp e m le (load chunk a) v'. Proof. intros. generalize H0; destruct v; simpl; intro; try discriminate. unfold load. - generalize (eval_addressing _ _ _ _ _ _ _ _ _ _ H (refl_equal _)). + generalize (eval_addressing _ _ _ _ _ H (refl_equal _)). destruct (addressing a). intros [vl [EV EQ]]. eapply eval_Eload; eauto. Qed. Lemma eval_store: - forall sp le e m1 a1 t1 m2 v1 a2 t2 m3 v2 chunk m4, - eval_expr ge sp le e m1 a1 t1 m2 v1 -> - eval_expr ge sp le e m2 a2 t2 m3 v2 -> - Mem.storev chunk m3 v1 v2 = Some m4 -> - eval_expr ge sp le e m1 (store chunk a1 a2) (t1**t2) m4 v2. + forall chunk a1 a2 v1 v2 m', + eval_expr ge sp e m nil a1 v1 -> + eval_expr ge sp e m nil a2 v2 -> + Mem.storev chunk m v1 v2 = Some m' -> + exec_stmt ge sp e m (store chunk a1 a2) E0 e m' Out_normal. Proof. intros. generalize H1; destruct v1; simpl; intro; try discriminate. unfold store. - generalize (eval_addressing _ _ _ _ _ _ _ _ _ _ H (refl_equal _)). + generalize (eval_addressing _ _ _ _ _ H (refl_equal _)). destruct (addressing a1). intros [vl [EV EQ]]. - eapply eval_Estore; eauto. + eapply exec_Sstore; eauto. Qed. (** * Correctness of instruction selection for operators *) @@ -1018,10 +877,10 @@ Qed. the results of the previous section. *) Lemma eval_sel_unop: - forall sp le e m op a1 t m1 v1 v, - eval_expr ge sp le e m a1 t m1 v1 -> + forall le op a1 v1 v, + eval_expr ge sp e m le a1 v1 -> eval_unop op v1 = Some v -> - eval_expr ge sp le e m (sel_unop op a1) t m1 v. + eval_expr ge sp e m le (sel_unop op a1) v. Proof. destruct op; simpl; intros; FuncInv; try subst v. apply eval_cast8unsigned; auto. @@ -1044,39 +903,39 @@ Proof. Qed. Lemma eval_sel_binop: - forall sp le e m op a1 a2 t1 m1 v1 t2 m2 v2 v, - eval_expr ge sp le e m a1 t1 m1 v1 -> - eval_expr ge sp le e m1 a2 t2 m2 v2 -> - eval_binop op v1 v2 m2 = Some v -> - eval_expr ge sp le e m (sel_binop op a1 a2) (t1 ** t2) m2 v. + forall le op a1 a2 v1 v2 v, + eval_expr ge sp e m le a1 v1 -> + eval_expr ge sp e m le a2 v2 -> + eval_binop op v1 v2 m = Some v -> + eval_expr ge sp e m le (sel_binop op a1 a2) v. Proof. destruct op; simpl; intros; FuncInv; try subst v. - eapply eval_add; eauto. - eapply eval_add_ptr_2; eauto. - eapply eval_add_ptr; eauto. - eapply eval_sub; eauto. - eapply eval_sub_ptr_int; eauto. + apply eval_add; auto. + apply eval_add_ptr_2; auto. + apply eval_add_ptr; auto. + apply eval_sub; auto. + apply eval_sub_ptr_int; auto. destruct (eq_block b b0); inv H1. eapply eval_sub_ptr_ptr; eauto. - eapply eval_mul; eauto. - generalize (Int.eq_spec i0 Int.zero). intro. destruct (Int.eq i0 Int.zero); inv H1. - eapply eval_divs; eauto. - generalize (Int.eq_spec i0 Int.zero). intro. destruct (Int.eq i0 Int.zero); inv H1. - eapply eval_divu; eauto. - generalize (Int.eq_spec i0 Int.zero). intro. destruct (Int.eq i0 Int.zero); inv H1. - eapply eval_mods; eauto. - generalize (Int.eq_spec i0 Int.zero). intro. destruct (Int.eq i0 Int.zero); inv H1. - eapply eval_modu; eauto. - eapply eval_and; eauto. - eapply eval_or; eauto. + apply eval_mul; eauto. + generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1. + apply eval_divs; eauto. + generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1. + apply eval_divu; eauto. + generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1. + apply eval_mods; eauto. + generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1. + apply eval_modu; eauto. + apply eval_and; auto. + apply eval_or; auto. EvalOp. caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1. - eapply eval_shl; eauto. + apply eval_shl; auto. EvalOp. caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1. - eapply eval_shru; eauto. - eapply eval_addf; eauto. - eapply eval_subf; eauto. + apply eval_shru; auto. + apply eval_addf; auto. + apply eval_subf; auto. EvalOp. EvalOp. EvalOp. simpl. destruct (Int.cmp c i i0); auto. @@ -1087,7 +946,7 @@ Proof. destruct (Int.eq i0 Int.zero). destruct c; intro EQ; inv EQ; auto. auto. EvalOp. simpl. - destruct (valid_pointer m2 b (Int.signed i) && valid_pointer m2 b0 (Int.signed i0)). + destruct (valid_pointer m b (Int.signed i) && valid_pointer m b0 (Int.signed i0)). destruct (eq_block b b0); inv H1. destruct (Int.cmp c i i0); auto. auto. @@ -1141,21 +1000,15 @@ Proof. intros. destruct f; reflexivity. Qed. -(** This is the main semantic preservation theorem: - instruction selection preserves the semantics of function invocations. - The proof is an induction over the Cminor evaluation derivation. *) +(** Semantic preservation for expressions. *) -Lemma sel_function_correct: - forall m fd vargs t m' vres, - Cminor.eval_funcall ge m fd vargs t m' vres -> - CminorSel.eval_funcall tge m (sel_fundef fd) vargs t m' vres. +Lemma sel_expr_correct: + forall sp e m a v, + Cminor.eval_expr ge sp e m a v -> + forall le, + eval_expr tge sp e m le (sel_expr a) v. Proof. - apply (Cminor.eval_funcall_ind4 ge - (fun sp le e m a t m' v => eval_expr tge sp le e m (sel_expr a) t m' v) - (fun sp le e m a t m' v => eval_exprlist tge sp le e m (sel_exprlist a) t m' v) - (fun m fd vargs t m' vres => eval_funcall tge m (sel_fundef fd) vargs t m' vres) - (fun sp e m s t e' m' out => exec_stmt tge sp e m (sel_stmt s) t e' m' out)); - intros; simpl. + induction 1; intros; simpl. (* Evar *) constructor; auto. (* Econst *) @@ -1164,40 +1017,65 @@ Proof. (* Eunop *) eapply eval_sel_unop; eauto. (* Ebinop *) - subst t. eapply eval_sel_binop; eauto. + eapply eval_sel_binop; eauto. (* Eload *) eapply eval_load; eauto. - (* Estore *) - subst t. eapply eval_store; eauto. - (* Ecall *) - econstructor; eauto. apply functions_translated; auto. - rewrite <- H4. apply sig_function_translated. (* Econdition *) econstructor; eauto. eapply eval_condition_of_expr; eauto. destruct b1; auto. - (* Elet *) - econstructor; eauto. - (* Eletvar *) - constructor; auto. - (* Ealloc *) - econstructor; eauto. - (* Enil *) - constructor. - (* Econs *) - econstructor; eauto. +Qed. + +Hint Resolve sel_expr_correct: evalexpr. + +Lemma sel_exprlist_correct: + forall sp e m a v, + Cminor.eval_exprlist ge sp e m a v -> + forall le, + eval_exprlist tge sp e m le (sel_exprlist a) v. +Proof. + induction 1; intros; simpl; constructor; auto with evalexpr. +Qed. + +Hint Resolve sel_exprlist_correct: evalexpr. + +(** Semantic preservation for terminating function calls and statements. *) + +Definition eval_funcall_exec_stmt_ind2 + (P1 : mem -> Cminor.fundef -> list val -> trace -> mem -> val -> Prop) + (P2 : val -> env -> mem -> Cminor.stmt -> trace -> env -> mem -> outcome -> Prop) := + fun a b c d e f g h i j k l m n o p q r => + conj (Cminor.eval_funcall_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q r) + (Cminor.exec_stmt_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q r). + +Lemma sel_function_stmt_correct: + (forall m fd vargs t m' vres, + Cminor.eval_funcall ge m fd vargs t m' vres -> + CminorSel.eval_funcall tge m (sel_fundef fd) vargs t m' vres) + /\ (forall sp e m s t e' m' out, + Cminor.exec_stmt ge sp e m s t e' m' out -> + CminorSel.exec_stmt tge sp e m (sel_stmt s) t e' m' out). +Proof. + apply eval_funcall_exec_stmt_ind2; intros; simpl. (* Internal function *) econstructor; eauto. (* External function *) econstructor; eauto. (* Sskip *) constructor. - (* Sexpr *) - econstructor; eauto. (* Sassign *) - econstructor; eauto. + econstructor; eauto with evalexpr. + (* Sstore *) + eapply eval_store; eauto with evalexpr. + (* Scall *) + econstructor; eauto with evalexpr. + apply functions_translated; auto. + rewrite <- H2. apply sig_function_translated. + (* Salloc *) + econstructor; eauto with evalexpr. (* Sifthenelse *) - econstructor; eauto. eapply eval_condition_of_expr; eauto. - destruct b1; auto. + econstructor; eauto with evalexpr. + eapply eval_condition_of_expr; eauto with evalexpr. + destruct b; auto. (* Sseq *) eapply exec_Sseq_continue; eauto. eapply exec_Sseq_stop; eauto. @@ -1209,32 +1087,97 @@ Proof. (* Sexit *) constructor. (* Sswitch *) - econstructor; eauto. + econstructor; eauto with evalexpr. (* Sreturn *) constructor. - econstructor; eauto. + econstructor; eauto with evalexpr. (* Stailcall *) - econstructor; eauto. apply functions_translated; auto. - rewrite <- H4. apply sig_function_translated. + econstructor; eauto with evalexpr. + apply functions_translated; auto. + rewrite <- H2. apply sig_function_translated. Qed. +Lemma sel_function_correct: + forall m fd vargs t m' vres, + Cminor.eval_funcall ge m fd vargs t m' vres -> + CminorSel.eval_funcall tge m (sel_fundef fd) vargs t m' vres. +Proof (proj1 sel_function_stmt_correct). + +Lemma sel_stmt_correct: + forall sp e m s t e' m' out, + Cminor.exec_stmt ge sp e m s t e' m' out -> + CminorSel.exec_stmt tge sp e m (sel_stmt s) t e' m' out. +Proof (proj2 sel_function_stmt_correct). + +Hint Resolve sel_stmt_correct: evalexpr. + +(** Semantic preservation for diverging function calls and statements. *) + +Lemma sel_function_divergence_correct: + forall m fd vargs t, + Cminor.evalinf_funcall ge m fd vargs t -> + CminorSel.evalinf_funcall tge m (sel_fundef fd) vargs t. +Proof. + cofix FUNCALL. + assert (STMT: forall sp e m s t, + Cminor.execinf_stmt ge sp e m s t -> + CminorSel.execinf_stmt tge sp e m (sel_stmt s) t). + cofix STMT; intros. + inversion H; subst; simpl. + (* Call *) + econstructor; eauto with evalexpr. + apply functions_translated; auto. + apply sig_function_translated. + (* Ifthenelse *) + econstructor; eauto with evalexpr. + eapply eval_condition_of_expr; eauto with evalexpr. + destruct b; eapply STMT; eauto. + (* Seq *) + apply execinf_Sseq_1; eauto. + eapply execinf_Sseq_2; eauto with evalexpr. + (* Loop *) + eapply execinf_Sloop_body; eauto. + eapply execinf_Sloop_loop; eauto with evalexpr. + change (Sloop (sel_stmt s0)) with (sel_stmt (Cminor.Sloop s0)). + apply STMT. auto. + (* Block *) + apply execinf_Sblock; eauto. + (* Tailcall *) + econstructor; eauto with evalexpr. + apply functions_translated; auto. + apply sig_function_translated. + + intros. inv H; simpl. + (* Internal functions *) + econstructor; eauto with evalexpr. + unfold sel_function; simpl. eapply STMT; eauto. +Qed. + End PRESERVATION. (** As a corollary, instruction selection preserves the observable behaviour of programs. *) Theorem sel_program_correct: - forall prog t r, - Cminor.exec_program prog t r -> - CminorSel.exec_program (sel_program prog) t r. + forall prog beh, + Cminor.exec_program prog beh -> + CminorSel.exec_program (sel_program prog) beh. Proof. - intros. - destruct H as [b [f [m [FINDS [FINDF [SIG EXEC]]]]]]. - exists b; exists (sel_fundef f); exists m. - split. simpl. rewrite <- FINDS. apply symbols_preserved. - split. apply function_ptr_translated. auto. - split. rewrite <- SIG. apply sig_function_translated. + intros. inv H. + (* Terminating *) + apply program_terminates with b (sel_fundef f) m. + simpl. rewrite <- H0. unfold ge. apply symbols_preserved. + apply function_ptr_translated. auto. + rewrite <- H2. apply sig_function_translated. replace (Genv.init_mem (sel_program prog)) with (Genv.init_mem prog). apply sel_function_correct; auto. symmetry. unfold sel_program. apply Genv.init_mem_transf. + (* Diverging *) + apply program_diverges with b (sel_fundef f). + simpl. rewrite <- H0. unfold ge. apply symbols_preserved. + apply function_ptr_translated. auto. + rewrite <- H2. apply sig_function_translated. + replace (Genv.init_mem (sel_program prog)) with (Genv.init_mem prog). + apply sel_function_divergence_correct; auto. + symmetry. unfold sel_program. apply Genv.init_mem_transf. Qed. |