Commit 6ddf4f97 authored by Alexander Weigl's avatar Alexander Weigl 🐼
Browse files

Merge branch 'weigl-sync' into 'master'

Everything new! Everything Better Now!!

See merge request !4
parents e6361f70 4ed3bd10
Pipeline #15115 passed with stages
in 6 minutes and 42 seconds
script A() {
A;
B;
C;
cases {
case x=2:
a;
}
}
script A() {
A;
B;
C;
F;
}
script A() {
E;F;
}
......@@ -77,8 +77,6 @@
</distributionManagement>
<build>
<extensions>
<extension>
......@@ -160,6 +158,9 @@
<version>1.12</version>
<configuration>
<licenseName>gpl_v3</licenseName>
<copyrightOwners>
Sarah Grebing, Alexander Weigl
</copyrightOwners>
</configuration>
</plugin>
......@@ -174,6 +175,66 @@
<useIncrementalCompilation>false</useIncrementalCompilation>
</configuration>
</plugin>
<!--
<plugin>
<artifactId>maven-assembly-plugin</artifactId>
<executions>
<execution>
<id>make-assembly</id>
<phase>package</phase>
<goals>
<goal>single</goal>
</goals>
</execution>
</executions>
<configuration>
<archive>
<manifest>
<mainClass>edu.kit.iti.formal.psdbg.gui.ProofScriptDebugger</mainClass>
</manifest>
</archive>
<descriptorRefs>
<descriptorRef>exe</descriptorRef>
</descriptorRefs>
</configuration>
</plugin>
-->
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-javadoc-plugin</artifactId>
<version>2.9</version>
<executions>
<execution>
<id>attach-javadocs</id>
<goals>
<goal>jar</goal>
</goals>
<configuration>
<additionalparam>-Xdoclint:none</additionalparam>
</configuration>
</execution>
</executions>
</plugin>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-site-plugin</artifactId>
<version>3.3</version>
<configuration>
<reportPlugins>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-javadoc-plugin</artifactId>
<configuration>
<additionalparam>-Xdoclint:none</additionalparam>
</configuration>
</plugin>
</reportPlugins>
</configuration>
</plugin>
</plugins>
</build>
......
package edu.kit.iti.formal.psdbg;
import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerCommand;
import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerFramework;
public class HardStopCommand<T> extends DebuggerCommand<T> {
@Override
public void execute(DebuggerFramework<T> dbg) {
}
}
package edu.kit.iti.formal.psdbg;
import de.uka.ilkd.key.api.KeYApi;
import de.uka.ilkd.key.api.ProofManagementApi;
import de.uka.ilkd.key.proof.io.ProblemLoaderException;
import de.uka.ilkd.key.util.KeYConstants;
import edu.kit.iti.formal.psdbg.interpreter.InterpreterBuilder;
import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
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.dbg.*;
import edu.kit.iti.formal.psdbg.parser.Facade;
import edu.kit.iti.formal.psdbg.parser.ast.*;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import java.io.BufferedReader;
import java.io.File;
import java.io.IOException;
import java.io.InputStreamReader;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
/**
* @author Alexander Weigl
* @version 1 (27.10.17)
*/
public class InteractiveCLIDebugger {
private static final Logger LOGGER = LogManager.getLogger();
static Map<String, DebuggerCommand<KeyData>> COMMANDS = new HashMap<>();
static {
COMMANDS.put("r", new ReturnCommand());
COMMANDS.put("s", new StartCommand<>(true));
COMMANDS.put("<", new StepBackCommand<>());
COMMANDS.put(">", new StepOverCommand<>());
COMMANDS.put(".", new StepIntoCommand<>());
COMMANDS.put(";", new HardStopCommand<>());
COMMANDS.put(";", new PauseCommand<>());
}
private final ProofManagementApi pma;
private final KeyInterpreter interpreter;
private final DebuggerFramework<KeyData> df;
public InteractiveCLIDebugger(String proof, String script) throws IOException, ProblemLoaderException, DebuggerException {
pma = KeYApi.loadFromKeyFile(new File(proof));
List<ProofScript> scripts = Facade.getAST(new File(script));
InterpreterBuilder ib = new InterpreterBuilder()
.addProofScripts(scripts)
.proof(pma.getLoadedProof())
.startState()
.macros()
.scriptCommands()
.scriptSearchPath(new File("."));
interpreter = ib.build();
//ControlFlowVisitor cfgVistor = new ControlFlowVisitor(ib.getLookup());
//MutableValueGraph<ControlFlowNode, ControlFlowTypes> cfg = cfgVistor.getGraph();
df = new DebuggerFramework<>(interpreter, scripts.get(0), null);
df.getStatePointerListener().add(this::printNode);
//df.getBeforeExecutionListener().add(this::printNode);
//df.getAfterExecutionListener().add(this::end);
loop();
}
public static void main(String[] args) throws ProblemLoaderException, IOException, DebuggerException {
System.out.println("Welcome to Psdbg with KeY" + KeYConstants.INTERNAL_VERSION);
LOGGER.info("KeY Version: {}", KeYConstants.INTERNAL_VERSION);
Runtime.getRuntime().addShutdownHook(new Thread(() -> LOGGER.info("Program exited")));
new InteractiveCLIDebugger(args[0], args[1]);
}
private void debug() {
//TODO write debug information
System.out.println("digraph G {");
for (PTreeNode<KeyData> n : df.getStates()) {
System.out.format("%d [label=\"%s@%s (G: %d)\"]%n", n.hashCode(),
n.getStatement().accept(new ShortCommandPrinter()),
n.getStatement().getStartPosition().getLineNumber(),
n.getStateBeforeStmt().getGoals().size()
);
if (n.getStepOver() != null)
System.out.format("%d -> %d [label=\"SO\"]%n", n.hashCode(), n.getStepOver().hashCode());
if (n.getStepInto() != null)
System.out.format("%d -> %d [label=\"SI\"]%n", n.hashCode(), n.getStepInto().hashCode());
if (n.getStepInvOver() != null)
System.out.format("%d -> %d [label=\"<SO\"]%n", n.hashCode(), n.getStepInvOver().hashCode());
if (n.getStepInvInto() != null)
System.out.format("%d -> %d [label=\"<SI\"]%n", n.hashCode(), n.getStepInvInto().hashCode());
if (n.getStepReturn() != null)
System.out.format("%d -> %d [label=\"R\"]%n", n.hashCode(), n.getStepReturn().hashCode());
}
System.out.println("}");
}
private void loop() throws DebuggerException {
try (BufferedReader br = new BufferedReader(new InputStreamReader(System.in))) {
while (true) {
int counter = 0;
while (true) {
boolean handled = false;
System.out.printf("dbg (%03d)> ", ++counter);
String input = br.readLine().trim().intern();
if (COMMANDS.containsKey(input)) {
handled = true;
try {
df.execute(COMMANDS.get(input));
} catch (DebuggerException e) {
if (e.isSevere())
throw e;
else {
System.err.println(e.getMessage());
}
}
}
//special
switch (input) {
case "!!":
System.exit(0);
case "dbg":
handled = true;
debug();
}
if (input.startsWith("b ")) {
handled = true;
setBreakpoint(Integer.parseInt(input.substring(2)));
}
if (!handled) System.err.println("Unknown command");
}
}
} catch (IOException e) {
e.printStackTrace();
}
}
private void end(PTreeNode<KeyData> keyDataPTreeNode) {
//TODO register if proof has ended!
}
private void printNode(PTreeNode<KeyData> node) {
System.out.format("%3d: %s%n",
node.getStatement().getStartPosition().getLineNumber(),
node.getStatement().accept(new ShortCommandPrinter())
);
for (GoalNode<KeyData> gn : node.getStateBeforeStmt().getGoals()) {
if (gn.equals(node.getStateBeforeStmt().getSelectedGoalNode()))
System.out.format("\t* ");
else
System.out.format("\t ");
System.out.println(gn.getData().getNode().sequent());
}
}
public void setBreakpoint(int breakpoint) {
//df.addBreakpoint(breakpoint);
}
}
package edu.kit.iti.formal.psdbg;
import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerCommand;
import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerFramework;
public class PauseCommand<T> extends DebuggerCommand<T> {
@Override
public void execute(DebuggerFramework<T> dbg) {
}
}
package edu.kit.iti.formal.psdbg;
import edu.kit.iti.formal.psdbg.interpreter.dbg.Blocker;
import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerCommand;
import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerException;
import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerFramework;
import lombok.AllArgsConstructor;
import lombok.*;
@AllArgsConstructor
public class StartCommand<T> extends DebuggerCommand<T> {
@Getter @Setter
private boolean directStop = true;
@Override
public void execute(DebuggerFramework<T> dbg) throws DebuggerException {
dbg.releaseUntil(new Blocker.CounterBlocker(1));
dbg.start();
}
}
package edu.kit.iti.formal.psdbg;
import edu.kit.iti.formal.psdbg.interpreter.dbg.*;
public class StepIntoCommand<T> extends DebuggerCommand<T> {
@Override
public void execute(DebuggerFramework<T> dbg) {
PTreeNode<T> statePointer = dbg.getStatePointer();
assert statePointer != null;
if (statePointer.isAtomic()) {
new StepOverCommand<T>().execute(dbg);
} else {
dbg.releaseUntil(new Blocker.CounterBlocker(1));
}
}
}
......@@ -117,7 +117,7 @@ public class InterpreterBuilder {
}
public InterpreterBuilder onEntry(Visitor v) {
interpreter.getEntryListeners().add(v);
interpreter.getEntryListeners().add(0, v);
return this;
}
......@@ -144,6 +144,8 @@ public class InterpreterBuilder {
public InterpreterBuilder proof(ProofApi pa) {
addKeyMatcher(pa);
pa.getRules().forEach(s -> pmr.getRules().put(s, null));
keyEnvironment = pa.getEnv();
proof = pa.getProof();
return this;
}
......
......@@ -238,8 +238,8 @@ public class KeYMatcher implements MatcherApi<KeyData> {
@Override
public List<VariableAssignment> matchSeq(GoalNode<KeyData> currentState, String data, Signature sig) {
System.out.println("State that will be matched " + currentState.getData().getNode().sequent() + " with pattern " + data);
System.out.println("Signature " + sig.toString());
//System.out.println("State that will be matched " + currentState.getData().getNode().sequent() + " with pattern " + data);
//System.out.println("Signature " + sig.toString());
Matchings m = MatcherFacade.matches(data, currentState.getData().getNode().sequent());
......
......@@ -50,9 +50,36 @@ public class KeYProofFacade {
* BooleanProperty inidcating whether KeY finished loading
*/
private BooleanBinding readyToExecute = proof.isNotNull();
//Workaround until api is relaxed
private ProofManagementApi pma;
/**
*
*/
public ProofState getProofState() {
Proof p = proof.get();
if (p == null)
return ProofState.EMPTY;
if (p.root().childrenCount() == 0)
return ProofState.VIRGIN;
return ProofState.DIRTY;
}
/**
* reload the current proof. synchronously because only the first load is slow.
*/
public void reload(File problemFile) throws ProofInputException, ProblemLoaderException {
if (contract.get() != null) {// reinstante the contract
setProof(getEnvironment().createProof(
contract.get().getProofObl(getEnvironment().getServices())));
} else {
setProof(KeYApi.loadFromKeyFile(problemFile).getLoadedProof().getProof());
}
}
//region loading
public Task<ProofApi> loadKeyFileTask(File keYFile) {
Task<ProofApi> task = new Task<ProofApi>() {
......@@ -117,14 +144,13 @@ public class KeYProofFacade {
proof.set(pa.getProof());
contract.set(null);
}
//endregion
/**
* Build the KeYInterpreter that handles the execution of the loaded key problem sourceName
*/
public InterpreterBuilder buildInterpreter() {
assert readyToExecute.getValue();
assert getEnvironment() != null && getProof() != null : "No proof loaded";
InterpreterBuilder interpreterBuilder = new InterpreterBuilder();
interpreterBuilder
.proof(environment.get(), proof.get())
......@@ -136,7 +162,7 @@ public class KeYProofFacade {
return interpreterBuilder;
}
//endregion
/**
* Reload all KeY structure if proof should be reloaded
......@@ -202,6 +228,21 @@ public class KeYProofFacade {
KeyData data = new KeyData(proof.get().root(), getEnvironment(), getProof());
return Collections.singleton(new GoalNode<>(null, data, data.getNode().isClosed()));
}
public enum ProofState {
/**
* There is no KeY Proof actually loaded.
*/
EMPTY,
/**
* The loaded KeY Proof is untouched iff there is only one node --- the root.
*/
VIRGIN,
/**
* The KeY Proof was ravished by Taclets and other stuff.
*/
DIRTY;
}
//endregion
}
......@@ -4,18 +4,19 @@ import com.google.common.collect.BiMap;
import com.google.common.collect.ImmutableBiMap;
import de.uka.ilkd.key.api.ScriptApi;
import de.uka.ilkd.key.api.VariableAssignments;
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 edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.interpreter.funchdl.CommandLookup;
import edu.kit.iti.formal.psdbg.parser.Visitor;
import edu.kit.iti.formal.psdbg.parser.ast.ClosesCase;
import edu.kit.iti.formal.psdbg.parser.ast.Statements;
import edu.kit.iti.formal.psdbg.parser.ast.TryCase;
import edu.kit.iti.formal.psdbg.parser.types.SimpleType;
import lombok.Getter;
import org.key_project.util.collection.ImmutableList;
import java.util.List;
......@@ -35,26 +36,26 @@ public class KeyInterpreter extends Interpreter<KeyData> {
.put(SimpleType.INT_ARRAY, VariableAssignments.VarType.INT_ARRAY)
.put(SimpleType.SEQ, VariableAssignments.VarType.SEQ)
.build();
@Getter
private ScriptApi scriptApi;
public KeyInterpreter(CommandLookup lookup) {
super(lookup);
}
@Override
public Object visit(ClosesCase closesCase) {
/*
State<KeyData> currentStateToMatch = peekState();
State<KeyData> currentStateToMatchCopy = currentStateToMatch.copy(); //deepcopy
GoalNode<KeyData> selectedGoalNode = currentStateToMatch.getSelectedGoalNode();
GoalNode<KeyData> selectedGoalCopy = currentStateToMatch.getSelectedGoalNode().deepCopy(); //deepcopy
*/
enterScope(closesCase);
//execute closesscript
executeBody(closesCase.getClosesScript(), selectedGoalNode, new VariableAssignment(selectedGoalNode.getAssignments()));
boolean closed = suspicionExecution(closesCase.getClosesGuard(), true);
//executeBody(closesCase.getClosesGuard(), selectedGoalNode, new VariableAssignment(selectedGoalNode.getAssignments()));
//check whether script closed proof
State<KeyData> stateafterIsClosable = peekState();
/*State<KeyData> stateafterIsClosable = peekState();
List<GoalNode<KeyData>> goals = stateafterIsClosable.getGoals();
boolean allClosed = true;
for (GoalNode<KeyData> goal : goals) {
......@@ -65,7 +66,7 @@ public class KeyInterpreter extends Interpreter<KeyData> {
}
}
//prune proof
System.out.println("The closes script " + (allClosed ? "closed the proof.\n" : "did not close the proof.\n") + "Rolling Back proof now.");
logger.debug("The closes script " + (allClosed ? "closed the proof.\n" : "did not close the proof.\n") + "Rolling Back proof now.");
Proof currentKeYproof = selectedGoalNode.getData().getProof();
ImmutableList<Goal> subtreeGoals = currentKeYproof.getSubtreeGoals(((KeyData) selectedGoalNode.getData()).getNode());
currentKeYproof.pruneProof(selectedGoalCopy.getData().getNode());
......@@ -73,73 +74,57 @@ public class KeyInterpreter extends Interpreter<KeyData> {
pushState(currentStateToMatchCopy);
exitScope(closesCase);
return allClosed;
*/
exitScope(closesCase);
return closed;
}
@Override
public Object visit(TryCase tryCase) {
State<KeyData> currentStateToMatch = peekState();
State<KeyData> currentStateToMatchCopy = currentStateToMatch.copy(); //deepcopy
GoalNode<KeyData> selectedGoalNode = currentStateToMatch.getSelectedGoalNode();
GoalNode<KeyData> selectedGoalCopy = currentStateToMatch.getSelectedGoalNode().deepCopy(); //deepcopy
//historylistener for recording try
logger.info(String.format("Beginning side computation of %s", tryCase.getNodeName()));
startSideComputation();
TryCaseHistoryLogger list = new TryCaseHistoryLogger(this);
enterScope(tryCase);
boolean b = suspicionExecution(tryCase.getBody(), false);
exitScope(tryCase);
return b;
}
executeBody(tryCase.getBody(), selectedGoalNode, new VariableAssignment(selectedGoalNode.getAssignments()));
State<KeyData> stateafterIsClosable = peekState();
List<GoalNode<KeyData>> goals = stateafterIsClosable.getGoals();
boolean allClosed = true;
for (GoalNode<KeyData> goal : goals) {
KeyData data = (KeyData) goal.getData();
if (!data.getNode().isClosed()) {
allClosed = false;
break;
}
}
logger.info(String.format("Ended Side Computation of %s", tryCase.getNodeName()));
endSideComputation();
if (!allClosed) {
logger.info("Try was not successful, rolling back proof");
Proof currentKeYproof = selectedGoalNode.getData().getProof();
ImmutableList<Goal> subtreeGoals = currentKeYproof.getSubtreeGoals(((KeyData) selectedGoalNode.getData()).getNode());
currentKeYproof.pruneProof(selectedGoalCopy.getData().getNode());
popState();
pushState(currentStateToMatchCopy);
} else {
//replay all proof events
//check if state is closed
exitScope(tryCase);
list.printSequenceOfEvents();
list.replayEvents(this);
logger.info("Replaying Events finished");
}
return allClosed;
/* //executeBody and if goal is closed afterwards return true
//else prune proof and return false
State<T> stateBeforeTry = peekState().copy();