diff --git a/src/org/sosy_lab/java_smt/SolverContextFactory.java b/src/org/sosy_lab/java_smt/SolverContextFactory.java index 43d64b5d14..d9e901814f 100644 --- a/src/org/sosy_lab/java_smt/SolverContextFactory.java +++ b/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"); diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java index 1bb109f98f..6ce40fc2b8 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java +++ b/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 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 arrayManager; @@ -140,6 +163,8 @@ public abstract class AbstractFormulaManager pFormulaCreator, AbstractUFManager functionManager, AbstractBooleanFormulaManager booleanManager, @@ -154,8 +179,11 @@ protected AbstractFormulaManager( @Nullable AbstractArrayFormulaManager arrayManager, @Nullable AbstractSLFormulaManager slManager, @Nullable AbstractStringFormulaManager strManager, - @Nullable AbstractEnumerationFormulaManager - enumManager) { + @Nullable AbstractEnumerationFormulaManager 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++; } diff --git a/src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java b/src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java index e549657947..31c7c78330 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java +++ b/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 (set-logic ..). * @@ -239,8 +249,21 @@ public static boolean isExitToken(String token) { *
  • reset * * - *

    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 + *

    These tokens manipulate the stack and are not supported while parsing SMT-lIB2 string. + * + *

    The list of forbidden tokens also contains operations that are not supported by JavaSMT: + * + *

      + *
    • declare-datatype + *
    • declare-datatypes + *
    • declare-sort + *
    • define-sort + *
    • declare-sort-parameter + *
    • define-fun-rec + *
    • define-funs-rec + *
    + * + *

    When a forbidden token is found parsing should be aborted by throwing an {@link * IllegalArgumentException} exception. * *

    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. + * + *

    The list of ignored tokens contains: + * + *

      + *
    • 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 + *
    + * + *

    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. + * + *

    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"); } } diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java index c384dd5545..d586a6303d 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java +++ b/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,6 +40,8 @@ final class BitwuzlaFormulaManager @SuppressWarnings("checkstyle:parameternumber") BitwuzlaFormulaManager( + LogManager pLogger, + Configuration pConfiguration, BitwuzlaFormulaCreator pFormulaCreator, BitwuzlaUFManager pFunctionManager, BitwuzlaBooleanFormulaManager pBooleanManager, @@ -44,8 +49,11 @@ final class BitwuzlaFormulaManager BitwuzlaQuantifiedFormulaManager pQuantifierManager, BitwuzlaFloatingPointManager pFloatingPointManager, BitwuzlaArrayFormulaManager pArrayManager, - Options pBitwuzlaOptions) { + Options pBitwuzlaOptions) + throws InvalidConfigurationException { super( + pLogger, + pConfiguration, pFormulaCreator, pFunctionManager, pBooleanManager, diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java index 2af48115d8..7425634325 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaSolverContext.java +++ b/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, diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java index 4b9e1cb7d9..7c76404c8b 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java +++ b/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 { 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, diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java index 6df6f5b30e..84e7488f7c 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java @@ -24,6 +24,7 @@ import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.ConfigurationBuilder; import org.sosy_lab.common.configuration.InvalidConfigurationException; +import org.sosy_lab.common.log.LogManager; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.BooleanFormulaManager; import org.sosy_lab.java_smt.api.FormulaManager; @@ -109,8 +110,10 @@ public void satSolverBackendTest() for (SatSolver satsolver : BoolectorSolverContext.SatSolver.values()) { ConfigurationBuilder config = Configuration.builder().setOption("solver.boolector.satSolver", satsolver.name()); + LogManager logger = LogManager.createTestLogManager(); try (BoolectorSolverContext context = BoolectorSolverContext.create( + logger, config.build(), ShutdownNotifier.createDummy(), null, @@ -133,8 +136,10 @@ public void satSolverBackendTest() @Test public void dumpVariableTest() throws InvalidConfigurationException { ConfigurationBuilder config = Configuration.builder(); + LogManager logger = LogManager.createTestLogManager(); try (BoolectorSolverContext context = BoolectorSolverContext.create( + logger, config.build(), ShutdownNotifier.createDummy(), null, @@ -155,8 +160,10 @@ public void dumpVariableTest() throws InvalidConfigurationException { public void dumpVariableWithAssertionsOnStackTest() throws InvalidConfigurationException, InterruptedException { ConfigurationBuilder config = Configuration.builder(); + LogManager logger = LogManager.createTestLogManager(); try (BoolectorSolverContext context = BoolectorSolverContext.create( + logger, config.build(), ShutdownNotifier.createDummy(), null, @@ -184,8 +191,10 @@ public void dumpVariableWithAssertionsOnStackTest() @Test public void repeatedDumpFormulaTest() throws InvalidConfigurationException { ConfigurationBuilder config = Configuration.builder(); + LogManager logger = LogManager.createTestLogManager(); try (BoolectorSolverContext context = BoolectorSolverContext.create( + logger, config.build(), ShutdownNotifier.createDummy(), null, diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java index e86aecaf0f..a4d29e3360 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java @@ -24,6 +24,7 @@ import org.sosy_lab.common.configuration.Option; import org.sosy_lab.common.configuration.Options; 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.InterpolatingProverEnvironment; import org.sosy_lab.java_smt.api.OptimizationProverEnvironment; @@ -77,6 +78,7 @@ private static class BoolectorSettings { } public static BoolectorSolverContext create( + LogManager pLogger, Configuration config, ShutdownNotifier pShutdownNotifier, @Nullable PathCounterTemplate solverLogfile, @@ -97,7 +99,7 @@ public static BoolectorSolverContext create( BoolectorArrayFormulaManager arrayTheory = new BoolectorArrayFormulaManager(creator); BoolectorFormulaManager manager = new BoolectorFormulaManager( - creator, functionTheory, booleanTheory, bitvectorTheory, arrayTheory); + pLogger, config, creator, functionTheory, booleanTheory, bitvectorTheory, arrayTheory); return new BoolectorSolverContext(manager, creator, pShutdownNotifier); } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaManager.java index 3f140e38de..12de61b778 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaManager.java @@ -21,6 +21,9 @@ import java.util.LinkedHashMap; import java.util.List; import java.util.Map; +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.api.FormulaType; import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager; @@ -31,6 +34,8 @@ class CVC4FormulaManager extends AbstractFormulaManager pLoader) { + Consumer pLoader) + throws InvalidConfigurationException { pLoader.accept("cvc4jni"); @@ -94,6 +97,8 @@ public static SolverContext create( CVC4StringFormulaManager strTheory = new CVC4StringFormulaManager(creator); CVC4FormulaManager manager = new CVC4FormulaManager( + pLogger, + pConfiguration, creator, functionTheory, booleanTheory, diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java index 379430a0b6..b1d1ac4049 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java @@ -25,6 +25,9 @@ import java.util.List; import java.util.Map; import java.util.Map.Entry; +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.api.FormulaType; import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager; @@ -35,6 +38,8 @@ class CVC5FormulaManager extends AbstractFormulaManager pLoader) { System.setProperty("cvc5.skipLibraryLoad", "true"); } - @SuppressWarnings({"unused", "resource"}) + @SuppressWarnings("resource") public static SolverContext create( LogManager pLogger, Configuration pConfig, @@ -126,7 +126,7 @@ public static SolverContext create( instances++; } - CVC5Settings settings = new CVC5Settings(pConfig); + CVC5SolverContext.CVC5Settings settings = new CVC5Settings(pConfig); loadLibrary(pLoader); @@ -166,6 +166,8 @@ public static SolverContext create( CVC5EnumerationFormulaManager enumTheory = new CVC5EnumerationFormulaManager(pCreator); CVC5FormulaManager manager = new CVC5FormulaManager( + pLogger, + pConfig, pCreator, functionTheory, booleanTheory, diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaManager.java index 5ad55840f6..edb1833b82 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaManager.java @@ -20,6 +20,9 @@ import com.google.common.primitives.Longs; import java.util.Collection; import java.util.Map; +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.BooleanFormula; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaManager; @@ -33,6 +36,8 @@ final class Mathsat5FormulaManager extends AbstractFormulaManager