improve and fix Unicode support in String theory.

Unicode characters were not handled in the same way in SMT solvers.
Z3, CVC4, and CVC5 require proper escaping.
Z3 also supports Java-based Unicode characters.
Princess only allows 16bit-sized Unicode, i.e., up to 0x0FFFF, which misses surrogate pairs up to 0x2FFFF as defined in SMTLIB.

Author: kfriedberger

src/org/sosy_lab/java_smt/api/StringFormulaManager.java

@@ -20,7 +20,10 @@
 public interface StringFormulaManager {
 
   /**
-   * Returns a {@link StringFormula} representing the given constant.
+   * Returns a {@link StringFormula} representing the given constant String. The String value is
+   * expected to be UTF16, i.e., plain Java string with Unicode characters. JavaSMT handles escaping
+   * internally, as some solvers follow the SMTLIB standard and escape Unicode characters with curly
+   * braces. We hide this detail from the user and allow to use plain Java Strings.
    *
    * @param value the string value the returned <code>Formula</code> should represent
    * @return a Formula representing the given value

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

@@ -8,12 +8,15 @@
 
 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;
 import java.util.Collections;
 import java.util.List;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.NumeralFormula;
@@ -27,6 +30,16 @@ public abstract class AbstractStringFormulaManager<TFormulaInfo, TType, TEnv, TF
     extends AbstractBaseFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl>
     implements StringFormulaManager {
 
+  private static final Pattern UNICODE_ESCAPE_PATTERN =
+      Pattern.compile(
+          // start with "\\u"
+          "\\\\u"
+              // either a plain Unicode letter like "\\u0061"
+              + "((?<codePoint>[0-9a-fA-F]{4})"
+              + "|"
+              // or curly brackets like "\\u{61}"
+              + "(\\{(?<codePointInBrackets>[0-9a-fA-F]{1,5})}))");
+
   protected AbstractStringFormulaManager(
       FormulaCreator<TFormulaInfo, TType, TEnv, TFuncDecl> pCreator) {
     super(pCreator);
@@ -46,9 +59,49 @@ protected IntegerFormula wrapInteger(TFormulaInfo formulaInfo) {
 
   @Override
   public StringFormula makeString(String value) {
+    checkArgument(
+        isCodePointInRange(value),
+        "String constant is out of supported Unicode range (Plane 0-2).");
     return wrapString(makeStringImpl(value));
   }
 
+  /** returns whether all Unicode characters in Planes 0-2. */
+  static boolean isCodePointInRange(String str) {
+    return str.codePoints().allMatch(codePoint -> 0x00000 <= codePoint && codePoint <= 0x2FFFF);
+  }
+
+  /** Replace Unicode letters in UTF16 representation with their escape sequences. */
+  protected static String escapeUnicodeForSmtlib(String input) {
+    StringBuilder sb = new StringBuilder();
+    for (int codePoint : input.codePoints().toArray()) {
+      if (0x20 <= codePoint && codePoint <= 0x7E) {
+        sb.appendCodePoint(codePoint); // normal printable chars
+      } else {
+        sb.append("\\u{").append(String.format("%05X", codePoint)).append("}");
+      }
+    }
+    return sb.toString();
+  }
+
+  /** Replace escaped Unicode letters in SMTLIB representation with their UTF16 pendant. */
+  public static String unescapeUnicodeForSmtlib(String input) {
+    Matcher matcher = UNICODE_ESCAPE_PATTERN.matcher(input);
+    StringBuilder sb = new StringBuilder();
+    while (matcher.find()) {
+      String hexCodePoint = matcher.group("codePoint");
+      if (hexCodePoint == null) {
+        hexCodePoint = matcher.group("codePointInBrackets");
+      }
+      int codePoint = Integer.parseInt(hexCodePoint, 16);
+      checkArgument(
+          0x00000 <= codePoint && codePoint <= 0x2FFFF,
+          "SMTLIB does only specify Unicode letters from Planes 0-2");
+      matcher.appendReplacement(sb, Character.toString(codePoint));
+    }
+    matcher.appendTail(sb);
+    return sb.toString();
+  }
+
   protected abstract TFormulaInfo makeStringImpl(String value);
 
   @Override

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

@@ -30,7 +30,7 @@ class CVC4StringFormulaManager extends AbstractStringFormulaManager<Expr, Type,
   @Override
   protected Expr makeStringImpl(String pValue) {
     // The boolean enables escape characters!
-    return exprManager.mkConst(new CVC4String(pValue, true));
+    return exprManager.mkConst(new CVC4String(escapeUnicodeForSmtlib(pValue), true));
   }
 
   @Override

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

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

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

@@ -8,6 +8,7 @@
 
 package org.sosy_lab.java_smt.solvers.princess;
 
+import static com.google.common.base.Preconditions.checkArgument;
 import static org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.toITermSeq;
 
 import ap.parser.IAtom;
@@ -29,104 +30,16 @@ public class PrincessStringFormulaManager
     super(pCreator);
   }
 
-  /**
-   * Tries to parse an escaped Unicode character
-   *
-   * <p>Returns the original String if parsing is not possible.
-   */
-  private static String literalOrSkip(String pToken) {
-    String literal;
-    if (pToken.startsWith("\\u{")) {
-      if (pToken.length() > 9 || !pToken.endsWith("}")) {
-        // Abort if there is no closing bracket, or if there are too many digits for the literal
-        // The longest allowed literal is \\u{d5 d4 d3 d2 d1}
-        return pToken;
-      }
-      literal = pToken.substring(3, pToken.length() - 1);
-    } else {
-      if (pToken.length() != 6) {
-        // Abort if there are not exactly 4 digits
-        // The literal must have this form: \\u d3 d2 d1 d0
-        return pToken;
-      }
-      literal = pToken.substring(2);
-    }
-
-    // Try to parse the digits as a (hexadecimal) integer
-    // Abort if there is an error
-    int value;
-    try {
-      value = Integer.parseInt(literal, 16);
-    } catch (NumberFormatException e) {
-      return pToken;
-    }
-
-    // Return the Unicode letter if it fits into a single 16bit character
-    // Otherwise throw an exception as we don't support Unicode characters with more than 4 digits
-    char[] chars = Character.toChars(value);
-    if (chars.length != 1) {
-      throw new IllegalArgumentException();
-    } else {
-      return String.valueOf(chars[0]);
-    }
-  }
-
-  /** Replace escape sequences for Unicode letters with their UTF16 representation. */
-  static String unescapeString(String pInput) {
-    StringBuilder builder = new StringBuilder();
-    while (!pInput.isEmpty()) {
-      // Search for the next escape sequence
-      int start = pInput.indexOf("\\u");
-      if (start == -1) {
-        // Append the rest of the String to the output if there are no more escaped Unicode
-        // characters
-        builder.append(pInput);
-        pInput = "";
-      } else {
-        // Store the prefix up to the escape sequence
-        String prefix = pInput.substring(0, start);
-
-        // Skip ahead and get the escape sequence
-        pInput = pInput.substring(start);
-        String value;
-        if (pInput.charAt(2) == '{') {
-          // Sequence has the form \\u{d5 d4 d3 d2 d1 d0}
-          // Find the closing bracket for the literal:
-          int stop = pInput.indexOf('}');
-          if (stop == -1) {
-            // Use the index right after "\\u{" if there is no closing bracket
-            stop = 2;
-          }
-          value = pInput.substring(0, stop + 1);
-          pInput = pInput.substring(stop + 1);
-        } else {
-          // Sequence has the form \\u d3 d2 d1 d0
-          int stop = 2;
-          while (stop < pInput.length()) {
-            char c = pInput.charAt(stop);
-            if (Character.digit(c, 16) == -1) {
-              break;
-            }
-            stop++;
-          }
-          value = pInput.substring(0, stop);
-          pInput = pInput.substring(stop);
-        }
-
-        // Try to parse the escape sequence to replace it with its 16bit Unicode character
-        // If parsing fails just keep it in the String
-        String nextToken = literalOrSkip(value);
-
-        // Collect the prefix and the (possibly) translated escape sequence
-        builder.append(prefix).append(nextToken);
-      }
-    }
-    return builder.toString();
-  }
-
   @Override
   protected IExpression makeStringImpl(String value) {
-    return PrincessEnvironment.stringTheory.string2Term(unescapeString(value));
+    value = unescapeUnicodeForSmtlib(value);
+    checkArgument(!containsSurrogatePair(value), "Princess does not support surrogate pairs.");
+    return PrincessEnvironment.stringTheory.string2Term(value);
+  }
+
+  /** returns whether any character of the string is part of a surrogate pair. */
+  private static boolean containsSurrogatePair(String str) {
+    return str.codePoints().anyMatch(Character::isSupplementaryCodePoint);
   }
 
   @Override

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

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