better status bar

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

@@ -6,12 +6,14 @@ import edu.kit.iti.formal.psdbg.interpreter.graphs.ControlFlowNode;
 import edu.kit.iti.formal.psdbg.interpreter.graphs.ControlFlowTypes;
 import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
 import lombok.Getter;
+import lombok.Setter;
 
 import javax.annotation.Nonnull;
 import javax.annotation.Nullable;
 import java.util.LinkedList;
 import java.util.List;
 import java.util.Set;
+import java.util.function.BiConsumer;
 import java.util.function.Consumer;
 
 /**
@@ -25,39 +27,37 @@ import java.util.function.Consumer;
  * <li>{@link StateWrapper}: signals the PTreeNodes</li>
  * <li></li>
  * </ol>
- *<code><pre>
- +------------------------------------------------------------------------------------------+
- |                                                                                          |
- |                               DebuggerFramework<T>                                       |
- |                                                                                          +------------+
- |                                                                                          |           execute(DebuggerCommand)
- |                                                                                          |              Commands: StepOver, StepInto,
- |    +------------------+       +-----------------+       +---------------------------+    |                        StepReturn, StepBack
- |    |                  |       |                 |       |                           |    |
- |    |  Interpreter<T>  +-------> StateWrapper<T> +------->  PTreeManager<T>          +--------->
- |    |                  |       |                 |       |                           |    |
- |    +---------+--------+       +-----------------+       +---------------------------+    |    statePointerChanged(PTreeNode<T>)
- |              |                                                                           |
- |              |         Listener                  emitNode                                |
- |              |                                                                           |
- |              |                                                                           |
- |    +---------v------------+                                                              |
- |    |                      <--------------------------------------------------------------------+  releaseForever()
- |    |    BlockerListener   |                                                              |        release()
- |    |                      |                                                              |        releaseUntil(BlockerPredicate)
- |    +----------------------+                                                              |        getBreakpoints()
- |                                                                                          |
- |                                                                                          |
- |    +----------------+      +---------------------+                                       |
- |    |                |      |                     |                                       |
- |    |   Breakpoint   |      |   BlockerPredicate  |                                       |
- |    |                |      |                     |                                       |
- |    +----------------+      +---------------------+                                       |
- |                                                                                          |
- +------------------------------------------------------------------------------------------+
- </pre></code>
- *
- *
+ * <code><pre>
+ * +------------------------------------------------------------------------------------------+
+ * |                                                                                          |
+ * |                               DebuggerFramework<T>                                       |
+ * |                                                                                          +------------+
+ * |                                                                                          |           execute(DebuggerCommand)
+ * |                                                                                          |              Commands: StepOver, StepInto,
+ * |    +------------------+       +-----------------+       +---------------------------+    |                        StepReturn, StepBack
+ * |    |                  |       |                 |       |                           |    |
+ * |    |  Interpreter<T>  +-------> StateWrapper<T> +------->  PTreeManager<T>          +--------->
+ * |    |                  |       |                 |       |                           |    |
+ * |    +---------+--------+       +-----------------+       +---------------------------+    |    statePointerChanged(PTreeNode<T>)
+ * |              |                                                                           |
+ * |              |         Listener                  emitNode                                |
+ * |              |                                                                           |
+ * |              |                                                                           |
+ * |    +---------v------------+                                                              |
+ * |    |                      <--------------------------------------------------------------------+  releaseForever()
+ * |    |    BlockerListener   |                                                              |        release()
+ * |    |                      |                                                              |        releaseUntil(BlockerPredicate)
+ * |    +----------------------+                                                              |        getBreakpoints()
+ * |                                                                                          |
+ * |                                                                                          |
+ * |    +----------------+      +---------------------+                                       |
+ * |    |                |      |                     |                                       |
+ * |    |   Breakpoint   |      |   BlockerPredicate  |                                       |
+ * |    |                |      |                     |                                       |
+ * |    +----------------+      +---------------------+                                       |
+ * |                                                                                          |
+ * +------------------------------------------------------------------------------------------+
+ * </pre></code>
  *
  * @author Alexander Weigl
  * @version 1 (27.10.17)
@@ -65,11 +65,12 @@ import java.util.function.Consumer;
 public class DebuggerFramework<T> {
     private final Interpreter<T> interpreter;
 
-    @Getter
+    /*@Getter
     private final List<Consumer<PTreeNode<T>>> beforeExecutionListener = new LinkedList<>();
 
     @Getter
     private final List<Consumer<PTreeNode<T>>> afterExecutionListener = new LinkedList<>();
+    */
 
     @Getter
     private final List<Consumer<PTreeNode<T>>> currentStatePointerListener = new LinkedList<>();
@@ -82,20 +83,35 @@ public class DebuggerFramework<T> {
 
     private final StateWrapper<T> stateWrapper;
 
+    private final ProofScript mainScript;
+
+    @Getter @Setter
+    private BiConsumer<DebuggerFramework<T>, Throwable> errorListener = (df, exc) -> {
+    };
+
+    @Getter @Setter
+    private Consumer<DebuggerFramework<T>> succeedListener = (df) -> {
+    };
+
     private Blocker.BreakpointLine<T> breakpointBlocker;
 
+    @Nullable
+    @Getter
+    private Throwable error;
+
 
     public DebuggerFramework(@Nonnull Interpreter<T> interpreter,
                              @Nonnull ProofScript main,
                              MutableValueGraph<ControlFlowNode, ControlFlowTypes> cfg) {
         this.interpreter = interpreter;
+        mainScript = main;
         blocker = new BlockListener<>(interpreter);
         breakpointBlocker = new Blocker.BreakpointLine<>(interpreter);
         blocker.getPredicates().add(breakpointBlocker);
         stateWrapper = new StateWrapper<>(interpreter);
         ptreeManager = new ProofTreeManager<>(cfg);
         stateWrapper.setEmitNode(ptreeManager::receiveNode);
-        interpreterThread = new Thread(() -> interpreter.interpret(main));
+        interpreterThread = new Thread(this::run);
     }
 
     public List<Consumer<PTreeNode<T>>> getStatePointerListener() {
@@ -115,6 +131,17 @@ public class DebuggerFramework<T> {
         interpreterThread.start();
     }
 
+    private void run() {
+        try {
+            interpreter.interpret(mainScript);
+            succeedListener.accept(this);
+        } catch (Exception e) {
+            error = e;
+            errorListener.accept(this, e);
+        }
+    }
+
+
     /**
      * stops the interpreter in the background on the next {@link edu.kit.iti.formal.psdbg.parser.ast.ASTNode}.
      * Does not stop the KeY framework in the background.
@@ -187,4 +214,12 @@ public class DebuggerFramework<T> {
     public Set<Breakpoint> getBreakpoints() {
         return breakpointBlocker.getBreakpoints();
     }
+
+    public Thread getInterpreterThread() {
+        return interpreterThread;
+    }
+
+    public boolean hasError() {
+        return error != null;
+    }
 }

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

@@ -6,8 +6,8 @@ import edu.kit.iti.formal.psdbg.interpreter.data.State;
 import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
 import edu.kit.iti.formal.psdbg.parser.Visitor;
 import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
+import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
 import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
-import edu.kit.iti.formal.psdbg.parser.ast.Statement;
 import edu.kit.iti.formal.psdbg.parser.ast.Statements;
 import lombok.Getter;
 import lombok.Setter;
@@ -66,7 +66,9 @@ public class StateWrapper<T> implements InterpreterObserver<T> {
         contextStack.add(node);
         State<T> currentInterpreterStateCopy = getInterpreterStateCopy();
         lastNode.setStateBeforeStmt(currentInterpreterStateCopy);
-
+        if (node instanceof CallStatement) {
+            lastNode.setAtomic(interpreter.getFunctionLookup().isAtomic((CallStatement) node));
+        }
         //add node to state graph
         return lastNode;
     }

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

@@ -6,12 +6,14 @@ 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.ShortCommandPrinter;
 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.gui.model.InterpreterThreadState;
 import edu.kit.iti.formal.psdbg.interpreter.InterpreterBuilder;
 import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
 import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
@@ -39,11 +41,17 @@ import org.apache.logging.log4j.Logger;
 import org.dockfx.DockNode;
 import org.dockfx.DockPane;
 import org.dockfx.DockPos;
+import org.reactfx.util.FxTimer;
+import org.reactfx.util.Timer;
 
+import javax.annotation.Nullable;
 import java.io.File;
+import java.io.FileWriter;
 import java.io.IOException;
+import java.io.PrintWriter;
 import java.net.URL;
 import java.nio.charset.Charset;
+import java.time.Duration;
 import java.util.List;
 import java.util.Optional;
 import java.util.ResourceBundle;
@@ -132,6 +140,8 @@ public class DebuggerMain implements Initializable {
     @FXML
     private Menu examplesMenu;
 
+    private Timer interpreterThreadTimer;
+
     @Override
     public void initialize(URL location, ResourceBundle resources) {
         Events.register(this);
@@ -194,6 +204,8 @@ public class DebuggerMain implements Initializable {
                 proofTreeDock,
                 DockPos.LEFT);
 
+        statusBar.interpreterStatusModelProperty().bind(model.interpreterStateProperty());
+        renewThreadStateTimer();
     }
 
 
@@ -427,6 +439,8 @@ public class DebuggerMain implements Initializable {
             ib.setScripts(scripts);
             KeyInterpreter interpreter = ib.build();
             DebuggerFramework<KeyData> df = new DebuggerFramework<>(interpreter, ms, null);
+            df.setSucceedListener(this::onInterpreterSucceed);
+            df.setErrorListener(this::onInterpreterError);
             if (addInitBreakpoint) {
                 df.releaseUntil(new Blocker.CounterBlocker(1)); // just execute
             }
@@ -441,6 +455,84 @@ public class DebuggerMain implements Initializable {
         }
     }
 
+    private void onInterpreterSucceed(DebuggerFramework<KeyData> keyDataDebuggerFramework) {
+        scriptController.getDebugPositionHighlighter().remove();
+        statusBar.publishMessage("Interpreter finished.");
+    }
+
+    @FXML
+    public void debugPrintDot(@Nullable ActionEvent ae) {
+        if (model.getDebuggerFramework() == null) {
+            statusBar.publishErrorMessage("can print debug info, no debugger started!");
+            return;
+        }
+        try (PrintWriter out = new PrintWriter(new FileWriter("debug.dot"))) {
+            out.println("digraph G {");
+            for (PTreeNode<KeyData> n : model.getDebuggerFramework().getStates()) {
+                out.format("%d [label=\"%s@%s (G: %d)\"]%n", n.hashCode(),
+                        n.getStatement().accept(new ShortCommandPrinter()),
+                        n.getStatement().getStartPosition().getLineNumber(),
+                        n.getStateBeforeStmt().getGoals().size()
+                );
+
+                if (n.getStepOver() != null)
+                    out.format("%d -> %d [label=\"SO\"]%n", n.hashCode(), n.getStepOver().hashCode());
+                if (n.getStepInto() != null)
+                    out.format("%d -> %d [label=\"SI\"]%n", n.hashCode(), n.getStepInto().hashCode());
+
+                if (n.getStepInvOver() != null)
+                    out.format("%d -> %d [label=\"<SO\"]%n", n.hashCode(), n.getStepInvOver().hashCode());
+                if (n.getStepInvInto() != null)
+                    out.format("%d -> %d [label=\"<SI\"]%n", n.hashCode(), n.getStepInvInto().hashCode());
+
+                if (n.getStepReturn() != null)
+                    out.format("%d -> %d [label=\"R\"]%n", n.hashCode(), n.getStepReturn().hashCode());
+
+            }
+            out.println("}");
+
+        } catch (IOException e) {
+            statusBar.publishErrorMessage(e.getMessage());
+        }
+    }
+
+    private void onInterpreterError(DebuggerFramework<KeyData> keyDataDebuggerFramework, Throwable throwable) {
+        Utils.showExceptionDialog("Error during Execution", "Error during Script Execution",
+                "Here should be some really good text...\nNothing will be the same. Everything broken.",
+                throwable
+        );
+    }
+
+    private void renewThreadStateTimer() {
+        if (interpreterThreadTimer != null) {
+            interpreterThreadTimer.stop();
+        }
+        interpreterThreadTimer = FxTimer.runPeriodically(Duration.ofMillis(500),
+                () -> {
+                    if (model.getDebuggerFramework() == null) {
+                        model.setInterpreterState(InterpreterThreadState.NO_THREAD);
+                    } else {
+                        Thread t = model.getDebuggerFramework().getInterpreterThread();
+                        switch (t.getState()) {
+                            case NEW:
+                            case BLOCKED:
+                            case WAITING:
+                            case TIMED_WAITING:
+                                model.setInterpreterState(InterpreterThreadState.WAIT);
+                                break;
+                            case TERMINATED:
+                                if (model.getDebuggerFramework().hasError())
+                                    model.setInterpreterState(InterpreterThreadState.ERROR);
+                                else
+                                    model.setInterpreterState(InterpreterThreadState.FINISHED);
+                                break;
+                            default:
+                                model.setInterpreterState(InterpreterThreadState.RUNNING);
+                        }
+                    }
+                });
+    }
+
     @FXML
     public void executeStepwise() {
         executeScript(true);

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/DebuggerStatusBar.java

 package edu.kit.iti.formal.psdbg.gui.controls;
 
+import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
+import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
 import edu.kit.iti.formal.psdbg.gui.controller.Events;
+import edu.kit.iti.formal.psdbg.gui.model.InterpreterThreadState;
 import edu.kit.iti.formal.psdbg.gui.model.MainScriptIdentifier;
+import javafx.animation.Animation;
+import javafx.animation.Interpolator;
+import javafx.animation.Transition;
 import javafx.beans.property.IntegerProperty;
 import javafx.beans.property.ObjectProperty;
 import javafx.beans.property.SimpleIntegerProperty;
 import javafx.beans.property.SimpleObjectProperty;
 import javafx.event.EventHandler;
+import javafx.geometry.Insets;
 import javafx.scene.control.Control;
 import javafx.scene.control.Label;
 import javafx.scene.control.ProgressIndicator;
+import javafx.scene.control.Separator;
 import javafx.scene.input.MouseEvent;
+import javafx.scene.layout.Background;
+import javafx.scene.layout.BackgroundFill;
+import javafx.scene.layout.CornerRadii;
+import javafx.scene.paint.Color;
+import javafx.util.Duration;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
 import org.controlsfx.control.StatusBar;
@@ -22,29 +35,49 @@ import org.controlsfx.control.StatusBar;
  */
 public class DebuggerStatusBar extends StatusBar {
     private static final Logger LOGGER = LogManager.getLogger(DebuggerStatusBar.class);
+
     //private final Dialog<Void> loggerDialog = createDialog();
     //private final ContextMenu contextMenu = createContextMenu();
     //private final Appender loggerHandler = createAppender();
     //private LogCatchHandlerFX logCatchHandler = new LogCatchHandlerFX();
+    private ObjectProperty<InterpreterThreadState> interpreterStatusModel = new SimpleObjectProperty<>();
 
     private ObjectProperty<MainScriptIdentifier> mainScriptIdentifier = new SimpleObjectProperty<>();
 
     private IntegerProperty numberOfGoals = new SimpleIntegerProperty(0);
 
+    private Label lblCurrentNodes = new Label("#nodes: %s");
+
+    private Label lblMainscript = new Label();
+
+    private MaterialDesignIconView interpreterStatusView =
+            new MaterialDesignIconView(MaterialDesignIcon.MATERIAL_UI, "2.3em");
+
+
+    private ProgressIndicator progressIndicator = new ProgressIndicator();
+
+    private EventHandler<MouseEvent> toolTipHandler = event ->
+            publishMessage(((Control) event.getTarget()).getTooltip().getText());
+
     public DebuggerStatusBar() {
         //listenOnField("psdbg");
 
         getRightItems().addAll(
-                lblMainscript
+                lblMainscript,
+                new Separator(),
+                interpreterStatusView
                 //lblCurrentNodes,
                 //progressIndicator
         );
 
-        /*setOnMouseClicked(event -> {
-            if (event.getButton() == MouseButton.SECONDARY) {
-                contextMenu.show(this, event.getScreenX(), event.getScreenY());
-            }
-        });*/
+        interpreterStatusModel.addListener((p, o, n) -> {
+            interpreterStatusView.setIcon(n.getIcon());
+            if (n == InterpreterThreadState.ERROR)
+                interpreterStatusView.setFill(Color.web("orangered"));
+            else
+                interpreterStatusView.setFill(Color.web("cornflowerblue"));
+        });
+
         numberOfGoals.addListener((observable, oldValue, newValue) -> {
             lblCurrentNodes.setText("#nodes: " + newValue);
         });
@@ -83,28 +116,10 @@ public class DebuggerStatusBar extends StatusBar {
         this.numberOfGoals.set(numberOfGoals);
     }
 
-    private Label lblCurrentNodes = new Label("#nodes: %s");
-    private Label lblMainscript = new Label();
-    private ProgressIndicator progressIndicator = new ProgressIndicator();
-    private EventHandler<MouseEvent> toolTipHandler = event -> {
-        publishMessage(((Control) event.getTarget()).getTooltip().getText());
-    };
-
     public IntegerProperty numberOfGoalsProperty() {
         return numberOfGoals;
     }
 
-    /*
-    private Appender createAppender() {
-        PatternLayout layout = PatternLayout.createDefaultLayout();
-        return new AbstractAppender("", null, layout) {
-            @Override
-            public void append(LogEvent event) {
-                publishMessage(event.getMessage().getFormattedMessage());
-            }
-        };
-    }*/
-
     public void publishMessage(String format, Object... args) {
         String msg = String.format(format, args);
         setText(msg);
@@ -114,25 +129,6 @@ public class DebuggerStatusBar extends StatusBar {
         return toolTipHandler;
     }
 
-    /*
-    public void listenOnField(ObservableStringValue value) {
-        value.addListener((observable, oldValue, newValue) -> {
-            publishMessage(newValue);
-        });
-    }*/
-
-    /*
-    public void listenOnField(Logger logger) {
-        org.apache.logging.log4j.core.Logger plogger = ((org.apache.logging.log4j.core.Logger) logger); // Bypassing the public API
-        plogger.addAppender(loggerHandler);
-        plogger.addAppender(logCatchHandler);
-        logger.info("Listener added");
-    }*/
-
-    /*public void listenOnField(String loggerCategory) {
-        listenOnField(LogManager.getLogger(loggerCategory));
-    }*/
-
     public void indicateProgress() {
         progressIndicator.setProgress(-1);
     }
@@ -141,15 +137,6 @@ public class DebuggerStatusBar extends StatusBar {
         progressIndicator.setProgress(100);
     }
 
-    /*public ContextMenu createContextMenu() {
-        ContextMenu cm = new ContextMenu();
-        Menu viewOptions = new Menu("View Options");
-        MenuItem showLog = new MenuItem("Show Log", new MaterialDesignIconView(MaterialDesignIcon.FORMAT_LIST_BULLETED));
-        showLog.setOnAction(this::showLog);
-        cm.getItems().addAll(viewOptions, showLog);
-        return cm;
-    }*/
-
     public MainScriptIdentifier getMainScriptIdentifier() {
         return mainScriptIdentifier.get();
     }
@@ -161,91 +148,33 @@ public class DebuggerStatusBar extends StatusBar {
     public ObjectProperty<MainScriptIdentifier> mainScriptIdentifierProperty() {
         return mainScriptIdentifier;
     }
-}
-
-    /*
-    private void showLog(ActionEvent actionEvent) {
-        loggerDialog.show();
-    }*/
 
-    /*public Dialog<Void> createDialog() {
-        final TableView<LogEvent> recordView = new TableView<>(logCatchHandler.recordsProperty());
-        recordView.setEditable(false);
-        recordView.setSortPolicy(param -> false);
-
-        TableColumn<LogEvent, Date> dateColumn = new TableColumn<>("Date");
-        TableColumn<LogEvent, Level> levelColumn = new TableColumn<>("Level");
-        //TableColumn<LogRecord, String> classColumn = new TableColumn<>("Class");
-        TableColumn<LogEvent, String> messageColumn = new TableColumn<>("Message");
-
-        recordView.getColumns().setAll(dateColumn, levelColumn, messageColumn);
-
-
-        dateColumn.setCellValueFactory(
-                param -> new SimpleObjectProperty<>(new Date(param.getValue().getTimeMillis())
-                ));
-
-        levelColumn.setCellValueFactory(
-                param -> new SimpleObjectProperty<>(param.getValue().getLevel())
-        );
-
-        messageColumn.setCellValueFactory(
-                param -> {
-                    return new SimpleStringProperty(param.getValue().getMessage().getFormattedMessage());
-}
-        );
-
-
-                Dialog<Void> dialog=new Dialog<>();
-        dialog.setResizable(true);
-        dialog.initModality(Modality.NONE);
-        dialog.setHeaderText("Logger Records");
-        DialogPane dpane=dialog.getDialogPane();
-        dpane.setContent(new BorderPane(recordView));
-        dpane.getButtonTypes().setAll(ButtonType.CLOSE);
-        return dialog;
-        }*/
-
-/*
-    public static class LogCatchHandlerFX extends AbstractAppender {
-        private ListProperty<LogEvent> records = new SimpleListProperty<>(FXCollections.observableList(
-                new LinkedList<>() //remove of head
-        ));
-
-        private int maxRecords = 5000;
-
-        protected LogCatchHandlerFX() {
-            super("LogCatchHandlerFX", null, PatternLayout.createDefaultLayout());
-        }
-
-        @Override
-        public void append(LogEvent event) {
-            records.add(event);
-            while (records.size() > maxRecords)
-                records.remove(0);
-        }
-
-
-        public ObservableList<LogEvent> getRecords() {
-            return records.get();
-        }
-
-        public void setRecords(ObservableList<LogEvent> records) {
-            this.records.set(records);
-        }
-
-        public ListProperty<LogEvent> recordsProperty() {
-            return records;
-        }
+    public InterpreterThreadState getInterpreterStatusModel() {
+        return interpreterStatusModel.get();
+    }
 
-        public int getMaxRecords() {
-            return maxRecords;
-        }
+    public void setInterpreterStatusModel(InterpreterThreadState interpreterStatusModel) {
+        this.interpreterStatusModel.set(interpreterStatusModel);
+    }
 
-        public void setMaxRecords(int maxRecords) {
-            this.maxRecords = maxRecords;
-        }
+    public ObjectProperty<InterpreterThreadState> interpreterStatusModelProperty() {
+        return interpreterStatusModel;
     }
-    }*/
 
+    public void publishErrorMessage(String message) {
+        publishMessage(message);
+        final Animation animation = new Transition() {