Merge branch 'master' into 'gradle'

Recent changes into new build infrastructure

See merge request !10

keydeps/README.user

@@ -4,9 +4,9 @@
 # Execute this in this folder.
 
 # Set to key/key/deployment/components/
-#COMPONENTS=${COMPONENTS:-/home/sarah/Documents/KIT_Mitarbeiter/KeYDevelopment/KeYGitDir/key/key/deployment/components/}
+COMPONENTS=${COMPONENTS:-/home/sarah/Documents/KIT_Mitarbeiter/KeYDevelopment/KeYGitDir/key/key/deployment/components/}
 #COMPONENTS=$HOME/work/key/key/deployment/components/
-COMPONENTS=lib/components/
+#COMPONENTS=lib/components/
 
 
 

lang/src/main/antlr/edu/kit/iti/formal/psdbg/parser/ScriptLanguage.g4

@@ -212,4 +212,4 @@ QUESTION_MARK: '?';
 
 DIGITS : DIGIT+ ;
 fragment DIGIT : [0-9] ;
-ID : ([a-zA-Z]|'#') ([_a-zA-Z0-9] | '.' | '\\'| '#')*;
\ No newline at end of file
+ID : ([a-zA-Z]|'#'|'_') ([_a-zA-Z0-9] | '.' | '\\'| '#')*;
\ No newline at end of file

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

@@ -197,7 +197,11 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
 
     @Override
     public Void visit(TermLiteral termLiteral) {
-        s.append(String.format("`%s`", termLiteral.getText()));
+        String termLit = termLiteral.getText();
+        if (termLit.contains("\n")) {
+            termLit = termLit.trim();
+        }
+        s.append(String.format("`%s`", termLit));
         return super.visit(termLiteral);
     }
 

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

@@ -39,7 +39,7 @@ import lombok.Setter;
 @RequiredArgsConstructor
 @AllArgsConstructor
 public abstract class CaseStatement extends Statement<ScriptLanguageParser.CasesListContext> {
-    protected Statements body;
+    protected Statements body = new Statements();
 
     /**
      * {@inheritDoc}

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

@@ -102,7 +102,7 @@ public class KeYMatcher implements MatcherApi<KeyData> {
      * Match the label of a goal node
      *
      * @param currentState goal node as possible match cancidate
-     * @param label        String representation for regualr expression for label to match
+     * @param label        String representation for regular expression for label to match
      * @return List of matches if match was sucessful, empty list otherwise
      */
     @Override
@@ -111,10 +111,17 @@ public class KeYMatcher implements MatcherApi<KeyData> {
         List<VariableAssignment> assignments = new ArrayList<>();
         resultsFromLabelMatch = new ArrayList<>();
         //compile pattern
-        Pattern regexpForLabel = Pattern.compile(label);
+        String cleanLabel = label.replaceAll(" ", "");
+        String cleanLabel2 = cleanLabel.replaceAll("\\(", "\\\\(");
+        cleanLabel = cleanLabel2.replaceAll("\\)", "\\\\)");
+
 
         String branchLabel = currentState.getData().getBranchingLabel();
-        Matcher branchLabelMatcher = regexpForLabel.matcher(branchLabel);
+        String cleanBranchLabel = branchLabel.replaceAll(" ", "");
+
+        Pattern regexpForLabel = Pattern.compile(cleanLabel);
+        Matcher branchLabelMatcher = regexpForLabel.matcher(cleanBranchLabel);
+
 
 
         if (branchLabelMatcher.matches()) {
@@ -160,16 +167,6 @@ public class KeYMatcher implements MatcherApi<KeyData> {
         return assignments.isEmpty()? null: assignments;
     }
 
-    private Value<String> toValueTerm(KeyData currentState, Term matched) {
-        String reprTerm = LogicPrinter.quickPrintTerm(matched, currentState.getEnv().getServices());
-        //Hack: to avoid newlines
-        String reprTermReformatted = reprTerm.trim();
-        return new Value<>(
-                new TermType(new SortType(matched.sort())),
-                reprTermReformatted
-        );
-    }
-
     @Override
     public List<VariableAssignment> matchSeq(GoalNode<KeyData> currentState,
                                              String data,
@@ -178,7 +175,7 @@ public class KeYMatcher implements MatcherApi<KeyData> {
         //System.out.println("Signature " + sig.toString());
 
         Matchings m = MatcherFacade.matches(data,
-                currentState.getData().getNode().sequent(), false, services);
+                currentState.getData().getNode().sequent(), false, currentState.getData().getProof().getServices());
 
         if (m.isEmpty()) {
             LOGGER.debug("currentState has no match= " + currentState.getData().getNode().sequent());
@@ -208,6 +205,17 @@ public class KeYMatcher implements MatcherApi<KeyData> {
         }
     }
 
+    private Value<String> toValueTerm(KeyData currentState, Term matched) {
+
+        String reprTerm = LogicPrinter.quickPrintTerm(matched, currentState.getProof().getServices());
+        //Hack: to avoid newlines
+        String reprTermReformatted = reprTerm.trim();
+        return new Value<>(
+                new TermType(new SortType(matched.sort())),
+                reprTermReformatted
+        );
+    }
+
 
     //private TermLiteral from(SequentFormula sf) {
     //    return new TermLiteral(sf.toString());

rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/instantiate.html

@@ -16,5 +16,6 @@
     <li><code>occ</code> : <em>INT</em> occurence of the top-level formula</li>
     <li><code>with</code> : <em>TERM</em> the term with which variables should be instantiated</li>
 </ul>
+
 </body>
 </html>
\ No newline at end of file

rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/KeYInterpreterTest.java

@@ -73,5 +73,13 @@ public class KeYInterpreterTest {
 
     }
 
+    @Test
+    public void testHookAssignments() throws IOException, ProblemLoaderException {
+        facade.loadKeyFileSync(new File("src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/contraposition.key"));
+        Interpreter<KeyData> i = execute(getClass().getResourceAsStream("contraposition/hookTestScript.kps"));
+        Assert.assertTrue(i.isStrictMode());
+
+    }
+
 
 }

rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/hookTestScript.kps

+script hookTest(){
+    __STRICT_MODE:= true;
+    impRight;
+
+
+}
\ No newline at end of file

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

@@ -140,6 +140,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
                 if (fireVariableAssignmentHook(node, var.getIdentifier(), v)) {
                     node.setVariableValue(var, v);
                 }
+                node.setVariableValue(var, v);
             }
         }
         exitScope(assignmentStatement);
@@ -628,7 +629,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
                 Set<GoalNode<T>> prevNodes = new HashSet<>(prev.getGoals());
                 Set<GoalNode<T>> endNodes = new HashSet<>(end.getGoals());
                 b = prevNodes.equals(endNodes);
-                b = b && counter <= maxIterationsRepeat;
+                b = !b && counter <= maxIterationsRepeat;
             } while (b);
         } catch (InterpreterRuntimeException e) {
             logger.debug("Catched!", e);

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

@@ -39,7 +39,8 @@ public abstract class DefaultAssignmentHook<T> implements VariableAssignmentHook
             Variable<T, S> variable = (Variable<T, S>) variables.get(variableName);
             return variable.setter.apply(data, value);
         }
-        return true;
+        //@AW: TODO was true: Why?
+        return false;
     }
 
 

ui/src/main/java/edu/kit/iti/formal/psdbg/examples/lulu/bigIntProof/BigIntExample.java

 package edu.kit.iti.formal.psdbg.examples.lulu.bigIntProof;
 
-import edu.kit.iti.formal.psdbg.examples.JavaExample;
+import edu.kit.iti.formal.psdbg.examples.Example;
 
-public class BigIntExample extends JavaExample {
+public class BigIntExample extends Example {
     public BigIntExample() {
+        setName("BigInt");
+        defaultInit(getClass());
     }
 
 }

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

@@ -136,7 +136,7 @@ public class DebuggerMain implements Initializable {
     //-----------------------------------------------------------------------------------------------------------------
     private ProofTree proofTree = new ProofTree();
     private DockNode proofTreeDock = new DockNode(proofTree, "Proof Tree");
-    private WelcomePaneFMEdition welcomePane = new WelcomePaneFMEdition(this);
+    private WelcomePane welcomePane = new WelcomePane(this);
     private DockNode welcomePaneDock = new DockNode(welcomePane, "Welcome", new MaterialDesignIconView(MaterialDesignIcon.ACCOUNT));
     private DockNode activeInspectorDock;
     private CommandHelp commandHelp = new CommandHelp();
@@ -428,31 +428,51 @@ public class DebuggerMain implements Initializable {
         executeScript(FACADE.buildInterpreter(), addInitBreakpoint);
     }
 
+    /**
+     * Reload a problem from the beginning
+     *
+     * @param event
+     */
     @FXML
-    public void abortExecution() {
+    public void reloadProblem(ActionEvent event) {
+        //abort current execution();
+        //save old information and refresh models
+        statusBar.publishMessage("Reloading...");
+        File lastLoaded;
+        if (model.getKeyFile() != null) {
+            lastLoaded = model.getKeyFile();
+        } else {
+            Contract chosen = model.getChosenContract();
+            lastLoaded = model.getJavaFile();
+        }
+        //model.reload();
+        abortExecution();
+        Platform.runLater(() -> model.setStatePointer(null));
+        handleStatePointerUI(null);
 
-        if (model.getDebuggerFramework() != null) {
-            try {
-                // try to friendly
-                Future future = executorService.submit(() -> {
-                    model.getDebuggerFramework().stop();
-                    model.getDebuggerFramework().unregister();
-                    model.getDebuggerFramework().release();
-                });
+        //reload getInspectionViewsController().getActiveInspectionViewTab().getModel()
+        InspectionModel iModel = getInspectionViewsController().getActiveInspectionViewTab().getModel();
+        //iModel.setHighlightedJavaLines(FXCollections.emptyObservableSet());
+        iModel.clearHighlightLines();
+        iModel.getGoals().clear();
+        iModel.setSelectedGoalNodeToShow(null);
 
-                // wait a second!
-                future.get(1, TimeUnit.SECONDS);
-                // urgently stop
-                model.getDebuggerFramework().hardStop();
-            } catch (InterruptedException | ExecutionException | TimeoutException e) {
-                e.printStackTrace();
-            } finally {
-                model.setDebuggerFramework(null);
+        try {
+            FACADE.reload(lastLoaded);
+            if (iModel.getGoals().size() > 0) {
+                iModel.setSelectedGoalNodeToShow(iModel.getGoals().get(0));
             }
-        } else {
-            LOGGER.info("no interpreter running");
+            if (FACADE.getReadyToExecute()) {
+                LOGGER.info("Reloaded Successfully");
+                statusBar.publishMessage("Reloaded Sucessfully");
+            }
+        } catch (ProofInputException e) {
+            e.printStackTrace();
+        } catch (ProblemLoaderException e) {
+            e.printStackTrace();
         }
-        assert model.getDebuggerFramework() == null;
+
+
     }
 
     @FXML
@@ -768,44 +788,32 @@ public class DebuggerMain implements Initializable {
         }
     }
 
-    /**
-     * Reload a problem from the beginning
-     *
-     * @param event
-     */
     @FXML
-    public void reloadProblem(ActionEvent event) {
-        //abort current execution();
-        //save old information and refresh models
-        File lastLoaded;
-        if (model.getKeyFile() != null) {
-            lastLoaded = model.getKeyFile();
-        } else {
-            Contract chosen = model.getChosenContract();
-            lastLoaded = model.getJavaFile();
-        }
-        //model.reload();
-        abortExecution();
-        handleStatePointerUI(null);
-        model.setStatePointer(null);
-        //reload getInspectionViewsController().getActiveInspectionViewTab().getModel()
-        InspectionModel iModel = getInspectionViewsController().getActiveInspectionViewTab().getModel();
-        iModel.setHighlightedJavaLines(null);
-        iModel.getGoals().clear();
-        iModel.setSelectedGoalNodeToShow(null);
+    public void abortExecution() {
+        statusBar.publishMessage("Aborting Execution...");
+        if (model.getDebuggerFramework() != null) {
+            try {
+                // try to friendly
+                Future future = executorService.submit(() -> {
+                    model.getDebuggerFramework().stop();
+                    model.getDebuggerFramework().unregister();
+                    model.getDebuggerFramework().release();
+                });
 
-        try {
-            FACADE.reload(lastLoaded);
-            if (iModel.getGoals().size() > 0) {
-                iModel.setSelectedGoalNodeToShow(iModel.getGoals().get(0));
+                // wait a second!
+                future.get(1, TimeUnit.SECONDS);
+                // urgently stop
+                model.getDebuggerFramework().hardStop();
+            } catch (InterruptedException | ExecutionException | TimeoutException e) {
+                e.printStackTrace();
+            } finally {
+                model.setDebuggerFramework(null);
+                statusBar.publishMessage("Execution aborted.");
             }
-        } catch (ProofInputException e) {
-            e.printStackTrace();
-        } catch (ProblemLoaderException e) {
-            e.printStackTrace();
+        } else {
+            LOGGER.info("no interpreter running");
         }
-
-
+        assert model.getDebuggerFramework() == null;
     }
 
     @FXML

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

@@ -9,6 +9,7 @@ import de.uka.ilkd.key.logic.SequentFormula;
 import de.uka.ilkd.key.macros.scripts.EngineState;
 import de.uka.ilkd.key.macros.scripts.RuleCommand;
 import de.uka.ilkd.key.macros.scripts.ScriptException;
+import de.uka.ilkd.key.pp.LogicPrinter;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
@@ -54,6 +55,7 @@ public class InteractiveModeController {
     private static final Logger LOGGER = LogManager.getLogger(InteractiveModeController.class);
 
     private final Map<Node, Statements> cases = new HashMap<>();
+
     private final ScriptController scriptController;
     private BooleanProperty activated = new SimpleBooleanProperty();
     private ScriptArea scriptArea;
@@ -72,6 +74,8 @@ public class InteractiveModeController {
 
     private boolean moreThanOneMatch = false;
 
+    private CasesStatement casesStatement;
+
     public void start(Proof currentProof, InspectionModel model) {
         Events.register(this);
         cases.clear();
@@ -81,7 +85,17 @@ public class InteractiveModeController {
         });
         this.scriptArea = scriptController.newScript();
         this.model = model;
-
+        casesStatement = new CasesStatement();
+        cases.forEach((k, v) -> {
+            val gcs = new GuardedCaseStatement();
+            val m = new MatchExpression();
+            m.setPattern(new StringLiteral(
+                    format(LabelFactory.getBranchingLabel(k))
+            ));
+            gcs.setGuard(m);
+            gcs.setBody(v);
+            casesStatement.getCases().add(gcs);
+        });
         savepointslist = new ArrayList<>();
         savepointsstatement = new ArrayList<>();
         nodeAtInteractionStart = debuggerFramework.getStatePointer();
@@ -147,19 +161,9 @@ public class InteractiveModeController {
         SequentFormula seqForm = tap.getPio().sequentFormula();
         //transform term to parsable string representation
         Sequent seq = g.sequent();
-        String sfTerm = edu.kit.iti.formal.psdbg.termmatcher.Utils.toPrettyTerm(seqForm.formula());
-        String onTerm = edu.kit.iti.formal.psdbg.termmatcher.Utils.toPrettyTerm(tap.getPio().subTerm());
+        String sfTerm = LogicPrinter.quickPrintTerm(seqForm.formula(), keYServices, false, false);
+        String onTerm = LogicPrinter.quickPrintTerm(tap.getPio().subTerm(), keYServices, false, false);
 
-        //check whether more than one possibility for match
-        //Matchings matches = MatcherFacade.matches(term, seq, true, keYServices);
-
-        /*Parameters params = new Parameters();
-        params.put(new Variable("formula"), new TermLiteral(term));
-        if (matches.size() > 1) {
-            moreThanOneMatch = true;
-            params.put(new Variable("occ"), new StringLiteral("0"));
-
-        }*/
 
         RuleCommand.Parameters params = new RuleCommand.Parameters();
         params.formula = seqForm.formula();
@@ -170,7 +174,6 @@ public class InteractiveModeController {
         int occ = rch.getOccurence(tap.getApp());
 
         Parameters callp = new Parameters();
-//        callp.put(new Variable("formula"), new TermLiteral(sfTerm));
         callp.put(new Variable("formula"), new TermLiteral(sfTerm));
         callp.put(new Variable("occ"), new IntegerLiteral(BigInteger.valueOf(occ)));
         callp.put(new Variable("on"), new TermLiteral(onTerm));
@@ -191,8 +194,8 @@ public class InteractiveModeController {
 
             applyRule(call, g);
             // Insert into the right cases
-            Node currentNode = g.node();
-            cases.get(findRoot(currentNode)).add(call);
+            // Node currentNode = g.node();
+            // cases.get(findRoot(currentNode)).add(call);
 
             // How to Play this on the Proof?
             // How to Build a new StatePointer? Is it still possible?
@@ -228,35 +231,11 @@ public class InteractiveModeController {
     }
 
     public String getCasesAsString() {
-        CasesStatement c = new CasesStatement();
-        cases.forEach((k, v) -> {
-            val gcs = new GuardedCaseStatement();
-            val m = new MatchExpression();
-            m.setPattern(new StringLiteral(
-                    format(LabelFactory.getBranchingLabel(k))
-            ));
-            gcs.setGuard(m);
-            gcs.setBody(v);
-            c.getCases().add(gcs);
-        });
-
         PrettyPrinter pp = new PrettyPrinter();
-        c.accept(pp);
+        casesStatement.accept(pp);
         return pp.toString();
     }
 
-    private String format(String branchingLabel) {
-        System.out.println("branchingLabel = " + branchingLabel);
-        String newLabel = branchingLabel;
-        if (branchingLabel.endsWith("$$")) {
-            newLabel = branchingLabel.substring(0, branchingLabel.length() - 2);
-            newLabel += ".*";
-            System.out.println("newLabel = " + newLabel);
-        }
-        return newLabel;
-    }
-
-
     private void applyRule(CallStatement call, Goal g) throws ScriptCommandNotApplicableException {
         savepointslist.add(g.node());
         savepointsstatement.add(call);
@@ -289,21 +268,46 @@ public class InteractiveModeController {
             map.put("#2", call.getCommand());
             EngineState estate = new EngineState(g.proof());
             estate.setGoal(g);
-            // System.out.println("on = " + map.get("on"));
-            // System.out.println("formula = " +map.get("formula"));
-            // System.out.println("occ = " + map.get("occ"));
+            //System.out.println("on = " + map.get("on"));
+            //System.out.println("formula = " + map.get("formula"));
+            //System.out.println("occ = " + map.get("occ"));
             RuleCommand.Parameters cc = c.evaluateArguments(estate, map); //reflection exception
 
             AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl();
             c.execute(uiControl, cc, estate);
 
-            ImmutableList<Goal> ngoals = g.proof().getSubtreeGoals(g.node());
+            ImmutableList<Goal> ngoals = g.proof().getSubtreeGoals(expandedNode.getData().getNode());
 
             goals.remove(expandedNode);
             GoalNode<KeyData> last = null;
-            for (Goal newGoalNode : ngoals) {
-                KeyData kdn = new KeyData(kd, newGoalNode.node());
-                goals.add(last = new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed()));
+
+
+            if (ngoals.size() > 1) {
+                cases.get(findRoot(ngoals.get(0).node())).add(call);
+                CasesStatement inner = new CasesStatement();
+                cases.get(findRoot(ngoals.get(0).node())).add(inner);
+
+                for (Goal newGoalNode : ngoals) {
+                    KeyData kdn = new KeyData(kd, newGoalNode.node());
+                    goals.add(last = new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed()));
+                    val caseForSubNode = new GuardedCaseStatement();
+                    val m = new MatchExpression();
+                    m.setPattern(new StringLiteral(
+                            format(LabelFactory.getBranchingLabel(newGoalNode.node()))
+                    ));
+                    caseForSubNode.setGuard(m);
+                    inner.getCases().add(caseForSubNode);
+                    cases.put(last.getData().getNode(), caseForSubNode.getBody());
+                }
+            } else {
+                if (ngoals.size() == 0) {
+                    cases.get(g).add(call);
+                } else {
+                    KeyData kdn = new KeyData(kd, ngoals.get(0).node());
+                    goals.add(last = new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed()));
+                    Node currentNode = last.getData().getNode();
+                    cases.get(findRoot(currentNode)).add(call);
+                }
             }
             if (last != null)
                 model.setSelectedGoalNodeToShow(last);
@@ -319,6 +323,17 @@ public class InteractiveModeController {
 
     }
 
+    private String format(String branchingLabel) {
+        // System.out.println("branchingLabel = " + branchingLabel);
+        String newLabel = branchingLabel;
+        if (branchingLabel.endsWith("$$")) {
+            newLabel = branchingLabel.substring(0, branchingLabel.length() - 2);
+            newLabel += ".*";
+            //   System.out.println("newLabel = " + newLabel);
+        }
+        return newLabel;
+    }
+
     public boolean isActivated() {
         return activated.get();
     }

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

@@ -66,7 +66,7 @@ public class BaseCodeArea extends CodeArea {
             final int start = lm.getLineStart(line);
             final int end = lm.getLineEnd(line);
             setStyle(start, end, Collections.singleton(clazz));
-        } catch (ArrayIndexOutOfBoundsException e) {
+        } catch (IndexOutOfBoundsException e) {
 
         }
 

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

@@ -56,10 +56,12 @@ public class JavaArea extends BaseCodeArea {
      * highlight new lines
      */
     private void highlightLineSet() {
-        linesToHighlightProperty().get().forEach(integer -> {
-            lineToClassProperty().get().put(integer - 1, "line-highlight");
-        });
-        highlightLines();
+        if (!linesToHighlight.get().isEmpty()) {
+            linesToHighlightProperty().get().forEach(integer -> {
+                lineToClassProperty().get().put(integer - 1, "line-highlight");
+            });
+            highlightLines();
+        }
     }
 
     private void updateView() {

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

@@ -317,7 +317,7 @@ public class ScriptController {
                 lastScriptArea = area;
                 lastRegion = r;
             } else {
-                logger.error("Could not find editor for the node to highlight: " + node.getOrigin());
+                logger.debug("Could not find editor for the node to highlight: " + node.getOrigin());
             }
         }