From a30d8e14ffdcfbae929cececa5c8fdc0cdddffd6 Mon Sep 17 00:00:00 2001
From: Gene Cooperman <gene@ccs.neu.edu>
Date: Wed, 29 May 2024 15:10:14 -0400
Subject: [PATCH] mcmini-gdb: fix "mcmini back"

---
 gdbinit_commands.py    |  6 ++----
 src/mcmini_private.cpp | 20 ++++++++++++++++++--
 2 files changed, 20 insertions(+), 6 deletions(-)

diff --git a/gdbinit_commands.py b/gdbinit_commands.py
index 3e11b597..8198a91c 100644
--- a/gdbinit_commands.py
+++ b/gdbinit_commands.py
@@ -253,12 +253,10 @@ def invoke(self, args, from_tty):
       print("GDB is in scheduler, not target process:" +
             "  Can't go to previous transition\n")
       return
-    iterationsForward = transitionId - 1
-    gdb.execute("mcmini finishTrace quiet")
     gdb.execute("set rerunCurrentTraceForDebugger = 1")
-    gdb.execute("mcmini nextTrace quiet")
+    iterationsForward = transitionId - 1
+    transitionId = 0
     gdb.execute("mcmini forward " + str(iterationsForward) + " quiet")
-    gdb.execute("set rerunCurrentTraceForDebugger = 0")
     print("DEBUGGING: " + "mcmini forward " + str(iterationsForward) + " quiet")
     print_user_frames_in_stack()
     print_mcmini_stats()
diff --git a/src/mcmini_private.cpp b/src/mcmini_private.cpp
index 3ff5e4ec..11215b94 100644
--- a/src/mcmini_private.cpp
+++ b/src/mcmini_private.cpp
@@ -291,9 +291,21 @@ mc_do_model_checking()
 {
   mc_prepare_to_model_check_new_program();
 
-  int nextBranchPoint = mc_explore_branch(FIRST_BRANCH);
-  while (nextBranchPoint != FIRST_BRANCH) { // while not backtracked to origin
+  int nextBranchPoint = FIRST_BRANCH;
+  while (true) { // while not backtracked to origin
+    if (rerunCurrentTraceForDebugger && traceId == 0) {
+      // FIXME:  Should we just keep current state,and re-initialize it?
+      mc_prepare_to_model_check_new_program();
+      nextBranchPoint = FIRST_BRANCH;
+      traceId--;
+    } else {
+      mcprintf("WARNING:  rerunCurrentTraceForDebugger set with 'tracedId > 0'."
+               "  Ignored.\n");
+    }
+    rerunCurrentTraceForDebugger = false;
+
     nextBranchPoint = mc_explore_branch(nextBranchPoint);
+    // IFXME:  Do we need this?  It seems that it just returns the same value.
     nextBranchPoint = programState->getDeepestDPORBranchPoint();
   }
 }
@@ -570,6 +582,10 @@ mc_search_dpor_branch_with_thread(const tid_t backtrackThread)
       mc_stop_model_checking(EXIT_FAILURE);
     }
 
+    if (rerunCurrentTraceForDebugger) {
+      break;  // Stop this trace.  We'll rerun to it later.
+    }
+
     depth++;
     transitionId++;