Merge branch 'luong_workbranch' into 'master'

Luong workbranch

See merge request !20

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

@@ -14,7 +14,7 @@ public class ASTDiff extends DefaultASTVisitor<ASTNode> {
         newScript.setSignature(proofScript.getSignature());
 
         other = ((ProofScript) other).getBody();
-        newScript.setBody(visit(newScript.getBody()));
+        newScript.setBody(visit(proofScript.getBody()));
         return newScript;
     }
 
@@ -61,12 +61,13 @@ public class ASTDiff extends DefaultASTVisitor<ASTNode> {
 
         int i = 0;
         for (; i < statements.size(); i++) {
-            if (statements.get(i).eq(other.get(i))) {
-                break;
+            if (!statements.get(i).isSame(other.get(i))) {
+                System.out.println("Alter Script wurde verändert");
+                return null;
             }
         }
 
-        for (int j = i; j < other.size(); j++) {
+        for (; i < other.size(); i++) {
             s.add(other.get(i));
         }
 

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

@@ -167,6 +167,11 @@ public abstract class ASTNode<T extends ParserRuleContext>
         return Objects.hash(getRuleContext());
     }
 
+    //TODO: param + class
+    public boolean isSame(ASTNode other) {
+        return this.getNodeName().equals(other.getNodeName());
+    }
+
     public int getSyntaxWidth() {
         if (ruleContext != null) {
             return ruleContext.stop.getStopIndex()

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

@@ -225,9 +225,10 @@ public class InterpreterBuilder {
 
     public InterpreterBuilder setProblemPath(File path){
         Map<String, CommandHandler<KeyData>> builtinsnew = this.bich.getBuiltins();
-        SaveCommand sc = new SaveCommand(path);
-        builtinsnew.put(SaveCommand.SAVE_COMMAND_NAME, sc);
+
+        builtinsnew.put(SaveCommand.SAVE_COMMAND_NAME, new SaveCommand(path));
         this.bich.setBuiltins(builtinsnew);
+
         return this;
 
     }

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

@@ -63,7 +63,8 @@ public class SaveCommand implements CommandHandler<KeyData> {
                 Semaphore semaphore = new Semaphore(0);
                 Platform.runLater(() -> {
                     Alert a = new Alert(Alert.AlertType.CONFIRMATION);
-                    a.setTitle("Foo");
+                    a.setTitle("Overwrite proof file");
+                    a.setContentText("Overwrite existing proof file \"" + sp.getName()+"\" (line "+ sp.getLineNumber() +") ?");
                     Optional<ButtonType> buttonType = a.showAndWait();
                     if(buttonType.isPresent() && buttonType.get() == ButtonType.OK){
                         execute.set(true);
@@ -86,10 +87,7 @@ public class SaveCommand implements CommandHandler<KeyData> {
     }
 
 
-    @Override
-    public boolean isUninterpretedParams(CallStatement call) {
-        return true;
-    }
+
 }
 
 

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

@@ -599,7 +599,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
 
     private VariableAssignment evaluateParametersStateLess(Parameters parameters) {
         VariableAssignment va = new VariableAssignment();
-        Evaluator<T> evaluator = createEvaluator(null, null);
+        Evaluator<T> evaluator = new Evaluator<>(null, null);
 
         parameters.entrySet().forEach(entry -> {
             try {

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

@@ -2,6 +2,7 @@ package edu.kit.iti.formal.psdbg.gui.controller;
 
 import alice.tuprolog.InvalidLibraryException;
 import alice.tuprolog.InvalidTheoryException;
+import antlr.collections.AST;
 import com.google.common.eventbus.Subscribe;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
@@ -25,6 +26,7 @@ import edu.kit.iti.formal.psdbg.gui.graph.GraphView;
 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.gui.model.MainScriptIdentifier;
 import edu.kit.iti.formal.psdbg.interpreter.InterpreterBuilder;
 import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
 import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
@@ -33,7 +35,12 @@ import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
 import edu.kit.iti.formal.psdbg.interpreter.data.SavePoint;
 import edu.kit.iti.formal.psdbg.interpreter.data.State;
 import edu.kit.iti.formal.psdbg.interpreter.dbg.*;
+import edu.kit.iti.formal.psdbg.parser.ASTDiff;
+import edu.kit.iti.formal.psdbg.parser.Facade;
+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.ProofScript;
+import edu.kit.iti.formal.psdbg.storage.KeyPersistentFacade;
 import javafx.application.Platform;
 import javafx.beans.InvalidationListener;
 import javafx.beans.binding.BooleanBinding;
@@ -54,6 +61,7 @@ import javafx.stage.FileChooser;
 import javafx.stage.Modality;
 import lombok.Getter;
 import lombok.RequiredArgsConstructor;
+import lombok.val;
 import org.apache.commons.io.FileUtils;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
@@ -66,13 +74,16 @@ import org.reactfx.util.Timer;
 
 import javax.annotation.Nullable;
 import javax.swing.*;
+import javax.xml.bind.JAXBException;
+import java.awt.event.WindowAdapter;
+import java.awt.event.WindowEvent;
+import java.awt.event.WindowListener;
+import java.awt.event.WindowStateListener;
 import java.awt.im.InputContext;
-import java.io.File;
-import java.io.FileWriter;
-import java.io.IOException;
-import java.io.PrintWriter;
+import java.io.*;
 import java.net.URL;
 import java.nio.charset.Charset;
+import java.security.Permission;
 import java.time.Duration;
 import java.util.*;
 import java.util.concurrent.*;
@@ -833,6 +844,9 @@ public class DebuggerMain implements Initializable {
     @FXML
     public void executeDiff() {
         //save old PT
+
+
+
         // Calculate top difference between current and last executed script
         // Find last state of common ASTNode
         // Use this state to build new interpreter in proof tree controller.
@@ -841,6 +855,36 @@ public class DebuggerMain implements Initializable {
 
     }
 
+
+
+
+    @Deprecated
+    public  void incremental() {
+        ProofScript oldScript = null; //used to be global var, that was set in selectSavepoint()
+
+        if (oldScript == null) {
+            return;
+        }
+        ProofScript newScript = scriptController.getMainScript().byName(scriptController.getCombinedAST()).get();
+
+        ASTDiff astDiff = new ASTDiff();
+        ProofScript scriptdiff = astDiff.diff(oldScript, newScript);
+        ASTNode pruneAstNode = scriptdiff.getBody().get(0);
+
+        Set<PTreeNode<KeyData>> ptnodes = model.getDebuggerFramework().getPtreeManager().getNodes();
+        Iterator iterator = ptnodes.iterator();
+        while (iterator.hasNext()) {
+            PTreeNode<KeyData> ptn = (PTreeNode<KeyData>) iterator.next();
+            if(ptn.getStatement().eq(pruneAstNode)) {
+                getFacade().getProof().pruneProof(ptn.getStateBeforeStmt().getSelectedGoalNode().getData().getNode());
+                break;
+            }
+        }
+
+
+        scriptController.setMainScript(oldScript);
+    }
+
     /**
      * Continue after the interpreter has reached a breakpoint
      *
@@ -932,12 +976,12 @@ public class DebuggerMain implements Initializable {
 
     @FXML
     public void saveAsScript() throws IOException {
-        File f = openFileChooserSaveDialog("Save script", "Save Script files", "kps");
-        if (f != null) {
-           /* if(!f.exists()){
-                f.createNewFile();
-            }*/
-            saveScript(f);
+        FileChooser fc = new FileChooser();
+        File file = fc.showSaveDialog(btnInteractiveMode.getScene().getWindow());
+        if (file != null) {
+                saveScript(file);
+        } else {
+            Utils.showInfoDialog("","Select a destination", "No valid path has been selected.");
         }
     }
 
@@ -1149,16 +1193,43 @@ public class DebuggerMain implements Initializable {
 
     @FXML
     public void selectSavepoint(ActionEvent actionEvent) {
-        if (cboSavePoints.getValue() != null) {
+        //TODO remove highlight of SPs
+
+        SavePoint selected = cboSavePoints.getValue();
+
+        if (selected == null) {
+            Utils.showInfoDialog("Select Savepoint", "Select Savepoint", "There is no selected Savepoint. Select a Savepoint first.");
+            return;
+        }
+
+        //prune to savepoint if possible
+        boolean pruneable = false;
+        try{
+            Iterator<PTreeNode<KeyData>> iterator = model.getDebuggerFramework().getPtreeManager().getNodes().iterator();
+            PTreeNode<KeyData> pTreeNodeOfSave;
+            while (iterator.hasNext()) {
+                pTreeNodeOfSave = iterator.next();
+
+                if (pTreeNodeOfSave.getStatement().getStartPosition().getLineNumber() == selected.getLineNumber()) {
+                    FACADE.getProof().pruneProof(pTreeNodeOfSave.getStateBeforeStmt().getSelectedGoalNode().getData().getNode());
+                    inspectionViewsController.getActiveInspectionViewTab().activate(pTreeNodeOfSave, pTreeNodeOfSave.getStateAfterStmt());
+                    break;
+                }
+            }
+
+            //TODO: refresh GUI (Context + Script)
+            //State<KeyData> proofstate = KeyPersistentFacade.read(FACADE.getEnvironment(), FACADE.getProof(), new StringReader());
+
+        } catch (Exception ex){
+
+            //Hard Loading of Savepoint
             stopDebugMode(actionEvent);
-            SavePoint selected = cboSavePoints.getValue();
 
             try {
                 abortExecution();
             } catch (Exception e) {
                 e.printStackTrace();
             }
-
             /**
              * reload with selected savepoint
              */
@@ -1166,6 +1237,7 @@ public class DebuggerMain implements Initializable {
             handleStatePointerUI(null);
             //reload getInspectionViewsController().getActiveInspectionViewTab().getModel()
             InspectionModel iModel = getInspectionViewsController().getActiveInspectionViewTab().getModel();
+
             //iModel.setHighlightedJavaLines(FXCollections.emptyObservableSet());
             iModel.clearHighlightLines();
             iModel.getGoals().clear();
@@ -1181,6 +1253,8 @@ public class DebuggerMain implements Initializable {
                     LOGGER.info("Reloaded Successfully");
                     statusBar.publishMessage("Reloaded Sucessfully");
                 }
+
+
             } catch (ProofInputException | ProblemLoaderException e) {
                 LOGGER.error(e);
                 Utils.showExceptionDialog("Loading Error", "Could not clear Environment",
@@ -1188,9 +1262,22 @@ public class DebuggerMain implements Initializable {
                         e
                 );
             }
+        }
 
-            // executeScriptFromSavePoint(interpreterBuilder, selected);
+        //Update Gui
+        MainScriptIdentifier msi = scriptController.getMainScript();
+        msi.getScriptArea().setSavepointMarker(selected.getLineNumber());
+        scriptController.getMainScript().getScriptArea().underlineSavepoint(selected);
+
+
+        try {
+            KeyPersistentFacade.read(FACADE.getEnvironment(), FACADE.getProof(), new StringReader(selected.getPersistedStateFile(FACADE.getFilepath()).toString()));
+        } catch (JAXBException e) {
+            e.printStackTrace();
         }
+        scriptExecutionController.executeScriptFromSavePoint(interpreterBuilder, selected);
+
+
 
     }
 
@@ -1279,22 +1366,34 @@ public class DebuggerMain implements Initializable {
 
     public void openInKey(@Nullable ActionEvent event) {
         if (FACADE.getProofState() == KeYProofFacade.ProofState.EMPTY) {
-            Alert alert = new Alert(Alert.AlertType.INFORMATION, "No proof is loaded yet. If laoding a proof was invoked, proof state loading may take a while.", ButtonType.OK);
+            Alert alert = new Alert(Alert.AlertType.INFORMATION, "No proof is loaded yet. If loading a proof was invoked, proof state loading may take a while.", ButtonType.OK);
             alert.show();
             return;
         }
 
         SwingUtilities.invokeLater(() -> {
+            SecurityManager secManager = new KeYSecurityManager();
+            System.setSecurityManager(secManager);
+
             // Swing Thread!
-            MainWindow keyWindow = MainWindow.getInstance();
-            keyWindow.addProblem(new SingleProof(FACADE.getProof(), "script"));
-            //keyWindow.getProofList().getModel().addProof();
-            keyWindow.makePrettyView();
-            keyWindow.setVisible(true);
+            try {
+                MainWindow keyWindow = MainWindow.getInstance();
+                keyWindow.addProblem(new SingleProof(FACADE.getProof(), "script"));
+                //keyWindow.getProofList().getModel().addProof();
+                keyWindow.makePrettyView();
+                keyWindow.setVisible(true);
+            } catch (SecurityException e) {
+                e.printStackTrace();
+            }
+
+
+
         });
+
     }
 
 
+
     public class ContractLoaderService extends Service<List<Contract>> {
         @Override
         protected void succeeded() {
@@ -1441,6 +1540,17 @@ public class DebuggerMain implements Initializable {
         }
     }
 
+
+    private class KeYSecurityManager extends SecurityManager {
+        @Override public void checkExit(int status) {
+            throw new SecurityException();
+        }
+
+        @Override public void checkPermission(Permission perm) {
+            // Allow other activities by default
+        }
+    }
+
     //endregion
 }
 //deprecated

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

@@ -110,7 +110,7 @@ public class InteractiveModeController {
      */
     public void undo(javafx.event.ActionEvent actionEvent) {
         if (savepointslist.isEmpty()) {
-            Debug.log("Kein vorheriger Zustand."); //TODO: events fire
+            Debug.log("Kein vorheriger Zustand.");
             return;
         }
 

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

@@ -8,7 +8,9 @@ import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
 import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
 import edu.kit.iti.formal.psdbg.interpreter.data.SavePoint;
 import edu.kit.iti.formal.psdbg.interpreter.dbg.Breakpoint;
+import edu.kit.iti.formal.psdbg.parser.ASTDiff;
 import edu.kit.iti.formal.psdbg.parser.Facade;
+import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
 import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
 import edu.kit.iti.formal.psdbg.parser.ast.Statements;
 import javafx.scene.control.Alert;
@@ -160,5 +162,10 @@ public class ScriptExecutionController {
     }
 
 
+    private ASTNode calculateDiff (ASTDiff dff) {
+
+        return null;
+    }
+
 
 }

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

@@ -29,11 +29,9 @@ import javafx.scene.control.cell.TextFieldTreeCell;
 import javafx.scene.layout.BorderPane;
 import javafx.util.StringConverter;
 import lombok.*;
+import sun.reflect.generics.tree.Tree;
 
-import java.util.HashMap;
-import java.util.Iterator;
-import java.util.Map;
-import java.util.Set;
+import java.util.*;
 import java.util.function.Consumer;
 
 
@@ -327,12 +325,14 @@ public class ProofTree extends BorderPane {
     }
 
 
+
     @AllArgsConstructor
     private static class TreeNode {
         String label;
         Node node;
     }
 
+
     class TreeTransformationKey {
 
         public TreeItem<TreeNode> create(Proof proof) {
@@ -414,6 +414,7 @@ public class ProofTree extends BorderPane {
     }
 
 
+
     @RequiredArgsConstructor
     class TreeTransformationScript extends TreeTransformationKey {
         final ProofTreeManager<KeyData> manager;
@@ -472,5 +473,44 @@ public class ProofTree extends BorderPane {
             TreeItem<TreeNode> ti = new TreeItem<>(new TreeNode(lbl, n));
             return ti;
         }
+
+
+        //TODO: Reverse ArrayList in the end or nah?
+        @Deprecated
+        public ArrayList<String> getBranchLabels (TreeNode node) {
+            TreeItem<TreeNode> proofTree = create(proof.get());
+
+            ArrayList<String> branchlabels = new ArrayList<>();
+
+            int i = 0;
+            branchlabels.set(0, node.label);
+            while (node != null) {
+                if(!branchlabels.get(i).equals(node.label)) {
+                    i++;
+                    branchlabels.set(i, node.label);
+                }
+                //TODO: node = node.parent
+            }
+
+            return branchlabels;
+        }
+
+        public  ArrayList<String> getBranchLabels (Node node) {
+            ArrayList<String> branchlabels = new ArrayList<>();
+
+            int i = 0;
+            //TODO: branchlabel = all branchlabels or only next one
+            branchlabels.set(0, node.getNodeInfo().getBranchLabel());
+            Node n = node.parent();
+            while (n != null) {
+                if(!branchlabels.get(i).equals(n.getNodeInfo().getBranchLabel())) {
+                    i++;
+                    branchlabels.set(i, n.getNodeInfo().getBranchLabel());
+                }
+                n = n.parent();
+            }
+
+            return branchlabels;
+        }
     }
 }

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

@@ -9,7 +9,10 @@ import edu.kit.iti.formal.psdbg.gui.actions.acomplete.Suggestion;
 import edu.kit.iti.formal.psdbg.gui.actions.inline.InlineActionSupplier;
 import edu.kit.iti.formal.psdbg.gui.controller.Events;
 import edu.kit.iti.formal.psdbg.gui.model.MainScriptIdentifier;
+import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
+import edu.kit.iti.formal.psdbg.interpreter.data.SavePoint;
 import edu.kit.iti.formal.psdbg.interpreter.dbg.Breakpoint;
+import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
 import edu.kit.iti.formal.psdbg.lint.LintProblem;
 import edu.kit.iti.formal.psdbg.lint.LinterStrategy;
 import edu.kit.iti.formal.psdbg.parser.Facade;
@@ -388,6 +391,10 @@ public class ScriptArea extends BorderPane {
         }
     }
 
+    public void underlineSavepoint(SavePoint sp){
+        codeArea.setStyle(sp.getLineNumber() -1, Collections.singleton("underlinesave"));
+    }
+
     private void highlightNonExecutionArea() {
         if (hasExecutionMarker()) {
             LOGGER.debug("getExecutionMarkerPosition() = " + getExecutionMarkerPosition());
@@ -455,11 +462,12 @@ public class ScriptArea extends BorderPane {
 
     }
 
-    private void underline(int linenumber) {
-
+    public void setAlertMarker(int lineNumber) {
+        gutter.getLineAnnotation(lineNumber - 1).setAlert(true);
     }
 
 
+
     private boolean hasExecutionMarker() {
         return getText().contains(EXECUTION_MARKER);
     }
@@ -646,6 +654,10 @@ public class ScriptArea extends BorderPane {
                 MaterialDesignIcon.CONTENT_SAVE, "12"
         );
 
+        private MaterialDesignIconView iconSkippedSave = new MaterialDesignIconView(
+                MaterialDesignIcon.ALERT, "12"
+        );
+
         private Label lineNumber = new Label("not set");
 
         public GutterView(GutterAnnotation ga) {
@@ -676,6 +688,8 @@ public class ScriptArea extends BorderPane {
             if (getAnnotation().isMainScript()) getChildren().add(iconMainScript);
             else if (getAnnotation().isSavepoint()) getChildren().add(iconSavepoint);
             else addPlaceholder();
+            if (getAnnotation().isAlert()) getChildren().add(iconSkippedSave);
+            else addPlaceholder();
             if (getAnnotation().isBreakpoint())
                 getChildren().add(getAnnotation().getConditional()
                         ? iconConditionalBreakPoint
@@ -717,6 +731,21 @@ public class ScriptArea extends BorderPane {
 
         private SimpleBooleanProperty savepoint = new SimpleBooleanProperty();
 
+        //for now specifically for skipped saved commands
+        private SimpleBooleanProperty alert = new SimpleBooleanProperty();
+
+        public boolean isAlert() {
+            return alert.get();
+        }
+
+        public SimpleBooleanProperty alertProperty() {
+            return alert;
+        }
+
+        public void setAlert(boolean alert) {
+            this.alert.set(alert);
+        }
+
         public String getText() {
             return text.get();
         }

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

@@ -88,6 +88,8 @@ public class ScriptController {
             if (o != null)
                 o.getScriptArea().textProperty().removeListener(a -> updateSavePoints());
             n.getScriptArea().textProperty().addListener(a -> updateSavePoints());
+
+
             updateSavePoints();
         });
 
@@ -95,48 +97,30 @@ public class ScriptController {
     }
 
     private void updateSavePoints() {
-        try{
-        Optional<ProofScript> ms = getMainScript().find(getCombinedAST());
-        if (ms.isPresent()) {
-            List<SavePoint> list = ms.get().getBody().stream()
-                    .filter(SavePoint::isSaveCommand)
-                    .map(a -> (CallStatement) a)
-                    .map(SavePoint::new)
-                    .collect(Collectors.toList());
-            mainScriptSavePoints.setAll(list);
-           // loggerConsole.info("Found savepoints: " + list);
-        }}catch (Exception e){}
-
-    }
-
-/*
-    public int getLineOfSavepoint(SavePoint sp) {
-        Optional<ProofScript> ms = getMainScript(). find(getCombinedAST());
-
-        if(ms.isPresent()) {
-            List<CallStatement> list = ms.get().getBody().stream()
-                    .filter(SavePoint::isSaveCommand)
-                    .map(a -> (CallStatement) a).
-                    collect(Collectors.toList());
-
-
-            if(!list.isEmpty()) {
-               for(int i = 0; i < list.size(); i++) {
-                   if(true) {