From f96547b3c522328e7b836a9e5dd29ac061e950e2 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 31 Dec 2024 15:55:19 +0100 Subject: [PATCH 01/16] Add more reserved keywords to the list of forbidden variable/UF names in AbstractFormulaManager --- .../basicimpl/AbstractFormulaManager.java | 173 +++++++++++++----- .../solvers/yices2/Yices2FormulaManager.java | 2 +- .../java_smt/test/VariableNamesTest.java | 3 +- 3 files changed, 133 insertions(+), 45 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java index 62330f2a38..265eda34df 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java @@ -15,8 +15,8 @@ import com.google.common.base.CharMatcher; import com.google.common.base.Preconditions; import com.google.common.collect.ImmutableBiMap; +import com.google.common.collect.ImmutableList; 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; @@ -58,29 +58,135 @@ 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("!", "+", "-", "*", "/", "%", "=", "<", ">", "<=", ">="); + 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", + // + any symbol starting with "bv" + "bvneg", + + // 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." + "fp.neg", + + // Integers and Reals + "-", + "+", + "*", + "div", + "mod", + "/", + "abs", + "<=", + "<", + ">=", + ">", + "divisible", + "to_real", + "to_int", + "is_int", + + // Strings + // + any symbol starting with "str." + "str.concat", + // + any symbol starting with "re." + "re.opt"); /** - * Avoid using basic keywords of SMT-LIB2 as names for symbols. + * Checks if the symbol name is a reserved keyword in SMTLIB2. * *

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"); + public static boolean isReserved(String pVar) { + return pVar.startsWith("bv") + || pVar.startsWith("fp.*") + || pVar.startsWith("str.") + || pVar.startsWith("re.") + || RESERVED.contains(pVar); + } /** * Avoid using escape characters of SMT-LIB2 as part of names for symbols. @@ -587,19 +693,7 @@ private Formula replace(Formula f) { */ @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; + return !pVar.isEmpty() && !DISALLOWED_CHARACTERS.matchesAnyOf(pVar) && !isReserved(pVar); } /** @@ -613,32 +707,27 @@ public final boolean isValidName(String pVar) { 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); + !variableName.isEmpty(), "Identifier for variable must not be empty."); 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", + + "because it contains an escape character %s of SMT-LIB2. %s", variableName, DISALLOWED_CHARACTER_REPLACEMENT .keySet(), // toString prints UTF8-encoded escape sequence, better than nothing. help); + Preconditions.checkArgument( + !isReserved(variableName), + "Identifier '%s' can not be used, because it is a reserved symbol in SMT-LIB2. " + "%s", + variableName, + help); } /* 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)) { + if (pVar.isEmpty() || isReserved(pVar)) { return ESCAPE + pVar; } if (pVar.indexOf(ESCAPE) != -1) { @@ -660,7 +749,7 @@ public final String unescape(String pVar) { // 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)) { + if (tmp.isEmpty() || isReserved(tmp)) { return tmp; } } 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..3136504150 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java @@ -133,7 +133,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(!isReserved(str)); if (VALID_CHARS.matchesAllOf(str) && !DIGITS.matches(str.charAt(0))) { // simple symbol diff --git a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java index 2f61eb09cd..fb4fe3caa2 100644 --- a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java +++ b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java @@ -162,8 +162,7 @@ public class VariableNamesTest extends SolverBasedTest0.ParameterizedSolverBased protected List getAllNames() { return ImmutableList.builder() .addAll(NAMES) - .addAll(AbstractFormulaManager.BASIC_OPERATORS) - .addAll(AbstractFormulaManager.SMTLIB2_KEYWORDS) + .addAll(AbstractFormulaManager.RESERVED) .addAll(AbstractFormulaManager.DISALLOWED_CHARACTER_REPLACEMENT.values()) .addAll(FURTHER_SMTLIB2_KEYWORDS) .addAll(UNSUPPORTED_NAMES) From e767a9ffe7b21b8b291b40bcbceb5976f47df575 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 31 Dec 2024 15:55:52 +0100 Subject: [PATCH 02/16] Remove "exit" from the list of legal variable names in VariableNamesTest --- src/org/sosy_lab/java_smt/test/VariableNamesTest.java | 1 - 1 file changed, 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java index fb4fe3caa2..f89af097f9 100644 --- a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java +++ b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java @@ -49,7 +49,6 @@ public class VariableNamesTest extends SolverBasedTest0.ParameterizedSolverBased "bar", "baz", "declare", - "exit", "(exit)", "!=", "~", From 4cd4fd2e1bb10b84dd91564285cc50c60bf5fcb6 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 1 Jan 2025 19:42:59 +0100 Subject: [PATCH 03/16] Explicitly blacklist all predefined bv functions as variable/uf names. Not allowing any variable names starting with "bv" lead to too many issues as the prefix is used frequently throughout the tests. --- .../basicimpl/AbstractFormulaManager.java | 31 +++++++++++++++++-- 1 file changed, 28 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java index 265eda34df..b81c3391d0 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java @@ -112,8 +112,34 @@ public abstract class AbstractFormulaManager Date: Wed, 1 Jan 2025 19:43:46 +0100 Subject: [PATCH 04/16] Rename a variable in one of the tests as its name "concat" is no longer allowed --- src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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( From a43cb6dc2528b851afdb0d2d759f3393dff46a3a Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 4 Jan 2025 18:31:32 +0100 Subject: [PATCH 05/16] Add a translation layer to automatically escape/unescape variable and Uf names. This is work in progress and will eventually allow us to support arbitrary names for variables. --- .../AbstractArrayFormulaManager.java | 6 +- .../AbstractBitvectorFormulaManager.java | 4 +- .../AbstractBooleanFormulaManager.java | 16 +- .../AbstractEnumerationFormulaManager.java | 12 +- .../AbstractFloatingPointFormulaManager.java | 5 +- .../basicimpl/AbstractFormulaManager.java | 281 +--------------- .../AbstractNumeralFormulaManager.java | 4 +- .../AbstractStringFormulaManager.java | 4 +- .../java_smt/basicimpl/AbstractUFManager.java | 9 +- .../java_smt/basicimpl/FormulaCreator.java | 294 ++++++++++++++++ .../solvers/yices2/Yices2FormulaManager.java | 3 +- .../test/ParserSymbolsEscapedTest.java | 317 ++++++++++++++++++ .../java_smt/test/VariableNamesTest.java | 23 +- 13 files changed, 669 insertions(+), 309 deletions(-) create mode 100644 src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java 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 b81c3391d0..79d5a425af 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java @@ -11,11 +11,7 @@ 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.ImmutableList; import com.google.common.collect.ImmutableMap; import com.google.common.collect.Iterables; import java.io.IOException; @@ -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,180 +55,6 @@ public abstract class AbstractFormulaManager implements FormulaManager { - @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", - "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." - "fp.neg", - - // Integers and Reals - "-", - "+", - "*", - "div", - "mod", - "/", - "abs", - "<=", - "<", - ">=", - ">", - "divisible", - "to_real", - "to_int", - "is_int", - - // Strings - // + any symbol starting with "str." - "str.concat", - // + any symbol starting with "re." - "re.opt"); - - /** - * Checks if the symbol name is a reserved keyword in SMTLIB2. - * - *

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. - */ - public static boolean isReserved(String pVar) { - return pVar.startsWith("fp.") - || pVar.startsWith("str.") - || pVar.startsWith("re.") - || RESERVED.contains(pVar); - } - - /** - * 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; @@ -458,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; @@ -572,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); } /** @@ -594,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 } @@ -606,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(); @@ -622,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); @@ -713,97 +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) { - return !pVar.isEmpty() && !DISALLOWED_CHARACTERS.matchesAnyOf(pVar) && !isReserved(pVar); - } - - /** - * 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 must not be empty."); - Preconditions.checkArgument( - DISALLOWED_CHARACTERS.matchesNoneOf(variableName), - "Identifier '%s' can not be used, " - + "because it contains an escape character %s of SMT-LIB2. %s", - variableName, - DISALLOWED_CHARACTER_REPLACEMENT - .keySet(), // toString prints UTF8-encoded escape sequence, better than nothing. - help); - Preconditions.checkArgument( - !isReserved(variableName), - "Identifier '%s' can not be used, because it is a reserved symbol in SMT-LIB2. " + "%s", - variableName, - 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() || isReserved(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() || isReserved(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..8f7a857733 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 */ @@ -567,4 +790,75 @@ protected static String dequote(String s) { } 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/yices2/Yices2FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java index 3136504150..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(!isReserved(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/ParserSymbolsEscapedTest.java b/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java new file mode 100644 index 0000000000..d7220375be --- /dev/null +++ b/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java @@ -0,0 +1,317 @@ +/* + * 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.RESERVED; + +import com.google.common.collect.FluentIterable; +import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableSet; +import java.util.Collection; +import org.junit.Before; +import org.junit.Test; +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; + +public class ParserSymbolsEscapedTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { + + 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", + "01", + "1.0", + "01.0", + "#xA04", + "#xR04", + "#o70"); + + private static final ImmutableList reserved = + ImmutableList.of( + // Reserved + "_", + "!", + "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 + // Array + "select", + "store", + // Bitvector + "concat", + "extract", + "bvnot", + "bvneg", + "bvand", + "bvor", + "bvadd", + "bvmul", + "bvudiv", + "bvurem", + "bvshl", + "bvlshr", + "true", + "false", + "not", + "=>", + "and", + "or", + "xor", + "=", + "distinct", + "ite" + // TODO: Add more theories + ); + + @Parameters(name = "{0},{1}") + public static Collection data() { + ImmutableSet.Builder builder = ImmutableSet.builder(); + for (Solvers solver : Solvers.values()) { + for (String symbol : + FluentIterable.concat( + RESERVED, + TEST_SYMBOLS, + VariableNamesTest.NAMES, + VariableNamesTest.UNSUPPORTED_NAMES)) { + 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(); + } + + /** Is this True if the symbol is a reserved keyword in the SMTLIB standard. */ + private static boolean isReserved(String pSymbol) { + return RESERVED.contains(pSymbol); + } + + /** True if the symbol is a simple symbol according to the SMTLIB standard. */ + private static boolean isSimple(String pSymbol) { + return pSymbol.matches("^[~!@$%^&*_\\-+=<>.?\\/0-9a-zA-Z]+$") + && !Character.isDigit(pSymbol.charAt(0)) + && !isReserved(pSymbol); + } + + /** + * True if the symbol is a valid symbol according to the SMTLIB standard. + * + *

Valid symbols can be either simple symbols or quoted symbols. + */ + private static boolean isValid(String pSymbol) { + if (pSymbol.length() >= 2 && pSymbol.startsWith("|") && pSymbol.endsWith("|")) { + return FormulaCreator.isValidName(removeQuotes(pSymbol)); + } else { + return pSymbol.matches("^[~!@$%^&*_\\-+=<>.?\\/0-9a-zA-Z]+$") + && FormulaCreator.isValidName(pSymbol); + } + } + + /** + * Remove quotes from the symbol. + * + *

If the symbol is not quoted, return it unchanged. + */ + private static String removeQuotes(String pSymbol) { + if (pSymbol.length() >= 2 && pSymbol.startsWith("|") && pSymbol.endsWith("|")) { + return pSymbol.substring(1, pSymbol.length() - 1); + } else { + return pSymbol; + } + } + + /** + * Add quotes to the symbol + * + *

Assumes that the symbol is not already quoted. + */ + private static String addQuotes(String pSymbol) { + return "|" + pSymbol + "|"; + } + + private static boolean hasQuotes(String pSymbol) { + return pSymbol.length() >= 2 && pSymbol.startsWith("|") && pSymbol.endsWith("|"); + } + + /** + * Return the canonical representation of the symbol. + * + *

The symbol will have quotes if and only if the same symbol without quotes would not be legal + * in SMTLIB. + */ + private static String canonical(String pSymbol) { + String noquotes = removeQuotes(pSymbol); + return isSimple(noquotes) ? noquotes : addQuotes(noquotes); + } + + /** Parse a variable definition in the SMTLIB format and return the term. */ + 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); + } + + private void forValidSymbols(String pSymbol) { + assume().that(isValid(pSymbol)).isTrue(); + } + + 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]+$"); + } + } + 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]+$"); + } + 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/VariableNamesTest.java b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java index f89af097f9..12716a02b8 100644 --- a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java +++ b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java @@ -8,6 +8,7 @@ package org.sosy_lab.java_smt.test; +import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.truth.Truth.assertThat; import static com.google.common.truth.TruthJUnit.assume; import static org.junit.Assert.assertThrows; @@ -34,12 +35,12 @@ 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 { - private static final ImmutableList NAMES = + public static final ImmutableList NAMES = ImmutableList.of( "java-smt", "JavaSMT", @@ -67,8 +68,9 @@ public class VariableNamesTest extends SolverBasedTest0.ParameterizedSolverBased "\"", "\"\"", "\"\"\"", - // TODO next line is disabled because of a problem in MathSAT5 (version 5.6.3). - // "'", "''", "'''", + "'", + "''", + "'''", "\n", "\t", "\u0000", @@ -139,10 +141,10 @@ public class VariableNamesTest extends SolverBasedTest0.ParameterizedSolverBased /** * Some special chars are not allowed to appear in symbol names. See {@link - * AbstractFormulaManager#DISALLOWED_CHARACTERS}. + * FormulaCreator#DISALLOWED_CHARACTERS}. */ @SuppressWarnings("javadoc") - private static final ImmutableSet UNSUPPORTED_NAMES = + public static final ImmutableSet UNSUPPORTED_NAMES = ImmutableSet.of( "|", "||", @@ -161,8 +163,8 @@ public class VariableNamesTest extends SolverBasedTest0.ParameterizedSolverBased protected List getAllNames() { return ImmutableList.builder() .addAll(NAMES) - .addAll(AbstractFormulaManager.RESERVED) - .addAll(AbstractFormulaManager.DISALLOWED_CHARACTER_REPLACEMENT.values()) + .addAll(FormulaCreator.RESERVED) + .addAll(FormulaCreator.DISALLOWED_CHARACTER_REPLACEMENT.values()) .addAll(FURTHER_SMTLIB2_KEYWORDS) .addAll(UNSUPPORTED_NAMES) .build(); @@ -626,10 +628,9 @@ public void sameBehaviorTest() { for (String name : getAllNames()) { if (mgr.isValidName(name)) { // should pass without exception - AbstractFormulaManager.checkVariableName(name); + checkArgument(FormulaCreator.isValidName(name)); } else { - assertThrows( - IllegalArgumentException.class, () -> AbstractFormulaManager.checkVariableName(name)); + assertThrows(IllegalArgumentException.class, () -> FormulaCreator.isValidName(name)); } } } From b12fbad87e988a85e5b431702473b0a05ccf7008 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 29 Dec 2024 22:39:42 +0100 Subject: [PATCH 06/16] Let Princess throw an IllegalArgumentException if a parsing error occurred --- .../java_smt/solvers/princess/PrincessFormulaManager.java | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) 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", From e8c89978d541f45154b88cef92349e459aab2a0a Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 29 Dec 2024 22:41:13 +0100 Subject: [PATCH 07/16] Fix FormulaCreator.dequote for symbol names have a length < 2 --- src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java index 8f7a857733..85b3423b96 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java @@ -785,7 +785,7 @@ public Object convertValue( /** Variable names (symbols) can be wrapped with "|". This function removes those chars. */ protected 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; From ad216947ad45114bf776ccab0b3f08c3d043671f Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 29 Dec 2024 22:42:04 +0100 Subject: [PATCH 08/16] In the Bitwuzla formula visitor remove symbol quotes when a free variable is visited --- .../java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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(); From f49600030f1a0f694b21789e93a1001d84f187b9 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 4 Jan 2025 20:59:16 +0100 Subject: [PATCH 09/16] Cleaned up ParserSymbolsEscapedTest an reduced the number of test inputs --- .../java_smt/basicimpl/FormulaCreator.java | 3 +- .../test/ParserSymbolsEscapedTest.java | 135 +++--------------- 2 files changed, 23 insertions(+), 115 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java index 85b3423b96..54ea57f7a2 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/basicimpl/FormulaCreator.java @@ -783,7 +783,8 @@ 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 (l >= 2 && s.charAt(0) == '|' && s.charAt(l - 1) == '|') { return s.substring(1, l - 1); diff --git a/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java b/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java index d7220375be..ef9d9b3697 100644 --- a/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java +++ b/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java @@ -13,21 +13,23 @@ 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.RESERVED; +import static org.sosy_lab.java_smt.basicimpl.FormulaCreator.dequote; import com.google.common.collect.FluentIterable; -import com.google.common.collect.ImmutableList; 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; -public class ParserSymbolsEscapedTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { +@RunWith(Parameterized.class) +public class ParserSymbolsEscapedTest extends SolverBasedTest0 { public static ImmutableSet TEST_SYMBOLS = ImmutableSet.of( @@ -46,110 +48,43 @@ public class ParserSymbolsEscapedTest extends SolverBasedTest0.ParameterizedSolv ".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"); - - private static final ImmutableList reserved = - ImmutableList.of( - // Reserved + "#o70", "_", - "!", - "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 - // Array - "select", "store", - // Bitvector "concat", - "extract", - "bvnot", - "bvneg", - "bvand", - "bvor", - "bvadd", - "bvmul", - "bvudiv", - "bvurem", - "bvshl", - "bvlshr", - "true", - "false", - "not", - "=>", - "and", - "or", - "xor", - "=", - "distinct", - "ite" - // TODO: Add more theories - ); + "="); @Parameters(name = "{0},{1}") public static Collection data() { ImmutableSet.Builder builder = ImmutableSet.builder(); for (Solvers solver : Solvers.values()) { - for (String symbol : - FluentIterable.concat( - RESERVED, - TEST_SYMBOLS, - VariableNamesTest.NAMES, - VariableNamesTest.UNSUPPORTED_NAMES)) { + for (String symbol : FluentIterable.concat(TEST_SYMBOLS)) { for (String variant : ImmutableSet.of( symbol, @@ -179,45 +114,21 @@ public void init() { requireParser(); } - /** Is this True if the symbol is a reserved keyword in the SMTLIB standard. */ - private static boolean isReserved(String pSymbol) { - return RESERVED.contains(pSymbol); - } - - /** True if the symbol is a simple symbol according to the SMTLIB standard. */ - private static boolean isSimple(String pSymbol) { - return pSymbol.matches("^[~!@$%^&*_\\-+=<>.?\\/0-9a-zA-Z]+$") - && !Character.isDigit(pSymbol.charAt(0)) - && !isReserved(pSymbol); - } - /** * True if the symbol is a valid symbol according to the SMTLIB standard. * - *

Valid symbols can be either simple symbols or quoted symbols. + *

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

If the symbol is not quoted, return it unchanged. - */ - private static String removeQuotes(String pSymbol) { - if (pSymbol.length() >= 2 && pSymbol.startsWith("|") && pSymbol.endsWith("|")) { - return pSymbol.substring(1, pSymbol.length() - 1); - } else { - return pSymbol; - } - } - /** * Add quotes to the symbol * @@ -227,22 +138,16 @@ private static String addQuotes(String pSymbol) { return "|" + pSymbol + "|"; } + /** Returns True if the symbol is quoted */ private static boolean hasQuotes(String pSymbol) { return pSymbol.length() >= 2 && pSymbol.startsWith("|") && pSymbol.endsWith("|"); } /** - * Return the canonical representation of the symbol. + * Parse a variable definition in the SMTLIB format and return the term. * - *

The symbol will have quotes if and only if the same symbol without quotes would not be legal - * in SMTLIB. + *

Returns a variable or a UF depending on the value of asUfSymbol */ - private static String canonical(String pSymbol) { - String noquotes = removeQuotes(pSymbol); - return isSimple(noquotes) ? noquotes : addQuotes(noquotes); - } - - /** Parse a variable definition in the SMTLIB format and return the term. */ private BooleanFormula parseSymbol(String pSymbol, boolean asUfSymbol) { String sort = solver == Solvers.BITWUZLA ? "(_ BitVec 8)" : "Int"; String query = @@ -254,10 +159,12 @@ private BooleanFormula parseSymbol(String pSymbol, boolean asUfSymbol) { 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(); } From 0775ef89d2c1281a3cd6b72d4e1b5b454554a5a9 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 8 Jan 2025 12:28:29 +0100 Subject: [PATCH 10/16] Remove tests that use formerly illegal variable names and expect and exception --- .../test/EnumerationFormulaManagerTest.java | 7 ---- .../sosy_lab/java_smt/test/UFManagerTest.java | 36 ------------------- 2 files changed, 43 deletions(-) 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/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(); From 51231a47df3a3405770ca1ff2df09b617e1fe5a9 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 8 Jan 2025 13:15:38 +0100 Subject: [PATCH 11/16] Rewrite VariableNamesTest as all variable names are now legal --- .../test/VariableNamesEscaperTest.java | 5 -- .../java_smt/test/VariableNamesTest.java | 73 +++---------------- 2 files changed, 11 insertions(+), 67 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/VariableNamesEscaperTest.java b/src/org/sosy_lab/java_smt/test/VariableNamesEscaperTest.java index 0e3a6cd039..301133e9ea 100644 --- a/src/org/sosy_lab/java_smt/test/VariableNamesEscaperTest.java +++ b/src/org/sosy_lab/java_smt/test/VariableNamesEscaperTest.java @@ -17,11 +17,6 @@ /** 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); diff --git a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java index 12716a02b8..6030bc3b21 100644 --- a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java +++ b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java @@ -8,10 +8,8 @@ package org.sosy_lab.java_smt.test; -import static com.google.common.base.Preconditions.checkArgument; 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; @@ -170,18 +168,9 @@ protected List getAllNames() { .build(); } - boolean allowInvalidNames() { - return true; - } - @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 +180,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 +192,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 +210,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("|" + name + "|")).isFalse(); } @Test @@ -296,8 +277,6 @@ 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) { testName0( name, @@ -335,8 +314,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, @@ -371,11 +348,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 +374,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 +397,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 +453,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 +478,6 @@ public void testBoolVariableNameInVisitor() { for (String name : getAllNames()) { BooleanFormula var = createVariableWith(bmgr::makeVariable, name); - if (var == null) { - continue; - } bmgr.visit( var, @@ -545,22 +506,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 +566,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,12 +580,7 @@ public void testBvArrayVariable() { @Test public void sameBehaviorTest() { for (String name : getAllNames()) { - if (mgr.isValidName(name)) { - // should pass without exception - checkArgument(FormulaCreator.isValidName(name)); - } else { - assertThrows(IllegalArgumentException.class, () -> FormulaCreator.isValidName(name)); - } + assertThat(mgr.isValidName(name)).isEqualTo(FormulaCreator.isValidName(name)); } } } From 07c0199418311f7a71089ac3ce7f510d80fcbeac Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 8 Jan 2025 14:16:52 +0100 Subject: [PATCH 12/16] Simplify VariableNamesTest classes --- .../test/ParserSymbolsEscapedTest.java | 6 +- .../test/VariableNamesEscaperTest.java | 14 +- .../test/VariableNamesInvalidTest.java | 72 -------- .../java_smt/test/VariableNamesTest.java | 162 +++--------------- 4 files changed, 31 insertions(+), 223 deletions(-) delete mode 100644 src/org/sosy_lab/java_smt/test/VariableNamesInvalidTest.java diff --git a/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java b/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java index ef9d9b3697..55b848e00a 100644 --- a/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java +++ b/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java @@ -120,7 +120,7 @@ public void init() { *

This function is stricter than {@link FormulaCreator#isValidName(String)} and won't allow * names such as "a \nb" without any SMTLIB quotes. */ - private static boolean isValid(String pSymbol) { + static boolean isValid(String pSymbol) { if (pSymbol.length() >= 2 && pSymbol.startsWith("|") && pSymbol.endsWith("|")) { return FormulaCreator.isValidName(dequote(pSymbol)); } else { @@ -134,12 +134,12 @@ private static boolean isValid(String pSymbol) { * *

Assumes that the symbol is not already quoted. */ - private static String addQuotes(String pSymbol) { + static String addQuotes(String pSymbol) { return "|" + pSymbol + "|"; } /** Returns True if the symbol is quoted */ - private static boolean hasQuotes(String pSymbol) { + static boolean hasQuotes(String pSymbol) { return pSymbol.length() >= 2 && pSymbol.startsWith("|") && pSymbol.endsWith("|"); } diff --git a/src/org/sosy_lab/java_smt/test/VariableNamesEscaperTest.java b/src/org/sosy_lab/java_smt/test/VariableNamesEscaperTest.java index 301133e9ea..a96c4c73a6 100644 --- a/src/org/sosy_lab/java_smt/test/VariableNamesEscaperTest.java +++ b/src/org/sosy_lab/java_smt/test/VariableNamesEscaperTest.java @@ -10,21 +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 - 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); } @@ -32,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 6030bc3b21..076375985e 100644 --- a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java +++ b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java @@ -13,12 +13,11 @@ 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; @@ -35,137 +34,26 @@ import org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor; import org.sosy_lab.java_smt.basicimpl.FormulaCreator; -@SuppressFBWarnings(value = "DLS_DEAD_LOCAL_STORE") +// 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. + public class VariableNamesTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { - public static final ImmutableList NAMES = - ImmutableList.of( - "java-smt", - "JavaSMT", - "sosylab", - "test", - "foo", - "bar", - "baz", - "declare", - "(exit)", - "!=", - "~", - ",", - ".", - ":", - " ", - " ", - "(", - ")", - "[", - "]", - "{", - "}", - "[]", - "\"", - "\"\"", - "\"\"\"", - "'", - "''", - "'''", - "\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 - * FormulaCreator#DISALLOWED_CHARACTERS}. - */ - @SuppressWarnings("javadoc") - public 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(FormulaCreator.RESERVED) - .addAll(FormulaCreator.DISALLOWED_CHARACTER_REPLACEMENT.values()) - .addAll(FURTHER_SMTLIB2_KEYWORDS) - .addAll(UNSUPPORTED_NAMES) - .build(); + 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 @@ -211,7 +99,7 @@ private void testName0( String dump = mgr.dumpFormula(eq.apply(var, var)).toString(); // Adding SMTLIB quotes to the name should make it illegal - assertThat(mgr.isValidName("|" + name + "|")).isFalse(); + assertThat(mgr.isValidName(ParserSymbolsEscapedTest.addQuotes(name))).isFalse(); } @Test @@ -277,7 +165,7 @@ public void testNameIntArray() throws SolverException, InterruptedException { public void testNameBvArray() throws SolverException, InterruptedException { requireBitvectors(); requireArrays(); - for (String name : NAMES) { + for (String name : getAllNames()) { testName0( name, s -> @@ -293,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)), @@ -305,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); } @@ -327,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); } @@ -337,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); } } From edf75a27e1b0b32d2007b6a92b0c4aec1b2ca92e Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 9 Jan 2025 01:05:19 +0100 Subject: [PATCH 13/16] Add more failing test inputs --- .../sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java b/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java index 55b848e00a..e44c82886d 100644 --- a/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java +++ b/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java @@ -78,7 +78,12 @@ public class ParserSymbolsEscapedTest extends SolverBasedTest0 { "define-fun-rec", "store", "concat", - "="); + "=", + "true", + "false", + "and", + "or", + "distinct"); @Parameters(name = "{0},{1}") public static Collection data() { From e8639e580e2db866344c7ccb8a28c9cb90a34126 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 9 Jan 2025 01:07:16 +0100 Subject: [PATCH 14/16] Fix parsing for Princess and make sure that an IllegalArgumentException is thrown if an invalid symbol name is used in the input script --- .../solvers/princess/PrincessEnvironment.java | 13 +++++++++++++ 1 file changed, 13 insertions(+) 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()); From b1fa368f91bec84df910b726f593ea231624fe0a Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 9 Jan 2025 01:19:46 +0100 Subject: [PATCH 15/16] Blacklist remaining failed test cases --- .../sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java b/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java index e44c82886d..34cbc4863d 100644 --- a/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java +++ b/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java @@ -205,6 +205,14 @@ public void testEscapedParserInvalid() { 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)); } From bc047e03e7cae26d7a945e06a2c36540f343e364 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 9 Jan 2025 15:38:18 +0100 Subject: [PATCH 16/16] Blacklist a Unicode test value as there seem to be some encoding issues on the Windows test system --- src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java b/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java index 34cbc4863d..9890558602 100644 --- a/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java +++ b/src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java @@ -230,6 +230,10 @@ public void testEscapedDumpAndParse() { // 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);