Skip to content

GitLab

P
ProofScriptParser
Commit cc20826f authored by Sarah Grebing's avatar Sarah Grebing
Browse files
Options

Interim state: some minor modifications at DebuggerMain and first part of... 

Interim state: some minor modifications at DebuggerMain and first part of semiseq matching, next part follows tomorrow
parent 750d02fb
Pipeline #12953 failed with stage
    in 1 minute and 41 seconds
    Hide whitespace changes
    Inline Side-by-side
    Showing with 360 additions and 208 deletions
    src/main/antlr4/edu/kit/formal/psdb/termmatcher/MatchPattern.g4
    View file @ cc20826f
    ......@@ -14,7 +14,8 @@ f(..., ...?X...)
    f(..., ... g(x) ...)
    f(_, x, _, y, ... y ...)
    */
    semiSeqPattern : termPattern (',' termPattern)*;
    sequentPattern : antec=semiSeqPattern? ARROW succ=semiSeqPattern?;
    termPattern :
    DONTCARE #dontCare
    //| STARDONTCARE #starDontCare
    ......@@ -25,8 +26,7 @@ termPattern :
    /*
    f(x), f(x,y,g(y)), X, ?Y, _, ..., f(... ?X ...), f(..., ?X), f(..., ...?X...), f(..., ... g(x) ...), f(_, x, _, y, ... y ...)
    */
    semiSeqPattern : termPattern (',' termPattern)*;
    sequentPattern : antec=semiSeqPattern? ARROW succ=semiSeqPattern?;
    ARROW : '⇒' | '==>';
    DONTCARE: '?' | '_' | '█';
    ......
    src/main/java/edu/kit/formal/psdb/gui/controller/ContractChooser.java
    View file @ cc20826f
    ......@@ -30,6 +30,12 @@ public class ContractChooser extends Dialog<Contract> {
    private final ListView<Contract> listOfContractsView = new ListView<>();
    private final Services services;
    public ContractChooser(Services services,
    SimpleListProperty<Contract> contracts) {
    this(services);
    listOfContractsView.itemsProperty().bind(contracts);
    }
    public ContractChooser(Services services) {
    super();
    this.services = services;
    ......@@ -59,12 +65,6 @@ public class ContractChooser extends Dialog<Contract> {
    listOfContractsView.setOnKeyPressed(event -> okButton.fire());
    }
    public ContractChooser(Services services,
    SimpleListProperty<Contract> contracts) {
    this(services);
    listOfContractsView.itemsProperty().bind(contracts);
    }
    public ContractChooser(Services service, List<Contract> contracts) {
    this(service);
    listOfContractsView.itemsProperty().get().setAll(contracts);
    ......@@ -97,7 +97,10 @@ public class ContractChooser extends Dialog<Contract> {
    private void render() {
    if (getItem() != null) {
    webView.getEngine().loadContent(getItem().getHTMLText(services));
    String content = beautifyContractHTML(getItem().getHTMLText(services), getItem().getTarget().toString());
    webView.getEngine().loadContent(content);
    //webView.getEngine().loadContent(getItem().getHTMLText(services));
    //int val = (int) webView.getEngine().executeScript("document.height");
    webView.setPrefHeight(150);
    webView.setDisable(true);
    ......@@ -107,5 +110,9 @@ public class ContractChooser extends Dialog<Contract> {
    }
    }
    }
    private String beautifyContractHTML(String html, String name) {
    return "Contract for <b>" + name + "</b><br>" + html;
    }
    }
    }
    src/main/java/edu/kit/formal/psdb/gui/controller/DebuggerMain.java
    View file @ cc20826f
    ......@@ -155,17 +155,6 @@ public class DebuggerMain implements Initializable {
    }
    private void initializeExamples() {
    examplesMenu.getItems().clear();
    Examples.loadExamples().forEach(example -> {
    MenuItem item = new MenuItem(example.getName());
    item.setOnAction(event -> {
    example.open(this);
    });
    examplesMenu.getItems().add(item);
    });
    }
    /**
    * If the mouse moves other toolbar button, the help text should display in the status bar
    */
    ......@@ -203,8 +192,16 @@ public class DebuggerMain implements Initializable {
    proofTreeController.currentHighlightNodeProperty().addListener((observable, oldValue, newValue) -> {
    scriptController.getDebugPositionHighlighter().highlight(newValue);
    });
    /*proofTreeController.currentExecutionEndProperty().addListener((observable, oldValue, newValue) -> {
    scriptController.getMainScript().getScriptArea().removeExecutionMarker();
    LineMapping lm = new LineMapping(scriptController.getMainScript().getScriptArea().getText());
    int i = lm.getLineEnd(newValue.getEndPosition().getLineNumber() - 1);
    scriptController.getMainScript().getScriptArea().insertExecutionMarker(i);
    });*/
    Utils.addDebugListener(proofTreeController.currentGoalsProperty(), Utils::reprKeyDataList);
    Utils.addDebugListener(proofTreeController.currentSelectedGoalProperty(), Utils::reprKeyData);
    Utils.addDebugListener(proofTreeController.currentHighlightNodeProperty());
    ......@@ -264,6 +261,17 @@ public class DebuggerMain implements Initializable {
    return inspectionViewsController;
    }
    private void initializeExamples() {
    examplesMenu.getItems().clear();
    Examples.loadExamples().forEach(example -> {
    MenuItem item = new MenuItem(example.getName());
    item.setOnAction(event -> {
    example.open(this);
    });
    examplesMenu.getItems().add(item);
    });
    }
    public void showCodeDock(ActionEvent actionEvent) {
    if (!javaAreaDock.isDocked()) {
    javaAreaDock.dock(dockStation, DockPos.RIGHT);
    ......@@ -285,29 +293,16 @@ public class DebuggerMain implements Initializable {
    }
    */
    //region Actions: Execution
    @FXML
    public void executeToBreakpoint() {
    }
    //region Actions: Menu
    /* @FXML
    public void closeProgram() {
    System.exit(0);
    }*/
    /* @FXML
    public void openScript() {
    File scriptFile = openFileChooserOpenDialog("Select Script File",
    "Proof Script File", "kps");
    if (scriptFile != null) {
    openScript(scriptFile);
    }
    }*/
    /**
    * When play button is used
    */
    @FXML
    public void executeScript() {
    executorHelper();
    }
    private void executorHelper() {
    if (proofTreeController.isAlreadyExecuted()) {
    File file;
    boolean isKeyfile = false;
    ......@@ -318,6 +313,7 @@ public class DebuggerMain implements Initializable {
    file = getKeyFile();
    }
    Task<Void> reloading = reloadEnvironment(file, isKeyfile);
    reloading.setOnSucceeded(event -> {
    statusBar.publishMessage("Cleared and Reloaded Environment");
    ......@@ -338,8 +334,29 @@ public class DebuggerMain implements Initializable {
    executeScript(FACADE.buildInterpreter(), false);
    }
    }
    public File getJavaFile() {
    return javaFile.get();
    }
    //region Actions: Menu
    /* @FXML
    public void closeProgram() {
    System.exit(0);
    }*/
    /* @FXML
    public void openScript() {
    File scriptFile = openFileChooserOpenDialog("Select Script File",
    "Proof Script File", "kps");
    if (scriptFile != null) {
    openScript(scriptFile);
    }
    }*/
    /* private void saveScript(File scriptFile) {
    try {
    scriptController.saveCurrentScriptAs(scriptFile);
    ......@@ -371,10 +388,6 @@ public class DebuggerMain implements Initializable {
    }
    }*/
    public File getJavaFile() {
    return javaFile.get();
    }
    public void setJavaFile(File javaFile) {
    this.javaFile.set(javaFile);
    }
    ......@@ -419,6 +432,7 @@ public class DebuggerMain implements Initializable {
    */
    private void executeScript(InterpreterBuilder ib, boolean debugMode) {
    Set<Breakpoint> breakpoints = scriptController.getBreakpoints();
    if (proofTreeController.isAlreadyExecuted()) {
    proofTreeController.saveGraphs();
    }
    ......@@ -442,12 +456,6 @@ public class DebuggerMain implements Initializable {
    }
    }
    /* @FXML
    protected void loadKeYFile() {
    File keyFile = openFileChooserOpenDialog("Select KeY File", "KeY Files", "key", "kps");
    openKeyFile(keyFile);
    }
    */
    public void openKeyFile(File keyFile) {
    if (keyFile != null) {
    setKeyFile(keyFile);
    ......@@ -456,7 +464,6 @@ public class DebuggerMain implements Initializable {
    task.setOnSucceeded(event -> {
    statusBar.publishMessage("Loaded key sourceName: %s", keyFile);
    statusBar.stopProgress();
    // getInspectionViewsController().getActiveInspectionViewTab().getModel().getGoals().setAll(FACADE.getPseudoGoals());
    });
    task.setOnFailed(event -> {
    ......@@ -473,11 +480,6 @@ public class DebuggerMain implements Initializable {
    }
    }
    //endregion
    //region Santa's Little Helper
    public void openJavaFile(File javaFile) {
    if (javaFile != null) {
    setJavaFile(javaFile);
    ......@@ -486,6 +488,32 @@ public class DebuggerMain implements Initializable {
    }
    }
    /* @FXML
    protected void loadKeYFile() {
    File keyFile = openFileChooserOpenDialog("Select KeY File", "KeY Files", "key", "kps");
    openKeyFile(keyFile);
    }
    */
    @FXML
    public void executeToBreakpoint() {
    Set<Breakpoint> breakpoints = scriptController.getBreakpoints();
    if (breakpoints.size() == 0) {
    //we need to add breakpoint at end if no breakpoint exists
    }
    executorHelper();
    }
    //endregion
    //region Santa's Little Helper
    @FXML
    public void executeInDebugMode() {
    executeScript(FACADE.buildInterpreter(), true);
    }
    @FXML
    public void saveScript() {
    try {
    ......@@ -501,17 +529,6 @@ public class DebuggerMain implements Initializable {
    showCodeDock(null);
    }
    /**
    * Save KeY proof as proof file
    *
    * @param
    */
    /* public void saveProof(ActionEvent actionEvent) {
    LOGGER.error("saveProof not implemented!!!");
    }*/
    //endregion
    //region Santa's Little Helper
    ......@@ -554,29 +571,7 @@ public class DebuggerMain implements Initializable {
    }
    //deprecated
    @FXML
    public void executeScriptFromCursor() {
    InterpreterBuilder ib = FACADE.buildInterpreter();
    //b.inheritState(interpreterService.interpreterProperty().get());
    // Get State before cursor
    // use goalnode to build new interpreter in proof tree controller.
    //
    //LineMapping lm = new LineMapping(scriptArea.getText());
    //int line = lm.getLine(scriptArea.getCaretPosition());
    //int inLine = lm.getCharInLine(scriptArea.getCaretPosition());
    //ib.ignoreLinesUntil(scriptController.getSelectedScriptArea().getCaretPosition());
    //executeScript(ib, true);
    }
    @FXML
    public void executeInDebugMode() {
    executeScript(FACADE.buildInterpreter(), true);
    }
    //endregion
    //region Actions: Menu
    ......@@ -883,3 +878,19 @@ public class DebuggerMain implements Initializable {
    //endregion
    }
    //deprecated
    /* @FXML
    public void executeScriptFromCursor() {
    InterpreterBuilder ib = FACADE.buildInterpreter();
    //b.inheritState(interpreterService.interpreterProperty().get());
    // Get State before cursor
    // use goalnode to build new interpreter in proof tree controller.
    //
    //LineMapping lm = new LineMapping(scriptArea.getText());
    //int line = lm.getLine(scriptArea.getCaretPosition());
    //int inLine = lm.getCharInLine(scriptArea.getCaretPosition());
    //ib.ignoreLinesUntil(scriptController.getSelectedScriptArea().getCaretPosition());
    //executeScript(ib, true);
    }*/
    src/main/java/edu/kit/formal/psdb/gui/controller/Events.java
    View file @ cc20826f
    ......@@ -4,6 +4,7 @@ import com.google.common.eventbus.EventBus;
    import de.uka.ilkd.key.logic.PosInOccurrence;
    import de.uka.ilkd.key.rule.TacletApp;
    import edu.kit.formal.psdb.gui.controls.ScriptArea;
    import edu.kit.formal.psdb.parser.ast.ASTNode;
    import edu.kit.formal.psdb.parser.ast.CallStatement;
    import lombok.Data;
    import lombok.RequiredArgsConstructor;
    ......@@ -48,4 +49,13 @@ public class Events {
    private final int line;
    private final CallStatement cs;
    }
    @Data
    @RequiredArgsConstructor
    /**
    * A new AST node of existing script was executed
    */
    public static class NewNodeExecuted {
    private final ASTNode correspondingASTNode;
    }
    }
    src/main/java/edu/kit/formal/psdb/gui/controls/ScriptArea.java
    View file @ cc20826f
    ......@@ -7,11 +7,11 @@ import de.uka.ilkd.key.logic.SequentFormula;
    import edu.kit.formal.psdb.gui.controller.Events;
    import edu.kit.formal.psdb.gui.model.Breakpoint;
    import edu.kit.formal.psdb.gui.model.MainScriptIdentifier;
    import edu.kit.formal.psdb.lint.LintProblem;
    import edu.kit.formal.psdb.lint.LinterStrategy;
    import edu.kit.formal.psdb.parser.Facade;
    import edu.kit.formal.psdb.parser.ScriptLanguageLexer;
    import edu.kit.formal.psdb.parser.ast.*;
    import edu.kit.formal.psdb.lint.LintProblem;
    import edu.kit.formal.psdb.lint.LinterStrategy;
    import javafx.beans.InvalidationListener;
    import javafx.beans.Observable;
    import javafx.beans.binding.BooleanBinding;
    ......@@ -389,15 +389,19 @@ public class ScriptArea extends CodeArea {
    return getText().replace("" + EXECUTION_MARKER, "");
    }
    /**
    * Insert Execution marker at absolute character position
    *
    * @param pos
    */
    public void insertExecutionMarker(int pos) {
    LOGGER.debug("ScriptArea.insertExecutionMarker");
    Events.register(this);
    String text = getText();
    setText(text.substring(0, pos) + EXECUTION_MARKER + text.substring(pos));
    }
    @Subscribe
    public void handle(Events.TacletApplicationEvent tap) {
    LOGGER.debug("ScriptArea.handleTacletApplication");
    ......@@ -430,6 +434,7 @@ public class ScriptArea extends CodeArea {
    }
    private static class GutterView extends HBox {
    private final SimpleObjectProperty<GutterAnnotation> annotation = new SimpleObjectProperty<>();
    ......
    src/main/java/edu/kit/formal/psdb/gui/controls/ScriptController.java
    View file @ cc20826f
    ......@@ -55,6 +55,37 @@ public class ScriptController {
    fsa.getScriptArea().requestFocus();
    }
    @Subscribe
    public void handle(Events.NewNodeExecuted newNode) {
    logger.debug("Handling new node added event!");
    ASTNode scriptNode = newNode.getCorrespondingASTNode();
    ScriptArea editor = findEditor(scriptNode);
    editor.removeExecutionMarker();
    LineMapping lm = new LineMapping(editor.getText());
    int pos = lm.getLineEnd(scriptNode.getStartPosition().getLineNumber() - 1);
    editor.insertExecutionMarker(pos);
    }
    private ScriptArea findEditor(ASTNode node) {
    File f = new File(node.getRuleContext().getStart().getInputStream().getSourceName());
    return findEditor(f);
    }
    /**
    * Find the scriptarea for the requested file
    *
    * @param filePath
    * @return
    */
    public ScriptArea findEditor(File filePath) {
    return openScripts.keySet().stream()
    .filter(scriptArea ->
    scriptArea.getFilePath().equals(filePath)
    )
    .findAny()
    .orElse(null);
    }
    public ObservableMap<ScriptArea, DockNode> getOpenScripts() {
    return openScripts;
    }
    ......@@ -153,38 +184,6 @@ public class ScriptController {
    return breakpoints;
    }
    /**
    * Find the scriptarea for the requested file
    * @param filePath
    * @return
    */
    public ScriptArea findEditor(File filePath) {
    return openScripts.keySet().stream()
    .filter(scriptArea ->
    scriptArea.getFilePath().equals(filePath)
    )
    .findAny()
    .orElse(null);
    }
    /**
    * Save the script currently in focus to the specified file
    * @param scriptFile
    * @throws IOException
    */
    public void saveCurrentScriptAs(File scriptFile) throws IOException {
    for (ScriptArea area : openScripts.keySet()) {
    if (openScripts.size() == 1 || area.isFocused()) {
    System.out.println(area.getText());
    FileUtils.write(scriptFile, area.getText(), Charset.defaultCharset());
    area.setFilePath(scriptFile);
    area.setDirty(false);
    }
    }
    }
    public List<ProofScript> getCombinedAST() {
    ArrayList<ProofScript> all = new ArrayList<>();
    for (ScriptArea area : openScripts.keySet()) {
    ......@@ -223,6 +222,25 @@ public class ScriptController {
    // throw new NotImplementedException();
    }
    /**
    * Save the script currently in focus to the specified file
    *
    * @param scriptFile
    * @throws IOException
    */
    public void saveCurrentScriptAs(File scriptFile) throws IOException {
    for (ScriptArea area : openScripts.keySet()) {
    if (openScripts.size() == 1 || area.isFocused()) {
    System.out.println(area.getText());
    FileUtils.write(scriptFile, area.getText(), Charset.defaultCharset());
    area.setFilePath(scriptFile);
    area.setDirty(false);
    }
    }
    }
    public MainScriptIdentifier getMainScript() {
    return mainScript.get();
    }
    ......@@ -235,11 +253,6 @@ public class ScriptController {
    return mainScript;
    }
    private ScriptArea findEditor(ASTNode node) {
    File f = new File(node.getRuleContext().getStart().getInputStream().getSourceName());
    return findEditor(f);
    }
    public class ASTNodeHighlighter {
    public final String clazzName;
    private ScriptArea.RegionStyle lastRegion;
    ......@@ -249,14 +262,6 @@ public class ScriptController {
    this.clazzName = clazzName;
    }
    public void remove() {
    logger.debug("remove highlight");
    if (lastScriptArea != null) {
    logger.debug("previous highlight on {} for {}", lastScriptArea, lastRegion);
    lastScriptArea.getMarkedRegions().remove(lastRegion);
    }
    }
    public void highlight(ASTNode node) {
    logger.debug("Highlight requested for {}", node);
    remove();
    ......@@ -274,6 +279,14 @@ public class ScriptController {
    lastRegion = r;
    }
    public void remove() {
    logger.debug("remove highlight");
    if (lastScriptArea != null) {
    logger.debug("previous highlight on {} for {}", lastScriptArea, lastRegion);
    lastScriptArea.getMarkedRegions().remove(lastRegion);
    }
    }
    private ScriptArea.RegionStyle asRegion(ASTNode node) {
    assert node != null;
    return new ScriptArea.RegionStyle(node.getRuleContext().getStart().getStartIndex(),
    ......
    src/main/java/edu/kit/formal/psdb/interpreter/graphs/ProofTreeController.java
    View file @ cc20826f
    ......@@ -106,7 +106,7 @@ public class ProofTreeController {
    //set value of newly computed node
    nextComputedNode.setValue(nodeAddedEvent.getAddedNode());
    //setNewState(this.statePointer.getState());
    //Events.fire(new Events.NewNodeExecuted(nodeAddedEvent.getAddedNode().getScriptstmt()));
    }
    };
    ......
    src/main/java/edu/kit/formal/psdb/termmatcher/MatcherFacade.java
    View file @ cc20826f
    ......@@ -2,15 +2,21 @@ package edu.kit.formal.psdb.termmatcher;
    import de.uka.ilkd.key.logic.Semisequent;
    import de.uka.ilkd.key.logic.Sequent;
    import de.uka.ilkd.key.logic.SequentFormula;
    import de.uka.ilkd.key.logic.Term;
    import org.antlr.v4.runtime.CharStream;
    import org.antlr.v4.runtime.CharStreams;
    import org.antlr.v4.runtime.CommonTokenStream;
    import org.key_project.util.collection.ImmutableList;
    import java.util.ArrayList;
    import java.util.List;
    /**
    * A facade for capturing everthing we want to do with matchers.
    *
    * @author Alexander Weigl
    * @author S.Grebing
    */
    public class MatcherFacade {
    public static Matchings matches(String pattern, Term keyTerm) {
    ......@@ -37,12 +43,12 @@ public class MatcherFacade {
    /**
    * Match a semisequent against a sequent
    *
    * @param pattern Semiseqeuent pattern e.g. f(x), f(x)
    * @param pattern Semisequent pattern e.g. f(x), f(x)
    * @param semiSeq Concrete KeY Semisequent
    * @return Matchings
    */
    public static Matchings matches(String pattern, Semisequent semiSeq) {
    MatcherImpl matcher = new MatcherImpl();
    MatchPatternParser mpp = getParser(pattern);
    MatchPatternParser.SemiSeqPatternContext ctx = mpp.semiSeqPattern();
    return matches(ctx, semiSeq);
    ......@@ -50,13 +56,57 @@ public class MatcherFacade {
    }
    public static Matchings matches(MatchPatternParser.SemiSeqPatternContext pattern, Semisequent semiSeq) {
    //semiSeq.iterator()
    // List<MatchPatternParser.TermPatternContext> termPatternContexts = ctx.termPattern();
    // for (MatchPatternParser.TermPatternContext termpattern: termPatternContexts) {
    //for all terms in seq
    // Matchings s = accept(termpattern, peek);
    // }
    return null;
    MatcherImpl matcher = new MatcherImpl();
    ImmutableList<SequentFormula> allSequentFormulas = semiSeq.asList();
    List<MatchPatternParser.TermPatternContext> termPatternContexts = pattern.termPattern();
    List<Matchings> allMatches = new ArrayList<>();
    for (MatchPatternParser.TermPatternContext termPatternContext : termPatternContexts) {
    Matchings m = new Matchings();
    for (SequentFormula form : allSequentFormulas) {
    Matchings temp = matcher.accept(termPatternContext, form.formula());
    m.addAll(temp);
    }
    allMatches.add(m);
    }
    Matchings res = reduceCompatibleMatches(allMatches);
    System.out.println("res = " + res);