[stm] join: check no error states are part of the document

The error-resiliency feature may have managed to reach the end
of the document by recovering some error

1 files changed, 17 insertions, 0 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 61b8140ae6..5e453ecfe6 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2729,12 +2729,29 @@ let rec join_admitted_proofs id =
        join_admitted_proofs view.next
   | _ -> join_admitted_proofs view.next
 
+(* Error resiliency may have tolerated some broken commands *)
+let rec check_no_err_states ~doc visited id =
+  let open Stateid in
+  if Set.mem id visited then visited else
+  match state_of_id ~doc id with
+  | `Error e -> raise e
+  | _ ->
+     let view = VCS.visit id in
+     match view.step with
+     | `Qed(_,id) ->
+         let visited = check_no_err_states ~doc (Set.add id visited) id in
+         check_no_err_states ~doc visited view.next
+     | _ -> check_no_err_states ~doc (Set.add id visited) view.next
+
 let join ~doc =
   let doc = wait ~doc in
   stm_prerr_endline (fun () -> "Joining the environment");
   Global.join_safe_environment ();
   stm_prerr_endline (fun () -> "Joining Admitted proofs");
   join_admitted_proofs (VCS.get_branch_pos VCS.Branch.master);
+  stm_prerr_endline (fun () -> "Checking no error states");
+  ignore(check_no_err_states ~doc (Stateid.Set.singleton Stateid.initial)
+    (VCS.get_branch_pos VCS.Branch.master));
   VCS.print ();
   doc