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

review

Browse Source
This commit is contained in:
Leo Alt 2021-05-20 18:07:40 +02:00
parent d828aeee23
commit f7b045b886
4 changed files with 24 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
libsmtutil/CHCSmtLib2Interface.cpp
View File

@ -23,6 +23,8 @@
#include <boost/algorithm/string/join.hpp> #include <boost/algorithm/string/join.hpp>
#include <boost/algorithm/string/predicate.hpp> #include <boost/algorithm/string/predicate.hpp>
#include <range/v3/view.hpp>
#include <array> #include <array>
#include <fstream> #include <fstream>
#include <iostream> #include <iostream>
@ -91,7 +93,7 @@ pair<CheckResult, CHCSolverInterface::CexGraph> CHCSmtLib2Interface::query(Expre
swap(m_accumulatedOutput, accumulated); swap(m_accumulatedOutput, accumulated);
solAssert(m_smtlib2, ""); solAssert(m_smtlib2, "");
writeHeader(); writeHeader();
for (auto const& [type, decl]: m_smtlib2->userSorts()) for (auto const& decl: m_smtlib2->userSorts() | ranges::views::values)
write(decl); write(decl);
m_accumulatedOutput += accumulated; m_accumulatedOutput += accumulated;

7
libsmtutil/SMTLib2Interface.h
View File

@ -66,7 +66,7 @@ public:
std::map<std::string, SortPointer> variables() { return m_variables; } std::map<std::string, SortPointer> variables() { return m_variables; }
std::vector<std::pair<std::string, std::string>>const& userSorts() const { return m_userSorts; } std::vector<std::pair<std::string, std::string>> const& userSorts() const { return m_userSorts; }
private: private:
void declareFunction(std::string const& _name, SortPointer const& _sort); void declareFunction(std::string const& _name, SortPointer const& _sort);
@ -81,6 +81,11 @@ private:
std::vector<std::string> m_accumulatedOutput; std::vector<std::string> m_accumulatedOutput;
std::map<std::string, SortPointer> m_variables; std::map<std::string, SortPointer> m_variables;
/// Each pair in this vector represents an SMTChecker created
/// sort (a user sort), and the smtlib2 declaration of that sort.
/// It needs to be a vector so that the declaration order is kept,
/// otherwise solvers cannot parse the queries.
std::vector<std::pair<std::string, std::string>> m_userSorts; std::vector<std::pair<std::string, std::string>> m_userSorts;
std::map<util::h256, std::string> m_queryResponses; std::map<util::h256, std::string> m_queryResponses;

16
libsmtutil/SolverInterface.h
View File

@ -64,8 +64,20 @@ public:
name(std::move(_name)), arguments(std::move(_arguments)), sort(std::move(_sort)) {} name(std::move(_name)), arguments(std::move(_arguments)), sort(std::move(_sort)) {}
Expression(size_t _number): Expression(std::to_string(_number), {}, SortProvider::sintSort) {} Expression(size_t _number): Expression(std::to_string(_number), {}, SortProvider::sintSort) {}
Expression(u256 const& _number): Expression(_number.str(), {}, SortProvider::sintSort) {} Expression(u256 const& _number): Expression(_number.str(), {}, SortProvider::sintSort) {}
Expression(s256 const& _number): Expression(_number.sign() >= 0 ? _number.str() : "-", _number.sign() >= 0 ? std::vector<Expression>{} : std::vector<Expression>{Expression(size_t(0)), u256(-_number)}, SortProvider::sintSort) {} Expression(s256 const& _number): Expression(
Expression(bigint const& _number): Expression(_number.sign() >= 0 ? _number.str() : "-", _number.sign() >= 0 ? std::vector<Expression>{} : std::vector<Expression>{Expression(size_t(0)), u256(-_number)}, SortProvider::sintSort) {} _number >= 0 ? _number.str() : "-",
_number >= 0 ?
std::vector<Expression>{} :
std::vector<Expression>{Expression(size_t(0)), bigint(-_number)},
SortProvider::sintSort
) {}
Expression(bigint const& _number): Expression(
_number >= 0 ? _number.str() : "-",
_number >= 0 ?
std::vector<Expression>{} :
std::vector<Expression>{Expression(size_t(0)), bigint(-_number)},
SortProvider::sintSort
) {}
Expression(Expression const&) = default; Expression(Expression const&) = default;
Expression(Expression&&) = default; Expression(Expression&&) = default;

1
libsolidity/formal/CHC.cpp
View File

@ -947,6 +947,7 @@ void CHC::resetSourceAnalysis()
{ {
auto smtlib2Interface = dynamic_cast<CHCSmtLib2Interface*>(m_interface.get()); auto smtlib2Interface = dynamic_cast<CHCSmtLib2Interface*>(m_interface.get());
solAssert(smtlib2Interface, ""); solAssert(smtlib2Interface, "");
smtlib2Interface->reset();
m_context.setSolver(smtlib2Interface->smtlib2Interface()); m_context.setSolver(smtlib2Interface->smtlib2Interface());
} }