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 ++++++++++++++++++++++++++++++------------------------ cfrontend/Csem.v | 2 +- driver/Interp.ml | 156 +++++++++++----------------- 3 files changed, 226 insertions(+), 231 deletions(-) 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... diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index e6e3a321..fafbf29f 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -317,7 +317,7 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := (More exactly, identification of function calls that can reduce.) *) Inductive callred: expr -> fundef -> list val -> type -> Prop := - | red_Ecall: forall vf tyf tyargs tyres cconv el ty fd vargs, + | red_call: forall vf tyf tyargs tyres cconv el ty fd vargs, Genv.find_funct ge vf = Some fd -> cast_arguments el tyargs vargs -> type_of_fundef fd = Tfunction tyargs tyres cconv -> diff --git a/driver/Interp.ml b/driver/Interp.ml index ab22cebb..2725dbfe 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -254,28 +254,14 @@ let compare_state s1 s2 = compare (rank_state s1) (rank_state s2) end -(* Sets of states already explored *) +(* Maps of states already explored. *) -module StateSet = - Set.Make(struct - type t = state * Determinism.world - let compare (s1,w1) (s2,w2) = compare_state s1 s2 +module StateMap = + Map.Make(struct + type t = state + let compare = compare_state end) -(* Purging states that will never be reached again based on their memory - next block. All states with nextblock <= the given nextblock are - removed. We take advantage of the fact that StateSets are sorted - by increasing nextblock, cf. the definition of compare_state above. *) - -let rec purge_seen nextblock seen = - let min = try Some(StateSet.min_elt seen) with Not_found -> None in - match min with - | None -> seen - | Some((s, w) as sw) -> - if P.le (mem_state s).Mem.nextblock nextblock - then purge_seen nextblock (StateSet.remove sw seen) - else seen - (* Extract a string from a global pointer *) let extract_string m blk ofs = @@ -435,7 +421,7 @@ and world_vstore ge m chunk id ofs ev = let do_event p ge time w ev = if !trace >= 1 then - fprintf p "@[Time %d: observable event:@ @[%a@]@]@." + fprintf p "@[Time %d: observable event:@ %a@]@." time print_event ev; (* Return new world after external action *) match ev with @@ -497,11 +483,10 @@ let diagnose_stuck_state p ge w = function | ExprState(f,a,k,e,m) -> ignore(diagnose_stuck_expr p ge w f a k e m) | _ -> () -(* Exploration *) +(* Execution of a single step. Return list of triples + (reduction rule, next state, next world). *) -let do_step p prog ge time (s, w) = - if !trace >= 2 then - fprintf p "@[Time %d: %a@]@." time print_state (prog, ge, s); +let do_step p prog ge time s w = match Cexec.at_final_state s with | Some r -> if !trace >= 1 then @@ -513,89 +498,71 @@ let do_step p prog ge time (s, w) = end | None -> let l = Cexec.do_step ge do_external_function do_inline_assembly w s in - if l = [] || List.exists (fun (t,s) -> s = Stuckstate) l then begin + if l = [] + || List.exists (fun (Cexec.TR(r,t,s)) -> s = Stuckstate) l + then begin pp_set_max_boxes p 1000; fprintf p "@[Stuck state: %a@]@." print_state (prog, ge, s); diagnose_stuck_state p ge w s; fprintf p "ERROR: Undefined behavior@."; exit 126 end else begin - List.map (fun (t, s') -> (s', do_events p ge time w t)) l + List.map (fun (Cexec.TR(r, t, s')) -> (r, s', do_events p ge time w t)) l end -let rec explore_one p prog ge time sw = - let succs = do_step p prog ge time sw in +(* Exploration of a single execution. *) + +let rec explore_one p prog ge time s w = + if !trace >= 2 then + fprintf p "@[Time %d:@ %a@]@." time print_state (prog, ge, s); + let succs = do_step p prog ge time s w in if succs <> [] then begin - let sw' = + let (r, s', w') = match !mode with | First -> List.hd succs | Random -> List.nth succs (Random.int (List.length succs)) | All -> assert false in - explore_one p prog ge (time + 1) sw' + if !trace >= 2 then + fprintf p "--[%s]-->@." (camlstring_of_coqstring r); + explore_one p prog ge (time + 1) s' w' end -(* A priority queue structure where the priority is inversely proportional - to the memory nextblock. *) - -module PrioQueue = struct - - type elt = int * StateSet.elt - - type queue = Empty | Node of elt * queue * queue - - let empty = Empty - - let singleton elt = Node(elt, Empty, Empty) - - let higher_prio (time1, (s1, w1)) (time2, (s2, w2)) = - P.lt (mem_state s1).Mem.nextblock (mem_state s2).Mem.nextblock - - let rec insert queue elt = - match queue with - | Empty -> Node(elt, Empty, Empty) - | Node(e, left, right) -> - if higher_prio elt e - then Node(elt, insert right e, left) - else Node(e, insert right elt, left) - - let rec remove_top = function - | Empty -> assert false - | Node(elt, left, Empty) -> left - | Node(elt, Empty, right) -> right - | Node(elt, (Node(lelt, _, _) as left), - (Node(relt, _, _) as right)) -> - if higher_prio lelt relt - then Node(lelt, remove_top left, right) - else Node(relt, left, remove_top right) - - let extract = function - | Empty -> None - | Node(elt, _, _) as queue -> Some(elt, remove_top queue) - - (* Return true if all elements of queue have strictly lower priority - than elt. *) - let dominate elt queue = - match queue with - | Empty -> true - | Node(e, _, _) -> higher_prio elt e -end - -let rec explore_all p prog ge seen queue = - match PrioQueue.extract queue with - | None -> () - | Some((time, sw) as tsw, queue') -> - if StateSet.mem sw seen then - explore_all p prog ge seen queue' - else - let succs = - List.rev_map (fun sw -> (time + 1, sw)) (do_step p prog ge time sw) in - let queue'' = List.fold_left PrioQueue.insert queue' succs in - let seen' = StateSet.add sw seen in - let seen'' = - if PrioQueue.dominate tsw queue'' - then purge_seen (mem_state (fst sw)).Mem.nextblock seen' - else seen' in - explore_all p prog ge seen'' queue'' +(* Exploration of all possible executions. *) + +let rec explore_all p prog ge time states = + if !trace >= 2 then begin + List.iter + (fun (n, s, w) -> + fprintf p "@[State %d.%d: @ %a@]@." + time n print_state (prog, ge, s)) + states + end; + let rec explore_next nextstates seen numseen = function + | [] -> + List.rev nextstates + | (n, s, w) :: states -> + add_reducts nextstates seen numseen states n (do_step p prog ge time s w) + + and add_reducts nextstates seen numseen states n = function + | [] -> + explore_next nextstates seen numseen states + | (r, s', w') :: reducts -> + let (n', nextstates', seen', numseen') = + try + (StateMap.find s' seen, nextstates, seen, numseen) + with Not_found -> + (numseen, + (numseen, s', w') :: nextstates, + StateMap.add s' numseen seen, + numseen + 1) in + if !trace >= 2 then begin + fprintf p "Transition state %d.%d --[%s]--> state %d.%d@." + time n (camlstring_of_coqstring r) (time + 1) n' + end; + add_reducts nextstates' seen' numseen' states n reducts + in + let nextstates = explore_next [] StateMap.empty 1 states in + if nextstates <> [] then explore_all p prog ge (time + 1) nextstates (* The variant of the source program used to build the world for executing events. @@ -680,7 +647,6 @@ let execute prog = | Some(ge, s) -> match !mode with | First | Random -> - explore_one p prog1 ge 0 (s, world wge wm) + explore_one p prog1 ge 0 s (world wge wm) | All -> - explore_all p prog1 ge StateSet.empty - (PrioQueue.singleton (0, (s, world wge wm))) + explore_all p prog1 ge 0 [(1, s, world wge wm)] -- cgit