Skip to content

Commit 998b730

Browse files
committed
improve model evaluation for Strings with Unicode characters.
1 parent 8e6fbee commit 998b730

File tree

5 files changed

+48
-4
lines changed

5 files changed

+48
-4
lines changed

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@
1010

1111
import static com.google.common.base.Preconditions.checkArgument;
1212
import static com.google.common.base.Preconditions.checkState;
13+
import static org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager.unescapeUnicodeForSmtlib;
1314

1415
import com.google.common.base.Preconditions;
1516
import com.google.common.collect.ImmutableList;
@@ -611,7 +612,7 @@ public Object convertValue(Expr expForType, Expr value) {
611612
return convertFloatingPoint(value);
612613

613614
} else if (valueType.isString()) {
614-
return value.getConstString().toString();
615+
return unescapeUnicodeForSmtlib(value.getConstString().toString());
615616

616617
} else {
617618
// String serialization for unknown terms.

src/org/sosy_lab/java_smt/solvers/princess/PrincessStringFormulaManager.java

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,8 @@ public class PrincessStringFormulaManager
3434
protected IExpression makeStringImpl(String value) {
3535
value = unescapeUnicodeForSmtlib(value);
3636
checkArgument(!containsSurrogatePair(value), "Princess does not support surrogate pairs.");
37-
return PrincessEnvironment.stringTheory.string2Term(value);
37+
IExpression strExpr = PrincessEnvironment.stringTheory.string2Term(value);
38+
return getFormulaCreator().getEnv().simplify(strExpr); // simplify MOD in chars
3839
}
3940

4041
/** returns whether any character of the string is part of a surrogate pair. */

src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@
99
package org.sosy_lab.java_smt.solvers.z3;
1010

1111
import static com.google.common.base.Preconditions.checkArgument;
12+
import static org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager.unescapeUnicodeForSmtlib;
1213

1314
import com.google.common.base.Preconditions;
1415
import com.google.common.collect.HashBasedTable;
@@ -893,7 +894,7 @@ public Object convertValue(Long value) {
893894
Rational ratValue = Rational.ofString(Native.getNumeralString(environment, value));
894895
return ratValue.isIntegral() ? ratValue.getNum() : ratValue;
895896
} else if (type.isStringType()) {
896-
return Native.getString(environment, value);
897+
return unescapeUnicodeForSmtlib(Native.getString(environment, value));
897898
} else if (type.isBitvectorType()) {
898899
return new BigInteger(Native.getNumeralString(environment, value));
899900
} else if (type.isFloatingPointType()) {

src/org/sosy_lab/java_smt/test/ModelEvaluationTest.java

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -147,9 +147,42 @@ public void testGetBooleansEvaluation() throws SolverException, InterruptedExcep
147147
Lists.newArrayList(null, bmgr.makeBoolean(defaultValue)));
148148
}
149149

150+
@SuppressWarnings("UnicodeEscape")
150151
@Test
151152
public void testGetStringsEvaluation() throws SolverException, InterruptedException {
152153
requireStrings();
154+
155+
// empty string
156+
evaluateInModel(
157+
smgr.equal(smgr.makeVariable("x"), smgr.makeString("")),
158+
smgr.makeVariable("x"),
159+
Lists.newArrayList(""),
160+
Lists.newArrayList(smgr.makeString("")));
161+
162+
// normal string
163+
evaluateInModel(
164+
smgr.equal(smgr.makeVariable("x"), smgr.makeString("hello WORLD")),
165+
smgr.makeVariable("x"),
166+
Lists.newArrayList("hello WORLD"),
167+
Lists.newArrayList(smgr.makeString("hello WORLD")));
168+
169+
// Unicode
170+
evaluateInModel(
171+
smgr.equal(smgr.makeVariable("x"), smgr.makeString("hello æ@€ \u1234 \\u{4321}")),
172+
smgr.makeVariable("x"),
173+
Lists.newArrayList("hello \u00e6@\u20ac \u1234 \u4321"),
174+
Lists.newArrayList(smgr.makeString("hello \u00e6@\u20ac \u1234 \u4321")));
175+
176+
// TODO Z3 and CVC4 seem to break escaping on invalid Unicode Strings.
177+
/*
178+
evaluateInModel(
179+
smgr.equal(smgr.makeVariable("x"), smgr.makeString("\\u")),
180+
smgr.makeVariable("x"),
181+
Lists.newArrayList("\\u"),
182+
Lists.newArrayList(smgr.makeString("\\u")));
183+
*/
184+
185+
// foreign variable: x vs y
153186
evaluateInModel(
154187
smgr.equal(smgr.makeVariable("x"), smgr.makeString("hello")),
155188
smgr.makeVariable("y"),

src/org/sosy_lab/java_smt/test/SolverVisitorTest.java

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -745,7 +745,7 @@ public void stringInStringFormulaVisit() throws SolverException, InterruptedExce
745745
.add(smgr.charAt(x, offset))
746746
.add(smgr.toStringFormula(offset))
747747
.add(smgr.concat(x, y, z));
748-
if (solverToUse() != Solvers.PRINCESS) {
748+
if (solverToUse() != Solvers.PRINCESS) { // TODO Princess crashes with MatchError of IFunApp
749749
formulas.add(smgr.fromCodePoint(cp));
750750
}
751751
if (solverToUse() != Solvers.Z3) {
@@ -758,6 +758,14 @@ public void stringInStringFormulaVisit() throws SolverException, InterruptedExce
758758
assertThat(f2).isEqualTo(f);
759759
assertThatFormula(bmgr.not(smgr.equal(f, f2))).isUnsatisfiable();
760760
}
761+
{
762+
IntegerFormula f = smgr.toCodePoint(y);
763+
mgr.visit(f, new FunctionDeclarationVisitorNoUF());
764+
mgr.visit(f, new FunctionDeclarationVisitorNoOther(mgr));
765+
IntegerFormula f2 = mgr.transformRecursively(f, new FormulaTransformationVisitor(mgr) {});
766+
assertThat(f2).isEqualTo(f);
767+
assertThatFormula(bmgr.not(imgr.equal(f, f2))).isUnsatisfiable();
768+
}
761769
}
762770

763771
@Test

0 commit comments

Comments
 (0)