Skip to content

Commit

Permalink
Replace EvalControl#Debug with DebugTool#EvalMode.
Browse files Browse the repository at this point in the history 
[Bug][TLC]
[Debugger]
  • Loading branch information
@lemmy
lemmy committed Mar 9, 2021
1 parent 6b2a79b commit d2928f0
Show file tree
Hide file tree
Showing 9 changed files with 159 additions and 115 deletions.
7 changes: 1 addition & 6 deletions tlatools/org.lamport.tlatools/src/tlc2/debug/StandaloneConstExpressionDebugger.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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);
Expand Down
31 changes: 7 additions & 24 deletions tlatools/org.lamport.tlatools/src/tlc2/debug/TLCActionStackFrame.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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 {

Expand All @@ -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<Variable> vars = new ArrayList<>();
final Map<UniqueString, IValue> vals = predecessor.getVals();
for (final Entry<UniqueString, IValue> 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);
}
Expand All @@ -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);
});
}
}
72 changes: 38 additions & 34 deletions tlatools/org.lamport.tlatools/src/tlc2/debug/TLCStackFrame.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<Variable> 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<Variable> 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() {
Expand Down
46 changes: 26 additions & 20 deletions tlatools/org.lamport.tlatools/src/tlc2/debug/TLCStateStackFrame.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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<Variable> vars = new ArrayList<>();
final Map<UniqueString, IValue> vals = state.getVals();
for (final Entry<UniqueString, IValue> 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<Variable> vars = new ArrayList<>();
final Map<UniqueString, IValue> vals = state.getVals();
for (final Entry<UniqueString, IValue> 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<Scope> scopes = new ArrayList<>();
Expand All @@ -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);
}
}
10 changes: 0 additions & 10 deletions tlatools/org.lamport.tlatools/src/tlc2/tool/EvalControl.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down Expand Up @@ -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);
}
}
4 changes: 4 additions & 0 deletions tlatools/org.lamport.tlatools/src/tlc2/tool/ITool.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -253,4 +254,7 @@ Context getFcnContext(IFcnLambdaValue fcn, ExprOrOpArgNode[] args, Context c, TL

TLCState evalAlias(TLCState curState, TLCState sucState);

default <T> T eval(Supplier<T> supplier) {
return supplier.get();
}
}
Loading

0 comments on commit d2928f0

Please sign in to comment.