Skip to content

Blacklist more SMTLIB keywords as variable/uf names and automatically escape all variable names that would be illegal #424

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 16 commits into
base: master
Choose a base branch
from
Open

Blacklist more SMTLIB keywords as variable/uf names and automatically escape all variable names that would be illegal #424

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
f96547b
Add more reserved keywords to the list of forbidden variable/UF names…
daniel-raffler Dec 31, 2024
e767a9f
Remove "exit" from the list of legal variable names in VariableNamesTest
daniel-raffler Dec 31, 2024
4cd4fd2
Explicitly blacklist all predefined bv functions as variable/uf names.
daniel-raffler Jan 1, 2025
142f6ba
Rename a variable in one of the tests as its name "concat" is no long…
daniel-raffler Jan 1, 2025
a43cb6d
Add a translation layer to automatically escape/unescape variable and…
daniel-raffler Jan 4, 2025
b12fbad
Let Princess throw an IllegalArgumentException if a parsing error occ…
daniel-raffler Dec 29, 2024
e8c8997
Fix FormulaCreator.dequote for symbol names have a length < 2
daniel-raffler Dec 29, 2024
ad21694
In the Bitwuzla formula visitor remove symbol quotes when a free vari…
daniel-raffler Dec 29, 2024
f496000
Cleaned up ParserSymbolsEscapedTest an reduced the number of test inputs
daniel-raffler Jan 4, 2025
0775ef8
Remove tests that use formerly illegal variable names and expect and …
daniel-raffler Jan 8, 2025
51231a4
Rewrite VariableNamesTest as all variable names are now legal
daniel-raffler Jan 8, 2025
07c0199
Simplify VariableNamesTest classes
daniel-raffler Jan 8, 2025
edf75a2
Add more failing test inputs
daniel-raffler Jan 9, 2025
e8639e5
Fix parsing for Princess and make sure that an IllegalArgumentExcepti…
daniel-raffler Jan 9, 2025
b1fa368
Blacklist remaining failed test cases
daniel-raffler Jan 9, 2025
bc047e0
Blacklist a Unicode test value as there seem to be some encoding issu…
daniel-raffler Jan 9, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
198 changes: 156 additions & 42 deletions src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -58,29 +58,160 @@
public abstract class AbstractFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl>
implements FormulaManager {

/**
* Avoid using basic mathematical or logical operators of SMT-LIB2 as names for symbols.
*
* <p>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<String> BASIC_OPERATORS =
ImmutableSet.of("!", "+", "-", "*", "/", "%", "=", "<", ">", "<=", ">=");
public static final ImmutableList<String> 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");
Copy link
Member

@kfriedberger kfriedberger Jan 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

String and Regex operations are matched via "startsWith" and not via String equality. Do we need these entries here?

Copy link
Contributor Author

@daniel-raffler daniel-raffler Jan 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The keywords in RESERVED are used by VariableNamesTest and I've included these two entries as "examples" for the tests. Otherwise, they could be removed. Come to think of it, VariableNamesTest is already kind of slow and it might even need to test all the entries in RESERVED. Maybe one or two examples for each "kind" of reserved word would be sufficient? Then we could just include those test cases directly in VariableNamesTest and remove these two dummy keywords from RESERVED.

Copy link
Contributor

@baierd baierd Jul 21, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess that it might be a good idea to split the tests into a full test run that only runs once in a while (e.g. weekly in the CI) and a subset of unit tests that run always, as this problem is also present in some other PRs. If @kfriedberger and @PhilippWendler agree i will create an issue.

Copy link
Member

@kfriedberger kfriedberger Jul 21, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

First, we already have split tests for all (slower) and some (fast) tests, that were introduced with the ARM-based CI.

Second, is the main issue here really, that the VariableNamesTests are slow individually, or just in general?
The tests only generate about 1000 variables (maybe a few more :-) ), and the issue is that we need to setup the whole JavaSMT context that often, e.g., we load the solver and initialize the managers several 1000 times, per solver.
Inlining the list of symbols into a simple loop might speedup the VariableNamesTests, with just loosing the granularity of reporting each symbol as individual test.


/**
* Avoid using basic keywords of SMT-LIB2 as names for symbols.
* Checks if the symbol name is a reserved keyword in SMTLIB2.
*
* <p>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<String> SMTLIB2_KEYWORDS =
ImmutableSet.of("true", "false", "and", "or", "select", "store", "xor", "distinct", "let");
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.
Expand Down Expand Up @@ -587,19 +718,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);
}

/**
Expand All @@ -613,32 +732,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) {
Expand All @@ -660,7 +774,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;
}
}
Expand Down
2 changes: 1 addition & 1 deletion src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand Down
4 changes: 1 addition & 3 deletions src/org/sosy_lab/java_smt/test/VariableNamesTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,6 @@ public class VariableNamesTest extends SolverBasedTest0.ParameterizedSolverBased
"bar",
"baz",
"declare",
"exit",
"(exit)",
"!=",
"~",
Expand Down Expand Up @@ -162,8 +161,7 @@ public class VariableNamesTest extends SolverBasedTest0.ParameterizedSolverBased
protected List<String> getAllNames() {
return ImmutableList.<String>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)
Expand Down