Merge branch 'weiglStatePersistence' into 'master'

Persistence of interpreter state

See merge request !17

build.gradle

@@ -39,27 +39,4 @@ subprojects {
         //compileOnly group: 'org.projectlombok', name: 'lombok', version: '1.16.20'
         compileOnly files("$rootDir/lombok-edge.jar")
     }
-
-    /*lombok { // optional: values below are the defaults
-        //version = "1.16.21" //bleeding edge
-        //sha256 = "c5178b18caaa1a15e17b99ba5e4023d2de2ebc18b58cde0f5a04ca4b31c10e6d"
-    }*/
-
-    compileJava {
-        /*  options.compilerArgs.addAll([
-                  "-Xlint:all,-processing,-cast,-serial,-try",
-                  "-J--add-opens=jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED",
-                  "-J--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED",
-                  "-J--add-opens=jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED",
-                  "-J--add-opens=jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED",
-                  "-J--add-opens=jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED",
-                  "-J--add-opens=jdk.compiler/com.sun.tools.javac.parser=ALL-UNNAMED",
-                  "-J--add-opens=jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED",
-                  "-J--add-opens=jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED",
-                  "-J--add-opens=jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED",
-                  "-J--add-opens=jdk.compiler/com.sun.tools.javac.jvm=ALL-UNNAMED",
-                  "-J--add-opens=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED",
-                  "-J--add-opens=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED"
-          ])*/
-    }
 }

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

@@ -3,10 +3,13 @@ package edu.kit.iti.formal.psdbg;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
+import javafx.util.Pair;
 import lombok.val;
 import org.apache.commons.lang.ArrayUtils;
 import org.key_project.util.collection.ImmutableList;
 
+import java.util.ArrayList;
+import java.util.Collection;
 import java.util.Collections;
 import java.util.List;
 import java.util.function.Function;
@@ -117,4 +120,5 @@ public class LabelFactory {
                 })
                 .collect(Collectors.toList());
     }
+
 }

rt-key/src/main/java/edu/kit/iti/formal/psdbg/storage/KeyPersistentFacade.java

+package edu.kit.iti.formal.psdbg.storage;
+
+import de.uka.ilkd.key.control.KeYEnvironment;
+import de.uka.ilkd.key.proof.Goal;
+import de.uka.ilkd.key.proof.Node;
+import de.uka.ilkd.key.proof.Proof;
+import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
+import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
+import edu.kit.iti.formal.psdbg.interpreter.data.State;
+
+import javax.xml.bind.JAXBException;
+import java.io.IOException;
+import java.io.Reader;
+import java.io.Writer;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (16.05.18)
+ */
+public class KeyPersistentFacade {
+    public static void write(State<KeyData> state, Writer fw) throws IOException, JAXBException {
+        PersistentState ps = new PersistentState();
+        for (GoalNode<KeyData> gn : state.getGoals()) {
+            PersistentGoal pg = new PersistentGoal();
+            pg.setGoalIdentifier(WalkableLabelFacade.getCompressedWalkableLabel(gn.getData().getNode()));
+            pg.setSelected(gn == state.getSelectedGoalNode());
+            gn.getAssignments().asMap().forEach((a, b) -> {
+                pg.addVariable(a.getIdentifier(),
+                        b.getType().toString(),
+                        b.getData().toString());
+
+            });
+            ps.getGoals().add(pg);
+        }
+        PersistentFacade.write(ps, fw);
+    }
+
+    public static State<KeyData> read(KeYEnvironment env, Proof proof, Reader reader)
+            throws JAXBException {
+        PersistentState ps = PersistentFacade.read(reader);
+        State<KeyData> state = new State<>();
+        for (PersistentGoal pg : ps.getGoals()) {
+            Node node = WalkableLabelFacade.findNode(proof, pg.getGoalIdentifier());
+            Goal goal = proof.getGoal(node);
+            KeyData kd = new KeyData(goal, env, proof);
+            GoalNode<KeyData> gn = new GoalNode<>(null, kd, false);
+            state.getGoals().add(gn);
+            if (pg.isSelected())
+                state.setSelectedGoalNode(gn);
+        }
+        return state;
+    }
+}

rt-key/src/main/java/edu/kit/iti/formal/psdbg/storage/PersistentFacade.java

+package edu.kit.iti.formal.psdbg.storage;
+
+import javax.xml.bind.JAXBContext;
+import javax.xml.bind.JAXBException;
+import java.io.Reader;
+import java.io.StringReader;
+import java.io.Writer;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (16.05.18)
+ */
+public class PersistentFacade {
+    public static JAXBContext createJAXBContext() throws JAXBException {
+        JAXBContext ctx = JAXBContext.newInstance(
+                PersistentState.class,
+                PersistentGoal.class,
+                PersistentVariable.class
+        );
+        return ctx;
+    }
+
+    public static void write(PersistentState state, Writer output) throws JAXBException {
+        JAXBContext ctx = createJAXBContext();
+        ctx.createMarshaller().marshal(state, output);
+    }
+
+    public static PersistentState read(Reader file) throws JAXBException {
+        JAXBContext ctx = createJAXBContext();
+        return (PersistentState) ctx.createUnmarshaller().unmarshal(file);
+    }
+}

rt-key/src/main/java/edu/kit/iti/formal/psdbg/storage/PersistentGoal.java

+package edu.kit.iti.formal.psdbg.storage;
+
+import lombok.AllArgsConstructor;
+import lombok.Data;
+import lombok.NoArgsConstructor;
+
+import javax.xml.bind.annotation.XmlAccessType;
+import javax.xml.bind.annotation.XmlAccessorType;
+import javax.xml.bind.annotation.XmlAttribute;
+import javax.xml.bind.annotation.XmlElement;
+import java.util.ArrayList;
+import java.util.List;
+
+@Data
+@AllArgsConstructor
+@NoArgsConstructor
+@XmlAccessorType(XmlAccessType.FIELD)
+public class PersistentGoal {
+    @XmlAttribute(name = "id")
+    public String goalIdentifier;
+
+    @XmlAttribute(name = "selected")
+    private boolean selected = false;
+
+    @XmlElement
+    private List<PersistentVariable> variables = new ArrayList<>();
+
+    public void addVariable(String identifier, String type, String value) {
+        variables.add(new PersistentVariable(identifier, type, value));
+    }
+}

rt-key/src/main/java/edu/kit/iti/formal/psdbg/storage/PersistentState.java

+package edu.kit.iti.formal.psdbg.storage;
+
+import lombok.AllArgsConstructor;
+import lombok.Data;
+import lombok.NoArgsConstructor;
+import lombok.RequiredArgsConstructor;
+
+import javax.xml.bind.annotation.XmlAccessType;
+import javax.xml.bind.annotation.XmlAccessorType;
+import javax.xml.bind.annotation.XmlElement;
+import javax.xml.bind.annotation.XmlRootElement;
+import java.util.ArrayList;
+import java.util.List;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (16.05.18)
+ */
+@Data
+@AllArgsConstructor
+@NoArgsConstructor
+@XmlRootElement(name = "psdbg-state")
+@XmlAccessorType(XmlAccessType.FIELD)
+public class PersistentState {
+    @XmlElement(name = "goal")
+    private List<PersistentGoal> goals = new ArrayList<>();
+
+
+}
+

rt-key/src/main/java/edu/kit/iti/formal/psdbg/storage/PersistentVariable.java

+package edu.kit.iti.formal.psdbg.storage;
+
+import lombok.AllArgsConstructor;
+import lombok.Data;
+import lombok.NoArgsConstructor;
+
+import javax.xml.bind.annotation.XmlAccessType;
+import javax.xml.bind.annotation.XmlAccessorType;
+import javax.xml.bind.annotation.XmlAttribute;
+import javax.xml.bind.annotation.XmlElement;
+
+@Data
+@AllArgsConstructor
+@NoArgsConstructor
+@XmlAccessorType(XmlAccessType.FIELD)
+public class PersistentVariable {
+    @XmlAttribute
+    private String name, type, value;
+}
\ No newline at end of file

rt-key/src/main/java/edu/kit/iti/formal/psdbg/storage/WalkableLabelFacade.java

+package edu.kit.iti.formal.psdbg.storage;
+
+import de.uka.ilkd.key.proof.Node;
+import de.uka.ilkd.key.proof.Proof;
+import javafx.util.Pair;
+import lombok.val;
+
+import java.util.*;
+import java.util.function.Function;
+import java.util.regex.Pattern;
+import java.util.stream.Collectors;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (16.05.18)
+ */
+public class WalkableLabelFacade {
+    public static final String SUFFIX_COMPRESSED_LABEL = "}";
+    public static final String PREFIX_COMPRESSED_LABEL = "{";
+    public static final String SUFFIX_WALKABLE_LABEL = "]";
+    public static final String PREFIX_WALKABLE_LABEL = "[";
+    public static final String ENTRY_DELIMITER = ",";
+    public static final String LENGTH_DELIMITER = "|";
+
+
+    public static String getCompressedWalkableLabel(Node node) {
+        ArrayList<Integer> walk = getWalkForNode(node);
+        Collection<Pair<Integer, Integer>> cwalk = compress(walk.iterator());
+        return cwalk.stream()
+                .map(p -> p.getKey() + LENGTH_DELIMITER + p.getValue())
+                .collect(Collectors.joining(ENTRY_DELIMITER, PREFIX_COMPRESSED_LABEL, SUFFIX_COMPRESSED_LABEL));
+    }
+
+    public static String getWalkableLabel(Node node) {
+        val walk = getWalkForNode(node);
+        return walk.stream()
+                .map(Object::toString)
+                .collect(Collectors.joining(ENTRY_DELIMITER, PREFIX_WALKABLE_LABEL, SUFFIX_WALKABLE_LABEL));
+    }
+
+    static ArrayList<Integer> getWalkForNode(Node current) {
+        if (current == null) throw new IllegalArgumentException();
+        ArrayList<Integer> walk = new ArrayList<>(1024 * 16);
+
+        while (current != null) {
+            Node parent = current.parent();
+            if (parent == null) break;
+            walk.add(parent.getChildNr(current));
+            current = parent;
+        }
+        Collections.reverse(walk);
+        return walk;
+    }
+
+    static <T> Collection<T> parseUncompressed(String input, String prefix, String suffix,
+                                               String delimEntries, Function<String, T> parse) {
+        input = removePrefixAndSuffix(input, prefix, suffix);
+        Pattern reOuter = Pattern.compile(delimEntries);
+        Collection<T> seq = new ArrayList<>();
+        reOuter.splitAsStream(input).forEach(
+                chunk -> {
+                    T obj = parse.apply(chunk);
+                    seq.add(obj);
+                }
+        );
+        return seq;
+    }
+
+    private static String removePrefixAndSuffix(String input, String prefix, String suffix) {
+        if (input.startsWith(prefix))
+            input = input.substring(prefix.length());
+
+        if (input.endsWith(suffix))
+            input = input.substring(0, input.length() - suffix.length());
+        return input;
+    }
+
+    static <T> Collection<Pair<Integer, T>> parseCompressed(String input, String prefix, String suffix,
+                                                            String delimEntries, String delimLength,
+                                                            Function<String, T> parse) {
+        input = removePrefixAndSuffix(input, prefix, suffix);
+
+        Pattern reOuter = Pattern.compile(delimEntries);
+        Collection<Pair<Integer, T>> seq = new ArrayList<>();
+        reOuter.splitAsStream(input).forEach(
+                chunk -> {
+                    String s[] = chunk.split(Pattern.quote(delimLength));
+                    int length = Integer.parseInt(s[0]);
+                    T obj = parse.apply(s[1]);
+                    seq.add(new Pair<>(length, obj));
+                }
+        );
+        return seq;
+    }
+
+    /**
+     * Uncompress a given run-length encoding.
+     *
+     * @param iter
+     * @param <T>  an arbitrary type
+     * @return
+     */
+    static <T> Collection<T> uncompress(Iterator<Pair<Integer, T>> iter) {
+        List<T> seq = new ArrayList<>();
+        while (iter.hasNext()) {
+            Pair<Integer, T> p = iter.next();
+            int length = p.getKey();
+            T obj = p.getValue();
+            for (int i = 0; i < length; i++)
+                seq.add(obj);
+        }
+        return seq;
+    }
+
+    /**
+     * run length compression
+     *
+     * @param iter
+     * @param <T>
+     * @return
+     */
+    static <T> Collection<Pair<Integer, T>> compress(Iterator<T> iter) {
+        if (iter.hasNext()) {
+            List<Pair<Integer, T>> compress = new ArrayList<>();
+            T last = iter.next();
+            int length = 1;
+
+            while (iter.hasNext()) {
+                T n = iter.next();
+                if (n.equals(last)) {
+                    length++;
+                } else {
+                    compress.add(new Pair<>(length, last));
+                    last = n;
+                    length = 1;
+                }
+            }
+            compress.add(new Pair<>(length, last));
+            return compress;
+        } else {
+            return Collections.emptyList();
+        }
+    }
+
+
+    public static Node findNode(Proof proof, String identifier) {
+        if (identifier.startsWith(PREFIX_WALKABLE_LABEL)
+                && identifier.endsWith(SUFFIX_WALKABLE_LABEL)) {
+            Collection<Integer> seq =
+                    parseUncompressed(identifier, PREFIX_WALKABLE_LABEL, SUFFIX_WALKABLE_LABEL,
+                            ENTRY_DELIMITER, Integer::parseInt);
+            return findNode(proof, seq);
+        }
+
+        if (identifier.startsWith(PREFIX_COMPRESSED_LABEL)
+                && identifier.endsWith(SUFFIX_COMPRESSED_LABEL)) {
+            Collection<Pair<Integer, Integer>> seq = parseCompressed(identifier, PREFIX_COMPRESSED_LABEL, SUFFIX_COMPRESSED_LABEL,
+                    ENTRY_DELIMITER, LENGTH_DELIMITER, Integer::parseInt);
+            return findNode(proof, uncompress(seq.iterator()));
+        }
+
+        throw new IllegalArgumentException("Given identifier is a valid walkable label");
+    }
+
+    public static Node findNode(Proof proof, Collection<Integer> walk) {
+        Node current = proof.root();
+        for (Integer i : walk) {
+            current = current.child(i);
+        }
+        return current;
+    }
+}

rt-key/src/test/java/edu/kit/iti/formal/psdbg/storage/KeyPersistentFacadeTest.java

+package edu.kit.iti.formal.psdbg.storage;
+
+import de.uka.ilkd.key.api.KeYApi;
+import de.uka.ilkd.key.api.ProofApi;
+import de.uka.ilkd.key.api.ProofManagementApi;
+import de.uka.ilkd.key.control.KeYEnvironment;
+import de.uka.ilkd.key.proof.Proof;
+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.State;
+import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
+import edu.kit.iti.formal.psdbg.parser.ast.Parameters;
+import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
+import org.junit.Assert;
+import org.junit.Test;
+
+import javax.xml.bind.JAXBException;
+import java.io.File;
+import java.io.IOException;
+import java.io.StringReader;
+import java.io.StringWriter;
+import java.util.ArrayList;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (16.05.18)
+ */
+public class KeyPersistentFacadeTest {
+    @Test
+    public void testWriteReadXml() throws JAXBException {
+        StringWriter writer = new StringWriter();
+        PersistentState state = new PersistentState();
+        PersistentGoal g1 = new PersistentGoal("g1", false, new ArrayList<>());
+        PersistentGoal g2 = new PersistentGoal("g2", true, new ArrayList<>());
+        PersistentGoal g3 = new PersistentGoal("g3", false, new ArrayList<>());
+        state.getGoals().add(g1);
+        state.getGoals().add(g2);
+        state.getGoals().add(g3);
+        g1.addVariable("a", "INT", "1");
+        g2.addVariable("a", "INT", "1");
+        g3.addVariable("a", "INT", "1");
+        g2.addVariable("b", "BOOL", "FALSE");
+
+        PersistentFacade.write(state, writer);
+        String output = writer.getBuffer().toString();
+        System.out.println(output);
+        PersistentState rstate = PersistentFacade.read(new StringReader(output));
+
+        Assert.assertEquals(state, rstate);
+    }
+
+
+    @Test
+    public void testWriteReadKey() throws ProblemLoaderException, IOException, JAXBException {
+        File cp = new File("src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/contraposition.key");
+        System.out.println(cp.getAbsolutePath());
+        ProofManagementApi a = KeYApi.loadFromKeyFile(cp);
+        System.out.println("KeyPersistentFacadeTest.testWriteReadKey");
+        ProofApi b = a.getLoadedProof();
+        KeYEnvironment env = b.getEnv();
+        Proof proof = b.getProof();
+        InterpreterBuilder ib = new InterpreterBuilder();
+        KeyInterpreter inter = ib.proof(b).startState().scriptCommands().macros().build();
+        State<KeyData> state = inter.getCurrentState();
+
+        StringWriter sw = new StringWriter();
+        KeyPersistentFacade.write(state, sw);
+        System.out.println(sw.toString());
+        State<KeyData> rstate = KeyPersistentFacade.read(env, proof, new StringReader(sw.getBuffer().toString()));
+
+        ProofScript ps = new ProofScript();
+        CallStatement cs = new CallStatement("impRight", new Parameters());
+        ps.getBody().add(cs);
+        inter.interpret(ps);
+
+        sw = new StringWriter();
+        KeyPersistentFacade.write(state, sw);
+        System.out.println(sw.toString());
+        State<KeyData> state1 = KeyPersistentFacade.read(env, proof, new StringReader(sw.getBuffer().toString()));
+
+    }
+}
\ No newline at end of file

rt-key/src/test/java/edu/kit/iti/formal/psdbg/storage/WalkableLabelFacadeTest.java

+package edu.kit.iti.formal.psdbg.storage;
+
+import javafx.util.Pair;
+import org.junit.Assert;
+import org.junit.Test;
+
+import java.util.Collection;
+import java.util.Collections;
+import java.util.List;
+
+import static edu.kit.iti.formal.psdbg.storage.WalkableLabelFacade.*;
+import static java.util.Arrays.asList;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (16.05.18)
+ */
+public class WalkableLabelFacadeTest {
+    @Test
+    public void testParseUncompressed() {
+        Collection<Integer> v1 = parseUncompressed("[0,1,2,3,4,0,1,2,3,4]", PREFIX_WALKABLE_LABEL, SUFFIX_WALKABLE_LABEL, ENTRY_DELIMITER, Integer::parseInt);
+        Collection<Integer> v2 = parseUncompressed("[]", PREFIX_WALKABLE_LABEL, SUFFIX_WALKABLE_LABEL, ENTRY_DELIMITER, Integer::parseInt);
+        Collection<Integer> v3 = parseUncompressed("[-111]", PREFIX_WALKABLE_LABEL, SUFFIX_WALKABLE_LABEL, ENTRY_DELIMITER, Integer::parseInt);
+        Collection<Integer> v4 = parseUncompressed("]", PREFIX_WALKABLE_LABEL, SUFFIX_WALKABLE_LABEL, ENTRY_DELIMITER, Integer::parseInt);
+        Collection<Integer> v5 = parseUncompressed("", PREFIX_WALKABLE_LABEL, SUFFIX_WALKABLE_LABEL, ENTRY_DELIMITER, Integer::parseInt);
+
+        Assert.assertEquals(asList(0, 1, 2, 3, 4, 0, 1, 2, 3, 4), v1);
+        Assert.assertEquals(Collections.emptyList(), v2);
+        Assert.assertEquals(asList(-111), v3);
+        Assert.assertEquals(Collections.emptyList(), v4);
+        Assert.assertEquals(Collections.emptyList(), v5);
+    }
+
+    @Test
+    public void testCompression() {
+        List<Integer> list = asList(0, 0, 0, 0, 1, 1, 1, 1, 1, 10, 0, 0, 1, 1, 1, 10, 0, 2, 2, 4);
+        List<Integer> list1 = Collections.singletonList(0);
+        List<Integer> list0 = Collections.emptyList();
+        List<Integer> list2 = asList(1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1);
+
+        compressAndUncompress(list);
+        compressAndUncompress(list1);
+        compressAndUncompress(list0);
+        compressAndUncompress(list2);
+
+        System.out.println(compress(list.iterator()));
+        System.out.println(compress(list1.iterator()));
+        System.out.println(compress(list2.iterator()));
+        System.out.println(compress(list0.iterator()));
+
+        Assert.assertEquals(
+                "[4=0, 5=1, 1=10, 2=0, 3=1, 1=10, 1=0, 2=2, 1=4]",
+                compress(list.iterator()).toString());
+
+        Assert.assertEquals("[1=0]", compress(list1.iterator()).toString());
+        Assert.assertEquals("[16=1]", compress(list2.iterator()).toString());
+        Assert.assertEquals("[]", compress(list0.iterator()).toString());
+    }
+
+    public void compressAndUncompress(List<Integer> list) {
+        Collection<Pair<Integer, Integer>> clist = compress(list.iterator());
+        Collection<Integer> uclist = uncompress(clist.iterator());
+        Assert.assertEquals(list, uclist);
+    }
+}
\ No newline at end of file