String theory: extend API with support for code points.

Author: kfriedberger

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

@@ -71,9 +71,8 @@ public interface StringFormulaManager {
   IntegerFormula indexOf(StringFormula str, StringFormula part, IntegerFormula startIndex);
 
   /**
-   * Get a substring of length 1 from the given String.
-   *
-   * <p>The result is underspecified, if the index is out of bounds for the given String.
+   * Get a substring of length 1 from the given String if the given index is within bounds.
+   * Otherwise, returns an empty string.
    */
   StringFormula charAt(StringFormula str, IntegerFormula index);
 
@@ -231,4 +230,17 @@ default RegexFormula concat(RegexFormula... parts) {
    * It returns the empty string <code>""</code> for negative numbers.
    */
   StringFormula toStringFormula(IntegerFormula number);
+
+  /**
+   * Returns an Integer formula representing the code point of the only character of the given
+   * String formula, if s is a singleton string. Otherwise, returns -1.
+   */
+  IntegerFormula toCodePoint(StringFormula str);
+
+  /**
+   * Returns the singleton string whose only character is the given code point if it is represented
+   * as a single char in UTF16, i.e., it is in the range [0, 196607]. Otherwise, returns the empty
+   * string.
+   */
+  StringFormula fromCodePoint(IntegerFormula codePoint);
 }

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

@@ -40,6 +40,10 @@ protected RegexFormula wrapRegex(TFormulaInfo formulaInfo) {
     return getFormulaCreator().encapsulateRegex(formulaInfo);
   }
 
+  protected IntegerFormula wrapInteger(TFormulaInfo formulaInfo) {
+    return getFormulaCreator().encapsulate(FormulaType.IntegerType, formulaInfo);
+  }
+
   @Override
   public StringFormula makeString(String value) {
     return wrapString(makeStringImpl(value));
@@ -141,10 +145,7 @@ public BooleanFormula contains(StringFormula str, StringFormula part) {
 
   @Override
   public IntegerFormula indexOf(StringFormula str, StringFormula part, IntegerFormula startIndex) {
-    return getFormulaCreator()
-        .encapsulate(
-            FormulaType.IntegerType,
-            indexOf(extractInfo(str), extractInfo(part), extractInfo(startIndex)));
+    return wrapInteger(indexOf(extractInfo(str), extractInfo(part), extractInfo(startIndex)));
   }
 
   protected abstract TFormulaInfo indexOf(
@@ -287,8 +288,7 @@ public RegexFormula times(RegexFormula regex, int repetitions) {
 
   @Override
   public IntegerFormula toIntegerFormula(StringFormula str) {
-    return getFormulaCreator()
-        .encapsulate(FormulaType.IntegerType, toIntegerFormula(extractInfo(str)));
+    return wrapInteger(toIntegerFormula(extractInfo(str)));
   }
 
   protected abstract TFormulaInfo toIntegerFormula(TFormulaInfo pParam);
@@ -299,4 +299,18 @@ public StringFormula toStringFormula(IntegerFormula number) {
   }
 
   protected abstract TFormulaInfo toStringFormula(TFormulaInfo pParam);
+
+  @Override
+  public IntegerFormula toCodePoint(StringFormula number) {
+    return wrapInteger(toCodePoint(extractInfo(number)));
+  }
+
+  protected abstract TFormulaInfo toCodePoint(TFormulaInfo pParam);
+
+  @Override
+  public StringFormula fromCodePoint(IntegerFormula number) {
+    return wrapString(fromCodePoint(extractInfo(number)));
+  }
+
+  protected abstract TFormulaInfo fromCodePoint(TFormulaInfo pParam);
 }

src/org/sosy_lab/java_smt/delegate/debugging/DebuggingStringFormulaManager.java

@@ -354,4 +354,22 @@ public StringFormula toStringFormula(IntegerFormula number) {
     debugging.addFormulaTerm(result);
     return result;
   }
+
+  @Override
+  public IntegerFormula toCodePoint(StringFormula str) {
+    debugging.assertThreadLocal();
+    debugging.assertFormulaInContext(str);
+    IntegerFormula result = delegate.toCodePoint(str);
+    debugging.addFormulaTerm(result);
+    return result;
+  }
+
+  @Override
+  public StringFormula fromCodePoint(IntegerFormula codepoint) {
+    debugging.assertThreadLocal();
+    debugging.assertFormulaInContext(codepoint);
+    StringFormula result = delegate.fromCodePoint(codepoint);
+    debugging.addFormulaTerm(result);
+    return result;
+  }
 }

src/org/sosy_lab/java_smt/delegate/statistics/StatisticsStringFormulaManager.java

@@ -233,4 +233,16 @@ public StringFormula toStringFormula(IntegerFormula number) {
     stats.stringOperations.getAndIncrement();
     return delegate.toStringFormula(number);
   }
+
+  @Override
+  public IntegerFormula toCodePoint(StringFormula str) {
+    stats.stringOperations.getAndIncrement();
+    return delegate.toCodePoint(str);
+  }
+
+  @Override
+  public StringFormula fromCodePoint(IntegerFormula codepoint) {
+    stats.stringOperations.getAndIncrement();
+    return delegate.fromCodePoint(codepoint);
+  }
 }

src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedStringFormulaManager.java

@@ -268,4 +268,18 @@ public StringFormula toStringFormula(IntegerFormula number) {
       return delegate.toStringFormula(number);
     }
   }
+
+  @Override
+  public IntegerFormula toCodePoint(StringFormula str) {
+    synchronized (sync) {
+      return delegate.toCodePoint(str);
+    }
+  }
+
+  @Override
+  public StringFormula fromCodePoint(IntegerFormula codepoint) {
+    synchronized (sync) {
+      return delegate.fromCodePoint(codepoint);
+    }
+  }
 }

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

@@ -190,4 +190,14 @@ protected Expr toIntegerFormula(Expr pParam) {
   protected Expr toStringFormula(Expr pParam) {
     return exprManager.mkExpr(Kind.STRING_ITOS, pParam);
   }
+
+  @Override
+  protected Expr toCodePoint(Expr pParam) {
+    return exprManager.mkExpr(Kind.STRING_TO_CODE, pParam);
+  }
+
+  @Override
+  protected Expr fromCodePoint(Expr pParam) {
+    return exprManager.mkExpr(Kind.STRING_FROM_CODE, pParam);
+  }
 }

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

@@ -186,4 +186,14 @@ protected Term toStringFormula(Term pParam) {
         "CVC5 only supports INT to STRING conversion.");
     return solver.mkTerm(Kind.STRING_FROM_INT, pParam);
   }
+
+  @Override
+  protected Term toCodePoint(Term pParam) {
+    return solver.mkTerm(Kind.STRING_TO_CODE, pParam);
+  }
+
+  @Override
+  protected Term fromCodePoint(Term pParam) {
+    return solver.mkTerm(Kind.STRING_FROM_CODE, pParam);
+  }
 }

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

@@ -309,4 +309,14 @@ protected ITerm toIntegerFormula(IExpression pParam) {
   protected ITerm toStringFormula(IExpression pParam) {
     return new IFunApp(PrincessEnvironment.stringTheory.int_to_str(), toITermSeq(pParam));
   }
+
+  @Override
+  protected IExpression toCodePoint(IExpression pParam) {
+    return new IFunApp(PrincessEnvironment.stringTheory.str_to_code(), toITermSeq(pParam));
+  }
+
+  @Override
+  protected IExpression fromCodePoint(IExpression pParam) {
+    return new IFunApp(PrincessEnvironment.stringTheory.str_from_code(), toITermSeq(pParam));
+  }
 }

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

@@ -178,4 +178,14 @@ protected Long toIntegerFormula(Long pParam) {
   protected Long toStringFormula(Long pParam) {
     return Native.mkIntToStr(z3context, pParam);
   }
+
+  @Override
+  protected Long toCodePoint(Long pParam) {
+    return Native.mkStringToCode(z3context, pParam);
+  }
+
+  @Override
+  protected Long fromCodePoint(Long pParam) {
+    return Native.mkStringFromCode(z3context, pParam);
+  }
 }

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

@@ -64,6 +64,8 @@ public class StringFormulaManagerTest extends SolverBasedTest0.ParameterizedSolv
           "abchurrdurr",
           "abcdefaaaaa");
 
+  private static final int MAX_SINGLE_CODE_POINT_IN_UTF16 = 0x2FFFF;
+
   private StringFormula a;
   private StringFormula b;
   private StringFormula ab;
@@ -736,6 +738,97 @@ public void testCharAtWithConstString() throws SolverException, InterruptedExcep
     assertDistinct(smgr.charAt(ab, imgr.makeNumber(1)), a);
   }
 
+  @Test
+  public void testCharAtHasAlwaysLengthZeroOrOne() throws SolverException, InterruptedException {
+    StringFormula someString = smgr.makeVariable("someString");
+    IntegerFormula position = imgr.makeVariable("position");
+    IntegerFormula length = smgr.length(smgr.charAt(someString, position));
+
+    BooleanFormula lengthZero = imgr.equal(length, imgr.makeNumber(0));
+    BooleanFormula lengthOne = imgr.equal(length, imgr.makeNumber(1));
+
+    assertThatFormula(bmgr.or(lengthZero, lengthOne)).isTautological();
+  }
+
+  @Test
+  public void testStringToCodePoint() throws SolverException, InterruptedException {
+    // TODO report to developers
+    assume()
+        .withMessage("Solver %s crashes", solverToUse())
+        .that(solverToUse())
+        .isNotEqualTo(Solvers.PRINCESS);
+
+    assertThatFormula(imgr.equal(smgr.toCodePoint(a), imgr.makeNumber('a'))).isTautological();
+    assertThatFormula(imgr.equal(smgr.toCodePoint(b), imgr.makeNumber('b'))).isTautological();
+
+    // string of length != 1 are invalid and return -1
+    assertThatFormula(imgr.equal(smgr.toCodePoint(ab), imgr.makeNumber(-1))).isTautological();
+    assertThatFormula(imgr.equal(smgr.toCodePoint(empty), imgr.makeNumber(-1))).isTautological();
+  }
+
+  @Test
+  public void testToCodePointInRange() throws SolverException, InterruptedException {
+    // TODO report to developers
+    assume()
+        .withMessage("Solver %s crashes", solverToUse())
+        .that(solverToUse())
+        .isNotEqualTo(Solvers.PRINCESS);
+
+    StringFormula str = smgr.makeVariable("str");
+    IntegerFormula cp = smgr.toCodePoint(str);
+    BooleanFormula invalidStr = imgr.equal(cp, imgr.makeNumber(-1));
+    BooleanFormula cpInRange =
+        bmgr.and(
+            imgr.lessOrEquals(imgr.makeNumber(0), cp),
+            imgr.lessOrEquals(cp, imgr.makeNumber(MAX_SINGLE_CODE_POINT_IN_UTF16)));
+    assertThatFormula(bmgr.or(invalidStr, cpInRange)).isTautological();
+  }
+
+  @Test
+  public void testFromCodePointInRange() throws SolverException, InterruptedException {
+    // TODO report to developers
+    assume()
+        .withMessage("Solver %s crashes", solverToUse())
+        .that(solverToUse())
+        .isNotEqualTo(Solvers.PRINCESS);
+
+    IntegerFormula cp = imgr.makeVariable("cp");
+    StringFormula str = smgr.fromCodePoint(cp);
+    IntegerFormula len = smgr.length(str);
+
+    // all normal code points are in range, i.e., string length is 1.
+    BooleanFormula cpInRange =
+        bmgr.and(
+            imgr.lessOrEquals(imgr.makeNumber(0), cp),
+            imgr.lessOrEquals(cp, imgr.makeNumber(MAX_SINGLE_CODE_POINT_IN_UTF16)));
+    assertThatFormula(cpInRange).isEquivalentTo(imgr.equal(len, imgr.makeNumber(1)));
+
+    // all other code points are out of range, i.e., they match the empty string with length 0.
+    assertThatFormula(bmgr.not(cpInRange)).isEquivalentTo(smgr.equal(str, empty));
+  }
+
+  @Test
+  public void testStringFromCodePoint() throws SolverException, InterruptedException {
+    StringFormula cpA = smgr.fromCodePoint(imgr.makeNumber('a'));
+    StringFormula cpB = smgr.fromCodePoint(imgr.makeNumber('b'));
+    assertThatFormula(smgr.equal(cpA, a)).isTautological();
+    assertThatFormula(smgr.equal(cpB, b)).isTautological();
+    assertThatFormula(smgr.equal(cpA, smgr.makeString(Character.toString(97)))).isTautological();
+
+    StringFormula cpOne = smgr.fromCodePoint(imgr.makeNumber(1));
+    StringFormula cpTen = smgr.fromCodePoint(imgr.makeNumber(10));
+    assertThatFormula(smgr.equal(cpOne, smgr.makeString(Character.toString(1)))).isTautological();
+    assertThatFormula(smgr.equal(cpTen, smgr.makeString(Character.toString(10)))).isTautological();
+
+    // negative numbers are invalid and return empty string
+    StringFormula cpNegOne = smgr.fromCodePoint(imgr.makeNumber(-1));
+    StringFormula cpNegTen = smgr.fromCodePoint(imgr.makeNumber(-10));
+    StringFormula cpNeg256 = smgr.fromCodePoint(imgr.makeNumber(-100));
+    assertThatFormula(smgr.equal(cpNegOne, empty)).isTautological();
+    assertThatFormula(smgr.equal(cpNegTen, empty)).isTautological();
+    assertThatFormula(smgr.equal(cpNeg256, empty)).isTautological();
+  }
+
   /**
    * Test escapecharacter treatment. Escape characters are treated as a single char! Example:
    * "a\u1234T" has "a" at position 0, "\u1234" at position 1 and "T" at position 2