Commit 90894510 authored by Alexander Weigl's avatar Alexander Weigl

Renaming/refactoring trying to make things easier

parent 31c8f187
Pipeline #15060 failed with stage
in 1 minute and 47 seconds
......@@ -116,12 +116,12 @@ casesStmt
casesList
: (TRY |
(CASE (expression
| (CLOSES INDENT closesScript=stmtList DEDENT) ) ) )
| (CLOSES INDENT closesGuard=stmtList DEDENT) ) ) )
COLON INDENT? body=stmtList DEDENT?
;
/*closesExpression
: CLOSES INDENT closesScript=stmtList DEDENT
: CLOSES INDENT closesGuard=stmtList DEDENT
;*/
forEachStmt
......
......@@ -29,7 +29,7 @@ public class ShortCommandPrinter extends DefaultASTVisitor<String> {
}
@Override
public String visit(SimpleCaseStatement caseStatement) {
public String visit(GuardedCaseStatement caseStatement) {
return "case " + Facade.prettyPrint(caseStatement.getGuard());
}
......@@ -40,7 +40,7 @@ public class ShortCommandPrinter extends DefaultASTVisitor<String> {
@Override
public String visit(ClosesCase closesCase) {
return "closes with {" + Facade.prettyPrint(closesCase.getClosesScript()) + "}";
return "closes with {" + Facade.prettyPrint(closesCase.getClosesGuard()) + "}";
}
@Override
......
......@@ -118,15 +118,15 @@ public class ASTChanger extends DefaultASTVisitor<ASTNode> {
}
@Override
public SimpleCaseStatement visit(SimpleCaseStatement simpleCaseStatement) {
simpleCaseStatement.getGuard().accept(this);
simpleCaseStatement.getBody().accept(this);
return simpleCaseStatement;
public GuardedCaseStatement visit(GuardedCaseStatement guardedCaseStatement) {
guardedCaseStatement.getGuard().accept(this);
guardedCaseStatement.getBody().accept(this);
return guardedCaseStatement;
}
@Override
public ASTNode visit(ClosesCase closesCase) {
closesCase.getClosesScript().accept(this);
closesCase.getClosesGuard().accept(this);
closesCase.getBody().accept(this);
return closesCase;
}
......
......@@ -167,9 +167,9 @@ public interface ASTTraversal<T> extends Visitor<T> {
}
@Override
default T visit(SimpleCaseStatement simpleCaseStatement) {
simpleCaseStatement.getGuard().accept(this);
simpleCaseStatement.getBody().accept(this);
default T visit(GuardedCaseStatement guardedCaseStatement) {
guardedCaseStatement.getGuard().accept(this);
guardedCaseStatement.getBody().accept(this);
return null;
}
......@@ -184,7 +184,7 @@ public interface ASTTraversal<T> extends Visitor<T> {
@Override
default T visit(ClosesCase closesCase) {
closesCase.getClosesScript().accept(this);
closesCase.getClosesGuard().accept(this);
closesCase.getBody().accept(this);
return null;
}
......
......@@ -143,8 +143,8 @@ public class DefaultASTVisitor<T> implements Visitor<T> {
}
@Override
public T visit(SimpleCaseStatement simpleCaseStatement) {
return defaultVisit(simpleCaseStatement);
public T visit(GuardedCaseStatement guardedCaseStatement) {
return defaultVisit(guardedCaseStatement);
}
@Override
......
......@@ -178,7 +178,7 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
}
@Override
public Void visit(SimpleCaseStatement caseStatement) {
public Void visit(GuardedCaseStatement caseStatement) {
s.append("case ");
caseStatement.getGuard().accept(this);
s.append(" {");
......
......@@ -352,14 +352,13 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
cs = new TryCase();
} else if (ctx.closesScript != null) {
cs = new ClosesCase();
cs.setClosedStmt(true);
Statements closes = (Statements) ctx.closesScript.accept(this);
((ClosesCase) cs).setClosesScript(closes);
((ClosesCase) cs).setClosesGuard(closes);
closes.setParent(cs);
} else {
cs = new SimpleCaseStatement();
cs = new GuardedCaseStatement();
Expression<ParserRuleContext> guard = (Expression<ParserRuleContext>) ctx.expression().accept(this);
((SimpleCaseStatement) cs).setGuard(guard);
((GuardedCaseStatement) cs).setGuard(guard);
}
cs.setBody(accept);
......
......@@ -72,7 +72,7 @@ public interface Visitor<T> {
T visit(TryCase TryCase);
T visit(SimpleCaseStatement simpleCaseStatement);
T visit(GuardedCaseStatement guardedCaseStatement);
T visit(CaseStatement caseStatement);
......
......@@ -38,8 +38,7 @@ import lombok.Setter;
@Setter
@RequiredArgsConstructor
@AllArgsConstructor
public class CaseStatement extends Statement<ScriptLanguageParser.CasesListContext> {
public boolean isClosedStmt;
public abstract class CaseStatement extends Statement<ScriptLanguageParser.CasesListContext> {
protected Statements body;
/**
......@@ -52,9 +51,6 @@ public class CaseStatement extends Statement<ScriptLanguageParser.CasesListConte
/**
* {@inheritDoc}
*/
@Override public CaseStatement copy() {
CaseStatement cs = new CaseStatement(isClosedStmt, body.copy());
cs.setRuleContext(this.ruleContext);
return cs;
}
@Override public abstract CaseStatement copy();
}
......@@ -10,23 +10,20 @@ import lombok.NoArgsConstructor;
@Data
@NoArgsConstructor
public class ClosesCase extends CaseStatement {
private boolean isClosedStmt = true;
/**
* Script that should be executed and shown whether case can be closed
*/
private Statements closesScript;
private Statements closesGuard;
/**
* A close subscript() {bodyscript} expression
*
* @param closesScript the script that is exectued in order to determine whether goal would clos. This proof is pruned afterwards
* @param closesGuard the script that is exectued in order to determine whether goal would clos. This proof is pruned afterwards
* @param body the actual script that is then executed when closesscript was successful and pruned
*/
public ClosesCase(Statements closesScript, Statements body) {
public ClosesCase(Statements closesGuard, Statements body) {
this.body = body;
this.closesScript = closesScript;
this.closesGuard = closesGuard;
}
/**
......@@ -42,7 +39,7 @@ public class ClosesCase extends CaseStatement {
*/
@Override
public ClosesCase copy() {
ClosesCase cs = new ClosesCase(closesScript.copy(), body.copy());
ClosesCase cs = new ClosesCase(closesGuard.copy(), body.copy());
cs.setRuleContext(this.ruleContext);
return cs;
}
......
......@@ -11,11 +11,10 @@ import lombok.NoArgsConstructor;
@Data
@NoArgsConstructor
@AllArgsConstructor
public class SimpleCaseStatement extends CaseStatement {
public class GuardedCaseStatement extends CaseStatement {
private Expression guard;
private boolean isClosedStmt = false;
public SimpleCaseStatement(Expression guard, Statements body) {
public GuardedCaseStatement(Expression guard, Statements body) {
this.guard = guard;
this.body = body;
}
......@@ -32,8 +31,8 @@ public class SimpleCaseStatement extends CaseStatement {
* {@inheritDoc}
*/
@Override
public SimpleCaseStatement copy() {
SimpleCaseStatement scs = new SimpleCaseStatement(guard.copy(), body.copy());
public GuardedCaseStatement copy() {
GuardedCaseStatement scs = new GuardedCaseStatement(guard.copy(), body.copy());
scs.setRuleContext(this.ruleContext);
return scs;
}
......
......@@ -10,8 +10,6 @@ import lombok.NoArgsConstructor;
@Data
@NoArgsConstructor
public class TryCase extends CaseStatement {
private boolean isClosedStmt = true;
public TryCase(Statements body) {
this.body = body;
}
......
......@@ -230,7 +230,18 @@ public class KeYProofFacade {
}
public enum ProofState {
EMPTY, VIRGIN, DIRTY;
/**
* There is no KeY Proof actually loaded.
*/
EMPTY,
/**
* The loaded KeY Proof is untouched iff there is only one node --- the root.
*/
VIRGIN,
/**
* The KeY Proof was ravished by Taclets and other stuff.
*/
DIRTY;
}
//endregion
}
......
......@@ -4,7 +4,6 @@ import com.google.common.collect.BiMap;
import com.google.common.collect.ImmutableBiMap;
import de.uka.ilkd.key.api.ScriptApi;
import de.uka.ilkd.key.api.VariableAssignments;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
......@@ -18,7 +17,6 @@ import edu.kit.iti.formal.psdbg.parser.ast.Statements;
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;
import java.util.List;
......@@ -38,8 +36,6 @@ public class KeyInterpreter extends Interpreter<KeyData> {
.put(SimpleType.INT_ARRAY, VariableAssignments.VarType.INT_ARRAY)
.put(SimpleType.SEQ, VariableAssignments.VarType.SEQ)
.build();
@Getter
private ScriptApi scriptApi;
public KeyInterpreter(CommandLookup lookup) {
super(lookup);
......@@ -48,15 +44,18 @@ public class KeyInterpreter extends Interpreter<KeyData> {
@Override
public Object visit(ClosesCase closesCase) {
/*
State<KeyData> currentStateToMatch = peekState();
State<KeyData> currentStateToMatchCopy = currentStateToMatch.copy(); //deepcopy
GoalNode<KeyData> selectedGoalNode = currentStateToMatch.getSelectedGoalNode();
GoalNode<KeyData> selectedGoalCopy = currentStateToMatch.getSelectedGoalNode().deepCopy(); //deepcopy
*/
enterScope(closesCase);
//execute closesscript
executeBody(closesCase.getClosesScript(), selectedGoalNode, new VariableAssignment(selectedGoalNode.getAssignments()));
boolean closed = suspicionExecution(closesCase.getClosesGuard(), true);
//executeBody(closesCase.getClosesGuard(), selectedGoalNode, new VariableAssignment(selectedGoalNode.getAssignments()));
//check whether script closed proof
State<KeyData> stateafterIsClosable = peekState();
/*State<KeyData> stateafterIsClosable = peekState();
List<GoalNode<KeyData>> goals = stateafterIsClosable.getGoals();
boolean allClosed = true;
for (GoalNode<KeyData> goal : goals) {
......@@ -75,39 +74,21 @@ public class KeyInterpreter extends Interpreter<KeyData> {
pushState(currentStateToMatchCopy);
exitScope(closesCase);
return allClosed;
*/
exitScope(closesCase);
return closed;
}
@Override
public Object visit(TryCase tryCase) {
//historylistener for recording try
enterScope(tryCase);
boolean b = suspicionExecution(tryCase.getBody());
boolean b = suspicionExecution(tryCase.getBody(), false);
exitScope(tryCase);
return b;
/* //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;
}
*/
}
private boolean suspicionExecution(Statements statements) {
private boolean suspicionExecution(Statements statements, boolean alwaysPrune) {
logger.debug(String.format("Beginning of suspicion execution of %s", statements));
GoalNode<KeyData> goalNode = getSelectedNode();
pushState(new State<>(goalNode.deepCopy())); // copy for later prove
......@@ -124,7 +105,7 @@ public class KeyInterpreter extends Interpreter<KeyData> {
.allMatch(g -> g.getData().getNode().isClosed());
logger.debug("Ended Side Computation");
if (!allGoalsClosed) {
if (!allGoalsClosed || alwaysPrune) {
logger.debug("Try was not successful, rolling back proof");
//Throw away the new state, and truncate the prove!
Proof currentKeYproof = goalNode.getData().getProof();
......
......@@ -198,7 +198,7 @@ public class Debugger {
}
@Override
public Void visit(SimpleCaseStatement caseStatement) {
public Void visit(GuardedCaseStatement caseStatement) {
suffix(caseStatement);
System.out.println("case " + Facade.prettyPrint(caseStatement.getGuard()));
return super.visit(caseStatement);
......
......@@ -32,22 +32,25 @@ import java.util.stream.Stream;
public class Interpreter<T> extends DefaultASTVisitor<Object>
implements ScopeObservable {
private static final int MAX_ITERATIONS = 5;
protected static Logger logger = LogManager.getLogger(Interpreter.class);
@Getter
public final AtomicBoolean hardStop = new AtomicBoolean(false);
private Stack<State<T>> stateStack = new Stack<>();
@Getter
protected List<Visitor> entryListeners = new ArrayList<>(),
exitListeners = new ArrayList<>();
private Stack<State<T>> stateStack = new Stack<>();
@Getter
@Setter
private MatcherApi<T> matcherApi;
@Getter
private CommandLookup functionLookup;
@Getter
@Setter
private boolean scrictSelectedGoalMode = false;
......@@ -55,6 +58,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
@Getter
@Setter
private VariableAssignmentHook<T> variableAssignmentHook = null;
@Getter
@Setter
private boolean suppressListeners = false;
......@@ -67,12 +71,12 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
public <T extends ParserRuleContext> void enterScope(ASTNode<T> node) {
if (hardStop.get())
throw new InterpreterRuntimeException("hard stop");
if(!suppressListeners) callListeners(getEntryListeners(), node);
if (!suppressListeners) callListeners(getEntryListeners(), node);
}
@Override
public <T extends ParserRuleContext> void exitScope(ASTNode<T> node) {
if(!suppressListeners) callListeners(getExitListeners(), node);
if (!suppressListeners) callListeners(getExitListeners(), node);
}
/**
......@@ -262,20 +266,22 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
}
@Override
public Object visit(SimpleCaseStatement simpleCaseStatement) {
Expression matchExpression = simpleCaseStatement.getGuard();
public Object visit(GuardedCaseStatement guardedCaseStatement) {
Expression matchExpression = guardedCaseStatement.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;
try {
enterScope(guardedCaseStatement);
if (va != null) {
executeBody(guardedCaseStatement.getBody(), selectedGoal, va);
return true;
} else {
return false;
}
} finally {
exitScope(guardedCaseStatement);
}
}
......@@ -319,13 +325,12 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
/**
* Match a set of goal nodes against a matchpattern of a case and return the matched goals together with instantiated variables
*
*/
/* private Map<GoalNode<T>, VariableAssignment> matchGoal(Set<GoalNode<T>> allGoalsBeforeCases, CaseStatement aCase) {
HashMap<GoalNode<T>, VariableAssignment> matchedGoals = new HashMap<>();
if (!aCase.isClosedStmt()) {
SimpleCaseStatement caseStmt = (SimpleCaseStatement) aCase;
GuardedCaseStatement caseStmt = (GuardedCaseStatement) aCase;
Expression matchExpression = caseStmt.getGuard();
for (GoalNode<T> goal : allGoalsBeforeCases) {
VariableAssignment va = evaluateMatchInGoal(matchExpression, goal);
......
......@@ -137,8 +137,8 @@ public class BlockListener<T> implements InterpreterObserver<T> {
}
@Override
public Void visit(SimpleCaseStatement simpleCaseStatement) {
return checkForHalt(simpleCaseStatement);
public Void visit(GuardedCaseStatement guardedCaseStatement) {
return checkForHalt(guardedCaseStatement);
}
@Override
......
package edu.kit.iti.formal.psdbg.interpreter.dbg;
public abstract class DebuggerCommand<T> {
public abstract void execute(DebuggerFramework<T> dbg) throws DebuggerException;
public void error(String msg) throws DebuggerException {
throw new DebuggerException(msg, true);
}
public void info(String msg) throws DebuggerException {
throw new DebuggerException(msg, false);
}
}
......@@ -25,6 +25,39 @@ import java.util.function.Consumer;
* <li>{@link StateWrapper}: signals the PTreeNodes</li>
* <li></li>
* </ol>
*<code><pre>
+------------------------------------------------------------------------------------------+
| |
| DebuggerFramework<T> |
| +------------+
| | execute(DebuggerCommand)
| | Commands: StepOver, StepInto,
| +------------------+ +-----------------+ +---------------------------+ | StepReturn, StepBack
| | | | | | | |
| | Interpreter<T> +-------> StateWrapper<T> +-------> PTreeManager<T> +--------->
| | | | | | | |
| +---------+--------+ +-----------------+ +---------------------------+ | statePointerChanged(PTreeNode<T>)
| | |
| | Listener emitNode |
| | |
| | |
| +---------v------------+ |
| | <--------------------------------------------------------------------+ releaseForever()
| | BlockerListener | | release()
| | | | releaseUntil(BlockerPredicate)
| +----------------------+ | getBreakpoints()
| |
| |
| +----------------+ +---------------------+ |
| | | | | |
| | Breakpoint | | BlockerPredicate | |
| | | | | |
| +----------------+ +---------------------+ |
| |
+------------------------------------------------------------------------------------------+
</pre></code>
*
*
*
* @author Alexander Weigl
* @version 1 (27.10.17)
......
......@@ -6,7 +6,8 @@ import javafx.beans.property.ObjectProperty;
import javafx.beans.property.SimpleListProperty;
import javafx.collections.ObservableList;
import javafx.scene.control.*;
import javafx.scene.web.WebView;
import javafx.scene.text.Text;
import javafx.scene.text.TextFlow;
import javafx.stage.Modality;
import lombok.Getter;
......@@ -26,8 +27,11 @@ import java.util.List;
public class ContractChooser extends Dialog<Contract> {
@Getter
private final MultipleSelectionModel<Contract> selectionModel;
private final ObjectProperty<ObservableList<Contract>> items;
private final ListView<Contract> listOfContractsView = new ListView<>();
private final Services services;
public ContractChooser(Services services,
......@@ -87,26 +91,49 @@ public class ContractChooser extends Dialog<Contract> {
}
private class ContractListCell extends ListCell<Contract> {
private final WebView webView = new WebView();
private final TextFlow text = new TextFlow();
ContractListCell(ListView<Contract> contractListView) {
itemProperty().addListener((observable, oldValue, newValue) -> render());
selectedProperty().addListener((observable, oldValue, newValue) -> render());
setGraphic(webView);
text.maxWidthProperty().bind(contractListView.widthProperty());
setGraphic(text);
}
private void render() {
if (getItem() != null) {
String content = beautifyContractHTML(getItem().getHTMLText(services), getItem().getTarget().toString());
webView.getEngine().loadContent(content);
//webView.getEngine().loadContent(getItem().getHTMLText(services));
//int val = (int) webView.getEngine().executeScript("document.height");
webView.setPrefHeight(150);
webView.setDisable(true);
text.getChildren().clear();
String content = getItem().getPlainText(services);
Text contract = new Text("Contract for method: ");
Text name = new Text(getItem().getTarget().toString());
Text tcontent = new Text(content);
contract.setStyle("-fx-font-weight: bold; -fx-font-size: 120%");
name.setStyle("-fx-font-family: monospace; -fx-font-size: 120%");
tcontent.setStyle("-fx-font-family: monospace");
text.getChildren().add(contract);
text.getChildren().add(name);
text.getChildren().add(new Text("\n"));
//text.getChildren().add(tcontent);
for (String line : content.split("\n")) {
if (line.contains(":")) {
String[] a = line.split(":", 2);
Text s = new Text(String.format("%-15s", a[0] + ":"));
Text t = new Text(a[1] + "\n");
s.setStyle("-fx-font-family: monospace;-fx-font-weight:bold;-fx-min-width: 10em");
t.setStyle("-fx-font-family: monospace");
text.getChildren().addAll(s, t);
} else {
Text t = new Text(line + "\n");
t.setStyle("-fx-font-family: monospace");
text.getChildren().addAll(t);
}
}
if (selectedProperty().get()) {
webView.setStyle("-fx-background-color: lightblue");
// text.setStyle("-fx-background-color: lightblue");
}
}
}
......@@ -114,5 +141,8 @@ public class ContractChooser extends Dialog<Contract> {
private String beautifyContractHTML(String html, String name) {
return "Contract for <b>" + name + "</b><br>" + html;
}
}
}
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