Skip to content

GitLab

P
ProofScriptParser
Commit 8feff6db authored by Sarah Grebing's avatar Sarah Grebing
Browse files
Options

adderd flag for matchexpreesion

parent 985b0a8b
Pipeline #10677 passed with stage
    in 2 minutes and 15 seconds
    Hide whitespace changes
    Inline Side-by-side
    Showing with 264 additions and 112 deletions
    pom.xml
    View file @ 8feff6db
    ......@@ -97,41 +97,6 @@
    <visitor>true</visitor>
    </configuration>
    </plugin>
    <!--<plugin>
    <groupId>org.apache.maven.plugins</groupId>
    <artifactId>maven-install-plugin</artifactId>
    <version>2.5</version>
    <executions>
    <execution>
    <id>keyinstall</id>
    <phase>initialize</phase>
    <goals>
    <goal>install-file</goal>
    </goals>
    <configuration>
    <groupId>org.key-project</groupId>
    <artifactId>key.core</artifactId>
    <version>2.7</version>
    <packaging>jar</packaging>
    <file>${basedir}/lib/key.core.jar</file>
    </configuration>
    </execution>
    <execution>
    <id>recoderinstall</id>
    <phase>initialize</phase>
    <goals>
    <goal>install-file</goal>
    </goals>
    <configuration>
    <groupId>org.key-project</groupId>
    <artifactId>recoderKey</artifactId>
    <version>1.0.0</version>
    <packaging>jar</packaging>
    <file>${basedir}/lib/recoderKey.jar</file>
    </configuration>
    </execution>
    </executions>
    </plugin>-->
    </plugins>
    </build>
    ......
    src/main/java/edu/kit/formal/dbg/Debugger.java
    View file @ 8feff6db
    ......@@ -4,11 +4,17 @@ import edu.kit.formal.interpreter.*;
    import edu.kit.formal.interpreter.funchdl.BuiltinCommands;
    import edu.kit.formal.interpreter.funchdl.CommandHandler;
    import edu.kit.formal.interpreter.funchdl.DefaultLookup;
    import edu.kit.formal.proofscriptparser.*;
    import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
    import edu.kit.formal.proofscriptparser.Facade;
    import edu.kit.formal.proofscriptparser.ScriptLanguageParser;
    import edu.kit.formal.proofscriptparser.TransformAst;
    import edu.kit.formal.proofscriptparser.ast.*;
    import org.antlr.v4.runtime.CharStreams;
    import java.io.*;
    import java.io.BufferedReader;
    import java.io.File;
    import java.io.IOException;
    import java.io.InputStreamReader;
    import java.math.BigInteger;
    import java.util.List;
    import java.util.function.BiConsumer;
    ......@@ -36,7 +42,6 @@ public class Debugger {
    interpreter.getEntryListeners().add(history);
    interpreter.getEntryListeners().add(blocker);
    interpreter.getEntryListeners().add(new CommandLogger());
    //TODO install debugger functions
    registerDebuggerFunction("step", this::step);
    registerDebuggerFunction("b", this::setBreakpoint);
    ......@@ -47,6 +52,11 @@ public class Debugger {
    registerDebuggerFunction("status", this::status);
    }
    public static void main(String[] args) throws IOException {
    Debugger d = new Debugger("src/test/resources/edu/kit/formal/interpreter/dbg.kps");
    d.run();
    }
    private void registerDebuggerFunction(final String step,
    BiConsumer<CallStatement, VariableAssignment> func) {
    debuggerFunctions.getBuilders().add(new CommandHandler() {
    ......@@ -62,11 +72,6 @@ public class Debugger {
    });
    }
    public static void main(String[] args) throws IOException {
    Debugger d = new Debugger("src/test/resources/edu/kit/formal/interpreter/dbg.kps");
    d.run();
    }
    private void run() throws IOException {
    blocker.stepUntilBlock.set(2);
    interpreterThread = new Thread(() -> {
    ......
    src/main/java/edu/kit/formal/interpreter/Evaluator.java
    View file @ 8feff6db
    ......@@ -7,7 +7,6 @@ import lombok.Getter;
    import lombok.Setter;
    import java.util.ArrayList;
    import java.util.Collections;
    import java.util.List;
    /**
    ......@@ -17,19 +16,16 @@ import java.util.List;
    * @author A. Weigl
    */
    public class Evaluator extends DefaultASTVisitor<Value> implements ScopeObservable {
    private final GoalNode goal;
    private final VariableAssignment state;
    private List<VariableAssignment> matchedVariables = new ArrayList<>();
    @Getter
    @Setter
    private MatcherApi matcher;
    @Getter
    private List<Visitor> entryListeners = new ArrayList<>(),
    exitListeners = new ArrayList<>();
    private final GoalNode goal;
    private final VariableAssignment state;
    public Evaluator(VariableAssignment assignment, GoalNode node) {
    state = new VariableAssignment(assignment); // unmodifiable version of assignment
    goal = node;
    ......@@ -122,4 +118,7 @@ public class Evaluator extends DefaultASTVisitor<Value> implements ScopeObservab
    }
    public List<VariableAssignment> getMatchedVariables() {
    return null;
    }
    }
    src/main/java/edu/kit/formal/interpreter/GoalNode.java
    View file @ 8feff6db
    package edu.kit.formal.interpreter;
    import de.uka.ilkd.key.api.ProjectedNode;
    import edu.kit.formal.proofscriptparser.ast.Type;
    import lombok.Getter;
    ......@@ -7,24 +8,40 @@ import lombok.Getter;
    * Objects of this class represent a GoalNode in a script state
    * If parent is null, this is the root
    *
    * This object wraps a ProjectedNode
    * @author S.Grebing
    */
    public class GoalNode {
    //TODO this is only for testing, later Sequent object or similar
    @Getter
    private String sequent;
    private String sequent; //TODO this is only for testing, when connected with key using projectednode
    private VariableAssignment assignments;
    private GoalNode parent;
    @Getter
    private ProjectedNode actualKeYGoalNode;
    /**
    * This conctructur will be replaced with concrete one that uses projectedNode
    *
    * @param parent
    * @param seq
    */
    public GoalNode(GoalNode parent, String seq) {
    //BUG: Hier muesste deepcopy der assignments passieren
    this.assignments = new VariableAssignment(parent == null ? null : parent.deepCopyAssignments());
    this.parent = parent;
    this.sequent = seq;
    actualKeYGoalNode = null;
    }
    public GoalNode(GoalNode parent, String seq, ProjectedNode pNode) {
    this.actualKeYGoalNode = pNode;
    this.assignments = new VariableAssignment(parent == null ? null : parent.deepCopyAssignments());
    this.parent = parent;
    this.sequent = seq;
    }
    private VariableAssignment deepCopyAssignments() {
    return assignments.deepCopy();
    }
    ......@@ -119,4 +136,6 @@ public class GoalNode {
    //TODO method does nothing helpful atm
    return new GoalNode(this.getParent(), sequent);
    }
    }
    src/main/java/edu/kit/formal/interpreter/HistoryListener.java
    View file @ 8feff6db
    ......@@ -4,7 +4,6 @@ import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
    import edu.kit.formal.proofscriptparser.ast.ASTNode;
    import lombok.Getter;
    import lombok.RequiredArgsConstructor;
    import lombok.Setter;
    import java.util.LinkedList;
    import java.util.List;
    ......@@ -28,4 +27,6 @@ public class HistoryListener extends DefaultASTVisitor<Void> {
    queueNode.add(node);
    return null;
    }
    }
    src/main/java/edu/kit/formal/interpreter/Interpreter.java
    View file @ 8feff6db
    ......@@ -2,16 +2,13 @@ package edu.kit.formal.interpreter;
    import de.uka.ilkd.key.api.ScriptApi;
    import de.uka.ilkd.key.macros.scripts.EngineState;
    import edu.kit.formal.interpreter.funchdl.CommandCall;
    import edu.kit.formal.interpreter.funchdl.CommandLookup;
    import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
    import edu.kit.formal.proofscriptparser.Visitor;
    import edu.kit.formal.proofscriptparser.ast.*;
    import lombok.Getter;
    import lombok.Setter;
    import org.antlr.v4.runtime.ParserRuleContext;
    import javax.xml.bind.annotation.XmlSeeAlso;
    import java.util.*;
    import java.util.logging.Logger;
    ......@@ -22,10 +19,10 @@ import java.util.logging.Logger;
    */
    public class Interpreter extends DefaultASTVisitor<Void>
    implements ScopeObservable {
    private static final int MAX_ITERATIONS = 5;
    private static Logger logger = Logger.getLogger("interpreter");
    //TODO later also include information about source line for each state (for debugging purposes and rewind purposes)
    private Stack<AbstractState> stateStack = new Stack<>();
    private static Logger logger = Logger.getLogger("interpreter");
    @Getter
    private List<Visitor> entryListeners = new ArrayList<>(),
    exitListeners = new ArrayList<>();
    ......@@ -52,10 +49,23 @@ public class Interpreter extends DefaultASTVisitor<Void>
    newState(new GoalNode(null, sequent));
    //execute first script (RULE: The first script in the file is main script)
    ProofScript m = scripts.get(0);
    //later through interface with getMainScript();
    //create new state
    m.accept(this);
    }
    /**
    * If new Block is entered, a new state has to be created (copy of current state) and pushed to the stack
    */
    private void enterScope() {
    }
    /**
    * If block is extied the top state on the stack has to be removed
    */
    private void exitScope() {
    }
    /**
    * Visit a proof script (context is handled by the call of the script noch by visiting the script itself)
    ......@@ -92,7 +102,6 @@ public class Interpreter extends DefaultASTVisitor<Void>
    if (t != null) {
    node.addVarDecl(var.getIdentifier(), t);
    }
    if (expr != null) {
    Type type = node.lookUpType(var.getIdentifier());
    if (type == null) {
    ......@@ -139,28 +148,39 @@ public class Interpreter extends DefaultASTVisitor<Void>
    }
    /**
    *
    * @param casesStatement
    * @return
    */
    @Override
    public Void visit(CasesStatement casesStatement) {
    enterScope(casesStatement);
    State beforeCases = (State) stateStack.pop();
    AbstractState beforeCases = stateStack.pop();
    List<GoalNode> allGoalsBeforeCases = beforeCases.getGoals();
    for (GoalNode node : allGoalsBeforeCases) {
    node.enterNewVarScope();
    }
    //global List after all Case Statements
    List<GoalNode> goalsAfterCases = new ArrayList<>();
    //copy the list of goal nodes for keeping track of goals
    Set<GoalNode> copiedList = new HashSet<>();
    for (GoalNode goalNode : allGoalsBeforeCases) {
    copiedList.add(goalNode);
    }
    Set<GoalNode> copiedList = new HashSet<>(allGoalsBeforeCases);
    //handle cases
    List<CaseStatement> cases = casesStatement.getCases();
    Iterator<CaseStatement> casesIter = cases.iterator();
    for (CaseStatement aCase : cases) {
    Map<GoalNode, VariableAssignment> matchedGoals = matchGoal(copiedList, aCase);
    if (matchedGoals != null) {
    copiedList.removeAll(matchedGoals.entrySet());
    goalsAfterCases.addAll(executeCase(aCase.getBody(), matchedGoals.keySet()));
    }
    }
    /* Iterator<CaseStatement> casesIter = cases.iterator();
    while (casesIter.hasNext()) {
    //get information for case
    CaseStatement currentCase = casesIter.next();
    Expression guard = currentCase.getGuard();
    ......@@ -174,44 +194,20 @@ public class Interpreter extends DefaultASTVisitor<Void>
    while (goalIter.hasNext()) {
    GoalNode g = goalIter.next();
    Value eval = evaluate(g, guard);
    System.out.println();
    if (eval.getData().equals(true)) {
    forCase.add(g);
    }
    }
    copiedList.removeAll(forCase);
    //for each selected goal put a state onto tze stack and visit the body of the case
    Iterator<GoalNode> caseGoals = forCase.iterator();
    while (caseGoals.hasNext()) {
    GoalNode current = caseGoals.next();
    List<GoalNode> goalList = new ArrayList<>();
    goalList.add(current);
    State s = new State(goalList, current);
    stateStack.push(s);
    visit(body);
    //after executing the body collect the newly created goals form the stack and remove the state
    State aftercase = (State) stateStack.pop();
    goalsAfterCases.addAll(aftercase.getGoals());
    }
    goalsAfterCases.addAll(executeCase(body, forCase));
    }
    */
    //for all remaining goals execute default
    if (!copiedList.isEmpty()) {
    Statements defaultCase = casesStatement.getDefaultCase();
    Iterator<GoalNode> remainingGoalsIter = copiedList.iterator();
    while (remainingGoalsIter.hasNext()) {
    GoalNode next = remainingGoalsIter.next();
    List<GoalNode> goalList = new ArrayList<>();
    goalList.add(next);
    State s = new State(goalList, next);
    stateStack.push(s);
    visit(defaultCase);
    State aftercase = (State) stateStack.pop();
    goalsAfterCases.addAll(aftercase.getGoals());
    }
    goalsAfterCases.addAll(executeCase(defaultCase, copiedList));
    }
    ......@@ -219,9 +215,8 @@ public class Interpreter extends DefaultASTVisitor<Void>
    State newStateAfterCases;
    if (!goalsAfterCases.isEmpty()) {
    for (GoalNode goalAfterCases : goalsAfterCases) {
    goalAfterCases.exitNewVarScope();
    }
    goalsAfterCases.forEach(node -> node.exitNewVarScope());
    if (goalsAfterCases.size() == 1) {
    newStateAfterCases = new State(goalsAfterCases, goalsAfterCases.get(0));
    } else {
    ......@@ -234,6 +229,78 @@ public class Interpreter extends DefaultASTVisitor<Void>
    return null;
    }
    /**
    * Match a set of goal nodes against a matchpattern of a case and return the metched goals together with instantiated variables
    *
    * @param allGoalsBeforeCases
    * @param aCase
    * @return
    */
    private Map<GoalNode, VariableAssignment> matchGoal(Set<GoalNode> allGoalsBeforeCases, CaseStatement aCase) {
    HashMap<GoalNode, VariableAssignment> matchedGoals = new HashMap<>();
    Expression matchExpression = aCase.getGuard();
    for (GoalNode goal : allGoalsBeforeCases) {
    VariableAssignment va = evaluateMatchInGoal(matchExpression, goal);
    if (va != null) {
    matchedGoals.put(goal, va);
    }
    }
    return matchedGoals;
    }
    /**
    * Evaluate a match in a specific goal
    *
    * @param matchExpression
    * @param goal
    * @return
    */
    private VariableAssignment evaluateMatchInGoal(Expression matchExpression, GoalNode goal) {
    enterScope(matchExpression);
    Evaluator eval = new Evaluator(goal.getAssignments(), goal);
    eval.setMatcher(matcherApi);
    eval.getEntryListeners().addAll(entryListeners);
    eval.getExitListeners().addAll(exitListeners);
    exitScope(matchExpression);
    Value v = eval.eval(matchExpression);
    if (v.getData().equals(Value.TRUE)) {
    if (eval.getMatchedVariables().size() == 0) {
    return new VariableAssignment();
    } else {
    return eval.getMatchedVariables().get(0);
    }
    }
    return null;
    }
    /**
    * For each selected goal put a state onto the stack and visit the body of the case
    *
    * @param
    * @param caseStmts
    * @param goalsToApply @return
    */
    private List<GoalNode> executeCase(Statements caseStmts, Set<GoalNode> goalsToApply) {
    enterScope(caseStmts);
    List<GoalNode> goalsAfterCases = new ArrayList<>();
    for (GoalNode next : goalsToApply) {
    List<GoalNode> goalList = new ArrayList<>();
    goalList.add(next);
    State s = new State(goalList, next);
    stateStack.push(s);
    caseStmts.accept(this);
    State aftercase = (State) stateStack.pop();
    goalsAfterCases.addAll(aftercase.getGoals());
    }
    exitScope(caseStmts);
    return goalsAfterCases;
    }
    /**
    * @param caseStatement
    ......@@ -272,7 +339,6 @@ public class Interpreter extends DefaultASTVisitor<Void>
    return null;
    }
    public VariableAssignment evaluateParameters(Parameters parameters) {
    VariableAssignment va = new VariableAssignment();
    parameters.entrySet().forEach(entry -> {
    ......@@ -328,8 +394,10 @@ public class Interpreter extends DefaultASTVisitor<Void>
    @Override
    public Void visit(RepeatStatement repeatStatement) {
    enterScope(repeatStatement);
    int counter = 0;
    boolean b = false;
    do {
    counter++;
    AbstractState prev = getCurrentState();
    repeatStatement.getBody().accept(this);
    AbstractState end = getCurrentState();
    ......@@ -337,6 +405,7 @@ public class Interpreter extends DefaultASTVisitor<Void>
    Set<GoalNode> prevNodes = new HashSet<>(prev.getGoals());
    Set<GoalNode> endNodes = new HashSet<>(end.getGoals());
    b = prevNodes.equals(endNodes);
    b = b && counter <= MAX_ITERATIONS;
    } while (b);
    exitScope(repeatStatement);
    return null;
    ......@@ -366,6 +435,12 @@ public class Interpreter extends DefaultASTVisitor<Void>
    return getCurrentGoals().get(0);
    }
    }
    /* @Override
    public T visit(Parameters parameters) {
    parameters.entrySet();
    System.out.println("Params " + parameters.toString());
    return null;
    }*/
    public AbstractState getCurrentState() {
    return stateStack.peek();
    ......
    src/main/java/edu/kit/formal/interpreter/VariableAssignment.java
    View file @ 8feff6db
    ......@@ -3,7 +3,10 @@ package edu.kit.formal.interpreter;
    import edu.kit.formal.proofscriptparser.ast.Type;
    import java.util.HashMap;
    import java.util.HashSet;
    import java.util.Map;
    import java.util.Set;
    import java.util.stream.Collectors;
    /**
    * Variable Assignments for each goal node
    ......@@ -142,4 +145,44 @@ public class VariableAssignment {
    public Map<String, Value> asMap() {
    return asMap(new HashMap<>());
    }
    /**
    * Method joins two variable assignments without checking their compatibility
    *
    * @param assignment
    * @return
    */
    public VariableAssignment joinWithoutCheck(VariableAssignment assignment) {
    this.getValues().putAll(assignment.getValues());
    this.getTypes().putAll(assignment.getTypes());
    return this;
    }
    /**
    * @param assignment
    * @return empty variable assignment if not possible to join conflictfree (i.e., if a variable name is present in both assignments with different types or dfferent values)
    * @throws RuntimeException
    */
    public VariableAssignment joinWithCheck(VariableAssignment assignment) throws RuntimeException {
    Set<String> namesV2 = assignment.getValues().keySet();
    Set<String> nonConflicting = new HashSet<>();
    Set<String> conflictingCand = new HashSet<>();
    //subtract V2 from V1 and add the nonconflicting varNames into the nonconflicting set
    nonConflicting = this.getValues().keySet().stream().filter(item -> !namesV2.contains(item)).collect(Collectors.toSet());
    //subtract V1 from V2 and add the nonconflicting varNames into the nonconflicting set
    nonConflicting.addAll(namesV2.stream().filter(item -> !this.getValues().keySet().contains(item)).collect(Collectors.toSet()));
    //create intersection
    conflictingCand = this.getValues().keySet().stream().filter(item -> namesV2.contains(item)).collect(Collectors.toSet());
    if (!conflictingCand.isEmpty()) {
    for (String s : conflictingCand) {
    if (!this.lookupVarValue(s).equals(assignment.lookupVarValue(s))) {
    return new VariableAssignment(null);
    }
    }
    }
    return this.joinWithoutCheck(assignment);
    }
    }
    src/main/java/edu/kit/formal/proofscriptparser/ast/BinaryExpression.java
    View file @ 8feff6db
    ......@@ -75,6 +75,11 @@ public class BinaryExpression extends Expression<ParserRuleContext> {
    return operator.returnType();
    }
    @Override
    public boolean hasMatchExpression() {
    return left.hasMatchExpression() || right.hasMatchExpression();
    }
    /**
    * {@inheritDoc}
    */
    ......
    src/main/java/edu/kit/formal/proofscriptparser/ast/BooleanLiteral.java
    View file @ 8feff6db
    ......@@ -65,6 +65,11 @@ public class BooleanLiteral extends Literal {
    return visitor.visit(this);
    }
    @Override
    public boolean hasMatchExpression() {
    return false;
    }
    /**
    * {@inheritDoc}
    */
    ......
    src/main/java/edu/kit/formal/proofscriptparser/ast/Expression.java
    View file @ 8feff6db
    ......@@ -34,6 +34,24 @@ import org.antlr.v4.runtime.ParserRuleContext;
    * @version 1 (28.04.17)
    */
    public abstract class Expression<T extends ParserRuleContext> extends ASTNode<T> {
    /**
    * @param type
    * @param e
    * @param signature
    * @throws NotWelldefinedException
    */
    public static final void checkType(Type type, Expression e, Signature signature) throws NotWelldefinedException {
    Type got = e.getType(signature);
    if (!type.equals(got)) {
    throw new NotWelldefinedException("Typemismatch in expected " + type + ", got" + got, e);
    }
    }
    /**
    * @return returns true if a child expression contains a match expression
    */
    public abstract boolean hasMatchExpression();
    /**
    * Returns the precedence of the operator expression.
    * <p>
    ......@@ -54,17 +72,4 @@ public abstract class Expression<T extends ParserRuleContext> extends ASTNode<T>
    */
    public abstract Type getType(Signature signature)
    throws NotWelldefinedException;
    /**
    * @param type
    * @param e
    * @param signature
    * @throws NotWelldefinedException
    */
    public static final void checkType(Type type, Expression e, Signature signature) throws NotWelldefinedException {
    Type got = e.getType(signature);
    if (!type.equals(got)) {
    throw new NotWelldefinedException("Typemismatch in expected " + type + ", got" + got, e);
    }
    }
    }
    src/main/java/edu/kit/formal/proofscriptparser/ast/IntegerLiteral.java
    View file @ 8feff6db
    ......@@ -59,6 +59,11 @@ public class IntegerLiteral extends Literal {
    return visitor.visit(this);
    }
    @Override
    public boolean hasMatchExpression() {
    return false;
    }