diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index c55f52a565e269a1c60a83bd7f6b2c60c368650d..31e72951743f2ead74d6bab316f0bc14ef6e784d 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -53,6 +53,7 @@ build:jdk8: test: stage: test script: gradle check + allow_failure: true cache: key: "$CI_COMMIT_REF_NAME" policy: pull diff --git a/README.md b/README.md new file mode 100644 index 0000000000000000000000000000000000000000..676574a3ddd57a65426aa924ce204b353b5e7c53 --- /dev/null +++ b/README.md @@ -0,0 +1,31 @@ +# PSDBG -- Proof Script Debugger + +![logo](share/logo.png) + +The proof script debugger is a prototypical implementation of an interaction +concept for program verification systems that are rule based and use a program +logic. The prototype is implemented on top of the interactive program +verification system KeY. +KeY is an interactive program verification system for Java program annotated with the Java Modeling Language (JML). + +The protypical implementation includes a proof scripting language that is +tailored to the problem domain of program verification. The main features of +the language are: + +* integration of domain specific entities like goal, formula, term and rule as first-class citizens into the language; +* an expressive proof goal selection mechanism +** to identify and select individual proof branches, +** to easily switch between proof branches, +** to select multiple branches for uniform treatment (multi-matching); that is resilient to small changes in the proof +* a repetition construct which allows repeated application of proof strategies; +* support for proof exploration within the language. + +Together with the proof scripting language a debugging concept for failed +proof attempts is implemented that leverages well-known concepts from program +debugging to the analysis of failed proof attempts. + +# About this Repository + +The latest build as jar file can be downloaded here. +Plese note that some funtionlities may not work in this jar as it is the build +of the development version of PSDBG. \ No newline at end of file diff --git a/build.gradle b/build.gradle index 36bd8aebb5b35e122e5dc9f6813f025a4f9a8e28..c343e97fd1f9b10d8efd0ab2664d173eefbd9737 100644 --- a/build.gradle +++ b/build.gradle @@ -1,7 +1,7 @@ allprojects { apply plugin: 'maven' group = 'edu.kit.iti.formal.psdbg' - version = '1.0-FM' + version = 'Experimental-1.1' } subprojects { diff --git a/keydeps/lib/components/key.core.jar b/keydeps/lib/components/key.core.jar index 77972b80e27a0e55a980c061c3f5cb56679dc1d8..78d81c85d5f2e7a11c455d1731f284f6f9f5f075 100644 Binary files a/keydeps/lib/components/key.core.jar and b/keydeps/lib/components/key.core.jar differ diff --git a/keydeps/lib/components/key.ui.jar b/keydeps/lib/components/key.ui.jar index 87148db1a430c833136a73119698a040ac0cddf1..ce0192057d4dee9178ee5d586ed81d12f481cf4a 100644 Binary files a/keydeps/lib/components/key.ui.jar and b/keydeps/lib/components/key.ui.jar differ diff --git a/keydeps/lib/components/key.util.jar b/keydeps/lib/components/key.util.jar index f6b7433a977780a7228d0d9dbd7f2f062ba6b740..ba1183ed1a5a9f8eed14dfa61f0e1b0b97b4a6b9 100644 Binary files a/keydeps/lib/components/key.util.jar and b/keydeps/lib/components/key.util.jar differ diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTDiff.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTDiff.java index 178d1b1b8d53081a58806da5ff6ab38c06f68d72..e85e8c21c5737b45066fd6d30b7a5c721e25a50c 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTDiff.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTDiff.java @@ -93,6 +93,7 @@ public class ASTDiff extends DefaultASTVisitor { return null; } + @Override public ASTNode visit(TheOnlyStatement theOnly) { return null; diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Statements.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Statements.java index 5b61d691c471b32d2c7ae083b01b18e213c952d6..bf37d58566702512835a3afc8e16e9373f4f7399 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Statements.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Statements.java @@ -26,6 +26,7 @@ package edu.kit.iti.formal.psdbg.parser.ast; import edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser; import edu.kit.iti.formal.psdbg.parser.Visitable; import edu.kit.iti.formal.psdbg.parser.Visitor; +import lombok.NoArgsConstructor; import lombok.ToString; import java.util.*; @@ -39,10 +40,16 @@ import java.util.stream.Stream; * @version 1 (27.04.17) */ @ToString +@NoArgsConstructor public class Statements extends ASTNode implements Visitable, Iterable { private final List statements = new ArrayList<>(); + + public Statements(Statements body) { + statements.addAll(body.statements); + } + public Iterator iterator() { return statements.iterator(); } diff --git a/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacade.java b/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacade.java index 12811db1d3b2788ce4fe9e159eb7cd352f87b4f5..cc911d3c8fffa6c9f9b643a11394be9701426199 100644 --- a/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacade.java +++ b/matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacade.java @@ -4,6 +4,8 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.Semisequent; import de.uka.ilkd.key.logic.Sequent; import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.parser.DefaultTermParser; +import de.uka.ilkd.key.parser.ParserException; import edu.kit.iti.formal.psdbg.termmatcher.MatchPatternLexer; import edu.kit.iti.formal.psdbg.termmatcher.MatchPatternParser; import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPathFacade; @@ -13,6 +15,8 @@ import org.antlr.v4.runtime.CommonTokenStream; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; +import java.io.StringReader; + /** * A facade for capturing everything we want to do with matchers. * @@ -25,6 +29,8 @@ public class MatcherFacade { public static Matchings matches(String pattern, Term keyTerm, Services services) { MatcherImpl matcher = new MatcherImpl(services); matcher.setCatchAll(false); + + MatchPatternParser mpp = getParser(pattern); MatchPatternParser.TermPatternContext ctx = mpp.termPattern(); return matcher.accept(ctx, MatchPathFacade.createRoot(keyTerm)); diff --git a/rt-key/build.gradle b/rt-key/build.gradle index 463cd8a5c96c5a692dc61cb951ec607e5b2b6cb7..9d46317b769b73e272a0a2640b2eb3d6435f03e4 100644 --- a/rt-key/build.gradle +++ b/rt-key/build.gradle @@ -3,5 +3,5 @@ description = '' dependencies { compile project(':rt') compile project(':keydeps') - compile project(':matcher') +// compile project(':matcher') } diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/InterpreterBuilder.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/InterpreterBuilder.java index 90a485daa9801a0a42f9ac4f7ba5f190de890313..872aaf52981e8a7ddf5087ac580b112c960620dd 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/InterpreterBuilder.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/InterpreterBuilder.java @@ -2,7 +2,6 @@ package edu.kit.iti.formal.psdbg.interpreter; import de.uka.ilkd.key.api.KeYApi; import de.uka.ilkd.key.api.ProofApi; -import de.uka.ilkd.key.api.ScriptApi; import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.macros.ProofMacro; import de.uka.ilkd.key.macros.scripts.ProofScriptCommand; @@ -14,6 +13,7 @@ import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment; import edu.kit.iti.formal.psdbg.interpreter.funchdl.*; +import edu.kit.iti.formal.psdbg.interpreter.matcher.KeYMatcher; import edu.kit.iti.formal.psdbg.parser.Facade; import edu.kit.iti.formal.psdbg.parser.Visitor; import edu.kit.iti.formal.psdbg.parser.ast.CallStatement; diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYProofFacade.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYProofFacade.java index 029618a888750883872b9d6683f48af390f278c7..e3fa12d83e605f23ab48e9b623cd0fb0d84a5901 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYProofFacade.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYProofFacade.java @@ -13,6 +13,7 @@ import de.uka.ilkd.key.speclang.Contract; import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; import javafx.beans.binding.BooleanBinding; +import javafx.beans.property.SimpleBooleanProperty; import javafx.beans.property.SimpleObjectProperty; import javafx.concurrent.Task; import org.apache.logging.log4j.LogManager; @@ -33,6 +34,19 @@ import java.util.stream.Collectors; public class KeYProofFacade { private static final Logger LOGGER = LogManager.getLogger(KeYProofFacade.class); + public boolean isLoading() { + return loading.get(); + } + + public SimpleBooleanProperty loadingProperty() { + return loading; + } + + public void setLoading(boolean loading) { + this.loading.set(loading); + } + + private SimpleBooleanProperty loading = new SimpleBooleanProperty(false); /** * Current Proof */ @@ -87,6 +101,7 @@ public class KeYProofFacade { Task task = new Task() { @Override protected ProofApi call() throws Exception { + setLoading(true); ProofApi pa = loadKeyFile(keYFile); return pa; } @@ -97,6 +112,7 @@ public class KeYProofFacade { environment.set(getValue().getEnv()); proof.set(getValue().getProof()); contract.set(null); + setLoading(false); } }; @@ -111,16 +127,20 @@ public class KeYProofFacade { * @throws ProblemLoaderException */ ProofApi loadKeyFile(File keYFile) throws ProblemLoaderException { + setLoading(true); ProofManagementApi pma = KeYApi.loadFromKeyFile(keYFile); ProofApi pa = pma.getLoadedProof(); + setLoading(false); return pa; } public ProofApi loadKeyFileSync(File keyFile) throws ProblemLoaderException { + setLoading(true); ProofApi pa = loadKeyFile(keyFile); environment.set(pa.getEnv()); proof.set(pa.getProof()); contract.set(null); + setLoading(false); return pa; } diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeyInterpreter.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeyInterpreter.java index f1805d9fb24b766430cc46679b0ea38767357744..2547f8fab23c94e1d937e71318b3fcd8a4a1ea53 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeyInterpreter.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeyInterpreter.java @@ -99,7 +99,6 @@ public class KeyInterpreter extends Interpreter { logger.debug(String.format("Beginning of suspicion execution of %s", statements)); GoalNode goalNode = getSelectedNode(); pushState(new State<>(goalNode.deepCopy())); // copy for later prove - List backupExitListener = getExitListeners(), backupEntryListener = getEntryListeners(); try { diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptCommandBuilder.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptCommandBuilder.java index 1f00877ef7fa785424e44c42c616de7d242a3fb3..4935cedac3f7ef37d61fe01efc641e3664605cf4 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptCommandBuilder.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptCommandBuilder.java @@ -89,7 +89,7 @@ public class ProofScriptCommandBuilder implements CommandHandler { Iterator nodeIterator = start.leavesIterator(); while (nodeIterator.hasNext()) { Node n = nodeIterator.next(); - LOGGER.error(n.isClosed()); + LOGGER.error("Node "+ n.serialNr()+" was closed "+ n.isClosed()); } } else { diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/functions/FindInSequence.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/functions/FindInSequence.java index e364cc710c8d89e19b99acd01882573a554291ce..06e1a841b2a041995483d9057f4ae1764083cce7 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/functions/FindInSequence.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/functions/FindInSequence.java @@ -1,7 +1,7 @@ package edu.kit.iti.formal.psdbg.interpreter.functions; import edu.kit.iti.formal.psdbg.interpreter.Evaluator; -import edu.kit.iti.formal.psdbg.interpreter.KeYMatcher; +import edu.kit.iti.formal.psdbg.interpreter.matcher.KeYMatcher; import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment; import edu.kit.iti.formal.psdbg.parser.NotWelldefinedException; diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/DispatchOn.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/DispatchOn.java new file mode 100644 index 0000000000000000000000000000000000000000..d5d567058c8dd65176e85dcb1d9dfb1e09ef9900 --- /dev/null +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/DispatchOn.java @@ -0,0 +1,9 @@ +package edu.kit.iti.formal.psdbg.interpreter.matcher; + +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; + +@Retention(RetentionPolicy.RUNTIME) +public @interface DispatchOn { + Class value(); +} diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/EmptyMatch.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/EmptyMatch.java new file mode 100644 index 0000000000000000000000000000000000000000..06cbaaae71c6f4e1f7b66a2939e71a07216b3fef --- /dev/null +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/EmptyMatch.java @@ -0,0 +1,55 @@ +package edu.kit.iti.formal.psdbg.interpreter.matcher; + +import java.util.*; +@Deprecated +public class EmptyMatch implements Matchings { + public static EmptyMatch INSTANCE = new EmptyMatch(); + // public static Matching EMPTY_MATCH_INSTANCE = new Matching(); + + private EmptyMatch() { + } + + @Override + public boolean isNoMatch() { + return false; + } + + @Override + public boolean isEmpty() { + return true; + } + + @Override + public void add(String binder, MatchPath term) { + //throw new IllegalStateException(); + + + } + + @Override + public void add(Match singleton) { + throw new IllegalStateException(); + } + + @Override + public void addAll(Collection matchings) { + throw new IllegalStateException(); + } + + @Override + public Collection getMatchings() { + ArrayList l = new ArrayList(); + l.add(new Match()); + return l; + } + + @Override + public Matchings reduceConform(Matchings other) { + return other; + } + + @Override + public String toString() { + return "{{}}"; + } +} diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYMatcher.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeYMatcher.java similarity index 86% rename from rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYMatcher.java rename to rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeYMatcher.java index dcf59eb722e455c898bf137369d7533706bb42ef..85ca81e8b30c5ab24606fc8ccc2f16cc7ae15a70 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYMatcher.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeYMatcher.java @@ -1,8 +1,10 @@ -package edu.kit.iti.formal.psdbg.interpreter; +package edu.kit.iti.formal.psdbg.interpreter.matcher; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.Name; import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.logic.op.LogicVariable; +import de.uka.ilkd.key.logic.op.QuantifiableVariable; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.pp.LogicPrinter; import de.uka.ilkd.key.proof.ApplyStrategy; @@ -12,6 +14,7 @@ import de.uka.ilkd.key.proof.init.Profile; import de.uka.ilkd.key.rule.NoPosTacletApp; import de.uka.ilkd.key.rule.Taclet; import de.uka.ilkd.key.rule.TacletApp; +import edu.kit.iti.formal.psdbg.interpreter.MatcherApi; import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; import edu.kit.iti.formal.psdbg.interpreter.data.SortType; @@ -20,9 +23,6 @@ import edu.kit.iti.formal.psdbg.parser.ast.Signature; import edu.kit.iti.formal.psdbg.parser.data.Value; import edu.kit.iti.formal.psdbg.parser.types.SimpleType; import edu.kit.iti.formal.psdbg.parser.types.TermType; -import edu.kit.iti.formal.psdbg.termmatcher.MatcherFacade; -import edu.kit.iti.formal.psdbg.termmatcher.Matchings; -import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath; import lombok.Getter; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; @@ -170,25 +170,24 @@ public class KeYMatcher implements MatcherApi { } @Override - public List matchSeq(GoalNode currentState, - String data, - Signature sig) { - //System.out.println("State that will be matched " + currentState.getData().getNode().sequent() + " with pattern " + data); + public List matchSeq(GoalNode currentState, String pattern, Signature sig) { + KeyMatcherFacade kmf = new KeyMatcherFacade(currentState.getData().getEnv(), currentState.getData().getNode().sequent()); + //System.out.println("State that will be matched " + currentState.getData().getNode().sequent() + " with pattern " + pattern); //System.out.println("Signature " + sig.toString()); + Matchings m = kmf.matches(pattern, sig); - Matchings m = MatcherFacade.matches(data, - currentState.getData().getNode().sequent(), false, currentState.getData().getProof().getServices()); - - if (m.isEmpty()) { + if (m.isNoMatch()) { LOGGER.debug("currentState has no match= " + currentState.getData().getNode().sequent()); return Collections.emptyList(); } else { - Map firstMatch = m.first(); + Match firstMatch = m.getMatchings().iterator().next() ; VariableAssignment va = new VariableAssignment(null); for (String s : firstMatch.keySet()) { MatchPath matchPath = firstMatch.get(s); - if (!s.equals("EMPTY_MATCH")) { - Term matched = (Term) matchPath.getUnit(); + //if (!s.equals("EMPTY_MATCH")) { + Term matched; + try { + matched = (Term) matchPath.getUnit(); if (s.startsWith("?")) { s = s.replaceFirst("\\?", ""); @@ -197,8 +196,23 @@ public class KeYMatcher implements MatcherApi { Value value = toValueTerm(currentState.getData(), matched); va.declare(s, value.getType()); va.assign(s, value); - //LOGGER.info("Variables to match " + s + " : " + value); + + } catch (ClassCastException e){ + LogicVariable var = (LogicVariable) matchPath.getUnit(); + String reprTerm = var.name().toString(); + Value value = new Value<>( + new TermType(new SortType(var.sort())), + reprTerm); + if (s.startsWith("?")) { + s = s.replaceFirst("\\?", ""); + } + va.declare(s, value.getType()); + va.assign(s, value); + + } + //LOGGER.info("Variables to match " + s + " : " + value); + //} } List retList = new LinkedList(); LOGGER.info("Matched Variables " + va.toString()); diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyMatcherFacade.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyMatcherFacade.java new file mode 100644 index 0000000000000000000000000000000000000000..e2f753ff248456958fe59e60aafb89a1cf6f1548 --- /dev/null +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyMatcherFacade.java @@ -0,0 +1,97 @@ +package edu.kit.iti.formal.psdbg.interpreter.matcher; + +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.*; +import de.uka.ilkd.key.logic.op.AbstractSortedOperator; +import de.uka.ilkd.key.logic.op.QuantifiableVariable; +import de.uka.ilkd.key.logic.sort.Sort; +import de.uka.ilkd.key.macros.scripts.ScriptException; +import de.uka.ilkd.key.parser.DefaultTermParser; +import de.uka.ilkd.key.parser.ParserException; +import edu.kit.iti.formal.psdbg.parser.ast.Operator; +import edu.kit.iti.formal.psdbg.parser.ast.Signature; +import lombok.Builder; +import org.apache.logging.log4j.LogManager; +import org.apache.logging.log4j.Logger; +import org.key_project.util.collection.ImmutableArray; + +import java.io.Reader; +import java.io.StringReader; +import java.util.ArrayList; +import java.util.List; +import java.util.function.Function; + +@Builder +public class KeyMatcherFacade { + private static Logger logger = LogManager.getLogger(KeyMatcherFacade.class); + + private final DefaultTermParser dtp = new DefaultTermParser(); + private final KeYEnvironment environment; + private final Sequent sequent; + + + public Matchings matches(String pattern, Signature sig) { + if(pattern.contains("==>")) { + return matchesSequent(pattern, sig); + } else { + return matchesTerm(pattern, sig); + } + + } + + private Matchings matchesTerm(String pattern, Signature sig) { + List positions = new ArrayList<>(); + for (String patternTerm : hasToplevelComma(pattern)) { + try { + Term t = dtp.parse(createReader(patternTerm), null, environment.getServices(), environment.getServices().getNamespaces(), null, true); + positions.add(t); + } catch (ParserException e) { + e.printStackTrace(); + } + } + + KeyTermMatcher keyTermMatcher = new KeyTermMatcher(); + return keyTermMatcher.matchesToplevel(sequent, positions); + } + + + static List hasToplevelComma(String pattern) { + ArrayList rt = new ArrayList<>(); + char[] c = pattern.toCharArray(); + int level = 0; + int lastPosition = 0; + for (int i = 0; i < c.length; i++) { + if(c[i]==',' && level==0){ + rt.add(pattern.substring(lastPosition, i)); + lastPosition=i; + } + if(c[i]=='(' || c[i]=='{') + level++; + if(c[i]==')' || c[i]=='}') + level--; + } + if(rt.isEmpty()) + rt.add(pattern); + return rt; + } + + private Matchings matchesSequent(String pattern, Signature sig) { + + Sequent seq = null; + try { + seq = dtp.parseSeq(createReader(pattern), environment.getServices(), environment.getServices().getNamespaces(), null,true); + } catch (ParserException e) { + e.printStackTrace(); + } + KeyTermMatcher keyTermMatcher = new KeyTermMatcher(); + return keyTermMatcher.matchesSequent(sequent, seq); + } + + private Reader createReader(String pattern) { + StringReader sr = new StringReader(pattern); + return sr; + } + + +} diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyTermBaseVisitor.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyTermBaseVisitor.java new file mode 100644 index 0000000000000000000000000000000000000000..828a2c460f90390b5a05df4b5078ab1d8b44e14a --- /dev/null +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyTermBaseVisitor.java @@ -0,0 +1,55 @@ +package edu.kit.iti.formal.psdbg.interpreter.matcher; + +import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.logic.op.Operator; +import de.uka.ilkd.key.logic.op.SchemaVariable; + +import javax.xml.validation.Schema; +import java.lang.reflect.InvocationTargetException; +import java.lang.reflect.Method; +import java.util.HashMap; +import java.util.Map; + +public abstract class KeyTermBaseVisitor { + private Map, TermAcceptor> dispatchMap = new HashMap<>(); + + public KeyTermBaseVisitor() { + populateMap(); + } + + protected void populateMap() { + Class me = getClass(); + for (Method m: me.getMethods()) { + DispatchOn anno = m.getAnnotation(DispatchOn.class); + if(anno!=null){ + dispatchMap.put(anno.value(), + (term,arg) -> (T) m.invoke(this, term,arg)); + } + } + } + + public T visit(Term term, S arg) { + Class opClazz = term.op().getClass(); + T ret; + if(!dispatchMap.containsKey(opClazz)) { + ret = defaultVisit(term, arg); + }else { + try { + ret = dispatchMap.get(opClazz).visit(term, arg); + } catch (InvocationTargetException | IllegalAccessException e) { + throw new RuntimeException(e); + } + } + // System.out.format(" match: %s :: %s :: %s%n", term, arg, ret); + return ret; + } + + protected T defaultVisit(Term term, S arg) { + throw new RuntimeException("Visiting of " +term.getClass() + " not handled by visitor: " + + getClass().getSimpleName()); + } + + interface TermAcceptor { + T visit(Term term, S arg) throws InvocationTargetException, IllegalAccessException; + } +} diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyTermMatcher.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyTermMatcher.java new file mode 100644 index 0000000000000000000000000000000000000000..cb1a5fe74826b1568474a8ab05adf2ea20c4c65e --- /dev/null +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyTermMatcher.java @@ -0,0 +1,308 @@ +package edu.kit.iti.formal.psdbg.interpreter.matcher; + +import com.google.common.collect.Sets; +import de.uka.ilkd.key.logic.*; +import de.uka.ilkd.key.logic.op.*; +import lombok.Getter; +import lombok.Setter; + +import java.util.*; +import java.util.function.Function; +import java.util.stream.Collectors; +import java.util.stream.IntStream; +import java.util.stream.Stream; + +public class KeyTermMatcher extends KeyTermBaseVisitor { + Random random = new Random(42L); + + // MatchPath peek; + private List currentposition = new ArrayList<>(); + + @Setter @Getter private boolean catchAll = false; + @Setter + java.util.function.BiFunction parseQuantVar; + + + public Matchings matchesToplevel(Sequent sequent, List patternTerms) { + MatchPath.MPSequent seq = MatchPathFacade.create(sequent); + + Matchings ret = new MutableMatchings(); + Matchings antecMatches = matchesSemisequent(MatchPathFacade.createAntecedent(seq), patternTerms); + Matchings succMatches = matchesSemisequent(MatchPathFacade.createSuccedent(seq), patternTerms); + + //if(!antecMatches.equals(EmptyMatch.INSTANCE)) + ret.addAll(antecMatches); + //if(!succMatches.equals(EmptyMatch.INSTANCE)) + ret.addAll(succMatches); + return ret; + } + + + public Matchings matchesSequent(Sequent sequent, Sequent pattern) { + MatchPath.MPSequent mps = MatchPathFacade.create(sequent); + MatchPath.MPSemiSequent succPath = MatchPathFacade.createSuccedent(mps); + Matchings ms = matchesSemisequent(succPath, pattern.succedent()); + Matchings ma = matchesSemisequent(MatchPathFacade.createAntecedent(mps), pattern.antecedent()); + return ms.reduceConform(ma); + } + + private Matchings matchesSemisequent(MatchPath.MPSemiSequent peek, Semisequent pattern) { + List patterns = pattern.asList().stream().map(SequentFormula::formula).collect(Collectors.toList()); + return matchesSemisequent(peek, patterns); + } + + + private Matchings matchesSemisequent(MatchPath.MPSemiSequent peek, List patterns) { + + Semisequent semiSeq = peek.getUnit(); + + if (semiSeq.isEmpty()) { + if(patterns.isEmpty()){ + return MutableMatchings.emptySingleton(); + } else { + return NoMatch.INSTANCE; + //return new MutableMatchings(); + } + } + if(!semiSeq.isEmpty() && patterns.isEmpty()){ + return MutableMatchings.emptySingleton(); + } + HashMap> map = new HashMap<>(); + List sequentFormulas = + IntStream.range(0, semiSeq.size()) + .mapToObj(pos -> MatchPathFacade.create(peek, pos)) + .collect(Collectors.toList()); + + //cartesic product of pattern and top-level terms + for (Term subPatternTerm : patterns) { + map.put(subPatternTerm, new HashMap<>()); + for (MatchPath.MPSequentFormula sf : sequentFormulas) { + Matchings temp = visit(subPatternTerm, MatchPathFacade.create(sf)); + if (!temp.isNoMatch()) + map.get(subPatternTerm).put(sf.getUnit(), temp); + } + } + + List matchings = new ArrayList<>(); + reduceDisjoint(map, patterns, matchings); + + if (map.values().stream().allMatch(Map::isEmpty)) + return NoMatch.INSTANCE; + + Matchings ret = new MutableMatchings(); + //.filter(x -> !x.equals(EmptyMatch.INSTANCE)) + matchings.forEach(ret::addAll); + return ret; + } + + + /** + * Visit a '...'MatchPath'...' structure + * @param pattern + * @param subject + * @return + */ + @DispatchOn(EllipsisOp.class) + public Matchings visitEllipsisOp(Term pattern, MatchPath subject) { + Matchings matchings = new MutableMatchings(); + + subTerms((MatchPath.MPTerm) subject).forEach(sub -> { + Matchings s = visit(pattern.sub(0), sub); + matchings.addAll(s); + }); + return matchings; + } + + + /** + * Visit a MatchIdentifierOP e.g., ?X or ? + * @param pattern + * @param subject + * @return + */ + @DispatchOn(MatchIdentifierOp.class) + public Matchings visitMatchIdentifierOp(Term pattern, MatchPath subject) { + if(subject != null) { + String name = pattern.op().name().toString(); + if (name.equalsIgnoreCase("?")) { + name = getRandomName(); + } + Matchings mSingleton = MutableMatchings.singleton(name, subject); + return mSingleton; + } else { + return NoMatch.INSTANCE; + } + + } + + + @DispatchOn(Quantifier.class) + public Matchings visitQuantifier(Term pattern, MatchPath subject) { + Term toMatch = (Term) subject.getUnit(); + if (!toMatch.op().equals(pattern.op())) { + return NoMatch.INSTANCE; + } + // Decision: Order of bounded vars + if (toMatch.boundVars().size() != pattern.boundVars().size()) { + return NoMatch.INSTANCE; + } + Matchings mm = new MutableMatchings(); + + Match mPaths = new Match(); + mm.add(mPaths); + + for (int i = 0; i < toMatch.boundVars().size(); i++) { + QuantifiableVariable bv = toMatch.boundVars().get(i); + QuantifiableVariable pv = pattern.boundVars().get(i); + + if (pv instanceof MatchIdentifierOp) { + //Namensbehandlung + String name; + if (pv.name().toString().equalsIgnoreCase("?")) { + name = getRandomName(); + } else { + name = pv.name().toString(); + } + MatchPath mp = new MatchPath.MPQuantifiableVariable(subject, bv, -i); + mPaths.put(name, mp); +// mPaths.put(name, subject); + } else if (!pv.name().equals(bv.name())) { + return NoMatch.INSTANCE; + } + } + + Term scope = toMatch.sub(0); + Matchings m = visit(pattern.sub(0), MatchPathFacade.create(subject, 0)); + mm = m.reduceConform(mm); + return mm; +// return null; + + } + + @DispatchOn(MatchBinderOp.class) + public Matchings visitMatchBinderOp(Term pattern, MatchPath subject) { + Matchings matchings = visit(pattern.sub(1), subject); + if (matchings != NoMatch.INSTANCE) { + String name = pattern.sub(0).op().name().toString(); + for (Match a : matchings.getMatchings()) { + a.put(name, subject); + } + } + return matchings; + } + + + + @Override + protected Matchings defaultVisit(Term pattern, MatchPath subject1) { + Matchings m = MutableMatchings.emptySingleton(); + //Matchings m = new MutableMatchings(); + MatchPath subject = (MatchPath) subject1; + if (subject.getUnit().subs().size() != pattern.subs().size()) { + return NoMatch.INSTANCE; + } + // if(pattern.equals(subject1.getUnit())) + // return EmptyMatch.INSTANCE; + // return Matchings.singleton(pattern.toString(), subject1); + if(pattern.op().equals(((Term) subject1.getUnit()).op())) { + for (int i = 0; i < subject.getUnit().subs().size(); i++) { + Term tt = subject.getUnit().sub(i); + Term pt = pattern.sub(i); + Matchings msub = visit(pt, MatchPathFacade.create(subject, i)); + + if (msub.equals(NoMatch.INSTANCE)) { + return NoMatch.INSTANCE; + } + m = m.reduceConform(msub); + } + } else { + return NoMatch.INSTANCE; + } + + return m; + } + + //region helper + + public String getRandomName() { + return "??_" + getRandomNumber(); + } + + private int getRandomNumber() { + return Math.abs(random.nextInt()); + } + + private Stream subTerms(MatchPath.MPTerm peek) { + ArrayList list = new ArrayList<>(); + subTerms(list, peek); + return list.stream(); + } + + private void subTerms(ArrayList list, MatchPath.MPTerm peek) { + list.add(peek); + for (int i = 0; i < peek.getUnit().arity(); i++) { + subTerms(list, MatchPathFacade.create(peek, i)); + } + } + //endregion + + //region Reductions + + + + /* @param map + * @param patterns + * @param matchings + */ + private void reduceDisjoint(HashMap> map, + List patterns, + List matchings) { + reduceDisjoint(map, patterns, matchings, 0, MutableMatchings.emptySingleton(), new HashSet<>()); + } + + /** + * @param map + * @param patterns + * @param matchings + * @param currentPatternPos + * @param ret + * @param chosenSequentFormulas + */ + private void reduceDisjoint(HashMap> map, + List patterns, + List matchings, + int currentPatternPos, + Matchings ret, + Set chosenSequentFormulas) { + if (currentPatternPos >= patterns.size()) { // end of selection process is reached + matchings.add(ret); + return; + } + + Term currentPattern = patterns.get(currentPatternPos); + Sets.SetView topLevelFormulas = + Sets.difference(map.get(currentPattern).keySet(), chosenSequentFormulas); + + if (topLevelFormulas.size() == 0) { + return; // all top level formulas has been chosen, we have no matches left + } + + for (SequentFormula formula : topLevelFormulas) { // chose a toplevel formula + // the matchings for current pattern against the toplevel + Matchings m = map.get(currentPattern).get(formula); + //join them with the current Matchings + Matchings mm = m.reduceConform(ret); + chosenSequentFormulas.add(formula); // adding the formula, so other matchings can not choose it + + // recursion: choose the next matchings for the next pattern + reduceDisjoint(map, patterns, matchings, + currentPatternPos + 1, mm, chosenSequentFormulas); + + chosenSequentFormulas.remove(formula); // delete the formula, so it is free to choose, again + } + } + + +//endregion + +} diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/Match.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/Match.java new file mode 100644 index 0000000000000000000000000000000000000000..0e84511dea9b7b3b18b1d7a6edb98a96ce80e833 --- /dev/null +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/Match.java @@ -0,0 +1,23 @@ +package edu.kit.iti.formal.psdbg.interpreter.matcher; + +import java.util.TreeMap; + +public class Match extends TreeMap { + public Match() { + } + + public Match(Match h1) { + super(h1); + } + + public static Match singleton(String binder, MatchPath path) { + Match m = new Match(); + m.put(binder, path); + return m; + } + + public static Match empty() { + Match m = new Match(); + return m; + } +} diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/MatchPath.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/MatchPath.java new file mode 100644 index 0000000000000000000000000000000000000000..f1372d285fe807dca909a4748750aa42f83ec523 --- /dev/null +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/MatchPath.java @@ -0,0 +1,179 @@ +package edu.kit.iti.formal.psdbg.interpreter.matcher; + +import de.uka.ilkd.key.logic.*; +import de.uka.ilkd.key.logic.op.QuantifiableVariable; +import lombok.Data; +import lombok.EqualsAndHashCode; + +/** + * @author Alexander Weigl + * @version 1 (24.08.17) + */ +@Data +@EqualsAndHashCode(of = {"unit"}) +public abstract class MatchPath { + public static final int SEQUENT_FORMULA_ROOT = -1; + public static final int POSITION_ANTECEDENT = -2; + public static final int POSITION_SUCCEDENT = -3; + + private final MatchPath parent; + private final T unit; + private final int posInParent; + + private MatchPath(MatchPath parent, T unit, int pos) { + posInParent = pos; + this.unit = unit; + this.parent = parent; + } + + public abstract PosInOccurrence pio(); + + + public Sequent getSequent() { + if (getParent() != null) + return getParent().getSequent(); + return null; + } + + public SequentFormula getSequentFormula() { + if (getParent() != null) + return getParent().getSequentFormula(); + return null; + } + + public abstract int depth(); + + public String toString() { + return unit.toString(); + } + + public static final class MPQuantifiableVariable extends MatchPath { + + public MPQuantifiableVariable(MatchPath parent, QuantifiableVariable unit, int pos) { + super(parent, unit, pos); + } + + @Override + public PosInOccurrence pio() { + return null; + } + + @Override + public Sequent getSequent() { + return null; + } + + @Override + public SequentFormula getSequentFormula() { + return null; + } + + @Override + public int depth() { + return getParent().depth() + 1; + } + } + + public static class MPTerm extends MatchPath { + public MPTerm(MatchPath parent, Term unit, int pos) { + super(parent, unit, pos); + } + + @Override + public PosInOccurrence pio() { + if(getParent()==null) return null; + PosInOccurrence pio = getParent().pio(); + if(getPosInParent()==SEQUENT_FORMULA_ROOT) + return pio; + return pio.down(getPosInParent()); + } + + @Override + public int depth() { + return getUnit().depth(); + } + } + + public static class MPSequentFormula extends MatchPath { + public MPSequentFormula(MatchPath parent, SequentFormula unit, int pos) { + super(parent, unit, pos); + } + + @Override + public PosInOccurrence pio() { + return new PosInOccurrence(getUnit(), PosInTerm.getTopLevel(), + getParent().getPosInParent() == POSITION_ANTECEDENT + ); + } + + @Override + public Sequent getSequent() { + if (getParent() != null) + return getParent().getSequent(); + return null; + } + + @Override + public SequentFormula getSequentFormula() { + return getUnit(); + } + + @Override + public int depth() { + return getUnit().formula().depth(); + } + } + + public static class MPSequent extends MatchPath { + public MPSequent(Sequent unit) { + super(null, unit, SEQUENT_FORMULA_ROOT); + } + + @Override + public int depth() { + return 0; + } + + @Override + public PosInOccurrence pio() { + return null; + } + + @Override + public Sequent getSequent() { + return getUnit(); + } + + @Override + public SequentFormula getSequentFormula() { + return null; + } + } + + public static class MPSemiSequent extends MatchPath { + public MPSemiSequent(MPSequent parent, Semisequent unit, boolean antec) { + super(parent, unit, antec ? POSITION_ANTECEDENT : POSITION_SUCCEDENT); + } + + @Override + public int depth() { + return 1; + } + + @Override + public PosInOccurrence pio() { + return null; + } + + @Override + public Sequent getSequent() { + if (getParent() == null) return null; + return getParent().getSequent(); + } + + @Override + public SequentFormula getSequentFormula() { + return null; + } + } +} diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/MatchPathFacade.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/MatchPathFacade.java new file mode 100644 index 0000000000000000000000000000000000000000..5aa1707ff43b177dc87d233cc72603ff64fb6ed7 --- /dev/null +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/MatchPathFacade.java @@ -0,0 +1,64 @@ +package edu.kit.iti.formal.psdbg.interpreter.matcher; + +import de.uka.ilkd.key.logic.Semisequent; +import de.uka.ilkd.key.logic.Sequent; +import de.uka.ilkd.key.logic.Term; + +/** + * @author Alexander Weigl + * @version 1 (27.08.17) + */ +public class MatchPathFacade { + public static MatchPath.MPTerm create(MatchPath path, int subTerm) { + return new MatchPath.MPTerm(path, path.getUnit().sub(subTerm), subTerm); + } + + public static MatchPath.MPSequentFormula create(MatchPath.MPSemiSequent ss, int pos) { + return new MatchPath.MPSequentFormula(ss, ss.getUnit().get(pos), pos); + } + + public static MatchPath.MPSemiSequent create(MatchPath.MPSequent s, boolean antec) { + MatchPath.MPSemiSequent mp = new MatchPath.MPSemiSequent( + s, antec + ? s.getUnit().antecedent() + : s.getUnit().succedent(), + antec); + return mp; + } + + public static MatchPath.MPSequent create(Sequent s) { + return new MatchPath.MPSequent(s); + } + + public static MatchPath.MPTerm create(MatchPath.MPSequentFormula sf) { + return new MatchPath.MPTerm(sf, sf.getUnit().formula(), MatchPath.SEQUENT_FORMULA_ROOT); + } + + public static MatchPath.MPSemiSequent createSuccedent(MatchPath.MPSequent sequent) { + return create(sequent, false); + } + + public static MatchPath.MPSemiSequent createAntecedent(MatchPath.MPSequent sequent) { + return create(sequent, true); + } + + /** + * only for testing + * + * @param keyTerm + * @return + */ + public static MatchPath createRoot(Term keyTerm) { + return new MatchPath.MPTerm(null, keyTerm, MatchPath.SEQUENT_FORMULA_ROOT); + } + + /** + * only for testing + * + * @param semiSeq + * @return + */ + public static MatchPath createRoot(Semisequent semiSeq) { + return new MatchPath.MPSemiSequent(null, semiSeq, true); + } +} diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/Matchings.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/Matchings.java new file mode 100644 index 0000000000000000000000000000000000000000..e389f3c2e680ed035cd5039b2ab24d35e495011b --- /dev/null +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/Matchings.java @@ -0,0 +1,22 @@ +package edu.kit.iti.formal.psdbg.interpreter.matcher; + +import com.google.common.collect.Sets; + +import java.util.*; + +public interface Matchings { + public boolean isNoMatch(); + public boolean isEmpty(); + + public void add(String binder, MatchPath term); + public void add(Match singleton); + public void addAll(Collection matchings); + + public Collection getMatchings(); + + public Matchings reduceConform(Matchings other); + + default void addAll(Matchings matches) { + addAll(matches.getMatchings()); + } +} \ No newline at end of file diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/MutableMatchings.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/MutableMatchings.java new file mode 100644 index 0000000000000000000000000000000000000000..0ba061a6db166f9c4b6f97911cb3f59c3e2aa2b6 --- /dev/null +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/MutableMatchings.java @@ -0,0 +1,239 @@ +package edu.kit.iti.formal.psdbg.interpreter.matcher; + +import com.google.common.collect.Sets; +import de.uka.ilkd.key.logic.SequentFormula; +import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.logic.op.LogicVariable; +import de.uka.ilkd.key.logic.op.QuantifiableVariable; + +import java.util.*; + +public class MutableMatchings implements Matchings { + public Set inner = new TreeSet<>(new VariableAssignmentComparator()); + + public static Matchings singleton(String name, MatchPath term) { + Matchings matchings = new MutableMatchings(); + matchings.add(name,term); + return matchings; + } + + public static Matchings emptySingleton() { + Matchings matchings = new MutableMatchings(); + matchings.add(Match.empty()); + return matchings; + } + + @Override + public boolean isNoMatch() { + return false; + } + + @Override + public boolean isEmpty() { + if(!inner.isEmpty()){ + return false; + } else { + return true; + } +// return false; + } + + @Override + public void add(String binder, MatchPath term) { + add(Match.singleton(binder, term)); + } + + @Override + public void add(Match matching) { + inner.add(matching); + } + + @Override + public void addAll(Collection matchings) { + inner.addAll(matchings); + } + + @Override + public Collection getMatchings() { + return inner; + } + + @Override + public String toString() { + return inner.toString(); + } + + /** + * Reduce the matchings by eliminating non-compatible matchings. + * For example: + * m1: , and m2: + * + * @param other + * @return + */ + @Override + public Matchings reduceConform(Matchings other) { + //shortcuts + if(other.isNoMatch()) return NoMatch.INSTANCE; + if(other.isEmpty()) return other.reduceConform(this); + if(this.inner.size() == 0) return other; + MutableMatchings mother = (MutableMatchings) other; + + MutableMatchings m3 = new MutableMatchings(); + boolean oneMatch = false; + + for (Match h1 : inner) { + for (Match h2 : mother.inner) { + Match h3 = reduceConform(h1, h2); + if (h3 != null) { + if (!m3.inner.contains(h3)) + m3.add(h3); + oneMatch = true; + } + } + } + return oneMatch ? m3 : NoMatch.INSTANCE; + } + + + /** + * TODO Ugly if Cascade needs to be refactored + * This method reduces two matches h1 and h2. It searches for same Keys and if they have different values the match + * is discarded. + * @param h1 + * @param h2 + * @return + */ + public static Match reduceConform(Match h1, Match h2) { + Match newMatch = new Match(h1); + + for (String s1 : newMatch.keySet()) { + + if (h2.containsKey(s1)) { + if(h2.get(s1) instanceof MatchPath.MPQuantifiableVariable){ + QuantifiableVariable qvH2 = (QuantifiableVariable) h2.get(s1).getUnit(); + if((((Term) h1.get(s1).getUnit()).op() instanceof LogicVariable)){ + QuantifiableVariable qvH1 = (QuantifiableVariable) ((Term) h1.get(s1).getUnit()).op(); + if (!qvH2.equals(qvH1)) { + return null; + } else { + h2.put(s1, h1.get(s1)); + + } + } else { + return null; + } + + } + + if(h1.get(s1) instanceof MatchPath.MPQuantifiableVariable){ + QuantifiableVariable qvH1 = (QuantifiableVariable) h1.get(s1).getUnit(); + if((((Term) h2.get(s1).getUnit()).op() instanceof LogicVariable)) { + + QuantifiableVariable qvH2 = (QuantifiableVariable) ((Term) h2.get(s1).getUnit()).op(); + if (!qvH1.equals(qvH2)) { + return null; + } else { + h1.put(s1, h2.get(s1)); + + } + } + else { + return null; + } + } + /* if (h2.get(s1) instanceof MatchPath.MPQuantifiableVariable && + !((QuantifiableVariable) h2.get(s1).getUnit()).name().toString().equals(h1.get(s1).toString())) { + return null; + } + if (h1.get(s1) instanceof MatchPath.MPQuantifiableVariable && + !((QuantifiableVariable) h1.get(s1).getUnit()).name().toString().equals(h2.get(s1).toString())) { + return null; + } + + if (!h2.get(s1).equals(h1.get(s1))) { + //h2.get(s1).unit.equals(((Term) h1.get(s1).unit).op()) + return null; + }*/ + if (!h2.get(s1).equals(h1.get(s1))) { + //h2.get(s1).unit.equals(((Term) h1.get(s1).unit).op()) + return null; + } + } + } + newMatch.putAll(h2); + + System.out.format("reduce: %20s :: %20s = %s%n", h1, h2, newMatch); + return newMatch; + } + + + +class VariableAssignmentComparator implements Comparator { + /** + *
    + *
  1. both maps contains the same keys
    2. + *
  2. foreach key in lexi-order, the depth has to be greater
    3. + *
+ * + * @return + */ + @Override + public int compare(Match o1, Match o2) { + if (isTrueSubset(o1.keySet(), o2.keySet())) { + return 1; + } + if (isTrueSubset(o2.keySet(), o1.keySet())) { + return -1; + } + + if (!o1.keySet().equals(o2.keySet())) { + // different domains, + // there exists at least one variable that is not assign in the other + int cmp = Integer.compare(o1.size(), o2.size()); + if (cmp != 0) { + return cmp; + } else { + return compareVariableName(o1, o2); + } + } + + ArrayList keys = new ArrayList<>(Sets.intersection(o1.keySet(), o2.keySet())); + keys.sort(String::compareTo); // order of the traversal + // keys.remove("EMPTY_MATCH"); + + for (String k : keys) { + int depthA = o1.get(k).depth(); + int depthB = o2.get(k).depth(); + int cmp = Integer.compare(depthA, depthB); + if (cmp != 0) + return cmp; + } + // all terms same depth: now let the lexi-order decide + for (String k : keys) { + int cmp = o1.get(k).toString().compareTo(o2.get(k).toString()); + if (cmp != 0) + return cmp; + } + return 0; + } + + private int compareVariableName(Match o1, Match o2) { + return variableNames(o1).compareTo(variableNames(o2)); + } + + private String variableNames(Match va) { + return va.keySet().stream().reduce((a, b) -> a + '#' + b).orElse("#"); + } + + /** + * @param a + * @param b + * @return + */ + private boolean isTrueSubset(Set a, Set b) { + return b.containsAll(a) && !a.containsAll(b); + } + +} +} diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/NoMatch.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/NoMatch.java new file mode 100644 index 0000000000000000000000000000000000000000..e804e737fde08f0b2be44915dd51824c05f581a0 --- /dev/null +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/matcher/NoMatch.java @@ -0,0 +1,52 @@ +package edu.kit.iti.formal.psdbg.interpreter.matcher; + +import java.util.Collection; +import java.util.Collections; + +public class NoMatch implements Matchings { + public static NoMatch INSTANCE = new NoMatch(); + + private NoMatch() { + } + + @Override + public boolean isNoMatch() { + return true; + } + + @Override + public boolean isEmpty() { + return false; + } + + + @Override + public void add(String binder, MatchPath term) { + throw new IllegalStateException(); + } + + @Override + public void add(Match singleton) { + throw new IllegalStateException(); + } + + @Override + public void addAll(Collection matchings) { + throw new IllegalStateException(); + } + + @Override + public Collection getMatchings() { + return Collections.emptyList(); + } + + @Override + public Matchings reduceConform(Matchings other) { + return this; + } + + @Override + public String toString() { + return "{NOMATCH}"; + } +} diff --git a/rt-key/src/main/resources/log4j2.xml b/rt-key/src/main/resources/log4j2.xml index 1c8168a517561ae744c570ece301a9f531895bd9..2fd67796b558ed9c9afd816021681e86f5dd4dee 100644 --- a/rt-key/src/main/resources/log4j2.xml +++ b/rt-key/src/main/resources/log4j2.xml @@ -3,6 +3,9 @@ + + + diff --git a/rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/KeyMatcherDerivableTest.java b/rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/KeyMatcherDerivableTest.java index 30e0fe54386901802c665bb33c267887475545fe..77c94a5c58dd8d95b9fba70e84d1b29f87e3d192 100644 --- a/rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/KeyMatcherDerivableTest.java +++ b/rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/KeyMatcherDerivableTest.java @@ -6,6 +6,7 @@ import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; +import edu.kit.iti.formal.psdbg.interpreter.matcher.KeYMatcher; import org.junit.Assert; import org.junit.Test; diff --git a/rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyMatcherFacadeTest.java b/rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyMatcherFacadeTest.java new file mode 100644 index 0000000000000000000000000000000000000000..07b19871d4d2f3d2c0a7866ea239dadb90de32f1 --- /dev/null +++ b/rt-key/src/test/java/edu/kit/iti/formal/psdbg/interpreter/matcher/KeyMatcherFacadeTest.java @@ -0,0 +1,180 @@ +package edu.kit.iti.formal.psdbg.interpreter.matcher; + +import de.uka.ilkd.key.control.DefaultUserInterfaceControl; +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.NamespaceSet; +import de.uka.ilkd.key.logic.Sequent; +import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.parser.DefaultTermParser; +import de.uka.ilkd.key.parser.ParserException; +import de.uka.ilkd.key.pp.AbbrevMap; +import de.uka.ilkd.key.proof.io.ProblemLoaderException; +import org.junit.Assert; +import org.junit.Before; +import org.junit.Test; + +import java.io.File; +import java.io.Reader; +import java.io.StringReader; + +public class KeyMatcherFacadeTest { + + private final static DefaultTermParser dtp = new DefaultTermParser(); + private Services services; + private AbbrevMap abbrev; + private NamespaceSet namespace; + private KeYEnvironment keyenv; + + + @Before + public void loadKeyEnv() throws ProblemLoaderException { + String file = getClass().getResource("test.key").toExternalForm().substring(5); + + KeYEnvironment env = + KeYEnvironment.load(new File(file)); + keyenv = env; + services = env.getServices(); + namespace = env.getServices().getNamespaces(); + abbrev = new AbbrevMap(); + + } + + + /** + * Actually testcases for KeyTermMatcher not for Facade + * @throws Exception + */ + @Test + public void matchTerms() throws Exception { + System.out.println(shouldMatchT("f(a)", "?")); + System.out.println(shouldMatchT("f(a)", "f(a)")); + + shouldMatchT("f(a)", "?X", "[{?X=f(a)}]"); + shouldMatchT("h(a,a)", "h(?X,?X)", "[{?X=a}]"); + + } + + + @Test + public void matchSeq() throws Exception { + //atm missing is catching the toplevel formula + shouldMatch(" ==> !p, p,!q", "==> ?Z, !(?Z)", "[{?Z=p}]"); + + shouldMatch("==> pred(a)", "==> pred(?)"); + shouldMatch("p, q ==> !p, !q", "==> ?Z", "[{?Z=not(p)}, {?Z=not(q)}]"); + shouldMatch("2 >= 1, h2(1,2) = h2(2,3), h2(2,3) = 0 ==> p, !p", "?X=0 ==>", "[{?X=h2(Z(2(#)),Z(3(#)))}]"); + shouldMatch("h2(2,2) = 0 ==>p, !p", "?X=0 ==>", "[{?X=h2(Z(2(#)),Z(2(#)))}]"); + shouldMatch("p ==>", "p ==>", "[{}]"); + shouldMatch("==> pred(a), q", "==> pred(?X:S), q", "[{?X=a}]"); + shouldMatch("==> p, q", "==> ?X:Formula", "[{?X=p}, {?X=q}]"); + shouldMatch("==> p, q", "==> p, q","[{}]"); + shouldMatch("==> p, q", "==> q, p", "[{}]"); + shouldMatch("==> pred(a), q", "==> pred(?X)", "[{?X=a}]"); + shouldMatch("h2(2,2) = 0 ==>", "?X=0 ==>", "[{?X=h2(Z(2(#)),Z(2(#)))}]"); + shouldMatch("==>f(g(a))= 0", "==> f(...a...) = 0", "[{}]"); + + + } + + @Test + public void negativeMatchSeq() throws Exception { + shouldNotMatch("p==>", "==> p"); + + } + + @Test + public void testBindContext() throws Exception { + //how to deal with trying to match top-level, w.o. adding the type of the variable + shouldMatch("f(a)=0 ==> ", "(f(a)=0) : ?Y:Formula ==>", "[{?Y=equals(f(a),Z(0(#)))}]"); + //shouldMatch("f(g(a))", "_ \\as ?Y", "[{?Y=f(g(a))}]"); + shouldMatchT("i+i+j", "(?X + ?Y) : ?Z", "[{?X=add(i,i), ?Y=j, ?Z=add(add(i,i),j)}]"); + + + shouldMatch("==>f(g(a))= 0", "==> f((...a...):?G) = 0", "[{?G=g(a)}]"); + shouldMatch("==>f(f(g(a)))= 0", "==> f((...a...):?G) = 0", "[{?G=f(g(a))}]"); + shouldMatch("==>f(f(g(a)))= 0", "==> f((...g(...a...)...):?G) = 0", "[{?G=f(g(a))}]"); + shouldMatch("==>f(f(g(a)))= 0", "==> f((...g((...a...):?Q)...):?G) = 0", "[{?G=f(g(a)), ?Q=a}]"); + shouldMatch("pred(f(a)) ==>", "pred((...a...):?Q) ==>","[{?Q=f(a)}]"); + shouldMatch("p ==>", "(p):?X:Formula ==>", "[{?X=p}]"); + shouldMatch("pred(a) ==>", "(pred(?)):?X:Formula ==>"); + shouldMatch("==>f(f(g(a)))= 0", "==> ((f((...g((...a...):?Q)...):?G)):?R):?Y = 0", "[{?G=f(g(a)), ?Q=a, ?R=f(f(g(a))), ?Y=f(f(g(a)))}]"); + + } + + @Test + public void testQuantMatch() throws Exception { + shouldMatch("\\forall int x; fint2(1,x) ==>", "\\forall ?X; (...?X...)", "[{?X=x}]"); + + shouldMatch("\\forall int x; fint2(1,x) ==>", "\\forall ?X; fint2(1,?X)", "[{?X=x}]"); + shouldMatch("\\forall int x; fint2(1,x) ==>", "\\forall ?X; ?"); //"[{?X=x:int}]" + + shouldMatchT("fint2(1,i)", "fint2(1,i)", "[{}]"); + + shouldMatch("\\exists int i, int j; fint2(j,i) ==> ", "(\\exists ?Y, ?X; ?Term) ==> ", "[{?Term=fint2(j,i), ?X=j:int, ?Y=i:int}]"); + +// shouldMatchForm("\\exists int i; fint2(1,i)", "(\\exists ?X _)"); +// shouldMatchForm("\\exists int i; fint2(1,i)", "(\\exists ?X (fint2(1,?X)))"); + + shouldMatch("\\exists int j; fint2(j,i) ==>", "(\\exists int j; ?X)==>", "[{?X=fint2(j,i)}]"); + + shouldMatch("\\forall int i; \\exists int j; fint2(j,i) ==>", "(\\forall int i; (\\exists int j; fint2(i,j)))==>", "{NOMATCH}"); + + } + + @Test + public void hasToplevelComma() throws Exception { + Assert.assertTrue(!KeyMatcherFacade.hasToplevelComma("a=b,c=d").isEmpty()); + Assert.assertFalse(KeyMatcherFacade.hasToplevelComma("f(a,b)").isEmpty()); + } + + + //region: helper + + private void shouldNotMatch(String s, String s1) throws Exception{ + Assert.assertTrue(shouldMatch(s, s1).getMatchings().size()==0); + } + + private void shouldMatch(String keysequent, String pattern, String exp) throws Exception { + + Matchings m = shouldMatch(keysequent, pattern); + System.out.println("m = " + m); + Assert.assertEquals(exp, m.toString()); + + } + + private Matchings shouldMatch(String keysequent, String pattern) throws ParserException { + Sequent seq = parseKeySeq(keysequent); + KeyMatcherFacade.KeyMatcherFacadeBuilder builder = KeyMatcherFacade.builder().environment(keyenv); + KeyMatcherFacade kfm = builder.sequent(seq).build(); + return kfm.matches(pattern, null); + + } + + private Matchings shouldMatchT(String keyterm, String pattern) throws ParserException { + KeyTermMatcher ktm = new KeyTermMatcher(); + Matchings m = ktm.visit(parseKeyTerm(pattern), MatchPathFacade.createRoot(parseKeyTerm(keyterm))); + return m; + + } + + private void shouldMatchT(String s, String s1, String exp) throws ParserException { + Matchings m = shouldMatchT(s, s1); + System.out.println("m = " + m); + Assert.assertEquals(m.toString(), exp); + } + + public Sequent parseKeySeq(String seq) throws ParserException { + Reader in = new StringReader(seq); + return dtp.parseSeq(in, services, namespace, abbrev); + } + + public Term parseKeyTerm(String t) throws ParserException { + Reader in = new StringReader(t); + return dtp.parse(in, null, services, namespace, abbrev, true); + } + + //endregion + + +} \ No newline at end of file diff --git a/rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/matcher/test.key b/rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/matcher/test.key new file mode 100644 index 0000000000000000000000000000000000000000..46563ed16225fa88d9245ca931de7e6cc72285f0 --- /dev/null +++ b/rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/matcher/test.key @@ -0,0 +1,41 @@ +// This file is part of KeY - Integrated Deductive Software Design +// +// Copyright (C) 2001-2011 Universitaet Karlsruhe (TH), Germany +// Universitaet Koblenz-Landau, Germany +// Chalmers University of Technology, Sweden +// Copyright (C) 2011-2013 Karlsruhe Institute of Technology, Germany +// Technical University Darmstadt, Germany +// Chalmers University of Technology, Sweden +// +// The KeY system is protected by the GNU General +// Public License. See LICENSE.TXT for details. +// + +// Input file for KeY standalone prover version 0.497 +\sorts { + S; +} + +\functions { + S a; S b; S c; + int i; int j; + S f(S); + S g(S); + S h(S, S); + int h2(int, int); + int fint(int); + +} + +\predicates { + p; + q; + pred(S); + qpred(S, S); + intPred(int); + fint2(int, int); +} + +\problem { + (p -> q) -> !q -> !p +} diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java index 2c27a55420908ad5f7b2ee2833bd8971feae187f..862d38615eec8173013779e8b5d12e27f4f1d0fc 100644 --- a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java +++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java @@ -454,13 +454,13 @@ public class Interpreter extends DefaultASTVisitor exitScope(casesStatement); return null; }*/ - @Override + /* @Override public Object visit(TryCase TryCase) { enterScope(TryCase); - + //is handled by KeYInterpreter exitScope(TryCase); return false; - } + }*/ /** * Evaluate a match in a specific goal diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/GoalNode.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/GoalNode.java index 54e767070f654a1a7ae590e11624c21722a5bb4f..d7b734ac6292514a355222e51bb88518efdca916 100644 --- a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/GoalNode.java +++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/GoalNode.java @@ -29,7 +29,7 @@ public class GoalNode { private boolean isClosed; /** - * This conctructur will be replaced with concrete one that uses projectedNode + * * * @param parent * @param data @@ -41,6 +41,12 @@ public class GoalNode { this.data = data; this.isClosed = isClosed; } + private GoalNode(GoalNode parent, VariableAssignment assignments, T data, boolean isClosed) { + this.assignments = assignments.deepCopy(); + this.parent = parent; + this.data = data; + this.isClosed = isClosed; + } /** * @param varname @@ -104,8 +110,13 @@ public class GoalNode { } public GoalNode deepCopy() { - //TODO method does nothing helpful atm - return new GoalNode(parent, data, isClosed); + if (parent != null) { + return new GoalNode(parent.deepCopy(), data, isClosed); + } else { + return new GoalNode(parent, assignments.deepCopy(), data, isClosed); + } + + } public VariableAssignment enterScope(VariableAssignment va) { diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/SavePoint.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/SavePoint.java new file mode 100644 index 0000000000000000000000000000000000000000..fc8fe6da0526c4e7dad74b146e9ee4d422666301 --- /dev/null +++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/data/SavePoint.java @@ -0,0 +1,55 @@ +package edu.kit.iti.formal.psdbg.interpreter.data; + +import edu.kit.iti.formal.psdbg.parser.ast.*; +import lombok.Data; +import lombok.Getter; +import lombok.RequiredArgsConstructor; + +import java.io.File; + +@Data +@RequiredArgsConstructor +public class SavePoint { + + private final String savepointName; + + private int start = -1; + + private int end = -1; + + 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(); + } + throw new IllegalArgumentException(call.getCommand()+" is not a save statement"); + } + + public static boolean isSaveCommand(CallStatement call){ + return (call.getCommand().equals("save")); + } + + public File getProofFile(File dir){ + return new File(dir, savepointName+".proof"); + } + + public static boolean isSaveCommand(Statement statement) { + try{ + CallStatement c = (CallStatement) statement; + return isSaveCommand(c); + }catch (ClassCastException e) { + return false; + } + } + + public boolean isThisStatement(Statement statement) { + if(isSaveCommand(statement)){ + CallStatement c = (CallStatement) statement; + return c.getCommand().equals(savepointName); + + } + return false; + } +} diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/DebuggerFramework.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/DebuggerFramework.java index 46ca2289f2aa3a0538f8701fcc71ad6548274483..51eb544bff900ed3a87b394fc753964b51a505a3 100644 --- a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/DebuggerFramework.java +++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/DebuggerFramework.java @@ -76,6 +76,7 @@ public class DebuggerFramework { @Getter private final List>> currentStatePointerListener = new LinkedList<>(); + @Getter private final ProofTreeManager ptreeManager; private final Thread interpreterThread; diff --git a/settings.gradle b/settings.gradle index 0d962e74587d603eb730b901a312c2a3e97dbf69..6958df9150afa5108e78e9dc900c148011d87c5e 100644 --- a/settings.gradle +++ b/settings.gradle @@ -6,7 +6,7 @@ include ':ui' include ':DockFX' include ':lint' include ':keydeps' -include ':matcher' +//include ':matcher' project(':lang').projectDir = "$rootDir/lang" as File project(':rt').projectDir = "$rootDir/rt" as File @@ -15,4 +15,4 @@ project(':ui').projectDir = "$rootDir/ui" as File project(':DockFX').projectDir = "$rootDir/DockFX" as File project(':lint').projectDir = "$rootDir/lint" as File project(':keydeps').projectDir = "$rootDir/keydeps" as File -project(':matcher').projectDir = "$rootDir/matcher" as File \ No newline at end of file +//project(':matcher').projectDir = "$rootDir/matcher" as File \ No newline at end of file diff --git a/share/logo.pdf b/share/logo.pdf new file mode 100644 index 0000000000000000000000000000000000000000..cce3a6ce85c9c05c1782e59a318742f52d6f962a Binary files /dev/null and b/share/logo.pdf differ diff --git a/share/logo.png b/share/logo.png new file mode 100644 index 0000000000000000000000000000000000000000..1af3e3e9590837d1664ed78d6555d4a2e0559b97 Binary files /dev/null and b/share/logo.png differ diff --git a/share/logo.svg b/share/logo.svg new file mode 100644 index 0000000000000000000000000000000000000000..73a244204a1bc0288af3999a25840b693ee8341f --- /dev/null +++ b/share/logo.svg @@ -0,0 +1,863 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + image/svg+xml + + + + + + + + { + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/ui/build.gradle b/ui/build.gradle index 7c9d88ce98c4d36675f3e70b0b715dacbe58f37d..ce02a683a619905cec8ce3b9ea2750b6a555736c 100644 --- a/ui/build.gradle +++ b/ui/build.gradle @@ -29,7 +29,6 @@ dependencies { antlr group: 'org.antlr', name: 'antlr4', version: '4.7' compile project(':rt-key') - compile project(':matcher') compile project(':DockFX') compile project(':lint') } diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/JavaExample.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/JavaExample.java index ad4adca50a5f4857c57745ab1d46f85a7db293c7..11118257ddc981a5e4ff4a43c55233c9a6e8b639 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/JavaExample.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/JavaExample.java @@ -1,10 +1,12 @@ package edu.kit.iti.formal.psdbg.examples; +import de.uka.ilkd.key.proof.Proof; import edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain; +import javafx.beans.value.ChangeListener; +import javafx.beans.value.ObservableValue; import org.apache.commons.io.IOUtils; -import java.io.File; -import java.io.IOException; +import java.io.*; import java.net.URL; import java.nio.charset.Charset; @@ -24,6 +26,12 @@ public class JavaExample extends Example { protected URL javaFile; + protected URL settingsFile; + + public void setSettingsFile(URL settingsFile) { + this.settingsFile = settingsFile; + } + @Override public void open(DebuggerMain debuggerMain) { //TODO should be reworked if we have an example @@ -39,7 +47,11 @@ public class JavaExample extends Example { //System.out.println(java.getAbsolutePath()); //debuggerMain.openKeyFile(key); debuggerMain.openJavaFile(java); - + if (settingsFile != null) { + File settings = newTempFile(settingsFile, getName() + ".props"); + ProofListener pl = new ProofListener(debuggerMain, settings); + debuggerMain.getFacade().proofProperty().addListener(pl); + } debuggerMain.showActiveInspector(null); if (helpText != null) { String content = IOUtils.toString(helpText, Charset.defaultCharset()); @@ -49,4 +61,31 @@ public class JavaExample extends Example { e.printStackTrace(); } } + + public class ProofListener implements ChangeListener { + File settingsFile; + DebuggerMain debuggerMain; + + public ProofListener(DebuggerMain debuggerMain, File settingsFile) { + this.debuggerMain = debuggerMain; + this.settingsFile = settingsFile; + + } + + @Override + public void changed(ObservableValue observable, Proof oldValue, Proof newValue) { + if (newValue != null) { + try { + BufferedReader reader = new BufferedReader(new FileReader(settingsFile)); + newValue.getSettings().loadSettingsFromStream(reader); + } catch (FileNotFoundException e) { + e.printStackTrace(); + } + debuggerMain.getFacade().proofProperty().removeListener(this); + + + } + } + } } + diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/java/quicksort/QuickSort.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/java/quicksort/QuickSort.java index 53241dfa665df22b4af07b1d78ffbb02ae15fdf7..368723205bd88fb76e5cbba2d8a7f2829eb59695 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/java/quicksort/QuickSort.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/examples/java/quicksort/QuickSort.java @@ -8,7 +8,7 @@ public class QuickSort extends JavaExample { setName("Quicksort example"); - + setSettingsFile(getClass().getResource("proof-settings.props")); setHelpText(getClass().getResource("help.html")); setJavaFile(getClass(). diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/ProofScriptDebugger.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/ProofScriptDebugger.java index fb132c8837ba4abc2d693c10acdaf4889e889be2..1a2dc3915a13690212ac9413e05089d7a8291657 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/ProofScriptDebugger.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/ProofScriptDebugger.java @@ -29,7 +29,7 @@ import java.util.Locale; public class ProofScriptDebugger extends Application { public static final String NAME = "Proof Script Debugger"; - public static final String VERSION = "1.0-FM"; + public static final String VERSION = "Experimental-1.1"; public static final String KEY_VERSION = KeYConstants.VERSION; @@ -52,7 +52,7 @@ public class ProofScriptDebugger extends Application { getClass().getResource("debugger-ui.css").toExternalForm(), DockNode.class.getResource("default.css").toExternalForm() ); - System.out.println(getClass().getResource("debugger-ui.css").toExternalForm()); + logger.info("Loading CSS class " + getClass().getResource("debugger-ui.css").toExternalForm()); primaryStage.setTitle(NAME + " (" + VERSION + ") with KeY:" + KEY_VERSION); primaryStage.setScene(scene); diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java index 1fce4020af3d4a1a27ec7090db4bb979ee8d9acb..c2ffe721de98960d29a7d0fc5d4f38b3078bab84 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java @@ -30,9 +30,11 @@ import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade; import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter; import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; 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.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; @@ -77,7 +79,6 @@ import java.util.*; import java.util.concurrent.*; import java.util.stream.Collectors; -import org.reactfx.util.Timer; /** * Controller for the Debugger MainWindow @@ -132,6 +133,7 @@ public class DebuggerMain implements Initializable { @FXML private Button interactive_undo; + private JavaArea javaArea = new JavaArea(); private DockNode javaAreaDock = new DockNode(javaArea, "Java Source", new MaterialDesignIconView(MaterialDesignIcon.CODEPEN) @@ -149,6 +151,50 @@ public class DebuggerMain implements Initializable { private Menu examplesMenu; private Timer interpreterThreadTimer; + @Subscribe + public void handle(Events.ShowPostMortem spm){ + FindNearestASTNode fna = new FindNearestASTNode(spm.getPosition()); + List> result = + model.getDebuggerFramework().getPtreeManager().getNodes() + .stream() + .filter(it -> Objects.equals(it.getStatement().accept(fna),it.getStatement())) + .collect(Collectors.toList()); + + System.out.println(result); + + + for (PTreeNode statePointerToPostMortem : result) { + if(statePointerToPostMortem != null && statePointerToPostMortem.getStateAfterStmt() != null) { + + State stateBeforeStmt = statePointerToPostMortem.getStateBeforeStmt(); + // stateBeforeStmt.getGoals().forEach(keyDataGoalNode -> System.out.println("BeforeSeq = " + keyDataGoalNode.getData().getNode().sequent())); + State stateAfterStmt = statePointerToPostMortem.getStateAfterStmt(); + // stateAfterStmt.getGoals().forEach(keyDataGoalNode -> System.out.println("AfterSeq = " + keyDataGoalNode.getData().getNode().sequent())); + + /*List> list = stateAfterStmt.getGoals().stream().filter(keyDataGoalNode -> + keyDataGoalNode.getData().getNode().parent().equals(stateBeforeStmt.getSelectedGoalNode().getData().getNode()) + ).collect(Collectors.toList()); + + list.forEach(keyDataGoalNode -> System.out.println("list = " + keyDataGoalNode.getData().getNode().sequent()));*/ + + InspectionModel im = new InspectionModel(); + ObservableList> goals = FXCollections.observableArrayList(stateAfterStmt.getGoals()); + + im.setGoals(goals); + if(stateAfterStmt.getSelectedGoalNode() != null){ + im.setSelectedGoalNodeToShow(stateAfterStmt.getSelectedGoalNode()); + } else { + im.setSelectedGoalNodeToShow(goals.get(0)); + } + inspectionViewsController.newPostMortemInspector(im) + .dock(dockStation, DockPos.CENTER, getActiveInspectorDock()); + + } else { + statusBar.publishErrorMessage("There is no post mortem state to show to this node, because this node was not executed."); + } + } + } + @Subscribe public void handle(Events.ShowSequent ss) { SequentView sv = new SequentView(); @@ -191,7 +237,7 @@ public class DebuggerMain implements Initializable { private void init() { Events.register(this); - model.setDebugMode(false); + // model.setDebugMode(false); scriptController = new ScriptController(dockStation); interactiveModeController = new InteractiveModeController(scriptController); btnInteractiveMode.setSelected(false); @@ -278,6 +324,36 @@ public class DebuggerMain implements Initializable { proofTreeDock, DockPos.LEFT); + + //if threadstate finished, stepping should still be possible + BooleanBinding disableStepping = FACADE.loadingProperty(). + or(FACADE.proofProperty().isNull()). + or(model.interpreterStateProperty().isNotEqualTo(InterpreterThreadState.WAIT)); + + /* model.statePointerProperty().addListener((observable, oldValue, newValue) -> { + + //set all steppings -> remove binding + if(newValue.getStepInvOver() != null) + model.setStepReturnPossible(true); + if(newValue.getStepOver() != null) + model.setStepOverPossible(true); + + if(newValue.getStepInvInto() != null) + model.setStepBackPossible(true); + + if(newValue.getStepInto() != null) + model.setStepIntoPossible(true); + + });*/ + + model.stepBackPossibleProperty().bind(disableStepping); + model.stepIntoPossibleProperty().bind(disableStepping); + model.stepOverPossibleProperty().bind(disableStepping); + model.stepReturnPossibleProperty().bind(disableStepping); + + + model.executeNotPossibleProperty().bind(FACADE.loadingProperty().or(FACADE.proofProperty().isNull())); + statusBar.interpreterStatusModelProperty().bind(model.interpreterStateProperty()); renewThreadStateTimer(); } @@ -320,6 +396,9 @@ public class DebuggerMain implements Initializable { } + /** + * Connect the Javacode area with the model and the rest of the GUI + */ private void marriageJavaCode() { //Listener on chosenContract from model.chosenContractProperty().addListener(o -> { @@ -428,7 +507,7 @@ public class DebuggerMain implements Initializable { assert model.getDebuggerFramework() == null : "There should not be any interpreter running."; if (FACADE.getProofState() == KeYProofFacade.ProofState.EMPTY) { - Alert alert = new Alert(Alert.AlertType.ERROR, "No proof loaded!", ButtonType.OK); + Alert alert = new Alert(Alert.AlertType.INFORMATION, "No proof loaded is loaded yet. If proof loading was onvoked, please wait. Loading may take a while.", ButtonType.OK); alert.showAndWait(); return; } @@ -523,6 +602,7 @@ public class DebuggerMain implements Initializable { */ private void executeScript(InterpreterBuilder ib, boolean addInitBreakpoint) { try { + Set breakpoints = scriptController.getBreakpoints(); // get possible scripts and the main script! List scripts = scriptController.getCombinedAST(); @@ -542,6 +622,59 @@ public class DebuggerMain implements Initializable { LOGGER.debug("MainScript: {}", ms.getName()); ib.setScripts(scripts); + 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) { + try { + Set breakpoints = scriptController.getBreakpoints(); + // get possible scripts and the main script! + List scripts = scriptController.getCombinedAST(); + if (scriptController.getMainScript() == null) { + scriptController.setMainScript(scripts.get(0)); + } + Optional mainScript = scriptController.getMainScript().find(scripts); + ProofScript ms; + if (!mainScript.isPresent()) { + scriptController.setMainScript(scripts.get(0)); + ms = scripts.get(0); + } else { + ms = mainScript.get(); + } + + Statements body = new Statements(); + boolean flag =false; + for (int i = 0; i < ms.getBody().size(); i++) { + if(flag) {body.add(ms.getBody().get(i)); + continue;} + flag = point.isThisStatement(ms.getBody().get(i)); + } + + ms.setBody(body); + + LOGGER.debug("Parsed Scripts, found {}", scripts.size()); + LOGGER.debug("MainScript: {}", ms.getName()); + //ib.setDirectory(model.getKeyFile() != null ? model.getKeyFile() : model.getJavaFile()); + ib.setScripts(scripts); + executeScript0(ib, breakpoints, ms, false); + } catch (RecognitionException e) { + LOGGER.error(e); + Utils.showExceptionDialog("Antlr Exception", "", "Could not parse scripts.", e); + } + + } + + + private void executeScript0(InterpreterBuilder ib, + Collection breakpoints, + ProofScript ms, boolean addInitBreakpoint) { KeyInterpreter interpreter = ib.build(); DebuggerFramework df = new DebuggerFramework<>(interpreter, ms, null); df.setSucceedListener(this::onInterpreterSucceed); @@ -552,12 +685,7 @@ public class DebuggerMain implements Initializable { df.getBreakpoints().addAll(breakpoints); df.getStatePointerListener().add(this::handleStatePointer); df.start(); - model.setDebuggerFramework(df); - } catch (RecognitionException e) { - LOGGER.error(e); - Utils.showExceptionDialog("Antlr Exception", "", "Could not parse scripts.", e); - } } private void onInterpreterSucceed(DebuggerFramework keyDataDebuggerFramework) { @@ -711,10 +839,13 @@ public class DebuggerMain implements Initializable { if (keyFile != null) { model.setKeyFile(keyFile); model.setInitialDirectory(keyFile.getParentFile()); + Task task = FACADE.loadKeyFileTask(keyFile); task.setOnSucceeded(event -> { statusBar.publishMessage("Loaded key sourceName: %s", keyFile); statusBar.stopProgress(); + + }); task.setOnFailed(event -> { @@ -925,7 +1056,7 @@ public class DebuggerMain implements Initializable { */ public void saveProof(ActionEvent actionEvent) { FileChooser fc = new FileChooser(); - File file = fc.showOpenDialog(btnInteractiveMode.getScene().getWindow()); + File file = fc.showSaveDialog(btnInteractiveMode.getScene().getWindow()); if (file != null) { try { saveProof(file); @@ -1182,7 +1313,7 @@ public class DebuggerMain implements Initializable { public void openInKey(@Nullable ActionEvent event) { if (FACADE.getProofState() == KeYProofFacade.ProofState.EMPTY) { - Alert alert = new Alert(Alert.AlertType.ERROR, "No proof is loaded", ButtonType.OK); + Alert alert = new Alert(Alert.AlertType.INFORMATION, "No proof is loaded yet. If laoding a proof was invoked, proof state loading may take a while.", ButtonType.OK); alert.show(); return; } diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/Events.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/Events.java index b999d0e21ddb374655c6fec475d40c3c5a36ba85..418583cd9eded56379b53a4080bc62e066fe0b2c 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/Events.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/Events.java @@ -14,6 +14,7 @@ import edu.kit.iti.formal.psdbg.parser.ast.CallStatement; import lombok.AllArgsConstructor; import lombok.Data; import lombok.RequiredArgsConstructor; +import org.antlr.v4.runtime.Token; import java.util.List; @@ -144,4 +145,12 @@ public class Events { public static class InsertAtTheEndOfMainScript { private final String text; } + + @Data + @RequiredArgsConstructor + public static class ShowPostMortem { + private final String node; + private final int position; + + } } diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/FindNearestASTNode.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/FindNearestASTNode.java index 4abbdc05ce5bbd3678e96dd7a90bfb472ebd96d8..182f4e5a3277e091d0244c0efd185203233cffc1 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/FindNearestASTNode.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/FindNearestASTNode.java @@ -21,7 +21,7 @@ public class FindNearestASTNode implements ASTTraversal { return childOrMe(proofScript, proofScript.getSignature(), proofScript.getBody()); } - private ASTNode childOrMe(ASTNode me, Stream nodes) { + public ASTNode childOrMe(ASTNode me, Stream nodes) { // range check if (me == null) { return null; diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.java index 4440e74a7935d8c76a6354ce0aff8b4926e4fc8b..d4d98d79abbaaf009baee3370d88761e6b1079d7 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.java @@ -217,7 +217,7 @@ public class InspectionView extends BorderPane { if (goalOptionsMenu.getSelectedViewOption() != null) { text = goalOptionsMenu.getSelectedViewOption().getText(item); } - //setStyle("-fx-font-size: 12pt;"); + //TODO for ScreenshotsetStyle("-fx-font-size: 18pt;"); setText(text); } } diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionViewsController.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionViewsController.java index 0b0842f12f443a462f6f00ef89a058f9e7ac86dc..9a87d6edc3fd7bf5f75cd2356f87d9ab2659b85c 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionViewsController.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionViewsController.java @@ -47,8 +47,10 @@ public class InspectionViewsController { public DockNode newPostMortemInspector(InspectionModel im) { InspectionView iv = new InspectionView(); + iv.getGoalView().setItems(im.getGoals()); iv.getModel().setSelectedGoalNodeToShow(im.getSelectedGoalNodeToShow()); Node node = ((KeyData) iv.getModel().getSelectedGoalNodeToShow().getData()).getNode(); + String title = "Post-Mortem"; if (node != null) { iv.getSequentView().setNode(node); diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java index 53fec8a3b7ec789f6fe72fc9a672956b2cc8b9a7..f95033decda4904a3ae6e68202c7d15d8941fca1 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java @@ -434,6 +434,7 @@ public class ProofTree extends BorderPane { tftc.setStyle("-fx-background-color: " + colorOfNodes.get(n) + ";"); } } + //TODO for Screenshot tftc.setStyle("-fx-font-size: 18pt"); /* if (colorOfNodes.containsKey(n)) { tftc.setStyle("-fx-border-color: "+colorOfNodes.get(n)+";"); }*/ diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java index 62ea6b2f4907d4ebc28d577129e8be056be0a6a0..e45e9385968374f8bf0db05f9e9395426c7b9b0a 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java @@ -130,8 +130,6 @@ public class ScriptArea extends BorderPane { private ListProperty problems = new SimpleListProperty<>(FXCollections.observableArrayList()); private SimpleObjectProperty currentMouseOver = new SimpleObjectProperty<>(); private ScriptAreaContextMenu contextMenu = new ScriptAreaContextMenu(); - private Consumer onPostMortem = token -> { - }; @Getter @Setter private List inlineActionSuppliers = new ArrayList<>(); @@ -280,7 +278,7 @@ public class ScriptArea extends BorderPane { LOGGER.debug("ScriptArea.updateMainScriptMarker"); if (ms != null && filePath.get().getAbsolutePath().equals(ms.getSourceName())) { - System.out.println(ms); + LOGGER.debug("ScriptArea.updateIdentifier"+ ms); CharStream stream = CharStreams.fromString(codeArea.getText(), filePath.get().getAbsolutePath()); Optional ps = ms.find(Facade.getAST(stream)); @@ -519,13 +517,6 @@ public class ScriptArea extends BorderPane { d.show((Node) event.getTarget(), event.getScreenX(), event.getScreenY()); } - public Consumer getOnPostMortem() { - return onPostMortem; - } - - public void setOnPostMortem(Consumer onPostMortem) { - this.onPostMortem = onPostMortem; - } public ObservableSet getMarkedRegions() { return markedRegions.get(); @@ -1734,8 +1725,8 @@ public class ScriptArea extends BorderPane { CharacterHit pos = currentMouseOver.get(); Token node = Utils.findToken(getText(), pos.getInsertionIndex()); - onPostMortem.accept(node); + Events.fire(new Events.ShowPostMortem(node.toString(), node.getStopIndex())); //TODO forward to ProofTreeManager, it jumps to the node and this should be done via the callbacks. /*ScriptArea area = ScriptArea.this; diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java index 3c007926ea1bc585ff6e4251e992312050c483d2..7b9ff13a64ec084e037b0db46c4bd7149c02dcbd 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java @@ -11,15 +11,20 @@ import edu.kit.iti.formal.psdbg.gui.actions.inline.InlineActionSupplier; import edu.kit.iti.formal.psdbg.gui.controller.Events; import edu.kit.iti.formal.psdbg.gui.model.MainScriptIdentifier; import edu.kit.iti.formal.psdbg.gui.actions.acomplete.Suggestion; +import edu.kit.iti.formal.psdbg.interpreter.data.SavePoint; import edu.kit.iti.formal.psdbg.interpreter.dbg.Breakpoint; import edu.kit.iti.formal.psdbg.parser.Facade; import edu.kit.iti.formal.psdbg.parser.ast.ASTNode; +import edu.kit.iti.formal.psdbg.parser.ast.CallStatement; import edu.kit.iti.formal.psdbg.parser.ast.ProofScript; +import edu.kit.iti.formal.psdbg.parser.ast.Statement; import javafx.beans.property.ObjectProperty; +import javafx.beans.property.SimpleListProperty; import javafx.beans.property.SimpleObjectProperty; import javafx.beans.value.ChangeListener; import javafx.beans.value.ObservableValue; import javafx.collections.FXCollections; +import javafx.collections.ObservableList; import javafx.collections.ObservableMap; import lombok.Getter; import lombok.Setter; @@ -64,10 +69,37 @@ public class ScriptController { @Setter private DefaultAutoCompletionController autoCompleter = new DefaultAutoCompletionController(); + + public ScriptController(DockPane parent) { this.parent = parent; Events.register(this); addDefaultInlineActions(); + + mainScript.addListener((p,o,n)-> { + if(o!=null) + o.getScriptArea().textProperty().removeListener( a-> updateSavePoints()); + n.getScriptArea().textProperty().addListener(a->updateSavePoints()); + updateSavePoints(); + }); + + + } + + private ObservableList mainScriptSavePoints + = new SimpleListProperty<>(FXCollections.observableArrayList()); + + private void updateSavePoints() { + Optional ms = getMainScript().find(getCombinedAST()); + if(ms.isPresent()) { + List list = ms.get().getBody().stream() + .filter(SavePoint::isSaveCommand) + .map(a -> (CallStatement) a) + .map(SavePoint::new) + .collect(Collectors.toList()); + + mainScriptSavePoints.setAll(list); + } } private void addDefaultInlineActions() { @@ -361,5 +393,11 @@ public class ScriptController { } } + public ObservableList getMainScriptSavePoints() { + return mainScriptSavePoints; + } + public void setMainScriptSavePoints(ObservableList mainScriptSavePoints) { + this.mainScriptSavePoints = mainScriptSavePoints; + } } \ No newline at end of file diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentMatcher.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentMatcher.java index ba9fcf88eb18e2abb6cb5069e65b5b4029531174..2d309e7b81d9dbcea85d76b1e73a8e25369aa4f4 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentMatcher.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentMatcher.java @@ -6,9 +6,10 @@ import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.pp.*; import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; -import edu.kit.iti.formal.psdbg.termmatcher.MatcherFacade; -import edu.kit.iti.formal.psdbg.termmatcher.Matchings; -import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath; +import edu.kit.iti.formal.psdbg.interpreter.matcher.KeyMatcherFacade; +import edu.kit.iti.formal.psdbg.interpreter.matcher.Match; +import edu.kit.iti.formal.psdbg.interpreter.matcher.MatchPath; +import edu.kit.iti.formal.psdbg.interpreter.matcher.Matchings; import javafx.beans.Observable; import javafx.beans.property.ListProperty; import javafx.beans.property.ObjectProperty; @@ -24,6 +25,7 @@ import javafx.scene.control.ListView; import javafx.scene.control.TextArea; import javafx.scene.input.MouseEvent; import javafx.scene.layout.BorderPane; +import org.controlsfx.control.StatusBar; import java.util.HashMap; import java.util.Map; @@ -47,11 +49,12 @@ public class SequentMatcher extends BorderPane { @FXML private TextArea matchpattern; @FXML - private ListView> matchingsView; + private ListView matchingsView; @FXML private Label nomatchings; //only shown when no matchings found, else always hidden private Map cursorPosition = new HashMap<>(); + public SequentMatcher(Services services) { this.services = services; @@ -66,8 +69,13 @@ public class SequentMatcher extends BorderPane { ); goalView.getSelectionModel().selectedItemProperty().addListener((prop, old, nnew) -> - selectedGoalNodeToShow.setValue(nnew) - ); + { + if (nnew != null) { + selectedGoalNodeToShow.setValue(nnew); + } else { + selectedGoalNodeToShow.setValue(old); + } + }); goalView.setCellFactory(GoalNodeListCell::new); @@ -118,11 +126,12 @@ public class SequentMatcher extends BorderPane { public void startMatch() { sequentView.clearHighlight(); + KeyMatcherFacade kmf = KeyMatcherFacade.builder().environment(getSelectedGoalNodeToShow().getData().getEnv()).sequent(getSelectedGoalNodeToShow().getData().getNode().sequent()).build(); + Matchings matchings = kmf.matches(matchpattern.getText(), null); + //MatcherFacade.matches(matchpattern.getText(), getSelectedGoalNodeToShow().getData().getNode().sequent(), true, + //services); - Matchings matchings = MatcherFacade.matches(matchpattern.getText(), getSelectedGoalNodeToShow().getData().getNode().sequent(), true, - services); - - ObservableList> resultlist = FXCollections.observableArrayList(matchings); + ObservableList resultlist = FXCollections.observableArrayList(matchings.getMatchings()); //If no matchings found, addCell "No matchings found" if (resultlist.isEmpty()) { @@ -131,17 +140,17 @@ public class SequentMatcher extends BorderPane { } else { nomatchings.setVisible(false); matchingsView.setItems(resultlist); - matchingsView.setCellFactory(param -> new ListCell>() { + matchingsView.setCellFactory(param -> new ListCell() { //needed to hide position information of match paths @Override - protected void updateItem(Map item, boolean empty) { + protected void updateItem(Match item, boolean empty) { super.updateItem(item, empty); if (empty || item == null) { setText(null); } else { - setText("Match " + (resultlist.indexOf(item) +1) + setText("Match " + (resultlist.indexOf(item) + 1) + ": " + matchingsToString(item)); } } @@ -155,6 +164,7 @@ public class SequentMatcher extends BorderPane { /** * Removes position information of the MatchPath + * * @param match * @return string without position information */ @@ -208,11 +218,11 @@ public class SequentMatcher extends BorderPane { return selectedGoalNodeToShow; } - public ListView> getMatchingsView() { + public ListView getMatchingsView() { return matchingsView; } - public void setMatchingsView(ListView> matchingsView) { + public void setMatchingsView(ListView matchingsView) { this.matchingsView = matchingsView; } diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentOptionsMenu.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentOptionsMenu.java index 92e5c8f90f51feceb95a3fdb20e5e1eaf5f43c1e..079293cce68b6dfb6936dcb2798454d6284458ec 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentOptionsMenu.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentOptionsMenu.java @@ -8,6 +8,7 @@ import javafx.fxml.FXML; import javafx.scene.Scene; import javafx.scene.control.*; import javafx.stage.Stage; +import org.controlsfx.control.StatusBar; public class SequentOptionsMenu extends ContextMenu { @@ -27,6 +28,7 @@ public class SequentOptionsMenu extends ContextMenu { try { // passt schon! + KeyData data = (KeyData) model.getSelectedGoalNodeToShow().getData(); SequentMatcher root1 = new SequentMatcher(data.getProof().getServices()); root1.setGoals(model.getGoals()); @@ -47,8 +49,11 @@ public class SequentOptionsMenu extends ContextMenu { } catch (Exception e) { - e.printStackTrace(); - System.out.println(e); + Utils.showExceptionDialog("Please Select a Goal first." , + "Please Select a Goal node from the list first to open the SequentMatcher Window.", + "Please Select a Goal node from the list first to open the SequentMatcher Window.", e); + // e.printStackTrace(); + // System.out.println(e); } } }); diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java index 698739a5b40bc93f56d5880b986e31e306164d17..624f68199adc827664c5250be1b3088b7bb75de0 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java @@ -9,9 +9,10 @@ import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.settings.ProofIndependentSettings; import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade; -import edu.kit.iti.formal.psdbg.termmatcher.MatcherFacade; -import edu.kit.iti.formal.psdbg.termmatcher.Matchings; -import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath; +import edu.kit.iti.formal.psdbg.interpreter.matcher.KeyMatcherFacade; +import edu.kit.iti.formal.psdbg.interpreter.matcher.Match; +import edu.kit.iti.formal.psdbg.interpreter.matcher.MatchPath; +import edu.kit.iti.formal.psdbg.interpreter.matcher.Matchings; import javafx.beans.Observable; import javafx.beans.property.SimpleObjectProperty; import javafx.beans.value.ObservableBooleanValue; @@ -26,7 +27,6 @@ import org.key_project.util.collection.ImmutableSLList; import java.io.StringWriter; import java.util.Collections; -import java.util.Map; /** * @author Alexander Weigl @@ -136,7 +136,6 @@ public class SequentView extends CodeArea { filter.setSequent(sequent); - ProgramPrinter prgPrinter = new ProgramPrinter(new StringWriter()); this.backend = new LogicPrinter.PosTableStringBackend(80); //unicode makes prettier syntax but is bad for matching @@ -208,12 +207,17 @@ public class SequentView extends CodeArea { } if (node.get().sequent() != null) { - Matchings m = MatcherFacade.matches(pattern, node.get().sequent(), true, services); - if (m.size() == 0) return false; - Map va = m.first(); + KeyMatcherFacade kmf = KeyMatcherFacade.builder().environment(this.getKeYProofFacade().getEnvironment()) + .sequent(node.get().sequent()).build(); + Matchings m = kmf.matches(pattern, null); + +// Matchings m = + //MatcherFacade.matches(pattern, node.get().sequent(), true, services); + if (m.isEmpty() || m.isNoMatch()) return false; + Match va = m.getMatchings().iterator().next(); //System.out.println(va);//TODO remove for (MatchPath mp : va.values()) { - System.out.println(mp.pio()); + System.out.println("SequentView"+ mp.pio()); highlightTerm(mp.pio()); } } diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentViewForMatcher.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentViewForMatcher.java index e402d2e8a7f5c7f5462de227a6cf003dc6335f80..333abe36ecac2bb4af3ffe3c6a8a351ae974749f 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentViewForMatcher.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentViewForMatcher.java @@ -9,9 +9,6 @@ import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.settings.ProofIndependentSettings; import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade; -import edu.kit.iti.formal.psdbg.termmatcher.MatcherFacade; -import edu.kit.iti.formal.psdbg.termmatcher.Matchings; -import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath; import javafx.beans.Observable; import javafx.beans.property.SimpleObjectProperty; import javafx.beans.value.ObservableBooleanValue; @@ -131,14 +128,9 @@ public class SequentViewForMatcher extends CodeArea { } - - - - - - - public LogicPrinter.PosTableStringBackend getBackend() { return backend; } + + } diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/Utils.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/Utils.java index 8680487b645fbed8d825fa425ae5abbe90fb1443..cbe1d3afc048f7172b5da2053ddfaf453ddc4c8f 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/Utils.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/Utils.java @@ -253,34 +253,14 @@ public class Utils { public static void showClosedProofDialog(String scriptName) { Alert alert = new Alert(Alert.AlertType.INFORMATION); + alert.setTitle("Proof Closed"); alert.setHeaderText("The proof is closed"); alert.setContentText("The proof using " + scriptName + " is closed"); - alert.setWidth(400); + alert.setWidth(500); alert.setHeight(400); + alert.setResizable(true); - /*StringWriter sw = new StringWriter(); - PrintWriter pw = new PrintWriter(sw); - ex.printStackTrace(pw); - String exceptionText = sw.toString(); - - Label label = new Label("The exception stacktrace was:"); - TextArea textArea = new TextArea(exceptionText); - textArea.setEditable(false); - textArea.setWrapText(true); - - textArea.setMaxWidth(Double.MAX_VALUE); - textArea.setMaxHeight(Double.MAX_VALUE); - GridPane.setVgrow(textArea, Priority.ALWAYS); - GridPane.setHgrow(textArea, Priority.ALWAYS); - - GridPane expContent = new GridPane(); - expContent.setMaxWidth(Double.MAX_VALUE); - expContent.addCell(label, 0, 0); - expContent.addCell(textArea, 0, 1); - - alert.getDialogPane().setExpandableContent(expContent); - */ alert.showAndWait(); } @@ -318,7 +298,7 @@ public class Utils { public static void intoClipboard(String s) { Map map = Collections.singletonMap(DataFormat.PLAIN_TEXT, s); Clipboard.getSystemClipboard().setContent(map); - System.err.println(s); + logger.info("Clipboard "+s); } /** diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/model/DebuggerMainModel.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/model/DebuggerMainModel.java index e1dc2723063f7595c87f7d8ed8e25ad931ba649f..ba7f69483eb4412ccfd930011892f35deedbd863 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/model/DebuggerMainModel.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/model/DebuggerMainModel.java @@ -25,6 +25,9 @@ public class DebuggerMainModel { */ private final ObjectProperty chosenContract = new SimpleObjectProperty<>(this, "chosenContract"); + /** + * Properties for stepping enabling and disabling + */ private ObjectProperty> debuggerFramework = new SimpleObjectProperty<>(); private ObjectProperty> statePointer = new SimpleObjectProperty<>(); @@ -41,9 +44,9 @@ public class DebuggerMainModel { InterpreterThreadState.NO_THREAD); /** - * True, iff the execution is not possible + * True, iff the execution of script is not possible */ - private ObservableBooleanValue executeNotPossible = new SimpleBooleanProperty();//proofTreeController.executeNotPossibleProperty().or(FACADE.readyToExecuteProperty().not()); + private BooleanProperty executeNotPossible = new SimpleBooleanProperty(true);//proofTreeController.executeNotPossibleProperty().or(FACADE.readyToExecuteProperty().not()); /** * @@ -56,7 +59,7 @@ public class DebuggerMainModel { private StringProperty javaCode = new SimpleStringProperty(this, "javaCode"); - private BooleanProperty debugMode = new SimpleBooleanProperty(this, "debugMode", false); + //private BooleanProperty debugMode = new SimpleBooleanProperty(this, "debugMode", false); public DebuggerFramework getDebuggerFramework() { return debuggerFramework.get(); @@ -170,7 +173,7 @@ public class DebuggerMainModel { return executeNotPossible.get(); } - public ObservableBooleanValue executeNotPossibleProperty() { + public BooleanProperty executeNotPossibleProperty() { return executeNotPossible; } @@ -198,6 +201,7 @@ public class DebuggerMainModel { return javaCode; } +/* public boolean isDebugMode() { return debugMode.get(); } @@ -210,6 +214,7 @@ public class DebuggerMainModel { return debugMode; } +*/ public InterpreterThreadState getInterpreterState() { return interpreterState.get(); } diff --git a/ui/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.examples.Example b/ui/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.examples.Example index b1e6b00887d2b2a3c6783a82374446fcfe5d8256..2e00750d20dfa79b6832899146a07131533ddb5d 100644 --- a/ui/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.examples.Example +++ b/ui/src/main/resources/META-INF/services/edu.kit.iti.formal.psdbg.examples.Example @@ -1,13 +1,13 @@ edu.kit.iti.formal.psdbg.examples.contraposition.ContrapositionExample edu.kit.iti.formal.psdbg.examples.fol.FirstOrderLogicExample edu.kit.iti.formal.psdbg.examples.java.simple.JavaSimpleExample -edu.kit.iti.formal.psdbg.examples.java.transitive.PaperExample -edu.kit.iti.formal.psdbg.examples.java.dpqs.DualPivotExample +#edu.kit.iti.formal.psdbg.examples.java.transitive.PaperExample +#edu.kit.iti.formal.psdbg.examples.java.dpqs.DualPivotExample edu.kit.iti.formal.psdbg.examples.java.quicksort.QuickSort edu.kit.iti.formal.psdbg.examples.agatha.AgathaExample -edu.kit.iti.formal.psdbg.examples.java.bubbleSort.BubbleSortExample -edu.kit.iti.formal.psdbg.examples.java.sumAndMax.SumAndMaxExample -edu.kit.iti.formal.psdbg.examples.lulu.LuLuDoubleLinkedList -edu.kit.iti.formal.psdbg.examples.lulu.LuLuQuickSort -edu.kit.iti.formal.psdbg.examples.lulu.LuLuSumAndMax +#edu.kit.iti.formal.psdbg.examples.java.bubbleSort.BubbleSortExample +#edu.kit.iti.formal.psdbg.examples.java.sumAndMax.SumAndMaxExample +#edu.kit.iti.formal.psdbg.examples.lulu.LuLuDoubleLinkedList +#edu.kit.iti.formal.psdbg.examples.lulu.LuLuQuickSort +#edu.kit.iti.formal.psdbg.examples.lulu.LuLuSumAndMax #edu.kit.iti.formal.psdbg.examples.lulu.bigIntProof.BigIntExample \ No newline at end of file diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps index 4400390ad4bf3be43d0228c5a13ba29c4d5b12a9..2b3f7e70198e47fdd29be577017486e9552f6422 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps @@ -1,14 +1,3 @@ -// Please select one of the following scripts. -// -script testSMT(){ - smt solver='Z3'; -} -script toRemove(){ - impRight; - useContract type='dependency' on=`p`; - -} - script autoScript(){ __STRICT_MODE := true; auto; @@ -26,7 +15,7 @@ impRight; impRight; impLeft; cases{ - case match `==> not(?Z), ?Z`: + case match `==> !(?Z), ?Z`: notRight; default: @@ -35,3 +24,13 @@ cases{ } } + +script usageOfTryInCases(){ +cases{ + try: impLeft; //if this mutator is successful, do this operation otherwise use next case + + default: + __KEY_MAX_STEPS:= 100; + impRight; + } +} \ No newline at end of file diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script_for_Testing.kps b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script_for_Testing.kps new file mode 100644 index 0000000000000000000000000000000000000000..baefca7f31dfc9a72fb11ea8edf4de5ce2dd3e48 --- /dev/null +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script_for_Testing.kps @@ -0,0 +1,46 @@ +// Please select one of the following scripts. +// +script testTry(){ +cases{ + try: impLeft; + default: + __KEY_MAX_STEPS:= 100; + impRight; +} +} + +script testSMT(){ + smt solver='Z3'; +} +script toRemove(){ + impRight; + useContract type='dependency' on=`p`; + +} + +script autoScript(){ + __STRICT_MODE := true; + auto; +} + +script interactive(){ + impRight; + impRight; + impLeft; + +} + +script interactive_with_match(){ +impRight; +impRight; +impLeft; +cases{ + case match `==> !(?Z), ?Z`: + notRight; + + default: + notLeft; + + } + +} diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/proof-settings.props b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/proof-settings.props new file mode 100644 index 0000000000000000000000000000000000000000..fce90e392f02ee2ee3e7fa389053861657854565 --- /dev/null +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/proof-settings.props @@ -0,0 +1,37 @@ +#Proof-Settings-Config-File +#Mon Feb 05 16:31:07 CET 2018 +[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON +[StrategyProperty]VBT_PHASE=VBT_SYM_EX +[SMTSettings]useUninterpretedMultiplication=true +[SMTSettings]SelectedTaclets= +[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT +[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF +[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER +[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_INVARIANT +[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF +[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF +[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS +[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_NONE +[SMTSettings]instantiateHierarchyAssumptions=true +[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF +[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON +[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT +[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE +[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF +[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF +[Strategy]Timeout=-1 +[Strategy]MaximumNumberOfAutomaticApplications=10000 +[SMTSettings]integersMaximum=2147483645 +[Choice]DefaultChoices=assertions-assertions\:safe , initialisation-initialisation\:disableStaticInitialisation , intRules-intRules\:arithmeticSemanticsIgnoringOF , programRules-programRules\:Java , runtimeExceptions-runtimeExceptions\:allow , JavaCard-JavaCard\:off , Strings-Strings\:on , modelFields-modelFields\:treatAsAxiom , bigint-bigint\:on , sequences-sequences\:on , moreSeqRules-moreSeqRules\:on , reach-reach\:on , integerSimplificationRules-integerSimplificationRules\:full , permissions-permissions\:off , wdOperator-wdOperator\:L , wdChecks-wdChecks\:off , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\:off +[SMTSettings]useConstantsForBigOrSmallIntegers=true +[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT +[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON +[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE +[SMTSettings]maxGenericSorts=2 +[SMTSettings]integersMinimum=-2147483645 +[SMTSettings]invariantForall=false +[SMTSettings]UseBuiltUniqueness=false +[SMTSettings]explicitTypeHierarchy=false +[Strategy]ActiveStrategy=JavaCardDLStrategy +[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED +[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/script.kps b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/script.kps index bbf483791605a2e9a174306ad885a64dbb905168..5eb96e09f7375d873d6f1d368ea1701a5d411784 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/script.kps +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/quicksort/script.kps @@ -10,12 +10,14 @@ script split_from_quicksort() { } - cases{ - case match `==> seqDef(_,_,_) = seqDef(_, _, _)`: +cases{ + case match `? ==> seqDef{?;}(?,?,?) = seqDef{?;}(?, ?, ?)`: + __KEY_MAX_STEPS:=10000; auto; - case match `==> (\exists ?X (\exists ?Y _))`: + case match `? ==> (\exists ?X:int; (\exists ?Y:int; ?))`: instantiate var=X with=`i_0`; instantiate var=Y with=`j_0`; + __KEY_MAX_STEPS:=60000; auto; } } diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/debugger-ui.less b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/debugger-ui.less index e2771c26b693f908fdcc3cb59b96f1c459a261fe..2149f33ccf909befa25b97c140035eb06b9fe380 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/debugger-ui.less +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/debugger-ui.less @@ -1,6 +1,8 @@ @base03: rgb(0, 43, 54); @base02: rgb(7, 54, 66); -@base01: rgb(88, 110, 117); +@base01: #000000; + +//@base01: rgb(88, 110, 117); @base00: rgb(101, 123, 131); @base0: rgb(131, 148, 150); @base1: rgb(147, 161, 161); @@ -15,9 +17,11 @@ @cyan: rgb(42, 161, 152); @green: rgb(38, 187, 108); @basenavy: #f6f8ff; +//screenshot @basenavy: #ffffff; @keywordColor: #200080; @stringliteralColor: #6679aa; @integerLiteralColor: #008c00; +@screenShotMarkerBase: #97ffc6; .solarized-dark() { background-color: @base03; @@ -35,7 +39,7 @@ -fx-font-family: "Inconsolata", monospace; //-fx-font-family: "Fira Code Medium", monospace; -fx-font-size: 12pt; - //-fx-font-size: 18pt; + // -fx-font-size: 20pt; -fx-fill: @base00; .lineno { @@ -112,7 +116,9 @@ } .line-highlight-postmortem { - -rtfx-background-color: @cyan; +// -rtfx-background-color: @cyan; + -rtfx-background-color: @screenShotMarkerBase; + } .line-unhighlight { @@ -120,7 +126,8 @@ } .line-highlight-mainScript { - -rtfx-background-color: @green; +// -rtfx-background-color: @green; + -rtfx-background-color: @screenShotMarkerBase; } } @@ -139,7 +146,7 @@ // -fx-background-color: @base3; -fx-font-family: "Inconsolata", monospace; -fx-font-size: 12pt; - //-fx-font-size: 18pt; + //-fx-font-size: 20pt; -fx-fill: @base01; .ABSTRACT, .ASSERT, .BOOLEAN, .BREAK, .BYTE, .CASE, .CATCH, .CHAR, .CLASS, .CONST, @@ -192,7 +199,9 @@ -fx-underline: true; } .line-highlight { - -rtfx-background-color: @cyan; +// -rtfx-background-color: @cyan; + -rtfx-background-color: @screenShotMarkerBase; + } .line-un-highlight { -rtfx-background-color: @basenavy; @@ -234,7 +243,7 @@ .sequent-view { -fx-font-size: 14pt; - //-fx-font-size: 18pt; +// -fx-font-size: 20pt; -fx-background-color: @basenavy; -fx-fill: black; diff --git a/website/docs/index.md b/website/docs/index.md index 2bd3a8fce3c13d98c39d1269fdf86a7f169eb619..54fdb51b5648bf1acb61030e97caefadd4d2d3c1 100644 --- a/website/docs/index.md +++ b/website/docs/index.md @@ -56,10 +56,9 @@ The main features of the language are: 1. integration of domain specific entities like goal, formula, term and rule as first-class citizens into the language; 1. an expressive proof goal selection mechanism - * to identify and select individual proof branches, - * to easily switch between proof branches, - * to select multiple branches for uniform treatment (multi-matching); - that is resilient to small changes in the proof + - to identify and select individual proof branches, + - to easily switch between proof branches, + - to select multiple branches for uniform treatment (multi-matching); that is resilient to small changes in the proof 1. a repetition construct which allows repeated application of proof strategies; 1. support for proof exploration within the language. @@ -71,7 +70,9 @@ the analysis of failed proof attempts. ## Publications A full description of the language and debugging-concept -is published at [HVC 2017](http://rdcu.be/E4fF) +is published at [HVC 2017](http://rdcu.be/E4fF). +A short tool description is also [available]( +http://arxiv.org/abs/1804.04402). ## Debugging Script for Quicksort's `split` method. @@ -208,18 +209,33 @@ interactive rule applications.

Downloads

    -
  • PSDBG - Version 1.0.1c-FM - psdbg-1.0.1c-fm.jar +
  • PSDBG - Experimental Version + psdbg-Experimental-1.1.jar
    - Special Version for the tool paper at Formal Methods 2018. - Including examples and all dependencies. + This version is an experimental development version of PSDBG, including examples. + Its enhancements are based on an evaluation of the first version. + Not all provided features in this version may be completely functional yet. +
    + One major change is the syntax for Matching Expressions. The wildcard symbol is now "?" instead of "_". +
    + Requires Java version 1.8.0_111 or higher; Not working with Java 9, because of depdendencies. +
    + License: GPLv3 + Third Party Licenses +
    + Executable with java -jar psdbg-Experimental-1.1.jar +
    • +
  • PSDBG - Version 1.0.2c-FM + psdbg-1.0.2c-fm.jar +
    + First implementation of PSDBG, including examples.
    Requires Java version 1.8.0_111 or higher; Not working with Java 9, because of depdendencies.
    License: GPLv3 Third Party Licenses
    - Executable with java -jar psdbg-1.0.1c-fm.jar + Executable with java -jar psdbg-1.0.2c-fm.jar
diff --git a/website/docs/logo.svg b/website/docs/logo.svg new file mode 100644 index 0000000000000000000000000000000000000000..73a244204a1bc0288af3999a25840b693ee8341f --- /dev/null +++ b/website/docs/logo.svg @@ -0,0 +1,863 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + image/svg+xml + + + + + + + + { + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +