Merge branch 'master' into derivableBugFix

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

@@ -14,6 +14,7 @@ import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
 import edu.kit.iti.formal.psdbg.interpreter.data.State;
 import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
 import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
+import javafx.scene.control.Alert;
 import lombok.Getter;
 import lombok.RequiredArgsConstructor;
 import org.apache.commons.io.IOUtils;
@@ -22,6 +23,8 @@ import org.apache.logging.log4j.Logger;
 import org.key_project.util.collection.ImmutableList;
 
 import java.io.IOException;
+import java.io.PrintWriter;
+import java.io.StringWriter;
 import java.lang.reflect.Method;
 import java.net.URISyntaxException;
 import java.net.URL;
@@ -62,7 +65,26 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
                          VariableAssignment params, KeyData data) {
         ProofScriptCommand c = commands.get(call.getCommand());
         State<KeyData> state = interpreter.getCurrentState();
+
+        //multiple goals exist
+        if(state.getGoals().size() > 1) {
+            throw new IllegalStateException("Multiple open goals: Please use a selector.");
+            /*
+            //TODO: Utils showWarning
+            Alert alert = new Alert(Alert.AlertType.WARNING);
+            alert.setTitle("Multiple open Goals");
+            alert.setHeaderText("Multiple open Goals");
+            alert.setContentText("There are multiple open goals so its undefined on which goal the command " + call.getCommand() +" should be applied. Please use a selector.");
+            alert.setWidth(400);
+            alert.setHeight(400);
+            alert.setHeight(600);
+            alert.setWidth(400);
+
+            alert.showAndWait();
+*/
+        }
         GoalNode<KeyData> expandedNode = state.getSelectedGoalNode();
+
         KeyData kd = expandedNode.getData();
         Map<String, Object> map = new HashMap<>();
         params.asMap().forEach((k, v) -> {

ui/src/main/java/edu/kit/iti/formal/psdbg/examples/Example.java

@@ -4,6 +4,7 @@ import edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain;
 import edu.kit.iti.formal.psdbg.gui.model.MainScriptIdentifier;
 import lombok.*;
 import org.apache.commons.io.FileUtils;
+import org.apache.commons.io.FilenameUtils;
 import org.apache.commons.io.IOUtils;
 
 import java.io.File;
@@ -24,7 +25,12 @@ public abstract class Example {
     protected MainScriptIdentifier mainScriptIdentifier;
 
     public static File newTempFile(URL url, String filename) throws IOException {
-        File f = new File(FileUtils.getTempDirectoryPath(), filename);
+
+
+        File psdbg = new File(FileUtils.getTempDirectoryPath(), "psdbg");
+        File examplefolder = new File(psdbg.getPath(), FilenameUtils.removeExtension(filename));
+
+        File f = new File(examplefolder, filename);
         FileUtils.copyURLToFile(url, f);
         return f;
     }

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

@@ -807,6 +807,7 @@ public class DebuggerMain implements Initializable {
         if (javaFile != null) {
             model.setJavaFile(javaFile);
             model.setInitialDirectory(javaFile.getParentFile());
+            contractLoaderService.reset();
             contractLoaderService.start();
         }
     }
@@ -1166,7 +1167,6 @@ public class DebuggerMain implements Initializable {
         } else {
             throw new RuntimeException("Something went wrong when reloading");
         }
-
     }
 
   /*  public void handle(Events.TacletApplicationEvent tap){
@@ -1408,7 +1408,31 @@ public class DebuggerMain implements Initializable {
         protected void succeeded() {
             statusBar.publishMessage("Contract loaded");
             List<Contract> contracts = getValue();
-            ContractChooser cc = new ContractChooser(FACADE.getService(), contracts);
+
+            /*
+            String javaFile = model.getJavaFile().getName();
+
+            List<Contract> filteredContracts = new ArrayList<>();
+            for (Contract contract : contracts) {
+                String contractFile = contract.getKJT().getFullName();
+                if (javaFile == contractFile) {
+                    filteredContracts.add(contract);
+                }
+            }
+
+            if (filteredContracts.size() == 0) {
+               Utils.showInfoDialog("No loadable contract", "No loadable contract",
+                       "There's no loadable contract for the chosen java file.");
+                return;
+            }
+            */
+
+            ContractChooser cc = null;
+            try {
+                cc = new ContractChooser(FACADE.getService(), FACADE.getContractsForJavaFile(model.getJavaFile()));
+            } catch (ProblemLoaderException e) {
+                e.printStackTrace();
+            }
 
             cc.showAndWait().ifPresent(result -> {
                 model.setChosenContract(result);

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

 package edu.kit.iti.formal.psdbg.gui.controller;
 
 import com.google.common.eventbus.Subscribe;
+import de.uka.ilkd.key.api.KeYApi;
 import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
 import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.Sequent;
 import de.uka.ilkd.key.logic.SequentFormula;
-import de.uka.ilkd.key.macros.ProofMacro;
 import de.uka.ilkd.key.macros.scripts.*;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Node;
@@ -26,7 +26,7 @@ import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
 import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerFramework;
 import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
 import edu.kit.iti.formal.psdbg.interpreter.exceptions.ScriptCommandNotApplicableException;
-import edu.kit.iti.formal.psdbg.interpreter.funchdl.MacroCommandHandler;
+import edu.kit.iti.formal.psdbg.interpreter.funchdl.ProofScriptCommandBuilder;
 import edu.kit.iti.formal.psdbg.parser.PrettyPrinter;
 import edu.kit.iti.formal.psdbg.parser.ast.*;
 import edu.kit.iti.formal.psdbg.parser.data.Value;
@@ -43,6 +43,7 @@ import org.key_project.util.collection.ImmutableList;
 import recoder.util.Debug;
 
 import javax.annotation.Nullable;
+import java.lang.reflect.Method;
 import java.math.BigInteger;
 import java.util.*;
 import java.util.stream.Collectors;
@@ -66,8 +67,8 @@ public class InteractiveModeController {
     private PTreeNode<KeyData> nodeAtInteractionStart;
 
     //needed for Undo-Operation
-    private ArrayList<CallStatement> savepointsstatement;
-    private ArrayList<Node> savepointslist;
+    private ArrayList<CallStatement> laststatementlist;
+    private ArrayList<Node> lastnodeslist;
 
     private Proof currentProof;
     private Services keYServices;
@@ -99,8 +100,8 @@ public class InteractiveModeController {
             gcs.setBody(v);
             casesStatement.getCases().add(gcs);
         });
-        savepointslist = new ArrayList<>();
-        savepointsstatement = new ArrayList<>();
+        lastnodeslist = new ArrayList<>();
+        laststatementlist = new ArrayList<>();
         nodeAtInteractionStart = debuggerFramework.getStatePointer();
 
     }
@@ -110,13 +111,14 @@ public class InteractiveModeController {
      * Undo the application of the last rule
      */
     public void undo(javafx.event.ActionEvent actionEvent) {
-        if (savepointslist.isEmpty()) {
+        if (lastnodeslist.isEmpty()) {
             Debug.log("Kein vorheriger Zustand.");
             return;
         }
 
-        val pruneNode = savepointslist.get(savepointslist.size() - 1);
-        savepointslist.remove(pruneNode);
+        val pruneNode = lastnodeslist.get(lastnodeslist.size() - 1);
+        lastnodeslist.remove(pruneNode);
+
         ImmutableList<Goal> goalsbeforePrune = currentProof.getSubtreeGoals(pruneNode);
 
         currentProof.pruneProof(pruneNode);
@@ -127,19 +129,55 @@ public class InteractiveModeController {
                 .filter(keyDataGoalNode -> goalsbeforePrune.contains(keyDataGoalNode.getData().getGoal()))
                 .collect(Collectors.toList());
 
+        if(prunedChildren.size() == 0) {
+            //TODO: add Utils.showInfoD
+            return;
+        }
         KeyData kd = prunedChildren.get(0).getData();
         goals.removeAll(prunedChildren);
+
+
+        //Set selected goal after prune
+
         GoalNode<KeyData> lastGoalNode = null;
-        for (Goal newGoalNode : goalsafterPrune) {
-            KeyData kdn = new KeyData(kd, newGoalNode.node());
+        KeyData kdn;
+        if (lastnodeslist.size() == 0) {
+            kdn = new KeyData(kd, goalsafterPrune.get(0).node());
             goals.add(
-                    lastGoalNode = new GoalNode<>(prunedChildren.get(0).getParent().getParent(), kdn, kdn.getNode().isClosed()));
+                    lastGoalNode = new GoalNode<>(prunedChildren.get(0).getParent(), kdn, kdn.getNode().isClosed()));
+        } else {
+            for (Goal newGoalNode : goalsafterPrune) {
+                kdn = new KeyData(kd, newGoalNode.node());
+                goals.add(
+                        lastGoalNode = new GoalNode<>(prunedChildren.get(0).getParent().getParent(), kdn, kdn.getNode().isClosed()));
+            }
         }
 
         model.setSelectedGoalNodeToShow(lastGoalNode);
 
-        val pruneStatement = savepointsstatement.get(savepointsstatement.size() - 1);
-        cases.forEach((k, v) -> v.remove(pruneStatement));
+
+        val pruneStatement = laststatementlist.get(laststatementlist.size() - 1);
+        laststatementlist.remove(laststatementlist.size() - 1);
+
+        //TODO: buggy cuz allstatements of same node removed
+
+        //remove statement from cases / script
+        Statements statements = (cases.get(pruneNode.parent()) == null)? cases.get(pruneNode) : cases.get(pruneNode.parent());
+        int i = statements.size()-1;
+
+        while(statements.get(i) != pruneStatement && i >= 0) {
+            statements.remove(i);
+            i--;
+        }
+        statements.remove(i);
+
+
+        /*
+        cases.forEach((k, v) -> {
+                v.remove(pruneStatement);
+
+        });
+        */
 
         String c = getCasesAsString();
         scriptArea.setText("" +
@@ -260,11 +298,39 @@ public class InteractiveModeController {
         }
     }
 
+    @Subscribe
+    public void handle(Events.CommandApplicationEvent map) {
+
+        LOGGER.debug("Handling {}", map);
+        Goal g = map.getCurrentGoal();
+
+        Parameters callp = new Parameters();
+        CallStatement call = new CallStatement(map.getCommandName().getName(), callp);
+        try {
+            applyRuleHelper(call, g, Type.SCRIPT_COMMAND);
+            String c = getCasesAsString();
+            scriptArea.setText("" +
+                    "//Preview \n" + c);
+
+
+        } catch (ScriptCommandNotApplicableException e) {
+            StringBuilder sb = new StringBuilder("The script command ");
+            sb.append(call.getCommand()).append(" was not applicable.");
+            System.out.println("e = " + e);
+            //sb.append("\nSequent Formula: formula=").append(sfTerm);
+            //sb.append("\nOn Sub Term: on=").append(onTerm);
+
+            Utils.showWarningDialog("Proof Command was not applicable",
+                    "Proof Command was not applicable.",
+                    sb.toString(), e);
+        }
+    }
+
 
     private void applyRuleHelper(CallStatement call, Goal g, Type t) throws ScriptCommandNotApplicableException {
 
-        savepointslist.add(g.node());
-        savepointsstatement.add(call);
+        lastnodeslist.add(g.node());
+        laststatementlist.add(call);
 
         ObservableList<GoalNode<KeyData>> goals = model.getGoals();
         GoalNode<KeyData> expandedNode;
@@ -312,10 +378,11 @@ public class InteractiveModeController {
                     postStateHandler(call, g, goals, expandedNode, kd);
                     break;
                 case SCRIPT_COMMAND:
-                    ScriptCommand.Parameters ccS = new ScriptCommand.Parameters();
-                    ScriptCommand cS = new ScriptCommand();
-                    ccS = valueInjector.inject(cS, ccS, map);
-                    cS.execute(uiControl, ccS, estate);
+                    ProofScriptCommandBuilder psb = new ProofScriptCommandBuilder(KeYApi.getScriptCommandApi().getScriptCommands());
+                    ProofScriptCommand ps = psb.getCommands().get(call.getCommand());
+
+                    Object temp = valueInjector.inject(ps, getParameterInstance(ps), map);
+                    ps.execute(uiControl, temp, estate);
                     postStateHandler(call, g, goals, expandedNode, kd);
                     break;
                 default:
@@ -335,6 +402,12 @@ public class InteractiveModeController {
 
     }
 
+    private <T> T getParameterInstance(ProofScriptCommand c) throws NoSuchMethodException, IllegalAccessException,
+            InstantiationException {
+        Method method = c.getClass().getMethod("evaluateArguments", EngineState.class, Map.class);
+        Class rtclazz = method.getReturnType();
+        return (T) rtclazz.newInstance();
+    }
     private void postStateHandler(CallStatement call, Goal g, ObservableList<GoalNode<KeyData>> goals, GoalNode<KeyData> expandedNode, KeyData kd) {
         ImmutableList<Goal> ngoals = g.proof().getSubtreeGoals(expandedNode.getData().getNode());
 
@@ -391,8 +464,8 @@ public class InteractiveModeController {
     }
 /*
     private void applyRule(CallStatement call, Goal g) throws ScriptCommandNotApplicableException {
-        savepointslist.add(g.node());
-        savepointsstatement.add(call);
+        lastnodeslist.add(g.node());
+        laststatementlist.add(call);
 
         ObservableList<GoalNode<KeyData>> goals = model.getGoals();
         GoalNode<KeyData> expandedNode;

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

@@ -66,9 +66,8 @@ public class ScriptExecutionController {
                 mainCtrl.FACADE.reload(mainCtrl.getModel().getKeyFile());
             } catch (ProofInputException | ProblemLoaderException e) {
                 LOGGER.error(e);
-                Utils.showExceptionDialog("Loading Error", "Could not clear Environment", "There was an error when clearing old environment",
-                        e
-                );
+
+                // Utils.showExceptionDialog("Loading Error", "Could not clear Environment", "There was an error when clearing old environment", e  );
             }
         }
 

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

@@ -10,8 +10,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;
@@ -89,7 +91,6 @@ import static org.fxmisc.wellbehaved.event.InputMap.*;
 public class ScriptArea extends BorderPane {
     public static final Logger LOGGER = LogManager.getLogger(ScriptArea.class);
     public static final Logger CONSOLE_LOGGER = LogManager.getLogger(ScriptArea.class);
-
     public static final String EXECUTION_MARKER = "\u2316";
 
     public static final FileReloadingService FILE_RELOADING_SERVICE = new FileReloadingService();
@@ -489,10 +490,12 @@ public class ScriptArea extends BorderPane {
     }
 
 
+    @Deprecated
     private boolean hasExecutionMarker() {
         return getText().contains(EXECUTION_MARKER);
     }
 
+    @Deprecated
     public int getExecutionMarkerPosition() {
         return getText().lastIndexOf(EXECUTION_MARKER);
     }
@@ -608,11 +611,13 @@ public class ScriptArea extends BorderPane {
         return dirty;
     }
 
+    @Deprecated
     public void removeExecutionMarker() {
         setText(getTextWithoutMarker());
         //Events.unregister(this);
     }
 
+    @Deprecated
     private String getTextWithoutMarker() {
         return getText().replace("" + EXECUTION_MARKER, "");
     }
@@ -622,6 +627,7 @@ public class ScriptArea extends BorderPane {
      *
      * @param pos
      */
+    @Deprecated
     public void insertExecutionMarker(int pos) {
         LOGGER.debug("ScriptArea.insertExecutionMarker");
         Events.register(this);
@@ -992,6 +998,7 @@ public class ScriptArea extends BorderPane {
             }*/
         }
 
+        @Deprecated
         public void setExecutionMarker(ActionEvent event) {
             LOGGER.debug("ScriptAreaContextMenu.setExecutionMarker");
             int pos = codeArea.getCaretPosition();

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps

+script empty(){
+
+}
+
 script full(){
   impRight;
   impRight;

ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/ScriptAreaContextMenu.fxml

@@ -10,7 +10,8 @@
     <MenuItem text="Show post mortem" onAction="#showPostMortem"/>
     <SeparatorMenuItem/>
     <MenuItem text="Set Main Script" onAction="#setMainScript"/>
-    <MenuItem text="Set Execution Marker" onAction="#setExecutionMarker" accelerator="Ctrl+m"/>
+    <!--<MenuItem text="Set Execution Marker" onAction="#setExecutionMarker" accelerator="Ctrl+m"/>
+    -->
 </items>
 
 </fx:root>