Commit bc93a6d2 authored by Alexander Weigl's avatar Alexander Weigl

DebuggerFramework Alpha Version

parent 9759947b
Pipeline #15030 failed with stage
in 2 minutes and 41 seconds
......@@ -4,8 +4,9 @@
# Execute this in this folder.
# Set to key/key/deployment/components/
COMPONENTS=${COMPONENTS:-/home/sarah/Documents/KIT_Mitarbeiter/KeYDevelopment/KeYGitDir/key/key/deployment/components/}
COMPONENTS=$HOME/work/key/key/deployment/components/
#COMPONENTS=${COMPONENTS:-/home/sarah/Documents/KIT_Mitarbeiter/KeYDevelopment/KeYGitDir/key/key/deployment/components/}
#COMPONENTS=$HOME/work/key/key/deployment/components/
COMPONENTS=lib/components/
......
......@@ -114,4 +114,13 @@ public abstract class ASTNode<T extends ParserRuleContext>
@Override
public abstract ASTNode<T> copy();
public boolean isAncestor(ASTNode node){
ASTNode n = this;
do {
if (n.equals(node))
return true;
n = n.getParent();
} while (n != null);
return true;
}
}
package edu.kit.iti.formal.psdbg;
import de.uka.ilkd.key.api.KeYApi;
import de.uka.ilkd.key.api.ProofManagementApi;
import de.uka.ilkd.key.proof.io.ProblemLoaderException;
import edu.kit.iti.formal.psdbg.interpreter.InterpreterBuilder;
import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
import java.io.File;
import java.io.IOException;
/**
* @author Alexander Weigl
* @version 1 (27.10.17)
*/
public class CommandLineDebugger {
public static void main(String[] args) throws ProblemLoaderException, IOException {
ProofManagementApi pma = KeYApi.loadFromKeyFile(new File(args[1]));
KeyInterpreter ib = new InterpreterBuilder()
.addProofScripts(new File(args[0]))
.proof(pma.getLoadedProof())
.build();
}
}
package edu.kit.iti.formal.psdbg;
import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerCommand;
import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerFramework;
public class HardStopCommand<T> extends DebuggerCommand<T> {
@Override
public void execute(DebuggerFramework<T> dbg) {
}
}
package edu.kit.iti.formal.psdbg;
import com.google.common.graph.MutableValueGraph;
import de.uka.ilkd.key.api.KeYApi;
import de.uka.ilkd.key.api.ProofManagementApi;
import de.uka.ilkd.key.proof.io.ProblemLoaderException;
import de.uka.ilkd.key.util.KeYConstants;
import edu.kit.iti.formal.psdbg.interpreter.InterpreterBuilder;
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.dbg.*;
import edu.kit.iti.formal.psdbg.interpreter.graphs.ControlFlowNode;
import edu.kit.iti.formal.psdbg.interpreter.graphs.ControlFlowTypes;
import edu.kit.iti.formal.psdbg.interpreter.graphs.ControlFlowVisitor;
import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
import edu.kit.iti.formal.psdbg.parser.Facade;
import edu.kit.iti.formal.psdbg.parser.ast.*;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import java.io.BufferedReader;
import java.io.File;
import java.io.IOException;
import java.io.InputStreamReader;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
/**
* @author Alexander Weigl
* @version 1 (27.10.17)
*/
public class InteractiveCLIDebugger {
private static final Logger LOGGER = LogManager.getLogger();
static Map<String, DebuggerCommand<KeyData>> COMMANDS = new HashMap<>();
static {
COMMANDS.put("r", new ReturnCommand());
COMMANDS.put("s", new StartCommand<>(true));
COMMANDS.put("<", new StepBackCommand<>());
COMMANDS.put(">", new StepOverCommand<>());
COMMANDS.put(".", new StepIntoCommand<>());
COMMANDS.put(";", new HardStopCommand<>());
COMMANDS.put(";", new PauseCommand<>());
}
private final ProofManagementApi pma;
private final KeyInterpreter interpreter;
private final DebuggerFramework<KeyData> df;
public InteractiveCLIDebugger(String proof, String script) throws IOException, ProblemLoaderException, DebuggerException {
pma = KeYApi.loadFromKeyFile(new File(proof));
List<ProofScript> scripts = Facade.getAST(new File(script));
InterpreterBuilder ib = new InterpreterBuilder()
.addProofScripts(scripts)
.proof(pma.getLoadedProof())
.startState()
.macros()
.scriptCommands()
.scriptSearchPath(new File("."));
interpreter = ib.build();
ControlFlowVisitor cfgVistor = new ControlFlowVisitor(ib.getLookup());
MutableValueGraph<ControlFlowNode, ControlFlowTypes> cfg = cfgVistor.getGraph();
df = new DebuggerFramework<>(interpreter, scripts.get(0), cfg);
df.getStatePointerListener().add(this::printNode);
//df.getBeforeExecutionListener().add(this::printNode);
//df.getAfterExecutionListener().add(this::end);
loop();
}
public static void main(String[] args) throws ProblemLoaderException, IOException, DebuggerException {
System.out.println("Welcome to Psdbg with KeY" + KeYConstants.INTERNAL_VERSION);
LOGGER.info("KeY Version: {}", KeYConstants.INTERNAL_VERSION);
Runtime.getRuntime().addShutdownHook(new Thread(() -> LOGGER.info("Program exited")));
new InteractiveCLIDebugger(args[0], args[1]);
}
private void debug() {
//TODO write debug information
System.out.println("digraph G {");
for (PTreeNode<KeyData> n : df.getStates()) {
System.out.format("%d [label=\"%s@%s (G: %d)\"]%n", n.hashCode(),
n.getStatement().accept(new CommandPrinter()),
n.getStatement().getStartPosition().getLineNumber(),
n.getStateBeforeStmt().getGoals().size()
);
if (n.getStepOver() != null)
System.out.format("%d -> %d [label=\"SO\"]%n", n.hashCode(), n.getStepOver().hashCode());
if (n.getStepInto() != null)
System.out.format("%d -> %d [label=\"SI\"]%n", n.hashCode(), n.getStepInto().hashCode());
if (n.getStepInvOver() != null)
System.out.format("%d -> %d [label=\"<SO\"]%n", n.hashCode(), n.getStepInvOver().hashCode());
if (n.getStepInvInto() != null)
System.out.format("%d -> %d [label=\"<SI\"]%n", n.hashCode(), n.getStepInvInto().hashCode());
if (n.getStepReturn() != null)
System.out.format("%d -> %d [label=\"R\"]%n", n.hashCode(), n.getStepReturn().hashCode());
}
System.out.println("}");
}
private void loop() throws DebuggerException {
try (BufferedReader br = new BufferedReader(new InputStreamReader(System.in))) {
while (true) {
int counter = 0;
while (true) {
boolean handled = false;
System.out.printf("dbg (%03d)> ", ++counter);
String input = br.readLine().trim().intern();
if (COMMANDS.containsKey(input)) {
handled = true;
try {
df.execute(COMMANDS.get(input));
} catch (DebuggerException e) {
if (e.isSevere())
throw e;
else {
System.err.println(e.getMessage());
}
}
}
//special
switch (input) {
case "!!":
System.exit(0);
case "dbg":
handled = true;
debug();
}
if (input.startsWith("b ")) {
handled = true;
setBreakpoint(Integer.parseInt(input.substring(2)));
}
if (!handled) System.err.println("Unknown command");
}
}
} catch (IOException e) {
e.printStackTrace();
}
}
private void end(PTreeNode<KeyData> keyDataPTreeNode) {
//TODO register if proof has ended!
}
private void printNode(PTreeNode<KeyData> node) {
System.out.format("%3d: %s%n",
node.getStatement().getStartPosition().getLineNumber(),
node.getStatement().accept(new CommandPrinter())
);
for (GoalNode<KeyData> gn : node.getStateBeforeStmt().getGoals()) {
if (gn.equals(node.getStateBeforeStmt().getSelectedGoalNode()))
System.out.format("\t* ");
else
System.out.format("\t ");
System.out.println(gn.getData().getNode().sequent());
}
}
public void setBreakpoint(int breakpoint) {
//df.addBreakpoint(breakpoint);
}
}
class CommandPrinter extends DefaultASTVisitor<String> {
@Override
public String defaultVisit(ASTNode node) {
return (Facade.prettyPrint(node));
}
@Override
public String visit(ProofScript proofScript) {
return String.format("script %s (%s) {%n",
proofScript.getName(),
Facade.prettyPrint(proofScript.getSignature()));
}
@Override
public String visit(CasesStatement casesStatement) {
return "cases {";
}
@Override
public String visit(SimpleCaseStatement caseStatement) {
return "case " + Facade.prettyPrint(caseStatement.getGuard());
}
@Override
public String visit(TryCase tryCase) {
return "try " + Facade.prettyPrint(tryCase.getBody());
}
@Override
public String visit(ClosesCase closesCase) {
return "closes with {" + Facade.prettyPrint(closesCase.getClosesScript()) + "}";
}
@Override
public String visit(TheOnlyStatement theOnly) {
return "theonly {";
}
@Override
public String visit(ForeachStatement foreach) {
return "foreach {";
}
@Override
public String visit(RepeatStatement repeatStatement) {
return ("repeat {");
}
}
package edu.kit.iti.formal.psdbg;
import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerCommand;
import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerFramework;
public class PauseCommand<T> extends DebuggerCommand<T> {
@Override
public void execute(DebuggerFramework<T> dbg) {
}
}
package edu.kit.iti.formal.psdbg;
import edu.kit.iti.formal.psdbg.interpreter.dbg.Blocker;
import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerCommand;
import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerException;
import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerFramework;
import lombok.AllArgsConstructor;
import lombok.*;
@AllArgsConstructor
public class StartCommand<T> extends DebuggerCommand<T> {
@Getter @Setter
private boolean directStop = true;
@Override
public void execute(DebuggerFramework<T> dbg) throws DebuggerException {
dbg.releaseUntil(new Blocker.CounterBlocker(1));
dbg.start();
}
}
package edu.kit.iti.formal.psdbg;
import 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()) {
new StepOverCommand<T>().execute(dbg);
} else {
dbg.releaseUntil(new Blocker.CounterBlocker(1));
}
}
}
......@@ -144,6 +144,8 @@ public class InterpreterBuilder {
public InterpreterBuilder proof(ProofApi pa) {
addKeyMatcher(pa);
pa.getRules().forEach(s -> pmr.getRules().put(s, null));
keyEnvironment = pa.getEnv();
proof = pa.getProof();
return this;
}
......
......@@ -238,8 +238,8 @@ public class KeYMatcher implements MatcherApi<KeyData> {
@Override
public List<VariableAssignment> matchSeq(GoalNode<KeyData> currentState, String data, Signature sig) {
System.out.println("State that will be matched " + currentState.getData().getNode().sequent() + " with pattern " + data);
System.out.println("Signature " + sig.toString());
//System.out.println("State that will be matched " + currentState.getData().getNode().sequent() + " with pattern " + data);
//System.out.println("Signature " + sig.toString());
Matchings m = MatcherFacade.matches(data, currentState.getData().getNode().sequent());
......
......@@ -5,13 +5,16 @@ 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;
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.VariableAssignment;
import edu.kit.iti.formal.psdbg.interpreter.funchdl.CommandLookup;
import edu.kit.iti.formal.psdbg.parser.Visitor;
import edu.kit.iti.formal.psdbg.parser.ast.ClosesCase;
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;
......@@ -43,7 +46,6 @@ public class KeyInterpreter extends Interpreter<KeyData> {
}
@Override
public Object visit(ClosesCase closesCase) {
State<KeyData> currentStateToMatch = peekState();
......@@ -65,7 +67,7 @@ public class KeyInterpreter extends Interpreter<KeyData> {
}
}
//prune proof
System.out.println("The closes script " + (allClosed ? "closed the proof.\n" : "did not close the proof.\n") + "Rolling Back proof now.");
logger.debug("The closes script " + (allClosed ? "closed the proof.\n" : "did not close the proof.\n") + "Rolling Back proof now.");
Proof currentKeYproof = selectedGoalNode.getData().getProof();
ImmutableList<Goal> subtreeGoals = currentKeYproof.getSubtreeGoals(((KeyData) selectedGoalNode.getData()).getNode());
currentKeYproof.pruneProof(selectedGoalCopy.getData().getNode());
......@@ -77,50 +79,11 @@ public class KeyInterpreter extends Interpreter<KeyData> {
@Override
public Object visit(TryCase tryCase) {
State<KeyData> currentStateToMatch = peekState();
State<KeyData> currentStateToMatchCopy = currentStateToMatch.copy(); //deepcopy
GoalNode<KeyData> selectedGoalNode = currentStateToMatch.getSelectedGoalNode();
GoalNode<KeyData> selectedGoalCopy = currentStateToMatch.getSelectedGoalNode().deepCopy(); //deepcopy
//historylistener for recording try
logger.info(String.format("Beginning side computation of %s", tryCase.getNodeName()));
startSideComputation();
TryCaseHistoryLogger list = new TryCaseHistoryLogger(this);
enterScope(tryCase);
executeBody(tryCase.getBody(), selectedGoalNode, new VariableAssignment(selectedGoalNode.getAssignments()));
State<KeyData> stateafterIsClosable = peekState();
List<GoalNode<KeyData>> goals = stateafterIsClosable.getGoals();
boolean allClosed = true;
for (GoalNode<KeyData> goal : goals) {
KeyData data = (KeyData) goal.getData();
if (!data.getNode().isClosed()) {
allClosed = false;
break;
}
}
logger.info(String.format("Ended Side Computation of %s", tryCase.getNodeName()));
endSideComputation();
if (!allClosed) {
logger.info("Try was not successful, rolling back proof");
Proof currentKeYproof = selectedGoalNode.getData().getProof();
ImmutableList<Goal> subtreeGoals = currentKeYproof.getSubtreeGoals(((KeyData) selectedGoalNode.getData()).getNode());
currentKeYproof.pruneProof(selectedGoalCopy.getData().getNode());
popState();
pushState(currentStateToMatchCopy);
} else {
//replay all proof events
//check if state is closed
exitScope(tryCase);
list.printSequenceOfEvents();
list.replayEvents(this);
logger.info("Replaying Events finished");
}
return allClosed;
boolean b = suspicionExecution(tryCase.getBody());
exitScope(tryCase);
return b;
/* //executeBody and if goal is closed afterwards return true
//else prune proof and return false
......@@ -142,4 +105,45 @@ public class KeyInterpreter extends Interpreter<KeyData> {
}
*/
}
private boolean suspicionExecution(Statements statements) {
logger.debug(String.format("Beginning of suspicion execution of %s", statements));
GoalNode<KeyData> goalNode = getSelectedNode();
pushState(new State<>(goalNode.deepCopy())); // copy for later prove
List<Visitor> backupExitListener = getExitListeners(),
backupEntryListener = getEntryListeners();
try {
TryCaseHistoryLogger list = new TryCaseHistoryLogger(this);
executeBody(statements, goalNode, new VariableAssignment(goalNode.getAssignments()));
State<KeyData> afterExec = peekState();
boolean allGoalsClosed = peekState().getGoals()
.stream()
.allMatch(g -> g.getData().getNode().isClosed());
logger.debug("Ended Side Computation");
if (!allGoalsClosed) {
logger.debug("Try was not successful, rolling back proof");
//Throw away the new state, and truncate the prove!
Proof currentKeYproof = goalNode.getData().getProof();
Node oldNode = goalNode.getData().getNode();
//ImmutableList<Goal> subtreeGoals = currentKeYproof.getSubtreeGoals(((KeyData) goalNode.getData()).getNode());
currentKeYproof.pruneProof(oldNode);
popState();
//pushState(goalNode);
} else {
//replay all proof events
//check if state is closed
//list.printSequenceOfEvents();
list.replayEvents(backupEntryListener, backupExitListener);
logger.info("Replaying Events finished");
}
return allGoalsClosed;
} finally {
exitListeners = backupExitListener;
entryListeners = backupEntryListener;
}
}
}
package edu.kit.iti.formal.psdbg.interpreter;
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.InterpreterObserver;
import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
import edu.kit.iti.formal.psdbg.parser.Visitor;
import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
import javafx.util.Pair;
import lombok.Getter;
import lombok.Setter;
import java.util.HashMap;
import java.util.LinkedList;
import java.util.ArrayList;
import java.util.List;
import java.util.Map;
/**
* Logger for Interpreting a try case. If the case was successful,
* the logged Events can be replayed back to the parent interpreter listeners
*/
public class TryCaseHistoryLogger extends HistoryListener {
private Interpreter currentInterpreter;
public class TryCaseHistoryLogger implements InterpreterObserver {
private final List<ASTNode> queueNode = new ArrayList<>(1024);
private final List<State> queueState = new ArrayList<>(1024);
private final List<Boolean> isEntryEvent = new ArrayList<>(1024);
@Getter @Setter private Interpreter interpreter;
@Getter
private EntryListener entryListener = new EntryListener();
@Getter
private ExitListener exitListener = new ExitListener();
/**
* Mapping of ASTNodes and their entry and exit states
*/
private Map<ASTNode, EntryExitPair> mapOfNodesAndStates = new HashMap<>();
/**
* List containing of pairs which contain an ASTNode and whether it was visited by entry or exit
*/
private List<Pair<EntryName, ASTNode>> sequenceOfEvents = new LinkedList<>();
public TryCaseHistoryLogger(Interpreter interpreter) {
super(interpreter);
this.currentInterpreter = interpreter;
this.interpreter = interpreter;
install(interpreter);
}
public void install(Interpreter interpreter) {
if (currentInterpreter != null) deinstall(interpreter);
interpreter.getEntryListeners().add(0, entryListener);
interpreter.getExitListeners().add(0, exitListener);
this.currentInterpreter = interpreter;
}
public void deinstall(Interpreter interpreter) {
if (interpreter != null) {
interpreter.getEntryListeners().remove(entryListener);
interpreter.getExitListeners().remove(exitListener);
}
}
public void printSequenceOfEvents() {
/* public void printSequenceOfEvents() {
for (int i = 0; i < sequenceOfEvents.size(); i++) {
Pair<EntryName, ASTNode> entryNameASTNodePair = sequenceOfEvents.get(i);
System.out.println(entryNameASTNodePair.getKey() + " " + entryNameASTNodePair.getValue().getStartPosition());
}
}
/**
* Create a new entry in maps. This is done when entering a node
*
* @param node
* @param state
* @return
*/
private Void createNewEntry(ASTNode node, State state) {
this.sequenceOfEvents.add(new Pair<>(EntryName.ENTRY, node));
this.mapOfNodesAndStates.put(node, new EntryExitPair(state));
return null;
}
/**
* Update the antrx after exiting the node
* @param node
* @param state
* @return
*/
private Void updateEntry(ASTNode node, State state) {
this.sequenceOfEvents.add(new Pair<>(EntryName.EXIT, node));
this.mapOfNodesAndStates.get(node).setExitState(state);
return null;
}
/**
* Play events back to interpreter that listeners are informed about computation
*
* @param interpreter
*/
public void replayEvents(Interpreter interpreter) {
assert sequenceOfEvents.get(0).getKey().equals(EntryName.ENTRY);
//get entry and exit listeners to inform about events
List<Visitor> entryListeners = interpreter.getEntryListeners();
List<Visitor> exitListeners = interpreter.getExitListeners();
//assert start state is equal to first entry state
State<GoalNode<KeyData>> entryState = mapOfNodesAndStates.get(sequenceOfEvents.get(0).getValue()).entryState;
assert interpreter.peekState().equals(entryState);
for (Pair<EntryName, ASTNode> nextevent : sequenceOfEvents) {
ASTNode node = nextevent.getValue();
if (nextevent.getKey().equals(EntryName.ENTRY)) {
if (entryListeners.size() != 0) {
entryListeners.forEach(node::accept);
}
interpreter.popState();
interpreter.pushState(mapOfNodesAndStates.get(node).entryState);
} else {
if (exitListeners.size() != 0) {
exitListeners.forEach(node::accept);
}
interpreter.popState();
interpreter.pushState(mapOfNodesAndStates.get(node).exitState);
}
*/
public void replayEvents(List<Visitor> entry, List<Visitor> exit) {
for (int i = 0; i < queueState.size(); i++) {
interpreter.pushState(queueState.get(i));
ASTNode node = queueNode.get(i);
if (isEntryEvent.get(i))
entry.forEach(node::accept);
else
exit.forEach(node::accept);
interpreter.popState(queueState.get(i));
}
//interpreter.popState()
}
private enum EntryName {ENTRY, EXIT}
private class EntryExitPair {