cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Remove smtlib2 solver option

Browse Source
This commit is contained in:
Martin Blicha 2023-06-26 13:41:17 +02:00
parent 72974adb92
commit f4b849972c
8 changed files with 19 additions and 37 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsmtutil/CHCSmtLib2Interface.cpp
View File

@ -183,7 +183,7 @@ std::string CHCSmtLib2Interface::querySolver(std::string const& _input)
if (m_queryResponses.count(inputHash))
return m_queryResponses.at(inputHash);
smtAssert(m_enabledSolvers.smtlib2 || m_enabledSolvers.eld || m_enabledSolvers.z3);
smtAssert(m_enabledSolvers.eld || m_enabledSolvers.z3);
smtAssert(m_smtCallback, "Callback must be set!");
std::string solverBinary = [&](){
if (m_enabledSolvers.eld)

22
libsmtutil/SolverInterface.h
View File

@ -43,15 +43,13 @@ struct SMTSolverChoice
{
bool cvc4 = false;
bool eld = false;
bool smtlib2 = false;
bool z3 = false;
static constexpr SMTSolverChoice All() noexcept { return {true, true, true, true}; }
static constexpr SMTSolverChoice CVC4() noexcept { return {true, false, false, false}; }
static constexpr SMTSolverChoice ELD() noexcept { return {false, true, false, false}; }
static constexpr SMTSolverChoice SMTLIB2() noexcept { return {false, false, true, false}; }
static constexpr SMTSolverChoice Z3() noexcept { return {false, false, false, true}; }
static constexpr SMTSolverChoice None() noexcept { return {false, false, false, false}; }
static constexpr SMTSolverChoice All() noexcept { return {true, true, true}; }
static constexpr SMTSolverChoice CVC4() noexcept { return {true, false, false}; }
static constexpr SMTSolverChoice ELD() noexcept { return {false, true, false}; }
static constexpr SMTSolverChoice Z3() noexcept { return {false, false, true}; }
static constexpr SMTSolverChoice None() noexcept { return {false, false, false}; }
static std::optional<SMTSolverChoice> fromString(std::string const& _solvers)
{
@ -67,7 +65,6 @@ struct SMTSolverChoice
{
cvc4 &= _other.cvc4;
eld &= _other.eld;
smtlib2 &= _other.smtlib2;
z3 &= _other.z3;
return *this;
}
@ -84,29 +81,26 @@ struct SMTSolverChoice
{
return cvc4 == _other.cvc4 &&
eld == _other.eld &&
smtlib2 == _other.smtlib2 &&
z3 == _other.z3;
}
bool setSolver(std::string const& _solver)
{
static std::set<std::string> const solvers{"cvc4", "eld", "smtlib2", "z3"};
static std::set<std::string> const solvers{"cvc4", "eld", "z3"};
if (!solvers.count(_solver))
return false;
if (_solver == "cvc4")
cvc4 = true;
if (_solver == "eld")
eld = true;
else if (_solver == "smtlib2")
smtlib2 = true;
else if (_solver == "z3")
z3 = true;
return true;
}
bool none() const noexcept { return !some(); }
bool some() const noexcept { return cvc4 || eld || smtlib2 || z3; }
bool all() const noexcept { return cvc4 && eld && smtlib2 && z3; }
bool some() const noexcept { return cvc4 || eld || z3; }
bool all() const noexcept { return cvc4 && eld && z3; }
};
enum class CheckResult

9
libsolidity/formal/BMC.cpp
View File

@ -47,7 +47,6 @@ BMC::BMC(
_smtlib2Responses, _smtCallback, _settings.solvers, _settings.timeout
))
{
solAssert(!_settings.printQuery || _settings.solvers == smtutil::SMTSolverChoice::SMTLIB2(), "Only SMTLib2 solver can be enabled to print queries");
if (m_settings.solvers.cvc4 || m_settings.solvers.z3)
if (!_smtlib2Responses.empty())
m_errorReporter.warning(
@ -62,7 +61,7 @@ BMC::BMC(
void BMC::analyze(SourceUnit const& _source, std::map<ASTNode const*, std::set<VerificationTargetType>, smt::EncodingContext::IdCompare> _solvedTargets)
{
// At this point every enabled solver is available.
if (!m_settings.solvers.cvc4 && !m_settings.solvers.smtlib2 && !m_settings.solvers.z3)
if (!m_settings.solvers.cvc4 && !m_settings.solvers.z3)
{
m_errorReporter.warning(
7710_error,
@ -121,11 +120,7 @@ void BMC::analyze(SourceUnit const& _source, std::map<ASTNode const*, std::set<V
// If this check is true, Z3 and CVC4 are not available
// and the query answers were not provided, since SMTPortfolio
// guarantees that SmtLib2Interface is the first solver, if enabled.
if (
!m_interface->unhandledQueries().empty() &&
m_interface->solvers() == 1 &&
m_settings.solvers.smtlib2
)
if (!m_interface->unhandledQueries().empty())
m_errorReporter.warning(
8084_error,
SourceLocation(),

8
libsolidity/formal/CHC.cpp
View File

@ -66,14 +66,12 @@ CHC::CHC(
SMTEncoder(_context, _settings, _errorReporter, _unsupportedErrorReporter, _charStreamProvider),
m_smtlib2Responses(_smtlib2Responses),
m_smtCallback(_smtCallback)
{
solAssert(!_settings.printQuery || _settings.solvers == smtutil::SMTSolverChoice::SMTLIB2(), "Only SMTLib2 solver can be enabled to print queries");
}
{}
void CHC::analyze(SourceUnit const& _source)
{
// At this point every enabled solver is available.
if (!m_settings.solvers.eld && !m_settings.solvers.smtlib2 && !m_settings.solvers.z3)
if (!m_settings.solvers.eld && !m_settings.solvers.z3)
{
m_errorReporter.warning(
7649_error,
@ -1168,7 +1166,7 @@ void CHC::resetSourceAnalysis()
m_blockCounter = 0;
// At this point every enabled solver is available.
solAssert(m_settings.solvers.smtlib2 || m_settings.solvers.eld || m_settings.solvers.z3);
solAssert(m_settings.solvers.eld || m_settings.solvers.z3);
if (!m_interface)
m_interface = std::make_unique<CHCSmtLib2Interface>(m_smtlib2Responses, m_smtCallback, m_settings.solvers, m_settings.timeout);

2
libsolidity/formal/ModelChecker.cpp
View File

@ -162,7 +162,7 @@ std::vector<std::string> ModelChecker::unhandledQueries()
SMTSolverChoice ModelChecker::availableSolvers()
{
smtutil::SMTSolverChoice available = smtutil::SMTSolverChoice::SMTLIB2();
smtutil::SMTSolverChoice available = smtutil::SMTSolverChoice::None();
#if defined(__linux) || defined(__APPLE__)
available.eld = !boost::process::search_path("eld").empty();
available.z3 = !boost::process::search_path("z3").empty();

3
libsolidity/interface/StandardCompiler.cpp
View File

@ -1094,9 +1094,6 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
if (!printQuery.isBool())
return formatFatalError(Error::Type::JSONError, "settings.modelChecker.printQuery must be a Boolean value.");
if (!(ret.modelCheckerSettings.solvers == smtutil::SMTSolverChoice::SMTLIB2()))
return formatFatalError(Error::Type::JSONError, "Only SMTLib2 solver can be enabled to print queries");
ret.modelCheckerSettings.printQuery = printQuery.asBool();
}

4
solc/CommandLineParser.cpp
View File

@ -853,7 +853,7 @@ General Information)").c_str(),
)
(
g_strModelCheckerSolvers.c_str(),
po::value<std::string>()->value_name("cvc4,eld,z3,smtlib2")->default_value("z3"),
po::value<std::string>()->value_name("cvc4,eld,z3")->default_value("z3"),
"Select model checker solvers."
)
(
@ -1323,8 +1323,6 @@ void CommandLineParser::processArgs()
if (m_args.count(g_strModelCheckerPrintQuery))
{
if (!(m_options.modelChecker.settings.solvers == smtutil::SMTSolverChoice::SMTLIB2()))
solThrow(CommandLineValidationError, "Only SMTLib2 solver can be enabled to print queries");
m_options.modelChecker.settings.printQuery = true;
}

6
test/solc/CommandLineParser.cpp
View File

@ -151,7 +151,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options)
"--model-checker-show-proved-safe",
"--model-checker-show-unproved",
"--model-checker-show-unsupported",
"--model-checker-solvers=z3,smtlib2",
"--model-checker-solvers=z3",
"--model-checker-targets=underflow,divByZero",
"--model-checker-timeout=5"
};
@ -221,7 +221,7 @@ BOOST_AUTO_TEST_CASE(cli_mode_options)
true,
true,
true,
{false, false, true, true},
{false, false, true},
{{VerificationTargetType::Underflow, VerificationTargetType::DivByZero}},
5,
};
@ -413,7 +413,7 @@ BOOST_AUTO_TEST_CASE(invalid_options_input_modes_combinations)
{"--model-checker-div-mod-no-slacks", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}},
{"--model-checker-engine=bmc", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}},
{"--model-checker-invariants=contract,reentrancy", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}},
{"--model-checker-solvers=z3,smtlib2", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}},
{"--model-checker-solvers=z3", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}},
{"--model-checker-timeout=5", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}},
{"--model-checker-contracts=contract1.yul:A,contract2.yul:B", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}},
{"--model-checker-targets=underflow,divByZero", {"--assemble", "--yul", "--strict-assembly", "--standard-json", "--link"}}