Skip to content

GitLab

P
ProofScriptParser
Commit 3722b8cb authored by Sarah Grebing's avatar Sarah Grebing
Browse files
Options

Line highlight first version

parent d0906b07
Pipeline #11892 passed with stage
    in 2 minutes and 18 seconds
    Hide whitespace changes
    Inline Side-by-side
    Showing with 221 additions and 99 deletions
    src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java
    View file @ 3722b8cb
    ......@@ -225,22 +225,24 @@ public class DebuggerMainWindowController implements Initializable {
    pc.setCurrentInterpreter(currentInterpreter);
    pc.setMainScript(scripts.get(0));
    pc.executeScript(this.debugMode.get());
    pc.currentGoalsProperty().addListener((o, old, fresh) -> {
    if (fresh != null) {
    model.currentGoalNodesProperty().setAll(fresh);
    }
    });
    pc.executeScript(this.debugMode.get());
    model.currentSelectedGoalNodeProperty().bind(pc.currentSelectedGoalProperty());
    /* pc.currentGoalsProperty().addListener((observable, oldValue, newValue) -> {
    if(newValue != null) {
    model.currentGoalNodesProperty().get().
    setAll(pc.currentGoalsProperty());
    pc.startHighlightPositionPropertyProperty().addListener((observable, oldValue, newValue) -> {
    if (newValue.getLineNumber() > -1) {
    tabPane.getSelectedScriptArea().highlightStmt(newValue.getLineNumber(), "line-highlight-postmortem");
    }
    if (oldValue.getLineNumber() > -1) {
    tabPane.getSelectedScriptArea().removeHighlightStmt(oldValue.getLineNumber());
    }
    });*/
    });
    //highlight signature of main script
    tabPane.getSelectedScriptArea().setDebugMark(scripts.get(0).getStartPosition().getLineNumber());
    } catch (RecognitionException e) {
    ......@@ -389,18 +391,12 @@ public class DebuggerMainWindowController implements Initializable {
    }
    public void stepOver(ActionEvent actionEvent) {
    // blocker.getStepUntilBlock().addAndGet(1);
    // blocker.unlock();
    PTreeNode newState = pc.stepOver();
    // model.currentGoalNodesProperty().setAll(newState.getState().getGoals());
    // model.setCurrentSelectedGoalNode(newState.getState().getSelectedGoalNode());
    }
    public void stepBack(ActionEvent actionEvent) {
    PTreeNode newState = pc.stepBack();
    // model.currentGoalNodesProperty().setAll(newState.getState().getGoals());
    // model.setCurrentSelectedGoalNode(newState.getState().getSelectedGoalNode());
    }
    ......@@ -432,8 +428,9 @@ public class DebuggerMainWindowController implements Initializable {
    }
    public void stopDebugMode(ActionEvent actionEvent) {
    //linenumberMainscript from model?
    // tabPane.getActiveScriptAreaTab().getScriptArea().removeHighlightStmt(lineNumberMainScript);
    //tabPane.getActiveScriptAreaTab().getScriptArea().removeHighlightStmt(lineNumberMainScript);
    //inspectionViewTabPane.getInspectionViewTab.clear();
    }
    ......
    src/main/java/edu/kit/formal/interpreter/graphs/ProgramFlowVisitor.java → src/main/java/edu/kit/formal/interpreter/graphs/ControlFlowVisitor.java
    View file @ 3722b8cb
    ......@@ -13,12 +13,15 @@ import java.util.*;
    /**
    * Visitor to create ProgramFlowGraph
    */
    public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
    public class ControlFlowVisitor extends DefaultASTVisitor<Void> {
    /**
    * Lookup for names of scripts
    */
    private final CommandLookup functionLookup;
    /**
    * Mapping of ASTNodes to CFG nodes
    */
    private Map<ASTNode, ControlFlowNode> mappingOfNodes;
    /**
    * Last visited Node
    ......@@ -30,17 +33,17 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
    */
    private MutableValueGraph<ControlFlowNode, EdgeTypes> graph = ValueGraphBuilder.directed().allowsSelfLoops(true).build();
    /**
    * Call context
    */
    private LinkedList<ASTNode> context = new LinkedList<>();
    public ProgramFlowVisitor(CommandLookup functionLookup) {
    public ControlFlowVisitor(CommandLookup functionLookup) {
    this.functionLookup = functionLookup;
    mappingOfNodes = new HashMap<>();
    }
    public MutableValueGraph<ControlFlowNode, EdgeTypes> getGraph() {
    return graph;
    }
    public Set<EndpointPair<ControlFlowNode>> getAllEdgesForNodeAsTarget(ASTNode node) {
    ......@@ -68,9 +71,10 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
    public Void visit(ProofScript proofScript) {
    ControlFlowNode scriptNode = new ControlFlowNode(proofScript);
    context.add(proofScript);
    mappingOfNodes.put(proofScript, scriptNode);
    graph.addNode(scriptNode);
    System.out.println("\n" + scriptNode + "\n");
    //System.out.println("\n" + scriptNode + "\n");
    lastNode = scriptNode;
    return this.visit(proofScript.getBody());
    ......@@ -82,7 +86,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
    ControlFlowNode assignmentNode = new ControlFlowNode(assignment);
    mappingOfNodes.put(assignment, assignmentNode);
    graph.addNode(assignmentNode);
    System.out.println("\n" + assignmentNode + "\n");
    //System.out.println("\n" + assignmentNode + "\n");
    lastNode = assignmentNode;
    return null;
    }
    ......@@ -149,7 +153,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
    ControlFlowNode currentNode = new ControlFlowNode(foreach);
    mappingOfNodes.put(foreach, currentNode);
    graph.addNode(currentNode);
    System.out.println("\n" + currentNode + "\n");
    //System.out.println("\n" + currentNode + "\n");
    graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER);
    graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_BACK);
    lastNode = currentNode;
    ......@@ -164,7 +168,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
    ControlFlowNode currentNode = new ControlFlowNode(theOnly);
    mappingOfNodes.put(theOnly, currentNode);
    graph.addNode(currentNode);
    System.out.println("\n" + currentNode + "\n");
    //System.out.println("\n" + currentNode + "\n");
    graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER);
    graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_BACK);
    lastNode = currentNode;
    ......@@ -180,7 +184,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
    ControlFlowNode currentNode = new ControlFlowNode(repeatStatement);
    mappingOfNodes.put(repeatStatement, currentNode);
    graph.addNode(currentNode);
    System.out.println("\n" + currentNode + "\n");
    // System.out.println("\n" + currentNode + "\n");
    graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER);
    graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_BACK);
    lastNode = currentNode;
    ......@@ -195,7 +199,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
    ControlFlowNode currentNode = new ControlFlowNode(casesStatement);
    mappingOfNodes.put(casesStatement, currentNode);
    graph.addNode(currentNode);
    System.out.println("\n" + currentNode + "\n");
    //System.out.println("\n" + currentNode + "\n");
    graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER);
    graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_BACK);
    List<CaseStatement> cases = casesStatement.getCases();
    ......@@ -203,7 +207,7 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
    ControlFlowNode caseNode = new ControlFlowNode(aCase);
    mappingOfNodes.put(aCase, caseNode);
    graph.addNode(caseNode);
    System.out.println("\n" + caseNode + "\n");
    //System.out.println("\n" + caseNode + "\n");
    graph.putEdgeValue(currentNode, caseNode, EdgeTypes.STEP_OVER); //??is this right?
    graph.putEdgeValue(caseNode, currentNode, EdgeTypes.STEP_BACK);
    lastNode = caseNode;
    ......@@ -241,5 +245,10 @@ public class ProgramFlowVisitor extends DefaultASTVisitor<Void> {
    return sb.toString();
    }
    public MutableValueGraph<ControlFlowNode, EdgeTypes> getGraph() {
    return graph;
    }
    }
    src/main/java/edu/kit/formal/interpreter/graphs/ProofTreeController.java
    View file @ 3722b8cb
    ......@@ -6,7 +6,6 @@ import edu.kit.formal.interpreter.InterpretingService;
    import edu.kit.formal.interpreter.data.GoalNode;
    import edu.kit.formal.interpreter.data.KeyData;
    import edu.kit.formal.interpreter.data.State;
    import edu.kit.formal.proofscriptparser.Visitor;
    import edu.kit.formal.proofscriptparser.ast.Position;
    import edu.kit.formal.proofscriptparser.ast.ProofScript;
    import javafx.beans.property.ListProperty;
    ......@@ -54,6 +53,7 @@ public class ProofTreeController {
    */
    private SimpleObjectProperty<PTreeNode> nextComputedNode = new SimpleObjectProperty<>();
    private SimpleObjectProperty<Position> startHighlightPositionProperty = new SimpleObjectProperty<>();
    private SimpleObjectProperty<Position> endHighlightPositionProperty = new SimpleObjectProperty<>();
    ......@@ -61,12 +61,12 @@ public class ProofTreeController {
    /**
    * Visitor to retrieve state graph
    */
    private StateGraphVisitor stateGraphVisitor;
    private StateGraphWrapper stateGraphWrapper;
    /**
    * Graph that is computed on the fly in order to allow stepping
    */
    private ProgramFlowVisitor controlFlowGraphVisitor;
    private ControlFlowVisitor controlFlowGraphVisitor;
    /**
    ......@@ -108,6 +108,7 @@ public class ProofTreeController {
    //update statepointer
    this.statePointer = newValue;
    setNewState(this.statePointer.getState());
    });
    ......@@ -120,7 +121,7 @@ public class ProofTreeController {
    * @param mainScript
    */
    private void buildControlFlowGraph(ProofScript mainScript) {
    this.controlFlowGraphVisitor = new ProgramFlowVisitor(currentInterpreter.getFunctionLookup());
    this.controlFlowGraphVisitor = new ControlFlowVisitor(currentInterpreter.getFunctionLookup());
    mainScript.accept(controlFlowGraphVisitor);
    System.out.println("CFG\n" + controlFlowGraphVisitor.asdot());
    ......@@ -139,14 +140,17 @@ public class ProofTreeController {
    //if pointer is null, we do not have a root yet
    if (currentPointer == null) {
    //ask for root
    currentPointer = stateGraphVisitor.rootProperty().get();
    currentPointer = stateGraphWrapper.rootProperty().get();
    statePointer = currentPointer;
    }
    PTreeNode nextNode = stateGraphVisitor.getStepOver(currentPointer);
    //get next node
    PTreeNode nextNode = stateGraphWrapper.getStepOver(currentPointer);
    //if nextnode is null ask interpreter
    if (nextNode != null) {
    this.statePointer = nextNode;
    setNewState(statePointer.getState());
    // setHighlightStmt(this.statePointer.getScriptstmt().getStartPosition(), this.statePointer.getScriptstmt().getStartPosition());
    } else {
    //no next node is present yet
    //let interpreter run for one step and let listener handle updating the statepointer
    ......@@ -164,8 +168,9 @@ public class ProofTreeController {
    */
    public PTreeNode stepBack() {
    PTreeNode current = statePointer;
    this.statePointer = stateGraphVisitor.getStepBack(current);
    this.statePointer = stateGraphWrapper.getStepBack(current);
    setNewState(statePointer.getState());
    //setHighlightStmt(this.statePointer.getScriptstmt().getStartPosition(), this.statePointer.getScriptstmt().getStartPosition());
    return statePointer;
    }
    ......@@ -190,12 +195,10 @@ public class ProofTreeController {
    //build CFG
    buildControlFlowGraph(mainScript);
    //build StateGraph
    this.stateGraphVisitor = new StateGraphVisitor(this.currentInterpreter, this.mainScript, this.controlFlowGraphVisitor);
    this.stateGraphWrapper = new StateGraphWrapper(currentInterpreter, this.mainScript, this.controlFlowGraphVisitor);
    currentInterpreter.getEntryListeners().add(this.stateGraphVisitor);
    //currentInterpreter.getExitListeners().add(this.stateGraphVisitor);
    this.stateGraphVisitor.addChangeListener(graphChangedListener);
    this.stateGraphWrapper.install(currentInterpreter);
    this.stateGraphWrapper.addChangeListener(graphChangedListener);
    blocker.getStepUntilBlock().set(1);
    }
    interpreterService.interpreterProperty().set(currentInterpreter);
    ......@@ -214,9 +217,24 @@ public class ProofTreeController {
    private void setNewState(State<KeyData> state) {
    this.setCurrentGoals(state.getGoals());
    this.setCurrentSelectedGoal(state.getSelectedGoalNode());
    setHighlightStmt(this.statePointer.getScriptstmt().getStartPosition(), this.statePointer.getScriptstmt().getStartPosition());
    System.out.println("New State from this command: " + this.statePointer.getScriptstmt().getNodeName() + "@" + this.statePointer.getScriptstmt().getStartPosition());
    }
    /**
    * Set Position for highlighting statement
    *
    * @param start
    * @param end
    */
    private void setHighlightStmt(Position start, Position end) {
    this.startHighlightPositionProperty.set(start);
    this.endHighlightPositionProperty.set(end);
    }
    /**************************************************************************************************************
    *
    * Getter and Setter
    ......@@ -232,8 +250,8 @@ public class ProofTreeController {
    }
    public Visitor getStateVisitor() {
    return this.stateGraphVisitor;
    public StateGraphWrapper getStateVisitor() {
    return this.stateGraphWrapper;
    }
    public List<GoalNode<KeyData>> getCurrentGoals() {
    ......@@ -268,6 +286,28 @@ public class ProofTreeController {
    return executeNotPossible;
    }
    public Position getStartHighlightPositionProperty() {
    return startHighlightPositionProperty.get();
    }
    public void setStartHighlightPositionProperty(Position startHighlightPositionProperty) {
    this.startHighlightPositionProperty.set(startHighlightPositionProperty);
    }
    public SimpleObjectProperty<Position> startHighlightPositionPropertyProperty() {
    return startHighlightPositionProperty;
    }
    public Position getEndHighlightPositionProperty() {
    return endHighlightPositionProperty.get();
    }
    public void setEndHighlightPositionProperty(Position endHighlightPositionProperty) {
    this.endHighlightPositionProperty.set(endHighlightPositionProperty);
    }
    public SimpleObjectProperty<Position> endHighlightPositionPropertyProperty() {
    return endHighlightPositionProperty;
    }
    }
    src/main/java/edu/kit/formal/interpreter/graphs/StateGraphVisitor.java → src/main/java/edu/kit/formal/interpreter/graphs/StateGraphWrapper.java
    View file @ 3722b8cb
    ......@@ -9,15 +9,13 @@ import edu.kit.formal.interpreter.data.KeyData;
    import edu.kit.formal.interpreter.data.State;
    import edu.kit.formal.interpreter.exceptions.StateGraphException;
    import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
    import edu.kit.formal.proofscriptparser.Visitor;
    import edu.kit.formal.proofscriptparser.ast.*;
    import javafx.application.Platform;
    import javafx.beans.property.SimpleObjectProperty;
    import lombok.Getter;
    import java.util.ArrayList;
    import java.util.HashSet;
    import java.util.List;
    import java.util.Set;
    import java.util.*;
    /**
    ......@@ -25,7 +23,7 @@ import java.util.Set;
    * A Node in the graph is a PTreeNode {@link PTreeNode}
    * Edges are computed on the fly while
    */
    public class StateGraphVisitor extends DefaultASTVisitor<Void> {
    public class StateGraphWrapper {
    /**
    * Listeners getting informed when new node added to state graph
    ......@@ -56,21 +54,28 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
    private PTreeNode lastNode;
    /**
    * Visitor for control flow graph
    * Mapping ASTNode to PTreeNode
    */
    private ProgramFlowVisitor cfgVisitor;
    private HashMap<ASTNode, PTreeNode> addedNodes = new LinkedHashMap<>();
    /**
    * Visitor for control flow graph
    */
    private ControlFlowVisitor cfgVisitor;
    private Visitor<Void> entryListener = new StateGraphWrapper.EntryListener();
    private Visitor<Void> exitListener = new StateGraphWrapper.ExitListener();
    private ProofScript mainScript;
    public StateGraphVisitor(Interpreter inter, ProofScript mainScript, ProgramFlowVisitor cfgVisitor) {
    public StateGraphWrapper(Interpreter inter, ProofScript mainScript, ControlFlowVisitor cfgVisitor) {
    stateGraph = ValueGraphBuilder.directed().build();
    this.currentInterpreter = inter;
    this.cfgVisitor = cfgVisitor;
    this.mainScript = mainScript;
    //createRootNode();
    // createRootNode(null);
    }
    ......@@ -107,7 +112,12 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
    //careful TODO look for right edges
    //TODO handle endpoint of graph
    public PTreeNode getStepOver(PTreeNode statePointer) {
    /*Set<PTreeNode> pTreeNodesNeigbours = stateGraph.adjacentNodes(statePointer);
    if(pTreeNodesNeigbours.isEmpty()){
    return null;
    }else{
    pTreeNodesNeigbours.forEach(e-> System.out.println(e.getScriptstmt().getNodeName()+e.getScriptstmt().getStartPosition()));
    }*/
    if (statePointer == null) {
    return this.rootProperty().get();
    }
    ......@@ -119,6 +129,7 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
    getNodeWithEdgeType(statePointer, EdgeTypes.STATE_FLOW);
    return (PTreeNode) sucs[0];
    }
    //return statePointer;
    }
    ......@@ -127,6 +138,7 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
    public PTreeNode getStepBack(PTreeNode statePointer) {
    Set<PTreeNode> pred = this.stateGraph.predecessors(statePointer);
    if (pred.isEmpty()) {
    return null;
    } else {
    ......@@ -134,6 +146,7 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
    return (PTreeNode) sucs[0];
    }
    //return statePointer;
    }
    private PTreeNode getNodeWithEdgeType(PTreeNode source, EdgeTypes type) {
    ......@@ -165,69 +178,45 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
    * @param node
    * @return
    */
    public Void createNewNode(ASTNode node) {
    private Void createNewNode(ASTNode node) {
    State<KeyData> lastState = lastNode.getState();
    PTreeNode newStateNode;
    newStateNode = new PTreeNode(node);
    State<KeyData> currentState = currentInterpreter.getCurrentState().copy();
    System.out.println("Equals of states " + currentState.equals(lastState));
    newStateNode.setState(currentState);
    //State<KeyData> currentState = currentInterpreter.getCurrentState().copy();
    //System.out.println("Equals of states " + currentState.equals(lastState));
    //newStateNode.setState(currentState);
    stateGraph.addNode(newStateNode);
    stateGraph.putEdgeValue(lastNode, newStateNode, EdgeTypes.STATE_FLOW);
    fireNodeAdded(new NodeAddedEvent(lastNode, newStateNode));
    addedNodes.put(node, newStateNode);
    lastNode = newStateNode;
    return null;
    }
    public Void addState(ASTNode node) {
    PTreeNode newStateNode = addedNodes.get(node);
    State<KeyData> currentState = currentInterpreter.getCurrentState().copy();
    @Override
    public Void visit(ProofScript proofScript) {
    if (this.root.get() == null) {
    createRootNode(proofScript);
    } else {
    createNewNode(proofScript);
    }
    newStateNode.setState(currentState);
    return null;
    }
    @Override
    public Void visit(AssignmentStatement assignment) {
    return createNewNode(assignment);
    }
    @Override
    public Void visit(CasesStatement casesStatement) {
    return createNewNode(casesStatement);
    }
    @Override
    public Void visit(CaseStatement caseStatement) {
    return createNewNode(caseStatement);
    }
    @Override
    public Void visit(CallStatement call) {
    return createNewNode(call);
    }
    @Override
    public Void visit(TheOnlyStatement theOnly) {
    return createNewNode(theOnly);
    }
    @Override
    public Void visit(ForeachStatement foreach) {
    return createNewNode(foreach);
    public void install(Interpreter<KeyData> interpreter) {
    if (currentInterpreter != null) deinstall(interpreter);
    interpreter.getEntryListeners().add(entryListener);
    interpreter.getEntryListeners().add(exitListener);
    currentInterpreter = interpreter;
    }
    @Override
    public Void visit(RepeatStatement repeatStatement) {
    return createNewNode(repeatStatement);
    public void deinstall(Interpreter<KeyData> interpreter) {
    if (interpreter != null) {
    interpreter.getEntryListeners().remove(entryListener);
    interpreter.getEntryListeners().remove(exitListener);
    }
    }
    public String asdot() {
    ......@@ -256,7 +245,6 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
    return sb.toString();
    }
    public PTreeNode getRoot() {
    return root.get();
    }
    ......@@ -277,7 +265,6 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
    changeListeners.remove(listener);
    }
    private void fireNodeAdded(NodeAddedEvent nodeAddedEvent) {
    changeListeners.forEach(list -> {
    Platform.runLater(() -> {
    ......@@ -287,5 +274,94 @@ public class StateGraphVisitor extends DefaultASTVisitor<Void> {
    }
    private class EntryListener extends DefaultASTVisitor<Void> {
    @Override
    public Void visit(ProofScript proofScript) {
    if (root.get() == null) {
    createRootNode(proofScript);
    } else {
    createNewNode(proofScript);
    }
    return null;
    }
    @Override
    public Void visit(AssignmentStatement assignment) {
    return createNewNode(assignment);
    }
    @Override
    public Void visit(CasesStatement casesStatement) {
    return createNewNode(casesStatement);
    }
    @Override
    public Void visit(CaseStatement caseStatement) {
    return createNewNode(caseStatement);
    }
    @Override
    public Void visit(CallStatement call) {
    return createNewNode(call);
    }
    @Override
    public Void visit(TheOnlyStatement theOnly) {
    return createNewNode(theOnly);
    }
    @Override
    public Void visit(ForeachStatement foreach) {
    return createNewNode(foreach);
    }
    @Override
    public Void visit(RepeatStatement repeatStatement) {
    return createNewNode(repeatStatement);
    }
    }
    private class ExitListener extends DefaultASTVisitor<Void> {
    @Override
    public Void visit(AssignmentStatement assignment) {
    return addState(assignment);
    }
    @Override
    public Void visit(CasesStatement casesStatement) {
    return addState(casesStatement);
    }
    @Override
    public Void visit(CaseStatement caseStatement) {
    return addState(caseStatement);
    }
    @Override
    public Void visit(CallStatement call) {
    return addState(call);
    }
    @Override
    public Void visit(TheOnlyStatement theOnly) {
    return addState(theOnly);
    }
    @Override
    public Void visit(ForeachStatement foreach) {
    return addState(foreach);
    }
    @Override
    public Void visit(RepeatStatement repeatStatement) {
    return addState(repeatStatement);
    }
    /* @Override