Commit fe351689 authored by Alexander Weigl's avatar Alexander Weigl

ProofTree changes

parent e6361f70
package edu.kit.iti.formal.psdbg.interpreter.dbg;
import edu.kit.iti.formal.psdbg.parser.Facade;
import edu.kit.iti.formal.psdbg.parser.ast.Expression;
import lombok.Data;
import lombok.EqualsAndHashCode;
@Data
@EqualsAndHashCode(of = {"sourceName", "lineNumber"})
public class Breakpoint {
private String sourceName;
private int lineNumber;
private boolean enabled;
private String condition;
private Expression conditionAst;
public Breakpoint(String file, int lineNumber) {
sourceName = file;
this.lineNumber = lineNumber;
}
public boolean isConditional() {
return condition != null;
}
public void setCondition(String condition) {
this.condition = condition;
if (condition != null)
this.conditionAst = Facade.parseExpression(condition);
}
}
\ No newline at end of file
......@@ -4,34 +4,36 @@ import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
import de.uka.ilkd.key.api.ProofApi;
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.gui.ProofScriptDebugger;
import edu.kit.iti.formal.psdbg.gui.controls.*;
import edu.kit.iti.formal.psdbg.gui.model.Breakpoint;
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.MainScriptIdentifier;
import edu.kit.iti.formal.psdbg.gui.model.InterpreterThreadState;
import edu.kit.iti.formal.psdbg.interpreter.InterpreterBuilder;
import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.dbg.*;
import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
import javafx.beans.property.*;
import javafx.beans.value.ChangeListener;
import javafx.beans.value.ObservableBooleanValue;
import javafx.beans.value.ObservableValue;
import javafx.application.Platform;
import javafx.beans.binding.BooleanBinding;
import javafx.collections.FXCollections;
import javafx.concurrent.Service;
import javafx.concurrent.Task;
import javafx.event.ActionEvent;
import javafx.event.EventHandler;
import javafx.fxml.FXML;
import javafx.fxml.Initializable;
import javafx.scene.control.Button;
import javafx.scene.control.Menu;
import javafx.scene.control.MenuItem;
import javafx.scene.control.ProgressBar;
import javafx.scene.control.*;
import javafx.scene.web.WebEngine;
import javafx.scene.web.WebView;
import javafx.stage.FileChooser;
import lombok.Getter;
import org.antlr.v4.runtime.RecognitionException;
import org.apache.commons.io.FileUtils;
import org.apache.logging.log4j.LogManager;
......@@ -39,16 +41,22 @@ import org.apache.logging.log4j.Logger;
import org.dockfx.DockNode;
import org.dockfx.DockPane;
import org.dockfx.DockPos;
import org.reactfx.util.FxTimer;
import org.reactfx.util.Timer;
import javax.annotation.Nullable;
import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
import java.io.PrintWriter;
import java.net.URL;
import java.nio.charset.Charset;
import java.time.Duration;
import java.util.List;
import java.util.Optional;
import java.util.ResourceBundle;
import java.util.Set;
import java.util.concurrent.ExecutorService;
import java.util.concurrent.Executors;
import java.util.concurrent.*;
/**
* Controller for the Debugger MainWindow
......@@ -58,23 +66,18 @@ import java.util.concurrent.Executors;
*/
public class DebuggerMain implements Initializable {
public static final KeYProofFacade FACADE = new KeYProofFacade();
protected static final Logger LOGGER = LogManager.getLogger(DebuggerMain.class);
public final ContractLoaderService contractLoaderService = new ContractLoaderService();
private final ProofTreeController proofTreeController = new ProofTreeController();
private final InspectionViewsController inspectionViewsController = new InspectionViewsController();
private final ExecutorService executorService = Executors.newFixedThreadPool(2);
/**
* Property: current loaded javaFile
*/
private final ObjectProperty<File> javaFile = new SimpleObjectProperty<>(this, "javaFile");
/**
* Property: current loaded KeY File
*/
private final ObjectProperty<File> keyFile = new SimpleObjectProperty<>(this, "keyFile");
/**
* Chosen contract for problem
*/
private final ObjectProperty<Contract> chosenContract = new SimpleObjectProperty<>(this, "chosenContract");
@Getter
private final DebuggerMainModel model = new DebuggerMainModel();
private ScriptController scriptController;
@FXML
......@@ -82,83 +85,134 @@ public class DebuggerMain implements Initializable {
@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;
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 = inspectionViewsController.getActiveInterpreterTabDock();
private BooleanProperty debugMode = new SimpleBooleanProperty(this, "debugMode", false);
private CommandHelp commandHelp = new CommandHelp();
private DockNode commandHelpDock = new DockNode(commandHelp, "Command Help");
/**
* True, iff the execution is not possible
*/
private ObservableBooleanValue executeNotPossible = proofTreeController.executeNotPossibleProperty().or(FACADE.readyToExecuteProperty().not());
// private ObservableBooleanValue stepNotPossible = proofTreeController.stepNotPossibleProperty();
/**
*
*/
private ObjectProperty<File> initialDirectory = new SimpleObjectProperty<>(this, "initialDirectory");
/**
*
*/
private StringProperty javaCode = new SimpleStringProperty(this, "javaCode");
private DockNode commandHelpDock = new DockNode(commandHelp, "DebuggerCommand Help");
//-----------------------------------------------------------------------------------------------------------------
@FXML
private Menu examplesMenu;
private Timer interpreterThreadTimer;
@Override
public void initialize(URL location, ResourceBundle resources) {
Events.register(this);
setDebugMode(false);
model.setDebugMode(false);
scriptController = new ScriptController(dockStation);
//register the welcome dock in the center
welcomePaneDock.dock(dockStation, DockPos.LEFT);
registerToolbarToStatusBar();
marriageProofTreeControllerWithActiveInspectionView();
//statusBar.publishMessage("File: " + (newValue != null ? newValue.getAbsolutePath() : "n/a"));
marriageJavaCode();
//marriage key proof facade to proof tree
getFacade().proofProperty().addListener(
(prop, o, n) -> {
proofTree.setRoot(n.root());
if (n == null) {
proofTree.setRoot(null);
} else {
proofTree.setRoot(n.root());
getInspectionViewsController().getActiveInspectionViewTab()
.getModel().getGoals().setAll(FACADE.getPseudoGoals());
}
proofTree.setProof(n);
getInspectionViewsController().getActiveInspectionViewTab().getModel().getGoals().setAll(FACADE.getPseudoGoals());
}
);
//Debugging
Utils.addDebugListener(javaCode);
Utils.addDebugListener(executeNotPossible, "executeNotPossible");
//
model.statePointerProperty().addListener((prop, o, n) -> {
this.handleStatePointerUI(n);
});
//Debugging
Utils.addDebugListener(model.javaCodeProperty());
Utils.addDebugListener(model.executeNotPossibleProperty(), "executeNotPossible");
scriptController.mainScriptProperty().bindBidirectional(statusBar.mainScriptIdentifierProperty());
initializeExamples();
dockingNodeHandling(togBtnActiveInspector,
miActiveInspector,
activeInspectorDock,
DockPos.CENTER);
dockingNodeHandling(togBtnCodeDock,
miCodeDock,
javaAreaDock,
DockPos.RIGHT);
dockingNodeHandling(togBtnCommandHelp,
miCommandHelp,
commandHelpDock,
DockPos.RIGHT);
dockingNodeHandling(togBtnWelcome,
miWelcomeDock,
welcomePaneDock,
DockPos.CENTER);
dockingNodeHandling(togBtnProofTree,
miProofTree,
proofTreeDock,
DockPos.LEFT);
statusBar.interpreterStatusModelProperty().bind(model.interpreterStateProperty());
renewThreadStateTimer();
}
/**
* If the mouse moves other toolbar button, the help text should display in the status bar
*/
private void registerToolbarToStatusBar() {
/*toolbar.getChildrenUnmodifiable().forEach(
n -> n.setOnMouseEntered(statusBar.getTooltipHandler()));
......@@ -167,61 +221,46 @@ public class DebuggerMain implements Initializable {
}
/**
* Connects the proof tree controller with the model of the active inspection view model.
* <b>Note:</b> This is executed in the Interpreter Thread!
* You should listen to the {@link DebuggerMainModel#statePointerProperty}
*
* @param node
*/
private void marriageProofTreeControllerWithActiveInspectionView() {
InspectionModel imodel = getInspectionViewsController().getActiveInspectionViewTab().getModel();
//set all listeners
proofTreeController.currentGoalsProperty().addListener((o, old, fresh) -> {
if (fresh != null) {
imodel.setGoals(fresh);
} else {
// no goals, set an empty list
imodel.setGoals(FXCollections.observableArrayList());
}
});
proofTreeController.currentSelectedGoalProperty().addListener((observable, oldValue, newValue) -> {
imodel.setCurrentInterpreterGoal(newValue);
//also update the selected to be shown
imodel.setSelectedGoalNodeToShow(newValue);
//System.out.println("Pos: "+newValue.getData().getNode().getNodeInfo().getActiveStatement().getPositionInfo());
});
proofTreeController.currentHighlightNodeProperty().addListener((observable, oldValue, newValue) -> {
if (newValue != null) {
System.out.println("Highlight" + newValue);
scriptController.getDebugPositionHighlighter().highlight(newValue);
}
private void handleStatePointer(PTreeNode<KeyData> node) {
Platform.runLater(() -> model.setStatePointer(node));
}
});
/**
* Handling of a new state in the {@link DebuggerFramework}, now in the JavaFX Thread
*
* @see {@link #handleStatePointer(PTreeNode)}
*/
private void handleStatePointerUI(PTreeNode<KeyData> node) {
InspectionModel im = getInspectionViewsController().getActiveInspectionViewTab().getModel();
imodel.goalsProperty().addListener((observable, oldValue, newValue) -> statusBar.setNumberOfGoals(newValue.size()));
im.getGoals().setAll(
node.getStateBeforeStmt().getGoals()
);
im.setSelectedGoalNodeToShow(
node.getStateBeforeStmt().getSelectedGoalNode());
/*proofTreeController.currentExecutionEndProperty().addListener((observable, oldValue, newValue) -> {
scriptController.getMainScript().getScriptArea().removeExecutionMarker();
LineMapping lm = new LineMapping(scriptController.getMainScript().getScriptArea().getText());
int i = lm.getLineEnd(newValue.getEndPosition().getLineNumber() - 1);
scriptController.getMainScript().getScriptArea().insertExecutionMarker(i);
scriptController.getDebugPositionHighlighter().highlight(node.getStatement());
});*/
Utils.addDebugListener(proofTreeController.currentGoalsProperty(), Utils::reprKeyDataList);
Utils.addDebugListener(proofTreeController.currentSelectedGoalProperty(), Utils::reprKeyData);
Utils.addDebugListener(proofTreeController.currentHighlightNodeProperty());
//Experimental
ComboBox<PTreeNode<KeyData>> frames = getInspectionViewsController().getActiveInspectionViewTab().getFrames();
List<PTreeNode<KeyData>> ctxn = node.getContextNodes();
frames.getItems().setAll(ctxn);
frames.getSelectionModel().select(node);
}
public void marriageJavaCode() {
private void marriageJavaCode() {
//Listener on chosenContract from
chosenContract.addListener(o -> {
model.chosenContractProperty().addListener(o -> {
//javaCode.set(Utils.getJavaCode(chosenContract.get()));
try {
System.out.println(chosenContract.get().getHTMLText(getFacade().getService()));
LOGGER.debug("Selected contract: {}", model.getChosenContract().getHTMLText(getFacade().getService()));
String encoding = null; //encoding Plattform default
javaCode.set(FileUtils.readFileToString(javaFile.get(), encoding));
model.setJavaCode(FileUtils.readFileToString(model.javaFileProperty().get(), Charset.defaultCharset()));
} catch (IOException e) {
e.printStackTrace();
}
......@@ -238,14 +277,11 @@ public class DebuggerMain implements Initializable {
}
});
javaCode.addListener(new ChangeListener<String>() {
@Override
public void changed(ObservableValue<? extends String> observable, String oldValue, String newValue) {
try {
javaArea.setText(newValue);
} catch (Exception e) {
LOGGER.catching(e);
}
model.javaCodeProperty().addListener((observable, oldValue, newValue) -> {
try {
javaArea.setText(newValue);
} catch (Exception e) {
LOGGER.catching(e);
}
});
......@@ -270,25 +306,6 @@ public class DebuggerMain implements Initializable {
});
}
public void showCodeDock(ActionEvent actionEvent) {
if (!javaAreaDock.isDocked()) {
javaAreaDock.dock(dockStation, DockPos.RIGHT);
}
}
//region Actions: Execution
/**
* When play button is used
*/
public File getJavaFile() {
return javaFile.get();
}
//region Actions: Menu
/*@FXML
......@@ -302,85 +319,97 @@ public class DebuggerMain implements Initializable {
}
}*/
public void setJavaFile(File javaFile) {
this.javaFile.set(javaFile);
}
public File getKeyFile() {
return keyFile.get();
public void showCodeDock(ActionEvent actionEvent) {
if (!javaAreaDock.isDocked()) {
javaAreaDock.dock(dockStation, DockPos.RIGHT);
}
}
public void setKeyFile(File keyFile) {
this.keyFile.set(keyFile);
}
public void dockingNodeHandling(ToggleButton btn, CheckMenuItem cmi, DockNode dn, DockPos defaultPosition) {
BooleanBinding prop = dn.dockedProperty().or(dn.floatingProperty());
prop.addListener((p, o, n) -> {
btn.setSelected(n);
cmi.setSelected(n);
});
/**
* Reload the KeY environment, to execute the script again
* TODO: reload views
*
* @param file
* @param keyfile
* @return
*/
public Task<Void> reloadEnvironment(File file, boolean keyfile) {
Task<Void> task = new Task<Void>() {
@Override
protected Void call() throws Exception {
FACADE.reloadEnvironment();
if (keyfile) {
openKeyFile(file);
} else {
openJavaFile(file);
}
return null;
EventHandler<ActionEvent> handler = event -> {
if (!prop.get()) {
if (dn.getLastDockPos() != null)
dn.dock(dockStation, dn.getLastDockPos());
else
dn.dock(dockStation, defaultPosition);
} else {
dn.undock();
}
};
return task;
btn.setOnAction(handler);
cmi.setOnAction(handler);
}
@FXML
public void executeScript() {
executorHelper(false);
executeScript(false);
}
private void executorHelper(boolean addInitBreakpoint) {
@FXML
public void abortExecution() {
if (model.getDebuggerFramework() != null) {
try {
// try to friendly
Future future = executorService.submit(() -> {
model.getDebuggerFramework().stop();
model.getDebuggerFramework().unregister();
model.getDebuggerFramework().release();
});
if (proofTreeController.isAlreadyExecuted()) {
File file;
boolean isKeyfile = false;
if (getJavaFile() != null) {
file = getJavaFile();
} else {
isKeyfile = true;
file = getKeyFile();
// wait a second!
future.get(1, TimeUnit.SECONDS);
// ungently stop
model.getDebuggerFramework().hardStop();
} catch (InterruptedException | ExecutionException | TimeoutException e) {
e.printStackTrace();
} finally {
model.setDebuggerFramework(null);
}
} else {
LOGGER.info("no interpreter running");
}
}
Task<Void> reloading = reloadEnvironment(file, isKeyfile);
reloading.setOnSucceeded(event -> {
statusBar.publishMessage("Cleared and Reloaded Environment");
executeScript(FACADE.buildInterpreter(), addInitBreakpoint);
private void executeScript(boolean addInitBreakpoint) {
if (model.getDebuggerFramework() != null) {
Alert alert = new Alert(Alert.AlertType.CONFIRMATION, "Interpreter is already running \nDo want to abort it?",
ButtonType.CANCEL, ButtonType.YES);
Optional<ButtonType> ans = alert.showAndWait();
ans.ifPresent(a -> {
if (a == ButtonType.OK) abortExecution();
});
}
reloading.setOnFailed(event -> {
event.getSource().exceptionProperty().get();
Utils.showExceptionDialog("Loading Error", "Could not clear Environment", "There was an error when clearing old environment",
(Throwable) event.getSource().exceptionProperty().get()
);
});
assert model.getDebuggerFramework() == null : "There should not be any interpreter running.";
ProgressBar bar = new ProgressBar();
bar.progressProperty().bind(reloading.progressProperty());
executorService.execute(reloading);
} else {
if (FACADE.getProofState() == KeYProofFacade.ProofState.EMPTY) {
Alert alert = new Alert(Alert.AlertType.ERROR, "No proof loaded!", ButtonType.OK);
alert.showAndWait();
return;
}
executeScript(FACADE.buildInterpreter(), addInitBreakpoint);
if (FACADE.getProofState() == KeYProofFacade.ProofState.DIRTY) {
try {
FACADE.reload(model.getKeyFile());
} catch (ProofInputException | ProblemLoaderException e) {
LOGGER.error(e);
Utils.showExceptionDialog("Loading Error", "Could not clear Environment", "There was an error when clearing old environment",
e
);
}
}
// else getProofState() == VIRGIN!
executeScript(FACADE.buildInterpreter(), addInitBreakpoint);
}
/**
* Execute the script that with using the interpreter that is build using the interpreterbuilder
*
......@@ -388,61 +417,129 @@ public class DebuggerMain implements Initializable {
* @param
*/
private void executeScript(InterpreterBuilder ib, boolean addInitBreakpoint) {
Set<Breakpoint> breakpoints = scriptController.getBreakpoints();
if (proofTreeController.isAlreadyExecuted()) {
proofTreeController.saveGraphs();
}
this.debugMode.set(addInitBreakpoint);
statusBar.publishMessage("Parse ...");
try {
//parsing
Set<Breakpoint> breakpoints = scriptController.getBreakpoints();
// get possible scripts and the main script!
List<ProofScript> scripts = scriptController.getCombinedAST();
System.out.println("Parsed Scripts");
int n = 0;
if (scriptController.getMainScript() == null) {
MainScriptIdentifier msi = new MainScriptIdentifier();
msi.setLineNumber(scripts.get(0).getStartPosition().getLineNumber());
msi.setScriptName(scripts.get(0).getName());
msi.setSourceName(scripts.get(0).getRuleContext().getStart().getInputStream().getSourceName());
msi.setScriptArea(scriptController.findEditor(new File(scripts.get(0).getRuleContext().getStart().getInputStream().getSourceName())));
scriptController.setMainScript(msi);
n = 0;
scriptController.setMainScript(scripts.get(0));
}
Optional<ProofScript> mainScript = scriptController.getMainScript().find(scripts);
ProofScript ms;
if (!mainScript.isPresent()) {
scriptController.setMainScript(scripts.get(0));
ms = scripts.get(0);
} else {
for (int i = 0; i < scripts.size(); i++) {
ProofScript proofScript = scripts.get(i);
if (proofScript.getName().equals(scriptController.getMainScript().getScriptName())) {
n = i;
break;
}