Merge pull request #14906 from ethereum/smt-eldarica

SMTChecker: Fix usage of Eldarica with SMT callback

Changelog.md

@@ -11,8 +11,9 @@ Compiler Features:
 Bugfixes:
  * Assembler: Prevent incorrect calculation of tag sizes.
  * EVM Assembly Import: Fix handling of missing source locations during import.
- * SMTChecker: Fix internal error caused by not respecting the sign of an integer type when constructing zero-value SMT expressions.
  * SMTChecker: Ensure query is properly flushed to a file before calling solver when using SMT-LIB interface.
+ * SMTChecker: Fix internal error caused by not respecting the sign of an integer type when constructing zero-value SMT expressions.
+ * SMTChecker: Run Eldarica only when explicitly requested with `--model-checker-solvers eld`, even when it is present on the system.
 
 
 ### 0.8.24 (2024-01-25)

libsolidity/formal/ModelCheckerSettings.h

@@ -175,7 +175,7 @@ struct ModelCheckerSettings
  bool showUnsupported = false;
  smtutil::SMTSolverChoice solvers = smtutil::SMTSolverChoice::Z3();
  ModelCheckerTargets targets = ModelCheckerTargets::Default();
- std::optional<unsigned> timeout;
+ std::optional<unsigned> timeout; // in milliseconds
 
  bool operator!=(ModelCheckerSettings const& _other) const noexcept { return !(*this == _other); }
  bool operator==(ModelCheckerSettings const& _other) const noexcept

libsolidity/interface/CompilerStack.cpp

@@ -53,6 +53,7 @@
 #include <libsolidity/interface/Natspec.h>
 #include <libsolidity/interface/GasEstimator.h>
 #include <libsolidity/interface/StorageLayout.h>
+#include <libsolidity/interface/UniversalCallback.h>
 #include <libsolidity/interface/Version.h>
 #include <libsolidity/parsing/Parser.h>
 
@@ -654,7 +655,12 @@ bool CompilerStack::analyzeLegacy(bool _noErrorsSoFar)
  // m_modelCheckerSettings is spread to engines and solver interfaces,
  // so we need to check whether the enabled ones are available before building the classes.
  if (m_modelCheckerSettings.engine.any())
+ {
  m_modelCheckerSettings.solvers = ModelChecker::checkRequestedSolvers(m_modelCheckerSettings.solvers, m_errorReporter);
+ if (auto* universalCallback = m_readFile.target<frontend::UniversalCallback>())
+ if (m_modelCheckerSettings.solvers.eld)
+ universalCallback->smtCommand().setEldarica(m_modelCheckerSettings.timeout);
+ }
 
  ModelChecker modelChecker(m_errorReporter, *this, m_smtlib2Responses, m_modelCheckerSettings, m_readFile);
  modelChecker.checkRequestedSourcesAndContracts(allSources);

libsolidity/interface/SMTSolverCommand.cpp

@@ -37,7 +37,17 @@ using solidity::util::errinfo_comment;
 namespace solidity::frontend
 {
 
-SMTSolverCommand::SMTSolverCommand(std::string _solverCmd) : m_solverCmd(_solverCmd) {}
+void SMTSolverCommand::setEldarica(std::optional<unsigned int> timeoutInMilliseconds)
+{
+ m_arguments.clear();
+ m_solverCmd = "eld";
+ if (timeoutInMilliseconds)
+ {
+ unsigned int timeoutInSeconds = timeoutInMilliseconds.value() / 1000u;
+ timeoutInSeconds = timeoutInSeconds == 0 ? 1 : timeoutInSeconds;
+ m_arguments.push_back("-t:" + std::to_string(timeoutInSeconds));
+ }
+}
 
 ReadCallback::Result SMTSolverCommand::solve(std::string const& _kind, std::string const& _query)
 {
@@ -46,6 +56,9 @@ ReadCallback::Result SMTSolverCommand::solve(std::string const& _kind, std::stri
  if (_kind != ReadCallback::kindString(ReadCallback::Kind::SMTQuery))
  solAssert(false, "SMTQuery callback used as callback kind " + _kind);
 
+ if (m_solverCmd.empty())
+ return ReadCallback::Result{false, "No solver set."};
+
  auto tempDir = solidity::util::TemporaryDirectory("smt");
  util::h256 queryHash = util::keccak256(_query);
  auto queryFileName = tempDir.path() / ("query_" + queryHash.hex() + ".smt2");
@@ -58,11 +71,15 @@ ReadCallback::Result SMTSolverCommand::solve(std::string const& _kind, std::stri
  if (eldBin.empty())
  return ReadCallback::Result{false, m_solverCmd + " binary not found."};
 
+ auto args = m_arguments;
+ args.push_back(queryFileName.string());
+
  boost::process::ipstream pipe;
  boost::process::child eld(
  eldBin,
- queryFileName,
- boost::process::std_out > pipe
+ args,
+ boost::process::std_out > pipe,
+ boost::process::std_err >boost::process::null
  );
 
  std::vector<std::string> data;

libsolidity/interface/SMTSolverCommand.h

@@ -28,8 +28,6 @@ namespace solidity::frontend
 class SMTSolverCommand
 {
 public:
- SMTSolverCommand(std::string _solverCmd);
-
  /// Calls an SMT solver with the given query.
  frontend::ReadCallback::Result solve(std::string const& _kind, std::string const& _query);
 
@@ -38,9 +36,12 @@ class SMTSolverCommand
  return [this](std::string const& _kind, std::string const& _query) { return solve(_kind, _query); };
  }
 
+ void setEldarica(std::optional<unsigned int> timeoutInMilliseconds);
+
 private:
  /// The name of the solver's binary.
- std::string const m_solverCmd;
+ std::string m_solverCmd;
+ std::vector<std::string> m_arguments;
 };
 
 }

libsolidity/interface/UniversalCallback.h

@@ -34,22 +34,27 @@ class UniversalCallback
  m_solver{_solver}
  {}
 
+ ReadCallback::Result operator()(std::string const& _kind, std::string const& _data)
+ {
+ if (_kind == ReadCallback::kindString(ReadCallback::Kind::ReadFile))
+ if (!m_fileReader)
+ return ReadCallback::Result{false, "No import callback."};
+ else
+ return m_fileReader->readFile(_kind, _data);
+ else if (_kind == ReadCallback::kindString(ReadCallback::Kind::SMTQuery))
+ return m_solver.solve(_kind, _data);
+ solAssert(false, "Unknown callback kind.");
+ }
+
  frontend::ReadCallback::Callback callback()
  {
- return [this](std::string const& _kind, std::string const& _data) -> ReadCallback::Result {
- if (_kind == ReadCallback::kindString(ReadCallback::Kind::ReadFile))
- if (!m_fileReader)
- return ReadCallback::Result{false, "No import callback."};
- else
- return m_fileReader->readFile(_kind, _data);
- else if (_kind == ReadCallback::kindString(ReadCallback::Kind::SMTQuery))
- return m_solver.solve(_kind, _data);
- solAssert(false, "Unknown callback kind.");
- };
+ return *this;
  }
 
  void resetImportCallback() { m_fileReader = nullptr; }
 
+ SMTSolverCommand& smtCommand() { return m_solver; }
+
 private:
  FileReader* m_fileReader;
  SMTSolverCommand& m_solver;

solc/CommandLineInterface.h

@@ -147,7 +147,7 @@ class CommandLineInterface
  std::ostream& m_serr;
  bool m_hasOutput = false;
  FileReader m_fileReader;
- SMTSolverCommand m_solverCommand{"eld"};
+ SMTSolverCommand m_solverCommand;
  UniversalCallback m_universalCallback{&m_fileReader, m_solverCommand};
  std::optional<std::string> m_standardJsonInput;
  std::unique_ptr<frontend::CompilerStack> m_compiler;