Commit e141acf7 authored by LULUDBR\Lulu's avatar LULUDBR\Lulu

Merge remote-tracking branch 'origin/master'

parents 7c42f49c 298ba538
......@@ -53,6 +53,7 @@ build:jdk8:
test:
stage: test
script: gradle check
allow_failure: true
cache:
key: "$CI_COMMIT_REF_NAME"
policy: pull
......
# 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
allprojects {
apply plugin: 'maven'
group = 'edu.kit.iti.formal.psdbg'
version = '1.0-FM'
version = 'Experimental-1.1'
}
subprojects {
......
......@@ -93,6 +93,7 @@ public class ASTDiff extends DefaultASTVisitor<ASTNode> {
return null;
}
@Override
public ASTNode visit(TheOnlyStatement theOnly) {
return null;
......
......@@ -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<ScriptLanguageParser.StmtListContext>
implements Visitable, Iterable<Statement> {
private final List<Statement> statements = new ArrayList<>();
public Statements(Statements body) {
statements.addAll(body.statements);
}
public Iterator<Statement> iterator() {
return statements.iterator();
}
......
......@@ -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));
......
......@@ -3,5 +3,5 @@ description = ''
dependencies {
compile project(':rt')
compile project(':keydeps')
compile project(':matcher')
// compile project(':matcher')
}
......@@ -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;
......
......@@ -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<ProofApi> task = new Task<ProofApi>() {
@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;
}
......
......@@ -99,7 +99,6 @@ public class KeyInterpreter extends Interpreter<KeyData> {
logger.debug(String.format("Beginning of suspicion execution of %s", statements));
GoalNode<KeyData> goalNode = getSelectedNode();
pushState(new State<>(goalNode.deepCopy())); // copy for later prove
List<Visitor> backupExitListener = getExitListeners(),
backupEntryListener = getEntryListeners();
try {
......
......@@ -89,7 +89,7 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
Iterator<Node> nodeIterator = start.leavesIterator();
while (nodeIterator.hasNext()) {
Node n = nodeIterator.next();
LOGGER.error(n.isClosed());
LOGGER.error("Node "+ n.serialNr()+" was closed "+ n.isClosed());
}
} else {
......
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;
......
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();
}
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<Match> matchings) {
throw new IllegalStateException();
}
@Override
public Collection<Match> getMatchings() {
ArrayList<Match> l = new ArrayList<Match>();
l.add(new Match());
return l;
}
@Override
public Matchings reduceConform(Matchings other) {
return other;
}
@Override
public String toString() {
return "{{}}";
}
}
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<KeyData> {
}
@Override
public List<VariableAssignment> matchSeq(GoalNode<KeyData> currentState,
String data,
Signature sig) {
//System.out.println("State that will be matched " + currentState.getData().getNode().sequent() + " with pattern " + data);
public List<VariableAssignment> matchSeq(GoalNode<KeyData> 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<String, MatchPath> 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<KeyData> {
Value<String> 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<String> 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<VariableAssignment> retList = new LinkedList();
LOGGER.info("Matched Variables " + va.toString());
......
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<Term> 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<String> hasToplevelComma(String pattern) {
ArrayList<String> 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;
}
}
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<T,S> {
private Map<Class<?>, TermAcceptor<T,S>> 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<? extends Operator> 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, S> {
T visit(Term term, S arg) throws InvocationTargetException, IllegalAccessException;
}
}
package edu.kit.iti.formal.psdbg.interpreter.matcher;
import java.util.TreeMap;
public class Match extends TreeMap<String, MatchPath> {
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;
}
}
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<T, P> {
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<? extends P, ?> parent;
private final T unit;
private final int posInParent;
private MatchPath(MatchPath<? extends P, ?> 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<QuantifiableVariable, Object> {
public MPQuantifiableVariable(MatchPath<? extends Object, ?> 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<Term, Object> {
public MPTerm(MatchPath<? extends Object, ?> 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());
}