it starts running, again!

* fixes of NPE
* connect UI to DebuggerFramework
* add frames combobox and context analysis
  * including bugs

Now, testing the big things!

lang/src/main/java/edu/kit/iti/formal/psdbg/ShortCommandPrinter.java

+package edu.kit.iti.formal.psdbg;
+
+import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
+import edu.kit.iti.formal.psdbg.parser.Facade;
+import edu.kit.iti.formal.psdbg.parser.ast.*;
+
+/**
+ * Prints every command to a single line representation.
+ *
+ * @author Alexander Weigl
+ * @version 1
+ */
+public class ShortCommandPrinter extends DefaultASTVisitor<String> {
+    @Override
+    public String defaultVisit(ASTNode node) {
+        return (Facade.prettyPrint(node));
+    }
+
+    @Override
+    public String visit(ProofScript proofScript) {
+        return String.format("script %s (%s) {%n",
+                proofScript.getName(),
+                Facade.prettyPrint(proofScript.getSignature()));
+    }
+
+    @Override
+    public String visit(CasesStatement casesStatement) {
+        return "cases {";
+    }
+
+    @Override
+    public String visit(SimpleCaseStatement caseStatement) {
+        return "case " + Facade.prettyPrint(caseStatement.getGuard());
+    }
+
+    @Override
+    public String visit(TryCase tryCase) {
+        return "try " + Facade.prettyPrint(tryCase.getBody());
+    }
+
+    @Override
+    public String visit(ClosesCase closesCase) {
+        return "closes with {" + Facade.prettyPrint(closesCase.getClosesScript()) + "}";
+    }
+
+    @Override
+    public String visit(TheOnlyStatement theOnly) {
+        return "theonly {";
+    }
+
+    @Override
+    public String visit(ForeachStatement foreach) {
+        return "foreach {";
+    }
+
+    @Override
+    public String visit(RepeatStatement repeatStatement) {
+        return ("repeat {");
+    }
+}

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/PrettyPrinter.java

@@ -41,12 +41,15 @@ import java.util.Map;
 public class PrettyPrinter extends DefaultASTVisitor<Void> {
 
     private final StringBuilder s = new StringBuilder();
+
     @Getter
     @Setter
     private int maxWidth = 80;
+
     @Getter
     @Setter
     private boolean unicode = true;
+
     private int indentation = 0;
 
     @Override
@@ -187,8 +190,11 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
 
     @Override
     public Void visit(CallStatement call) {
-        s.append(call.getCommand()).append(' ');
-        call.getParameters().accept(this);
+        s.append(call.getCommand());
+        if (call.getParameters().size() != 0) {
+            s.append(' ');
+            call.getParameters().accept(this);
+        }
         s.append(";");
         return null;
     }

rt-key/src/main/java/edu/kit/iti/formal/psdbg/InteractiveCLIDebugger.java

@@ -9,7 +9,6 @@ import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
 import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
 import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
 import edu.kit.iti.formal.psdbg.interpreter.dbg.*;
-import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
 import edu.kit.iti.formal.psdbg.parser.Facade;
 import edu.kit.iti.formal.psdbg.parser.ast.*;
 import org.apache.logging.log4j.LogManager;
@@ -82,7 +81,7 @@ public class InteractiveCLIDebugger {
         System.out.println("digraph G {");
         for (PTreeNode<KeyData> n : df.getStates()) {
             System.out.format("%d [label=\"%s@%s (G: %d)\"]%n", n.hashCode(),
-                    n.getStatement().accept(new CommandPrinter()),
+                    n.getStatement().accept(new ShortCommandPrinter()),
                     n.getStatement().getStartPosition().getLineNumber(),
                     n.getStateBeforeStmt().getGoals().size()
             );
@@ -154,7 +153,7 @@ public class InteractiveCLIDebugger {
     private void printNode(PTreeNode<KeyData> node) {
         System.out.format("%3d: %s%n",
                 node.getStatement().getStartPosition().getLineNumber(),
-                node.getStatement().accept(new CommandPrinter())
+                node.getStatement().accept(new ShortCommandPrinter())
         );
 
         for (GoalNode<KeyData> gn : node.getStateBeforeStmt().getGoals()) {
@@ -171,52 +170,3 @@ public class InteractiveCLIDebugger {
         //df.addBreakpoint(breakpoint);
     }
 }
-
-class CommandPrinter extends DefaultASTVisitor<String> {
-    @Override
-    public String defaultVisit(ASTNode node) {
-        return (Facade.prettyPrint(node));
-    }
-
-    @Override
-    public String visit(ProofScript proofScript) {
-        return String.format("script %s (%s) {%n",
-                proofScript.getName(),
-                Facade.prettyPrint(proofScript.getSignature()));
-    }
-
-    @Override
-    public String visit(CasesStatement casesStatement) {
-        return "cases {";
-    }
-
-    @Override
-    public String visit(SimpleCaseStatement caseStatement) {
-        return "case " + Facade.prettyPrint(caseStatement.getGuard());
-    }
-
-    @Override
-    public String visit(TryCase tryCase) {
-        return "try " + Facade.prettyPrint(tryCase.getBody());
-    }
-
-    @Override
-    public String visit(ClosesCase closesCase) {
-        return "closes with {" + Facade.prettyPrint(closesCase.getClosesScript()) + "}";
-    }
-
-    @Override
-    public String visit(TheOnlyStatement theOnly) {
-        return "theonly {";
-    }
-
-    @Override
-    public String visit(ForeachStatement foreach) {
-        return "foreach {";
-    }
-
-    @Override
-    public String visit(RepeatStatement repeatStatement) {
-        return ("repeat {");
-    }
-}

rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYProofFacade.java

@@ -50,9 +50,36 @@ public class KeYProofFacade {
      * BooleanProperty inidcating whether KeY finished loading
      */
     private BooleanBinding readyToExecute = proof.isNotNull();
+
     //Workaround until api is relaxed
     private ProofManagementApi pma;
 
+    /**
+     *
+     */
+    public ProofState getProofState() {
+        Proof p = proof.get();
+        if (p == null)
+            return ProofState.EMPTY;
+
+        if (p.root().childrenCount() == 0)
+            return ProofState.VIRGIN;
+
+        return ProofState.DIRTY;
+    }
+
+    /**
+     * reload the current proof. synchronously because only the first load is slow.
+     */
+    public void reload() throws ProofInputException, ProblemLoaderException {
+        if (contract.get() != null) {// reinstante the contract
+            setProof(getEnvironment().createProof(
+                    contract.get().getProofObl(getEnvironment().getServices())));
+        } else {
+            setProof(KeYApi.loadFromKeyFile(proof.get().getProofFile()).getLoadedProof().getProof());
+        }
+    }
+
     //region loading
     public Task<ProofApi> loadKeyFileTask(File keYFile) {
         Task<ProofApi> task = new Task<ProofApi>() {
@@ -117,14 +144,13 @@ public class KeYProofFacade {
         proof.set(pa.getProof());
         contract.set(null);
     }
-    //endregion
 
     /**
      * Build the KeYInterpreter that handles the execution of the loaded key problem sourceName
      */
     public InterpreterBuilder buildInterpreter() {
         assert readyToExecute.getValue();
-
+        assert getEnvironment() != null && getProof() != null : "No proof loaded";
         InterpreterBuilder interpreterBuilder = new InterpreterBuilder();
         interpreterBuilder
                 .proof(environment.get(), proof.get())
@@ -136,7 +162,7 @@ public class KeYProofFacade {
 
         return interpreterBuilder;
     }
-
+    //endregion
 
     /**
      * Reload all KeY structure if proof should be reloaded
@@ -202,6 +228,10 @@ public class KeYProofFacade {
         KeyData data = new KeyData(proof.get().root(), getEnvironment(), getProof());
         return Collections.singleton(new GoalNode<>(null, data, data.getNode().isClosed()));
     }
+
+    public enum ProofState {
+        EMPTY, VIRGIN, DIRTY;
+    }
     //endregion
 }
 

rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/Blocker.java

@@ -9,8 +9,8 @@ import lombok.Getter;
 import lombok.RequiredArgsConstructor;
 import lombok.val;
 
+import java.util.HashSet;
 import java.util.Set;
-import java.util.TreeSet;
 import java.util.concurrent.atomic.AtomicInteger;
 import java.util.function.Predicate;
 
@@ -25,7 +25,7 @@ public abstract class Blocker {
         private final Interpreter<T> interpreter;
 
         @Getter
-        private final Set<Breakpoint> breakpoints = new TreeSet<>();
+        private final Set<Breakpoint> breakpoints = new HashSet<>();
 
         private final Breakpoint cmp = new Breakpoint(null, 0);
 
@@ -52,7 +52,7 @@ public abstract class Blocker {
                     }
                 }
             }
-            return breakpoints.contains(cmp);
+            return false;
         }
     }
 
@@ -66,8 +66,9 @@ public abstract class Blocker {
 
         @Override
         public boolean test(ASTNode astNode) {
-            if (stepUntilBlock.get() >= 0) {
-                return 0 == stepUntilBlock.decrementAndGet();
+            int value;
+            if ((value = stepUntilBlock.decrementAndGet()) >= 0) {
+                return 0 == value;
             }
             return false;
         }

rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/Breakpoint.java

@@ -3,9 +3,11 @@ package edu.kit.iti.formal.psdbg.interpreter.dbg;
 import edu.kit.iti.formal.psdbg.parser.Facade;
 import edu.kit.iti.formal.psdbg.parser.ast.Expression;
 import lombok.Data;
+import lombok.EqualsAndHashCode;
 import org.antlr.v4.runtime.CharStreams;
 
 @Data
+@EqualsAndHashCode(of = {"sourceName", "lineNumber"})
 public class Breakpoint {
     private String sourceName;
 

rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/PTreeNode.java

 package edu.kit.iti.formal.psdbg.interpreter.dbg;
 
+import edu.kit.iti.formal.psdbg.ShortCommandPrinter;
 import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
 import edu.kit.iti.formal.psdbg.interpreter.data.State;
 import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
 import edu.kit.iti.formal.psdbg.parser.ast.CaseStatement;
-import edu.kit.iti.formal.psdbg.parser.ast.Parameters;
-import lombok.*;
+import lombok.Getter;
+import lombok.RequiredArgsConstructor;
+import lombok.Setter;
 
 import javax.annotation.Nullable;
-import java.util.Collections;
-import java.util.HashMap;
-import java.util.List;
-import java.util.Map;
+import java.util.*;
 
 /**
  * PTreeNode represents a node in the state graph.
@@ -23,29 +22,34 @@ import java.util.Map;
  */
 @Getter
 @Setter
-@ToString
 @RequiredArgsConstructor
 public class PTreeNode<T> {
     private final ASTNode statement;
 
     private Map<CaseStatement, List<GoalNode<T>>> mappingOfCaseToStates = new HashMap<>();
+
     private State<T> stateBeforeStmt;
+
     private State<T> stateAfterStmt;
+
     private ASTNode[] context;
 
     private boolean atomic;
 
     @Nullable
     private PTreeNode<T> stepInto;
+
     @Nullable
     private PTreeNode<T> stepOver;
+
     @Nullable
     private PTreeNode<T> stepInvOver;
+
     @Nullable
     private PTreeNode<T> stepInvInto;
+
     @Nullable
     private PTreeNode<T> stepReturn;
-    private Parameters goals;
 
     public void connectStepOver(PTreeNode<T> jumpOverTo) {
         setStepOver(jumpOverTo);
@@ -60,4 +64,36 @@ public class PTreeNode<T> {
     public List<GoalNode<T>> getActiveGoalsForCase(CaseStatement caseStmt) {
         return mappingOfCaseToStates.getOrDefault(caseStmt, Collections.emptyList());
     }
+
+    public List<PTreeNode<T>> getContextNodes() {
+        List<PTreeNode<T>> contextNodes = new ArrayList<>(context.length);
+        PTreeNode<T> cur = this;
+        outer : do {
+            // add the current node, and every node that can be reached by an inverse into pointer.
+            contextNodes.add(cur);
+
+            // if the current node doesn't have an inverse into pointer, then trace
+            // inverse over pointer (same context)
+            while (cur.getStepInvInto() == null) {
+                cur = cur.getStepInvOver();
+                if (cur == null) break outer; // we could reach the beginning of execution
+            }
+            cur = cur.getStepInvInto();
+        } while (cur != null);
+        return contextNodes;
+    }
+
+    public String getSingleRepresentation() {
+        if (getStatement().getStartPosition() != null)
+            return String.format("%d: %s",
+                    getStatement().getStartPosition().getLineNumber(),
+                    getStatement().accept(new ShortCommandPrinter()));
+        else
+            return (String) getStatement().accept(new ShortCommandPrinter());
+    }
+
+    @Override
+    public String toString() {
+        return getSingleRepresentation();
+    }
 }
\ No newline at end of file

rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/ProofTreeManager.java

@@ -159,4 +159,5 @@ public class ProofTreeManager<T> {
         if (!suppressStatePointerListener)
             statePointerListener.forEach(l -> l.accept(statePointer));
     }
+
 }

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java

@@ -4,11 +4,14 @@ import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
 import de.uka.ilkd.key.api.ProofApi;
 import de.uka.ilkd.key.proof.init.ProofInputException;
+import de.uka.ilkd.key.proof.io.ProblemLoaderException;
 import de.uka.ilkd.key.speclang.Contract;
+import edu.kit.iti.formal.psdbg.StepIntoCommand;
 import edu.kit.iti.formal.psdbg.examples.Examples;
 import edu.kit.iti.formal.psdbg.gui.ProofScriptDebugger;
 import edu.kit.iti.formal.psdbg.gui.controls.*;
 import edu.kit.iti.formal.psdbg.gui.model.DebuggerMainModel;
+import edu.kit.iti.formal.psdbg.gui.model.InspectionModel;
 import edu.kit.iti.formal.psdbg.interpreter.InterpreterBuilder;
 import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
 import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
@@ -105,19 +108,28 @@ public class DebuggerMain implements Initializable {
 
         //register the welcome dock in the center
         welcomePaneDock.dock(dockStation, DockPos.LEFT);
-        registerToolbarToStatusBar();
         //statusBar.publishMessage("File: " + (newValue != null ? newValue.getAbsolutePath() : "n/a"));
         marriageJavaCode();
 
         //marriage key proof facade to proof tree
         getFacade().proofProperty().addListener(
                 (prop, o, n) -> {
-                    proofTree.setRoot(n.root());
+                    if (n == null) {
+                        proofTree.setRoot(null);
+                    } else {
+                        proofTree.setRoot(n.root());
+                        getInspectionViewsController().getActiveInspectionViewTab()
+                                .getModel().getGoals().setAll(FACADE.getPseudoGoals());
+                    }
                     proofTree.setProof(n);
-                    getInspectionViewsController().getActiveInspectionViewTab().getModel().getGoals().setAll(FACADE.getPseudoGoals());
                 }
         );
 
+        //
+        model.statePointerProperty().addListener((prop, o, n) -> {
+            this.handleStatePointerUI(n);
+        });
+
         //Debugging
         Utils.addDebugListener(model.javaCodeProperty());
         Utils.addDebugListener(model.executeNotPossibleProperty(), "executeNotPossible");
@@ -125,6 +137,7 @@ public class DebuggerMain implements Initializable {
         initializeExamples();
     }
 
+
     /**
      * If the mouse moves other toolbar button, the help text should display in the status bar
      */
@@ -137,7 +150,8 @@ public class DebuggerMain implements Initializable {
     }
 
     /**
-     * *Note:* This is executed in the Interpreter!
+     * <b>Note:</b> This is executed in the Interpreter Thread!
+     * You should listen to the {@link DebuggerMainModel#statePointerProperty}
      *
      * @param node
      */
@@ -145,6 +159,29 @@ public class DebuggerMain implements Initializable {
         Platform.runLater(() -> model.setStatePointer(node));
     }
 
+    /**
+     * Handling of a new state in the {@link DebuggerFramework}, now in the JavaFX Thread
+     *
+     * @see {@link #handleStatePointer(PTreeNode)}
+     */
+    private void handleStatePointerUI(PTreeNode<KeyData> node) {
+        InspectionModel im = getInspectionViewsController().getActiveInspectionViewTab().getModel();
+
+        im.getGoals().setAll(
+                node.getStateBeforeStmt().getGoals()
+        );
+        im.setSelectedGoalNodeToShow(
+                node.getStateBeforeStmt().getSelectedGoalNode());
+
+        scriptController.getDebugPositionHighlighter().highlight(node.getStatement());
+
+        //Experimental
+        ComboBox<PTreeNode<KeyData>> frames = getInspectionViewsController().getActiveInspectionViewTab().getFrames();
+        List<PTreeNode<KeyData>> ctxn = node.getContextNodes();
+        frames.getItems().setAll(ctxn);
+        frames.getSelectionModel().select(node);
+    }
+
     private void marriageJavaCode() {
         //Listener on chosenContract from
         model.chosenContractProperty().addListener(o -> {
@@ -217,30 +254,6 @@ public class DebuggerMain implements Initializable {
         }
     }
 
-    /**
-     * Reload the KeY environment, to execute the script again
-     * TODO: reload views
-     *
-     * @param file
-     * @param keyfile
-     * @return
-     */
-    public Task<Void> reloadEnvironment(File file, boolean keyfile) {
-        Task<Void> task = new Task<Void>() {
-            @Override
-            protected Void call() throws Exception {
-                FACADE.reloadEnvironment();
-                if (keyfile) {
-                    openKeyFile(file);
-                } else {
-                    openJavaFile(file);
-                }
-                return null;
-            }
-        };
-        return task;
-    }
-
     @FXML
     public void executeScript() {
         executeScript(false);
@@ -283,32 +296,25 @@ public class DebuggerMain implements Initializable {
 
         assert model.getDebuggerFramework() == null : "There should not be any interpreter running.";
 
-        File file;
-        boolean isKeyfile = false;
-        if (model.getJavaFile() != null) {
-            file = model.getJavaFile();
-        } else {
-            isKeyfile = true;
-            file = model.getKeyFile();
+        if (FACADE.getProofState() == KeYProofFacade.ProofState.EMPTY) {
+            Alert alert = new Alert(Alert.AlertType.ERROR, "No proof loaded!", ButtonType.OK);
+            alert.showAndWait();
+            return;
         }
 
+        if (FACADE.getProofState() == KeYProofFacade.ProofState.DIRTY) {
+            try {
+                FACADE.reload();
+            } catch (ProofInputException | ProblemLoaderException e) {
+                //TODO
+                Utils.showExceptionDialog("Loading Error", "Could not clear Environment", "There was an error when clearing old environment",
+                        e
+                );
+            }
+        }
 
-        Task<Void> reloading = reloadEnvironment(file, isKeyfile);
-        reloading.setOnSucceeded(event -> {
-            statusBar.publishMessage("Cleared and Reloaded Environment");
-            executeScript(FACADE.buildInterpreter(), addInitBreakpoint);
-        });
-
-        reloading.setOnFailed(event -> {
-            event.getSource().exceptionProperty().get();
-            Utils.showExceptionDialog("Loading Error", "Could not clear Environment", "There was an error when clearing old environment",
-                    (Throwable) event.getSource().exceptionProperty().get()
-            );
-        });
-
-        ProgressBar bar = new ProgressBar();
-        bar.progressProperty().bind(reloading.progressProperty());
-        executorService.execute(reloading);
+        // else getProofState() == VIRGIN!
+        executeScript(FACADE.buildInterpreter(), addInitBreakpoint);
     }
 
 
@@ -342,9 +348,10 @@ public class DebuggerMain implements Initializable {
             KeyInterpreter interpreter = ib.build();
             DebuggerFramework<KeyData> df = new DebuggerFramework<>(interpreter, ms, null);
             if (addInitBreakpoint) {
-                df.releaseUntil(new Blocker.CounterBlocker(0)); // just execute
+                df.releaseUntil(new Blocker.CounterBlocker(1)); // just execute
             }
             df.getBreakpoints().addAll(breakpoints);
+            df.getStatePointerListener().add(this::handleStatePointer);
             df.start();
 
             model.setDebuggerFramework(df);
@@ -363,7 +370,7 @@ public class DebuggerMain implements Initializable {
     public void executeToBreakpoint() {
         Set<Breakpoint> breakpoints = scriptController.getBreakpoints();
         if (breakpoints.size() == 0) {
-            System.out.println(scriptController.mainScriptProperty().get().getLineNumber());
+            //System.out.println(scriptController.mainScriptProperty().get().getLineNumber());
             //we need to add breakpoint at end if no breakpoint exists
         }
         executeScript(false);
@@ -561,6 +568,21 @@ public class DebuggerMain implements Initializable {
         }
     }
 
+
+    /**
+     * Perform a step into
+     * @param actionEvent
+     */
+    public void stepInto(ActionEvent actionEvent) {
+        LOGGER.debug("DebuggerMain.stepOver");
+        try {
+            model.getDebuggerFramework().execute(new StepIntoCommand<>());
+        } catch (DebuggerException e) {
+            Utils.showExceptionDialog("", "", "", e);
+            LOGGER.error(e);
+        }
+    }
+