From a15858a0a8fcea82db02fe8c9bd2ed912210419f Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 18 Aug 2010 09:06:55 +0000 Subject: Merge of branches/full-expr-4: - Csyntax, Csem: source C language has side-effects within expressions, performs implicit casts, and has nondeterministic reduction semantics for expressions - Cstrategy: deterministic red. sem. for the above - Clight: the previous source C language, with pure expressions. Added: temporary variables + implicit casts. - New pass SimplExpr to pull side-effects out of expressions (previously done in untrusted Caml code in cparser/) - Csharpminor: added temporary variables to match Clight. - Cminorgen: adapted, removed cast optimization (moved to back-end) - CastOptim: RTL-level optimization of casts - cparser: transformations Bitfields, StructByValue and StructAssign now work on non-simplified expressions - Added pretty-printers for several intermediate languages, and matching -dxxx command-line flags. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1467 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/SimplExprproof.v | 1851 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1851 insertions(+) create mode 100644 cfrontend/SimplExprproof.v (limited to 'cfrontend/SimplExprproof.v') diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v new file mode 100644 index 00000000..603e2730 --- /dev/null +++ b/cfrontend/SimplExprproof.v @@ -0,0 +1,1851 @@ +(* *********************************************************************) +(* *) +(* 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 proof for expression simplification. *) + +Require Import Coq.Program.Equality. +Require Import Axioms. +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Errors. +Require Import Integers. +Require Import Values. +Require Import Memory. +Require Import Events. +Require Import Smallstep. +Require Import Globalenvs. +Require Import Determinism. +Require Import Csyntax. +Require Import Csem. +Require Import Cstrategy. +Require Import Clight. +Require Import SimplExpr. +Require Import SimplExprspec. + +Section PRESERVATION. + +Variable prog: C.program. +Variable tprog: Clight.program. +Hypothesis TRANSL: transl_program prog = OK tprog. + +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +(** Invariance properties. *) + +Lemma symbols_preserved: + forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof + (Genv.find_symbol_transf_partial transl_fundef _ TRANSL). + +Lemma function_ptr_translated: + forall b f, + Genv.find_funct_ptr ge b = Some f -> + exists tf, + Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf. +Proof + (Genv.find_funct_ptr_transf_partial transl_fundef _ TRANSL). + +Lemma functions_translated: + forall v f, + Genv.find_funct ge v = Some f -> + exists tf, + Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf. +Proof + (Genv.find_funct_transf_partial transl_fundef _ TRANSL). + +Lemma varinfo_preserved: + forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. +Proof + (Genv.find_var_info_transf_partial transl_fundef _ TRANSL). + +Lemma type_of_fundef_preserved: + forall f tf, transl_fundef f = OK tf -> + type_of_fundef tf = C.type_of_fundef f. +Proof. + intros. destruct f; monadInv H. + exploit transl_function_spec; eauto. intros [A [B [C D]]]. + simpl. unfold type_of_function, C.type_of_function. congruence. + auto. +Qed. + +Lemma function_return_preserved: + forall f tf, transl_function f = OK tf -> + fn_return tf = C.fn_return f. +Proof. + intros. unfold transl_function in H. + destruct (transl_stmt (C.fn_body f) initial_generator); inv H. + auto. +Qed. + +Lemma type_of_global_preserved: + forall b ty, + Csem.type_of_global ge b = Some ty -> + type_of_global tge b = Some ty. +Proof. + intros until ty. unfold Csem.type_of_global, type_of_global. + rewrite varinfo_preserved. destruct (Genv.find_var_info ge b). auto. + case_eq (Genv.find_funct_ptr ge b); intros. + inv H0. exploit function_ptr_translated; eauto. intros [tf [A B]]. + rewrite A. decEq. apply type_of_fundef_preserved; auto. + congruence. +Qed. + +(** Translation of simple expressions. *) + +Lemma tr_simple_nil: + (forall le dst r sl a tmps, tr_expr le dst r sl a tmps -> + dst = For_val \/ dst = For_effects -> simple r -> sl = nil) +/\(forall le rl sl al tmps, tr_exprlist le rl sl al tmps -> + simplelist rl -> sl = nil). +Proof. + assert (A: forall dst a, dst = For_val \/ dst = For_effects -> final dst a = nil). + intros. destruct H; subst dst; auto. + apply tr_expr_exprlist; intros; simpl in *; try contradiction; auto. + rewrite H0; auto. simpl; auto. + rewrite H0; auto. simpl; auto. + destruct H1; congruence. + rewrite H0; auto. simpl; auto. + rewrite H0; auto. simpl; auto. + rewrite H0; auto. simpl; auto. + destruct H7. rewrite H0; auto. rewrite H2; auto. simpl; auto. + rewrite H0; auto. simpl; auto. + destruct H6. rewrite H0; auto. +Qed. + +Lemma tr_simple_expr_nil: + forall le dst r sl a tmps, tr_expr le dst r sl a tmps -> + dst = For_val \/ dst = For_effects -> simple r -> sl = nil. +Proof (proj1 tr_simple_nil). + +Lemma tr_simple_exprlist_nil: + forall le rl sl al tmps, tr_exprlist le rl sl al tmps -> + simplelist rl -> sl = nil. +Proof (proj2 tr_simple_nil). + +(** Evaluation of simple expressions and of their translation *) + +Lemma tr_simple: + forall e m, + (forall r v, + eval_simple_rvalue ge e m r v -> + forall le dst sl a tmps, + tr_expr le dst r sl a tmps -> + match dst with + | For_val => sl = nil /\ C.typeof r = typeof a /\ eval_expr tge e le m a v + | For_effects => sl = nil + | For_test s1 s2 => + exists b, sl = makeif b s1 s2 :: nil /\ C.typeof r = typeof b /\ eval_expr tge e le m b v + end) +/\ + (forall l b ofs, + eval_simple_lvalue ge e m l b ofs -> + forall le sl a tmps, + tr_expr le For_val l sl a tmps -> + sl = nil /\ C.typeof l = typeof a /\ eval_lvalue tge e le m a b ofs). +Proof. +Opaque makeif. + intros e m. + apply (eval_simple_rvalue_lvalue_ind ge e m); intros until tmps; intros TR; inv TR. +(* value *) + auto. + auto. + exists a0; auto. +(* rvalof *) + exploit H0; eauto. intros [A [B C]]. + subst sl1; simpl. + assert (eval_expr tge e le m a v). eapply eval_Elvalue. eauto. congruence. + destruct dst; auto. + econstructor. split. simpl; eauto. auto. +(* addrof *) + exploit H0; eauto. intros [A [B C]]. + subst sl1; simpl. + assert (eval_expr tge e le m (Eaddrof a1 ty) (Vptr b ofs)). econstructor; eauto. + destruct dst; auto. simpl; econstructor; eauto. +(* unop *) + exploit H0; eauto. intros [A [B C]]. + subst sl1; simpl. + assert (eval_expr tge e le m (Eunop op a1 ty) v). econstructor; eauto. congruence. + destruct dst; auto. simpl; econstructor; eauto. +(* binop *) + exploit H0; eauto. intros [A [B C]]. + exploit H2; eauto. intros [D [E F]]. + subst sl1 sl2; simpl. + assert (eval_expr tge e le m (Ebinop op a1 a2 ty) v). econstructor; eauto. congruence. + destruct dst; auto. simpl; econstructor; eauto. +(* cast *) + exploit H0; eauto. intros [A [B C]]. + subst sl1; simpl. + assert (eval_expr tge e le m (Ecast a1 ty) v). econstructor; eauto. congruence. + destruct dst; auto. simpl; econstructor; eauto. +(* sizeof *) + destruct dst. + split; auto. split; auto. constructor. + auto. + exists (Esizeof ty1 ty). split. auto. split. auto. constructor. +(* var local *) + split; auto. split; auto. apply eval_Evar_local; auto. +(* var global *) + split; auto. split; auto. apply eval_Evar_global; auto. + rewrite symbols_preserved; auto. + eapply type_of_global_preserved; eauto. +(* deref *) + exploit H0; eauto. intros [A [B C]]. subst sl1. + split; auto. split; auto. constructor; auto. +(* field struct *) + exploit H0; eauto. intros [A [B C]]. subst sl1. + split; auto. split; auto. rewrite B in H1. eapply eval_Efield_struct; eauto. +(* field union *) + exploit H0; eauto. intros [A [B C]]. subst sl1. + split; auto. split; auto. rewrite B in H1. eapply eval_Efield_union; eauto. +Qed. + +Lemma tr_simple_rvalue: + forall e m r v, + eval_simple_rvalue ge e m r v -> + forall le dst sl a tmps, + tr_expr le dst r sl a tmps -> + match dst with + | For_val => sl = nil /\ C.typeof r = typeof a /\ eval_expr tge e le m a v + | For_effects => sl = nil + | For_test s1 s2 => + exists b, sl = makeif b s1 s2 :: nil /\ C.typeof r = typeof b /\ eval_expr tge e le m b v + end. +Proof. + intros e m. exact (proj1 (tr_simple e m)). +Qed. + +Lemma tr_simple_lvalue: + forall e m l b ofs, + eval_simple_lvalue ge e m l b ofs -> + forall le sl a tmps, + tr_expr le For_val l sl a tmps -> + sl = nil /\ C.typeof l = typeof a /\ eval_lvalue tge e le m a b ofs. +Proof. + intros e m. exact (proj2 (tr_simple e m)). +Qed. + +Lemma tr_simple_exprlist: + forall le rl sl al tmps, + tr_exprlist le rl sl al tmps -> + forall e m tyl vl, + eval_simple_list ge e m rl tyl vl -> + sl = nil /\ eval_exprlist tge e le m al tyl vl. +Proof. + induction 1; intros. + inv H. split. auto. constructor. + inv H4. + exploit tr_simple_rvalue; eauto. intros [A [B C]]. + exploit IHtr_exprlist; eauto. intros [D E]. + split. subst; auto. econstructor; eauto. congruence. +Qed. + +(** Commutation between the translation of expressions and left contexts. *) + +Lemma typeof_context: + forall k1 k2 C, leftcontext k1 k2 C -> + forall e1 e2, C.typeof e1 = C.typeof e2 -> + C.typeof (C e1) = C.typeof (C e2). +Proof. + induction 1; intros; auto. +Qed. + +Inductive compat_dest: (C.expr -> C.expr) -> purpose -> purpose -> list statement -> Prop := + | compat_dest_base: forall dst, + compat_dest (fun x => x) dst dst nil + | compat_dest_val: forall C dst sl, + compat_dest C For_val dst sl + | compat_dest_effects: forall C dst sl, + compat_dest C For_effects dst sl + | compat_dest_paren: forall C ty dst' dst sl, + compat_dest C dst' dst sl -> + compat_dest (fun x => C.Eparen (C x) ty) dst' dst sl. + +Lemma compat_dest_not_test: + forall C dst' dst sl, + compat_dest C dst' dst sl -> + dst = For_val \/ dst = For_effects -> + dst' = For_val \/ dst' = For_effects. +Proof. + induction 1; intros; auto. +Qed. + +Lemma compat_dest_change: + forall C1 dst' dst1 sl1 C2 dst2 sl2, + compat_dest C1 dst' dst1 sl1 -> + dst1 = For_val \/ dst1 = For_effects -> + compat_dest C2 dst' dst2 sl2. +Proof. + intros. exploit compat_dest_not_test; eauto. intros [A | A]; subst dst'; constructor. +Qed. + +Scheme leftcontext_ind2 := Minimality for leftcontext Sort Prop + with leftcontextlist_ind2 := Minimality for leftcontextlist Sort Prop. +Combined Scheme leftcontext_leftcontextlist_ind from leftcontext_ind2, leftcontextlist_ind2. + +Lemma tr_expr_leftcontext_rec: + ( + forall from to C, leftcontext from to C -> + forall le e dst sl a tmps, + tr_expr le dst (C e) sl a tmps -> + exists dst', exists sl1, exists sl2, exists a', exists tmp', + tr_expr le dst' e sl1 a' tmp' + /\ sl = sl1 ++ sl2 + /\ compat_dest C dst' dst sl2 + /\ incl tmp' tmps + /\ (forall le' e' sl3, + tr_expr le' dst' e' sl3 a' tmp' -> + (forall id, ~In id tmp' -> le'!id = le!id) -> + C.typeof e' = C.typeof e -> + tr_expr le' dst (C e') (sl3 ++ sl2) a tmps) + ) /\ ( + forall from C, leftcontextlist from C -> + forall le e sl a tmps, + tr_exprlist le (C e) sl a tmps -> + exists dst', exists sl1, exists sl2, exists a', exists tmp', + tr_expr le dst' e sl1 a' tmp' + /\ sl = sl1 ++ sl2 + /\ match dst' with For_test _ _ => False | _ => True end + /\ incl tmp' tmps + /\ (forall le' e' sl3, + tr_expr le' dst' e' sl3 a' tmp' -> + (forall id, ~In id tmp' -> le'!id = le!id) -> + C.typeof e' = C.typeof e -> + tr_exprlist le' (C e') (sl3 ++ sl2) a tmps) +). +Proof. + +Ltac TR := + econstructor; econstructor; econstructor; econstructor; econstructor; + split; [eauto | split; [idtac | split; [eauto | split]]]. + +Ltac NOTIN := + match goal with + | [ H1: In ?x ?l, H2: list_disjoint ?l _ |- ~In ?x _ ] => + red; intro; elim (H2 x x); auto + | [ H1: In ?x ?l, H2: list_disjoint _ ?l |- ~In ?x _ ] => + red; intro; elim (H2 x x); auto + end. + +Ltac UNCHANGED := + match goal with + | [ H: (forall (id: ident), ~In id _ -> ?le' ! id = ?le ! id) |- + (forall (id: ident), In id _ -> ?le' ! id = ?le ! id) ] => + intros; apply H; NOTIN + end. + + generalize compat_dest_change; intro CDC. + apply leftcontext_leftcontextlist_ind; intros. + +(* base *) + TR. rewrite <- app_nil_end; auto. constructor. red; auto. + intros. rewrite <- app_nil_end; auto. +(* deref *) + inv H1. + exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. subst sl1; rewrite app_ass; eauto. auto. + intros. rewrite <- app_ass. econstructor; eauto. +(* field *) + inv H1. + exploit H0. eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. subst sl1; rewrite app_ass; eauto. auto. + intros. rewrite <- app_ass. econstructor; eauto. +(* rvalof *) + inv H1. + exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. subst sl1; rewrite app_ass; eauto. auto. + intros. rewrite <- app_ass; econstructor; eauto. +(* addrof *) + inv H1. + exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. subst sl1; rewrite app_ass; eauto. auto. + intros. rewrite <- app_ass. econstructor; eauto. +(* unop *) + inv H1. + exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. subst sl1; rewrite app_ass; eauto. auto. + intros. rewrite <- app_ass. econstructor; eauto. +(* binop left *) + inv H1. + exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. subst sl1. rewrite app_ass. eauto. + red; auto. + intros. rewrite <- app_ass. econstructor; eauto. + eapply tr_expr_invariant; eauto. UNCHANGED. +(* binop right *) + inv H2. + assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl. + exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. subst sl2. rewrite app_ass. eauto. + red; auto. + intros. rewrite <- app_ass. change (sl3 ++ sl2') with (nil ++ sl3 ++ sl2'). rewrite app_ass. econstructor; eauto. + eapply tr_expr_invariant; eauto. UNCHANGED. +(* cast *) + inv H1. + exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. subst sl1; rewrite app_ass; eauto. auto. + intros. rewrite <- app_ass. econstructor; eauto. +(* condition *) + inv H1. + (* for val *) + exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. + rewrite Q. rewrite app_ass. eauto. + red; auto. + intros. rewrite <- app_ass. econstructor. apply S; auto. + eapply tr_expr_invariant; eauto. UNCHANGED. + eapply tr_expr_invariant; eauto. UNCHANGED. + auto. auto. auto. auto. auto. auto. auto. + (* for effects *) + exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. + rewrite Q. rewrite app_ass. eauto. + red; auto. + intros. rewrite <- app_ass. econstructor. auto. apply S; auto. + eapply tr_expr_invariant; eauto. UNCHANGED. + eapply tr_expr_invariant; eauto. UNCHANGED. + auto. auto. auto. auto. auto. +(* assign left *) + inv H1. + (* for effects *) + exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. subst sl1. rewrite app_ass. eauto. + red; auto. + intros. rewrite <- app_ass. econstructor. apply S; auto. + eapply tr_expr_invariant; eauto. UNCHANGED. + auto. auto. auto. + (* for val *) + exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. subst sl1. rewrite app_ass. eauto. + red; auto. + intros. rewrite <- app_ass. econstructor. apply S; auto. + eapply tr_expr_invariant; eauto. UNCHANGED. + auto. auto. auto. auto. auto. auto. + eapply typeof_context; eauto. + auto. +(* assign right *) + inv H2. + (* for effects *) + assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl. + exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. subst sl2. rewrite app_ass. eauto. + red; auto. + intros. rewrite <- app_ass. change (sl3 ++ sl2') with (nil ++ (sl3 ++ sl2')). rewrite app_ass. + econstructor. + eapply tr_expr_invariant; eauto. UNCHANGED. + apply S; auto. auto. auto. auto. + (* for val *) + assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl. + exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. subst sl2. rewrite app_ass. eauto. + red; auto. + intros. rewrite <- app_ass. change (sl3 ++ sl2') with (nil ++ (sl3 ++ sl2')). rewrite app_ass. + econstructor. + eapply tr_expr_invariant; eauto. UNCHANGED. + apply S; auto. auto. auto. auto. auto. auto. auto. auto. + eapply typeof_context; eauto. +(* assignop left *) + inv H1. + (* for effects *) + exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. subst sl1. rewrite app_ass. eauto. + red; auto. + intros. rewrite <- app_ass. econstructor. apply S; auto. + eapply tr_expr_invariant; eauto. UNCHANGED. + auto. auto. auto. + (* for val *) + exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. subst sl1. rewrite app_ass. eauto. + red; auto. + intros. rewrite <- app_ass. econstructor. apply S; auto. + eapply tr_expr_invariant; eauto. UNCHANGED. + auto. auto. auto. auto. auto. auto. + eapply typeof_context; eauto. +(* assignop right *) + inv H2. + (* for effects *) + assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl. + exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. subst sl2. rewrite app_ass. eauto. + red; auto. + intros. rewrite <- app_ass. change (sl3 ++ sl2') with (nil ++ sl3 ++ sl2'). rewrite app_ass. econstructor. + eapply tr_expr_invariant; eauto. UNCHANGED. + apply S; auto. auto. auto. auto. + (* for val *) + assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl. + exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. subst sl2. rewrite app_ass. eauto. + red; auto. + intros. rewrite <- app_ass. change (sl3 ++ sl2') with (nil ++ sl3 ++ sl2'). rewrite app_ass. econstructor. + eapply tr_expr_invariant; eauto. UNCHANGED. + apply S; auto. auto. auto. auto. auto. auto. auto. auto. +(* postincr *) + inv H1. + (* for effects *) + exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. rewrite Q; rewrite app_ass; eauto. red; auto. + intros. replace (C.typeof (C e)) with (C.typeof (C e')). rewrite <- app_ass. + econstructor; eauto. + eapply typeof_context; eauto. + (* for val *) + exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. rewrite Q; rewrite app_ass; eauto. red; auto. + intros. rewrite <- app_ass. econstructor; eauto. + eapply typeof_context; eauto. +(* call left *) + inv H1. + (* for effects *) + exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. rewrite Q; rewrite app_ass; eauto. red; auto. + intros. rewrite <- app_ass. econstructor. apply S; auto. + eapply tr_exprlist_invariant; eauto. UNCHANGED. + auto. auto. auto. + (* for val *) + exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. rewrite Q; rewrite app_ass; eauto. red; auto. + intros. rewrite <- app_ass. econstructor. auto. apply S; auto. + eapply tr_exprlist_invariant; eauto. UNCHANGED. + auto. auto. auto. auto. +(* call right *) + inv H2. + (* for effects *) + assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl. + exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. rewrite Q; rewrite app_ass; eauto. destruct dst'; contradiction || constructor. + red; auto. + intros. rewrite <- app_ass. change (sl3++sl2') with (nil ++ sl3 ++ sl2'). rewrite app_ass. econstructor. + eapply tr_expr_invariant; eauto. UNCHANGED. + apply S; auto. auto. auto. auto. + (* for val *) + assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl. + exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. rewrite Q; rewrite app_ass; eauto. destruct dst'; contradiction || constructor. + red; auto. + intros. rewrite <- app_ass. change (sl3++sl2') with (nil ++ sl3 ++ sl2'). rewrite app_ass. econstructor. + auto. eapply tr_expr_invariant; eauto. UNCHANGED. + apply S; auto. + auto. auto. auto. auto. +(* comma *) + inv H1. + exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. rewrite Q; rewrite app_ass; eauto. red; auto. + intros. rewrite <- app_ass. econstructor. apply S; auto. + eapply tr_expr_invariant; eauto. UNCHANGED. + auto. auto. auto. +(* paren *) + inv H1. + (* for val *) + exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. rewrite Q. rewrite app_ass. eauto. red; auto. + intros. rewrite <- app_ass. econstructor; eauto. + (* for effects *) + exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. rewrite Q. eauto. constructor; auto. auto. + intros. econstructor; eauto. +(* cons left *) + inv H1. + exploit H0; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. subst sl1. rewrite app_ass. eauto. + exploit compat_dest_not_test; eauto. intros [A|A]; subst dst'; auto. + red; auto. + intros. rewrite <- app_ass. econstructor. apply S; auto. + eapply tr_exprlist_invariant; eauto. UNCHANGED. + auto. auto. auto. +(* cons right *) + inv H2. + assert (sl1 = nil) by (eapply tr_simple_expr_nil; eauto). subst sl1; simpl. + exploit H1; eauto. intros [dst' [sl1' [sl2' [a' [tmp' [P [Q [U [R S]]]]]]]]]. + TR. subst sl2. eauto. + red; auto. + intros. change sl3 with (nil ++ sl3). rewrite app_ass. econstructor. + eapply tr_expr_invariant; eauto. UNCHANGED. + apply S; auto. + auto. auto. auto. +Qed. + +Theorem tr_expr_leftcontext: + forall C le r dst sl a tmps, + leftcontext RV RV C -> + tr_expr le dst (C r) sl a tmps -> + exists dst', exists sl1, exists sl2, exists a', exists tmp', + tr_expr le dst' r sl1 a' tmp' + /\ sl = sl1 ++ sl2 + /\ compat_dest C dst' dst sl2 + /\ incl tmp' tmps + /\ (forall le' r' sl3, + tr_expr le' dst' r' sl3 a' tmp' -> + (forall id, ~In id tmp' -> le'!id = le!id) -> + C.typeof r' = C.typeof r -> + tr_expr le' dst (C r') (sl3 ++ sl2) a tmps). +Proof. + intros. eapply (proj1 tr_expr_leftcontext_rec); eauto. +Qed. + +Theorem tr_top_leftcontext: + forall e le m dst rtop sl a tmps, + tr_top tge e le m dst rtop sl a tmps -> + forall r C, + rtop = C r -> + leftcontext RV RV C -> + exists dst', exists sl1, exists sl2, exists a', exists tmp', + tr_top tge e le m dst' r sl1 a' tmp' + /\ sl = sl1 ++ sl2 + /\ compat_dest C dst' dst sl2 + /\ incl tmp' tmps + /\ (forall le' m' r' sl3, + tr_expr le' dst' r' sl3 a' tmp' -> + (forall id, ~In id tmp' -> le'!id = le!id) -> + C.typeof r' = C.typeof r -> + tr_top tge e le' m' dst (C r') (sl3 ++ sl2) a tmps). +Proof. + induction 1; intros. +(* val for val *) + inv H2; inv H1. + exists For_val; econstructor; econstructor; econstructor; econstructor. + split. apply tr_top_val_val; eauto. + split. instantiate (1 := nil); auto. + split. constructor. + split. apply incl_refl. + intros. rewrite <- app_nil_end. constructor; auto. +(* val for test *) + inv H2; inv H1. + exists (For_test s1 s2); econstructor; econstructor; econstructor; econstructor. + split. apply tr_top_val_test; eauto. + split. instantiate (1 := nil); auto. + split. constructor. + split. apply incl_refl. + intros. rewrite <- app_nil_end. constructor; eauto. +(* base *) + subst r. exploit tr_expr_leftcontext; eauto. + intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [R [S T]]]]]]]]]. + exists dst'; exists sl1; exists sl2; exists a'; exists tmp'. + split. apply tr_top_base; auto. + split. auto. split. auto. split. auto. + intros. apply tr_top_base. apply T; auto. +(* paren *) + inv H1; inv H0. + (* at top *) + exists (For_test s1 s2); econstructor; econstructor; econstructor; econstructor. + split. apply tr_top_paren_test; eauto. + split. instantiate (1 := nil). rewrite <- app_nil_end; auto. + split. constructor. + split. apply incl_refl. + intros. rewrite <- app_nil_end. constructor; eauto. + (* below *) + exploit (IHtr_top r0 C0); auto. + intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]]. + exists dst'; exists sl1; exists sl2; exists a'; exists tmp'. + split. auto. + split. auto. + split. constructor; auto. + split. auto. + intros. apply tr_top_paren_test. apply S; auto. +Qed. + +Theorem tr_top_testcontext: + forall C s1 s2 dst sl2 r sl1 a tmps e le m, + compat_dest C (For_test s1 s2) dst sl2 -> + tr_top tge e le m (For_test s1 s2) r sl1 a tmps -> + dst = For_test s1 s2 /\ tr_top tge e le m dst (C r) (sl1 ++ sl2) a tmps. +Proof. + intros. dependent induction H. + split. auto. rewrite <- app_nil_end. auto. + exploit IHcompat_dest; eauto. intros [A B]. + split. auto. subst dst. apply tr_top_paren_test. auto. +Qed. + +(** Semantics of smart constructors *) + +Lemma step_makeif_true: + forall f a s1 s2 k e le m v1, + eval_expr tge e le m a v1 -> + is_true v1 (typeof a) -> + star step tge (State f (makeif a s1 s2) k e le m) + E0 (State f s1 k e le m). +Proof. + intros. functional induction (makeif a s1 s2). + inversion H. subst v1. inversion H0. congruence. congruence. + inversion H1. + apply star_refl. + apply star_one. apply step_ifthenelse_true with v1; auto. +Qed. + +Lemma step_makeif_false: + forall f a s1 s2 k e le m v1, + eval_expr tge e le m a v1 -> + is_false v1 (typeof a) -> + star step tge (State f (makeif a s1 s2) k e le m) + E0 (State f s2 k e le m). +Proof. + intros. functional induction (makeif a s1 s2). + apply star_refl. + inversion H. subst v1. inversion H0. congruence. congruence. + inversion H1. + apply star_one. apply step_ifthenelse_false with v1; auto. +Qed. + +(** Matching between continuations *) + +Fixpoint Kseqlist (sl: list statement) (k: cont) := + match sl with + | nil => k + | s :: l => Kseq s (Kseqlist l k) + end. + +Remark Kseqlist_app: + forall sl1 sl2 k, + Kseqlist (sl1 ++ sl2) k = Kseqlist sl1 (Kseqlist sl2 k). +Proof. + induction sl1; simpl; congruence. +Qed. + +Inductive match_cont : Csem.cont -> cont -> Prop := + | match_Kstop: + match_cont Csem.Kstop Kstop + | match_Kseq: forall s k ts tk, + tr_stmt s ts -> + match_cont k tk -> + match_cont (Csem.Kseq s k) (Kseq ts tk) + | match_Kwhile2: forall r s k s' ts tk, + tr_if r Sskip Sbreak s' -> + tr_stmt s ts -> + match_cont k tk -> + match_cont (Csem.Kwhile2 r s k) + (Kwhile expr_true (Ssequence s' ts) tk) + | match_Kdowhile1: forall r s k s' ts tk, + tr_if r Sskip Sbreak s' -> + tr_stmt s ts -> + match_cont k tk -> + match_cont (Csem.Kdowhile1 r s k) + (Kfor2 expr_true s' ts tk) + | match_Kfor3: forall r s3 s k ts3 s' ts tk, + tr_if r Sskip Sbreak s' -> + tr_stmt s3 ts3 -> + tr_stmt s ts -> + match_cont k tk -> + match_cont (Csem.Kfor3 r s3 s k) + (Kfor2 expr_true ts3 (Ssequence s' ts) tk) + | match_Kfor4: forall r s3 s k ts3 s' ts tk, + tr_if r Sskip Sbreak s' -> + tr_stmt s3 ts3 -> + tr_stmt s ts -> + match_cont k tk -> + match_cont (Csem.Kfor4 r s3 s k) + (Kfor3 expr_true ts3 (Ssequence s' ts) tk) + | match_Kswitch2: forall k tk, + match_cont k tk -> + match_cont (Csem.Kswitch2 k) (Kswitch tk) + | match_Kcall_none: forall f e C ty k tf le sl tk a dest tmps, + transl_function f = Errors.OK tf -> + leftcontext RV RV C -> + (forall v m, tr_top tge e le m dest (C (C.Eval v ty)) sl a tmps) -> + match_cont_exp dest a k tk -> + match_cont (Csem.Kcall f e C ty k) + (Kcall None tf e le (Kseqlist sl tk)) + | match_Kcall_some: forall f e C ty k dst tf le sl tk a dest tmps, + transl_function f = Errors.OK tf -> + leftcontext RV RV C -> + (forall v m, tr_top tge e (PTree.set dst v le) m dest (C (C.Eval v ty)) sl a tmps) -> + match_cont_exp dest a k tk -> + match_cont (Csem.Kcall f e C ty k) + (Kcall (Some dst) tf e le (Kseqlist sl tk)) + +with match_cont_exp : purpose -> expr -> Csem.cont -> cont -> Prop := + | match_Kdo: forall k a tk, + match_cont k tk -> + match_cont_exp For_effects a (Csem.Kdo k) tk + | match_Kifthenelse_1: forall a s1 s2 k ts1 ts2 tk, + tr_stmt s1 ts1 -> tr_stmt s2 ts2 -> + match_cont k tk -> + match_cont_exp For_val a (Csem.Kifthenelse s1 s2 k) (Kseq (Sifthenelse a ts1 ts2) tk) + | match_Kifthenelse_2: forall a s1 s2 k ts1 ts2 tk, + tr_stmt s1 ts1 -> tr_stmt s2 ts2 -> + match_cont k tk -> + match_cont_exp (For_test ts1 ts2) a (Csem.Kifthenelse s1 s2 k) tk + | match_Kwhile1: forall r s k s' a ts tk, + tr_if r Sskip Sbreak s' -> + tr_stmt s ts -> + match_cont k tk -> + match_cont_exp (For_test Sskip Sbreak) a + (Csem.Kwhile1 r s k) + (Kseq ts (Kwhile expr_true (Ssequence s' ts) tk)) + | match_Kdowhile2: forall r s k s' a ts tk, + tr_if r Sskip Sbreak s' -> + tr_stmt s ts -> + match_cont k tk -> + match_cont_exp (For_test Sskip Sbreak) a + (Csem.Kdowhile2 r s k) + (Kfor3 expr_true s' ts tk) + | match_Kfor2: forall r s3 s k s' a ts3 ts tk, + tr_if r Sskip Sbreak s' -> + tr_stmt s3 ts3 -> + tr_stmt s ts -> + match_cont k tk -> + match_cont_exp (For_test Sskip Sbreak) a + (Csem.Kfor2 r s3 s k) + (Kseq ts (Kfor2 expr_true ts3 (Ssequence s' ts) tk)) + | match_Kswitch1: forall ls k a tls tk, + tr_lblstmts ls tls -> + match_cont k tk -> + match_cont_exp For_val a (Csem.Kswitch1 ls k) (Kseq (Sswitch a tls) tk) + | match_Kreturn: forall k a tk, + match_cont k tk -> + match_cont_exp For_val a (Csem.Kreturn k) (Kseq (Sreturn (Some a)) tk). + +Lemma match_cont_call: + forall k tk, + match_cont k tk -> + match_cont (Csem.call_cont k) (call_cont tk). +Proof. + induction 1; simpl; auto. constructor. econstructor; eauto. econstructor; eauto. +Qed. + +Lemma match_cont_exp_for_test_inv: + forall s1 s2 a a' k tk, + match_cont_exp (For_test s1 s2) a k tk -> + match_cont_exp (For_test s1 s2) a' k tk. +Proof. + intros. inv H; econstructor; eauto. +Qed. + +(** Matching between states *) + +Inductive match_states: Csem.state -> state -> Prop := + | match_exprstates: forall f r k e m tf sl tk le dest a tmps, + transl_function f = Errors.OK tf -> + tr_top tge e le m dest r sl a tmps -> + match_cont_exp dest a k tk -> + match_states (Csem.ExprState f r k e m) + (State tf Sskip (Kseqlist sl tk) e le m) + | match_regularstates: forall f s k e m tf ts tk le, + transl_function f = Errors.OK tf -> + tr_stmt s ts -> + match_cont k tk -> + match_states (Csem.State f s k e m) + (State tf ts tk e le m) + | match_callstates: forall fd args k m tfd tk, + transl_fundef fd = Errors.OK tfd -> + match_cont k tk -> + match_states (Csem.Callstate fd args k m) + (Callstate tfd args tk m) + | match_returnstates: forall res k m tk, + match_cont k tk -> + match_states (Csem.Returnstate res k m) + (Returnstate res tk m). + +Lemma push_seq: + forall f sl k e le m, + star step tge (State f (makeseq sl) k e le m) + E0 (State f Sskip (Kseqlist sl k) e le m). +Proof. + intros. unfold makeseq. generalize Sskip. revert sl k. + induction sl; simpl; intros. + apply star_refl. + eapply star_right. apply IHsl. constructor. traceEq. +Qed. + +(** Additional results on translation of statements *) + +Lemma tr_select_switch: + forall n ls tls, + tr_lblstmts ls tls -> + tr_lblstmts (Csem.select_switch n ls) (select_switch n tls). +Proof. + induction 1; simpl. + constructor; auto. + destruct (Int.eq n0 n). constructor; auto. auto. +Qed. + +Lemma tr_seq_of_labeled_statement: + forall ls tls, + tr_lblstmts ls tls -> + tr_stmt (Csem.seq_of_labeled_statement ls) (seq_of_labeled_statement tls). +Proof. + induction 1; simpl. auto. constructor; auto. +Qed. + +(** Commutation between translation and the "find label" operation. *) + +Section FIND_LABEL. + +Variable lbl: label. + +Definition nolabel (s: statement) : Prop := + forall k, find_label lbl s k = None. + +Fixpoint nolabel_list (sl: list statement) : Prop := + match sl with + | nil => True + | s1 :: sl' => nolabel s1 /\ nolabel_list sl' + end. + +Lemma nolabel_list_app: + forall sl2 sl1, nolabel_list sl1 -> nolabel_list sl2 -> nolabel_list (sl1 ++ sl2). +Proof. + induction sl1; simpl; intros. auto. tauto. +Qed. + +Lemma makeseq_nolabel: + forall sl, nolabel_list sl -> nolabel (makeseq sl). +Proof. + assert (forall sl s, nolabel s -> nolabel_list sl -> nolabel (makeseq_rec s sl)). + induction sl; simpl; intros. auto. destruct H0. apply IHsl; auto. + red. intros; simpl. rewrite H. apply H0. + intros. unfold makeseq. apply H; auto. red. auto. +Qed. + +Lemma small_stmt_nolabel: + forall s, small_stmt s = true -> nolabel s. +Proof. + induction s; simpl; intros; congruence || (red; auto). + destruct (andb_prop _ _ H). intros; simpl. rewrite IHs1; auto. apply IHs2; auto. +Qed. + +Lemma makeif_nolabel: + forall a s1 s2, nolabel s1 -> nolabel s2 -> nolabel (makeif a s1 s2). +Proof. + intros. functional induction (makeif a s1 s2); auto. + red; simpl; intros. rewrite H; auto. +Qed. + +Definition nolabel_dest (dst: purpose) : Prop := + match dst with + | For_val => True + | For_effects => True + | For_test s1 s2 => nolabel s1 /\ nolabel s2 + end. + +Lemma nolabel_final: + forall dst a, nolabel_dest dst -> nolabel_list (final dst a). +Proof. + destruct dst; simpl; intros. auto. auto. + split; auto. destruct H. apply makeif_nolabel; auto. +Qed. + +Ltac NoLabelTac := + match goal with + | [ |- nolabel_list nil ] => exact I + | [ |- nolabel_list (final _ _) ] => apply nolabel_final; NoLabelTac + | [ |- nolabel_list (_ :: _) ] => simpl; split; NoLabelTac + | [ |- nolabel_list (_ ++ _) ] => apply nolabel_list_app; NoLabelTac + | [ |- nolabel_dest For_val ] => exact I + | [ |- nolabel_dest For_effects ] => exact I + | [ H: _ -> nolabel_list ?x |- nolabel_list ?x ] => apply H; NoLabelTac + | [ |- nolabel _ ] => red; intros; simpl; auto + | [ |- _ /\ _ ] => split; NoLabelTac + | _ => auto + end. + +Lemma tr_find_label_expr: + (forall le dst r sl a tmps, tr_expr le dst r sl a tmps -> nolabel_dest dst -> nolabel_list sl) +/\(forall le rl sl al tmps, tr_exprlist le rl sl al tmps -> nolabel_list sl). +Proof. + apply tr_expr_exprlist; intros; NoLabelTac. + destruct H1. apply makeif_nolabel; auto. + apply makeif_nolabel; NoLabelTac. + rewrite (makeseq_nolabel sl2); auto. + rewrite (makeseq_nolabel sl3); auto. + apply makeif_nolabel; NoLabelTac. + rewrite (makeseq_nolabel sl2); auto. + rewrite (makeseq_nolabel sl3); auto. +Qed. + +Lemma tr_find_label_top: + forall e le m dst r sl a tmps, + tr_top tge e le m dst r sl a tmps -> nolabel_dest dst -> nolabel_list sl. +Proof. + induction 1; intros; NoLabelTac. + destruct H1. apply makeif_nolabel; auto. + eapply (proj1 tr_find_label_expr); eauto. +Qed. + +Lemma tr_find_label_expression: + forall r s a, tr_expression r s a -> forall k, find_label lbl s k = None. +Proof. + intros. inv H. + assert (nolabel (makeseq sl)). apply makeseq_nolabel. + eapply tr_find_label_top with (e := empty_env) (le := PTree.empty val) (m := Mem.empty). + eauto. exact I. + apply H. +Qed. + +Lemma tr_find_label_expr_stmt: + forall r s, tr_expr_stmt r s -> forall k, find_label lbl s k = None. +Proof. + intros. inv H. + assert (nolabel (makeseq sl)). apply makeseq_nolabel. + eapply tr_find_label_top with (e := empty_env) (le := PTree.empty val) (m := Mem.empty). + eauto. exact I. + apply H. +Qed. + +Lemma tr_find_label_if: + forall r s1 s2 s, + tr_if r s1 s2 s -> + small_stmt s1 = true -> small_stmt s2 = true -> + forall k, find_label lbl s k = None. +Proof. + intros. inv H. + assert (nolabel (makeseq sl)). apply makeseq_nolabel. + eapply tr_find_label_top with (e := empty_env) (le := PTree.empty val) (m := Mem.empty). + eauto. split; apply small_stmt_nolabel; auto. + apply H. +Qed. + +Lemma tr_find_label: + forall s k ts tk + (TR: tr_stmt s ts) + (MC: match_cont k tk), + match Csem.find_label lbl s k with + | None => + find_label lbl ts tk = None + | Some (s', k') => + exists ts', exists tk', + find_label lbl ts tk = Some (ts', tk') + /\ tr_stmt s' ts' + /\ match_cont k' tk' + end +with tr_find_label_ls: + forall s k ts tk + (TR: tr_lblstmts s ts) + (MC: match_cont k tk), + match Csem.find_label_ls lbl s k with + | None => + find_label_ls lbl ts tk = None + | Some (s', k') => + exists ts', exists tk', + find_label_ls lbl ts tk = Some (ts', tk') + /\ tr_stmt s' ts' + /\ match_cont k' tk' + end. +Proof. + induction s; intros; inversion TR; subst; clear TR; simpl. + auto. + eapply tr_find_label_expr_stmt; eauto. +(* seq *) + exploit (IHs1 (Csem.Kseq s2 k)); eauto. constructor; eauto. + destruct (Csem.find_label lbl s1 (Csem.Kseq s2 k)) as [[s' k'] | ]. + intros [ts' [tk' [A [B C]]]]. rewrite A. exists ts'; exists tk'; auto. + intro EQ. rewrite EQ. eapply IHs2; eauto. +(* if no-opt *) + rename s' into sr. + rewrite (tr_find_label_expression _ _ _ H2). + exploit (IHs1 k); eauto. + destruct (Csem.find_label lbl s1 k) as [[s' k'] | ]. + intros [ts' [tk' [A [B C]]]]. rewrite A. exists ts'; exists tk'; intuition. + intro EQ. rewrite EQ. eapply IHs2; eauto. +(* if opt *) + rewrite (tr_find_label_if _ _ _ _ H7); auto. + exploit (IHs1 k); eauto. + destruct (Csem.find_label lbl s1 k) as [[s' k'] | ]. + intros [ts' [tk' [A [B C]]]]. + exploit small_stmt_nolabel. eexact H4. instantiate (1 := tk). congruence. + intros. + exploit (IHs2 k); eauto. + destruct (Csem.find_label lbl s2 k) as [[s' k'] | ]. + intros [ts' [tk' [A [B C]]]]. + exploit small_stmt_nolabel. eexact H6. instantiate (1 := tk). congruence. + auto. +(* while *) + rename s' into sr. + rewrite (tr_find_label_if _ _ _ _ H1); auto. + eapply IHs; eauto. econstructor; eauto. +(* dowhile *) + rename s' into sr. + rewrite (tr_find_label_if _ _ _ _ H1); auto. + exploit (IHs (Kdowhile1 e s k)); eauto. econstructor; eauto. + destruct (Csem.find_label lbl s (Kdowhile1 e s k)) as [[s' k'] | ]. + intros [ts' [tk' [A [B C]]]]. rewrite A. exists ts'; exists tk'; intuition. + intro EQ. rewrite EQ. auto. +(* for skip *) + rename s' into sr. + rewrite (tr_find_label_if _ _ _ _ H4); auto. + exploit (IHs3 (Csem.Kfor3 e s2 s3 k)); eauto. econstructor; eauto. + destruct (Csem.find_label lbl s3 (Csem.Kfor3 e s2 s3 k)) as [[s' k'] | ]. + intros [ts' [tk' [A [B C]]]]. rewrite A. exists ts'; exists tk'; intuition. + intro EQ. rewrite EQ. + exploit (IHs2 (Csem.Kfor4 e s2 s3 k)); eauto. econstructor; eauto. +(* for not skip *) + rename s' into sr. + rewrite (tr_find_label_if _ _ _ _ H3); auto. + exploit (IHs1 (Csem.Kseq (C.Sfor C.Sskip e s2 s3) k)); eauto. + econstructor; eauto. econstructor; eauto. + destruct (Csem.find_label lbl s1 + (Csem.Kseq (C.Sfor C.Sskip e s2 s3) k)) as [[s' k'] | ]. + intros [ts' [tk' [A [B C]]]]. rewrite A. exists ts'; exists tk'; intuition. + intro EQ; rewrite EQ. + exploit (IHs3 (Csem.Kfor3 e s2 s3 k)); eauto. econstructor; eauto. + destruct (Csem.find_label lbl s3 (Csem.Kfor3 e s2 s3 k)) as [[s'' k''] | ]. + intros [ts' [tk' [A [B C]]]]. rewrite A. exists ts'; exists tk'; intuition. + intro EQ'. rewrite EQ'. + exploit (IHs2 (Csem.Kfor4 e s2 s3 k)); eauto. econstructor; eauto. +(* break, continue, return 0 *) + auto. auto. auto. +(* return 1 *) + rewrite (tr_find_label_expression _ _ _ H0). auto. +(* switch *) + rewrite (tr_find_label_expression _ _ _ H1). apply tr_find_label_ls. auto. constructor; auto. +(* labeled stmt *) + destruct (ident_eq lbl l). exists ts0; exists tk; auto. apply IHs; auto. +(* goto *) + auto. + + induction s; intros; inversion TR; subst; clear TR; simpl. +(* default *) + apply tr_find_label; auto. +(* case *) + exploit (tr_find_label s (Csem.Kseq (Csem.seq_of_labeled_statement s0) k)); eauto. + econstructor; eauto. apply tr_seq_of_labeled_statement; eauto. + destruct (Csem.find_label lbl s + (Csem.Kseq (Csem.seq_of_labeled_statement s0) k)) as [[s' k'] | ]. + intros [ts' [tk' [A [B C]]]]. rewrite A. exists ts'; exists tk'; auto. + intro EQ. rewrite EQ. eapply IHs; eauto. +Qed. + +End FIND_LABEL. + +(** Anti-stuttering measure *) + +(** There are some stuttering steps in the translation: +- The execution of [Sdo a] where [a] is side-effect free, + which is three transitions in the source: +<< + Sdo a, k ---> a, Kdo k ---> rval v, Kdo k ---> Sskip, k +>> + but the translation, which is [Sskip], makes no transitions. +- The reduction [C.Ecomma (C.Eval v) r2 --> r2]. +- The reduction [C.Eparen (C.Eval v) --> C.Eval v] in a [For_effects] context. + +The following measure decreases for these stuttering steps. *) + +Fixpoint esize (a: C.expr) : nat := + match a with + | C.Eloc _ _ _ => 1%nat + | C.Evar _ _ => 1%nat + | C.Ederef r1 _ => S(esize r1) + | C.Efield l1 _ _ => S(esize l1) + | C.Eval _ _ => O + | C.Evalof l1 _ => S(esize l1) + | C.Eaddrof l1 _ => S(esize l1) + | C.Eunop _ r1 _ => S(esize r1) + | C.Ebinop _ r1 r2 _ => S(esize r1 + esize r2)%nat + | C.Ecast r1 _ => S(esize r1) + | C.Econdition r1 _ _ _ => S(esize r1) + | C.Esizeof _ _ => 1%nat + | C.Eassign l1 r2 _ => S(esize l1 + esize r2)%nat + | C.Eassignop _ l1 r2 _ _ => S(esize l1 + esize r2)%nat + | C.Epostincr _ l1 _ => S(esize l1) + | C.Ecomma r1 r2 _ => S(esize r1 + esize r2)%nat + | C.Ecall r1 rl2 _ => S(esize r1 + esizelist rl2)%nat + | C.Eparen r1 _ => S(esize r1) + end + +with esizelist (el: C.exprlist) : nat := + match el with + | C.Enil => O + | C.Econs r1 rl2 => (esize r1 + esizelist rl2)%nat + end. + +Definition measure (st: Csem.state) : nat := + match st with + | Csem.ExprState _ r _ _ _ => (esize r + 1)%nat + | Csem.State _ C.Sskip _ _ _ => 0%nat + | Csem.State _ (C.Sdo r) _ _ _ => (esize r + 2)%nat + | Csem.State _ (C.Sifthenelse r _ _) _ _ _ => (esize r + 2)%nat + | _ => 0%nat + end. + +Lemma leftcontext_size: + forall from to C, + leftcontext from to C -> + forall e1 e2, + (esize e1 < esize e2)%nat -> + (esize (C e1) < esize (C e2))%nat +with leftcontextlist_size: + forall from C, + leftcontextlist from C -> + forall e1 e2, + (esize e1 < esize e2)%nat -> + (esizelist (C e1) < esizelist (C e2))%nat. +Proof. + induction 1; intros; simpl; auto with arith. exploit leftcontextlist_size; eauto. auto with arith. + induction 1; intros; simpl; auto with arith. exploit leftcontext_size; eauto. auto with arith. +Qed. + +(** Forward simulation for expressions. *) + +Lemma tr_val_gen: + forall le dst v ty a tmp, + typeof a = ty -> + (forall tge e le' m, + (forall id, In id tmp -> le'!id = le!id) -> + eval_expr tge e le' m a v) -> + tr_expr le dst (C.Eval v ty) (final dst a) a tmp. +Proof. + intros. destruct dst; simpl; econstructor; auto. +Qed. + +Lemma estep_simulation: + forall S1 t S2, Cstrategy.estep ge S1 t S2 -> + forall S1' (MS: match_states S1 S1'), + exists S2', + (plus step tge S1' t S2' \/ + (star step tge S1' t S2' /\ measure S2 < measure S1)%nat) + /\ match_states S2 S2'. +Proof. + induction 1; intros; inv MS. +(* expr *) + assert (tr_expr le dest r sl a tmps). + inv H9. contradiction. contradiction. auto. inv H. + econstructor; split. + right; split. apply star_refl. destruct r; simpl; (contradiction || omega). + econstructor; eauto. + instantiate (1 := tmps). + exploit tr_simple_rvalue; eauto. destruct dest. + intros [A [B C]]. subst sl. apply tr_top_val_val; auto. + intros A. subst sl. apply tr_top_base. constructor. + intros [b [A [B C]]]. subst sl. apply tr_top_val_test; auto. +(* condition true *) + exploit tr_top_leftcontext; eauto. clear H10. + intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]]. + inv P. inv H2. + (* for value *) + exploit tr_simple_rvalue; eauto. intros [SL [TY EV]]. + subst sl0; simpl Kseqlist. + econstructor; split. + left. eapply plus_left. constructor. + eapply star_trans. apply step_makeif_true with v; auto. congruence. + eapply star_left. constructor. apply push_seq. + reflexivity. reflexivity. traceEq. + replace (Kseqlist sl3 (Kseq (Sset t a2) (Kseqlist sl2 tk))) + with (Kseqlist (sl3 ++ Sset t a2 :: sl2) tk). + eapply match_exprstates; eauto. + change (Sset t a2 :: sl2) with ((Sset t a2 :: nil) ++ sl2). rewrite <- app_ass. + apply S. econstructor; eauto. auto. auto. + rewrite Kseqlist_app. auto. + (* for effects *) + exploit tr_simple_rvalue; eauto. intros [SL [TY EV]]. + subst sl0; simpl Kseqlist. + econstructor; split. + left. eapply plus_left. constructor. + eapply star_trans. apply step_makeif_true with v; auto. congruence. + apply push_seq. + reflexivity. traceEq. + rewrite <- Kseqlist_app. + econstructor. eauto. apply S. + econstructor; eauto. apply tr_expr_monotone with tmp2; eauto. + econstructor; eauto. + auto. auto. +(* condition false *) + exploit tr_top_leftcontext; eauto. clear H10. + intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]]. + inv P. inv H2. + (* for value *) + exploit tr_simple_rvalue; eauto. intros [SL [TY EV]]. + subst sl0; simpl Kseqlist. + econstructor; split. + left. eapply plus_left. constructor. + eapply star_trans. apply step_makeif_false with v; auto. congruence. + eapply star_left. constructor. apply push_seq. + reflexivity. reflexivity. traceEq. + replace (Kseqlist sl4 (Kseq (Sset t a3) (Kseqlist sl2 tk))) + with (Kseqlist (sl4 ++ Sset t a3 :: sl2) tk). + eapply match_exprstates; eauto. + change (Sset t a3 :: sl2) with ((Sset t a3 :: nil) ++ sl2). rewrite <- app_ass. + apply S. econstructor; eauto. auto. auto. + rewrite Kseqlist_app. auto. + (* for effects *) + exploit tr_simple_rvalue; eauto. intros [SL [TY EV]]. + subst sl0; simpl Kseqlist. + econstructor; split. + left. eapply plus_left. constructor. + eapply star_trans. apply step_makeif_false with v; auto. congruence. + apply push_seq. + reflexivity. traceEq. + rewrite <- Kseqlist_app. + econstructor. eauto. apply S. + econstructor; eauto. apply tr_expr_monotone with tmp3; eauto. + auto. auto. auto. +(* assign *) + exploit tr_top_leftcontext; eauto. clear H12. + intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]]. + inv P. inv H4. + (* for effects *) + exploit tr_simple_rvalue; eauto. intros [SL2 [TY2 EV2]]. + exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]]. + subst; simpl Kseqlist. + econstructor; split. + left. eapply plus_left. constructor. + apply star_one. econstructor; eauto. + rewrite <- TY1; rewrite <- TY2; eauto. + rewrite <- TY1; eauto. + traceEq. + econstructor. auto. change sl2 with (nil ++ sl2). apply S. + constructor. auto. auto. auto. + (* for value *) + exploit tr_simple_rvalue; eauto. intros [SL2 [TY2 EV2]]. + exploit tr_simple_lvalue. eauto. + eapply tr_expr_invariant with (le' := PTree.set t v le). eauto. + intros. apply PTree.gso. intuition congruence. + intros [SL1 [TY1 EV1]]. + subst; simpl Kseqlist. + econstructor; split. + left. eapply plus_left. constructor. + eapply star_left. constructor. eauto. + eapply star_left. constructor. + apply star_one. econstructor; eauto. constructor. apply PTree.gss. + simpl. rewrite <- TY1; eauto. + rewrite <- TY1; eauto. + reflexivity. reflexivity. traceEq. + econstructor. auto. apply S. + apply tr_val_gen. auto. intros. econstructor; eauto. constructor. + rewrite H4; auto. apply PTree.gss. + intros. apply PTree.gso. intuition congruence. + auto. auto. +(* assignop *) + exploit tr_top_leftcontext; eauto. clear H14. + intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]]. + inv P. inv H6. + (* for effects *) + exploit tr_simple_rvalue; eauto. intros [SL2 [TY2 EV2]]. + exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]]. + subst; simpl Kseqlist. + econstructor; split. + left. eapply plus_left. constructor. + apply star_one. econstructor; eauto. + econstructor; eauto. eapply eval_Elvalue; eauto. rewrite <- TY1; eauto. + rewrite <- TY1; rewrite <- TY2; eauto. + rewrite <- TY1; eauto. + rewrite <- TY1; eauto. + traceEq. + econstructor. auto. change sl2 with (nil ++ sl2). apply S. + constructor. auto. auto. auto. + (* for value *) + exploit tr_simple_rvalue; eauto. intros [SL2 [TY2 EV2]]. + exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]]. + exploit tr_simple_lvalue. eauto. + eapply tr_expr_invariant with (le' := PTree.set t v3 le). eauto. + intros. apply PTree.gso. intuition congruence. + intros [SL3 [TY3 EV3]]. + subst; simpl Kseqlist. + econstructor; split. + left. eapply plus_left. constructor. + eapply star_left. constructor. + econstructor. eapply eval_Elvalue; eauto. rewrite <- TY1; eauto. eauto. + rewrite <- TY1; rewrite <- TY2. eauto. + eapply star_left. constructor. + apply star_one. econstructor. eauto. constructor. apply PTree.gss. + rewrite <- TY1. eauto. rewrite <- TY1. eauto. + reflexivity. reflexivity. traceEq. + econstructor. auto. apply S. + apply tr_val_gen. auto. intros. econstructor; eauto. constructor. + rewrite H6; auto. apply PTree.gss. + intros. apply PTree.gso. intuition congruence. + auto. auto. +(* postincr *) + exploit tr_top_leftcontext; eauto. clear H13. + intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]]. + inv P. inv H5. + (* for effects *) + exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]]. + assert (EV2: eval_expr tge e le m a1 v1). eapply eval_Elvalue; eauto. rewrite <- TY1; auto. + subst; simpl Kseqlist. + econstructor; split. + left. eapply plus_two. constructor. + econstructor; eauto. + unfold transl_incrdecr. destruct id; simpl in H2. + econstructor. eauto. constructor. simpl. rewrite <- TY1. eauto. + econstructor. eauto. constructor. simpl. rewrite <- TY1. eauto. + rewrite <- TY1. instantiate (1 := v3). destruct id; auto. + rewrite <- TY1. eauto. + traceEq. + econstructor. auto. change sl2 with (nil ++ sl2). apply S. + constructor. auto. auto. auto. + (* for value *) + exploit tr_simple_lvalue; eauto. intros [SL1 [TY1 EV1]]. + exploit tr_simple_lvalue. eauto. + eapply tr_expr_invariant with (le' := PTree.set t v1 le). eauto. + intros. apply PTree.gso. intuition congruence. + intros [SL2 [TY2 EV2]]. + subst; simpl Kseqlist. + econstructor; split. + left. eapply plus_four. constructor. + constructor. eapply eval_Elvalue; eauto. rewrite <- TY1; eauto. + constructor. + econstructor. eauto. + unfold transl_incrdecr. destruct id; simpl in H2. + econstructor. constructor. apply PTree.gss. constructor. simpl. eauto. + econstructor. constructor. apply PTree.gss. constructor. simpl. eauto. + rewrite <- TY1. instantiate (1 := v3). destruct id; auto. + rewrite <- TY1. eauto. + traceEq. + econstructor. auto. apply S. + apply tr_val_gen. auto. intros. econstructor; eauto. + rewrite H5; auto. apply PTree.gss. + intros. apply PTree.gso. intuition congruence. + auto. auto. +(* comma *) + exploit tr_top_leftcontext; eauto. clear H9. + intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]]. + inv P. inv H1. + exploit tr_simple_rvalue; eauto. simpl; intro SL1. + subst sl0; simpl Kseqlist. + econstructor; split. + right; split. apply star_refl. simpl. apply plus_lt_compat_r. + apply (leftcontext_size _ _ _ H). simpl. omega. + econstructor; eauto. apply S. + eapply tr_expr_monotone; eauto. + auto. auto. +(* paren *) + exploit tr_top_leftcontext; eauto. clear H9. + intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [T [R S]]]]]]]]]. + inv P. inv H1. + (* for value *) + exploit tr_simple_rvalue; eauto. intros [SL1 [TY1 EV1]]. + subst sl0; simpl Kseqlist. + econstructor; split. + left. eapply plus_left. constructor. apply star_one. + econstructor. eauto. traceEq. + econstructor; eauto. change sl2 with (final For_val (Etempvar t (C.typeof r)) ++ sl2). apply S. + constructor. auto. intros. constructor. rewrite H1; auto. apply PTree.gss. + intros. apply PTree.gso. intuition congruence. + auto. + (* for effects *) + econstructor; split. + right; split. apply star_refl. simpl. apply plus_lt_compat_r. + apply (leftcontext_size _ _ _ H). simpl. omega. + econstructor; eauto. + exploit tr_simple_rvalue; eauto. destruct dst'. + (* dst' = For_val: impossible *) + congruence. + (* dst' = For_effects: easy *) + intros A. subst sl1. apply S. constructor; auto. auto. auto. + (* dst' = For_test: then dest is For_test as well and C is a string of C.Eparen, + so we can apply tr_top_paren. *) + intros [b [A [B D]]]. + eapply tr_top_testcontext; eauto. + subst sl1. apply tr_top_val_test; auto. + (* already reduced *) + econstructor; split. + right; split. apply star_refl. simpl. apply plus_lt_compat_r. + apply (leftcontext_size _ _ _ H). simpl. omega. + econstructor; eauto. instantiate (1 := @nil ident). + inv H7. + inv H0. eapply tr_top_testcontext; eauto. constructor. auto. auto. + exploit tr_simple_rvalue; eauto. simpl. intros [b [A [B D]]]. + eapply tr_top_testcontext; eauto. subst sl1. apply tr_top_val_test. auto. auto. + inv H0. +(* call *) + exploit tr_top_leftcontext; eauto. clear H12. + intros [dst' [sl1 [sl2 [a' [tmp' [P [Q [U [R S]]]]]]]]]. + inv P. inv H5. + (* for effects *) + exploit tr_simple_rvalue; eauto. intros [SL1 [TY1 EV1]]. + exploit tr_simple_exprlist; eauto. intros [SL2 EV2]. + subst. simpl Kseqlist. + exploit functions_translated; eauto. intros [tfd [J K]]. + econstructor; split. + left. eapply plus_left. constructor. apply star_one. + econstructor; eauto. rewrite <- TY1; eauto. + exploit type_of_fundef_preserved; eauto. congruence. + traceEq. + constructor; auto. econstructor; eauto. + intros. change sl2 with (nil ++ sl2). apply S. + constructor. auto. auto. + (* for value *) + exploit tr_simple_rvalue; eauto. intros [SL1 [TY1 EV1]]. + exploit tr_simple_exprlist; eauto. intros [SL2 EV2]. + subst. simpl Kseqlist. + exploit functions_translated; eauto. intros [tfd [J K]]. + econstructor; split. + left. eapply plus_left. constructor. apply star_one. + econstructor; eauto. rewrite <- TY1; eauto. + exploit type_of_fundef_preserved; eauto. congruence. + traceEq. + constructor; auto. econstructor; eauto. + intros. apply S. + destruct dst'; constructor. + auto. intros. constructor. rewrite H5; auto. apply PTree.gss. + auto. intros. constructor. rewrite H5; auto. apply PTree.gss. + intros. apply PTree.gso. intuition congruence. + auto. +Qed. + +(** Forward simulation for statements. *) + +Lemma tr_top_val_for_val_inv: + forall e le m v ty sl a tmps, + tr_top tge e le m For_val (C.Eval v ty) sl a tmps -> + sl = nil /\ typeof a = ty /\ eval_expr tge e le m a v. +Proof. + intros. inv H. auto. inv H0. auto. +Qed. + +Lemma tr_top_val_for_test_inv: + forall s1 s2 e le m v ty sl a tmps, + tr_top tge e le m (For_test s1 s2) (C.Eval v ty) sl a tmps -> + exists b, sl = makeif b s1 s2 :: nil /\ typeof b = ty /\ eval_expr tge e le m b v. +Proof. + intros. inv H. exists a0; auto. + inv H0. exists a0; auto. +Qed. + +Lemma sstep_simulation: + forall S1 t S2, Csem.sstep ge S1 t S2 -> + forall S1' (MS: match_states S1 S1'), + exists S2', + (plus step tge S1' t S2' \/ + (star step tge S1' t S2' /\ measure S2 < measure S1)%nat) + /\ match_states S2 S2'. +Proof. + induction 1; intros; inv MS. +(* do 1 *) + inv H6. inv H0. + econstructor; split. + right; split. apply push_seq. + simpl. omega. + econstructor; eauto. constructor. auto. +(* do 2 *) + inv H7. inv H6. inv H. + econstructor; split. + right; split. apply star_refl. simpl. omega. + econstructor; eauto. constructor. + +(* seq *) + inv H6. econstructor; split. left. apply plus_one. constructor. + econstructor; eauto. constructor; auto. +(* skip seq *) + inv H6; inv H7. econstructor; split. + left. apply plus_one; constructor. + econstructor; eauto. +(* continue seq *) + inv H6; inv H7. econstructor; split. + left. apply plus_one; constructor. + econstructor; eauto. constructor. +(* break seq *) + inv H6; inv H7. econstructor; split. + left. apply plus_one; constructor. + econstructor; eauto. constructor. + +(* ifthenelse *) + inv H6. + (* not optimized *) + inv H2. econstructor; split. + left. eapply plus_left. constructor. apply push_seq. traceEq. + econstructor; eauto. econstructor; eauto. + (* optimized *) + inv H10. econstructor; split. + right; split. apply push_seq. simpl. omega. + econstructor; eauto. constructor; auto. +(* ifthenelse true *) + inv H8. + (* not optimized *) + exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst. + econstructor; split. + left. eapply plus_two. constructor. + apply step_ifthenelse_true with v; auto. traceEq. + econstructor; eauto. + (* optimized *) + exploit tr_top_val_for_test_inv; eauto. intros [b [A [B C]]]. subst. + econstructor; split. + left. simpl. eapply plus_left. constructor. + apply step_makeif_true with v; auto. traceEq. + econstructor; eauto. +(* ifthenelse false *) + inv H8. + (* not optimized *) + exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst. + econstructor; split. + left. eapply plus_two. constructor. + apply step_ifthenelse_false with v; auto. traceEq. + econstructor; eauto. + (* optimized *) + exploit tr_top_val_for_test_inv; eauto. intros [b [A [B C]]]. subst. + econstructor; split. + left. simpl. eapply plus_left. constructor. + apply step_makeif_false with v; auto. traceEq. + econstructor; eauto. + +(* while *) + inv H6. inv H1. econstructor; split. + left. eapply plus_left. eapply step_while_true. constructor. + simpl. constructor. apply Int.one_not_zero. + eapply star_left. constructor. + apply push_seq. + reflexivity. traceEq. + econstructor; eauto. econstructor; eauto. econstructor; eauto. +(* while false *) + inv H8. + exploit tr_top_val_for_test_inv; eauto. intros [b [A [B C]]]. subst. + econstructor; split. + left. simpl. eapply plus_left. constructor. + eapply star_trans. apply step_makeif_false with v; auto. + eapply star_two. constructor. apply step_break_while. + reflexivity. reflexivity. traceEq. + constructor; auto. constructor. +(* while true *) + inv H8. + exploit tr_top_val_for_test_inv; eauto. intros [b [A [B C]]]. subst. + econstructor; split. + left. simpl. eapply plus_left. constructor. + eapply star_right. apply step_makeif_true with v; auto. + constructor. + reflexivity. traceEq. + constructor; auto. constructor; auto. +(* skip-or-continue while *) + assert (ts = Sskip \/ ts = Scontinue). destruct H; subst s0; inv H7; auto. + inv H8. + econstructor; split. + left. apply plus_one. apply step_skip_or_continue_while; auto. + constructor; auto. constructor; auto. +(* break while *) + inv H6. inv H7. + econstructor; split. + left. apply plus_one. apply step_break_while. + constructor; auto. constructor. + +(* dowhile *) + inv H6. + econstructor; split. + left. apply plus_one. + apply step_for_true with (Vint Int.one). constructor. simpl; constructor. apply Int.one_not_zero. + constructor; auto. constructor; auto. +(* skip_or_continue dowhile *) + assert (ts = Sskip \/ ts = Scontinue). destruct H; subst s0; inv H7; auto. + inv H8. inv H4. + econstructor; split. + left. eapply plus_left. apply step_skip_or_continue_for2. auto. + apply push_seq. + reflexivity. traceEq. + econstructor; eauto. econstructor; auto. econstructor; eauto. +(* dowhile false *) + inv H8. + exploit tr_top_val_for_test_inv; eauto. intros [b [A [B C]]]. subst. + econstructor; split. + left. simpl. eapply plus_left. constructor. + eapply star_right. apply step_makeif_false with v; auto. + constructor. + reflexivity. traceEq. + constructor; auto. constructor. +(* dowhile true *) + inv H8. + exploit tr_top_val_for_test_inv; eauto. intros [b [A [B C]]]. subst. + econstructor; split. + left. simpl. eapply plus_left. constructor. + eapply star_right. apply step_makeif_true with v; auto. + constructor. + reflexivity. traceEq. + constructor; auto. constructor; auto. +(* break dowhile *) + inv H6. inv H7. + econstructor; split. + left. apply plus_one. apply step_break_for2. + constructor; auto. constructor. + +(* for start *) + inv H7. congruence. + econstructor; split. + left; apply plus_one. constructor. + econstructor; eauto. constructor; auto. econstructor; eauto. +(* for *) + inv H6; try congruence. inv H2. + econstructor; split. + left. eapply plus_left. apply step_for_true with (Vint Int.one). + constructor. simpl; constructor. apply Int.one_not_zero. + eapply star_left. constructor. apply push_seq. + reflexivity. traceEq. + econstructor; eauto. constructor; auto. econstructor; eauto. +(* for false *) + inv H8. exploit tr_top_val_for_test_inv; eauto. intros [b [A [B C]]]. subst. + econstructor; split. + left. simpl. eapply plus_left. constructor. + eapply star_trans. apply step_makeif_false with v; auto. + eapply star_two. constructor. apply step_break_for2. + reflexivity. reflexivity. traceEq. + constructor; auto. constructor. +(* for true *) + inv H8. exploit tr_top_val_for_test_inv; eauto. intros [b [A [B C]]]. subst. + econstructor; split. + left. simpl. eapply plus_left. constructor. + eapply star_right. apply step_makeif_true with v; auto. + constructor. + reflexivity. traceEq. + constructor; auto. constructor; auto. +(* skip_or_continue for3 *) + assert (ts = Sskip \/ ts = Scontinue). destruct H; subst x; inv H7; auto. + inv H8. + econstructor; split. + left. apply plus_one. apply step_skip_or_continue_for2. auto. + econstructor; eauto. econstructor; auto. +(* break for3 *) + inv H6. inv H7. + econstructor; split. + left. apply plus_one. apply step_break_for2. + econstructor; eauto. constructor. +(* skip for4 *) + inv H6. inv H7. + econstructor; split. + left. apply plus_one. constructor. + econstructor; eauto. constructor; auto. + +(* return none *) + inv H8. econstructor; split. + left. apply plus_one. econstructor; eauto. + rewrite <- H. apply function_return_preserved; auto. + constructor. apply match_cont_call; auto. +(* return some 1 *) + inv H7. inv H1. econstructor; split. + left; eapply plus_left. constructor. apply push_seq. traceEq. + econstructor; eauto. constructor. auto. +(* return some 2 *) + inv H9. exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst. + econstructor; split. + left. eapply plus_two. constructor. econstructor. eauto. + replace (fn_return tf) with (C.fn_return f). eauto. + exploit transl_function_spec; eauto. intuition congruence. + eauto. traceEq. + constructor. apply match_cont_call; auto. +(* skip return *) + inv H9. + assert (is_call_cont tk). inv H10; simpl in *; auto. + econstructor; split. + left. apply plus_one. apply step_skip_call; eauto. + rewrite <- H0. apply function_return_preserved; auto. + constructor. auto. + +(* switch *) + inv H6. inv H1. + econstructor; split. + left; eapply plus_left. constructor. apply push_seq. traceEq. + econstructor; eauto. constructor; auto. +(* expr switch *) + inv H7. exploit tr_top_val_for_val_inv; eauto. intros [A [B C]]. subst. + econstructor; split. + left; eapply plus_two. constructor. econstructor; eauto. traceEq. + econstructor; eauto. + apply tr_seq_of_labeled_statement. apply tr_select_switch. auto. + constructor; auto. + +(* skip-or-break switch *) + assert (ts = Sskip \/ ts = Sbreak). destruct H; subst x; inv H7; auto. + inv H8. + econstructor; split. + left; apply plus_one. apply step_skip_break_switch. auto. + constructor; auto. constructor. + +(* continue switch *) + inv H6. inv H7. + econstructor; split. + left; apply plus_one. apply step_continue_switch. + constructor; auto. constructor. + +(* label *) + inv H6. econstructor; split. + left; apply plus_one. constructor. + constructor; auto. + +(* goto *) + inv H7. + exploit transl_function_spec; eauto. intros [A [B [C D]]]. + exploit tr_find_label. eexact A. apply match_cont_call. eauto. + instantiate (1 := lbl). rewrite H. + intros [ts' [tk' [P [Q R]]]]. + econstructor; split. + left. apply plus_one. econstructor; eauto. + econstructor; eauto. + +(* internal function *) + monadInv H7. + exploit transl_function_spec; eauto. intros [A [B [C D]]]. + econstructor; split. + left; apply plus_one. eapply step_internal_function. + rewrite C; rewrite D; auto. + rewrite C; rewrite D; eauto. + rewrite C; eauto. + constructor; auto. + +(* external function *) + monadInv H5. + econstructor; split. + left; apply plus_one. econstructor; eauto. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + constructor; auto. + +(* return *) + inv H3. + (* none *) + econstructor; split. + left; apply plus_one. constructor. + econstructor; eauto. + (* some *) + econstructor; split. + left; apply plus_one. constructor. + econstructor; eauto. +Qed. + +(** Semantic preservation *) + +Theorem simulation: + forall S1 t S2, Cstrategy.step ge S1 t S2 -> + forall S1' (MS: match_states S1 S1'), + exists S2', + (plus step tge S1' t S2' \/ + (star step tge S1' t S2' /\ measure S2 < measure S1)%nat) + /\ match_states S2 S2'. +Proof. + intros S1 t S2 STEP. destruct STEP. + apply estep_simulation; auto. + apply sstep_simulation; auto. +Qed. + +Lemma transl_initial_states: + forall S, + Csem.initial_state prog S -> + exists S', Clight.initial_state tprog S' /\ match_states S S'. +Proof. + intros. inv H. + exploit function_ptr_translated; eauto. intros [tf [FIND TR]]. + econstructor; split. + econstructor. + apply (Genv.init_mem_transf_partial _ _ TRANSL). eauto. + simpl. fold tge. rewrite symbols_preserved. + replace (prog_main tprog) with (prog_main prog). eexact H1. + symmetry. unfold transl_program in TRANSL. + eapply transform_partial_program_main; eauto. + eexact FIND. + rewrite <- H3. apply type_of_fundef_preserved. auto. + constructor. auto. constructor. +Qed. + +Lemma transl_final_states: + forall S S' r, + match_states S S' -> Csem.final_state S r -> Clight.final_state S' r. +Proof. + intros. inv H0. inv H. inv H4. constructor. +Qed. + +Theorem transl_program_correct: + forall (beh: program_behavior), + not_wrong beh -> Cstrategy.exec_program prog beh -> + Clight.exec_program tprog beh. +Proof. + unfold Cstrategy.exec_program, Clight.exec_program. intros. + eapply simulation_star_wf_preservation; eauto. + eexact transl_initial_states. + eexact transl_final_states. + instantiate (1 := ltof _ measure). apply well_founded_ltof. + exact simulation. +Qed. + +End PRESERVATION. -- cgit