Merge pull request #456 from sosy-lab/allow-empty-string-ranges

Allow empty String ranges

Author: daniel-raffler

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

@@ -8,7 +8,6 @@
 
 package org.sosy_lab.java_smt.api;
 
-import com.google.common.base.Preconditions;
 import java.util.Arrays;
 import java.util.List;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
@@ -155,13 +154,6 @@ default StringFormula concat(StringFormula... parts) {
    * @see #range(StringFormula, StringFormula)
    */
   default RegexFormula range(char start, char end) {
-    Preconditions.checkArgument(
-        start <= end,
-        "Range from start '%s' (%s) to end '%s' (%s) is empty.",
-        start,
-        (int) start,
-        end,
-        (int) end);
     return range(makeString(String.valueOf(start)), makeString(String.valueOf(end)));
   }
 

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

@@ -143,9 +143,33 @@ protected Expr allCharImpl() {
     return exprManager.mkExpr(Kind.REGEXP_SIGMA, new vectorExpr());
   }
 
+  /**
+   * Check if the String only contains printable US ASCII characters.
+   *
+   * <p>We use this function to check if the String contains any characters that would have to be
+   * escaped in SMTLIB.
+   */
+  private boolean isAsciiString(String str) {
+    return str.codePoints().allMatch(c -> c >= 0x20 && c <= 0x7E);
+  }
+
   @Override
   protected Expr range(Expr start, Expr end) {
-    return exprManager.mkExpr(Kind.REGEXP_RANGE, start, end);
+    Preconditions.checkArgument(
+        start.isConst() && end.isConst(), "CVC4 does not support variables as bounds");
+
+    String lower = (String) formulaCreator.convertValue(start, start);
+    String upper = (String) formulaCreator.convertValue(end, end);
+
+    Preconditions.checkArgument(
+        isAsciiString(lower) && isAsciiString(upper),
+        "CVC4 only allows printable US ASCII characters as bounds");
+
+    // Return the empty language if the bounds are not single character Strings, or if the upper
+    // bound is smaller than the lower bound
+    return lower.length() != 1 || upper.length() != 1 || upper.compareTo(lower) < 0
+        ? noneImpl()
+        : exprManager.mkExpr(Kind.REGEXP_RANGE, start, end);
   }
 
   @Override

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

@@ -140,7 +140,16 @@ protected Term allCharImpl() {
 
   @Override
   protected Term range(Term start, Term end) {
-    return solver.mkTerm(Kind.REGEXP_RANGE, start, end);
+    // Precondition: Both bounds must be single character Strings
+    // CVC5 already checks that the lower bound is smaller than the upper bound and returns the
+    // empty language otherwise.
+    Term one = solver.mkInteger(1);
+    Term cond =
+        solver.mkTerm(
+            Kind.AND,
+            solver.mkTerm(Kind.EQUAL, length(start), one),
+            solver.mkTerm(Kind.EQUAL, length(end), one));
+    return solver.mkTerm(Kind.ITE, cond, solver.mkTerm(Kind.REGEXP_RANGE, start, end), noneImpl());
   }
 
   @Override

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

@@ -605,6 +605,9 @@ static FormulaType<?> getFormulaType(IExpression pFormula) {
    * @throws IllegalArgumentException for any other type.
    */
   private static FormulaType<?> mergeFormulaTypes(FormulaType<?> type1, FormulaType<?> type2) {
+    if (type1.equals(type2)) {
+      return type1;
+    }
     if ((type1.isIntegerType() || type1.isRationalType())
         && (type2.isIntegerType() || type2.isRationalType())) {
       return type1.isRationalType() ? type1 : type2;

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

@@ -11,11 +11,16 @@
 import static com.google.common.base.Preconditions.checkArgument;
 import static org.sosy_lab.java_smt.solvers.princess.PrincessEnvironment.toITermSeq;
 
+import ap.basetypes.IdealInt;
 import ap.parser.IAtom;
+import ap.parser.IBinFormula;
+import ap.parser.IBinJunctor;
 import ap.parser.IExpression;
 import ap.parser.IFormula;
 import ap.parser.IFunApp;
+import ap.parser.IIntLit;
 import ap.parser.ITerm;
+import ap.parser.ITermITE;
 import ap.types.Sort;
 import com.google.common.collect.ImmutableList;
 import java.util.List;
@@ -166,7 +171,17 @@ protected IExpression allCharImpl() {
 
   @Override
   protected ITerm range(IExpression start, IExpression end) {
-    return new IFunApp(PrincessEnvironment.stringTheory.re_range(), toITermSeq());
+    // Precondition: Both bounds must be single character Strings
+    // Princess already checks that the lower bound is smaller than the upper bound and returns the
+    // empty language otherwise.
+    ITerm one = new IIntLit(IdealInt.apply(1));
+    IFormula cond =
+        new IBinFormula(
+            IBinJunctor.And(), length(start).$eq$eq$eq(one), length(end).$eq$eq$eq(one));
+    return new ITermITE(
+        cond,
+        new IFunApp(PrincessEnvironment.stringTheory.re_range(), toITermSeq(start, end)),
+        noneImpl());
   }
 
   @Override

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

@@ -260,6 +260,75 @@ public void testStringConcatEmpty() throws SolverException, InterruptedException
     assertEqual(empty, smgr.concat(ImmutableList.of(empty, empty, empty, empty)));
   }
 
+  @Test
+  public void testStringRange() throws SolverException, InterruptedException {
+    StringFormula var = smgr.makeVariable("str");
+
+    // Try something simple:
+    // StringFormulaManager.range("a","b") should not be empty
+    assertThatFormula(smgr.in(var, smgr.range(smgr.makeString("a"), smgr.makeString("b"))))
+        .isSatisfiable();
+    assertThatFormula(smgr.in(var, smgr.range('a', 'b'))).isSatisfiable();
+
+    // Check again with a single element interval:
+    // StringFormulaManager.range("a","a") should not be empty
+    assertThatFormula(smgr.in(var, smgr.range(smgr.makeString("a"), smgr.makeString("a"))))
+        .isSatisfiable();
+    assertThatFormula(smgr.in(var, smgr.range('a', 'a'))).isSatisfiable();
+
+    // Check again for Unicode characters:
+    // StringFormulaManager.range("ꯍ","ꯎ") should not be empty
+    if (solver != Solvers.CVC4) {
+      // FIXME CVC4 only support ASCII characters for range()
+      assertThatFormula(smgr.in(var, smgr.range(smgr.makeString("ꯍ"), smgr.makeString("ꯎ"))))
+          .isSatisfiable();
+      assertThatFormula(smgr.in(var, smgr.range('ꯍ', 'ꯎ'))).isSatisfiable();
+    }
+
+    // And once more with Unicode characters that are not in the BMP:
+    // StringFormulaManager.range("𠃋","𠃋") should not be empty
+    if (solver != Solvers.PRINCESS && solver != Solvers.CVC4) {
+      // FIXME CVC4 only support ASCII characters for range()
+      // FIXME Princess can't handle surrogate pairs
+      assertThatFormula(smgr.in(var, smgr.range(smgr.makeString("𠃋"), smgr.makeString("𠃋"))))
+          .isSatisfiable();
+    }
+
+    // Check some corner cases:
+    // StringFormulaManager.range("b", "a") should be empty
+    assertThatFormula(smgr.in(var, smgr.range(smgr.makeString("b"), smgr.makeString("a"))))
+        .isUnsatisfiable();
+    assertThatFormula(smgr.in(var, smgr.range('b', 'a'))).isUnsatisfiable();
+
+    // Only 'singleton' Strings (= Strings with one character) are allowed:
+    // StringFormulaManager.range("", "a") should be empty
+    assertThatFormula(smgr.in(var, smgr.range(smgr.makeString(""), smgr.makeString("a"))))
+        .isUnsatisfiable();
+
+    // Try again with two characters:
+    // StringFormulaManager.range("aa", "ab") should be empty
+    assertThatFormula(smgr.in(var, smgr.range(smgr.makeString("aa"), smgr.makeString("ab"))))
+        .isUnsatisfiable();
+
+    // Now use variables for the bounds:
+    // StringFormulaManager.range(lower, "b") should be empty iff "b" < lower
+    StringFormula lower = smgr.makeVariable("lower");
+    if (solver != Solvers.PRINCESS && solver != Solvers.CVC4) {
+      // FIXME CVC4 only supports String constants as bounds and will fail for variables
+      // FIXME Princess will crash when using variables as bounds
+      assertThatFormula(
+              bmgr.and(
+                  smgr.equal(lower, smgr.makeString("a")),
+                  smgr.in(var, smgr.range(lower, smgr.makeString("b")))))
+          .isSatisfiable();
+      assertThatFormula(
+              bmgr.and(
+                  smgr.equal(lower, smgr.makeString("c")),
+                  smgr.in(var, smgr.range(lower, smgr.makeString("b")))))
+          .isUnsatisfiable();
+    }
+  }
+
   @Test
   public void testStringPrefixSuffixConcat() throws SolverException, InterruptedException {
     // FIXME: Princess will timeout on this test