Commit 79786fc6 authored by Sarah Grebing's avatar Sarah Grebing

Reverted changes for cases and some bugfixes

parent 79fbb50d
Pipeline #13264 failed with stage
in 10 seconds
......@@ -112,9 +112,9 @@ public class ASTChanger extends DefaultASTVisitor<ASTNode> {
}
@Override
public tryCase visit(tryCase tryCase) {
tryCase.getBody().accept(this);
return tryCase;
public TryCase visit(TryCase TryCase) {
TryCase.getBody().accept(this);
return TryCase;
}
@Override
......
......@@ -161,8 +161,8 @@ public interface ASTTraversal<T> extends Visitor<T> {
}
@Override
default T visit(tryCase tryCase) {
tryCase.getBody().accept(this);
default T visit(TryCase TryCase) {
TryCase.getBody().accept(this);
return null;
}
......
......@@ -133,8 +133,8 @@ public class DefaultASTVisitor<T> implements Visitor<T> {
}
@Override
public T visit(tryCase tryCase) {
return defaultVisit(tryCase);
public T visit(TryCase TryCase) {
return defaultVisit(TryCase);
}
@Override
......
......@@ -319,10 +319,10 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
public Object visitCasesList(ScriptLanguageParser.CasesListContext ctx) {
if (ctx.TRY() != null) {
tryCase tryCase = new tryCase();
tryCase.setRuleContext(ctx);
tryCase.setBody((Statements) ctx.body.accept(this));
return tryCase;
TryCase TryCase = new TryCase();
TryCase.setRuleContext(ctx);
TryCase.setBody((Statements) ctx.body.accept(this));
return TryCase;
}
if (ctx.closesScript != null) {
ClosesCase closesCase = new ClosesCase();
......
......@@ -68,7 +68,7 @@ public interface Visitor<T> {
T visit(UnaryExpression e);
T visit(tryCase tryCase);
T visit(TryCase TryCase);
T visit(SimpleCaseStatement simpleCaseStatement);
......
......@@ -9,10 +9,10 @@ import lombok.NoArgsConstructor;
*/
@Data
@NoArgsConstructor
public class tryCase extends CaseStatement {
public class TryCase extends CaseStatement {
private boolean isClosedStmt = true;
public tryCase(Statements body) {
public TryCase(Statements body) {
this.body = body;
}
......@@ -28,7 +28,7 @@ public class tryCase extends CaseStatement {
* {@inheritDoc}
*/
@Override
public tryCase copy() {
return new tryCase(body.copy());
public TryCase copy() {
return new TryCase(body.copy());
}
}
......@@ -12,7 +12,7 @@ import edu.kit.iti.formal.psdbg.interpreter.data.State;
import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.interpreter.funchdl.CommandLookup;
import edu.kit.iti.formal.psdbg.parser.ast.ClosesCase;
import edu.kit.iti.formal.psdbg.parser.ast.tryCase;
import edu.kit.iti.formal.psdbg.parser.ast.TryCase;
import edu.kit.iti.formal.psdbg.parser.types.SimpleType;
import lombok.Getter;
import org.key_project.util.collection.ImmutableList;
......@@ -46,24 +46,43 @@ public class KeyInterpreter extends Interpreter<KeyData> {
@Override
public Object visit(ClosesCase closesCase) {
State<KeyData> currentStateToMatch = peekState();
State<KeyData> currentStateToMatchCopy = peekState().copy(); //deepcopy
State<KeyData> currentStateToMatchCopy = currentStateToMatch.copy(); //deepcopy
GoalNode<KeyData> selectedGoalNode = currentStateToMatch.getSelectedGoalNode();
GoalNode<KeyData> selectedGoalCopy = currentStateToMatch.getSelectedGoalNode().deepCopy(); //deepcopy
enterScope(closesCase);
// executeBody(closesCase.getClosesScript(), )
//execute closesscript
executeBody(closesCase.getClosesScript(), selectedGoalNode, new VariableAssignment(selectedGoalNode.getAssignments()));
//check whether script closed proof
State<KeyData> stateafterIsClosable = peekState();
List<GoalNode<KeyData>> goals = stateafterIsClosable.getGoals();
boolean allClosed = true;
for (GoalNode<KeyData> goal : goals) {
KeyData data = (KeyData) goal.getData();
if (!data.getNode().isClosed()) {
allClosed = false;
break;
}
}
//prune proof
System.out.println("The closes script " + (allClosed ? "closed the proof.\n" : "did not close the proof.\n") + "Rolling Back proof now.");
Proof currentKeYproof = selectedGoalNode.getData().getProof();
ImmutableList<Goal> subtreeGoals = currentKeYproof.getSubtreeGoals(((KeyData) selectedGoalNode.getData()).getNode());
currentKeYproof.pruneProof(selectedGoalCopy.getData().getNode());
popState();
pushState(currentStateToMatchCopy);
exitScope(closesCase);
return false;
return allClosed;
}
@Override
public Object visit(tryCase tryCase) {
public Object visit(TryCase TryCase) {
State<KeyData> currentStateToMatch = peekState();
State<KeyData> currentStateToMatchCopy = peekState().copy(); //deepcopy
State<KeyData> currentStateToMatchCopy = currentStateToMatch.copy(); //deepcopy
GoalNode<KeyData> selectedGoalNode = currentStateToMatch.getSelectedGoalNode();
GoalNode<KeyData> selectedGoalCopy = currentStateToMatch.getSelectedGoalNode().deepCopy(); //deepcopy
enterScope(tryCase);
executeBody(tryCase.getBody(), selectedGoalNode, new VariableAssignment(selectedGoalNode.getAssignments()));
enterScope(TryCase);
executeBody(TryCase.getBody(), selectedGoalNode, new VariableAssignment(selectedGoalNode.getAssignments()));
State<KeyData> stateafterIsClosable = peekState();
List<GoalNode<KeyData>> goals = stateafterIsClosable.getGoals();
boolean allClosed = true;
......@@ -83,7 +102,7 @@ public class KeyInterpreter extends Interpreter<KeyData> {
pushState(currentStateToMatchCopy);
}
//check if state is closed
exitScope(tryCase);
exitScope(TryCase);
return allClosed;
/* //executeBody and if goal is closed afterwards return true
......
......@@ -8,7 +8,6 @@ import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
import org.antlr.v4.runtime.CharStreams;
import org.junit.Assert;
import org.junit.Before;
import org.junit.Ignore;
import org.junit.Test;
import java.io.File;
......@@ -35,7 +34,7 @@ public class KeYInterpreterTest {
return i;
}
@Ignore
@Test
public void testIsClosable() throws IOException, ProblemLoaderException {
facade.loadKeyFileSync(new File("src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/contraposition.key"));
......
package edu.kit.iti.formal.psdbg.interpreter;
import com.google.common.collect.Sets;
import edu.kit.iti.formal.psdbg.interpreter.assignhook.VariableAssignmentHook;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.State;
......@@ -13,10 +12,8 @@ import edu.kit.iti.formal.psdbg.parser.Visitor;
import edu.kit.iti.formal.psdbg.parser.ast.*;
import edu.kit.iti.formal.psdbg.parser.data.Value;
import edu.kit.iti.formal.psdbg.parser.types.Type;
import javafx.util.Pair;
import lombok.Getter;
import lombok.Setter;
import sun.reflect.generics.reflectiveObjects.NotImplementedException;
import java.util.*;
import java.util.logging.Logger;
......@@ -167,38 +164,13 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
return null;
}
@Override
public Object visit(tryCase tryCase) {
enterScope(tryCase);
exitScope(tryCase);
return false;
}
@Override
public Object visit(SimpleCaseStatement simpleCaseStatement) {
Expression matchExpression = simpleCaseStatement.getGuard();
State<T> currentStateToMatch = peekState();
GoalNode<T> selectedGoal = currentStateToMatch.getSelectedGoalNode();
VariableAssignment va = evaluateMatchInGoal(matchExpression, selectedGoal);
if (va != null) {
enterScope(simpleCaseStatement);
executeBody(simpleCaseStatement.getBody(), selectedGoal, va);
exitScope(simpleCaseStatement);
return true;
} else {
return false;
}
}
/**
* Old visit method, for deocumentation purposes
*
* @param casesStatement
* @return
*/
@Deprecated
public Object visitOld(CasesStatement casesStatement) {
@Override
public Object visit(CasesStatement casesStatement) {
enterScope(casesStatement);
State<T> beforeCases = peekState();
......@@ -212,7 +184,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
//handle cases
List<CaseStatement> cases = casesStatement.getCases();
Map<GoalNode, Pair<VariableAssignment, Statements>> goalToCaseMapping = matchGoalsToCases(allGoalsBeforeCases, casesStatement);
// Map<GoalNode, Pair<VariableAssignment, Statements>> goalToCaseMapping = matchGoalsToCases(allGoalsBeforeCases, casesStatement);
for (GoalNode<T> goal : allGoalsBeforeCases) {
newState(goal); //to allow the visit method for the case stmt to retrieve goal
......@@ -266,13 +238,37 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
return null;
}
/* @Override
public Object visit(SimpleCaseStatement simpleCaseStatement) {
Expression matchExpression = simpleCaseStatement.getGuard();
State<T> currentStateToMatch = peekState();
GoalNode<T> selectedGoal = currentStateToMatch.getSelectedGoalNode();
VariableAssignment va = evaluateMatchInGoal(matchExpression, selectedGoal);
if (va != null) {
enterScope(simpleCaseStatement);
executeBody(simpleCaseStatement.getBody(), selectedGoal, va);
exitScope(simpleCaseStatement);
return true;
} else {
return false;
}
}*/
@Override
public Object visit(TryCase TryCase) {
enterScope(TryCase);
exitScope(TryCase);
return false;
}
/**
* Computes which goals are handled by the different cases in the order the cases appear in the script
* @param allGoalsBeforeCases
* @param cases all cases as ordered list
* @return a mapping of each goal to the matched case body together with variableassignments from the matching process
*/
private Map<GoalNode, Pair<VariableAssignment, Statements>> matchGoalsToCases(List<GoalNode<T>> allGoalsBeforeCases, CasesStatement cases) {
/* private Map<GoalNode, Pair<VariableAssignment, Statements>> matchGoalsToCases(List<GoalNode<T>> allGoalsBeforeCases, CasesStatement cases) {
//list of cases
List<CaseStatement> caseStmts = cases.getCases();
//remaining goals
......@@ -302,7 +298,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
return returnMap;
}
}*/
/**
* Match a set of goal nodes against a matchpattern of a case and return the matched goals together with instantiated variables
......@@ -311,7 +307,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
* @param aCase
* @return
*/
private Map<GoalNode<T>, VariableAssignment> matchGoal(Set<GoalNode<T>> allGoalsBeforeCases, CaseStatement aCase) {
/* private Map<GoalNode<T>, VariableAssignment> matchGoal(Set<GoalNode<T>> allGoalsBeforeCases, CaseStatement aCase) {
HashMap<GoalNode<T>, VariableAssignment> matchedGoals = new HashMap<>();
if (!aCase.isClosedStmt()) {
......@@ -326,16 +322,41 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
return matchedGoals;
} else {
//handle try and closes
throw new NotImplementedException();
if(aCase instanceof ClosesCase){
ClosesCase closesCase = (ClosesCase) aCase;
for (GoalNode<T> goal : allGoalsBeforeCases) {
//put state onto stack
newState(goal);
boolean matched = (Boolean) closesCase.accept(this);
if (matched) {
matchedGoals.put(goal, new VariableAssignment(null));
}
}
return matchedGoals;
}else{
TryCase tryCase = (TryCase) aCase;
for (GoalNode<T> goal : allGoalsBeforeCases) {
//put state onto stack
newState(goal);
boolean matched = (Boolean) tryCase.accept(this);
if (matched) {
matchedGoals.put(goal, new VariableAssignment(null));
}
}
return matchedGoals;
}
}
}
}*/
/**
* @param casesStatement
* @return
*/
@Override
public Object visit(CasesStatement casesStatement) {
/*
public Object visitOld(CasesStatement casesStatement) {
enterScope(casesStatement);
State<T> beforeCases = peekState();
......@@ -352,13 +373,17 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
Map<GoalNode, Pair<VariableAssignment, Statements>> goalToCaseMapping = matchGoalsToCases(allGoalsBeforeCases, casesStatement);
goalToCaseMapping.forEach((goalNode, variableAssignmentStatementsPair) -> {
State<T> createdState = newState(goalNode);
executeBody(variableAssignmentStatementsPair.getValue(), goalNode, variableAssignmentStatementsPair.getKey());
//stmts.accept(this);
State<T> stateAfterCase = popState(); //remove state from stack
if (stateAfterCase.getGoals() != null) {
resultingGoals.addAll(stateAfterCase.getGoals());
if(variableAssignmentStatementsPair.getValue().isEmpty()){
//TODO this is the try case
}else {
State<T> createdState = newState(goalNode);
executeBody(variableAssignmentStatementsPair.getValue(), goalNode, variableAssignmentStatementsPair.getKey());
//stmts.accept(this);
State<T> stateAfterCase = popState(); //remove state from stack
if (stateAfterCase.getGoals() != null) {
resultingGoals.addAll(stateAfterCase.getGoals());
}
}
});
......@@ -381,7 +406,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
//stateStack.peek().getGoals().removeAll(beforeCases.getGoals());
exitScope(casesStatement);
return null;
}
}*/
/**
* Evaluate a match in a specific goal
......
......@@ -74,13 +74,21 @@ public class State<T> {
}
/**
* TODO correct this method, atm does nothing helpful!
* Deep Copy state
*
* @return
*/
public State<T> copy() {
List<GoalNode<T>> copiedGoals = new ArrayList<>(goals);
GoalNode<T> refToSelGoal = selectedGoalNode;
List<GoalNode<T>> copiedGoals = new ArrayList<>();
GoalNode<T> refToSelGoal = null;
for (GoalNode<T> goal : goals) {
GoalNode<T> deepcopy = goal.deepCopy();
copiedGoals.add(deepcopy);
if (goal.equals(selectedGoalNode)) {
refToSelGoal = deepcopy;
}
}
return new State<T>(copiedGoals, refToSelGoal);
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment