Commit fbfe9ac5 authored by Lulu Luong's avatar Lulu Luong
Browse files

merge with master

parents 7e12bf82 36832366
Pipeline #33843 failed with stages
in 54 seconds
......@@ -58,6 +58,11 @@ public class GoalNode<T> {
this.id = id;
}
private GoalNode(int id, GoalNode<T> parent, VariableAssignment ass, T data, boolean isClosed) {
this(parent, ass, data, isClosed);
this.id = id;
}
private GoalNode(int id, T data, boolean isClosed) {
this(data);
this.isClosed = isClosed;
......@@ -133,7 +138,8 @@ public class GoalNode<T> {
*/
public GoalNode<T> deepCopy() {
if (parent != null) {
return new GoalNode<T>(id, parent.deepCopy(), data, isClosed);
VariableAssignment deepCopy = parent.assignments.deepCopy();
return new GoalNode<T>(id, parent.deepCopy(), deepCopy, data, isClosed);
} else {
return new GoalNode<T>(id, data, isClosed);
}
......
......@@ -49,6 +49,13 @@ public class PseudoMatcher implements MatcherApi<String> {
}
return Collections.singletonList(va);
}
@Override
public GoalNode<String> isDerivable(GoalNode<String> currentState, Value v) {
return null;
}
}
\ No newline at end of file
......@@ -4,6 +4,7 @@ import edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain;
import edu.kit.iti.formal.psdbg.gui.model.MainScriptIdentifier;
import lombok.*;
import org.apache.commons.io.FileUtils;
import org.apache.commons.io.FilenameUtils;
import org.apache.commons.io.IOUtils;
import java.io.File;
......@@ -24,7 +25,12 @@ public abstract class Example {
protected MainScriptIdentifier mainScriptIdentifier;
public static File newTempFile(URL url, String filename) throws IOException {
File f = new File(FileUtils.getTempDirectoryPath(), filename);
File psdbg = new File(FileUtils.getTempDirectoryPath(), "psdbg");
File examplefolder = new File(psdbg.getPath(), FilenameUtils.removeExtension(filename));
File f = new File(examplefolder, filename);
FileUtils.copyURLToFile(url, f);
return f;
}
......
......@@ -190,7 +190,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) {
......@@ -214,13 +214,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.");
}
}
}
......@@ -547,10 +552,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();
......@@ -564,8 +570,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));
......@@ -805,6 +814,7 @@ public class DebuggerMain implements Initializable {
if (javaFile != null) {
model.setJavaFile(javaFile);
model.setInitialDirectory(javaFile.getParentFile());
contractLoaderService.reset();
contractLoaderService.start();
}
}
......@@ -1164,7 +1174,6 @@ public class DebuggerMain implements Initializable {
} else {
throw new RuntimeException("Something went wrong when reloading");
}
}
/* public void handle(Events.TacletApplicationEvent tap){
......@@ -1448,7 +1457,31 @@ public class DebuggerMain implements Initializable {
protected void succeeded() {
statusBar.publishMessage("Contract loaded");
List<Contract> contracts = getValue();
ContractChooser cc = new ContractChooser(FACADE.getService(), contracts);
/*
String javaFile = model.getJavaFile().getName();
List<Contract> filteredContracts = new ArrayList<>();
for (Contract contract : contracts) {
String contractFile = contract.getKJT().getFullName();
if (javaFile == contractFile) {
filteredContracts.add(contract);
}
}
if (filteredContracts.size() == 0) {
Utils.showInfoDialog("No loadable contract", "No loadable contract",
"There's no loadable contract for the chosen java file.");
return;
}
*/
ContractChooser cc = null;
try {
cc = new ContractChooser(FACADE.getService(), FACADE.getContractsForJavaFile(model.getJavaFile()));
} catch (ProblemLoaderException e) {
e.printStackTrace();
}
cc.showAndWait().ifPresent(result -> {
model.setChosenContract(result);
......@@ -1499,13 +1532,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 {
......@@ -1522,6 +1562,7 @@ public class DebuggerMain implements Initializable {
}
ptree.expandRootToSentinels();
System.out.println("ptree = " + ptree.getRoot());
DockNode node = new DockNode(ptree, "Proof Tree for Step Into: " +
original.getStatement().accept(new ShortCommandPrinter())
);
......
......@@ -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;
}
}
package edu.kit.iti.formal.psdbg.gui.controller;
import com.google.common.eventbus.Subscribe;
import de.uka.ilkd.key.api.KeYApi;
import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
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.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.ProofScriptCommandBuilder;
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;
......@@ -43,10 +43,12 @@ import org.key_project.util.collection.ImmutableList;
import recoder.util.Debug;
import javax.annotation.Nullable;
import java.lang.reflect.Method;
import java.math.BigInteger;
import java.util.*;
import java.util.stream.Collectors;
@Getter
@Setter
@RequiredArgsConstructor
......@@ -65,8 +67,8 @@ public class InteractiveModeController {
private PTreeNode<KeyData> nodeAtInteractionStart;
//needed for Undo-Operation
private ArrayList<CallStatement> savepointsstatement;
private ArrayList<Node> savepointslist;
private ArrayList<CallStatement> laststatementlist;
private ArrayList<Node> lastnodeslist;
private Proof currentProof;
private Services keYServices;
......@@ -98,8 +100,8 @@ public class InteractiveModeController {
gcs.setBody(v);
casesStatement.getCases().add(gcs);
});
savepointslist = new ArrayList<>();
savepointsstatement = new ArrayList<>();
lastnodeslist = new ArrayList<>();
laststatementlist = new ArrayList<>();
nodeAtInteractionStart = debuggerFramework.getStatePointer();
}
......@@ -109,13 +111,14 @@ public class InteractiveModeController {
* Undo the application of the last rule
*/
public void undo(javafx.event.ActionEvent actionEvent) {
if (savepointslist.isEmpty()) {
if (lastnodeslist.isEmpty()) {
Debug.log("Kein vorheriger Zustand.");
return;
}
val pruneNode = savepointslist.get(savepointslist.size() - 1);
savepointslist.remove(pruneNode);
val pruneNode = lastnodeslist.get(lastnodeslist.size() - 1);
lastnodeslist.remove(pruneNode);
ImmutableList<Goal> goalsbeforePrune = currentProof.getSubtreeGoals(pruneNode);
currentProof.pruneProof(pruneNode);
......@@ -126,19 +129,55 @@ public class InteractiveModeController {
.filter(keyDataGoalNode -> goalsbeforePrune.contains(keyDataGoalNode.getData().getGoal()))
.collect(Collectors.toList());
if(prunedChildren.size() == 0) {
//TODO: add Utils.showInfoD
return;
}
KeyData kd = prunedChildren.get(0).getData();
goals.removeAll(prunedChildren);
//Set selected goal after prune
GoalNode<KeyData> lastGoalNode = null;
for (Goal newGoalNode : goalsafterPrune) {
KeyData kdn = new KeyData(kd, newGoalNode.node());
KeyData kdn;
if (lastnodeslist.size() == 0) {
kdn = new KeyData(kd, goalsafterPrune.get(0).node());
goals.add(
lastGoalNode = new GoalNode<>(prunedChildren.get(0).getParent().getParent(), kdn, kdn.getNode().isClosed()));
lastGoalNode = new GoalNode<>(prunedChildren.get(0).getParent(), kdn, kdn.getNode().isClosed()));
} else {
for (Goal newGoalNode : goalsafterPrune) {
kdn = new KeyData(kd, newGoalNode.node());
goals.add(
lastGoalNode = new GoalNode<>(prunedChildren.get(0).getParent().getParent(), kdn, kdn.getNode().isClosed()));
}
}
model.setSelectedGoalNodeToShow(lastGoalNode);
val pruneStatement = savepointsstatement.get(savepointsstatement.size() - 1);
cases.forEach((k, v) -> v.remove(pruneStatement));
val pruneStatement = laststatementlist.get(laststatementlist.size() - 1);
laststatementlist.remove(laststatementlist.size() - 1);
//TODO: buggy cuz allstatements of same node removed
//remove statement from cases / script
Statements statements = (cases.get(pruneNode.parent()) == null)? cases.get(pruneNode) : cases.get(pruneNode.parent());
int i = statements.size()-1;
while(statements.get(i) != pruneStatement && i >= 0) {
statements.remove(i);
i--;
}
statements.remove(i);
/*
cases.forEach((k, v) -> {
v.remove(pruneStatement);
});
*/
String c = getCasesAsString();
scriptArea.setText("" +
......@@ -202,7 +241,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 +270,184 @@ 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);
}
}
@Subscribe
public void handle(Events.CommandApplicationEvent map) {
LOGGER.debug("Handling {}", map);
Goal g = map.getCurrentGoal();
Parameters callp = new Parameters();
CallStatement call = new CallStatement(map.getCommandName().getName(), callp);
try {
applyRuleHelper(call, g, Type.SCRIPT_COMMAND);
String c = getCasesAsString();
scriptArea.setText("" +
"//Preview \n" + c);
} catch (ScriptCommandNotApplicableException e) {
StringBuilder sb = new StringBuilder("The script 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 {
lastnodeslist.add(g.node());
laststatementlist.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:
ProofScriptCommandBuilder psb = new ProofScriptCommandBuilder(KeYApi.getScriptCommandApi().getScriptCommands());
ProofScriptCommand ps = psb.getCommands().get(call.getCommand());
Object temp = valueInjector.inject(ps, getParameterInstance(ps), map);
ps.execute(uiControl, temp, 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 <T> T getParameterInstance(ProofScriptCommand c) throws NoSuchMethodException, IllegalAccessException,
InstantiationException {
Method method = c.getClass().getMethod("evaluateArguments", EngineState.class, Map.class);
Class rtclazz = method.getReturnType();
return (T) rtclazz.newInstance();
}
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,10 +462,10 @@ 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);
lastnodeslist.add(g.node());
laststatementlist.add(call);