Commit afb7ec68 authored by Sarah Grebing's avatar Sarah Grebing

Merge remote-tracking branch 'origin/grebing_luong_workbranch' into grebing_luong_workbranch

parents 67adb6bb 47be55f7
......@@ -13,17 +13,17 @@ import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof;
import edu.kit.iti.formal.psdbg.interpreter.data.TermValue;
import javafx.scene.Scene;
import javafx.stage.Stage;
import lombok.RequiredArgsConstructor;
import lombok.Value;
import java.io.StringReader;
import java.lang.annotation.Retention;
import java.lang.reflect.Field;
import java.lang.reflect.Method;
import java.math.BigInteger;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.*;
/**
* @author Alexander Weigl
......@@ -86,8 +86,8 @@ public class ValueInjector {
vi.addConverter(Long.TYPE, Long::parseLong);
vi.addConverter(Double.TYPE, Double::parseDouble);
vi.addConverter(Float.TYPE, Float::parseFloat);
vi.addConverter(BigInteger.class,Integer.class, (BigInteger b) -> b.intValue());
vi.addConverter(BigInteger.class,Integer.TYPE, (BigInteger b) -> b.intValue());
vi.addConverter(BigInteger.class, Integer.class, (BigInteger b) -> b.intValue());
vi.addConverter(BigInteger.class, Integer.TYPE, (BigInteger b) -> b.intValue());
return vi;
}
......@@ -111,7 +111,7 @@ public class ValueInjector {
return s.getTerm();
} else {
NamespaceSet nss = null;
if(s.getNs() !=null) {
if (s.getNs() != null) {
nss = s.getNs();
}
......@@ -149,7 +149,7 @@ public class ValueInjector {
ns = node.proof().getNamespaces();
}
if(additionalNamespace!=null) {
if (additionalNamespace != null) {
ns = ns.copy();
ns.add(additionalNamespace);
}
......@@ -160,7 +160,8 @@ public class ValueInjector {
}
}
@Value public static class SortConverter implements Converter<String, Sort>{
@Value
public static class SortConverter implements Converter<String, Sort> {
private Proof proof;
@Override
......@@ -241,12 +242,43 @@ public class ValueInjector {
final Object val = args.get(meta.getName());
if (val == null) {
if (meta.isRequired()) {
throw new ArgumentRequiredException(
String.format("Argument %s:%s is required, but %s was given. " +
"For comamnd class: '%s'",
meta.getName(), meta.getField().getType(), val,
meta.getCommand().getClass()), meta);
//TODO MissingInstWindow:
String userinput = "p -> q";
DefaultTermParser dtp = new DefaultTermParser();
TermConverter tc = (TermConverter) getConverter(String.class, Term.class);
Term t;
try {
t = tc.convert(userinput);
} catch (ParserException pe) {
System.out.println("edu/kit/iti/formal/psdbg/ValueInjector.java:250 ParserException");
throw new ArgumentRequiredException(
String.format("Argument %s:%s is required, but %s was given. " +
"For comamnd class: '%s'",
meta.getName(), meta.getField().getType(), val,
meta.getCommand().getClass()), meta);
}
//TODO: inject t into meta?
meta.setRequired(false);
args.put("#2", t);
Object valnew = args.get(meta.getName());
Object value = convert(meta, valnew);
try {
//if (meta.getType() != value.getClass())
// throw new ConversionException("The typed returned '" + val.getClass()
// + "' from the converter mismtached with the
// type of the field " + meta.getType(), meta);
meta.getField().set(obj, value);
} catch (IllegalAccessException e) {
throw new InjectionReflectionException("Could not inject values via reflection",
e, meta);
}
}
} else {
Object value = convert(meta, val);
try {
......@@ -255,6 +287,7 @@ public class ValueInjector {
// + "' from the converter mismtached with the
// type of the field " + meta.getType(), meta);
meta.getField().set(obj, value);
} catch (IllegalAccessException e) {
throw new InjectionReflectionException("Could not inject values via reflection",
e, meta);
......@@ -282,24 +315,24 @@ public class ValueInjector {
/**
* Registers the given converter for the specified class.
*
* @param conv a converter for the given class
* @param <T> an arbitrary type
* @param conv a converter for the given class
* @param <T> an arbitrary type
*/
public <T,R> void addConverter(Class<T> from, Class<R> to, Converter<T,R> conv) {
converters.add(new ConverterWrapper<T,R>(from, to, conv));
public <T, R> void addConverter(Class<T> from, Class<R> to, Converter<T, R> conv) {
converters.add(new ConverterWrapper<T, R>(from, to, conv));
}
public <R> void addConverter(Class<R> to, Converter<String,R> conv) {
public <R> void addConverter(Class<R> to, Converter<String, R> conv) {
addConverter(String.class, to, conv);
}
public <T,R> void addConverter(Converter<T,R> conv) {
public <T, R> void addConverter(Converter<T, R> conv) {
Method[] ms = conv.getClass().getMethods();
for (Method m : ms) {
if (m.getParameterCount() == 1) {
Class<T> t = (Class<T>) m.getParameterTypes()[0];
Class<R> c = (Class<R>) m.getReturnType();
addConverter(t,c, conv);
addConverter(t, c, conv);
}
}
......@@ -307,26 +340,27 @@ public class ValueInjector {
/**
* Finds a converter for the given class.
*
* @return null or a suitable converter (registered) converter for the requested class.
*/
@SuppressWarnings("unchecked")
public <T,R> Converter<T,R> getConverter(Class<T> from, Class<R> to) {
for (ConverterWrapper c: converters) {
if(c.getFrom().equals(from) && c.getTo().equals(to))
return c.getConverter();
}
public <T, R> Converter<T, R> getConverter(Class<T> from, Class<R> to) {
for (ConverterWrapper c : converters) {
if (c.getFrom().equals(from) && c.getTo().equals(to))
return c.getConverter();
}
throw new RuntimeException("Could not find a suitable converter for types " + from + " to " + to);
}
@Value
private static class ConverterWrapper<T,R> {
private static class ConverterWrapper<T, R> {
Class<T> from;
Class<R> to;
Converter<T,R> converter;
Converter<T, R> converter;
}
interface Converter<T, R> {
interface Converter<T, R> {
R convert(T o) throws Exception;
}
}
......@@ -2,6 +2,7 @@ package edu.kit.iti.formal.psdbg.interpreter.funchdl;
import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
import de.uka.ilkd.key.control.instantiation_model.TacletInstantiationModel;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.PosInOccurrence;
import de.uka.ilkd.key.logic.PosInTerm;
......@@ -12,6 +13,7 @@ import de.uka.ilkd.key.macros.scripts.ScriptException;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.proof.RuleAppIndex;
import de.uka.ilkd.key.proof.SVInstantiationException;
import de.uka.ilkd.key.proof.rulefilter.TacletFilter;
import de.uka.ilkd.key.rule.Rule;
import de.uka.ilkd.key.rule.Taclet;
......@@ -26,17 +28,30 @@ import edu.kit.iti.formal.psdbg.interpreter.exceptions.ScriptCommandNotApplicabl
import edu.kit.iti.formal.psdbg.interpreter.exceptions.VariableNotDeclaredException;
import edu.kit.iti.formal.psdbg.interpreter.exceptions.VariableNotDefinedException;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import edu.kit.iti.formal.psdbg.parser.ast.Statement;
import edu.kit.iti.formal.psdbg.parser.ast.Variable;
import javafx.collections.FXCollections;
import javafx.event.ActionEvent;
import javafx.event.EventHandler;
import javafx.geometry.Pos;
import javafx.scene.Scene;
import javafx.scene.control.Button;
import javafx.scene.control.ListView;
import javafx.scene.control.TextField;
import javafx.scene.layout.VBox;
import javafx.stage.Modality;
import javafx.stage.Stage;
import javafx.stage.StageStyle;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.key_project.util.collection.ImmutableList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;
import java.io.IOException;
import java.util.*;
import java.util.concurrent.ConcurrentMap;
import java.util.concurrent.TimeUnit;
/**
* @author Alexander Weigl
......@@ -52,6 +67,8 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
@Getter
private final Map<String, Rule> rules;
private Scanner scanner = new Scanner(System.in);
public RuleCommandHandler() {
this(new HashMap<>());
}
......@@ -77,7 +94,7 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
try {
for (SequentFormula sf : g.node().sequent().succedent()) {
ImmutableList<TacletApp> apps = index.getTacletAppAtAndBelow(filter,
new PosInOccurrence(sf, PosInTerm.getTopLevel(), false),
new PosInOccurrence(sf, PosInTerm.getTopLevel(), true),
services);
apps.forEach(t -> set.add(t.taclet().name().toString()));
}
......@@ -120,16 +137,20 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
params.asMap().forEach((k, v) -> map.put(k.getIdentifier(), v.getData()));
LOGGER.info("Execute {} with {}", call, map);
RuleCommand.Parameters cc;
try {
map.put("#2", call.getCommand());
EngineState estate = new EngineState(kd.getProof());
estate.setGoal(kd.getNode());
RuleCommand.Parameters cc = new RuleCommand.Parameters();
cc = new RuleCommand.Parameters();
ValueInjector valueInjector = ValueInjector.createDefault(kd.getNode());
cc = valueInjector.inject(c, cc, map);
AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl();
c.execute(uiControl, cc, estate);
//TODO auslagern / finally
ImmutableList<Goal> ngoals = kd.getProof().getSubtreeGoals(kd.getNode());
state.getGoals().remove(expandedNode);
if (state.getSelectedGoalNode().equals(expandedNode)) {
......@@ -141,36 +162,52 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
}
} catch (ScriptException e) {
//TODO: adding UserinteractionWindow
/*TODO: possible cases not applicable, because
command not recognized (can be ignored)
boolean exceptionsolved = false;
command multiple matches -> need more specification with on + formula
if(e.getMessage().equals("More than one applicable occurrence")) {
//TODO: open UserinteractionWindow with selectionbox , need (RuleCommand: 121)
if (e instanceof ScriptException.IndistinctFormula) {
List<TacletApp> matchingapps = ((ScriptException.IndistinctFormula) e).getMatchingApps();
ImmutableList<TacletApp> allApps = c.findAllTacletApps(cc, state);
List<TacletApp> matchingApps = c.filterList(cc, allApps);
//IndistinctPrompt prompt = new IndistinctPrompt(matchingapps);
//TacletApp chosen = prompt.getChosen();
//TODO: (re)apply completed TacletApp
int inputindex = -1;
//TODO: insert into script
while (true) {
System.out.println("Taclet " + matchingapps.get(0).taclet().displayName() + " is applicable on multiple formulas, " +
"please choose one of the following by entering a number from 0 to " + (matchingapps.size() - 1) + " :");
matchingapps.forEach(k -> System.out.println(k));
System.out.flush();
// User input
try {
inputindex = System.in.read();
} catch (IOException ioe) {
System.out.println("No valid input");
continue;
}
if (0 <= inputindex && inputindex <= matchingapps.size() - 1) {
System.out.println("Acceptable inputindex = " + inputindex);
break;
} else {
System.out.println("No valid input");
}
}
TacletApp chosenApp = matchingapps.get(inputindex);
TacletInstantiationModel tim = new TacletInstantiationModel(chosenApp, data.getGoal().sequent(), data.getGoal().getLocalNamespaces(), null, data.getGoal());
try {
TacletApp newTA = tim.createTacletApp();
newTA.execute(data.getGoal(), data.getProof().getServices());
command not complete -> missig parameters
solution:
if(e.getMessage().equals("Not a unique \\assumes instantiation")) {
//TODO: open UserinteractionWindow with selectionbox , need (RuleCommand: 56)
ImmutableList<TacletApp> assumesCandidates = theApp.findIfFormulaInstantiations(state.getFirstOpenGoal().sequent(), proof.getServices());
int linenr = call.getStartPosition().getLineNumber();
exceptionsolved = true;
} catch (SVInstantiationException svie) {
//TODO: (re)apply completed TacletApp
}
}
if (exceptionsolved) return;
//TODO: insert into script
}
*/
if (interpreter.isStrictMode()) {
throw new ScriptCommandNotApplicableException(e, c, map);
} else {
......@@ -196,4 +233,66 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
return params;
}
private class IndistinctPrompt {
private final TacletApp chosen = null;
IndistinctPrompt(List<TacletApp> matchingapps) {
final Stage dialog = new Stage();
dialog.setTitle("Select a Tacletapp");
dialog.initStyle(StageStyle.UTILITY);
dialog.initModality(Modality.WINDOW_MODAL);
ListView listView = new ListView(FXCollections.observableArrayList(matchingapps));
final TextField textField = new TextField();
final Button submitButton = new Button("Submit");
submitButton.setDefaultButton(true);
submitButton.setOnAction(new EventHandler<ActionEvent>() {
@Override
public void handle(ActionEvent t) {
String userinput = textField.getText();
if (userinput.equals("")) {
System.out.println("Invalid input!");
return;
}
int index;
try {
index = Integer.parseInt(userinput);
} catch (NumberFormatException e) {
System.out.println("Invalid input!");
return;
}
if (0 < index && index < matchingapps.size()) {
final TacletApp chosen = matchingapps.get(index);
dialog.close();
} else {
System.out.println("Invalid input!");
return;
}
}
});
final VBox layout = new VBox(10);
layout.setAlignment(Pos.CENTER_RIGHT);
layout.setStyle("-fx-background-color: azure; -fx-padding: 10;");
layout.getChildren().setAll(
listView,
textField,
submitButton
);
dialog.setScene(new Scene(layout));
dialog.showAndWait();
}
private TacletApp getChosen() {
return chosen;
}
}
}
......@@ -41,6 +41,7 @@ dependencies {
def mainClassName = 'edu.kit.iti.formal.psdbg.gui.ProofScriptDebugger'
task runApp(type: JavaExec) {
standardInput = System.in
jvmArgs << '-Dsun.awt.disablegrab=true' << '-Dglass.disableGrab=true'
/*applicationDefaultJvmArgs = [
// For accessing VirtualFlow field from the base class in GridViewSkin
......@@ -72,4 +73,4 @@ task customFatJar(type: Jar) {
from { configurations.compile.collect { it.isDirectory() ? it : zipTree(it) } }
with jar
}
customFatJar.dependsOn jar
\ No newline at end of file
customFatJar.dependsOn jar
package edu.kit.iti.formal.psdbg.examples.impLeft;
import edu.kit.iti.formal.psdbg.examples.Example;
public class ImpLeftExample extends Example {
public ImpLeftExample() {
setName("ImpLeft");
defaultInit(getClass());
}
}
......@@ -151,6 +151,8 @@ public class DebuggerMain implements Initializable {
@FXML
private CheckMenuItem miScriptTree;
@FXML
private CheckMenuItem miViewSettings;
@FXML
private ToggleButton btnInteractiveMode;
@FXML
......@@ -177,6 +179,8 @@ public class DebuggerMain implements Initializable {
private InteractiveModeController interactiveModeController;
private ScriptExecutionController scriptExecutionController;
private ViewSettings viewSettings;
@FXML
private Menu examplesMenu;
private Timer interpreterThreadTimer;
......@@ -411,6 +415,8 @@ public class DebuggerMain implements Initializable {
savePointController = new SavePointController(this);
viewSettings = new ViewSettings(this);
}
/**
......@@ -1377,6 +1383,16 @@ public class DebuggerMain implements Initializable {
stage.show();
}
@FXML
public void showViewSettings(ActionEvent actionEvent) {
Stage stage = new Stage();
stage.setTitle("View Settings");
Scene scene = (viewSettings.getScene() == null) ? new Scene(viewSettings) : viewSettings.getScene();
stage.setScene(scene);
stage.show();
}
public DockNode getJavaAreaDock() {
return javaAreaDock;
}
......
......@@ -4,10 +4,7 @@ import de.uka.ilkd.key.proof.Node;
import edu.kit.iti.formal.psdbg.gui.controls.TreeNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
import edu.kit.iti.formal.psdbg.parser.ast.GuardedCaseStatement;
import edu.kit.iti.formal.psdbg.parser.ast.MatchExpression;
import edu.kit.iti.formal.psdbg.parser.ast.TermLiteral;
import edu.kit.iti.formal.psdbg.parser.ast.*;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
import lombok.Setter;
......@@ -42,8 +39,20 @@ public class ScriptTreeNode extends AbstractTreeNode {
String label;
if (isMatchEx()) {
String matchexpression = (scriptState.getStatement() instanceof GuardedCaseStatement)?((TermLiteral) ((MatchExpression) ((GuardedCaseStatement) scriptState.getStatement()).getGuard()).getPattern()).getContent()
: "default";
String matchexpression = "";
if (scriptState.getStatement() instanceof GuardedCaseStatement) {
MatchExpression me = (MatchExpression) ((GuardedCaseStatement) scriptState.getStatement()).getGuard();
try {
matchexpression = ((TermLiteral) me.getPattern()).getContent();
} catch (ClassCastException cce) {
//not a Termliteral but a Stringliteral
matchexpression = ((StringLiteral) me.getPattern()).getText();
}
} else { //default case statement
matchexpression = "default";
}
label = "match ("+ matchexpression +") in line " + linenr;
} else {
label = ((CallStatement)scriptState.getStatement()).getCommand() + " (line " + linenr + ")";
......
package edu.kit.iti.formal.psdbg.gui.controls;
import alice.tuprolog.Var;
import edu.kit.iti.formal.psdbg.gui.controls.Utils;
import edu.kit.iti.formal.psdbg.gui.model.InspectionModel;
import edu.kit.iti.formal.psdbg.interpreter.assignhook.DefaultAssignmentHook;
import de.uka.ilkd.key.macros.scripts.ScriptException;
import edu.kit.iti.formal.psdbg.interpreter.Evaluator;
import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.interpreter.matcher.KeyMatcherFacade;
import edu.kit.iti.formal.psdbg.parser.ast.Variable;
import edu.kit.iti.formal.psdbg.parser.NotWelldefinedException;
import edu.kit.iti.formal.psdbg.parser.Visitor;
import edu.kit.iti.formal.psdbg.parser.ast.Expression;
import edu.kit.iti.formal.psdbg.parser.ast.Signature;
import edu.kit.iti.formal.psdbg.parser.ast.StringLiteral;
import edu.kit.iti.formal.psdbg.parser.data.Value;
import edu.kit.iti.formal.psdbg.parser.types.Type;
import javafx.beans.Observable;
import javafx.beans.property.SimpleStringProperty;
import javafx.collections.FXCollections;
import javafx.collections.ObservableList;
import javafx.fxml.FXML;
......@@ -17,11 +17,9 @@ import javafx.scene.control.*;
import javafx.scene.control.cell.PropertyValueFactory;
import javafx.scene.layout.BorderPane;
import lombok.Getter;
import lombok.Setter;
import javax.script.ScriptEngine;
import javax.script.ScriptEngineManager;
import javax.script.ScriptException;
import java.util.*;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
......@@ -33,6 +31,9 @@ public class VariableAssignmentWindow extends BorderPane {
@FXML
TableView special_tableView;
@FXML
TableView history;
@FXML
TextArea match_variables;
......@@ -44,14 +45,16 @@ public class VariableAssignmentWindow extends BorderPane {
/** Variables that start with __ **/
private ObservableList<VariableModel> specialModel;
private String numeric_matchexp;
private String var; //var in numeric_matchexp
private String matchexp;
private ScriptEngineManager mgr = new ScriptEngineManager();
private ScriptEngine engine = mgr.getEngineByName("JavaScript");
private List<VariableModel> matchlist_declarative = new ArrayList<>();
private List<VariableModel> matchlist_special = new ArrayList<>();
private List<VariableModel> historylist = new ArrayList<>();
private Evaluator evaluator;
public VariableAssignmentWindow(VariableAssignment assignment) {
......@@ -133,6 +136,8 @@ public class VariableAssignmentWindow extends BorderPane {
}
}
});
evaluator = new Evaluator(assignment, null);
}
/**
......@@ -172,19 +177,22 @@ public class VariableAssignmentWindow extends BorderPane {
*/
private void startMatch() {
clearHighlights();
numeric_matchexp = match_variables.getText();
if (numeric_matchexp.equals("")) return;
var = getVariable(numeric_matchexp);
if (var.equals("")) {
Utils.showInfoDialog("Variable not found", "Explicit variable not found",
"Please declare exactly one variable starting with \"?\". ");
return;
}
matchexp = match_variables.getText();
if (matchexp.equals("")) return;
Value value = evaluator.visit(new StringLiteral(matchexp));
new StringLiteral(matchexp).accept(evaluator);
System.out.println("Value of Evaluator: " + value);
System.out.println("Visit " + new StringLiteral(matchexp).accept(evaluator));
System.out.println("Eval: " + evaluator.eval(new StringLiteral(matchexp)));
/*
matchlist_declarative = getVariableMatches(declarativeModel);
matchlist_special = getVariableMatches(specialModel);
*/
highlight(matchlist_declarative);
highlight(matchlist_special);
......@@ -194,6 +202,20 @@ public class VariableAssignmentWindow extends BorderPane {
if (matchlist_special != null) System.out.println("matchlist_special = " + matchlist_special.size());
}
@FXML
private void evaluate() {
matchexp = match_variables.getText();
if (matchexp.equals("")) return;
Value value = evaluator.visit(new StringLiteral(matchexp));
new StringLiteral(matchexp).accept(evaluator);
System.out.println("Value of Evaluator: " + value);
System.out.println("Visit " + new StringLiteral(matchexp).accept(evaluator));
System.out.println("Eval: " + evaluator.eval(new StringLiteral(matchexp)));
}
/**
* Highlight all varlist items in the view
*
......@@ -243,12 +265,16 @@ public class VariableAssignmentWindow extends BorderPane {
/**
* Calculate matching results of matchexpression with given list
*
* @param varlist
* @param
* @return list of matching VariableModels
*
*/
/*
private List<VariableModel> getVariableMatches(ObservableList<VariableModel> varlist) {
//Contains numbers
if (!Pattern.compile("[0-9]+").matcher(numeric_matchexp).find()) return null;
if (!Pattern.compile("[0-9]+").matcher(matchexp).find()) return null;
List<VariableModel> matchlist = new ArrayList<>();
......@@ -256,7 +282,7 @@ public class VariableAssignmentWindow extends BorderPane {
String new_var = "\\" + var;
for (VariableModel vm : varlist) {
String boolexpression = numeric_matchexp.replaceAll(new_var, vm.getVarval());
String boolexpression = matchexp.replaceAll(new_var, vm.getVarval());
try {
if (vm.getVartype().equals("int")) {