Skip to content

Commit

Permalink
TLA+ debugger support for:
Browse files Browse the repository at this point in the history 
In addition to evaluation exceptions, the debuggers now halts on
violated invariants (box properties) and missing unchanged statements
unless halting is turned off explicitly.  The debugger handles all
exceptions only once at the call site.

Reset (stepping back) to the previous stack-frame and initial
stack-frame, where a frame is defined as a point in the evaluation, from
which the
the interpreter (Tool) can resume.  However, resetting to an earlier
frame interferes with BFS because TLC's queue & seen set do *not* get
reset.

[Feature][TLC][Debugger]
  • Loading branch information
@lemmy
lemmy committed Oct 18, 2021
1 parent 235fb28 commit 4653876
Show file tree
Hide file tree
Showing 9 changed files with 354 additions and 136 deletions.
35 changes: 28 additions & 7 deletions tlatools/org.lamport.tlatools/src/tlc2/debug/IDebugTarget.java
View file
Expand Up @@ -29,6 +29,7 @@
import tla2sany.semantic.SemanticNode;
import tlc2.tool.Action;
import tlc2.tool.INextStateFunctor;
import tlc2.tool.StatefulRuntimeException;
import tlc2.tool.TLCState;
import tlc2.tool.impl.Tool;
import tlc2.util.Context;
Expand All @@ -37,9 +38,23 @@
public interface IDebugTarget {

public enum Step {
In, Out, Over, Continue
In, Out, Over, Continue, Reset, Reset_Start
};

@SuppressWarnings("serial")
class ResetEvalException extends RuntimeException {

public final TLCStackFrame frame;

public ResetEvalException(TLCStackFrame frame) {
this.frame = frame;
}

public boolean isTarget(SemanticNode expr) {
return frame.getNode() == expr;
}
}

IDebugTarget pushFrame(Tool tool, SemanticNode expr, Context c);

IDebugTarget popFrame(Tool tool, SemanticNode expr, Context c);
Expand All @@ -60,19 +75,25 @@ public enum Step {

IDebugTarget popFrame(Tool tool, SemanticNode expr, Context c, Value v, TLCState predecessor, TLCState state);

IDebugTarget popExceptionFrame(Tool tool, SemanticNode expr, Context c, Value v, TLCState predecessor, TLCState state, StatefulRuntimeException e);

IDebugTarget popFrame(Tool tool, OpDefNode expr, Context c, TLCState predecessor, Action a, INextStateFunctor fun);

// No popExceptionFrame because TLC cannot recover from an exception!
IDebugTarget pushExceptionFrame(Tool tool, SemanticNode expr, Context c, RuntimeException e);
IDebugTarget pushExceptionFrame(Tool tool, SemanticNode expr, Context c, StatefulRuntimeException e);

IDebugTarget popExceptionFrame(Tool tool, SemanticNode expr, Context c, Value v, StatefulRuntimeException e);

IDebugTarget pushExceptionFrame(Tool tool, SemanticNode expr, Context c, TLCState state, StatefulRuntimeException e);

IDebugTarget pushExceptionFrame(Tool tool, SemanticNode expr, Context c, TLCState state, RuntimeException e);
IDebugTarget popExceptionFrame(Tool tool, SemanticNode expr, Context c, Value v, TLCState state, StatefulRuntimeException e);

IDebugTarget pushExceptionFrame(Tool tool, SemanticNode expr, Context c, TLCState predecessor, Action a, TLCState state,
RuntimeException e);
StatefulRuntimeException e);

IDebugTarget markInvariantViolatedFrame(Tool debugTool, SemanticNode pred, Context c, TLCState predecessor, TLCState state, RuntimeException e);
IDebugTarget popExceptionFrame(Tool tool, SemanticNode expr, Context c, TLCState predecessor, Action a, TLCState state,
StatefulRuntimeException e);

IDebugTarget markInvariantViolatedFrame(Tool debugTool, SemanticNode pred, Context c, TLCState predecessor, Action a, TLCState state, RuntimeException e);
IDebugTarget markInvariantViolatedFrame(Tool debugTool, SemanticNode pred, Context c, TLCState predecessor, Action a, TLCState state, StatefulRuntimeException e);

//------------------------ Wrapper --------------------------//

Expand Down
136 changes: 100 additions & 36 deletions tlatools/org.lamport.tlatools/src/tlc2/debug/TLCDebugger.java
View file
Expand Up @@ -50,6 +50,7 @@
import org.eclipse.lsp4j.debug.NextArguments;
import org.eclipse.lsp4j.debug.OutputEventArguments;
import org.eclipse.lsp4j.debug.PauseArguments;
import org.eclipse.lsp4j.debug.ReverseContinueArguments;
import org.eclipse.lsp4j.debug.ScopesArguments;
import org.eclipse.lsp4j.debug.ScopesResponse;
import org.eclipse.lsp4j.debug.SetBreakpointsArguments;
Expand All @@ -62,6 +63,7 @@
import org.eclipse.lsp4j.debug.StackFrame;
import org.eclipse.lsp4j.debug.StackTraceArguments;
import org.eclipse.lsp4j.debug.StackTraceResponse;
import org.eclipse.lsp4j.debug.StepBackArguments;
import org.eclipse.lsp4j.debug.StepInArguments;
import org.eclipse.lsp4j.debug.StepOutArguments;
import org.eclipse.lsp4j.debug.StoppedEventArguments;
Expand All @@ -82,6 +84,7 @@
import tlc2.TLCGlobals;
import tlc2.tool.Action;
import tlc2.tool.INextStateFunctor;
import tlc2.tool.StatefulRuntimeException;
import tlc2.tool.TLCState;
import tlc2.tool.impl.Tool;
import tlc2.util.Context;
Expand All @@ -96,20 +99,23 @@ public abstract class TLCDebugger extends AbstractDebugger implements IDebugTarg

public TLCDebugger() {
this.step = Step.In;
this.halt = true;
this.haltExp = true;
this.haltInv = true;
}

public TLCDebugger(final Step s, final boolean halt) {
this.step = s;
this.halt = halt;
this.haltExp = halt;
this.haltInv = halt;
}

/*
* Unit testing only!!!
*/
TLCDebugger(final Step s, final boolean halt, final boolean executionIsHalted) {
this.step = s;
this.halt = halt;
this.haltExp = halt;
this.haltInv = halt;
this.executionIsHalted = executionIsHalted;
}

Expand Down Expand Up @@ -158,25 +164,36 @@ public synchronized CompletableFuture<Capabilities> initialize(InitializeRequest
capabilities.setSupportsConditionalBreakpoints(false);
capabilities.setSupportsLogPoints(false);
// TODO: Implement stepping back for model-checking and simulation/generation.
capabilities.setSupportsStepBack(false);
// Stepping back would be hugely useful especially because TLC's evaluation behavior might be
// surprising (non-determinism). This can cause users to miss the stack-frame they wish to see.
// Implementing arbitrary navigation along stack-frames is impossible unless one implements
// undo operations for each Tool action. However, it should be good enough to reset Tool
// to e.g. the beginning of the evaluation of the next-state relation for state s, evaluation
// of the invariant for state s, evaluation of state- & action-constraints for s, ... by
// throwing a ResetEvalException.
capabilities.setSupportsStepBack(true);
return CompletableFuture.completedFuture(capabilities);
}

private ExceptionBreakpointsFilter[] getExceptionBreakpointFilters() {
final ExceptionBreakpointsFilter filter = new ExceptionBreakpointsFilter();
filter.setDefault_(this.halt);
filter.setDefault_(this.haltExp);
filter.setFilter("ExceptionBreakpointsFilter");
filter.setLabel("Halt (break) on exceptions");
return new ExceptionBreakpointsFilter[] {filter};

final ExceptionBreakpointsFilter violations = new ExceptionBreakpointsFilter();
violations.setDefault_(this.haltInv);
violations.setFilter("InvariantBreakpointsFilter");
violations.setLabel("Halt (break) on violations");

return new ExceptionBreakpointsFilter[] {filter, violations};
}

@Override
public synchronized CompletableFuture<Void> setExceptionBreakpoints(SetExceptionBreakpointsArguments args) {
if (Arrays.asList(args.getFilters()).contains("ExceptionBreakpointsFilter")) {
this.halt = true;
} else {
this.halt = false;
}
final List<String> asList = Arrays.asList(args.getFilters());
this.haltExp = asList.contains("ExceptionBreakpointsFilter");
this.haltInv = asList.contains("InvariantBreakpointsFilter");
return CompletableFuture.completedFuture(null);
}

Expand Down Expand Up @@ -242,7 +259,8 @@ public synchronized CompletableFuture<Void> disconnect(DisconnectArguments args)
breakpoints.clear();
targetLevel = -1;
step = Step.Continue;
halt = false;
haltExp = false;
haltInv = false;
this.notify();

return CompletableFuture.completedFuture(null);
Expand Down Expand Up @@ -463,6 +481,22 @@ public synchronized CompletableFuture<Void> pause(PauseArguments args) {
});
return CompletableFuture.completedFuture(null);
}

@Override
public synchronized CompletableFuture<Void> stepBack(StepBackArguments args) {
step = Step.Reset;
this.notify();

return CompletableFuture.completedFuture(null);
}

@Override
public synchronized CompletableFuture<Void> reverseContinue(ReverseContinueArguments args) {
step = Step.Reset_Start;
this.notify();

return CompletableFuture.completedFuture(null);
}

// 8888888888888888888888888888888888888888888888888888888888888888888888888 //

Expand All @@ -477,9 +511,10 @@ public synchronized CompletableFuture<Void> pause(PauseArguments args) {
private volatile int targetLevel = 1;
private volatile Step step = Step.In;

private volatile boolean halt;
private volatile boolean haltExp;
private volatile boolean haltInv;
private volatile boolean executionIsHalted = false;

@Override
public synchronized IDebugTarget pushFrame(Tool tool, SemanticNode expr, Context c) {
final TLCStackFrame frame = new TLCStackFrame(stack.peek(), expr, c, tool);
Expand Down Expand Up @@ -561,7 +596,7 @@ public synchronized IDebugTarget popFrame(Tool tool, SemanticNode expr, Context
new String(new char[this.stack.size()]).replace('\0', '#'), expr, this.stack.size()));
}
final TLCStackFrame pop = stack.pop();
assert expr == pop.getNode();
assert pop.matches(expr);
return this;
}

Expand Down Expand Up @@ -593,7 +628,7 @@ public synchronized IDebugTarget popFrame(Tool tool, SemanticNode expr, Context
@Override
public synchronized IDebugTarget popFrame(Tool tool, SemanticNode expr, Context c, TLCState s) {
final TLCStackFrame pop = stack.pop();
assert expr == pop.getNode();
assert pop.matches(expr);
return this;
}

Expand All @@ -613,62 +648,80 @@ public synchronized IDebugTarget popFrame(Tool tool, SemanticNode expr, Context
popFrame(tool, expr, c, v);
return this;
}

@Override
public synchronized IDebugTarget popExceptionFrame(Tool tool, SemanticNode expr, Context c, Value v, StatefulRuntimeException e) {
if (LOGGER.isLoggable(Level.FINER)) {
LOGGER.finer(String.format("%s Call popExceptionFrame: [%s], level: %s\n",
new String(new char[this.stack.size()]).replace('\0', '#'), expr, this.stack.size()));
}
final TLCStackFrame pop = stack.pop();
assert pop.matches(expr, e);
return this;
}

@Override
public synchronized IDebugTarget popExceptionFrame(Tool tool, SemanticNode expr, Context c, Value v, TLCState s, StatefulRuntimeException e) {
return popExceptionFrame(tool, expr, c, v, e);
}

@Override
public synchronized IDebugTarget popExceptionFrame(Tool tool, SemanticNode expr, Context c, Value v, TLCState s, TLCState t, StatefulRuntimeException e) {
return popExceptionFrame(tool, expr, c, v, e);
}

private boolean exceptionNotYetHandled(final RuntimeException e) {
private boolean exceptionNotYetHandled(final StatefulRuntimeException e) {
// The debugger handles an exception such as
// EvalException/TLCRuntimeException/InvariantViolationException) (close to) the
// call-site in Tool to point users to the most specific location. However, the
// exception also gets re-thrown for TLC's generic exception handling to deal
// with it. Potentially, this causes the debugger to catch the same exception
// again when it travels up Tool's call-stack. Here, we make sure that an exception
// only gets handled by the debugger once. Alternatively, we could have added a flag
// to EE, TRE, and IVE to mark an exception as handled by the debugger.
return stack.isEmpty() || stack.peek().exception != e;
// again when it travels up Tool's call-stack. Here, we make sure that the debugger
// handles an exception only once.
return !e.setKnown();
}

@Override
public synchronized IDebugTarget pushExceptionFrame(Tool tool, SemanticNode expr, Context c, RuntimeException e) {
public synchronized IDebugTarget pushExceptionFrame(Tool tool, SemanticNode expr, Context c, StatefulRuntimeException e) {
if (exceptionNotYetHandled(e)) {
return pushFrameAndHalt(new TLCStackFrame(stack.peek(), expr, c, tool, e), e);
return pushFrameAndHalt(haltExp, new TLCStackFrame(stack.peek(), expr, c, tool, e), e);
}
return this;
}

@Override
public synchronized IDebugTarget pushExceptionFrame(Tool tool, SemanticNode expr, Context c,
TLCState state, RuntimeException e) {
TLCState state, StatefulRuntimeException e) {
if (exceptionNotYetHandled(e)) {
return pushFrameAndHalt(new TLCStateStackFrame(stack.peek(), expr, c, tool, state, e), e);
return pushFrameAndHalt(haltExp, new TLCStateStackFrame(stack.peek(), expr, c, tool, state, e), e);
}
return this;
}

@Override
public synchronized IDebugTarget pushExceptionFrame(Tool tool, SemanticNode expr, Context c, TLCState s,
Action a, TLCState t, RuntimeException e) {
Action a, TLCState t, StatefulRuntimeException e) {
if (exceptionNotYetHandled(e)) {
return pushFrameAndHalt(new TLCActionStackFrame(stack.peek(), expr, c, tool, s, a, t, e), e);
return pushFrameAndHalt(haltExp, new TLCActionStackFrame(stack.peek(), expr, c, tool, s, a, t, e), e);
}
return this;
}

@Override
public synchronized IDebugTarget markInvariantViolatedFrame(Tool debugTool, SemanticNode expr, Context c, TLCState predecessor, TLCState state, RuntimeException e) {
if (exceptionNotYetHandled(e)) {
pushFrameAndHalt(new TLCStateStackFrame(stack.peek(), expr, c, tool, state, e), e);
}
return this;
public synchronized IDebugTarget popExceptionFrame(Tool tool, SemanticNode expr, Context c, TLCState s,
Action a, TLCState t, StatefulRuntimeException e) {
return popExceptionFrame(tool, expr, c, null, e);
}

@Override
public synchronized IDebugTarget markInvariantViolatedFrame(Tool debugTool, SemanticNode expr, Context c, TLCState predecessor, Action a, TLCState state, RuntimeException e) {
public synchronized IDebugTarget markInvariantViolatedFrame(Tool debugTool, SemanticNode expr, Context c, TLCState predecessor, Action a, TLCState state, StatefulRuntimeException e) {
if (exceptionNotYetHandled(e)) {
pushFrameAndHalt(new TLCActionStackFrame(stack.peek(), expr, c, tool, predecessor, a, state, e), e);
pushFrameAndHalt(haltInv, new TLCActionStackFrame(stack.peek(), expr, c, tool, predecessor, a, state, e), e);
}
return this;
}

private IDebugTarget pushFrameAndHalt(final TLCStackFrame frame, final RuntimeException e) {
private IDebugTarget pushFrameAndHalt(final boolean halt, final TLCStackFrame frame, final RuntimeException e) {
// Calling methods duplicate the top-most stack-frame with the exception causes
// the front-end to raise a corresponding error in the editor.

Expand Down Expand Up @@ -711,6 +764,17 @@ protected void haltExecution(final TLCStackFrame frame) {
notExpectedToHappen.printStackTrace();
java.lang.Thread.currentThread().interrupt();
}

if (Step.Reset == step) {
step = Step.In;
if (frame.parent != null) {
// If frame has no parent, there is nothing the debugger reset to--it marks the entry point of the evaluation.
throw new ResetEvalException(frame.parent);
}
} else if (Step.Reset_Start == step) {
step = Step.In;
throw new ResetEvalException(stack.getLast());
}
}

protected void sendStopped(final TLCStackFrame frame) {
Expand Down
12 changes: 12 additions & 0 deletions tlatools/org.lamport.tlatools/src/tlc2/debug/TLCStackFrame.java
View file
Expand Up @@ -59,6 +59,7 @@
import tla2sany.st.Location;
import tlc2.output.EC;
import tlc2.tool.EvalException;
import tlc2.tool.INextStateFunctor.InvariantViolatedException;
import tlc2.tool.impl.SpecProcessor;
import tlc2.tool.impl.Tool;
import tlc2.util.Context;
Expand Down Expand Up @@ -135,6 +136,9 @@ public TLCStackFrame(TLCStackFrame parent, SemanticNode node, Context ctxt, Tool

if (node instanceof NumeralNode) {
setName(Integer.toString(((NumeralNode)node).val()));
} else if (e instanceof InvariantViolatedException) {
setName(String.format("(Invariant) %s", node.getHumanReadableImage()));
setPresentationHint(StackFramePresentationHint.SUBTLE);
} else if (e != null) {
setName(String.format("(Exception) %s", node.getHumanReadableImage()));
setPresentationHint(StackFramePresentationHint.SUBTLE);
Expand Down Expand Up @@ -578,4 +582,12 @@ public boolean matches(final TLCSourceBreakpoint bp) {
//TODO why *smaller* than BEGINcolumn?
&& bp.getColumnAsInt() <= node.getLocation().beginColumn();
}

boolean matches(SemanticNode expr, RuntimeException e) {
return node == expr || (e instanceof TLCDetailedRuntimeException && ((TLCDetailedRuntimeException)e).expr == node);
}

public boolean matches(SemanticNode expr) {
return node == expr;
}
}
2 changes: 1 addition & 1 deletion tlatools/org.lamport.tlatools/src/tlc2/tool/EvalException.java
View file
Expand Up @@ -12,7 +12,7 @@
* @author Simon Zambrovski
* @version $Id$
*/
public class EvalException extends RuntimeException
public class EvalException extends StatefulRuntimeException
{
// SZ Jul 14, 2009: not used since error codes are in the {@link EC} class
// public final static int ERROR = 0;
Expand Down
2 changes: 1 addition & 1 deletion tlatools/org.lamport.tlatools/src/tlc2/tool/INextStateFunctor.java
View file
Expand Up @@ -31,7 +31,7 @@ public interface INextStateFunctor extends IStateFunctor {

Object addElement(final TLCState s, final Action a, final TLCState t);

public static class InvariantViolatedException extends RuntimeException {
public static class InvariantViolatedException extends StatefulRuntimeException {

}

Expand Down

1 comment on commit 4653876

@lemmy
Copy link
Member Author

@lemmy lemmy commented on 4653876 Oct 20, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

#677 discusses how this feature helps.

Please sign in to comment.