Commit 726585a1 authored by Sarah Grebing's avatar Sarah Grebing
Browse files

minor changes in KeYInterpreter

parent 880c6ea1
Pipeline #13252 failed with stage
in 10 seconds
...@@ -114,12 +114,12 @@ casesStmt ...@@ -114,12 +114,12 @@ casesStmt
; ;
casesList casesList
: (TRY | CASE (expression | closesExpression)) COLON? INDENT? stmtList DEDENT? : (TRY | (CASE (expression | (CLOSES INDENT closesScript=stmtList DEDENT)))) COLON INDENT? body=stmtList DEDENT?
; ;
closesExpression /*closesExpression
: CLOSES INDENT closesScript=stmtList DEDENT : CLOSES INDENT closesScript=stmtList DEDENT
; ;*/
forEachStmt forEachStmt
: FOREACH INDENT stmtList DEDENT : FOREACH INDENT stmtList DEDENT
......
...@@ -321,56 +321,28 @@ public class TransformAst implements ScriptLanguageVisitor<Object> { ...@@ -321,56 +321,28 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
if (ctx.TRY() != null) { if (ctx.TRY() != null) {
tryCase tryCase = new tryCase(); tryCase tryCase = new tryCase();
tryCase.setRuleContext(ctx); tryCase.setRuleContext(ctx);
tryCase.setBody((Statements) ctx.stmtList().accept(this)); tryCase.setBody((Statements) ctx.body.accept(this));
return tryCase; return tryCase;
} }
if (ctx.closesExpression() != null) { if (ctx.closesScript != null) {
ClosesCase closesCase = new ClosesCase(); ClosesCase closesCase = new ClosesCase();
closesCase.setClosedStmt(true); closesCase.setClosedStmt(true);
closesCase.setRuleContext(ctx); closesCase.setRuleContext(ctx);
closesCase.setClosesScript((Statements) ctx.closesExpression().closesScript.accept(this));
closesCase.setBody((Statements) ctx.stmtList().accept(this)); closesCase.setClosesScript((Statements) ctx.closesScript.accept(this));
closesCase.setBody((Statements) ctx.body.accept(this));
return closesCase; return closesCase;
} else { } else {
SimpleCaseStatement caseStatement = new SimpleCaseStatement(); SimpleCaseStatement caseStatement = new SimpleCaseStatement();
caseStatement.setRuleContext(ctx); caseStatement.setRuleContext(ctx);
caseStatement.setGuard((Expression<ParserRuleContext>) ctx.expression().accept(this)); caseStatement.setGuard((Expression<ParserRuleContext>) ctx.expression().accept(this));
caseStatement.setBody((Statements) ctx.stmtList().accept(this)); caseStatement.setBody((Statements) ctx.body.accept(this));
return caseStatement; return caseStatement;
} }
/* CaseStatement caseStatement = new CaseStatement();
caseStatement.setRuleContext(ctx);
caseStatement.setGuard((Expression) ctx.expression().accept(this));
caseStatement.setBody((Statements) ctx.stmtList().accept(this));
return caseStatement;*/
}
@Override
public Object visitClosesExpression(ScriptLanguageParser.ClosesExpressionContext ctx) {
return null;
} }
/*
@Override
public Object visitSimpleCase(ScriptLanguageParser.SimpleCaseContext ctx) {
SimpleCaseStatement caseStatement = new SimpleCaseStatement();
caseStatement.setRuleContext(ctx);
caseStatement.setGuard((Expression) ctx.expression().accept(this));
caseStatement.setBody((Statements) ctx.stmtList().accept(this));
return caseStatement;
}
@Override
public Object visitClosableCase(ScriptLanguageParser.ClosableCaseContext ctx) {
IsClosableCase isClosableCase = new IsClosableCase();
isClosableCase.setRuleContext(ctx);
isClosableCase.setBody((Statements) ctx.stmtList().accept(this));
return isClosableCase;
}
*/
@Override @Override
public Object visitForEachStmt(ScriptLanguageParser.ForEachStmtContext ctx) { public Object visitForEachStmt(ScriptLanguageParser.ForEachStmtContext ctx) {
......
...@@ -76,5 +76,5 @@ public interface Visitor<T> { ...@@ -76,5 +76,5 @@ public interface Visitor<T> {
T visit(SubstituteExpression subst); T visit(SubstituteExpression subst);
T visit(ClosesCase colsesCase); T visit(ClosesCase closesCase);
} }
package edu.kit.iti.formal.psdbg.lint; package edu.kit.iti.formal.psdbg.lint;
import com.github.mustachejava.DefaultMustacheFactory; import com.github.mustachejava.DefaultMustacheFactory;
import com.github.mustachejava.Mustache; import com.github.mustachejava.Mustache;
import com.github.mustachejava.reflect.ReflectionObjectHandler; import com.github.mustachejava.reflect.ReflectionObjectHandler;
......
...@@ -13,7 +13,7 @@ import org.apache.logging.log4j.LogManager; ...@@ -13,7 +13,7 @@ import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger; import org.apache.logging.log4j.Logger;
/** /**
* A facade for capturing everthing we want to do with matchers. * A facade for capturing everything we want to do with matchers.
* *
* @author Alexander Weigl * @author Alexander Weigl
* @author S.Grebing * @author S.Grebing
......
...@@ -11,6 +11,7 @@ import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; ...@@ -11,6 +11,7 @@ import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.data.State; 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.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.interpreter.funchdl.CommandLookup; 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 edu.kit.iti.formal.psdbg.parser.types.SimpleType;
import lombok.Getter; import lombok.Getter;
...@@ -42,6 +43,18 @@ public class KeyInterpreter extends Interpreter<KeyData> { ...@@ -42,6 +43,18 @@ public class KeyInterpreter extends Interpreter<KeyData> {
} }
@Override
public Object visit(ClosesCase closesCase) {
State<KeyData> currentStateToMatch = peekState();
State<KeyData> currentStateToMatchCopy = peekState().copy(); //deepcopy
GoalNode<KeyData> selectedGoalNode = currentStateToMatch.getSelectedGoalNode();
GoalNode<KeyData> selectedGoalCopy = currentStateToMatch.getSelectedGoalNode().deepCopy(); //deepcopy
enterScope(closesCase);
// executeBody(closesCase.getClosesScript(), )
exitScope(closesCase);
return false;
}
@Override @Override
public Object visit(tryCase tryCase) { public Object visit(tryCase tryCase) {
State<KeyData> currentStateToMatch = peekState(); State<KeyData> currentStateToMatch = peekState();
...@@ -71,6 +84,26 @@ public class KeyInterpreter extends Interpreter<KeyData> { ...@@ -71,6 +84,26 @@ public class KeyInterpreter extends Interpreter<KeyData> {
} }
//check if state is closed //check if state is closed
exitScope(tryCase); exitScope(tryCase);
return false; return allClosed;
/* //executeBody and if goal is closed afterwards return true
//else prune proof and return false
State<T> stateBeforeTry = peekState().copy();
State<T> tState = executeBody(tryCase.getBody(), peekState().getSelectedGoalNode(), peekState().getSelectedGoalNode().getAssignments());
boolean isClosed = tState.getGoals().stream().allMatch(tGoalNode -> tGoalNode.isClosed());
if(!isClosed){
exitScope(tryCase);
return false;
}else{
exitScope(tryCase);
return true;
}
*/
} }
} }
...@@ -16,6 +16,7 @@ public class KeyAssignmentHook extends DefaultAssignmentHook<KeyData> { ...@@ -16,6 +16,7 @@ public class KeyAssignmentHook extends DefaultAssignmentHook<KeyData> {
public KeyAssignmentHook() { public KeyAssignmentHook() {
register("MAX_AUTO_STEPS", this::setMaxAutosteps, this::getMaxAutosteps); register("MAX_AUTO_STEPS", this::setMaxAutosteps, this::getMaxAutosteps);
//register()
} }
public Value<BigInteger> getMaxAutosteps(KeyData data) { public Value<BigInteger> getMaxAutosteps(KeyData data) {
......
...@@ -204,15 +204,20 @@ public class ControlFlowVisitor extends DefaultASTVisitor<Void> { ...@@ -204,15 +204,20 @@ public class ControlFlowVisitor extends DefaultASTVisitor<Void> {
graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_BACK); graph.putEdgeValue(currentNode, lastNode, EdgeTypes.STEP_BACK);
List<CaseStatement> cases = casesStatement.getCases(); List<CaseStatement> cases = casesStatement.getCases();
for (CaseStatement aCase : cases) { for (CaseStatement aCase : cases) {
ControlFlowNode caseNode = new ControlFlowNode(aCase);
mappingOfNodes.put(aCase, caseNode); if (aCase.isClosedStmt) {
graph.addNode(caseNode); System.out.println("Handle sondercases");
//System.out.println("\n" + caseNode + "\n"); } else {
graph.putEdgeValue(currentNode, caseNode, EdgeTypes.STEP_OVER); //??is this right? ControlFlowNode caseNode = new ControlFlowNode(aCase);
graph.putEdgeValue(caseNode, currentNode, EdgeTypes.STEP_BACK); mappingOfNodes.put(aCase, caseNode);
lastNode = caseNode; graph.addNode(caseNode);
aCase.getBody().accept(this); //System.out.println("\n" + caseNode + "\n");
graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN); graph.putEdgeValue(currentNode, caseNode, EdgeTypes.STEP_OVER); //??is this right?
graph.putEdgeValue(caseNode, currentNode, EdgeTypes.STEP_BACK);
lastNode = caseNode;
aCase.getBody().accept(this);
graph.putEdgeValue(lastNode, currentNode, EdgeTypes.STEP_RETURN);
}
} }
lastNode = currentNode; lastNode = currentNode;
return null; return null;
......
// Please select one of the following scripts. // Please select one of the following scripts.
// //
script main() {}
script cpauto () {
auto;
}
script cpwob () {
impRight;
impRight;
notLeft;
notRight;
replace_known_left occ='2';
concrete_impl_1;
close;
}
script cpwb () {
impRight;
impLeft;
cases{
case match `==> p`:{
auto;
}
default:{
auto;
}
}
}
script cpClosable(){ script cpClosable(){
impRight; impRight;
impRight; impRight;
cases{ cases{
case try:{ try:
notLeft; notLeft;
notRight; notRight;
replace_known_left occ='2'; replace_known_left occ='2';
concrete_impl_1; concrete_impl_1;
close; close;
}
default:{ default:
auto; auto;
}
} }
} }
\ No newline at end of file
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