Strings: Remove support for Unicode escape sequences

Mixing Unicode characters with SMTLIB escape sequences leads to confusing corner cases and has therefore been removed from StringFormulaManager.makeString. Users can call unescapeUnicodeForSmtlib() from AbstractStringFormulaManager to convert a String with escape sequences before handing it of to makeString(). In the other direction escapeUnicodeForSmtlib() can be used to convert (Unicode) Strings from the model into an escaped format that is compatible with other SMTLIB based solvers.

Author: daniel-raffler

src/org/sosy_lab/java_smt/basicimpl/AbstractStringFormulaManager.java

@@ -60,22 +60,19 @@ protected IntegerFormula wrapInteger(TFormulaInfo formulaInfo) {
   @Override
   public StringFormula makeString(String value) {
     checkArgument(
-        areAllCodePointsInRange(value),
-        "String constant is out of supported Unicode range (Plane 0-2).");
+        areAllCodePointsInRange(value, 0, 0x2FFFF),
+        "String constants may only contain Unicode characters from the first three planes "
+            + "(codepoints 0x00000 to 0x2FFFF).");
     return wrapString(makeStringImpl(value));
   }
 
-  /** returns whether all Unicode characters in Planes 0-2. */
-  private static boolean areAllCodePointsInRange(String str) {
-    return str.codePoints().allMatch(AbstractStringFormulaManager::isCodePointInRange);
-  }
-
-  private static boolean isCodePointInRange(int codePoint) {
-    return 0x00000 <= codePoint && codePoint <= 0x2FFFF;
+  /** Check if the codepoints of all characters in the String are in range. */
+  private static boolean areAllCodePointsInRange(String str, int lower, int upper) {
+    return str.codePoints().allMatch(codePoint -> lower <= codePoint && codePoint <= upper);
   }
 
   /** Replace Unicode letters in UTF16 representation with their escape sequences. */
-  protected static String escapeUnicodeForSmtlib(String input) {
+  public static String escapeUnicodeForSmtlib(String input) {
     StringBuilder sb = new StringBuilder();
     for (int codePoint : input.codePoints().toArray()) {
       if (codePoint == 0x5c) {
@@ -102,7 +99,7 @@ public static String unescapeUnicodeForSmtlib(String input) {
       }
       int codePoint = Integer.parseInt(hexCodePoint, 16);
       checkArgument(
-          isCodePointInRange(codePoint),
+          0 <= codePoint && codePoint <= 0x2FFFF,
           "SMTLIB does only specify Unicode letters from Planes 0-2");
       String replacement = Character.toString(codePoint);
       if (replacement.equals("\\")) {

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

@@ -29,8 +29,7 @@ class CVC4StringFormulaManager extends AbstractStringFormulaManager<Expr, Type,
 
   @Override
   protected Expr makeStringImpl(String pValue) {
-    String str = escapeUnicodeForSmtlib(unescapeUnicodeForSmtlib(pValue));
-    return exprManager.mkConst(new CVC4String(str, true));
+    return exprManager.mkConst(new CVC4String(escapeUnicodeForSmtlib(pValue), true));
   }
 
   @Override

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5StringFormulaManager.java

@@ -27,8 +27,7 @@ class CVC5StringFormulaManager extends AbstractStringFormulaManager<Term, Sort,
 
   @Override
   protected Term makeStringImpl(String pValue) {
-    String str = escapeUnicodeForSmtlib(unescapeUnicodeForSmtlib(pValue));
-    return solver.mkString(str, true);
+    return solver.mkString(escapeUnicodeForSmtlib(pValue), true);
   }
 
   @Override

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

@@ -32,7 +32,6 @@ public class PrincessStringFormulaManager
 
   @Override
   protected IExpression makeStringImpl(String value) {
-    value = unescapeUnicodeForSmtlib(value);
     checkArgument(!containsSurrogatePair(value), "Princess does not support surrogate pairs.");
     IExpression strExpr = PrincessEnvironment.stringTheory.string2Term(value);
     return getFormulaCreator().getEnv().simplify(strExpr); // simplify MOD in chars

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

@@ -9,7 +9,6 @@
 package org.sosy_lab.java_smt.solvers.z3;
 
 import static com.google.common.base.Preconditions.checkArgument;
-import static org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager.unescapeUnicodeForSmtlib;
 
 import com.google.common.base.Preconditions;
 import com.google.common.collect.HashBasedTable;
@@ -58,6 +57,7 @@
 import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.api.StringFormula;
 import org.sosy_lab.java_smt.api.visitors.FormulaVisitor;
+import org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager;
 import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
 import org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl;
 import org.sosy_lab.java_smt.solvers.z3.Z3Formula.Z3ArrayFormula;
@@ -921,7 +921,8 @@ public Object convertValue(Long value) {
         Rational ratValue = Rational.ofString(Native.getNumeralString(environment, value));
         return ratValue.isIntegral() ? ratValue.getNum() : ratValue;
       } else if (type.isStringType()) {
-        return unescapeUnicodeForSmtlib(Native.getString(environment, value));
+        String str = Native.getString(environment, value);
+        return AbstractStringFormulaManager.unescapeUnicodeForSmtlib(str);
       } else if (type.isBitvectorType()) {
         return new BigInteger(Native.getNumeralString(environment, value));
       } else if (type.isFloatingPointType()) {

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

@@ -25,8 +25,7 @@ class Z3StringFormulaManager extends AbstractStringFormulaManager<Long, Long, Lo
 
   @Override
   protected Long makeStringImpl(String pValue) {
-    String str = escapeUnicodeForSmtlib(unescapeUnicodeForSmtlib(pValue));
-    return Native.mkString(z3context, str);
+    return Native.mkString(z3context, escapeUnicodeForSmtlib(pValue));
   }
 
   @Override

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

@@ -31,6 +31,7 @@
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
 import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.api.StringFormula;
+import org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager;
 
 @SuppressWarnings("ConstantConditions")
 @SuppressFBWarnings(value = "DLS_DEAD_LOCAL_STORE", justification = "test code")
@@ -111,6 +112,15 @@ private void assertDistinct(StringFormula str1, StringFormula str2)
     assertThatFormula(smgr.equal(str1, str2)).isUnsatisfiable();
   }
 
+  /**
+   * Resolve any SMTLIB escape sequences and create a new String constant.
+   *
+   * <p>The input String may still contain Unicode characters.
+   */
+  private StringFormula makeStringEscaped(String pString) {
+    return smgr.makeString(AbstractStringFormulaManager.unescapeUnicodeForSmtlib(pString));
+  }
+
   private void requireVariableStringLiterals() {
     // FIXME: Remove once support for operations on non-singleton Strings has been added
     // See https://github.com/uuverifiers/ostrich/issues/88
@@ -126,12 +136,15 @@ private void requireVariableStringLiterals() {
 
   @Test
   public void testInputEscape() throws SolverException, InterruptedException {
-    // Test if SMTLIB Unicode literals are recognized and converted to their Unicode characters.
-    assertEqual(smgr.length(smgr.makeString("\\u{39E}")), imgr.makeNumber(1));
-    assertEqual(smgr.length(smgr.makeString("Ξ")), imgr.makeNumber(1));
+    // Check that escape sequences are not substituted
+    assertEqual(smgr.length(smgr.makeString("\\u{39E}")), imgr.makeNumber(7));
+    // ...unless we're doing so explicitly:
+    assertEqual(smgr.length(makeStringEscaped("\\u{39E}")), imgr.makeNumber(1));
 
-    // Test with a character that is not in the BMP
+    // Test that Unicode characters are working
+    assertEqual(smgr.length(smgr.makeString("Ξ")), imgr.makeNumber(1));
     if (solver != Solvers.PRINCESS) {
+      // Test with a character that is not in the BMP
       String str = Character.toString(0x200cb);
       assertEqual(smgr.length(smgr.makeString(str)), imgr.makeNumber(1));
     }
@@ -143,8 +156,9 @@ public void testOutputUnescape() throws SolverException, InterruptedException {
     try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
       assertThat(!prover.isUnsat()).isTrue();
       try (Model model = prover.getModel()) {
-        assertThat(model.evaluate(smgr.makeString("\\u{39E}"))).isEqualTo("Ξ");
-        assertThat(model.evaluate(smgr.concat(smgr.makeString("\\u{39E"), smgr.makeString("}"))))
+        assertThat(model.evaluate(makeStringEscaped("\\u{39E}"))).isEqualTo("Ξ");
+        assertThat(
+                model.evaluate(smgr.concat(makeStringEscaped("\\u{39E"), makeStringEscaped("}"))))
             .isEqualTo("\\u{39E}");
 
         // Test with a character that is not in the BMP
@@ -197,18 +211,18 @@ public void testRegexAllCharUnicode() throws SolverException, InterruptedExcepti
     // special single characters.
 
     // Greek Capital Letter Delta
-    assertThatFormula(smgr.in(smgr.makeString("\\u0394"), regexAllChar)).isTautological();
-    assertThatFormula(smgr.in(smgr.makeString("Δ"), regexAllChar)).isTautological();
+    assertThatFormula(smgr.in(makeStringEscaped("\\u0394"), regexAllChar)).isTautological();
+    assertThatFormula(smgr.in(makeStringEscaped("Δ"), regexAllChar)).isTautological();
     // CJK Compatibility Ideograph from Basic Multilingual Plane.
-    assertThatFormula(smgr.in(smgr.makeString("\\u{fa6a}"), regexAllChar)).isTautological();
+    assertThatFormula(smgr.in(makeStringEscaped("\\u{fa6a}"), regexAllChar)).isTautological();
     // Xiangqi Black Horse from Supplementary Multilingual Plane
-    assertThatFormula(smgr.in(smgr.makeString("\\u{1fa6a}"), regexAllChar)).isTautological();
+    assertThatFormula(smgr.in(makeStringEscaped("\\u{1fa6a}"), regexAllChar)).isTautological();
 
     // Combining characters are not matched as one character.
-    assertThatFormula(smgr.in(smgr.makeString("ab"), regexAllChar)).isUnsatisfiable();
-    assertThatFormula(smgr.in(smgr.makeString("abcdefgh"), regexAllChar)).isUnsatisfiable();
-    assertThatFormula(smgr.in(smgr.makeString("a\\u0336"), regexAllChar)).isUnsatisfiable();
-    assertThatFormula(smgr.in(smgr.makeString("\\n"), regexAllChar)).isUnsatisfiable();
+    assertThatFormula(smgr.in(makeStringEscaped("ab"), regexAllChar)).isUnsatisfiable();
+    assertThatFormula(smgr.in(makeStringEscaped("abcdefgh"), regexAllChar)).isUnsatisfiable();
+    assertThatFormula(smgr.in(makeStringEscaped("a\\u0336"), regexAllChar)).isUnsatisfiable();
+    assertThatFormula(smgr.in(makeStringEscaped("\\n"), regexAllChar)).isUnsatisfiable();
 
     StringFormula x = smgr.makeVariable("x");
     assertThatFormula(smgr.in(x, smgr.range('a', 'z'))).isSatisfiable();
@@ -400,7 +414,7 @@ public void testStringLength() throws SolverException, InterruptedException {
     assertEqual(imgr.makeNumber(1), smgr.length(smgr.makeString("\n")));
     assertEqual(imgr.makeNumber(1), smgr.length(smgr.makeString("\t")));
 
-    assertEqual(imgr.makeNumber(1), smgr.length(smgr.makeString("\\u{20AC}")));
+    assertEqual(imgr.makeNumber(1), smgr.length(makeStringEscaped("\\u{20AC}")));
     assertEqual(imgr.makeNumber(1), smgr.length(smgr.makeString("€")));
     assertEqual(imgr.makeNumber(1), smgr.length(smgr.makeString("Δ")));
 
@@ -905,8 +919,8 @@ public void testCharAtWithSpecialCharacters() throws SolverException, Interrupte
     String workaround = "au{1234}";
     StringFormula au1234WOEscapeCurly = smgr.makeString(workaround);
     StringFormula backSlash = smgr.makeString("\\");
-    StringFormula u1234 = smgr.makeString("\\u{1234}");
-    StringFormula au1234b = smgr.makeString("a\\u{1234}b");
+    StringFormula u1234 = makeStringEscaped("\\u{1234}");
+    StringFormula au1234b = makeStringEscaped("a\\u{1234}b");
 
     assertEqual(smgr.length(backSlash), imgr.makeNumber(1));
     assertEqual(smgr.charAt(au1234b, imgr.makeNumber(0)), a);
@@ -936,22 +950,22 @@ public void testCharAtWithSpecialCharacters() throws SolverException, Interrupte
   @Test
   public void testUnicodeEscaping() throws SolverException, InterruptedException {
     // SMTLIB has different representations for the same symbol
-    assertEqual(a, smgr.makeString("\u0061"));
-    assertEqual(a, smgr.makeString("\\u0061"));
-    assertEqual(a, smgr.makeString("\\u{61}"));
-    assertEqual(a, smgr.makeString("\\u{00061}"));
+    assertEqual(a, makeStringEscaped("\u0061"));
+    assertEqual(a, makeStringEscaped("\\u0061"));
+    assertEqual(a, makeStringEscaped("\\u{61}"));
+    assertEqual(a, makeStringEscaped("\\u{00061}"));
     assertEqual(smgr.length(a), imgr.makeNumber(1));
 
-    StringFormula u0 = smgr.makeString("\\u0000");
-    assertEqual(u0, smgr.makeString("\u0000"));
-    assertEqual(u0, smgr.makeString("\\u{0}"));
-    assertEqual(u0, smgr.makeString("\\u{00000}"));
+    StringFormula u0 = makeStringEscaped("\\u0000");
+    assertEqual(u0, makeStringEscaped("\u0000"));
+    assertEqual(u0, makeStringEscaped("\\u{0}"));
+    assertEqual(u0, makeStringEscaped("\\u{00000}"));
     assertEqual(smgr.length(u0), imgr.makeNumber(1));
 
-    StringFormula u1 = smgr.makeString("\\u1234");
-    assertEqual(u1, smgr.makeString("\u1234"));
-    assertEqual(u1, smgr.makeString("\\u{1234}"));
-    assertEqual(u1, smgr.makeString("\\u{01234}"));
+    StringFormula u1 = makeStringEscaped("\\u1234");
+    assertEqual(u1, makeStringEscaped("\u1234"));
+    assertEqual(u1, makeStringEscaped("\\u{1234}"));
+    assertEqual(u1, makeStringEscaped("\\u{01234}"));
     assertEqual(smgr.length(u1), imgr.makeNumber(1));
 
     if (solverToUse() == Solvers.PRINCESS) {
@@ -961,10 +975,10 @@ public void testUnicodeEscaping() throws SolverException, InterruptedException {
               Character.toString(0x10000),
               "\\u{2FFFF}",
               Character.toString(0x2FFFF))) {
-        assertThrows(IllegalArgumentException.class, () -> smgr.makeString(invalidStr));
+        assertThrows(IllegalArgumentException.class, () -> makeStringEscaped(invalidStr));
       }
     } else {
-      StringFormula u2 = smgr.makeString("\\u{2FFFF}");
+      StringFormula u2 = makeStringEscaped("\\u{2FFFF}");
       assertEqual(u2, smgr.makeString(Character.toString(0x2FFFF)));
       assertEqual(smgr.length(u2), imgr.makeNumber(1));
     }
@@ -978,10 +992,10 @@ public void testUnicodeEscaping() throws SolverException, InterruptedException {
   public void testCharAtWithSpecialCharacters2Byte() throws SolverException, InterruptedException {
     StringFormula num7 = smgr.makeString("7");
     StringFormula u = smgr.makeString("u");
-    StringFormula curlyOpen2BUnicode = smgr.makeString("\\u{7B}");
-    StringFormula curlyClose2BUnicode = smgr.makeString("\\u{7D}");
-    StringFormula acurlyClose2BUnicodeb = smgr.makeString("a\\u{7D}b");
-    StringFormula acurlyOpen2BUnicodeWOEscapeCurly = smgr.makeString("au{7B}");
+    StringFormula curlyOpen2BUnicode = makeStringEscaped("\\u{7B}");
+    StringFormula curlyClose2BUnicode = makeStringEscaped("\\u{7D}");
+    StringFormula acurlyClose2BUnicodeb = makeStringEscaped("a\\u{7D}b");
+    StringFormula acurlyOpen2BUnicodeWOEscapeCurly = makeStringEscaped("au{7B}");
     StringFormula backSlash = smgr.makeString("\\");
 
     assertEqual(smgr.length(backSlash), imgr.makeNumber(1));
@@ -1070,10 +1084,10 @@ public void testConstStringContains() throws SolverException, InterruptedExcepti
     StringFormula abbbbbb = smgr.makeString("abbbbbb");
     StringFormula aaaaaaaB = smgr.makeString("aaaaaaaB");
     StringFormula abcAndSoOn = smgr.makeString("abcdefghijklmnopqrstuVwxyz");
-    StringFormula curlyOpen2BUnicode = smgr.makeString("\\u{7B}");
-    StringFormula curlyClose2BUnicode = smgr.makeString("\\u{7D}");
-    StringFormula multipleCurlys2BUnicode = smgr.makeString("\\u{7B}\\u{7D}\\u{7B}\\u{7B}");
-    StringFormula curlyClose2BUnicodeEncased = smgr.makeString("blabla\\u{7D}bla");
+    StringFormula curlyOpen2BUnicode = makeStringEscaped("\\u{7B}");
+    StringFormula curlyClose2BUnicode = makeStringEscaped("\\u{7D}");
+    StringFormula multipleCurlys2BUnicode = makeStringEscaped("\\u{7B}\\u{7D}\\u{7B}\\u{7B}");
+    StringFormula curlyClose2BUnicodeEncased = makeStringEscaped("blabla\\u{7D}bla");
 
     assertThatFormula(smgr.contains(empty, empty)).isSatisfiable();
     assertThatFormula(smgr.contains(empty, a)).isUnsatisfiable();
@@ -1113,8 +1127,8 @@ public void testStringVariableContains() throws SolverException, InterruptedExce
     StringFormula bUppercase = smgr.makeString("B");
     StringFormula bbbbbb = smgr.makeString("bbbbbb");
     StringFormula abbbbbb = smgr.makeString("abbbbbb");
-    StringFormula curlyOpen2BUnicode = smgr.makeString("\\u{7B}");
-    StringFormula curlyClose2BUnicode = smgr.makeString("\\u{7D}");
+    StringFormula curlyOpen2BUnicode = makeStringEscaped("\\u{7B}");
+    StringFormula curlyClose2BUnicode = makeStringEscaped("\\u{7D}");
 
     assertThatFormula(
             bmgr.and(smgr.contains(var1, empty), imgr.equal(imgr.makeNumber(0), smgr.length(var1))))
@@ -1175,10 +1189,10 @@ public void testConstStringIndexOf() throws SolverException, InterruptedExceptio
     StringFormula bbbbbbb = smgr.makeString("bbbbbbb");
     StringFormula abbbbbb = smgr.makeString("abbbbbb");
     StringFormula abcAndSoOn = smgr.makeString("abcdefghijklmnopqrstuVwxyz");
-    StringFormula curlyOpen2BUnicode = smgr.makeString("\\u{7B}");
-    StringFormula curlyClose2BUnicode = smgr.makeString("\\u{7D}");
-    StringFormula multipleCurlys2BUnicode = smgr.makeString("\\u{7B}\\u{7D}\\u{7B}\\u{7B}");
-    StringFormula curlys2BUnicodeWOEscape = smgr.makeString("\\u7B\\u7D");
+    StringFormula curlyOpen2BUnicode = makeStringEscaped("\\u{7B}");
+    StringFormula curlyClose2BUnicode = makeStringEscaped("\\u{7D}");
+    StringFormula multipleCurlys2BUnicode = makeStringEscaped("\\u{7B}\\u{7D}\\u{7B}\\u{7B}");
+    StringFormula curlys2BUnicodeWOEscape = makeStringEscaped("\\u7B\\u7D");
 
     IntegerFormula zero = imgr.makeNumber(0);
     IntegerFormula one = imgr.makeNumber(1);
@@ -1213,7 +1227,7 @@ public void testStringVariableIndexOf() throws SolverException, InterruptedExcep
     StringFormula var2 = smgr.makeVariable("var2");
     IntegerFormula intVar = imgr.makeVariable("intVar");
 
-    StringFormula curlyOpen2BUnicode = smgr.makeString("\\u{7B}");
+    StringFormula curlyOpen2BUnicode = makeStringEscaped("\\u{7B}");
 
     IntegerFormula zero = imgr.makeNumber(0);
 
@@ -1316,9 +1330,9 @@ public void testConstStringSubStrings() throws SolverException, InterruptedExcep
     StringFormula aUppercase = smgr.makeString("A");
     StringFormula bUppercase = smgr.makeString("B");
     StringFormula bbbbbb = smgr.makeString("bbbbbb");
-    StringFormula curlyOpen2BUnicode = smgr.makeString("\\u{7B}");
-    StringFormula curlyClose2BUnicode = smgr.makeString("\\u{7D}");
-    StringFormula multipleCurlys2BUnicode = smgr.makeString("\\u{7B}\\u{7D}\\u{7B}\\u{7B}");
+    StringFormula curlyOpen2BUnicode = makeStringEscaped("\\u{7B}");
+    StringFormula curlyClose2BUnicode = makeStringEscaped("\\u{7D}");
+    StringFormula multipleCurlys2BUnicode = makeStringEscaped("\\u{7B}\\u{7D}\\u{7B}\\u{7B}");
 
     IntegerFormula zero = imgr.makeNumber(0);
     IntegerFormula one = imgr.makeNumber(1);
@@ -1363,8 +1377,8 @@ public void testStringSubstringOutOfBounds() throws SolverException, Interrupted
     StringFormula bbbbbb = smgr.makeString("bbbbbb");
     StringFormula abbbbbb = smgr.makeString("abbbbbb");
 
-    StringFormula multipleCurlys2BUnicode = smgr.makeString("\\u{7B}\\u{7D}\\u{7B}\\u{7B}");
-    StringFormula multipleCurlys2BUnicodeFromIndex1 = smgr.makeString("\\u{7D}\\u{7B}\\u{7B}");
+    StringFormula multipleCurlys2BUnicode = makeStringEscaped("\\u{7B}\\u{7D}\\u{7B}\\u{7B}");
+    StringFormula multipleCurlys2BUnicodeFromIndex1 = makeStringEscaped("\\u{7D}\\u{7B}\\u{7B}");
 
     assertEqual(smgr.substring(abbbbbb, imgr.makeNumber(0), imgr.makeNumber(10000)), abbbbbb);
     assertEqual(smgr.substring(abbbbbb, imgr.makeNumber(6), imgr.makeNumber(10000)), b);
@@ -1760,11 +1774,11 @@ public void testStringVariableReplaceAllSubstring() throws SolverException, Inte
   public void testStringConcatWUnicode() throws SolverException, InterruptedException {
     StringFormula backslash = smgr.makeString("\\");
     StringFormula u = smgr.makeString("u");
-    StringFormula curlyOpen = smgr.makeString("\\u{7B}");
+    StringFormula curlyOpen = makeStringEscaped("\\u{7B}");
     StringFormula sevenB = smgr.makeString("7B");
-    StringFormula curlyClose = smgr.makeString("\\u{7D}");
+    StringFormula curlyClose = makeStringEscaped("\\u{7D}");
     StringFormula concat = smgr.concat(backslash, u, curlyOpen, sevenB, curlyClose);
-    StringFormula complete = smgr.makeString("\\u{7B}");
+    StringFormula complete = makeStringEscaped("\\u{7B}");
 
     // Concatting parts of unicode does not result in the unicode char!
     assertDistinct(concat, complete);