Skip to content

GitLab

Commit 2577adfe authored by Alexander Weigl's avatar Alexander Weigl
Browse files

Merge branch 'extendedState' of git.scc.kit.edu:xt9634/ProofScriptParser into extendedState 

* 'extendedState' of git.scc.kit.edu:xt9634/ProofScriptParser:
  Dual Pivot Quicksort Example
  Agatha Example
parents 9dfb35b5 283db775
Pipeline #14965 failed with stage
in 2 minutes and 2 seconds
Hide whitespace changes
Inline Side-by-side
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/ControlFlowVisitor.java
View file @ 2577adfe
......@@ -191,12 +191,12 @@ public class ControlFlowVisitor extends DefaultASTVisitor<Void> {
@Override
public Void visit(CasesStatement casesStatement) {
ControlFlowNode currentNode = new ControlFlowNode(casesStatement);
mappingOfNodes.put(casesStatement, currentNode);
graph.addNode(currentNode);
//System.out.println("\n" + currentNode + "\n");
graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER);
graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_BACK);
ControlFlowNode casesNode = new ControlFlowNode(casesStatement);
mappingOfNodes.put(casesStatement, casesNode);
graph.addNode(casesNode);
//System.out.println("\n" + casesNode + "\n");
graph.putEdgeValue(lastNode, casesNode, EdgeTypes.STEP_OVER);
graph.putEdgeValue(casesNode, lastNode, EdgeTypes.STEP_BACK);
List<CaseStatement> cases = casesStatement.getCases();
for (CaseStatement aCase : cases) {
......@@ -206,12 +206,12 @@ public class ControlFlowVisitor extends DefaultASTVisitor<Void> {
ControlFlowNode caseNode = new ControlFlowNode(aCase);
mappingOfNodes.put(aCase, caseNode);
graph.addNode(caseNode);
//System.out.println("\n" + caseNode + "\n");
graph.putEdgeValue(currentNode, caseNode, EdgeTypes.STEP_OVER); //??is this right?
graph.putEdgeValue(caseNode, currentNode, EdgeTypes.STEP_BACK);
//TODO rethink
graph.putEdgeValue(casesNode, caseNode, EdgeTypes.STEP_INTO); //??is this right?
graph.putEdgeValue(caseNode, casesNode, EdgeTypes.STEP_BACK);
lastNode = caseNode;
aCase.getBody().accept(this);
graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN);
graph.putEdgeValue(lastNode, casesNode, EdgeTypes.STEP_RETURN);
// }
}
//casesStatement.getDefaultCase()
......@@ -220,25 +220,25 @@ public class ControlFlowVisitor extends DefaultASTVisitor<Void> {
ControlFlowNode caseNode = new ControlFlowNode(defCase);
mappingOfNodes.put(defCase, caseNode);
graph.addNode(caseNode);
//System.out.println("\n" + caseNode + "\n");
graph.putEdgeValue(currentNode, caseNode, EdgeTypes.STEP_OVER); //??is this right?
graph.putEdgeValue(caseNode, currentNode, EdgeTypes.STEP_BACK);
//TODO rethink
graph.putEdgeValue(casesNode, caseNode, EdgeTypes.STEP_INTO); //??is this right?
graph.putEdgeValue(caseNode, casesNode, EdgeTypes.STEP_BACK);
lastNode = caseNode;
defCase.getBody().accept(this);
graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN);
graph.putEdgeValue(lastNode, casesNode, EdgeTypes.STEP_RETURN);
/*Statements defaultCase = defCase.getBody();
ControlFlowNode caseNode = new ControlFlowNode(defaultCase);
mappingOfNodes.put(defaultCase, caseNode);
graph.addNode(caseNode);
//System.out.println("\n" + caseNode + "\n");
graph.putEdgeValue(currentNode, caseNode, EdgeTypes.STEP_OVER); //??is this right?
graph.putEdgeValue(caseNode, currentNode, EdgeTypes.STEP_BACK);
graph.putEdgeValue(casesNode, caseNode, EdgeTypes.STEP_OVER); //??is this right?
graph.putEdgeValue(caseNode, casesNode, EdgeTypes.STEP_BACK);
lastNode = caseNode;
defaultCase.accept(this);
graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN);*/
graph.putEdgeValue(lastNode, casesNode, EdgeTypes.STEP_RETURN);*/
}
lastNode = currentNode;
lastNode = casesNode;
return null;
}
......
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/StateGraphWrapper.java
View file @ 2577adfe
......@@ -94,6 +94,8 @@ public class StateGraphWrapper<T> {
}
private static int counter = 0;
public MutableValueGraph<PTreeNode<T>, EdgeTypes> getStateGraph() {
return stateGraph;
}
......@@ -116,7 +118,7 @@ public class StateGraphWrapper<T> {
LOGGER.info("Stepover requested for null, therefore returning root");
return this.rootProperty().get();
}
LOGGER.info("Stepover requested for node {}@{}", statePointer.getScriptStmt(), statePointer.getScriptStmt().getNodeName());
LOGGER.info("Stepover requested for node {}@{}", statePointer.getScriptstmt(), statePointer.getScriptstmt().getNodeName());
//look for successors in the graph
Set<PTreeNode<T>> successors = this.stateGraph.successors(statePointer);
//if there are no successors they have to be computed therefore return null, to trigger the proof tree controller
......@@ -126,8 +128,11 @@ public class StateGraphWrapper<T> {
} else {
//if there are successors we want those which are connetced with State-Flow
Object[] sucs = successors.toArray();
getNodeWithEdgeType(statePointer, EdgeTypes.STATE_FLOW);
return (PTreeNode<T>) sucs[0];
PTreeNode nodeWithEdgeTypeSO = getNodeWithEdgeType(statePointer, EdgeTypes.STEP_OVER);
PTreeNode nodeWithEdgeTypeSF = getNodeWithEdgeType(statePointer, EdgeTypes.STATE_FLOW);
//return (PTreeNode<T>) sucs[0];
return nodeWithEdgeTypeSO;
}
//return statePointer;
......@@ -162,6 +167,13 @@ public class StateGraphWrapper<T> {
return null;
}
/**
* Return the predecessor node from the statepointer if it exists, the statepointer itself is not-existing,
* because in this case we have reached the end of the graph
*
* @param statePointer
* @return
*/
public PTreeNode<T> getStepBack(PTreeNode statePointer) {
Set<PTreeNode<T>> pred = this.stateGraph.predecessors(statePointer);
//if pred is empty we have reached the root
......@@ -175,6 +187,9 @@ public class StateGraphWrapper<T> {
//return statePointer;
}
private Void createNewNode(ASTNode node) {
return createNewNode(node, false);
}
......@@ -193,10 +208,10 @@ public class StateGraphWrapper<T> {
newStateNode.getContext().push(node);
State<T> currentInterpreterStateCopy = currentInterpreter.getCurrentState().copy();
//copy current state before executing statement
//newStateNode.setState(currentInterpreterStateCopy);
newStateNode.setState(currentInterpreterStateCopy);
//create extended State
InterpreterExtendedState<T> extState = new InterpreterExtendedState<>(null);
InterpreterExtendedState<T> extState = new InterpreterExtendedState<>();
extState.setStmt(node);
extState.setStateBeforeStmt(currentInterpreterStateCopy);
newStateNode.setExtendedState(extState);
......@@ -234,7 +249,7 @@ public class StateGraphWrapper<T> {
if (isCasesStmt) {
newStateNode.getContext().push(node);
extState = new InterpreterExtendedState<>(lastNode.getExtendedState());
extState = new InterpreterExtendedState<>(lastNode.getExtendedState().copy());
extState.setStmt(node);
extState.setStateBeforeStmt(lastState.copy());
Map<CaseStatement, List<GoalNode<T>>> mappingOfCaseToStates = extState.getMappingOfCaseToStates();
......@@ -245,7 +260,11 @@ public class StateGraphWrapper<T> {
});
extState.setMappingOfCaseToStates(mappingOfCaseToStates);
//TODO default case
newStateNode.setState(lastState.copy());
} else {
//set pointer to parent extended state
extState = new InterpreterExtendedState<>(lastNode.getExtendedState().copy());
extState.setStmt(node);
......@@ -261,7 +280,9 @@ public class StateGraphWrapper<T> {
newStateNode.setExtendedState(extState);
stateGraph.addNode(newStateNode);
stateGraph.putEdgeValue(lastNode, newStateNode, EdgeTypes.STATE_FLOW);
//inform listeners about a new node in the graph
fireNodeAdded(new NodeAddedEvent(lastNode, newStateNode));
addedNodes.put(node, newStateNode);
......@@ -269,6 +290,47 @@ public class StateGraphWrapper<T> {
return null;
}
/**
* Add a new state to an existing PTreeNode
*
* @param node
* @param fireStateAdded
* @return
*/
private Void addState(ASTNode node, boolean fireStateAdded) {
LOGGER.info("Adding a new state for statement {}@{}", node.getNodeName(), node.getStartPosition());
//get node from addedNodes Map
PTreeNode<T> newStateNode = addedNodes.get(node);
//copy Current Interpreter state
State<T> currentState = currentInterpreter.getCurrentState().copy();
//set the state
if (node != this.root.get().getScriptstmt()) {
newStateNode.setState(currentState);
newStateNode.getExtendedState().setStateAfterStmt(currentState);
if (newStateNode.getContext().peek().equals(node)) {
newStateNode.getContext().pop();
}
} else {
// newStateNode.setState(currentState);
newStateNode.getExtendedState().setStateAfterStmt(currentState);
if (newStateNode.getContext().peek().equals(node)) {
newStateNode.getContext().pop();
}
}
if (fireStateAdded) {
fireStateAdded(new StateAddedEvent(newStateNode, currentState, newStateNode.getExtendedState()));
}
LOGGER.debug("Extended state for {} updated with {} \n", node.getStartPosition(), newStateNode.getExtendedState().toString());
return null;
}
private void fireStateAdded(StateAddedEvent stateAddedEvent) {
changeListeners.forEach(list -> Platform.runLater(() -> {
list.graphChanged(stateAddedEvent);
// LOGGER.debug("New StateGraphChange " + this.asdot());
}));
}
private void fireNodeAdded(NodeAddedEvent nodeAddedEvent) {
changeListeners.forEach(list -> Platform.runLater(() -> {
list.graphChanged(nodeAddedEvent);
......@@ -315,7 +377,17 @@ public class StateGraphWrapper<T> {
public PTreeNode<T> getNode(List<GoalNode<T>> newValue) {
for (Map.Entry<ASTNode, PTreeNode<T>> next : addedNodes.entrySet()) {
PTreeNode value = next.getValue();
if (value.getExtendedState().getStateBeforeStmt().getGoals().equals(newValue)) {
if (value.getState().getGoals().equals(newValue)) {
return value;
}
}
return null;
}
public PTreeNode<T> getNode(InterpreterExtendedState newValue) {
for (Map.Entry<ASTNode, PTreeNode<T>> next : addedNodes.entrySet()) {
PTreeNode value = next.getValue();
if (value.getExtendedState().equals(newValue)) {
return value;
}
}
......@@ -333,9 +405,9 @@ public class StateGraphWrapper<T> {
stateGraph.nodes().forEach(n -> {
sb.append(n.hashCode())
.append(" [label=\"")
.append(n.getScriptStmt().getNodeName())
.append(n.getScriptstmt().getNodeName())
.append("@")
.append(n.getScriptStmt().getStartPosition().getLineNumber())
.append(n.getScriptstmt().getStartPosition().getLineNumber())
.append(n.extendedStateToString())
.append("\"]\n");
});
......@@ -366,39 +438,7 @@ public class StateGraphWrapper<T> {
return sb.toString();
}
private Void addState(ASTNode node, boolean fireStateAdded) {
LOGGER.info("Adding a new state for statement {}@{}", node.getNodeName(), node.getStartPosition());
//get node from addedNodes Map
PTreeNode<T> newStateNode = addedNodes.get(node);
//copy Current Interpreter state
State<T> currentState = currentInterpreter.getCurrentState().copy();
//set the state
if (node != this.root.get().getScriptStmt()) {
//newStateNode.setState(currentState);
newStateNode.getExtendedState().setStateAfterStmt(currentState);
if (newStateNode.getContext().peek().equals(node)) {
newStateNode.getContext().pop();
}
} else {
// newStateNode.setState(currentState);
newStateNode.getExtendedState().setStateAfterStmt(currentState);
if (newStateNode.getContext().peek().equals(node)) {
newStateNode.getContext().pop();
}
}
if (fireStateAdded) {
fireStateAdded(new StateAddedEvent(newStateNode, currentState, newStateNode.getExtendedState()));
}
LOGGER.debug("Extended state for {} updated with {} \n", node.getStartPosition(), newStateNode.getExtendedState().toString());
return null;
}
private void fireStateAdded(StateAddedEvent stateAddedEvent) {
changeListeners.forEach(list -> Platform.runLater(() -> {
list.graphChanged(stateAddedEvent);
// LOGGER.debug("New StateGraphChange " + this.asdot());
}));
}
private class EntryListener extends DefaultASTVisitor<Void> {
@Override
......@@ -406,7 +446,7 @@ public class StateGraphWrapper<T> {
if (root.get() == null) {
createRootNode(proofScript);
} else {
if (!root.get().getScriptStmt().equals(proofScript)) {
if (!root.get().getScriptstmt().equals(proofScript)) {
createNewNode(proofScript);
}
}
......
ui/src/main/java/edu/kit/iti/formal/psdbg/examples/agatha/AgathaExample.java 0 → 100644
View file @ 2577adfe
package edu.kit.iti.formal.psdbg.examples.agatha;
import edu.kit.iti.formal.psdbg.examples.Example;
public class AgathaExample extends Example {
public AgathaExample() {
setName("Agatha");
defaultInit(getClass());
System.out.println(this);
}
}
ui/src/main/java/edu/kit/iti/formal/psdbg/examples/java/dpqs/DualPivotExample.java 0 → 100644
View file @ 2577adfe
package edu.kit.iti.formal.psdbg.examples.java.dpqs;
import edu.kit.iti.formal.psdbg.examples.JavaExample;
public class DualPivotExample extends JavaExample {
public DualPivotExample() {
setName("Dual Pivot Quicksort");
setJavaFile(this.getClass().getResource("DualPivotQuicksort.java"));
defaultInit(getClass());
System.out.println(this);
}
}
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
View file @ 2577adfe
......@@ -186,6 +186,7 @@ public class DebuggerMain implements Initializable {
proofTreeController.currentSelectedGoalProperty().addListener((observable, oldValue, newValue) -> {
imodel.setCurrentInterpreterGoal(newValue);
//also update the selected to be shown
imodel.setSelectedGoalNodeToShow(newValue);
......
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java
View file @ 2577adfe
......@@ -2,7 +2,6 @@ package edu.kit.iti.formal.psdbg.gui.controller;
import com.google.common.eventbus.Subscribe;
import com.google.common.graph.MutableValueGraph;
import de.uka.ilkd.key.proof.Goal;
import edu.kit.iti.formal.psdbg.InterpretingService;
import edu.kit.iti.formal.psdbg.gui.controls.ASTNodeHiglightListener;
import edu.kit.iti.formal.psdbg.gui.controls.DebuggerStatusBar;
......@@ -27,7 +26,6 @@ import org.apache.logging.log4j.Logger;
import java.util.Collections;
import java.util.List;
import java.util.Set;
import java.util.stream.Collectors;
/**
* Class controlling and maintaining proof tree structure for debugger and handling step functions for the debugger
......@@ -41,10 +39,8 @@ public class ProofTreeController {
* To control stepping
*/
private final PuppetMaster blocker = new PuppetMaster();
/**
* Goals of the state which is referenced by the statePointer
* TODO: weigl I don't understand this.
*/
private final ListProperty<GoalNode<KeyData>> currentGoals = new SimpleListProperty<>(FXCollections.observableArrayList());
......@@ -127,10 +123,10 @@ public class ProofTreeController {
@Override
public void graphChanged(NodeAddedEvent nodeAddedEvent) {
PTreeNode added = nodeAddedEvent.getAddedNode();
if (added.getExtendedState().getStateBeforeStmt() != null) {
if (added.getState() != null) {
LOGGER.info("Graph changed with the following PTreeNode: {} and the statepointer points to {}", nodeAddedEvent.getAddedNode(), statePointer);
nextComputedNode.setValue(nodeAddedEvent.getAddedNode());
// Events.fire(new Events.NewNodeExecuted(nodeAddedEvent.getAddedNode().getScriptStmt()));
// Events.fire(new Events.NewNodeExecuted(nodeAddedEvent.getAddedNode().getScriptstmt()));
}
}
......@@ -140,15 +136,28 @@ public class ProofTreeController {
PTreeNode changedNode = stateAddedEvent.getChangedNode();
LOGGER.info("Graph changed by adding a state to PTreeNode: {} and the statepointer points to {}", stateAddedEvent, statePointer);
nextComputedNode.set(changedNode);
//Events.fire(new Events.NewNodeExecuted(changedNode.getScriptStmt()));
//Events.fire(new Events.NewNodeExecuted(changedNode.getScriptstmt()));
}
};
public ProofScript getMainScript() {
return mainScript.get();
}
public void setMainScript(ProofScript mainScript) {
this.mainScript.set(mainScript);
}
public SimpleObjectProperty<ProofScript> mainScriptProperty() {
return mainScript;
}
/**
* Create a new ProofTreeController
* and bind properties
* Create a new ProofTreeController
* and bind properties
*/
public ProofTreeController() {
......@@ -163,61 +172,38 @@ public class ProofTreeController {
nextComputedNode.addListener((observable, oldValue, newValue) -> {
//update statepointer
if (newValue != null) {
LOGGER.info("New node {} was computed and the statepointer was set to {}", newValue.getScriptStmt(), newValue);
LOGGER.info("New node {} was computed and the statepointer was set to {}", newValue.getScriptstmt(), newValue);
this.statePointer = newValue;
//setNewState(blocker.currentStateProperty().get());
setNewState(newValue.getExtendedState().getStateBeforeStmt());
setNewState(newValue.getState());
}
});
}
private static boolean compareCtrlFlowNodes(ControlFlowNode newNode, ControlFlowNode oldNode) {
return newNode.getScriptstmt().getNodeName().equals(oldNode.getScriptstmt().getNodeName());
}
private static boolean comparePTreeNodes(PTreeNode newTreeNode, PTreeNode oldTreeNode) {
return false;
}
public ProofScript getMainScript() {
return mainScript.get();
}
public void setMainScript(ProofScript mainScript) {
this.mainScript.set(mainScript);
}
//TODO handle endpoint
public SimpleObjectProperty<ProofScript> mainScriptProperty() {
return mainScript;
}
//TODO handle endpoint of graph
/**
* Sets the properties that may notify GUI about statechanges with new state values
* CurrentGoalsProperty and SelectedGoal are both listened by InspectionViewModel
*
* @param state
*/
private void setNewState(State<KeyData> state) {
LOGGER.info("Setting new State " + state.toString());
//Statepointer null wenn anfangszustand?
if (statePointer != null && state != null) {
LOGGER.info("Setting new State " + state.toString());
//setCurrentHighlightNode(statePointer.getScriptStmt());
//setCurrentHighlightNode(statePointer.getScriptstmt());
//get all goals that are open
//List<GoalNode<KeyData>> arr = state.getGoals().stream().filter(keyDataGoalNode -> !keyDataGoalNode.isClosed()).collect(Collectors.toList());
Object[] arr = state.getGoals().stream().filter(keyDataGoalNode -> !keyDataGoalNode.isClosed()).toArray();
//if there is no selected goal node we might have reached
//a closed proof
if (state.getSelectedGoalNode() == null) {
setCurrentSelectedGoal(null);
setCurrentGoals(state.getGoals());
setCurrentGoals(arr.length == 0 ? Collections.emptyList() : state.getGoals());
} else {
setCurrentGoals(state.getGoals());
......@@ -226,8 +212,8 @@ public class ProofTreeController {
LOGGER.debug("New State from this command: {}@{}",
this.statePointer.getScriptStmt().getNodeName(),
this.statePointer.getScriptStmt().getStartPosition());
this.statePointer.getScriptstmt().getNodeName(),
this.statePointer.getScriptstmt().getStartPosition());
} else {
throw new RuntimeException("The state pointer was null when setting new state");
}
......@@ -235,6 +221,19 @@ public class ProofTreeController {
}
//TODO handle endpoint
private static boolean compareCtrlFlowNodes(ControlFlowNode newNode, ControlFlowNode oldNode) {
return newNode.getScriptstmt().getNodeName().equals(oldNode.getScriptstmt().getNodeName());
}
//TODO handle endpoint of graph
private static boolean comparePTreeNodes(PTreeNode newTreeNode, PTreeNode oldTreeNode) {
return false;
}
/**
* StepOver and return the node to which the state pointer is pointing to
*
......@@ -255,7 +254,7 @@ public class ProofTreeController {
//if nextnode is null ask interpreter to execute next statement and compute next state
if (nextNode != null) {
//setCurrentHighlightNode(nextNode.getScriptStmt());
setCurrentHighlightNode(nextNode.getScriptstmt());
}
if (nextNode != null && nextNode.getExtendedState().getStateAfterStmt() != null) {
......@@ -292,6 +291,7 @@ public class ProofTreeController {
this.statePointer = stateGraphWrapper.getStepBack(current);
if (this.statePointer != null) {
setNewState(statePointer.getExtendedState().getStateBeforeStmt());
setCurrentHighlightNode(statePointer.getScriptstmt());
} else {
this.statePointer = current;
}
......@@ -299,6 +299,8 @@ public class ProofTreeController {
}
public PTreeNode stepInto() {
PTreeNode current = this.statePointer;
return null;
}
......@@ -308,7 +310,6 @@ public class ProofTreeController {
/**
* Execute script with breakpoints
*
* @param debugMode
* @param statusBar
* @param breakpoints
......@@ -392,7 +393,7 @@ public class ProofTreeController {
this.controlFlowGraphVisitor = new ControlFlowVisitor(currentInterpreter.getFunctionLookup());
mainScript.accept(controlFlowGraphVisitor);
this.setMainScript(mainScript);
LOGGER.debug("CFG\n" + controlFlowGraphVisitor.asdot());
LOGGER.info("CFG\n" + controlFlowGraphVisitor.asdot());
}
......
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ASTNodeHiglightListener.java
View file @ 2577adfe
......@@ -3,8 +3,7 @@ package edu.kit.iti.formal.psdbg.gui.controls;
import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
import edu.kit.iti.formal.psdbg.parser.ast.Parameters;
import edu.kit.iti.formal.psdbg.parser.ast.Statements;
import javafx.application.Platform;
import javafx.beans.property.SimpleObjectProperty;
......@@ -54,15 +53,9 @@ public class ASTNodeHiglightListener<T> {
}
public class HighlightEntryListener extends DefaultASTVisitor<Void> {
@Override
public Void visit(ProofScript proofScript) {
return defaultVisit(proofScript);
}
@Override
public Void visit(CallStatement proofScript) {
return defaultVisit(proofScript);
public Void visit(Parameters parameters) {
return null;
}
@Override
......@@ -74,9 +67,6 @@ public class ASTNodeHiglightListener<T> {
public Void defaultVisit(ASTNode node) {
if (node != null) {
lastHighlightedNode = node;
System.out.println("nodeInHighlighter = " + node);