Skip to content

GitLab

Commit e7c3af0d authored by LULUDBR\Lulu's avatar LULUDBR\Lulu
Browse files
Options

Merge remote-tracking branch 'origin/master'

parents b36a3c1f 93bd3ef3
Hide whitespace changes
Inline Side-by-side
Showing with 1054 additions and 152 deletions
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java
View file @ e7c3af0d
......@@ -114,6 +114,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
s.setSignature(sig);
}
s.setBody((Statements) ctx.body.accept(this));
s.getBody().setParent(s);
return s;
}
......
matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacadeTest.java
View file @ e7c3af0d
......@@ -98,13 +98,9 @@ public class MatcherFacadeTest {
shouldMatch("1*j", "1 + ?Y", "[]");
shouldMatch("1*j", "1 * ?Y", "[{?Y=j}]");
//does not match
shouldMatch("1*j", "?Y * 1", "[{?Y=j}]");
//shouldMatch("f(a) ==> f(a), f(b)" , "==> f(?X)", [{?X=a}]);
//shouldMatch("f(a) ==> f(a), f(b)" , "f(a) ==> f(?X)", [{?X=a}]);
//shouldNotMatch("f(a) ==> f(a), f(b)" , "f(?X) ==> f(?X), f(a)");
}
@Test
......
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYMatcher.java
View file @ e7c3af0d
package edu.kit.iti.formal.psdbg.interpreter;
import de.uka.ilkd.key.api.ProofApi;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.Name;
import de.uka.ilkd.key.logic.Term;
......@@ -163,10 +162,11 @@ public class KeYMatcher implements MatcherApi<KeyData> {
private Value<String> toValueTerm(KeyData currentState, Term matched) {
String reprTerm = LogicPrinter.quickPrintTerm(matched, currentState.getEnv().getServices());
//Hack: to avoid newlines
String reprTermReformatted = reprTerm.trim();
return new Value<>(
new TermType(new SortType(matched.sort())),
reprTerm
reprTermReformatted
);
}
......
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptCommandBuilder.java
View file @ e7c3af0d
......@@ -4,7 +4,6 @@ import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
import de.uka.ilkd.key.macros.scripts.EngineState;
import de.uka.ilkd.key.macros.scripts.ProofScriptCommand;
import de.uka.ilkd.key.macros.scripts.meta.ProofScriptArgument;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Node;
import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
......@@ -15,10 +14,14 @@ import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
import org.apache.commons.io.IOUtils;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.key_project.util.collection.ImmutableList;
import java.io.IOException;
import java.net.URISyntaxException;
import java.net.URL;
import java.util.Collection;
import java.util.HashMap;
import java.util.Iterator;
......@@ -61,7 +64,11 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
GoalNode<KeyData> expandedNode = state.getSelectedGoalNode();
KeyData kd = expandedNode.getData();
Map<String, String> map = new HashMap<>();
params.asMap().forEach((k, v) -> map.put(k.getIdentifier(), v.getData().toString()));
params.asMap().forEach((k, v) -> {
System.out.println("v.getData().toString() = " + v.getData().toString());
map.put(k.getIdentifier(), v.getData().toString());
}
);
try {
EngineState estate = new EngineState(kd.getProof());
estate.setGoal(kd.getNode());
......@@ -100,6 +107,17 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
@Override
public String getHelp(CallStatement call) {
ProofScriptCommand c = commands.get(call.getCommand());
URL res = getClass().getResource("/commands/" + call.getCommand() + ".html");
try {
return IOUtils.toString(res.toURI(), "utf-8");
} catch (NullPointerException | IOException | URISyntaxException e) {
return "No Help found for " + call.getCommand();
}
/*
StringBuilder html = new StringBuilder();
......@@ -150,5 +168,6 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
html.append("</body></html>");
return html.toString();
*/
}
}
rt-key/src/main/resources/edu/kit/iti/formal/psdbg/commands/auto.html 0 → 100644
View file @ e7c3af0d
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<title>Title</title>
</head>
<body>
</body>
</html>
\ No newline at end of file
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java
View file @ e7c3af0d
......@@ -161,10 +161,10 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
}
private Value evaluate(GoalNode<T> g, Expression expr) {
enterScope(expr);
//enterScope(expr);
Evaluator<T> evaluator = new Evaluator<>(g.getAssignments(), g);
evaluator.setMatcher(matcherApi);
exitScope(expr);
//exitScope(expr);
return evaluator.eval(expr);
}
......
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/DebuggerFramework.java
View file @ e7c3af0d
......@@ -134,7 +134,7 @@ public class DebuggerFramework<T> {
private void run() {
try {
interpreter.interpret(mainScript);
//dummyproofnode
ptreeManager.fireStatePointerChanged();
succeedListener.accept(this);
} catch (Exception e) {
error = e;
......
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/ProofTreeManager.java
View file @ e7c3af0d
......@@ -76,7 +76,7 @@ public class ProofTreeManager<T> {
int ctxLength = node.getContext().length;
// We got a step deeper in the ASTNode stack.
// So we a caller
// So we have a caller
if (getContextDepth() < ctxLength) {
pushContext();
intoCurrentContext(node);
......
rt-key/src/main/java/edu/kit/iti/formal/psdbg/StepIntoCommand.java → rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepIntoCommand.java
View file @ e7c3af0d
package edu.kit.iti.formal.psdbg;
import edu.kit.iti.formal.psdbg.interpreter.dbg.*;
package edu.kit.iti.formal.psdbg.interpreter.dbg;
public class StepIntoCommand<T> extends DebuggerCommand<T> {
@Override
public void execute(DebuggerFramework<T> dbg) {
PTreeNode<T> statePointer = dbg.getStatePointer();
assert statePointer != null;
if (statePointer.isAtomic()) {
if (statePointer.isAtomic()) { // atomic same as step over
new StepOverCommand<T>().execute(dbg);
} else {
dbg.releaseUntil(new Blocker.CounterBlocker(1));
if (statePointer.getStepInto() != null) { // if there is already an step into take it!
dbg.setStatePointer(statePointer.getStepInto());
} else {
if (!statePointer.isLastNode()) { // execute non last commands, one step wide!
dbg.releaseUntil(new Blocker.CounterBlocker(1));
}
}
}
}
}
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/StepIntoReverseCommand.java
View file @ e7c3af0d
package edu.kit.iti.formal.psdbg.interpreter.dbg;
import lombok.val;
public class StepIntoReverseCommand<T> extends DebuggerCommand<T> {
@Override
public void execute(DebuggerFramework<T> dbg) throws DebuggerException {
val statePointer = dbg.getCurrentStatePointer();
PTreeNode<T> stepBack = statePointer.getStepInvInto() != null ?
statePointer.getStepInvInto() :
statePointer.getStepInvOver();
PTreeNode<T> statePointer = dbg.getStatePointer();
assert statePointer != null;
if (stepBack == null) {
info("There is no previous state to the current one.");
if (statePointer.getStepInvInto() != null) {
dbg.setStatePointer(statePointer.getStepInvInto());
} else {
if (statePointer.getStepInvOver() != null) {
PTreeNode<T> statementBefore = statePointer.getStepInvOver();
dbg.setStatePointer(statementBefore);
} else{
dbg.setStatePointer(statePointer);
}
}
dbg.setStatePointer(stepBack);
}
}
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ContractChooser.java
View file @ e7c3af0d
......@@ -114,7 +114,7 @@ public class ContractChooser extends Dialog<Contract> {
text.getChildren().add(contract);
text.getChildren().add(name);
text.getChildren().add(new Text("\n"));
//text.getChildren().add(tcontent);
//text.getChildren().addCell(tcontent);
for (String line : content.split("\n")) {
if (line.contains(":")) {
......
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
View file @ e7c3af0d
......@@ -15,11 +15,12 @@ import de.uka.ilkd.key.proof.init.ProofInputException;
import de.uka.ilkd.key.proof.io.ProblemLoaderException;
import de.uka.ilkd.key.speclang.Contract;
import edu.kit.iti.formal.psdbg.ShortCommandPrinter;
import edu.kit.iti.formal.psdbg.StepIntoCommand;
import edu.kit.iti.formal.psdbg.examples.Examples;
import edu.kit.iti.formal.psdbg.fmt.DefaultFormatter;
import edu.kit.iti.formal.psdbg.gui.ProofScriptDebugger;
import edu.kit.iti.formal.psdbg.gui.controls.*;
import edu.kit.iti.formal.psdbg.gui.graph.Graph;
import edu.kit.iti.formal.psdbg.gui.graph.GraphView;
import edu.kit.iti.formal.psdbg.gui.model.DebuggerMainModel;
import edu.kit.iti.formal.psdbg.gui.model.InspectionModel;
import edu.kit.iti.formal.psdbg.gui.model.InterpreterThreadState;
......@@ -28,6 +29,7 @@ import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
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.data.State;
import edu.kit.iti.formal.psdbg.interpreter.dbg.*;
import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
import javafx.application.Platform;
......@@ -88,76 +90,53 @@ public class DebuggerMain implements Initializable {
@Getter
private final DebuggerMainModel model = new DebuggerMainModel();
private final GraphView graphView = new GraphView();
private final Graph.PTreeGraph graph = graphView.getGraph();
private final DockNode graphViewNode = new DockNode(graphView, "Debug graph");
private InspectionViewsController inspectionViewsController;
private ScriptController scriptController;
@FXML
private DebuggerStatusBar statusBar;
@FXML
private DockPane dockStation;
@FXML
private ToggleButton togBtnCommandHelp;
@FXML
private ToggleButton togBtnProofTree;
@FXML
private ToggleButton togBtnActiveInspector;
@FXML
private ToggleButton togBtnWelcome;
@FXML
private ToggleButton togBtnCodeDock;
@FXML
private CheckMenuItem miCommandHelp;
@FXML
private CheckMenuItem miCodeDock;
@FXML
private CheckMenuItem miWelcomeDock;
@FXML
private CheckMenuItem miActiveInspector;
@FXML
private CheckMenuItem miProofTree;
@FXML
private ToggleButton btnInteractiveMode;
private JavaArea javaArea = new JavaArea();
private DockNode javaAreaDock = new DockNode(javaArea, "Java Source",
new MaterialDesignIconView(MaterialDesignIcon.CODEPEN)
);
//-----------------------------------------------------------------------------------------------------------------
private ProofTree proofTree = new ProofTree();
private DockNode proofTreeDock = new DockNode(proofTree, "Proof Tree");
private WelcomePane welcomePane = new WelcomePane(this);
private DockNode welcomePaneDock = new DockNode(welcomePane, "Welcome", new MaterialDesignIconView(MaterialDesignIcon.ACCOUNT));
private DockNode activeInspectorDock;
private CommandHelp commandHelp = new CommandHelp();
private DockNode commandHelpDock = new DockNode(commandHelp, "DebuggerCommand Help");
private InteractiveModeController interactiveModeController;
@FXML
private Menu examplesMenu;
private Timer interpreterThreadTimer;
@Subscribe
......@@ -303,6 +282,8 @@ public class DebuggerMain implements Initializable {
* @see {@link #handleStatePointer(PTreeNode)}
*/
private void handleStatePointerUI(PTreeNode<KeyData> node) {
graph.addPartiallyAndMark(node);
if (node != null) {
getInspectionViewsController().getActiveInspectionViewTab().activate(node, node.getStateBeforeStmt());
scriptController.getDebugPositionHighlighter().highlight(node.getStatement());
......@@ -326,7 +307,7 @@ public class DebuggerMain implements Initializable {
showCodeDock(null);
});
//add listener for linehighlighting when changing selection in inspectionview
//addCell listener for linehighlighting when changing selection in inspectionview
getInspectionViewsController().getActiveInspectionViewTab().getModel().highlightedJavaLinesProperty().
addListener((observable, oldValue, newValue) -> {
if (newValue != null) {
......@@ -346,6 +327,19 @@ public class DebuggerMain implements Initializable {
}
//region Actions: Menu
/*@FXML
public void saveAsScript() throws IOException {
File f = openFileChooserSaveDialog("Save script", "Save Script files", "kps");
if (f != null) {
/* if(!f.exists()){
f.createNewFile();
}
saveScript(f);
}
}*/
public KeYProofFacade getFacade() {
return FACADE;
}
......@@ -365,19 +359,6 @@ public class DebuggerMain implements Initializable {
});
}
//region Actions: Menu
/*@FXML
public void saveAsScript() throws IOException {
File f = openFileChooserSaveDialog("Save script", "Save Script files", "kps");
if (f != null) {
/* if(!f.exists()){
f.createNewFile();
}
saveScript(f);
}
}*/
public void showCodeDock(ActionEvent actionEvent) {
if (!javaAreaDock.isDocked()) {
javaAreaDock.dock(dockStation, DockPos.RIGHT);
......@@ -474,7 +455,6 @@ public class DebuggerMain implements Initializable {
}
}
/**
* Execute the script that with using the interpreter that is build using the interpreterbuilder
*
......@@ -527,20 +507,54 @@ public class DebuggerMain implements Initializable {
btnInteractiveMode.setDisable(false);
assert model.getDebuggerFramework() != null;
btnInteractiveMode.setSelected(true);
/*PTreeNode<KeyData> statePointer = model.getDebuggerFramework().getStatePointer();
PTreeNode<KeyData> statePointer = model.getDebuggerFramework().getStatePointer();
assert statePointer!=null;
State<KeyData> lastState = statePointer.getStateAfterStmt();
getInspectionViewsController().getActiveInspectionViewTab().activate(statePointer, lastState);
*/
});
}
@FXML
public void debugGraph(ActionEvent event) {
if (!graphViewNode.isDocked() && !graphViewNode.isFloating()) {
graphViewNode.dock(dockStation, DockPos.CENTER);
}
graph.clear(true);
for (PTreeNode<KeyData> n : model.getDebuggerFramework().getStates()) {
graph.addCell(n);
}
for (PTreeNode<KeyData> n : model.getDebuggerFramework().getStates()) {
if (n.getStepOver() != null) {
graph.addEdge(n, n.getStepOver(), "over");
}
if (n.getStepInto() != null) {
graph.addEdge(n, n.getStepInto(), "into");
}
if (n.getStepInvOver() != null) {
graph.addEdge(n, n.getStepInvOver(), "revo");
}
if (n.getStepInvInto() != null) {
graph.addEdge(n, n.getStepInvInto(), "otni");
}
if (n.getStepReturn() != null) {
graph.addEdge(n, n.getStepReturn(), "rtrn");
}
}
}
@FXML
public void debugPrintDot(@Nullable ActionEvent ae) {
if (model.getDebuggerFramework() == null) {
statusBar.publishErrorMessage("can print debug info, no debugger started!");
return;
}
debugGraph(ae);
try (PrintWriter out = new PrintWriter(new FileWriter("debug.dot"))) {
out.println("digraph G {");
for (PTreeNode<KeyData> n : model.getDebuggerFramework().getStates()) {
......@@ -729,6 +743,7 @@ public class DebuggerMain implements Initializable {
/**
* Reload a problem from the beginning
*
* @param event
*/
@FXML
......@@ -765,6 +780,7 @@ public class DebuggerMain implements Initializable {
}
@FXML
public void closeProgram() {
System.exit(0);
......@@ -893,7 +909,7 @@ public class DebuggerMain implements Initializable {
* @param actionEvent
*/
public void stepInto(ActionEvent actionEvent) {
LOGGER.debug("DebuggerMain.stepOver");
LOGGER.debug("DebuggerMain.stepInto");
try {
if (model.getDebuggerFramework().getStatePointer().isAtomic()) {
model.getDebuggerFramework().getStatePointerListener()
......@@ -914,8 +930,10 @@ public class DebuggerMain implements Initializable {
/**
* Perform a step back
* Does stepinto back
*
* @param actionEvent
*/
@Deprecated
public void stepBack(ActionEvent actionEvent) {
LOGGER.debug("DebuggerMain.stepBack");
try {
......@@ -938,13 +956,26 @@ public class DebuggerMain implements Initializable {
public void stepIntoReverse(ActionEvent actionEvent) {
LOGGER.debug("DebuggerMain.stepOverReverse");
LOGGER.debug("DebuggerMain.stepIntoReverser");
try {
if (model.getDebuggerFramework().getStatePointer().isAtomic()) {
model.getDebuggerFramework().getStatePointerListener()
.add(new StepIntoReverseHandler(model.getStatePointer()));
}
model.getDebuggerFramework().execute(new StepIntoReverseCommand<>());
} catch (DebuggerException e) {
Utils.showExceptionDialog("", "", "", e);
LOGGER.error(e);
}
/* LOGGER.debug("DebuggerMain.stepOverReverse");
try {
model.getDebuggerFramework().execute(new StepIntoReverseCommand<>());
} catch (DebuggerException e) {
Utils.showExceptionDialog("", "", "", e);
LOGGER.error(e);
}*/
}
public void stopDebugMode(ActionEvent actionEvent) {
......@@ -1048,7 +1079,7 @@ public class DebuggerMain implements Initializable {
webEngine.load(url);
DockNode dn = new DockNode(browser);
dn.setTitle("ScriptLanguage Description");
//this.dockStation.getChildren().add(dn);
//this.dockStation.getChildren().addCell(dn);
dn.dock(dockStation, DockPos.LEFT);
}
......@@ -1182,6 +1213,64 @@ public class DebuggerMain implements Initializable {
node.dock(dockStation, DockPos.CENTER, scriptController.getOpenScripts().get(getScriptController().getMainScript().getScriptArea()));
}
}
@RequiredArgsConstructor
private class StepIntoReverseHandler implements java.util.function.Consumer<PTreeNode<KeyData>> {
private final PTreeNode<KeyData> original;
@Override
public void accept(PTreeNode<KeyData> keyDataPTreeNode) {
Platform.runLater(this::acceptUI);
}
public void acceptUI() {
model.getDebuggerFramework().getStatePointerListener().remove(this);
PTreeNode<KeyData> stepInvOver = model.getDebuggerFramework().getStatePointer();
GoalNode<KeyData> beforeNode = stepInvOver.getStateBeforeStmt().getSelectedGoalNode();
List<GoalNode<KeyData>> stateAfterStmt = stepInvOver.getStateAfterStmt().getGoals();
ProofTree ptree = new ProofTree();
Proof proof = beforeNode.getData().getProof();
Node pnode = beforeNode.getData().getNode();
// stateAfterStmt.forEach(keyDataGoalNode -> System.out.println("keyDataGoalNode.getData().getNode().serialNr() = " + keyDataGoalNode.getData().getNode().serialNr()));
ptree.setProof(proof);
ptree.setRoot(pnode);
ptree.addNodeColor(pnode, "blueviolet");
ptree.setDeactivateRefresh(true);
if (stateAfterStmt.size() > 0) {
Set<Node> sentinels = proof.getSubtreeGoals(pnode)
.stream()
.map(Goal::node)
.collect(Collectors.toSet());
ptree.getSentinels().addAll(sentinels);
sentinels.forEach(node -> ptree.addNodeColor(node, "blueviolet"));
} else {
Set<Node> sentinels = new HashSet<>();
Iterator<Node> nodeIterator = beforeNode.getData().getNode().leavesIterator();
while (nodeIterator.hasNext()) {
Node next = nodeIterator.next();
sentinels.add(next);
}
ptree.getSentinels().addAll(sentinels);
sentinels.forEach(node -> ptree.addNodeColor(node, "blueviolet"));
//traverseProofTreeAndAddSentinelsToLeaves();
}
ptree.expandRootToSentinels();
DockNode node = new DockNode(ptree, "Proof Tree for Step Inverse Into: " +
original.getStatement().accept(new ShortCommandPrinter())