Skip to content
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

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

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 all 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
6 changes: 3 additions & 3 deletions src/org/sosy_lab/java_smt/basicimpl/AbstractArrayFormulaManager.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -65,8 +65,8 @@ protected abstract TFormulaInfo store(
FTI extends FormulaType<TI>,
FTE extends FormulaType<TE>>
ArrayFormula<TI, TE> 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);
}

Expand Down
4 changes: 1 addition & 3 deletions src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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);
Expand Down
16 changes: 10 additions & 6 deletions src/org/sosy_lab/java_smt/basicimpl/AbstractBooleanFormulaManager.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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<TFormulaInfo, TType, TEnv, TFuncDecl>
Expand All @@ -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);
Expand Down Expand Up @@ -279,21 +278,26 @@ public final <T extends Formula> T ifThenElse(BooleanFormula pBits, T f1, T f2)

@Override
public <R> R visit(BooleanFormula pFormula, BooleanFormulaVisitor<R> visitor) {
return formulaCreator.visit(pFormula, new DelegatingFormulaVisitor<>(visitor));
return formulaCreator.visit(
pFormula, new SymbolViewVisitor<>(new DelegatingFormulaVisitor<>(visitor)));
}

@Override
public void visitRecursively(
BooleanFormula pF, BooleanFormulaVisitor<TraversalProcess> 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<R> implements FormulaVisitor<R> {
Expand Down
12 changes: 7 additions & 5 deletions src/org/sosy_lab/java_smt/basicimpl/AbstractEnumerationFormulaManager.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -77,8 +79,9 @@ private void checkSameEnumerationType(EnumerationFormula pF1, EnumerationFormula

@Override
public EnumerationFormulaType declareEnumeration(String pName, Set<String> pElementNames) {
checkVariableName(pName);
return declareEnumerationImpl(pName, pElementNames);
return declareEnumerationImpl(
escapeName(pName),
ImmutableSet.copyOf(Iterables.transform(pElementNames, FormulaCreator::escapeName)));
}

protected EnumerationFormulaType declareEnumerationImpl(String pName, Set<String> pElementNames) {
Expand Down Expand Up @@ -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) {
Expand Down
5 changes: 2 additions & 3 deletions src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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(
Expand Down
Loading