Skip to content

GitLab

Commit 6ede00a5 authored by Lulu Luong's avatar Lulu Luong
Browse files

Merge remote-tracking branch 'origin/master'

parents 2d326cb3 5c4735b3
Hide whitespace changes
Inline Side-by-side
Showing with 450 additions and 82 deletions
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Statements.java
View file @ 6ede00a5
......@@ -47,7 +47,9 @@ public class Statements extends ASTNode<ScriptLanguageParser.StmtListContext>
@Override
public ASTNode[] getChildren() {
return (ASTNode[]) toArray();
Object[] arr = toArray();
return toArray(new ASTNode[arr.length]);
//return (ASTNode[]) toArray();
}
public Statements(Statements body) {
......
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYProofFacade.java
View file @ 6ede00a5
......@@ -8,6 +8,7 @@ import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.proof.init.ProofInputException;
import de.uka.ilkd.key.proof.init.ProofOblInput;
import de.uka.ilkd.key.proof.io.ProblemLoaderException;
import de.uka.ilkd.key.speclang.Contract;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
......@@ -91,8 +92,23 @@ public class KeYProofFacade {
*/
public void reload(File problemFile) throws ProofInputException, ProblemLoaderException {
if (contract.get() != null) {// reinstante the contract
setProof(getEnvironment().createProof(
contract.get().getProofObl(getEnvironment().getServices())));
pma = KeYApi.loadFromKeyFile(problemFile);
List<Contract> contracts = pma.getProofContracts();
contracts.forEach(contract1 -> {
if(contract.get().getName().equals(contract1.getName())){
contractProperty().set(contract1);
}
});
if(contract.get() != null){
try{
activateContract(contract.get());
}catch (ProofInputException pie){
throw new ProofInputException("Contract not reloadable.", pie.getCause());
}
}
/*setProof(getEnvironment().createProof(
contract.get().getProofObl(getEnvironment().getServices())));*/
} else {
setProof(KeYApi.loadFromKeyFile(problemFile).getLoadedProof().getProof());
}
......
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/exceptions/ScriptCommandNotApplicableException.java
View file @ 6ede00a5
package edu.kit.iti.formal.psdbg.interpreter.exceptions;
import de.uka.ilkd.key.macros.scripts.AbstractCommand;
import de.uka.ilkd.key.macros.scripts.RuleCommand;
import java.util.Map;
......@@ -13,6 +14,9 @@ public class ScriptCommandNotApplicableException extends InterpreterRuntimeExcep
public ScriptCommandNotApplicableException(Exception e, RuleCommand c) {
System.out.println("Call " + c.getName() + " was not applicable");
}
public ScriptCommandNotApplicableException(Exception e, AbstractCommand c) {
System.out.println("Call " + c.getName() + " was not applicable");
}
public ScriptCommandNotApplicableException(Exception e, RuleCommand c, Map<String, Object> params) {
super(createMessage(c, params), e);
......
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/SaveCommand.java
View file @ 6ede00a5
......@@ -87,10 +87,7 @@ public class SaveCommand implements CommandHandler<KeyData> {
}
@Override
public boolean isUninterpretedParams(CallStatement call) {
return true;
}
}
......
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
View file @ 6ede00a5
......@@ -74,6 +74,7 @@ import org.reactfx.util.Timer;
import javax.annotation.Nullable;
import javax.swing.*;
import javax.xml.bind.JAXBException;
import java.awt.event.WindowAdapter;
import java.awt.event.WindowEvent;
import java.awt.event.WindowListener;
......@@ -188,7 +189,7 @@ public class DebuggerMain implements Initializable {
.filter(it -> Objects.equals(fna.childOrMe(it.getStatement()), it.getStatement()))
.collect(Collectors.toList());
System.out.println(result);
LOGGER.info(result);
for (PTreeNode<KeyData> statePointerToPostMortem : result) {
......@@ -212,13 +213,18 @@ public class DebuggerMain implements Initializable {
if (stateAfterStmt.getSelectedGoalNode() != null) {
im.setSelectedGoalNodeToShow(stateAfterStmt.getSelectedGoalNode());
} else {
im.setSelectedGoalNodeToShow(goals.get(0));
if(goals.size() > 0) {
im.setSelectedGoalNodeToShow(goals.get(0));
} else {
im.setSelectedGoalNodeToShow(stateBeforeStmt.getSelectedGoalNode());
statusBar.publishMessage("This goal node was closed by the selected mutator.");
}
}
inspectionViewsController.newPostMortemInspector(im)
.dock(dockStation, DockPos.CENTER, getActiveInspectorDock());
} else {
statusBar.publishErrorMessage("There is no post mortem state to show to this node, because this node was not executed.");
statusBar.publishErrorMessage("There is no post mortem state to show to this node, because this node was not executed or is a selector statement.");
}
}
}
......@@ -544,10 +550,11 @@ public class DebuggerMain implements Initializable {
//save old information and refresh models
statusBar.publishMessage("Reloading...");
File lastLoaded;
Contract chosen = null;
if (model.getKeyFile() != null) {
lastLoaded = model.getKeyFile();
} else {
Contract chosen = model.getChosenContract();
chosen = model.getChosenContract();
lastLoaded = model.getJavaFile();
}
//model.reload();
......@@ -561,8 +568,11 @@ public class DebuggerMain implements Initializable {
iModel.clearHighlightLines();
iModel.getGoals().clear();
iModel.setSelectedGoalNodeToShow(null);
if(chosen != null) {
FACADE.contractProperty().set(chosen);
}
try {
FACADE.reload(lastLoaded);
if (iModel.getGoals().size() > 0) {
iModel.setSelectedGoalNodeToShow(iModel.getGoals().get(0));
......@@ -1266,10 +1276,16 @@ public class DebuggerMain implements Initializable {
//Update Gui
MainScriptIdentifier msi = scriptController.getMainScript();
msi.getScriptArea().setSavepointMarker(selected.getLineNumber());
msi.getScriptArea().getCodeArea().setStyleClass(selected.getStartOffset(), selected.getEndOffset() + 1, "underlinesave"); scriptExecutionController.executeScriptFromSavePoint(interpreterBuilder, selected);
scriptController.getMainScript().getScriptArea().underlineSavepoint(selected);
try {
KeyPersistentFacade.read(FACADE.getEnvironment(), FACADE.getProof(), new StringReader(selected.getPersistedStateFile(FACADE.getFilepath()).toString()));
} catch (JAXBException e) {
e.printStackTrace();
}
scriptExecutionController.executeScriptFromSavePoint(interpreterBuilder, selected);
//TODO: KeyPersistentFacade.read(FACADE.getEnvironment(), FACADE.getProof(), new StringReader(selected.getPersistedStateFile(FACADE.getFilepath()).toString()));
//TODO (NullpointerEx: interpreterbuilder == null): scriptExecutionController.executeScriptFromSavePoint(interpreterBuilder, selected);
}
......@@ -1443,13 +1459,20 @@ public class DebuggerMain implements Initializable {
ptree.setProof(proof);
ptree.setRoot(pnode);
ptree.setNodeColor(pnode, "blueviolet");
ptree.setDeactivateRefresh(true);
ptree.setDeactivateRefresh(false);
if (stateAfterStmt.size() > 0) {
Set<Node> sentinels = proof.getSubtreeGoals(pnode)
proof.getSubtreeGoals(pnode).forEach(goal -> System.out.println("goal.node().serialNr() = " + goal.node().serialNr()));
Set<Node> sentinels;
sentinels = proof.getSubtreeGoals(pnode)
.stream()
.map(Goal::node)
.collect(Collectors.toSet());
if(sentinels.size() == 0){
sentinels = new LinkedHashSet();
sentinels.add(pnode);
//sentinels.add(stateAfterStmt.get(0).getData().getNode());
}
ptree.getSentinels().addAll(sentinels);
sentinels.forEach(node -> ptree.setNodeColor(node, "blueviolet"));
} else {
......@@ -1465,8 +1488,8 @@ public class DebuggerMain implements Initializable {
//traverseProofTreeAndAddSentinelsToLeaves();
}
ptree.expandRootToSentinels();
System.out.println("ptree = " + ptree.getRoot());
DockNode node = new DockNode(ptree, "Proof Tree for Step Into: " +
original.getStatement().accept(new ShortCommandPrinter())
);
......
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/Events.java
View file @ 6ede00a5
......@@ -2,6 +2,9 @@ package edu.kit.iti.formal.psdbg.gui.controller;
import com.google.common.eventbus.EventBus;
import de.uka.ilkd.key.logic.PosInOccurrence;
import de.uka.ilkd.key.macros.ProofMacro;
import de.uka.ilkd.key.macros.scripts.ProofScriptCommand;
import de.uka.ilkd.key.macros.scripts.ScriptCommand;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.rule.TacletApp;
......@@ -59,7 +62,7 @@ public class Events {
@Data
@RequiredArgsConstructor
public static class CommandApplicationEvent {
private final String commandName;
private final ProofScriptCommand commandName;
private final PosInOccurrence pio;
private final Goal currentGoal;
......@@ -153,4 +156,12 @@ public class Events {
private final int position;
}
@Data
@RequiredArgsConstructor
public static class MacroApplicationEvent {
private final ProofMacro macroName;
private final PosInOccurrence posInOccurrence;
private final Goal goal;
}
}
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java
View file @ 6ede00a5
......@@ -6,9 +6,8 @@ import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.Sequent;
import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.macros.scripts.EngineState;
import de.uka.ilkd.key.macros.scripts.RuleCommand;
import de.uka.ilkd.key.macros.scripts.ScriptException;
import de.uka.ilkd.key.macros.ProofMacro;
import de.uka.ilkd.key.macros.scripts.*;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof;
......@@ -27,6 +26,7 @@ import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerFramework;
import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
import edu.kit.iti.formal.psdbg.interpreter.exceptions.ScriptCommandNotApplicableException;
import edu.kit.iti.formal.psdbg.interpreter.funchdl.MacroCommandHandler;
import edu.kit.iti.formal.psdbg.parser.PrettyPrinter;
import edu.kit.iti.formal.psdbg.parser.ast.*;
import edu.kit.iti.formal.psdbg.parser.data.Value;
......@@ -47,6 +47,7 @@ import java.math.BigInteger;
import java.util.*;
import java.util.stream.Collectors;
@Getter
@Setter
@RequiredArgsConstructor
......@@ -202,7 +203,7 @@ public class InteractiveModeController {
try {
applyRule(call, g);
applyRuleHelper(call, g, Type.RULE);
// Insert into the right cases
// Node currentNode = g.node();
// cases.get(findRoot(currentNode)).add(call);
......@@ -231,6 +232,149 @@ public class InteractiveModeController {
}
@Subscribe
public void handle(Events.MacroApplicationEvent map) {
LOGGER.debug("Handling {}", map);
Goal g = map.getGoal();
MacroCommand.Parameters params = new MacroCommand.Parameters();
Parameters callp = new Parameters();
CallStatement call = new CallStatement(map.getMacroName().getScriptCommandName(), callp);
try {
applyRuleHelper(call, g, Type.MACRO);
String c = getCasesAsString();
scriptArea.setText("" +
"//Preview \n" + c);
} catch (ScriptCommandNotApplicableException e) {
StringBuilder sb = new StringBuilder("The macro command ");
sb.append(call.getCommand()).append(" was not applicable.");
System.out.println("e = " + e);
//sb.append("\nSequent Formula: formula=").append(sfTerm);
//sb.append("\nOn Sub Term: on=").append(onTerm);
Utils.showWarningDialog("Proof Command was not applicable",
"Proof Command was not applicable.",
sb.toString(), e);
}
}
private void applyRuleHelper(CallStatement call, Goal g, Type t) throws ScriptCommandNotApplicableException {
savepointslist.add(g.node());
savepointsstatement.add(call);
ObservableList<GoalNode<KeyData>> goals = model.getGoals();
GoalNode<KeyData> expandedNode;
List<GoalNode<KeyData>> collect = goals.stream().filter(keyDataGoalNode -> keyDataGoalNode.getData().getGoal().equals(g)).collect(Collectors.toList());
if (collect.isEmpty() || collect.size() > 1) {
throw new RuntimeException("Interactive Rule can not be applied, can not find goal in goal list");
} else {
expandedNode = collect.get(0);
}
// KeyData kd = g.getData();
Evaluator eval = new Evaluator(expandedNode.getAssignments(), expandedNode);
Map<String, Object> map = new HashMap<>();
call.getParameters().forEach((variable, expression) -> {
Value exp = eval.eval(expression);
map.put(variable.getIdentifier(), exp.getData());
});
LOGGER.info("Execute {} with {}", call, map);
try {
KeyData kd = expandedNode.getData();
map.put("#2", call.getCommand());
EngineState estate = new EngineState(g.proof());
estate.setGoal(g);
ValueInjector valueInjector = ValueInjector.createDefault(kd.getNode());
AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl();
switch (t){
case MACRO:
MacroCommand.Parameters cc = new MacroCommand.Parameters();
MacroCommand c = new MacroCommand();
cc = valueInjector.inject(c, cc, map);
c.execute(uiControl, cc, estate);
postStateHandler(call, g, goals, expandedNode, kd);
break;
case RULE:
RuleCommand.Parameters ccR = new RuleCommand.Parameters();
RuleCommand cR = new RuleCommand();
ccR = valueInjector.inject(cR, ccR, map);
cR.execute(uiControl, ccR, estate);
postStateHandler(call, g, goals, expandedNode, kd);
break;
case SCRIPT_COMMAND:
ScriptCommand.Parameters ccS = new ScriptCommand.Parameters();
ScriptCommand cS = new ScriptCommand();
ccS = valueInjector.inject(cS, ccS, map);
cS.execute(uiControl, ccS, estate);
postStateHandler(call, g, goals, expandedNode, kd);
break;
default:
throw new Exception("Command not found");
}
} catch (Exception e) {
if (e.getClass().equals(ScriptException.class)) {
System.out.println("e.getMessage() = " + e.getMessage());
throw new ScriptCommandNotApplicableException(e, null, map);
} else {
throw new RuntimeException(e);
}
}
}
private void postStateHandler(CallStatement call, Goal g, ObservableList<GoalNode<KeyData>> goals, GoalNode<KeyData> expandedNode, KeyData kd) {
ImmutableList<Goal> ngoals = g.proof().getSubtreeGoals(expandedNode.getData().getNode());
goals.remove(expandedNode);
GoalNode<KeyData> last = null;
if (ngoals.size() > 1) {
cases.get(findRoot(ngoals.get(0).node())).add(call);
CasesStatement inner = new CasesStatement();
cases.get(findRoot(ngoals.get(0).node())).add(inner);
for (Goal newGoalNode : ngoals) {
KeyData kdn = new KeyData(kd, newGoalNode.node());
goals.add(last = new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed()));
val caseForSubNode = new GuardedCaseStatement();
val m = new MatchExpression();
m.setPattern(new StringLiteral(
format(LabelFactory.getBranchingLabel(newGoalNode.node()))
));
caseForSubNode.setGuard(m);
inner.getCases().add(caseForSubNode);
cases.put(last.getData().getNode(), caseForSubNode.getBody());
}
} else {
if (ngoals.size() == 0) {
cases.get(findRoot(expandedNode.getData().getNode())).add(call);
} else {
KeyData kdn = new KeyData(kd, ngoals.get(0).node());
goals.add(last = new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed()));
Node currentNode = last.getData().getNode();
cases.get(findRoot(currentNode)).add(call);
}
}
if (last != null)
model.setSelectedGoalNodeToShow(last);
}
private Node findRoot(Node cur) {
while (cur != null) {
if (cases.keySet().contains(cur))
......@@ -245,7 +389,7 @@ public class InteractiveModeController {
casesStatement.accept(pp);
return pp.toString();
}
/*
private void applyRule(CallStatement call, Goal g) throws ScriptCommandNotApplicableException {
savepointslist.add(g.node());
savepointsstatement.add(call);
......@@ -282,6 +426,7 @@ public class InteractiveModeController {
//System.out.println("formula = " + map.get("formula"));
//System.out.println("occ = " + map.get("occ"));
ValueInjector valueInjector = ValueInjector.createDefault(kd.getNode());
RuleCommand.Parameters cc = new RuleCommand.Parameters();
cc = valueInjector.inject(c, cc, map);
AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl();
......@@ -333,7 +478,7 @@ public class InteractiveModeController {
}
}
}
}*/
private String format(String branchingLabel) {
// System.out.println("branchingLabel = " + branchingLabel);
......@@ -363,4 +508,8 @@ public class InteractiveModeController {
}
static enum Type {
MACRO, RULE, SCRIPT_COMMAND;
}
}
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java
View file @ 6ede00a5
......@@ -20,6 +20,7 @@ import javafx.collections.FXCollections;
import javafx.collections.ObservableList;
import javafx.collections.ObservableMap;
import javafx.collections.ObservableSet;
import javafx.event.EventHandler;
import javafx.fxml.FXML;
import javafx.scene.control.ContextMenu;
import javafx.scene.control.TreeCell;
......@@ -30,10 +31,7 @@ import javafx.scene.layout.BorderPane;
import javafx.util.StringConverter;
import lombok.*;
import java.util.HashMap;
import java.util.Iterator;
import java.util.Map;
import java.util.Set;
import java.util.*;
import java.util.function.Consumer;
......@@ -161,18 +159,22 @@ public class ProofTree extends BorderPane {
this.colorOfNodes.put(n, color);
}
public void expandRootToSentinels() {
if (getTreeProof().getRoot() == null) {
if (root.get() != null) {
TreeItem<TreeNode> item = populate("Proof", root.get());
//populate(root.get().serialNr() + ": " + toString(root.get()), root.get());
//val treeNode = new TreeNode("Proof", root.get());
TreeItem<TreeNode> item;
if(sentinels.contains(root.get())){
item = treeCreation.itemFactory(root.get());
} else {
item = treeCreation.populate("Proof", root.get());
}
treeProof.setRoot(item);
}
}
//expandRootToLeaves(getTreeProof().getRoot());
expandRootToLeaves(getTreeProof().getRoot());
}
public TreeView<TreeNode> getTreeProof() {
......@@ -215,38 +217,40 @@ public class ProofTree extends BorderPane {
}
};
tftc.setConverter(stringConverter);
tftc.itemProperty().addListener((p, o, n) -> {
if (n != null)
if (n != null )
repaint(tftc);
});
//colorOfNodes.addListener((InvalidationListener) o -> repaint(tftc));
return tftc;
}
private void repaint(TextFieldTreeCell<TreeNode> tftc) {
TreeNode item = tftc.getItem();
Node n = item.node;
tftc.setStyle("");
if (n != null) {
if (n.leaf() && !item.label.contains("BRANCH")) {
if (n.isClosed()) {
colorOfNodes.putIfAbsent(n, "lightseagreen");
//tftc.setStyle("-fx-background-color: greenyellow");
} else {
colorOfNodes.putIfAbsent(n, "indianred");
}
if (colorOfNodes.containsKey(n)) {
tftc.setStyle("-fx-background-color: " + colorOfNodes.get(n) + ";");
if (n.leaf() && !item.label.contains("CASE") ) {
if (n.isClosed()) {
colorOfNodes.putIfAbsent(n, "lightseagreen");
} else {
colorOfNodes.putIfAbsent(n, "indianred");
}
if (colorOfNodes.containsKey(n)) {
tftc.setStyle("-fx-background-color: " + colorOfNodes.get(n) + ";");
}
}
}
//TODO for Screenshot tftc.setStyle("-fx-font-size: 18pt");
/* if (colorOfNodes.containsKey(n)) {
tftc.setStyle("-fx-border-color: "+colorOfNodes.get(n)+";");
}*/
}
expandRootToItem(tftc.getTreeItem());
//System.out.println("colorOfNodes = " + colorOfNodes);
}
......@@ -321,11 +325,46 @@ public class ProofTree extends BorderPane {
if (root.get() != null) {
TreeItem<TreeNode> item = treeCreation.create(proof.get());
item.addEventHandler(TreeItem.branchExpandedEvent(), new EventHandler<TreeItem.TreeModificationEvent<TreeNode>>() {
@Override
public void handle(TreeItem.TreeModificationEvent<TreeNode> event) {
expandTreeView(event.getTreeItem());
}
});
item.addEventHandler(TreeItem.branchCollapsedEvent(), new EventHandler<TreeItem.TreeModificationEvent<TreeNode>>() {
@Override
public void handle(TreeItem.TreeModificationEvent<TreeNode> event) {
collapseTreeView(event.getTreeItem());
treeProof.setCellFactory(ProofTree.this::cellFactory);
}