Skip to content

GitLab

P
ProofScriptParser
Commit 5e6b1ed9 authored by Alexander Weigl's avatar Alexander Weigl
Browse files
Options

add Java Source Code view

parent 7f3ef00d
Hide whitespace changes
Inline Side-by-side
Showing with 615 additions and 210 deletions
src/main/antlr4/antlrgrammars/Java8.g4
View file @ 5e6b1ed9
......@@ -1767,13 +1767,13 @@ ELLIPSIS : '...';
// Whitespace and comments
//
WS : [ \t\r\n\u000C]+ -> skip
WS : [ \t\r\n\u000C]+ -> channel(HIDDEN)
;
COMMENT
: '/*' .*? '*/' -> skip
: '/*' .*? '*/' -> channel(HIDDEN)
;
LINE_COMMENT
: '//' ~[\r\n]* -> skip
: '//' ~[\r\n]* -> channel(HIDDEN)
;
\ No newline at end of file
src/main/java/edu/kit/formal/gui/ProofScriptDebugger.java
View file @ 5e6b1ed9
......@@ -2,12 +2,12 @@ package edu.kit.formal.gui;
/**
* Main Entry for Debugger GUI
*
* @author S. Grebing
*/
import de.jensd.fx.glyphs.materialdesignicons.demo.MaterialDesignIconsDemoApp;
import de.uka.ilkd.key.util.KeYConstants;
import edu.kit.formal.gui.controller.DebuggerMainWindowController;
import edu.kit.formal.gui.model.RootModel;
import javafx.application.Application;
import javafx.fxml.FXMLLoader;
import javafx.scene.Parent;
......@@ -15,8 +15,14 @@ import javafx.scene.Scene;
import javafx.stage.Stage;
import java.io.IOException;
import java.util.logging.Logger;
public class ProofScriptDebugger extends Application {
public static final String NAME = "Proof Script Debugger";
public static final String VERSION = "0.1";
public static final String KEY_VERSION = KeYConstants.VERSION;
private Logger logger = Logger.getLogger("psdbg");
public static void main(String[] args) {
launch(args);
......@@ -24,20 +30,18 @@ public class ProofScriptDebugger extends Application {
@Override
public void start(Stage primaryStage) {
RootModel rm = new RootModel();
FXMLLoader fxmlLoader = new FXMLLoader(getClass().getResource("/DebuggerMain.fxml"));
logger.info("Start: " + NAME);
logger.info("Version: " + VERSION);
logger.info("KeY: " + KeYConstants.COPYRIGHT);
logger.info("KeY Version: " + KeYConstants.VERSION);
logger.info("KeY Internal: " + KeYConstants.INTERNAL_VERSION);
Parent root = null;
try {
root = (Parent) fxmlLoader.load();
DebuggerMainWindowController controller = fxmlLoader.<DebuggerMainWindowController>getController();
controller.setStage(primaryStage);
controller.setModel(rm);
controller.init();
FXMLLoader fxmlLoader = new FXMLLoader(getClass().getResource("/DebuggerMain.fxml"));
Parent root = fxmlLoader.load();
//DebuggerMainWindowController controller = fxmlLoader.<DebuggerMainWindowController>getController();
Scene scene = new Scene(root);
primaryStage.setTitle("Proof Script Debugger");
primaryStage.setTitle(NAME + " (" + VERSION + ") with KeY:" + KEY_VERSION);
primaryStage.setScene(scene);
primaryStage.show();
} catch (IOException e) {
......
src/main/java/edu/kit/formal/gui/controller/ContractChooser.java
View file @ 5e6b1ed9
package edu.kit.formal.gui.controller;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.speclang.Contract;
import javafx.beans.property.ObjectProperty;
import javafx.beans.property.SimpleListProperty;
import javafx.beans.property.SimpleObjectProperty;
import javafx.scene.control.ListView;
import javafx.collections.ObservableList;
import javafx.scene.control.*;
import javafx.scene.layout.VBox;
import lombok.Getter;
import org.controlsfx.dialog.WizardPane;
/**
* WozardPane to dosplay all available contracts
*/
public class ContractChooser extends WizardPane {
ListView listOfContractsView;
public class ContractChooser extends Dialog<Contract> {
@Getter
SimpleObjectProperty<Contract> chosen;
private final MultipleSelectionModel<Contract> selectionModel;
private final ObjectProperty<ObservableList<Contract>> items;
private final ListView<Contract> listOfContractsView;
private final Services services;
public ContractChooser(Services services) {
super();
setTitle("Key Contract Chooser");
setHeaderText("Please select a contract");
this.services = services;
listOfContractsView = new ListView<>();
selectionModel = listOfContractsView.getSelectionModel();
items = listOfContractsView.itemsProperty();
DialogPane dpane = new DialogPane();
dpane.setContent(listOfContractsView);
setDialogPane(dpane);
listOfContractsView.setCellFactory(ContractListCell::new);
setResizable(true);
dpane.setPrefSize(680, 320);
setResultConverter((value) -> value == ButtonType.OK ? listOfContractsView.getSelectionModel().getSelectedItem() : null);
dpane.getButtonTypes().addAll(ButtonType.OK, ButtonType.CANCEL);
}
public ContractChooser(SimpleListProperty<Contract> contracts, Contract chosenContract) {
initPane();
public ContractChooser(Services services,
SimpleListProperty<Contract> contracts) {
this(services);
listOfContractsView.itemsProperty().bind(contracts);
this.chosen.bind(listOfContractsView.getSelectionModel().selectedItemProperty());
}
public MultipleSelectionModel<Contract> getSelectionModel() {
return selectionModel;
}
public ObservableList<Contract> getItems() {
return items.get();
}
public ObjectProperty<ObservableList<Contract>> itemsProperty() {
return items;
}
public void setItems(ObservableList<Contract> items) {
this.items.set(items);
}
private void initPane() {
this.setHeaderText("KeY Contractchooser");
private class ContractListCell extends ListCell<Contract> {
public ContractListCell(ListView<Contract> contractListView) {
itemProperty().addListener((observable, oldValue, newValue) -> render());
selectedProperty().addListener((observable, oldValue, newValue) -> render());
}
private void render() {
/*
FunctionalOperationContractImpl c = (FunctionalOperationContractImpl) getItem();
IProgramMethod pm = c.getTarget();
Operator originalSelfVar = c.get != null ? contractSelf.op() : null;
Operator originalResultVar = resultTerm != null ? resultTerm.op() : null;
ImmutableList<? extends SVSubstitute> originalParamVars;
ProgramVariable originalExcVar;
boolean hasMby = c.hasMby();
Term originalMby = ;
Map<LocationVariable, Term> originalMods;
Map<LocationVariable, Boolean> hasRealModifiesClause;
de.uka.ilkd.key.logic.Term globalDefs;
Map<LocationVariable, Term> originalPres;
Map<LocationVariable, Term> originalFreePres;
Map<LocationVariable, Term> originalPosts;
Map<LocationVariable, Term> originalFreePosts;
Map<LocationVariable, Term> originalAxioms,
Modality modality;
boolean transaction;
boolean includeHtmlMarkup;
boolean usePrettyPrinting,
boolean useUnicodeSymbols
HeapLDT heapLDT = services.getTypeConverter().getHeapLDT();
TermBuilder tb = services.getTermBuilder();
LocationVariable baseHeap = heapLDT.getHeap();
StringBuffer sig = new StringBuffer();
if (originalResultVar != null) {
sig.append(originalResultVar);
sig.append(" = ");
} else if (pm.isConstructor()) {
sig.append(originalSelfVar);
sig.append(" = new ");
}
if (!pm.isStatic() && !pm.isConstructor()) {
sig.append(originalSelfVar);
sig.append(".");
}
sig.append(pm.getName());
sig.append("(");
Iterator var25 = originalParamVars.iterator();
while (var25.hasNext()) {
SVSubstitute subst = (SVSubstitute) var25.next();
if (subst instanceof Named) {
Named named = (Named) subst;
sig.append(named.name()).append(", ");
} else if (subst instanceof Term) {
sig.append(LogicPrinter.quickPrintTerm((Term) subst, services, usePrettyPrinting, useUnicodeSymbols).trim()).append(", ");
} else {
sig.append(subst).append(", ");
}
}
if (!originalParamVars.isEmpty()) {
sig.setLength(sig.length() - 2);
}
sig.append(")");
if (!pm.isModel()) {
sig.append(" catch(");
sig.append(originalExcVar);
sig.append(")");
}
String mby = hasMby ? LogicPrinter.quickPrintTerm(originalMby, services, usePrettyPrinting, useUnicodeSymbols) : null;
String mods = "";
Iterator var38 = heapLDT.getAllHeaps().iterator();
String freePres;
while (var38.hasNext()) {
LocationVariable h = (LocationVariable) var38.next();
if (originalMods.get(h) != null) {
freePres = LogicPrinter.quickPrintTerm((Term) originalMods.get(h), services, usePrettyPrinting, useUnicodeSymbols);
mods = mods + (includeHtmlMarkup ? "<br><b>" : "\n") + "mod" + (h == baseHeap ? "" : "[" + h + "]") + (includeHtmlMarkup ? "</b> " : ": ") + (includeHtmlMarkup ? LogicPrinter.escapeHTML(freePres, false) : freePres.trim());
if (!((Boolean) hasRealModifiesClause.get(h)).booleanValue()) {
mods = mods + (includeHtmlMarkup ? "<b>" : "") + ", creates no new objects" + (includeHtmlMarkup ? "</b>" : "");
}
}
}
String globalUpdates = "";
String pres;
if (globalDefs != null) {
pres = LogicPrinter.quickPrintTerm(globalDefs, services, usePrettyPrinting, useUnicodeSymbols);
globalUpdates = (includeHtmlMarkup ? "<br><b>" : "\n") + "defs" + (includeHtmlMarkup ? "</b> " : ": ") + (includeHtmlMarkup ? LogicPrinter.escapeHTML(pres, false) : pres.trim());
}
pres = "";
Iterator var41 = heapLDT.getAllHeaps().iterator();
String freePosts;
while (var41.hasNext()) {
LocationVariable h = (LocationVariable) var41.next();
if (originalPres.get(h) != null) {
freePosts = LogicPrinter.quickPrintTerm((Term) originalPres.get(h), services, usePrettyPrinting, useUnicodeSymbols);
pres = pres + (includeHtmlMarkup ? "<br><b>" : "\n") + "pre" + (h == baseHeap ? "" : "[" + h + "]") + (includeHtmlMarkup ? "</b> " : ": ") + (includeHtmlMarkup ? LogicPrinter.escapeHTML(freePosts, false) : freePosts.trim());
}
}
freePres = "";
Iterator var42 = heapLDT.getAllHeaps().iterator();
String printPosts;
while (var42.hasNext()) {
LocationVariable h = (LocationVariable) var42.next();
Term freePre = (Term) originalFreePres.get(h);
if (freePre != null && !freePre.equals(tb.tt())) {
printPosts = LogicPrinter.quickPrintTerm(freePre, services, usePrettyPrinting, useUnicodeSymbols);
freePres = freePres + (includeHtmlMarkup ? "<br><b>" : "\n") + "free pre" + (h == baseHeap ? "" : "[" + h + "]") + (includeHtmlMarkup ? "</b> " : ": ") + (includeHtmlMarkup ? LogicPrinter.escapeHTML(printPosts, false) : printPosts.trim());
}
}
String posts = "";
Iterator var45 = heapLDT.getAllHeaps().iterator();
while (var45.hasNext()) {
LocationVariable h = (LocationVariable) var45.next();
if (originalPosts.get(h) != null) {
printPosts = LogicPrinter.quickPrintTerm((Term) originalPosts.get(h), services, usePrettyPrinting, useUnicodeSymbols);
posts = posts + (includeHtmlMarkup ? "<br><b>" : "\n") + "post" + (h == baseHeap ? "" : "[" + h + "]") + (includeHtmlMarkup ? "</b> " : ": ") + (includeHtmlMarkup ? LogicPrinter.escapeHTML(printPosts, false) : printPosts.trim());
}
}
freePosts = "";
Iterator var47 = heapLDT.getAllHeaps().iterator();
String printAxioms;
while (var47.hasNext()) {
LocationVariable h = (LocationVariable) var47.next();
Term freePost = (Term) originalFreePosts.get(h);
if (freePost != null && !freePost.equals(tb.tt())) {
printAxioms = LogicPrinter.quickPrintTerm(freePost, services, usePrettyPrinting, useUnicodeSymbols);
freePosts = freePosts + (includeHtmlMarkup ? "<br><b>" : "\n") + "free post" + (h == baseHeap ? "" : "[" + h + "]") + (includeHtmlMarkup ? "</b> " : ": ") + (includeHtmlMarkup ? LogicPrinter.escapeHTML(printAxioms, false) : printAxioms.trim());
}
}
String axioms = "";
if (originalAxioms != null) {
Iterator var50 = heapLDT.getAllHeaps().iterator();
while (var50.hasNext()) {
LocationVariable h = (LocationVariable) var50.next();
if (originalAxioms.get(h) != null) {
printAxioms = LogicPrinter.quickPrintTerm((Term) originalAxioms.get(h), services, usePrettyPrinting, useUnicodeSymbols);
posts = posts + (includeHtmlMarkup ? "<br><b>" : "\n") + "axiom" + (h == baseHeap ? "" : "[" + h + "]") + (includeHtmlMarkup ? "</b> " : ": ") + (includeHtmlMarkup ? LogicPrinter.escapeHTML(printAxioms, false) : printAxioms.trim());
}
}
}
this.listOfContractsView = new ListView();
this.listOfContractsView.setVisible(true);
this.setContent(listOfContractsView);
this.setVisible(true);
this.chosen = new SimpleObjectProperty<Contract>();
return includeHtmlMarkup ? "<html><i>" + LogicPrinter.escapeHTML(sig.toString(), false) + "</i>" + globalUpdates + pres + freePres + posts + freePosts + axioms + mods + (hasMby ? "<br><b>measured-by</b> " + LogicPrinter.escapeHTML(mby, false) : "") + "<br><b>termination</b> " + modality + (transaction ? "<br><b>transaction applicable</b>" : "") + "</html>" : sig.toString() + globalUpdates + pres + freePres + posts + freePosts + axioms + mods + (hasMby ? "\nmeasured-by: " + mby : "") + "\ntermination: " + modality + (transaction ? "\ntransaction applicable:" : "");
*/
if (getItem() == null) {
setGraphic(null);
return;
}
Label head = new Label(getItem().getDisplayName() + "\n");
head.setWrapText(true);
head.setStyle("-fx-font-weight: bold; -fx-font-size: 120%");
setGraphic(new VBox(head, new Label(getItem().getPlainText(services))));
}
}
}
src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java
View file @ 5e6b1ed9
package edu.kit.formal.gui.controller;
import de.uka.ilkd.key.logic.op.IProgramMethod;
import de.uka.ilkd.key.pp.ProgramPrinter;
import de.uka.ilkd.key.speclang.Contract;
import edu.kit.formal.gui.controls.JavaArea;
import edu.kit.formal.gui.controls.ScriptArea;
import edu.kit.formal.gui.model.RootModel;
import edu.kit.formal.interpreter.KeYProofFacade;
......@@ -8,9 +11,9 @@ import edu.kit.formal.interpreter.data.GoalNode;
import edu.kit.formal.interpreter.data.KeyData;
import edu.kit.formal.interpreter.dbg.Debugger;
import javafx.beans.property.SimpleBooleanProperty;
import javafx.beans.property.SimpleObjectProperty;
import javafx.concurrent.Service;
import javafx.concurrent.Task;
import javafx.event.ActionEvent;
import javafx.fxml.FXML;
import javafx.fxml.Initializable;
import javafx.scene.control.*;
......@@ -18,7 +21,6 @@ import javafx.scene.layout.GridPane;
import javafx.scene.layout.Pane;
import javafx.scene.layout.Priority;
import javafx.stage.FileChooser;
import javafx.stage.Stage;
import lombok.Setter;
import org.apache.commons.io.FileUtils;
import org.controlsfx.dialog.Wizard;
......@@ -40,137 +42,188 @@ import java.util.concurrent.Executors;
* @author S.Grebing
*/
public class DebuggerMainWindowController implements Initializable {
private static String testFile1 = "/home/sarah/Documents/KIT_Mitarbeiter/ProofScriptingLanguage/src/test/resources/edu/kit/formal/interpreter/";
private static String testFile = "/home/sarah/Documents/KIT_Mitarbeiter/ProofScriptingLanguage/src/test/resources/edu/kit/formal/interpreter/contraposition/";
private SimpleBooleanProperty debugMode = new SimpleBooleanProperty(false);
@FXML
Pane rootPane;
private Pane rootPane;
@FXML
SplitPane splitPane;
private SplitPane splitPane;
/***********************************************************************************************************
* Code Area
* **********************************************************************************************************/
@FXML
ScrollPane scrollPaneCode;
private ScrollPane scrollPaneCode;
@FXML
ScriptArea scriptArea;
private ScriptArea scriptArea;
/***********************************************************************************************************
* MenuBar
* **********************************************************************************************************/
@FXML
MenuBar menubar;
private MenuBar menubar;
@FXML
Menu fileMenu;
private Menu fileMenu;
@FXML
MenuItem closeMenuItem;
private MenuItem closeMenuItem;
/***********************************************************************************************************
* ToolBar
* **********************************************************************************************************/
@FXML
ToolBar toolbar;
private ToolBar toolbar;
@FXML
Button buttonStartInterpreter;
private Button buttonStartInterpreter;
@FXML
Button startDebugMode;
private Button startDebugMode;
/***********************************************************************************************************
* GoalView
* **********************************************************************************************************/
@FXML
ListView goalView;
private ListView goalView;
private ExecutorService executorService = null;
private KeYProofFacade facade;
private Wizard contractChooserDialog = new Wizard();
private ContractLoaderService cls;
/**
* Model for the DebuggerController containing the neccessary references to objects needed for controlling backend through UI
* Model for the DebuggerController containing the neccessary
* references to objects needed for controlling backend through UI
*/
private RootModel model;
@FXML
private Label lblStatusMessage;
@FXML
private Label lblCurrentNodes;
@FXML
private Label lblFilename;
@Setter
private Debugger debugger;
private Stage stage;
private File initialDirectory;
@FXML
private JavaArea javaSourceCode;
/**
* @param location
* @param resources
*/
@Override
public void initialize(URL location, ResourceBundle resources) {
model = new RootModel();
setDebugMode(false);
facade = new KeYProofFacade(this.model);
cls = new ContractLoaderService();
model.scriptFileProperty().addListener((observable, oldValue, newValue) -> {
lblFilename.setText("File: " + (newValue != null ? newValue.getAbsolutePath() : "n/a"));
});
model.chosenContractProperty().addListener(o -> {
IProgramMethod method = (IProgramMethod) model.getChosenContract().getTarget();
javaSourceCode.clear();
javaSourceCode.getMarkedLines().clear();
StringWriter writer = new StringWriter();
ProgramPrinter pp = new ProgramPrinter(writer);
try {
pp.printFullMethodSignature(method);
pp.printStatementBlock(method.getBody());
writer.flush();
} catch (IOException e) {
e.printStackTrace();
}
javaSourceCode.insertText(0, writer.toString());
//debug
javaSourceCode.getMarkedLines().add(2);
javaSourceCode.getMarkedLines().add(3);
});
}
//region Actions: Execution
@FXML
public void executeScript() {
buttonStartInterpreter.setText("Interpreting...");
startDebugMode.setDisable(true);
facade.executeScript(model.getCurrentScript());
facade.executeScript(scriptArea.getText());
List<GoalNode<KeyData>> g = model.getCurrentState().getGoals();
this.model.getCurrentGoalNodes().addAll(g);
buttonStartInterpreter.setText("execute Script");
}
@FXML
public void changeToDebugMode() {
public void executeInDebugMode() {
setDebugMode(true);
executeScript();
}
//endregion
//region Actions: Menu
@FXML
protected void closeProgram() {
public void closeProgram() {
System.exit(0);
}
@FXML
protected void openScript() {
File scriptFile = openFileChooserDialog("Select Script File", "Proof Script File", "kps");
File scriptFile = openFileChooserOpenDialog("Select Script File",
"Proof Script File", "kps");
if (scriptFile != null) {
try {
String code = FileUtils.readFileToString(scriptFile, Charset.defaultCharset());
model.currentScriptProperty().set(code);
model.setScriptFile(scriptFile);
} catch (IOException e) {
showExceptionDialog("Exception occured", "",
"Could not load file " + scriptFile, e);
}
openScript(scriptFile);
}
}
public void showExceptionDialog(String title, String headerText, String contentText, Exception ex) {
Alert alert = new Alert(Alert.AlertType.ERROR);
alert.setTitle(title);
alert.setHeaderText(headerText);
alert.setContentText(contentText);
StringWriter sw = new StringWriter();
PrintWriter pw = new PrintWriter(sw);
ex.printStackTrace(pw);
String exceptionText = sw.toString();
Label label = new Label("The exception stacktrace was:");
TextArea textArea = new TextArea(exceptionText);
textArea.setEditable(false);
textArea.setWrapText(true);
@FXML
public void saveScript() {
if (model.getScriptFile() != null) {
saveScript(model.getScriptFile());
} else {
saveAsScript();
}
}
textArea.setMaxWidth(Double.MAX_VALUE);
textArea.setMaxHeight(Double.MAX_VALUE);
GridPane.setVgrow(textArea, Priority.ALWAYS);
GridPane.setHgrow(textArea, Priority.ALWAYS);
private void saveScript(File scriptFile) {
try {
FileUtils.write(scriptFile, scriptArea.getText(), Charset.defaultCharset());
} catch (IOException e) {
showExceptionDialog("Could not save file", "blubb", "...fsfsfsf fsa", e);
}
}
GridPane expContent = new GridPane();
expContent.setMaxWidth(Double.MAX_VALUE);
expContent.add(label, 0, 0);
expContent.add(textArea, 0, 1);
@FXML
public void saveAsScript() {
File f = openFileChooserSaveDialog("Save script", "", "kps");
if (f != null) {
saveScript(f);
}
}
alert.getDialogPane().setExpandableContent(expContent);
public void openScript(File scriptFile) {
assert scriptFile != null;
try {
String code = FileUtils.readFileToString(scriptFile, Charset.defaultCharset());
openScript(code);
model.setScriptFile(scriptFile);
} catch (IOException e) {
showExceptionDialog("Exception occured", "",
"Could not load file " + scriptFile, e);
}
}
alert.showAndWait();
private void openScript(String code) {
model.setScriptFile(null);
scriptArea.clear();
scriptArea.setText(code);
}
@FXML
protected void loadKeYFile() {
File keyFile = openFileChooserDialog("Select KeY File", "KeY Files", "key", "script");
File keyFile = openFileChooserOpenDialog("Select KeY File", "KeY Files", "key", "script");
this.model.setKeYFile(keyFile);
if (keyFile != null) {
buildKeYProofFacade();
......@@ -178,72 +231,34 @@ public class DebuggerMainWindowController implements Initializable {
}
public void saveProof(ActionEvent actionEvent) {