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

Introduce bitvector sort.

Browse Source
This commit is contained in:
chriseth 2020-05-11 19:56:29 +02:00
parent 202332405f
commit a2cac93cbf
8 changed files with 21 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsmtutil/CVC4Interface.cpp
View File

@ -289,6 +289,8 @@ CVC4::Type CVC4Interface::cvc4Sort(Sort const& _sort)
return m_context.booleanType(); return m_context.booleanType();
case Kind::Int: case Kind::Int:
return m_context.integerType(); return m_context.integerType();
case Kind::BitVector:
return m_context.mkBitVectorType(dynamic_cast<BitVectorSort const&>(_sort).size);
case Kind::Function: case Kind::Function:
{ {
FunctionSort const& fSort = dynamic_cast<FunctionSort const&>(_sort); FunctionSort const& fSort = dynamic_cast<FunctionSort const&>(_sort);

8
libsmtutil/SMTLib2Interface.cpp
View File

@ -38,11 +38,11 @@ using namespace solidity::frontend;
using namespace solidity::smtutil; using namespace solidity::smtutil;
SMTLib2Interface::SMTLib2Interface( SMTLib2Interface::SMTLib2Interface(
map<h256, string> const& _queryResponses, map<h256, string> _queryResponses,
ReadCallback::Callback _smtCallback ReadCallback::Callback _smtCallback
): ):
m_queryResponses(_queryResponses), m_queryResponses(move(_queryResponses)),
m_smtCallback(std::move(_smtCallback)) m_smtCallback(move(_smtCallback))
{ {
reset(); reset();
} }
@ -215,6 +215,8 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
return "Int"; return "Int";
case Kind::Bool: case Kind::Bool:
return "Bool"; return "Bool";
case Kind::BitVector:
return "(_ BitVec " + to_string(dynamic_cast<BitVectorSort const&>(_sort).size) + ")";
case Kind::Array: case Kind::Array:
{ {
auto const& arraySort = dynamic_cast<ArraySort const&>(_sort); auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);

6
libsmtutil/SMTLib2Interface.h
View File

@ -39,8 +39,8 @@ class SMTLib2Interface: public SolverInterface, public boost::noncopyable
{ {
public: public:
explicit SMTLib2Interface( explicit SMTLib2Interface(
std::map<util::h256, std::string> const& _queryResponses, std::map<util::h256, std::string> _queryResponses = {},
frontend::ReadCallback::Callback _smtCallback frontend::ReadCallback::Callback _smtCallback = {}
); );
void reset() override; void reset() override;
@ -77,7 +77,7 @@ private:
std::map<std::string, SortPointer> m_variables; std::map<std::string, SortPointer> m_variables;
std::set<std::string> m_userSorts; std::set<std::string> m_userSorts;
std::map<util::h256, std::string> const& m_queryResponses; std::map<util::h256, std::string> m_queryResponses;
std::vector<std::string> m_unhandledQueries; std::vector<std::string> m_unhandledQueries;
frontend::ReadCallback::Callback m_smtCallback; frontend::ReadCallback::Callback m_smtCallback;

6
libsmtutil/SMTPortfolio.cpp
View File

@ -33,12 +33,12 @@ using namespace solidity::frontend;
using namespace solidity::smtutil; using namespace solidity::smtutil;
SMTPortfolio::SMTPortfolio( SMTPortfolio::SMTPortfolio(
map<h256, string> const& _smtlib2Responses, map<h256, string> _smtlib2Responses,
frontend::ReadCallback::Callback const& _smtCallback, frontend::ReadCallback::Callback _smtCallback,
[[maybe_unused]] SMTSolverChoice _enabledSolvers [[maybe_unused]] SMTSolverChoice _enabledSolvers
) )
{ {
m_solvers.emplace_back(make_unique<SMTLib2Interface>(_smtlib2Responses, _smtCallback)); m_solvers.emplace_back(make_unique<SMTLib2Interface>(move(_smtlib2Responses), move(_smtCallback)));
#ifdef HAVE_Z3 #ifdef HAVE_Z3
if (_enabledSolvers.z3) if (_enabledSolvers.z3)
m_solvers.emplace_back(make_unique<Z3Interface>()); m_solvers.emplace_back(make_unique<Z3Interface>());

6
libsmtutil/SMTPortfolio.h
View File

@ -40,9 +40,9 @@ class SMTPortfolio: public SolverInterface, public boost::noncopyable
{ {
public: public:
SMTPortfolio( SMTPortfolio(
std::map<util::h256, std::string> const& _smtlib2Responses, std::map<util::h256, std::string> _smtlib2Responses = {},
frontend::ReadCallback::Callback const& _smtCallback, frontend::ReadCallback::Callback _smtCallback = {},
SMTSolverChoice _enabledSolvers SMTSolverChoice _enabledSolvers = SMTSolverChoice::All()
); );
void reset() override; void reset() override;

2
libsmtutil/Sorts.cpp
View File

@ -35,4 +35,6 @@ shared_ptr<IntSort> SortProvider::intSort(bool _signed)
return uintSort; return uintSort;
} }
shared_ptr<BitVectorSort> const SortProvider::bitVectorSort{make_shared<BitVectorSort>(256)};
} }

1
libsmtutil/Sorts.h
View File

@ -195,6 +195,7 @@ struct SortProvider
static std::shared_ptr<IntSort> const uintSort; static std::shared_ptr<IntSort> const uintSort;
static std::shared_ptr<IntSort> const sintSort; static std::shared_ptr<IntSort> const sintSort;
static std::shared_ptr<IntSort> intSort(bool _signed = false); static std::shared_ptr<IntSort> intSort(bool _signed = false);
static std::shared_ptr<BitVectorSort> const bitVectorSort;
}; };
} }

2
libsmtutil/Z3Interface.cpp
View File

@ -245,6 +245,8 @@ z3::sort Z3Interface::z3Sort(Sort const& _sort)
return m_context.bool_sort(); return m_context.bool_sort();
case Kind::Int: case Kind::Int:
return m_context.int_sort(); return m_context.int_sort();
case Kind::BitVector:
return m_context.bv_sort(dynamic_cast<BitVectorSort const&>(_sort).size);
case Kind::Array: case Kind::Array:
{ {
auto const& arraySort = dynamic_cast<ArraySort const&>(_sort); auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);