Skip to content

GitLab

Commit 58789c46 authored by Alexander Weigl's avatar Alexander Weigl
Browse files

cleaning up save point 

* consolelogger
* fixes ... change to #save
parent bdab4f23
Pipeline #21799 passed with stages
in 3 minutes and 23 seconds
Hide whitespace changes
Inline Side-by-side
Showing with 354 additions and 218 deletions
build.gradle
View file @ 58789c46
allprojects {
apply plugin: 'maven'
group = 'edu.kit.iti.formal.psdbg'
version = 'Experimental-1.1'
version = '1.1-experimental'
}
subprojects {
......
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/SaveCommand.java
View file @ 58789c46
......@@ -4,26 +4,23 @@ import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
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.VariableAssignment;
import edu.kit.iti.formal.psdbg.interpreter.funchdl.BuiltinCommands;
import edu.kit.iti.formal.psdbg.interpreter.funchdl.CommandHandler;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import edu.kit.iti.formal.psdbg.parser.ast.Parameters;
import edu.kit.iti.formal.psdbg.parser.data.Value;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
import lombok.Setter;
import sun.security.ssl.Debug;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import javax.annotation.Nullable;
import java.io.File;
import java.io.IOException;
import java.sql.Savepoint;
import java.util.ArrayList;
import java.util.List;
public class SaveCommand implements CommandHandler<KeyData>{
public class SaveCommand implements CommandHandler<KeyData> {
private static final String SAVE_COMMAND_NAME = "#save";
private static Logger logger = LogManager.getLogger(SaveCommand.class);
private static Logger consoleLogger = LogManager.getLogger("console");
@Getter @Setter
@Getter
@Setter
private File path;
public SaveCommand(File path) {
......@@ -33,7 +30,7 @@ public class SaveCommand implements CommandHandler<KeyData>{
@Override
public boolean handles(CallStatement call, @Nullable KeyData data) throws IllegalArgumentException {
return call.getCommand().equals("save");
return call.getCommand().equals(SAVE_COMMAND_NAME);
}
@Override
......@@ -41,18 +38,20 @@ public class SaveCommand implements CommandHandler<KeyData>{
//be careful parameters are uninterpreted
SavePoint sp = new SavePoint(call);
//Not via Parentpath -> dependency on OS
String parentpath = path.getAbsolutePath();
parentpath = parentpath.substring(0, parentpath.length() - path.getName().length());
/* String parentPath = path.getAbsolutePath();
parentPath = parentPath.substring(0, parentPath.length() - path.getName().length());*/
File parent = path.getParentFile();
File newFile = sp.getProofFile(parent);
consoleLogger.info("(Safepoint) Location to be saved to = " + newFile.getAbsolutePath());
File newfile = new File(parentpath + sp.getSavepointName() + ".key");
System.out.println("(Safepoint) Location to be saved to = " + newfile.getAbsolutePath());
try {
interpreter.getSelectedNode().getData().getProof().saveToFile(newfile);
interpreter.getSelectedNode().getData().getProof().saveToFile(newFile);
//TODO Call to key persistend facade
} catch (IOException e) {
e.printStackTrace();
}
}
......
rt-key/src/main/resources/log4j2.xml
View file @ 58789c46
<?xml version="1.0" encoding="UTF-8"?>
<!--
https://logging.apache.org/log4j/2.x/manual/configuration.html
-->
<Configuration status="error">
<Appenders>
<Console name="ConsoleErr" target="SYSTEM_ERR">
<PatternLayout pattern="%d{HH:mm:ss.SSS} [%t] %-5level %logger{36} - %msg%n"/>
</Console>
<Console name="Console" target="SYSTEM_OUT">
<PatternLayout pattern="[%-5level] %msg%n"/>
<!--<PatternLayout pattern="%d{HH:mm:ss.SSS} [%t] %-5level %logger{36} - %msg%n"/>-->
<PatternLayout>
<!-- <pattern>%d %highlight{%p} %style{%C{1.} [%t] %m}{bold,green}%n</pattern>-->
<pattern>%r %highlight{%p} %style{[%t] %m}{bold,green} \n\t\tfrom %l%n</pattern>
</PatternLayout>
</Console>
<File name="F" fileName="debug.log" bufferSize="0" bufferedIO="false" append="false">
<PatternLayout pattern="%d{HH:mm:ss.SSS} [%t] %-5level %logger{36} - %msg%n"/>
</File>
</Appenders>
<Loggers>
<Root level="trace">
<AppenderRef ref="Console" level="warn"/>
<AppenderRef ref="ConsoleErr" level="error"/>
<AppenderRef ref="F"/>
</Root>
<Logger name="console">
<AppenderRef ref="Console" level="info"/>
</Logger>
</Loggers>
</Configuration>
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/SavePoint.java
View file @ 58789c46
package edu.kit.iti.formal.psdbg.interpreter.data;
import com.google.errorprone.annotations.Var;
import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
import edu.kit.iti.formal.psdbg.parser.ast.*;
import lombok.AllArgsConstructor;
import lombok.Data;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
import java.io.File;
@Data
@RequiredArgsConstructor
public class SavePoint {
@AllArgsConstructor
public class SavePoint {
private final String name;
private int startOffset = -1;
private int endOffset = -1;
private int lineNumer = -1;
private ForceOption force = ForceOption.YES;
private final String savepointName;
private int start = -1;
private int end = -1;
public SavePoint(CallStatement call){
if(isSaveCommand(call)){
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();
} else {
throw new IllegalArgumentException(call.getCommand()+" is not a save statement");
}}
name = evalAsText(p, "#2", "not-available");
force = ForceOption.valueOf(evalAsText(p, "force", "yes").toUpperCase());
public static boolean isSaveCommand(CallStatement call){
return (call.getCommand().equals("save"));
try {
startOffset = call.getRuleContext().getStart().getStartIndex();
endOffset = call.getRuleContext().getStart().getStopIndex();
lineNumer = call.getRuleContext().getStart().getLine();
} catch (NullPointerException npe) {
}
} else {
throw new IllegalArgumentException(call.getCommand() + " is not a save statement");
}
}
public File getProofFile(File dir){
return new File(dir, savepointName+".proof");
public static boolean isSaveCommand(CallStatement call) {
return (call.getCommand().equals("#save"));
}
public static boolean isSaveCommand(Statement statement) {
try{
try {
CallStatement c = (CallStatement) statement;
return isSaveCommand(c);
}catch (ClassCastException e) {
} catch (ClassCastException e) {
return false;
}
}
public boolean exists(File dir) {
return getProofFile(dir).exists() && getPersistedStateFile(dir).exists();
}
public static String evalAsText(Parameters p, String key, String defaultValue) {
Variable k = new Variable(key);
if (!p.containsKey(k)) {
return defaultValue;
}
return (String) p.get(k).accept(new DefaultASTVisitor<String>() {
@Override
public String defaultVisit(ASTNode node) {
throw new IllegalArgumentException();
}
@Override
public String visit(Variable variable) {
return variable.getIdentifier();
}
@Override
public String visit(StringLiteral stringLiteral) {
return stringLiteral.getText();
}
@Override
public String visit(BooleanLiteral booleanLiteral) {
return Boolean.toString(booleanLiteral.isValue());
}
@Override
public String visit(IntegerLiteral integer) {
return (integer.getValue().toString());
}
});
}
public File getProofFile(File dir) {
return new File(dir, name + ".proof");
}
public File getPersistedStateFile(File dir) {
return new File(dir, name + ".psdbgstate.xml");
}
public boolean isThisStatement(Statement statement) {
if(isSaveCommand(statement)){
if (isSaveCommand(statement)) {
CallStatement c = (CallStatement) statement;
return c.getCommand().equals(savepointName);
return c.getCommand().equals(name);
}
return false;
}
public enum ForceOption {
YES, NO, INTERACTIVE;
}
}
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/ProofScriptDebugger.java
View file @ 58789c46
......@@ -34,6 +34,8 @@ public class ProofScriptDebugger extends Application {
public static final String KEY_VERSION = KeYConstants.VERSION;
private Logger logger = LogManager.getLogger("psdbg");
private static Logger consoleLogger = LogManager.getLogger("console");
public static void main(String[] args) {
launch(args);
......@@ -65,6 +67,8 @@ public class ProofScriptDebugger extends Application {
logger.info("KeY Version: " + KeYConstants.VERSION);
logger.info("KeY Internal: " + KeYConstants.INTERNAL_VERSION);
consoleLogger.info("Welcome!");
} catch (Exception e) {
e.printStackTrace();
System.exit(1);
......
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
View file @ 58789c46
......@@ -33,14 +33,12 @@ 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.interpreter.exceptions.InterpreterRuntimeException;
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.collections.FXCollections;
import javafx.collections.ListChangeListener;
import javafx.collections.ObservableList;
import javafx.concurrent.Service;
import javafx.concurrent.Task;
......@@ -55,7 +53,6 @@ import javafx.scene.web.WebEngine;
import javafx.scene.web.WebView;
import javafx.stage.FileChooser;
import javafx.stage.Modality;
import javafx.util.Callback;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
import org.antlr.v4.runtime.RecognitionException;
......@@ -69,7 +66,6 @@ import org.key_project.util.collection.ImmutableList;
import org.reactfx.util.FxTimer;
import org.reactfx.util.Timer;
import javax.annotation.Nullable;
import javax.swing.*;
import java.io.File;
......@@ -83,6 +79,8 @@ import java.util.*;
import java.util.concurrent.*;
import java.util.stream.Collectors;
import org.reactfx.util.Timer;
/**
* Controller for the Debugger MainWindow
......@@ -105,11 +103,24 @@ public class DebuggerMain implements Initializable {
private final Graph.PTreeGraph graph = graphView.getGraph();
private final DockNode graphViewNode = new DockNode(graphView, "Debug graph");
private InspectionViewsController inspectionViewsController;
private ScriptController scriptController;
private InterpreterBuilder interpreterBuilder;
@FXML
public Menu menuExecuteFromSavepoint;
@FXML
public Menu menuRestartFromSavepoint;
@FXML
SplitMenuButton buttonStartInterpreter;
ScriptController scriptController;
@FXML
ComboBox<SavePoint> cboSavePoints;
@FXML
Button btnSavePointRollback;
private InspectionViewsController inspectionViewsController;
private SavePointController savePointController;
private InterpreterBuilder interpreterBuilder;
@FXML
private DebuggerStatusBar statusBar;
@FXML
......@@ -136,16 +147,8 @@ public class DebuggerMain implements Initializable {
private CheckMenuItem miProofTree;
@FXML
private ToggleButton btnInteractiveMode;
@FXML
private Button interactive_undo;
@FXML
private ComboBox<SavePoint> combo_savepoints;
@FXML
private Button spselect;
//TODO: dir
private File dir;
......@@ -166,25 +169,30 @@ public class DebuggerMain implements Initializable {
private Menu examplesMenu;
private Timer interpreterThreadTimer;
public static void saveProof(File file) throws IOException {
if (FACADE.getProof() != null)
FACADE.getProof().saveToFile(file);
}
@Subscribe
public void handle(Events.ShowPostMortem spm){
public void handle(Events.ShowPostMortem spm) {
FindNearestASTNode fna = new FindNearestASTNode(spm.getPosition());
List<PTreeNode<KeyData>> result =
model.getDebuggerFramework().getPtreeManager().getNodes()
.stream()
.filter(it -> Objects.equals(it.getStatement().accept(fna),it.getStatement()))
.collect(Collectors.toList());
model.getDebuggerFramework().getPtreeManager().getNodes()
.stream()
.filter(it -> Objects.equals(it.getStatement().accept(fna), it.getStatement()))
.collect(Collectors.toList());
System.out.println(result);
for (PTreeNode<KeyData> statePointerToPostMortem : result) {
if(statePointerToPostMortem != null && statePointerToPostMortem.getStateAfterStmt() != null) {
if (statePointerToPostMortem != null && statePointerToPostMortem.getStateAfterStmt() != null) {
State<KeyData> stateBeforeStmt = statePointerToPostMortem.getStateBeforeStmt();
// stateBeforeStmt.getGoals().forEach(keyDataGoalNode -> System.out.println("BeforeSeq = " + keyDataGoalNode.getData().getNode().sequent()));
// stateBeforeStmt.getGoals().forEach(keyDataGoalNode -> System.out.println("BeforeSeq = " + keyDataGoalNode.getData().getNode().sequent()));
State<KeyData> stateAfterStmt = statePointerToPostMortem.getStateAfterStmt();
// stateAfterStmt.getGoals().forEach(keyDataGoalNode -> System.out.println("AfterSeq = " + keyDataGoalNode.getData().getNode().sequent()));
// stateAfterStmt.getGoals().forEach(keyDataGoalNode -> System.out.println("AfterSeq = " + keyDataGoalNode.getData().getNode().sequent()));
/*List<GoalNode<KeyData>> list = stateAfterStmt.getGoals().stream().filter(keyDataGoalNode ->
keyDataGoalNode.getData().getNode().parent().equals(stateBeforeStmt.getSelectedGoalNode().getData().getNode())
......@@ -196,7 +204,7 @@ public class DebuggerMain implements Initializable {
ObservableList<GoalNode<KeyData>> goals = FXCollections.observableArrayList(stateAfterStmt.getGoals());
im.setGoals(goals);
if(stateAfterStmt.getSelectedGoalNode() != null){
if (stateAfterStmt.getSelectedGoalNode() != null) {
im.setSelectedGoalNodeToShow(stateAfterStmt.getSelectedGoalNode());
} else {
im.setSelectedGoalNodeToShow(goals.get(0));
......@@ -252,7 +260,7 @@ public class DebuggerMain implements Initializable {
private void init() {
Events.register(this);
// model.setDebugMode(false);
// model.setDebugMode(false);
scriptController = new ScriptController(dockStation);
//TODO:
interactiveModeController = new InteractiveModeController(scriptController);
......@@ -373,49 +381,7 @@ public class DebuggerMain implements Initializable {
statusBar.interpreterStatusModelProperty().bind(model.interpreterStateProperty());
renewThreadStateTimer();
//TODO: nach draußen verlagern
combo_savepoints.setCellFactory(new Callback<ListView<SavePoint>, ListCell<SavePoint>>() {
@Override
public ListCell<SavePoint> call(ListView<SavePoint> param) {
return new ListCell<SavePoint>(){
@Override
protected void updateItem(SavePoint item, boolean empty) {
super.updateItem(item, empty);
if (item == null || empty) {
setGraphic(null);
} else {
setText(item.getSavepointName());
}
}
};
}
});
//update Combobox on changed Savepoints
scriptController.getMainScriptSavePoints().addListener(new ListChangeListener<SavePoint>() {
@Override
public void onChanged(Change<? extends SavePoint> c) {
if(scriptController.getMainScriptSavePoints().size() > 0){
combo_savepoints.setItems(scriptController.getMainScriptSavePoints());
spselect.setDisable(false);
combo_savepoints.setDisable(false);
} else {
spselect.setDisable(true);
combo_savepoints.setDisable(true);
}
}
});
savePointController = new SavePointController(this);
}
/**
......@@ -498,7 +464,6 @@ public class DebuggerMain implements Initializable {
interactiveModeController.undo(e);
}
public KeYProofFacade getFacade() {
return FACADE;
}
......@@ -687,17 +652,14 @@ public class DebuggerMain implements Initializable {
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) {
}
private void executeScriptFromSavePoint(InterpreterBuilder ib, SavePoint point) {
try {
Set<Breakpoint> breakpoints = scriptController.getBreakpoints();
// get possible scripts and the main script!
......@@ -715,10 +677,12 @@ public class DebuggerMain implements Initializable {
}
Statements body = new Statements();
boolean flag =false;
boolean flag = false;
for (int i = 0; i < ms.getBody().size(); i++) {
if(flag) {body.add(ms.getBody().get(i));
continue;}
if (flag) {
body.add(ms.getBody().get(i));
continue;
}
flag = point.isThisStatement(ms.getBody().get(i));
}
......@@ -733,24 +697,23 @@ public class DebuggerMain implements Initializable {
LOGGER.error(e);
Utils.showExceptionDialog("Antlr Exception", "", "Could not parse scripts.", e);
}
}
private void executeScript0(InterpreterBuilder ib,
Collection<? extends Breakpoint> breakpoints,
ProofScript ms, boolean addInitBreakpoint) {
KeyInterpreter interpreter = ib.build();
DebuggerFramework<KeyData> df = new DebuggerFramework<>(interpreter, ms, null);
df.setSucceedListener(this::onInterpreterSucceed);
df.setErrorListener(this::onInterpreterError);
if (addInitBreakpoint) {
df.releaseUntil(new Blocker.CounterBlocker(1)); // just execute
}
private void executeScript0(InterpreterBuilder ib,
Collection<? extends Breakpoint> breakpoints,
ProofScript ms, boolean addInitBreakpoint) {
KeyInterpreter interpreter = ib.build();
DebuggerFramework<KeyData> df = new DebuggerFramework<>(interpreter, ms, null);
df.setSucceedListener(this::onInterpreterSucceed);
df.setErrorListener(this::onInterpreterError);
if (addInitBreakpoint) {
df.releaseUntil(new Blocker.CounterBlocker(1)); // just execute
}
df.getBreakpoints().addAll(breakpoints);
df.getStatePointerListener().add(this::handleStatePointer);
df.start();
model.setDebuggerFramework(df);
df.getBreakpoints().addAll(breakpoints);
df.getStatePointerListener().add(this::handleStatePointer);
df.start();
model.setDebuggerFramework(df);
}
private void onInterpreterSucceed(DebuggerFramework<KeyData> keyDataDebuggerFramework) {
......@@ -775,7 +738,6 @@ public class DebuggerMain implements Initializable {
});
}
@FXML
......@@ -1035,17 +997,17 @@ public class DebuggerMain implements Initializable {
assert model.getDebuggerFramework() == null;
}
@FXML
public void closeProgram() {
System.exit(0);
}
/* public void openJavaFile() {
loadJavaFile();
showCodeDock(null);
}
*/
@FXML
public void closeProgram() {
System.exit(0);
}
@FXML
public void openScript() {
File scriptFile = openFileChooserOpenDialog("Select Script File",
......@@ -1089,6 +1051,7 @@ public class DebuggerMain implements Initializable {
saveScript(f);
}
}
//endregion
/**
* Creates a filechooser dialog
......@@ -1105,7 +1068,6 @@ public class DebuggerMain implements Initializable {
if (file != null) model.setInitialDirectory