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".

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 "@[<hov 2>Time %d: observable event:@ @[<hov 2>%a@]@]@."
+    fprintf p "@[<hov 2>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 "@[<hov 2>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 "@[<hov 2>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 "@[<hov 2>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 "@[<hov 2>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)]