cerc-io/solidity
11
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

[SMTChecker] User timeout option

Browse Source
This commit is contained in:
Leonardo Alt
2020-11-03 10:46:11 +00:00
parent 22b31054b6
commit d03ddeb0fa
47 changed files with 436 additions and 62 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsmtutil/CHCSmtLib2Interface.cpp
+8 -4
View File
@@ -36,11 +36,13 @@ using namespace solidity::frontend;
using namespace solidity::smtutil;
CHCSmtLib2Interface::CHCSmtLib2Interface(
map<h256, string> const& _queryResponses,
ReadCallback::Callback const& _smtCallback
map<h256, string> _queryResponses,
ReadCallback::Callback _smtCallback,
optional<unsigned> _queryTimeout
):
m_smtlib2(make_unique<SMTLib2Interface>(_queryResponses, _smtCallback)),
m_queryResponses(_queryResponses),
CHCSolverInterface(_queryTimeout),
m_smtlib2(make_unique<SMTLib2Interface>(_queryResponses, _smtCallback, m_queryTimeout)),
m_queryResponses(move(_queryResponses)),
m_smtCallback(_smtCallback)
{
reset();
@@ -51,6 +53,8 @@ void CHCSmtLib2Interface::reset()
m_accumulatedOutput.clear();
m_variables.clear();
m_unhandledQueries.clear();
if (m_queryTimeout)
write("(set-option :timeout " + to_string(*m_queryTimeout) + ")");
}
void CHCSmtLib2Interface::registerRelation(Expression const& _expr)
libsmtutil/CHCSmtLib2Interface.h
+3 -2
View File
@@ -33,8 +33,9 @@ class CHCSmtLib2Interface: public CHCSolverInterface
{
public:
explicit CHCSmtLib2Interface(
std::map<util::h256, std::string> const& _queryResponses,
frontend::ReadCallback::Callback const& _smtCallback
std::map<util::h256, std::string> _queryResponses = {},
frontend::ReadCallback::Callback _smtCallback = {},
std::optional<unsigned> _queryTimeout = {}
);
void reset();
libsmtutil/CHCSolverInterface.h
+5
View File
@@ -33,6 +33,8 @@ namespace solidity::smtutil
class CHCSolverInterface
{
public:
CHCSolverInterface(std::optional<unsigned> _queryTimeout = {}): m_queryTimeout(_queryTimeout) {}
virtual ~CHCSolverInterface() = default;
virtual void declareVariable(std::string const& _name, SortPointer const& _sort) = 0;
@@ -56,6 +58,9 @@ public:
virtual std::pair<CheckResult, CexGraph> query(
Expression const& _expr
) = 0;
protected:
std::optional<unsigned> m_queryTimeout;
};
}
libsmtutil/CVC4Interface.cpp
+6 -2
View File
@@ -27,7 +27,8 @@ using namespace solidity;
using namespace solidity::util;
using namespace solidity::smtutil;
CVC4Interface::CVC4Interface():
CVC4Interface::CVC4Interface(optional<unsigned> _queryTimeout):
SolverInterface(_queryTimeout),
m_solver(&m_context)
{
reset();
@@ -38,7 +39,10 @@ void CVC4Interface::reset()
m_variables.clear();
m_solver.reset();
m_solver.setOption("produce-models", true);
m_solver.setResourceLimit(resourceLimit);
if (m_queryTimeout)
m_solver.setTimeLimit(*m_queryTimeout);
else
m_solver.setResourceLimit(resourceLimit);
}
void CVC4Interface::push()
libsmtutil/CVC4Interface.h
+1 -1
View File
@@ -40,7 +40,7 @@ namespace solidity::smtutil
class CVC4Interface: public SolverInterface, public boost::noncopyable
{
public:
CVC4Interface();
CVC4Interface(std::optional<unsigned> _queryTimeout = {});
void reset() override;
libsmtutil/SMTLib2Interface.cpp
+5 -1
View File
@@ -39,8 +39,10 @@ using namespace solidity::smtutil;
SMTLib2Interface::SMTLib2Interface(
map<h256, string> _queryResponses,
ReadCallback::Callback _smtCallback
ReadCallback::Callback _smtCallback,
optional<unsigned> _queryTimeout
):
SolverInterface(_queryTimeout),
m_queryResponses(move(_queryResponses)),
m_smtCallback(move(_smtCallback))
{
@@ -54,6 +56,8 @@ void SMTLib2Interface::reset()
m_variables.clear();
m_userSorts.clear();
write("(set-option :produce-models true)");
if (m_queryTimeout)
write("(set-option :timeout " + to_string(*m_queryTimeout) + ")");
write("(set-logic ALL)");
}
libsmtutil/SMTLib2Interface.h
+2 -1
View File
@@ -40,7 +40,8 @@ class SMTLib2Interface: public SolverInterface, public boost::noncopyable
public:
explicit SMTLib2Interface(
std::map<util::h256, std::string> _queryResponses = {},
frontend::ReadCallback::Callback _smtCallback = {}
frontend::ReadCallback::Callback _smtCallback = {},
std::optional<unsigned> _queryTimeout = {}
);
void reset() override;
libsmtutil/SMTPortfolio.cpp
+7 -5
View File
@@ -35,17 +35,19 @@ using namespace solidity::smtutil;
SMTPortfolio::SMTPortfolio(
map<h256, string> _smtlib2Responses,
frontend::ReadCallback::Callback _smtCallback,
[[maybe_unused]] SMTSolverChoice _enabledSolvers
)
[[maybe_unused]] SMTSolverChoice _enabledSolvers,
optional<unsigned> _queryTimeout
):
SolverInterface(_queryTimeout)
{
m_solvers.emplace_back(make_unique<SMTLib2Interface>(move(_smtlib2Responses), move(_smtCallback)));
m_solvers.emplace_back(make_unique<SMTLib2Interface>(move(_smtlib2Responses), move(_smtCallback), m_queryTimeout));
#ifdef HAVE_Z3
if (_enabledSolvers.z3)
m_solvers.emplace_back(make_unique<Z3Interface>());
m_solvers.emplace_back(make_unique<Z3Interface>(m_queryTimeout));
#endif
#ifdef HAVE_CVC4
if (_enabledSolvers.cvc4)
m_solvers.emplace_back(make_unique<CVC4Interface>());
m_solvers.emplace_back(make_unique<CVC4Interface>(m_queryTimeout));
#endif
}
libsmtutil/SMTPortfolio.h
+2 -1
View File
@@ -42,7 +42,8 @@ public:
SMTPortfolio(
std::map<util::h256, std::string> _smtlib2Responses = {},
frontend::ReadCallback::Callback _smtCallback = {},
SMTSolverChoice _enabledSolvers = SMTSolverChoice::All()
SMTSolverChoice _enabledSolvers = SMTSolverChoice::All(),
std::optional<unsigned> _queryTimeout = {}
);
void reset() override;
libsmtutil/SolverInterface.h
+5
View File
@@ -374,6 +374,8 @@ DEV_SIMPLE_EXCEPTION(SolverError);
class SolverInterface
{
public:
SolverInterface(std::optional<unsigned> _queryTimeout = {}): m_queryTimeout(_queryTimeout) {}
virtual ~SolverInterface() = default;
virtual void reset() = 0;
@@ -401,6 +403,9 @@ public:
/// @returns how many SMT solvers this interface has.
virtual unsigned solvers() { return 1; }
protected:
std::optional<unsigned> m_queryTimeout;
};
}
libsmtutil/Z3CHCInterface.cpp
+15 -4
View File
@@ -27,14 +27,19 @@ using namespace std;
using namespace solidity;
using namespace solidity::smtutil;
Z3CHCInterface::Z3CHCInterface():
m_z3Interface(make_unique<Z3Interface>()),
Z3CHCInterface::Z3CHCInterface(optional<unsigned> _queryTimeout):
CHCSolverInterface(_queryTimeout),
m_z3Interface(make_unique<Z3Interface>(m_queryTimeout)),
m_context(m_z3Interface->context()),
m_solver(*m_context)
{
// These need to be set globally.
z3::set_param("rewriter.pull_cheap_ite", true);
z3::set_param("rlimit", Z3Interface::resourceLimit);
if (m_queryTimeout)
m_context->set("timeout", int(*m_queryTimeout));
else
z3::set_param("rlimit", Z3Interface::resourceLimit);
setSpacerOptions();
}
@@ -97,7 +102,13 @@ pair<CheckResult, CHCSolverInterface::CexGraph> Z3CHCInterface::query(Expression
}
catch (z3::exception const& _err)
{
if (_err.msg() == string("max. resource limit exceeded"))
set<string> msgs{
/// Resource limit (rlimit) exhausted.
"max. resource limit exceeded",
/// User given timeout exhausted.
"canceled"
};
if (msgs.count(_err.msg()))
result = CheckResult::UNKNOWN;
else
result = CheckResult::ERROR;
libsmtutil/Z3CHCInterface.h
+1 -1
View File
@@ -33,7 +33,7 @@ namespace solidity::smtutil
class Z3CHCInterface: public CHCSolverInterface
{
public:
Z3CHCInterface();
Z3CHCInterface(std::optional<unsigned> _queryTimeout = {});
/// Forwards variable declaration to Z3Interface.
void declareVariable(std::string const& _name, SortPointer const& _sort) override;
libsmtutil/Z3Interface.cpp
+19 -4
View File
@@ -27,12 +27,17 @@ using namespace std;
using namespace solidity::smtutil;
using namespace solidity::util;
Z3Interface::Z3Interface():
Z3Interface::Z3Interface(std::optional<unsigned> _queryTimeout):
SolverInterface(_queryTimeout),
m_solver(m_context)
{
// These need to be set globally.
z3::set_param("rewriter.pull_cheap_ite", true);
z3::set_param("rlimit", resourceLimit);
if (m_queryTimeout)
m_context.set("timeout", int(*m_queryTimeout));
else
z3::set_param("rlimit", resourceLimit);
}
void Z3Interface::reset()
@@ -104,9 +109,19 @@ pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _
values.push_back(util::toString(m.eval(toZ3Expr(e))));
}
}
catch (z3::exception const&)
catch (z3::exception const& _err)
{
result = CheckResult::ERROR;
set<string> msgs{
/// Resource limit (rlimit) exhausted.
"max. resource limit exceeded",
/// User given timeout exhausted.
"canceled"
};
if (msgs.count(_err.msg()))
result = CheckResult::UNKNOWN;
else
result = CheckResult::ERROR;
values.clear();
}
libsmtutil/Z3Interface.h
+1 -1
View File
@@ -28,7 +28,7 @@ namespace solidity::smtutil
class Z3Interface: public SolverInterface, public boost::noncopyable
{
public:
Z3Interface();
Z3Interface(std::optional<unsigned> _queryTimeout = {});
void reset() override;