Add an option to reject/log Smtlib inputs with illegal commands

src/org/sosy_lab/java_smt/SolverContextFactory.java

@@ -250,6 +250,7 @@ private SolverContext generateContext0(Solvers solverToCreate)
       case CVC4:
         return CVC4SolverContext.create(
             logger,
+            config,
             shutdownNotifier,
             (int) randomSeed,
             nonLinearArithmetic,
@@ -305,17 +306,25 @@ private SolverContext generateContext0(Solvers solverToCreate)
 
       case PRINCESS:
         return PrincessSolverContext.create(
-            config, shutdownNotifier, logfile, (int) randomSeed, nonLinearArithmetic);
+            logger, config, shutdownNotifier, logfile, (int) randomSeed, nonLinearArithmetic);
 
       case YICES2:
-        return Yices2SolverContext.create(config, nonLinearArithmetic, shutdownNotifier, loader);
+        return Yices2SolverContext.create(
+            logger, config, nonLinearArithmetic, shutdownNotifier, loader);
 
       case BOOLECTOR:
-        return BoolectorSolverContext.create(config, shutdownNotifier, logfile, randomSeed, loader);
+        return BoolectorSolverContext.create(
+            logger, config, shutdownNotifier, logfile, randomSeed, loader);
 
       case BITWUZLA:
         return BitwuzlaSolverContext.create(
-            config, shutdownNotifier, logfile, randomSeed, floatingPointRoundingMode, loader);
+            logger,
+            config,
+            shutdownNotifier,
+            logfile,
+            randomSeed,
+            floatingPointRoundingMode,
+            loader);
 
       default:
         throw new AssertionError("no solver selected");

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

@@ -26,11 +26,17 @@
 import java.util.ArrayList;
 import java.util.List;
 import java.util.Map;
+import java.util.logging.Level;
 import java.util.stream.Collectors;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.common.Appender;
 import org.sosy_lab.common.Appenders;
 import org.sosy_lab.common.collect.Collections3;
+import org.sosy_lab.common.configuration.Configuration;
+import org.sosy_lab.common.configuration.InvalidConfigurationException;
+import org.sosy_lab.common.configuration.Option;
+import org.sosy_lab.common.configuration.Options;
+import org.sosy_lab.common.log.LogManager;
 import org.sosy_lab.java_smt.api.ArrayFormulaManager;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.EnumerationFormulaManager;
@@ -64,6 +70,21 @@
 public abstract class AbstractFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl>
     implements FormulaManager {
 
+  @Options(prefix = "solver.parser")
+  private static class ParserOptions {
+    @Option(
+        secure = true,
+        description = "Sets how unknown commands should be handled while parsing",
+        values = {"ignore", "log", "fail"})
+    String illegalInput = "ignore";
+
+    ParserOptions(Configuration config) throws InvalidConfigurationException {
+      config.inject(this);
+    }
+  }
+
+  private final ParserOptions options;
+
   /**
    * Avoid using basic mathematical or logical operators of SMT-LIB2 as names for symbols.
    *
@@ -107,6 +128,8 @@ public abstract class AbstractFormulaManager<TFormulaInfo, TType, TEnv, TFuncDec
 
   private static final char ESCAPE = '$'; // just some allowed symbol, can be any char
 
+  private final LogManager logger;
+
   private final @Nullable AbstractArrayFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl>
       arrayManager;
 
@@ -140,6 +163,8 @@ public abstract class AbstractFormulaManager<TFormulaInfo, TType, TEnv, TFuncDec
   /** Builds a solver from the given theory implementations. */
   @SuppressWarnings("checkstyle:parameternumber")
   protected AbstractFormulaManager(
+      LogManager logger,
+      Configuration config,
       FormulaCreator<TFormulaInfo, TType, TEnv, TFuncDecl> pFormulaCreator,
       AbstractUFManager<TFormulaInfo, ?, TType, TEnv> functionManager,
       AbstractBooleanFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl> booleanManager,
@@ -154,8 +179,11 @@ protected AbstractFormulaManager(
       @Nullable AbstractArrayFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl> arrayManager,
       @Nullable AbstractSLFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl> slManager,
       @Nullable AbstractStringFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl> strManager,
-      @Nullable AbstractEnumerationFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl>
-          enumManager) {
+      @Nullable AbstractEnumerationFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl> enumManager)
+      throws InvalidConfigurationException {
+
+    this.options = new ParserOptions(config);
+    this.logger = logger;
 
     this.arrayManager = arrayManager;
     this.quantifiedManager = quantifiedManager;
@@ -415,28 +443,26 @@ private String sanitize(String formulaStr) {
 
       } else if (Tokenizer.isForbiddenToken(token)) {
         // Throw an exception if the script contains commands like (pop) or (reset) that change the
-        // state of the assertion stack.
-        // We could keep track of the state of the stack and only consider the formulas that remain
-        // on the stack at the end of the script. However, this does not seem worth it at the
-        // moment. If needed, this feature can still be added later.
-        String message;
-        if (Tokenizer.isPushToken(token)) {
-          message = "(push ...)";
-        } else if (Tokenizer.isPopToken(token)) {
-          message = "(pop ...)";
-        } else if (Tokenizer.isResetAssertionsToken(token)) {
-          message = "(reset-assertions)";
-        } else if (Tokenizer.isResetToken(token)) {
-          message = "(reset)";
-        } else {
-          // Should be unreachable
-          throw new UnsupportedOperationException();
-        }
+        // state of the assertion stack, or if the command is not supported by JavaSMT
         throw new IllegalArgumentException(
-            String.format("SMTLIB command '%s' is not supported when parsing formulas.", message));
+            String.format(
+                "SMTLIB command '%s' is not supported when parsing formulas.",
+                Tokenizer.getCommand(token)));
+
+      } else if (Tokenizer.isIgnoredToken(token)) {
+        // We can safely skip this token
 
       } else {
-        // Remove everything else, such as unknown or solver-specific commands, comments, etc.
+        // We've encountered an illegal command
+        // Skip, report or crash, depending on value of the 'parser.illegalInput' option
+        var msg = String.format("Unexpected input: %s", token);
+        if (options.illegalInput.equals("fail")) {
+          throw new IllegalArgumentException(msg);
+        } else if (options.illegalInput.equals("log")) {
+          logger.log(Level.WARNING, msg);
+        } else {
+          // Ignore
+        }
       }
       pos++;
     }

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

@@ -10,9 +10,12 @@
 
 package org.sosy_lab.java_smt.basicimpl;
 
+import static com.google.common.base.Preconditions.checkArgument;
+
 import com.google.common.collect.ImmutableList;
 import java.util.List;
 import java.util.Optional;
+import java.util.regex.Pattern;
 
 /**
  * Helper class for splitting up an SMT-LIB2 file into a string of commands.
@@ -146,6 +149,13 @@ private static boolean matchesOneOf(String token, String... regexp) {
     return token.matches("\\(\\s*(" + String.join("|", regexp) + ")[\\S\\s]*");
   }
 
+  /** Return the name of a command from a token. */
+  public static String getCommand(String token) {
+    var m = Pattern.compile("\\(\\s*([a-z-]*)[\\s()][\\S\\s]*").matcher(token);
+    checkArgument(m.find());
+    return m.group(1);
+  }
+
   /**
    * Check if the token is <code>(set-logic ..)</code>.
    *
@@ -239,8 +249,21 @@ public static boolean isExitToken(String token) {
    *   <li>reset
    * </ul>
    *
-   * <p>Forbidden tokens manipulate the stack and are not supported while parsing SMT-lIB2 string.
-   * When a forbidden token is found parsing should be aborted by throwing an {@link
+   * <p>These tokens manipulate the stack and are not supported while parsing SMT-lIB2 string.
+   *
+   * <p>The list of forbidden tokens also contains operations that are not supported by JavaSMT:
+   *
+   * <ul>
+   *   <li>declare-datatype
+   *   <li>declare-datatypes
+   *   <li>declare-sort
+   *   <li>define-sort
+   *   <li>declare-sort-parameter
+   *   <li>define-fun-rec
+   *   <li>define-funs-rec
+   * </ul>
+   *
+   * <p>When a forbidden token is found parsing should be aborted by throwing an {@link
    * IllegalArgumentException} exception.
    *
    * <p>Use {@link #tokenize(String)} to turn an SMT-LIB2 script into a string of input tokens.
@@ -249,6 +272,62 @@ public static boolean isForbiddenToken(String token) {
     return isPushToken(token)
         || isPopToken(token)
         || isResetAssertionsToken(token)
-        || isResetToken(token);
+        || isResetToken(token)
+        || matchesOneOf(
+            token,
+            "declare-datatype",
+            "declare-datatypes",
+            "declare-sort",
+            "define-sort",
+            "declare-sort-parameter",
+            "define-fun-rec",
+            "define-funs-rec");
+  }
+
+  /**
+   * Check if this token can be ignored.
+   *
+   * <p>The list of ignored tokens contains:
+   *
+   * <ul>
+   *   <li>echo
+   *   <li>set-info
+   *   <li>set-option
+   *   <li>get-assertions
+   *   <li>get-assignment
+   *   <li>get-info
+   *   <li>get-option
+   *   <li>get-model
+   *   <li>get-proof
+   *   <li>get-unsat-assumptions
+   *   <li>get-unsat-core
+   *   <li>get-value
+   *   <li>check-sat
+   *   <li>check-sat-assuming
+   * </ul>
+   *
+   * <p>Tokens on this list print their results to the screen and are meant to be used
+   * interactively. They don't change the assertion stack or add new symbols, and can therefore be
+   * ignored while parsing.
+   *
+   * <p>Use {@link #tokenize(String)} to turn an SMT-LIB2 script into a string of input tokens.
+   */
+  public static boolean isIgnoredToken(String token) {
+    return matchesOneOf(
+        token,
+        "echo",
+        "set-info",
+        "set-option",
+        "get-assertions",
+        "get-assignment",
+        "get-info",
+        "get-option",
+        "get-model",
+        "get-proof",
+        "get-unsat-assumptions",
+        "get-unsat-core",
+        "get-value",
+        "check-sat",
+        "check-sat-assuming");
   }
 }

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java

@@ -16,6 +16,9 @@
 import java.util.Collection;
 import java.util.List;
 import org.sosy_lab.common.collect.Collections3;
+import org.sosy_lab.common.configuration.Configuration;
+import org.sosy_lab.common.configuration.InvalidConfigurationException;
+import org.sosy_lab.common.log.LogManager;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager;
 import org.sosy_lab.java_smt.basicimpl.Tokenizer;
@@ -37,15 +40,20 @@ final class BitwuzlaFormulaManager
 
   @SuppressWarnings("checkstyle:parameternumber")
   BitwuzlaFormulaManager(
+      LogManager pLogger,
+      Configuration pConfiguration,
       BitwuzlaFormulaCreator pFormulaCreator,
       BitwuzlaUFManager pFunctionManager,
       BitwuzlaBooleanFormulaManager pBooleanManager,
       BitwuzlaBitvectorFormulaManager pBitvectorManager,
       BitwuzlaQuantifiedFormulaManager pQuantifierManager,
       BitwuzlaFloatingPointManager pFloatingPointManager,
       BitwuzlaArrayFormulaManager pArrayManager,
-      Options pBitwuzlaOptions) {
+      Options pBitwuzlaOptions)
+      throws InvalidConfigurationException {
     super(
+        pLogger,
+        pConfiguration,
         pFormulaCreator,
         pFunctionManager,
         pBooleanManager,

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java

@@ -29,6 +29,7 @@
 import org.sosy_lab.common.configuration.Configuration;
 import org.sosy_lab.common.configuration.InvalidConfigurationException;
 import org.sosy_lab.common.io.PathCounterTemplate;
+import org.sosy_lab.common.log.LogManager;
 import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;
 import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment;
@@ -105,6 +106,7 @@ String getFurtherOptions() {
 
   @SuppressWarnings("unused")
   public static BitwuzlaSolverContext create(
+      LogManager pLogger,
       Configuration config,
       ShutdownNotifier pShutdownNotifier,
       @Nullable PathCounterTemplate solverLogfile,
@@ -135,6 +137,8 @@ public static BitwuzlaSolverContext create(
     BitwuzlaArrayFormulaManager arrayTheory = new BitwuzlaArrayFormulaManager(creator);
     BitwuzlaFormulaManager manager =
         new BitwuzlaFormulaManager(
+            pLogger,
+            config,
             creator,
             functionTheory,
             booleanTheory,

src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java

@@ -9,18 +9,26 @@
 package org.sosy_lab.java_smt.solvers.boolector;
 
 import java.util.List;
+import org.sosy_lab.common.configuration.Configuration;
+import org.sosy_lab.common.configuration.InvalidConfigurationException;
+import org.sosy_lab.common.log.LogManager;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager;
 
 final class BoolectorFormulaManager extends AbstractFormulaManager<Long, Long, Long, Long> {
 
   BoolectorFormulaManager(
+      LogManager pLogger,
+      Configuration pConfiguration,
       BoolectorFormulaCreator pFormulaCreator,
       BoolectorUFManager pFunctionManager,
       BoolectorBooleanFormulaManager pBooleanManager,
       BoolectorBitvectorFormulaManager pBitvectorManager,
-      BoolectorArrayFormulaManager pArrayManager) {
+      BoolectorArrayFormulaManager pArrayManager)
+      throws InvalidConfigurationException {
     super(
+        pLogger,
+        pConfiguration,
         pFormulaCreator,
         pFunctionManager,
         pBooleanManager,