diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTDiff.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTDiff.java index 178d1b1b8d53081a58806da5ff6ab38c06f68d72..e85e8c21c5737b45066fd6d30b7a5c721e25a50c 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTDiff.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTDiff.java @@ -93,6 +93,7 @@ public class ASTDiff extends DefaultASTVisitor { return null; } + @Override public ASTNode visit(TheOnlyStatement theOnly) { return null; diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Statements.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Statements.java index 5b61d691c471b32d2c7ae083b01b18e213c952d6..bf37d58566702512835a3afc8e16e9373f4f7399 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Statements.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Statements.java @@ -26,6 +26,7 @@ package edu.kit.iti.formal.psdbg.parser.ast; import edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser; import edu.kit.iti.formal.psdbg.parser.Visitable; import edu.kit.iti.formal.psdbg.parser.Visitor; +import lombok.NoArgsConstructor; import lombok.ToString; import java.util.*; @@ -39,10 +40,16 @@ import java.util.stream.Stream; * @version 1 (27.04.17) */ @ToString +@NoArgsConstructor public class Statements extends ASTNode implements Visitable, Iterable { private final List statements = new ArrayList<>(); + + public Statements(Statements body) { + statements.addAll(body.statements); + } + public Iterator iterator() { return statements.iterator(); } diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/SavePoint.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/SavePoint.java new file mode 100644 index 0000000000000000000000000000000000000000..fc8fe6da0526c4e7dad74b146e9ee4d422666301 --- /dev/null +++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/SavePoint.java @@ -0,0 +1,55 @@ +package edu.kit.iti.formal.psdbg.interpreter.data; + +import edu.kit.iti.formal.psdbg.parser.ast.*; +import lombok.Data; +import lombok.Getter; +import lombok.RequiredArgsConstructor; + +import java.io.File; + +@Data +@RequiredArgsConstructor +public class SavePoint { + + private final String savepointName; + + private int start = -1; + + private int end = -1; + + public SavePoint(CallStatement call){ + if(isSaveCommand(call)){ + Parameters p = call.getParameters(); + savepointName = ((StringLiteral) p.get(new Variable("#2"))).getText(); + start = call.getRuleContext().getStart().getStartIndex(); + end = call.getRuleContext().getStart().getStopIndex(); + } + throw new IllegalArgumentException(call.getCommand()+" is not a save statement"); + } + + public static boolean isSaveCommand(CallStatement call){ + return (call.getCommand().equals("save")); + } + + public File getProofFile(File dir){ + return new File(dir, savepointName+".proof"); + } + + public static boolean isSaveCommand(Statement statement) { + try{ + CallStatement c = (CallStatement) statement; + return isSaveCommand(c); + }catch (ClassCastException e) { + return false; + } + } + + public boolean isThisStatement(Statement statement) { + if(isSaveCommand(statement)){ + CallStatement c = (CallStatement) statement; + return c.getCommand().equals(savepointName); + + } + return false; + } +} diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java index 3d8ade79d9e686d73651ef5d128066a2f9c4f773..c2ffe721de98960d29a7d0fc5d4f38b3078bab84 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java @@ -30,14 +30,14 @@ import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade; 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.data.SavePoint; import edu.kit.iti.formal.psdbg.interpreter.data.State; import edu.kit.iti.formal.psdbg.interpreter.dbg.*; import edu.kit.iti.formal.psdbg.parser.ast.ProofScript; +import edu.kit.iti.formal.psdbg.parser.ast.Statements; import javafx.application.Platform; import javafx.beans.InvalidationListener; import javafx.beans.binding.BooleanBinding; -import javafx.beans.property.BooleanProperty; -import javafx.beans.property.SimpleBooleanProperty; import javafx.collections.FXCollections; import javafx.collections.ObservableList; import javafx.concurrent.Service; @@ -602,6 +602,7 @@ public class DebuggerMain implements Initializable { */ private void executeScript(InterpreterBuilder ib, boolean addInitBreakpoint) { try { + Set breakpoints = scriptController.getBreakpoints(); // get possible scripts and the main script! List scripts = scriptController.getCombinedAST(); @@ -621,6 +622,59 @@ public class DebuggerMain implements Initializable { LOGGER.debug("MainScript: {}", ms.getName()); ib.setScripts(scripts); + executeScript0(ib, breakpoints, ms, addInitBreakpoint); + } catch (RecognitionException e) { + LOGGER.error(e); + Utils.showExceptionDialog("Antlr Exception", "", "Could not parse scripts.", e); + } + + } + + + + private void executeScriptFromSavePoint(InterpreterBuilder ib, SavePoint point) { + try { + Set breakpoints = scriptController.getBreakpoints(); + // get possible scripts and the main script! + List scripts = scriptController.getCombinedAST(); + if (scriptController.getMainScript() == null) { + scriptController.setMainScript(scripts.get(0)); + } + Optional mainScript = scriptController.getMainScript().find(scripts); + ProofScript ms; + if (!mainScript.isPresent()) { + scriptController.setMainScript(scripts.get(0)); + ms = scripts.get(0); + } else { + ms = mainScript.get(); + } + + Statements body = new Statements(); + boolean flag =false; + for (int i = 0; i < ms.getBody().size(); i++) { + if(flag) {body.add(ms.getBody().get(i)); + continue;} + flag = point.isThisStatement(ms.getBody().get(i)); + } + + ms.setBody(body); + + LOGGER.debug("Parsed Scripts, found {}", scripts.size()); + LOGGER.debug("MainScript: {}", ms.getName()); + //ib.setDirectory(model.getKeyFile() != null ? model.getKeyFile() : model.getJavaFile()); + ib.setScripts(scripts); + executeScript0(ib, breakpoints, ms, false); + } catch (RecognitionException e) { + LOGGER.error(e); + Utils.showExceptionDialog("Antlr Exception", "", "Could not parse scripts.", e); + } + + } + + + private void executeScript0(InterpreterBuilder ib, + Collection breakpoints, + ProofScript ms, boolean addInitBreakpoint) { KeyInterpreter interpreter = ib.build(); DebuggerFramework df = new DebuggerFramework<>(interpreter, ms, null); df.setSucceedListener(this::onInterpreterSucceed); @@ -631,12 +685,7 @@ public class DebuggerMain implements Initializable { df.getBreakpoints().addAll(breakpoints); df.getStatePointerListener().add(this::handleStatePointer); df.start(); - model.setDebuggerFramework(df); - } catch (RecognitionException e) { - LOGGER.error(e); - Utils.showExceptionDialog("Antlr Exception", "", "Could not parse scripts.", e); - } } private void onInterpreterSucceed(DebuggerFramework keyDataDebuggerFramework) { @@ -1007,7 +1056,7 @@ public class DebuggerMain implements Initializable { */ public void saveProof(ActionEvent actionEvent) { FileChooser fc = new FileChooser(); - File file = fc.showOpenDialog(btnInteractiveMode.getScene().getWindow()); + File file = fc.showSaveDialog(btnInteractiveMode.getScene().getWindow()); if (file != null) { try { saveProof(file); diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java index 3c007926ea1bc585ff6e4251e992312050c483d2..7b9ff13a64ec084e037b0db46c4bd7149c02dcbd 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java @@ -11,15 +11,20 @@ import edu.kit.iti.formal.psdbg.gui.actions.inline.InlineActionSupplier; import edu.kit.iti.formal.psdbg.gui.controller.Events; import edu.kit.iti.formal.psdbg.gui.model.MainScriptIdentifier; import edu.kit.iti.formal.psdbg.gui.actions.acomplete.Suggestion; +import edu.kit.iti.formal.psdbg.interpreter.data.SavePoint; import edu.kit.iti.formal.psdbg.interpreter.dbg.Breakpoint; import edu.kit.iti.formal.psdbg.parser.Facade; import edu.kit.iti.formal.psdbg.parser.ast.ASTNode; +import edu.kit.iti.formal.psdbg.parser.ast.CallStatement; import edu.kit.iti.formal.psdbg.parser.ast.ProofScript; +import edu.kit.iti.formal.psdbg.parser.ast.Statement; import javafx.beans.property.ObjectProperty; +import javafx.beans.property.SimpleListProperty; import javafx.beans.property.SimpleObjectProperty; import javafx.beans.value.ChangeListener; import javafx.beans.value.ObservableValue; import javafx.collections.FXCollections; +import javafx.collections.ObservableList; import javafx.collections.ObservableMap; import lombok.Getter; import lombok.Setter; @@ -64,10 +69,37 @@ public class ScriptController { @Setter private DefaultAutoCompletionController autoCompleter = new DefaultAutoCompletionController(); + + public ScriptController(DockPane parent) { this.parent = parent; Events.register(this); addDefaultInlineActions(); + + mainScript.addListener((p,o,n)-> { + if(o!=null) + o.getScriptArea().textProperty().removeListener( a-> updateSavePoints()); + n.getScriptArea().textProperty().addListener(a->updateSavePoints()); + updateSavePoints(); + }); + + + } + + private ObservableList mainScriptSavePoints + = new SimpleListProperty<>(FXCollections.observableArrayList()); + + private void updateSavePoints() { + Optional ms = getMainScript().find(getCombinedAST()); + if(ms.isPresent()) { + List list = ms.get().getBody().stream() + .filter(SavePoint::isSaveCommand) + .map(a -> (CallStatement) a) + .map(SavePoint::new) + .collect(Collectors.toList()); + + mainScriptSavePoints.setAll(list); + } } private void addDefaultInlineActions() { @@ -361,5 +393,11 @@ public class ScriptController { } } + public ObservableList getMainScriptSavePoints() { + return mainScriptSavePoints; + } + public void setMainScriptSavePoints(ObservableList mainScriptSavePoints) { + this.mainScriptSavePoints = mainScriptSavePoints; + } } \ No newline at end of file diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/Utils.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/Utils.java index b81038c0bdd6af8b172fd11691aa002b89d29e82..cbe1d3afc048f7172b5da2053ddfaf453ddc4c8f 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/Utils.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/Utils.java @@ -253,34 +253,14 @@ public class Utils { public static void showClosedProofDialog(String scriptName) { Alert alert = new Alert(Alert.AlertType.INFORMATION); + alert.setTitle("Proof Closed"); alert.setHeaderText("The proof is closed"); alert.setContentText("The proof using " + scriptName + " is closed"); alert.setWidth(500); alert.setHeight(400); alert.setResizable(true); - /*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); - textArea.setMaxWidth(Double.MAX_VALUE); - textArea.setMaxHeight(Double.MAX_VALUE); - GridPane.setVgrow(textArea, Priority.ALWAYS); - GridPane.setHgrow(textArea, Priority.ALWAYS); - - GridPane expContent = new GridPane(); - expContent.setMaxWidth(Double.MAX_VALUE); - expContent.addCell(label, 0, 0); - expContent.addCell(textArea, 0, 1); - - alert.getDialogPane().setExpandableContent(expContent); - */ alert.showAndWait(); }