...

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

@@ -81,4 +81,8 @@ public class Value<T> {
     public String toString() {
         return data + ":" + type;
     }
+
+    public static Value<BigInteger> from(long val) {
+        return from(BigInteger.valueOf(val));
+    }
 }

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

@@ -8,6 +8,7 @@ import de.uka.ilkd.key.control.KeYEnvironment;
 import de.uka.ilkd.key.macros.ProofMacro;
 import de.uka.ilkd.key.macros.scripts.ProofScriptCommand;
 import de.uka.ilkd.key.proof.Proof;
+import edu.kit.iti.formal.psdbg.interpreter.assignhook.InterpreterOptionsHook;
 import edu.kit.iti.formal.psdbg.interpreter.assignhook.KeyAssignmentHook;
 import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
 import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
@@ -52,10 +53,14 @@ public class InterpreterBuilder {
     private ScopeLogger logger;
     @Getter
     private DefaultLookup lookup = new DefaultLookup(psh, pmh, pmc, pmr);
+
+    @Getter
+    private KeyAssignmentHook keyHooks = new KeyAssignmentHook();
+
     private KeyInterpreter interpreter = new KeyInterpreter(lookup);
 
     @Getter
-    private KeyAssignmentHook variableHook = new KeyAssignmentHook();
+    private InterpreterOptionsHook<KeyData> optionsHook = new InterpreterOptionsHook<>(interpreter);
 
     public InterpreterBuilder addProofScripts(File file) throws IOException {
         return addProofScripts(Facade.getAST(file));
@@ -72,7 +77,8 @@ public class InterpreterBuilder {
     }
 
     public KeyInterpreter build() {
-        interpreter.setVariableAssignmentHook(variableHook);
+        interpreter.getVariableHooks().add(keyHooks);
+        interpreter.getVariableHooks().add(optionsHook);
         return interpreter;
     }
 

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

 package edu.kit.iti.formal.psdbg.interpreter.assignhook;
 
+import com.google.common.base.Converter;
+import com.google.common.collect.BiMap;
+import com.google.common.collect.HashBiMap;
+import com.google.common.collect.Maps;
+import de.uka.ilkd.key.settings.ProofDependentSMTSettings;
+import de.uka.ilkd.key.settings.ProofIndependentSMTSettings;
 import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
 import edu.kit.iti.formal.psdbg.parser.data.Value;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
 
 import java.math.BigInteger;
+import java.util.function.BiConsumer;
+import java.util.function.BiFunction;
+import java.util.function.Function;
+
+import static de.uka.ilkd.key.strategy.StrategyProperties.*;
 
 /**
  * @author Alexander Weigl
@@ -15,15 +26,202 @@ public class KeyAssignmentHook extends DefaultAssignmentHook<KeyData> {
     private static Logger logger = LogManager.getLogger(KeyAssignmentHook.class);
 
     public KeyAssignmentHook() {
-        register("MAX_AUTO_STEPS", this::setMaxAutosteps, this::getMaxAutosteps);
-        //register()
+        register("__KEY_MAX_STEPS",
+                "Should be a positive number and is the limit for rule application in automatic proof searchs.\n",
+                (kd, val) -> {
+                    try {
+                        kd.getProof().getSettings().getStrategySettings().setMaxSteps(
+                                ((BigInteger) val.getData()).intValue()
+                        );
+                    } catch (ClassCastException e) {
+                        return false;
+                    }
+                    return true;
+                },
+                (kd) -> Value.from(kd.getProof().getSettings().getStrategySettings().getMaxSteps()));
+
+        register("__KEY_TIMEOUT",
+                (kd, val) -> {
+                    try {
+                        kd.getProof().getSettings().getStrategySettings().setTimeout(
+                                ((BigInteger) val.getData()).longValue()
+                        );
+                    } catch (ClassCastException e) {
+                        return false;
+                    }
+                    return true;
+                },
+                (kd) -> Value.from(BigInteger.valueOf(kd.getProof().getSettings().getStrategySettings().getTimeout())));
+
+        /*TODO        register("__KEY_CHOICE", ((keyData, value) -> {
+                keyData.getProof().getSettings().getChoiceSettings().getChoices()
+        }), keyData -> {
+
+        })
+        */
+
+        this.registerSMTPD("INVARIANT_ALL",
+                "",
+                (ss) -> Value.from(ss.invariantForall),
+                ((ss, val) -> ss.invariantForall = val));
+
+        this.registerSMTPD("MAX_GENERIC_SORTS", "",
+                (ss) -> Value.from(ss.maxGenericSorts),
+                (ss, v) -> ss.maxGenericSorts = v.intValue());
+
+        this.registerSMTPD("MAX_INTEGER", "",
+                (ss) -> Value.from(ss.maxInteger),
+                (ss, v) -> ss.maxInteger = v.intValue());
+
+        this.registerSMTPD("MIN_INTEGER", "",
+                (ss) -> Value.from(ss.minInteger),
+                (ss, v) -> ss.minInteger = v.intValue());
+
+        this.registerSMTPD("USE_BUILTIN_UNIQUENESS", "",
+                (ss) -> Value.from(ss.useBuiltInUniqueness),
+                (ss, v) -> ss.useBuiltInUniqueness = v);
+
+        this.registerSMTPD("USE_CONSTANTS_FOR_INTEGERS", "",
+                (ss) -> Value.from(ss.useConstantsForIntegers),
+                (ss, v) -> ss.useConstantsForIntegers = v);
+
+        this.registerSMTPD("useExplicitTypeHierarchy", "",
+                (ss) -> Value.from(ss.useExplicitTypeHierarchy),
+                (ss, v) -> ss.useExplicitTypeHierarchy = v);
+
+        this.registerSMTPD("useNullInstantiation", "",
+                (ss) -> Value.from(ss.useNullInstantiation),
+                (ss, v) -> ss.useNullInstantiation = v);
+
+        this.registerSMTPD("USE_UI_MULTIPLICATION", "",
+                (ss) -> Value.from(ss.useUIMultiplication),
+                (ss, v) -> ss.useUIMultiplication = v);
+
+        registerSMTPI("ACTIVE_SOLVER", "",
+                (ss) -> Value.from(ss.activeSolver),
+                (ss, v) -> ss.activeSolver = v);
+
+        registerSMTPI("CHECK_FOR_SUPPORT", "",
+                (ss) -> Value.from(ss.checkForSupport),
+                (ss, v) -> ss.checkForSupport = v);
+
+        registerSMTPI("heapBound", "",
+                (ss) -> Value.from(ss.heapBound),
+                (ss, v) -> ss.heapBound = v.intValue());
+
+        registerSMTPI("INT_BOUND", "",
+                (ss) -> Value.from(ss.intBound),
+                (ss, v) -> ss.intBound = v.intValue());
+
+        registerSMTPI("LOCSET_BOUND", "",
+                (ss) -> Value.from(ss.locsetBound),
+                (ss, v) -> ss.locsetBound = v.intValue());
+
+        registerSMTPI("MAX_CONCURRENT_PROCESSES", "",
+                (ss) -> Value.from(ss.maxConcurrentProcesses),
+                (ss, v) -> ss.maxConcurrentProcesses = v.intValue());
+
+        registerSMTPI("MODE_OF_PROGRESS_DIALOG", "",
+                (ss) -> Value.from(ss.modeOfProgressDialog),
+                (ss, v) -> ss.modeOfProgressDialog = v.intValue());
+
+        registerSMTPI("OBJECT_BOUND", "",
+                (ss) -> Value.from(ss.objectBound),
+                (ss, v) -> ss.objectBound = v.intValue());
+
+        registerSMTPI("PATH_FOR_SMT_TRANSLATION", "",
+                (ss) -> Value.from(ss.pathForSMTTranslation),
+                (ss, v) -> ss.pathForSMTTranslation = v);
+
+        registerSMTPI("SEQ_BOUND", "",
+                (ss) -> Value.from(ss.seqBound),
+                (ss, v) -> ss.seqBound = v.intValue());
+
+        registerSMTPI("SHOW_RESULTS_AFTER_EXECUTION", "",
+                (ss) -> Value.from(ss.showResultsAfterExecution),
+                (ss, v) -> ss.showResultsAfterExecution = v);
+
+        registerSMTPI("STORE_TRANSLATION_TO_FILE", "",
+                (ss) -> Value.from(ss.storeSMTTranslationToFile),
+                (ss, v) -> ss.storeSMTTranslationToFile = v);
+
+        registerSMTPI("TIMEOUT", "",
+                (ss) -> Value.from(ss.timeout),
+                (ss, v) -> ss.timeout = v.intValue());
+
+        BiMap<String, String> methodMap = HashBiMap.create(3);
+        methodMap.put("method", METHOD_CONTRACT);
+        methodMap.put("expand", METHOD_EXPAND);
+        methodMap.put("none", METHOD_NONE);
+        registerKeYMultiOptions("__KEY_METHOD_OPTION", METHOD_OPTIONS_KEY, Maps.asConverter(methodMap));
+
+        BiMap<String, String> nonLinArithMap = HashBiMap.create(3);
+        nonLinArithMap.put("completion", NON_LIN_ARITH_COMPLETION);
+        nonLinArithMap.put("defops", NON_LIN_ARITH_DEF_OPS);
+        nonLinArithMap.put("none", NON_LIN_ARITH_NONE);
+        registerKeYMultiOptions("__KEY_NON_LINEAR_ARITHMETIC", NON_LIN_ARITH_OPTIONS_KEY,
+                Maps.asConverter(nonLinArithMap));
+
+        BiMap<String, String> stopModeMap = HashBiMap.create(3);
+        stopModeMap.put("nonclose", STOPMODE_NONCLOSE);
+        stopModeMap.put("default", STOPMODE_DEFAULT);
+        registerKeYMultiOptions("__KEY_STOP_MODE", STOPMODE_OPTIONS_KEY, Maps.asConverter(stopModeMap));
+
+        registerKeYOnOffOption("__KEY_DEP", DEP_OPTIONS_KEY, DEP_ON, DEP_OFF);
+        registerKeYOnOffOption("__KEY_QUERY", QUERY_OPTIONS_KEY, QUERY_ON, QUERY_OFF);
+    }
+
+    private <K> Variable registerSMTPI(String name, String doc, Function<ProofIndependentSMTSettings, Value<K>> init,
+                                       BiConsumer<ProofIndependentSMTSettings, K> setter) {
+        BiFunction<KeyData, Value<K>, Boolean> s = ((KeyData keyData, Value<K> value) -> {
+            try {
+                ProofIndependentSMTSettings ss = ProofIndependentSMTSettings.getDefaultSettingsData();
+                setter.accept(ss, (K) value.getData());
+                return true;
+            } catch (ClassCastException e) {
+                return false;
+            }
+        });
+        Function<KeyData, Value<K>> i = (KeyData keyData) -> init.apply(ProofIndependentSMTSettings.getDefaultSettingsData());
+        return register("__KEY_SMT__" + name, doc, s, i);
+    }
+
+    private <K> Variable registerSMTPD(String name, String doc, Function<ProofDependentSMTSettings, Value<K>> init,
+                                       BiConsumer<ProofDependentSMTSettings, K> setter) {
+        BiFunction<KeyData, Value<K>, Boolean> s = ((KeyData keyData, Value<K> value) -> {
+            try {
+                ProofDependentSMTSettings ss = keyData.getProof().getSettings().getSMTSettings();
+                setter.accept(ss, value.getData());
+                return true;
+            } catch (ClassCastException e) {
+                return false;
+            }
+        });
+        Function<KeyData, Value<K>> i = (KeyData keyData) -> init.apply(keyData.getProof().getSettings().getSMTSettings());
+        return register("__KEY_SMT__" + name, doc, s, i);
     }
 
-    public Value<BigInteger> getMaxAutosteps(KeyData data) {
-        return Value.from(100);
+    private void registerKeYMultiOptions(String name, String key, Converter<String, String> map) {
+        Function<KeyData, Value<String>> init = keyData -> Value.from(map.reverse().convert(keyData.getActiveStrategyProperties().getProperty(key)));
+        BiFunction<KeyData, Value<String>, Boolean> setter = (kd, val) -> {
+            try {
+                kd.getActiveStrategyProperties().setProperty(key, map.convert((String) val.getData()));
+            } catch (ClassCastException e) {
+                return false;
+            }
+            return true;
+        };
+        register(name, setter, init);
     }
 
-    public boolean setMaxAutosteps(KeyData data, Value<BigInteger> val) {
-        return true;
+    private void registerKeYOnOffOption(String name, String key, String on, String off) {
+        Function<KeyData, Value<Boolean>> init = keyData -> Value.from(on.equals(keyData.getActiveStrategyProperties().getProperty(key)));
+        BiFunction<KeyData, Value<Boolean>, Boolean> setter = (keyData, value) -> {
+            keyData.getActiveStrategyProperties().setProperty(key,
+                    value.getData() ? on : off
+            );
+            return true;
+        };
+        register(name, setter, init);
     }
 }

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

@@ -5,6 +5,7 @@ import de.uka.ilkd.key.java.SourceElement;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
+import de.uka.ilkd.key.strategy.StrategyProperties;
 import edu.kit.iti.formal.psdbg.LabelFactory;
 import lombok.*;
 
@@ -166,4 +167,7 @@ public class KeyData {
     }
 
 
+    public StrategyProperties getActiveStrategyProperties() {
+        return getProof().getSettings().getStrategySettings().getActiveStrategyProperties();
+    }
 }

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

-import static org.junit.Assert.*;
+package edu.kit.iti.formal.psdbg.interpreter.assignhook;
+
+import de.uka.ilkd.key.api.KeYApi;
+import de.uka.ilkd.key.proof.io.ProblemLoaderException;
+import edu.kit.iti.formal.psdbg.interpreter.InterpreterBuilder;
+import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
+import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
+import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
+import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
+import edu.kit.iti.formal.psdbg.parser.ast.Variable;
+import edu.kit.iti.formal.psdbg.parser.data.Value;
+import edu.kit.iti.formal.psdbg.parser.types.SimpleType;
+import org.junit.Test;
+
+import java.io.File;
+import java.util.ArrayList;
+import java.util.List;
+
+import static edu.kit.iti.formal.psdbg.TestHelper.getFile;
 
 /**
  * @author Alexander Weigl
  * @version 1 (20.11.17)
  */
-public class PrintVariables {
+public class PrintSpecialVariables {
+    @Test
+    public void printSpecialVariables() throws ProblemLoaderException {
+        File f = new File(getFile(getClass(), "../contraposition/contraposition.key"));
+        InterpreterBuilder ib = new InterpreterBuilder();
+        KeyInterpreter inter = ib.proof(KeYApi.loadFromKeyFile(f).getLoadedProof())
+                .startState()
+                .build();
+        inter.interpret(new ProofScript());
+        VariableAssignment va = inter.peekState().getSelectedGoalNode().getAssignments();
+
+
+        for (VariableAssignmentHook<KeyData> hook : inter.getVariableHooks()) {
+            System.out.format("### %s%n%n", hook.toString());
+            try {
+                DefaultAssignmentHook<KeyData> dfhook = (DefaultAssignmentHook<KeyData>) hook;
+                List<String> vars = new ArrayList<>(dfhook.getVariables().keySet());
+                vars.sort(String::compareTo);
+
+                for (String varname : vars) {
+                    DefaultAssignmentHook.Variable v = dfhook.getVariables().get(varname);
+                    Variable var = new Variable(v.getName());
+                    Value rt = va.getValue(var);
+
+                    System.out.printf("* `%s : %s = %s`%n%n",
+                            v.getName(),
+                            rt.getType(),
+                            (rt.getType() == SimpleType.STRING
+                                    ? ('"' + rt.getData().toString() + '"')
+                                    : rt.getData())
+                    );
+
+
+                    String doc = "no documentation";
+                    if (v.getDocumentation() != null && !v.getDocumentation().isEmpty())
+                        doc = v.getDocumentation().replace("\n", "\n  ");
+                    System.out.println("  " + doc);
+                    System.out.println();
+                }
+            } catch (ClassCastException e) {
+
+            }
+        }
+    }
 
 }
\ No newline at end of file

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

@@ -36,36 +36,26 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
 
     @Getter
     public final AtomicBoolean hardStop = new AtomicBoolean(false);
-
+    @Getter
+    private final List<VariableAssignmentHook<T>> variableHooks = new LinkedList<>();
     @Getter
     protected List<Visitor> entryListeners = new ArrayList<>(),
             exitListeners = new ArrayList<>();
-
     /**
      *
      */
     @Getter
     @Setter
     private int maxIterationsRepeat = 10000;
-
     private Stack<State<T>> stateStack = new Stack<>();
-
     @Getter
     @Setter
     private MatcherApi<T> matcherApi;
-
     @Getter
     private CommandLookup functionLookup;
-
     @Getter
     @Setter
     private boolean strictMode = false;
-
-    @Getter
-    @Setter
-    private VariableAssignmentHook<T> variableAssignmentHook = null;
-
-
     @Getter
     @Setter
     private boolean suppressListeners = false;
@@ -96,12 +86,11 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
         }
 
         //initialize environment variables
-        if (variableAssignmentHook != null) {
-            VariableAssignment va = variableAssignmentHook.getStartAssignment(getSelectedNode().getData());
+        for (VariableAssignmentHook<T> hook : variableHooks) {
+            VariableAssignment va = hook.getStartAssignment(getSelectedNode().getData());
             getSelectedNode().setAssignments(
                     getSelectedNode().getAssignments().push(va));
         }
-
         script.accept(this);
         exitScope(script);
     }
@@ -159,10 +148,12 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
     }
 
     protected boolean fireVariableAssignmentHook(GoalNode<T> node, String identifier, Value v) {
-        if (variableAssignmentHook != null) {
-            return variableAssignmentHook.handleAssignment(node.getData(), identifier, v);
+        for (VariableAssignmentHook<T> hook : variableHooks) {
+            if (hook.handleAssignment(node.getData(), identifier, v)) {
+                return true;
+            }
         }
-        return true;
+        return variableHooks.size() == 0;
     }
 
     private Value evaluate(Expression expr) {

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

 package edu.kit.iti.formal.psdbg.interpreter.assignhook;
 
-import edu.kit.iti.formal.psdbg.parser.data.Value;
 import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
+import edu.kit.iti.formal.psdbg.parser.data.Value;
+import lombok.Getter;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
 
 import java.util.HashMap;
-import java.util.Map;
 import java.util.function.BiFunction;
 import java.util.function.Function;
 
@@ -17,33 +17,48 @@ import java.util.function.Function;
 public abstract class DefaultAssignmentHook<T> implements VariableAssignmentHook<T> {
     private static Logger logger = LogManager.getLogger(DefaultAssignmentHook.class);
 
-    private Map<String, Function<T, Value>> initFunctions = new HashMap<>();
-    private Map<String, BiFunction<T, Value, Boolean>> hooks = new HashMap<>();
+    @Getter
+    private final HashMap<String, Variable> variables = new HashMap<>();
+
+    protected <K> Variable register(String varName, String doc, BiFunction<T, Value<K>, Boolean> setter, Function<T, Value<K>> getter) {
+        return register(new Variable<>(varName, doc, getter, setter));
+    }
 
+    protected <K> Variable register(String varName, BiFunction<T, Value<K>, Boolean> setter, Function<T, Value<K>> getter) {
+        return register(new Variable<>(varName, null, getter, setter));
+    }
 
-    protected void register(String varName, BiFunction<T, Value, Boolean> setter, Function<T, Value> getter) {
-        initFunctions.put(varName, getter);
-        hooks.put(varName, setter);
+    protected <K> Variable register(Variable<T, K> var) {
+        return variables.put(var.name, var);
     }
 
     @Override
+    @SuppressWarnings("unchecked")
     public <S> boolean handleAssignment(T data, String variableName, Value<S> value) {
-        if (hooks.containsKey(variableName)) {
-            return hooks.get(variableName).apply(data, value);
+        if (variables.containsKey(variableName)) {
+            Variable<T, S> variable = (Variable<T, S>) variables.get(variableName);
+            return variable.setter.apply(data, value);
         }
         return true;
     }
 
 
     @Override
+    @SuppressWarnings("unchecked")
     public VariableAssignment getStartAssignment(T data) {
         VariableAssignment va = new VariableAssignment();
-        for (Map.Entry<String, Function<T, Value>> s : initFunctions.entrySet()) {
-            Value apply = s.getValue().apply(data);
-            va.declare(s.getKey(), apply.getType());
-            va.assign(s.getKey(), apply);
+        for (Variable<T, ?> var : variables.values()) {
+            Value val = var.init.apply(data);
+            va.declare(var.name, val.getType());
+            va.assign(var.name, val);
         }
         return va;
     }
 
+    @lombok.Value
+    public static class Variable<T, K> {
+        String name, documentation;
+        Function<T, Value<K>> init;
+        BiFunction<T, Value<K>, Boolean> setter;
+    }
 }

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

@@ -5,6 +5,8 @@ import edu.kit.iti.formal.psdbg.parser.data.Value;
 import lombok.Getter;
 import lombok.Setter;
 
+import java.math.BigInteger;
+
 public class InterpreterOptionsHook<T> extends DefaultAssignmentHook<T> {
     @Getter
     @Setter
@@ -13,10 +15,10 @@ public class InterpreterOptionsHook<T> extends DefaultAssignmentHook<T> {
     public InterpreterOptionsHook(Interpreter<T> interpreter) {
         this.interpreter = interpreter;
 
-
         register("__MAX_ITERATIONS_REPEAT",
-                (T data, Value v) -> {
-                    interpreter.setMaxIterationsRepeat((Integer) v.getData());
+                "Sets the the upper limit for iterations in repeat loops. Default value is really high.",
+                (T data, Value<BigInteger> v) -> {
+                    interpreter.setMaxIterationsRepeat(v.getData().intValue());
                     return true;
                 },
                 (T data) -> Value.from(interpreter.getMaxIterationsRepeat())
@@ -24,12 +26,16 @@ public class InterpreterOptionsHook<T> extends DefaultAssignmentHook<T> {
 
 
         register("__STRICT_MODE",
-                (T data, Value v) -> {
-                    interpreter.setStrictMode((boolean) v.getData());
+                        "Defines if the interpreter is in strict or relax mode. \n\n" +
+                        "In strict mode the interpreter throws an exception in following cases:\n\n" +
+                        "* access to undeclared or unassigned variable\n" +
+                        "* application of non-applicable rule\n\n" +
+                        "In non-strict mode these errors are ignored&mdash;a warning is given on the console.",
+                (T data, Value<Boolean> v) -> {
+                    interpreter.setStrictMode(v.getData());
                     return true;
                 },
                 (T data) -> Value.from(interpreter.isStrictMode())
         );
-
     }
 }

website/docs/variables.md

@@ -34,27 +34,139 @@ you can do conditions other these options.