Merge branch 'luongSavepoint' into 'master'

Luong savepoint

See merge request !19

build.gradle

@@ -6,7 +6,7 @@ plugins {
 allprojects {
     apply plugin: 'maven'
     group = 'edu.kit.iti.formal.psdbg'
-    version = 'Experimental-1.1'
+    version = '1.1-experimental'
 }
 
 subprojects {

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

+package edu.kit.iti.formal.psdbg.parser;
+
+import edu.kit.iti.formal.psdbg.parser.ast.*;
+import javafx.util.Pair;
+
+
+
+public class SavepointVisitor extends DefaultASTVisitor {
+
+
+    @Override
+    public Parameters visit(CallStatement call) {
+        if (call.getCommand().toString().equals("save")) {
+            Parameters param = call.getParameters().copy();
+            return param;
+        } else {
+            return null;
+        }
+
+    }
+
+}

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

@@ -23,10 +23,7 @@ import org.key_project.util.collection.ImmutableList;
 
 import java.io.File;
 import java.io.IOException;
-import java.util.Arrays;
-import java.util.Collection;
-import java.util.List;
-import java.util.Set;
+import java.util.*;
 import java.util.stream.Collectors;
 
 /**
@@ -44,6 +41,8 @@ public class InterpreterBuilder {
     @Getter
     private ProofScriptCommandBuilder pmc = new ProofScriptCommandBuilder();
     @Getter
+    private BuiltInCommandHandler bich = new BuiltInCommandHandler();
+    @Getter
     private ProofScript entryPoint;
     @Getter
     private Proof proof;
@@ -54,13 +53,15 @@ public class InterpreterBuilder {
     @Getter
     private ScopeLogger logger;
     @Getter
-    private DefaultLookup lookup = new DefaultLookup(psh, pmh, pmc, pmr);
+    private DefaultLookup lookup = new DefaultLookup(psh, pmh, pmc, bich, pmr);
 
     @Getter
     private KeyAssignmentHook keyHooks = new KeyAssignmentHook();
 
     private KeyInterpreter interpreter = new KeyInterpreter(lookup);
 
+
+
     @Getter
     private InterpreterOptionsHook<KeyData> optionsHook = new InterpreterOptionsHook<>(interpreter);
 
@@ -202,18 +203,33 @@ public class InterpreterBuilder {
         if (proof == null || keyEnvironment == null)
             throw new IllegalStateException("Call proof(..) before startState");
 
+
         ImmutableList<Goal> openGoals = proof.getSubtreeGoals(proof.root());
         List<GoalNode<KeyData>> goals = openGoals.stream().map(g ->
                 new GoalNode<>(null, new KeyData(g, keyEnvironment, proof), false))
                 .collect(Collectors.toList());
+
+
         interpreter.newState(goals);
+
+
         return this;
 
     }
 
     private InterpreterBuilder startState(GoalNode<KeyData> startGoal) {
         interpreter.newState(startGoal);
+
+        return this;
+    }
+
+    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);
+        this.bich.setBuiltins(builtinsnew);
         return this;
+
     }
 
 }

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

@@ -16,6 +16,7 @@ import javafx.beans.binding.BooleanBinding;
 import javafx.beans.property.SimpleBooleanProperty;
 import javafx.beans.property.SimpleObjectProperty;
 import javafx.concurrent.Task;
+import jdk.nashorn.internal.objects.annotations.Getter;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
 import org.key_project.util.collection.ImmutableList;
@@ -70,6 +71,8 @@ public class KeYProofFacade {
     //Workaround until api is relaxed
     private ProofManagementApi pma;
 
+    private File filepath;
+
     /**
      *
      */
@@ -131,6 +134,7 @@ public class KeYProofFacade {
         ProofManagementApi pma = KeYApi.loadFromKeyFile(keYFile);
         ProofApi pa = pma.getLoadedProof();
         setLoading(false);
+        filepath = keYFile;
         return pa;
     }
 
@@ -141,6 +145,7 @@ public class KeYProofFacade {
         proof.set(pa.getProof());
         contract.set(null);
         setLoading(false);
+        filepath = keyFile;
         return pa;
     }
 
@@ -249,6 +254,13 @@ public class KeYProofFacade {
         return readyToExecute;
     }
 
+    /**
+        returns filepath of loaded KeY problem
+     **/
+    public File getFilepath() {
+        return filepath;
+    }
+
     public Collection<GoalNode<KeyData>> getPseudoGoals() {
         Proof p = getProof();
         KeYEnvironment env = getEnvironment();

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

+package edu.kit.iti.formal.psdbg.interpreter.funchdl;
+
+import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
+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.VariableAssignment;
+import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
+import lombok.Getter;
+import lombok.Setter;
+
+import javax.annotation.Nullable;
+import java.util.HashMap;
+import java.util.Map;
+
+
+public class BuiltInCommandHandler implements CommandHandler<KeyData> {
+
+    @Getter @Setter
+    private Map<String, CommandHandler<KeyData>> builtins;
+
+
+    public BuiltInCommandHandler() {
+        builtins = new HashMap<>();
+
+    }
+
+
+    @Override
+    public boolean handles(CallStatement call, @Nullable KeyData data) throws IllegalArgumentException {
+        // handler only knows SaveCommand for now
+        return builtins.containsKey(call.getCommand());
+    }
+
+    @Override
+    public void evaluate(Interpreter<KeyData> interpreter, CallStatement call, VariableAssignment params, KeyData data) {
+        builtins.get(call.getCommand()).evaluate(interpreter,call,params, data);
+    }
+
+    @Override
+    public boolean isUninterpretedParams(CallStatement call) {
+        if(builtins.containsKey(call.getCommand())){
+            return builtins.get(call.getCommand()).isUninterpretedParams(call);
+        } else {
+            return false;
+        }
+    }
+}

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

@@ -85,11 +85,16 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
     @Override
     public boolean handles(CallStatement call, KeyData data) throws IllegalArgumentException {
         if (rules.containsKey(call.getCommand())) return true;//static/rigid rules
+        try{
         if (data != null) {
             Goal goal = data.getGoal();
             Set<String> rules = findTaclets(data.getProof(), goal);
             return rules.contains(call.getCommand());
         }
+        } catch (NullPointerException npe) {
+            System.out.println("npe = " + npe);
+            return false;    
+        }
         return false;
     }
 

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

+package edu.kit.iti.formal.psdbg.interpreter.funchdl;
+
+import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
+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.VariableAssignment;
+import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
+import lombok.Getter;
+import lombok.Setter;
+import org.apache.logging.log4j.LogManager;
+import org.apache.logging.log4j.Logger;
+
+import javax.annotation.Nullable;
+import java.io.File;
+import java.io.IOException;
+
+public class SaveCommand implements CommandHandler<KeyData> {
+    public static final String SAVE_COMMAND_NAME = "#save";
+    private static Logger logger = LogManager.getLogger(SaveCommand.class);
+    private static Logger consoleLogger = LogManager.getLogger("console");
+
+    @Getter
+    @Setter
+    private File path;
+
+    public SaveCommand(File path) {
+        this.path = path;
+    }
+
+
+    @Override
+    public boolean handles(CallStatement call, @Nullable KeyData data) throws IllegalArgumentException {
+        return call.getCommand().equals(SAVE_COMMAND_NAME);
+    }
+
+    @Override
+    public void evaluate(Interpreter<KeyData> interpreter, CallStatement call, VariableAssignment params, KeyData data) {
+        //be careful parameters are uninterpreted
+        SavePoint sp = new SavePoint(call);
+        //Not via Parentpath -> dependency on OS
+           /*     String parentPath = path.getAbsolutePath();
+        parentPath = parentPath.substring(0, parentPath.length() - path.getName().length());*/
+
+        File parent = path.getParentFile();
+        File newFile = sp.getProofFile(parent);
+
+        consoleLogger.info("(Safepoint) Location to be saved to = " + newFile.getAbsolutePath());
+
+        try {
+            interpreter.getSelectedNode().getData().getProof().saveToFile(newFile);
+            //TODO Call to key persistend facade
+        } catch (IOException e) {
+            e.printStackTrace();
+        }
+    }
+
+
+    @Override
+    public boolean isUninterpretedParams(CallStatement call) {
+        return true;
+    }
+}
+
+
+
+
+
+
+

rt-key/src/main/resources/log4j2.xml

 <?xml version="1.0" encoding="UTF-8"?>
+<!--
+https://logging.apache.org/log4j/2.x/manual/configuration.html
+-->
 <Configuration status="error">
     <Appenders>
+        <Console name="ConsoleErr" target="SYSTEM_ERR">
+            <PatternLayout pattern="%d{HH:mm:ss.SSS} [%t] %-5level %logger{36} - %msg%n"/>
+        </Console>
         <Console name="Console" target="SYSTEM_OUT">
-            <PatternLayout pattern="[%-5level] %msg%n"/>
-            <!--<PatternLayout pattern="%d{HH:mm:ss.SSS} [%t] %-5level %logger{36} - %msg%n"/>-->
-
-
+            <PatternLayout>
+                <!--                <pattern>%d %highlight{%p} %style{%C{1.} [%t] %m}{bold,green}%n</pattern>-->
+                <pattern>%r %highlight{%p} %style{[%t] %m}{bold,green} \n\t\tfrom %l%n</pattern>
+            </PatternLayout>
         </Console>
+
         <File name="F" fileName="debug.log" bufferSize="0" bufferedIO="false" append="false">
             <PatternLayout pattern="%d{HH:mm:ss.SSS} [%t] %-5level %logger{36} - %msg%n"/>
         </File>
     </Appenders>
     <Loggers>
         <Root level="trace">
-            <AppenderRef ref="Console" level="warn"/>
+            <AppenderRef ref="ConsoleErr" level="error"/>
             <AppenderRef ref="F"/>
         </Root>
+
+        <Logger name="console">
+            <AppenderRef ref="Console" level="info"/>
+        </Logger>
     </Loggers>
 </Configuration>

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

@@ -148,7 +148,7 @@ public class Evaluator<T> extends DefaultASTVisitor<Value> implements ScopeObser
                 String name = m.group().substring(1); // remove trailing '?'
                 Expression t = expr.getSubstitution().get(m.group());
 
-                //either evalute the substitent or find ?X in the
+                //either evalute the substituent or find ?X in the
                 String newVal = "";
                 if (t != null)
                     newVal = ((Value) t.accept(this)).getData().toString();

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

@@ -85,7 +85,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
             throw new InterpreterRuntimeException("no state on stack. call newState before interpret");
         }
 
-        if(getSelectedNode() != null) {
+        if (getSelectedNode() != null) {
             //initialize environment variables
             for (VariableAssignmentHook<T> hook : variableHooks) {
                 VariableAssignment va = hook.getStartAssignment(getSelectedNode().getData());
@@ -186,7 +186,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
         return evaluator.eval(expr);
     }
 
-    protected  Evaluator<T> createEvaluator(VariableAssignment assignments, GoalNode<T> g) {
+    protected Evaluator<T> createEvaluator(VariableAssignment assignments, GoalNode<T> g) {
         Evaluator<T> evaluator = new Evaluator<>(assignments, g);
         evaluator.setMatcher(matcherApi);
         return evaluator;
@@ -562,30 +562,61 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
         enterScope(call);
         if (!call.getCommand().isEmpty()) //real call, can handle pseudo calls!
         {
-            // System.out.println(stateStack.peek().hashCode());
             //neuer VarScope
             //enter new variable scope
-            VariableAssignment params = evaluateParameters(call.getParameters());
-            GoalNode<T> g = getSelectedNode();
-            g.enterScope();
+            VariableAssignment params;
+            GoalNode<T> g = null;
+            boolean unInterpretedParams = functionLookup.isUninterpretedParams(call);
+            if (!unInterpretedParams) {
+                params = evaluateParameters(call.getParameters());
+                g = getSelectedNode();
+                g.enterScope();
+            } else {
+                params = evaluateParametersStateLess(call.getParameters());
+
+            }
             try {
                 functionLookup.callCommand(this, call, params);
+
             } catch (RuntimeException e) {
-                System.err.println("Call command not applicable");
+                System.err.println("Call command " + call.getCommand() + "not applicable");
                 throw e;
                 //TODO handling of error state for each visit
                 //State<T> newErrorState = newState(null, null);
                 //newErrorState.setErrorState(true);
                 //pushState(newErrorState);
             } finally {
-                g.exitScope();
-                //  System.out.println(stateStack.peek().hashCode());
+                if (!unInterpretedParams) {
+                    //TODO this may not be needed
+                    g.exitScope();
+                }
             }
+
         }
         exitScope(call);
         return null;
     }
 
+    private VariableAssignment evaluateParametersStateLess(Parameters parameters) {
+        VariableAssignment va = new VariableAssignment();
+        Evaluator<T> evaluator = createEvaluator(null, null);
+
+        parameters.entrySet().forEach(entry -> {
+            try {
+                Value val = evaluate(entry.getValue());
+                va.declare(entry.getKey(), val.getType());
+                va.assign(entry.getKey(), val);
+            } catch (NullPointerException npe) {
+                System.out.println("Caught Nullpointer in evaluation of Stateless parameters: " + entry.toString()
+                );
+                Value val = evaluator.eval(entry.getValue());
+                va.declare(entry.getKey(), val.getType());
+                va.assign(entry.getKey(), val);
+            }
+        });
+        return va;
+    }
+
     public VariableAssignment evaluateParameters(Parameters parameters) {
         VariableAssignment va = new VariableAssignment();
         parameters.entrySet().forEach(entry -> {
@@ -669,9 +700,9 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
         // TODO: quickfix
 
         List<GoalNode<T>> currentGoals = getCurrentGoals();
-        if(getCurrentGoals().size() > 1) {
-            if(getSelectedNode() == null) {
-                for(GoalNode<T> goal: currentGoals) {
+        if (getCurrentGoals().size() > 1) {
+            if (getSelectedNode() == null) {
+                for (GoalNode<T> goal : currentGoals) {
 
                     goal.enterScope();
                     signature.forEach(goal::declareVariable);
@@ -694,8 +725,10 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
             GoalNode<T> selectedGoalNode = stateStack.peek().getSelectedGoalNode();
             if (selectedGoalNode != null) {
                 assert stateStack.peek().getGoals().contains(selectedGoalNode);
+                return selectedGoalNode;
+            } else {
+                throw new IllegalStateException();
             }
-            return selectedGoalNode;
         } catch (IllegalStateException e) {
             if (strictMode)
                 throw e;

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

 package edu.kit.iti.formal.psdbg.interpreter.data;
 
+import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
 import edu.kit.iti.formal.psdbg.parser.ast.*;
+import lombok.AllArgsConstructor;
 import lombok.Data;
 import lombok.Getter;
 import lombok.RequiredArgsConstructor;
@@ -9,47 +11,102 @@ import java.io.File;
 
 @Data
 @RequiredArgsConstructor
-public class SavePoint   {
+@AllArgsConstructor
+public class SavePoint {
+    @Getter
+    private final String name;
+    private int startOffset = -1;
+    private int endOffset = -1;
+    @Getter
+    private int lineNumber = -1;
+    private ForceOption force = ForceOption.YES;
 
-    private final String savepointName;
-
-    private int start = -1;
-
-    private int end = -1;
-
-    public SavePoint(CallStatement call){
-        if(isSaveCommand(call)){
+    public SavePoint(CallStatement call) {
+        if (isSaveCommand(call)) {
             Parameters p = call.getParameters();
-            savepointName = ((StringLiteral) p.get(new Variable("#2"))).getText();
-            start = call.getRuleContext().getStart().getStartIndex();
-            end = call.getRuleContext().getStart().getStopIndex();
-        }
-        throw new IllegalArgumentException(call.getCommand()+" is not a save statement");
-    }
+            name = evalAsText(p, "#2", "not-available");
+            force = ForceOption.valueOf(evalAsText(p, "force", "yes").toUpperCase());
 
-    public static boolean isSaveCommand(CallStatement call){
-        return (call.getCommand().equals("save"));
+            try {
+                startOffset = call.getRuleContext().getStart().getStartIndex();
+                endOffset = call.getRuleContext().getStart().getStopIndex();
+                lineNumber = call.getRuleContext().getStart().getLine();
+            } catch (NullPointerException npe) {
+            }
+        } else {
+            throw new IllegalArgumentException(call.getCommand() + " is not a save statement");
+        }
     }
 
-    public File getProofFile(File dir){
-        return new File(dir, savepointName+".proof");
+    public static boolean isSaveCommand(CallStatement call) {
+        return (call.getCommand().equals("#save"));
     }
 
     public static boolean isSaveCommand(Statement statement) {
-        try{
+        try {
             CallStatement c = (CallStatement) statement;
             return isSaveCommand(c);
-        }catch (ClassCastException e) {
+        } catch (ClassCastException e) {
             return false;
         }
     }
 
+    public boolean exists(File dir) {
+        return getProofFile(dir).exists() && getPersistedStateFile(dir).exists();
+    }
+
+    public static String evalAsText(Parameters p, String key, String defaultValue) {
+        Variable k = new Variable(key);
+        if (!p.containsKey(k)) {
+            return defaultValue;
+        }
+
+        return (String) p.get(k).accept(new DefaultASTVisitor<String>() {
+            @Override
+            public String defaultVisit(ASTNode node) {
+                throw new IllegalArgumentException();
+            }
+
+            @Override
+            public String visit(Variable variable) {
+                return variable.getIdentifier();
+            }
+
+            @Override
+            public String visit(StringLiteral stringLiteral) {
+                return stringLiteral.getText();
+            }
+
+            @Override
+            public String visit(BooleanLiteral booleanLiteral) {
+                return Boolean.toString(booleanLiteral.isValue());
+            }
+
+            @Override
+            public String visit(IntegerLiteral integer) {
+                return (integer.getValue().toString());
+            }
+        });
+    }
+
+    public File getProofFile(File dir) {
+        return new File(dir, name + ".proof");
+    }
+
+    public File getPersistedStateFile(File dir) {
+        return new File(dir, name + ".psdbgstate.xml");
+    }
+
     public boolean isThisStatement(Statement statement) {
-        if(isSaveCommand(statement)){
+        if (isSaveCommand(statement)) {
             CallStatement c = (CallStatement) statement;
-            return c.getCommand().equals(savepointName);
+            return c.getCommand().equals(name);
 
         }
         return false;
     }
+