From 0d749c9f4fa8749e1284552c2de46c5b7272ed16 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Sat, 14 Mar 2026 04:02:48 +0000 Subject: [PATCH 01/23] Cmdline: Added `JavaSMTMain` class, main entry point for the cmdline interface. --- .../java_smt/cmdline/JavaSMTMain.java | 180 ++++++++++++++++++ 1 file changed, 180 insertions(+) create mode 100644 src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java 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..c5c58facd0 --- /dev/null +++ b/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java @@ -0,0 +1,180 @@ +/* + * 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.annotations.VisibleForTesting; +import com.google.common.collect.ImmutableMap; +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Paths; +import java.util.List; +import java.util.Locale; +import java.util.Map; +import java.util.logging.Level; +import org.checkerframework.checker.nullness.qual.Nullable; +import org.sosy_lab.common.ShutdownManager; +import org.sosy_lab.common.ShutdownNotifier; +import org.sosy_lab.common.annotations.SuppressForbidden; +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.configuration.Option; +import org.sosy_lab.common.configuration.Options; +import org.sosy_lab.common.log.BasicLogManager; +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.FormulaManager; +import org.sosy_lab.java_smt.api.ProverEnvironment; +import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.SolverException; + +/** + * Main entry point for JavaSMT command-line interface. Executes SMT2 files using a selected solver + * and reports the result (sat/unsat/unknown). + */ +@SuppressForbidden("System.out in this class is ok") +public class JavaSMTMain { + + static final int ERROR_EXIT_CODE = 1; + + /** + * Main method for running JavaSMT from command line. + * + * @param args Command-line arguments: [--solver SOLVER] [--logic LOGIC] file.smt2 + */ + @SuppressWarnings("resource") // We don't close LogManager + public static void main(String[] args) { + Locale.setDefault(Locale.US); + + if (args.length == 0) { + args = new String[] {"--help"}; + } + + final Configuration config; + final LogManager logManager; + final MainOptions options; + final Map cmdLineOptions; + try { + cmdLineOptions = CmdLineArguments.processArguments(args); + config = createConfiguration(cmdLineOptions); + logManager = BasicLogManager.create(config); + options = new MainOptions(config); + + String logic = cmdLineOptions.get("solver.opensmt.logic"); + String solver = cmdLineOptions.get("solver.solver"); + if (logic != null && (solver == null || !solver.equals("OPENSMT"))) { + logManager.log( + Level.WARNING, + "Option --logic is only effective with OpenSMT solver, but solver is set to " + + (solver != null ? solver : "default") + + ". The logic setting will be ignored."); + } + } catch (InvalidCmdlineArgumentException e) { + throw Output.fatalError("Could not process command line arguments: %s", e.getMessage()); + } catch (InvalidConfigurationException e) { + throw Output.fatalError("Invalid configuration: %s", e.getMessage()); + } + + if (options.smt2File == null) { + CmdLineArguments.printHelp(System.out); + System.exit(0); + return; + } + + if (!Files.isReadable(Paths.get(options.smt2File))) { + throw Output.fatalError( + "Please provide a valid, readable SMT2 file: %s", options.smt2File); + } + + run(config, logManager, options); + } + + private static final ImmutableMap EXTERN_OPTION_DEFAULTS = + ImmutableMap.of("log.level", Level.INFO.toString()); + + @VisibleForTesting + @Options + static final class MainOptions { + + private MainOptions(Configuration config) throws InvalidConfigurationException { + config.inject(this); + } + + @Option(secure = true, name = "smt2.file", description = "The SMT2 file to execute") + private @Nullable String smt2File = null; + + @Option(secure = true, name = "solver.solver", description = "The SMT solver to use") + private Solvers solver = Solvers.SMTINTERPOL; + } + + /** + * Creates a Configuration from command-line arguments. + * + * @param cmdLineOptions Processed command-line options map + * @return Configuration object for solver context + * @throws InvalidConfigurationException if configuration is invalid + */ + @VisibleForTesting + public static Configuration createConfiguration(Map cmdLineOptions) + throws InvalidConfigurationException { + + ConfigurationBuilder configBuilder = Configuration.builder(); + configBuilder.setOptions(EXTERN_OPTION_DEFAULTS); + configBuilder.setOptions(cmdLineOptions); + + Configuration config = configBuilder.build(); + + return config; + } + + private static void run(Configuration config, LogManager logManager, MainOptions options) { + + String input; + try { + input = Files.readString(Paths.get(options.smt2File)); + } catch (IOException e) { + throw Output.fatalError("Could not read SMT2 file: %s", e.getMessage()); + } + + ShutdownManager shutdownManager = ShutdownManager.create(); + ShutdownNotifier notifier = shutdownManager.getNotifier(); + + try (SolverContext context = + SolverContextFactory.createSolverContext(config, logManager, notifier, options.solver); + ProverEnvironment prover = context.newProverEnvironment()) { + + FormulaManager formulaManager = context.getFormulaManager(); + List formulas = formulaManager.parseAll(input); + for (BooleanFormula formula : formulas) { + prover.addConstraint(formula); + } + + boolean isUnsat = prover.isUnsat(); + System.out.println(isUnsat ? "unsat" : "sat"); + System.exit(0); + + } catch (InvalidConfigurationException e) { + throw Output.fatalError("Invalid configuration: %s", e.getMessage()); + } catch (InterruptedException e) { + logManager.log(Level.WARNING, "SMT execution was interrupted."); + System.out.println("unknown"); + System.exit(ERROR_EXIT_CODE); + } catch (SolverException e) { + logManager.logUserException(Level.SEVERE, e, "Error executing SMT2 solver"); + System.out.println("unknown"); + System.exit(ERROR_EXIT_CODE); + } + } + + private JavaSMTMain() {} +} From 6d2edd41a4205eb9e22788b38728a6190fd7349e Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Sat, 14 Mar 2026 04:10:13 +0000 Subject: [PATCH 02/23] Cmdline: Added `CmdLineArgument` class. --- .../java_smt/cmdline/CmdLineArgument.java | 138 ++++++++++++++++++ 1 file changed, 138 insertions(+) create mode 100644 src/org/sosy_lab/java_smt/cmdline/CmdLineArgument.java 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..c600ad21cd --- /dev/null +++ b/src/org/sosy_lab/java_smt/cmdline/CmdLineArgument.java @@ -0,0 +1,138 @@ +/* + * 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.ImmutableSet; +import com.google.errorprone.annotations.CanIgnoreReturnValue; +import java.util.HashMap; +import java.util.Iterator; +import java.util.Map; +import java.util.Map.Entry; + +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; + } + + String getMainName() { + return names.iterator().next(); + } + + @Override + public int compareTo(CmdLineArgument other) { + return names.toString().compareTo(other.names.toString()); + } + + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + return o instanceof CmdLineArgument && names.equals(((CmdLineArgument) o).names); + } + + @Override + public int hashCode() { + return names.hashCode(); + } + + @Override + public String toString() { + String s = + com.google.common.collect.FluentIterable.from(names) + .filter(arg -> !CmdLineArguments.isOldStyleArgument(arg)) + .join(Joiner.on("/")); + if (description.isEmpty()) { + return s; + } else { + return String.format("%1$-20s %2$s", s, description); + } + } + + boolean apply(Map properties, String currentArg, Iterator argsIt) + throws InvalidCmdlineArgumentException { + if (names.contains(currentArg)) { + apply0(properties, currentArg, argsIt); + return true; + } + return false; + } + + abstract void apply0(Map properties, String currentArg, Iterator argsIt) + throws InvalidCmdlineArgumentException; + + static class CmdLineArgument1 extends CmdLineArgument { + + private String option; + + CmdLineArgument1(String... pNames) { + super(pNames); + } + + CmdLineArgument1 settingOption(String pOption) { + option = pOption; + return this; + } + + @Override + final void apply0(Map properties, String currentArg, Iterator args) + throws InvalidCmdlineArgumentException { + if (args.hasNext()) { + handleArg(properties, currentArg, args.next()); + } else { + throw new InvalidCmdlineArgumentException(currentArg + " argument missing."); + } + } + + void handleArg(Map pProperties, String pCurrentArg, String pArgValue) + throws InvalidCmdlineArgumentException { + checkState(option != null); + putIfNotExistent(pProperties, option, pArgValue); + } + } + + static class PropertyAddingCmdLineArgument extends CmdLineArgument { + + private final Map additionalIfNotExistentArgs = new HashMap<>(); + + PropertyAddingCmdLineArgument(String... pNames) { + super(pNames); + } + + @CanIgnoreReturnValue + PropertyAddingCmdLineArgument settingProperty(String pName, String pValue) { + additionalIfNotExistentArgs.put(pName, pValue); + return this; + } + + @Override + void apply0(Map properties, String currentArg, Iterator args) + throws InvalidCmdlineArgumentException { + for (Entry e : additionalIfNotExistentArgs.entrySet()) { + putIfNotExistent(properties, e.getKey(), e.getValue()); + } + } + } +} From fcb24db4bcc01373a60d03795c7fa00847aa9774 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Sat, 14 Mar 2026 04:10:26 +0000 Subject: [PATCH 03/23] Cmdline: Added `CmdLineArguments` class. --- .../java_smt/cmdline/CmdLineArguments.java | 128 ++++++++++++++++++ 1 file changed, 128 insertions(+) create mode 100644 src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java 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..27f0be5f63 --- /dev/null +++ b/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java @@ -0,0 +1,128 @@ +/* + * 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.Preconditions; +import com.google.common.collect.ImmutableSortedSet; +import java.io.PrintStream; +import java.nio.file.Path; +import java.nio.file.Paths; +import java.util.Arrays; +import java.util.HashMap; +import java.util.Iterator; +import java.util.Map; +import org.sosy_lab.java_smt.cmdline.CmdLineArgument.CmdLineArgument1; +import org.sosy_lab.java_smt.cmdline.CmdLineArgument.PropertyAddingCmdLineArgument; + +/** Processes command-line arguments for JavaSMT. */ +public final class CmdLineArguments { + + private CmdLineArguments() {} + + private static final ImmutableSortedSet CMD_LINE_ARGS = + ImmutableSortedSet.of( + new CmdLineArgument1("--solver", "-solver") + .settingOption("solver.solver") + .withDescription("Set SMT solver to use"), + new CmdLineArgument1("--logic", "-logic") + .settingOption("solver.opensmt.logic") + .withDescription("Set SMT logic (only for OpenSMT)"), + new PropertyAddingCmdLineArgument("--help", "-h", "-help") + .settingProperty("help", "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 = Arrays.asList(pArgs).iterator(); + + 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("smt2.file")) { + throw new InvalidCmdlineArgumentException( + "Multiple input files are not supported: " + + properties.get("smt2.file") + + " and " + + arg); + } + Path file = Paths.get(arg); + properties.put("smt2.file", file.toString()); + } + } + } + + return properties; + } + + static boolean isOldStyleArgument(String arg) { + return arg.length() > 2 && arg.startsWith("-") && !arg.startsWith("--"); + } + + private static void printVersion(PrintStream out) { + out.println(); + Package pkg = CmdLineArguments.class.getPackage(); + String version = pkg != null ? pkg.getImplementationVersion() : "unknown"; + out.println("JavaSMT " + version); + } + + /** + * Prints the help message to the given output stream. + * + * @param out The output stream to print to + */ + public static void printHelp(PrintStream out) { + printVersion(out); + out.println(); + out.println("Usage: javasmt [options] "); + out.println("Options:"); + for (CmdLineArgument cmdLineArg : CMD_LINE_ARGS) { + if (!isOldStyleArgument(cmdLineArg.getMainName())) { + out.println(" " + cmdLineArg); + } + } + out.println(); + out.println("JavaSMT executes SMT2 files using the selected solver."); + out.println("javasmt --solver "); + } + + static void putIfNotExistent(Map properties, String key, String value) + throws InvalidCmdlineArgumentException { + if (properties.containsKey(key) && !properties.get(key).equals(value)) { + throw new InvalidCmdlineArgumentException( + String.format( + "Option %s specified twice on command-line with values '%s' and '%s'.", + key, properties.get(key), value)); + } + properties.put(key, value); + } +} From b2f8b2897547fd092cfd844453aedf9a1766095a Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Sat, 14 Mar 2026 04:10:59 +0000 Subject: [PATCH 04/23] Cmdline: Added `InvalidCmdlineArgumentException` class. --- .../InvalidCmdlineArgumentException.java | 25 +++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 src/org/sosy_lab/java_smt/cmdline/InvalidCmdlineArgumentException.java 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..eb4db2f7b3 --- /dev/null +++ b/src/org/sosy_lab/java_smt/cmdline/InvalidCmdlineArgumentException.java @@ -0,0 +1,25 @@ +/* + * 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; + +/** Exception thrown when an invalid command-line argument is provided. */ +public class InvalidCmdlineArgumentException extends Exception { + + private static final long serialVersionUID = -6526968677815416436L; + + public InvalidCmdlineArgumentException(final String msg) { + super(msg); + } + + public InvalidCmdlineArgumentException(final String msg, final Throwable cause) { + super(msg, cause); + } +} From 6af7ff83de608e2c8bd9db56fdc9ede6a4b3c3ce Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Sat, 14 Mar 2026 04:11:17 +0000 Subject: [PATCH 05/23] Cmdline: Added `Output` class. --- src/org/sosy_lab/java_smt/cmdline/Output.java | 60 +++++++++++++++++++ 1 file changed, 60 insertions(+) create mode 100644 src/org/sosy_lab/java_smt/cmdline/Output.java 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..2a4d945de7 --- /dev/null +++ b/src/org/sosy_lab/java_smt/cmdline/Output.java @@ -0,0 +1,60 @@ +/* + * 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.PrintStream; +import org.checkerframework.dataflow.qual.TerminatesExecution; +import org.sosy_lab.common.annotations.SuppressForbidden; +import org.sosy_lab.common.io.IO; + +/** + * Utility class for formatted output and error handling in JavaSMT command-line interface. + * + *

Provides methods for printing error messages with optional color support. + */ +@SuppressForbidden("System.out in this class is ok") +final class Output { + + private Output() {} + + private static final PrintStream ERROR_OUTPUT = System.err; + + 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"; + + @TerminatesExecution + @FormatMethod + static RuntimeException fatalError(String msg, Object... args) { + coloredOutput(ERROR_COLOR, msg, args); + System.exit(JavaSMTMain.ERROR_EXIT_CODE); + return new RuntimeException("never reached"); + } + + @FormatMethod + private static void coloredOutput(String color, @FormatString String msg, Object... args) { + ERROR_OUTPUT.println(); + + if (USE_COLORS) { + ERROR_OUTPUT.print(color); + } + + ERROR_OUTPUT.printf(msg, args); + + if (USE_COLORS) { + ERROR_OUTPUT.print(REGULAR_COLOR); + } + + ERROR_OUTPUT.println(); + } +} From df6dd0c745e1479fb528b09588d01cb8062ed1da Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Sat, 14 Mar 2026 04:11:44 +0000 Subject: [PATCH 06/23] Cmdline: Added `JavaSMTMainTest` test class. --- .../java_smt/test/JavaSMTMainTest.java | 114 ++++++++++++++++++ 1 file changed, 114 insertions(+) create mode 100644 src/org/sosy_lab/java_smt/test/JavaSMTMainTest.java 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..cd0e096919 --- /dev/null +++ b/src/org/sosy_lab/java_smt/test/JavaSMTMainTest.java @@ -0,0 +1,114 @@ +/* + * 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 java.util.Map; +import org.junit.Test; +import org.sosy_lab.java_smt.cmdline.CmdLineArguments; +import org.sosy_lab.java_smt.cmdline.InvalidCmdlineArgumentException; + +public class JavaSMTMainTest { + + @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(expected = InvalidCmdlineArgumentException.class) + public void testProcessArgumentsMultipleFiles() throws Exception { + CmdLineArguments.processArguments(new String[] {"file1.smt2", "file2.smt2"}); + } + + @Test(expected = InvalidCmdlineArgumentException.class) + public void testProcessArgumentsUnknownArgument() throws Exception { + CmdLineArguments.processArguments(new String[] {"--unknown", "file.smt2"}); + } + + @Test(expected = InvalidCmdlineArgumentException.class) + public void testProcessArgumentsSolverMissingValue() throws Exception { + 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 testProcessArgumentsDefaultSolver() throws Exception { + Map result = CmdLineArguments.processArguments(new String[] {"test.smt2"}); + assertThat(result.get("smt2.file")).isEqualTo("test.smt2"); + assertThat(result.get("solver.solver")).isNull(); + } + + @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("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"); + } + + @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("smt2.file")).isEqualTo("test.smt2"); + } + + @Test(expected = InvalidCmdlineArgumentException.class) + public void testProcessArgumentsLogicMissingValue() throws Exception { + CmdLineArguments.processArguments(new String[] {"--logic"}); + } +} From 685ecfd4e74b29863440794fdec754e285399c60 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Sat, 14 Mar 2026 04:12:13 +0000 Subject: [PATCH 07/23] Cmdline: Added package info to `cmdline`. --- .../sosy_lab/java_smt/cmdline/package-info.java | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 src/org/sosy_lab/java_smt/cmdline/package-info.java 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..ceaea29cff --- /dev/null +++ b/src/org/sosy_lab/java_smt/cmdline/package-info.java @@ -0,0 +1,14 @@ +/* + * 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. + */ +package org.sosy_lab.java_smt.cmdline; \ No newline at end of file From 9f678f09b5d7e5128e611a52d7d97065fc968be5 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Thu, 19 Mar 2026 02:10:06 +0000 Subject: [PATCH 08/23] refaster. --- src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java | 3 +-- src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java | 6 +++--- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java b/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java index 27f0be5f63..f2de975f3c 100644 --- a/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java +++ b/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java @@ -14,7 +14,6 @@ import com.google.common.collect.ImmutableSortedSet; import java.io.PrintStream; import java.nio.file.Path; -import java.nio.file.Paths; import java.util.Arrays; import java.util.HashMap; import java.util.Iterator; @@ -75,7 +74,7 @@ public static Map processArguments(String[] pArgs) + " and " + arg); } - Path file = Paths.get(arg); + Path file = Path.of(arg); properties.put("smt2.file", file.toString()); } } diff --git a/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java b/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java index c5c58facd0..07c572b84a 100644 --- a/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java +++ b/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java @@ -14,7 +14,7 @@ import com.google.common.collect.ImmutableMap; import java.io.IOException; import java.nio.file.Files; -import java.nio.file.Paths; +import java.nio.file.Path; import java.util.List; import java.util.Locale; import java.util.Map; @@ -91,7 +91,7 @@ public static void main(String[] args) { return; } - if (!Files.isReadable(Paths.get(options.smt2File))) { + if (!Files.isReadable(Path.of(options.smt2File))) { throw Output.fatalError( "Please provide a valid, readable SMT2 file: %s", options.smt2File); } @@ -141,7 +141,7 @@ private static void run(Configuration config, LogManager logManager, MainOptions String input; try { - input = Files.readString(Paths.get(options.smt2File)); + input = Files.readString(Path.of(options.smt2File)); } catch (IOException e) { throw Output.fatalError("Could not read SMT2 file: %s", e.getMessage()); } From b4a89b673200e3838e831d8bd83ca8d562b507b9 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Thu, 19 Mar 2026 02:19:17 +0000 Subject: [PATCH 09/23] checkstyle. --- src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java b/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java index 07c572b84a..7da1403e74 100644 --- a/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java +++ b/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java @@ -43,7 +43,7 @@ * and reports the result (sat/unsat/unknown). */ @SuppressForbidden("System.out in this class is ok") -public class JavaSMTMain { +public final class JavaSMTMain { static final int ERROR_EXIT_CODE = 1; From aba6237471da5728fa474ec6aece9d64beda9509 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Thu, 19 Mar 2026 02:21:42 +0000 Subject: [PATCH 10/23] Cmdline: removed unused argument in a helper function from `CmdLineArgument`. --- src/org/sosy_lab/java_smt/cmdline/CmdLineArgument.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/cmdline/CmdLineArgument.java b/src/org/sosy_lab/java_smt/cmdline/CmdLineArgument.java index c600ad21cd..a1858145a0 100644 --- a/src/org/sosy_lab/java_smt/cmdline/CmdLineArgument.java +++ b/src/org/sosy_lab/java_smt/cmdline/CmdLineArgument.java @@ -100,13 +100,13 @@ CmdLineArgument1 settingOption(String pOption) { final void apply0(Map properties, String currentArg, Iterator args) throws InvalidCmdlineArgumentException { if (args.hasNext()) { - handleArg(properties, currentArg, args.next()); + handleArg(properties, args.next()); } else { throw new InvalidCmdlineArgumentException(currentArg + " argument missing."); } } - void handleArg(Map pProperties, String pCurrentArg, String pArgValue) + void handleArg(Map pProperties, String pArgValue) throws InvalidCmdlineArgumentException { checkState(option != null); putIfNotExistent(pProperties, option, pArgValue); From e90044b57dc7ed8b4704dc70da63e06cb6f2bc5b Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Thu, 19 Mar 2026 02:26:51 +0000 Subject: [PATCH 11/23] format. --- src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java | 3 +-- src/org/sosy_lab/java_smt/cmdline/package-info.java | 6 ++---- 2 files changed, 3 insertions(+), 6 deletions(-) diff --git a/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java b/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java index 7da1403e74..d2496bcccd 100644 --- a/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java +++ b/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java @@ -92,8 +92,7 @@ public static void main(String[] args) { } if (!Files.isReadable(Path.of(options.smt2File))) { - throw Output.fatalError( - "Please provide a valid, readable SMT2 file: %s", options.smt2File); + throw Output.fatalError("Please provide a valid, readable SMT2 file: %s", options.smt2File); } run(config, logManager, options); diff --git a/src/org/sosy_lab/java_smt/cmdline/package-info.java b/src/org/sosy_lab/java_smt/cmdline/package-info.java index ceaea29cff..6a970cc13f 100644 --- a/src/org/sosy_lab/java_smt/cmdline/package-info.java +++ b/src/org/sosy_lab/java_smt/cmdline/package-info.java @@ -8,7 +8,5 @@ * SPDX-License-Identifier: Apache-2.0 */ -/** - * The frontend of JavaSMT for using it as a standalone application on the command line. - */ -package org.sosy_lab.java_smt.cmdline; \ No newline at end of file +/** The frontend of JavaSMT for using it as a standalone application on the command line. */ +package org.sosy_lab.java_smt.cmdline; From 7e5485a796c630cca8bc6ca7d13db5ebf28c5512 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Tue, 31 Mar 2026 19:22:21 +0000 Subject: [PATCH 12/23] Cmdline: removed preconditions check that the (set-logic) command should be at the start of the smt2 file to be parsed set by private helper method `sanitize` in `AbstractFormulaManager`. --- .../sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java index 1bb109f98f..f95c261801 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java @@ -401,7 +401,9 @@ private String sanitize(String formulaStr) { for (String token : tokens) { if (Tokenizer.isSetLogicToken(token)) { // Skip the (set-logic ...) command at the beginning of the input - Preconditions.checkArgument(pos == 0); + // The command at the top is not (set-logic) but (set-info) for some non-incremental + // benchmarks from the SMT-LIB release 2025 + // Preconditions.checkArgument(pos == 0); } else if (Tokenizer.isExitToken(token)) { // Skip the (exit) command at the end of the input From f2f3aa1e1f97c3cfd3823f3a1064b5386f86e6ac Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Wed, 16 Sep 2026 15:50:39 +0000 Subject: [PATCH 13/23] Cmdline: fixed bug when the solver used is Princess. Fixed compile error --- .../java_smt/cmdline/CmdLineArgument.java | 2 +- .../sosy_lab/java_smt/cmdline/JavaSMTMain.java | 18 +++++++++++------- 2 files changed, 12 insertions(+), 8 deletions(-) diff --git a/src/org/sosy_lab/java_smt/cmdline/CmdLineArgument.java b/src/org/sosy_lab/java_smt/cmdline/CmdLineArgument.java index a1858145a0..5a6eb151b3 100644 --- a/src/org/sosy_lab/java_smt/cmdline/CmdLineArgument.java +++ b/src/org/sosy_lab/java_smt/cmdline/CmdLineArgument.java @@ -50,7 +50,7 @@ public boolean equals(Object o) { if (this == o) { return true; } - return o instanceof CmdLineArgument && names.equals(((CmdLineArgument) o).names); + return o instanceof CmdLineArgument other && names.equals(other.names); } @Override diff --git a/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java b/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java index d2496bcccd..b6be16cf19 100644 --- a/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java +++ b/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java @@ -72,7 +72,7 @@ public static void main(String[] args) { String logic = cmdLineOptions.get("solver.opensmt.logic"); String solver = cmdLineOptions.get("solver.solver"); - if (logic != null && (solver == null || !solver.equals("OPENSMT"))) { + if (logic != null && (solver == null || !solver.equalsIgnoreCase("OPENSMT"))) { logManager.log( Level.WARNING, "Option --logic is only effective with OpenSMT solver, but solver is set to " @@ -149,16 +149,20 @@ private static void run(Configuration config, LogManager logManager, MainOptions ShutdownNotifier notifier = shutdownManager.getNotifier(); try (SolverContext context = - SolverContextFactory.createSolverContext(config, logManager, notifier, options.solver); - ProverEnvironment prover = context.newProverEnvironment()) { + SolverContextFactory.createSolverContext(config, logManager, notifier, options.solver)) { + // Parse before creating the prover: Princess does not know symbols that are declared after + // the prover environment was created. FormulaManager formulaManager = context.getFormulaManager(); List formulas = formulaManager.parseAll(input); - for (BooleanFormula formula : formulas) { - prover.addConstraint(formula); - } - boolean isUnsat = prover.isUnsat(); + boolean isUnsat; + try (ProverEnvironment prover = context.newProverEnvironment()) { + for (BooleanFormula formula : formulas) { + prover.addConstraint(formula); + } + isUnsat = prover.isUnsat(); + } System.out.println(isUnsat ? "unsat" : "sat"); System.exit(0); From 99f4e766cea649d48f2792b61a8bf1f6c2fe7e66 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Wed, 16 Sep 2026 17:44:08 +0000 Subject: [PATCH 14/23] Cmdline: print "unknown" instead of "null" as version in `--help` when running from bin/. --- src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java b/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java index f2de975f3c..3714ec1b27 100644 --- a/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java +++ b/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java @@ -89,9 +89,10 @@ static boolean isOldStyleArgument(String arg) { private static void printVersion(PrintStream out) { out.println(); + // The version is only available from the manifest of the JAR, not when running from bin/. Package pkg = CmdLineArguments.class.getPackage(); - String version = pkg != null ? pkg.getImplementationVersion() : "unknown"; - out.println("JavaSMT " + version); + String version = pkg != null ? pkg.getImplementationVersion() : null; + out.println("JavaSMT " + (version != null ? version : "unknown")); } /** From 9c536e07e77caf6f51ef281c3cd31a61df0a8aaf Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Wed, 16 Sep 2026 17:47:32 +0000 Subject: [PATCH 15/23] Cmdline: added launcher script `javasmt` for the command-line interface --- javasmt | 126 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 126 insertions(+) create mode 100755 javasmt diff --git a/javasmt b/javasmt new file mode 100755 index 0000000000..633c6654bc --- /dev/null +++ b/javasmt @@ -0,0 +1,126 @@ +#!/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" + echo "$java_version" + echo "Please make sure you are able to execute Java processes by running \"$JAVA\"." + 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 compiled classes below bin/ or as a JAR. The JARs with the +# sources and the documentation carry no +# classes to run, so they are skipped. +JAVASMT_JAR="" +for jar in "$PATH_TO_JAVASMT"/java-smt-*.jar; do + case "$jar" in + *-sources.jar | *-javadoc.jar) continue ;; + esac + [ -e "$jar" ] && JAVASMT_JAR="$jar" +done + +if [ ! -e "$PATH_TO_JAVASMT/bin/org/sosy_lab/java_smt/cmdline/JavaSMTMain.class" ] \ + && [ -z "$JAVASMT_JAR" ] ; then + echo "Could not find JavaSMT binary, please check path to project directory" 1>&2 + exit 1 +fi + +# the classpath contains the compiled classes, the JAR if there is one, +# the core JARs, and every solver present +CLASSPATH="$PATH_TO_JAVASMT/bin" +[ -n "$JAVASMT_JAR" ] && CLASSPATH="$CLASSPATH$SEP$JAVASMT_JAR" +CLASSPATH="$CLASSPATH$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[@]}" From 69bfdcb811473d011f00fb07c152f19aeac372af Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Thu, 17 Sep 2026 17:57:01 +0000 Subject: [PATCH 16/23] Cmdline: refactored `JavaSMTMain` for testing and fixed `--help`, logging, input checks, error reporting, and shutdown. Added `ShutdownHook` --- .../java_smt/cmdline/CmdLineArguments.java | 19 +- .../java_smt/cmdline/JavaSMTMain.java | 259 ++++++++++++------ src/org/sosy_lab/java_smt/cmdline/Output.java | 33 +-- .../java_smt/cmdline/ShutdownHook.java | 70 +++++ 4 files changed, 269 insertions(+), 112 deletions(-) create mode 100644 src/org/sosy_lab/java_smt/cmdline/ShutdownHook.java diff --git a/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java b/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java index 3714ec1b27..43f66bb129 100644 --- a/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java +++ b/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java @@ -26,16 +26,23 @@ public final class CmdLineArguments { private CmdLineArguments() {} + /** Keys in the map returned by {@link #processArguments(String[])}. */ + static final String SOLVER_OPTION = "solver.solver"; + + static final String LOGIC_OPTION = "solver.opensmt.logic"; + static final String FILE_OPTION = "smt2.file"; + static final String HELP_OPTION = "help"; + private static final ImmutableSortedSet CMD_LINE_ARGS = ImmutableSortedSet.of( new CmdLineArgument1("--solver", "-solver") - .settingOption("solver.solver") + .settingOption(SOLVER_OPTION) .withDescription("Set SMT solver to use"), new CmdLineArgument1("--logic", "-logic") - .settingOption("solver.opensmt.logic") + .settingOption(LOGIC_OPTION) .withDescription("Set SMT logic (only for OpenSMT)"), new PropertyAddingCmdLineArgument("--help", "-h", "-help") - .settingProperty("help", "true") + .settingProperty(HELP_OPTION, "true") .withDescription("Print this help message")); /** @@ -67,15 +74,15 @@ public static Map processArguments(String[] pArgs) if (arg.startsWith("-")) { throw new InvalidCmdlineArgumentException("Unknown command-line argument: " + arg); } else { - if (properties.containsKey("smt2.file")) { + if (properties.containsKey(FILE_OPTION)) { throw new InvalidCmdlineArgumentException( "Multiple input files are not supported: " - + properties.get("smt2.file") + + properties.get(FILE_OPTION) + " and " + arg); } Path file = Path.of(arg); - properties.put("smt2.file", file.toString()); + properties.put(FILE_OPTION, file.toString()); } } } diff --git a/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java b/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java index b6be16cf19..c78007a982 100644 --- a/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java +++ b/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java @@ -10,151 +10,183 @@ package org.sosy_lab.java_smt.cmdline; -import com.google.common.annotations.VisibleForTesting; -import com.google.common.collect.ImmutableMap; import java.io.IOException; +import java.io.PrintStream; import java.nio.file.Files; import java.nio.file.Path; import java.util.List; import java.util.Locale; import java.util.Map; import java.util.logging.Level; +import java.util.logging.LogRecord; +import java.util.logging.StreamHandler; +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.annotations.SuppressForbidden; 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.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.FormulaManager; 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, 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. */ -@SuppressForbidden("System.out in this class is ok") public final class JavaSMTMain { - static final int ERROR_EXIT_CODE = 1; + /** Exit code for unknown results and for all errors. */ + public static final int ERROR_EXIT_CODE = 1; /** * Main method for running JavaSMT from command line. * * @param args Command-line arguments: [--solver SOLVER] [--logic LOGIC] file.smt2 */ - @SuppressWarnings("resource") // We don't close LogManager 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()); + + // 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 args Command-line arguments: [--solver SOLVER] [--logic LOGIC] file.smt2 + * @param out stream for the result, i.e., sat, unsat, unknown, or the help message + * @param err stream for diagnostics and logging + * @param shutdownNotifier 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[] args, PrintStream out, PrintStream err, ShutdownNotifier shutdownNotifier) { if (args.length == 0) { + // be nice to user args = new String[] {"--help"}; } - final Configuration config; - final LogManager logManager; - final MainOptions options; final Map cmdLineOptions; try { cmdLineOptions = CmdLineArguments.processArguments(args); - config = createConfiguration(cmdLineOptions); - logManager = BasicLogManager.create(config); - options = new MainOptions(config); - - String logic = cmdLineOptions.get("solver.opensmt.logic"); - String solver = cmdLineOptions.get("solver.solver"); - if (logic != null && (solver == null || !solver.equalsIgnoreCase("OPENSMT"))) { - logManager.log( - Level.WARNING, - "Option --logic is only effective with OpenSMT solver, but solver is set to " - + (solver != null ? solver : "default") - + ". The logic setting will be ignored."); - } } catch (InvalidCmdlineArgumentException e) { - throw Output.fatalError("Could not process command line arguments: %s", e.getMessage()); - } catch (InvalidConfigurationException e) { - throw Output.fatalError("Invalid configuration: %s", e.getMessage()); + Output.error(err, "Could not process command line arguments: %s", e.getMessage()); + return ERROR_EXIT_CODE; } - if (options.smt2File == null) { - CmdLineArguments.printHelp(System.out); - System.exit(0); - return; + if (cmdLineOptions.remove(CmdLineArguments.HELP_OPTION) != null) { + CmdLineArguments.printHelp(out); + return 0; } - if (!Files.isReadable(Path.of(options.smt2File))) { - throw Output.fatalError("Please provide a valid, readable SMT2 file: %s", options.smt2File); + final Configuration config; + final MainOptions options; + try { + config = Configuration.builder().setOptions(cmdLineOptions).build(); + options = new MainOptions(config); + } catch (InvalidConfigurationException e) { + Output.error(err, "Invalid configuration: %s", e.getMessage()); + return ERROR_EXIT_CODE; } - run(config, logManager, options); - } - - private static final ImmutableMap EXTERN_OPTION_DEFAULTS = - ImmutableMap.of("log.level", Level.INFO.toString()); - - @VisibleForTesting - @Options - static final class MainOptions { - - private MainOptions(Configuration config) throws InvalidConfigurationException { - config.inject(this); + if (options.smt2File == null) { + Output.error(err, "No SMT2 file given, see --help for usage."); + return ERROR_EXIT_CODE; } - @Option(secure = true, name = "smt2.file", description = "The SMT2 file to execute") - private @Nullable String smt2File = null; - - @Option(secure = true, name = "solver.solver", description = "The SMT solver to use") - private Solvers solver = Solvers.SMTINTERPOL; - } - - /** - * Creates a Configuration from command-line arguments. - * - * @param cmdLineOptions Processed command-line options map - * @return Configuration object for solver context - * @throws InvalidConfigurationException if configuration is invalid - */ - @VisibleForTesting - public static Configuration createConfiguration(Map cmdLineOptions) - throws InvalidConfigurationException { - - ConfigurationBuilder configBuilder = Configuration.builder(); - configBuilder.setOptions(EXTERN_OPTION_DEFAULTS); - configBuilder.setOptions(cmdLineOptions); + LogManager logManager = createLogManager(err); - Configuration config = configBuilder.build(); - - return config; - } - - private static void run(Configuration config, LogManager logManager, MainOptions options) { + if (cmdLineOptions.containsKey(CmdLineArguments.LOGIC_OPTION) + && options.solver != Solvers.OPENSMT) { + logManager.log( + Level.WARNING, + "Option --logic is only effective with OpenSMT solver, but solver is set to", + options.solver + ". The logic setting will be ignored."); + } - String input; + final String input; try { input = Files.readString(Path.of(options.smt2File)); } catch (IOException e) { - throw Output.fatalError("Could not read SMT2 file: %s", e.getMessage()); + Output.error(err, "Could not read SMT2 file: %s", e.getMessage()); + return ERROR_EXIT_CODE; } - ShutdownManager shutdownManager = ShutdownManager.create(); - ShutdownNotifier notifier = shutdownManager.getNotifier(); + // 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. + final boolean hasCheckSat; + try { + hasCheckSat = containsCheckSat(input); + } catch (IllegalArgumentException e) { + // The tokenizer rejects syntactically broken input, e.g., unbalanced parentheses. + Output.error(err, "Could not parse SMT2 file: %s", describe(e)); + return ERROR_EXIT_CODE; + } + if (!hasCheckSat) { + Output.error(err, "SMT2 file contains no (check-sat) command: %s", options.smt2File); + return ERROR_EXIT_CODE; + } + + return solve(config, logManager, shutdownNotifier, options.solver, input, out, err); + } + + private static int solve( + Configuration config, + LogManager logManager, + ShutdownNotifier shutdownNotifier, + Solvers solver, + String input, + PrintStream out, + PrintStream err) { try (SolverContext context = - SolverContextFactory.createSolverContext(config, logManager, notifier, options.solver)) { + SolverContextFactory.createSolverContext(config, logManager, shutdownNotifier, solver)) { // Parse before creating the prover: Princess does not know symbols that are declared after // the prover environment was created. - FormulaManager formulaManager = context.getFormulaManager(); - List formulas = formulaManager.parseAll(input); + final List formulas; + try { + formulas = context.getFormulaManager().parseAll(input); + } catch (IllegalArgumentException e) { + // All parsers report input they cannot handle like this: syntax errors, undeclared + // symbols, type errors, unsupported sorts or commands. + Output.error(err, "Could not parse SMT2 file with %s: %s", solver, describe(e)); + return ERROR_EXIT_CODE; + } catch (UnsupportedOperationException e) { + // Solvers without a parser for SMT-LIB2, e.g., Yices2. + Output.error(err, "Solver %s does not support parsing SMT-LIB2 input.%s", solver, + e.getMessage() == null ? "" : " " + e.getMessage()); + 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. boolean isUnsat; try (ProverEnvironment prover = context.newProverEnvironment()) { @@ -163,20 +195,73 @@ private static void run(Configuration config, LogManager logManager, MainOptions } isUnsat = prover.isUnsat(); } - System.out.println(isUnsat ? "unsat" : "sat"); - System.exit(0); + out.println(isUnsat ? "unsat" : "sat"); + return 0; } catch (InvalidConfigurationException e) { - throw Output.fatalError("Invalid configuration: %s", e.getMessage()); + Output.error(err, "Invalid configuration: %s", describe(e)); + return ERROR_EXIT_CODE; } catch (InterruptedException e) { - logManager.log(Level.WARNING, "SMT execution was interrupted."); - System.out.println("unknown"); - System.exit(ERROR_EXIT_CODE); + // Thrown by the solver after a shutdown request, see ShutdownHook. + String reason = shutdownNotifier.shouldShutdown() ? shutdownNotifier.getReason() : ""; + logManager.log(Level.WARNING, "SMT execution was interrupted.", reason); + out.println("unknown"); + return ERROR_EXIT_CODE; } catch (SolverException e) { logManager.logUserException(Level.SEVERE, e, "Error executing SMT2 solver"); - System.out.println("unknown"); - System.exit(ERROR_EXIT_CODE); + out.println("unknown"); + return ERROR_EXIT_CODE; + } + } + + /** The message of an exception, or its class if it has no message. */ + private static String describe(Throwable e) { + return e.getMessage() != null ? e.getMessage() : e.getClass().getSimpleName(); + } + + /** Matches the commands (check-sat) and (check-sat-assuming ..). */ + private static final Pattern CHECK_SAT_COMMAND = Pattern.compile("\\(\\s*check-sat[\\S\\s]*"); + + private static boolean containsCheckSat(String input) { + for (String token : SMTLibTokenizer.of(input)) { + if (CHECK_SAT_COMMAND.matcher(token).matches()) { + return true; + } + } + return false; + } + + /** Creates a logger that writes messages of level INFO and above to the given stream. */ + private static LogManager createLogManager(PrintStream err) { + StreamHandler handler = + new StreamHandler(err, ConsoleLogFormatter.withColorsIfPossible()) { + @Override + public synchronized void publish(LogRecord record) { + super.publish(record); + flush(); // like ConsoleHandler, do not buffer messages + } + + @Override + public synchronized void close() { + flush(); // do not close the stream, it may be System.err + } + }; + handler.setLevel(Level.INFO); + return BasicLogManager.createWithHandler(handler); + } + + @Options + private static final class MainOptions { + + private MainOptions(Configuration config) throws InvalidConfigurationException { + config.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 = Solvers.SMTINTERPOL; } private JavaSMTMain() {} diff --git a/src/org/sosy_lab/java_smt/cmdline/Output.java b/src/org/sosy_lab/java_smt/cmdline/Output.java index 2a4d945de7..42ef5cd512 100644 --- a/src/org/sosy_lab/java_smt/cmdline/Output.java +++ b/src/org/sosy_lab/java_smt/cmdline/Output.java @@ -13,8 +13,6 @@ import com.google.errorprone.annotations.FormatMethod; import com.google.errorprone.annotations.FormatString; import java.io.PrintStream; -import org.checkerframework.dataflow.qual.TerminatesExecution; -import org.sosy_lab.common.annotations.SuppressForbidden; import org.sosy_lab.common.io.IO; /** @@ -22,39 +20,36 @@ * *

Provides methods for printing error messages with optional color support. */ -@SuppressForbidden("System.out in this class is ok") final class Output { private Output() {} - private static final PrintStream ERROR_OUTPUT = System.err; - 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"; - @TerminatesExecution - @FormatMethod - static RuntimeException fatalError(String msg, Object... args) { - coloredOutput(ERROR_COLOR, msg, args); - System.exit(JavaSMTMain.ERROR_EXIT_CODE); - return new RuntimeException("never reached"); - } - + /** + * Prints an error message to the given stream. This method does not terminate the program, the + * caller is responsible for returning the appropriate exit code. + * + * @param err the stream for error messages, usually {@link System#err} + * @param msg the message as format string for {@link PrintStream#printf} + * @param args the arguments for the format string + */ @FormatMethod - private static void coloredOutput(String color, @FormatString String msg, Object... args) { - ERROR_OUTPUT.println(); + static void error(PrintStream err, @FormatString String msg, Object... args) { + err.println(); if (USE_COLORS) { - ERROR_OUTPUT.print(color); + err.print(ERROR_COLOR); } - ERROR_OUTPUT.printf(msg, args); + err.printf(msg, args); if (USE_COLORS) { - ERROR_OUTPUT.print(REGULAR_COLOR); + err.print(REGULAR_COLOR); } - ERROR_OUTPUT.println(); + err.println(); } } 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..71adcaa06b --- /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 + } + } + } +} From 28f1acb866381cf362195c7ae13ffad8d4441b50 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Thu, 17 Sep 2026 18:00:57 +0000 Subject: [PATCH 17/23] Cmdline: added multiple tests --- .../java_smt/test/JavaSMTMainTest.java | 326 ++++++++++++++++++ 1 file changed, 326 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/JavaSMTMainTest.java b/src/org/sosy_lab/java_smt/test/JavaSMTMainTest.java index cd0e096919..f60ae70b43 100644 --- a/src/org/sosy_lab/java_smt/test/JavaSMTMainTest.java +++ b/src/org/sosy_lab/java_smt/test/JavaSMTMainTest.java @@ -11,14 +11,340 @@ package org.sosy_lab.java_smt.test; import static com.google.common.truth.Truth.assertThat; +import static com.google.common.truth.TruthJUnit.assume; +import java.io.ByteArrayOutputStream; +import java.io.IOException; +import java.io.PrintStream; +import java.nio.charset.StandardCharsets; +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.List; +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) + """; + + @Rule public TemporaryFolder tempDir = new TemporaryFolder(); + + /** The result of one invocation of the command-line interface. */ + private static final class Run { + final int exitCode; + final String out; + final String err; + + Run(int pExitCode, String pOut, String pErr) { + exitCode = pExitCode; + out = pOut; + err = pErr; + } + } + + /** 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) { + ByteArrayOutputStream outBytes = new ByteArrayOutputStream(); + ByteArrayOutputStream errBytes = new ByteArrayOutputStream(); + int exitCode; + try (PrintStream out = new PrintStream(outBytes, true, StandardCharsets.UTF_8); + PrintStream err = new PrintStream(errBytes, true, StandardCharsets.UTF_8)) { + exitCode = JavaSMTMain.run(args, out, err, shutdownNotifier); + } + return new Run( + exitCode, + outBytes.toString(StandardCharsets.UTF_8), + errBytes.toString(StandardCharsets.UTF_8)); + } + + 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\n"); + assertThat(r.exitCode).isEqualTo(0); + } + + @Test + public void testRunUnsatWithSeveralAssertions() throws IOException { + Run r = run("--solver", "PRINCESS", smt2File(UNSAT_INPUT)); + assertThat(r.out).isEqualTo("unsat\n"); + assertThat(r.exitCode).isEqualTo(0); + } + + @Test + public void testRunDefaultSolverIsSmtInterpol() throws IOException { + Run r = run(smt2File(UNSAT_INPUT)); + assertThat(r.out).isEqualTo("unsat\n"); + 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\n"); + assertThat(r.exitCode).isEqualTo(0); + } + + @Test + public void testRunHelpTakesPrecedenceOverFile() throws IOException { + Run r = run("--help", "--solver", "SMTINTERPOL", smt2File(SAT_INPUT)); + assertThat(r.out).contains("Usage: javasmt"); + assertThat(r.out).doesNotContain("sat\n"); + assertThat(r.exitCode).isEqualTo(0); + } + + @Test + public void testRunWithoutArgumentsPrintsHelp() { + Run r = run(); + assertThat(r.out).contains("Usage: javasmt"); + assertThat(r.exitCode).isEqualTo(0); + } + + @Test + public void testRunWithoutFileIsAnError() { + Run r = run("--solver", "SMTINTERPOL"); + assertThat(r.out).isEmpty(); + assertThat(r.err).contains("No SMT2 file given"); + 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).contains("Unknown command-line argument: --unknown"); + 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).contains("Invalid configuration"); + 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).contains("Could not read SMT2 file"); + 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).contains("no (check-sat) command"); + assertThat(r.exitCode).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test + public void testRunUnparsableFileIsAnError() throws IOException { + Run r = run("--solver", "SMTINTERPOL", smt2File("this is not an SMT2 file\n")); + assertThat(r.out).isEmpty(); + assertThat(r.err).contains("no (check-sat) command"); + 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\n"); + 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).contains("Could not parse SMT2 file"); + assertThat(r.err).doesNotContain("Exception in thread"); + 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).contains("Could not parse SMT2 file with SMTINTERPOL"); + assertThat(r.err).doesNotContain("Exception in thread"); + 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).contains("Could not parse SMT2 file with PRINCESS"); + assertThat(r.exitCode).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test + public void testRunUnsupportedCommandIsAnError() 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).contains("Could not parse SMT2 file"); + assertThat(r.err).contains("(push ...)"); + assertThat(r.exitCode).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + + @Test + public void testRunLogicWithoutOpenSmtWarnsOnce() throws IOException { + Run r = run("--logic", "QF_LIA", "--solver", "SMTINTERPOL", smt2File(SAT_INPUT)); + assertThat(r.out).isEqualTo("sat\n"); + assertThat(r.exitCode).isEqualTo(0); + assertThat(r.err).contains("Option --logic is only effective with OpenSMT"); + assertThat(r.err.indexOf("--logic")).isEqualTo(r.err.lastIndexOf("--logic")); + + // Running again must not duplicate the log output of the first run. + Run r2 = run("--logic", "QF_LIA", "--solver", "SMTINTERPOL", smt2File(SAT_INPUT)); + assertThat(r2.err.indexOf("--logic")).isEqualTo(r2.err.lastIndexOf("--logic")); + } + + /** + * 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\n"); + assertThat(r.err).contains("requested by test"); + 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\n"); + assertThat(r.err).contains("requested by test while solving"); + 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( + List.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(); + 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\n"); + assertThat(process.exitValue()).isNotEqualTo(0); + } + + // Tests for the argument parsing. + @Test public void testProcessArgumentsWithSolverAndFile() throws Exception { Map result = From a2499fe5e7df2f2636115d359b756eeea995b6cd Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Thu, 17 Sep 2026 21:42:29 +0000 Subject: [PATCH 18/23] Cmdline: write output via `Appendable` instead of `PrintStream`, fixed formatting. --- .../java_smt/cmdline/CmdLineArguments.java | 25 ++++---- .../java_smt/cmdline/JavaSMTMain.java | 64 ++++++++++++------- src/org/sosy_lab/java_smt/cmdline/Output.java | 43 ++++++------- .../java_smt/cmdline/ShutdownHook.java | 8 +-- .../java_smt/test/JavaSMTMainTest.java | 46 ++++++------- 5 files changed, 99 insertions(+), 87 deletions(-) diff --git a/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java b/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java index 43f66bb129..687d2e3ce9 100644 --- a/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java +++ b/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java @@ -12,7 +12,6 @@ import com.google.common.base.Preconditions; import com.google.common.collect.ImmutableSortedSet; -import java.io.PrintStream; import java.nio.file.Path; import java.util.Arrays; import java.util.HashMap; @@ -94,32 +93,32 @@ static boolean isOldStyleArgument(String arg) { return arg.length() > 2 && arg.startsWith("-") && !arg.startsWith("--"); } - private static void printVersion(PrintStream out) { - out.println(); + private static void printVersion(Appendable out) { + Output.println(out, ""); // The version is only available from the manifest of the JAR, not when running from bin/. Package pkg = CmdLineArguments.class.getPackage(); String version = pkg != null ? pkg.getImplementationVersion() : null; - out.println("JavaSMT " + (version != null ? version : "unknown")); + Output.println(out, "JavaSMT " + (version != null ? version : "unknown")); } /** * Prints the help message to the given output stream. * - * @param out The output stream to print to + * @param out The output to print to */ - public static void printHelp(PrintStream out) { + public static void printHelp(Appendable out) { printVersion(out); - out.println(); - out.println("Usage: javasmt [options] "); - out.println("Options:"); + Output.println(out, ""); + Output.println(out, "Usage: javasmt [options] "); + Output.println(out, "Options:"); for (CmdLineArgument cmdLineArg : CMD_LINE_ARGS) { if (!isOldStyleArgument(cmdLineArg.getMainName())) { - out.println(" " + cmdLineArg); + Output.println(out, " " + cmdLineArg); } } - out.println(); - out.println("JavaSMT executes SMT2 files using the selected solver."); - out.println("javasmt --solver "); + Output.println(out, ""); + Output.println(out, "JavaSMT executes SMT2 files using the selected solver."); + Output.println(out, "javasmt --solver "); } static void putIfNotExistent(Map properties, String key, String value) diff --git a/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java b/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java index c78007a982..22a16daa2d 100644 --- a/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java +++ b/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java @@ -11,15 +11,15 @@ package org.sosy_lab.java_smt.cmdline; import java.io.IOException; -import java.io.PrintStream; +import java.io.UncheckedIOException; import java.nio.file.Files; import java.nio.file.Path; import java.util.List; import java.util.Locale; import java.util.Map; +import java.util.logging.Handler; import java.util.logging.Level; import java.util.logging.LogRecord; -import java.util.logging.StreamHandler; import java.util.regex.Pattern; import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.ShutdownManager; @@ -68,6 +68,8 @@ public static void main(String[] args) { Runtime.getRuntime().addShutdownHook(shutdownHook); int exitCode = run(args, System.out, System.err, shutdownManager.getNotifier()); + System.out.flush(); + System.err.flush(); // The result is reported, the hook must not delay the exit anymore. shutdownHook.disableAndStop(); @@ -80,13 +82,13 @@ public static void main(String[] args) { * terminating the JVM, such that it can be used from tests. * * @param args Command-line arguments: [--solver SOLVER] [--logic LOGIC] file.smt2 - * @param out stream for the result, i.e., sat, unsat, unknown, or the help message - * @param err stream for diagnostics and logging + * @param out output for the result, i.e., sat, unsat, unknown, or the help message + * @param err output for diagnostics and logging * @param shutdownNotifier 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[] args, PrintStream out, PrintStream err, ShutdownNotifier shutdownNotifier) { + String[] args, Appendable out, Appendable err, ShutdownNotifier shutdownNotifier) { if (args.length == 0) { // be nice to user args = new String[] {"--help"}; @@ -163,8 +165,8 @@ private static int solve( ShutdownNotifier shutdownNotifier, Solvers solver, String input, - PrintStream out, - PrintStream err) { + Appendable out, + Appendable err) { try (SolverContext context = SolverContextFactory.createSolverContext(config, logManager, shutdownNotifier, solver)) { @@ -181,7 +183,10 @@ private static int solve( return ERROR_EXIT_CODE; } catch (UnsupportedOperationException e) { // Solvers without a parser for SMT-LIB2, e.g., Yices2. - Output.error(err, "Solver %s does not support parsing SMT-LIB2 input.%s", solver, + Output.error( + err, + "Solver %s does not support parsing SMT-LIB2 input.%s", + solver, e.getMessage() == null ? "" : " " + e.getMessage()); return ERROR_EXIT_CODE; } @@ -195,7 +200,7 @@ private static int solve( } isUnsat = prover.isUnsat(); } - out.println(isUnsat ? "unsat" : "sat"); + Output.println(out, isUnsat ? "unsat" : "sat"); return 0; } catch (InvalidConfigurationException e) { @@ -205,11 +210,11 @@ private static int solve( // Thrown by the solver after a shutdown request, see ShutdownHook. String reason = shutdownNotifier.shouldShutdown() ? shutdownNotifier.getReason() : ""; logManager.log(Level.WARNING, "SMT execution was interrupted.", reason); - out.println("unknown"); + Output.println(out, "unknown"); return ERROR_EXIT_CODE; } catch (SolverException e) { logManager.logUserException(Level.SEVERE, e, "Error executing SMT2 solver"); - out.println("unknown"); + Output.println(out, "unknown"); return ERROR_EXIT_CODE; } } @@ -231,21 +236,28 @@ private static boolean containsCheckSat(String input) { return false; } - /** Creates a logger that writes messages of level INFO and above to the given stream. */ - private static LogManager createLogManager(PrintStream err) { - StreamHandler handler = - new StreamHandler(err, ConsoleLogFormatter.withColorsIfPossible()) { + /** Creates a logger that writes messages of level INFO and above to the given output. */ + private static LogManager createLogManager(Appendable err) { + Handler handler = + new Handler() { @Override - public synchronized void publish(LogRecord record) { - super.publish(record); - flush(); // like ConsoleHandler, do not buffer messages + public void publish(LogRecord record) { + if (isLoggable(record)) { + try { + err.append(getFormatter().format(record)); + } catch (IOException e) { + throw new UncheckedIOException(e); + } + } } @Override - public synchronized void close() { - flush(); // do not close the stream, it may be System.err - } + public void flush() {} + + @Override + public void close() {} }; + handler.setFormatter(ConsoleLogFormatter.withColorsIfPossible()); handler.setLevel(Level.INFO); return BasicLogManager.createWithHandler(handler); } @@ -257,10 +269,16 @@ private MainOptions(Configuration config) throws InvalidConfigurationException { config.inject(this); } - @Option(secure = true, name = CmdLineArguments.FILE_OPTION, description = "The SMT2 file to execute") + @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") + @Option( + secure = true, + name = CmdLineArguments.SOLVER_OPTION, + description = "The SMT solver to use") private Solvers solver = Solvers.SMTINTERPOL; } diff --git a/src/org/sosy_lab/java_smt/cmdline/Output.java b/src/org/sosy_lab/java_smt/cmdline/Output.java index 42ef5cd512..fc83f7b2f3 100644 --- a/src/org/sosy_lab/java_smt/cmdline/Output.java +++ b/src/org/sosy_lab/java_smt/cmdline/Output.java @@ -12,13 +12,13 @@ import com.google.errorprone.annotations.FormatMethod; import com.google.errorprone.annotations.FormatString; -import java.io.PrintStream; +import java.io.IOException; +import java.io.UncheckedIOException; import org.sosy_lab.common.io.IO; /** - * Utility class for formatted output and error handling in JavaSMT command-line interface. - * - *

Provides methods for printing error messages with optional color support. + * 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 { @@ -28,28 +28,27 @@ private Output() {} 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 out, String line) { + try { + out.append(line).append(System.lineSeparator()); + } catch (IOException e) { + throw new UncheckedIOException(e); + } + } + /** - * Prints an error message to the given stream. This method does not terminate the program, the - * caller is responsible for returning the appropriate exit code. + * 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 err the stream for error messages, usually {@link System#err} - * @param msg the message as format string for {@link PrintStream#printf} + * @param err the output for error messages, usually {@link System#err} + * @param msg the message as format string for {@link String#format} * @param args the arguments for the format string */ @FormatMethod - static void error(PrintStream err, @FormatString String msg, Object... args) { - err.println(); - - if (USE_COLORS) { - err.print(ERROR_COLOR); - } - - err.printf(msg, args); - - if (USE_COLORS) { - err.print(REGULAR_COLOR); - } - - err.println(); + static void error(Appendable err, @FormatString String msg, Object... args) { + String message = String.format(msg, args); + println(err, ""); + println(err, USE_COLORS ? ERROR_COLOR + message + REGULAR_COLOR : message); } } diff --git a/src/org/sosy_lab/java_smt/cmdline/ShutdownHook.java b/src/org/sosy_lab/java_smt/cmdline/ShutdownHook.java index 71adcaa06b..97c4536e64 100644 --- a/src/org/sosy_lab/java_smt/cmdline/ShutdownHook.java +++ b/src/org/sosy_lab/java_smt/cmdline/ShutdownHook.java @@ -15,10 +15,10 @@ 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. + * 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 { diff --git a/src/org/sosy_lab/java_smt/test/JavaSMTMainTest.java b/src/org/sosy_lab/java_smt/test/JavaSMTMainTest.java index f60ae70b43..77dd67e19a 100644 --- a/src/org/sosy_lab/java_smt/test/JavaSMTMainTest.java +++ b/src/org/sosy_lab/java_smt/test/JavaSMTMainTest.java @@ -13,10 +13,7 @@ import static com.google.common.truth.Truth.assertThat; import static com.google.common.truth.TruthJUnit.assume; -import java.io.ByteArrayOutputStream; import java.io.IOException; -import java.io.PrintStream; -import java.nio.charset.StandardCharsets; import java.nio.file.Files; import java.nio.file.Path; import java.util.List; @@ -53,6 +50,8 @@ public class JavaSMTMainTest { (check-sat) """; + private static final String NL = System.lineSeparator(); + @Rule public TemporaryFolder tempDir = new TemporaryFolder(); /** The result of one invocation of the command-line interface. */ @@ -74,17 +73,10 @@ private static Run run(String... args) { } private static Run run(ShutdownNotifier shutdownNotifier, String... args) { - ByteArrayOutputStream outBytes = new ByteArrayOutputStream(); - ByteArrayOutputStream errBytes = new ByteArrayOutputStream(); - int exitCode; - try (PrintStream out = new PrintStream(outBytes, true, StandardCharsets.UTF_8); - PrintStream err = new PrintStream(errBytes, true, StandardCharsets.UTF_8)) { - exitCode = JavaSMTMain.run(args, out, err, shutdownNotifier); - } - return new Run( - exitCode, - outBytes.toString(StandardCharsets.UTF_8), - errBytes.toString(StandardCharsets.UTF_8)); + 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 { @@ -100,21 +92,21 @@ private String smt2File(String content) throws IOException { @Test public void testRunSat() throws IOException { Run r = run("--solver", "SMTINTERPOL", smt2File(SAT_INPUT)); - assertThat(r.out).isEqualTo("sat\n"); + 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\n"); + 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\n"); + assertThat(r.out).isEqualTo("unsat" + NL); assertThat(r.exitCode).isEqualTo(0); assertThat(r.err).isEmpty(); } @@ -122,7 +114,7 @@ public void testRunDefaultSolverIsSmtInterpol() throws IOException { @Test public void testRunSolverNameIsCaseInsensitive() throws IOException { Run r = run("--solver", "smtinterpol", smt2File(SAT_INPUT)); - assertThat(r.out).isEqualTo("sat\n"); + assertThat(r.out).isEqualTo("sat" + NL); assertThat(r.exitCode).isEqualTo(0); } @@ -130,7 +122,7 @@ public void testRunSolverNameIsCaseInsensitive() throws IOException { public void testRunHelpTakesPrecedenceOverFile() throws IOException { Run r = run("--help", "--solver", "SMTINTERPOL", smt2File(SAT_INPUT)); assertThat(r.out).contains("Usage: javasmt"); - assertThat(r.out).doesNotContain("sat\n"); + assertThat(r.out).doesNotContain("sat" + NL); assertThat(r.exitCode).isEqualTo(0); } @@ -167,7 +159,11 @@ public void testRunUnknownSolverIsAnError() throws IOException { @Test public void testRunMissingFileIsAnError() { - Run r = run("--solver", "SMTINTERPOL", tempDir.getRoot().toPath().resolve("missing.smt2").toString()); + Run r = + run( + "--solver", + "SMTINTERPOL", + tempDir.getRoot().toPath().resolve("missing.smt2").toString()); assertThat(r.out).isEmpty(); assertThat(r.err).contains("Could not read SMT2 file"); assertThat(r.exitCode).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); @@ -192,7 +188,7 @@ public void testRunUnparsableFileIsAnError() throws IOException { @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\n"); + assertThat(r.out).isEqualTo("sat" + NL); assertThat(r.exitCode).isEqualTo(0); } @@ -239,7 +235,7 @@ public void testRunUnsupportedCommandIsAnError() throws IOException { @Test public void testRunLogicWithoutOpenSmtWarnsOnce() throws IOException { Run r = run("--logic", "QF_LIA", "--solver", "SMTINTERPOL", smt2File(SAT_INPUT)); - assertThat(r.out).isEqualTo("sat\n"); + assertThat(r.out).isEqualTo("sat" + NL); assertThat(r.exitCode).isEqualTo(0); assertThat(r.err).contains("Option --logic is only effective with OpenSMT"); assertThat(r.err.indexOf("--logic")).isEqualTo(r.err.lastIndexOf("--logic")); @@ -286,7 +282,7 @@ 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\n"); + assertThat(r.out).isEqualTo("unknown" + NL); assertThat(r.err).contains("requested by test"); assertThat(r.exitCode).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); } @@ -307,7 +303,7 @@ public void testRunShutdownRequestedWhileSolvingIsUnknown() throws Exception { requester.start(); Run r = run(shutdown.getNotifier(), "--solver", "SMTINTERPOL", smt2File(pigeonholeInput(12))); requester.join(); - assertThat(r.out).isEqualTo("unknown\n"); + assertThat(r.out).isEqualTo("unknown" + NL); assertThat(r.err).contains("requested by test while solving"); assertThat(r.exitCode).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); } @@ -339,7 +335,7 @@ public void testMainReportsUnknownWhenTerminated() throws Exception { process.destroy(); assertThat(process.waitFor(30, TimeUnit.SECONDS)).isTrue(); - assertThat(Files.readString(outFile)).isEqualTo("unknown\n"); + assertThat(Files.readString(outFile)).isEqualTo("unknown" + NL); assertThat(process.exitValue()).isNotEqualTo(0); } From 08c8073c8fdff341902b8325fc7832cf6513a380 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Mon, 21 Sep 2026 11:18:30 +0000 Subject: [PATCH 19/23] Cmdline: added handling of unsupported cases of commands in the smt2 files. `JavaSMTMainTest` now tests for this. --- .../java_smt/cmdline/JavaSMTMain.java | 54 +++++++++++++++---- .../java_smt/test/JavaSMTMainTest.java | 36 +++++++++++++ 2 files changed, 79 insertions(+), 11 deletions(-) diff --git a/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java b/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java index 22a16daa2d..a2ef3ae106 100644 --- a/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java +++ b/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java @@ -17,6 +17,7 @@ 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; @@ -140,19 +141,16 @@ public static int run( return ERROR_EXIT_CODE; } - // 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. - final boolean hasCheckSat; + final Optional scriptError; try { - hasCheckSat = containsCheckSat(input); + scriptError = checkScript(input); } catch (IllegalArgumentException e) { // The tokenizer rejects syntactically broken input, e.g., unbalanced parentheses. Output.error(err, "Could not parse SMT2 file: %s", describe(e)); return ERROR_EXIT_CODE; } - if (!hasCheckSat) { - Output.error(err, "SMT2 file contains no (check-sat) command: %s", options.smt2File); + if (scriptError.isPresent()) { + Output.error(err, "%s: %s", scriptError.orElseThrow(), options.smt2File); return ERROR_EXIT_CODE; } @@ -227,13 +225,47 @@ private static String describe(Throwable e) { /** Matches the commands (check-sat) and (check-sat-assuming ..). */ private static final Pattern CHECK_SAT_COMMAND = Pattern.compile("\\(\\s*check-sat[\\S\\s]*"); - private static boolean containsCheckSat(String input) { + /** + * 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 input) { + // 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. To be supported once parseAll + // handles the assertion stack and resets. + boolean hasCheckSat = false; + boolean afterExit = false; for (String token : SMTLibTokenizer.of(input)) { - if (CHECK_SAT_COMMAND.matcher(token).matches()) { - return true; + if (afterExit) { + return Optional.of("Command (exit) is only allowed as the last command in the SMT2 file"); + } + if (SMTLibTokenizer.isPopToken(token) + || SMTLibTokenizer.isResetToken(token) + || SMTLibTokenizer.isResetAssertionsToken(token)) { + return Optional.of( + "Command " + + token + + " is not supported, the assertion stack is not tracked when parsing SMT2 files"); + } else if (SMTLibTokenizer.isExitToken(token)) { + afterExit = true; + } else if (CHECK_SAT_COMMAND.matcher(token).matches()) { + hasCheckSat = true; } } - return false; + if (!hasCheckSat) { + return Optional.of("SMT2 file contains no (check-sat) command"); + } + return Optional.empty(); } /** Creates a logger that writes messages of level INFO and above to the given output. */ diff --git a/src/org/sosy_lab/java_smt/test/JavaSMTMainTest.java b/src/org/sosy_lab/java_smt/test/JavaSMTMainTest.java index 77dd67e19a..051080bb78 100644 --- a/src/org/sosy_lab/java_smt/test/JavaSMTMainTest.java +++ b/src/org/sosy_lab/java_smt/test/JavaSMTMainTest.java @@ -222,6 +222,42 @@ public void testRunTypeErrorIsAnError() throws IOException { 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).contains("Command (pop 1) is not supported"); + 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).contains("Command (reset) is not supported"); + 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).contains("Command (reset-assertions) is not supported"); + 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).contains("Command (exit) is only allowed as the last command"); + assertThat(r.exitCode).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + } + @Test public void testRunUnsupportedCommandIsAnError() throws IOException { String input = "(declare-fun x () Int)\n(push 1)\n(assert (> x 0))\n(check-sat)\n"; From d9307460e9b55e9469b852533846b4726372c3bc Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Mon, 21 Sep 2026 22:31:45 +0000 Subject: [PATCH 20/23] Cmdline: added `SolverResul` enum with the results of a satisfiability check. --- .../java_smt/cmdline/SolverResult.java | 30 +++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 src/org/sosy_lab/java_smt/cmdline/SolverResult.java 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; + } +} From d2c5eef71e26ed6fea6f126bb1e19fc4c4a79666 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Mon, 21 Sep 2026 23:46:45 +0000 Subject: [PATCH 21/23] Cmdline: - converted repeated Strings into final constants. - changes to style to better adhere to the CPAchecker's StyleGuide. - avoided shorthand if-then-else. - expanded `--help` argument. - only one `(check-sat)` is supported per smt2 file. Assertions after it are rejected. Text outside any command is rejected. `push`, `pop`, `reset` are rejected. - redirect the launchers JVM-probe failure messages to stderr. - exit code 1 if the result could not be written to stdout. - an `InvalidPathException` in `CmdLineArguments` and `JavaSMTMain` was previously not handled. - added some tests and a cleanup of `testMainReportsUnknownWhenTerminated()`. Using `assertThrows` instead of `expected`. - added static analysis hints to the package-info. --- javasmt | 52 +-- .../java_smt/cmdline/CmdLineArgument.java | 64 +-- .../java_smt/cmdline/CmdLineArguments.java | 107 +++-- .../InvalidCmdlineArgumentException.java | 12 +- .../java_smt/cmdline/JavaSMTMain.java | 204 ++++++---- src/org/sosy_lab/java_smt/cmdline/Output.java | 23 +- .../java_smt/cmdline/package-info.java | 4 + .../java_smt/test/JavaSMTMainTest.java | 364 +++++++++++------- 8 files changed, 532 insertions(+), 298 deletions(-) diff --git a/javasmt b/javasmt index 633c6654bc..6e934b1b91 100755 --- a/javasmt +++ b/javasmt @@ -30,9 +30,9 @@ if [ $result -eq 127 ]; then exit 1 fi if [ $result -ne 0 ]; then - echo "Failed to execute Java VM, return code was $result and output was" - echo "$java_version" - echo "Please make sure you are able to execute Java processes by running \"$JAVA\"." + 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-`" @@ -63,28 +63,34 @@ case "$platform" in ;; esac -# JavaSMT can be present either as compiled classes below bin/ or as a JAR. The JARs with the -# sources and the documentation carry no -# classes to run, so they are skipped. -JAVASMT_JAR="" -for jar in "$PATH_TO_JAVASMT"/java-smt-*.jar; do - case "$jar" in - *-sources.jar | *-javadoc.jar) continue ;; - esac - [ -e "$jar" ] && JAVASMT_JAR="$jar" -done - -if [ ! -e "$PATH_TO_JAVASMT/bin/org/sosy_lab/java_smt/cmdline/JavaSMTMain.class" ] \ - && [ -z "$JAVASMT_JAR" ] ; then - echo "Could not find JavaSMT binary, please check path to project directory" 1>&2 - exit 1 +# JavaSMT can be present either as compiled classes below bin/, which take precedence, or as +# the JAR that "ant jar" produces. 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. +if [ -e "$PATH_TO_JAVASMT/bin/org/sosy_lab/java_smt/cmdline/JavaSMTMain.class" ]; then + JAVASMT_CLASSES="$PATH_TO_JAVASMT/bin" +else + 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 + echo "Could not find JavaSMT binary, please check path to project directory" 1>&2 + exit 1 + fi fi -# the classpath contains the compiled classes, the JAR if there is one, -# the core JARs, and every solver present -CLASSPATH="$PATH_TO_JAVASMT/bin" -[ -n "$JAVASMT_JAR" ] && CLASSPATH="$CLASSPATH$SEP$JAVASMT_JAR" -CLASSPATH="$CLASSPATH$SEP$PATH_TO_JAVASMT/lib/java/core/*" +# 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 diff --git a/src/org/sosy_lab/java_smt/cmdline/CmdLineArgument.java b/src/org/sosy_lab/java_smt/cmdline/CmdLineArgument.java index 5a6eb151b3..4ae134aa34 100644 --- a/src/org/sosy_lab/java_smt/cmdline/CmdLineArgument.java +++ b/src/org/sosy_lab/java_smt/cmdline/CmdLineArgument.java @@ -14,13 +14,20 @@ 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.HashMap; 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; @@ -36,33 +43,35 @@ CmdLineArgument withDescription(String pDescription) { return this; } + /** The first name given in the constructor. */ String getMainName() { return names.iterator().next(); } @Override - public int compareTo(CmdLineArgument other) { - return names.toString().compareTo(other.names.toString()); + 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(Object o) { - if (this == o) { + public boolean equals(@Nullable Object pOther) { + if (this == pOther) { return true; } - return o instanceof CmdLineArgument other && names.equals(other.names); + return pOther instanceof CmdLineArgument other && names.asList().equals(other.names.asList()); } @Override public int hashCode() { - return names.hashCode(); + return names.asList().hashCode(); } @Override public String toString() { String s = - com.google.common.collect.FluentIterable.from(names) - .filter(arg -> !CmdLineArguments.isOldStyleArgument(arg)) + FluentIterable.from(names) + .filter(pName -> !CmdLineArguments.isOldStyleArgument(pName)) .join(Joiner.on("/")); if (description.isEmpty()) { return s; @@ -71,51 +80,62 @@ public String toString() { } } - boolean apply(Map properties, String currentArg, Iterator argsIt) + /** + * 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(currentArg)) { - apply0(properties, currentArg, argsIt); + if (names.contains(pCurrentArg)) { + apply0(pProperties, pCurrentArg, pArgsIt); return true; } return false; } - abstract void apply0(Map properties, String currentArg, Iterator argsIt) + 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 String option; + 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 properties, String currentArg, Iterator args) + final void apply0(Map pProperties, String pCurrentArg, Iterator pArgsIt) throws InvalidCmdlineArgumentException { - if (args.hasNext()) { - handleArg(properties, args.next()); + if (pArgsIt.hasNext()) { + handleArg(pProperties, pArgsIt.next()); } else { - throw new InvalidCmdlineArgumentException(currentArg + " argument missing."); + throw new InvalidCmdlineArgumentException(pCurrentArg + " argument missing."); } } void handleArg(Map pProperties, String pArgValue) throws InvalidCmdlineArgumentException { - checkState(option != null); + 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 { - private final Map additionalIfNotExistentArgs = new HashMap<>(); + // Insertion order determines which conflict is reported first. + private final Map additionalIfNotExistentArgs = new LinkedHashMap<>(); PropertyAddingCmdLineArgument(String... pNames) { super(pNames); @@ -128,10 +148,10 @@ PropertyAddingCmdLineArgument settingProperty(String pName, String pValue) { } @Override - void apply0(Map properties, String currentArg, Iterator args) + void apply0(Map pProperties, String pCurrentArg, Iterator pArgsIt) throws InvalidCmdlineArgumentException { for (Entry e : additionalIfNotExistentArgs.entrySet()) { - putIfNotExistent(properties, e.getKey(), e.getValue()); + 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 index 687d2e3ce9..15bb1fec10 100644 --- a/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java +++ b/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java @@ -10,37 +10,48 @@ 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.Arrays; 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 {@link #processArguments(String[])}. */ + // Keys in the map returned by processArguments() static final String SOLVER_OPTION = "solver.solver"; - static final String LOGIC_OPTION = "solver.opensmt.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); + private static final ImmutableSortedSet CMD_LINE_ARGS = ImmutableSortedSet.of( new CmdLineArgument1("--solver", "-solver") .settingOption(SOLVER_OPTION) - .withDescription("Set SMT solver to use"), + .withDescription("Set the SMT solver, default: " + JavaSMTMain.DEFAULT_SOLVER), new CmdLineArgument1("--logic", "-logic") .settingOption(LOGIC_OPTION) - .withDescription("Set SMT logic (only for OpenSMT)"), - new PropertyAddingCmdLineArgument("--help", "-h", "-help") + .withDescription("Set the logic of OpenSMT, ignored for other solvers"), + new PropertyAddingCmdLineArgument(HELP_ARGUMENT, "-h", "-help") .settingProperty(HELP_OPTION, "true") .withDescription("Print this help message")); @@ -56,7 +67,7 @@ public static Map processArguments(String[] pArgs) Preconditions.checkNotNull(pArgs); Map properties = new HashMap<>(); - Iterator argsIt = Arrays.asList(pArgs).iterator(); + Iterator argsIt = Iterators.forArray(pArgs); while (argsIt.hasNext()) { String arg = argsIt.next(); @@ -80,7 +91,12 @@ public static Map processArguments(String[] pArgs) + " and " + arg); } - Path file = Path.of(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()); } } @@ -89,46 +105,79 @@ public static Map processArguments(String[] pArgs) return properties; } - static boolean isOldStyleArgument(String arg) { - return arg.length() > 2 && arg.startsWith("-") && !arg.startsWith("--"); + /** 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 out) { - Output.println(out, ""); + 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(); - String version = pkg != null ? pkg.getImplementationVersion() : null; - Output.println(out, "JavaSMT " + (version != null ? version : "unknown")); + if (pkg != null && pkg.getImplementationVersion() != null) { + version = pkg.getImplementationVersion(); + } else { + version = "unknown"; + } + Output.println(pOut, "JavaSMT " + version); } /** - * Prints the help message to the given output stream. + * Prints the help message, including the allowed arguments and the restrictions on the input, to + * the given output. * - * @param out The output to print to + * @param pOut The output to print to */ - public static void printHelp(Appendable out) { - printVersion(out); - Output.println(out, ""); - Output.println(out, "Usage: javasmt [options] "); - Output.println(out, "Options:"); + 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(out, " " + cmdLineArg); + Output.println(pOut, " " + cmdLineArg); } } - Output.println(out, ""); - Output.println(out, "JavaSMT executes SMT2 files using the selected solver."); - Output.println(out, "javasmt --solver "); + 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, "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."); } - static void putIfNotExistent(Map properties, String key, String value) + static void putIfNotExistent(Map pProperties, String pKey, String pValue) throws InvalidCmdlineArgumentException { - if (properties.containsKey(key) && !properties.get(key).equals(value)) { + 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'.", - key, properties.get(key), value)); + pKey, pProperties.get(pKey), pValue)); } - properties.put(key, value); + 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 index eb4db2f7b3..98e51d6ee9 100644 --- a/src/org/sosy_lab/java_smt/cmdline/InvalidCmdlineArgumentException.java +++ b/src/org/sosy_lab/java_smt/cmdline/InvalidCmdlineArgumentException.java @@ -10,16 +10,18 @@ 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 { - private static final long serialVersionUID = -6526968677815416436L; + @Serial private static final long serialVersionUID = -6526968677815416436L; - public InvalidCmdlineArgumentException(final String msg) { - super(msg); + public InvalidCmdlineArgumentException(String pMsg) { + super(pMsg); } - public InvalidCmdlineArgumentException(final String msg, final Throwable cause) { - super(msg, cause); + 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 index a2ef3ae106..d57f873b8f 100644 --- a/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java +++ b/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java @@ -13,6 +13,7 @@ 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; @@ -45,15 +46,29 @@ * 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, 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. + * 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. * @@ -71,6 +86,11 @@ public static void main(String[] args) { 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(); @@ -82,29 +102,32 @@ public static void main(String[] args) { * {@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 args Command-line arguments: [--solver SOLVER] [--logic LOGIC] file.smt2 - * @param out output for the result, i.e., sat, unsat, unknown, or the help message - * @param err output for diagnostics and logging - * @param shutdownNotifier a shutdown request aborts the solver, and unknown is reported + * @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[] args, Appendable out, Appendable err, ShutdownNotifier shutdownNotifier) { - if (args.length == 0) { + String[] pArgs, Appendable pOut, Appendable pErr, ShutdownNotifier pShutdownNotifier) { + final String[] args; + if (pArgs.length == 0) { // be nice to user - args = new String[] {"--help"}; + args = new String[] {CmdLineArguments.HELP_ARGUMENT}; + } else { + args = pArgs; } final Map cmdLineOptions; try { cmdLineOptions = CmdLineArguments.processArguments(args); } catch (InvalidCmdlineArgumentException e) { - Output.error(err, "Could not process command line arguments: %s", e.getMessage()); + 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(out); + CmdLineArguments.printHelp(pOut); return 0; } @@ -114,30 +137,31 @@ public static int run( config = Configuration.builder().setOptions(cmdLineOptions).build(); options = new MainOptions(config); } catch (InvalidConfigurationException e) { - Output.error(err, "Invalid configuration: %s", e.getMessage()); + Output.error(pErr, INVALID_CONFIGURATION, describe(e)); return ERROR_EXIT_CODE; } if (options.smt2File == null) { - Output.error(err, "No SMT2 file given, see --help for usage."); + Output.error(pErr, "No SMT2 file given, see --help for usage."); return ERROR_EXIT_CODE; } - LogManager logManager = createLogManager(err); + LogManager logManager = createLogManager(pErr); if (cmdLineOptions.containsKey(CmdLineArguments.LOGIC_OPTION) && options.solver != Solvers.OPENSMT) { - logManager.log( + logManager.logf( Level.WARNING, - "Option --logic is only effective with OpenSMT solver, but solver is set to", - options.solver + ". The logic setting will be ignored."); + "Option --logic is only effective with OpenSMT solver, 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 e) { - Output.error(err, "Could not read SMT2 file: %s", e.getMessage()); + } catch (IOException | InvalidPathException e) { + Output.error(pErr, "Could not read SMT2 file: %s", describe(e)); return ERROR_EXIT_CODE; } @@ -146,85 +170,99 @@ public static int run( scriptError = checkScript(input); } catch (IllegalArgumentException e) { // The tokenizer rejects syntactically broken input, e.g., unbalanced parentheses. - Output.error(err, "Could not parse SMT2 file: %s", describe(e)); + Output.error(pErr, COULD_NOT_PARSE_FILE + ": %s", describe(e)); return ERROR_EXIT_CODE; } if (scriptError.isPresent()) { - Output.error(err, "%s: %s", scriptError.orElseThrow(), options.smt2File); + Output.error(pErr, "%s: %s", scriptError.orElseThrow(), options.smt2File); return ERROR_EXIT_CODE; } - return solve(config, logManager, shutdownNotifier, options.solver, input, out, err); + 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 config, - LogManager logManager, - ShutdownNotifier shutdownNotifier, - Solvers solver, - String input, - Appendable out, - Appendable err) { + Configuration pConfig, + LogManager pLogManager, + ShutdownNotifier pShutdownNotifier, + Solvers pSolver, + String pInput, + Appendable pOut, + Appendable pErr) { try (SolverContext context = - SolverContextFactory.createSolverContext(config, logManager, shutdownNotifier, solver)) { + 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(input); + 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(err, "Could not parse SMT2 file with %s: %s", solver, describe(e)); + 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( - err, - "Solver %s does not support parsing SMT-LIB2 input.%s", - solver, - e.getMessage() == null ? "" : " " + e.getMessage()); + 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. - boolean isUnsat; + final SolverResult result; try (ProverEnvironment prover = context.newProverEnvironment()) { for (BooleanFormula formula : formulas) { prover.addConstraint(formula); } - isUnsat = prover.isUnsat(); + if (prover.isUnsat()) { + result = SolverResult.UNSAT; + } else { + result = SolverResult.SAT; + } } - Output.println(out, isUnsat ? "unsat" : "sat"); + Output.println(pOut, result.toString()); return 0; } catch (InvalidConfigurationException e) { - Output.error(err, "Invalid configuration: %s", describe(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. - String reason = shutdownNotifier.shouldShutdown() ? shutdownNotifier.getReason() : ""; - logManager.log(Level.WARNING, "SMT execution was interrupted.", reason); - Output.println(out, "unknown"); + // 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) { - logManager.logUserException(Level.SEVERE, e, "Error executing SMT2 solver"); - Output.println(out, "unknown"); + 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 e) { - return e.getMessage() != null ? e.getMessage() : e.getClass().getSimpleName(); + private static String describe(Throwable pException) { + if (pException.getMessage() != null) { + return pException.getMessage(); + } else { + return pException.getClass().getSimpleName(); + } } - /** Matches the commands (check-sat) and (check-sat-assuming ..). */ - private static final Pattern CHECK_SAT_COMMAND = Pattern.compile("\\(\\s*check-sat[\\S\\s]*"); - /** * Checks the commands of the script for those that cannot be handled. * @@ -236,47 +274,67 @@ private static String describe(Throwable e) { * @throws IllegalArgumentException if the tokenizer rejects the script, e.g., for unbalanced * parentheses */ - private static Optional checkScript(String input) { + 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. To be supported once parseAll - // handles the assertion stack and resets. - boolean hasCheckSat = false; + // 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(input)) { + 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 (SMTLibTokenizer.isPopToken(token) - || SMTLibTokenizer.isResetToken(token) - || SMTLibTokenizer.isResetAssertionsToken(token)) { + 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( - "Command " - + token - + " is not supported, the assertion stack is not tracked when parsing SMT2 files"); + 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()) { - hasCheckSat = true; + 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 (!hasCheckSat) { + 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 err) { + private static LogManager createLogManager(Appendable pErr) { Handler handler = new Handler() { @Override - public void publish(LogRecord record) { - if (isLoggable(record)) { + public void publish(LogRecord pRecord) { + if (isLoggable(pRecord)) { try { - err.append(getFormatter().format(record)); + pErr.append(getFormatter().format(pRecord)); } catch (IOException e) { throw new UncheckedIOException(e); } @@ -297,8 +355,8 @@ public void close() {} @Options private static final class MainOptions { - private MainOptions(Configuration config) throws InvalidConfigurationException { - config.inject(this); + private MainOptions(Configuration pConfig) throws InvalidConfigurationException { + pConfig.inject(this); } @Option( @@ -311,7 +369,7 @@ private MainOptions(Configuration config) throws InvalidConfigurationException { secure = true, name = CmdLineArguments.SOLVER_OPTION, description = "The SMT solver to use") - private Solvers solver = Solvers.SMTINTERPOL; + 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 index fc83f7b2f3..f7d556d8fc 100644 --- a/src/org/sosy_lab/java_smt/cmdline/Output.java +++ b/src/org/sosy_lab/java_smt/cmdline/Output.java @@ -29,9 +29,9 @@ private Output() {} private static final String REGULAR_COLOR = "\033[m"; /** Appends the line and a line separator to the given output. */ - static void println(Appendable out, String line) { + static void println(Appendable pOut, String pLine) { try { - out.append(line).append(System.lineSeparator()); + pOut.append(pLine).append(System.lineSeparator()); } catch (IOException e) { throw new UncheckedIOException(e); } @@ -41,14 +41,19 @@ static void println(Appendable out, String line) { * 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 err the output for error messages, usually {@link System#err} - * @param msg the message as format string for {@link String#format} - * @param args the arguments for the format string + * @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 err, @FormatString String msg, Object... args) { - String message = String.format(msg, args); - println(err, ""); - println(err, USE_COLORS ? ERROR_COLOR + message + REGULAR_COLOR : message); + 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/package-info.java b/src/org/sosy_lab/java_smt/cmdline/package-info.java index 6a970cc13f..469ff40366 100644 --- a/src/org/sosy_lab/java_smt/cmdline/package-info.java +++ b/src/org/sosy_lab/java_smt/cmdline/package-info.java @@ -9,4 +9,8 @@ */ /** 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 index 051080bb78..b8ea59d52e 100644 --- a/src/org/sosy_lab/java_smt/test/JavaSMTMainTest.java +++ b/src/org/sosy_lab/java_smt/test/JavaSMTMainTest.java @@ -12,11 +12,12 @@ 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.List; import java.util.Locale; import java.util.Map; import java.util.concurrent.TimeUnit; @@ -51,21 +52,14 @@ public class JavaSMTMainTest { """; 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 static final class Run { - final int exitCode; - final String out; - final String err; - - Run(int pExitCode, String pOut, String pErr) { - exitCode = pExitCode; - out = pOut; - err = pErr; - } - } + 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) { @@ -91,194 +85,244 @@ private String smt2File(String content) throws IOException { @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); + 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); + 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(); + 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); + 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).contains("Usage: javasmt"); - assertThat(r.out).doesNotContain("sat" + NL); - assertThat(r.exitCode).isEqualTo(0); + 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).contains("Usage: javasmt"); - assertThat(r.exitCode).isEqualTo(0); + 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).contains("No SMT2 file given"); - assertThat(r.exitCode).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + 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).contains("Unknown command-line argument: --unknown"); - assertThat(r.exitCode).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + 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).contains("Invalid configuration"); - assertThat(r.exitCode).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + 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).contains("Could not read SMT2 file"); - assertThat(r.exitCode).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + 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).contains("no (check-sat) command"); - assertThat(r.exitCode).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + 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 { - Run r = run("--solver", "SMTINTERPOL", smt2File("this is not an SMT2 file\n")); - assertThat(r.out).isEmpty(); - assertThat(r.err).contains("no (check-sat) command"); - assertThat(r.exitCode).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + // 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); + 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).contains("Could not parse SMT2 file"); - assertThat(r.err).doesNotContain("Exception in thread"); - assertThat(r.exitCode).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + 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).contains("Could not parse SMT2 file with SMTINTERPOL"); - assertThat(r.err).doesNotContain("Exception in thread"); - assertThat(r.exitCode).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + 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", + SOLVER, + PRINCESS, smt2File("(declare-fun x () Int)\n(assert (> x true))\n(check-sat)\n")); - assertThat(r.out).isEmpty(); - assertThat(r.err).contains("Could not parse SMT2 file with PRINCESS"); - assertThat(r.exitCode).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + 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).contains("Command (pop 1) is not supported"); - assertThat(r.exitCode).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + 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).contains("Command (reset) is not supported"); - assertThat(r.exitCode).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + 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).contains("Command (reset-assertions) is not supported"); - assertThat(r.exitCode).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + 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).contains("Command (exit) is only allowed as the last command"); - assertThat(r.exitCode).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + 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 testRunUnsupportedCommandIsAnError() throws IOException { + 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).contains("Could not parse SMT2 file"); - assertThat(r.err).contains("(push ...)"); - assertThat(r.exitCode).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + 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 { - Run r = run("--logic", "QF_LIA", "--solver", "SMTINTERPOL", smt2File(SAT_INPUT)); - assertThat(r.out).isEqualTo("sat" + NL); - assertThat(r.exitCode).isEqualTo(0); - assertThat(r.err).contains("Option --logic is only effective with OpenSMT"); - assertThat(r.err.indexOf("--logic")).isEqualTo(r.err.lastIndexOf("--logic")); + 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", smt2File(SAT_INPUT)); - assertThat(r2.err.indexOf("--logic")).isEqualTo(r2.err.lastIndexOf("--logic")); + Run r2 = run("--logic", "QF_LIA", SOLVER, SMTINTERPOL, file); + assertThat(r2.err()).isEqualTo(r.err()); } /** @@ -317,10 +361,10 @@ private static String pigeonholeInput(int holes) { 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).contains("requested by test"); - assertThat(r.exitCode).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + 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) @@ -337,11 +381,11 @@ public void testRunShutdownRequestedWhileSolvingIsUnknown() throws Exception { shutdown.requestShutdown("requested by test while solving"); }); requester.start(); - Run r = run(shutdown.getNotifier(), "--solver", "SMTINTERPOL", smt2File(pigeonholeInput(12))); + Run r = run(shutdown.getNotifier(), SOLVER, SMTINTERPOL, smt2File(pigeonholeInput(12))); requester.join(); - assertThat(r.out).isEqualTo("unknown" + NL); - assertThat(r.err).contains("requested by test while solving"); - assertThat(r.exitCode).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); + assertThat(r.out()).isEqualTo("unknown" + NL); + assertThat(r.err()).isNotEmpty(); + assertThat(r.exitCode()).isEqualTo(JavaSMTMain.ERROR_EXIT_CODE); } @Test(timeout = 60_000) @@ -356,23 +400,54 @@ public void testMainReportsUnknownWhenTerminated() throws Exception { Path outFile = tempDir.newFile("stdout").toPath(); Process process = new ProcessBuilder( - List.of( + ImmutableList.of( Path.of(System.getProperty("java.home"), "bin", "java").toString(), "-cp", System.getProperty("java.class.path"), JavaSMTMain.class.getName(), - "--solver", - "SMTINTERPOL", + SOLVER, + SMTINTERPOL, smt2File(pigeonholeInput(12)))) .redirectOutput(outFile.toFile()) .redirectError(ProcessBuilder.Redirect.DISCARD) .start(); - Thread.sleep(3000); // let the JVM start and the solver run - process.destroy(); - assertThat(process.waitFor(30, TimeUnit.SECONDS)).isTrue(); + 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(); + } + } - assertThat(Files.readString(outFile)).isEqualTo("unknown" + NL); - assertThat(process.exitValue()).isNotEqualTo(0); + @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. @@ -380,7 +455,7 @@ public void testMainReportsUnknownWhenTerminated() throws Exception { @Test public void testProcessArgumentsWithSolverAndFile() throws Exception { Map result = - CmdLineArguments.processArguments(new String[] {"--solver", "Z3", "test.smt2"}); + CmdLineArguments.processArguments(new String[] {SOLVER, "Z3", "test.smt2"}); assertThat(result.get("solver.solver")).isEqualTo("Z3"); assertThat(result.get("smt2.file")).isEqualTo("test.smt2"); } @@ -410,34 +485,40 @@ public void testProcessArgumentsOnlyFile() throws Exception { assertThat(result.get("smt2.file")).isEqualTo("input.smt2"); } - @Test(expected = InvalidCmdlineArgumentException.class) - public void testProcessArgumentsMultipleFiles() throws Exception { - CmdLineArguments.processArguments(new String[] {"file1.smt2", "file2.smt2"}); + @Test + public void testProcessArgumentsMultipleFiles() { + assertThrows( + InvalidCmdlineArgumentException.class, + () -> CmdLineArguments.processArguments(new String[] {"file1.smt2", "file2.smt2"})); } - @Test(expected = InvalidCmdlineArgumentException.class) - public void testProcessArgumentsUnknownArgument() throws Exception { - CmdLineArguments.processArguments(new String[] {"--unknown", "file.smt2"}); + @Test + public void testProcessArgumentsUnknownArgument() { + assertThrows( + InvalidCmdlineArgumentException.class, + () -> CmdLineArguments.processArguments(new String[] {"--unknown", "file.smt2"})); } - @Test(expected = InvalidCmdlineArgumentException.class) - public void testProcessArgumentsSolverMissingValue() throws Exception { - CmdLineArguments.processArguments(new String[] {"--solver"}); + @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"}); + 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 testProcessArgumentsDefaultSolver() throws Exception { + public void testProcessArgumentsWithoutSolverLeavesSolverUnset() throws Exception { Map result = CmdLineArguments.processArguments(new String[] {"test.smt2"}); assertThat(result.get("smt2.file")).isEqualTo("test.smt2"); - assertThat(result.get("solver.solver")).isNull(); + assertThat(result).doesNotContainKey("solver.solver"); } @Test @@ -459,14 +540,23 @@ public void testProcessArgumentsWithLogicShortFlag() throws Exception { public void testProcessArgumentsWithSolverAndLogic() throws Exception { Map result = CmdLineArguments.processArguments( - new String[] {"--solver", "OPENSMT", "--logic", "QF_LIA", "test.smt2"}); + 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("smt2.file")).isEqualTo("test.smt2"); } - @Test(expected = InvalidCmdlineArgumentException.class) - public void testProcessArgumentsLogicMissingValue() throws Exception { - CmdLineArguments.processArguments(new String[] {"--logic"}); + @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"})); } } From 66529fb84ef2e7c5c2ea9c711bdafe8f814f744f Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Tue, 22 Sep 2026 16:31:46 +0000 Subject: [PATCH 22/23] Cmdline: `--logic` also allows to set a logic for Z3. --- .../java_smt/cmdline/CmdLineArguments.java | 20 ++++++++++++++++--- .../java_smt/cmdline/JavaSMTMain.java | 10 ++++++---- .../java_smt/test/JavaSMTMainTest.java | 3 +++ 3 files changed, 26 insertions(+), 7 deletions(-) diff --git a/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java b/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java index 15bb1fec10..6a8646f48d 100644 --- a/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java +++ b/src/org/sosy_lab/java_smt/cmdline/CmdLineArguments.java @@ -32,7 +32,8 @@ private CmdLineArguments() {} // Keys in the map returned by processArguments() static final String SOLVER_OPTION = "solver.solver"; - static final String LOGIC_OPTION = "solver.opensmt.logic"; + 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"; @@ -43,14 +44,18 @@ private CmdLineArguments() {} 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(LOGIC_OPTION) - .withDescription("Set the logic of OpenSMT, ignored for other solvers"), + .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")); @@ -102,6 +107,13 @@ public static Map processArguments(String[] pArgs) } } + // 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; } @@ -155,6 +167,7 @@ public static void printHelp(Appendable 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, ""); @@ -168,6 +181,7 @@ public static void printHelp(Appendable pOut) { 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) diff --git a/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java b/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java index d57f873b8f..34e66b42d7 100644 --- a/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java +++ b/src/org/sosy_lab/java_smt/cmdline/JavaSMTMain.java @@ -148,12 +148,14 @@ public static int run( LogManager logManager = createLogManager(pErr); - if (cmdLineOptions.containsKey(CmdLineArguments.LOGIC_OPTION) - && options.solver != Solvers.OPENSMT) { + // --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 OpenSMT solver, but solver is set to %s." - + " The logic setting will be ignored.", + "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); } diff --git a/src/org/sosy_lab/java_smt/test/JavaSMTMainTest.java b/src/org/sosy_lab/java_smt/test/JavaSMTMainTest.java index b8ea59d52e..9928cd9366 100644 --- a/src/org/sosy_lab/java_smt/test/JavaSMTMainTest.java +++ b/src/org/sosy_lab/java_smt/test/JavaSMTMainTest.java @@ -526,6 +526,7 @@ 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"); } @@ -534,6 +535,7 @@ 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 @@ -543,6 +545,7 @@ public void testProcessArgumentsWithSolverAndLogic() throws Exception { 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"); } From d9112e9238fb5b379e5ad54869c45b2dbfdb5ff3 Mon Sep 17 00:00:00 2001 From: gcarpio21 Date: Wed, 23 Sep 2026 17:04:05 +0000 Subject: [PATCH 23/23] Cmdline: launcher now gives priority to the jar if present, picks bin otherwise. --- javasmt | 40 ++++++++++++++++++++-------------------- 1 file changed, 20 insertions(+), 20 deletions(-) diff --git a/javasmt b/javasmt index 6e934b1b91..58126c53ef 100755 --- a/javasmt +++ b/javasmt @@ -63,27 +63,27 @@ case "$platform" in ;; esac -# JavaSMT can be present either as compiled classes below bin/, which take precedence, or as -# the JAR that "ant jar" produces. 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. -if [ -e "$PATH_TO_JAVASMT/bin/org/sosy_lab/java_smt/cmdline/JavaSMTMain.class" ]; then - JAVASMT_CLASSES="$PATH_TO_JAVASMT/bin" -else - 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" +# 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 - done - if [ -z "$JAVASMT_CLASSES" ]; then + 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