diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-08-18 09:06:55 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-08-18 09:06:55 +0000 |
| commit | a15858a0a8fcea82db02fe8c9bd2ed912210419f (patch) | |
| tree | 5c0c19439f0d0f9e8873ce0dad2034cb9cafc4ba /cfrontend/Cstrategy.v | |
| parent | adedca3a1ff17ff8ac66eb2bcd533a50df0927a0 (diff) | |
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
Diffstat (limited to 'cfrontend/Cstrategy.v')
| -rw-r--r-- | cfrontend/Cstrategy.v | 2825 |
1 files changed, 2825 insertions, 0 deletions
diff --git a/cfrontend/Cstrategy.v b/cfrontend/Cstrategy.v new file mode 100644 index 0000000..3d81899 --- /dev/null +++ b/cfrontend/Cstrategy.v @@ -0,0 +1,2825 @@ +(* *********************************************************************) +(* *) +(* 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 GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** A deterministic evaluation strategy for C. *) + +Require Import Coq.Program.Equality. +Require Import Axioms. +Require Import Coqlib. +Require Import Errors. +Require Import Maps. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import AST. +Require Import Memory. +Require Import Events. +Require Import Globalenvs. +Require Import Smallstep. +Require Import Determinism. +Require Import Csyntax. +Require Import Csem. + +Section STRATEGY. + +Variable ge: genv. + +(** * Definition of the strategy *) + +(** We now formalize a particular strategy for reducing expressions which + is the one implemented by the CompCert compiler. It evaluates effectful + subexpressions first, in leftmost-innermost order, then finishes + with the evaluation of the remaining simple expression. *) + +(** Simple expressions are defined as follows. *) + +Fixpoint simple (a: expr) : Prop := + match a with + | Eloc _ _ _ => True + | Evar _ _ => True + | Ederef r _ => simple r + | Efield l1 _ _ => simple l1 + | Eval _ _ => True + | Evalof l _ => simple l + | Eaddrof l _ => simple l + | Eunop _ r1 _ => simple r1 + | Ebinop _ r1 r2 _ => simple r1 /\ simple r2 + | Ecast r1 _ => simple r1 + | Econdition _ _ _ _ => False + | Esizeof _ _ => True + | Eassign _ _ _ => False + | Eassignop _ _ _ _ _ => False + | Epostincr _ _ _ => False + | Ecomma _ _ _ => False + | Ecall _ _ _ => False + | Eparen _ _ => False + end. + +Fixpoint simplelist (rl: exprlist) : Prop := + match rl with Enil => True | Econs r rl' => simple r /\ simplelist rl' end. + +(** Simple expressions have interesting properties: their evaluations always + terminate, are deterministic, and preserve the memory state. + We seize this opportunity to define a big-step semantics for simple + expressions. *) + +Section SIMPLE_EXPRS. + +Variable e: env. +Variable m: mem. + +Inductive eval_simple_lvalue: expr -> block -> int -> Prop := + | esl_loc: forall b ofs ty, + eval_simple_lvalue (Eloc b ofs ty) b ofs + | esl_var_local: forall x ty b, + e!x = Some(b, ty) -> + eval_simple_lvalue (Evar x ty) b Int.zero + | esl_var_global: forall x ty b, + e!x = None -> + Genv.find_symbol ge x = Some b -> + type_of_global ge b = Some ty -> + eval_simple_lvalue (Evar x ty) b Int.zero + | esl_deref: forall r ty b ofs, + eval_simple_rvalue r (Vptr b ofs) -> + eval_simple_lvalue (Ederef r ty) b ofs + | esl_field_struct: forall l f ty b ofs id fList delta, + eval_simple_lvalue l b ofs -> + typeof l = Tstruct id fList -> field_offset f fList = OK delta -> + eval_simple_lvalue (Efield l f ty) b (Int.add ofs (Int.repr delta)) + | esl_field_union: forall l f ty b ofs id fList, + eval_simple_lvalue l b ofs -> + typeof l = Tunion id fList -> + eval_simple_lvalue (Efield l f ty) b ofs + +with eval_simple_rvalue: expr -> val -> Prop := + | esr_val: forall v ty, + eval_simple_rvalue (Eval v ty) v + | esr_rvalof: forall b ofs l ty v, + eval_simple_lvalue l b ofs -> + ty = typeof l -> + load_value_of_type ty m b ofs = Some v -> + eval_simple_rvalue (Evalof l ty) v + | esr_addrof: forall b ofs l ty, + eval_simple_lvalue l b ofs -> + eval_simple_rvalue (Eaddrof l ty) (Vptr b ofs) + | esr_unop: forall op r1 ty v1 v, + eval_simple_rvalue r1 v1 -> + sem_unary_operation op v1 (typeof r1) = Some v -> + eval_simple_rvalue (Eunop op r1 ty) v + | esr_binop: forall op r1 r2 ty v1 v2 v, + eval_simple_rvalue r1 v1 -> eval_simple_rvalue r2 v2 -> + sem_binary_operation op v1 (typeof r1) v2 (typeof r2) m = Some v -> + eval_simple_rvalue (Ebinop op r1 r2 ty) v + | esr_cast: forall ty r1 v1 v, + eval_simple_rvalue r1 v1 -> + cast v1 (typeof r1) ty v -> + eval_simple_rvalue (Ecast r1 ty) v + | esr_sizeof: forall ty1 ty, + eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ty1))). + +Inductive eval_simple_list: exprlist -> typelist -> list val -> Prop := + | esrl_nil: + eval_simple_list Enil Tnil nil + | esrl_cons: forall r rl ty tyl v vl v', + eval_simple_rvalue r v' -> cast v' (typeof r) ty v -> + eval_simple_list rl tyl vl -> + eval_simple_list (Econs r rl) (Tcons ty tyl) (v :: vl). + +Scheme eval_simple_rvalue_ind2 := Minimality for eval_simple_rvalue Sort Prop + with eval_simple_lvalue_ind2 := Minimality for eval_simple_lvalue Sort Prop. +Combined Scheme eval_simple_rvalue_lvalue_ind from eval_simple_rvalue_ind2, eval_simple_lvalue_ind2. + +End SIMPLE_EXPRS. + +(** Left reduction contexts. These contexts allow reducing to the right + of a binary operator only if the left subexpression is simple. *) + +Inductive leftcontext: kind -> kind -> (expr -> expr) -> Prop := + | lctx_top: forall k, + leftcontext k k (fun x => x) + | lctx_deref: forall k C ty, + leftcontext k RV C -> leftcontext k LV (fun x => Ederef (C x) ty) + | lctx_field: forall k C f ty, + leftcontext k LV C -> leftcontext k LV (fun x => Efield (C x) f ty) + | lctx_rvalof: forall k C ty, + leftcontext k LV C -> leftcontext k RV (fun x => Evalof (C x) ty) + | lctx_addrof: forall k C ty, + leftcontext k LV C -> leftcontext k RV (fun x => Eaddrof (C x) ty) + | lctx_unop: forall k C op ty, + leftcontext k RV C -> leftcontext k RV (fun x => Eunop op (C x) ty) + | lctx_binop_left: forall k C op e2 ty, + leftcontext k RV C -> leftcontext k RV (fun x => Ebinop op (C x) e2 ty) + | lctx_binop_right: forall k C op e1 ty, + simple e1 -> leftcontext k RV C -> + leftcontext k RV (fun x => Ebinop op e1 (C x) ty) + | lctx_cast: forall k C ty, + leftcontext k RV C -> leftcontext k RV (fun x => Ecast (C x) ty) + | lctx_condition: forall k C r2 r3 ty, + leftcontext k RV C -> leftcontext k RV (fun x => Econdition (C x) r2 r3 ty) + | lctx_assign_left: forall k C e2 ty, + leftcontext k LV C -> leftcontext k RV (fun x => Eassign (C x) e2 ty) + | lctx_assign_right: forall k C e1 ty, + simple e1 -> leftcontext k RV C -> + leftcontext k RV (fun x => Eassign e1 (C x) ty) + | lctx_assignop_left: forall k C op e2 tyres ty, + leftcontext k LV C -> leftcontext k RV (fun x => Eassignop op (C x) e2 tyres ty) + | lctx_assignop_right: forall k C op e1 tyres ty, + simple e1 -> leftcontext k RV C -> + leftcontext k RV (fun x => Eassignop op e1 (C x) tyres ty) + | lctx_postincr: forall k C id ty, + leftcontext k LV C -> leftcontext k RV (fun x => Epostincr id (C x) ty) + | lctx_call_left: forall k C el ty, + leftcontext k RV C -> leftcontext k RV (fun x => Ecall (C x) el ty) + | lctx_call_right: forall k C e1 ty, + simple e1 -> leftcontextlist k C -> + leftcontext k RV (fun x => Ecall e1 (C x) ty) + | lctx_comma: forall k C e2 ty, + leftcontext k RV C -> leftcontext k RV (fun x => Ecomma (C x) e2 ty) + | lctx_paren: forall k C ty, + leftcontext k RV C -> leftcontext k RV (fun x => Eparen (C x) ty) + +with leftcontextlist: kind -> (expr -> exprlist) -> Prop := + | lctx_list_head: forall k C el, + leftcontext k RV C -> leftcontextlist k (fun x => Econs (C x) el) + | lctx_list_tail: forall k C e1, + simple e1 -> leftcontextlist k C -> + leftcontextlist k (fun x => Econs e1 (C x)). + +Lemma leftcontext_context: + forall k1 k2 C, leftcontext k1 k2 C -> context k1 k2 C +with leftcontextlist_contextlist: + forall k C, leftcontextlist k C -> contextlist k C. +Proof. + induction 1; constructor; auto. + induction 1; constructor; auto. +Qed. + +Hint Resolve leftcontext_context. + +(** Strategy for reducing expressions. We reduce the leftmost innermost + non-simple subexpression, evaluating its arguments (which are necessarily + simple expressions) with the big-step semantics. + If there are none, the whole expression is simple and is evaluated in + one big step. *) + +Inductive estep: state -> trace -> state -> Prop := + + | step_expr: forall f r k e m v ty, + eval_simple_rvalue e m r v -> + match r with Eval _ _ => False | _ => True end -> + ty = typeof r -> + estep (ExprState f r k e m) + E0 (ExprState f (Eval v ty) k e m) + + | step_condition_true: forall f C r1 r2 r3 ty k e m v, + leftcontext RV RV C -> + eval_simple_rvalue e m r1 v -> + is_true v (typeof r1) -> + typeof r2 = ty -> + estep (ExprState f (C (Econdition r1 r2 r3 ty)) k e m) + E0 (ExprState f (C (Eparen r2 ty)) k e m) + + | step_condition_false: forall f C r1 r2 r3 ty k e m v, + leftcontext RV RV C -> + eval_simple_rvalue e m r1 v -> + is_false v (typeof r1) -> + typeof r3 = ty -> + estep (ExprState f (C (Econdition r1 r2 r3 ty)) k e m) + E0 (ExprState f (C (Eparen r3 ty)) k e m) + + | step_assign: forall f C l r ty k e m b ofs v v' m', + leftcontext RV RV C -> + eval_simple_lvalue e m l b ofs -> + eval_simple_rvalue e m r v -> + cast v (typeof r) (typeof l) v' -> + store_value_of_type (typeof l) m b ofs v' = Some m' -> + ty = typeof l -> + estep (ExprState f (C (Eassign l r ty)) k e m) + E0 (ExprState f (C (Eval v' ty)) k e m') + + | step_assignop: forall f C op l r tyres ty k e m b ofs v1 v2 v3 v4 m', + leftcontext RV RV C -> + eval_simple_lvalue e m l b ofs -> + load_value_of_type (typeof l) m b ofs = Some v1 -> + eval_simple_rvalue e m r v2 -> + sem_binary_operation op v1 (typeof l) v2 (typeof r) m = Some v3 -> + cast v3 tyres (typeof l) v4 -> + store_value_of_type (typeof l) m b ofs v4 = Some m' -> + ty = typeof l -> + estep (ExprState f (C (Eassignop op l r tyres ty)) k e m) + E0 (ExprState f (C (Eval v4 ty)) k e m') + + | step_postincr: forall f C id l ty k e m b ofs v1 v2 v3 m', + leftcontext RV RV C -> + eval_simple_lvalue e m l b ofs -> + load_value_of_type ty m b ofs = Some v1 -> + sem_incrdecr id v1 ty = Some v2 -> + cast v2 (typeconv ty) ty v3 -> + store_value_of_type ty m b ofs v3 = Some m' -> + ty = typeof l -> + estep (ExprState f (C (Epostincr id l ty)) k e m) + E0 (ExprState f (C (Eval v1 ty)) k e m') + + | step_comma: forall f C r1 r2 ty k e m v, + leftcontext RV RV C -> + eval_simple_rvalue e m r1 v -> + ty = typeof r2 -> + estep (ExprState f (C (Ecomma r1 r2 ty)) k e m) + E0 (ExprState f (C r2) k e m) + + | step_paren: forall f C r ty k e m v, + leftcontext RV RV C -> + eval_simple_rvalue e m r v -> + ty = typeof r -> + estep (ExprState f (C (Eparen r ty)) k e m) + E0 (ExprState f (C (Eval v ty)) k e m) + + | step_call: forall f C rf rargs ty k e m targs tres vf vargs fd, + leftcontext RV RV C -> + typeof rf = Tfunction targs tres -> + eval_simple_rvalue e m rf vf -> + eval_simple_list e m rargs targs vargs -> + Genv.find_funct ge vf = Some fd -> + type_of_fundef fd = Tfunction targs tres -> + estep (ExprState f (C (Ecall rf rargs ty)) k e m) + E0 (Callstate fd vargs (Kcall f e C ty k) m). + +Definition step (S: state) (t: trace) (S': state) : Prop := + estep S t S' \/ sstep ge S t S'. + +(** * Safe executions. *) + +(** A C program is safe (in the nondeterministic strategy) + if it cannot get stuck. The definition is parameterized by + an external world (cf. file [Determinism]) to constrain the behavior + of external functions. *) + +Inductive immsafe: world -> state -> Prop := + | immsafe_final: forall w s r, + final_state s r -> + immsafe w s + | immsafe_step: forall w s t s' w', + Csem.step ge s t s' -> possible_trace w t w' -> + immsafe w s. + +Definition safe (w: world) (s: Csem.state) : Prop := + forall t s' w', star Csem.step ge s t s' -> possible_trace w t w' -> immsafe w' s'. + +Lemma safe_steps: + forall w s t s' w', + safe w s -> star Csem.step ge s t s' -> possible_trace w t w' -> safe w' s'. +Proof. + intros; red; intros. + eapply H. eapply star_trans; eauto. eapply possible_trace_app; eauto. +Qed. + +Lemma safe_imm: + forall w s, safe w s -> immsafe w s. +Proof. + intros. eapply H. apply star_refl. constructor. +Qed. + +Lemma not_stuck_val: + forall e v ty m, + not_stuck ge e (Eval v ty) m. +Proof. + intros; red; intros. inv H; try congruence. subst e'. constructor. +Qed. + +Lemma safe_not_stuck: + forall w f a k e m, + safe w (ExprState f a k e m) -> + not_stuck ge e a m. +Proof. + intros. exploit safe_imm; eauto; intro IS; inv IS. + inv H0. + inv H0. inv H2; auto; apply not_stuck_val. inv H2; apply not_stuck_val. +Qed. + +Lemma safe_not_imm_stuck: + forall k C w f a K e m, + safe w (ExprState f (C a) K e m) -> + context k RV C -> + not_imm_stuck ge e k a m. +Proof. + intros. exploit safe_not_stuck; eauto. +Qed. + +(** Simple, non-stuck expressions are well-formed with respect to + l-values and r-values. *) + +Lemma context_compose: + forall k2 k3 C2, context k2 k3 C2 -> + forall k1 C1, context k1 k2 C1 -> + context k1 k3 (fun x => C2(C1 x)) +with contextlist_compose: + forall k2 C2, contextlist k2 C2 -> + forall k1 C1, context k1 k2 C1 -> + contextlist k1 (fun x => C2(C1 x)). +Proof. + induction 1; intros; try (constructor; eauto). + replace (fun x => C1 x) with C1. auto. apply extensionality; auto. + induction 1; intros; constructor; eauto. +Qed. + +Definition expr_kind (a: expr) : kind := + match a with + | Eloc _ _ _ => LV + | Evar _ _ => LV + | Ederef _ _ => LV + | Efield _ _ _ => LV + | _ => RV + end. + +Lemma lred_kind: + forall e a m a' m', lred ge e a m a' m' -> expr_kind a = LV. +Proof. + induction 1; auto. +Qed. + +Lemma rred_kind: + forall a m a' m', rred a m a' m' -> expr_kind a = RV. +Proof. + induction 1; auto. +Qed. + +Lemma callred_kind: + forall a fd args ty, callred ge a fd args ty -> expr_kind a = RV. +Proof. + induction 1; auto. +Qed. + +Lemma context_kind: + forall a from to C, context from to C -> expr_kind a = from -> expr_kind (C a) = to. +Proof. + induction 1; intros; simpl; auto. +Qed. + +Lemma not_imm_stuck_kind: + forall e k a m, not_imm_stuck ge e k a m -> expr_kind a = k. +Proof. + induction 1. + auto. + auto. + eapply context_kind; eauto. eapply lred_kind; eauto. + eapply context_kind; eauto. eapply rred_kind; eauto. + eapply context_kind; eauto. eapply callred_kind; eauto. +Qed. + +Lemma safe_expr_kind: + forall from C w f a k e m, + context from RV C -> + safe w (ExprState f (C a) k e m) -> + expr_kind a = from. +Proof. + intros. eapply not_imm_stuck_kind. eapply safe_not_imm_stuck; eauto. +Qed. + +(** Painful inversion lemmas on particular states that are not stuck. *) + +Section INVERSION_LEMMAS. + +Variable e: env. + +Fixpoint exprlist_all_values (rl: exprlist) : Prop := + match rl with + | Enil => True + | Econs (Eval v ty) rl' => exprlist_all_values rl' + | Econs _ _ => False + end. + +Definition invert_expr_prop (a: expr) (m: mem) : Prop := + match a with + | Eloc b ofs ty => False + | Evar x ty => + exists b, + e!x = Some(b, ty) + \/ (e!x = None /\ Genv.find_symbol ge x = Some b /\ type_of_global ge b = Some ty) + | Ederef (Eval v ty1) ty => + exists b, exists ofs, v = Vptr b ofs + | Efield (Eloc b ofs ty1) f ty => + match ty1 with + | Tstruct _ fList => exists delta, field_offset f fList = Errors.OK delta + | Tunion _ _ => True + | _ => False + end + | Eval v ty => False + | Evalof (Eloc b ofs ty') ty => + ty' = ty /\ exists v, load_value_of_type ty m b ofs = Some v + | Eunop op (Eval v1 ty1) ty => + exists v, sem_unary_operation op v1 ty1 = Some v + | Ebinop op (Eval v1 ty1) (Eval v2 ty2) ty => + exists v, sem_binary_operation op v1 ty1 v2 ty2 m = Some v + | Ecast (Eval v1 ty1) ty => + exists v, cast v1 ty1 ty v + | Econdition (Eval v1 ty1) r1 r2 ty => + ((is_true v1 ty1 /\ typeof r1 = ty) \/ (is_false v1 ty1 /\ typeof r2 = ty)) + | Eassign (Eloc b ofs ty1) (Eval v2 ty2) ty => + exists v, exists m', + ty = ty1 /\ cast v2 ty2 ty1 v /\ store_value_of_type ty1 m b ofs v = Some m' + | Eassignop op (Eloc b ofs ty1) (Eval v2 ty2) tyres ty => + exists v1, exists v, exists v', exists m', + ty = ty1 + /\ load_value_of_type ty1 m b ofs = Some v1 + /\ sem_binary_operation op v1 ty1 v2 ty2 m = Some v + /\ cast v tyres ty1 v' + /\ store_value_of_type ty1 m b ofs v' = Some m' + | Epostincr id (Eloc b ofs ty1) ty => + exists v1, exists v2, exists v3, exists m', + ty = ty1 + /\ load_value_of_type ty m b ofs = Some v1 + /\ sem_incrdecr id v1 ty = Some v2 + /\ cast v2 (typeconv ty) ty v3 + /\ store_value_of_type ty m b ofs v3 = Some m' + | Ecomma (Eval v ty1) r2 ty => + typeof r2 = ty + | Eparen (Eval v ty1) ty => + ty = ty1 + | Ecall (Eval vf tyf) rargs ty => + exprlist_all_values rargs -> + exists tyargs, exists tyres, exists fd, exists vl, + tyf = Tfunction tyargs tyres + /\ Genv.find_funct ge vf = Some fd + /\ cast_arguments rargs tyargs vl + /\ type_of_fundef fd = Tfunction tyargs tyres + | _ => True + end. + +Lemma lred_invert: + forall l m l' m', lred ge e l m l' m' -> invert_expr_prop l m. +Proof. + induction 1; red; auto. + exists b; auto. + exists b; auto. + exists b; exists ofs; auto. + exists delta; auto. +Qed. + +Lemma rred_invert: + forall r m r' m', rred r m r' m' -> invert_expr_prop r m. +Proof. + induction 1; red; auto. + split; auto; exists v; auto. + exists v; auto. + exists v; auto. + exists v; auto. + exists v; exists m'; auto. + exists v1; exists v; exists v'; exists m'; auto. + exists v1; exists v2; exists v3; exists m'; auto. + destruct r; auto. +Qed. + +Lemma callred_invert: + forall r fd args ty m, + callred ge r fd args ty -> + invert_expr_prop r m. +Proof. + intros. inv H. simpl. + intros. exists tyargs; exists tyres; exists fd; exists args; auto. +Qed. + +Scheme context_ind2 := Minimality for context Sort Prop + with contextlist_ind2 := Minimality for contextlist Sort Prop. +Combined Scheme context_contextlist_ind from context_ind2, contextlist_ind2. + +Lemma invert_expr_context: + (forall from to C, context from to C -> + forall a m, + invert_expr_prop a m -> + invert_expr_prop (C a) m) +/\(forall from C, contextlist from C -> + forall a m, + invert_expr_prop a m -> + ~exprlist_all_values (C a)). +Proof. + apply context_contextlist_ind; intros; try (exploit H0; [eauto|intros]). + auto. + simpl. destruct (C a); auto. contradiction. + simpl. destruct (C a); auto. contradiction. + simpl. destruct (C a); auto. contradiction. + simpl. auto. + simpl. destruct (C a); auto. contradiction. + simpl. destruct (C a); auto. contradiction. + simpl. + destruct e1; auto. destruct (C a); auto. contradiction. + simpl. destruct (C a); auto. contradiction. + simpl. destruct (C a); auto. contradiction. + simpl. destruct (C a); auto. contradiction. + simpl. + destruct e1; auto. destruct (C a); auto. contradiction. + simpl. destruct (C a); auto. contradiction. + simpl. + destruct e1; auto. destruct (C a); auto. contradiction. + simpl. destruct (C a); auto. contradiction. + simpl. destruct (C a); auto. contradiction. + simpl. destruct e1; auto. intros. elim (H0 a m); auto. + simpl. destruct (C a); auto. contradiction. + simpl. destruct (C a); auto. contradiction. + simpl. red; intros. destruct (C a); auto. + simpl; red; intros. destruct e1; auto. elim (H0 a m); auto. +Qed. + +Lemma not_imm_stuck_inv: + forall k a m, + not_imm_stuck ge e k a m -> + match a with + | Eloc _ _ _ => True + | Eval _ _ => True + | _ => invert_expr_prop a m + end. +Proof. + destruct invert_expr_context as [A B]. + intros. inv H. + auto. + auto. + assert (invert_expr_prop (C e0) m). + eapply A; eauto. eapply lred_invert; eauto. + red in H. destruct (C e0); auto; contradiction. + assert (invert_expr_prop (C e0) m). + eapply A; eauto. eapply rred_invert; eauto. + red in H. destruct (C e0); auto; contradiction. + assert (invert_expr_prop (C e0) m). + eapply A; eauto. eapply callred_invert; eauto. + red in H. destruct (C e0); auto; contradiction. +Qed. + +End INVERSION_LEMMAS. + +(** * Correctness of the strategy. *) + +Section SIMPLE_EVAL. + +Variable f: function. +Variable k: cont. +Variable e: env. +Variable m: mem. +Variable w: world. + +Lemma simple_eval: + forall a from C, + simple a -> context from RV C -> safe w (ExprState f (C a) k e m) -> + match from with + | LV => + exists b, exists ofs, + eval_simple_lvalue e m a b ofs + /\ star Csem.step ge (ExprState f (C a) k e m) + E0 (ExprState f (C (Eloc b ofs (typeof a))) k e m) + | RV => + exists v, + eval_simple_rvalue e m a v + /\ star Csem.step ge (ExprState f (C a) k e m) + E0 (ExprState f (C (Eval v (typeof a))) k e m) + end. +Proof. + induction a; intros from C S CTX SAFE; + generalize (safe_expr_kind _ _ _ _ _ _ _ _ CTX SAFE); intro K; subst; + simpl in S; try contradiction; simpl. +(* val *) + exists v; split. constructor. apply star_refl. +(* var *) + exploit not_imm_stuck_inv. eapply safe_not_imm_stuck; eauto. + simpl. intros [b A]. + exists b; exists Int.zero; split. + intuition. apply esl_var_local; auto. apply esl_var_global; auto. + apply star_one. left; apply step_lred. + intuition. apply red_var_local; auto. apply red_var_global; auto. + eapply safe_not_stuck; eauto. auto. +(* field *) + set (C1 := fun x => Efield x f0 ty). + set (C2 := fun x => C(C1 x)). + exploit (IHa LV C2); auto. eapply context_compose; eauto. repeat constructor. + unfold C2, C1; intros [b [ofs [A B]]]. + exploit not_imm_stuck_inv. + eapply safe_not_imm_stuck. eapply safe_steps; eauto. constructor. eauto. + simpl. + case_eq (typeof a); intros; try contradiction. + destruct H0 as [delta EQ]. + exists b; econstructor; split. + eapply esl_field_struct; eauto. + eapply star_right. eauto. left; apply step_lred. + rewrite H. constructor; auto. + eapply safe_not_stuck. eapply safe_steps; eauto. constructor. auto. + traceEq. + exists b; exists ofs; split. + eapply esl_field_union; eauto. + eapply star_right. eauto. left; apply step_lred. + rewrite H. constructor; auto. + eapply safe_not_stuck. eapply safe_steps; eauto. constructor. auto. + traceEq. +(* valof *) + set (C1 := fun x => Evalof x ty). + set (C2 := fun x => C(C1 x)). + exploit (IHa LV C2); auto. eapply context_compose; eauto. repeat constructor. + unfold C2, C1; intros [b [ofs [A B]]]. + exploit not_imm_stuck_inv. + eapply safe_not_imm_stuck. eapply safe_steps; eauto. constructor. eauto. + simpl. intros [D [v E]]. + exists v; split. + econstructor; eauto. + eapply star_right. eauto. left; apply step_rred. + simpl. rewrite D. constructor. auto. + eapply safe_not_stuck. eapply safe_steps; eauto. constructor. auto. + traceEq. +(* deref *) + set (C1 := fun x => Ederef x ty). + set (C2 := fun x => C(C1 x)). + exploit (IHa RV C2); auto. eapply context_compose; eauto. repeat constructor. + unfold C2, C1; intros [v1 [A B]]. + exploit not_imm_stuck_inv. + eapply safe_not_imm_stuck. eapply safe_steps; eauto. constructor. eauto. + simpl. intros [b [ofs D]]. subst v1. + exists b; exists ofs; split. + econstructor; eauto. + eapply star_right. eauto. left; apply step_lred. + simpl. constructor. + eapply safe_not_stuck. eapply safe_steps; eauto. constructor. auto. + traceEq. +(* addrof *) + set (C1 := fun x => Eaddrof x ty). + set (C2 := fun x => C(C1 x)). + exploit (IHa LV C2); auto. eapply context_compose; eauto. repeat constructor. + unfold C2, C1; intros [b [ofs [A B]]]. + exists (Vptr b ofs); split. + econstructor; eauto. + eapply star_right. eauto. left; apply step_rred. + simpl. constructor. + eapply safe_not_stuck. eapply safe_steps; eauto. constructor. auto. + traceEq. +(* unop *) + set (C1 := fun x => Eunop op x ty). + set (C2 := fun x => C(C1 x)). + exploit (IHa RV C2); auto. eapply context_compose; eauto. repeat constructor. + unfold C2, C1; intros [v1 [A B]]. + exploit not_imm_stuck_inv. + eapply safe_not_imm_stuck. eapply safe_steps; eauto. constructor. eauto. + simpl. intros [v E]. + exists v; split. + econstructor; eauto. + eapply star_right. eauto. left; apply step_rred. + simpl. constructor. auto. + eapply safe_not_stuck. eapply safe_steps; eauto. constructor. auto. + traceEq. +(* binop *) + set (C1 := fun x => Ebinop op x a2 ty). + set (C2 := fun x => C(C1 x)). + exploit (IHa1 RV C2). tauto. eapply context_compose; eauto. repeat constructor. auto. + unfold C2, C1; intros [v1 [A B]]. + assert (safe w (ExprState f (C (Ebinop op (Eval v1 (typeof a1)) a2 ty)) k e m)). + eapply safe_steps; eauto. constructor. + set (C3 := fun x => Ebinop op (Eval v1 (typeof a1)) x ty). + set (C4 := fun x => C(C3 x)). + exploit (IHa2 RV C4). tauto. eapply context_compose; eauto. repeat constructor. auto. + unfold C4, C3; intros [v2 [D E]]. + assert (safe w (ExprState f (C (Ebinop op (Eval v1 (typeof a1)) (Eval v2 (typeof a2)) ty)) k e m)). + eapply safe_steps; eauto. constructor. + exploit not_imm_stuck_inv. + eapply safe_not_imm_stuck. eexact H0. eauto. + simpl. intros [v F]. + exists v; split. + econstructor; eauto. + eapply star_right. eapply star_trans; eauto. left; apply step_rred. + simpl. constructor. auto. + eapply safe_not_stuck. eauto. + auto. + traceEq. +(* cast *) + set (C1 := fun x => Ecast x ty). + set (C2 := fun x => C(C1 x)). + exploit (IHa RV C2); auto. eapply context_compose; eauto. repeat constructor. + unfold C2, C1; intros [v1 [A B]]. + exploit not_imm_stuck_inv. + eapply safe_not_imm_stuck. eapply safe_steps; eauto. constructor. eauto. + simpl. intros [v E]. + exists v; split. + econstructor; eauto. + eapply star_right. eauto. left; apply step_rred. + simpl. constructor. auto. + eapply safe_not_stuck. eapply safe_steps; eauto. constructor. auto. + traceEq. +(* sizeof *) + econstructor; split. constructor. + apply star_one. left; apply step_rred. constructor. + eapply safe_not_stuck; eauto. + auto. +(* loc *) + exploit not_imm_stuck_inv. eapply safe_not_imm_stuck; eauto. + simpl. intros. + exists b; exists ofs; split. constructor. apply star_refl. +Qed. + +Lemma simple_eval_r: + forall r C, + simple r -> context RV RV C -> safe w (ExprState f (C r) k e m) -> + exists v, + eval_simple_rvalue e m r v + /\ star Csem.step ge (ExprState f (C r) k e m) + E0 (ExprState f (C (Eval v (typeof r))) k e m). +Proof. + intros. apply (simple_eval r RV); auto. +Qed. + +Lemma simple_eval_l: + forall l C, + simple l -> context LV RV C -> safe w (ExprState f (C l) k e m) -> + exists b, exists ofs, + eval_simple_lvalue e m l b ofs + /\ star Csem.step ge (ExprState f (C l) k e m) + E0 (ExprState f (C (Eloc b ofs (typeof l))) k e m). +Proof. + intros. apply (simple_eval l LV); auto. +Qed. + +Fixpoint rval_list (vl: list val) (rl: exprlist) : exprlist := + match vl, rl with + | v1 :: vl', Econs r1 rl' => Econs (Eval v1 (typeof r1)) (rval_list vl' rl') + | _, _ => Enil + end. + +Inductive eval_simple_list': exprlist -> list val -> Prop := + | esrl'_nil: + eval_simple_list' Enil nil + | esrl'_cons: forall r rl v vl, + eval_simple_rvalue e m r v -> + eval_simple_list' rl vl -> + eval_simple_list' (Econs r rl) (v :: vl). + +Fixpoint exprlist_app (rl1 rl2: exprlist) : exprlist := + match rl1 with + | Enil => rl2 + | Econs r1 rl1' => Econs r1 (exprlist_app rl1' rl2) + end. + +Lemma exprlist_app_assoc: + forall rl2 rl3 rl1, + exprlist_app (exprlist_app rl1 rl2) rl3 = + exprlist_app rl1 (exprlist_app rl2 rl3). +Proof. + induction rl1; auto. simpl. congruence. +Qed. + +Inductive contextlist' : (exprlist -> expr) -> Prop := + | contextlist'_intro: forall r1 rl0 ty C, + context RV RV C -> + contextlist' (fun rl => C (Ecall r1 (exprlist_app rl0 rl) ty)). + +Lemma exprlist_app_context: + forall rl1 rl2, + contextlist RV (fun x => exprlist_app rl1 (Econs x rl2)). +Proof. + induction rl1; simpl; intros. + apply ctx_list_head. constructor. + apply ctx_list_tail. auto. +Qed. + +Lemma contextlist'_head: + forall rl C, + contextlist' C -> + context RV RV (fun x => C (Econs x rl)). +Proof. + intros. inv H. + set (C' := fun x => Ecall r1 (exprlist_app rl0 (Econs x rl)) ty). + assert (context RV RV C'). constructor. apply exprlist_app_context. + change (context RV RV (fun x => C0 (C' x))). + eapply context_compose; eauto. +Qed. + +Lemma contextlist'_tail: + forall r1 C, + contextlist' C -> + contextlist' (fun x => C (Econs r1 x)). +Proof. + intros. inv H. + replace (fun x => C0 (Ecall r0 (exprlist_app rl0 (Econs r1 x)) ty)) + with (fun x => C0 (Ecall r0 (exprlist_app (exprlist_app rl0 (Econs r1 Enil)) x) ty)). + constructor. auto. + apply extensionality; intros. f_equal. f_equal. apply exprlist_app_assoc. +Qed. + +Lemma simple_eval_rlist: + forall rl C, + simplelist rl -> + contextlist' C -> + safe w (ExprState f (C rl) k e m) -> + exists vl, + eval_simple_list' rl vl + /\ star Csem.step ge (ExprState f (C rl) k e m) + E0 (ExprState f (C (rval_list vl rl)) k e m). +Proof. + induction rl; intros. + econstructor; split. constructor. simpl. apply star_refl. + simpl in H; destruct H. + set (C1 := fun x => C (Econs x rl)). + exploit (simple_eval_r r1 C1). auto. apply contextlist'_head. auto. auto. + unfold C1; intros [v [X Y]]. + assert (safe w (ExprState f (C (Econs (Eval v (typeof r1)) rl)) k e m)). + eapply safe_steps; eauto. constructor. + set (C2 := fun x => C (Econs (Eval v (typeof r1)) x)). + destruct (IHrl C2) as [vl [U V]]. auto. apply contextlist'_tail. auto. auto. + unfold C2 in V. + exists (v :: vl); split. constructor; auto. + simpl. eapply star_trans; eauto. +Qed. + +Lemma rval_list_all_values: + forall vl rl, exprlist_all_values (rval_list vl rl). +Proof. + induction vl; simpl; intros. auto. + destruct rl; simpl; auto. +Qed. + +Lemma can_eval_simple_list: + forall rl vl, + eval_simple_list' rl vl -> + forall tyl vl', + cast_arguments (rval_list vl rl) tyl vl' -> + eval_simple_list e m rl tyl vl'. +Proof. + induction 1; simpl; intros. + inv H. constructor. + inv H1. econstructor; eauto. +Qed. + +End SIMPLE_EVAL. + +(** Decomposition *) + +Section DECOMPOSITION. + +Variable f: function. +Variable k: cont. +Variable e: env. +Variable m: mem. +Variable w: world. + +Definition simple_side_effect (r: expr) : Prop := + match r with + | Econdition r1 r2 r3 ty => simple r1 + | Eassign l1 r2 _ => simple l1 /\ simple r2 + | Eassignop _ l1 r2 _ _ => simple l1 /\ simple r2 + | Epostincr _ l1 _ => simple l1 + | Ecomma r1 r2 _ => simple r1 + | Ecall r1 rl _ => simple r1 /\ simplelist rl + | Eparen r1 _ => simple r1 + | _ => False + end. + +Scheme expr_ind2 := Induction for expr Sort Prop + with exprlist_ind2 := Induction for exprlist Sort Prop. +Combined Scheme expr_expr_list_ind from expr_ind2, exprlist_ind2. + +Lemma decompose_expr: + (forall a from C, + context from RV C -> safe w (ExprState f (C a) k e m) -> + simple a + \/ exists C', exists a', simple_side_effect a' /\ leftcontext RV from C' /\ a = C' a') +/\(forall rl C, + contextlist' C -> safe w (ExprState f (C rl) k e m) -> + simplelist rl + \/ exists C', exists a', simple_side_effect a' /\ leftcontextlist RV C' /\ rl = C' a'). +Proof. + apply expr_expr_list_ind; intros; simpl; auto. +(* field *) + exploit safe_expr_kind; eauto; simpl; intros. subst. + destruct (H LV (fun x => C (Efield x f0 ty))) as [A | [C' [a' [A [B D]]]]]. + eapply context_compose; eauto. repeat constructor. auto. + auto. + right; exists (fun x => Efield (C' x) f0 ty); exists a'. + split. auto. split. constructor; auto. rewrite D; auto. +(* rvalof *) + exploit safe_expr_kind; eauto; simpl; intros. subst. + destruct (H LV (fun x => C (Evalof x ty))) as [A | [C' [a' [A [B D]]]]]. + eapply context_compose; eauto. repeat constructor. auto. + auto. + right; exists (fun x => Evalof (C' x) ty); exists a'. + split. auto. split. constructor; auto. rewrite D; auto. +(* deref *) + exploit safe_expr_kind; eauto; simpl; intros. subst. + subst. destruct (H RV (fun x => C (Ederef x ty))) as [A | [C' [a' [A [B D]]]]]. + eapply context_compose; eauto. repeat constructor. auto. + auto. + right; exists (fun x => Ederef (C' x) ty); exists a'. + split. auto. split. constructor; auto. rewrite D; auto. +(* addrof *) + exploit safe_expr_kind; eauto; simpl; intros. subst. + destruct (H LV (fun x => C (Eaddrof x ty))) as [A | [C' [a' [A [B D]]]]]. + eapply context_compose; eauto. repeat constructor. auto. + auto. + right; exists (fun x => Eaddrof (C' x) ty); exists a'. + split. auto. split. constructor; auto. rewrite D; auto. +(* unop *) + exploit safe_expr_kind; eauto; simpl; intros. subst. + destruct (H RV (fun x => C (Eunop op x ty))) as [A | [C' [a' [A [B D]]]]]. + eapply context_compose; eauto. repeat constructor. auto. + auto. + right; exists (fun x => Eunop op (C' x) ty); exists a'. + split. auto. split. constructor; auto. rewrite D; auto. +(* binop *) + exploit safe_expr_kind; eauto; simpl; intros. subst. + destruct (H RV (fun x => C (Ebinop op x r2 ty))) as [A | [C' [a' [A [B D]]]]]. + eapply context_compose; eauto. repeat constructor. auto. + destruct (H0 RV (fun x => C (Ebinop op r1 x ty))) as [A' | [C' [a' [A' [B D]]]]]. + eapply context_compose; eauto. repeat constructor. auto. + auto. + right; exists (fun x => Ebinop op r1 (C' x) ty); exists a'. + split. auto. split. constructor; auto. rewrite D; auto. + right; exists (fun x => Ebinop op (C' x) r2 ty); exists a'. + split. auto. split. constructor; auto. rewrite D; auto. +(* cast *) + exploit safe_expr_kind; eauto; simpl; intros. subst. + destruct (H RV (fun x => C (Ecast x ty))) as [A | [C' [a' [A [B D]]]]]. + eapply context_compose; eauto. repeat constructor. auto. + auto. + right; exists (fun x => Ecast (C' x) ty); exists a'. + split. auto. split. constructor; auto. rewrite D; auto. +(* condition *) + exploit safe_expr_kind; eauto; simpl; intros. subst. + destruct (H RV (fun x => C(Econdition x r2 r3 ty))) as [A | [C' [a' [A [B D]]]]]. + eapply context_compose; eauto. repeat constructor. auto. + right. exists (fun x => x); exists (Econdition r1 r2 r3 ty). + split. red; auto. split. constructor. auto. + right; exists (fun x => Econdition (C' x) r2 r3 ty); exists a'. + split. auto. split. constructor; auto. rewrite D; auto. +(* assign *) + exploit safe_expr_kind; eauto; simpl; intros. subst. + destruct (H LV (fun x => C (Eassign x r ty))) as [A | [C' [a' [A [B D]]]]]. + eapply context_compose; eauto. repeat constructor. auto. + destruct (H0 RV (fun x => C (Eassign l x ty))) as [A' | [C' [a' [A' [B D]]]]]. + eapply context_compose; eauto. repeat constructor. auto. + right. exists (fun x => x); exists (Eassign l r ty). + split. red; auto. split. constructor. auto. + right; exists (fun x => Eassign l (C' x) ty); exists a'. + split. auto. split. constructor; auto. rewrite D; auto. + right; exists (fun x => Eassign (C' x) r ty); exists a'. + split. auto. split. constructor; auto. rewrite D; auto. +(* assignop *) + exploit safe_expr_kind; eauto; simpl; intros. subst. + destruct (H LV (fun x => C (Eassignop op x r tyres ty))) as [A | [C' [a' [A [B D]]]]]. + eapply context_compose; eauto. repeat constructor. auto. + destruct (H0 RV (fun x => C (Eassignop op l x tyres ty))) as [A' | [C' [a' [A' [B D]]]]]. + eapply context_compose; eauto. repeat constructor. auto. + right. exists (fun x => x); exists (Eassignop op l r tyres ty). + split. red; auto. split. constructor. auto. + right; exists (fun x => Eassignop op l (C' x) tyres ty); exists a'. + split. auto. split. constructor; auto. rewrite D; auto. + right; exists (fun x => Eassignop op (C' x) r tyres ty); exists a'. + split. auto. split. constructor; auto. rewrite D; auto. +(* postincr *) + exploit safe_expr_kind; eauto; simpl; intros. subst. + destruct (H LV (fun x => C(Epostincr id x ty))) as [A | [C' [a' [A [B D]]]]]. + eapply context_compose; eauto. repeat constructor. auto. + right. exists (fun x => x); exists (Epostincr id l ty). + split. red; auto. split. constructor. auto. + right; exists (fun x => Epostincr id (C' x) ty); exists a'. + split. auto. split. econstructor; eauto. rewrite D; auto. +(* comma *) + exploit safe_expr_kind; eauto; simpl; intros. subst. + destruct (H RV (fun x => C(Ecomma x r2 ty))) as [A | [C' [a' [A [B D]]]]]. + eapply context_compose; eauto. repeat constructor. auto. + right. exists (fun x => x); exists (Ecomma r1 r2 ty). + split. red; auto. split. constructor. auto. + right; exists (fun x => Ecomma (C' x) r2 ty); exists a'. + split. auto. split. econstructor; eauto. rewrite D; auto. +(* call *) + exploit safe_expr_kind; eauto; simpl; intros. subst. + destruct (H RV (fun x => C (Ecall x rargs ty))) as [A | [C' [a' [A [B D]]]]]. + eapply context_compose; eauto. repeat constructor. auto. + destruct (H0 (fun x => C (Ecall r1 x ty))) as [A' | [C' [a' [A' [B D]]]]]. + eapply contextlist'_intro with (C := C) (rl0 := Enil). auto. auto. + right. exists (fun x => x); exists (Ecall r1 rargs ty). + split. red; auto. split. constructor. auto. + right; exists (fun x => Ecall r1 (C' x) ty); exists a'. + split. auto. split. constructor; auto. rewrite D; auto. + right; exists (fun x => Ecall (C' x) rargs ty); exists a'. + split. auto. split. constructor; auto. rewrite D; auto. +(* rparen *) + exploit safe_expr_kind; eauto; simpl; intros. subst. + destruct (H RV (fun x => C (Eparen x ty))) as [A | [C' [a' [A [B D]]]]]. + eapply context_compose; eauto. repeat constructor. auto. + right. exists (fun x => x); exists (Eparen r ty). + split. red; auto. split. constructor. auto. + right; exists (fun x => Eparen (C' x) ty); exists a'. + split. auto. split. econstructor; eauto. rewrite D; auto. +(* cons *) + destruct (H RV (fun x => C (Econs x rl))) as [A | [C' [a' [A [B D]]]]]. + eapply contextlist'_head; eauto. auto. + destruct (H0 (fun x => C (Econs r1 x))) as [A' | [C' [a' [A' [B D]]]]]. + eapply contextlist'_tail; eauto. auto. + auto. + right; exists (fun x => Econs r1 (C' x)); exists a'. + split. auto. split. constructor; auto. rewrite D; auto. + right; exists (fun x => Econs (C' x) rl); exists a'. + split. auto. split. constructor; auto. rewrite D; auto. +Qed. + +Lemma decompose_topexpr: + forall a, + safe w (ExprState f a k e m) -> + simple a + \/ exists C, exists a', simple_side_effect a' /\ leftcontext RV RV C /\ a = C a'. +Proof. + intros. eapply (proj1 decompose_expr). apply ctx_top. auto. +Qed. + +End DECOMPOSITION. + +(** Simulation for expressions. *) + +Lemma can_estep: + forall w f a k e m, + safe w (ExprState f a k e m) -> + match a with Eval _ _ => False | _ => True end -> + exists S, + estep (ExprState f a k e m) E0 S + /\ plus Csem.step ge (ExprState f a k e m) E0 S. +Proof. + intros. destruct (decompose_topexpr f k e m w a H) as [A | [C [b [P [Q R]]]]]. +(* expr *) + exploit (simple_eval_r f k e m w a (fun x => x)); auto. constructor. + intros [v [S T]]. + econstructor; split. + eapply step_expr; eauto. + inversion T. rewrite H2 in H0. contradiction. econstructor; eauto. +(* side effect *) + clear H0. subst a. red in P. destruct b; try contradiction. +(* condition *) + set (C1 := fun x => Econdition x b2 b3 ty). + exploit (simple_eval_r f k e m w b1 (fun x => C(C1 x))). auto. + eapply context_compose; eauto. repeat constructor. auto. + unfold C1; intros [v [A B]]. + exploit not_imm_stuck_inv. + eapply safe_not_imm_stuck. eapply safe_steps; eauto. constructor. eauto. + simpl. intros [[X Y] | [X Y]]. + econstructor; split. eapply step_condition_true; eauto. + eapply plus_right. eauto. left; eapply step_rred. constructor; auto. + eapply safe_not_stuck. eapply safe_steps; eauto. constructor. apply leftcontext_context; auto. + traceEq. + econstructor; split. eapply step_condition_false; eauto. + eapply plus_right. eauto. left; eapply step_rred. constructor; auto. + eapply safe_not_stuck. eapply safe_steps; eauto. constructor. apply leftcontext_context; auto. + traceEq. +(* assign *) + destruct P. + set (C1 := fun x => Eassign x b2 ty). + exploit (simple_eval_l f k e m w b1 (fun x => C(C1 x))). auto. + eapply context_compose; eauto. repeat constructor. auto. + unfold C1; intros [blk [ofs [A B]]]. + assert (S1: safe w (ExprState f (C (Eassign (Eloc blk ofs (typeof b1)) b2 ty)) k e m)). + eapply safe_steps; eauto. constructor. + set (C2 := fun x => Eassign (Eloc blk ofs (typeof b1)) x ty). + exploit (simple_eval_r f k e m w b2 (fun x => C(C2 x))). auto. + eapply context_compose; eauto. repeat constructor. auto. + unfold C2; intros [v [E F]]. + assert (S2: safe w (ExprState f + (C (Eassign (Eloc blk ofs (typeof b1)) (Eval v (typeof b2)) ty)) k e + m)). + eapply safe_steps; eauto. constructor. + exploit not_imm_stuck_inv. eapply safe_not_imm_stuck. eexact S2. eauto. + simpl. intros [v' [m' [X [Y Z]]]]. + econstructor; split. + eapply step_assign with (C := C); eauto. + eapply star_plus_trans. eapply star_trans; eauto. + apply plus_one. left. apply step_rred. rewrite X. econstructor; eauto. + eapply safe_not_stuck; eauto. apply leftcontext_context; auto. + traceEq. +(* assignop *) + destruct P. + set (C1 := fun x => Eassignop op x b2 tyres ty). + exploit (simple_eval_l f k e m w b1 (fun x => C(C1 x))). auto. + eapply context_compose; eauto. repeat constructor. auto. + unfold C1; intros [blk [ofs [A B]]]. + assert (S1: safe w (ExprState f (C (Eassignop op (Eloc blk ofs (typeof b1)) b2 tyres ty)) k e m)). + eapply safe_steps; eauto. constructor. + set (C2 := fun x => Eassignop op (Eloc blk ofs (typeof b1)) x tyres ty). + exploit (simple_eval_r f k e m w b2 (fun x => C(C2 x))). auto. + eapply context_compose; eauto. repeat constructor. auto. + unfold C2; intros [v [E F]]. + assert (S2: safe w (ExprState f + (C + (Eassignop op (Eloc blk ofs (typeof b1)) (Eval v (typeof b2)) + tyres ty)) k e m)). + eapply safe_steps; eauto. constructor. + exploit not_imm_stuck_inv. eapply safe_not_imm_stuck. eexact S2. eauto. + simpl. intros [v1 [v2 [v3 [m' [U [V [W [X Y]]]]]]]]. + econstructor; split. + eapply step_assignop with (C := C); eauto. + eapply star_plus_trans. eapply star_trans; eauto. + apply plus_one. left. apply step_rred. rewrite U. econstructor; eauto. + eapply safe_not_stuck; eauto. apply leftcontext_context; auto. + traceEq. +(* postincr *) + set (C1 := fun x => Epostincr id x ty). + exploit (simple_eval_l f k e m w b (fun x => C(C1 x))). auto. + eapply context_compose; eauto. repeat constructor. auto. + unfold C1; intros [blk [ofs [A B]]]. + assert (S1: safe w (ExprState f (C (Epostincr id (Eloc blk ofs (typeof b)) ty)) k e m)). + eapply safe_steps; eauto. constructor. + exploit not_imm_stuck_inv. eapply safe_not_imm_stuck. eexact S1. eauto. + simpl. intros [v1 [v2 [v3 [m' [U [V [W [X Y]]]]]]]]. + econstructor; split. + eapply step_postincr with (C := C); eauto. + eapply star_plus_trans. eauto. + apply plus_one. left. apply step_rred. subst ty. econstructor; eauto. + eapply safe_not_stuck; eauto. apply leftcontext_context; auto. + traceEq. +(* comma *) + set (C1 := fun x => Ecomma x b2 ty). + exploit (simple_eval_r f k e m w b1 (fun x => C(C1 x))). auto. + eapply context_compose; eauto. repeat constructor. auto. + unfold C1; intros [v1 [A B]]. + assert (S1: safe w (ExprState f (C (Ecomma (Eval v1 (typeof b1)) b2 ty)) k e m)). + eapply safe_steps; eauto. constructor. + exploit not_imm_stuck_inv. eapply safe_not_imm_stuck. eexact S1. eauto. + simpl. intro X. + econstructor; split. + eapply step_comma with (C := C); eauto. + eapply star_plus_trans. eauto. + apply plus_one. left. apply step_rred. subst ty. econstructor; eauto. + eapply safe_not_stuck; eauto. apply leftcontext_context; auto. + traceEq. +(* call *) + destruct P. + set (C1 := fun x => Ecall x rargs ty). + exploit (simple_eval_r f k e m w b (fun x => C(C1 x))). auto. + eapply context_compose; eauto. repeat constructor. auto. + unfold C1; intros [vf [A B]]. + assert (S1: safe w (ExprState f (C (Ecall (Eval vf (typeof b)) rargs ty)) k e m)). + eapply safe_steps; eauto. constructor. + exploit (simple_eval_rlist f k e m w rargs (fun x => C(Ecall (Eval vf (typeof b)) x ty))). + auto. eapply contextlist'_intro with (rl0 := Enil). auto. auto. + intros [vl [E F]]. + assert (S2: safe w (ExprState f (C (Ecall (Eval vf (typeof b)) (rval_list vl rargs) ty)) + k e m)). + eapply safe_steps; eauto. constructor. + exploit not_imm_stuck_inv. eapply safe_not_imm_stuck. eexact S2. eauto. + simpl. intros X. + destruct X as [tyargs [tyres [fd [vl' [U [V [W X]]]]]]]. + apply rval_list_all_values. + econstructor; split. + eapply step_call with (C := C); eauto. eapply can_eval_simple_list; eauto. + eapply plus_right. eapply star_trans; eauto. + left. econstructor. rewrite U. econstructor; eauto. + eapply safe_not_stuck; eauto. apply leftcontext_context; auto. + traceEq. +(* rparen *) + set (C1 := fun x => Eparen x ty). + exploit (simple_eval_r f k e m w b (fun x => C(C1 x))). auto. + eapply context_compose; eauto. repeat constructor. auto. + unfold C1; intros [v [A B]]. + assert (S1: safe w (ExprState f (C (Eparen (Eval v (typeof b)) ty)) k e m)). + eapply safe_steps; eauto. constructor. + exploit not_imm_stuck_inv. eapply safe_not_imm_stuck. eexact S1. eauto. + simpl. intros EQ. subst ty. + econstructor; split. + eapply step_paren with (C := C); eauto. + eapply star_plus_trans. eauto. + apply plus_one. left. apply step_rred. econstructor; eauto. + eapply safe_not_stuck; eauto. apply leftcontext_context; auto. + traceEq. +Qed. + +(** The main simulation result. *) + +Theorem strategy_simulation: + forall w S, + safe w S -> + (exists r, final_state S r) + \/ (exists t, exists S', exists w', + step S t S' + /\ plus Csem.step ge S t S' + /\ possible_trace w t w'). +Proof. + intros. exploit safe_imm; eauto. intros IS; inv IS. +(* terminated *) + left; exists r; auto. + destruct H0. +(* expression step *) + inv H0. + (* lred *) + exploit can_estep; eauto. inv H4; auto. + intros [S [A B]]. right. exists E0; exists S; exists w. + split. left; auto. split. auto. constructor. + (* rred *) + exploit can_estep; eauto. inv H4; auto. inv H2; auto. + intros [S [A B]]. right. exists E0; exists S; exists w. + split. left; auto. split. auto. constructor. + (* callred *) + exploit can_estep; eauto. inv H4; auto. inv H2; auto. + intros [S [A B]]. right. exists E0; exists S; exists w. + split. left; auto. split. auto. constructor. +(* other step *) + right. exists t; exists s'; exists w'. + split. right. auto. + split. apply plus_one. right. auto. + auto. +Qed. + +End STRATEGY. + +(** * Whole-program behaviors *) + +Definition exec_program (p: program) (beh: program_behavior) : Prop := + program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. + +Definition safeprog (p: program) (w: world) : Prop := + (exists s, initial_state p s) + /\ (forall s, initial_state p s -> safe (Genv.globalenv p) w s). + +(** We now show the existence of a safe behavior for the strategy, + which is also an acceptable behavior for the nondeterministic semantics. *) + +Section BEHAVIOR. + +Variable prog: program. +Variable initial_world: world. + +(** We define a transition semantics that combines +- one strategy step; +- one or several nondeterministic steps; +- the state of the external world. +*) + +Local Open Scope pair_scope. + +Definition comb_state := (state * world)%type. + +Definition comb_step (ge: genv) (s: comb_state) (t: trace) (s': comb_state) : Prop := + (step ge s#1 t s'#1 /\ plus Csem.step ge s#1 t s'#1) + /\ possible_trace s#2 t s'#2. + +Definition comb_initial_state (s: comb_state) : Prop := + initial_state prog s#1 /\ s#2 = initial_world. + +Definition comb_final_state (s: comb_state) (r: int) : Prop := + final_state s#1 r. + +Definition comb_program_behaves (beh: program_behavior) : Prop := + program_behaves comb_step comb_initial_state comb_final_state (Genv.globalenv prog) beh. + +(** If the source program is safe, the combined semantics cannot go wrong. *) + +Remark proj_star_comb_step: + forall ge s t s', + star comb_step ge s t s' -> + star Csem.step ge s#1 t s'#1 /\ possible_trace s#2 t s'#2. +Proof. + induction 1. split; constructor. + destruct H as [[A B] C]. destruct IHstar. + split. eapply star_trans. apply plus_star; eauto. eauto. auto. + subst t. eapply possible_trace_app; eauto. +Qed. + +Lemma comb_behavior_not_wrong: + forall beh, + safeprog prog initial_world -> comb_program_behaves beh -> not_wrong beh. +Proof. + intros. destruct H. inv H0; simpl; auto. +(* Goes wrong after some steps *) + destruct H2. exploit proj_star_comb_step; eauto. intros [A B]. + assert (C: safe (Genv.globalenv prog) s'#2 s'#1). + eapply safe_steps. apply H1. eauto. eauto. congruence. + exploit strategy_simulation. eexact C. + intros [[r P] | [t' [s'' [w'' [P [Q R]]]]]]. + elim (H5 r). auto. + elim (H4 t' (s'', w'')). red. auto. +(* Goes initiall wrong *) + destruct H as [s A]. elim (H2 (s, initial_world)). red; auto. +Qed. + +(** Any non-wrong behavior of the combined semantics is a behavior + for the nondeterministic semantics. *) + +Lemma proj1_comb_behavior: + forall beh, + not_wrong beh -> + comb_program_behaves beh -> + Csem.exec_program prog beh. +Proof. + intros. red in H0. red. + eapply simulation_plus_preservation with + (match_states := fun (S1: comb_state) (S2: state) => S2 = S1#1); eauto. + intros. destruct H1. exists (st1#1); auto. + intros. red in H2. congruence. + intros. destruct H1 as [[A B] D]. subst st2. exists (st1'#1); auto. +Qed. + +(** Likewise, any non-wrong behavior of the combined semantics is a behavior + for the strategy. *) + +Lemma proj2_comb_behavior: + forall beh, + not_wrong beh -> + comb_program_behaves beh -> + exec_program prog beh. +Proof. + intros. red in H0. red. + eapply simulation_step_preservation with + (match_states := fun (S1: comb_state) (S2: state) => S2 = S1#1); eauto. + intros. destruct H1. exists (st1#1); auto. + intros. red in H2. congruence. + intros. destruct H1 as [[A B] D]. subst st2. exists (st1'#1); auto. +Qed. + +(** Finally, any behavior of the combined semantics is possible in the + initial world. *) + +Lemma possible_comb_behavior: + forall beh, + comb_program_behaves beh -> + possible_behavior initial_world beh. +Proof. + intros. + apply (project_behaviors_trace _ _ + (fun ge s t s' => step ge s t s' /\ plus Csem.step ge s t s') + (initial_state prog) + final_state + initial_world (Genv.globalenv prog)). + exact H. +Qed. + +(** It follows that a safe C program has a non-wrong behavior that + follows the strategy. *) + +Theorem strategy_behavior: + safeprog prog initial_world -> + exists beh, not_wrong beh + /\ Csem.exec_program prog beh + /\ exec_program prog beh + /\ possible_behavior initial_world beh. +Proof. + intros. + assert (exists beh, comb_program_behaves beh). + unfold comb_program_behaves. apply program_behaves_exists. + destruct H0 as [beh CPB]. + assert (not_wrong beh). eapply comb_behavior_not_wrong; eauto. + exists beh. split. auto. + split. apply proj1_comb_behavior; auto. + split. apply proj2_comb_behavior; auto. + apply possible_comb_behavior; auto. +Qed. + +End BEHAVIOR. + +(** * A big-step semantics implementing the reduction strategy. *) + +Section BIGSTEP. + +Variable ge: genv. + +(** The execution of a statement produces an ``outcome'', indicating + how the execution terminated: either normally or prematurely + through the execution of a [break], [continue] or [return] statement. *) + +Inductive outcome: Type := + | Out_break: outcome (**r terminated by [break] *) + | Out_continue: outcome (**r terminated by [continue] *) + | Out_normal: outcome (**r terminated normally *) + | Out_return: option (val * type) -> outcome. (**r terminated by [return] *) + +Inductive out_normal_or_continue : outcome -> Prop := + | Out_normal_or_continue_N: out_normal_or_continue Out_normal + | Out_normal_or_continue_C: out_normal_or_continue Out_continue. + +Inductive out_break_or_return : outcome -> outcome -> Prop := + | Out_break_or_return_B: out_break_or_return Out_break Out_normal + | Out_break_or_return_R: forall ov, + out_break_or_return (Out_return ov) (Out_return ov). + +Definition outcome_switch (out: outcome) : outcome := + match out with + | Out_break => Out_normal + | o => o + end. + +Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop := + match out, t with + | Out_normal, Tvoid => v = Vundef + | Out_return None, Tvoid => v = Vundef + | Out_return (Some (v', ty')), ty => ty <> Tvoid /\ cast v' ty' ty v + | _, _ => False + end. + +(** [eval_expression ge e m1 a t m2 a'] describes the evaluation of the + complex expression e. [v] is the resulting value, [m2] the final + memory state, and [t] the trace of input/output events performed + during this evaluation. *) + +Inductive eval_expression: env -> mem -> expr -> trace -> mem -> val -> Prop := + | eval_expression_intro: forall e m a t m' a' v, + eval_expr e m RV a t m' a' -> eval_simple_rvalue ge e m' a' v -> + eval_expression e m a t m' v + +with eval_expr: env -> mem -> kind -> expr -> trace -> mem -> expr -> Prop := + | eval_val: forall e m v ty, + eval_expr e m RV (Eval v ty) E0 m (Eval v ty) + | eval_var: forall e m x ty, + eval_expr e m LV (Evar x ty) E0 m (Evar x ty) + | eval_field: forall e m a t m' a' f ty, + eval_expr e m LV a t m' a' -> + eval_expr e m LV (Efield a f ty) t m' (Efield a' f ty) + | eval_valof: forall e m a t m' a' ty, + eval_expr e m LV a t m' a' -> + eval_expr e m RV (Evalof a ty) t m' (Evalof a' ty) + | eval_deref: forall e m a t m' a' ty, + eval_expr e m RV a t m' a' -> + eval_expr e m LV (Ederef a ty) t m' (Ederef a' ty) + | eval_addrof: forall e m a t m' a' ty, + eval_expr e m LV a t m' a' -> + eval_expr e m RV (Eaddrof a ty) t m' (Eaddrof a' ty) + | eval_unop: forall e m a t m' a' op ty, + eval_expr e m RV a t m' a' -> + eval_expr e m RV (Eunop op a ty) t m' (Eunop op a' ty) + | eval_binop: forall e m a1 t1 m' a1' a2 t2 m'' a2' op ty, + eval_expr e m RV a1 t1 m' a1' -> eval_expr e m' RV a2 t2 m'' a2' -> + eval_expr e m RV (Ebinop op a1 a2 ty) (t1 ** t2) m'' (Ebinop op a1' a2' ty) + | eval_cast: forall e m a t m' a' ty, + eval_expr e m RV a t m' a' -> + eval_expr e m RV (Ecast a ty) t m' (Ecast a' ty) + | eval_condition_true: forall e m a1 a2 a3 ty t1 m' a1' v1 t2 m'' a2' v, + eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> is_true v1 (typeof a1) -> + eval_expr e m' RV a2 t2 m'' a2' -> eval_simple_rvalue ge e m'' a2' v -> + ty = typeof a2 -> + eval_expr e m RV (Econdition a1 a2 a3 ty) (t1**t2) m'' (Eval v ty) + | eval_condition_false: forall e m a1 a2 a3 ty t1 m' a1' v1 t2 m'' a3' v, + eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> is_false v1 (typeof a1) -> + eval_expr e m' RV a3 t2 m'' a3' -> eval_simple_rvalue ge e m'' a3' v -> + ty = typeof a3 -> + eval_expr e m RV (Econdition a1 a2 a3 ty) (t1**t2) m'' (Eval v ty) + | eval_sizeof: forall e m ty' ty, + eval_expr e m RV (Esizeof ty' ty) E0 m (Esizeof ty' ty) + | eval_assign: forall e m l r ty t1 m1 l' t2 m2 r' b ofs v v' m3, + eval_expr e m LV l t1 m1 l' -> eval_expr e m1 RV r t2 m2 r' -> + eval_simple_lvalue ge e m2 l' b ofs -> + eval_simple_rvalue ge e m2 r' v -> + cast v (typeof r) (typeof l) v' -> + store_value_of_type (typeof l) m2 b ofs v' = Some m3 -> + ty = typeof l -> + eval_expr e m RV (Eassign l r ty) (t1**t2) m3 (Eval v' ty) + | eval_assignop: forall e m op l r tyres ty t1 m1 l' t2 m2 r' b ofs + v1 v2 v3 v4 m3, + eval_expr e m LV l t1 m1 l' -> eval_expr e m1 RV r t2 m2 r' -> + eval_simple_lvalue ge e m2 l' b ofs -> + load_value_of_type (typeof l) m2 b ofs = Some v1 -> + eval_simple_rvalue ge e m2 r' v2 -> + sem_binary_operation op v1 (typeof l) v2 (typeof r) m2 = Some v3 -> + cast v3 tyres (typeof l) v4 -> + store_value_of_type (typeof l) m2 b ofs v4 = Some m3 -> + ty = typeof l -> + eval_expr e m RV (Eassignop op l r tyres ty) (t1**t2) m3 (Eval v4 ty) + | eval_postincr: forall e m id l ty t m1 l' b ofs v1 v2 v3 m2, + eval_expr e m LV l t m1 l' -> + eval_simple_lvalue ge e m1 l' b ofs -> + load_value_of_type ty m1 b ofs = Some v1 -> + sem_incrdecr id v1 ty = Some v2 -> + cast v2 (typeconv ty) ty v3 -> + store_value_of_type ty m1 b ofs v3 = Some m2 -> + ty = typeof l -> + eval_expr e m RV (Epostincr id l ty) t m2 (Eval v1 ty) + | eval_comma: forall e m r1 r2 ty t1 m1 r1' v1 t2 m2 r2', + eval_expr e m RV r1 t1 m1 r1' -> + eval_simple_rvalue ge e m1 r1' v1 -> + eval_expr e m1 RV r2 t2 m2 r2' -> + ty = typeof r2 -> + eval_expr e m RV (Ecomma r1 r2 ty) (t1**t2) m2 r2' + | eval_call: forall e m rf rargs ty t1 m1 rf' t2 m2 rargs' vf vargs + targs tres fd t3 m3 vres, + eval_expr e m RV rf t1 m1 rf' -> eval_exprlist e m1 rargs t2 m2 rargs' -> + eval_simple_rvalue ge e m2 rf' vf -> + eval_simple_list ge e m2 rargs' targs vargs -> + typeof rf = Tfunction targs tres -> + Genv.find_funct ge vf = Some fd -> + type_of_fundef fd = Tfunction targs tres -> + eval_funcall m2 fd vargs t3 m3 vres -> + eval_expr e m RV (Ecall rf rargs ty) (t1**t2**t3) m3 (Eval vres ty) + +with eval_exprlist: env -> mem -> exprlist -> trace -> mem -> exprlist -> Prop := + | eval_nil: forall e m, + eval_exprlist e m Enil E0 m Enil + | eval_cons: forall e m a1 al t1 m1 a1' t2 m2 al', + eval_expr e m RV a1 t1 m1 a1' -> eval_exprlist e m1 al t2 m2 al' -> + eval_exprlist e m (Econs a1 al) (t1**t2) m2 (Econs a1' al') + +(** [exec_stmt ge e m1 s t m2 out] describes the execution of + the statement [s]. [out] is the outcome for this execution. + [m1] is the initial memory state, [m2] the final memory state. + [t] is the trace of input/output events performed during this + evaluation. *) + +with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := + | exec_Sskip: forall e m, + exec_stmt e m Sskip + E0 m Out_normal + | exec_Sdo: forall e m a t m' v, + eval_expression e m a t m' v -> + exec_stmt e m (Sdo a) + t m' Out_normal + | exec_Sseq_1: forall e m s1 s2 t1 m1 t2 m2 out, + exec_stmt e m s1 t1 m1 Out_normal -> + exec_stmt e m1 s2 t2 m2 out -> + exec_stmt e m (Ssequence s1 s2) + (t1 ** t2) m2 out + | exec_Sseq_2: forall e m s1 s2 t1 m1 out, + exec_stmt e m s1 t1 m1 out -> + out <> Out_normal -> + exec_stmt e m (Ssequence s1 s2) + t1 m1 out + | exec_Sifthenelse_true: forall e m a s1 s2 t1 m1 v1 t2 m2 out, + eval_expression e m a t1 m1 v1 -> + is_true v1 (typeof a) -> + exec_stmt e m1 s1 t2 m2 out -> + exec_stmt e m (Sifthenelse a s1 s2) + (t1**t2) m2 out + | exec_Sifthenelse_false: forall e m a s1 s2 t1 m1 v1 t2 m2 out, + eval_expression e m a t1 m1 v1 -> + is_false v1 (typeof a) -> + exec_stmt e m1 s2 t2 m2 out -> + exec_stmt e m (Sifthenelse a s1 s2) + (t1**t2) m2 out + | exec_Sreturn_none: forall e m, + exec_stmt e m (Sreturn None) + E0 m (Out_return None) + | exec_Sreturn_some: forall e m a t m' v, + eval_expression e m a t m' v -> + exec_stmt e m (Sreturn (Some a)) + t m' (Out_return (Some(v, typeof a))) + | exec_Sbreak: forall e m, + exec_stmt e m Sbreak + E0 m Out_break + | exec_Scontinue: forall e m, + exec_stmt e m Scontinue + E0 m Out_continue + | exec_Swhile_false: forall e m a s t m' v, + eval_expression e m a t m' v -> + is_false v (typeof a) -> + exec_stmt e m (Swhile a s) + t m' Out_normal + | exec_Swhile_stop: forall e m a s t1 m1 v t2 m2 out' out, + eval_expression e m a t1 m1 v -> + is_true v (typeof a) -> + exec_stmt e m1 s t2 m2 out' -> + out_break_or_return out' out -> + exec_stmt e m (Swhile a s) + (t1**t2) m2 out + | exec_Swhile_loop: forall e m a s t1 m1 v t2 m2 out1 t3 m3 out, + eval_expression e m a t1 m1 v -> + is_true v (typeof a) -> + exec_stmt e m1 s t2 m2 out1 -> + out_normal_or_continue out1 -> + exec_stmt e m2 (Swhile a s) t3 m3 out -> + exec_stmt e m (Swhile a s) + (t1 ** t2 ** t3) m3 out + | exec_Sdowhile_false: forall e m s a t1 m1 out1 t2 m2 v, + exec_stmt e m s t1 m1 out1 -> + out_normal_or_continue out1 -> + eval_expression e m1 a t2 m2 v -> + is_false v (typeof a) -> + exec_stmt e m (Sdowhile a s) + (t1 ** t2) m2 Out_normal + | exec_Sdowhile_stop: forall e m s a t m1 out1 out, + exec_stmt e m s t m1 out1 -> + out_break_or_return out1 out -> + exec_stmt e m (Sdowhile a s) + t m1 out + | exec_Sdowhile_loop: forall e m s a t1 m1 out1 t2 m2 v t3 m3 out, + exec_stmt e m s t1 m1 out1 -> + out_normal_or_continue out1 -> + eval_expression e m1 a t2 m2 v -> + is_true v (typeof a) -> + exec_stmt e m2 (Sdowhile a s) t3 m3 out -> + exec_stmt e m (Sdowhile a s) + (t1 ** t2 ** t3) m3 out + | exec_Sfor_start: forall e m s a1 a2 a3 out m1 m2 t1 t2, + exec_stmt e m a1 t1 m1 Out_normal -> + exec_stmt e m1 (Sfor Sskip a2 a3 s) t2 m2 out -> + exec_stmt e m (Sfor a1 a2 a3 s) + (t1 ** t2) m2 out + | exec_Sfor_false: forall e m s a2 a3 t m' v, + eval_expression e m a2 t m' v -> + is_false v (typeof a2) -> + exec_stmt e m (Sfor Sskip a2 a3 s) + t m' Out_normal + | exec_Sfor_stop: forall e m s a2 a3 t1 m1 v t2 m2 out1 out, + eval_expression e m a2 t1 m1 v -> + is_true v (typeof a2) -> + exec_stmt e m1 s t2 m2 out1 -> + out_break_or_return out1 out -> + exec_stmt e m (Sfor Sskip a2 a3 s) + (t1 ** t2) m2 out + | exec_Sfor_loop: forall e m s a2 a3 t1 m1 v t2 m2 out1 t3 m3 t4 m4 out, + eval_expression e m a2 t1 m1 v -> + is_true v (typeof a2) -> + exec_stmt e m1 s t2 m2 out1 -> + out_normal_or_continue out1 -> + exec_stmt e m2 a3 t3 m3 Out_normal -> + exec_stmt e m3 (Sfor Sskip a2 a3 s) t4 m4 out -> + exec_stmt e m (Sfor Sskip a2 a3 s) + (t1 ** t2 ** t3 ** t4) m4 out + | exec_Sswitch: forall e m a sl t1 m1 n t2 m2 out, + eval_expression e m a t1 m1 (Vint n) -> + exec_stmt e m1 (seq_of_labeled_statement (select_switch n sl)) t2 m2 out -> + exec_stmt e m (Sswitch a sl) + (t1 ** t2) m2 (outcome_switch out) + +(** [eval_funcall m1 fd args t m2 res] describes the invocation of + function [fd] with arguments [args]. [res] is the value returned + by the call. *) + +with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := + | eval_funcall_internal: forall m f vargs t e m1 m2 m3 out vres m4, + list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) -> + alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> + bind_parameters e m1 f.(fn_params) vargs m2 -> + exec_stmt e m2 f.(fn_body) t m3 out -> + outcome_result_value out f.(fn_return) vres -> + Mem.free_list m3 (blocks_of_env e) = Some m4 -> + eval_funcall m (Internal f) vargs t m4 vres + | eval_funcall_external: forall m ef targs tres vargs t vres m', + external_call ef ge vargs m t vres m' -> + eval_funcall m (External ef targs tres) vargs t m' vres. + +Scheme eval_expression_ind5 := Minimality for eval_expression Sort Prop + with eval_expr_ind5 := Minimality for eval_expr Sort Prop + with eval_exprlist_ind5 := Minimality for eval_exprlist Sort Prop + with exec_stmt_ind5 := Minimality for exec_stmt Sort Prop + with eval_funcall_ind5 := Minimality for eval_funcall Sort Prop. + +Combined Scheme bigstep_induction from + eval_expression_ind5, eval_expr_ind5, eval_exprlist_ind5, + exec_stmt_ind5, eval_funcall_ind5. + +(** [evalinf_expr ge e m1 K a T] denotes the fact that expression [a] + diverges in initial state [m1]. [T] is the trace of input/output + events performed during this evaluation. *) + +CoInductive evalinf_expr: env -> mem -> kind -> expr -> traceinf -> Prop := + | evalinf_field: forall e m a t f ty, + evalinf_expr e m LV a t -> + evalinf_expr e m LV (Efield a f ty) t + | evalinf_valof: forall e m a t ty, + evalinf_expr e m LV a t -> + evalinf_expr e m RV (Evalof a ty) t + | evalinf_deref: forall e m a t ty, + evalinf_expr e m RV a t -> + evalinf_expr e m LV (Ederef a ty) t + | evalinf_addrof: forall e m a t ty, + evalinf_expr e m LV a t -> + evalinf_expr e m RV (Eaddrof a ty) t + | evalinf_unop: forall e m a t op ty, + evalinf_expr e m RV a t -> + evalinf_expr e m RV (Eunop op a ty) t + | evalinf_binop_left: forall e m a1 t1 a2 op ty, + evalinf_expr e m RV a1 t1 -> + evalinf_expr e m RV (Ebinop op a1 a2 ty) t1 + | evalinf_binop_right: forall e m a1 t1 m' a1' a2 t2 op ty, + eval_expr e m RV a1 t1 m' a1' -> evalinf_expr e m' RV a2 t2 -> + evalinf_expr e m RV (Ebinop op a1 a2 ty) (t1 *** t2) + | evalinf_cast: forall e m a t ty, + evalinf_expr e m RV a t -> + evalinf_expr e m RV (Ecast a ty) t + | evalinf_condition: forall e m a1 a2 a3 ty t1, + evalinf_expr e m RV a1 t1 -> + evalinf_expr e m RV (Econdition a1 a2 a3 ty) t1 + | evalinf_condition_true: forall e m a1 a2 a3 ty t1 m' a1' v1 t2, + eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> is_true v1 (typeof a1) -> + evalinf_expr e m' RV a2 t2 -> + ty = typeof a2 -> + evalinf_expr e m RV (Econdition a1 a2 a3 ty) (t1***t2) + | evalinf_condition_false: forall e m a1 a2 a3 ty t1 m' a1' v1 t2, + eval_expr e m RV a1 t1 m' a1' -> eval_simple_rvalue ge e m' a1' v1 -> is_false v1 (typeof a1) -> + evalinf_expr e m' RV a3 t2 -> + ty = typeof a3 -> + evalinf_expr e m RV (Econdition a1 a2 a3 ty) (t1***t2) + | evalinf_assign_left: forall e m a1 t1 a2 ty, + evalinf_expr e m LV a1 t1 -> + evalinf_expr e m RV (Eassign a1 a2 ty) t1 + | evalinf_assign_right: forall e m a1 t1 m' a1' a2 t2 ty, + eval_expr e m LV a1 t1 m' a1' -> evalinf_expr e m' RV a2 t2 -> + evalinf_expr e m RV (Eassign a1 a2 ty) (t1 *** t2) + | evalinf_assignop_left: forall e m a1 t1 a2 op tyres ty, + evalinf_expr e m LV a1 t1 -> + evalinf_expr e m RV (Eassignop op a1 a2 tyres ty) t1 + | evalinf_assignop_right: forall e m a1 t1 m' a1' a2 t2 op tyres ty, + eval_expr e m LV a1 t1 m' a1' -> evalinf_expr e m' RV a2 t2 -> + evalinf_expr e m RV (Eassignop op a1 a2 tyres ty) (t1 *** t2) + | evalinf_postincr: forall e m a t id ty, + evalinf_expr e m LV a t -> + evalinf_expr e m RV (Epostincr id a ty) t + | evalinf_comma_left: forall e m a1 t1 a2 ty, + evalinf_expr e m RV a1 t1 -> + evalinf_expr e m RV (Ecomma a1 a2 ty) t1 + | evalinf_comma_right: forall e m a1 t1 m1 a1' v1 a2 t2 ty, + eval_expr e m RV a1 t1 m1 a1' -> eval_simple_rvalue ge e m1 a1' v1 -> + ty = typeof a2 -> + evalinf_expr e m1 RV a2 t2 -> + evalinf_expr e m RV (Ecomma a1 a2 ty) (t1 *** t2) + | evalinf_call_left: forall e m a1 t1 a2 ty, + evalinf_expr e m RV a1 t1 -> + evalinf_expr e m RV (Ecall a1 a2 ty) t1 + | evalinf_call_right: forall e m a1 t1 m1 a1' a2 t2 ty, + eval_expr e m RV a1 t1 m1 a1' -> + evalinf_exprlist e m1 a2 t2 -> + evalinf_expr e m RV (Ecall a1 a2 ty) (t1 *** t2) + | evalinf_call: forall e m rf rargs ty t1 m1 rf' t2 m2 rargs' vf vargs + targs tres fd t3, + eval_expr e m RV rf t1 m1 rf' -> eval_exprlist e m1 rargs t2 m2 rargs' -> + eval_simple_rvalue ge e m2 rf' vf -> + eval_simple_list ge e m2 rargs' targs vargs -> + typeof rf = Tfunction targs tres -> + Genv.find_funct ge vf = Some fd -> + type_of_fundef fd = Tfunction targs tres -> + evalinf_funcall m2 fd vargs t3 -> + evalinf_expr e m RV (Ecall rf rargs ty) (t1***t2***t3) + +with evalinf_exprlist: env -> mem -> exprlist -> traceinf -> Prop := + | evalinf_cons_left: forall e m a1 al t1, + evalinf_expr e m RV a1 t1 -> + evalinf_exprlist e m (Econs a1 al) t1 + | evalinf_cons_right: forall e m a1 al t1 m1 a1' t2, + eval_expr e m RV a1 t1 m1 a1' -> evalinf_exprlist e m1 al t2 -> + evalinf_exprlist e m (Econs a1 al) (t1***t2) + +(** [execinf_stmt ge e m1 s t] describes the diverging execution of + the statement [s]. *) + +with execinf_stmt: env -> mem -> statement -> traceinf -> Prop := + | execinf_Sdo: forall e m a t, + evalinf_expr e m RV a t -> + execinf_stmt e m (Sdo a) t + | execinf_Sseq_1: forall e m s1 s2 t1, + execinf_stmt e m s1 t1 -> + execinf_stmt e m (Ssequence s1 s2) t1 + | execinf_Sseq_2: forall e m s1 s2 t1 m1 t2, + exec_stmt e m s1 t1 m1 Out_normal -> + execinf_stmt e m1 s2 t2 -> + execinf_stmt e m (Ssequence s1 s2) (t1***t2) + | execinf_Sifthenelse_test: forall e m a s1 s2 t1, + evalinf_expr e m RV a t1 -> + execinf_stmt e m (Sifthenelse a s1 s2) t1 + | execinf_Sifthenelse_true: forall e m a s1 s2 t1 m1 v1 t2, + eval_expression e m a t1 m1 v1 -> + is_true v1 (typeof a) -> + execinf_stmt e m1 s1 t2 -> + execinf_stmt e m (Sifthenelse a s1 s2) (t1***t2) + | execinf_Sifthenelse_false: forall e m a s1 s2 t1 m1 v1 t2, + eval_expression e m a t1 m1 v1 -> + is_false v1 (typeof a) -> + execinf_stmt e m1 s2 t2 -> + execinf_stmt e m (Sifthenelse a s1 s2) (t1***t2) + | execinf_Sreturn_some: forall e m a t, + evalinf_expr e m RV a t -> + execinf_stmt e m (Sreturn (Some a)) t + | execinf_Swhile_test: forall e m a s t1, + evalinf_expr e m RV a t1 -> + execinf_stmt e m (Swhile a s) t1 + | execinf_Swhile_body: forall e m a s t1 m1 v t2, + eval_expression e m a t1 m1 v -> + is_true v (typeof a) -> + execinf_stmt e m1 s t2 -> + execinf_stmt e m (Swhile a s) (t1***t2) + | execinf_Swhile_loop: forall e m a s t1 m1 v t2 m2 out1 t3, + eval_expression e m a t1 m1 v -> + is_true v (typeof a) -> + exec_stmt e m1 s t2 m2 out1 -> + out_normal_or_continue out1 -> + execinf_stmt e m2 (Swhile a s) t3 -> + execinf_stmt e m (Swhile a s) (t1***t2***t3) + | execinf_Sdowhile_body: forall e m s a t1, + execinf_stmt e m s t1 -> + execinf_stmt e m (Sdowhile a s) t1 + | execinf_Sdowhile_test: forall e m s a t1 m1 out1 t2, + exec_stmt e m s t1 m1 out1 -> + out_normal_or_continue out1 -> + evalinf_expr e m1 RV a t2 -> + execinf_stmt e m (Sdowhile a s) (t1***t2) + | execinf_Sdowhile_loop: forall e m s a t1 m1 out1 t2 m2 v t3, + exec_stmt e m s t1 m1 out1 -> + out_normal_or_continue out1 -> + eval_expression e m1 a t2 m2 v -> + is_true v (typeof a) -> + execinf_stmt e m2 (Sdowhile a s) t3 -> + execinf_stmt e m (Sdowhile a s) (t1***t2***t3) + | execinf_Sfor_start_1: forall e m s a1 a2 a3 t1, + execinf_stmt e m a1 t1 -> + execinf_stmt e m (Sfor a1 a2 a3 s) t1 + | execinf_Sfor_start_2: forall e m s a1 a2 a3 m1 t1 t2, + exec_stmt e m a1 t1 m1 Out_normal -> a1 <> Sskip -> + execinf_stmt e m1 (Sfor Sskip a2 a3 s) t2 -> + execinf_stmt e m (Sfor a1 a2 a3 s) (t1***t2) + | execinf_Sfor_test: forall e m s a2 a3 t, + evalinf_expr e m RV a2 t -> + execinf_stmt e m (Sfor Sskip a2 a3 s) t + | execinf_Sfor_body: forall e m s a2 a3 t1 m1 v t2, + eval_expression e m a2 t1 m1 v -> + is_true v (typeof a2) -> + execinf_stmt e m1 s t2 -> + execinf_stmt e m (Sfor Sskip a2 a3 s) (t1***t2) + | execinf_Sfor_next: forall e m s a2 a3 t1 m1 v t2 m2 out1 t3, + eval_expression e m a2 t1 m1 v -> + is_true v (typeof a2) -> + exec_stmt e m1 s t2 m2 out1 -> + out_normal_or_continue out1 -> + execinf_stmt e m2 a3 t3 -> + execinf_stmt e m (Sfor Sskip a2 a3 s) (t1***t2***t3) + | execinf_Sfor_loop: forall e m s a2 a3 t1 m1 v t2 m2 out1 t3 m3 t4, + eval_expression e m a2 t1 m1 v -> + is_true v (typeof a2) -> + exec_stmt e m1 s t2 m2 out1 -> + out_normal_or_continue out1 -> + exec_stmt e m2 a3 t3 m3 Out_normal -> + execinf_stmt e m3 (Sfor Sskip a2 a3 s) t4 -> + execinf_stmt e m (Sfor Sskip a2 a3 s) (t1***t2***t3***t4) + | execinf_Sswitch_expr: forall e m a sl t1, + evalinf_expr e m RV a t1 -> + execinf_stmt e m (Sswitch a sl) t1 + | execinf_Sswitch_body: forall e m a sl t1 m1 n t2, + eval_expression e m a t1 m1 (Vint n) -> + execinf_stmt e m1 (seq_of_labeled_statement (select_switch n sl)) t2 -> + execinf_stmt e m (Sswitch a sl) (t1***t2) + +(** [evalinf_funcall m1 fd args t m2 res] describes a diverging + invocation of function [fd] with arguments [args]. *) + +with evalinf_funcall: mem -> fundef -> list val -> traceinf -> Prop := + | evalinf_funcall_internal: forall m f vargs t e m1 m2, + list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) -> + alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> + bind_parameters e m1 f.(fn_params) vargs m2 -> + execinf_stmt e m2 f.(fn_body) t -> + evalinf_funcall m (Internal f) vargs t. + +(** ** Implication from big-step semantics to transition semantics *) + +Inductive outcome_state_match + (e: env) (m: mem) (f: function) (k: cont): outcome -> state -> Prop := + | osm_normal: + outcome_state_match e m f k Out_normal (State f Sskip k e m) + | osm_break: + outcome_state_match e m f k Out_break (State f Sbreak k e m) + | osm_continue: + outcome_state_match e m f k Out_continue (State f Scontinue k e m) + | osm_return_none: forall k', + call_cont k' = call_cont k -> + outcome_state_match e m f k + (Out_return None) (State f (Sreturn None) k' e m) + | osm_return_some: forall v ty k', + call_cont k' = call_cont k -> + outcome_state_match e m f k + (Out_return (Some (v, ty))) (ExprState f (Eval v ty) (Kreturn k') e m). + +Lemma is_call_cont_call_cont: + forall k, is_call_cont k -> call_cont k = k. +Proof. + destruct k; simpl; intros; contradiction || auto. +Qed. + +Lemma leftcontext_compose: + forall k2 k3 C2, leftcontext k2 k3 C2 -> + forall k1 C1, leftcontext k1 k2 C1 -> + leftcontext k1 k3 (fun x => C2(C1 x)) +with leftcontextlist_compose: + forall k2 C2, leftcontextlist k2 C2 -> + forall k1 C1, leftcontext k1 k2 C1 -> + leftcontextlist k1 (fun x => C2(C1 x)). +Proof. + induction 1; intros; try (constructor; eauto). + replace (fun x => C1 x) with C1. auto. apply extensionality; auto. + induction 1; intros; constructor; eauto. +Qed. + +Lemma exprlist_app_leftcontext: + forall rl1 rl2, + simplelist rl1 -> leftcontextlist RV (fun x => exprlist_app rl1 (Econs x rl2)). +Proof. + induction rl1; simpl; intros. + apply lctx_list_head. constructor. + destruct H. apply lctx_list_tail. auto. auto. +Qed. + +Lemma exprlist_app_simple: + forall rl1 rl2, simplelist rl1 -> simplelist rl2 -> simplelist (exprlist_app rl1 rl2). +Proof. + induction rl1; simpl; intros. auto. destruct H; auto. +Qed. + +Lemma bigstep_to_steps: + (forall e m a t m' v, + eval_expression e m a t m' v -> + forall f k, + star step ge (ExprState f a k e m) t (ExprState f (Eval v (typeof a)) k e m')) +/\(forall e m K a t m' a', + eval_expr e m K a t m' a' -> + forall C f k, leftcontext K RV C -> + simple a' /\ typeof a' = typeof a /\ + star step ge (ExprState f (C a) k e m) t (ExprState f (C a') k e m')) +/\(forall e m al t m' al', + eval_exprlist e m al t m' al' -> + forall a1 al2 ty C f k, leftcontext RV RV C -> simple a1 -> simplelist al2 -> + simplelist al' /\ + star step ge (ExprState f (C (Ecall a1 (exprlist_app al2 al) ty)) k e m) + t (ExprState f (C (Ecall a1 (exprlist_app al2 al') ty)) k e m')) +/\(forall e m s t m' out, + exec_stmt e m s t m' out -> + forall f k, + match out with + | Out_return None => fn_return f = Tvoid + | Out_return (Some(v, ty)) => fn_return f <> Tvoid + | _ => True + end -> + exists S, + star step ge (State f s k e m) t S /\ outcome_state_match e m' f k out S) +/\(forall m fd args t m' res, + eval_funcall m fd args t m' res -> + forall k, + is_call_cont k -> + star step ge (Callstate fd args k m) t (Returnstate res k m')). +Proof. + apply bigstep_induction; intros. +(* expression, general *) + exploit (H0 (fun x => x) f k). constructor. intros [A [B C]]. + assert (match a' with Eval _ _ => False | _ => True end -> + star step ge (ExprState f a k e m) t (ExprState f (Eval v (typeof a)) k e m')). + intro. eapply star_right. eauto. left. eapply step_expr; eauto. traceEq. + destruct a'; auto. + simpl in B. rewrite B in C. inv H1. auto. + +(* val *) + simpl; intuition. apply star_refl. +(* var *) + simpl; intuition. apply star_refl. +(* field *) + exploit (H0 (fun x => C(Efield x f ty))). + eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. + simpl; intuition; eauto. +(* valof *) + exploit (H0 (fun x => C(Evalof x ty))). + eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. + simpl; intuition; eauto. +(* deref *) + exploit (H0 (fun x => C(Ederef x ty))). + eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. + simpl; intuition; eauto. +(* addrof *) + exploit (H0 (fun x => C(Eaddrof x ty))). + eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. + simpl; intuition; eauto. +(* unop *) + exploit (H0 (fun x => C(Eunop op x ty))). + eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. + simpl; intuition; eauto. +(* binop *) + exploit (H0 (fun x => C(Ebinop op x a2 ty))). + eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. + exploit (H2 (fun x => C(Ebinop op a1' x ty))). + eapply leftcontext_compose; eauto. repeat constructor. auto. intros [E [F G]]. + simpl; intuition. eapply star_trans; eauto. +(* cast *) + exploit (H0 (fun x => C(Ecast x ty))). + eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. + simpl; intuition; eauto. +(* condition *) + exploit (H0 (fun x => C(Econdition x a2 a3 ty))). + eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. + exploit (H4 (fun x => C(Eparen x ty))). + eapply leftcontext_compose; eauto. repeat constructor. intros [E [F G]]. + simpl; intuition. + eapply star_trans. eexact D. + eapply star_left. left; eapply step_condition_true; eauto. congruence. + eapply star_right. eexact G. left; eapply step_paren; eauto. congruence. + reflexivity. reflexivity. traceEq. +(* condition false *) + exploit (H0 (fun x => C(Econdition x a2 a3 ty))). + eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. + exploit (H4 (fun x => C(Eparen x ty))). + eapply leftcontext_compose; eauto. repeat constructor. intros [E [F G]]. + simpl; intuition. + eapply star_trans. eexact D. + eapply star_left. left; eapply step_condition_false; eauto. congruence. + eapply star_right. eexact G. left; eapply step_paren; eauto. congruence. + reflexivity. reflexivity. traceEq. +(* sizeof *) + simpl; intuition. apply star_refl. +(* assign *) + exploit (H0 (fun x => C(Eassign x r ty))). + eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. + exploit (H2 (fun x => C(Eassign l' x ty))). + eapply leftcontext_compose; eauto. repeat constructor. auto. intros [E [F G]]. + simpl; intuition. + eapply star_trans. eexact D. + eapply star_right. eexact G. + left. eapply step_assign; eauto. congruence. congruence. congruence. + reflexivity. traceEq. +(* assignop *) + exploit (H0 (fun x => C(Eassignop op x r tyres ty))). + eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. + exploit (H2 (fun x => C(Eassignop op l' x tyres ty))). + eapply leftcontext_compose; eauto. repeat constructor. auto. intros [E [F G]]. + simpl; intuition. + eapply star_trans. eexact D. + eapply star_right. eexact G. + left. eapply step_assignop; eauto. + rewrite B; eauto. rewrite B; rewrite F; eauto. congruence. congruence. congruence. + reflexivity. traceEq. +(* postincr *) + exploit (H0 (fun x => C(Epostincr id x ty))). + eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. + simpl; intuition. + eapply star_right. eexact D. + left. eapply step_postincr; eauto. congruence. + traceEq. +(* comma *) + exploit (H0 (fun x => C(Ecomma x r2 ty))). + eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. + exploit (H3 C). auto. intros [E [F G]]. + simpl; intuition. congruence. + eapply star_trans. eexact D. + eapply star_left. left; eapply step_comma; eauto. + eexact G. + reflexivity. traceEq. +(* call *) + exploit (H0 (fun x => C(Ecall x rargs ty))). + eapply leftcontext_compose; eauto. repeat constructor. intros [A [B D]]. + exploit (H2 rf' Enil ty C); eauto. red; auto. intros [E F]. + simpl; intuition. + eapply star_trans. eexact D. + eapply star_trans. eexact F. + eapply star_left. left; eapply step_call; eauto. congruence. + eapply star_right. eapply H9. red; auto. + right; constructor. + reflexivity. reflexivity. reflexivity. traceEq. +(* nil *) + simpl; intuition. apply star_refl. +(* cons *) + exploit (H0 (fun x => C(Ecall a0 (exprlist_app al2 (Econs x al)) ty))). + eapply leftcontext_compose; eauto. repeat constructor. auto. + apply exprlist_app_leftcontext; auto. intros [A [B D]]. + exploit (H2 a0 (exprlist_app al2 (Econs a1' Enil))); eauto. + apply exprlist_app_simple; auto. simpl. auto. + repeat rewrite exprlist_app_assoc. simpl. + intros [E F]. + + simpl; intuition. + eapply star_trans; eauto. + +(* skip *) + econstructor; split. apply star_refl. constructor. + +(* do *) + econstructor; split. + eapply star_left. right; constructor. + eapply star_right. apply H0. right; constructor. + reflexivity. traceEq. + constructor. + +(* sequence 2 *) + destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]]; auto. inv B1. + destruct (H2 f k) as [S2 [A2 B2]]; auto. + econstructor; split. + eapply star_left. right; econstructor. + eapply star_trans. eexact A1. + eapply star_left. right; constructor. eexact A2. + reflexivity. reflexivity. traceEq. + auto. + +(* sequence 1 *) + destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]]; auto. + set (S2 := + match out with + | Out_break => State f Sbreak k e m1 + | Out_continue => State f Scontinue k e m1 + | _ => S1 + end). + exists S2; split. + eapply star_left. right; econstructor. + eapply star_trans. eexact A1. + unfold S2; inv B1. + congruence. + apply star_one. right; apply step_break_seq. + apply star_one. right; apply step_continue_seq. + apply star_refl. + apply star_refl. + reflexivity. traceEq. + unfold S2; inv B1; congruence || econstructor; eauto. + +(* ifthenelse true *) + destruct (H3 f k) as [S1 [A1 B1]]; auto. + exists S1; split. + eapply star_left. right; apply step_ifthenelse. + eapply star_trans. eapply H0. + eapply star_left. right; eapply step_ifthenelse_true; eauto. + eexact A1. + reflexivity. reflexivity. traceEq. + auto. + +(* ifthenelse false *) + destruct (H3 f k) as [S1 [A1 B1]]; auto. + exists S1; split. + eapply star_left. right; apply step_ifthenelse. + eapply star_trans. eapply H0. + eapply star_left. right; eapply step_ifthenelse_false; eauto. + eexact A1. + reflexivity. reflexivity. traceEq. + auto. + +(* return none *) + econstructor; split. apply star_refl. constructor. auto. + +(* return some *) + econstructor; split. + eapply star_left. right; apply step_return_1. auto. + eapply H0. traceEq. + econstructor; eauto. + +(* break *) + econstructor; split. apply star_refl. constructor. + +(* continue *) + econstructor; split. apply star_refl. constructor. + +(* while false *) + econstructor; split. + eapply star_left. right; apply step_while. + eapply star_right. apply H0. right; eapply step_while_false; eauto. + reflexivity. traceEq. + constructor. + +(* while stop *) + destruct (H3 f (Kwhile2 a s k)) as [S1 [A1 B1]]. inv H4; auto. + set (S2 := + match out' with + | Out_break => State f Sskip k e m2 + | _ => S1 + end). + exists S2; split. + eapply star_left. right; apply step_while. + eapply star_trans. apply H0. + eapply star_left. right; eapply step_while_true; eauto. + eapply star_trans. eexact A1. + unfold S2. inversion H4; subst. + inv B1. apply star_one. right; constructor. + apply star_refl. + reflexivity. reflexivity. reflexivity. traceEq. + unfold S2. inversion H4; subst. constructor. inv B1; econstructor; eauto. + +(* while loop *) + destruct (H3 f (Kwhile2 a s k)) as [S1 [A1 B1]]. inv H4; auto. + destruct (H6 f k) as [S2 [A2 B2]]; auto. + exists S2; split. + eapply star_left. right; apply step_while. + eapply star_trans. apply H0. + eapply star_left. right; eapply step_while_true; eauto. + eapply star_trans. eexact A1. + eapply star_left. + inv H4; inv B1; right; apply step_skip_or_continue_while; auto. + eexact A2. + reflexivity. reflexivity. reflexivity. reflexivity. traceEq. + auto. + +(* dowhile false *) + destruct (H0 f (Kdowhile1 a s k)) as [S1 [A1 B1]]. inv H1; auto. + exists (State f Sskip k e m2); split. + eapply star_left. right; constructor. + eapply star_trans. eexact A1. + eapply star_left. + inv H1; inv B1; right; eapply step_skip_or_continue_dowhile; eauto. + eapply star_right. apply H3. + right; eapply step_dowhile_false; eauto. + reflexivity. reflexivity. reflexivity. traceEq. + constructor. + +(* dowhile stop *) + destruct (H0 f (Kdowhile1 a s k)) as [S1 [A1 B1]]. inv H1; auto. + set (S2 := + match out1 with + | Out_break => State f Sskip k e m1 + | _ => S1 + end). + exists S2; split. + eapply star_left. right; apply step_dowhile. + eapply star_trans. eexact A1. + unfold S2. inversion H1; subst. + inv B1. apply star_one. right; constructor. + apply star_refl. + reflexivity. traceEq. + unfold S2. inversion H1; subst. constructor. inv B1; econstructor; eauto. + +(* dowhile loop *) + destruct (H0 f (Kdowhile1 a s k)) as [S1 [A1 B1]]. inv H1; auto. + destruct (H6 f k) as [S2 [A2 B2]]; auto. + exists S2; split. + eapply star_left. right; constructor. + eapply star_trans. eexact A1. + eapply star_left. + inv H1; inv B1; right; eapply step_skip_or_continue_dowhile; eauto. + eapply star_trans. apply H3. + eapply star_left. right; eapply step_dowhile_true; eauto. + eexact A2. + reflexivity. reflexivity. reflexivity. reflexivity. traceEq. + auto. + +(* for start *) + assert (a1 = Sskip \/ a1 <> Sskip). destruct a1; auto; right; congruence. + destruct H4. + subst a1. inv H. apply H2; auto. + destruct (H0 f (Kseq (Sfor Sskip a2 a3 s) k)) as [S1 [A1 B1]]; auto. inv B1. + destruct (H2 f k) as [S2 [A2 B2]]; auto. + exists S2; split. + eapply star_left. right; apply step_for_start; auto. + eapply star_trans. eexact A1. + eapply star_left. right; constructor. eexact A2. + reflexivity. reflexivity. traceEq. + auto. + +(* for false *) + econstructor; split. + eapply star_left. right; apply step_for. + eapply star_right. apply H0. right; eapply step_for_false; eauto. + reflexivity. traceEq. + constructor. + +(* for stop *) + destruct (H3 f (Kfor3 a2 a3 s k)) as [S1 [A1 B1]]. inv H4; auto. + set (S2 := + match out1 with + | Out_break => State f Sskip k e m2 + | _ => S1 + end). + exists S2; split. + eapply star_left. right; apply step_for. + eapply star_trans. apply H0. + eapply star_left. right; eapply step_for_true; eauto. + eapply star_trans. eexact A1. + unfold S2. inversion H4; subst. + inv B1. apply star_one. right; constructor. + apply star_refl. + reflexivity. reflexivity. reflexivity. traceEq. + unfold S2. inversion H4; subst. constructor. inv B1; econstructor; eauto. + +(* for loop *) + destruct (H3 f (Kfor3 a2 a3 s k)) as [S1 [A1 B1]]. inv H4; auto. + destruct (H6 f (Kfor4 a2 a3 s k)) as [S2 [A2 B2]]; auto. inv B2. + destruct (H8 f k) as [S3 [A3 B3]]; auto. + exists S3; split. + eapply star_left. right; apply step_for. + eapply star_trans. apply H0. + eapply star_left. right; eapply step_for_true; eauto. + eapply star_trans. eexact A1. + eapply star_trans with (s2 := State f a3 (Kfor4 a2 a3 s k) e m2). + inv H4; inv B1. + apply star_one. right; constructor; auto. + apply star_one. right; constructor; auto. + eapply star_trans. eexact A2. + eapply star_left. right; constructor. + eexact A3. + reflexivity. reflexivity. reflexivity. reflexivity. + reflexivity. reflexivity. traceEq. + auto. + +(* switch *) + destruct (H2 f (Kswitch2 k)) as [S1 [A1 B1]]. destruct out; auto. + set (S2 := + match out with + | Out_normal => State f Sskip k e m2 + | Out_break => State f Sskip k e m2 + | Out_continue => State f Scontinue k e m2 + | _ => S1 + end). + exists S2; split. + eapply star_left. right; eapply step_switch. + eapply star_trans. apply H0. + eapply star_left. right; eapply step_expr_switch. + eapply star_trans. eexact A1. + unfold S2; inv B1. + apply star_one. right; constructor. auto. + apply star_one. right; constructor. auto. + apply star_one. right; constructor. + apply star_refl. + apply star_refl. + reflexivity. reflexivity. reflexivity. traceEq. + unfold S2. inv B1; simpl; econstructor; eauto. + +(* call internal *) + destruct (H3 f k) as [S1 [A1 B1]]. + red in H4. destruct out; auto. destruct o as [[v' ty'] | ]. + tauto. destruct (fn_return f); tauto. + eapply star_left. right; eapply step_internal_function; eauto. + eapply star_right. eexact A1. + inv B1; simpl in H4; try contradiction. + (* Out_normal *) + assert (fn_return f = Tvoid /\ vres = Vundef). + destruct (fn_return f); auto || contradiction. + destruct H7. subst vres. right; apply step_skip_call; auto. + (* Out_return None *) + assert (fn_return f = Tvoid /\ vres = Vundef). + destruct (fn_return f); auto || contradiction. + destruct H8. subst vres. + rewrite <- (is_call_cont_call_cont k H6). rewrite <- H7. + right; apply step_return_0; auto. + (* Out_return Some *) + destruct H4. + rewrite <- (is_call_cont_call_cont k H6). rewrite <- H7. + right; eapply step_return_2; eauto. + reflexivity. traceEq. + +(* call external *) + apply star_one. right; apply step_external_function; auto. +Qed. + +Lemma eval_expression_to_steps: + forall e m a t m' v, + eval_expression e m a t m' v -> + forall f k, + star step ge (ExprState f a k e m) t (ExprState f (Eval v (typeof a)) k e m'). +Proof (proj1 bigstep_to_steps). + +Lemma eval_expr_to_steps: + forall e m K a t m' a', + eval_expr e m K a t m' a' -> + forall C f k, leftcontext K RV C -> + simple a' /\ typeof a' = typeof a /\ + star step ge (ExprState f (C a) k e m) t (ExprState f (C a') k e m'). +Proof (proj1 (proj2 bigstep_to_steps)). + +Lemma eval_exprlist_to_steps: + forall e m al t m' al', + eval_exprlist e m al t m' al' -> + forall a1 al2 ty C f k, leftcontext RV RV C -> simple a1 -> simplelist al2 -> + simplelist al' /\ + star step ge (ExprState f (C (Ecall a1 (exprlist_app al2 al) ty)) k e m) + t (ExprState f (C (Ecall a1 (exprlist_app al2 al') ty)) k e m'). +Proof (proj1 (proj2 (proj2 bigstep_to_steps))). + +Lemma exec_stmt_to_steps: + forall e m s t m' out, + exec_stmt e m s t m' out -> + forall f k, + match out with + | Out_return None => fn_return f = Tvoid + | Out_return (Some(v, ty)) => fn_return f <> Tvoid + | _ => True + end -> + exists S, + star step ge (State f s k e m) t S /\ outcome_state_match e m' f k out S. +Proof (proj1 (proj2 (proj2 (proj2 bigstep_to_steps)))). + +Lemma eval_funcall_to_steps: + forall m fd args t m' res, + eval_funcall m fd args t m' res -> + forall k, + is_call_cont k -> + star step ge (Callstate fd args k m) t (Returnstate res k m'). +Proof (proj2 (proj2 (proj2 (proj2 bigstep_to_steps)))). + +Fixpoint esize (a: expr) : nat := + match a with + | Eloc _ _ _ => 1%nat + | Evar _ _ => 1%nat + | Ederef r1 _ => S(esize r1) + | Efield l1 _ _ => S(esize l1) + | Eval _ _ => O + | Evalof l1 _ => S(esize l1) + | Eaddrof l1 _ => S(esize l1) + | Eunop _ r1 _ => S(esize r1) + | Ebinop _ r1 r2 _ => S(esize r1 + esize r2)%nat + | Ecast r1 _ => S(esize r1) + | Econdition r1 _ _ _ => S(esize r1) + | Esizeof _ _ => 1%nat + | Eassign l1 r2 _ => S(esize l1 + esize r2)%nat + | Eassignop _ l1 r2 _ _ => S(esize l1 + esize r2)%nat + | Epostincr _ l1 _ => S(esize l1) + | Ecomma r1 r2 _ => S(esize r1 + esize r2)%nat + | Ecall r1 rl2 _ => S(esize r1 + esizelist rl2)%nat + | Eparen r1 _ => S(esize r1) + end + +with esizelist (el: exprlist) : nat := + match el with + | Enil => O + | Econs r1 rl2 => S(esize r1 + esizelist rl2)%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. + +Axiom ADMITTED: forall (P: Prop), P. + +Lemma evalinf_funcall_steps: + forall m fd args t k, + evalinf_funcall m fd args t -> + forever_N step lt ge O (Callstate fd args k m) t. +Proof. + cofix COF. + + assert (COS: + forall e m s t f k, + execinf_stmt e m s t -> + forever_N step lt ge O (State f s k e m) t). + cofix COS. + + assert (COE: + forall e m K a t C f k, + evalinf_expr e m K a t -> + leftcontext K RV C -> + forever_N step lt ge (esize a) (ExprState f (C a) k e m) t). + cofix COE. + + assert (COEL: + forall e m a t C f k a1 al ty, + evalinf_exprlist e m a t -> + leftcontext RV RV C -> simple a1 -> simplelist al -> + forever_N step lt ge (esizelist a) + (ExprState f (C (Ecall a1 (exprlist_app al a) ty)) k e m) t). + cofix COEL. + intros. inv H. +(* cons left *) + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply COE with (C := fun x => C(Ecall a1 (exprlist_app al (Econs x al0)) ty)). + eauto. eapply leftcontext_compose; eauto. constructor. auto. + apply exprlist_app_leftcontext; auto. traceEq. +(* cons right *) + destruct (eval_expr_to_steps _ _ _ _ _ _ _ H3 + (fun x => C(Ecall a1 (exprlist_app al (Econs x al0)) ty)) f k) + as [P [Q R]]. + eapply leftcontext_compose; eauto. repeat constructor. auto. + apply exprlist_app_leftcontext; auto. + eapply forever_N_star with (a2 := (esizelist al0)). + eexact R. simpl; omega. + change (Econs a1' al0) with (exprlist_app (Econs a1' Enil) al0). + rewrite <- exprlist_app_assoc. + eapply COEL. eauto. auto. auto. + apply exprlist_app_simple. auto. simpl; auto. traceEq. + + intros. inv H. +(* field *) + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply COE with (C := fun x => C(Efield x f0 ty)). eauto. + eapply leftcontext_compose; eauto. repeat constructor. traceEq. +(* valof *) + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply COE with (C := fun x => C(Evalof x ty)). eauto. + eapply leftcontext_compose; eauto. repeat constructor. traceEq. +(* deref *) + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply COE with (C := fun x => C(Ederef x ty)). eauto. + eapply leftcontext_compose; eauto. repeat constructor. traceEq. +(* addrof *) + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply COE with (C := fun x => C(Eaddrof x ty)). eauto. + eapply leftcontext_compose; eauto. repeat constructor. traceEq. +(* unop *) + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply COE with (C := fun x => C(Eunop op x ty)). eauto. + eapply leftcontext_compose; eauto. repeat constructor. traceEq. +(* binop left *) + eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. + eapply COE with (C := fun x => C(Ebinop op x a2 ty)). eauto. + eapply leftcontext_compose; eauto. repeat constructor. traceEq. +(* binop right *) + destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Ebinop op x a2 ty)) f k) + as [P [Q R]]. + eapply leftcontext_compose; eauto. repeat constructor. + eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; omega. + eapply COE with (C := fun x => C(Ebinop op a1' x ty)). eauto. + eapply leftcontext_compose; eauto. repeat constructor. auto. traceEq. +(* cast *) + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply COE with (C := fun x => C(Ecast x ty)). eauto. + eapply leftcontext_compose; eauto. repeat constructor. traceEq. +(* condition top *) + eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. + eapply COE with (C := fun x => C(Econdition x a2 a3 ty)). eauto. + eapply leftcontext_compose; eauto. repeat constructor. traceEq. +(* condition true *) + destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Econdition x a2 a3 (typeof a2))) f k) + as [P [Q R]]. + eapply leftcontext_compose; eauto. repeat constructor. + eapply forever_N_plus. eapply plus_right. eexact R. + left; eapply step_condition_true; eauto. congruence. + reflexivity. + eapply COE with (C := fun x => (C (Eparen x (typeof a2)))). eauto. + eapply leftcontext_compose; eauto. repeat constructor. traceEq. +(* condition false *) + destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Econdition x a2 a3 (typeof a3))) f k) + as [P [Q R]]. + eapply leftcontext_compose; eauto. repeat constructor. + eapply forever_N_plus. eapply plus_right. eexact R. + left; eapply step_condition_false; eauto. congruence. + reflexivity. + eapply COE with (C := fun x => (C (Eparen x (typeof a3)))). eauto. + eapply leftcontext_compose; eauto. repeat constructor. traceEq. +(* assign left *) + eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. + eapply COE with (C := fun x => C(Eassign x a2 ty)). eauto. + eapply leftcontext_compose; eauto. repeat constructor. traceEq. +(* assign right *) + destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Eassign x a2 ty)) f k) + as [P [Q R]]. + eapply leftcontext_compose; eauto. repeat constructor. + eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; omega. + eapply COE with (C := fun x => C(Eassign a1' x ty)). eauto. + eapply leftcontext_compose; eauto. repeat constructor. auto. traceEq. +(* assignop left *) + eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. + eapply COE with (C := fun x => C(Eassignop op x a2 tyres ty)). eauto. + eapply leftcontext_compose; eauto. repeat constructor. traceEq. +(* assignop right *) + destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Eassignop op x a2 tyres ty)) f k) + as [P [Q R]]. + eapply leftcontext_compose; eauto. repeat constructor. + eapply forever_N_star with (a2 := (esize a2)). eexact R. simpl; omega. + eapply COE with (C := fun x => C(Eassignop op a1' x tyres ty)). eauto. + eapply leftcontext_compose; eauto. repeat constructor. auto. traceEq. +(* postincr *) + eapply forever_N_star with (a2 := (esize a0)). apply star_refl. simpl; omega. + eapply COE with (C := fun x => C(Epostincr id x ty)). eauto. + eapply leftcontext_compose; eauto. repeat constructor. traceEq. +(* comma left *) + eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. + eapply COE with (C := fun x => C(Ecomma x a2 ty)). eauto. + eapply leftcontext_compose; eauto. repeat constructor. traceEq. +(* comma right *) + destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Ecomma x a2 (typeof a2))) f k) + as [P [Q R]]. + eapply leftcontext_compose; eauto. repeat constructor. + eapply forever_N_plus. eapply plus_right. eexact R. + left; eapply step_comma; eauto. reflexivity. + eapply COE with (C := C); eauto. traceEq. +(* call left *) + eapply forever_N_star with (a2 := (esize a1)). apply star_refl. simpl; omega. + eapply COE with (C := fun x => C(Ecall x a2 ty)). eauto. + eapply leftcontext_compose; eauto. repeat constructor. traceEq. +(* call right *) + destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Ecall x a2 ty)) f k) + as [P [Q R]]. + eapply leftcontext_compose; eauto. repeat constructor. + eapply forever_N_star with (a2 := (esizelist a2)). eexact R. simpl; omega. + eapply COEL with (al := Enil). eauto. auto. auto. red; auto. traceEq. +(* call *) + destruct (eval_expr_to_steps _ _ _ _ _ _ _ H1 (fun x => C(Ecall x rargs ty)) f k) + as [P [Q R]]. + eapply leftcontext_compose; eauto. repeat constructor. + destruct (eval_exprlist_to_steps _ _ _ _ _ _ H2 rf' Enil ty C f k) + as [S T]. auto. auto. simpl; auto. + eapply forever_N_plus. eapply plus_right. + eapply star_trans. eexact R. eexact T. reflexivity. + simpl. left; eapply step_call; eauto. congruence. reflexivity. + apply COF. eauto. traceEq. + +(* statements *) + intros. inv H. +(* do *) + eapply forever_N_plus. apply plus_one; right; constructor. + eapply COE with (C := fun x => x); eauto. constructor. traceEq. +(* seq 1 *) + eapply forever_N_plus. apply plus_one; right; constructor. + eapply COS; eauto. traceEq. +(* seq 2 *) + destruct (exec_stmt_to_steps _ _ _ _ _ _ H0 f (Kseq s2 k)) as [S1 [A1 B1]]; auto. inv B1. + eapply forever_N_plus. + eapply plus_left. right; constructor. + eapply star_right. eauto. right; constructor. + reflexivity. reflexivity. + eapply COS; eauto. traceEq. +(* if test *) + eapply forever_N_plus. apply plus_one; right; constructor. + eapply COE with (C := fun x => x); eauto. constructor. traceEq. +(* if true *) + eapply forever_N_plus. + eapply plus_left. right; constructor. + eapply star_right. eapply eval_expression_to_steps; eauto. + right. apply step_ifthenelse_true. auto. + reflexivity. reflexivity. + eapply COS; eauto. traceEq. +(* if false *) + eapply forever_N_plus. + eapply plus_left. right; constructor. + eapply star_right. eapply eval_expression_to_steps; eauto. + right. apply step_ifthenelse_false. auto. + reflexivity. reflexivity. + eapply COS; eauto. traceEq. +(* return some *) + eapply forever_N_plus. apply plus_one; right; constructor. apply ADMITTED. + eapply COE with (C := fun x => x); eauto. constructor. traceEq. +(* while test *) + eapply forever_N_plus. apply plus_one; right; constructor. + eapply COE with (C := fun x => x); eauto. constructor. traceEq. +(* while body *) + eapply forever_N_plus. + eapply plus_left. right; constructor. + eapply star_right. eapply eval_expression_to_steps; eauto. + right; apply step_while_true; auto. + reflexivity. reflexivity. + eapply COS; eauto. traceEq. +(* while loop *) + destruct (exec_stmt_to_steps _ _ _ _ _ _ H2 f (Kwhile2 a s0 k)) as [S1 [A1 B1]]; auto. inv H3; auto. + eapply forever_N_plus. + eapply plus_left. right; constructor. + eapply star_trans. eapply eval_expression_to_steps; eauto. + eapply star_left. right; apply step_while_true; auto. + eapply star_trans. eexact A1. + inv H3; inv B1; apply star_one; right; apply step_skip_or_continue_while; auto. + reflexivity. reflexivity. reflexivity. reflexivity. + eapply COS; eauto. traceEq. +(* dowhile body *) + eapply forever_N_plus. apply plus_one; right; constructor. + eapply COS; eauto. traceEq. +(* dowhile test *) + destruct (exec_stmt_to_steps _ _ _ _ _ _ H0 f (Kdowhile1 a s0 k)) as [S1 [A1 B1]]; auto. inv H1; auto. + eapply forever_N_plus. + eapply plus_left. right; constructor. + eapply star_trans. eexact A1. + eapply star_one. right. inv H1; inv B1; apply step_skip_or_continue_dowhile; auto. + reflexivity. reflexivity. + eapply COE with (C := fun x => x); eauto. constructor. traceEq. +(* dowhile loop *) + destruct (exec_stmt_to_steps _ _ _ _ _ _ H0 f (Kdowhile1 a s0 k)) as [S1 [A1 B1]]; auto. inv H1; auto. + eapply forever_N_plus. + eapply plus_left. right; constructor. + eapply star_trans. eexact A1. + eapply star_left. right. inv H1; inv B1; apply step_skip_or_continue_dowhile; auto. + eapply star_right. eapply eval_expression_to_steps; eauto. + right; apply step_dowhile_true; auto. + reflexivity. reflexivity. reflexivity. reflexivity. + eapply COS; eauto. traceEq. +(* for start 1 *) + assert (a1 <> Sskip). red; intros; subst a1; inv H0. + eapply forever_N_plus. apply plus_one. right. constructor. auto. + eapply COS; eauto. traceEq. +(* for start 2 *) + destruct (exec_stmt_to_steps _ _ _ _ _ _ H0 f (Kseq (Sfor Sskip a2 a3 s0) k)) as [S1 [A1 B1]]; auto. inv B1. + eapply forever_N_plus. + eapply plus_left. right; constructor. auto. + eapply star_trans. eexact A1. + apply star_one. right; constructor. + reflexivity. reflexivity. + eapply COS; eauto. traceEq. +(* for test *) + eapply forever_N_plus. apply plus_one; right; apply step_for. + eapply COE with (C := fun x => x); eauto. constructor. traceEq. +(* for body *) + eapply forever_N_plus. + eapply plus_left. right; apply step_for. + eapply star_right. eapply eval_expression_to_steps; eauto. + right; apply step_for_true; auto. + reflexivity. reflexivity. + eapply COS; eauto. traceEq. +(* for next *) + destruct (exec_stmt_to_steps _ _ _ _ _ _ H2 f (Kfor3 a2 a3 s0 k)) as [S1 [A1 B1]]; auto. inv H3; auto. + eapply forever_N_plus. + eapply plus_left. right; apply step_for. + eapply star_trans. eapply eval_expression_to_steps; eauto. + eapply star_left. right; apply step_for_true; auto. + eapply star_trans. eexact A1. + inv H3; inv B1; apply star_one; right; apply step_skip_or_continue_for3; auto. + reflexivity. reflexivity. reflexivity. reflexivity. + eapply COS; eauto. traceEq. +(* for loop *) + destruct (exec_stmt_to_steps _ _ _ _ _ _ H2 f (Kfor3 a2 a3 s0 k)) as [S1 [A1 B1]]; auto. inv H3; auto. + destruct (exec_stmt_to_steps _ _ _ _ _ _ H4 f (Kfor4 a2 a3 s0 k)) as [S2 [A2 B2]]; auto. inv B2. + eapply forever_N_plus. + eapply plus_left. right; apply step_for. + eapply star_trans. eapply eval_expression_to_steps; eauto. + eapply star_left. right; apply step_for_true; auto. + eapply star_trans. eexact A1. + eapply star_left. + inv H3; inv B1; right; apply step_skip_or_continue_for3; auto. + eapply star_right. eexact A2. + right; constructor. + reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. + eapply COS; eauto. traceEq. +(* switch expr *) + eapply forever_N_plus. apply plus_one; right; constructor. + eapply COE with (C := fun x => x); eauto. constructor. traceEq. +(* switch body *) + eapply forever_N_plus. + eapply plus_left. right; constructor. + eapply star_right. eapply eval_expression_to_steps; eauto. + right; constructor. + reflexivity. reflexivity. + eapply COS; eauto. traceEq. + +(* funcalls *) + intros. inv H. + eapply forever_N_plus. apply plus_one. right; econstructor; eauto. + eapply COS; eauto. traceEq. +Qed. + +End BIGSTEP. + +(** ** Whole-program behaviors, big-step style. *) + +Inductive bigstep_program_terminates (p: program): trace -> int -> Prop := + | bigstep_program_terminates_intro: forall b f m0 m1 t r, + let ge := Genv.globalenv p in + Genv.init_mem p = Some m0 -> + Genv.find_symbol ge p.(prog_main) = Some b -> + Genv.find_funct_ptr ge b = Some f -> + type_of_fundef f = Tfunction Tnil (Tint I32 Signed) -> + eval_funcall ge m0 f nil t m1 (Vint r) -> + bigstep_program_terminates p t r. + +Inductive bigstep_program_diverges (p: program): traceinf -> Prop := + | bigstep_program_diverges_intro: forall b f m0 t, + let ge := Genv.globalenv p in + Genv.init_mem p = Some m0 -> + Genv.find_symbol ge p.(prog_main) = Some b -> + Genv.find_funct_ptr ge b = Some f -> + type_of_fundef f = Tfunction Tnil (Tint I32 Signed) -> + evalinf_funcall ge m0 f nil t -> + bigstep_program_diverges p t. + +Theorem bigstep_program_terminates_exec: + forall prog t r, + bigstep_program_terminates prog t r -> exec_program prog (Terminates t r). +Proof. + intros. inv H. + econstructor. + econstructor; eauto. + apply eval_funcall_to_steps. eauto. red; auto. + econstructor. +Qed. + +Theorem bigstep_program_diverges_exec: + forall prog T, + bigstep_program_diverges prog T -> + exec_program prog (Reacts T) \/ + exists t, exec_program prog (Diverges t) /\ traceinf_prefix t T. +Proof. + intros. inv H. + set (st := Callstate f nil Kstop m0). + assert (forever step ge st T). + eapply forever_N_forever with (order := lt). + apply lt_wf. + eapply evalinf_funcall_steps; eauto. + destruct (forever_silent_or_reactive _ _ _ _ _ _ H) + as [A | [t [s' [T' [B [C D]]]]]]. + left. econstructor. econstructor; eauto. eauto. + right. exists t. split. + econstructor. econstructor; eauto. eauto. auto. + subst T. rewrite <- (E0_right t) at 1. apply traceinf_prefix_app. constructor. +Qed. + |