Skip to content

Commit

Permalink
fix bugs by KeYProject#3538
Browse files Browse the repository at this point in the history
  • Loading branch information
@wadoon
wadoon committed Jan 20, 2025
1 parent 45ce7d0 commit b6201c6
Show file tree
Hide file tree
Showing 7 changed files with 125 additions and 59 deletions.
149 changes: 108 additions & 41 deletions key.core/src/main/java/de/uka/ilkd/key/macros/scripts/EngineState.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,37 +3,41 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.macros.scripts;

import java.nio.file.Path;
import java.nio.file.Paths;
import java.util.Deque;
import java.util.LinkedList;
import java.util.Objects;
import java.util.Optional;
import java.util.function.Consumer;

import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.NamespaceSet;
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.macros.scripts.meta.ConversionException;
import de.uka.ilkd.key.macros.scripts.meta.Converter;
import de.uka.ilkd.key.macros.scripts.meta.NoSpecifiedConverterException;
import de.uka.ilkd.key.macros.scripts.meta.ValueInjector;
import de.uka.ilkd.key.nparser.KeYParser.ProofScriptExpressionContext;
import de.uka.ilkd.key.nparser.KeyIO;
import de.uka.ilkd.key.parser.ParserException;
import de.uka.ilkd.key.pp.AbbrevMap;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.settings.ProofSettings;

import org.key_project.logic.sort.Sort;
import org.key_project.util.collection.ImmutableList;

import org.antlr.v4.runtime.CharStreams;
import org.jspecify.annotations.NonNull;
import org.jspecify.annotations.NullMarked;
import org.jspecify.annotations.Nullable;
import org.key_project.logic.sort.Sort;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.java.StringUtil;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

import java.nio.file.Path;
import java.nio.file.Paths;
import java.util.Deque;
import java.util.LinkedList;
import java.util.Objects;
import java.util.Optional;
import java.util.function.Consumer;

/**
* @author Alexander Weigl
* @version 1 (28.03.17)
Expand All @@ -47,7 +51,7 @@ public class EngineState {

private final AbbrevMap abbrevMap = new AbbrevMap();
private final ValueInjector valueInjector = createDefaultValueInjector();

private final ExprEvaluator exprEvaluator = new ExprEvaluator(this);

private @Nullable Consumer<ProofScriptEngine.Message> observer;
private Path baseFileName = Paths.get(".");
Expand Down Expand Up @@ -77,9 +81,66 @@ private ValueInjector createDefaultValueInjector() {
v.addConverter(Term.class, String.class, (str) -> this.toTerm(str, null));
v.addConverter(Sequent.class, String.class, this::toSequent);
v.addConverter(Sort.class, String.class, this::toSort);

v.addConverter(Integer.TYPE, Integer.class, (Integer i) -> (int) i);
v.addConverter(Double.TYPE, Double.class, d -> d);
v.addConverter(Boolean.TYPE, Boolean.class, b -> b);

v.addConverter(Integer.TYPE, String.class, Integer::parseInt);
v.addConverter(Double.TYPE, String.class, Double::parseDouble);
v.addConverter(Boolean.TYPE, String.class, Boolean::parseBoolean);
v.addConverter(Integer.class, String.class, Integer::parseInt);
v.addConverter(Double.class, String.class, Double::parseDouble);
v.addConverter(Boolean.class, String.class, Boolean::parseBoolean);

addContextTranslator(v, String.class);
addContextTranslator(v, Term.class);
addContextTranslator(v, Integer.class);
addContextTranslator(v, Byte.class);
addContextTranslator(v, Long.class);
addContextTranslator(v, Boolean.class);
addContextTranslator(v, Character.class);
addContextTranslator(v, Sequent.class);
addContextTranslator(v, Integer.TYPE);
addContextTranslator(v, Byte.TYPE);
addContextTranslator(v, Long.TYPE);
addContextTranslator(v, Boolean.TYPE);
addContextTranslator(v, Character.TYPE);
addContextTranslator(v, Term.class);
addContextTranslator(v, Sequent.class);
addContextTranslator(v, Semisequent.class);
return v;
}

private <T> void addContextTranslator(ValueInjector v, Class<T> aClass) {
Converter<T, ProofScriptExpressionContext> converter =
(ProofScriptExpressionContext a) -> convertToString(v, aClass, a);
v.addConverter(aClass, ProofScriptExpressionContext.class, converter);
}

@SuppressWarnings("unchecked")
private <R, T> R convertToString(ValueInjector inj, Class<R> aClass, ProofScriptExpressionContext ctx)
throws Exception {
try {
if (aClass == String.class && ctx.string_literal() != null) {
return inj.getConverter(aClass, String.class)
.convert(StringUtil.trim(ctx.string_literal().getText(), '"'));
}
if (aClass == String.class) {
return inj.getConverter(aClass, String.class).convert(ctx.getText());
}

T value = (T) ctx.accept(exprEvaluator);
Class<T> tClass = (Class<T>) value.getClass();
if (aClass.isAssignableFrom(value.getClass())) {
return aClass.cast(value);
}
return inj.getConverter(aClass, tClass).convert(value);
} catch (ConversionException | NoSpecifiedConverterException e) {
return inj.getConverter(aClass, String.class).convert(ctx.getText());
}
}

protected static Goal getGoal(ImmutableList<Goal> openGoals, Node node) {
for (Goal goal : openGoals) {
if (goal.node() == node) {
Expand All @@ -103,10 +164,10 @@ public Proof getProof() {
*
* @param checkAutomatic Set to true if the returned {@link Goal} should be automatic.
* @return the first open goal, which has to be automatic iff checkAutomatic
* is true.
* is true.
* @throws ProofAlreadyClosedException If the proof is already closed when calling this method.
* @throws ScriptException If there is no such {@link Goal}, or something else goes
* wrong.
* @throws ScriptException If there is no such {@link Goal}, or something else goes
* wrong.
*/
@SuppressWarnings("unused")
public @NonNull Goal getFirstOpenGoal(boolean checkAutomatic) throws ScriptException {
Expand Down Expand Up @@ -168,38 +229,39 @@ private Goal findGoalFromRoot(final Node rootNode, boolean checkAutomatic) {
Goal result = null;
Node node = rootNode;

loop: while (node != null) {
loop:
while (node != null) {
if (node.isClosed()) {
return null;
}

int childCount = node.childrenCount();

switch (childCount) {
case 0 -> {
result = getGoal(proof.openGoals(), node);
if (!checkAutomatic || Objects.requireNonNull(result).isAutomatic()) {
// We found our goal
break loop;
case 0 -> {
result = getGoal(proof.openGoals(), node);
if (!checkAutomatic || Objects.requireNonNull(result).isAutomatic()) {
// We found our goal
break loop;
}
node = choices.pollLast();
}
node = choices.pollLast();
}
case 1 -> node = node.child(0);
default -> {
Node next = null;
for (int i = 0; i < childCount; i++) {
Node child = node.child(i);
if (!child.isClosed()) {
if (next == null) {
next = child;
} else {
choices.add(child);
case 1 -> node = node.child(0);
default -> {
Node next = null;
for (int i = 0; i < childCount; i++) {
Node child = node.child(i);
if (!child.isClosed()) {
if (next == null) {
next = child;
} else {
choices.add(child);
}
}
}
assert next != null;
node = next;
}
assert next != null;
node = next;
}
}
}

Expand All @@ -214,7 +276,7 @@ public Term toTerm(String string, @Nullable Sort sort) throws ParserException, S
return term;
else
throw new IllegalStateException(
"Unexpected sort for term: " + term + ". Expected: " + sort);
"Unexpected sort for term: " + term + ". Expected: " + sort);
}

private @NonNull KeyIO getKeyIO() throws ScriptException {
Expand Down Expand Up @@ -297,9 +359,14 @@ public ProofScriptEngine getEngine() {
}

public NamespaceSet getCurrentNamespaces() {
if (goal != null) {
return goal.getLocalNamespaces();
try {
return getFirstOpenAutomaticGoal().getLocalNamespaces();
} catch (ScriptException e) {
return proof.getNamespaces();
}
return proof.getNamespaces();
}

public ExprEvaluator getEvaluator() {
return exprEvaluator;
}
}
2 changes: 1 addition & 1 deletion key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ProofScriptEngine.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -176,7 +176,7 @@ public void execute(AbstractUserInterfaceControl uiControl,
String.format("Error while executing script: %s%n%nCommand: %s%nPosition: %s%n",
e.getMessage(),
prettyPrintCommand(commandContext),
BuilderHelpers.getPosition(commandContext)));
BuilderHelpers.getPosition(commandContext)),e);
}
}
}
Expand Down
1 change: 0 additions & 1 deletion key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -226,7 +226,6 @@ public Includes readIncludes() throws ProofInputException {

@Override
public File readBootClassPath() {
@NonNull
ProblemInformation pi = getProblemInformation();
String bootClassPath = pi.getBootClassPath();
if (bootClassPath == null) {
Expand Down
8 changes: 4 additions & 4 deletions key.core/src/main/resources/de/uka/ilkd/key/proof/rules/charListRules.key
View file
Original file line number Diff line number Diff line change
Expand Up @@ -168,7 +168,7 @@
\varcond(\notFreeIn(iv, l),
\notFreeIn(iv, c),
\notFreeIn(iv, i))
\replacewith(\ifExiv; (i >= 0
\replacewith(\ifEx iv; (i >= 0
& iv >= i
& iv < seqLen(l)
& int::seqGet(l, iv) = c)
Expand Down Expand Up @@ -275,7 +275,7 @@
\schemaVar \variables int iv;
\find(clIndexOfCl(sourceStr, i, searchStr))
\varcond(\notFreeIn(iv, searchStr), \notFreeIn(iv, sourceStr), \notFreeIn(iv, i))
\replacewith(\ifExiv; (iv >= i
\replacewith(\ifEx iv; (iv >= i
& iv >= 0
& iv + seqLen(searchStr) <= seqLen(sourceStr)
& (seqSub(sourceStr, iv, iv + seqLen(searchStr)) = searchStr))
Expand All @@ -294,7 +294,7 @@
\schemaVar \variables int iv;
\find(clLastIndexOfChar(sourceStr, c, i))
\varcond(\notFreeIn(iv, c), \notFreeIn(iv, i), \notFreeIn(iv, sourceStr))
\replacewith(\ifExiv; (iv > 0
\replacewith(\ifEx iv; (iv > 0
& i >= iv
& i - iv < seqLen(sourceStr)
& int::seqGet(sourceStr, i - iv) = c)
Expand All @@ -312,7 +312,7 @@
\schemaVar \variables int iv;
\find(clLastIndexOfCl(sourceStr, i, searchStr))
\varcond(\notFreeIn(iv, searchStr), \notFreeIn(iv, i), \notFreeIn(iv, sourceStr))
\replacewith(\ifExiv; (iv > 0
\replacewith(\ifEx iv; (iv > 0
& i - iv >= 0
& seqLen(searchStr) + i - iv <= seqLen(sourceStr)
& (seqSub(sourceStr, i - iv, seqLen(searchStr) + i - iv) = searchStr))
Expand Down
4 changes: 2 additions & 2 deletions key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ifThenElseRules.key
View file
Original file line number Diff line number Diff line change
Expand Up @@ -250,7 +250,7 @@
\sameUpdateLevel
\varcond(\notFreeIn(intVar, intValue))
\replacewith({\subst intVar; intValue}then);
\replacewith(\ifExintVar; (phi)\then(then)\else(else))
\replacewith(\ifEx intVar; (phi)\then(then)\else(else))
\add( ==> {\subst intVar; intValue}phi &
\forall intVar; (phi -> wellOrderLeqInt(intValue, intVar)))
};
Expand Down Expand Up @@ -281,7 +281,7 @@
\sameUpdateLevel
\varcond(\notFreeIn(intVar, intValue))
\replacewith({\subst intVar; intValue}b);
\replacewith(\ifExintVar; (phi)\then(b)\else(c))
\replacewith(\ifEx intVar; (phi)\then(b)\else(c))
\add( ==> {\subst intVar; intValue}phi &
\forall intVar; (phi -> wellOrderLeqInt(intValue, intVar)))
\displayname "ifExthenelse1_solve"
Expand Down
14 changes: 7 additions & 7 deletions key.core/src/main/resources/de/uka/ilkd/key/proof/rules/wdFormulaRules.key
View file
Original file line number Diff line number Diff line change
Expand Up @@ -127,7 +127,7 @@
wd_Logical_Op_ExCond_Expr {

\find(
wd(\ifExj; (a)\then(s)\else(t))
wd(\ifEx j; (a)\then(s)\else(t))
)
\varcond(
\notFreeIn(j, t)
Expand All @@ -142,7 +142,7 @@
wd_Logical_Op_ExCond_Form {

\find(
WD(\ifExj; (a)\then(b)\else(c))
WD(\ifEx j; (a)\then(b)\else(c))
)
\varcond(
\notFreeIn(j, c)
Expand Down Expand Up @@ -259,7 +259,7 @@
wd_Logical_Op_ExCond_Expr {

\find(
wd(\ifExj; (a)\then(s)\else(t))
wd(\ifEx j; (a)\then(s)\else(t))
)
\varcond(
\notFreeIn(j, t),
Expand All @@ -278,7 +278,7 @@
wd_Logical_Op_ExCond_Form {

\find(
WD(\ifExj; (a)\then(b)\else(c))
WD(\ifEx j; (a)\then(b)\else(c))
)
\varcond(
\notFreeIn(j, c),
Expand Down Expand Up @@ -465,7 +465,7 @@
wd_Logical_Op_ExCond_Expr {

\find(
wd(\ifExj; (a)\then(s)\else(t))
wd(\ifEx j; (a)\then(s)\else(t))
)
\varcond(
\notFreeIn(j, t),
Expand All @@ -484,7 +484,7 @@
wd_T_Logical_Op_ExCond_Form {

\find(
T(\ifExj; (a)\then(b)\else(c))
T(\ifEx j; (a)\then(b)\else(c))
)
\varcond(
\notFreeIn(j, c),
Expand All @@ -503,7 +503,7 @@
wd_F_Logical_Op_ExCond_Form {

\find(
F(\ifExj; (a)\then(b)\else(c))
F(\ifEx j; (a)\then(b)\else(c))
)
\varcond(
\notFreeIn(j, c),
Expand Down
6 changes: 3 additions & 3 deletions key.core/tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,14 +46,14 @@


\proofScript {
macro split-prop;
rule schiffl_lemma_2 formula=`seqPerm(f_s, f_t)`;
macro "split-prop";
rule schiffl_lemma_2 formula=`seqPerm(f_s,f_t)`;
instantiate hide var=x with=`f_x`;
instantiate hide var=y with=`f_y`;
rule impLeft;
tryclose branch;
rule exLeft;
macro split-prop;
macro "split-prop";
rule seqPermDef occ=1;
rule andRight;
tryclose branch;
Expand Down

0 comments on commit b6201c6

Please sign in to comment.