Commit caab9b9a authored by alexander.weigl's avatar alexander.weigl 🐼

Persistence of interpreter state

parent 9f895c89
...@@ -39,27 +39,4 @@ subprojects { ...@@ -39,27 +39,4 @@ subprojects {
//compileOnly group: 'org.projectlombok', name: 'lombok', version: '1.16.20' //compileOnly group: 'org.projectlombok', name: 'lombok', version: '1.16.20'
compileOnly files("$rootDir/lombok-edge.jar") 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"
])*/
}
} }
...@@ -3,10 +3,13 @@ package edu.kit.iti.formal.psdbg; ...@@ -3,10 +3,13 @@ package edu.kit.iti.formal.psdbg;
import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.Proof;
import javafx.util.Pair;
import lombok.val; import lombok.val;
import org.apache.commons.lang.ArrayUtils; import org.apache.commons.lang.ArrayUtils;
import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableList;
import java.util.ArrayList;
import java.util.Collection;
import java.util.Collections; import java.util.Collections;
import java.util.List; import java.util.List;
import java.util.function.Function; import java.util.function.Function;
...@@ -117,4 +120,5 @@ public class LabelFactory { ...@@ -117,4 +120,5 @@ public class LabelFactory {
}) })
.collect(Collectors.toList()); .collect(Collectors.toList());
} }
} }
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;
}
}
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);
}
}
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));
}
}
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<>();
}
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
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;
}
}
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
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
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment