Throw an exception if the input for the SMT-LIB2 sanitizer contains stack operations like (pop), (reset-assertions) or (reset). Change the expected behavior in SanitizerTest.

Author: daniel-raffler

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

@@ -294,6 +294,16 @@ private String sanitize(String formulaStr) {
         // Keep only declaration, definitions and assertion
         builder.append(token).append('\n');
 
+      } else if (Tokenizer.isUnsupportedToken(token)) {
+        // Throw an exception if the script contains commands like (pop) or (reset) that change the
+        // state of the assertion stack.
+        // We could keept track of the state of the stack and only consider the formulas that remain
+        // on it until the end
+        // of the script. However, this does not seem worth it at the moment. If needed, this
+        // feature can still be added
+        // later.
+        throw new IllegalArgumentException();
+
       } else {
         // Remove everything else
       }

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

@@ -181,4 +181,22 @@ public static boolean isSetLogicToken(String token) {
   public static boolean isExitToken(String token) {
     return matchesOneOf(token, "exit");
   }
+
+  /**
+   * Check if this is an unsupported token.
+   *
+   * <p>The list of unsupported tokens contains:
+   *
+   * <ul>
+   *   <li>push
+   *   <li>pop
+   *   <li>reset-assertions
+   *   <li>reset
+   * </ul>
+   *
+   * <p>Use {@link #tokenize(String)} to turn an SMT-LIB2 script into a string of input tokens.
+   */
+  public static boolean isUnsupportedToken(String token) {
+    return matchesOneOf(token, "push", "pop", "reset-assertions", "reset");
+  }
 }

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

@@ -28,14 +28,13 @@ public void init() {
   public void logicTest() throws SolverException, InterruptedException {
     // Valid input string that sets the logic to QF_ALL
     BooleanFormula expected = mgr.parse("(declare-const v Int)(assert (= v 3))");
-    BooleanFormula validLogic =
-        mgr.parse("(set-logic QF_ALL)" + "(declare-const v Int)" + "(assert (= v 3))");
-    assertThatFormula(expected).isEquivalentTo(validLogic);
+    String validLogic = "(set-logic QF_ALL)" + "(declare-const v Int)" + "(assert (= v 3))";
+    assertThatFormula(mgr.parse(validLogic)).isEquivalentTo(expected);
 
-    // Invalid string that sets QF_UF, even though integers are needed
-    // Most solvers seem to just ignore the logic that was chosen
+    // Invalid string that sets logic QF_UF, even though integers are needed
+    // FIXME: We don't check for this as most solvers seem to ignore the logic anyway
     String wrongLogic = "(set-logic QF_UF)" + "(declare-const v Int)" + "(assert (= v 3))";
-    assertThrows(IllegalArgumentException.class, () -> mgr.parse(wrongLogic));
+    assertThatFormula(mgr.parse(wrongLogic)).isEquivalentTo(expected);
 
     // Try setting logic after another command was already used
     String logicAfterOption =
@@ -51,13 +50,15 @@ public void logicTest() throws SolverException, InterruptedException {
     assertThrows(IllegalArgumentException.class, () -> mgr.parse(logicTwice));
 
     // Call (reset) and *then* set the logic again
+    // FIXME: We currently don't support the (reset) command and expect and exception to be thrown
+    // here
     String logicReset =
         "(set-logic QF_UF)"
             + "(reset)"
             + "(set-logic ALL)"
             + "(declare-const v Int)"
             + "(assert (= v 3))";
-    assertThatFormula(mgr.parse(logicReset)).isEquivalentTo(expected);
+    assertThrows(IllegalArgumentException.class, () -> mgr.parse(logicReset));
   }
 
   @Test
@@ -77,12 +78,13 @@ public void exitAtTheEnd() throws SolverException, InterruptedException {
 
   @Test
   public void stackPushTest() throws SolverException, InterruptedException {
-    BooleanFormula expected = mgr.parse("(declare-const v Int)(assert (= v 3))");
+    // FIXME: We currently don't support stack operations and expect an exceptions to be thrown for
+    // these inputs
 
-    // Push assertions and then pop the stack to remove them
+    // Push an assertion and then use (pop) to remove it again
     String stackPush =
         "(declare-const v Int)" + "(push 1)" + "(assert (= v 0))" + "(pop 1)" + "(assert (= v 3))";
-    assertThatFormula(mgr.parse(stackPush)).isEquivalentTo(expected);
+    assertThrows(IllegalArgumentException.class, () -> mgr.parse(stackPush));
 
     // Use (reset-assertions) to remove all assertions from the stack
     String stackResetAssertions =
@@ -91,7 +93,7 @@ public void stackPushTest() throws SolverException, InterruptedException {
             + "(reset-assertions)"
             + "(declare-const v Int)"
             + "(assert (= v 0))";
-    assertThatFormula((mgr.parse(stackResetAssertions))).isEquivalentTo(expected);
+    assertThrows(IllegalArgumentException.class, () -> mgr.parse(stackResetAssertions));
 
     // With :global-declarations the reset will also remove all declarations
     String globalStackResetAssertions =
@@ -100,7 +102,7 @@ public void stackPushTest() throws SolverException, InterruptedException {
             + "(assert (= v 3))"
             + "(reset-assertions)"
             + "(assert (= v 0))";
-    assertThatFormula(mgr.parse(globalStackResetAssertions)).isEquivalentTo(expected);
+    assertThrows(IllegalArgumentException.class, () -> mgr.parse(globalStackResetAssertions));
 
     // Just calling (reset) will also clear the stack
     String stackReset =
@@ -109,6 +111,6 @@ public void stackPushTest() throws SolverException, InterruptedException {
             + "(reset)"
             + "(declare-const v Int)"
             + "(assert (= v 3))";
-    assertThatFormula(mgr.parse(stackReset)).isEquivalentTo(expected);
+    assertThrows(IllegalArgumentException.class, () -> mgr.parse(stackReset));
   }
 }