Skip to content

GitLab

Commit bc6fe5ad authored by LULUDBR\Lulu's avatar LULUDBR\Lulu
Browse files

recognizing and saving of Savepoints + updating combobox 

missing: saving of Proofs in SaveCommand -> need access from SaveCommand to DebuggerMain
parent a2b1fa2f
Pipeline #21571 passed with stages
in 6 minutes and 6 seconds
Hide whitespace changes
Inline Side-by-side
Showing with 178 additions and 7 deletions
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/InterpreterBuilder.java
View file @ bc6fe5ad
......@@ -44,6 +44,8 @@ public class InterpreterBuilder {
@Getter
private ProofScriptCommandBuilder pmc = new ProofScriptCommandBuilder();
@Getter
private BuiltInCommandHandler bich = new BuiltInCommandHandler();
@Getter
private ProofScript entryPoint;
@Getter
private Proof proof;
......@@ -54,7 +56,7 @@ public class InterpreterBuilder {
@Getter
private ScopeLogger logger;
@Getter
private DefaultLookup lookup = new DefaultLookup(psh, pmh, pmc, pmr);
private DefaultLookup lookup = new DefaultLookup(psh, pmh, pmc, pmr, bich);
@Getter
private KeyAssignmentHook keyHooks = new KeyAssignmentHook();
......
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/BuiltInCommandHandler.java 0 → 100644
View file @ bc6fe5ad
package edu.kit.iti.formal.psdbg.interpreter.funchdl;
import edu.kit.iti.formal.psdbg.SaveCommand;
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.parser.ast.CallStatement;
import lombok.Getter;
import javax.annotation.Nullable;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
public class BuiltInCommandHandler implements CommandHandler<KeyData> {
@Getter
private final Map<String, BuiltinCommands.BuiltinCommand> builtins;
@Getter
private final SaveCommand sc = new SaveCommand();
public BuiltInCommandHandler() {
builtins = new HashMap<>();
builtins.put("save", sc);
}
@Override
public boolean handles(CallStatement call, @Nullable KeyData data) throws IllegalArgumentException {
// handler only knows SaveCommand for now
return builtins.containsKey(call.getCommand());
}
@Override
public void evaluate(Interpreter<KeyData> interpreter, CallStatement call, VariableAssignment params, KeyData data) {
if(SavePoint.isSaveCommand(call)) {
//TODO: interpreter ist ast visitor, so not needed?
sc.evaluate(null,call,params,null);
}
}
}
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/SaveCommand.java → rt/src/main/java/edu/kit/iti/formal/psdbg/SaveCommand.java
View file @ bc6fe5ad
package edu.kit.iti.formal.psdbg.interpreter.funchdl;
package edu.kit.iti.formal.psdbg;
import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
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.parser.ast.CallStatement;
import edu.kit.iti.formal.psdbg.parser.ast.Parameters;
import edu.kit.iti.formal.psdbg.parser.ast.Variable;
import edu.kit.iti.formal.psdbg.parser.data.Value;
import lombok.Getter;
import sun.security.ssl.Debug;
import java.io.File;
import java.math.BigInteger;
import java.nio.file.Path;
import java.io.IOException;
import java.sql.Savepoint;
import java.util.ArrayList;
import java.util.List;
public class SaveCommand extends BuiltinCommands.BuiltinCommand<String>{
public SaveCommand() {
public class SaveCommand extends BuiltinCommands.BuiltinCommand<String> {
@Getter
private final List<SavePoint> splist;
public SaveCommand() {
super("save");
splist = new ArrayList<>();
}
@Override
public void evaluate(Interpreter<String> interpreter, CallStatement call, VariableAssignment params, String data) {
//TODO: another param entry with id for the savepoint
SavePoint sp = new SavePoint(call);
Value<Path> val = (Value<Path>) params.getValues().getOrDefault(
new Variable("filepath"),
Value.from(2));
// check if Savepoint already in list
boolean inlist = false;
if (splist.size() != 0) {
for (int i = 0; i < splist.size(); i++) {
if (splist.get(i).getSavepointName().equals(sp.getSavepointName())) {
inlist = true;
File savepoint = new File(val.toString());
}
//TODO: force replace?!
splist.add(i, sp);
}
}
}
private class Parameters extends edu.kit.iti.formal.psdbg.parser.ast.Parameters{
if(!inlist) {
splist.add(sp);
}
}
}
}
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/SavePoint.java
View file @ bc6fe5ad
......@@ -23,9 +23,9 @@ public class SavePoint {
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");
}
}}
public static boolean isSaveCommand(CallStatement call){
return (call.getCommand().equals("save"));
......
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
View file @ bc6fe5ad
......@@ -15,6 +15,7 @@ import de.uka.ilkd.key.proof.SingleProof;
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.SaveCommand;
import edu.kit.iti.formal.psdbg.ShortCommandPrinter;
import edu.kit.iti.formal.psdbg.examples.Examples;
import edu.kit.iti.formal.psdbg.fmt.DefaultFormatter;
......@@ -53,6 +54,7 @@ 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;
......@@ -66,8 +68,10 @@ 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.awt.event.ActionListener;
import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
......@@ -104,6 +108,9 @@ public class DebuggerMain implements Initializable {
private final DockNode graphViewNode = new DockNode(graphView, "Debug graph");
private InspectionViewsController inspectionViewsController;
private ScriptController scriptController;
private InterpreterBuilder interpreterBuilder;
@FXML
private DebuggerStatusBar statusBar;
@FXML
......@@ -135,8 +142,12 @@ public class DebuggerMain implements Initializable {
private Button interactive_undo;
@FXML
private ComboBox<Path> combo_savepoints;
private ComboBox<SavePoint> combo_savepoints;
@FXML
private Button spselect;
//TODO: dir
private File dir;
private JavaArea javaArea = new JavaArea();
private DockNode javaAreaDock = new DockNode(javaArea, "Java Source",
......@@ -529,7 +540,8 @@ public class DebuggerMain implements Initializable {
}
// else getProofState() == VIRGIN!
executeScript(FACADE.buildInterpreter(), addInitBreakpoint);
interpreterBuilder = FACADE.buildInterpreter();
executeScript(interpreterBuilder, addInitBreakpoint);
}
/**
......@@ -628,6 +640,9 @@ public class DebuggerMain implements Initializable {
ib.setScripts(scripts);
executeScript0(ib, breakpoints, ms, addInitBreakpoint);
} catch (RecognitionException e) {
LOGGER.error(e);
Utils.showExceptionDialog("Antlr Exception", "", "Could not parse scripts.", e);
......@@ -713,6 +728,40 @@ public class DebuggerMain implements Initializable {
}
});
//SavePoints
//get savepoints
ObservableList<SavePoint> splist = FXCollections.observableArrayList(interpreterBuilder.getBich().getSc().getSplist());
if(splist.size() > 0) {
combo_savepoints.setDisable(false);
combo_savepoints.setItems(splist);
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());
}
}
};
}
});
spselect.setDisable(false);
} else {
combo_savepoints.setDisable(true);
spselect.setDisable(true);
}
}
@FXML
......@@ -1071,7 +1120,7 @@ public class DebuggerMain implements Initializable {
}
}
public void saveProof(File file) throws IOException {
public static void saveProof(File file) throws IOException {
if (FACADE.getProof() != null)
FACADE.getProof().saveToFile(file);
}
......@@ -1236,6 +1285,12 @@ public class DebuggerMain implements Initializable {
@FXML
public void selectSavepoint(ActionEvent actionEvent) {
if (combo_savepoints.getItems().size() > 0) {
SavePoint selected = combo_savepoints.getValue();
System.out.println("Clicked on Savepoint:" + selected);
openKeyFile(selected.getProofFile(dir));
executeScriptFromSavePoint(interpreterBuilder, selected);
}
}
......
ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml
View file @ bc6fe5ad
......@@ -326,7 +326,14 @@
<ComboBox fx:id="combo_savepoints" disable="true" prefWidth="100" prefHeight="30">
</ComboBox>
<Button fx:id="spselect" onAction="#selectSavepoint" disable="true">
<graphic>
<MaterialDesignIconView glyphName="CHECK" size="22.0"/>
</graphic>
<tooltip>
<Tooltip text="Select Savepoint"/>
</tooltip>
</Button>
<Pane HBox.hgrow="ALWAYS"/>
<Label text="Windows:"/>
<ToggleButton fx:id="togBtnCodeDock" onAction="#showCodeDock">
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment