diff --git a/javasmt b/javasmt new file mode 100755 index 0000000000..58126c53ef --- /dev/null +++ b/javasmt @@ -0,0 +1,132 @@ +#!/usr/bin/env bash + +# This file is part of JavaSMT, +# an API wrapper for a collection of SMT solvers: +# https://github.com/sosy-lab/java-smt +# +# SPDX-FileCopyrightText: 2026 Dirk Beyer +# +# SPDX-License-Identifier: Apache-2.0 + +# Launcher for the command-line interface of JavaSMT. Benchmarking frameworks such +# as BenchExec need a single executable inside the project directory, so that the +# tool can be located and transferred via that path. The classpath is assembled the +# same way as in runExamples.sh. +# +# This script sets no JVM option that influences what is measured, so that every +# solver runs under the same conditions. The heap size comes from the memory limit +# of the run and is passed by the tool-info module. + +# the location of the java command +[ -z "$JAVA" ] && JAVA=java + +java_version="`"$JAVA" -XX:-UsePerfData -Xmx5m -version 2>&1`" +result=$? +if [ $result -eq 127 ]; then + echo "Java not found, please install Java 17 or newer." 1>&2 + echo "For Ubuntu: sudo apt-get install openjdk-17-jre" 1>&2 + echo "If you have installed Java 17, but it is not in your PATH," 1>&2 + echo "let the environment variable JAVA point to the \"java\" binary." 1>&2 + exit 1 +fi +if [ $result -ne 0 ]; then + echo "Failed to execute Java VM, return code was $result and output was" 1>&2 + echo "$java_version" 1>&2 + echo "Please make sure you are able to execute Java processes by running \"$JAVA\"." 1>&2 + exit 1 +fi +java_version="`echo "$java_version" | grep -e "^\(java\|openjdk\) version" | cut -f2 -d\\\" | cut -f1 -d. | cut -f1 -d-`" +if [ -z "$java_version" ] || [ "$java_version" -lt 17 ] ; then + echo "Your Java version is too old, please install Java 17 or newer." 1>&2 + echo "For Ubuntu: sudo apt-get install openjdk-17-jre" 1>&2 + echo "If you have installed Java 17, but it is not in your PATH," 1>&2 + echo "let the environment variable JAVA point to the \"java\" binary." 1>&2 + exit 1 +fi + +platform="`uname -s`" +SEP=":" + +# where the project directory is, relative to the location of this script +case "$platform" in + Linux|CYGWIN*) + SCRIPT="$(readlink -f "$0")" + [ -n "$PATH_TO_JAVASMT" ] || PATH_TO_JAVASMT="$(readlink -f "$(dirname "$SCRIPT")")" + ;; + MINGW64*) + PATH_TO_JAVASMT="." # assume working directory is the current directory + SEP=";" + ;; + # other platforms like Mac don't support readlink -f + *) + [ -n "$PATH_TO_JAVASMT" ] || PATH_TO_JAVASMT="$(dirname "$0")" + ;; +esac + +# JavaSMT can be present either as the JAR that "ant jar" produces, which takes precedence, or as +# compiled classes below bin/. The JARs with the sources and the documentation carry no classes +# to run, so they are skipped. Several JARs would make it ambiguous which version runs, so this +# is refused. +JAVASMT_CLASSES="" +for jar in "$PATH_TO_JAVASMT"/java-smt-*.jar; do + case "$jar" in + *-sources.jar | *-javadoc.jar) continue ;; + esac + if [ -e "$jar" ]; then + if [ -n "$JAVASMT_CLASSES" ]; then + echo "Found several JavaSMT JARs, please remove all but one: $JAVASMT_CLASSES $jar" 1>&2 + exit 1 + fi + JAVASMT_CLASSES="$jar" + fi +done +if [ -z "$JAVASMT_CLASSES" ]; then + if [ -e "$PATH_TO_JAVASMT/bin/org/sosy_lab/java_smt/cmdline/JavaSMTMain.class" ]; then + JAVASMT_CLASSES="$PATH_TO_JAVASMT/bin" + else + echo "Could not find JavaSMT binary, please check path to project directory" 1>&2 + exit 1 + fi +fi + +# the classpath contains the classes of JavaSMT, the core JARs, and every solver present +CLASSPATH="$JAVASMT_CLASSES$SEP$PATH_TO_JAVASMT/lib/java/core/*" +for solver_dir in "$PATH_TO_JAVASMT"/lib/java/runtime-*; do + [ -d "$solver_dir" ] && CLASSPATH="$CLASSPATH$SEP$solver_dir/*" +done + +# loop over all input parameters and parse them +declare -a OPTIONS +declare -a JAVA_VM_ARGUMENTS +while [ $# -gt 0 ]; do + + case $1 in + -X*) # params starting with "-X" are used for JVM, this includes -Xmx + JAVA_VM_ARGUMENTS+=("$1") + ;; + *) # other params are only for JavaSMT + OPTIONS+=("$1") + ;; + esac + + shift +done + +# Determine temp dir to use for JVM +if [ -n "$TMPDIR" ]; then + JAVA_VM_ARGUMENTS+=("-Djava.io.tmpdir=$TMPDIR") +elif [ -n "$TEMP" ]; then + JAVA_VM_ARGUMENTS+=("-Djava.io.tmpdir=$TEMP") +elif [ -n "$TMP" ]; then + JAVA_VM_ARGUMENTS+=("-Djava.io.tmpdir=$TMP") +fi + +# Run JavaSMT. Everything given here comes before the arguments from the command +# line, so that a benchmark definition can override any of it. +exec "$JAVA" \ + -XX:+PerfDisableSharedMem \ + -Djava.awt.headless=true \ + "${JAVA_VM_ARGUMENTS[@]}" \ + -cp "$CLASSPATH" \ + org.sosy_lab.java_smt.cmdline.JavaSMTMain \ + "${OPTIONS[@]}" diff --git a/src/org/sosy_lab/java_smt/cmdline/CmdLineArgument.java b/src/org/sosy_lab/java_smt/cmdline/CmdLineArgument.java new file mode 100644 index 0000000000..4ae134aa34 --- /dev/null +++ b/src/org/sosy_lab/java_smt/cmdline/CmdLineArgument.java @@ -0,0 +1,158 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.cmdline; + +import static com.google.common.base.Preconditions.checkState; +import static org.sosy_lab.java_smt.cmdline.CmdLineArguments.putIfNotExistent; + +import com.google.common.base.Joiner; +import com.google.common.collect.FluentIterable; +import com.google.common.collect.ImmutableSet; +import com.google.errorprone.annotations.CanIgnoreReturnValue; +import java.util.Iterator; +import java.util.LinkedHashMap; +import java.util.Map; +import java.util.Map.Entry; +import org.checkerframework.checker.nullness.qual.Nullable; + +/** + * A command-line argument with one or more names, e.g., --solver and -solver + * . The first name is the main name that is shown in the help message. Sorting and equality + * are both based on the sequence of names. + */ +abstract class CmdLineArgument implements Comparable { + + private final ImmutableSet names; + private String description = ""; + + CmdLineArgument(String... pNames) { + names = ImmutableSet.copyOf(pNames); + } + + @CanIgnoreReturnValue + CmdLineArgument withDescription(String pDescription) { + description = pDescription; + return this; + } + + /** The first name given in the constructor. */ + String getMainName() { + return names.iterator().next(); + } + + @Override + public int compareTo(CmdLineArgument pOther) { + // Consistent with equals(): the string of an ImmutableSet lists the names in insertion order. + return names.toString().compareTo(pOther.names.toString()); + } + + @Override + public boolean equals(@Nullable Object pOther) { + if (this == pOther) { + return true; + } + return pOther instanceof CmdLineArgument other && names.asList().equals(other.names.asList()); + } + + @Override + public int hashCode() { + return names.asList().hashCode(); + } + + @Override + public String toString() { + String s = + FluentIterable.from(names) + .filter(pName -> !CmdLineArguments.isOldStyleArgument(pName)) + .join(Joiner.on("/")); + if (description.isEmpty()) { + return s; + } else { + return String.format("%1$-20s %2$s", s, description); + } + } + + /** + * Applies this argument if it matches the current argument. + * + * @return whether the current argument matched one of the names of this argument + */ + boolean apply(Map pProperties, String pCurrentArg, Iterator pArgsIt) + throws InvalidCmdlineArgumentException { + if (names.contains(pCurrentArg)) { + apply0(pProperties, pCurrentArg, pArgsIt); + return true; + } + return false; + } + + abstract void apply0( + Map pProperties, String pCurrentArg, Iterator pArgsIt) + throws InvalidCmdlineArgumentException; + + /** A command-line argument with one value that is given as the next argument. */ + static class CmdLineArgument1 extends CmdLineArgument { + + private @Nullable String option; + + CmdLineArgument1(String... pNames) { + super(pNames); + } + + /** Sets the name of the option that receives the value of this argument. */ + @CanIgnoreReturnValue + CmdLineArgument1 settingOption(String pOption) { + option = pOption; + return this; + } + + @Override + final void apply0(Map pProperties, String pCurrentArg, Iterator pArgsIt) + throws InvalidCmdlineArgumentException { + if (pArgsIt.hasNext()) { + handleArg(pProperties, pArgsIt.next()); + } else { + throw new InvalidCmdlineArgumentException(pCurrentArg + " argument missing."); + } + } + + void handleArg(Map pProperties, String pArgValue) + throws InvalidCmdlineArgumentException { + checkState(option != null, "settingOption() has to be called first"); + putIfNotExistent(pProperties, option, pArgValue); + } + } + + /** A command-line argument that sets some properties to fixed values. */ + static class PropertyAddingCmdLineArgument extends CmdLineArgument { + + // Insertion order determines which conflict is reported first. + private final Map additionalIfNotExistentArgs = new LinkedHashMap<>(); + + PropertyAddingCmdLineArgument(String... pNames) { + super(pNames); + } + + @CanIgnoreReturnValue + PropertyAddingCmdLineArgument settingProperty(String pName, String pValue) { + additionalIfNotExistentArgs.put(pName, pValue); + return this; + } + + @Override + void apply0(Map pProperties, String pCurrentArg, Iterator pArgsIt) + throws InvalidCmdlineArgumentException { + for (Entry e : additionalIfNotExistentArgs.entrySet()) { + putIfNotExistent(pProperties, e.getKey(), e.getValue()); + } + } + } +} diff --git a/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java b/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java new file mode 100644 index 0000000000..6a8646f48d --- /dev/null +++ b/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java @@ -0,0 +1,197 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.cmdline; + +import com.google.common.base.Joiner; +import com.google.common.base.Preconditions; +import com.google.common.collect.ImmutableSet; +import com.google.common.collect.ImmutableSortedSet; +import com.google.common.collect.Iterators; +import java.nio.file.InvalidPathException; +import java.nio.file.Path; +import java.util.HashMap; +import java.util.Iterator; +import java.util.Map; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; +import org.sosy_lab.java_smt.cmdline.CmdLineArgument.CmdLineArgument1; +import org.sosy_lab.java_smt.cmdline.CmdLineArgument.PropertyAddingCmdLineArgument; +import org.sosy_lab.java_smt.solvers.opensmt.Logics; + +/** Processes command-line arguments for JavaSMT. */ +public final class CmdLineArguments { + + private CmdLineArguments() {} + + // Keys in the map returned by processArguments() + static final String SOLVER_OPTION = "solver.solver"; + static final String OPENSMT_LOGIC_OPTION = "solver.opensmt.logic"; + static final String Z3_LOGIC_OPTION = "solver.z3.logic"; + static final String FILE_OPTION = "smt2.file"; + static final String HELP_OPTION = "help"; + + /** The command-line argument that requests the help message. */ + static final String HELP_ARGUMENT = "--help"; + + /** Solvers that cannot parse SMT-LIB2 input, see {@link #printHelp}. */ + private static final ImmutableSet SOLVERS_WITHOUT_PARSER = + ImmutableSet.of(Solvers.BOOLECTOR, Solvers.CVC4, Solvers.YICES2); + + /** Solvers that have an option for the logic, i.e., for which --logic is effective. */ + static final ImmutableSet SOLVERS_WITH_LOGIC_OPTION = + ImmutableSet.of(Solvers.OPENSMT, Solvers.Z3); + + private static final ImmutableSortedSet CMD_LINE_ARGS = + ImmutableSortedSet.of( + new CmdLineArgument1("--solver", "-solver") + .settingOption(SOLVER_OPTION) + .withDescription("Set the SMT solver, default: " + JavaSMTMain.DEFAULT_SOLVER), + new CmdLineArgument1("--logic", "-logic") + .settingOption(OPENSMT_LOGIC_OPTION) + .withDescription("Set the logic for OpenSMT and Z3, ignored for other solvers"), + new PropertyAddingCmdLineArgument(HELP_ARGUMENT, "-h", "-help") + .settingProperty(HELP_OPTION, "true") + .withDescription("Print this help message")); + + /** + * Processes command-line arguments and returns a map of option names to values. + * + * @param pArgs Raw command-line arguments + * @return Map of option names to their values + * @throws InvalidCmdlineArgumentException if arguments are invalid + */ + public static Map processArguments(String[] pArgs) + throws InvalidCmdlineArgumentException { + Preconditions.checkNotNull(pArgs); + + Map properties = new HashMap<>(); + Iterator argsIt = Iterators.forArray(pArgs); + + while (argsIt.hasNext()) { + String arg = argsIt.next(); + + boolean found = false; + for (CmdLineArgument cmd : CMD_LINE_ARGS) { + if (cmd.apply(properties, arg, argsIt)) { + found = true; + break; + } + } + + if (!found) { + if (arg.startsWith("-")) { + throw new InvalidCmdlineArgumentException("Unknown command-line argument: " + arg); + } else { + if (properties.containsKey(FILE_OPTION)) { + throw new InvalidCmdlineArgumentException( + "Multiple input files are not supported: " + + properties.get(FILE_OPTION) + + " and " + + arg); + } + final Path file; + try { + file = Path.of(arg); + } catch (InvalidPathException e) { + throw new InvalidCmdlineArgumentException("Invalid path of SMT2 file: " + arg, e); + } + properties.put(FILE_OPTION, file.toString()); + } + } + } + + // OpenSMT and Z3 read the logic from different options, and --logic sets both of them. + // Only the solver that is used reads its option, the other one is never looked at. + String logic = properties.get(OPENSMT_LOGIC_OPTION); + if (logic != null) { + properties.put(Z3_LOGIC_OPTION, logic); + } + + return properties; + } + + /** Whether the argument has the old single-dash style, e.g., -solver. */ + static boolean isOldStyleArgument(String pArg) { + return pArg.length() > 2 && pArg.startsWith("-") && !pArg.startsWith("--"); + } + + private static void printVersion(Appendable pOut) { + Output.println(pOut, ""); + // The version is only available from the manifest of the JAR, not when running from bin/. + final String version; + Package pkg = CmdLineArguments.class.getPackage(); + if (pkg != null && pkg.getImplementationVersion() != null) { + version = pkg.getImplementationVersion(); + } else { + version = "unknown"; + } + Output.println(pOut, "JavaSMT " + version); + } + + /** + * Prints the help message, including the allowed arguments and the restrictions on the input, to + * the given output. + * + * @param pOut The output to print to + */ + public static void printHelp(Appendable pOut) { + printVersion(pOut); + Output.println(pOut, ""); + Output.println(pOut, "Usage: javasmt [--solver SOLVER] [--logic LOGIC] "); + Output.println(pOut, "Options:"); + for (CmdLineArgument cmdLineArg : CMD_LINE_ARGS) { + if (!isOldStyleArgument(cmdLineArg.getMainName())) { + Output.println(pOut, " " + cmdLineArg); + } + } + Output.println(pOut, ""); + Output.println( + pOut, + "JavaSMT checks the satisfiability of the assertions in the given SMT-LIB2 file with the"); + Output.println( + pOut, "selected solver and prints exactly one of sat, unsat, or unknown on stdout, or"); + Output.println( + pOut, "nothing in case of an error. All other output goes to stderr. The exit code is 0"); + Output.println(pOut, "for sat and unsat, and 1 for unknown and for all errors."); + Output.println(pOut, ""); + Output.println(pOut, "Solvers: " + Joiner.on(", ").join(Solvers.values())); + Output.println( + pOut, + "Solvers without a parser for SMT-LIB2 input cannot be used: " + + Joiner.on(", ").join(SOLVERS_WITHOUT_PARSER)); + Output.println(pOut, "Logics for OpenSMT: " + Joiner.on(", ").join(Logics.values())); + Output.println(pOut, "Logics for Z3: the SMT-LIB2 logics, e.g., QF_LIA, or ALL, the default."); + Output.println( + pOut, "Arguments starting with -X, e.g., -Xmx4g, are passed to the JVM by the launcher."); + Output.println(pOut, ""); + Output.println(pOut, "Restrictions on the SMT-LIB2 file:"); + Output.println(pOut, " - It has to contain exactly one (check-sat) command."); + Output.println(pOut, " - All assertions have to precede the (check-sat) command."); + Output.println(pOut, " - (check-sat-assuming ...) is not supported."); + Output.println( + pOut, " - (push ...), (pop ...), (reset), and (reset-assertions) are not supported."); + Output.println(pOut, " - (exit) is only allowed as the last command."); + Output.println( + pOut, " - Only declarations, definitions, and assertions are evaluated, other commands"); + Output.println(pOut, " such as (set-option ...) or (get-model) are ignored."); + Output.println(pOut, " - (set-logic ...) is ignored as well, use --logic to select the logic."); + } + + static void putIfNotExistent(Map pProperties, String pKey, String pValue) + throws InvalidCmdlineArgumentException { + if (pProperties.containsKey(pKey) && !pProperties.get(pKey).equals(pValue)) { + throw new InvalidCmdlineArgumentException( + String.format( + "Option %s specified twice on command-line with values '%s' and '%s'.", + pKey, pProperties.get(pKey), pValue)); + } + pProperties.put(pKey, pValue); + } +} diff --git a/src/org/sosy_lab/java_smt/cmdline/InvalidCmdlineArgumentException.java b/src/org/sosy_lab/java_smt/cmdline/InvalidCmdlineArgumentException.java new file mode 100644 index 0000000000..98e51d6ee9 --- /dev/null +++ b/src/org/sosy_lab/java_smt/cmdline/InvalidCmdlineArgumentException.java @@ -0,0 +1,27 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.cmdline; + +import java.io.Serial; + +/** Exception thrown when an invalid command-line argument is provided. */ +public class InvalidCmdlineArgumentException extends Exception { + + @Serial private static final long serialVersionUID = -6526968677815416436L; + + public InvalidCmdlineArgumentException(String pMsg) { + super(pMsg); + } + + public InvalidCmdlineArgumentException(String pMsg, Throwable pCause) { + super(pMsg, pCause); + } +} diff --git a/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java b/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java new file mode 100644 index 0000000000..34e66b42d7 --- /dev/null +++ b/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java @@ -0,0 +1,378 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.cmdline; + +import java.io.IOException; +import java.io.UncheckedIOException; +import java.nio.file.Files; +import java.nio.file.InvalidPathException; +import java.nio.file.Path; +import java.util.List; +import java.util.Locale; +import java.util.Map; +import java.util.Optional; +import java.util.logging.Handler; +import java.util.logging.Level; +import java.util.logging.LogRecord; +import java.util.regex.Pattern; +import org.checkerframework.checker.nullness.qual.Nullable; +import org.sosy_lab.common.ShutdownManager; +import org.sosy_lab.common.ShutdownNotifier; +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.BasicLogManager; +import org.sosy_lab.common.log.ConsoleLogFormatter; +import org.sosy_lab.common.log.LogManager; +import org.sosy_lab.java_smt.SolverContextFactory; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.ProverEnvironment; +import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.basicimpl.SMTLibTokenizer; + +/** + * Main entry point for JavaSMT command-line interface. Executes SMT2 files using a selected solver + * and reports the result (sat/unsat/unknown). + * + *

Contract for callers such as benchmarking frameworks: exactly one of sat, + * unsat, or unknown is printed to stdout, or nothing in case of an error. All + * diagnostics and logging go to stderr. The exit code is 0 for sat and unsat + * , and {@link #ERROR_EXIT_CODE} for unknown and for all errors. If the JVM is + * terminated by a signal, the exit code is the one of the JVM, e.g., 143 for SIGTERM. + */ +public final class JavaSMTMain { + + /** Exit code for unknown results and for all errors. */ + public static final int ERROR_EXIT_CODE = 1; + + /** The solver that is used if none is given on the command line. */ + static final Solvers DEFAULT_SOLVER = Solvers.SMTINTERPOL; + + private static final String COULD_NOT_PARSE_FILE = "Could not parse SMT2 file"; + private static final String INVALID_CONFIGURATION = "Invalid configuration: %s"; + + /** Matches exactly the command (check-sat). */ + private static final Pattern CHECK_SAT_COMMAND = Pattern.compile("\\(\\s*check-sat\\s*\\)"); + + /** Matches every command starting with check-sat, e.g., check-sat-assuming. */ + private static final Pattern CHECK_SAT_LIKE_COMMAND = + Pattern.compile("\\(\\s*check-sat[\\S\\s]*"); + + /** + * Main method for running JavaSMT from command line. + * + * @param args Command-line arguments: [--solver SOLVER] [--logic LOGIC] file.smt2 + */ + public static void main(String[] args) { + // JavaSMT uses American English for output, so make sure numbers are formatted appropriately. + Locale.setDefault(Locale.US); + + // Ctrl+C or SIGTERM requests a shutdown from the solver, such that "unknown" is reported. + ShutdownManager shutdownManager = ShutdownManager.create(); + ShutdownHook shutdownHook = new ShutdownHook(shutdownManager); + Runtime.getRuntime().addShutdownHook(shutdownHook); + + int exitCode = run(args, System.out, System.err, shutdownManager.getNotifier()); + System.out.flush(); + System.err.flush(); + // System.out and System.err do not throw on I/O errors but only record them internally, + // so the result might not have been delivered even though nothing was reported. + if (System.out.checkError() || System.err.checkError()) { + exitCode = ERROR_EXIT_CODE; + } + + // The result is reported, the hook must not delay the exit anymore. + shutdownHook.disableAndStop(); + System.exit(exitCode); + } + + /** + * Runs the command-line interface with the given arguments. This method has the same behavior as + * {@link #main(String[])}, but writes to the given streams and returns the exit code instead of + * terminating the JVM, such that it can be used from tests. + * + * @param pArgs Command-line arguments: [--solver SOLVER] [--logic LOGIC] file.smt2 + * @param pOut output for the result, i.e., sat, unsat, unknown, or the help message + * @param pErr output for diagnostics and logging + * @param pShutdownNotifier a shutdown request aborts the solver, and unknown is reported + * @return exit code, 0 for sat and unsat, {@link #ERROR_EXIT_CODE} otherwise + */ + public static int run( + String[] pArgs, Appendable pOut, Appendable pErr, ShutdownNotifier pShutdownNotifier) { + final String[] args; + if (pArgs.length == 0) { + // be nice to user + args = new String[] {CmdLineArguments.HELP_ARGUMENT}; + } else { + args = pArgs; + } + + final Map cmdLineOptions; + try { + cmdLineOptions = CmdLineArguments.processArguments(args); + } catch (InvalidCmdlineArgumentException e) { + Output.error(pErr, "Could not process command line arguments: %s", e.getMessage()); + return ERROR_EXIT_CODE; + } + + if (cmdLineOptions.remove(CmdLineArguments.HELP_OPTION) != null) { + CmdLineArguments.printHelp(pOut); + return 0; + } + + final Configuration config; + final MainOptions options; + try { + config = Configuration.builder().setOptions(cmdLineOptions).build(); + options = new MainOptions(config); + } catch (InvalidConfigurationException e) { + Output.error(pErr, INVALID_CONFIGURATION, describe(e)); + return ERROR_EXIT_CODE; + } + + if (options.smt2File == null) { + Output.error(pErr, "No SMT2 file given, see --help for usage."); + return ERROR_EXIT_CODE; + } + + LogManager logManager = createLogManager(pErr); + + // --logic sets the logic option of every solver that has one, + // so either of them shows that it was given. + if (cmdLineOptions.containsKey(CmdLineArguments.OPENSMT_LOGIC_OPTION) + && !CmdLineArguments.SOLVERS_WITH_LOGIC_OPTION.contains(options.solver)) { + logManager.logf( + Level.WARNING, + "Option --logic is only effective with the solvers OpenSMT and Z3, but solver is set" + + " to %s. The logic setting will be ignored.", + options.solver); + } + + final String input; + try { + input = Files.readString(Path.of(options.smt2File)); + } catch (IOException | InvalidPathException e) { + Output.error(pErr, "Could not read SMT2 file: %s", describe(e)); + return ERROR_EXIT_CODE; + } + + final Optional scriptError; + try { + scriptError = checkScript(input); + } catch (IllegalArgumentException e) { + // The tokenizer rejects syntactically broken input, e.g., unbalanced parentheses. + Output.error(pErr, COULD_NOT_PARSE_FILE + ": %s", describe(e)); + return ERROR_EXIT_CODE; + } + if (scriptError.isPresent()) { + Output.error(pErr, "%s: %s", scriptError.orElseThrow(), options.smt2File); + return ERROR_EXIT_CODE; + } + + return solve(config, logManager, pShutdownNotifier, options.solver, input, pOut, pErr); + } + + /** + * Parses the assertions of the script with the given solver and checks their satisfiability. + * + * @return exit code, 0 for sat and unsat, {@link #ERROR_EXIT_CODE} otherwise + */ + private static int solve( + Configuration pConfig, + LogManager pLogManager, + ShutdownNotifier pShutdownNotifier, + Solvers pSolver, + String pInput, + Appendable pOut, + Appendable pErr) { + + try (SolverContext context = + SolverContextFactory.createSolverContext( + pConfig, pLogManager, pShutdownNotifier, pSolver)) { + + // Parse before creating the prover: Princess does not know symbols that are declared after + // the prover environment was created. + final List formulas; + try { + formulas = context.getFormulaManager().parseAll(pInput); + } catch (IllegalArgumentException e) { + // All parsers report input they cannot handle like this: syntax errors, undeclared + // symbols, type errors, unsupported sorts or commands. + Output.error(pErr, COULD_NOT_PARSE_FILE + " with %s: %s", pSolver, describe(e)); + return ERROR_EXIT_CODE; + } catch (UnsupportedOperationException e) { + // Solvers without a parser for SMT-LIB2, e.g., Yices2. + final String details; + if (e.getMessage() == null) { + details = ""; + } else { + details = " " + e.getMessage(); + } + Output.error( + pErr, "Solver %s does not support parsing SMT-LIB2 input.%s", pSolver, details); + return ERROR_EXIT_CODE; + } + // Any other exception is unexpected, e.g., a bug in a solver binding, and is intentionally + // not caught, such that it terminates the program with a stack trace on stderr. + + final SolverResult result; + try (ProverEnvironment prover = context.newProverEnvironment()) { + for (BooleanFormula formula : formulas) { + prover.addConstraint(formula); + } + if (prover.isUnsat()) { + result = SolverResult.UNSAT; + } else { + result = SolverResult.SAT; + } + } + Output.println(pOut, result.toString()); + return 0; + + } catch (InvalidConfigurationException e) { + Output.error(pErr, INVALID_CONFIGURATION, describe(e)); + return ERROR_EXIT_CODE; + } catch (InterruptedException e) { + // Thrown by the solver after a shutdown request, see ShutdownHook. The exception carries + // the reason of the shutdown request. + pLogManager.logUserException(Level.WARNING, e, "SMT execution was interrupted"); + Output.println(pOut, SolverResult.UNKNOWN.toString()); + return ERROR_EXIT_CODE; + } catch (SolverException e) { + pLogManager.logUserException(Level.SEVERE, e, "Error executing SMT2 solver"); + Output.println(pOut, SolverResult.UNKNOWN.toString()); + return ERROR_EXIT_CODE; + } + } + + /** The message of an exception, or its class if it has no message. */ + private static String describe(Throwable pException) { + if (pException.getMessage() != null) { + return pException.getMessage(); + } else { + return pException.getClass().getSimpleName(); + } + } + + /** + * Checks the commands of the script for those that cannot be handled. + * + *

The parser silently ignores everything that is not a declaration, definition, or assertion, + * so an empty or unparsable file would be reported as sat. Every benchmark that asks a question + * contains (check-sat), so we require it. + * + * @return an error message if the script cannot be handled + * @throws IllegalArgumentException if the tokenizer rejects the script, e.g., for unbalanced + * parentheses + */ + private static Optional checkScript(String pInput) { + // TODO: parseAll does not track the assertion stack, i.e., (push ...) and (pop ...) are not + // applied, and (reset) and (reset-assertions) are ignored. The assertions of a script using + // these commands can therefore not be reconstructed, and such scripts are rejected here for + // now. The same holds for (exit) that is not the last command. + // Furthermore, each (check-sat) is a separate query over the assertions on the stack at that + // point, but we perform a single check over all assertions of the script, so only one + // (check-sat) is allowed, no assertion may follow it, and (check-sat-assuming ...) is not + // supported. + // To be supported once parseAll handles the assertion stack, resets, and check-sat commands. + int checkSatCount = 0; + boolean afterExit = false; + for (String token : SMTLibTokenizer.of(pInput)) { + if (afterExit) { + return Optional.of("Command (exit) is only allowed as the last command in the SMT2 file"); + } + if (!token.startsWith("(")) { + // The parser silently ignores everything that is not a command. + return Optional.of(String.format("Unexpected input '%s' in the SMT2 file", token)); + } + if (SMTLibTokenizer.isForbiddenToken(token)) { + // push, pop, reset-assertions, reset + return Optional.of( + String.format( + "Command %s is not supported, the assertion stack is not tracked when parsing" + + " SMT2 files", + token)); + } else if (SMTLibTokenizer.isExitToken(token)) { + afterExit = true; + } else if (CHECK_SAT_COMMAND.matcher(token).matches()) { + checkSatCount++; + } else if (CHECK_SAT_LIKE_COMMAND.matcher(token).matches()) { + return Optional.of( + String.format("Command %s is not supported, only (check-sat) is supported", token)); + } else if (SMTLibTokenizer.isAssertToken(token) && checkSatCount > 0) { + return Optional.of( + "Command (assert ...) after (check-sat) is not supported, all assertions have to" + + " precede (check-sat)"); + } + } + if (checkSatCount == 0) { + return Optional.of("SMT2 file contains no (check-sat) command"); + } + if (checkSatCount > 1) { + return Optional.of( + String.format( + "Only one (check-sat) command is supported, but the SMT2 file contains %d", + checkSatCount)); + } + return Optional.empty(); + } + + /** Creates a logger that writes messages of level INFO and above to the given output. */ + private static LogManager createLogManager(Appendable pErr) { + Handler handler = + new Handler() { + @Override + public void publish(LogRecord pRecord) { + if (isLoggable(pRecord)) { + try { + pErr.append(getFormatter().format(pRecord)); + } catch (IOException e) { + throw new UncheckedIOException(e); + } + } + } + + @Override + public void flush() {} + + @Override + public void close() {} + }; + handler.setFormatter(ConsoleLogFormatter.withColorsIfPossible()); + handler.setLevel(Level.INFO); + return BasicLogManager.createWithHandler(handler); + } + + @Options + private static final class MainOptions { + + private MainOptions(Configuration pConfig) throws InvalidConfigurationException { + pConfig.inject(this); + } + + @Option( + secure = true, + name = CmdLineArguments.FILE_OPTION, + description = "The SMT2 file to execute") + private @Nullable String smt2File = null; + + @Option( + secure = true, + name = CmdLineArguments.SOLVER_OPTION, + description = "The SMT solver to use") + private Solvers solver = DEFAULT_SOLVER; + } + + private JavaSMTMain() {} +} diff --git a/src/org/sosy_lab/java_smt/cmdline/Output.java b/src/org/sosy_lab/java_smt/cmdline/Output.java new file mode 100644 index 0000000000..f7d556d8fc --- /dev/null +++ b/src/org/sosy_lab/java_smt/cmdline/Output.java @@ -0,0 +1,59 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.cmdline; + +import com.google.errorprone.annotations.FormatMethod; +import com.google.errorprone.annotations.FormatString; +import java.io.IOException; +import java.io.UncheckedIOException; +import org.sosy_lab.common.io.IO; + +/** + * Utility class for output in JavaSMT command-line interface. All output goes to an {@link + * Appendable}, such that stdout and stderr can be replaced in tests. + */ +final class Output { + + private Output() {} + + private static final boolean USE_COLORS = IO.mayUseColorForOutput(); + private static final String ERROR_COLOR = "\033[31;1m"; // bold red + private static final String REGULAR_COLOR = "\033[m"; + + /** Appends the line and a line separator to the given output. */ + static void println(Appendable pOut, String pLine) { + try { + pOut.append(pLine).append(System.lineSeparator()); + } catch (IOException e) { + throw new UncheckedIOException(e); + } + } + + /** + * Prints an error message to the given output, in color if the console supports it. This method + * does not terminate the program, the caller is responsible for returning the exit code. + * + * @param pErr the output for error messages, usually {@link System#err} + * @param pMsg the message as format string for {@link String#format} + * @param pArgs the arguments for the format string + */ + @FormatMethod + static void error(Appendable pErr, @FormatString String pMsg, Object... pArgs) { + final String message; + if (USE_COLORS) { + message = ERROR_COLOR + String.format(pMsg, pArgs) + REGULAR_COLOR; + } else { + message = String.format(pMsg, pArgs); + } + println(pErr, ""); + println(pErr, message); + } +} diff --git a/src/org/sosy_lab/java_smt/cmdline/ShutdownHook.java b/src/org/sosy_lab/java_smt/cmdline/ShutdownHook.java new file mode 100644 index 0000000000..97c4536e64 --- /dev/null +++ b/src/org/sosy_lab/java_smt/cmdline/ShutdownHook.java @@ -0,0 +1,70 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.cmdline; + +import static com.google.common.base.Preconditions.checkNotNull; + +import org.sosy_lab.common.ShutdownManager; + +/** + * Shutdown hook for the JVM that requests a shutdown from the solver if the JVM is terminated while + * the solver is running, e.g., because Ctrl+C was pressed or SIGTERM was sent. The hook then keeps + * the JVM alive for a grace period, such that the main thread can report unknown and + * close the solver. + */ +final class ShutdownHook extends Thread { + + /** + * How long to wait for the main thread after a shutdown request. Solvers are not guaranteed to + * respond to shutdown requests, see {@link org.sosy_lab.java_smt.api.ProverEnvironment}. + */ + private static final long GRACE_PERIOD_MILLIS = 10_000; + + private final ShutdownManager shutdownManager; + private final Thread mainThread; + + // Whether this hook should act at all. Monotonic (true -> false). + private volatile boolean enabled = true; + + /** + * Create a shutdown hook. This constructor needs to be called from the thread that runs the + * solver, as the hook waits for this thread to finish. + */ + ShutdownHook(ShutdownManager pShutdownManager) { + super("Shutdown Hook"); + shutdownManager = checkNotNull(pShutdownManager); + mainThread = Thread.currentThread(); + } + + /** + * Disable this hook once the result is reported, such that it neither requests a shutdown nor + * delays the exit of the JVM. Must be called before {@link System#exit(int)}, otherwise the exit + * would wait for this hook, which waits for the main thread that is blocked in the exit. + */ + void disableAndStop() { + enabled = false; + interrupt(); // in case it is already waiting for the main thread + } + + @SuppressWarnings("ThreadJoinLoop") // interrupt is used on purpose by disableAndStop() + @Override + public void run() { + if (enabled && mainThread.isAlive()) { + shutdownManager.requestShutdown( + "The JVM is shutting down, probably because Ctrl+C was pressed."); + try { + mainThread.join(GRACE_PERIOD_MILLIS); + } catch (InterruptedException expected) { + // disableAndStop() was called, the result is reported + } + } + } +} diff --git a/src/org/sosy_lab/java_smt/cmdline/SolverResult.java b/src/org/sosy_lab/java_smt/cmdline/SolverResult.java new file mode 100644 index 0000000000..ef2664029f --- /dev/null +++ b/src/org/sosy_lab/java_smt/cmdline/SolverResult.java @@ -0,0 +1,30 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.cmdline; + +/** The result of a satisfiability check, as reported by the command-line interface. */ +enum SolverResult { + SAT("sat"), + UNSAT("unsat"), + UNKNOWN("unknown"); + + private final String output; + + SolverResult(String pOutput) { + output = pOutput; + } + + /** The result as printed on stdout, i.e., in SMT-LIB2 notation. */ + @Override + public String toString() { + return output; + } +} diff --git a/src/org/sosy_lab/java_smt/cmdline/package-info.java b/src/org/sosy_lab/java_smt/cmdline/package-info.java new file mode 100644 index 0000000000..469ff40366 --- /dev/null +++ b/src/org/sosy_lab/java_smt/cmdline/package-info.java @@ -0,0 +1,16 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +/** The frontend of JavaSMT for using it as a standalone application on the command line. */ +@com.google.errorprone.annotations.CheckReturnValue +@javax.annotation.ParametersAreNonnullByDefault +@org.sosy_lab.common.annotations.FieldsAreNonnullByDefault +@org.sosy_lab.common.annotations.ReturnValuesAreNonnullByDefault +package org.sosy_lab.java_smt.cmdline; diff --git a/src/org/sosy_lab/java_smt/test/JavaSMTMainTest.java b/src/org/sosy_lab/java_smt/test/JavaSMTMainTest.java new file mode 100644 index 0000000000..9928cd9366 --- /dev/null +++ b/src/org/sosy_lab/java_smt/test/JavaSMTMainTest.java @@ -0,0 +1,565 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.test; + +import static com.google.common.truth.Truth.assertThat; +import static com.google.common.truth.TruthJUnit.assume; +import static org.junit.Assert.assertThrows; + +import com.google.common.collect.ImmutableList; +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.Locale; +import java.util.Map; +import java.util.concurrent.TimeUnit; +import org.junit.Rule; +import org.junit.Test; +import org.junit.rules.TemporaryFolder; +import org.sosy_lab.common.ShutdownManager; +import org.sosy_lab.common.ShutdownNotifier; +import org.sosy_lab.java_smt.cmdline.CmdLineArguments; +import org.sosy_lab.java_smt.cmdline.InvalidCmdlineArgumentException; +import org.sosy_lab.java_smt.cmdline.JavaSMTMain; + +public class JavaSMTMainTest { + + private static final String SAT_INPUT = + """ + (set-logic QF_LIA) + (declare-fun x () Int) + (assert (> x 0)) + (check-sat) + (exit) + """; + + private static final String UNSAT_INPUT = + """ + (set-info :smt-lib-version 2.6) + (set-logic QF_LIA) + (declare-fun x () Int) + (assert (> x 0)) + (assert (< x 0)) + (check-sat) + """; + + private static final String NL = System.lineSeparator(); + private static final String SOLVER = "--solver"; + private static final String SMTINTERPOL = "SMTINTERPOL"; + private static final String PRINCESS = "PRINCESS"; + + @Rule public TemporaryFolder tempDir = new TemporaryFolder(); + + /** The result of one invocation of the command-line interface. */ + private record Run(int exitCode, String out, String err) {} + + /** Runs the command-line interface in-process, capturing stdout and stderr. */ + private static Run run(String... args) { + return run(ShutdownNotifier.createDummy(), args); + } + + private static Run run(ShutdownNotifier shutdownNotifier, String... args) { + StringBuilder out = new StringBuilder(); + StringBuilder err = new StringBuilder(); + int exitCode = JavaSMTMain.run(args, out, err, shutdownNotifier); + return new Run(exitCode, out.toString(), err.toString()); + } + + private String smt2File(String content) throws IOException { + Path file = Files.createTempFile(tempDir.getRoot().toPath(), "input", ".smt2"); + Files.writeString(file, content); + return file.toString(); + } + + // Tests for the whole command-line interface. + // Only the pure-Java solvers SMTInterpol and Princess are used, so that these tests can run on + // every platform without native libraries. + + @Test + public void testRunSat() throws IOException { + Run r = run(SOLVER, SMTINTERPOL, smt2File(SAT_INPUT)); + assertThat(r.out()).isEqualTo("sat" + NL); + assertThat(r.exitCode()).isEqualTo(0); + } + + @Test + public void testRunUnsatWithSeveralAssertions() throws IOException { + Run r = run(SOLVER, PRINCESS, smt2File(UNSAT_INPUT)); + assertThat(r.out()).isEqualTo("unsat" + NL); + assertThat(r.exitCode()).isEqualTo(0); + } + + @Test + public void testRunDefaultSolverIsSmtInterpol() throws IOException { + Run r = run(smt2File(UNSAT_INPUT)); + assertThat(r.out()).isEqualTo("unsat" + NL); + assertThat(r.exitCode()).isEqualTo(0); + assertThat(r.err()).isEmpty(); + } + + @Test + public void testRunSolverNameIsCaseInsensitive() throws IOException { + Run r = run(SOLVER, "smtinterpol", smt2File(SAT_INPUT)); + assertThat(r.out()).isEqualTo("sat" + NL); + assertThat(r.exitCode()).isEqualTo(0); + } + + @Test + public void testRunHelpTakesPrecedenceOverFile() throws IOException { + Run r = run("--help", SOLVER, SMTINTERPOL, smt2File(SAT_INPUT)); + assertThat(r.out()).isNotEmpty(); + assertThat(r.out()).isNotEqualTo("sat" + NL); + assertThat(r.err()).isEmpty(); + assertThat(r.exitCode()).isEqualTo(0); + } + + @Test + public void testRunWithoutArgumentsPrintsHelp() { + Run r = run(); + assertThat(r.out()).isNotEmpty(); + assertThat(r.err()).isEmpty(); + assertThat(r.exitCode()).isEqualTo(0); + } + + @Test + public void testRunWithoutFileIsAnError() { + Run r = run(SOLVER, SMTINTERPOL); + assertThat(r.out()).isEmpty(); + assertThat(r.err()).isNotEmpty(); + assertThat(r.exitCode()).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test + public void testRunUnknownArgumentIsAnError() throws IOException { + Run r = run("--unknown", smt2File(SAT_INPUT)); + assertThat(r.out()).isEmpty(); + assertThat(r.err()).isNotEmpty(); + assertThat(r.exitCode()).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test + public void testRunUnknownSolverIsAnError() throws IOException { + Run r = run(SOLVER, "NOSUCHSOLVER", smt2File(SAT_INPUT)); + assertThat(r.out()).isEmpty(); + assertThat(r.err()).isNotEmpty(); + assertThat(r.exitCode()).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test + public void testRunMissingFileIsAnError() { + Run r = run(SOLVER, SMTINTERPOL, tempDir.getRoot().toPath().resolve("missing.smt2").toString()); + assertThat(r.out()).isEmpty(); + assertThat(r.err()).isNotEmpty(); + assertThat(r.exitCode()).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test + public void testRunEmptyFileIsAnError() throws IOException { + Run r = run(SOLVER, SMTINTERPOL, smt2File("")); + assertThat(r.out()).isEmpty(); + assertThat(r.err()).isNotEmpty(); + assertThat(r.exitCode()).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test + public void testRunFileWithoutCommandsIsAnError() throws IOException { + Run r = run(SOLVER, SMTINTERPOL, smt2File("this is not an SMT2 file\n")); + assertThat(r.out()).isEmpty(); + assertThat(r.err()).isNotEmpty(); + assertThat(r.exitCode()).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test + public void testRunUnparsableFileIsAnError() throws IOException { + // The parser would ignore the text and report sat for the (check-sat). + Run r = run(SOLVER, SMTINTERPOL, smt2File("this is not an SMT2 file\n(check-sat)\n")); + assertThat(r.out()).isEmpty(); + assertThat(r.err()).isNotEmpty(); + assertThat(r.exitCode()).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test + public void testRunAssertionAfterCheckSatIsAnError() throws IOException { + // parseAll collects all assertions, the answer would be unsat instead of sat. + String input = "(declare-const x Int)\n(assert (> x 0))\n(check-sat)\n(assert (< x 0))\n"; + Run r = run(SOLVER, SMTINTERPOL, smt2File(input)); + assertThat(r.out()).isEmpty(); + assertThat(r.err()).isNotEmpty(); + assertThat(r.exitCode()).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test + public void testRunWithoutAssertionsIsSat() throws IOException { + Run r = run(SOLVER, SMTINTERPOL, smt2File("(set-logic QF_LIA)\n(check-sat)\n")); + assertThat(r.out()).isEqualTo("sat" + NL); + assertThat(r.exitCode()).isEqualTo(0); + } + + @Test + public void testRunUnbalancedParenthesesIsAnError() throws IOException { + Run r = run(SOLVER, SMTINTERPOL, smt2File("(declare-fun x () Int)\n(assert (> x 0)\n")); + assertThat(r.out()).isEmpty(); + assertThat(r.err()).isNotEmpty(); + assertThat(r.exitCode()).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test + public void testRunUndeclaredSymbolIsAnError() throws IOException { + Run r = run(SOLVER, SMTINTERPOL, smt2File("(assert (> y 0))\n(check-sat)\n")); + assertThat(r.out()).isEmpty(); + assertThat(r.err()).isNotEmpty(); + assertThat(r.exitCode()).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test + public void testRunTypeErrorIsAnError() throws IOException { + Run r = + run( + SOLVER, + PRINCESS, + smt2File("(declare-fun x () Int)\n(assert (> x true))\n(check-sat)\n")); + assertThat(r.out()).isEmpty(); + assertThat(r.err()).isNotEmpty(); + assertThat(r.exitCode()).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test + public void testRunTwoCheckSatsIsAnError() throws IOException { + String input = "(declare-fun x () Int)\n(assert (> x 0))\n(check-sat)\n(check-sat)\n"; + Run r = run(SOLVER, SMTINTERPOL, smt2File(input)); + assertThat(r.out()).isEmpty(); + assertThat(r.err()).isNotEmpty(); + assertThat(r.exitCode()).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test + public void testRunCheckSatAssumingIsAnError() throws IOException { + // parseAll ignores (check-sat-assuming ...), the answer would be sat instead of unsat. + String input = "(declare-fun p () Bool)\n(assert p)\n(check-sat-assuming ((not p)))\n"; + Run r = run(SOLVER, SMTINTERPOL, smt2File(input)); + assertThat(r.out()).isEmpty(); + assertThat(r.err()).isNotEmpty(); + assertThat(r.exitCode()).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test + public void testRunMalformedCheckSatIsAnError() throws IOException { + String input = "(declare-fun x () Int)\n(assert (> x 0))\n(check-sat 1)\n"; + Run r = run(SOLVER, SMTINTERPOL, smt2File(input)); + assertThat(r.out()).isEmpty(); + assertThat(r.err()).isNotEmpty(); + assertThat(r.exitCode()).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test + public void testRunInvalidPathIsAnError() { + Run r = run(SOLVER, SMTINTERPOL, "bad\0name.smt2"); + assertThat(r.out()).isEmpty(); + assertThat(r.err()).isNotEmpty(); + assertThat(r.exitCode()).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test + public void testRunPopIsAnError() throws IOException { + String input = "(declare-fun x () Int)\n(assert (> x 0))\n(pop 1)\n(check-sat)\n"; + Run r = run(SOLVER, SMTINTERPOL, smt2File(input)); + assertThat(r.out()).isEmpty(); + assertThat(r.err()).isNotEmpty(); + assertThat(r.exitCode()).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test + public void testRunResetIsAnError() throws IOException { + String input = "(declare-fun x () Int)\n(assert (> x 0))\n(reset)\n(check-sat)\n"; + Run r = run(SOLVER, SMTINTERPOL, smt2File(input)); + assertThat(r.out()).isEmpty(); + assertThat(r.err()).isNotEmpty(); + assertThat(r.exitCode()).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test + public void testRunResetAssertionsIsAnError() throws IOException { + String input = "(declare-fun x () Int)\n(assert (> x 0))\n(reset-assertions)\n(check-sat)\n"; + Run r = run(SOLVER, SMTINTERPOL, smt2File(input)); + assertThat(r.out()).isEmpty(); + assertThat(r.err()).isNotEmpty(); + assertThat(r.exitCode()).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test + public void testRunExitBeforeLastCommandIsAnError() throws IOException { + String input = "(declare-fun x () Int)\n(assert (> x 0))\n(exit)\n(check-sat)\n"; + Run r = run(SOLVER, SMTINTERPOL, smt2File(input)); + assertThat(r.out()).isEmpty(); + assertThat(r.err()).isNotEmpty(); + assertThat(r.exitCode()).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test + public void testRunPushIsAnError() throws IOException { + String input = "(declare-fun x () Int)\n(push 1)\n(assert (> x 0))\n(check-sat)\n"; + Run r = run(SOLVER, SMTINTERPOL, smt2File(input)); + assertThat(r.out()).isEmpty(); + assertThat(r.err()).isNotEmpty(); + assertThat(r.exitCode()).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test + public void testRunLogicWithoutOpenSmtWarnsOnce() throws IOException { + String file = smt2File(SAT_INPUT); + Run r = run("--logic", "QF_LIA", SOLVER, SMTINTERPOL, file); + assertThat(r.out()).isEqualTo("sat" + NL); + assertThat(r.exitCode()).isEqualTo(0); + assertThat(r.err()).isNotEmpty(); // the warning + + // Running again must not duplicate the log output of the first run. + Run r2 = run("--logic", "QF_LIA", SOLVER, SMTINTERPOL, file); + assertThat(r2.err()).isEqualTo(r.err()); + } + + /** + * The pigeonhole principle for the given number of holes, an unsatisfiable propositional problem + * that takes resolution-based solvers exponential time. Used as input that does not terminate + * within the time of a test. + */ + private static String pigeonholeInput(int holes) { + int pigeons = holes + 1; + StringBuilder sb = new StringBuilder("(set-logic QF_UF)\n"); + for (int p = 0; p < pigeons; p++) { + for (int h = 0; h < holes; h++) { + sb.append("(declare-const p").append(p).append("h").append(h).append(" Bool)\n"); + } + } + for (int p = 0; p < pigeons; p++) { // every pigeon is in some hole + sb.append("(assert (or"); + for (int h = 0; h < holes; h++) { + sb.append(" p").append(p).append("h").append(h); + } + sb.append("))\n"); + } + for (int h = 0; h < holes; h++) { // no two pigeons share a hole + for (int p = 0; p < pigeons; p++) { + for (int q = p + 1; q < pigeons; q++) { + sb.append("(assert (not (and p").append(p).append("h").append(h); + sb.append(" p").append(q).append("h").append(h).append(")))\n"); + } + } + } + sb.append("(check-sat)\n"); + return sb.toString(); + } + + @Test + public void testRunShutdownRequestedBeforeSolvingIsUnknown() throws IOException { + ShutdownManager shutdown = ShutdownManager.create(); + shutdown.requestShutdown("requested by test"); + Run r = run(shutdown.getNotifier(), SOLVER, SMTINTERPOL, smt2File(UNSAT_INPUT)); + assertThat(r.out()).isEqualTo("unknown" + NL); + assertThat(r.err()).isNotEmpty(); + assertThat(r.exitCode()).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test(timeout = 60_000) + public void testRunShutdownRequestedWhileSolvingIsUnknown() throws Exception { + ShutdownManager shutdown = ShutdownManager.create(); + Thread requester = + new Thread( + () -> { + try { + Thread.sleep(500); + } catch (InterruptedException e) { + Thread.currentThread().interrupt(); + } + shutdown.requestShutdown("requested by test while solving"); + }); + requester.start(); + Run r = run(shutdown.getNotifier(), SOLVER, SMTINTERPOL, smt2File(pigeonholeInput(12))); + requester.join(); + assertThat(r.out()).isEqualTo("unknown" + NL); + assertThat(r.err()).isNotEmpty(); + assertThat(r.exitCode()).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test(timeout = 60_000) + public void testMainReportsUnknownWhenTerminated() throws Exception { + // Process.destroy() sends SIGTERM on Unix, which runs the shutdown hook of the JVM. + // On Windows the process is killed immediately without running any hook. + assume() + .withMessage("SIGTERM cannot be sent on Windows") + .that(System.getProperty("os.name").toLowerCase(Locale.ROOT).startsWith("win")) + .isFalse(); + + Path outFile = tempDir.newFile("stdout").toPath(); + Process process = + new ProcessBuilder( + ImmutableList.of( + Path.of(System.getProperty("java.home"), "bin", "java").toString(), + "-cp", + System.getProperty("java.class.path"), + JavaSMTMain.class.getName(), + SOLVER, + SMTINTERPOL, + smt2File(pigeonholeInput(12)))) + .redirectOutput(outFile.toFile()) + .redirectError(ProcessBuilder.Redirect.DISCARD) + .start(); + try { + Thread.sleep(3000); // let the JVM start and the solver run + process.destroy(); + assertThat(process.waitFor(30, TimeUnit.SECONDS)).isTrue(); + + assertThat(Files.readString(outFile)).isEqualTo("unknown" + NL); + // The JVM exits with 128 + signal number after running the shutdown hooks. + assertThat(process.exitValue()).isEqualTo(128 + 15); + } finally { + process.destroyForcibly(); + } + } + + @Test(timeout = 60_000) + public void testMainReportsFailureToWriteResult() throws Exception { + Path devFull = Path.of("/dev/full"); + assume().withMessage("/dev/full is not available").that(Files.exists(devFull)).isTrue(); + + Process process = + new ProcessBuilder( + ImmutableList.of( + Path.of(System.getProperty("java.home"), "bin", "java").toString(), + "-cp", + System.getProperty("java.class.path"), + JavaSMTMain.class.getName(), + SOLVER, + SMTINTERPOL, + smt2File(SAT_INPUT))) + .redirectOutput(devFull.toFile()) + .redirectError(ProcessBuilder.Redirect.DISCARD) + .start(); + try { + assertThat(process.waitFor(30, TimeUnit.SECONDS)).isTrue(); + assertThat(process.exitValue()).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } finally { + process.destroyForcibly(); + } + } + + // Tests for the argument parsing. + + @Test + public void testProcessArgumentsWithSolverAndFile() throws Exception { + Map result = + CmdLineArguments.processArguments(new String[] {SOLVER, "Z3", "test.smt2"}); + assertThat(result.get("solver.solver")).isEqualTo("Z3"); + assertThat(result.get("smt2.file")).isEqualTo("test.smt2"); + } + + @Test + public void testProcessArgumentsSolverShortFlag() throws Exception { + Map result = + CmdLineArguments.processArguments(new String[] {"-solver", "SMTINTERPOL", "file.smt2"}); + assertThat(result.get("solver.solver")).isEqualTo("SMTINTERPOL"); + } + + @Test + public void testProcessArgumentsHelp() throws Exception { + Map result = CmdLineArguments.processArguments(new String[] {"--help"}); + assertThat(result).containsKey("help"); + } + + @Test + public void testProcessArgumentsHelpShortFlag() throws Exception { + Map result = CmdLineArguments.processArguments(new String[] {"-h"}); + assertThat(result).containsKey("help"); + } + + @Test + public void testProcessArgumentsOnlyFile() throws Exception { + Map result = CmdLineArguments.processArguments(new String[] {"input.smt2"}); + assertThat(result.get("smt2.file")).isEqualTo("input.smt2"); + } + + @Test + public void testProcessArgumentsMultipleFiles() { + assertThrows( + InvalidCmdlineArgumentException.class, + () -> CmdLineArguments.processArguments(new String[] {"file1.smt2", "file2.smt2"})); + } + + @Test + public void testProcessArgumentsUnknownArgument() { + assertThrows( + InvalidCmdlineArgumentException.class, + () -> CmdLineArguments.processArguments(new String[] {"--unknown", "file.smt2"})); + } + + @Test + public void testProcessArgumentsSolverMissingValue() { + assertThrows( + InvalidCmdlineArgumentException.class, + () -> CmdLineArguments.processArguments(new String[] {SOLVER})); + } + + @Test + public void testProcessArgumentsFileBeforeSolver() throws Exception { + Map result = + CmdLineArguments.processArguments(new String[] {"test.smt2", SOLVER, "Z3"}); + assertThat(result.get("smt2.file")).isEqualTo("test.smt2"); + assertThat(result.get("solver.solver")).isEqualTo("Z3"); + } + + @Test + public void testProcessArgumentsWithoutSolverLeavesSolverUnset() throws Exception { + Map result = CmdLineArguments.processArguments(new String[] {"test.smt2"}); + assertThat(result.get("smt2.file")).isEqualTo("test.smt2"); + assertThat(result).doesNotContainKey("solver.solver"); + } + + @Test + public void testProcessArgumentsWithLogic() throws Exception { + Map result = + CmdLineArguments.processArguments(new String[] {"--logic", "QF_LIA", "test.smt2"}); + assertThat(result.get("solver.opensmt.logic")).isEqualTo("QF_LIA"); + assertThat(result.get("solver.z3.logic")).isEqualTo("QF_LIA"); + assertThat(result.get("smt2.file")).isEqualTo("test.smt2"); + } + + @Test + public void testProcessArgumentsWithLogicShortFlag() throws Exception { + Map result = + CmdLineArguments.processArguments(new String[] {"-logic", "QF_UF", "test.smt2"}); + assertThat(result.get("solver.opensmt.logic")).isEqualTo("QF_UF"); + assertThat(result.get("solver.z3.logic")).isEqualTo("QF_UF"); + } + + @Test + public void testProcessArgumentsWithSolverAndLogic() throws Exception { + Map result = + CmdLineArguments.processArguments( + new String[] {SOLVER, "OPENSMT", "--logic", "QF_LIA", "test.smt2"}); + assertThat(result.get("solver.solver")).isEqualTo("OPENSMT"); + assertThat(result.get("solver.opensmt.logic")).isEqualTo("QF_LIA"); + assertThat(result.get("solver.z3.logic")).isEqualTo("QF_LIA"); + assertThat(result.get("smt2.file")).isEqualTo("test.smt2"); + } + + @Test + public void testProcessArgumentsLogicMissingValue() { + assertThrows( + InvalidCmdlineArgumentException.class, + () -> CmdLineArguments.processArguments(new String[] {"--logic"})); + } + + @Test + public void testProcessArgumentsInvalidPath() { + assertThrows( + InvalidCmdlineArgumentException.class, + () -> CmdLineArguments.processArguments(new String[] {"bad\0name.smt2"})); + } +}