Skip to content

P
ProofScriptParser
Commit 7e5e33d0 authored by Sarah Grebing's avatar Sarah Grebing
Browse files
Options

Merge remote-tracking branch 'origin/master' 

# Conflicts:
#	src/main/java/edu/kit/formal/psdb/gui/controller/DebuggerMain.java
#	src/main/java/edu/kit/formal/psdb/interpreter/graphs/ProofTreeController.java
parents 96b2b783 932ccd8b
Hide whitespace changes
Inline Side-by-side
Showing with 1391 additions and 733 deletions
pom.xml
View file @ 7e5e33d0
......@@ -129,7 +129,7 @@
</executions>
<configuration>
<!-- The package of your generated sources -->
<packageName>edu.kit.formal.proofscriptparser.lint</packageName>
<packageName>edu.kit.formal.psdb.lint</packageName>
</configuration>
</plugin>
......@@ -207,7 +207,7 @@
<transformer
implementation="org.apache.maven.plugins.shade.resource.ManifestResourceTransformer">
<mainClass>
edu.kit.formal.gui.ProofScriptDebugger
edu.kit.formal.psdb.gui.ProofScriptDebugger
</mainClass>
</transformer>
</transformers>
......
src/main/antlr4/edu/kit/formal/psdb/termmatcher/MatchPattern.g4 0 → 100644
View file @ 7e5e33d0
grammar MatchPattern;
/* Examples for testing
f(x)
f(x,y,g(y))
X
?Y
_
...
f(... ?X ...)
f(..., ?X)
f(..., ...?X...)
f(..., ... g(x) ...)
f(_, x, _, y, ... y ...)
*/
termPattern :
DONTCARE #dontCare
//| STARDONTCARE #starDontCare
| SID #schemaVar
| STARDONTCARE termPattern STARDONTCARE #anywhere
| func=ID ( '(' termPattern (',' termPattern)* ')')? #function
;
/*
f(x), f(x,y,g(y)), X, ?Y, _, ..., f(... ?X ...), f(..., ?X), f(..., ...?X...), f(..., ... g(x) ...), f(_, x, _, y, ... y ...)
*/
semiSeqPattern : termPattern (',' termPattern)*;
sequentPattern : semiSeqPattern? ARROW semiSeqPattern?;
ARROW : '⇒' | '==>';
DONTCARE: '?' | '_' | '█';
STARDONTCARE: '...' | '…';
DIGITS : DIGIT+ ;
fragment DIGIT : [0-9] ;
SID: '?' [_a-zA-Z0-9\\]+ ;
ID : [a-zA-Z\\_] ([_a-zA-Z0-9\\])* ;
COMMENT: '//' ~[\n\r]* -> channel(HIDDEN);
WS: [\n\f\r\t ] -> channel(HIDDEN);
\ No newline at end of file
src/main/antlr4/edu/kit/formal/termmatcher/MatchPattern.g4 deleted 100644 → 0
View file @ 96b2b783
grammar MatchPattern;
schemaTerm :
'_'
|'...'
| schemaVar
| logicalVar
| functionSymbol ('('schemaTerm (',' schemaTerm)? ')')?
;
termHelper :
schemaTerm
| functionSymbol '('termHelper (',' termHelper)? ')'
;
functionSymbol :
ID+
;
schemaVar:
'?'ID+
;
logicalVar:
ID+
;
DIGITS : DIGIT+ ;
fragment DIGIT : [0-9] ;
ID : [a-zA-Z] ([_a-zA-Z0-9] | '.' | '\\' | '[]' | '-')* ;
\ No newline at end of file
src/main/java/edu/kit/formal/gui/ProofScriptDebugger.java → src/main/java/edu/kit/formal/psdb/gui/ProofScriptDebugger.java
View file @ 7e5e33d0
package edu.kit.formal.gui;
package edu.kit.formal.psdb.gui;
/**
* Main Entry for Debugger GUI
......@@ -17,7 +17,6 @@ import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.dockfx.DockNode;
import java.io.IOException;
import java.util.Locale;
public class ProofScriptDebugger extends Application {
......@@ -36,9 +35,9 @@ public class ProofScriptDebugger extends Application {
Locale.setDefault(Locale.ENGLISH);
try {
FXMLLoader fxmlLoader = new FXMLLoader(getClass().getResource("/DebuggerMain.fxml"));
FXMLLoader fxmlLoader = new FXMLLoader(getClass().getResource("/edu/kit/formal/psdb/gui/controller/DebuggerMain.fxml"));
Parent root = fxmlLoader.load();
//DebuggerMainWindowController controller = fxmlLoader.<DebuggerMainWindowController>getController();
//DebuggerMain controller = fxmlLoader.<DebuggerMain>getController();
Scene scene = new Scene(root);
primaryStage.setOnCloseRequest(event -> Platform.exit());
scene.getStylesheets().addAll(
......@@ -58,8 +57,9 @@ public class ProofScriptDebugger extends Application {
//logger.error("sfklsajflksajfsdajfsdalfjsdaf", new IllegalAccessError("dlfsdalfjsadflj"));
} catch (IOException e) {
} catch (Exception e) {
e.printStackTrace();
System.exit(1);
}
}
......
src/main/java/edu/kit/formal/gui/controller/ContractChooser.java → src/main/java/edu/kit/formal/psdb/gui/controller/ContractChooser.java
View file @ 7e5e33d0
package edu.kit.formal.gui.controller;
package edu.kit.formal.psdb.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.collections.ObservableList;
import javafx.event.EventHandler;
import javafx.scene.control.*;
import javafx.scene.layout.VBox;
import javafx.stage.Modality;
import lombok.Getter;
import java.awt.event.KeyEvent;
import java.util.List;
/**
......
src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java → src/main/java/edu/kit/formal/psdb/gui/controller/DebuggerMain.java
View file @ 7e5e33d0
package edu.kit.formal.gui.controller;
package edu.kit.formal.psdb.gui.controller;
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.speclang.Contract;
import edu.kit.formal.gui.ProofScriptDebugger;
import edu.kit.formal.gui.controls.*;
import edu.kit.formal.gui.model.Breakpoint;
import edu.kit.formal.gui.model.InspectionModel;
import edu.kit.formal.interpreter.Interpreter;
import edu.kit.formal.interpreter.InterpreterBuilder;
import edu.kit.formal.interpreter.KeYProofFacade;
import edu.kit.formal.interpreter.data.KeyData;
import edu.kit.formal.interpreter.graphs.PTreeNode;
import edu.kit.formal.interpreter.graphs.ProofTreeController;
import edu.kit.formal.proofscriptparser.ast.ProofScript;
import edu.kit.formal.psdb.gui.ProofScriptDebugger;
import edu.kit.formal.psdb.gui.controls.*;
import edu.kit.formal.psdb.gui.model.InspectionModel;
import edu.kit.formal.psdb.interpreter.Interpreter;
import edu.kit.formal.psdb.interpreter.InterpreterBuilder;
import edu.kit.formal.psdb.interpreter.KeYProofFacade;
import edu.kit.formal.psdb.interpreter.data.KeyData;
import edu.kit.formal.psdb.interpreter.graphs.PTreeNode;
import edu.kit.formal.psdb.interpreter.graphs.ProofTreeController;
import edu.kit.formal.psdb.parser.ast.ProofScript;
import javafx.beans.property.*;
import javafx.beans.value.ChangeListener;
import javafx.beans.value.ObservableBooleanValue;
......@@ -53,9 +53,9 @@ import java.util.concurrent.Executors;
* @author S.Grebing
* @author Alexander Weigl
*/
public class DebuggerMainWindowController implements Initializable {
public class DebuggerMain implements Initializable {
public static final KeYProofFacade FACADE = new KeYProofFacade();
protected static final Logger LOGGER = LogManager.getLogger(DebuggerMainWindowController.class);
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();
......@@ -86,6 +86,8 @@ public class DebuggerMainWindowController implements Initializable {
//-----------------------------------------------------------------------------------------------------------------
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();
......@@ -124,6 +126,17 @@ public class DebuggerMainWindowController implements Initializable {
//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());
proofTree.setProof(n);
getInspectionViewsController().getActiveInspectionViewTab().getModel().getGoals().setAll(FACADE.getPseudoGoals());
}
);
//Debugging
Utils.addDebugListener(javaCode);
Utils.addDebugListener(executeNotPossible, "executeNotPossible");
......@@ -345,11 +358,74 @@ public class DebuggerMainWindowController implements Initializable {
}
}
//region Actions: Menu
@FXML
public void closeProgram() {
System.exit(0);
}
@FXML
public void openScript() {
File scriptFile = openFileChooserOpenDialog("Select Script File",
"Proof Script File", "kps");
if (scriptFile != null) {
openScript(scriptFile);
}
}
@FXML
public void saveScript() {
try {
scriptController.saveCurrentScript();
} catch (IOException e) {
Utils.showExceptionDialog("Could not save file", "Saving File Error", "Could not save current script", e);
}
}
private void saveScript(File scriptFile) {
try {
scriptController.saveCurrentScriptAs(scriptFile);
} catch (IOException e) {
Utils.showExceptionDialog("Could not save file", "Saving File Error", "Could not save to file " + scriptFile.getName(), e);
}
}
@FXML
public void saveAsScript() throws IOException {
File f = openFileChooserSaveDialog("Save script", "Save Script files", "kps");
if (f != null) {
/* if(!f.exists()){
f.createNewFile();
}*/
saveScript(f);
}
}
public void openScript(File scriptFile) {
assert scriptFile != null;
setInitialDirectory(scriptFile.getParentFile());
try {
String code = FileUtils.readFileToString(scriptFile, Charset.defaultCharset());
ScriptArea area = scriptController.createNewTab(scriptFile);
} catch (IOException e) {
Utils.showExceptionDialog("Exception occured", "",
"Could not load sourceName " + scriptFile, e);
}
}
@FXML
protected void loadKeYFile() {
File keyFile = openFileChooserOpenDialog("Select KeY File", "KeY Files", "key", "kps");
openKeyFile(keyFile);
}
public void openKeyFile(File keyFile) {
if (keyFile != null) {
setKeyFile(keyFile);
setInitialDirectory(keyFile.getParentFile());
Task<Void> task = FACADE.loadKeyFileTask(keyFile);
Task<ProofApi> task = FACADE.loadKeyFileTask(keyFile);
task.setOnSucceeded(event -> {
statusBar.publishMessage("Loaded key sourceName: %s", keyFile);
statusBar.stopProgress();
......@@ -370,6 +446,27 @@ public class DebuggerMainWindowController implements Initializable {
}
}
/**
* Save KeY proof as proof file
*
* @param actionEvent
*/
public void saveProof(ActionEvent actionEvent) {
LOGGER.error("saveProof not implemented!!!");
}
//endregion
//region Santa's Little Helper
@FXML
protected void loadJavaFile() {
File javaFile = openFileChooserOpenDialog("Select Java File", "Java Files", "java");
openJavaFile(javaFile);
}
public void openJavaFile(File javaFile) {
if (javaFile != null) {
setJavaFile(javaFile);
......@@ -378,8 +475,9 @@ public class DebuggerMainWindowController implements Initializable {
}
}
public void setKeyFile(File keyFile) {
this.keyFile.set(keyFile);
public void openJavaFile() {
loadJavaFile();
showCodeDock(null);
}
@FXML
......@@ -545,19 +643,25 @@ public class DebuggerMainWindowController implements Initializable {
}
public void stepOver(ActionEvent actionEvent) {
LOGGER.debug("DebuggerMainWindowController.stepOver");
LOGGER.debug("DebuggerMain.stepOver");
PTreeNode newState = proofTreeController.stepOver();
}
public void stepBack(ActionEvent actionEvent) {
LOGGER.debug("DebuggerMainWindowController.stepBack");
LOGGER.debug("DebuggerMain.stepBack");
PTreeNode newState = proofTreeController.stepBack();
}
public KeYProofFacade getFacade() {
return FACADE;
}
//region Property
public boolean isDebugMode() {
return debugMode.get();
}
//endregion
public void setDebugMode(boolean debugMode) {
this.debugMode.set(debugMode);
......@@ -587,6 +691,12 @@ public class DebuggerMainWindowController implements Initializable {
scriptController.newScript();
}
public void showCodeDock(ActionEvent actionEvent) {
if (!javaAreaDock.isDocked()) {
javaAreaDock.dock(dockStation, DockPos.RIGHT);
}
}
public void showWelcomeDock(ActionEvent actionEvent) {
if (!welcomePaneDock.isDocked()) {
welcomePaneDock.dock(dockStation, DockPos.CENTER);
......@@ -600,6 +710,13 @@ public class DebuggerMainWindowController implements Initializable {
}
}
@FXML
public void showProofTree(ActionEvent actionEvent) {
if (!proofTreeDock.isDocked() && !proofTreeDock.isFloating()) {
proofTreeDock.dock(dockStation, DockPos.CENTER);
}
}
public DockNode getJavaAreaDock() {
return javaAreaDock;
}
......@@ -632,6 +749,10 @@ public class DebuggerMainWindowController implements Initializable {
return proofTreeController;
}
public InspectionViewsController getInspectionViewsController() {
return inspectionViewsController;
}
public ExecutorService getExecutorService() {
return executorService;
}
......@@ -656,10 +777,26 @@ public class DebuggerMainWindowController implements Initializable {
return welcomePane;
}
public File getJavaFile() {
return javaFile.get();
}
public void setJavaFile(File javaFile) {
this.javaFile.set(javaFile);
}
public ObjectProperty<File> javaFileProperty() {
return javaFile;
}
public File getKeyFile() {
return keyFile.get();
}
public void setKeyFile(File keyFile) {
this.keyFile.set(keyFile);
}
public ObjectProperty<File> keyFileProperty() {
return keyFile;
}
......@@ -705,16 +842,6 @@ public class DebuggerMainWindowController implements Initializable {
}
});
}
@Override
protected void failed() {
Utils.showExceptionDialog("", "", "", exceptionProperty().get());
}
@Override
protected Task<List<Contract>> createTask() {
return FACADE.getContractsForJavaFileTask(getJavaFile());
}
}
//endregion
......
src/main/java/edu/kit/formal/gui/controller/Events.java → src/main/java/edu/kit/formal/psdb/gui/controller/Events.java
View file @ 7e5e33d0
package edu.kit.formal.gui.controller;
package edu.kit.formal.psdb.gui.controller;
import com.google.common.eventbus.EventBus;
import de.uka.ilkd.key.logic.PosInOccurrence;
import de.uka.ilkd.key.rule.TacletApp;
import edu.kit.formal.gui.controls.ScriptArea;
import edu.kit.formal.proofscriptparser.ast.CallStatement;
import edu.kit.formal.psdb.gui.controls.ScriptArea;
import edu.kit.formal.psdb.parser.ast.CallStatement;
import lombok.Data;
import lombok.RequiredArgsConstructor;
......
src/main/java/edu/kit/formal/gui/controller/PuppetMaster.java → src/main/java/edu/kit/formal/psdb/gui/controller/PuppetMaster.java
View file @ 7e5e33d0
package edu.kit.formal.gui.controller;
import edu.kit.formal.interpreter.HistoryListener;
import edu.kit.formal.interpreter.Interpreter;
import edu.kit.formal.interpreter.data.GoalNode;
import edu.kit.formal.interpreter.data.KeyData;
import edu.kit.formal.interpreter.data.State;
import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
import edu.kit.formal.proofscriptparser.Visitor;
import edu.kit.formal.proofscriptparser.ast.*;
package edu.kit.formal.psdb.gui.controller;
import edu.kit.formal.psdb.interpreter.HistoryListener;
import edu.kit.formal.psdb.interpreter.Interpreter;
import edu.kit.formal.psdb.interpreter.data.GoalNode;
import edu.kit.formal.psdb.interpreter.data.KeyData;
import edu.kit.formal.psdb.interpreter.data.State;
import edu.kit.formal.psdb.parser.DefaultASTVisitor;
import edu.kit.formal.psdb.parser.Visitor;
import edu.kit.formal.psdb.parser.ast.*;
import javafx.application.Platform;
import javafx.beans.property.SimpleObjectProperty;
......
src/main/java/edu/kit/formal/gui/controls/ANTLR4LexerHighlighter.java → src/main/java/edu/kit/formal/psdb/gui/controls/ANTLR4LexerHighlighter.java
View file @ 7e5e33d0
package edu.kit.formal.gui.controls;
package edu.kit.formal.psdb.gui.controls;
import org.antlr.v4.runtime.Lexer;
import org.antlr.v4.runtime.Token;
......
src/main/java/edu/kit/formal/gui/controls/BaseCodeArea.java → src/main/java/edu/kit/formal/psdb/gui/controls/BaseCodeArea.java
View file @ 7e5e33d0
package edu.kit.formal.gui.controls;
package edu.kit.formal.psdb.gui.controls;
import javafx.beans.property.BooleanProperty;
import javafx.beans.property.MapProperty;
......
src/main/java/edu/kit/formal/gui/controls/CustomTabPaneSkin.java → src/main/java/edu/kit/formal/psdb/gui/controls/CustomTabPaneSkin.java
View file @ 7e5e33d0
package edu.kit.formal.gui.controls;
package edu.kit.formal.psdb.gui.controls;
import com.sun.javafx.scene.control.skin.TabPaneSkin;
import javafx.scene.Node;
......
src/main/java/edu/kit/formal/gui/controls/DebuggerStatusBar.java → src/main/java/edu/kit/formal/psdb/gui/controls/DebuggerStatusBar.java
View file @ 7e5e33d0
package edu.kit.formal.gui.controls;
import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
import edu.kit.formal.gui.controller.Events;
import edu.kit.formal.gui.model.MainScriptIdentifier;
import javafx.beans.property.*;
import javafx.beans.value.ObservableStringValue;
import javafx.collections.FXCollections;
import javafx.collections.ObservableList;
import javafx.event.ActionEvent;
package edu.kit.formal.psdb.gui.controls;
import edu.kit.formal.psdb.gui.controller.Events;
import edu.kit.formal.psdb.gui.model.MainScriptIdentifier;
import javafx.beans.property.ObjectProperty;
import javafx.beans.property.SimpleObjectProperty;
import javafx.event.EventHandler;
import javafx.scene.control.*;
import javafx.scene.input.MouseButton;
import javafx.scene.control.Control;
import javafx.scene.control.Label;
import javafx.scene.control.ProgressIndicator;
import javafx.scene.input.MouseEvent;
import javafx.scene.layout.BorderPane;
import javafx.stage.Modality;
import org.apache.logging.log4j.Level;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.apache.logging.log4j.core.Appender;
import org.apache.logging.log4j.core.LogEvent;
import org.apache.logging.log4j.core.appender.AbstractAppender;
import org.apache.logging.log4j.core.layout.PatternLayout;
import org.controlsfx.control.StatusBar;
import java.util.Date;
import java.util.LinkedList;
/**
* Created by weigl on 09.06.2017.
* Created on 09.06.2017
*
* @author Alexander Weigl
*/
public class DebuggerStatusBar extends StatusBar {
private static final Logger LOGGER = LogManager.getLogger(DebuggerStatusBar.class);
private final Appender loggerHandler = createAppender();
private final ContextMenu contextMenu = createContextMenu();
//private final Dialog<Void> loggerDialog = createDialog();
//private final ContextMenu contextMenu = createContextMenu();
//private final Appender loggerHandler = createAppender();
//private LogCatchHandlerFX logCatchHandler = new LogCatchHandlerFX();
private ObjectProperty<MainScriptIdentifier> mainScriptIdentifier = new SimpleObjectProperty<>();
private Label lblCurrentNodes = new Label("#nodes: %s");
private Label lblMainscript = new Label();
private ProgressIndicator progressIndicator = new ProgressIndicator();
private LogCatchHandlerFX logCatchHandler = new LogCatchHandlerFX();
private final Dialog<Void> loggerDialog = createDialog();
private EventHandler<MouseEvent> toolTipHandler = event -> {
publishMessage(((Control) event.getTarget()).getTooltip().getText());
};
public DebuggerStatusBar() {
listenOnField("psdbg");
//listenOnField("psdbg");
getRightItems().addAll(
lblMainscript,
......@@ -53,11 +42,11 @@ public class DebuggerStatusBar extends StatusBar {
progressIndicator
);
setOnMouseClicked(event -> {
/*setOnMouseClicked(event -> {
if (event.getButton() == MouseButton.SECONDARY) {
contextMenu.show(this, event.getScreenX(), event.getScreenY());
}
});
});*/
mainScriptIdentifier.addListener((ov, o, n) -> {
......@@ -84,9 +73,9 @@ public class DebuggerStatusBar extends StatusBar {
Events.fire(new Events.FocusScriptArea(area));
}
});
}
/*