From f2b1c25aa56a27836652aef3feeee0856c04235c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 8 Feb 2015 16:41:45 +0100 Subject: Interpreter produces more detailed trace, including name of semantic rules used. Cexec: record names of rules used in every reduction. Interp: print these rule names in -trace mode. Also: simplified the exploration in "-all" mode; give unique names to states. Csem: fix name of reduction rule "red_call". --- cfrontend/Cexec.v | 299 ++++++++++++++++++++++++++++++------------------------ 1 file changed, 164 insertions(+), 135 deletions(-) (limited to 'cfrontend/Cexec.v') diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 952d148d..ed67286f 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -12,6 +12,7 @@ (** Animating the CompCert C semantics *) +Require Import String. Require Import Axioms. Require Import Classical. Require Import Coqlib. @@ -31,6 +32,9 @@ Require Import Csyntax. Require Import Csem. Require Cstrategy. +Local Open Scope string_scope. +Local Open Scope list_scope. + (** Error monad with options or lists *) Notation "'do' X <- A ; B" := (match A with Some X => B | None => None end) @@ -661,9 +665,9 @@ Qed. (** * Reduction of expressions *) Inductive reduction: Type := - | Lred (l': expr) (m': mem) - | Rred (r': expr) (m': mem) (t: trace) - | Callred (fd: fundef) (args: list val) (tyres: type) (m': mem) + | Lred (rule: string) (l': expr) (m': mem) + | Rred (rule: string) (r': expr) (m': mem) (t: trace) + | Callred (rule: string) (fd: fundef) (args: list val) (tyres: type) (m': mem) | Stuckred. Section EXPRS. @@ -728,15 +732,15 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match e!x with | Some(b, ty') => check type_eq ty ty'; - topred (Lred (Eloc b Int.zero ty) m) + topred (Lred "red_var_local" (Eloc b Int.zero ty) m) | None => do b <- Genv.find_symbol ge x; - topred (Lred (Eloc b Int.zero ty) m) + topred (Lred "red_var_global" (Eloc b Int.zero ty) m) end | LV, Ederef r ty => match is_val r with | Some(Vptr b ofs, ty') => - topred (Lred (Eloc b ofs ty) m) + topred (Lred "red_deref" (Eloc b ofs ty) m) | Some _ => stuck | None => @@ -750,11 +754,11 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := do co <- ge.(genv_cenv)!id; match field_offset ge f (co_members co) with | Error _ => stuck - | OK delta => topred (Lred (Eloc b (Int.add ofs (Int.repr delta)) ty) m) + | OK delta => topred (Lred "red_field_struct" (Eloc b (Int.add ofs (Int.repr delta)) ty) m) end | Tunion id _ => do co <- ge.(genv_cenv)!id; - topred (Lred (Eloc b ofs ty) m) + topred (Lred "red_field_union" (Eloc b ofs ty) m) | _ => stuck end | Some _ => @@ -769,20 +773,20 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := | Some(b, ofs, ty') => check type_eq ty ty'; do w',t,v <- do_deref_loc w ty m b ofs; - topred (Rred (Eval v ty) m t) + topred (Rred "red_rvalof" (Eval v ty) m t) | None => incontext (fun x => Evalof x ty) (step_expr LV l m) end | RV, Eaddrof l ty => match is_loc l with - | Some(b, ofs, ty') => topred (Rred (Eval (Vptr b ofs) ty) m E0) + | Some(b, ofs, ty') => topred (Rred "red_addrof" (Eval (Vptr b ofs) ty) m E0) | None => incontext (fun x => Eaddrof x ty) (step_expr LV l m) end | RV, Eunop op r1 ty => match is_val r1 with | Some(v1, ty1) => do v <- sem_unary_operation op v1 ty1; - topred (Rred (Eval v ty) m E0) + topred (Rred "red_unop" (Eval v ty) m E0) | None => incontext (fun x => Eunop op x ty) (step_expr RV r1 m) end @@ -790,7 +794,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match is_val r1, is_val r2 with | Some(v1, ty1), Some(v2, ty2) => do v <- sem_binary_operation ge op v1 ty1 v2 ty2 m; - topred (Rred (Eval v ty) m E0) + topred (Rred "red_binop" (Eval v ty) m E0) | _, _ => incontext2 (fun x => Ebinop op x r2 ty) (step_expr RV r1 m) (fun x => Ebinop op r1 x ty) (step_expr RV r2 m) @@ -799,7 +803,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match is_val r1 with | Some(v1, ty1) => do v <- sem_cast v1 ty1 ty; - topred (Rred (Eval v ty) m E0) + topred (Rred "red_cast" (Eval v ty) m E0) | None => incontext (fun x => Ecast x ty) (step_expr RV r1 m) end @@ -807,8 +811,8 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match is_val r1 with | Some(v1, ty1) => do b <- bool_val v1 ty1; - if b then topred (Rred (Eparen r2 type_bool ty) m E0) - else topred (Rred (Eval (Vint Int.zero) ty) m E0) + if b then topred (Rred "red_seqand_true" (Eparen r2 type_bool ty) m E0) + else topred (Rred "red_seqand_false" (Eval (Vint Int.zero) ty) m E0) | None => incontext (fun x => Eseqand x r2 ty) (step_expr RV r1 m) end @@ -816,8 +820,8 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match is_val r1 with | Some(v1, ty1) => do b <- bool_val v1 ty1; - if b then topred (Rred (Eval (Vint Int.one) ty) m E0) - else topred (Rred (Eparen r2 type_bool ty) m E0) + if b then topred (Rred "red_seqor_true" (Eval (Vint Int.one) ty) m E0) + else topred (Rred "red_seqor_false" (Eparen r2 type_bool ty) m E0) | None => incontext (fun x => Eseqor x r2 ty) (step_expr RV r1 m) end @@ -825,21 +829,21 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match is_val r1 with | Some(v1, ty1) => do b <- bool_val v1 ty1; - topred (Rred (Eparen (if b then r2 else r3) ty ty) m E0) + topred (Rred "red_condition" (Eparen (if b then r2 else r3) ty ty) m E0) | None => incontext (fun x => Econdition x r2 r3 ty) (step_expr RV r1 m) end | RV, Esizeof ty' ty => - topred (Rred (Eval (Vint (Int.repr (sizeof ge ty'))) ty) m E0) + topred (Rred "red_sizeof" (Eval (Vint (Int.repr (sizeof ge ty'))) ty) m E0) | RV, Ealignof ty' ty => - topred (Rred (Eval (Vint (Int.repr (alignof ge ty'))) ty) m E0) + topred (Rred "red_alignof" (Eval (Vint (Int.repr (alignof ge ty'))) ty) m E0) | RV, Eassign l1 r2 ty => match is_loc l1, is_val r2 with | Some(b, ofs, ty1), Some(v2, ty2) => check type_eq ty1 ty; do v <- sem_cast v2 ty2 ty1; do w',t,m' <- do_assign_loc w ty1 m b ofs v; - topred (Rred (Eval v ty) m' t) + topred (Rred "red_assign" (Eval v ty) m' t) | _, _ => incontext2 (fun x => Eassign x r2 ty) (step_expr LV l1 m) (fun x => Eassign l1 x ty) (step_expr RV r2 m) @@ -851,7 +855,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := do w',t,v1 <- do_deref_loc w ty1 m b ofs; let r' := Eassign (Eloc b ofs ty1) (Ebinop op (Eval v1 ty1) (Eval v2 ty2) tyres) ty1 in - topred (Rred r' m t) + topred (Rred "red_assignop" r' m t) | _, _ => incontext2 (fun x => Eassignop op x r2 tyres ty) (step_expr LV l1 m) (fun x => Eassignop op l1 x tyres ty) (step_expr RV r2 m) @@ -867,7 +871,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := (Ebinop op (Eval v1 ty) (Eval (Vint Int.one) type_int32s) (incrdecr_type ty)) ty) (Eval v1 ty) ty in - topred (Rred r' m t) + topred (Rred "red_postincr" r' m t) | None => incontext (fun x => Epostincr id x ty) (step_expr LV l m) end @@ -875,7 +879,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match is_val r1 with | Some _ => check type_eq (typeof r2) ty; - topred (Rred r2 m E0) + topred (Rred "red_comma" r2 m E0) | None => incontext (fun x => Ecomma x r2 ty) (step_expr RV r1 m) end @@ -883,7 +887,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := match is_val r1 with | Some (v1, ty1) => do v <- sem_cast v1 ty1 tycast; - topred (Rred (Eval v ty) m E0) + topred (Rred "red_paren" (Eval v ty) m E0) | None => incontext (fun x => Eparen x tycast ty) (step_expr RV r1 m) end @@ -895,7 +899,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := do fd <- Genv.find_funct ge vf; do vargs <- sem_cast_arguments vtl tyargs; check type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv); - topred (Callred fd vargs ty m) + topred (Callred "red_call" fd vargs ty m) | _ => stuck end | _, _ => @@ -908,7 +912,7 @@ Fixpoint step_expr (k: kind) (a: expr) (m: mem): reducts expr := do vargs <- sem_cast_arguments vtl tyargs; match do_external ef w vargs m with | None => stuck - | Some(w',t,v,m') => topred (Rred (Eval v ty) m' t) + | Some(w',t,v,m') => topred (Rred "red_builtin" (Eval v ty) m' t) end | _ => incontext (fun x => Ebuiltin ef tyargs x ty) (step_exprlist rargs m) @@ -956,21 +960,6 @@ Proof. eapply imm_safe_callred; eauto. Qed. -(* -Definition not_stuck (a: expr) (m: mem) := - forall a' k C, context k RV C -> a = C a' -> imm_safe_t k a' m. - -Lemma safe_expr_kind: - forall k C a m, - context k RV C -> - not_stuck (C a) m -> - k = Cstrategy.expr_kind a. -Proof. - intros. - symmetry. eapply Cstrategy.imm_safe_kind. eapply imm_safe_t_imm_safe. eauto. -Qed. -*) - Fixpoint exprlist_all_values (rl: exprlist) : Prop := match rl with | Enil => True @@ -1163,9 +1152,9 @@ Hint Resolve context_compose contextlist_compose. Definition reduction_ok (k: kind) (a: expr) (m: mem) (rd: reduction) : Prop := match k, rd with - | LV, Lred l' m' => lred ge e a m l' m' - | RV, Rred r' m' t => rred ge a m t r' m' /\ exists w', possible_trace w t w' - | RV, Callred fd args tyres m' => callred ge a fd args tyres /\ m' = m + | LV, Lred _ l' m' => lred ge e a m l' m' + | RV, Rred _ r' m' t => rred ge a m t r' m' /\ exists w', possible_trace w t w' + | RV, Callred _ fd args tyres m' => callred ge a fd args tyres /\ m' = m | LV, Stuckred => ~imm_safe_t k a m | RV, Stuckred => ~imm_safe_t k a m | _, _ => False @@ -1521,7 +1510,7 @@ Proof with (try (apply not_invert_ok; simpl; intro; myinv; intuition congruence; destruct (Genv.find_funct ge vf) as [fd|] eqn:?... destruct (sem_cast_arguments vtl tyargs) as [vargs|] eqn:?... destruct (type_eq (type_of_fundef fd) (Tfunction tyargs tyres cconv))... - apply topred_ok; auto. red. split; auto. eapply red_Ecall; eauto. + apply topred_ok; auto. red. split; auto. eapply red_call; eauto. eapply sem_cast_arguments_sound; eauto. apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. congruence. apply not_invert_ok; simpl; intros; myinv. specialize (H ALLVAL). myinv. @@ -1583,73 +1572,77 @@ Qed. Lemma lred_topred: forall l1 m1 l2 m2, lred ge e l1 m1 l2 m2 -> - step_expr LV l1 m1 = topred (Lred l2 m2). + exists rule, step_expr LV l1 m1 = topred (Lred rule l2 m2). Proof. induction 1; simpl. (* var local *) - rewrite H. rewrite dec_eq_true; auto. + rewrite H. rewrite dec_eq_true. econstructor; eauto. (* var global *) - rewrite H; rewrite H0. auto. + rewrite H; rewrite H0. econstructor; eauto. (* deref *) - auto. + econstructor; eauto. (* field struct *) - rewrite H, H0; auto. + rewrite H, H0; econstructor; eauto. (* field union *) - rewrite H; auto. + rewrite H; econstructor; eauto. Qed. Lemma rred_topred: forall w' r1 m1 t r2 m2, rred ge r1 m1 t r2 m2 -> possible_trace w t w' -> - step_expr RV r1 m1 = topred (Rred r2 m2 t). + exists rule, step_expr RV r1 m1 = topred (Rred rule r2 m2 t). Proof. induction 1; simpl; intros. (* valof *) - rewrite dec_eq_true; auto. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H0). auto. + rewrite dec_eq_true. + rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H0). econstructor; eauto. (* addrof *) - inv H. auto. + inv H. econstructor; eauto. (* unop *) - inv H0. rewrite H; auto. + inv H0. rewrite H; econstructor; eauto. (* binop *) - inv H0. rewrite H; auto. + inv H0. rewrite H; econstructor; eauto. (* cast *) - inv H0. rewrite H; auto. + inv H0. rewrite H; econstructor; eauto. (* seqand *) - inv H0. rewrite H; auto. - inv H0. rewrite H; auto. + inv H0. rewrite H; econstructor; eauto. + inv H0. rewrite H; econstructor; eauto. (* seqor *) - inv H0. rewrite H; auto. - inv H0. rewrite H; auto. + inv H0. rewrite H; econstructor; eauto. + inv H0. rewrite H; econstructor; eauto. (* condition *) - inv H0. rewrite H; auto. + inv H0. rewrite H; econstructor; eauto. (* sizeof *) - inv H. auto. + inv H. econstructor; eauto. (* alignof *) - inv H. auto. + inv H. econstructor; eauto. (* assign *) - rewrite dec_eq_true; auto. rewrite H. rewrite (do_assign_loc_complete _ _ _ _ _ _ _ _ _ H0 H1). auto. + rewrite dec_eq_true. rewrite H. rewrite (do_assign_loc_complete _ _ _ _ _ _ _ _ _ H0 H1). + econstructor; eauto. (* assignop *) - rewrite dec_eq_true; auto. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H0). auto. + rewrite dec_eq_true. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H0). + econstructor; eauto. (* postincr *) - rewrite dec_eq_true; auto. subst. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H1). auto. + rewrite dec_eq_true. subst. rewrite (do_deref_loc_complete _ _ _ _ _ _ _ _ H H1). + econstructor; eauto. (* comma *) - inv H0. rewrite dec_eq_true; auto. + inv H0. rewrite dec_eq_true. econstructor; eauto. (* paren *) - inv H0. rewrite H; auto. + inv H0. rewrite H; econstructor; eauto. (* builtin *) exploit sem_cast_arguments_complete; eauto. intros [vtl [A B]]. exploit do_ef_external_complete; eauto. intros C. - rewrite A. rewrite B. rewrite C. auto. + rewrite A. rewrite B. rewrite C. econstructor; eauto. Qed. Lemma callred_topred: forall a fd args ty m, callred ge a fd args ty -> - step_expr RV a m = topred (Callred fd args ty m). + exists rule, step_expr RV a m = topred (Callred rule fd args ty m). Proof. induction 1; simpl. rewrite H2. exploit sem_cast_arguments_complete; eauto. intros [vtl [A B]]. - rewrite A; rewrite H; rewrite B; rewrite H1; rewrite dec_eq_true. auto. + rewrite A; rewrite H; rewrite B; rewrite H1; rewrite dec_eq_true. econstructor; eauto. Qed. Definition reducts_incl {A B: Type} (C: A -> B) (res1: reducts A) (res2: reducts B) : Prop := @@ -1956,44 +1949,54 @@ Proof. simpl. auto. Qed. +Inductive transition : Type := TR (rule: string) (t: trace) (S': state). + Definition expr_final_state (f: function) (k: cont) (e: env) (C_rd: (expr -> expr) * reduction) := match snd C_rd with - | Lred a m => (E0, ExprState f (fst C_rd a) k e m) - | Rred a m t => (t, ExprState f (fst C_rd a) k e m) - | Callred fd vargs ty m => (E0, Callstate fd vargs (Kcall f e (fst C_rd) ty k) m) - | Stuck => (E0, Stuckstate) + | Lred rule a m => TR rule E0 (ExprState f (fst C_rd a) k e m) + | Rred rule a m t => TR rule t (ExprState f (fst C_rd a) k e m) + | Callred rule fd vargs ty m => TR rule E0 (Callstate fd vargs (Kcall f e (fst C_rd) ty k) m) + | Stuckred => TR "step_stuck" E0 Stuckstate end. Local Open Scope list_monad_scope. -Definition ret (S: state) : list (trace * state) := (E0, S) :: nil. +Definition ret (rule: string) (S: state) : list transition := + TR rule E0 S :: nil. -Definition do_step (w: world) (s: state) : list (trace * state) := +Definition do_step (w: world) (s: state) : list transition := match s with | ExprState f a k e m => match is_val a with | Some(v, ty) => match k with - | Kdo k => ret (State f Sskip k e m ) + | Kdo k => ret "step_do_2" (State f Sskip k e m ) | Kifthenelse s1 s2 k => - do b <- bool_val v ty; ret (State f (if b then s1 else s2) k e m) + do b <- bool_val v ty; + ret "step_ifthenelse_2" (State f (if b then s1 else s2) k e m) | Kwhile1 x s k => do b <- bool_val v ty; - if b then ret (State f s (Kwhile2 x s k) e m) else ret (State f Sskip k e m) + if b + then ret "step_while_true" (State f s (Kwhile2 x s k) e m) + else ret "step_while_false" (State f Sskip k e m) | Kdowhile2 x s k => do b <- bool_val v ty; - if b then ret (State f (Sdowhile x s) k e m) else ret (State f Sskip k e m) + if b + then ret "step_dowhile_true" (State f (Sdowhile x s) k e m) + else ret "step_dowhile_false" (State f Sskip k e m) | Kfor2 a2 a3 s k => do b <- bool_val v ty; - if b then ret (State f s (Kfor3 a2 a3 s k) e m) else ret (State f Sskip k e m) + if b + then ret "step_for_true" (State f s (Kfor3 a2 a3 s k) e m) + else ret "step_for_false" (State f Sskip k e m) | Kreturn k => do v' <- sem_cast v ty f.(fn_return); do m' <- Mem.free_list m (blocks_of_env ge e); - ret (Returnstate v' (call_cont k) m') + ret "step_return_2" (Returnstate v' (call_cont k) m') | Kswitch1 sl k => do n <- sem_switch_arg v ty; - ret (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch2 k) e m) + ret "step_expr_switch" (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch2 k) e m) | _ => nil end @@ -2001,48 +2004,66 @@ Definition do_step (w: world) (s: state) : list (trace * state) := map (expr_final_state f k e) (step_expr e w RV a m) end - | State f (Sdo x) k e m => ret(ExprState f x (Kdo k) e m) - - | State f (Ssequence s1 s2) k e m => ret(State f s1 (Kseq s2 k) e m) - | State f Sskip (Kseq s k) e m => ret (State f s k e m) - | State f Scontinue (Kseq s k) e m => ret (State f Scontinue k e m) - | State f Sbreak (Kseq s k) e m => ret (State f Sbreak k e m) - - | State f (Sifthenelse a s1 s2) k e m => ret (ExprState f a (Kifthenelse s1 s2 k) e m) - - | State f (Swhile x s) k e m => ret (ExprState f x (Kwhile1 x s k) e m) - | State f (Sskip|Scontinue) (Kwhile2 x s k) e m => ret (State f (Swhile x s) k e m) - | State f Sbreak (Kwhile2 x s k) e m => ret (State f Sskip k e m) - - | State f (Sdowhile a s) k e m => ret (State f s (Kdowhile1 a s k) e m) - | State f (Sskip|Scontinue) (Kdowhile1 x s k) e m => ret (ExprState f x (Kdowhile2 x s k) e m) - | State f Sbreak (Kdowhile1 x s k) e m => ret (State f Sskip k e m) + | State f (Sdo x) k e m => + ret "step_do_1" (ExprState f x (Kdo k) e m) + | State f (Ssequence s1 s2) k e m => + ret "step_seq" (State f s1 (Kseq s2 k) e m) + | State f Sskip (Kseq s k) e m => + ret "step_skip_seq" (State f s k e m) + | State f Scontinue (Kseq s k) e m => + ret "step_continue_seq" (State f Scontinue k e m) + | State f Sbreak (Kseq s k) e m => + ret "step_break_seq" (State f Sbreak k e m) + + | State f (Sifthenelse a s1 s2) k e m => + ret "step_ifthenelse_1" (ExprState f a (Kifthenelse s1 s2 k) e m) + + | State f (Swhile x s) k e m => + ret "step_while" (ExprState f x (Kwhile1 x s k) e m) + | State f (Sskip|Scontinue) (Kwhile2 x s k) e m => + ret "step_skip_or_continue_while" (State f (Swhile x s) k e m) + | State f Sbreak (Kwhile2 x s k) e m => + ret "step_break_while" (State f Sskip k e m) + + | State f (Sdowhile a s) k e m => + ret "step_dowhile" (State f s (Kdowhile1 a s k) e m) + | State f (Sskip|Scontinue) (Kdowhile1 x s k) e m => + ret "step_skip_or_continue_dowhile" (ExprState f x (Kdowhile2 x s k) e m) + | State f Sbreak (Kdowhile1 x s k) e m => + ret "step_break_dowhile" (State f Sskip k e m) | State f (Sfor a1 a2 a3 s) k e m => if is_skip a1 - then ret (ExprState f a2 (Kfor2 a2 a3 s k) e m) - else ret (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m) - | State f Sskip (Kfor3 a2 a3 s k) e m => ret (State f a3 (Kfor4 a2 a3 s k) e m) - | State f Scontinue (Kfor3 a2 a3 s k) e m => ret (State f a3 (Kfor4 a2 a3 s k) e m) - | State f Sbreak (Kfor3 a2 a3 s k) e m => ret (State f Sskip k e m) - | State f Sskip (Kfor4 a2 a3 s k) e m => ret (State f (Sfor Sskip a2 a3 s) k e m) + then ret "step_for" (ExprState f a2 (Kfor2 a2 a3 s k) e m) + else ret "step_for_start" (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m) + | State f (Sskip|Scontinue) (Kfor3 a2 a3 s k) e m => + ret "step_skip_or_continue_for3" (State f a3 (Kfor4 a2 a3 s k) e m) + | State f Sbreak (Kfor3 a2 a3 s k) e m => + ret "step_break_for3" (State f Sskip k e m) + | State f Sskip (Kfor4 a2 a3 s k) e m => + ret "step_skip_for4" (State f (Sfor Sskip a2 a3 s) k e m) | State f (Sreturn None) k e m => do m' <- Mem.free_list m (blocks_of_env ge e); - ret (Returnstate Vundef (call_cont k) m') - | State f (Sreturn (Some x)) k e m => ret (ExprState f x (Kreturn k) e m) + ret "step_return_0" (Returnstate Vundef (call_cont k) m') + | State f (Sreturn (Some x)) k e m => + ret "step_return_1" (ExprState f x (Kreturn k) e m) | State f Sskip ((Kstop | Kcall _ _ _ _ _) as k) e m => do m' <- Mem.free_list m (blocks_of_env ge e); - ret (Returnstate Vundef k m') + ret "step_skip_call" (Returnstate Vundef k m') - | State f (Sswitch x sl) k e m => ret (ExprState f x (Kswitch1 sl k) e m) - | State f (Sskip|Sbreak) (Kswitch2 k) e m => ret (State f Sskip k e m) - | State f Scontinue (Kswitch2 k) e m => ret (State f Scontinue k e m) + | State f (Sswitch x sl) k e m => + ret "step_switch" (ExprState f x (Kswitch1 sl k) e m) + | State f (Sskip|Sbreak) (Kswitch2 k) e m => + ret "step_skip_break_switch" (State f Sskip k e m) + | State f Scontinue (Kswitch2 k) e m => + ret "step_continue_switch" (State f Scontinue k e m) - | State f (Slabel lbl s) k e m => ret (State f s k e m) + | State f (Slabel lbl s) k e m => + ret "step_label" (State f s k e m) | State f (Sgoto lbl) k e m => match find_label lbl f.(fn_body) (call_cont k) with - | Some(s', k') => ret (State f s' k' e m) + | Some(s', k') => ret "step_goto" (State f s' k' e m) | None => nil end @@ -2050,14 +2071,15 @@ Definition do_step (w: world) (s: state) : list (trace * state) := check (list_norepet_dec ident_eq (var_names (fn_params f) ++ var_names (fn_vars f))); let (e,m1) := do_alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) in do m2 <- sem_bind_parameters w e m1 f.(fn_params) vargs; - ret (State f f.(fn_body) k e m2) + ret "step_internal_function" (State f f.(fn_body) k e m2) | Callstate (External ef _ _ _) vargs k m => match do_external ef w vargs m with | None => nil - | Some(w',t,v,m') => (t, Returnstate v k m') :: nil + | Some(w',t,v,m') => TR "step_external_function" t (Returnstate v k m') :: nil end - | Returnstate v (Kcall f e C ty k) m => ret (ExprState f (C (Eval v ty)) k e m) + | Returnstate v (Kcall f e C ty k) m => + ret "step_returnstate" (ExprState f (C (Eval v ty)) k e m) | _ => nil end. @@ -2065,7 +2087,7 @@ Definition do_step (w: world) (s: state) : list (trace * state) := Ltac myinv := match goal with | [ |- In _ nil -> _ ] => intro X; elim X - | [ |- In _ (ret _) -> _ ] => + | [ |- In _ (ret _ _) -> _ ] => intro X; elim X; clear X; [intro EQ; unfold ret in EQ; inv EQ; myinv | myinv] | [ |- In _ (_ :: nil) -> _ ] => @@ -2079,8 +2101,8 @@ Ltac myinv := Hint Extern 3 => exact I. Theorem do_step_sound: - forall w S t S', - In (t, S') (do_step w S) -> + forall w S rule t S', + In (TR rule t S') (do_step w S) -> Csem.step ge S t S' \/ (t = E0 /\ S' = Stuckstate /\ can_crash_world w S). Proof with try (left; right; econstructor; eauto; fail). intros until S'. destruct S; simpl. @@ -2145,45 +2167,52 @@ Proof. Qed. Theorem do_step_complete: - forall w S t S' w', possible_trace w t w' -> Csem.step ge S t S' -> In (t, S') (do_step w S). -Proof with (unfold ret; auto with coqlib). + forall w S t S' w', + possible_trace w t w' -> Csem.step ge S t S' -> exists rule, In (TR rule t S') (do_step w S). +Proof with (unfold ret; eauto with coqlib). intros until w'; intros PT H. destruct H. (* Expression step *) inversion H; subst; exploit estep_not_val; eauto; intro NOTVAL. (* lred *) unfold do_step; rewrite NOTVAL. - change (E0, ExprState f (C a') k e m') with (expr_final_state f k e (C, Lred a' m')). + exploit lred_topred; eauto. instantiate (1 := w). intros (rule & STEP). + exists rule. change (TR rule E0 (ExprState f (C a') k e m')) with (expr_final_state f k e (C, Lred rule a' m')). apply in_map. generalize (step_expr_context e w _ _ _ H1 a m). unfold reducts_incl. - intro. replace C with (fun x => C x). apply H2. - rewrite (lred_topred _ _ _ _ _ _ H0). unfold topred; auto with coqlib. + intro. replace C with (fun x => C x). apply H2. + rewrite STEP. unfold topred; auto with coqlib. apply extensionality; auto. (* rred *) unfold do_step; rewrite NOTVAL. - change (t, ExprState f (C a') k e m') with (expr_final_state f k e (C, Rred a' m' t)). + exploit rred_topred; eauto. instantiate (1 := e). intros (rule & STEP). + exists rule. + change (TR rule t (ExprState f (C a') k e m')) with (expr_final_state f k e (C, Rred rule a' m' t)). apply in_map. generalize (step_expr_context e w _ _ _ H1 a m). unfold reducts_incl. - intro. replace C with (fun x => C x). apply H2. - rewrite (rred_topred _ _ _ _ _ _ _ _ H0 PT). unfold topred; auto with coqlib. + intro. replace C with (fun x => C x). apply H2. + rewrite STEP; unfold topred; auto with coqlib. apply extensionality; auto. (* callred *) unfold do_step; rewrite NOTVAL. - change (E0, Callstate fd vargs (Kcall f e C ty k) m) with (expr_final_state f k e (C, Callred fd vargs ty m)). + exploit callred_topred; eauto. instantiate (1 := m). instantiate (1 := w). instantiate (1 := e). + intros (rule & STEP). exists rule. + change (TR rule E0 (Callstate fd vargs (Kcall f e C ty k) m)) with (expr_final_state f k e (C, Callred rule fd vargs ty m)). apply in_map. generalize (step_expr_context e w _ _ _ H1 a m). unfold reducts_incl. intro. replace C with (fun x => C x). apply H2. - rewrite (callred_topred _ _ _ _ _ _ _ H0). unfold topred; auto with coqlib. + rewrite STEP; unfold topred; auto with coqlib. apply extensionality; auto. (* stuck *) exploit not_imm_safe_stuck_red. eauto. red; intros; elim H1. eapply imm_safe_t_imm_safe. eauto. instantiate (1 := w). intros [C' IN]. - simpl do_step. rewrite NOTVAL. - change (E0, Stuckstate) with (expr_final_state f k e (C', Stuckred)). + simpl do_step. rewrite NOTVAL. + exists "step_stuck". + change (TR "step_stuck" E0 Stuckstate) with (expr_final_state f k e (C', Stuckred)). apply in_map. auto. (* Statement step *) - inv H; simpl... + inv H; simpl; econstructor... rewrite H0... rewrite H0... rewrite H0... -- cgit