diff --git a/tlatools/org.lamport.tlatools/src/tlc2/debug/StandaloneConstExpressionDebugger.java b/tlatools/org.lamport.tlatools/src/tlc2/debug/StandaloneConstExpressionDebugger.java index ca1e10c022..36858ddbd5 100644 --- a/tlatools/org.lamport.tlatools/src/tlc2/debug/StandaloneConstExpressionDebugger.java +++ b/tlatools/org.lamport.tlatools/src/tlc2/debug/StandaloneConstExpressionDebugger.java @@ -44,12 +44,8 @@ import tla2sany.semantic.ModuleNode; import tla2sany.semantic.OpDefNode; import tlc2.TLCGlobals; -import tlc2.tool.EvalControl; -import tlc2.tool.TLCState; -import tlc2.tool.coverage.CostModel; import tlc2.tool.impl.DebugTool; import tlc2.tool.impl.Tool; -import tlc2.util.Context; import tlc2.util.FP64; import util.SimpleFilenameToStream; import util.ToolIO; @@ -120,8 +116,7 @@ public void print(String str) { // as a side-effect of the debugger. TLCGlobals.expand = false; - tool.eval(valueNode.getBody(), Context.Empty, TLCState.Empty, TLCState.Empty, EvalControl.Debug, - CostModel.DO_NOT_RECORD); + tool.eval(valueNode.getBody()); }); return CompletableFuture.completedFuture(null); diff --git a/tlatools/org.lamport.tlatools/src/tlc2/debug/TLCActionStackFrame.java b/tlatools/org.lamport.tlatools/src/tlc2/debug/TLCActionStackFrame.java index 2bc3c59846..b078be767d 100644 --- a/tlatools/org.lamport.tlatools/src/tlc2/debug/TLCActionStackFrame.java +++ b/tlatools/org.lamport.tlatools/src/tlc2/debug/TLCActionStackFrame.java @@ -28,8 +28,6 @@ import java.util.ArrayList; import java.util.Arrays; import java.util.List; -import java.util.Map; -import java.util.Map.Entry; import org.eclipse.lsp4j.debug.Scope; import org.eclipse.lsp4j.debug.Variable; @@ -38,9 +36,7 @@ import tlc2.tool.TLCState; import tlc2.tool.impl.Tool; import tlc2.util.Context; -import tlc2.value.IValue; import tlc2.value.impl.LazyValue; -import util.UniqueString; public class TLCActionStackFrame extends TLCStateStackFrame { @@ -60,23 +56,9 @@ public TLCActionStackFrame(SemanticNode expr, Context c, Tool tool, TLCState pre @Override public Variable[] getVariables(int vr) { if (vr == predId) { - final List vars = new ArrayList<>(); - final Map vals = predecessor.getVals(); - for (final Entry e : vals.entrySet()) { - final UniqueString key = e.getKey(); - final IValue value = e.getValue(); - final DebugTLCVariable variable; - if (value == null) { - variable = new DebugTLCVariable(key.toString()); - variable.setValue("null"); - } else { - variable = (DebugTLCVariable) value - .toTLCVariable(new DebugTLCVariable(key.toString()), rnd); - nestedVariables.put(variable.getVariablesReference(), variable); - } - vars.add(variable); - } - return vars.toArray(new Variable[vars.size()]); + return tool.eval(() -> { + return getStateVariables(predecessor); + }); } return super.getVariables(vr); } @@ -95,8 +77,9 @@ public Scope[] getScopes() { } @Override - protected Object unlazy(LazyValue value) { - return value.eval(tool, predecessor, state); // Do not pass EvalControl.Debug here because we don't - // want to debug the un-lazying the value. + protected Object unlazy(final LazyValue lv) { + return tool.eval(() -> { + return lv.eval(tool, predecessor, state); + }); } } diff --git a/tlatools/org.lamport.tlatools/src/tlc2/debug/TLCStackFrame.java b/tlatools/org.lamport.tlatools/src/tlc2/debug/TLCStackFrame.java index ff440024f5..b9d3d5d54b 100644 --- a/tlatools/org.lamport.tlatools/src/tlc2/debug/TLCStackFrame.java +++ b/tlatools/org.lamport.tlatools/src/tlc2/debug/TLCStackFrame.java @@ -106,46 +106,50 @@ Variable[] getVariables() { } public Variable[] getVariables(final int vr) { - if (nestedVariables.containsKey(vr)) { - DebugTLCVariable[] nested = nestedVariables.get(vr).getNested(rnd); - for (DebugTLCVariable debugTLCVariable : nested) { - nestedVariables.put(debugTLCVariable.getVariablesReference(), debugTLCVariable); + return tool.eval(() -> { + if (nestedVariables.containsKey(vr)) { + DebugTLCVariable[] nested = nestedVariables.get(vr).getNested(rnd); + for (DebugTLCVariable debugTLCVariable : nested) { + nestedVariables.put(debugTLCVariable.getVariablesReference(), debugTLCVariable); + } + return nested; } - return nested; - } - final List vars = new ArrayList<>(); - if (stackId == vr) { - Context c = this.ctxt; - while (c.hasNext()) { - Object val = c.getValue(); - if (val instanceof LazyValue) { - // unlazy/eval LazyValues - val = unlazy((LazyValue) c.getValue()); + final List vars = new ArrayList<>(); + if (stackId == vr) { + Context c = this.ctxt; + while (c.hasNext()) { + Object val = c.getValue(); + if (val instanceof LazyValue) { + // unlazy/eval LazyValues + val = unlazy((LazyValue) c.getValue()); + } + if (val instanceof Value) { + final Value value = (Value) val; + final DebugTLCVariable variable = (DebugTLCVariable) value + .toTLCVariable(new DebugTLCVariable(c.getName().getName().toString()), rnd); + nestedVariables.put(variable.getVariablesReference(), variable); + vars.add(variable); + } else if (val instanceof SemanticNode) { + final Variable variable = new Variable(); + variable.setName(c.getName().getSignature()); + variable.setValue(((SemanticNode) val).getHumanReadableImage()); + vars.add(variable); + } else { + System.err.println("This is interesting!!! What's this??? " + val.toString()); + } + c = c.next(); } - if (val instanceof Value) { - final Value value = (Value) val; - final DebugTLCVariable variable = (DebugTLCVariable) value - .toTLCVariable(new DebugTLCVariable(c.getName().getName().toString()), rnd); - nestedVariables.put(variable.getVariablesReference(), variable); - vars.add(variable); - } else if (val instanceof SemanticNode) { - final Variable variable = new Variable(); - variable.setName(c.getName().getSignature()); - variable.setValue(((SemanticNode) val).getHumanReadableImage()); - vars.add(variable); - } else { - System.err.println("This is interesting!!! What's this??? " + val.toString()); - } - c = c.next(); } - } - return vars.toArray(new Variable[vars.size()]); + + return vars.toArray(new Variable[vars.size()]); + }); } - protected Object unlazy(final LazyValue value) { - return value.eval(tool); // Do not pass EvalControl.Debug here because we don't - // want to debug the un-lazying the value. + protected Object unlazy(final LazyValue lv) { + return tool.eval(() -> { + return lv.eval(tool); + }); } public Scope[] getScopes() { diff --git a/tlatools/org.lamport.tlatools/src/tlc2/debug/TLCStateStackFrame.java b/tlatools/org.lamport.tlatools/src/tlc2/debug/TLCStateStackFrame.java index ee4e9eb654..2664d0d906 100644 --- a/tlatools/org.lamport.tlatools/src/tlc2/debug/TLCStateStackFrame.java +++ b/tlatools/org.lamport.tlatools/src/tlc2/debug/TLCStateStackFrame.java @@ -36,6 +36,7 @@ import tla2sany.semantic.SemanticNode; import tlc2.tool.TLCState; +import tlc2.tool.impl.DebugTool; import tlc2.tool.impl.Tool; import tlc2.util.Context; import tlc2.value.IValue; @@ -60,27 +61,33 @@ public TLCStateStackFrame(SemanticNode node, Context ctxt, Tool tool, TLCState s @Override public Variable[] getVariables(int vr) { if (vr == stateId) { - final List vars = new ArrayList<>(); - final Map vals = state.getVals(); - for (final Entry e : vals.entrySet()) { - final UniqueString key = e.getKey(); - final IValue value = e.getValue(); - final DebugTLCVariable variable; - if (value == null) { - variable = new DebugTLCVariable(key.toString()); - variable.setValue("null"); - } else { - variable = (DebugTLCVariable) value - .toTLCVariable(new DebugTLCVariable(key.toString()), rnd); - nestedVariables.put(variable.getVariablesReference(), variable); - } - vars.add(variable); - } - return vars.toArray(new Variable[vars.size()]); + return ((DebugTool) tool).eval(() -> { + return getStateVariables(state); + }); } return super.getVariables(vr); } + protected Variable[] getStateVariables(final TLCState state) { + final List vars = new ArrayList<>(); + final Map vals = state.getVals(); + for (final Entry e : vals.entrySet()) { + final UniqueString key = e.getKey(); + final IValue value = e.getValue(); + final DebugTLCVariable variable; + if (value == null) { + variable = new DebugTLCVariable(key.toString()); + variable.setValue("null"); + } else { + variable = (DebugTLCVariable) value + .toTLCVariable(new DebugTLCVariable(key.toString()), rnd); + nestedVariables.put(variable.getVariablesReference(), variable); + } + vars.add(variable); + } + return vars.toArray(new Variable[vars.size()]); + } + @Override public Scope[] getScopes() { final List scopes = new ArrayList<>(); @@ -95,8 +102,7 @@ public Scope[] getScopes() { } @Override - protected Object unlazy(LazyValue value) { - return value.eval(tool, state); // Do not pass EvalControl.Debug here because we don't - // want to debug the un-lazying the value. + protected Object unlazy(LazyValue lv) { + return lv.eval(tool, state); } } diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/EvalControl.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/EvalControl.java index 61e811cbb0..c7062adcb7 100644 --- a/tlatools/org.lamport.tlatools/src/tlc2/tool/EvalControl.java +++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/EvalControl.java @@ -27,8 +27,6 @@ public class EvalControl { */ public static final int Init = 1 << 3; - public static final int Debug = 1 <<4; - public static final int Clear = 0; private static boolean isSet(final int control, final int constant) { @@ -73,12 +71,4 @@ public static int setEnabled(int control) { public static boolean isInit(int control) { return isSet(control, Init); } - - public static int setDebug(int control) { - return control | Debug; - } - - public static boolean isDebug(int control) { - return isSet(control, Debug); - } } diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/ITool.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/ITool.java index 6e249e2814..7f29635579 100644 --- a/tlatools/org.lamport.tlatools/src/tlc2/tool/ITool.java +++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/ITool.java @@ -27,6 +27,7 @@ import java.io.File; import java.util.List; +import java.util.function.Supplier; import tla2sany.semantic.ExprNode; import tla2sany.semantic.ExprOrOpArgNode; @@ -253,4 +254,7 @@ Context getFcnContext(IFcnLambdaValue fcn, ExprOrOpArgNode[] args, Context c, TL TLCState evalAlias(TLCState curState, TLCState sucState); + default T eval(Supplier supplier) { + return supplier.get(); + } } \ No newline at end of file diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/DebugTool.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/DebugTool.java index 09d07c7ed6..444cb58019 100644 --- a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/DebugTool.java +++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/DebugTool.java @@ -28,6 +28,7 @@ import java.util.Arrays; import java.util.HashSet; import java.util.Set; +import java.util.function.Supplier; import tla2sany.semantic.ASTConstants; import tla2sany.semantic.OpApplNode; @@ -41,6 +42,7 @@ import tlc2.tool.TLCState; import tlc2.tool.coverage.CostModel; import tlc2.util.Context; +import tlc2.value.IValue; import tlc2.value.impl.Value; import util.FilenameToStream; @@ -52,14 +54,48 @@ public class DebugTool extends Tool { private final IDebugTarget target; + private EvalMode mode = EvalMode.Const; + + public enum EvalMode { + Const, State, Action, Debugger; + } + public DebugTool(String mainFile, String configFile, FilenameToStream resolver, IDebugTarget target) { super(mainFile, configFile, resolver); this.target = target; } + // 88888888888888888888888888888888888888888888888888888888888888888888888888 // + + @Override + public final IValue eval(SemanticNode expr, Context c, TLCState s0) { + mode = EvalMode.Const; + return this.evalImpl(expr, c, s0, TLCState.Empty, EvalControl.Clear, CostModel.DO_NOT_RECORD); + } + + @Override + public IValue eval(SemanticNode expr, Context c, TLCState s0, CostModel cm) { + mode = EvalMode.State; + return this.evalImpl(expr, c, s0, TLCState.Empty, EvalControl.Clear, cm); + } + @Override public final Value eval(final SemanticNode expr, final Context c, final TLCState s0, final TLCState s1, final int control, final CostModel cm) { + if (mode == EvalMode.Debugger) { + return evalImpl(expr, c, s0, s1, control, cm); + } + if (s1 == null) { + mode = EvalMode.State; + return evalImpl(expr, c, s0, s1, control, cm); + } + if (mode == EvalMode.State && s1 != null && s1.noneAssigned()) { + return evalImpl(expr, c, s0, s1, control, cm); + } + if (mode == EvalMode.Const && s0.noneAssigned() && s1.noneAssigned()) { + return evalImpl(expr, c, s0, s1, control, cm); + } + mode = EvalMode.Action; return evalImpl(expr, c, s0, s1, control, cm); } @@ -71,11 +107,6 @@ protected Value evalImpl(final SemanticNode expr, final Context c, final TLCStat // operators in SpecProcessor. return super.evalImpl(expr, c, s0, s1, control, cm); } - if (EvalControl.isDebug(control)) { - // Skip debugging when evaluation was triggered by the debugger itself. For - // example, when LazyValues get unlazied. - return super.evalImpl(expr, c, s0, s1, control, cm); - } if (KINDS.contains(expr.getKind())) { // These nodes don't seem interesting to users. They are leaves and we don't // care to see how TLC figures out that then token 1 evaluates to the IntValue 1. @@ -104,12 +135,18 @@ protected Value evalImpl(final SemanticNode expr, final Context c, final TLCStat // // base-level is). // return super.evalImpl(expr, c, s0, s1, control, cm); // } - if (s0.noneAssigned()) { - assert !s1.noneAssigned(); + if (mode == EvalMode.Debugger) { + // Skip debugging when evaluation was triggered by the debugger itself. For + // example, when LazyValues get unlazied. + return super.evalImpl(expr, c, s0, s1, control, cm); + } + if (mode == EvalMode.Const) { + assert s0.noneAssigned() && s1.noneAssigned(); // s0 and s1 can be dummies that are passed by some value instances or Tool // during the evaluation of the init-predicate or other const-level expressions. return constLevelEval(expr, c, s0, s1, control, cm); - } else if (s1.noneAssigned()) { + } else if (mode == EvalMode.State) { + assert s1 == null || s1.noneAssigned(); return stateLevelEval(expr, c, s0, s1, control, cm); } else { return actionLevelEval(expr, c, s0, s1, control, cm); @@ -170,12 +207,14 @@ protected final TLCState enabledUnchanged(final SemanticNode expr, final ActionI @Override protected final TLCState getNextStates(final Action action, final SemanticNode pred, final ActionItemList acts, final Context c, final TLCState s0, final TLCState s1, final INextStateFunctor nss, final CostModel cm) { + mode = EvalMode.Action; return getNextStatesImpl(action, pred, acts, c, s0, s1, nss, cm); } @Override protected final TLCState getNextStatesAppl(final Action action, final OpApplNode pred, final ActionItemList acts, final Context c, final TLCState s0, final TLCState s1, final INextStateFunctor nss, final CostModel cm) { + mode = EvalMode.Action; target.pushFrame(this, pred, c, s0, s1); TLCState s = getNextStatesApplImpl(action, pred, acts, c, s0, s1, nss, cm); target.popFrame(this, pred, c, s0, s1); @@ -191,6 +230,7 @@ protected final TLCState processUnchanged(final Action action, final SemanticNod @Override protected void getInitStates(SemanticNode init, ActionItemList acts, Context c, TLCState ps, IStateFunctor states, CostModel cm) { + mode = EvalMode.State; if (states instanceof WrapperStateFunctor) { // Wrap the IStateFunctor so we can intercept Tool adding a new state to the // functor. Without it, the debugger wouldn't show the fully assigned state and @@ -204,6 +244,7 @@ protected void getInitStates(SemanticNode init, ActionItemList acts, Context c, @Override protected void getInitStatesAppl(OpApplNode init, ActionItemList acts, Context c, TLCState ps, IStateFunctor states, CostModel cm) { + mode = EvalMode.State; target.pushFrame(this, init, c, ps); super.getInitStatesAppl(init, acts, c, ps, states, cm); target.popFrame(this, init, c, ps); @@ -211,6 +252,7 @@ protected void getInitStatesAppl(OpApplNode init, ActionItemList acts, Context c @Override public boolean getNextStates(final INextStateFunctor functor, final TLCState state) { + mode = EvalMode.Action; if (functor instanceof WrapperNextStateFunctor) { return super.getNextStates(functor, state); } else { @@ -250,4 +292,24 @@ public Object addElement(TLCState predecessor, Action a, TLCState state) { return addElement; } } + + @Override + public final T eval(final Supplier supplier) { + // Evaluate supplier in the context of the debugger. In other words, the + // evaluation is *not* intercepted by DebugTool. For example, Value#toString and + // LazyValue#eval should not be intercepted when the debugger triggers toString + // or eval. + final EvalMode old = setDebugger(); + try { + return supplier.get(); + } finally { + mode = old; + } + } + + public EvalMode setDebugger() { + final EvalMode old = this.mode; + this.mode = EvalMode.Debugger; + return old; + } } diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java index c1c341b12a..b8adfb9001 100644 --- a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java +++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java @@ -1422,7 +1422,7 @@ else if (val instanceof LazyValue) { } @Override - public final IValue eval(SemanticNode expr, Context c, TLCState s0) { + public IValue eval(SemanticNode expr, Context c, TLCState s0) { return this.eval(expr, c, s0, TLCState.Empty, EvalControl.Clear, CostModel.DO_NOT_RECORD); } @@ -1538,7 +1538,7 @@ public TLCStateInfo evalAlias(TLCStateInfo current, TLCState successor) { /* Special version of eval for state expressions. */ @Override - public final IValue eval(SemanticNode expr, Context c, TLCState s0, CostModel cm) { + public IValue eval(SemanticNode expr, Context c, TLCState s0, CostModel cm) { return this.eval(expr, c, s0, TLCState.Empty, EvalControl.Clear, cm); } @@ -3264,7 +3264,7 @@ public final boolean isValid(Action act) { @Override public final boolean isValid(ExprNode expr) { - IValue val = this.eval(expr, Context.Empty, TLCState.Empty, CostModel.DO_NOT_RECORD); + IValue val = this.eval(expr); if (!(val instanceof BoolValue)) { Assert.fail(EC.TLC_EXPECTED_VALUE, new String[]{"boolean", expr.toString()}); } diff --git a/tlatools/org.lamport.tlatools/src/tlc2/value/impl/LazyValue.java b/tlatools/org.lamport.tlatools/src/tlc2/value/impl/LazyValue.java index d5739df1a7..70f7373b12 100644 --- a/tlatools/org.lamport.tlatools/src/tlc2/value/impl/LazyValue.java +++ b/tlatools/org.lamport.tlatools/src/tlc2/value/impl/LazyValue.java @@ -13,9 +13,9 @@ import tla2sany.semantic.SemanticNode; import tlc2.tool.EvalControl; import tlc2.tool.FingerprintException; -import tlc2.tool.ITool; import tlc2.tool.TLCState; import tlc2.tool.coverage.CostModel; +import tlc2.tool.impl.Tool; import tlc2.util.Context; import tlc2.value.IMVPerm; import tlc2.value.IValue; @@ -295,15 +295,15 @@ public final StringBuffer toString(StringBuffer sb, int offset, boolean swallow) } } - public Object eval(ITool tool) { - return this.eval(tool, TLCState.Empty); - } + public IValue eval(Tool tool) { + return eval(tool, TLCState.Empty); + } - public Object eval(ITool tool, TLCState s0) { - return this.eval(tool, s0, null); - } + public IValue eval(Tool tool, TLCState s0) { + return eval(tool, s0, null); + } - public Object eval(ITool tool, TLCState s0, TLCState s1) { - return tool.eval(expr, con, s0, s1, EvalControl.Debug, getCostModel()); - } + public IValue eval(Tool tool, TLCState s0, TLCState s1) { + return tool.eval(expr, con, s0, s1, EvalControl.Clear, cm); + } }