Skip to content

GitLab

Commit 7c503d34 authored by LULUDBR\Lulu's avatar LULUDBR\Lulu
Browse files

Savepoints loadable in Contraposition

parent bc6fe5ad
Pipeline #21658 failed with stages
in 1 minute and 40 seconds
Hide whitespace changes
Inline Side-by-side
Showing with 142 additions and 117 deletions
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/InterpreterBuilder.java
View file @ 7c503d34
......@@ -23,10 +23,7 @@ import org.key_project.util.collection.ImmutableList;
import java.io.File;
import java.io.IOException;
import java.util.Arrays;
import java.util.Collection;
import java.util.List;
import java.util.Set;
import java.util.*;
import java.util.stream.Collectors;
/**
......@@ -63,6 +60,8 @@ public class InterpreterBuilder {
private KeyInterpreter interpreter = new KeyInterpreter(lookup);
@Getter
private InterpreterOptionsHook<KeyData> optionsHook = new InterpreterOptionsHook<>(interpreter);
......@@ -204,18 +203,32 @@ public class InterpreterBuilder {
if (proof == null || keyEnvironment == null)
throw new IllegalStateException("Call proof(..) before startState");
ImmutableList<Goal> openGoals = proof.getSubtreeGoals(proof.root());
List<GoalNode<KeyData>> goals = openGoals.stream().map(g ->
new GoalNode<>(null, new KeyData(g, keyEnvironment, proof), false))
.collect(Collectors.toList());
interpreter.newState(goals);
return this;
}
private InterpreterBuilder startState(GoalNode<KeyData> startGoal) {
interpreter.newState(startGoal);
return this;
}
public InterpreterBuilder setProblemPath(File path){
Map<String, CommandHandler<KeyData>> builtinsnew = this.bich.getBuiltins();
builtinsnew.put("save", new SaveCommand(path));
this.bich.setBuiltins(builtinsnew);
return this;
}
}
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYProofFacade.java
View file @ 7c503d34
......@@ -16,6 +16,7 @@ import javafx.beans.binding.BooleanBinding;
import javafx.beans.property.SimpleBooleanProperty;
import javafx.beans.property.SimpleObjectProperty;
import javafx.concurrent.Task;
import jdk.nashorn.internal.objects.annotations.Getter;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.key_project.util.collection.ImmutableList;
......@@ -70,6 +71,8 @@ public class KeYProofFacade {
//Workaround until api is relaxed
private ProofManagementApi pma;
private File filepath;
/**
*
*/
......@@ -131,6 +134,7 @@ public class KeYProofFacade {
ProofManagementApi pma = KeYApi.loadFromKeyFile(keYFile);
ProofApi pa = pma.getLoadedProof();
setLoading(false);
filepath = keYFile;
return pa;
}
......@@ -141,6 +145,7 @@ public class KeYProofFacade {
proof.set(pa.getProof());
contract.set(null);
setLoading(false);
filepath = keyFile;
return pa;
}
......@@ -249,6 +254,13 @@ public class KeYProofFacade {
return readyToExecute;
}
/**
returns filepath of loaded KeY problem
**/
public File getFilepath() {
return filepath;
}
public Collection<GoalNode<KeyData>> getPseudoGoals() {
Proof p = getProof();
KeYEnvironment env = getEnvironment();
......
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/BuiltInCommandHandler.java
View file @ 7c503d34
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 lombok.Setter;
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 @Setter
private Map<String, CommandHandler<KeyData>> builtins;
@Getter
private final SaveCommand sc = new SaveCommand();
@Getter @Setter
private SaveCommand sc;
public BuiltInCommandHandler() {
builtins = new HashMap<>();
......@@ -37,14 +35,6 @@ public class BuiltInCommandHandler implements CommandHandler<KeyData> {
@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);
}
builtins.get(call.getCommand()).evaluate(interpreter,call,params, data);
}
}
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/RuleCommandHandler.java
View file @ 7c503d34
......@@ -85,11 +85,16 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
@Override
public boolean handles(CallStatement call, KeyData data) throws IllegalArgumentException {
if (rules.containsKey(call.getCommand())) return true;//static/rigid rules
try{
if (data != null) {
Goal goal = data.getGoal();
Set<String> rules = findTaclets(data.getProof(), goal);
return rules.contains(call.getCommand());
}
} catch (NullPointerException npe) {
System.out.println("npe = " + npe);
return false;
}
return false;
}
......
rt/src/main/java/edu/kit/iti/formal/psdbg/SaveCommand.java deleted 100644 → 0
View file @ bc6fe5ad
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 lombok.Getter;
import sun.security.ssl.Debug;
import java.io.File;
import java.io.IOException;
import java.sql.Savepoint;
import java.util.ArrayList;
import java.util.List;
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) {
SavePoint sp = new SavePoint(call);
// 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;
//TODO: force replace?!
splist.add(i, sp);
}
}
}
if(!inlist) {
splist.add(sp);
}
}
}
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
View file @ 7c503d34
......@@ -15,7 +15,6 @@ 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;
......@@ -34,12 +33,14 @@ 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;
......@@ -71,14 +72,12 @@ 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;
import java.io.PrintWriter;
import java.net.URL;
import java.nio.charset.Charset;
import java.nio.file.Path;
import java.time.Duration;
import java.util.*;
import java.util.concurrent.*;
......@@ -143,6 +142,7 @@ public class DebuggerMain implements Initializable {
@FXML
private ComboBox<SavePoint> combo_savepoints;
@FXML
private Button spselect;
......@@ -372,6 +372,51 @@ 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);
}
}
});
}
/**
......@@ -539,8 +584,8 @@ public class DebuggerMain implements Initializable {
}
}
// else getProofState() == VIRGIN!
interpreterBuilder = FACADE.buildInterpreter();
interpreterBuilder.setProblemPath(FACADE.getFilepath());
executeScript(interpreterBuilder, addInitBreakpoint);
}
......@@ -639,6 +684,7 @@ public class DebuggerMain implements Initializable {
LOGGER.debug("MainScript: {}", ms.getName());
ib.setScripts(scripts);
System.out.println("ms = " + FACADE.getProof().getProofFile());
executeScript0(ib, breakpoints, ms, addInitBreakpoint);
......@@ -729,38 +775,7 @@ 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);
}
}
......@@ -1285,11 +1300,49 @@ public class DebuggerMain implements Initializable {
@FXML
public void selectSavepoint(ActionEvent actionEvent) {
if (combo_savepoints.getItems().size() > 0) {
if (combo_savepoints.getValue() != null) {
stopDebugMode(actionEvent);
SavePoint selected = combo_savepoints.getValue();
System.out.println("Clicked on Savepoint:" + selected);
openKeyFile(selected.getProofFile(dir));
executeScriptFromSavePoint(interpreterBuilder, selected);
try {
abortExecution();
} catch (Exception e) {
e.printStackTrace();
}
/**
* reload with selected savepoint
*/
Platform.runLater(() -> model.setStatePointer(null));
handleStatePointerUI(null);
//reload getInspectionViewsController().getActiveInspectionViewTab().getModel()
InspectionModel iModel = getInspectionViewsController().getActiveInspectionViewTab().getModel();
//iModel.setHighlightedJavaLines(FXCollections.emptyObservableSet());
iModel.clearHighlightLines();
iModel.getGoals().clear();
iModel.setSelectedGoalNodeToShow(null);
try {
String parentpath = FACADE.getFilepath().getAbsolutePath();
parentpath = parentpath.substring(0, parentpath.length() - FACADE.getFilepath().getName().length());
File loadfile = new File(parentpath + selected.getSavepointName() + ".key");
System.out.println("loadfile = " + loadfile);
FACADE.reload(loadfile);
if (iModel.getGoals().size() > 0) {
iModel.setSelectedGoalNodeToShow(iModel.getGoals().get(0));
}
if (FACADE.getReadyToExecute()) {
LOGGER.info("Reloaded Successfully");
statusBar.publishMessage("Reloaded Sucessfully");
}
} catch (ProofInputException | ProblemLoaderException e) {
LOGGER.error(e);
Utils.showExceptionDialog("Loading Error", "Could not clear Environment", "There was an error when clearing old environment",
e
);
}
// executeScriptFromSavePoint(interpreterBuilder, selected);
}
}
......
ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps
View file @ 7c503d34
script test123() {
impRight;
save 'test0';
impRight;
save 'test1';
impLeft;
//save 'test2';
}
script autoScript(){
__STRICT_MODE := true;
auto;
......
ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml
View file @ 7c503d34
......@@ -323,7 +323,7 @@
<Tooltip text="Undo"/>
</tooltip>
</Button>
<ComboBox fx:id="combo_savepoints" disable="true" prefWidth="100" prefHeight="30">
<ComboBox fx:id="combo_savepoints" disable="true" prefWidth="100" prefHeight="30">
</ComboBox>
<Button fx:id="spselect" onAction="#selectSavepoint" disable="true">
......
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