Commit b765012c authored by Alexander Weigl's avatar Alexander Weigl

syncing to desktop

parent 2577adfe
Pipeline #15009 failed with stage
in 1 minute and 52 seconds
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.interpreter.dbg;
package edu.kit.iti.formal.psdbg;
import edu.kit.iti.formal.psdbg.interpreter.HistoryListener;
import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
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.dbg.Blocker;
import edu.kit.iti.formal.psdbg.interpreter.dbg.PseudoMatcher;
import edu.kit.iti.formal.psdbg.interpreter.funchdl.BuiltinCommands;
import edu.kit.iti.formal.psdbg.interpreter.funchdl.CommandHandler;
import edu.kit.iti.formal.psdbg.interpreter.funchdl.DefaultLookup;
......
......@@ -14,8 +14,10 @@ import edu.kit.iti.formal.psdbg.parser.data.Value;
import edu.kit.iti.formal.psdbg.parser.types.Type;
import lombok.Getter;
import lombok.Setter;
import org.antlr.v4.runtime.ParserRuleContext;
import java.util.*;
import java.util.concurrent.atomic.AtomicBoolean;
import java.util.logging.Logger;
import java.util.stream.Collectors;
import java.util.stream.Stream;
......@@ -32,13 +34,15 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
protected static Logger logger = Logger.getLogger("interpreter");
@Getter
public final AtomicBoolean hardStop = new AtomicBoolean(false);
//TODO later also include information about source line for each state (for debugging purposes and rewind purposes)
private Stack<State<T>> stateStack = new Stack<>();
//We now need thet stack of listeners to handle try statements scuh that listnersa re only informed if a try was sucessfull
//We now need the stack of listeners to handle try statements scuh that listnersa re only informed if a try was sucessfull
private Stack<List<Visitor>> entryListenerStack = new Stack<>();
private Stack<List<Visitor>> exitListenerStack = new Stack<>();
//there is at most one special listener that is allowed to block and that is invoked last when informing all listeners
private Visitor blockingEntryListener = new DefaultASTVisitor();
//@Getter
//private List<Visitor> entryListeners = new ArrayList<>(),
......@@ -73,12 +77,11 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
return entryListenerStack.peek();
}
public void addBlockingEntryListener(Visitor v) {
blockingEntryListener = v;
}
public void removeBlockingEntryListener() {
blockingEntryListener = new DefaultASTVisitor();
@Override
public <T extends ParserRuleContext> void enterScope(ASTNode<T> node) {
if(hardStop.get())
throw new InterpreterRuntimeException("hard stop");
callListeners(getEntryListeners(),node);
}
/**
......@@ -110,7 +113,6 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
*/
@Override
public Object visit(ProofScript proofScript) {
//add vars
visit(proofScript.getSignature());
enterScope(proofScript);
......@@ -213,7 +215,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
List<CaseStatement> cases = casesStatement.getCases();
for (GoalNode<T> goal : allGoalsBeforeCases) {
newState(goal); //to allow the visit method for the case stmt to retrieve goal
newState(goal); //to allow the visit method for the case statement to retrieve goal
boolean result = false;
for (CaseStatement aCase : cases) {
......
package edu.kit.iti.formal.psdbg.interpreter;
import edu.kit.iti.formal.psdbg.interpreter.graphs.PTreeNode;
import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
import lombok.Getter;
/**
......
......@@ -3,7 +3,7 @@ package edu.kit.iti.formal.psdbg.interpreter;
import edu.kit.iti.formal.psdbg.interpreter.data.InterpreterExtendedState;
import edu.kit.iti.formal.psdbg.interpreter.data.State;
import edu.kit.iti.formal.psdbg.interpreter.graphs.PTreeNode;
import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
import lombok.Getter;
/**
......
package edu.kit.iti.formal.psdbg.interpreter.data;
import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
import edu.kit.iti.formal.psdbg.parser.ast.CaseStatement;
import lombok.Data;
import lombok.RequiredArgsConstructor;
import java.util.Collections;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
@RequiredArgsConstructor
@Data
public class InterpreterExtendedState<T> {
/**
* Null if root
*/
private final InterpreterExtendedState<T> predecessor;
/**
* If we are in a case statement, this map defines which
*/
private Map<CaseStatement, List<GoalNode<T>>> mappingOfCaseToStates = new HashMap<>();
/**
* State before the statement;
*/
private State<T> stateBeforeStmt;
/**
* State after execution of statement
*/
private State<T> stateAfterStmt;
/**
* Statement
*/
private ASTNode stmt;
public InterpreterExtendedState<T> copy() {
InterpreterExtendedState<T> ext = new InterpreterExtendedState<>(
this.predecessor != null
? this.predecessor.copy()
: null);
ext.setStmt(stmt);
if (stateAfterStmt != null) {
ext.setStateAfterStmt(this.stateAfterStmt.copy());
}
if (stateBeforeStmt != null) {
ext.setStateBeforeStmt(this.stateBeforeStmt.copy());
}
return ext;
}
/*
public List<GoalNode<T>> getClosedNodes() {
return super.getGoals().stream().filter(nodes -> nodes.isClosed()).collect(Collectors.toList());
}
public List<GoalNode<T>> getOpenNodes() {
return super.getGoals().stream().filter(nodes -> !nodes.isClosed()).collect(Collectors.toList());
}*/
public List<GoalNode<T>> getActiveGoalsForCase(CaseStatement caseStmt) {
return mappingOfCaseToStates.getOrDefault(caseStmt, Collections.emptyList());
}
@Override
public String toString() {
StringBuilder sb = new StringBuilder();
//sb.append("\n%%%%%%%%%%%%%%%%%%%%%\n");
sb.append("Extended State ");
if (getStmt() != null) {
sb.append(getStmt().getNodeName() + ": \n");
}
sb.append("State before Statement: \n");
if (stateBeforeStmt != null) {
stateBeforeStmt.getGoals().stream().map(GoalNode::getData).forEach(sb::append);
} else {
sb.append("Before is Empty");
}
sb.append("\nAfter Statement:\n");
if (stateAfterStmt != null) {
stateAfterStmt.getGoals().stream().map(GoalNode::getData).forEach(sb::append);
} else {
sb.append("After is empty");
}
if (getMappingOfCaseToStates().containsKey(stmt)) {
sb.append("Case Stmt with");
getMappingOfCaseToStates().get(stmt).forEach(tGoalNode -> {
sb.append(tGoalNode.getData());
});
}
//sb.append("\n%%%%%%%%%%%%%%%%%%%%\n");
return sb.toString();
// this.stateBeforeStmt.toString()+"\n"+this.stateAfterStmt.toString();
}
//getuserSelected/
//verfuegbar im case
//map<case, listgoal>
//regel anwendbar oder nicht
}
package edu.kit.iti.formal.psdbg.gui.controller;
package edu.kit.iti.formal.psdbg.interpreter.dbg;
import edu.kit.iti.formal.psdbg.interpreter.HistoryListener;
import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.data.State;
import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
import edu.kit.iti.formal.psdbg.parser.Visitor;
import edu.kit.iti.formal.psdbg.parser.ast.*;
import javafx.application.Platform;
import javafx.beans.property.SimpleObjectProperty;
import lombok.Getter;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import java.util.Collections;
import java.util.Set;
import java.util.concurrent.ConcurrentSkipListSet;
import java.util.TreeSet;
import java.util.concurrent.atomic.AtomicInteger;
import java.util.concurrent.locks.Condition;
import java.util.concurrent.locks.Lock;
......@@ -22,60 +19,33 @@ import java.util.concurrent.locks.ReentrantLock;
/**
* Created by weigl on 21.05.2017.
*/
public class PuppetMaster {
public class BlockListener<T> {
private static Logger LOGGER = LogManager.getLogger(BlockListener.class);
private final Lock lock = new ReentrantLock();
private final Condition block = lock.newCondition();
/**
* Properties that are changed, when new states are added using the blocker
*/
//private final SimpleObjectProperty<List<GoalNode<KeyData>>> currentGoals = new SimpleObjectProperty<>();
//private final SimpleObjectProperty<GoalNode<KeyData>> currentSelectedGoal = new SimpleObjectProperty<>();
private final SimpleObjectProperty<State<KeyData>> currentState = new SimpleObjectProperty<>();
public State<KeyData> getCurrentState() {
return currentState.get();
}
public void setCurrentState(State<KeyData> currentState) {
this.currentState.set(currentState);
}
public SimpleObjectProperty<State<KeyData>> currentStateProperty() {
return currentState;
}
private KeyInterpreter puppet;
@Getter
private final Set<Integer> breakpoints = new TreeSet<>();
private Interpreter<T> puppet;
private AtomicInteger stepUntilBlock = new AtomicInteger(-1);
private HistoryListener historyLogger;
private Set<Integer> brkpnts = new ConcurrentSkipListSet<>();
private Visitor<Void> entryListener = new EntryListener();
private Visitor<Void> exitListener = new ExitListener();
public PuppetMaster() {
public BlockListener() {
}
public PuppetMaster(Interpreter<KeyData> inter) {
public BlockListener(Interpreter<T> inter) {
install(puppet);
}
/*public SimpleObjectProperty<List<GoalNode<KeyData>>> currentGoalsProperty() {
return currentGoals;
}*/
public HistoryListener getHistoryLogger() {
return historyLogger;
}
public void install(KeyInterpreter interpreter) {
public void install(Interpreter<T> interpreter) {
if (puppet != null) deinstall(puppet);
interpreter.getEntryListeners().add(entryListener);
interpreter.getEntryListeners().add(exitListener);
puppet = interpreter;
}
public void deinstall(Interpreter<KeyData> interpreter) {
public void deinstall(Interpreter<T> interpreter) {
if (interpreter != null) {
interpreter.getEntryListeners().remove(entryListener);
interpreter.getEntryListeners().remove(exitListener);
......@@ -83,7 +53,7 @@ public class PuppetMaster {
}
public Void checkForHalt(ASTNode node) {
//("PuppetMaster CheckForHalt node = [" + node + "]");
//("BlockListener CheckForHalt node = [" + node + "]");
//<0 run
if (stepUntilBlock.get() > 0)
......@@ -96,60 +66,13 @@ public class PuppetMaster {
int lineNumber = node.getStartPosition().getLineNumber();
if (brkpnts.contains(lineNumber)) {
if (breakpoints.contains(lineNumber)) {
//publishState();
block();
}
return null;
}
/**
* Publish state is called after the interpreter or debugger thread terminated. The resulting goals are set in the root model
*/
public void publishState() {
//("PuppetMaster.publishState");
//puppet is null if successful interpreter state and publish state
if (puppet != null) {
final State<KeyData> state = puppet.getCurrentState().copy();
Platform.runLater(() -> {
this.setCurrentState(state);
});
/* Platform.runLater(() -> {
//filter whether all goals are closed
Object[] arr = state.getGoals().stream().filter(keyDataGoalNode -> !keyDataGoalNode.isClosed()).toArray();
setCurrentState(state);
//currentState.set(state);
/*if (state.getSelectedGoalNode() == null) {
if (arr.length == 0) {
currentGoals.set(Collections.emptyList());
//currentSelectedGoal.set(state.getGoals().get(0));
currentSelectedGoal.set(null);
} else {
currentGoals.set(state.getGoals());
currentSelectedGoal.set(null);
}
} else {
currentGoals.set(state.getGoals());
currentSelectedGoal.set(state.getSelectedGoalNode());
}
});*/
} else {
//if puppet is null an empty state may be reached therefore state get goals etc returns null
Platform.runLater(() -> {
setCurrentState(new State<KeyData>(Collections.emptyList(), null));
// currentGoals.set(Collections.emptyList());
// currentSelectedGoal.set(null);
});
}
}
/**
* Blocks the current thread. Makes him awakable on {@code block}.
*/
......@@ -165,7 +88,7 @@ public class PuppetMaster {
}
public void addBreakpoint(int i) {
brkpnts.add(i);
breakpoints.add(i);
}
public void unlock() {
......@@ -177,47 +100,10 @@ public class PuppetMaster {
}
}
/* public GoalNode<KeyData> getCurrentSelectedGoal() {
return currentSelectedGoal.get();
}
public void setCurrentSelectedGoal(GoalNode<KeyData> currentSelectedGoal) {
this.currentSelectedGoal.set(currentSelectedGoal);
}
public SimpleObjectProperty<GoalNode<KeyData>> currentSelectedGoalProperty() {
return currentSelectedGoal;
}
public List<GoalNode<KeyData>> getCurrentGoals() {
return currentGoals.get();
}
public void setCurrentGoals(List<GoalNode<KeyData>> currentGoals) {
this.currentGoals.set(currentGoals);
}
/* public SimpleObjectProperty<List<GoalNode<KeyData>>> currentGoalsProperty() {
return currentGoals;
}*/
public Set<Integer> getBreakpoints() {
return brkpnts;
}
public AtomicInteger getStepUntilBlock() {
return stepUntilBlock;
}
public void deinstall() {
deinstall(puppet);
}
public void addHistoryLogger(HistoryListener historyLogger) {
this.historyLogger = historyLogger;
}
private class EntryListener extends DefaultASTVisitor<Void> {
@Override
......
package edu.kit.iti.formal.psdbg.interpreter.dbg;
import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
import edu.kit.iti.formal.psdbg.parser.ast.*;
import java.util.Set;
import java.util.TreeSet;
import java.util.concurrent.atomic.AtomicInteger;
import java.util.concurrent.locks.Condition;
import java.util.concurrent.locks.Lock;
import java.util.concurrent.locks.ReentrantLock;
/**
* Created by weigl on 21.05.2017.
*/
public class Blocker extends DefaultASTVisitor<Void> {
AtomicInteger stepUntilBlock = new AtomicInteger(-1);
//needs to threadable
Set<Integer> brkpnts = new TreeSet<>();
final Lock lock = new ReentrantLock();
final Condition block = lock.newCondition();
//better a semaphore?
//Semaphore semaphore = new Semaphore();
public Void checkForHalt(ASTNode node) {
if (stepUntilBlock.get() > 0)
stepUntilBlock.decrementAndGet();
if (stepUntilBlock.get() == 0)
block();
int lineNumber = node.getStartPosition().getLineNumber();
if (brkpnts.contains(lineNumber)) {
block();
}
return super.defaultVisit(node);
}
private void block() {
try {
lock.lock();
block.await();
} catch (InterruptedException e) {
e.printStackTrace();
} finally {
lock.unlock();
}
}
public void addBreakpoint(int i) {
brkpnts.add(i);
}
public void unlock() {
try {
lock.lock();
block.signal();
} finally {
lock.unlock();
}
}
@Override
public Void visit(ProofScript proofScript) {
return checkForHalt(proofScript);
}
@Override
public Void visit(AssignmentStatement assignment) {
return checkForHalt(assignment);
}
@Override
public Void visit(CasesStatement casesStatement) {
return checkForHalt(casesStatement);
}
@Override
public Void visit(CaseStatement caseStatement) {
return checkForHalt(caseStatement);
}
@Override
public Void visit(CallStatement call) {
return checkForHalt(call);
}
@Override
public Void visit(TheOnlyStatement theOnly) {
return checkForHalt(theOnly);
}
@Override
public Void visit(ForeachStatement foreach) {
return checkForHalt(foreach);
}
@Override
public Void visit(RepeatStatement repeatStatement) {
return checkForHalt(repeatStatement);
}
}
package edu.kit.iti.formal.psdbg.interpreter.dbg;
import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
import javafx.event.EventHandler;
import javax.annotation.Nonnull;
import java.util.LinkedList;
import java.util.List;
/**
* @author Alexander Weigl
* @version 1 (27.10.17)
*/
public class DebuggerFramework<T> {
private final Interpreter<T> interpreter;
private Thread interpreterThread;
private BlockListener<T> listener;
private StateWrapper stateWrapper;
private List<EventHandler<BeforeExecution>> beforeExecutionListener = new LinkedList<>();
private List<EventHandler<AfterExecution>> beforeExecutionListener = new LinkedList<>();
public DebuggerFramework(@Nonnull Interpreter<T> interpreter,
@Nonnull final ProofScript script) {
this.interpreter = interpreter;
listener = new BlockListener<>(interpreter);
interpreterThread = new Thread(() -> interpreter.interpret(script));
}
public void start() {
interpreterThread.start();
}
public void hardStop() {
interpreter.getHardStop().set(true);
//interpreterThread.stop();
}
}
package edu.kit.iti.formal.psdbg.interpreter.graphs;
package edu.kit.iti.formal.psdbg.interpreter.dbg;
import edu.kit.iti.formal.psdbg.interpreter.NodeAddedEvent;
import edu.kit.iti.formal.psdbg.interpreter.StateAddedEvent;
......@@ -7,11 +7,6 @@ import edu.kit.iti.formal.psdbg.interpreter.StateAddedEvent;
* Listener for Change events in the state graph
*/
public interface GraphChangedListener {
abstract void graphChanged(NodeAddedEvent nodeAddedEvent);
abstract void graphChanged(StateAddedEvent stateAddedEvent);
}
package edu.kit.iti.formal.psdbg.interpreter.dbg;
import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
import edu.kit.iti.formal.psdbg.parser.Visitor;
/**
* @author Alexander Weigl
* @version 1 (27.10.17)
*/
public interface InterpreterObserver<T> {
default void install(Interpreter<T> interpreter) {
if (getInterpreter() != null) deinstall(interpreter);
interpreter.getEntryListeners().add(0, getEntryListener());
interpreter.getExitListeners().add(0, getExitListener());
setInterpreter(interpreter);
}
Interpreter<T> getInterpreter();
void setInterpreter(Interpreter<T> interpreter);
default void deinstall(Interpreter<T> interpreter) {
if (interpreter != null) {
interpreter.getEntryListeners().remove(getEntryListener());
interpreter.getExitListeners().remove(getExitListener());
}
}
Visitor getExitListener();
Visitor getEntryListener();
}
package edu.kit.iti.formal.psdbg.interpreter.dbg;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.State;
import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
import edu.kit.iti.formal.psdbg.parser.ast.CaseStatement;
import lombok.Data;
import lombok.RequiredArgsConstructor;
import lombok.ToString;
import java.util.*;
/**
* PTreeNode represents a node in the state graph.
* <p>
* This class is visualized by the debugger. Their interdepencies are given via the {@link StateGraphWrapper}.
* </p>
* A node contains a reference to the ASTNode and a reference to the corresponding interpreter state
* if this state is already interpreted, null otherwise.
*/
@Data
@ToString
@RequiredArgsConstructor
public class PTreeNode<T> {
private final ASTNode statement;
private Map<CaseStatement, List<GoalNode<T>>> mappingOfCaseToStates = new HashMap<>();
private State<T> stateBeforeStmt;