Commit f15159ee authored by Sarah Grebing's avatar Sarah Grebing

Interim (incomplete commit)

parent 444581f3
Pipeline #11567 failed with stage
in 2 minutes and 23 seconds
...@@ -4,10 +4,7 @@ import de.uka.ilkd.key.proof.init.ProofInputException; ...@@ -4,10 +4,7 @@ import de.uka.ilkd.key.proof.init.ProofInputException;
import de.uka.ilkd.key.speclang.Contract; import de.uka.ilkd.key.speclang.Contract;
import edu.kit.formal.gui.controls.*; import edu.kit.formal.gui.controls.*;
import edu.kit.formal.gui.model.RootModel; import edu.kit.formal.gui.model.RootModel;
import edu.kit.formal.interpreter.Interpreter; import edu.kit.formal.interpreter.*;
import edu.kit.formal.interpreter.InterpreterBuilder;
import edu.kit.formal.interpreter.KeYProofFacade;
import edu.kit.formal.interpreter.ProofTreeController;
import edu.kit.formal.interpreter.data.KeyData; import edu.kit.formal.interpreter.data.KeyData;
import edu.kit.formal.interpreter.data.State; import edu.kit.formal.interpreter.data.State;
import edu.kit.formal.proofscriptparser.Facade; import edu.kit.formal.proofscriptparser.Facade;
...@@ -113,6 +110,7 @@ public class DebuggerMainWindowController implements Initializable { ...@@ -113,6 +110,7 @@ public class DebuggerMainWindowController implements Initializable {
private ObservableBooleanValue executeNotPossible = interpreterService.runningProperty().or(facade.readyToExecuteProperty().not()); private ObservableBooleanValue executeNotPossible = interpreterService.runningProperty().or(facade.readyToExecuteProperty().not());
private ProofTreeController pc;
public static void showExceptionDialog(String title, String headerText, String contentText, Throwable ex) { public static void showExceptionDialog(String title, String headerText, String contentText, Throwable ex) {
Alert alert = new Alert(Alert.AlertType.ERROR); Alert alert = new Alert(Alert.AlertType.ERROR);
alert.setTitle(title); alert.setTitle(title);
...@@ -225,8 +223,11 @@ public class DebuggerMainWindowController implements Initializable { ...@@ -225,8 +223,11 @@ public class DebuggerMainWindowController implements Initializable {
Interpreter<KeyData> currentInterpreter = ib.build(); Interpreter<KeyData> currentInterpreter = ib.build();
if (debugMode) { if (debugMode) {
ProofTreeController pc = new ProofTreeController(currentInterpreter, scripts.get(0)); blocker.getStepUntilBlock().set(1);
//blocker.getStepUntilBlock().set(1); //for stepping functionality
StateGraphVisitor visitor = new StateGraphVisitor(currentInterpreter, scripts.get(0));
pc = new ProofTreeController(currentInterpreter, scripts.get(0), visitor);
currentInterpreter.getEntryListeners().add(visitor);
} }
blocker.install(currentInterpreter); blocker.install(currentInterpreter);
...@@ -386,11 +387,13 @@ public class DebuggerMainWindowController implements Initializable { ...@@ -386,11 +387,13 @@ public class DebuggerMainWindowController implements Initializable {
public void stepOver(ActionEvent actionEvent) { public void stepOver(ActionEvent actionEvent) {
blocker.getStepUntilBlock().addAndGet(1); blocker.getStepUntilBlock().addAndGet(1);
blocker.unlock(); blocker.unlock();
pc.stepOver();
} }
public void stepBack(ActionEvent actionEvent) { public void stepBack(ActionEvent actionEvent) {
System.out.println(blocker.getHistoryLogger()); System.out.println(blocker.getHistoryLogger());
blocker.unlock(); blocker.unlock();
pc.stepBack();
} }
......
...@@ -5,20 +5,21 @@ import edu.kit.formal.proofscriptparser.ast.ASTNode; ...@@ -5,20 +5,21 @@ import edu.kit.formal.proofscriptparser.ast.ASTNode;
/** /**
* ControlFlowNode for ControlFlowGraph to look up step-edges for teh debugger. * ControlFlowNode for ControlFlowGraph to look up step-edges for teh debugger.
*/ */
@Deprecated
public class ControlFlowNode { public class ControlFlowNode {
ASTNode scriptstmt; edu.kit.formal.proofscriptparser.ast.ASTNode scriptstmt;
public ControlFlowNode(ASTNode node) { public ControlFlowNode(ASTNode node) {
this.setScriptstmt(node); this.setScriptstmt(node);
} }
public ASTNode getScriptstmt() { public edu.kit.formal.proofscriptparser.ast.ASTNode getScriptstmt() {
return scriptstmt; return scriptstmt;
} }
public void setScriptstmt(ASTNode scriptstmt) { public void setScriptstmt(edu.kit.formal.proofscriptparser.ast.ASTNode scriptstmt) {
this.scriptstmt = scriptstmt; this.scriptstmt = scriptstmt;
} }
...@@ -34,4 +35,5 @@ public class ControlFlowNode { ...@@ -34,4 +35,5 @@ public class ControlFlowNode {
return sb.toString(); return sb.toString();
} }
} }
...@@ -4,5 +4,5 @@ package edu.kit.formal.interpreter; ...@@ -4,5 +4,5 @@ package edu.kit.formal.interpreter;
* Created by sarah on 6/20/17. * Created by sarah on 6/20/17.
*/ */
public enum EdgeTypes { public enum EdgeTypes {
STEP_INTO, STEP_OVER, STEP_BACK, STEP_RETURN; STEP_INTO, STEP_OVER, STEP_BACK, STEP_RETURN, STEP_OVER_COND, STATE_FLOW;
} }
package edu.kit.formal.interpreter; package edu.kit.formal.interpreter;
import edu.kit.formal.interpreter.data.GoalNode;
import edu.kit.formal.interpreter.data.KeyData; import edu.kit.formal.interpreter.data.KeyData;
import edu.kit.formal.interpreter.data.State; import edu.kit.formal.interpreter.data.State;
import edu.kit.formal.proofscriptparser.ast.ASTNode; import edu.kit.formal.proofscriptparser.ast.ASTNode;
...@@ -10,7 +9,7 @@ import edu.kit.formal.proofscriptparser.ast.ASTNode; ...@@ -10,7 +9,7 @@ import edu.kit.formal.proofscriptparser.ast.ASTNode;
* A node contains a reference to the ASTNode and a reference to the corresponding interpreter state if this state is already interpreted, null otherwise. * A node contains a reference to the ASTNode and a reference to the corresponding interpreter state if this state is already interpreted, null otherwise.
*/ */
public class PTreeNode { public class PTreeNode {
State<GoalNode<KeyData>> state; State<KeyData> state;
ASTNode scriptstmt; ASTNode scriptstmt;
...@@ -18,11 +17,11 @@ public class PTreeNode { ...@@ -18,11 +17,11 @@ public class PTreeNode {
this.setScriptstmt(node); this.setScriptstmt(node);
} }
public State<GoalNode<KeyData>> getState() { public State<KeyData> getState() {
return state; return state;
} }
public void setState(State<GoalNode<KeyData>> state) { public void setState(State<KeyData> state) {
this.state = state; this.state = state;
} }
...@@ -42,10 +41,15 @@ public class PTreeNode { ...@@ -42,10 +41,15 @@ public class PTreeNode {
StringBuilder sb = new StringBuilder(); StringBuilder sb = new StringBuilder();
sb.append("Node {"); sb.append("Node {");
if (scriptstmt != null) { if (scriptstmt != null) {
sb.append(scriptstmt.toString()); sb.append(scriptstmt.getNodeName() + "\n");
} else { } else {
sb.append("No Stmt"); sb.append("No Stmt");
} }
if (hasState()) {
sb.append("\nState " + state.getGoals() + "\n");
} else {
sb.append("No State yet");
}
sb.append("}"); sb.append("}");
return sb.toString(); return sb.toString();
} }
......
...@@ -2,50 +2,60 @@ package edu.kit.formal.interpreter; ...@@ -2,50 +2,60 @@ package edu.kit.formal.interpreter;
import com.google.common.graph.MutableValueGraph; import com.google.common.graph.MutableValueGraph;
import com.google.common.graph.ValueGraphBuilder; import com.google.common.graph.ValueGraphBuilder;
import edu.kit.formal.interpreter.data.KeyData;
import edu.kit.formal.interpreter.funchdl.CommandLookup; import edu.kit.formal.interpreter.funchdl.CommandLookup;
import edu.kit.formal.interpreter.funchdl.ProofScriptHandler; import edu.kit.formal.interpreter.funchdl.ProofScriptHandler;
import edu.kit.formal.proofscriptparser.DefaultASTVisitor; import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
import edu.kit.formal.proofscriptparser.ast.*; import edu.kit.formal.proofscriptparser.ast.*;
import java.util.List;
/** /**
* Visitor to create ProgramFlowGraph * Visitor to create ProgramFlowGraph
*/ */
public class ProgramFlowVisitor extends DefaultASTVisitor<Void> { public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
/**
* Lookup for names of scripts
*/
private final CommandLookup functionLookup; private final CommandLookup functionLookup;
private ControlFlowNode lastNode;
private MutableValueGraph<ControlFlowNode, EdgeTypes> graph = ValueGraphBuilder.directed().allowsSelfLoops(true).build(); /**
* Last visited Node
*/
private ASTNode lastNode;
/**
* Control Flow Graph
*/
private MutableValueGraph<ASTNode, EdgeTypes> graph = ValueGraphBuilder.directed().allowsSelfLoops(true).build();
private Interpreter<KeyData> inter;
public ProgramFlowVisitor(CommandLookup functionLookup) { public ProgramFlowVisitor(CommandLookup functionLookup) {
this.functionLookup = functionLookup; this.functionLookup = functionLookup;
} }
public MutableValueGraph<ControlFlowNode, EdgeTypes> getGraph() { public MutableValueGraph<ASTNode, EdgeTypes> getGraph() {
return graph; return graph;
} }
@Override @Override
public Void visit(ProofScript proofScript) { public Void visit(ProofScript proofScript) {
ControlFlowNode scriptNode = new ControlFlowNode(proofScript);
lastNode = scriptNode; lastNode = proofScript;
return this.visit(proofScript.getBody()); return this.visit(proofScript.getBody());
} }
@Override @Override
public Void visit(AssignmentStatement assignment) { public Void visit(AssignmentStatement assignment) {
ControlFlowNode node = new ControlFlowNode(assignment);
graph.addNode(node); graph.addNode(assignment);
lastNode = node; lastNode = assignment;
return null; return null;
} }
@Override @Override
public Void visit(Statements statements) { public Void visit(Statements statements) {
ControlFlowNode curLastNode = lastNode; ASTNode curLastNode = lastNode;
for (Statement stmnt : statements) { for (Statement stmnt : statements) {
stmnt.accept(this); stmnt.accept(this);
graph.putEdgeValue(curLastNode, lastNode, EdgeTypes.STEP_OVER); graph.putEdgeValue(curLastNode, lastNode, EdgeTypes.STEP_OVER);
...@@ -58,7 +68,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> { ...@@ -58,7 +68,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
@Override @Override
public Void visit(CallStatement call) { public Void visit(CallStatement call) {
ControlFlowNode currentNode = new ControlFlowNode(call); ASTNode currentNode = call;
graph.addNode(currentNode); graph.addNode(currentNode);
graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER); graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER);
...@@ -73,14 +83,15 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> { ...@@ -73,14 +83,15 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
//Annahme: wenn ich zwischendrin keine return kante habe, dann wird solange durchgegangen, bis eine return kante da ist //Annahme: wenn ich zwischendrin keine return kante habe, dann wird solange durchgegangen, bis eine return kante da ist
if (atomic) { if (atomic) {
graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_INTO);
// graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN); // graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN);
ProofScriptHandler psh = (ProofScriptHandler) functionLookup.getBuilder(call); ProofScriptHandler psh = (ProofScriptHandler) functionLookup.getBuilder(call);
psh.getScript(call.getCommand()).getBody().accept(this); psh.getScript(call.getCommand()).getBody().accept(this);
//verbinde letzten knoten aus auruf mi step return zu aktuellem knoten //verbinde letzten knoten aus auruf mit step return zu aktuellem knoten
graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN); graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN);
graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_INTO);
} }
lastNode = currentNode; lastNode = currentNode;
...@@ -90,30 +101,62 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> { ...@@ -90,30 +101,62 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
@Override @Override
public Void visit(ForeachStatement foreach) { public Void visit(ForeachStatement foreach) {
ControlFlowNode currentNode = new ControlFlowNode(foreach); ASTNode currentNode = foreach;
graph.addNode(currentNode); graph.addNode(currentNode);
graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER); graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER);
graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_BACK); graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_BACK);
lastNode = currentNode; lastNode = currentNode;
foreach.getBody().accept(this); foreach.getBody().accept(this);
graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_RETURN); graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN);
lastNode = currentNode; //lastNode = currentNode; ??
return null; return null;
} }
@Override @Override
public Void visit(TheOnlyStatement theOnly) { public Void visit(TheOnlyStatement theOnly) {
return super.visit(theOnly); ASTNode currentNode = theOnly;
graph.addNode(currentNode);
graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER);
graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_BACK);
lastNode = currentNode;
theOnly.getBody().accept(this);
graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN);
//lastNode = currentNode; ??
return null;
} }
@Override @Override
public Void visit(RepeatStatement repeatStatement) { public Void visit(RepeatStatement repeatStatement) {
return super.visit(repeatStatement); ASTNode currentNode = repeatStatement;
graph.addNode(currentNode);
graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER);
graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_BACK);
lastNode = currentNode;
repeatStatement.getBody().accept(this);
graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER);
lastNode = currentNode;
return null;
} }
@Override @Override
public Void visit(CasesStatement casesStatement) { public Void visit(CasesStatement casesStatement) {
return super.visit(casesStatement); ASTNode currentNode = casesStatement;
graph.addNode(currentNode);
graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER);
graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_BACK);
List<CaseStatement> cases = casesStatement.getCases();
for (CaseStatement aCase : cases) {
ASTNode caseNode = aCase;
graph.addNode(caseNode);
graph.putEdgeValue(currentNode, caseNode, EdgeTypes.STEP_OVER); //??is this right?
graph.putEdgeValue(caseNode, currentNode, EdgeTypes.STEP_BACK);
lastNode = caseNode;
aCase.getBody().accept(this);
graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN);
}
lastNode = currentNode;
return null;
} }
...@@ -124,9 +167,9 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> { ...@@ -124,9 +167,9 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
graph.nodes().forEach(n -> { graph.nodes().forEach(n -> {
sb.append(n.hashCode()) sb.append(n.hashCode())
.append(" [label=\"") .append(" [label=\"")
.append(n.getScriptstmt().getNodeName()) .append(n.getNodeName())
.append("@") .append("@")
.append(n.getScriptstmt().getStartPosition().getLineNumber()) .append(n.getStartPosition().getLineNumber())
.append("\"]\n"); .append("\"]\n");
}); });
......
...@@ -2,6 +2,7 @@ package edu.kit.formal.interpreter; ...@@ -2,6 +2,7 @@ package edu.kit.formal.interpreter;
import com.google.common.graph.MutableValueGraph; import com.google.common.graph.MutableValueGraph;
import edu.kit.formal.interpreter.data.KeyData; import edu.kit.formal.interpreter.data.KeyData;
import edu.kit.formal.proofscriptparser.ast.ASTNode;
import edu.kit.formal.proofscriptparser.ast.ProofScript; import edu.kit.formal.proofscriptparser.ast.ProofScript;
/** /**
...@@ -10,30 +11,34 @@ import edu.kit.formal.proofscriptparser.ast.ProofScript; ...@@ -10,30 +11,34 @@ import edu.kit.formal.proofscriptparser.ast.ProofScript;
* @author S. Grebing * @author S. Grebing
*/ */
public class ProofTreeController { public class ProofTreeController {
//TODO Listener auf den Interperter
StateGraphVisitor stateGraphVisitor;
/** /**
* ControlFlowGraph to lookup edges * ControlFlowGraph to lookup edges
*/ */
private MutableValueGraph<ControlFlowNode, EdgeTypes> controlFlowGraph; private MutableValueGraph<ASTNode, EdgeTypes> controlFlowGraph;
/** /**
* Graph that is computed on the fly in order to allow stepping * Graph that is computed on the fly in order to allow stepping
*/ */
private MutableValueGraph<PTreeNode, EdgeTypes> stateGraph; private MutableValueGraph<PTreeNode, EdgeTypes> stateGraph;
/** /**
* Current interpreter * Current interpreter
*/ */
private Interpreter<KeyData> currentInterpreter; private Interpreter<KeyData> currentInterpreter;
/** /**
* Current State in graph * Current State in graph
*/ */
private PTreeNode statePointer; private PTreeNode statePointer;
public ProofTreeController(Interpreter<KeyData> inter, ProofScript mainScript) { public ProofTreeController(Interpreter<KeyData> inter, ProofScript mainScript, StateGraphVisitor stateGraphVisitor) {
this.currentInterpreter = inter; this.currentInterpreter = inter;
buildControlFlowGraph(mainScript); buildControlFlowGraph(mainScript);
stateGraph = stateGraphVisitor.getStateGraph();
statePointer = stateGraphVisitor.getRootNode();
this.stateGraphVisitor = stateGraphVisitor;
// System.out.println(stateGraph.nodes());
//initializeStateGraph(mainScript);
} }
...@@ -48,13 +53,41 @@ public class ProofTreeController { ...@@ -48,13 +53,41 @@ public class ProofTreeController {
mainScript.accept(visitor); mainScript.accept(visitor);
this.controlFlowGraph = visitor.getGraph(); this.controlFlowGraph = visitor.getGraph();
System.out.println(visitor.asdot()); // System.out.println(visitor.asdot());
// System.out.println(controlFlowGraph);
} }
/* private void initializeStateGraph(ProofScript mainScript){
stateGraph = ValueGraphBuilder.directed().build();
State<KeyData> initState = currentInterpreter.getCurrentState();
System.out.println(initState);
PTreeNode initNode = new PTreeNode(mainScript);
initNode.setState(initState);
stateGraph.addNode(initNode);
// statePointer = initNode;
}*/
public PTreeNode stepOver() { public PTreeNode stepOver() {
PTreeNode current = statePointer;
ASTNode stmt = current.getScriptstmt();
if (controlFlowGraph.asGraph().nodes().contains(stmt)) {
// System.out.println("\n\nAdjacent:{\n"+controlFlowGraph.asGraph().adjacentNodes(stmt)+"}\n\n\n");
Object[] nodeArray = controlFlowGraph.asGraph().adjacentNodes(stmt).toArray();
ASTNode firtSucc = (ASTNode) nodeArray[0];
for (PTreeNode succ : stateGraph.successors(current)) {
if (succ.getScriptstmt().equals(firtSucc)) {
statePointer = succ;
}
}
}
//System.out.println(stateGraphVisitor.asdot());
return null; return null;
} }
......
package edu.kit.formal.interpreter;
import com.google.common.graph.MutableValueGraph;
import com.google.common.graph.ValueGraphBuilder;
import edu.kit.formal.interpreter.data.KeyData;
import edu.kit.formal.interpreter.data.State;
import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
import edu.kit.formal.proofscriptparser.ast.ASTNode;
import edu.kit.formal.proofscriptparser.ast.ProofScript;
/**
* Created by sarah on 6/26/17.
*/
public class StateGraphVisitor extends DefaultASTVisitor<Void> {
Interpreter currentInterpreter;
/**
* Graph that is computed on the fly in order to allow stepping
*/
private MutableValueGraph<PTreeNode, EdgeTypes> stateGraph;
private PTreeNode root;
private PTreeNode lastNode;
public StateGraphVisitor(Interpreter inter, ProofScript mainScript) {
stateGraph = ValueGraphBuilder.directed().build();
this.currentInterpreter = inter;
State<KeyData> initState = currentInterpreter.getCurrentState();
System.out.println(initState);
PTreeNode initNode = new PTreeNode(mainScript);
initNode.setState(initState);
stateGraph.addNode(initNode);
root = initNode;
lastNode = initNode;
}
public MutableValueGraph<PTreeNode, EdgeTypes> getStateGraph() {
return stateGraph;
}
public PTreeNode getRootNode() {
return root;
}
public PTreeNode getLastNode() {
return lastNode;
}
@Override
public Void defaultVisit(ASTNode node) {
PTreeNode newStateNode = new PTreeNode(node);
newStateNode.setState(currentInterpreter.getCurrentState());
stateGraph.addNode(newStateNode);
stateGraph.putEdgeValue(lastNode, newStateNode, EdgeTypes.STATE_FLOW);
lastNode = newStateNode;
System.out.println(asdot());
return null;
}
public String asdot() {
StringBuilder sb = new StringBuilder();
sb.append("digraph G {\nnode [shape=rect]\n ");
stateGraph.nodes().forEach(n -> {
sb.append(n.hashCode())
.append(" [label=\"")
.append(n.getScriptstmt().getNodeName())
.append("@")
.append(n.getScriptstmt().getStartPosition().getLineNumber())
.append("\"]\n");
});
stateGraph.edges().forEach(edge -> {
sb.append(edge.source().hashCode())
.append(" -> ")
.append(edge.target().hashCode())
.append(" [label=\"")
.append(stateGraph.edgeValue(edge.source(), edge.target()).name())
.append("\"]\n");
});