diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractArrayFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractArrayFormulaManager.java index dca5dcd68b..3d7ded2ed8 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractArrayFormulaManager.java @@ -8,7 +8,7 @@ package org.sosy_lab.java_smt.basicimpl; -import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.checkVariableName; +import static org.sosy_lab.java_smt.basicimpl.FormulaCreator.escapeName; import org.sosy_lab.java_smt.api.ArrayFormula; import org.sosy_lab.java_smt.api.ArrayFormulaManager; @@ -65,8 +65,8 @@ protected abstract TFormulaInfo store( FTI extends FormulaType, FTE extends FormulaType> ArrayFormula makeArray(String pName, FTI pIndexType, FTE pElementType) { - checkVariableName(pName); - final TFormulaInfo namedArrayFormula = internalMakeArray(pName, pIndexType, pElementType); + final TFormulaInfo namedArrayFormula = + internalMakeArray(escapeName(pName), pIndexType, pElementType); return getFormulaCreator().encapsulateArray(namedArrayFormula, pIndexType, pElementType); } diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java index 19a797a485..585e352f86 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java @@ -9,7 +9,6 @@ package org.sosy_lab.java_smt.basicimpl; import static com.google.common.base.Preconditions.checkArgument; -import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.checkVariableName; import com.google.common.base.Preconditions; import com.google.common.collect.Lists; @@ -294,8 +293,7 @@ public BitvectorFormula makeVariable(BitvectorType type, String pVar) { @Override public BitvectorFormula makeVariable(int pLength, String pVar) { - checkVariableName(pVar); - return wrap(makeVariableImpl(pLength, pVar)); + return wrap(makeVariableImpl(pLength, FormulaCreator.escapeName(pVar))); } protected abstract TFormulaInfo makeVariableImpl(int pLength, String pVar); diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractBooleanFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractBooleanFormulaManager.java index 2a6f552249..e894c3a645 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractBooleanFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractBooleanFormulaManager.java @@ -10,7 +10,6 @@ import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkState; -import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.checkVariableName; import com.google.common.collect.Collections2; import com.google.common.collect.ImmutableList; @@ -40,6 +39,7 @@ import org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor; import org.sosy_lab.java_smt.api.visitors.FormulaVisitor; import org.sosy_lab.java_smt.api.visitors.TraversalProcess; +import org.sosy_lab.java_smt.basicimpl.FormulaCreator.SymbolViewVisitor; @SuppressWarnings("ClassTypeParameterName") public abstract class AbstractBooleanFormulaManager @@ -60,8 +60,7 @@ private BooleanFormula wrap(TFormulaInfo formulaInfo) { @Override public BooleanFormula makeVariable(String pVar) { - checkVariableName(pVar); - return wrap(makeVariableImpl(pVar)); + return wrap(makeVariableImpl(FormulaCreator.escapeName(pVar))); } protected abstract TFormulaInfo makeVariableImpl(String pVar); @@ -279,21 +278,26 @@ public final T ifThenElse(BooleanFormula pBits, T f1, T f2) @Override public R visit(BooleanFormula pFormula, BooleanFormulaVisitor visitor) { - return formulaCreator.visit(pFormula, new DelegatingFormulaVisitor<>(visitor)); + return formulaCreator.visit( + pFormula, new SymbolViewVisitor<>(new DelegatingFormulaVisitor<>(visitor))); } @Override public void visitRecursively( BooleanFormula pF, BooleanFormulaVisitor pFormulaVisitor) { formulaCreator.visitRecursively( - new DelegatingFormulaVisitor<>(pFormulaVisitor), pF, p -> p instanceof BooleanFormula); + new SymbolViewVisitor<>(new DelegatingFormulaVisitor<>(pFormulaVisitor)), + pF, + p -> p instanceof BooleanFormula); } @Override public BooleanFormula transformRecursively( BooleanFormula f, BooleanFormulaTransformationVisitor pVisitor) { return formulaCreator.transformRecursively( - new DelegatingFormulaVisitor<>(pVisitor), f, p -> p instanceof BooleanFormula); + new SymbolViewVisitor<>(new DelegatingFormulaVisitor<>(pVisitor)), + f, + p -> p instanceof BooleanFormula); } private class DelegatingFormulaVisitor implements FormulaVisitor { diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractEnumerationFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractEnumerationFormulaManager.java index 0dd8e5263b..141a64a735 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractEnumerationFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractEnumerationFormulaManager.java @@ -10,10 +10,12 @@ import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkNotNull; -import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.checkVariableName; +import static org.sosy_lab.java_smt.basicimpl.FormulaCreator.escapeName; import com.google.common.base.Preconditions; import com.google.common.collect.ImmutableMap; +import com.google.common.collect.ImmutableSet; +import com.google.common.collect.Iterables; import java.util.LinkedHashMap; import java.util.Map; import java.util.Set; @@ -77,8 +79,9 @@ private void checkSameEnumerationType(EnumerationFormula pF1, EnumerationFormula @Override public EnumerationFormulaType declareEnumeration(String pName, Set pElementNames) { - checkVariableName(pName); - return declareEnumerationImpl(pName, pElementNames); + return declareEnumerationImpl( + escapeName(pName), + ImmutableSet.copyOf(Iterables.transform(pElementNames, FormulaCreator::escapeName))); } protected EnumerationFormulaType declareEnumerationImpl(String pName, Set pElementNames) { @@ -114,8 +117,7 @@ protected TFormulaInfo makeConstantImpl(String pName, EnumerationFormulaType pTy @Override public EnumerationFormula makeVariable(String pVar, EnumerationFormulaType pType) { - checkVariableName(pVar); - return wrap(makeVariableImpl(pVar, pType)); + return wrap(makeVariableImpl(escapeName(pVar), pType)); } protected TFormulaInfo makeVariableImpl(String pVar, EnumerationFormulaType pType) { diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java index d1e0b5eb9d..86e7873454 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java @@ -8,7 +8,7 @@ package org.sosy_lab.java_smt.basicimpl; -import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.checkVariableName; +import static org.sosy_lab.java_smt.basicimpl.FormulaCreator.escapeName; import com.google.common.base.Preconditions; import java.math.BigDecimal; @@ -153,8 +153,7 @@ protected abstract TFormulaInfo makeNumberAndRound( @Override public FloatingPointFormula makeVariable(String pVar, FormulaType.FloatingPointType pType) { - checkVariableName(pVar); - return wrap(makeVariableImpl(pVar, pType)); + return wrap(makeVariableImpl(escapeName(pVar), pType)); } protected abstract TFormulaInfo makeVariableImpl( diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java index 62330f2a38..79d5a425af 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java @@ -11,12 +11,8 @@ import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkNotNull; -import com.google.common.annotations.VisibleForTesting; -import com.google.common.base.CharMatcher; import com.google.common.base.Preconditions; -import com.google.common.collect.ImmutableBiMap; import com.google.common.collect.ImmutableMap; -import com.google.common.collect.ImmutableSet; import com.google.common.collect.Iterables; import java.io.IOException; import java.util.Arrays; @@ -46,6 +42,7 @@ import org.sosy_lab.java_smt.api.visitors.FormulaTransformationVisitor; import org.sosy_lab.java_smt.api.visitors.FormulaVisitor; import org.sosy_lab.java_smt.api.visitors.TraversalProcess; +import org.sosy_lab.java_smt.basicimpl.FormulaCreator.SymbolViewVisitor; import org.sosy_lab.java_smt.basicimpl.tactics.NNFVisitor; import org.sosy_lab.java_smt.utils.SolverUtils; @@ -58,49 +55,6 @@ public abstract class AbstractFormulaManager implements FormulaManager { - /** - * Avoid using basic mathematical or logical operators of SMT-LIB2 as names for symbols. - * - *

We do not accept some names as identifiers for variables or UFs, because they easily - * misguide the user. Most solvers even would allow such identifiers directly, currently only - * SMTInterpol has problems with some of them. For consistency, we disallow those names for all - * solvers. - */ - @VisibleForTesting - public static final ImmutableSet BASIC_OPERATORS = - ImmutableSet.of("!", "+", "-", "*", "/", "%", "=", "<", ">", "<=", ">="); - - /** - * Avoid using basic keywords of SMT-LIB2 as names for symbols. - * - *

We do not accept some names as identifiers for variables or UFs, because they easily - * misguide the user. Most solvers even would allow such identifiers directly, currently only - * SMTInterpol has problems with some of them. For consistency, we disallow those names for all - * solvers. - */ - @VisibleForTesting - public static final ImmutableSet SMTLIB2_KEYWORDS = - ImmutableSet.of("true", "false", "and", "or", "select", "store", "xor", "distinct", "let"); - - /** - * Avoid using escape characters of SMT-LIB2 as part of names for symbols. - * - *

We do not accept some names as identifiers for variables or UFs, because they easily - * misguide the user. Most solvers even would allow such identifiers directly, currently only - * SMTInterpol has problems with some of them. For consistency, we disallow those names for all - * solvers. - */ - private static final CharMatcher DISALLOWED_CHARACTERS = CharMatcher.anyOf("|\\"); - - /** Mapping of disallowed char to their escaped counterparts. */ - /* Keep this map in sync with {@link #DISALLOWED_CHARACTERS}. - * Counterparts can be any unique string. For optimization, we could even use plain chars. */ - @VisibleForTesting - public static final ImmutableBiMap DISALLOWED_CHARACTER_REPLACEMENT = - ImmutableBiMap.of('|', "pipe", '\\', "backslash"); - - private static final char ESCAPE = '$'; // just some allowed symbol, can be any char - private final @Nullable AbstractArrayFormulaManager arrayManager; @@ -327,7 +281,12 @@ private String sanitize(String formulaStr) { @Override public BooleanFormula parse(String formulaStr) throws IllegalArgumentException { - return formulaCreator.encapsulateBoolean(parseImpl(sanitize(formulaStr))); + BooleanFormula r = formulaCreator.encapsulateBoolean(parseImpl(sanitize(formulaStr))); + formulaCreator.extractVariablesAndUFs( + r, + true, + (pS, pFormula) -> checkArgument(FormulaCreator.isValidName(FormulaCreator.dequote(pS)))); + return r; } protected abstract String dumpFormulaImpl(TFormulaInfo t) throws IOException; @@ -441,18 +400,18 @@ protected TFormulaInfo simplify(TFormulaInfo f) throws InterruptedException, Sol @Override public R visit(Formula input, FormulaVisitor visitor) { - return formulaCreator.visit(input, visitor); + return formulaCreator.visit(input, new SymbolViewVisitor<>(visitor)); } @Override public void visitRecursively(Formula pF, FormulaVisitor pFormulaVisitor) { - formulaCreator.visitRecursively(pFormulaVisitor, pF); + formulaCreator.visitRecursively(new SymbolViewVisitor<>(pFormulaVisitor), pF); } @Override public T transformRecursively( T f, FormulaTransformationVisitor pFormulaVisitor) { - return formulaCreator.transformRecursively(pFormulaVisitor, f); + return formulaCreator.transformRecursively(new SymbolViewVisitor<>(pFormulaVisitor), f); } /** @@ -463,7 +422,8 @@ public T transformRecursively( @Override public ImmutableMap extractVariables(Formula f) { ImmutableMap.Builder found = ImmutableMap.builder(); - formulaCreator.extractVariablesAndUFs(f, false, found::put); + formulaCreator.extractVariablesAndUFs( + f, false, (pS, pFormula) -> found.put(FormulaCreator.unescapeName(pS), pFormula)); return found.buildOrThrow(); // visitation should not visit any symbol twice } @@ -475,7 +435,8 @@ public ImmutableMap extractVariables(Formula f) { @Override public ImmutableMap extractVariablesAndUFs(Formula f) { ImmutableMap.Builder found = ImmutableMap.builder(); - formulaCreator.extractVariablesAndUFs(f, true, found::put); + formulaCreator.extractVariablesAndUFs( + f, true, (pS, pFormula) -> found.put(FormulaCreator.unescapeName(pS), pFormula)); // We can find duplicate keys with different values, like UFs with distinct parameters. // In such a case, we use only one appearance (the last one). return found.buildKeepingLast(); @@ -491,7 +452,6 @@ public BooleanFormula translateFrom(BooleanFormula formula, FormulaManager other @Override public T makeVariable(FormulaType formulaType, String name) { - checkVariableName(name); Formula t; if (formulaType.isBooleanType()) { t = booleanManager.makeVariable(name); @@ -582,114 +542,21 @@ private Formula replace(Formula f) { /** * Check whether the given String can be used as symbol/name for variables or undefined functions. * We disallow some keywords from SMTLib2 and other basic operators to be used as symbols. - * - *

This method must be kept in sync with {@link #checkVariableName}. */ @Override public final boolean isValidName(String pVar) { - if (pVar.isEmpty()) { - return false; - } - if (BASIC_OPERATORS.contains(pVar)) { - return false; - } - if (SMTLIB2_KEYWORDS.contains(pVar)) { - return false; - } - if (DISALLOWED_CHARACTERS.matchesAnyOf(pVar)) { - return false; - } - return true; - } - - /** - * This method is similar to {@link #isValidName} and throws an exception for invalid symbol - * names. While {@link #isValidName} can be used from users, this method should be used internally - * to validate user-given symbol names. - * - *

This method must be kept in sync with {@link #isValidName}. - */ - @VisibleForTesting - public static void checkVariableName(final String variableName) { - final String help = "Use FormulaManager#isValidName to check your identifier before using it."; - Preconditions.checkArgument( - !variableName.isEmpty(), "Identifier for variable should not be empty."); - Preconditions.checkArgument( - !BASIC_OPERATORS.contains(variableName), - "Identifier '%s' can not be used, because it is a simple operator. %s", - variableName, - help); - Preconditions.checkArgument( - !SMTLIB2_KEYWORDS.contains(variableName), - "Identifier '%s' can not be used, because it is a keyword of SMT-LIB2. %s", - variableName, - help); - Preconditions.checkArgument( - DISALLOWED_CHARACTERS.matchesNoneOf(variableName), - "Identifier '%s' can not be used, " - + "because it should not contain an escape character %s of SMT-LIB2. %s", - variableName, - DISALLOWED_CHARACTER_REPLACEMENT - .keySet(), // toString prints UTF8-encoded escape sequence, better than nothing. - help); + return FormulaCreator.isValidName(pVar); } /* This escaping works for simple escape sequences only, i.e., keywords are unique enough. */ @Override public final String escape(String pVar) { - // as long as keywords stay simple, this simple escaping is sufficient - if (pVar.isEmpty() || BASIC_OPERATORS.contains(pVar) || SMTLIB2_KEYWORDS.contains(pVar)) { - return ESCAPE + pVar; - } - if (pVar.indexOf(ESCAPE) != -1) { - pVar = pVar.replace("" + ESCAPE, "" + ESCAPE + ESCAPE); - } - if (DISALLOWED_CHARACTERS.matchesAnyOf(pVar)) { - for (Map.Entry e : DISALLOWED_CHARACTER_REPLACEMENT.entrySet()) { - pVar = pVar.replace(e.getKey().toString(), ESCAPE + e.getValue()); - } - } - return pVar; // unchanged + return FormulaCreator.escapeName(pVar); } /* This unescaping works for simple escape sequences only, i.e., keywords are unique enough. */ @Override public final String unescape(String pVar) { - int idx = pVar.indexOf(ESCAPE); - if (idx != -1) { - // unescape BASIC_OPERATORS and SMTLIB2_KEYWORDS - if (idx == 0) { - String tmp = pVar.substring(1); - if (tmp.isEmpty() || BASIC_OPERATORS.contains(tmp) || SMTLIB2_KEYWORDS.contains(tmp)) { - return tmp; - } - } - - // unescape DISALLOWED_CHARACTERS - StringBuilder str = new StringBuilder(); - int i = 0; - while (i < pVar.length()) { - if (pVar.charAt(i) == ESCAPE) { - if (pVar.charAt(i + 1) == ESCAPE) { - str.append(ESCAPE); - i++; - } else { - String rest = pVar.substring(i + 1); - for (Map.Entry e : DISALLOWED_CHARACTER_REPLACEMENT.entrySet()) { - if (rest.startsWith(e.getValue())) { - str.append(e.getKey()); - i += e.getValue().length(); - break; - } - } - } - } else { - str.append(pVar.charAt(i)); - } - i++; - } - return str.toString(); - } - return pVar; // unchanged + return FormulaCreator.unescapeName(pVar); } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractNumeralFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractNumeralFormulaManager.java index 5c4cbe26b8..bf260bb400 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractNumeralFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractNumeralFormulaManager.java @@ -9,7 +9,6 @@ package org.sosy_lab.java_smt.basicimpl; import static com.google.common.base.Preconditions.checkNotNull; -import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.checkVariableName; import com.google.common.base.Preconditions; import com.google.common.collect.ImmutableList; @@ -171,8 +170,7 @@ private static BigInteger convertBigDecimalToBigInteger(BigDecimal d) @Override public ResultFormulaType makeVariable(String pVar) { - checkVariableName(pVar); - return wrap(makeVariableImpl(pVar)); + return wrap(makeVariableImpl(FormulaCreator.escapeName(pVar))); } protected abstract TFormulaInfo makeVariableImpl(String i); diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractStringFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractStringFormulaManager.java index 9b68dfa57b..8b427129e4 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractStringFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractStringFormulaManager.java @@ -9,7 +9,6 @@ package org.sosy_lab.java_smt.basicimpl; import static com.google.common.base.Preconditions.checkArgument; -import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.checkVariableName; import com.google.common.collect.Iterables; import com.google.common.collect.Lists; @@ -110,8 +109,7 @@ public static String unescapeUnicodeForSmtlib(String input) { @Override public StringFormula makeVariable(String pVar) { - checkVariableName(pVar); - return wrapString(makeVariableImpl(pVar)); + return wrapString(makeVariableImpl(FormulaCreator.escapeName(pVar))); } protected abstract TFormulaInfo makeVariableImpl(String pVar); diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractUFManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractUFManager.java index 8843b2a100..97b904b8cb 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractUFManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractUFManager.java @@ -8,8 +8,6 @@ package org.sosy_lab.java_smt.basicimpl; -import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.checkVariableName; - import com.google.common.collect.Lists; import java.util.Arrays; import java.util.List; @@ -39,20 +37,19 @@ protected AbstractUFManager(FormulaCreator FunctionDeclaration declareUF( String pName, FormulaType pReturnType, List> pArgTypes) { - checkVariableName(pName); List argTypes = Lists.transform(pArgTypes, this::toSolverType); return FunctionDeclarationImpl.of( pName, FunctionDeclarationKind.UF, pArgTypes, pReturnType, - formulaCreator.declareUFImpl(pName, toSolverType(pReturnType), argTypes)); + formulaCreator.declareUFImpl( + FormulaCreator.escapeName(pName), toSolverType(pReturnType), argTypes)); } @Override public FunctionDeclaration declareUF( String pName, FormulaType pReturnType, FormulaType... pArgs) { - checkVariableName(pName); return declareUF(pName, pReturnType, Arrays.asList(pArgs)); } @@ -70,7 +67,6 @@ public final T callUF( @Override public T declareAndCallUF( String name, FormulaType pReturnType, List pArgs) { - checkVariableName(name); List> argTypes = Lists.transform(pArgs, getFormulaCreator()::getFormulaType); FunctionDeclaration func = declareUF(name, pReturnType, argTypes); return callUF(func, pArgs); @@ -79,7 +75,6 @@ public T declareAndCallUF( @Override public T declareAndCallUF( String name, FormulaType pReturnType, Formula... pArgs) { - checkVariableName(name); return declareAndCallUF(name, pReturnType, Arrays.asList(pArgs)); } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java index e5dd09e4ad..54ea57f7a2 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java @@ -11,6 +11,10 @@ import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkNotNull; +import com.google.common.annotations.VisibleForTesting; +import com.google.common.base.CharMatcher; +import com.google.common.collect.ImmutableBiMap; +import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableSet; import com.google.common.collect.Lists; import com.google.common.collect.Sets; @@ -77,6 +81,179 @@ public abstract class FormulaCreator { private final @Nullable TType regexType; protected final TEnv environment; + /** + * Avoid using escape characters of SMT-LIB2 as part of names for symbols. + * + *

We do not accept some names as identifiers for variables or UFs, because they easily + * misguide the user. Most solvers even would allow such identifiers directly, currently only + * SMTInterpol has problems with some of them. For consistency, we disallow those names for all + * solvers. + */ + @VisibleForTesting + public static final ImmutableList RESERVED = + ImmutableList.of( + // Keywords + "_", + "!", + "as", + "let", + "exists", + "forall", + "match", + "par", + + // Commands + "assert", + "check-sat", + "check-sat-assuming", + "declare-const", + "declare-datatype", + "declare-datatypes", + "declare-fun", + "declare-sort", + "define-fun", + "define-fun-rec", + "define-funs-rec", + "define-sort", + "echo", + "exit", + "get-assertions", + "get-assignment", + "get-info", + "get-model", + "get-option", + "get-proof", + "get-unsat-assumptions", + "get-unsat-core", + "get-value", + "pop", + "push", + "reset", + "reset-assertions", + "set-info", + "set-logic", + "set-option", + + // Predefined symbols + // Arrays + "select", + "store", + "const", + + // Bitvectors + "concat", + "extract", + "zero_extend", + "sign_extend", + "rotate_left", + "rotate_right", + "bv2int", + "int2bv", + "bvadd", + "bvsub", + "bvneg", + "bvmul", + "bvudiv", + "bvsdiv", + "bvurem", + "bvsrem", + "bvsmod", + "bvshl", + "bvlshr", + "bvashr", + "bvor", + "bvand", + "bvnot", + "bvxor", + "bvule", + "bvult", + "bvuge", + "bvugt", + "bvsle", + "bvslt", + "bvsge", + "bvsgt", + + // Core + "true", + "false", + "not", + "=>", + "and", + "or", + "xor", + "=", + "distinct", + "ite", + + // Floats + "roundNearestTiesToEven RoundingMode", + "roundNearestTiesToAway", + "roundTowardPositive", + "roundTowardNegative", + "roundTowardZero", + "RNE", + "RNA", + "RTP", + "RTN", + "RTZ", + "fp", + "+oo", + "-oo", + "+zero", + "-zero", + "NaN", + "to_fp", + "to_fp_unsigned", + // + any symbol starting with "fp." + + // Integers and Reals + "-", + "~", + "+", + "*", + "div", + "mod", + "/", + "abs", + "<=", + "<", + ">=", + ">", + "divisible", + "to_real", + "to_int", + "is_int" + + // Strings + // + any symbol starting with "str." + // + any symbol starting with "re." + ); + + /** + * Avoid using escape characters of SMT-LIB2 as part of names for symbols. + * + *

We do not accept some names as identifiers for variables or UFs, because they easily + * misguide the user. Most solvers even would allow such identifiers directly, currently only + * SMTInterpol has problems with some of them. For consistency, we disallow those names for all + * solvers. + */ + @VisibleForTesting + public static final CharMatcher DISALLOWED_CHARACTERS = CharMatcher.anyOf("|\\,"); + + /** + * Mapping of disallowed char to their escaped counterparts. + * + *

Keep this map in sync with {@link #DISALLOWED_CHARACTERS}. Counterparts can be any unique + * string. For optimization, we could even use plain chars. + */ + @VisibleForTesting + public static final ImmutableBiMap DISALLOWED_CHARACTER_REPLACEMENT = + ImmutableBiMap.of('|', "pipe", '\\', "backslash", ',', "comma"); + + @VisibleForTesting + public static final char ESCAPE = '$'; // just some allowed symbol, can be any char + protected FormulaCreator( TEnv env, TType boolType, @@ -288,6 +465,52 @@ protected FormulaType getFormulaType(T formula) { public abstract FormulaType getFormulaType(TFormulaInfo formula); + static class SymbolViewVisitor implements FormulaVisitor { + private final FormulaVisitor delegate; + + SymbolViewVisitor(FormulaVisitor pDelegate) { + delegate = pDelegate; + } + + @Override + public R visitFreeVariable(Formula f, String name) { + return delegate.visitFreeVariable(f, unescapeName(name)); + } + + @Override + public R visitBoundVariable(Formula f, int deBruijnIdx) { + return delegate.visitBoundVariable(f, deBruijnIdx); + } + + @Override + public R visitConstant(Formula f, Object value) { + return delegate.visitConstant(f, value); + } + + @Override + public R visitQuantifier( + BooleanFormula f, + Quantifier quantifier, + List boundVariables, + BooleanFormula body) { + return delegate.visitQuantifier(f, quantifier, boundVariables, body); + } + + @Override + public R visitFunction( + Formula f, List args, FunctionDeclaration functionDeclaration) { + return delegate.visitFunction( + f, + args, + FunctionDeclarationImpl.of( + unescapeName(functionDeclaration.getName()), + functionDeclaration.getKind(), + functionDeclaration.getArgumentTypes(), + functionDeclaration.getType(), + ((FunctionDeclarationImpl) functionDeclaration).getSolverDeclaration())); + } + } + /** * @see org.sosy_lab.java_smt.api.FormulaManager#visit */ @@ -560,11 +783,83 @@ public Object convertValue( } /** Variable names (symbols) can be wrapped with "|". This function removes those chars. */ - protected static String dequote(String s) { + @VisibleForTesting + public static String dequote(String s) { int l = s.length(); - if (s.charAt(0) == '|' && s.charAt(l - 1) == '|') { + if (l >= 2 && s.charAt(0) == '|' && s.charAt(l - 1) == '|') { return s.substring(1, l - 1); } return s; } + + private static boolean isReservedName(String pVar) { + return pVar.isEmpty() + || pVar.matches("^-?[0-9].*") + || pVar.startsWith("'") + || pVar.startsWith("fp.") + || pVar.startsWith("re.") + || pVar.startsWith("str.") + || RESERVED.contains(pVar); + } + + @VisibleForTesting + public static boolean isValidName(String pVar) { + return !isReservedName(pVar) && !DISALLOWED_CHARACTERS.matchesAnyOf(pVar); + } + + /* This escaping works for simple escape sequences only, i.e., keywords are unique enough. */ + @VisibleForTesting + public static String escapeName(String pVar) { + // as long as keywords stay simple, this simple escaping is sufficient + String prefix = ""; + if (isReservedName(pVar)) { + prefix += ESCAPE; + } + if (pVar.indexOf(ESCAPE) != -1) { + pVar = pVar.replace("" + ESCAPE, "" + ESCAPE + ESCAPE); + } + if (DISALLOWED_CHARACTERS.matchesAnyOf(pVar)) { + for (Map.Entry e : DISALLOWED_CHARACTER_REPLACEMENT.entrySet()) { + pVar = pVar.replace(e.getKey().toString(), ESCAPE + e.getValue()); + } + } + return prefix + pVar; + } + + static String unescapeName(String pVar) { + int idx = pVar.indexOf(ESCAPE); + if (idx != -1) { + // unescape BASIC_OPERATORS and SMTLIB2_KEYWORDS + if (idx == 0) { + String tmp = pVar.substring(1); + if (!isValidName(tmp)) { + pVar = tmp; + } + } + + // unescape DISALLOWED_CHARACTERS + StringBuilder str = new StringBuilder(); + for (int i = 0; i < pVar.length(); i++) { + if (pVar.charAt(i) == ESCAPE) { + if (pVar.charAt(i + 1) == ESCAPE) { + str.append(ESCAPE); + i++; + } else { + String rest = pVar.substring(i + 1); + for (Map.Entry e : DISALLOWED_CHARACTER_REPLACEMENT.entrySet()) { + if (rest.startsWith(e.getValue())) { + str.append(e.getKey()); + i += e.getValue().length(); + break; + } + } + } + } else { + str.append(pVar.charAt(i)); + } + } + return str.toString(); + } + return pVar; // unchanged + } } diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java index d231b49305..f7e8e20be0 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java @@ -401,7 +401,7 @@ public R visit(FormulaVisitor visitor, Formula formula, Term f) return visitor.visitConstant(formula, convertValue(f)); } else if (f.is_const()) { String name = f.symbol(); - return visitor.visitFreeVariable(formula, name); + return visitor.visitFreeVariable(formula, dequote(name)); } else if (f.is_variable()) { String name = f.symbol(); diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java index 29f2032780..4347fe1759 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java @@ -8,6 +8,7 @@ package org.sosy_lab.java_smt.solvers.princess; +import static com.google.common.base.Preconditions.checkArgument; import static scala.collection.JavaConverters.asJava; import static scala.collection.JavaConverters.collectionAsScalaIterableConverter; @@ -82,6 +83,7 @@ import org.sosy_lab.common.io.PathCounterTemplate; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; +import org.sosy_lab.java_smt.basicimpl.FormulaCreator; import ostrich.OFlags; import ostrich.OstrichStringTheory; import scala.Tuple2; @@ -323,6 +325,17 @@ public List parseStringToTerms(String s, PrincessFormulaC final List formulas = asJava(parserResult._1()); + // Check that all user defined function, constant and predicate symbols have valid names + for (IFunction f : asJava(parserResult._2().keySet())) { + checkArgument(FormulaCreator.isValidName(FormulaCreator.dequote(f.name()))); + } + for (ConstantTerm c : asJava(parserResult._3()).keySet()) { + checkArgument(FormulaCreator.isValidName(FormulaCreator.dequote(c.name()))); + } + for (Predicate p : asJava(parserResult._4()).keySet()) { + checkArgument(FormulaCreator.isValidName(FormulaCreator.dequote(p.name()))); + } + ImmutableSet.Builder declaredFunctions = ImmutableSet.builder(); for (IExpression f : formulas) { declaredFunctions.addAll(creator.extractVariablesAndUFs(f, true).values()); diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaManager.java index db166985cc..3c5ea3203d 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaManager.java @@ -57,7 +57,12 @@ BooleanFormula encapsulateBooleanFormula(IExpression t) { @Override public IExpression parseImpl(String pS) throws IllegalArgumentException { - List formulas = getEnvironment().parseStringToTerms(pS, creator); + List formulas; + try { + formulas = getEnvironment().parseStringToTerms(pS, creator); + } catch (Throwable pThrowable) { + throw new IllegalArgumentException(pThrowable); + } Preconditions.checkState( formulas.size() == 1, "parsing expects exactly one asserted term, but got %s terms", diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java index 8408917411..1713dfcdba 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java @@ -30,6 +30,7 @@ import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager; +import org.sosy_lab.java_smt.basicimpl.FormulaCreator; public class Yices2FormulaManager extends AbstractFormulaManager { @@ -133,7 +134,7 @@ assert getFormulaCreator().getFormulaType(formula) == FormulaType.BooleanType private static String quote(String str) { Preconditions.checkArgument(!Strings.isNullOrEmpty(str)); Preconditions.checkArgument(CharMatcher.anyOf("|\\").matchesNoneOf(str)); - Preconditions.checkArgument(!SMTLIB2_KEYWORDS.contains(str)); + Preconditions.checkArgument(FormulaCreator.isValidName(str)); if (VALID_CHARS.matchesAllOf(str) && !DIGITS.matches(str.charAt(0))) { // simple symbol diff --git a/src/org/sosy_lab/java_smt/test/EnumerationFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/EnumerationFormulaManagerTest.java index 0413e9adb3..93fd8caa42 100644 --- a/src/org/sosy_lab/java_smt/test/EnumerationFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/EnumerationFormulaManagerTest.java @@ -159,13 +159,6 @@ public void testIncompatibleEnumeration() { assertThrows(IllegalArgumentException.class, () -> emgr.equivalence(blue, circle)); } - @Test - public void testInvalidName() { - assertThrows(IllegalArgumentException.class, () -> emgr.declareEnumeration("true", "X", "Y")); - EnumerationFormulaType colorType = emgr.declareEnumeration("ColorE", "Blue", "White"); - assertThrows(IllegalArgumentException.class, () -> emgr.makeVariable("true", colorType)); - } - private static class ConstantsVisitor extends DefaultFormulaVisitor { final Set constants = new HashSet<>(); diff --git a/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java b/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java new file mode 100644 index 0000000000..9890558602 --- /dev/null +++ b/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java @@ -0,0 +1,241 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.test; + +import static com.google.common.truth.Truth.assertThat; +import static com.google.common.truth.TruthJUnit.assume; +import static org.junit.Assert.assertThrows; +import static org.sosy_lab.java_smt.basicimpl.FormulaCreator.dequote; + +import com.google.common.collect.FluentIterable; +import com.google.common.collect.ImmutableSet; +import java.util.Collection; +import org.junit.Before; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import org.junit.runners.Parameterized.Parameter; +import org.junit.runners.Parameterized.Parameters; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.basicimpl.FormulaCreator; + +@RunWith(Parameterized.class) +public class ParserSymbolsEscapedTest extends SolverBasedTest0 { + + public static ImmutableSet TEST_SYMBOLS = + ImmutableSet.of( + // Simple symbols from the standard: + "+", + "<=", + "x", + "plus", + "**", + "$", + "", + "abc77", + "*$s&6", + ".kkk", + ".8", + "+34", + "-32", + + // Quoted symbols from the standard: + "this is a quoted symbol", + "so is\nthis one", + "\" can occur too", + "af klj ^*0 asfe2 (&*)&(#^ $ > > >?\" ’]]984", + + // Some more edge cases + "", + " ", + ",", + "'", + "\n", + "ꯍ", + "#b101011", + "#b2", + "1", + ",1", + "01", + "1.0", + "01.0", + "#xA04", + "#xR04", + "#o70", + "_", + "forall", + "assert", + "define-fun-rec", + "store", + "concat", + "=", + "true", + "false", + "and", + "or", + "distinct"); + + @Parameters(name = "{0},{1}") + public static Collection data() { + ImmutableSet.Builder builder = ImmutableSet.builder(); + for (Solvers solver : Solvers.values()) { + for (String symbol : FluentIterable.concat(TEST_SYMBOLS)) { + for (String variant : + ImmutableSet.of( + symbol, + addQuotes(symbol), + FormulaCreator.escapeName(symbol), + addQuotes(FormulaCreator.escapeName(symbol)))) { + builder.add(new Object[] {solver, variant}); + } + } + } + return builder.build(); + } + + @Parameter(0) + public Solvers solver; + + @Parameter(1) + public String symbol; + + @Override + protected Solvers solverToUse() { + return solver; + } + + @Before + public void init() { + requireParser(); + } + + /** + * True if the symbol is a valid symbol according to the SMTLIB standard. + * + *

This function is stricter than {@link FormulaCreator#isValidName(String)} and won't allow + * names such as "a \nb" without any SMTLIB quotes. + */ + static boolean isValid(String pSymbol) { + if (pSymbol.length() >= 2 && pSymbol.startsWith("|") && pSymbol.endsWith("|")) { + return FormulaCreator.isValidName(dequote(pSymbol)); + } else { + return pSymbol.matches("^[~!@$%^&*_\\-+=<>.?\\/0-9a-zA-Z]+$") + && FormulaCreator.isValidName(pSymbol); + } + } + + /** + * Add quotes to the symbol + * + *

Assumes that the symbol is not already quoted. + */ + static String addQuotes(String pSymbol) { + return "|" + pSymbol + "|"; + } + + /** Returns True if the symbol is quoted */ + static boolean hasQuotes(String pSymbol) { + return pSymbol.length() >= 2 && pSymbol.startsWith("|") && pSymbol.endsWith("|"); + } + + /** + * Parse a variable definition in the SMTLIB format and return the term. + * + *

Returns a variable or a UF depending on the value of asUfSymbol + */ + private BooleanFormula parseSymbol(String pSymbol, boolean asUfSymbol) { + String sort = solver == Solvers.BITWUZLA ? "(_ BitVec 8)" : "Int"; + String query = + asUfSymbol + ? String.format( + "(declare-const c %s)(declare-fun %s (%s) Bool)(assert (%s c))", + sort, pSymbol, sort, pSymbol) + : String.format("(declare-const %s Bool)(assert %s)", pSymbol, pSymbol); + return mgr.parse(query); + } + + /* Only consider valid SMTLIB symbols for this test */ + private void forValidSymbols(String pSymbol) { + assume().that(isValid(pSymbol)).isTrue(); + } + + /* Only consider invalid symbols. */ + private void forInvalidSymbols(String pSymbol) { + assume().that(isValid(pSymbol)).isFalse(); + } + + @Test + @SuppressWarnings("CheckReturnValue") + public void testEscapedParserValid() { + forValidSymbols(symbol); + if (solver == Solvers.BITWUZLA) { + // TODO Report as a bug + assume().that(symbol).matches("^[~!@$%^&*_\\-+=<>.?\\/0-9a-zA-Z]+$"); + } + parseSymbol(symbol, false); + } + + @Test + @SuppressWarnings("CheckReturnValue") + public void testEscapedParserValidUf() { + forValidSymbols(symbol); + if (solver == Solvers.BITWUZLA) { + // TODO Report as a bug + assume().that(symbol).matches("^[~!@$%^&*_\\-+=<>.?\\/0-9a-zA-Z]+$"); + } + parseSymbol(symbol, true); + } + + @Test + public void testEscapedParserInvalid() { + forInvalidSymbols(symbol); + if (solver == Solvers.OPENSMT) { + // TODO Report as a bug + if (!hasQuotes(symbol)) { + assume().that(symbol).matches("^[~!@$%^&*_\\-+=<>.?\\/0-9a-zA-Z]+$"); + } + } + if (solver == Solvers.SMTINTERPOL) { + // TODO Report as a bug + assume().that(dequote(symbol)).isNoneOf("true", "false", "ꯍ"); + } + if (solver == Solvers.OPENSMT) { + // TODO Report as a bug + assume().that(dequote(symbol)).isNoneOf("true", "false"); + } + assertThrows(IllegalArgumentException.class, () -> parseSymbol(symbol, false)); + } + + @Test + public void testEscapedVariableVisitor() { + BooleanFormula f = mgr.getBooleanFormulaManager().makeVariable(symbol); + ImmutableSet variables = mgr.extractVariables(f).keySet(); + assertThat(variables).containsExactly(symbol); + } + + @Test + public void testEscapedDumpAndParse() { + if (solver == Solvers.BITWUZLA) { + // TODO This might already be fixed in another branch + // FIXME Fix the exception handler so that Bitwuzla doesn't crash the JVM + assume().that(symbol).matches("^[~!@$%^&*_\\-+=<>.?\\/0-9a-zA-Z]+$"); + } + if (solver == Solvers.PRINCESS) { + // FIXME Unicode parsing (or printing?) seems to be broken on the Windows test system + assume().that(dequote(symbol)).isNotEqualTo("ꯍ"); + } + BooleanFormula f = mgr.getBooleanFormulaManager().makeVariable(symbol); + BooleanFormula g = mgr.parse(mgr.dumpFormula(f).toString()); + assertThat(f).isEqualTo(g); + } +} diff --git a/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java index 1611b3e15b..c596a8d6bc 100644 --- a/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java @@ -265,10 +265,10 @@ public void testStringPrefixSuffixConcat() throws SolverException, InterruptedEx // FIXME: Princess will timeout on this test assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); - // check whether "prefix + suffix == concat" + // check whether "prefix + suffix == concatenated" StringFormula prefix = smgr.makeVariable("prefix"); StringFormula suffix = smgr.makeVariable("suffix"); - StringFormula concat = smgr.makeVariable("concat"); + StringFormula concat = smgr.makeVariable("concatenated"); assertThatFormula( bmgr.and( diff --git a/src/org/sosy_lab/java_smt/test/UFManagerTest.java b/src/org/sosy_lab/java_smt/test/UFManagerTest.java index 9a8fa079e5..6a56eb4783 100644 --- a/src/org/sosy_lab/java_smt/test/UFManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/UFManagerTest.java @@ -244,22 +244,6 @@ public void testDeclareAndCallUFWithBooleanAndBVTypes() { } } - @SuppressWarnings("CheckReturnValue") - @Test - public void testDeclareAndCallUFWithIntWithUnsupportedName() { - requireIntegers(); - assertThrows( - IllegalArgumentException.class, - () -> - fmgr.declareAndCallUF( - "|Func|", FormulaType.IntegerType, ImmutableList.of(imgr.makeNumber(1)))); - assertThrows( - IllegalArgumentException.class, - () -> - fmgr.declareUF( - "|Func|", FormulaType.IntegerType, ImmutableList.of(FormulaType.IntegerType))); - } - @Test public void testDeclareAndCallUFWithBv() { requireBitvectors(); @@ -276,26 +260,6 @@ public void testDeclareAndCallUFWithBv() { } } - @Test - @SuppressWarnings("CheckReturnValue") - public void testDeclareAndCallUFWithBvWithUnsupportedName() { - requireBitvectors(); - assertThrows( - IllegalArgumentException.class, - () -> - fmgr.declareAndCallUF( - "|Func|", - FormulaType.getBitvectorTypeWithSize(4), - ImmutableList.of(bvmgr.makeBitvector(4, 1)))); - assertThrows( - IllegalArgumentException.class, - () -> - fmgr.declareUF( - "|Func|", - FormulaType.getBitvectorTypeWithSize(4), - ImmutableList.of(FormulaType.getBitvectorTypeWithSize(4)))); - } - @Test public void testDeclareAndCallUFWithTypedArgs() { requireBooleanArgument(); diff --git a/src/org/sosy_lab/java_smt/test/VariableNamesEscaperTest.java b/src/org/sosy_lab/java_smt/test/VariableNamesEscaperTest.java index 0e3a6cd039..a96c4c73a6 100644 --- a/src/org/sosy_lab/java_smt/test/VariableNamesEscaperTest.java +++ b/src/org/sosy_lab/java_smt/test/VariableNamesEscaperTest.java @@ -10,26 +10,13 @@ import static com.google.common.truth.Truth.assertThat; -import com.google.common.collect.Lists; -import java.util.List; import org.junit.Test; -/** inherits many tests from {@link VariableNamesTest}. */ -public class VariableNamesEscaperTest extends VariableNamesTest { - - @Override - boolean allowInvalidNames() { - return false; - } - - @Override - protected List getAllNames() { - return Lists.transform(super.getAllNames(), mgr::escape); - } +public class VariableNamesEscaperTest extends SolverBasedTest0 { @Test public void testEscapeUnescape() { - for (String var : getAllNames()) { + for (String var : VariableNamesTest.getAllNames()) { assertThat(mgr.unescape(mgr.escape(var))).isEqualTo(var); assertThat(mgr.unescape(mgr.unescape(mgr.escape(mgr.escape(var))))).isEqualTo(var); } @@ -37,7 +24,7 @@ public void testEscapeUnescape() { @Test public void testDoubleEscapeUnescape() { - for (String var : getAllNames()) { + for (String var : VariableNamesTest.getAllNames()) { assertThat(mgr.unescape(mgr.escape(var))).isEqualTo(var); assertThat(mgr.unescape(mgr.unescape(mgr.escape(mgr.escape(var))))).isEqualTo(var); } diff --git a/src/org/sosy_lab/java_smt/test/VariableNamesInvalidTest.java b/src/org/sosy_lab/java_smt/test/VariableNamesInvalidTest.java deleted file mode 100644 index 49c1e19c2d..0000000000 --- a/src/org/sosy_lab/java_smt/test/VariableNamesInvalidTest.java +++ /dev/null @@ -1,72 +0,0 @@ -// This file is part of JavaSMT, -// an API wrapper for a collection of SMT solvers: -// https://github.com/sosy-lab/java-smt -// -// SPDX-FileCopyrightText: 2020 Dirk Beyer -// -// SPDX-License-Identifier: Apache-2.0 - -package org.sosy_lab.java_smt.test; - -import edu.umd.cs.findbugs.annotations.SuppressFBWarnings; -import org.junit.Test; -import org.sosy_lab.java_smt.api.Formula; -import org.sosy_lab.java_smt.api.FormulaType; - -@SuppressFBWarnings(value = "DLS_DEAD_LOCAL_STORE") -public class VariableNamesInvalidTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { - - // currently the only invalid String is the empty String - - @Test(expected = IllegalArgumentException.class) - public void testInvalidBoolVariable() { - @SuppressWarnings("unused") - Formula var = bmgr.makeVariable(""); - } - - @Test(expected = IllegalArgumentException.class) - public void testInvalidIntVariable() { - requireIntegers(); - @SuppressWarnings("unused") - Formula var = imgr.makeVariable(""); - } - - @Test(expected = IllegalArgumentException.class) - public void testInvalidRatVariable() { - requireRationals(); - @SuppressWarnings("unused") - Formula var = rmgr.makeVariable(""); - } - - @Test(expected = IllegalArgumentException.class) - public void testInvalidBVVariable() { - requireBitvectors(); - @SuppressWarnings("unused") - Formula var = bvmgr.makeVariable(4, ""); - } - - @Test(expected = IllegalArgumentException.class) - public void testInvalidFloatVariable() { - requireFloats(); - @SuppressWarnings("unused") - Formula var = fpmgr.makeVariable("", FormulaType.getSinglePrecisionFloatingPointType()); - } - - @Test(expected = IllegalArgumentException.class) - public void testInvalidIntArrayVariable() { - requireIntegers(); - requireArrays(); - @SuppressWarnings("unused") - Formula var = amgr.makeArray("", FormulaType.IntegerType, FormulaType.IntegerType); - } - - @Test(expected = IllegalArgumentException.class) - public void testInvalidBvArrayVariable() { - requireBitvectors(); - requireArrays(); - @SuppressWarnings("unused") - Formula var = - amgr.makeArray( - "", FormulaType.getBitvectorTypeWithSize(2), FormulaType.getBitvectorTypeWithSize(2)); - } -} diff --git a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java index 2f61eb09cd..076375985e 100644 --- a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java +++ b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java @@ -10,16 +10,14 @@ import static com.google.common.truth.Truth.assertThat; import static com.google.common.truth.TruthJUnit.assume; -import static org.junit.Assert.assertThrows; import static org.sosy_lab.java_smt.api.FormulaType.BooleanType; import static org.sosy_lab.java_smt.api.FormulaType.IntegerType; -import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableSet; import com.google.errorprone.annotations.CanIgnoreReturnValue; -import edu.umd.cs.findbugs.annotations.SuppressFBWarnings; import java.util.List; import java.util.Map; +import java.util.Set; import java.util.function.BiFunction; import java.util.function.Function; import org.junit.Test; @@ -34,154 +32,33 @@ import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.api.visitors.DefaultBooleanFormulaVisitor; import org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor; -import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager; +import org.sosy_lab.java_smt.basicimpl.FormulaCreator; -@SuppressFBWarnings(value = "DLS_DEAD_LOCAL_STORE") -public class VariableNamesTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { +// TODO Reduce the number of tests in this class. +// For variable name escaping we don't have to try every combination of Sort x Name. It should be +// enough to test the names once, and then check that escaping is applied for variables/ufs of all +// types. - private static final ImmutableList NAMES = - ImmutableList.of( - "java-smt", - "JavaSMT", - "sosylab", - "test", - "foo", - "bar", - "baz", - "declare", - "exit", - "(exit)", - "!=", - "~", - ",", - ".", - ":", - " ", - " ", - "(", - ")", - "[", - "]", - "{", - "}", - "[]", - "\"", - "\"\"", - "\"\"\"", - // TODO next line is disabled because of a problem in MathSAT5 (version 5.6.3). - // "'", "''", "'''", - "\n", - "\t", - "\u0000", - "\u0001", - "\u1234", - "\u2e80", - " this is a quoted symbol ", - " so is \n this one ", - " \" can occur too ", - " af klj ^*0 asfe2 (&*)&(#^ $ > > >?\" ’]]984"); - - private static final ImmutableSet FURTHER_SMTLIB2_KEYWORDS = - ImmutableSet.of( - "let", - "forall", - "exists", - "match", - "Bool", - "continued-execution", - "error", - "immediate-exit", - "incomplete", - "logic", - "memout", - "sat", - "success", - "theory", - "unknown", - "unsupported", - "unsat", - "_", - "as", - "BINARY", - "DECIMAL", - "HEXADECIMAL", - "NUMERAL", - "par", - "STRING", - "assert", - "check-sat", - "check-sat-assuming", - "declare-const", - "declare-datatype", - "declare-datatypes", - "declare-fun", - "declare-sort", - "define-fun", - "define-fun-rec", - "define-sort", - "echo", - "exit", - "get-assertions", - "get-assignment", - "get-info", - "get-model", - "get-option", - "get-proof", - "get-unsat-assumptions", - "get-unsat-core", - "get-value", - "pop", - "push", - "reset", - "reset-assertions", - "set-info", - "set-logic", - "set-option"); - - /** - * Some special chars are not allowed to appear in symbol names. See {@link - * AbstractFormulaManager#DISALLOWED_CHARACTERS}. - */ - @SuppressWarnings("javadoc") - private static final ImmutableSet UNSUPPORTED_NAMES = - ImmutableSet.of( - "|", - "||", - "|||", - "|test", - "|test|", - "t|e|s|t", - "\\", - "\\s", - "\\|\\|", - "| this is a quoted symbol |", - "| so is \n this one |", - "| \" can occur too |", - "| af klj ^*0 asfe2 (&*)&(#^ $ > > >?\" ’]]984|"); - - protected List getAllNames() { - return ImmutableList.builder() - .addAll(NAMES) - .addAll(AbstractFormulaManager.BASIC_OPERATORS) - .addAll(AbstractFormulaManager.SMTLIB2_KEYWORDS) - .addAll(AbstractFormulaManager.DISALLOWED_CHARACTER_REPLACEMENT.values()) - .addAll(FURTHER_SMTLIB2_KEYWORDS) - .addAll(UNSUPPORTED_NAMES) - .build(); - } +public class VariableNamesTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { - boolean allowInvalidNames() { - return true; + static Set getAllNames() { + ImmutableSet.Builder builder = ImmutableSet.builder(); + for (String symbol : ParserSymbolsEscapedTest.TEST_SYMBOLS) { + for (String variant : + ImmutableSet.of( + symbol, + ParserSymbolsEscapedTest.addQuotes(symbol), + FormulaCreator.escapeName(symbol), + ParserSymbolsEscapedTest.addQuotes(FormulaCreator.escapeName(symbol)))) { + builder.add(variant); + } + } + return builder.build(); } @CanIgnoreReturnValue private T createVariableWith(Function creator, String name) { - if (allowInvalidNames() && !mgr.isValidName(name)) { - assertThrows(IllegalArgumentException.class, () -> creator.apply(name)); - return null; - } else { - return creator.apply(name); - } + return creator.apply(name); } private void testName0( @@ -191,9 +68,6 @@ private void testName0( // create a variable T var = createVariableWith(creator, name); - if (var == null) { - return; - } // check whether it exists with the given name Map map = mgr.extractVariables(var); @@ -206,9 +80,6 @@ private void testName0( // check whether we can create the same variable again T var2 = createVariableWith(creator, name); - if (var2 == null) { - return; - } // for simple formulas, we can expect a direct equality // (for complex formulas this is not satisfied) @@ -227,10 +98,8 @@ private void testName0( @SuppressWarnings("unused") String dump = mgr.dumpFormula(eq.apply(var, var)).toString(); - if (allowInvalidNames()) { - // try to create a new (!) variable with a different name, the escaped previous name. - assertThat(createVariableWith(creator, "|" + name + "|")).isEqualTo(null); - } + // Adding SMTLIB quotes to the name should make it illegal + assertThat(mgr.isValidName(ParserSymbolsEscapedTest.addQuotes(name))).isFalse(); } @Test @@ -296,9 +165,7 @@ public void testNameIntArray() throws SolverException, InterruptedException { public void testNameBvArray() throws SolverException, InterruptedException { requireBitvectors(); requireArrays(); - // Someone who knows princess has to debug this! - assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); - for (String name : NAMES) { + for (String name : getAllNames()) { testName0( name, s -> @@ -314,7 +181,7 @@ public void testNameBvArray() throws SolverException, InterruptedException { @Test public void testNameUF1Bool() throws SolverException, InterruptedException { requireIntegers(); - for (String name : NAMES) { + for (String name : getAllNames()) { testName0( name, s -> fmgr.declareAndCallUF(s, BooleanType, imgr.makeNumber(0)), @@ -326,7 +193,7 @@ public void testNameUF1Bool() throws SolverException, InterruptedException { @Test public void testNameUF1Int() throws SolverException, InterruptedException { requireIntegers(); - for (String name : NAMES) { + for (String name : getAllNames()) { testName0( name, s -> fmgr.declareAndCallUF(s, IntegerType, imgr.makeNumber(0)), imgr::equal, true); } @@ -335,8 +202,6 @@ public void testNameUF1Int() throws SolverException, InterruptedException { @Test public void testNameUFBv() throws SolverException, InterruptedException { requireBitvectors(); - // Someone who knows princess has to debug this! - assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); for (String name : getAllNames()) { testName0( name, @@ -350,7 +215,7 @@ public void testNameUFBv() throws SolverException, InterruptedException { public void testNameUF2Bool() throws SolverException, InterruptedException { requireIntegers(); IntegerFormula zero = imgr.makeNumber(0); - for (String name : NAMES) { + for (String name : getAllNames()) { testName0( name, s -> fmgr.declareAndCallUF(s, BooleanType, zero, zero), bmgr::equivalence, true); } @@ -360,7 +225,7 @@ public void testNameUF2Bool() throws SolverException, InterruptedException { public void testNameUF2Int() throws SolverException, InterruptedException { requireIntegers(); IntegerFormula zero = imgr.makeNumber(0); - for (String name : NAMES) { + for (String name : getAllNames()) { testName0(name, s -> fmgr.declareAndCallUF(s, IntegerType, zero, zero), imgr::equal, true); } } @@ -371,11 +236,7 @@ public void testNameInQuantification() { requireIntegers(); for (String name : getAllNames()) { - IntegerFormula var = createVariableWith(imgr::makeVariable, name); - if (var == null) { - continue; - } IntegerFormula zero = imgr.makeNumber(0); BooleanFormula eq = imgr.equal(var, zero); BooleanFormula exists = qmgr.exists(var, eq); @@ -401,10 +262,7 @@ public Void visitQuantifier( Quantifier pQuantifier, List pBoundVariables, BooleanFormula pBody) { - if (solverToUse() != Solvers.PRINCESS) { - // TODO Princess does not (yet) return quantified variables. - assertThat(pBoundVariables).hasSize(1); - } + assertThat(pBoundVariables).hasSize(1); for (Formula f : pBoundVariables) { Map map = mgr.extractVariables(f); assertThat(map).hasSize(1); @@ -427,11 +285,7 @@ public void testNameInNestedQuantification() { requireIntegers(); for (String name : getAllNames()) { - IntegerFormula var1 = createVariableWith(imgr::makeVariable, name + 1); - if (var1 == null) { - continue; - } IntegerFormula var2 = createVariableWith(imgr::makeVariable, name + 2); IntegerFormula var3 = createVariableWith(imgr::makeVariable, name + 3); IntegerFormula var4 = createVariableWith(imgr::makeVariable, name + 4); @@ -487,10 +341,8 @@ public Void visitQuantifier( Quantifier pQuantifier, List pBoundVariables, BooleanFormula pBody) { - if (solverToUse() != Solvers.PRINCESS) { - // TODO Princess does not return quantified variables. - assertThat(pBoundVariables).hasSize(1); - } + assertThat(pBoundVariables).hasSize(1); + assertThat(pBoundVariables).hasSize(1); for (Formula f : pBoundVariables) { Map map = mgr.extractVariables(f); assertThat(map).hasSize(1); @@ -514,9 +366,6 @@ public void testBoolVariableNameInVisitor() { for (String name : getAllNames()) { BooleanFormula var = createVariableWith(bmgr::makeVariable, name); - if (var == null) { - continue; - } bmgr.visit( var, @@ -545,22 +394,17 @@ public void testBoolVariableDump() { assume().that(solverToUse()).isNotEqualTo(Solvers.YICES2); for (String name : getAllNames()) { BooleanFormula var = createVariableWith(bmgr::makeVariable, name); - if (var != null) { - @SuppressWarnings("unused") - String dump = mgr.dumpFormula(var).toString(); - } + @SuppressWarnings("unused") + String dump = mgr.dumpFormula(var).toString(); } } @Test public void testEqBoolVariableDump() { - // FIXME: Rewrite test? Most solvers will simplify the formula to `true`. for (String name : getAllNames()) { BooleanFormula var = createVariableWith(bmgr::makeVariable, name); - if (var != null) { - @SuppressWarnings("unused") - String dump = mgr.dumpFormula(bmgr.equivalence(var, var)).toString(); - } + @SuppressWarnings("unused") + String dump = mgr.dumpFormula(bmgr.equivalence(var, var)).toString(); } } @@ -610,8 +454,6 @@ public void testIntArrayVariable() { public void testBvArrayVariable() { requireArrays(); requireBitvectors(); - // Someone who knows princess has to debug this! - assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); for (String name : getAllNames()) { createVariableWith( v -> @@ -626,13 +468,7 @@ public void testBvArrayVariable() { @Test public void sameBehaviorTest() { for (String name : getAllNames()) { - if (mgr.isValidName(name)) { - // should pass without exception - AbstractFormulaManager.checkVariableName(name); - } else { - assertThrows( - IllegalArgumentException.class, () -> AbstractFormulaManager.checkVariableName(name)); - } + assertThat(mgr.isValidName(name)).isEqualTo(FormulaCreator.isValidName(name)); } } }