Skip to content

GitLab

P
ProofScriptParser
Commit 4f5faf1f authored by Alexander Weigl's avatar Alexander Weigl
Browse files
Options

Fixing UI, tommorrow NPE hunting

parent c7ec5de9
Pipeline #15031 failed with stage
    in 1 minute and 57 seconds
    Expand all Hide whitespace changes
    Inline Side-by-side
    Showing with 605 additions and 1911 deletions
    lang/src/main/java/edu/kit/iti/formal/psdbg/parser/Facade.java
    View file @ 4f5faf1f
    ......@@ -24,7 +24,9 @@ package edu.kit.iti.formal.psdbg.parser;
    import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
    import edu.kit.iti.formal.psdbg.parser.ast.Expression;
    import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
    import lombok.val;
    import org.antlr.v4.runtime.CharStream;
    import org.antlr.v4.runtime.CharStreams;
    import org.antlr.v4.runtime.CommonTokenStream;
    ......@@ -33,7 +35,6 @@ import org.antlr.v4.runtime.ParserRuleContext;
    import java.io.File;
    import java.io.IOException;
    import java.util.List;
    import edu.kit.iti.formal.psdbg.parser.ast.*;
    /**
    * This class captures high-level functions of this package.
    ......@@ -104,4 +105,9 @@ public abstract class Facade {
    node.accept(prettyPrinter);
    return prettyPrinter.toString();
    }
    public static Expression parseExpression(String condition) {
    val ctx = getParser(CharStreams.fromString(condition)).expression();
    return (Expression) ctx.accept(new TransformAst());
    }
    }
    rt-key/src/main/java/edu/kit/iti/formal/psdbg/InteractiveCLIDebugger.java
    View file @ 4f5faf1f
    package edu.kit.iti.formal.psdbg;
    import com.google.common.graph.MutableValueGraph;
    import de.uka.ilkd.key.api.KeYApi;
    import de.uka.ilkd.key.api.ProofManagementApi;
    import de.uka.ilkd.key.proof.io.ProblemLoaderException;
    ......@@ -10,9 +9,6 @@ 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.interpreter.graphs.ControlFlowNode;
    import edu.kit.iti.formal.psdbg.interpreter.graphs.ControlFlowTypes;
    import edu.kit.iti.formal.psdbg.interpreter.graphs.ControlFlowVisitor;
    import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
    import edu.kit.iti.formal.psdbg.parser.Facade;
    import edu.kit.iti.formal.psdbg.parser.ast.*;
    ......@@ -62,10 +58,10 @@ public class InteractiveCLIDebugger {
    .scriptSearchPath(new File("."));
    interpreter = ib.build();
    ControlFlowVisitor cfgVistor = new ControlFlowVisitor(ib.getLookup());
    MutableValueGraph<ControlFlowNode, ControlFlowTypes> cfg = cfgVistor.getGraph();
    //ControlFlowVisitor cfgVistor = new ControlFlowVisitor(ib.getLookup());
    //MutableValueGraph<ControlFlowNode, ControlFlowTypes> cfg = cfgVistor.getGraph();
    df = new DebuggerFramework<>(interpreter, scripts.get(0), cfg);
    df = new DebuggerFramework<>(interpreter, scripts.get(0), null);
    df.getStatePointerListener().add(this::printNode);
    //df.getBeforeExecutionListener().add(this::printNode);
    //df.getAfterExecutionListener().add(this::end);
    ......
    rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/Blocker.java
    View file @ 4f5faf1f
    package edu.kit.iti.formal.psdbg.interpreter.dbg;
    import edu.kit.iti.formal.psdbg.interpreter.Evaluator;
    import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
    import edu.kit.iti.formal.psdbg.interpreter.exceptions.InterpreterRuntimeException;
    import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
    import lombok.Data;
    import edu.kit.iti.formal.psdbg.parser.types.SimpleType;
    import lombok.Getter;
    import lombok.RequiredArgsConstructor;
    import lombok.Setter;
    import lombok.val;
    import java.util.Set;
    import java.util.TreeSet;
    ......@@ -15,24 +18,41 @@ public abstract class Blocker {
    public interface BlockPredicate extends Predicate<ASTNode> {
    }
    @Data
    public static class Breakpoint {
    private int line;
    private String source;
    }
    public static class BreakpointLine implements BlockPredicate {
    @RequiredArgsConstructor
    public static class BreakpointLine<T> implements BlockPredicate {
    @Getter
    private final Interpreter<T> interpreter;
    @Getter
    @Setter
    private final Set<Integer> lines = new TreeSet<>();
    private final Set<Breakpoint> breakpoints = new TreeSet<>();
    private final Breakpoint cmp = new Breakpoint();
    private final Breakpoint cmp = new Breakpoint(null, 0);
    @Override
    public boolean test(ASTNode node) {
    cmp.line = node.getStartPosition().getLineNumber();
    cmp.source = node.getOrigin();
    return lines.contains(cmp);
    Evaluator<T> evaluator = new Evaluator<>(interpreter.getSelectedNode().getAssignments(), interpreter.getSelectedNode());
    for (Breakpoint brkpt : getBreakpoints()) {
    // check file name
    if (brkpt.getSourceName().equals(node.getOrigin())) {
    // check line
    if (brkpt.getLineNumber() == node.getStartPosition().getLineNumber()) {
    // if there is no condition
    if (brkpt.getConditionAst() == null) {
    return true; // no condition ==> trigger
    } else { // if there is a condition, we check:
    val v = evaluator.eval(brkpt.getConditionAst());
    if (v.getType() != SimpleType.BOOL)
    throw new InterpreterRuntimeException(
    String.format("Condition %s of breakpoint %s returned type %s",
    brkpt.getCondition(), brkpt, v.getType()));
    if (v.getData() == Boolean.TRUE)
    return true;
    }
    }
    }
    }
    return breakpoints.contains(cmp);
    }
    }
    ......@@ -46,10 +66,10 @@ public abstract class Blocker {
    @Override
    public boolean test(ASTNode astNode) {
    if (stepUntilBlock.get() > 0) {
    stepUntilBlock.decrementAndGet();
    if (stepUntilBlock.get() >= 0) {
    return 0 == stepUntilBlock.decrementAndGet();
    }
    return stepUntilBlock.get() == 0;
    return false;
    }
    public void deactivate() {
    ......
    ui/src/main/java/edu/kit/iti/formal/psdbg/gui/model/Breakpoint.java → rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/Breakpoint.java
    View file @ 4f5faf1f
    package edu.kit.iti.formal.psdbg.gui.model;
    package edu.kit.iti.formal.psdbg.interpreter.dbg;
    import edu.kit.iti.formal.psdbg.parser.Facade;
    import edu.kit.iti.formal.psdbg.parser.ast.Expression;
    import lombok.Data;
    import lombok.EqualsAndHashCode;
    import lombok.RequiredArgsConstructor;
    import lombok.ToString;
    import org.antlr.v4.runtime.CharStreams;
    import java.io.File;
    /**
    * @author Alexander Weigl
    * @version 1 (21.06.17)
    */
    @Data
    @RequiredArgsConstructor
    @ToString
    @EqualsAndHashCode
    public class Breakpoint {
    private File file;
    private String sourceName;
    private int lineNumber;
    private boolean enabled;
    private String condition;
    public Breakpoint(File file, int lineNumber) {
    this.file = file;
    private Expression conditionAst;
    public Breakpoint(String file, int lineNumber) {
    sourceName = file;
    this.lineNumber = lineNumber;
    }
    public boolean isConditional() {
    return condition != null;
    }
    }
    public void setCondition(String condition) {
    this.condition = condition;
    this.conditionAst = Facade.parseExpression(condition);
    }
    }
    \ No newline at end of file
    rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/DebuggerFramework.java
    View file @ 4f5faf1f
    ......@@ -42,16 +42,23 @@ public class DebuggerFramework<T> {
    private final List<Consumer<PTreeNode<T>>> currentStatePointerListener = new LinkedList<>();
    private final ProofTreeManager<T> ptreeManager;
    private final Thread interpreterThread;
    private final BlockListener<T> blocker;
    private final StateWrapper<T> stateWrapper;
    private Blocker.BreakpointLine<T> breakpointBlocker;
    public DebuggerFramework(@Nonnull Interpreter<T> interpreter,
    @Nonnull ProofScript main,
    MutableValueGraph<ControlFlowNode, ControlFlowTypes> cfg) {
    this.interpreter = interpreter;
    blocker = new BlockListener<>(interpreter);
    breakpointBlocker = new Blocker.BreakpointLine<>(interpreter);
    blocker.getPredicates().add(breakpointBlocker);
    stateWrapper = new StateWrapper<>(interpreter);
    ptreeManager = new ProofTreeManager<>(cfg);
    stateWrapper.setEmitNode(ptreeManager::receiveNode);
    ......@@ -116,7 +123,35 @@ public class DebuggerFramework<T> {
    blocker.unlock();
    }
    /**
    * Let the interpreter run, without adding any further blockers.
    */
    public void release() {
    blocker.unlock();
    }
    /**
    * Let the interpreter run, without adding any further blockers.
    */
    public void releaseForever() {
    blocker.getPredicates().clear();
    release();
    }
    public Set<PTreeNode<T>> getStates() {
    return ptreeManager.getNodes();
    }
    /**
    * Unregister all state pointer listeners.
    */
    public void unregister() {
    ptreeManager.getStatePointerListener().clear();
    }
    public Set<Breakpoint> getBreakpoints() {
    return breakpointBlocker.getBreakpoints();
    }
    }
    rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/ControlFlowVisitor.java deleted 100644 → 0
    View file @ c7ec5de9
    package edu.kit.iti.formal.psdbg.interpreter.graphs;
    import com.google.common.graph.EndpointPair;
    import com.google.common.graph.MutableValueGraph;
    import com.google.common.graph.ValueGraphBuilder;
    import edu.kit.iti.formal.psdbg.interpreter.funchdl.CommandLookup;
    import edu.kit.iti.formal.psdbg.interpreter.funchdl.ProofScriptHandler;
    import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
    import edu.kit.iti.formal.psdbg.parser.ast.*;
    import javafx.util.Pair;
    import java.util.*;
    /**
    * Visitor to create ProgramFlowGraph
    */
    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
    */
    private ControlFlowNode lastNode;
    /**
    * Control Flow Graph
    */
    private MutableValueGraph<ControlFlowNode, EdgeTypes> graph = ValueGraphBuilder.directed().allowsSelfLoops(true).build();
    /**
    * Call context
    */
    private LinkedList<ASTNode> context = new LinkedList<>();
    public ControlFlowVisitor(CommandLookup functionLookup) {
    this.functionLookup = functionLookup;
    mappingOfNodes = new HashMap<>();
    }
    /**
    * Return all nodes that have the parameter node as target in the graph
    *
    * @param node
    * @return
    */
    public Set<EndpointPair<ControlFlowNode>> getAllEdgesForNodeAsTarget(ASTNode node) {
    ControlFlowNode assocNode = mappingOfNodes.get(node);
    if (assocNode != null) {
    Set<EndpointPair<ControlFlowNode>> edges = new HashSet<>();
    graph.edges().forEach(e -> {
    if (e.target().equals(assocNode)) {
    edges.add(e);
    //System.out.println(e.target());
    //System.out.println(e.source());
    //System.out.println(graph.edgeValue(e.target(), e.source()));
    }
    });
    return edges;
    } else {
    return Collections.EMPTY_SET;
    }
    }
    public Collection<Pair<ControlFlowNode, EdgeTypes>> getPredecessorsAndTheirEdges(ASTNode node) {
    ControlFlowNode assocNode = getCorrespondingNode(node);
    List<Pair<ControlFlowNode, EdgeTypes>> allPreds = new LinkedList<>();
    if (assocNode != null) {
    graph.edges().forEach(edge -> {
    if (edge.target().equals(assocNode)) {
    allPreds.add(new Pair(edge.source(), graph.edgeValue(edge.source(), edge.target())));
    }
    });
    return allPreds;
    } else {
    return Collections.EMPTY_LIST;
    }
    }
    public ControlFlowNode getCorrespondingNode(ASTNode node) {
    ControlFlowNode ctrl = null;
    for (ASTNode astNode : mappingOfNodes.keySet()) {
    if (astNode.getStartPosition().equals(node.getStartPosition())
    && astNode.getEndPosition().equals(node.getEndPosition())) {
    ctrl = mappingOfNodes.get(astNode);
    break;
    }
    }
    return ctrl;
    }
    public Collection<Pair<ControlFlowNode, EdgeTypes>> getPredecessorsAsTarget(ASTNode node) {
    ControlFlowNode assocNode = getCorrespondingNode(node);
    List<Pair<ControlFlowNode, EdgeTypes>> allPreds = new LinkedList<>();
    if (assocNode != null) {
    graph.edges().forEach(edge -> {
    if (edge.source().equals(assocNode)) {
    allPreds.add(new Pair(edge.target(), graph.edgeValue(edge.source(), edge.target())));
    }
    });
    return allPreds;
    } else {
    return Collections.EMPTY_LIST;
    }
    }
    @Override
    public Void visit(ProofScript proofScript) {
    ControlFlowNode scriptNode = new ControlFlowNode(proofScript);
    context.add(proofScript);
    mappingOfNodes.put(proofScript, scriptNode);
    graph.addNode(scriptNode);
    lastNode = scriptNode;
    return this.visit(proofScript.getBody());
    }
    @Override
    public Void visit(AssignmentStatement assignment) {
    ControlFlowNode assignmentNode = new ControlFlowNode(assignment);
    mappingOfNodes.put(assignment, assignmentNode);
    graph.addNode(assignmentNode);
    lastNode = assignmentNode;
    return null;
    }
    @Override
    public Void visit(Statements statements) {
    //ControlFlowNode curLastNode = lastNode;
    for (Statement stmnt : statements) {
    stmnt.accept(this);
    //graph.putEdgeValue(curLastNode, lastNode, EdgeTypes.STEP_OVER);
    //graph.putEdgeValue(lastNode, curLastNode, EdgeTypes.STEP_BACK);
    //curLastNode = lastNode;
    }
    //lastNode = curLastNode;
    return null;
    }
    @Override
    public Void visit(CallStatement call) {
    ControlFlowNode currentNode = new ControlFlowNode(call);
    if (!context.isEmpty()) {
    currentNode.setCallCtx(context);
    }
    mappingOfNodes.put(call, currentNode);
    graph.addNode(currentNode);
    graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER);
    graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_BACK);
    lastNode = currentNode;
    boolean atomic = functionLookup.isAtomic(call);
    //Annahme: wenn ich zwischendrin keine return kante habe, dann wird solange durchgegangen, bis eine return kante da ist
    if (atomic) {
    LinkedList<ASTNode> copiedContext = new LinkedList<>();
    //to check whether context is restored properly, copy context before call
    context.stream().forEach(e -> {
    copiedContext.add(e);
    });
    context.add(call);
    ProofScriptHandler psh = (ProofScriptHandler) functionLookup.getBuilder(call);
    psh.getScript(call.getCommand()).getBody().accept(this);
    //verbinde letzten knoten aus auruf mit step return zu aktuellem knoten
    graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN);
    graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_INTO);
    context.removeLast();
    //check if context is restored properly
    //copiedcontext == context
    }
    lastNode = currentNode;
    return null;
    }
    @Override
    public Void visit(ForeachStatement foreach) {
    ControlFlowNode currentNode = new ControlFlowNode(foreach);
    mappingOfNodes.put(foreach, currentNode);
    graph.addNode(currentNode);
    //System.out.println("\n" + currentNode + "\n");
    graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_OVER);
    graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_BACK);
    lastNode = currentNode;
    foreach.getBody().accept(this);
    graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN);
    //lastNode = currentNode; ??
    return null;
    }
    @Override
    public Void visit(TheOnlyStatement theOnly) {
    ControlFlowNode currentNode = new ControlFlowNode(theOnly);
    mappingOfNodes.put(theOnly, currentNode);
    graph.addNode(currentNode);
    //System.out.println("\n" + currentNode + "\n");
    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
    public Void visit(RepeatStatement repeatStatement) {
    ControlFlowNode currentNode = new ControlFlowNode(repeatStatement);
    mappingOfNodes.put(repeatStatement, currentNode);
    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
    public Void visit(CasesStatement casesStatement) {
    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) {
    // if (aCase.isClosedStmt) {
    // } else {
    ControlFlowNode caseNode = new ControlFlowNode(aCase);
    mappingOfNodes.put(aCase, caseNode);
    graph.addNode(caseNode);
    //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, casesNode, EdgeTypes.STEP_RETURN);
    // }
    }
    //casesStatement.getDefaultCase()
    if (casesStatement.getDefCaseStmt() != null) {
    DefaultCaseStatement defCase = casesStatement.getDefCaseStmt();
    ControlFlowNode caseNode = new ControlFlowNode(defCase);
    mappingOfNodes.put(defCase, caseNode);
    graph.addNode(caseNode);
    //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, 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(casesNode, caseNode, EdgeTypes.STEP_OVER); //??is this right?
    graph.putEdgeValue(caseNode, casesNode, EdgeTypes.STEP_BACK);
    lastNode = caseNode;
    defaultCase.accept(this);
    graph.putEdgeValue(lastNode, casesNode, EdgeTypes.STEP_RETURN);*/
    }
    lastNode = casesNode;
    return null;
    }
    public String asdot() {
    StringBuilder sb = new StringBuilder();
    sb.append("digraph G {\nnode [shape=rect]\n ");
    graph.nodes().forEach(n -> {
    sb.append(n.hashCode())
    .append(" [label=\"")
    .append(n.getScriptstmt().getNodeName())
    .append("@")
    .append(n.getScriptstmt().getStartPosition().getLineNumber())
    .append("\"]\n");
    });
    graph.edges().forEach(edge -> {
    sb.append(edge.source().hashCode())
    .append(" -> ")
    .append(edge.target().hashCode())
    .append(" [label=\"")
    .append(graph.edgeValue(edge.source(), edge.target()).name())
    .append("\"]\n");
    });
    sb.append("}");
    return sb.toString();
    }
    public MutableValueGraph<ControlFlowNode, EdgeTypes> getGraph() {
    return graph;
    }
    }
    rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/graphs/PTreeNode.java deleted 100644 → 0
    View file @ c7ec5de9
    package edu.kit.iti.formal.psdbg.interpreter.graphs;
    import edu.kit.iti.formal.psdbg.interpreter.data.InterpreterExtendedState;
    import edu.kit.iti.formal.ps