Instantiate FastTool *before* DebugTool to prevent NullPointerExceptions

when DebugTool tries to access FastTool during its own instantiation. Follow up of Github PR #1062 #1062 [Bug][TLC] Signed-off-by: Markus Alexander Kuppe <[email protected]>
tlaplus · Dec 6, 2024 · e0bd541 · e0bd541
1 parent 3bf6f25
commit e0bd541
Show file tree

Hide file tree

Showing 5 changed files with 32 additions and 185 deletions.
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/TLC.java b/tlatools/org.lamport.tlatools/src/tlc2/TLC.java
@@ -32,16 +32,15 @@
 import tlc2.output.MP;
 import tlc2.output.Messages;
 import tlc2.tool.DFIDModelChecker;
-import tlc2.tool.ITool;
 import tlc2.tool.ModelChecker;
 import tlc2.tool.Simulator;
-import tlc2.tool.SingleThreadedSimulator;
 import tlc2.tool.fp.FPSet;
 import tlc2.tool.fp.FPSetConfiguration;
 import tlc2.tool.fp.FPSetFactory;
 import tlc2.tool.impl.DebugTool;
 import tlc2.tool.impl.FastTool;
 import tlc2.tool.impl.ParameterizedSpecObj;
+import tlc2.tool.impl.ParameterizedSpecObj.Invariant;
 import tlc2.tool.impl.ParameterizedSpecObj.PostCondition;
 import tlc2.tool.impl.Tool;
 import tlc2.tool.management.ModelCheckerMXWrapper;
@@ -189,7 +188,7 @@ public enum RunMode {
     /**
      * Interface to retrieve model properties.
      */
-    private volatile ITool tool;
+    private volatile Tool tool;
 
     /**
      * Records errors as TLC runs.
@@ -492,8 +491,12 @@ public boolean handleParameters(String[] args)
                 TLCGlobals.debug = true;
             } else if (args[index].equals("-debugger"))
             {
-                index++;
-                debugPort = 4712;  //standard port.
+				index++;
+				@SuppressWarnings("unchecked")
+				final List<Invariant> invs = (List<Invariant>) params.computeIfAbsent(ParameterizedSpecObj.INVARIANT,
+						k -> new ArrayList<Invariant>());
+				invs.add(new Invariant("_TLAPlusDebugger", "_TLAPlusDebuggerInvariant"));
+				debugPort = 4712; // standard port.
 				if ((index < args.length) && (args[index].contains("port=") || args[index].contains("nosuspend")
 						|| args[index].contains("nohalt") || args[index].contains("suspend")
 						|| args[index].contains("halt"))) {
@@ -1014,12 +1017,6 @@ else if (index < args.length)
             }
         }
 
-		if (TLCGlobals.getNumWorkers() != 1 && debugPort >= 0
-				&& !Boolean.getBoolean(TLC.class.getName() + ".multiWorkerDebug")) {
-			printErrorMsg("Error: TLA+ Debugger does not support running with multiple workers.");
-			return false;
-		}
-
         startTime = System.currentTimeMillis();
 
 		if (mainFile == null) {
@@ -1198,23 +1195,15 @@ public int process()
 				printStartupBanner(EC.TLC_MODE_SIMU, getSimulationRuntime(seed));
 
 				Simulator simulator;
+				tool = new FastTool(mainFile, configFile, resolver, Tool.Mode.Simulation, params);
 				if (debugPort >= 0) {
 					final TLCDebugger instance = TLCDebugger.Factory.getInstance(debugPort, suspend, halt);
 					synchronized (instance) {
-						tool = new DebugTool(mainFile, configFile, resolver, Tool.Mode.Simulation, params, instance);
+						tool = new DebugTool(tool, instance);
 					}
-					if (Boolean.getBoolean(TLC.class.getName() + ".multiWorkerDebug")) {
-						simulator = new Simulator(tool, metadir, traceFile, deadlock, traceDepth, 
-								traceNum, traceActions, rng, seed, resolver, TLCGlobals.getNumWorkers());
-					} else {
-						simulator = new SingleThreadedSimulator(tool, metadir, traceFile, deadlock, traceDepth, 
-								traceNum, traceActions, rng, seed, resolver);
-					}	
-				} else {
-					tool = new FastTool(mainFile, configFile, resolver, Tool.Mode.Simulation, params);
-					simulator = new Simulator(tool, metadir, traceFile, deadlock, traceDepth, 
-	                        traceNum, traceActions, rng, seed, resolver, TLCGlobals.getNumWorkers());
 				}
+				simulator = new Simulator(tool, metadir, traceFile, deadlock, traceDepth, 
+						traceNum, traceActions, rng, seed, resolver, TLCGlobals.getNumWorkers());
                 TLCGlobals.simulator = simulator;
                 result = simulator.simulate();
 			} else { // RunMode.MODEL_CHECK
@@ -1231,13 +1220,13 @@ public int process()
 				printStartupBanner(isBFS() ? EC.TLC_MODE_MC : EC.TLC_MODE_MC_DFS, getModelCheckingRuntime(fpIndex, fpSetConfiguration));
 
             	// model checking
+				tool = new FastTool(mainFile, configFile, resolver, debugPort >= 0 ? Tool.Mode.MC_DEBUG : Tool.Mode.MC,
+						params);
 				if (debugPort >= 0) {
 					final TLCDebugger instance = TLCDebugger.Factory.getInstance(debugPort, suspend, halt);
 					synchronized (instance) {
-						tool = new DebugTool(mainFile, configFile, resolver, params, instance);
-					}
-				} else {
-					tool = new FastTool(mainFile, configFile, resolver, params);
+						tool = new DebugTool(tool, instance);
+					}											
 				}
                 deadlock = deadlock && tool.getModelConfig().getCheckDeadlock();
                 if (isBFS())

diff --git a/tlatools/org.lamport.tlatools/src/tlc2/debug/StandaloneConstExpressionDebugger.java b/tlatools/org.lamport.tlatools/src/tlc2/debug/StandaloneConstExpressionDebugger.java
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/DebugTool.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/DebugTool.java
@@ -25,11 +25,8 @@
  ******************************************************************************/
 package tlc2.tool.impl;
 
-import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.HashSet;
-import java.util.List;
-import java.util.Map;
 import java.util.Set;
 import java.util.function.Supplier;
 
@@ -42,6 +39,7 @@
 import tlc2.debug.IDebugTarget.AbortEvalException;
 import tlc2.debug.IDebugTarget.ResetEvalException;
 import tlc2.debug.IDebugTarget.StepDirection;
+import tlc2.debug.TLCDebugger;
 import tlc2.tool.Action;
 import tlc2.tool.EvalControl;
 import tlc2.tool.EvalException;
@@ -54,13 +52,11 @@
 import tlc2.tool.TLCStateFun;
 import tlc2.tool.TLCStateMutExt;
 import tlc2.tool.coverage.CostModel;
-import tlc2.tool.impl.ParameterizedSpecObj.Invariant;
 import tlc2.util.Context;
 import tlc2.util.SetOfStates;
 import tlc2.value.IValue;
 import tlc2.value.impl.Value;
 import util.Assert.TLCRuntimeException;
-import util.FilenameToStream;
 
 @SuppressWarnings("serial")
 public class DebugTool extends Tool {
@@ -74,14 +70,6 @@ public static boolean forceViolation() {
 	public static void setForceViolation() {
 		forceViolation = true;
 	}
-
-	private static Map<String, Object> getParams(Map<String, Object> params) {
-		@SuppressWarnings("unchecked")
-		final List<Invariant> invs = (List<Invariant>) params.computeIfAbsent(
-				ParameterizedSpecObj.INVARIANT, k -> new ArrayList<Invariant>());
-		invs.add(new Invariant("_TLAPlusDebugger","_TLAPlusDebuggerInvariant"));
-		return params;
-	}
 
 	private static final Set<Integer> KINDS = new HashSet<>(
 			Arrays.asList(ASTConstants.NumeralKind, ASTConstants.DecimalKind, ASTConstants.StringKind));
@@ -94,7 +82,7 @@ private static Map<String, Object> getParams(Map<String, Object> params) {
 	 * inferring what calls correspond to liveness expressions, the liveness-related
 	 * code gets this FastTool.
 	 */
-	private final FastTool fastTool;
+	private final Tool fastTool;
 
 	private EvalMode mode = EvalMode.Const;
 
@@ -111,20 +99,13 @@ private static Map<String, Object> getParams(Map<String, Object> params) {
 	public enum EvalMode {
 		Const, State, Action, Debugger;
 	}
-
-	public DebugTool(String mainFile, String configFile, FilenameToStream resolver, final Map<String, Object> params, IDebugTarget target) {
-		this(mainFile, configFile, resolver, Mode.MC_DEBUG, params, target);
-	}
-
-	public DebugTool(String mainFile, String configFile, FilenameToStream resolver, Mode mode, final Map<String, Object> params, IDebugTarget target) {
-		super(mainFile, configFile, resolver, mode, getParams(params));
-
-		// This and FastTool share state.  Do not evaluate things concurrently.
-		this.fastTool = new FastTool(this);
-
+
+	public DebugTool(Tool tool, TLCDebugger target) {
+		super(tool);
+		this.fastTool = tool;
 		this.target = target.setTool(this);
 	}
-
+	
 	// 88888888888888888888888888888888888888888888888888888888888888888888888888 //
 
 	@Override

diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/WorkerValue.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/WorkerValue.java
@@ -27,7 +27,6 @@
 
 import tla2sany.semantic.ExprOrOpArgNode;
 import tlc2.TLCGlobals;
-import tlc2.tool.ITool;
 import tlc2.tool.TLCState;
 import tlc2.tool.coverage.CostModel;
 import tlc2.util.Context;
@@ -132,8 +131,7 @@ public static Object demux(final OpDefEvaluator spec, final ExprOrOpArgNode en,
     			RandomEnumerableValues.setSeed(seed);
     			// Ideally, we could invoke IValue#deepCopy here instead of evaluating opDef again.  However,
     			// IValue#deepCopy doesn't create copies for most values.
-				final ITool noDebug = ((ITool) spec).noDebug();
-				values[i] = noDebug.eval(en, Context.Empty, TLCState.Empty, cm);
+				values[i] = spec.eval(en, Context.Empty, TLCState.Empty, cm);
     			values[i].deepNormalize();
     		}
 

diff --git a/tlatools/org.lamport.tlatools/test/tlc2/tool/SimulatorTest.java b/tlatools/org.lamport.tlatools/test/tlc2/tool/SimulatorTest.java
@@ -1,27 +1,26 @@
 package tlc2.tool;
 
+import static org.junit.Assert.assertTrue;
+
+import java.io.IOException;
+import java.util.HashMap;
+
 import org.junit.Test;
 
-import tlc2.debug.StandaloneConstExpressionDebugger;
 import tlc2.output.EC;
 import tlc2.output.MP;
-import tlc2.tool.impl.DebugTool;
+import tlc2.tool.impl.FastTool;
 import tlc2.util.RandomGenerator;
 import util.Assert;
 import util.SimpleFilenameToStream;
 
-import java.io.IOException;
-import java.util.HashMap;
-
-import static org.junit.Assert.assertTrue;
-
 public class SimulatorTest extends CommonTestCase {
 
     @Test
     public void testPrintBehaviorShouldPrintErrorState() throws IOException {
         MP.setRecorder(recorder);
-        Simulator simulator = new Simulator(new DebugTool(BASE_PATH + "Github726", BASE_PATH + "Github726", new SimpleFilenameToStream(),
-                new HashMap<>(), new StandaloneConstExpressionDebugger()), null,
+        Simulator simulator = new Simulator(new FastTool(BASE_PATH + "Github726", BASE_PATH + "Github726", new SimpleFilenameToStream(),
+                new HashMap<>()), null,
                 "", false, -1, 0, null,
                 new RandomGenerator(0), 0, new SimpleFilenameToStream(), 0);
         final StateVec stateVec = new StateVec(1);