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

Merge pull request #8976 from ethereum/libsmtutil

Browse Source 
libsmtutil
This commit is contained in:
Leonardo 2020-05-20 16:14:37 +02:00 committed by GitHub
commit 56b5f1bb12
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
43 changed files with 688 additions and 618 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
CMakeLists.txt
View File

@ -51,8 +51,26 @@ configure_file("${CMAKE_SOURCE_DIR}/cmake/templates/license.h.in" include/licens
include(EthOptions)
configure_project(TESTS)
find_package(Z3 4.6.0)
if (${Z3_FOUND})
add_definitions(-DHAVE_Z3)
message("Z3 SMT solver found. This enables optional SMT checking with Z3.")
endif()
find_package(CVC4 QUIET)
if (${CVC4_FOUND})
add_definitions(-DHAVE_CVC4)
message("CVC4 SMT solver found. This enables optional SMT checking with CVC4.")
endif()
if (NOT (${Z3_FOUND} OR ${CVC4_FOUND}))
message("No SMT solver found (or it has been forcefully disabled). Optional SMT checking will not be available.\
\nPlease install Z3 or CVC4 or remove the option disabling them (USE_Z3, USE_CVC4).")
endif()
add_subdirectory(libsolutil)
add_subdirectory(liblangutil)
add_subdirectory(libsmtutil)
add_subdirectory(libevmasm)
add_subdirectory(libyul)
add_subdirectory(libsolidity)

22
libsolidity/formal/CHCSmtLib2Interface.cpp → libsmtutil/CHCSmtLib2Interface.cpp
View File

@ -15,7 +15,7 @@
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
#include <libsolidity/formal/CHCSmtLib2Interface.h>
#include <libsmtutil/CHCSmtLib2Interface.h>
#include <libsolutil/Keccak256.h>
@ -32,7 +32,7 @@ using namespace std;
using namespace solidity;
using namespace solidity::util;
using namespace solidity::frontend;
using namespace solidity::frontend::smt;
using namespace solidity::smtutil;
CHCSmtLib2Interface::CHCSmtLib2Interface(
map<h256, string> const& _queryResponses,
@ -51,10 +51,10 @@ void CHCSmtLib2Interface::reset()
m_variables.clear();
}
void CHCSmtLib2Interface::registerRelation(smt::Expression const& _expr)
void CHCSmtLib2Interface::registerRelation(Expression const& _expr)
{
solAssert(_expr.sort, "");
solAssert(_expr.sort->kind == smt::Kind::Function, "");
smtAssert(_expr.sort, "");
smtAssert(_expr.sort->kind == Kind::Function, "");
if (!m_variables.count(_expr.name))
{
auto fSort = dynamic_pointer_cast<FunctionSort>(_expr.sort);
@ -71,7 +71,7 @@ void CHCSmtLib2Interface::registerRelation(smt::Expression const& _expr)
}
}
void CHCSmtLib2Interface::addRule(smt::Expression const& _expr, std::string const& _name)
void CHCSmtLib2Interface::addRule(Expression const& _expr, std::string const& _name)
{
write(
"(rule (! " +
@ -82,7 +82,7 @@ void CHCSmtLib2Interface::addRule(smt::Expression const& _expr, std::string cons
);
}
pair<CheckResult, vector<string>> CHCSmtLib2Interface::query(smt::Expression const& _block)
pair<CheckResult, vector<string>> CHCSmtLib2Interface::query(Expression const& _block)
{
string accumulated{};
swap(m_accumulatedOutput, accumulated);
@ -112,7 +112,7 @@ pair<CheckResult, vector<string>> CHCSmtLib2Interface::query(smt::Expression con
void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const& _sort)
{
solAssert(_sort, "");
smtAssert(_sort, "");
if (_sort->kind == Kind::Function)
declareFunction(_name, _sort);
else if (!m_variables.count(_name))
@ -124,13 +124,13 @@ void CHCSmtLib2Interface::declareVariable(string const& _name, SortPointer const
void CHCSmtLib2Interface::declareFunction(string const& _name, SortPointer const& _sort)
{
solAssert(_sort, "");
solAssert(_sort->kind == smt::Kind::Function, "");
smtAssert(_sort, "");
smtAssert(_sort->kind == Kind::Function, "");
// TODO Use domain and codomain as key as well
if (!m_variables.count(_name))
{
auto fSort = dynamic_pointer_cast<FunctionSort>(_sort);
solAssert(fSort->codomain, "");
smtAssert(fSort->codomain, "");
string domain = m_smtlib2->toSmtLibSort(fSort->domain);
string codomain = m_smtlib2->toSmtLibSort(*fSort->codomain);
m_variables.insert(_name);

10
libsolidity/formal/CHCSmtLib2Interface.h → libsmtutil/CHCSmtLib2Interface.h
View File

@ -21,11 +21,11 @@
#pragma once
#include <libsolidity/formal/CHCSolverInterface.h>
#include <libsmtutil/CHCSolverInterface.h>
#include <libsolidity/formal/SMTLib2Interface.h>
#include <libsmtutil/SMTLib2Interface.h>
namespace solidity::frontend::smt
namespace solidity::smtutil
{
class CHCSmtLib2Interface: public CHCSolverInterface
@ -33,7 +33,7 @@ class CHCSmtLib2Interface: public CHCSolverInterface
public:
explicit CHCSmtLib2Interface(
std::map<util::h256, std::string> const& _queryResponses,
ReadCallback::Callback const& _smtCallback
frontend::ReadCallback::Callback const& _smtCallback
);
void reset();
@ -67,7 +67,7 @@ private:
std::map<util::h256, std::string> const& m_queryResponses;
std::vector<std::string> m_unhandledQueries;
ReadCallback::Callback m_smtCallback;
frontend::ReadCallback::Callback m_smtCallback;
};
}

4
libsolidity/formal/CHCSolverInterface.h → libsmtutil/CHCSolverInterface.h
View File

@ -21,9 +21,9 @@
#pragma once
#include <libsolidity/formal/SolverInterface.h>
#include <libsmtutil/SolverInterface.h>
namespace solidity::frontend::smt
namespace solidity::smtutil
{
class CHCSolverInterface

35
libsmtutil/CMakeLists.txt Normal file
View File

@ -0,0 +1,35 @@
set(sources
CHCSmtLib2Interface.cpp
CHCSmtLib2Interface.h
Exceptions.h
SMTLib2Interface.cpp
SMTLib2Interface.h
SMTPortfolio.cpp
SMTPortfolio.h
SolverInterface.h
Sorts.cpp
Sorts.h
)
if (${Z3_FOUND})
set(z3_SRCS Z3Interface.cpp Z3Interface.h Z3CHCInterface.cpp Z3CHCInterface.h)
else()
set(z3_SRCS)
endif()
if (${CVC4_FOUND})
set(cvc4_SRCS CVC4Interface.cpp CVC4Interface.h)
else()
set(cvc4_SRCS)
endif()
add_library(smtutil ${sources} ${z3_SRCS} ${cvc4_SRCS})
target_link_libraries(smtutil PUBLIC solutil Boost::boost)
if (${Z3_FOUND})
target_link_libraries(smtutil PUBLIC z3::libz3)
endif()
if (${CVC4_FOUND})
target_link_libraries(smtutil PUBLIC CVC4::CVC4)
endif()

39
libsolidity/formal/CVC4Interface.cpp → libsmtutil/CVC4Interface.cpp
View File

@ -15,15 +15,14 @@
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
#include <libsolidity/formal/CVC4Interface.h>
#include <libsmtutil/CVC4Interface.h>
#include <liblangutil/Exceptions.h>
#include <libsolutil/CommonIO.h>
using namespace std;
using namespace solidity;
using namespace solidity::util;
using namespace solidity::frontend::smt;
using namespace solidity::smtutil;
CVC4Interface::CVC4Interface():
m_solver(&m_context)
@ -51,7 +50,7 @@ void CVC4Interface::pop()
void CVC4Interface::declareVariable(string const& _name, SortPointer const& _sort)
{
solAssert(_sort, "");
smtAssert(_sort, "");
m_variables[_name] = m_context.mkVar(_name.c_str(), cvc4Sort(*_sort));
}
@ -63,19 +62,19 @@ void CVC4Interface::addAssertion(Expression const& _expr)
}
catch (CVC4::TypeCheckingException const& _e)
{
solAssert(false, _e.what());
smtAssert(false, _e.what());
}
catch (CVC4::LogicException const& _e)
{
solAssert(false, _e.what());
smtAssert(false, _e.what());
}
catch (CVC4::UnsafeInterruptException const& _e)
{
solAssert(false, _e.what());
smtAssert(false, _e.what());
}
catch (CVC4::Exception const& _e)
{
solAssert(false, _e.what());
smtAssert(false, _e.what());
}
}
@ -97,7 +96,7 @@ pair<CheckResult, vector<string>> CVC4Interface::check(vector<Expression> const&
result = CheckResult::UNKNOWN;
break;
default:
solAssert(false, "");
smtAssert(false, "");
}
if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty())
@ -147,15 +146,15 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
}
catch (CVC4::TypeCheckingException const& _e)
{
solAssert(false, _e.what());
smtAssert(false, _e.what());
}
catch (CVC4::Exception const& _e)
{
solAssert(false, _e.what());
smtAssert(false, _e.what());
}
}
solAssert(_expr.hasCorrectArity(), "");
smtAssert(_expr.hasCorrectArity(), "");
if (n == "ite")
return arguments[0].iteExpr(arguments[1], arguments[2]);
else if (n == "not")
@ -193,13 +192,13 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
else if (n == "const_array")
{
shared_ptr<SortSort> sortSort = std::dynamic_pointer_cast<SortSort>(_expr.arguments[0].sort);
solAssert(sortSort, "");
smtAssert(sortSort, "");
return m_context.mkConst(CVC4::ArrayStoreAll(cvc4Sort(*sortSort->inner), arguments[1]));
}
else if (n == "tuple_get")
{
shared_ptr<TupleSort> tupleSort = std::dynamic_pointer_cast<TupleSort>(_expr.arguments[0].sort);
solAssert(tupleSort, "");
smtAssert(tupleSort, "");
CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components));
CVC4::Datatype const& dt = tt.getDatatype();
size_t index = std::stoi(_expr.arguments[1].name);
@ -209,25 +208,25 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
else if (n == "tuple_constructor")
{
shared_ptr<TupleSort> tupleSort = std::dynamic_pointer_cast<TupleSort>(_expr.sort);
solAssert(tupleSort, "");
smtAssert(tupleSort, "");
CVC4::DatatypeType tt = m_context.mkTupleType(cvc4Sort(tupleSort->components));
CVC4::Datatype const& dt = tt.getDatatype();
CVC4::Expr c = dt[0].getConstructor();
return m_context.mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, c, arguments);
}
solAssert(false, "");
smtAssert(false, "");
}
catch (CVC4::TypeCheckingException const& _e)
{
solAssert(false, _e.what());
smtAssert(false, _e.what());
}
catch (CVC4::Exception const& _e)
{
solAssert(false, _e.what());
smtAssert(false, _e.what());
}
solAssert(false, "");
smtAssert(false, "");
}
CVC4::Type CVC4Interface::cvc4Sort(Sort const& _sort)
@ -256,7 +255,7 @@ CVC4::Type CVC4Interface::cvc4Sort(Sort const& _sort)
default:
break;
}
solAssert(false, "");
smtAssert(false, "");
// Cannot be reached.
return m_context.integerType();
}

8
libsolidity/formal/CVC4Interface.h → libsmtutil/CVC4Interface.h
View File

@ -17,7 +17,7 @@
#pragma once
#include <libsolidity/formal/SolverInterface.h>
#include <libsmtutil/SolverInterface.h>
#include <boost/noncopyable.hpp>
#if defined(__GLIBC__)
@ -33,7 +33,7 @@
#undef _GLIBCXX_PERMIT_BACKWARD_HASH
#endif
namespace solidity::frontend::smt
namespace solidity::smtutil
{
class CVC4Interface: public SolverInterface, public boost::noncopyable
@ -53,8 +53,8 @@ public:
private:
CVC4::Expr toCVC4Expr(Expression const& _expr);
CVC4::Type cvc4Sort(smt::Sort const& _sort);
std::vector<CVC4::Type> cvc4Sort(std::vector<smt::SortPointer> const& _sorts);
CVC4::Type cvc4Sort(Sort const& _sort);
std::vector<CVC4::Type> cvc4Sort(std::vector<SortPointer> const& _sorts);
CVC4::ExprManager m_context;
CVC4::SmtEngine m_solver;

31
libsmtutil/Exceptions.h Normal file
View File

@ -0,0 +1,31 @@
/*
This file is part of solidity.
solidity is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
solidity is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
#pragma once
#include <libsolutil/Assertions.h>
#include <libsolutil/Exceptions.h>
namespace solidity::smtutil
{
struct SMTLogicError: virtual util::Exception {};
#define smtAssert(CONDITION, DESCRIPTION) \
assertThrow(CONDITION, SMTLogicError, DESCRIPTION)
}

42
libsolidity/formal/SMTLib2Interface.cpp → libsmtutil/SMTLib2Interface.cpp
View File

@ -15,7 +15,7 @@
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
#include <libsolidity/formal/SMTLib2Interface.h>
#include <libsmtutil/SMTLib2Interface.h>
#include <libsolutil/Keccak256.h>
@ -34,7 +34,7 @@ using namespace std;
using namespace solidity;
using namespace solidity::util;
using namespace solidity::frontend;
using namespace solidity::frontend::smt;
using namespace solidity::smtutil;
SMTLib2Interface::SMTLib2Interface(
map<h256, string> const& _queryResponses,
@ -63,13 +63,13 @@ void SMTLib2Interface::push()
void SMTLib2Interface::pop()
{
solAssert(!m_accumulatedOutput.empty(), "");
smtAssert(!m_accumulatedOutput.empty(), "");
m_accumulatedOutput.pop_back();
}
void SMTLib2Interface::declareVariable(string const& _name, SortPointer const& _sort)
{
solAssert(_sort, "");
smtAssert(_sort, "");
if (_sort->kind == Kind::Function)
declareFunction(_name, _sort);
else if (!m_variables.count(_name))
@ -81,8 +81,8 @@ void SMTLib2Interface::declareVariable(string const& _name, SortPointer const& _
void SMTLib2Interface::declareFunction(string const& _name, SortPointer const& _sort)
{
solAssert(_sort, "");
solAssert(_sort->kind == smt::Kind::Function, "");
smtAssert(_sort, "");
smtAssert(_sort->kind == Kind::Function, "");
// TODO Use domain and codomain as key as well
if (!m_variables.count(_name))
{
@ -102,12 +102,12 @@ void SMTLib2Interface::declareFunction(string const& _name, SortPointer const& _
}
}
void SMTLib2Interface::addAssertion(smt::Expression const& _expr)
void SMTLib2Interface::addAssertion(Expression const& _expr)
{
write("(assert " + toSExpr(_expr) + ")");
}
pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<smt::Expression> const& _expressionsToEvaluate)
pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> const& _expressionsToEvaluate)
{
string response = querySolver(
boost::algorithm::join(m_accumulatedOutput, "\n") +
@ -131,7 +131,7 @@ pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<smt::Expression
return make_pair(result, values);
}
string SMTLib2Interface::toSExpr(smt::Expression const& _expr)
string SMTLib2Interface::toSExpr(Expression const& _expr)
{
if (_expr.arguments.empty())
return _expr.name;
@ -139,26 +139,26 @@ string SMTLib2Interface::toSExpr(smt::Expression const& _expr)
std::string sexpr = "(";
if (_expr.name == "const_array")
{
solAssert(_expr.arguments.size() == 2, "");
smtAssert(_expr.arguments.size() == 2, "");
auto sortSort = std::dynamic_pointer_cast<SortSort>(_expr.arguments.at(0).sort);
solAssert(sortSort, "");
smtAssert(sortSort, "");
auto arraySort = dynamic_pointer_cast<ArraySort>(sortSort->inner);
solAssert(arraySort, "");
smtAssert(arraySort, "");
sexpr += "(as const " + toSmtLibSort(*arraySort) + ") ";
sexpr += toSExpr(_expr.arguments.at(1));
}
else if (_expr.name == "tuple_get")
{
solAssert(_expr.arguments.size() == 2, "");
smtAssert(_expr.arguments.size() == 2, "");
auto tupleSort = dynamic_pointer_cast<TupleSort>(_expr.arguments.at(0).sort);
unsigned index = std::stoi(_expr.arguments.at(1).name);
solAssert(index < tupleSort->members.size(), "");
smtAssert(index < tupleSort->members.size(), "");
sexpr += "|" + tupleSort->members.at(index) + "| " + toSExpr(_expr.arguments.at(0));
}
else if (_expr.name == "tuple_constructor")
{
auto tupleSort = dynamic_pointer_cast<TupleSort>(_expr.sort);
solAssert(tupleSort, "");
smtAssert(tupleSort, "");
sexpr += "|" + tupleSort->name + "|";
for (auto const& arg: _expr.arguments)
sexpr += " " + toSExpr(arg);
@ -184,7 +184,7 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
case Kind::Array:
{
auto const& arraySort = dynamic_cast<ArraySort const&>(_sort);
solAssert(arraySort.domain && arraySort.range, "");
smtAssert(arraySort.domain && arraySort.range, "");
return "(Array " + toSmtLibSort(*arraySort.domain) + ' ' + toSmtLibSort(*arraySort.range) + ')';
}
case Kind::Tuple:
@ -195,7 +195,7 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
{
m_userSorts.insert(tupleName);
string decl("(declare-datatypes ((" + tupleName + " 0)) (((" + tupleName);
solAssert(tupleSort.members.size() == tupleSort.components.size(), "");
smtAssert(tupleSort.members.size() == tupleSort.components.size(), "");
for (unsigned i = 0; i < tupleSort.members.size(); ++i)
decl += " (|" + tupleSort.members.at(i) + "| " + toSmtLibSort(*tupleSort.components.at(i)) + ")";
decl += "))))";
@ -205,7 +205,7 @@ string SMTLib2Interface::toSmtLibSort(Sort const& _sort)
return tupleName;
}
default:
solAssert(false, "Invalid SMT sort");
smtAssert(false, "Invalid SMT sort");
}
}
@ -220,11 +220,11 @@ string SMTLib2Interface::toSmtLibSort(vector<SortPointer> const& _sorts)
void SMTLib2Interface::write(string _data)
{
solAssert(!m_accumulatedOutput.empty(), "");
smtAssert(!m_accumulatedOutput.empty(), "");
m_accumulatedOutput.back() += move(_data) + "\n";
}
string SMTLib2Interface::checkSatAndGetValuesCommand(vector<smt::Expression> const& _expressionsToEvaluate)
string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _expressionsToEvaluate)
{
string command;
if (_expressionsToEvaluate.empty())
@ -235,7 +235,7 @@ string SMTLib2Interface::checkSatAndGetValuesCommand(vector<smt::Expression> con
for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
{
auto const& e = _expressionsToEvaluate.at(i);
solAssert(e.sort->kind == Kind::Int || e.sort->kind == Kind::Bool, "Invalid sort for expression to evaluate.");
smtAssert(e.sort->kind == Kind::Int || e.sort->kind == Kind::Bool, "Invalid sort for expression to evaluate.");
command += "(declare-const |EVALEXPR_" + to_string(i) + "| " + (e.sort->kind == Kind::Int ? "Int" : "Bool") + ")\n";
command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n";
}

18
libsolidity/formal/SMTLib2Interface.h → libsmtutil/SMTLib2Interface.h
View File

@ -17,10 +17,10 @@
#pragma once
#include <libsolidity/formal/SolverInterface.h>
#include <libsmtutil/SolverInterface.h>
#include <libsolidity/interface/ReadFile.h>
#include <liblangutil/Exceptions.h>
#include <libsolutil/Common.h>
#include <libsolutil/FixedHash.h>
@ -31,7 +31,7 @@
#include <string>
#include <vector>
namespace solidity::frontend::smt
namespace solidity::smtutil
{
class SMTLib2Interface: public SolverInterface, public boost::noncopyable
@ -39,7 +39,7 @@ class SMTLib2Interface: public SolverInterface, public boost::noncopyable
public:
explicit SMTLib2Interface(
std::map<util::h256, std::string> const& _queryResponses,
ReadCallback::Callback _smtCallback
frontend::ReadCallback::Callback _smtCallback
);
void reset() override;
@ -49,13 +49,13 @@ public:
void declareVariable(std::string const&, SortPointer const&) override;
void addAssertion(smt::Expression const& _expr) override;
std::pair<CheckResult, std::vector<std::string>> check(std::vector<smt::Expression> const& _expressionsToEvaluate) override;
void addAssertion(Expression const& _expr) override;
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
std::vector<std::string> unhandledQueries() override { return m_unhandledQueries; }
// Used by CHCSmtLib2Interface
std::string toSExpr(smt::Expression const& _expr);
std::string toSExpr(Expression const& _expr);
std::string toSmtLibSort(Sort const& _sort);
std::string toSmtLibSort(std::vector<SortPointer> const& _sort);
@ -66,7 +66,7 @@ private:
void write(std::string _data);
std::string checkSatAndGetValuesCommand(std::vector<smt::Expression> const& _expressionsToEvaluate);
std::string checkSatAndGetValuesCommand(std::vector<Expression> const& _expressionsToEvaluate);
std::vector<std::string> parseValues(std::string::const_iterator _start, std::string::const_iterator _end);
/// Communicates with the solver via the callback. Throws SMTSolverError on error.
@ -79,7 +79,7 @@ private:
std::map<util::h256, std::string> const& m_queryResponses;
std::vector<std::string> m_unhandledQueries;
ReadCallback::Callback m_smtCallback;
frontend::ReadCallback::Callback m_smtCallback;
};
}

28
libsolidity/formal/SMTPortfolio.cpp → libsmtutil/SMTPortfolio.cpp
View File

@ -15,36 +15,36 @@
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
#include <libsolidity/formal/SMTPortfolio.h>
#include <libsmtutil/SMTPortfolio.h>
#ifdef HAVE_Z3
#include <libsolidity/formal/Z3Interface.h>
#include <libsmtutil/Z3Interface.h>
#endif
#ifdef HAVE_CVC4
#include <libsolidity/formal/CVC4Interface.h>
#include <libsmtutil/CVC4Interface.h>
#endif
#include <libsolidity/formal/SMTLib2Interface.h>
#include <libsmtutil/SMTLib2Interface.h>
using namespace std;
using namespace solidity;
using namespace solidity::util;
using namespace solidity::frontend;
using namespace solidity::frontend::smt;
using namespace solidity::smtutil;
SMTPortfolio::SMTPortfolio(
map<h256, string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback,
frontend::ReadCallback::Callback const& _smtCallback,
[[maybe_unused]] SMTSolverChoice _enabledSolvers
)
{
m_solvers.emplace_back(make_unique<smt::SMTLib2Interface>(_smtlib2Responses, _smtCallback));
m_solvers.emplace_back(make_unique<SMTLib2Interface>(_smtlib2Responses, _smtCallback));
#ifdef HAVE_Z3
if (_enabledSolvers.z3)
m_solvers.emplace_back(make_unique<smt::Z3Interface>());
m_solvers.emplace_back(make_unique<Z3Interface>());
#endif
#ifdef HAVE_CVC4
if (_enabledSolvers.cvc4)
m_solvers.emplace_back(make_unique<smt::CVC4Interface>());
m_solvers.emplace_back(make_unique<CVC4Interface>());
#endif
}
@ -68,12 +68,12 @@ void SMTPortfolio::pop()
void SMTPortfolio::declareVariable(string const& _name, SortPointer const& _sort)
{
solAssert(_sort, "");
smtAssert(_sort, "");
for (auto const& s: m_solvers)
s->declareVariable(_name, _sort);
}
void SMTPortfolio::addAssertion(smt::Expression const& _expr)
void SMTPortfolio::addAssertion(Expression const& _expr)
{
for (auto const& s: m_solvers)
s->addAssertion(_expr);
@ -109,7 +109,7 @@ void SMTPortfolio::addAssertion(smt::Expression const& _expr)
*
* If all solvers return ERROR, the result is ERROR.
*/
pair<CheckResult, vector<string>> SMTPortfolio::check(vector<smt::Expression> const& _expressionsToEvaluate)
pair<CheckResult, vector<string>> SMTPortfolio::check(vector<Expression> const& _expressionsToEvaluate)
{
CheckResult lastResult = CheckResult::ERROR;
vector<string> finalValues;
@ -141,8 +141,8 @@ vector<string> SMTPortfolio::unhandledQueries()
{
// This code assumes that the constructor guarantees that
// SmtLib2Interface is in position 0.
solAssert(!m_solvers.empty(), "");
solAssert(dynamic_cast<smt::SMTLib2Interface*>(m_solvers.front().get()), "");
smtAssert(!m_solvers.empty(), "");
smtAssert(dynamic_cast<SMTLib2Interface*>(m_solvers.front().get()), "");
return m_solvers.front()->unhandledQueries();
}

14
libsolidity/formal/SMTPortfolio.h → libsmtutil/SMTPortfolio.h
View File

@ -18,7 +18,7 @@
#pragma once
#include <libsolidity/formal/SolverInterface.h>
#include <libsmtutil/SolverInterface.h>
#include <libsolidity/interface/ReadFile.h>
#include <libsolutil/FixedHash.h>
@ -26,7 +26,7 @@
#include <map>
#include <vector>
namespace solidity::frontend::smt
namespace solidity::smtutil
{
/**
@ -40,7 +40,7 @@ class SMTPortfolio: public SolverInterface, public boost::noncopyable
public:
SMTPortfolio(
std::map<util::h256, std::string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback,
frontend::ReadCallback::Callback const& _smtCallback,
SMTSolverChoice _enabledSolvers
);
@ -51,18 +51,18 @@ public:
void declareVariable(std::string const&, SortPointer const&) override;
void addAssertion(smt::Expression const& _expr) override;
void addAssertion(Expression const& _expr) override;
std::pair<CheckResult, std::vector<std::string>> check(std::vector<smt::Expression> const& _expressionsToEvaluate) override;
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
std::vector<std::string> unhandledQueries() override;
unsigned solvers() override { return m_solvers.size(); }
private:
static bool solverAnswered(CheckResult result);
std::vector<std::unique_ptr<smt::SolverInterface>> m_solvers;
std::vector<std::unique_ptr<SolverInterface>> m_solvers;
std::vector<smt::Expression> m_assertions;
std::vector<Expression> m_assertions;
};
}

63
libsolidity/formal/SolverInterface.h → libsmtutil/SolverInterface.h
View File

@ -17,13 +17,10 @@
#pragma once
#include <libsolidity/formal/Sorts.h>
#include <libsmtutil/Exceptions.h>
#include <libsmtutil/Sorts.h>
#include <libsolidity/ast/Types.h>
#include <libsolidity/interface/ReadFile.h>
#include <liblangutil/Exceptions.h>
#include <libsolutil/Common.h>
#include <libsolutil/Exceptions.h>
#include <boost/noncopyable.hpp>
#include <cstdio>
@ -32,7 +29,7 @@
#include <string>
#include <vector>
namespace solidity::frontend::smt
namespace solidity::smtutil
{
struct SMTSolverChoice
@ -55,17 +52,13 @@ enum class CheckResult
SATISFIABLE, UNSATISFIABLE, UNKNOWN, CONFLICTING, ERROR
};
// Forward declaration.
SortPointer smtSort(Type const& _type);
/// C++ representation of an SMTLIB2 expression.
class Expression
{
friend class SolverInterface;
public:
explicit Expression(bool _v): Expression(_v ? "true" : "false", Kind::Bool) {}
explicit Expression(frontend::TypePointer _type): Expression(_type->toString(true), {}, std::make_shared<SortSort>(smtSort(*_type))) {}
explicit Expression(std::shared_ptr<SortSort> _sort): Expression("", {}, _sort) {}
explicit Expression(std::shared_ptr<SortSort> _sort, std::string _name = ""): Expression(std::move(_name), {}, _sort) {}
Expression(size_t _number): Expression(std::to_string(_number), Kind::Int) {}
Expression(u256 const& _number): Expression(_number.str(), Kind::Int) {}
Expression(s256 const& _number): Expression(_number.str(), Kind::Int) {}
@ -81,7 +74,7 @@ public:
if (name == "tuple_constructor")
{
auto tupleSort = std::dynamic_pointer_cast<TupleSort>(sort);
solAssert(tupleSort, "");
smtAssert(tupleSort, "");
return arguments.size() == tupleSort->components.size();
}
@ -111,7 +104,7 @@ public:
static Expression ite(Expression _condition, Expression _trueValue, Expression _falseValue)
{
solAssert(*_trueValue.sort == *_falseValue.sort, "");
smtAssert(*_trueValue.sort == *_falseValue.sort, "");
SortPointer sort = _trueValue.sort;
return Expression("ite", std::vector<Expression>{
std::move(_condition), std::move(_trueValue), std::move(_falseValue)
@ -131,11 +124,11 @@ public:
/// select is the SMT representation of an array index access.
static Expression select(Expression _array, Expression _index)
{
solAssert(_array.sort->kind == Kind::Array, "");
smtAssert(_array.sort->kind == Kind::Array, "");
std::shared_ptr<ArraySort> arraySort = std::dynamic_pointer_cast<ArraySort>(_array.sort);
solAssert(arraySort, "");
solAssert(_index.sort, "");
solAssert(*arraySort->domain == *_index.sort, "");
smtAssert(arraySort, "");
smtAssert(_index.sort, "");
smtAssert(*arraySort->domain == *_index.sort, "");
return Expression(
"select",
std::vector<Expression>{std::move(_array), std::move(_index)},
@ -148,11 +141,11 @@ public:
static Expression store(Expression _array, Expression _index, Expression _element)
{
auto arraySort = std::dynamic_pointer_cast<ArraySort>(_array.sort);
solAssert(arraySort, "");
solAssert(_index.sort, "");
solAssert(_element.sort, "");
solAssert(*arraySort->domain == *_index.sort, "");
solAssert(*arraySort->range == *_element.sort, "");
smtAssert(arraySort, "");
smtAssert(_index.sort, "");
smtAssert(_element.sort, "");
smtAssert(*arraySort->domain == *_index.sort, "");
smtAssert(*arraySort->range == *_element.sort, "");
return Expression(
"store",
std::vector<Expression>{std::move(_array), std::move(_index), std::move(_element)},
@ -162,12 +155,12 @@ public:
static Expression const_array(Expression _sort, Expression _value)
{
solAssert(_sort.sort->kind == Kind::Sort, "");
smtAssert(_sort.sort->kind == Kind::Sort, "");
auto sortSort = std::dynamic_pointer_cast<SortSort>(_sort.sort);
auto arraySort = std::dynamic_pointer_cast<ArraySort>(sortSort->inner);
solAssert(sortSort && arraySort, "");
solAssert(_value.sort, "");
solAssert(*arraySort->range == *_value.sort, "");
smtAssert(sortSort && arraySort, "");
smtAssert(_value.sort, "");
smtAssert(*arraySort->range == *_value.sort, "");
return Expression(
"const_array",
std::vector<Expression>{std::move(_sort), std::move(_value)},
@ -177,10 +170,10 @@ public:
static Expression tuple_get(Expression _tuple, size_t _index)
{
solAssert(_tuple.sort->kind == Kind::Tuple, "");
smtAssert(_tuple.sort->kind == Kind::Tuple, "");
std::shared_ptr<TupleSort> tupleSort = std::dynamic_pointer_cast<TupleSort>(_tuple.sort);
solAssert(tupleSort, "");
solAssert(_index < tupleSort->components.size(), "");
smtAssert(tupleSort, "");
smtAssert(_index < tupleSort->components.size(), "");
return Expression(
"tuple_get",
std::vector<Expression>{std::move(_tuple), Expression(_index)},
@ -190,11 +183,11 @@ public:
static Expression tuple_constructor(Expression _tuple, std::vector<Expression> _arguments)
{
solAssert(_tuple.sort->kind == Kind::Sort, "");
smtAssert(_tuple.sort->kind == Kind::Sort, "");
auto sortSort = std::dynamic_pointer_cast<SortSort>(_tuple.sort);
auto tupleSort = std::dynamic_pointer_cast<TupleSort>(sortSort->inner);
solAssert(tupleSort, "");
solAssert(_arguments.size() == tupleSort->components.size(), "");
smtAssert(tupleSort, "");
smtAssert(_arguments.size() == tupleSort->components.size(), "");
return Expression(
"tuple_constructor",
std::move(_arguments),
@ -260,12 +253,12 @@ public:
}
Expression operator()(std::vector<Expression> _arguments) const
{
solAssert(
smtAssert(
sort->kind == Kind::Function,
"Attempted function application to non-function."
);
auto fSort = dynamic_cast<FunctionSort const*>(sort.get());
solAssert(fSort, "");
smtAssert(fSort, "");
return Expression(name, std::move(_arguments), fSort->codomain);
}
@ -303,7 +296,7 @@ public:
Expression newVariable(std::string _name, SortPointer const& _sort)
{
// Subclasses should do something here
solAssert(_sort, "");
smtAssert(_sort, "");
declareVariable(_name, _sort);
return Expression(std::move(_name), {}, _sort);
}

4
libsolidity/formal/Sorts.cpp → libsmtutil/Sorts.cpp
View File

@ -16,11 +16,11 @@
*/
#include <libsolidity/formal/Sorts.h>
#include <libsmtutil/Sorts.h>
using namespace std;
namespace solidity::frontend::smt
namespace solidity::smtutil
{
shared_ptr<Sort> const SortProvider::boolSort{make_shared<Sort>(Kind::Bool)};

30
libsolidity/formal/Sorts.h → libsmtutil/Sorts.h
View File

@ -17,14 +17,14 @@
#pragma once
#include <liblangutil/Exceptions.h>
#include <libsmtutil/Exceptions.h>
#include <libsolutil/Common.h>
#include <libsolutil/Exceptions.h>
#include <memory>
#include <vector>
namespace solidity::frontend::smt
namespace solidity::smtutil
{
enum class Kind
@ -57,7 +57,7 @@ struct FunctionSort: public Sort
if (!Sort::operator==(_other))
return false;
auto _otherFunction = dynamic_cast<FunctionSort const*>(&_other);
solAssert(_otherFunction, "");
smtAssert(_otherFunction, "");
if (domain.size() != _otherFunction->domain.size())
return false;
if (!std::equal(
@ -67,8 +67,8 @@ struct FunctionSort: public Sort
[&](SortPointer _a, SortPointer _b) { return *_a == *_b; }
))
return false;
solAssert(codomain, "");
solAssert(_otherFunction->codomain, "");
smtAssert(codomain, "");
smtAssert(_otherFunction->codomain, "");
return *codomain == *_otherFunction->codomain;
}
@ -87,11 +87,11 @@ struct ArraySort: public Sort
if (!Sort::operator==(_other))
return false;
auto _otherArray = dynamic_cast<ArraySort const*>(&_other);
solAssert(_otherArray, "");
solAssert(_otherArray->domain, "");
solAssert(_otherArray->range, "");
solAssert(domain, "");
solAssert(range, "");
smtAssert(_otherArray, "");
smtAssert(_otherArray->domain, "");
smtAssert(_otherArray->range, "");
smtAssert(domain, "");
smtAssert(range, "");
return *domain == *_otherArray->domain && *range == *_otherArray->range;
}
@ -107,9 +107,9 @@ struct SortSort: public Sort
if (!Sort::operator==(_other))
return false;
auto _otherSort = dynamic_cast<SortSort const*>(&_other);
solAssert(_otherSort, "");
solAssert(_otherSort->inner, "");
solAssert(inner, "");
smtAssert(_otherSort, "");
smtAssert(_otherSort->inner, "");
smtAssert(inner, "");
return *inner == *_otherSort->inner;
}
@ -134,7 +134,7 @@ struct TupleSort: public Sort
if (!Sort::operator==(_other))
return false;
auto _otherTuple = dynamic_cast<TupleSort const*>(&_other);
solAssert(_otherTuple, "");
smtAssert(_otherTuple, "");
if (name != _otherTuple->name)
return false;
if (members != _otherTuple->members)

7
libsolidity/formal/Z3CHCInterface.cpp → libsmtutil/Z3CHCInterface.cpp
View File

@ -15,14 +15,13 @@
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
#include <libsolidity/formal/Z3CHCInterface.h>
#include <libsmtutil/Z3CHCInterface.h>
#include <liblangutil/Exceptions.h>
#include <libsolutil/CommonIO.h>
using namespace std;
using namespace solidity;
using namespace solidity::frontend::smt;
using namespace solidity::smtutil;
Z3CHCInterface::Z3CHCInterface():
m_z3Interface(make_unique<Z3Interface>()),
@ -48,7 +47,7 @@ Z3CHCInterface::Z3CHCInterface():
void Z3CHCInterface::declareVariable(string const& _name, SortPointer const& _sort)
{
solAssert(_sort, "");
smtAssert(_sort, "");
m_z3Interface->declareVariable(_name, _sort);
}

6
libsolidity/formal/Z3CHCInterface.h → libsmtutil/Z3CHCInterface.h
View File

@ -21,10 +21,10 @@
#pragma once
#include <libsolidity/formal/CHCSolverInterface.h>
#include <libsolidity/formal/Z3Interface.h>
#include <libsmtutil/CHCSolverInterface.h>
#include <libsmtutil/Z3Interface.h>
namespace solidity::frontend::smt
namespace solidity::smtutil
{
class Z3CHCInterface: public CHCSolverInterface

31
libsolidity/formal/Z3Interface.cpp → libsmtutil/Z3Interface.cpp
View File

@ -15,13 +15,12 @@
along with solidity. If not, see <http://www.gnu.org/licenses/>.
*/
#include <libsolidity/formal/Z3Interface.h>
#include <libsmtutil/Z3Interface.h>
#include <liblangutil/Exceptions.h>
#include <libsolutil/CommonIO.h>
using namespace std;
using namespace solidity::frontend::smt;
using namespace solidity::smtutil;
Z3Interface::Z3Interface():
m_solver(m_context)
@ -50,7 +49,7 @@ void Z3Interface::pop()
void Z3Interface::declareVariable(string const& _name, SortPointer const& _sort)
{
solAssert(_sort, "");
smtAssert(_sort, "");
if (_sort->kind == Kind::Function)
declareFunction(_name, *_sort);
else if (m_constants.count(_name))
@ -61,7 +60,7 @@ void Z3Interface::declareVariable(string const& _name, SortPointer const& _sort)
void Z3Interface::declareFunction(string const& _name, Sort const& _sort)
{
solAssert(_sort.kind == smt::Kind::Function, "");
smtAssert(_sort.kind == Kind::Function, "");
FunctionSort fSort = dynamic_cast<FunctionSort const&>(_sort);
if (m_functions.count(_name))
m_functions.at(_name) = m_context.function(_name.c_str(), z3Sort(fSort.domain), z3Sort(*fSort.codomain));
@ -124,7 +123,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
return m_functions.at(n)(arguments);
else if (m_constants.count(n))
{
solAssert(arguments.empty(), "");
smtAssert(arguments.empty(), "");
return m_constants.at(n);
}
else if (arguments.empty())
@ -136,7 +135,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
else if (_expr.sort->kind == Kind::Sort)
{
auto sortSort = dynamic_pointer_cast<SortSort>(_expr.sort);
solAssert(sortSort, "");
smtAssert(sortSort, "");
return m_context.constant(n.c_str(), z3Sort(*sortSort->inner));
}
else
@ -146,11 +145,11 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
}
catch (z3::exception const& _e)
{
solAssert(false, _e.msg());
smtAssert(false, _e.msg());
}
}
solAssert(_expr.hasCorrectArity(), "");
smtAssert(_expr.hasCorrectArity(), "");
if (n == "ite")
return z3::ite(arguments[0], arguments[1], arguments[2]);
else if (n == "not")
@ -188,9 +187,9 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
else if (n == "const_array")
{
shared_ptr<SortSort> sortSort = std::dynamic_pointer_cast<SortSort>(_expr.arguments[0].sort);
solAssert(sortSort, "");
smtAssert(sortSort, "");
auto arraySort = dynamic_pointer_cast<ArraySort>(sortSort->inner);
solAssert(arraySort && arraySort->domain, "");
smtAssert(arraySort && arraySort->domain, "");
return z3::const_array(z3Sort(*arraySort->domain), arguments[1]);
}
else if (n == "tuple_get")
@ -201,21 +200,21 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
else if (n == "tuple_constructor")
{
auto constructor = z3::func_decl(m_context, Z3_get_tuple_sort_mk_decl(m_context, z3Sort(*_expr.sort)));
solAssert(constructor.arity() == arguments.size(), "");
smtAssert(constructor.arity() == arguments.size(), "");
z3::expr_vector args(m_context);
for (auto const& arg: arguments)
args.push_back(arg);
return constructor(args);
}
solAssert(false, "");
smtAssert(false, "");
}
catch (z3::exception const& _e)
{
solAssert(false, _e.msg());
smtAssert(false, _e.msg());
}
solAssert(false, "");
smtAssert(false, "");
}
z3::sort Z3Interface::z3Sort(Sort const& _sort)
@ -256,7 +255,7 @@ z3::sort Z3Interface::z3Sort(Sort const& _sort)
default:
break;
}
solAssert(false, "");
smtAssert(false, "");
// Cannot be reached.
return m_context.int_sort();
}

8
libsolidity/formal/Z3Interface.h → libsmtutil/Z3Interface.h
View File

@ -17,11 +17,11 @@
#pragma once
#include <libsolidity/formal/SolverInterface.h>
#include <libsmtutil/SolverInterface.h>
#include <boost/noncopyable.hpp>
#include <z3++.h>
namespace solidity::frontend::smt
namespace solidity::smtutil
{
class Z3Interface: public SolverInterface, public boost::noncopyable
@ -55,8 +55,8 @@ public:
private:
void declareFunction(std::string const& _name, Sort const& _sort);
z3::sort z3Sort(smt::Sort const& _sort);
z3::sort_vector z3Sort(std::vector<smt::SortPointer> const& _sorts);
z3::sort z3Sort(Sort const& _sort);
z3::sort_vector z3Sort(std::vector<SortPointer> const& _sorts);
z3::context m_context;
z3::solver m_solver;

44
libsolidity/CMakeLists.txt
View File

@ -94,22 +94,12 @@ set(sources
formal/BMC.h
formal/CHC.cpp
formal/CHC.h
formal/CHCSmtLib2Interface.cpp
formal/CHCSmtLib2Interface.h
formal/CHCSolverInterface.h
formal/EncodingContext.cpp
formal/EncodingContext.h
formal/ModelChecker.cpp
formal/ModelChecker.h
formal/SMTEncoder.cpp
formal/SMTEncoder.h
formal/SMTLib2Interface.cpp
formal/SMTLib2Interface.h
formal/SMTPortfolio.cpp
formal/SMTPortfolio.h
formal/SolverInterface.h
formal/Sorts.cpp
formal/Sorts.h
formal/SSAVariable.cpp
formal/SSAVariable.h
formal/SymbolicState.cpp
@ -144,36 +134,6 @@ set(sources
parsing/Token.h
)
find_package(Z3 4.6.0)
if (${Z3_FOUND})
add_definitions(-DHAVE_Z3)
message("Z3 SMT solver found. This enables optional SMT checking with Z3.")
set(z3_SRCS formal/Z3Interface.cpp formal/Z3Interface.h formal/Z3CHCInterface.cpp formal/Z3CHCInterface.h)
else()
set(z3_SRCS)
endif()
add_library(solidity ${sources})
target_link_libraries(solidity PUBLIC yul evmasm langutil smtutil solutil Boost::boost)
find_package(CVC4 QUIET)
if (${CVC4_FOUND})
add_definitions(-DHAVE_CVC4)
message("CVC4 SMT solver found. This enables optional SMT checking with CVC4.")
set(cvc4_SRCS formal/CVC4Interface.cpp formal/CVC4Interface.h)
else()
set(cvc4_SRCS)
endif()
if (NOT (${Z3_FOUND} OR ${CVC4_FOUND}))
message("No SMT solver found (or it has been forcefully disabled). Optional SMT checking will not be available.\
\nPlease install Z3 or CVC4 or remove the option disabling them (USE_Z3, USE_CVC4).")
endif()
add_library(solidity ${sources} ${z3_SRCS} ${cvc4_SRCS})
target_link_libraries(solidity PUBLIC yul evmasm langutil solutil Boost::boost)
if (${Z3_FOUND})
target_link_libraries(solidity PUBLIC z3::libz3)
endif()
if (${CVC4_FOUND})
target_link_libraries(solidity PUBLIC CVC4::CVC4)
endif()

93
libsolidity/formal/BMC.cpp
View File

@ -17,10 +17,11 @@
#include <libsolidity/formal/BMC.h>
#include <libsolidity/formal/SMTPortfolio.h>
#include <libsolidity/formal/SymbolicState.h>
#include <libsolidity/formal/SymbolicTypes.h>
#include <libsmtutil/SMTPortfolio.h>
using namespace std;
using namespace solidity;
using namespace solidity::util;
@ -32,10 +33,10 @@ BMC::BMC(
ErrorReporter& _errorReporter,
map<h256, string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback,
smt::SMTSolverChoice _enabledSolvers
smtutil::SMTSolverChoice _enabledSolvers
):
SMTEncoder(_context),
m_interface(make_unique<smt::SMTPortfolio>(_smtlib2Responses, _smtCallback, _enabledSolvers)),
m_interface(make_unique<smtutil::SMTPortfolio>(_smtlib2Responses, _smtCallback, _enabledSolvers)),
m_outerErrorReporter(_errorReporter)
{
#if defined (HAVE_Z3) || defined (HAVE_CVC4)
@ -132,7 +133,7 @@ void BMC::endVisit(ContractDefinition const& _contract)
{
inlineConstructorHierarchy(_contract);
/// Check targets created by state variable initialization.
smt::Expression constraints = m_context.assertions();
smtutil::Expression constraints = m_context.assertions();
checkVerificationTargets(constraints);
m_verificationTargets.clear();
}
@ -166,7 +167,7 @@ void BMC::endVisit(FunctionDefinition const& _function)
{
if (isRootFunction())
{
smt::Expression constraints = m_context.assertions();
smtutil::Expression constraints = m_context.assertions();
checkVerificationTargets(constraints);
m_verificationTargets.clear();
}
@ -293,7 +294,7 @@ bool BMC::visit(ForStatement const& _node)
if (_node.condition())
_node.condition()->accept(*this);
auto forCondition = _node.condition() ? expr(*_node.condition()) : smt::Expression(true);
auto forCondition = _node.condition() ? expr(*_node.condition()) : smtutil::Expression(true);
mergeVariables(touchedVars, forCondition, indicesAfterLoop, copyVariableIndices());
m_loopExecutionHappened = true;
@ -380,7 +381,7 @@ void BMC::endVisit(FunctionCall const& _funCall)
SMTEncoder::endVisit(_funCall);
auto value = _funCall.arguments().front();
solAssert(value, "");
smt::Expression thisBalance = m_context.state().balance();
smtutil::Expression thisBalance = m_context.state().balance();
addVerificationTarget(
VerificationTarget::Type::Balance,
@ -452,7 +453,7 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
void BMC::abstractFunctionCall(FunctionCall const& _funCall)
{
vector<smt::Expression> smtArguments;
vector<smtutil::Expression> smtArguments;
for (auto const& arg: _funCall.arguments())
smtArguments.push_back(expr(*arg));
defineExpr(_funCall, (*m_context.expression(_funCall.expression()))(smtArguments));
@ -479,10 +480,10 @@ void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
}
}
pair<smt::Expression, smt::Expression> BMC::arithmeticOperation(
pair<smtutil::Expression, smtutil::Expression> BMC::arithmeticOperation(
Token _op,
smt::Expression const& _left,
smt::Expression const& _right,
smtutil::Expression const& _left,
smtutil::Expression const& _right,
TypePointer const& _commonType,
Expression const& _expression
)
@ -515,9 +516,9 @@ void BMC::reset()
m_loopExecutionHappened = false;
}
pair<vector<smt::Expression>, vector<string>> BMC::modelExpressions()
pair<vector<smtutil::Expression>, vector<string>> BMC::modelExpressions()
{
vector<smt::Expression> expressionsToEvaluate;
vector<smtutil::Expression> expressionsToEvaluate;
vector<string> expressionNames;
for (auto const& var: m_context.variables())
if (var.first->type()->isValueType())
@ -530,7 +531,7 @@ pair<vector<smt::Expression>, vector<string>> BMC::modelExpressions()
auto const& type = var.second->type();
if (
type->isValueType() &&
smt::smtKind(type->category()) != smt::Kind::Function
smt::smtKind(type->category()) != smtutil::Kind::Function
)
{
expressionsToEvaluate.emplace_back(var.second->currentValue());
@ -549,13 +550,13 @@ pair<vector<smt::Expression>, vector<string>> BMC::modelExpressions()
/// Verification targets.
void BMC::checkVerificationTargets(smt::Expression const& _constraints)
void BMC::checkVerificationTargets(smtutil::Expression const& _constraints)
{
for (auto& target: m_verificationTargets)
checkVerificationTarget(target, _constraints);
}
void BMC::checkVerificationTarget(BMCVerificationTarget& _target, smt::Expression const& _constraints)
void BMC::checkVerificationTarget(BMCVerificationTarget& _target, smtutil::Expression const& _constraints)
{
switch (_target.type)
{
@ -596,7 +597,7 @@ void BMC::checkConstantCondition(BMCVerificationTarget& _target)
);
}
void BMC::checkUnderflow(BMCVerificationTarget& _target, smt::Expression const& _constraints)
void BMC::checkUnderflow(BMCVerificationTarget& _target, smtutil::Expression const& _constraints)
{
solAssert(
_target.type == VerificationTarget::Type::Underflow ||
@ -618,7 +619,7 @@ void BMC::checkUnderflow(BMCVerificationTarget& _target, smt::Expression const&
);
}
void BMC::checkOverflow(BMCVerificationTarget& _target, smt::Expression const& _constraints)
void BMC::checkOverflow(BMCVerificationTarget& _target, smtutil::Expression const& _constraints)
{
solAssert(
_target.type == VerificationTarget::Type::Overflow ||
@ -688,7 +689,7 @@ void BMC::checkAssert(BMCVerificationTarget& _target)
void BMC::addVerificationTarget(
VerificationTarget::Type _type,
smt::Expression const& _value,
smtutil::Expression const& _value,
Expression const* _expression
)
{
@ -711,21 +712,21 @@ void BMC::addVerificationTarget(
/// Solving.
void BMC::checkCondition(
smt::Expression _condition,
smtutil::Expression _condition,
vector<SMTEncoder::CallStackEntry> const& _callStack,
pair<vector<smt::Expression>, vector<string>> const& _modelExpressions,
pair<vector<smtutil::Expression>, vector<string>> const& _modelExpressions,
SourceLocation const& _location,
ErrorId _errorHappens,
ErrorId _errorMightHappen,
string const& _description,
string const& _additionalValueName,
smt::Expression const* _additionalValue
smtutil::Expression const* _additionalValue
)
{
m_interface->push();
m_interface->addAssertion(_condition);
vector<smt::Expression> expressionsToEvaluate;
vector<smtutil::Expression> expressionsToEvaluate;
vector<string> expressionNames;
tie(expressionsToEvaluate, expressionNames) = _modelExpressions;
if (_callStack.size())
@ -734,7 +735,7 @@ void BMC::checkCondition(
expressionsToEvaluate.emplace_back(*_additionalValue);
expressionNames.push_back(_additionalValueName);
}
smt::CheckResult result;
smtutil::CheckResult result;
vector<string> values;
tie(result, values) = checkSatisfiableAndGenerateModel(expressionsToEvaluate);
@ -755,7 +756,7 @@ void BMC::checkCondition(
switch (result)
{
case smt::CheckResult::SATISFIABLE:
case smtutil::CheckResult::SATISFIABLE:
{
std::ostringstream message;
message << _description << " happens here";
@ -787,15 +788,15 @@ void BMC::checkCondition(
}
break;
}
case smt::CheckResult::UNSATISFIABLE:
case smtutil::CheckResult::UNSATISFIABLE:
break;
case smt::CheckResult::UNKNOWN:
case smtutil::CheckResult::UNKNOWN:
m_errorReporter.warning(_errorMightHappen, _location, _description + " might happen here.", secondaryLocation);
break;
case smt::CheckResult::CONFLICTING:
case smtutil::CheckResult::CONFLICTING:
m_errorReporter.warning(1584_error, _location, "At least two SMT solvers provided conflicting answers. Results might not be sound.");
break;
case smt::CheckResult::ERROR:
case smtutil::CheckResult::ERROR:
m_errorReporter.warning(1823_error, _location, "Error trying to invoke SMT solver.");
break;
}
@ -805,8 +806,8 @@ void BMC::checkCondition(
void BMC::checkBooleanNotConstant(
Expression const& _condition,
smt::Expression const& _constraints,
smt::Expression const& _value,
smtutil::Expression const& _constraints,
smtutil::Expression const& _value,
vector<SMTEncoder::CallStackEntry> const& _callStack
)
{
@ -824,32 +825,32 @@ void BMC::checkBooleanNotConstant(
auto negatedResult = checkSatisfiable();
m_interface->pop();
if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR)
if (positiveResult == smtutil::CheckResult::ERROR || negatedResult == smtutil::CheckResult::ERROR)
m_errorReporter.warning(8592_error, _condition.location(), "Error trying to invoke SMT solver.");
else if (positiveResult == smt::CheckResult::CONFLICTING || negatedResult == smt::CheckResult::CONFLICTING)
else if (positiveResult == smtutil::CheckResult::CONFLICTING || negatedResult == smtutil::CheckResult::CONFLICTING)
m_errorReporter.warning(3356_error, _condition.location(), "At least two SMT solvers provided conflicting answers. Results might not be sound.");
else if (positiveResult == smt::CheckResult::SATISFIABLE && negatedResult == smt::CheckResult::SATISFIABLE)
else if (positiveResult == smtutil::CheckResult::SATISFIABLE && negatedResult == smtutil::CheckResult::SATISFIABLE)
{
// everything fine.
}
else if (positiveResult == smt::CheckResult::UNKNOWN || negatedResult == smt::CheckResult::UNKNOWN)
else if (positiveResult == smtutil::CheckResult::UNKNOWN || negatedResult == smtutil::CheckResult::UNKNOWN)
{
// can't do anything.
}
else if (positiveResult == smt::CheckResult::UNSATISFIABLE && negatedResult == smt::CheckResult::UNSATISFIABLE)
else if (positiveResult == smtutil::CheckResult::UNSATISFIABLE && negatedResult == smtutil::CheckResult::UNSATISFIABLE)
m_errorReporter.warning(2512_error, _condition.location(), "Condition unreachable.", SMTEncoder::callStackMessage(_callStack));
else
{
string description;
if (positiveResult == smt::CheckResult::SATISFIABLE)
if (positiveResult == smtutil::CheckResult::SATISFIABLE)
{
solAssert(negatedResult == smt::CheckResult::UNSATISFIABLE, "");
solAssert(negatedResult == smtutil::CheckResult::UNSATISFIABLE, "");
description = "Condition is always true.";
}
else
{
solAssert(positiveResult == smt::CheckResult::UNSATISFIABLE, "");
solAssert(negatedResult == smt::CheckResult::SATISFIABLE, "");
solAssert(positiveResult == smtutil::CheckResult::UNSATISFIABLE, "");
solAssert(negatedResult == smtutil::CheckResult::SATISFIABLE, "");
description = "Condition is always false.";
}
m_errorReporter.warning(
@ -861,22 +862,22 @@ void BMC::checkBooleanNotConstant(
}
}
pair<smt::CheckResult, vector<string>>
BMC::checkSatisfiableAndGenerateModel(vector<smt::Expression> const& _expressionsToEvaluate)
pair<smtutil::CheckResult, vector<string>>
BMC::checkSatisfiableAndGenerateModel(vector<smtutil::Expression> const& _expressionsToEvaluate)
{
smt::CheckResult result;
smtutil::CheckResult result;
vector<string> values;
try
{
tie(result, values) = m_interface->check(_expressionsToEvaluate);
}
catch (smt::SolverError const& _e)
catch (smtutil::SolverError const& _e)
{
string description("Error querying SMT solver");
if (_e.comment())
description += ": " + *_e.comment();
m_errorReporter.warning(8140_error, description);
result = smt::CheckResult::ERROR;
result = smtutil::CheckResult::ERROR;
}
for (string& value: values)
@ -892,7 +893,7 @@ BMC::checkSatisfiableAndGenerateModel(vector<smt::Expression> const& _expression
return make_pair(result, values);
}
smt::CheckResult BMC::checkSatisfiable()
smtutil::CheckResult BMC::checkSatisfiable()
{
return checkSatisfiableAndGenerateModel({}).first;
}

43
libsolidity/formal/BMC.h
View File

@ -30,9 +30,10 @@
#include <libsolidity/formal/EncodingContext.h>
#include <libsolidity/formal/SMTEncoder.h>
#include <libsolidity/formal/SolverInterface.h>
#include <libsolidity/interface/ReadFile.h>
#include <libsmtutil/SolverInterface.h>
#include <liblangutil/ErrorReporter.h>
#include <set>
@ -59,7 +60,7 @@ public:
langutil::ErrorReporter& _errorReporter,
std::map<h256, std::string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback,
smt::SMTSolverChoice _enabledSolvers
smtutil::SMTSolverChoice _enabledSolvers
);
void analyze(SourceUnit const& _sources, std::set<Expression const*> _safeAssertions);
@ -102,10 +103,10 @@ private:
void internalOrExternalFunctionCall(FunctionCall const& _funCall);
/// Creates underflow/overflow verification targets.
std::pair<smt::Expression, smt::Expression> arithmeticOperation(
std::pair<smtutil::Expression, smtutil::Expression> arithmeticOperation(
Token _op,
smt::Expression const& _left,
smt::Expression const& _right,
smtutil::Expression const& _left,
smtutil::Expression const& _right,
TypePointer const& _commonType,
Expression const& _expression
) override;
@ -113,7 +114,7 @@ private:
void resetStorageReferences();
void reset();
std::pair<std::vector<smt::Expression>, std::vector<std::string>> modelExpressions();
std::pair<std::vector<smtutil::Expression>, std::vector<std::string>> modelExpressions();
//@}
/// Verification targets.
@ -122,20 +123,20 @@ private:
{
Expression const* expression;
std::vector<CallStackEntry> callStack;
std::pair<std::vector<smt::Expression>, std::vector<std::string>> modelExpressions;
std::pair<std::vector<smtutil::Expression>, std::vector<std::string>> modelExpressions;
};
void checkVerificationTargets(smt::Expression const& _constraints);
void checkVerificationTarget(BMCVerificationTarget& _target, smt::Expression const& _constraints = smt::Expression(true));
void checkVerificationTargets(smtutil::Expression const& _constraints);
void checkVerificationTarget(BMCVerificationTarget& _target, smtutil::Expression const& _constraints = smtutil::Expression(true));
void checkConstantCondition(BMCVerificationTarget& _target);
void checkUnderflow(BMCVerificationTarget& _target, smt::Expression const& _constraints);
void checkOverflow(BMCVerificationTarget& _target, smt::Expression const& _constraints);
void checkUnderflow(BMCVerificationTarget& _target, smtutil::Expression const& _constraints);
void checkOverflow(BMCVerificationTarget& _target, smtutil::Expression const& _constraints);
void checkDivByZero(BMCVerificationTarget& _target);
void checkBalance(BMCVerificationTarget& _target);
void checkAssert(BMCVerificationTarget& _target);
void addVerificationTarget(
VerificationTarget::Type _type,
smt::Expression const& _value,
smtutil::Expression const& _value,
Expression const* _expression
);
//@}
@ -144,31 +145,31 @@ private:
//@{
/// Check that a condition can be satisfied.
void checkCondition(
smt::Expression _condition,
smtutil::Expression _condition,
std::vector<CallStackEntry> const& _callStack,
std::pair<std::vector<smt::Expression>, std::vector<std::string>> const& _modelExpressions,
std::pair<std::vector<smtutil::Expression>, std::vector<std::string>> const& _modelExpressions,
langutil::SourceLocation const& _location,
langutil::ErrorId _errorHappens,
langutil::ErrorId _errorMightHappen,
std::string const& _description,
std::string const& _additionalValueName = "",
smt::Expression const* _additionalValue = nullptr
smtutil::Expression const* _additionalValue = nullptr
);
/// Checks that a boolean condition is not constant. Do not warn if the expression
/// is a literal constant.
void checkBooleanNotConstant(
Expression const& _condition,
smt::Expression const& _constraints,
smt::Expression const& _value,
smtutil::Expression const& _constraints,
smtutil::Expression const& _value,
std::vector<CallStackEntry> const& _callStack
);
std::pair<smt::CheckResult, std::vector<std::string>>
checkSatisfiableAndGenerateModel(std::vector<smt::Expression> const& _expressionsToEvaluate);
std::pair<smtutil::CheckResult, std::vector<std::string>>
checkSatisfiableAndGenerateModel(std::vector<smtutil::Expression> const& _expressionsToEvaluate);
smt::CheckResult checkSatisfiable();
smtutil::CheckResult checkSatisfiable();
//@}
std::unique_ptr<smt::SolverInterface> m_interface;
std::unique_ptr<smtutil::SolverInterface> m_interface;
/// Flags used for better warning messages.
bool m_loopExecutionHappened = false;

180
libsolidity/formal/CHC.cpp
View File

@ -17,22 +17,22 @@
#include <libsolidity/formal/CHC.h>
#include <libsolidity/formal/CHCSmtLib2Interface.h>
#ifdef HAVE_Z3
#include <libsolidity/formal/Z3CHCInterface.h>
#include <libsmtutil/Z3CHCInterface.h>
#endif
#include <libsolidity/formal/SymbolicTypes.h>
#include <libsolidity/ast/TypeProvider.h>
#include <libsmtutil/CHCSmtLib2Interface.h>
#include <libsolutil/Algorithms.h>
using namespace std;
using namespace solidity;
using namespace solidity::util;
using namespace solidity::langutil;
using namespace solidity::smtutil;
using namespace solidity::frontend;
CHC::CHC(
@ -40,7 +40,7 @@ CHC::CHC(
ErrorReporter& _errorReporter,
map<util::h256, string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback,
[[maybe_unused]] smt::SMTSolverChoice _enabledSolvers
[[maybe_unused]] smtutil::SMTSolverChoice _enabledSolvers
):
SMTEncoder(_context),
m_outerErrorReporter(_errorReporter),
@ -48,10 +48,10 @@ CHC::CHC(
{
#ifdef HAVE_Z3
if (_enabledSolvers.z3)
m_interface = make_unique<smt::Z3CHCInterface>();
m_interface = make_unique<smtutil::Z3CHCInterface>();
#endif
if (!m_interface)
m_interface = make_unique<smt::CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback);
m_interface = make_unique<smtutil::CHCSmtLib2Interface>(_smtlib2Responses, _smtCallback);
}
void CHC::analyze(SourceUnit const& _source)
@ -63,14 +63,14 @@ void CHC::analyze(SourceUnit const& _source)
usesZ3 = m_enabledSolvers.z3;
if (usesZ3)
{
auto z3Interface = dynamic_cast<smt::Z3CHCInterface const*>(m_interface.get());
auto z3Interface = dynamic_cast<smtutil::Z3CHCInterface const*>(m_interface.get());
solAssert(z3Interface, "");
m_context.setSolver(z3Interface->z3Interface());
}
#endif
if (!usesZ3)
{
auto smtlib2Interface = dynamic_cast<smt::CHCSmtLib2Interface const*>(m_interface.get());
auto smtlib2Interface = dynamic_cast<smtutil::CHCSmtLib2Interface const*>(m_interface.get());
solAssert(smtlib2Interface, "");
m_context.setSolver(smtlib2Interface->smtlib2Interface());
}
@ -80,9 +80,9 @@ void CHC::analyze(SourceUnit const& _source)
resetSourceAnalysis();
auto genesisSort = make_shared<smt::FunctionSort>(
vector<smt::SortPointer>(),
smt::SortProvider::boolSort
auto genesisSort = make_shared<smtutil::FunctionSort>(
vector<smtutil::SortPointer>(),
smtutil::SortProvider::boolSort
);
m_genesisPredicate = createSymbolicBlock(genesisSort, "genesis");
addRule(genesis(), "genesis");
@ -108,7 +108,7 @@ void CHC::analyze(SourceUnit const& _source)
auto [result, model] = query(error(), assertion->location());
// This should be fine but it's a bug in the old compiler
(void)model;
if (result == smt::CheckResult::UNSATISFIABLE)
if (result == smtutil::CheckResult::UNSATISFIABLE)
m_safeAssertions.insert(assertion);
}
}
@ -120,10 +120,10 @@ void CHC::analyze(SourceUnit const& _source)
auto [result, model] = query(error(), scope->location());
// This should be fine but it's a bug in the old compiler
(void)model;
if (result != smt::CheckResult::UNSATISFIABLE)
if (result != smtutil::CheckResult::UNSATISFIABLE)
{
string msg = "Empty array \"pop\" ";
if (result == smt::CheckResult::SATISFIABLE)
if (result == smtutil::CheckResult::SATISFIABLE)
msg += "detected here.";
else
msg += "might happen here.";
@ -142,7 +142,7 @@ void CHC::analyze(SourceUnit const& _source)
vector<string> CHC::unhandledQueries() const
{
if (auto smtlib2 = dynamic_cast<smt::CHCSmtLib2Interface const*>(m_interface.get()))
if (auto smtlib2 = dynamic_cast<smtutil::CHCSmtLib2Interface const*>(m_interface.get()))
return smtlib2->unhandledQueries();
return {};
@ -182,14 +182,14 @@ void CHC::endVisit(ContractDefinition const& _contract)
else
inlineConstructorHierarchy(_contract);
auto summary = predicate(*m_constructorSummaryPredicate, vector<smt::Expression>{m_error.currentValue()} + currentStateVariables());
auto summary = predicate(*m_constructorSummaryPredicate, vector<smtutil::Expression>{m_error.currentValue()} + currentStateVariables());
connectBlocks(m_currentBlock, summary);
clearIndices(m_currentContract, nullptr);
auto stateExprs = vector<smt::Expression>{m_error.currentValue()} + currentStateVariables();
auto stateExprs = vector<smtutil::Expression>{m_error.currentValue()} + currentStateVariables();
setCurrentBlock(*m_constructorSummaryPredicate, &stateExprs);
addAssertVerificationTarget(m_currentContract, m_currentBlock, smt::Expression(true), m_error.currentValue());
addAssertVerificationTarget(m_currentContract, m_currentBlock, smtutil::Expression(true), m_error.currentValue());
connectBlocks(m_currentBlock, interface(), m_error.currentValue() == 0);
SMTEncoder::endVisit(_contract);
@ -265,10 +265,10 @@ void CHC::endVisit(FunctionDefinition const& _function)
{
string suffix = m_currentContract->name() + "_" + to_string(m_currentContract->id());
auto constructorExit = createSymbolicBlock(constructorSort(), "constructor_exit_" + suffix);
connectBlocks(m_currentBlock, predicate(*constructorExit, vector<smt::Expression>{m_error.currentValue()} + currentStateVariables()));
connectBlocks(m_currentBlock, predicate(*constructorExit, vector<smtutil::Expression>{m_error.currentValue()} + currentStateVariables()));
clearIndices(m_currentContract, m_currentFunction);
auto stateExprs = vector<smt::Expression>{m_error.currentValue()} + currentStateVariables();
auto stateExprs = vector<smtutil::Expression>{m_error.currentValue()} + currentStateVariables();
setCurrentBlock(*constructorExit, &stateExprs);
}
else
@ -417,7 +417,7 @@ bool CHC::visit(ForStatement const& _for)
connectBlocks(m_currentBlock, predicate(*loopHeaderBlock));
setCurrentBlock(*loopHeaderBlock);
auto condition = smt::Expression(true);
auto condition = smtutil::Expression(true);
if (auto forCondition = _for.condition())
{
forCondition->accept(*this);
@ -656,7 +656,7 @@ bool CHC::shouldVisit(FunctionDefinition const& _function) const
void CHC::setCurrentBlock(
smt::SymbolicFunctionVariable const& _block,
vector<smt::Expression> const* _arguments
vector<smtutil::Expression> const* _arguments
)
{
if (m_context.solverStackHeigh() > 0)
@ -670,7 +670,7 @@ void CHC::setCurrentBlock(
m_currentBlock = predicate(_block);
}
set<Expression const*, CHC::IdCompare> CHC::transactionAssertions(ASTNode const* _txRoot)
set<frontend::Expression const*, CHC::IdCompare> CHC::transactionAssertions(ASTNode const* _txRoot)
{
set<Expression const*, IdCompare> assertions;
solidity::util::BreadthFirstSearch<ASTNode const*>{{_txRoot}}.run([&](auto const* function, auto&& _addChild) {
@ -690,7 +690,7 @@ vector<VariableDeclaration const*> CHC::stateVariablesIncludingInheritedAndPriva
);
}
vector<smt::SortPointer> CHC::stateSorts(ContractDefinition const& _contract)
vector<smtutil::SortPointer> CHC::stateSorts(ContractDefinition const& _contract)
{
return applyMap(
stateVariablesIncludingInheritedAndPrivate(_contract),
@ -698,35 +698,35 @@ vector<smt::SortPointer> CHC::stateSorts(ContractDefinition const& _contract)
);
}
smt::SortPointer CHC::constructorSort()
smtutil::SortPointer CHC::constructorSort()
{
return make_shared<smt::FunctionSort>(
vector<smt::SortPointer>{smt::SortProvider::intSort} + m_stateSorts,
smt::SortProvider::boolSort
return make_shared<smtutil::FunctionSort>(
vector<smtutil::SortPointer>{smtutil::SortProvider::intSort} + m_stateSorts,
smtutil::SortProvider::boolSort
);
}
smt::SortPointer CHC::interfaceSort()
smtutil::SortPointer CHC::interfaceSort()
{
return make_shared<smt::FunctionSort>(
return make_shared<smtutil::FunctionSort>(
m_stateSorts,
smt::SortProvider::boolSort
smtutil::SortProvider::boolSort
);
}
smt::SortPointer CHC::interfaceSort(ContractDefinition const& _contract)
smtutil::SortPointer CHC::interfaceSort(ContractDefinition const& _contract)
{
return make_shared<smt::FunctionSort>(
return make_shared<smtutil::FunctionSort>(
stateSorts(_contract),
smt::SortProvider::boolSort
smtutil::SortProvider::boolSort
);
}
smt::SortPointer CHC::arity0FunctionSort()
smtutil::SortPointer CHC::arity0FunctionSort()
{
return make_shared<smt::FunctionSort>(
vector<smt::SortPointer>(),
smt::SortProvider::boolSort
return make_shared<smtutil::FunctionSort>(
vector<smtutil::SortPointer>(),
smtutil::SortProvider::boolSort
);
}
@ -741,33 +741,33 @@ smt::SortPointer CHC::arity0FunctionSort()
/// - Current input variables
/// At the beginning of the function these must equal set 1
/// - 1 set of output variables
smt::SortPointer CHC::sort(FunctionDefinition const& _function)
smtutil::SortPointer CHC::sort(FunctionDefinition const& _function)
{
auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
auto inputSorts = applyMap(_function.parameters(), smtSort);
auto outputSorts = applyMap(_function.returnParameters(), smtSort);
return make_shared<smt::FunctionSort>(
vector<smt::SortPointer>{smt::SortProvider::intSort} + m_stateSorts + inputSorts + m_stateSorts + inputSorts + outputSorts,
smt::SortProvider::boolSort
return make_shared<smtutil::FunctionSort>(
vector<smtutil::SortPointer>{smtutil::SortProvider::intSort} + m_stateSorts + inputSorts + m_stateSorts + inputSorts + outputSorts,
smtutil::SortProvider::boolSort
);
}
smt::SortPointer CHC::sort(ASTNode const* _node)
smtutil::SortPointer CHC::sort(ASTNode const* _node)
{
if (auto funDef = dynamic_cast<FunctionDefinition const*>(_node))
return sort(*funDef);
auto fSort = dynamic_pointer_cast<smt::FunctionSort>(sort(*m_currentFunction));
auto fSort = dynamic_pointer_cast<smtutil::FunctionSort>(sort(*m_currentFunction));
solAssert(fSort, "");
auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
return make_shared<smt::FunctionSort>(
return make_shared<smtutil::FunctionSort>(
fSort->domain + applyMap(m_currentFunction->localVariables(), smtSort),
smt::SortProvider::boolSort
smtutil::SortProvider::boolSort
);
}
smt::SortPointer CHC::summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract)
smtutil::SortPointer CHC::summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract)
{
auto stateVariables = stateVariablesIncludingInheritedAndPrivate(_contract);
auto sorts = stateSorts(_contract);
@ -775,13 +775,13 @@ smt::SortPointer CHC::summarySort(FunctionDefinition const& _function, ContractD
auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
auto inputSorts = applyMap(_function.parameters(), smtSort);
auto outputSorts = applyMap(_function.returnParameters(), smtSort);
return make_shared<smt::FunctionSort>(
vector<smt::SortPointer>{smt::SortProvider::intSort} + sorts + inputSorts + sorts + outputSorts,
smt::SortProvider::boolSort
return make_shared<smtutil::FunctionSort>(
vector<smtutil::SortPointer>{smtutil::SortProvider::intSort} + sorts + inputSorts + sorts + outputSorts,
smtutil::SortProvider::boolSort
);
}
unique_ptr<smt::SymbolicFunctionVariable> CHC::createSymbolicBlock(smt::SortPointer _sort, string const& _name)
unique_ptr<smt::SymbolicFunctionVariable> CHC::createSymbolicBlock(smtutil::SortPointer _sort, string const& _name)
{
auto block = make_unique<smt::SymbolicFunctionVariable>(
_sort,
@ -808,7 +808,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
}
}
smt::Expression CHC::interface()
smtutil::Expression CHC::interface()
{
auto paramExprs = applyMap(
m_stateVariables,
@ -817,32 +817,32 @@ smt::Expression CHC::interface()
return (*m_interfaces.at(m_currentContract))(paramExprs);
}
smt::Expression CHC::interface(ContractDefinition const& _contract)
smtutil::Expression CHC::interface(ContractDefinition const& _contract)
{
return (*m_interfaces.at(&_contract))(stateVariablesAtIndex(0, _contract));
}
smt::Expression CHC::error()
smtutil::Expression CHC::error()
{
return (*m_errorPredicate)({});
}
smt::Expression CHC::error(unsigned _idx)
smtutil::Expression CHC::error(unsigned _idx)
{
return m_errorPredicate->functionValueAtIndex(_idx)({});
}
smt::Expression CHC::summary(ContractDefinition const&)
smtutil::Expression CHC::summary(ContractDefinition const&)
{
return (*m_constructorSummaryPredicate)(
vector<smt::Expression>{m_error.currentValue()} +
vector<smtutil::Expression>{m_error.currentValue()} +
currentStateVariables()
);
}
smt::Expression CHC::summary(FunctionDefinition const& _function)
smtutil::Expression CHC::summary(FunctionDefinition const& _function)
{
vector<smt::Expression> args{m_error.currentValue()};
vector<smtutil::Expression> args{m_error.currentValue()};
auto contract = _function.annotation().contract;
args += contract->isLibrary() ? stateVariablesAtIndex(0, *contract) : initialStateVariables();
args += applyMap(_function.parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); });
@ -877,27 +877,27 @@ void CHC::createErrorBlock()
m_interface->registerRelation(m_errorPredicate->currentFunctionValue());
}
void CHC::connectBlocks(smt::Expression const& _from, smt::Expression const& _to, smt::Expression const& _constraints)
void CHC::connectBlocks(smtutil::Expression const& _from, smtutil::Expression const& _to, smtutil::Expression const& _constraints)
{
smt::Expression edge = smt::Expression::implies(
smtutil::Expression edge = smtutil::Expression::implies(
_from && m_context.assertions() && _constraints,
_to
);
addRule(edge, _from.name + "_to_" + _to.name);
}
vector<smt::Expression> CHC::initialStateVariables()
vector<smtutil::Expression> CHC::initialStateVariables()
{
return stateVariablesAtIndex(0);
}
vector<smt::Expression> CHC::stateVariablesAtIndex(int _index)
vector<smtutil::Expression> CHC::stateVariablesAtIndex(int _index)
{
solAssert(m_currentContract, "");
return applyMap(m_stateVariables, [&](auto _var) { return valueAtIndex(*_var, _index); });
}
vector<smt::Expression> CHC::stateVariablesAtIndex(int _index, ContractDefinition const& _contract)
vector<smtutil::Expression> CHC::stateVariablesAtIndex(int _index, ContractDefinition const& _contract)
{
return applyMap(
stateVariablesIncludingInheritedAndPrivate(_contract),
@ -905,23 +905,23 @@ vector<smt::Expression> CHC::stateVariablesAtIndex(int _index, ContractDefinitio
);
}
vector<smt::Expression> CHC::currentStateVariables()
vector<smtutil::Expression> CHC::currentStateVariables()
{
solAssert(m_currentContract, "");
return applyMap(m_stateVariables, [this](auto _var) { return currentValue(*_var); });
}
vector<smt::Expression> CHC::currentFunctionVariables()
vector<smtutil::Expression> CHC::currentFunctionVariables()
{
vector<smt::Expression> initInputExprs;
vector<smt::Expression> mutableInputExprs;
vector<smtutil::Expression> initInputExprs;
vector<smtutil::Expression> mutableInputExprs;
for (auto const& var: m_currentFunction->parameters())
{
initInputExprs.push_back(m_context.variable(*var)->valueAtIndex(0));
mutableInputExprs.push_back(m_context.variable(*var)->currentValue());
}
auto returnExprs = applyMap(m_currentFunction->returnParameters(), [this](auto _var) { return currentValue(*_var); });
return vector<smt::Expression>{m_error.currentValue()} +
return vector<smtutil::Expression>{m_error.currentValue()} +
initialStateVariables() +
initInputExprs +
currentStateVariables() +
@ -929,7 +929,7 @@ vector<smt::Expression> CHC::currentFunctionVariables()
returnExprs;
}
vector<smt::Expression> CHC::currentBlockVariables()
vector<smtutil::Expression> CHC::currentBlockVariables()
{
if (m_currentFunction)
return currentFunctionVariables() + applyMap(m_currentFunction->localVariables(), [this](auto _var) { return currentValue(*_var); });
@ -954,27 +954,27 @@ string CHC::predicateName(ASTNode const* _node, ContractDefinition const* _contr
return prefix + "_" + to_string(_node->id()) + "_" + to_string(contract->id());
}
smt::Expression CHC::predicate(smt::SymbolicFunctionVariable const& _block)
smtutil::Expression CHC::predicate(smt::SymbolicFunctionVariable const& _block)
{
return _block(currentBlockVariables());
}
smt::Expression CHC::predicate(
smtutil::Expression CHC::predicate(
smt::SymbolicFunctionVariable const& _block,
vector<smt::Expression> const& _arguments
vector<smtutil::Expression> const& _arguments
)
{
return _block(_arguments);
}
smt::Expression CHC::predicate(FunctionCall const& _funCall)
smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
{
auto const* function = functionCallToDefinition(_funCall);
if (!function)
return smt::Expression(true);
return smtutil::Expression(true);
m_error.increaseIndex();
vector<smt::Expression> args{m_error.currentValue()};
vector<smtutil::Expression> args{m_error.currentValue()};
auto const* contract = function->annotation().contract;
args += contract->isLibrary() ? stateVariablesAtIndex(0, *contract) : currentStateVariables();
@ -998,28 +998,28 @@ smt::Expression CHC::predicate(FunctionCall const& _funCall)
return (*m_summaries.at(m_currentContract).at(function))(args);
}
void CHC::addRule(smt::Expression const& _rule, string const& _ruleName)
void CHC::addRule(smtutil::Expression const& _rule, string const& _ruleName)
{
m_interface->addRule(_rule, _ruleName);
}
pair<smt::CheckResult, vector<string>> CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _location)
pair<smtutil::CheckResult, vector<string>> CHC::query(smtutil::Expression const& _query, langutil::SourceLocation const& _location)
{
smt::CheckResult result;
smtutil::CheckResult result;
vector<string> values;
tie(result, values) = m_interface->query(_query);
switch (result)
{
case smt::CheckResult::SATISFIABLE:
case smtutil::CheckResult::SATISFIABLE:
break;
case smt::CheckResult::UNSATISFIABLE:
case smtutil::CheckResult::UNSATISFIABLE:
break;
case smt::CheckResult::UNKNOWN:
case smtutil::CheckResult::UNKNOWN:
break;
case smt::CheckResult::CONFLICTING:
case smtutil::CheckResult::CONFLICTING:
m_outerErrorReporter.warning(1988_error, _location, "At least two SMT solvers provided conflicting answers. Results might not be sound.");
break;
case smt::CheckResult::ERROR:
case smtutil::CheckResult::ERROR:
m_outerErrorReporter.warning(1218_error, _location, "Error trying to invoke SMT solver.");
break;
}
@ -1029,26 +1029,26 @@ pair<smt::CheckResult, vector<string>> CHC::query(smt::Expression const& _query,
void CHC::addVerificationTarget(
ASTNode const* _scope,
VerificationTarget::Type _type,
smt::Expression _from,
smt::Expression _constraints,
smt::Expression _errorId
smtutil::Expression _from,
smtutil::Expression _constraints,
smtutil::Expression _errorId
)
{
m_verificationTargets.emplace(_scope, CHCVerificationTarget{{_type, _from, _constraints}, _errorId});
}
void CHC::addAssertVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId)
void CHC::addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId)
{
addVerificationTarget(_scope, VerificationTarget::Type::Assert, _from, _constraints, _errorId);
}
void CHC::addArrayPopVerificationTarget(ASTNode const* _scope, smt::Expression _errorId)
void CHC::addArrayPopVerificationTarget(ASTNode const* _scope, smtutil::Expression _errorId)
{
solAssert(m_currentContract, "");
solAssert(m_currentFunction, "");
if (m_currentFunction->isConstructor())
addVerificationTarget(_scope, VerificationTarget::Type::PopEmptyArray, summary(*m_currentContract), smt::Expression(true), _errorId);
addVerificationTarget(_scope, VerificationTarget::Type::PopEmptyArray, summary(*m_currentContract), smtutil::Expression(true), _errorId);
else
{
auto iface = (*m_interfaces.at(m_currentContract))(initialStateVariables());

80
libsolidity/formal/CHC.h
View File

@ -32,10 +32,10 @@
#include <libsolidity/formal/SMTEncoder.h>
#include <libsolidity/formal/CHCSolverInterface.h>
#include <libsolidity/interface/ReadFile.h>
#include <libsmtutil/CHCSolverInterface.h>
#include <set>
namespace solidity::frontend
@ -49,7 +49,7 @@ public:
langutil::ErrorReporter& _errorReporter,
std::map<util::h256, std::string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback,
smt::SMTSolverChoice _enabledSolvers
smtutil::SMTSolverChoice _enabledSolvers
);
void analyze(SourceUnit const& _sources);
@ -96,43 +96,43 @@ private:
void eraseKnowledge();
void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override;
bool shouldVisit(FunctionDefinition const& _function) const;
void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector<smt::Expression> const* _arguments = nullptr);
void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector<smtutil::Expression> const* _arguments = nullptr);
std::set<Expression const*, IdCompare> transactionAssertions(ASTNode const* _txRoot);
static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract);
//@}
/// Sort helpers.
//@{
static std::vector<smt::SortPointer> stateSorts(ContractDefinition const& _contract);
smt::SortPointer constructorSort();
smt::SortPointer interfaceSort();
static smt::SortPointer interfaceSort(ContractDefinition const& _const);
smt::SortPointer arity0FunctionSort();
smt::SortPointer sort(FunctionDefinition const& _function);
smt::SortPointer sort(ASTNode const* _block);
static std::vector<smtutil::SortPointer> stateSorts(ContractDefinition const& _contract);
smtutil::SortPointer constructorSort();
smtutil::SortPointer interfaceSort();
static smtutil::SortPointer interfaceSort(ContractDefinition const& _const);
smtutil::SortPointer arity0FunctionSort();
smtutil::SortPointer sort(FunctionDefinition const& _function);
smtutil::SortPointer sort(ASTNode const* _block);
/// @returns the sort of a predicate that represents the summary of _function in the scope of _contract.
/// The _contract is also needed because the same function might be in many contracts due to inheritance,
/// where the sort changes because the set of state variables might change.
static smt::SortPointer summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract);
static smtutil::SortPointer summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract);
//@}
/// Predicate helpers.
//@{
/// @returns a new block of given _sort and _name.
std::unique_ptr<smt::SymbolicFunctionVariable> createSymbolicBlock(smt::SortPointer _sort, std::string const& _name);
std::unique_ptr<smt::SymbolicFunctionVariable> createSymbolicBlock(smtutil::SortPointer _sort, std::string const& _name);
/// Creates summary predicates for all functions of all contracts
/// in a given _source.
void defineInterfacesAndSummaries(SourceUnit const& _source);
/// Genesis predicate.
smt::Expression genesis() { return (*m_genesisPredicate)({}); }
smtutil::Expression genesis() { return (*m_genesisPredicate)({}); }
/// Interface predicate over current variables.
smt::Expression interface();
smt::Expression interface(ContractDefinition const& _contract);
smtutil::Expression interface();
smtutil::Expression interface(ContractDefinition const& _contract);
/// Error predicate over current variables.
smt::Expression error();
smt::Expression error(unsigned _idx);
smtutil::Expression error();
smtutil::Expression error(unsigned _idx);
/// Creates a block for the given _node.
std::unique_ptr<smt::SymbolicFunctionVariable> createBlock(ASTNode const* _node, std::string const& _prefix = "");
@ -144,48 +144,48 @@ private:
/// Also registers the predicate.
void createErrorBlock();
void connectBlocks(smt::Expression const& _from, smt::Expression const& _to, smt::Expression const& _constraints = smt::Expression(true));
void connectBlocks(smtutil::Expression const& _from, smtutil::Expression const& _to, smtutil::Expression const& _constraints = smtutil::Expression(true));
/// @returns the symbolic values of the state variables at the beginning
/// of the current transaction.
std::vector<smt::Expression> initialStateVariables();
std::vector<smt::Expression> stateVariablesAtIndex(int _index);
std::vector<smt::Expression> stateVariablesAtIndex(int _index, ContractDefinition const& _contract);
std::vector<smtutil::Expression> initialStateVariables();
std::vector<smtutil::Expression> stateVariablesAtIndex(int _index);
std::vector<smtutil::Expression> stateVariablesAtIndex(int _index, ContractDefinition const& _contract);
/// @returns the current symbolic values of the current state variables.
std::vector<smt::Expression> currentStateVariables();
std::vector<smtutil::Expression> currentStateVariables();
/// @returns the current symbolic values of the current function's
/// input and output parameters.
std::vector<smt::Expression> currentFunctionVariables();
std::vector<smtutil::Expression> currentFunctionVariables();
/// @returns the same as currentFunctionVariables plus
/// local variables.
std::vector<smt::Expression> currentBlockVariables();
std::vector<smtutil::Expression> currentBlockVariables();
/// @returns the predicate name for a given node.
std::string predicateName(ASTNode const* _node, ContractDefinition const* _contract = nullptr);
/// @returns a predicate application over the current scoped variables.
smt::Expression predicate(smt::SymbolicFunctionVariable const& _block);
smtutil::Expression predicate(smt::SymbolicFunctionVariable const& _block);
/// @returns a predicate application over @param _arguments.
smt::Expression predicate(smt::SymbolicFunctionVariable const& _block, std::vector<smt::Expression> const& _arguments);
smtutil::Expression predicate(smt::SymbolicFunctionVariable const& _block, std::vector<smtutil::Expression> const& _arguments);
/// @returns the summary predicate for the called function.
smt::Expression predicate(FunctionCall const& _funCall);
smtutil::Expression predicate(FunctionCall const& _funCall);
/// @returns a predicate that defines a constructor summary.
smt::Expression summary(ContractDefinition const& _contract);
smtutil::Expression summary(ContractDefinition const& _contract);
/// @returns a predicate that defines a function summary.
smt::Expression summary(FunctionDefinition const& _function);
smtutil::Expression summary(FunctionDefinition const& _function);
//@}
/// Solver related.
//@{
/// Adds Horn rule to the solver.
void addRule(smt::Expression const& _rule, std::string const& _ruleName);
void addRule(smtutil::Expression const& _rule, std::string const& _ruleName);
/// @returns <true, empty> if query is unsatisfiable (safe).
/// @returns <false, model> otherwise.
std::pair<smt::CheckResult, std::vector<std::string>> query(smt::Expression const& _query, langutil::SourceLocation const& _location);
std::pair<smtutil::CheckResult, std::vector<std::string>> query(smtutil::Expression const& _query, langutil::SourceLocation const& _location);
void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId);
void addAssertVerificationTarget(ASTNode const* _scope, smt::Expression _from, smt::Expression _constraints, smt::Expression _errorId);
void addArrayPopVerificationTarget(ASTNode const* _scope, smt::Expression _errorId);
void addVerificationTarget(ASTNode const* _scope, VerificationTarget::Type _type, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId);
void addAssertVerificationTarget(ASTNode const* _scope, smtutil::Expression _from, smtutil::Expression _constraints, smtutil::Expression _errorId);
void addArrayPopVerificationTarget(ASTNode const* _scope, smtutil::Expression _errorId);
//@}
/// Misc.
@ -231,7 +231,7 @@ private:
//@{
/// State variables sorts.
/// Used by all predicates.
std::vector<smt::SortPointer> m_stateSorts;
std::vector<smtutil::SortPointer> m_stateSorts;
/// State variables.
/// Used to create all predicates.
std::vector<VariableDeclaration const*> m_stateVariables;
@ -241,7 +241,7 @@ private:
//@{
struct CHCVerificationTarget: VerificationTarget
{
smt::Expression errorId;
smtutil::Expression errorId;
};
std::map<ASTNode const*, CHCVerificationTarget, IdCompare> m_verificationTargets;
@ -261,7 +261,7 @@ private:
std::map<ASTNode const*, std::set<Expression const*>, IdCompare> m_functionAssertions;
/// The current block.
smt::Expression m_currentBlock = smt::Expression(true);
smtutil::Expression m_currentBlock = smtutil::Expression(true);
/// Counter to generate unique block names.
unsigned m_blockCounter = 0;
@ -276,13 +276,13 @@ private:
//@}
/// CHC solver.
std::unique_ptr<smt::CHCSolverInterface> m_interface;
std::unique_ptr<smtutil::CHCSolverInterface> m_interface;
/// ErrorReporter that comes from CompilerStack.
langutil::ErrorReporter& m_outerErrorReporter;
/// SMT solvers that are chosen at runtime.
smt::SMTSolverChoice m_enabledSolvers;
smtutil::SMTSolverChoice m_enabledSolvers;
};
}

8
libsolidity/formal/EncodingContext.cpp
View File

@ -92,7 +92,7 @@ void EncodingContext::resetAllVariables()
resetVariables([&](frontend::VariableDeclaration const&) { return true; });
}
Expression EncodingContext::newValue(frontend::VariableDeclaration const& _decl)
smtutil::Expression EncodingContext::newValue(frontend::VariableDeclaration const& _decl)
{
solAssert(knownVariable(_decl), "");
return m_variables.at(&_decl)->increaseIndex();
@ -179,10 +179,10 @@ bool EncodingContext::knownGlobalSymbol(string const& _var) const
/// Solver.
Expression EncodingContext::assertions()
smtutil::Expression EncodingContext::assertions()
{
if (m_assertions.empty())
return Expression(true);
return smtutil::Expression(true);
return m_assertions.back();
}
@ -201,7 +201,7 @@ void EncodingContext::popSolver()
m_assertions.pop_back();
}
void EncodingContext::addAssertion(Expression const& _expr)
void EncodingContext::addAssertion(smtutil::Expression const& _expr)
{
if (m_assertions.empty())
m_assertions.push_back(_expr);

19
libsolidity/formal/EncodingContext.h
View File

@ -17,10 +17,11 @@
#pragma once
#include <libsolidity/formal/SolverInterface.h>
#include <libsolidity/formal/SymbolicState.h>
#include <libsolidity/formal/SymbolicVariables.h>
#include <libsmtutil/SolverInterface.h>
#include <unordered_map>
#include <set>
@ -45,7 +46,7 @@ public:
/// Sets the current solver used by the current engine for
/// SMT variable declaration.
void setSolver(SolverInterface* _solver)
void setSolver(smtutil::SolverInterface* _solver)
{
solAssert(_solver, "");
m_solver = _solver;
@ -55,7 +56,7 @@ public:
void setAssertionAccumulation(bool _acc) { m_accumulateAssertions = _acc; }
/// Forwards variable creation to the solver.
Expression newVariable(std::string _name, SortPointer _sort)
smtutil::Expression newVariable(std::string _name, smtutil::SortPointer _sort)
{
solAssert(m_solver, "");
return m_solver->newVariable(move(_name), move(_sort));
@ -85,7 +86,7 @@ public:
/// Allocates a new index for the declaration, updates the current
/// index to this value and returns the expression.
Expression newValue(frontend::VariableDeclaration const& _decl);
smtutil::Expression newValue(frontend::VariableDeclaration const& _decl);
/// Sets the value of the declaration to zero.
void setZeroValue(frontend::VariableDeclaration const& _decl);
void setZeroValue(SymbolicVariable& _variable);
@ -125,12 +126,12 @@ public:
/// Solver.
//@{
/// @returns conjunction of all added assertions.
Expression assertions();
smtutil::Expression assertions();
void pushSolver();
void popSolver();
void addAssertion(Expression const& _e);
void addAssertion(smtutil::Expression const& _e);
unsigned solverStackHeigh() { return m_assertions.size(); } const
SolverInterface* solver()
smtutil::SolverInterface* solver()
{
solAssert(m_solver, "");
return m_solver;
@ -159,10 +160,10 @@ private:
/// Solver related.
//@{
/// Solver can be SMT solver or Horn solver in the future.
SolverInterface* m_solver = nullptr;
smtutil::SolverInterface* m_solver = nullptr;
/// Assertion stack.
std::vector<Expression> m_assertions;
std::vector<smtutil::Expression> m_assertions;
/// Whether to conjoin assertions in the assertion stack.
bool m_accumulateAssertions = true;

6
libsolidity/formal/ModelChecker.cpp
View File

@ -27,7 +27,7 @@ ModelChecker::ModelChecker(
ErrorReporter& _errorReporter,
map<h256, string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback,
smt::SMTSolverChoice _enabledSolvers
smtutil::SMTSolverChoice _enabledSolvers
):
m_context(),
m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers),
@ -49,9 +49,9 @@ vector<string> ModelChecker::unhandledQueries()
return m_bmc.unhandledQueries() + m_chc.unhandledQueries();
}
smt::SMTSolverChoice ModelChecker::availableSolvers()
solidity::smtutil::SMTSolverChoice ModelChecker::availableSolvers()
{
smt::SMTSolverChoice available = smt::SMTSolverChoice::None();
smtutil::SMTSolverChoice available = smtutil::SMTSolverChoice::None();
#ifdef HAVE_Z3
available.z3 = true;
#endif

7
libsolidity/formal/ModelChecker.h
View File

@ -25,9 +25,10 @@
#include <libsolidity/formal/BMC.h>
#include <libsolidity/formal/CHC.h>
#include <libsolidity/formal/EncodingContext.h>
#include <libsolidity/formal/SolverInterface.h>
#include <libsolidity/interface/ReadFile.h>
#include <libsmtutil/SolverInterface.h>
#include <liblangutil/ErrorReporter.h>
namespace solidity::langutil
@ -48,7 +49,7 @@ public:
langutil::ErrorReporter& _errorReporter,
std::map<solidity::util::h256, std::string> const& _smtlib2Responses,
ReadCallback::Callback const& _smtCallback = ReadCallback::Callback(),
smt::SMTSolverChoice _enabledSolvers = smt::SMTSolverChoice::All()
smtutil::SMTSolverChoice _enabledSolvers = smtutil::SMTSolverChoice::All()
);
void analyze(SourceUnit const& _sources);
@ -59,7 +60,7 @@ public:
std::vector<std::string> unhandledQueries();
/// @returns SMT solvers that are available via the C++ API.
static smt::SMTSolverChoice availableSolvers();
static smtutil::SMTSolverChoice availableSolvers();
private:
/// Stores the context of the encoding.

116
libsolidity/formal/SMTEncoder.cpp
View File

@ -18,10 +18,11 @@
#include <libsolidity/formal/SMTEncoder.h>
#include <libsolidity/ast/TypeProvider.h>
#include <libsolidity/formal/SMTPortfolio.h>
#include <libsolidity/formal/SymbolicState.h>
#include <libsolidity/formal/SymbolicTypes.h>
#include <libsmtutil/SMTPortfolio.h>
#include <boost/range/adaptors.hpp>
#include <boost/range/adaptor/reversed.hpp>
@ -180,7 +181,7 @@ void SMTEncoder::inlineModifierInvocation(ModifierInvocation const* _invocation,
solAssert(_invocation, "");
_invocation->accept(*this);
vector<smt::Expression> args;
vector<smtutil::Expression> args;
if (auto const* arguments = _invocation->arguments())
{
auto const& modifierParams = _definition->parameters();
@ -366,7 +367,7 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
else
{
auto const& type = _assignment.annotation().type;
vector<smt::Expression> rightArguments;
vector<smtutil::Expression> rightArguments;
if (auto const* tupleTypeRight = dynamic_cast<TupleType const*>(_assignment.rightHandSide().annotation().type))
{
auto symbTupleLeft = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_assignment.leftHandSide()));
@ -640,7 +641,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
auto const& value = args.front();
solAssert(value, "");
smt::Expression thisBalance = m_context.state().balance();
smtutil::Expression thisBalance = m_context.state().balance();
setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), m_context);
m_context.state().transfer(m_context.state().thisAddress(), expr(address), expr(*value));
@ -778,7 +779,7 @@ void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
else
{
auto const& intType = dynamic_cast<IntegerType const&>(*m_context.expression(_funCall)->type());
defineExpr(_funCall, smt::Expression::ite(
defineExpr(_funCall, smtutil::Expression::ite(
expr(*argument) >= smt::minValue(intType) && expr(*argument) <= smt::maxValue(intType),
expr(*argument),
expr(_funCall)
@ -809,9 +810,9 @@ void SMTEncoder::endVisit(Literal const& _literal)
solAssert(_literal.annotation().type, "Expected type for AST node");
Type const& type = *_literal.annotation().type;
if (smt::isNumber(type.category()))
defineExpr(_literal, smt::Expression(type.literalValue(&_literal)));
defineExpr(_literal, smtutil::Expression(type.literalValue(&_literal)));
else if (smt::isBool(type.category()))
defineExpr(_literal, smt::Expression(_literal.token() == Token::TrueLiteral ? true : false));
defineExpr(_literal, smtutil::Expression(_literal.token() == Token::TrueLiteral ? true : false));
else if (smt::isStringLiteral(type.category()))
createExpr(_literal);
else
@ -964,7 +965,7 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
auto arrayVar = dynamic_pointer_cast<smt::SymbolicArrayVariable>(array);
solAssert(arrayVar, "");
defineExpr(_indexAccess, smt::Expression::select(
defineExpr(_indexAccess, smtutil::Expression::select(
arrayVar->elements(),
expr(*_indexAccess.indexExpression())
));
@ -991,7 +992,7 @@ void SMTEncoder::arrayAssignment()
m_arrayAssignmentHappened = true;
}
void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression const& _rightHandSide)
void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide)
{
auto toStore = _rightHandSide;
auto indexAccess = dynamic_cast<IndexAccess const*>(&_expr);
@ -1038,7 +1039,7 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression c
});
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.variable(*varDecl));
smt::Expression store = smt::Expression::store(
smtutil::Expression store = smtutil::Expression::store(
symbArray->elements(),
expr(*indexAccess->indexExpression()),
toStore
@ -1049,7 +1050,7 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression c
m_context.addAssertion(symbArray->length() == oldLength);
// Update the SMT select value after the assignment,
// necessary for sound models.
defineExpr(*indexAccess, smt::Expression::select(
defineExpr(*indexAccess, smtutil::Expression::select(
symbArray->elements(),
expr(*indexAccess->indexExpression())
));
@ -1060,9 +1061,10 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression c
{
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(m_context.expression(*base));
solAssert(symbArray, "");
toStore = smt::Expression::tuple_constructor(
smt::Expression(base->annotation().type),
{smt::Expression::store(symbArray->elements(), expr(*indexAccess->indexExpression()), toStore), symbArray->length()}
auto baseType = base->annotation().type;
toStore = smtutil::Expression::tuple_constructor(
smtutil::Expression(make_shared<smtutil::SortSort>(smt::smtSort(*baseType)), baseType->toString(true)),
{smtutil::Expression::store(symbArray->elements(), expr(*indexAccess->indexExpression()), toStore), symbArray->length()}
);
indexAccess = base;
}
@ -1091,10 +1093,10 @@ void SMTEncoder::arrayPush(FunctionCall const& _funCall)
m_context.addAssertion(oldLength + 1 < (smt::maxValue(*TypeProvider::uint256()) - 1));
auto const& arguments = _funCall.arguments();
smt::Expression element = arguments.empty() ?
smtutil::Expression element = arguments.empty() ?
smt::zeroValue(_funCall.annotation().type) :
expr(*arguments.front());
smt::Expression store = smt::Expression::store(
smtutil::Expression store = smtutil::Expression::store(
symbArray->elements(),
oldLength,
element
@ -1124,7 +1126,7 @@ void SMTEncoder::arrayPop(FunctionCall const& _funCall)
symbArray->increaseIndex();
m_context.addAssertion(symbArray->elements() == oldElements);
auto newLength = smt::Expression::ite(
auto newLength = smtutil::Expression::ite(
oldLength == 0,
smt::maxValue(*TypeProvider::uint256()),
oldLength - 1
@ -1134,7 +1136,7 @@ void SMTEncoder::arrayPop(FunctionCall const& _funCall)
arrayPushPopAssign(memberAccess->expression(), symbArray->currentValue());
}
void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smt::Expression const& _array)
void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression const& _array)
{
if (auto const* id = dynamic_cast<Identifier const*>(&_expr))
{
@ -1175,9 +1177,9 @@ bool SMTEncoder::shortcutRationalNumber(Expression const& _expr)
auto rationalType = dynamic_cast<RationalNumberType const*>(_expr.annotation().type);
solAssert(rationalType, "");
if (rationalType->isNegative())
defineExpr(_expr, smt::Expression(u2s(rationalType->literalValue(nullptr))));
defineExpr(_expr, smtutil::Expression(u2s(rationalType->literalValue(nullptr))));
else
defineExpr(_expr, smt::Expression(rationalType->literalValue(nullptr)));
defineExpr(_expr, smtutil::Expression(rationalType->literalValue(nullptr)));
return true;
}
return false;
@ -1223,10 +1225,10 @@ void SMTEncoder::arithmeticOperation(BinaryOperation const& _op)
);
}
pair<smt::Expression, smt::Expression> SMTEncoder::arithmeticOperation(
pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
Token _op,
smt::Expression const& _left,
smt::Expression const& _right,
smtutil::Expression const& _left,
smtutil::Expression const& _right,
TypePointer const& _commonType,
Expression const&
)
@ -1243,7 +1245,7 @@ pair<smt::Expression, smt::Expression> SMTEncoder::arithmeticOperation(
solAssert(_commonType->category() == Type::Category::Integer, "");
auto const& intType = dynamic_cast<IntegerType const&>(*_commonType);
smt::Expression valueNoMod(
smtutil::Expression valueNoMod(
_op == Token::Add ? _left + _right :
_op == Token::Sub ? _left - _right :
_op == Token::Div ? division(_left, _right, intType) :
@ -1254,11 +1256,11 @@ pair<smt::Expression, smt::Expression> SMTEncoder::arithmeticOperation(
if (_op == Token::Div || _op == Token::Mod)
m_context.addAssertion(_right != 0);
smt::Expression intValueRange = (0 - smt::minValue(intType)) + smt::maxValue(intType) + 1;
auto value = smt::Expression::ite(
smtutil::Expression intValueRange = (0 - smt::minValue(intType)) + smt::maxValue(intType) + 1;
auto value = smtutil::Expression::ite(
valueNoMod > smt::maxValue(intType),
valueNoMod % intValueRange,
smt::Expression::ite(
smtutil::Expression::ite(
valueNoMod < smt::minValue(intType),
valueNoMod % intValueRange,
valueNoMod
@ -1266,7 +1268,7 @@ pair<smt::Expression, smt::Expression> SMTEncoder::arithmeticOperation(
);
if (intType.isSigned())
value = smt::Expression::ite(
value = smtutil::Expression::ite(
value > smt::maxValue(intType),
value - intValueRange,
value
@ -1281,13 +1283,13 @@ void SMTEncoder::compareOperation(BinaryOperation const& _op)
solAssert(commonType, "");
if (smt::isSupportedType(commonType->category()))
{
smt::Expression left(expr(_op.leftExpression(), commonType));
smt::Expression right(expr(_op.rightExpression(), commonType));
smtutil::Expression left(expr(_op.leftExpression(), commonType));
smtutil::Expression right(expr(_op.rightExpression(), commonType));
Token op = _op.getOperator();
shared_ptr<smt::Expression> value;
shared_ptr<smtutil::Expression> value;
if (smt::isNumber(commonType->category()))
{
value = make_shared<smt::Expression>(
value = make_shared<smtutil::Expression>(
op == Token::Equal ? (left == right) :
op == Token::NotEqual ? (left != right) :
op == Token::LessThan ? (left < right) :
@ -1299,7 +1301,7 @@ void SMTEncoder::compareOperation(BinaryOperation const& _op)
else // Bool
{
solUnimplementedAssert(smt::isBool(commonType->category()), "Operation not yet supported");
value = make_shared<smt::Expression>(
value = make_shared<smtutil::Expression>(
op == Token::Equal ? (left == right) :
/*op == Token::NotEqual*/ (left != right)
);
@ -1344,14 +1346,14 @@ void SMTEncoder::booleanOperation(BinaryOperation const& _op)
);
}
smt::Expression SMTEncoder::division(smt::Expression _left, smt::Expression _right, IntegerType const& _type)
smtutil::Expression SMTEncoder::division(smtutil::Expression _left, smtutil::Expression _right, IntegerType const& _type)
{
// Signed division in SMTLIB2 rounds differently for negative division.
if (_type.isSigned())
return (smt::Expression::ite(
return (smtutil::Expression::ite(
_left >= 0,
smt::Expression::ite(_right >= 0, _left / _right, 0 - (_left / (0 - _right))),
smt::Expression::ite(_right >= 0, 0 - ((0 - _left) / _right), (0 - _left) / (0 - _right))
smtutil::Expression::ite(_right >= 0, _left / _right, 0 - (_left / (0 - _right))),
smtutil::Expression::ite(_right >= 0, 0 - ((0 - _left) / _right), (0 - _left) / (0 - _right))
));
else
return _left / _right;
@ -1359,7 +1361,7 @@ smt::Expression SMTEncoder::division(smt::Expression _left, smt::Expression _rig
void SMTEncoder::assignment(
Expression const& _left,
vector<smt::Expression> const& _right,
vector<smtutil::Expression> const& _right,
TypePointer const& _type,
langutil::SourceLocation const& _location
)
@ -1405,7 +1407,7 @@ void SMTEncoder::assignment(
);
}
smt::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment)
smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment)
{
static map<Token, Token> const compoundToArithmetic{
{Token::AssignAdd, Token::Add},
@ -1439,7 +1441,7 @@ void SMTEncoder::assignment(VariableDeclaration const& _variable, Expression con
// TODO else { store each string literal byte into the array }
}
void SMTEncoder::assignment(VariableDeclaration const& _variable, smt::Expression const& _value)
void SMTEncoder::assignment(VariableDeclaration const& _variable, smtutil::Expression const& _value)
{
TypePointer type = _variable.type();
if (type->category() == Type::Category::Mapping)
@ -1447,12 +1449,12 @@ void SMTEncoder::assignment(VariableDeclaration const& _variable, smt::Expressio
m_context.addAssertion(m_context.newValue(_variable) == _value);
}
SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, smt::Expression _condition)
SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, smtutil::Expression _condition)
{
return visitBranch(_statement, &_condition);
}
SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, smt::Expression const* _condition)
SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, smtutil::Expression const* _condition)
{
auto indicesBeforeBranch = copyVariableIndices();
if (_condition)
@ -1465,7 +1467,7 @@ SMTEncoder::VariableIndices SMTEncoder::visitBranch(ASTNode const* _statement, s
return indicesAfterBranch;
}
void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _function, vector<smt::Expression> const& _callArgs)
void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _function, vector<smtutil::Expression> const& _callArgs)
{
auto const& funParams = _function.parameters();
solAssert(funParams.size() == _callArgs.size(), "");
@ -1562,7 +1564,7 @@ TypePointer SMTEncoder::typeWithoutPointer(TypePointer const& _type)
return _type;
}
void SMTEncoder::mergeVariables(set<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse)
void SMTEncoder::mergeVariables(set<VariableDeclaration const*> const& _variables, smtutil::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse)
{
auto cmp = [] (VariableDeclaration const* var1, VariableDeclaration const* var2) {
return var1->id() < var2->id();
@ -1589,7 +1591,7 @@ void SMTEncoder::mergeVariables(set<VariableDeclaration const*> const& _variable
int trueIndex = _indicesEndTrue.at(decl);
int falseIndex = _indicesEndFalse.at(decl);
solAssert(trueIndex != falseIndex, "");
m_context.addAssertion(m_context.newValue(*decl) == smt::Expression::ite(
m_context.addAssertion(m_context.newValue(*decl) == smtutil::Expression::ite(
_condition,
valueAtIndex(*decl, trueIndex),
valueAtIndex(*decl, falseIndex))
@ -1597,13 +1599,13 @@ void SMTEncoder::mergeVariables(set<VariableDeclaration const*> const& _variable
}
}
smt::Expression SMTEncoder::currentValue(VariableDeclaration const& _decl)
smtutil::Expression SMTEncoder::currentValue(VariableDeclaration const& _decl)
{
solAssert(m_context.knownVariable(_decl), "");
return m_context.variable(_decl)->currentValue();
}
smt::Expression SMTEncoder::valueAtIndex(VariableDeclaration const& _decl, int _index)
smtutil::Expression SMTEncoder::valueAtIndex(VariableDeclaration const& _decl, int _index)
{
solAssert(m_context.knownVariable(_decl), "");
return m_context.variable(_decl)->valueAtIndex(_index);
@ -1626,7 +1628,7 @@ bool SMTEncoder::createVariable(VariableDeclaration const& _varDecl)
return true;
}
smt::Expression SMTEncoder::expr(Expression const& _e, TypePointer _targetType)
smtutil::Expression SMTEncoder::expr(Expression const& _e, TypePointer _targetType)
{
if (!m_context.knownExpression(_e))
{
@ -1648,10 +1650,10 @@ void SMTEncoder::createExpr(Expression const& _e)
);
}
void SMTEncoder::defineExpr(Expression const& _e, smt::Expression _value)
void SMTEncoder::defineExpr(Expression const& _e, smtutil::Expression _value)
{
createExpr(_e);
solAssert(_value.sort->kind != smt::Kind::Function, "Equality operator applied to type that is not fully supported");
solAssert(_value.sort->kind != smtutil::Kind::Function, "Equality operator applied to type that is not fully supported");
m_context.addAssertion(expr(_e) == _value);
}
@ -1661,15 +1663,15 @@ void SMTEncoder::popPathCondition()
m_pathConditions.pop_back();
}
void SMTEncoder::pushPathCondition(smt::Expression const& _e)
void SMTEncoder::pushPathCondition(smtutil::Expression const& _e)
{
m_pathConditions.push_back(currentPathConditions() && _e);
}
smt::Expression SMTEncoder::currentPathConditions()
smtutil::Expression SMTEncoder::currentPathConditions()
{
if (m_pathConditions.empty())
return smt::Expression(true);
return smtutil::Expression(true);
return m_pathConditions.back();
}
@ -1697,9 +1699,9 @@ void SMTEncoder::pushCallStack(CallStackEntry _entry)
m_callStack.push_back(_entry);
}
void SMTEncoder::addPathImpliedExpression(smt::Expression const& _e)
void SMTEncoder::addPathImpliedExpression(smtutil::Expression const& _e)
{
m_context.addAssertion(smt::Expression::implies(currentPathConditions(), _e));
m_context.addAssertion(smtutil::Expression::implies(currentPathConditions(), _e));
}
bool SMTEncoder::isRootFunction()
@ -1835,12 +1837,12 @@ void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
defineExpr(_funCall, currentValue(*returnParams.front()));
}
vector<smt::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _funCall)
vector<smtutil::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _funCall)
{
auto const* function = functionCallToDefinition(_funCall);
solAssert(function, "");
vector<smt::Expression> args;
vector<smtutil::Expression> args;
Expression const* calledExpr = &_funCall.expression();
auto const& funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
solAssert(funType, "");

48
libsolidity/formal/SMTEncoder.h
View File

@ -99,10 +99,10 @@ protected:
/// @returns _op(_left, _right) with and without modular arithmetic.
/// Used by the function above, compound assignments and
/// unary increment/decrement.
virtual std::pair<smt::Expression, smt::Expression> arithmeticOperation(
virtual std::pair<smtutil::Expression, smtutil::Expression> arithmeticOperation(
Token _op,
smt::Expression const& _left,
smt::Expression const& _right,
smtutil::Expression const& _left,
smtutil::Expression const& _right,
TypePointer const& _commonType,
Expression const& _expression
);
@ -135,32 +135,32 @@ protected:
/// while aliasing is not supported.
void arrayAssignment();
/// Handles assignment to SMT array index.
void arrayIndexAssignment(Expression const& _expr, smt::Expression const& _rightHandSide);
void arrayIndexAssignment(Expression const& _expr, smtutil::Expression const& _rightHandSide);
void arrayPush(FunctionCall const& _funCall);
void arrayPop(FunctionCall const& _funCall);
void arrayPushPopAssign(Expression const& _expr, smt::Expression const& _array);
void arrayPushPopAssign(Expression const& _expr, smtutil::Expression const& _array);
/// Allows BMC and CHC to create verification targets for popping
/// an empty array.
virtual void makeArrayPopVerificationTarget(FunctionCall const&) {}
/// Division expression in the given type. Requires special treatment because
/// of rounding for signed division.
smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type);
smtutil::Expression division(smtutil::Expression _left, smtutil::Expression _right, IntegerType const& _type);
void assignment(VariableDeclaration const& _variable, Expression const& _value);
/// Handles assignments to variables of different types.
void assignment(VariableDeclaration const& _variable, smt::Expression const& _value);
void assignment(VariableDeclaration const& _variable, smtutil::Expression const& _value);
/// Handles assignments between generic expressions.
/// Will also be used for assignments of tuple components.
void assignment(
Expression const& _left,
std::vector<smt::Expression> const& _right,
std::vector<smtutil::Expression> const& _right,
TypePointer const& _type,
langutil::SourceLocation const& _location
);
/// Computes the right hand side of a compound assignment.
smt::Expression compoundAssignment(Assignment const& _assignment);
smtutil::Expression compoundAssignment(Assignment const& _assignment);
/// Maps a variable to an SSA index.
using VariableIndices = std::unordered_map<VariableDeclaration const*, int>;
@ -168,8 +168,8 @@ protected:
/// Visits the branch given by the statement, pushes and pops the current path conditions.
/// @param _condition if present, asserts that this condition is true within the branch.
/// @returns the variable indices after visiting the branch.
VariableIndices visitBranch(ASTNode const* _statement, smt::Expression const* _condition = nullptr);
VariableIndices visitBranch(ASTNode const* _statement, smt::Expression _condition);
VariableIndices visitBranch(ASTNode const* _statement, smtutil::Expression const* _condition = nullptr);
VariableIndices visitBranch(ASTNode const* _statement, smtutil::Expression _condition);
using CallStackEntry = std::pair<CallableDeclaration const*, ASTNode const*>;
@ -177,7 +177,7 @@ protected:
void initializeStateVariables(ContractDefinition const& _contract);
void createLocalVariables(FunctionDefinition const& _function);
void initializeLocalVariables(FunctionDefinition const& _function);
void initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector<smt::Expression> const& _callArgs);
void initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector<smtutil::Expression> const& _callArgs);
void resetStateVariables();
/// @returns the type without storage pointer information if it has it.
TypePointer typeWithoutPointer(TypePointer const& _type);
@ -185,31 +185,31 @@ protected:
/// Given two different branches and the touched variables,
/// merge the touched variables into after-branch ite variables
/// using the branch condition as guard.
void mergeVariables(std::set<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse);
void mergeVariables(std::set<VariableDeclaration const*> const& _variables, smtutil::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse);
/// Tries to create an uninitialized variable and returns true on success.
bool createVariable(VariableDeclaration const& _varDecl);
/// @returns an expression denoting the value of the variable declared in @a _decl
/// at the current point.
smt::Expression currentValue(VariableDeclaration const& _decl);
smtutil::Expression currentValue(VariableDeclaration const& _decl);
/// @returns an expression denoting the value of the variable declared in @a _decl
/// at the given index. Does not ensure that this index exists.
smt::Expression valueAtIndex(VariableDeclaration const& _decl, int _index);
smtutil::Expression valueAtIndex(VariableDeclaration const& _decl, int _index);
/// Returns the expression corresponding to the AST node.
/// If _targetType is not null apply conversion.
/// Throws if the expression does not exist.
smt::Expression expr(Expression const& _e, TypePointer _targetType = nullptr);
smtutil::Expression expr(Expression const& _e, TypePointer _targetType = nullptr);
/// Creates the expression (value can be arbitrary)
void createExpr(Expression const& _e);
/// Creates the expression and sets its value.
void defineExpr(Expression const& _e, smt::Expression _value);
void defineExpr(Expression const& _e, smtutil::Expression _value);
/// Adds a new path condition
void pushPathCondition(smt::Expression const& _e);
void pushPathCondition(smtutil::Expression const& _e);
/// Remove the last path condition
void popPathCondition();
/// Returns the conjunction of all path conditions or True if empty
smt::Expression currentPathConditions();
smtutil::Expression currentPathConditions();
/// @returns a human-readable call stack. Used for models.
langutil::SecondarySourceLocation callStackMessage(std::vector<CallStackEntry> const& _callStack);
/// Copies and pops the last called node.
@ -217,7 +217,7 @@ protected:
/// Adds (_definition, _node) to the callstack.
void pushCallStack(CallStackEntry _entry);
/// Add to the solver: the given expression implied by the current path conditions
void addPathImpliedExpression(smt::Expression const& _e);
void addPathImpliedExpression(smtutil::Expression const& _e);
/// Copy the SSA indices of m_variables.
VariableIndices copyVariableIndices();
@ -240,7 +240,7 @@ protected:
/// @returns the symbolic arguments for a function call,
/// taking into account bound functions and
/// type conversion.
std::vector<smt::Expression> symbolicArguments(FunctionCall const& _funCall);
std::vector<smtutil::Expression> symbolicArguments(FunctionCall const& _funCall);
/// @returns a note to be added to warnings.
std::string extraComment();
@ -248,8 +248,8 @@ protected:
struct VerificationTarget
{
enum class Type { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert, PopEmptyArray } type;
smt::Expression value;
smt::Expression constraints;
smtutil::Expression value;
smtutil::Expression constraints;
};
smt::VariableUsage m_variableUsage;
@ -261,7 +261,7 @@ protected:
/// These may be direct application of UFs or Array index access.
/// Used to retrieve models.
std::set<Expression const*> m_uninterpretedTerms;
std::vector<smt::Expression> m_pathConditions;
std::vector<smtutil::Expression> m_pathConditions;
/// Local SMTEncoder ErrorReporter.
/// This is necessary to show the "No SMT solver available"
/// warning before the others in case it's needed.

17
libsolidity/formal/SymbolicState.cpp
View File

@ -20,6 +20,7 @@
#include <libsolidity/formal/EncodingContext.h>
using namespace std;
using namespace solidity;
using namespace solidity::frontend::smt;
SymbolicState::SymbolicState(EncodingContext& _context):
@ -35,22 +36,22 @@ void SymbolicState::reset()
// Blockchain
Expression SymbolicState::thisAddress()
smtutil::Expression SymbolicState::thisAddress()
{
return m_thisAddress.currentValue();
}
Expression SymbolicState::balance()
smtutil::Expression SymbolicState::balance()
{
return balance(m_thisAddress.currentValue());
}
Expression SymbolicState::balance(Expression _address)
smtutil::Expression SymbolicState::balance(smtutil::Expression _address)
{
return Expression::select(m_balances.elements(), move(_address));
return smtutil::Expression::select(m_balances.elements(), move(_address));
}
void SymbolicState::transfer(Expression _from, Expression _to, Expression _value)
void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value)
{
unsigned indexBefore = m_balances.index();
addBalance(_from, 0 - _value);
@ -59,7 +60,7 @@ void SymbolicState::transfer(Expression _from, Expression _to, Expression _value
solAssert(indexAfter > indexBefore, "");
m_balances.increaseIndex();
/// Do not apply the transfer operation if _from == _to.
auto newBalances = Expression::ite(
auto newBalances = smtutil::Expression::ite(
move(_from) == move(_to),
m_balances.valueAtIndex(indexBefore),
m_balances.valueAtIndex(indexAfter)
@ -69,9 +70,9 @@ void SymbolicState::transfer(Expression _from, Expression _to, Expression _value
/// Private helpers.
void SymbolicState::addBalance(Expression _address, Expression _value)
void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression _value)
{
auto newBalances = Expression::store(
auto newBalances = smtutil::Expression::store(
m_balances.elements(),
_address,
balance(_address) + move(_value)

17
libsolidity/formal/SymbolicState.h
View File

@ -17,10 +17,11 @@
#pragma once
#include <libsolidity/formal/Sorts.h>
#include <libsolidity/formal/SolverInterface.h>
#include <libsolidity/formal/SymbolicVariables.h>
#include <libsmtutil/Sorts.h>
#include <libsmtutil/SolverInterface.h>
namespace solidity::frontend::smt
{
@ -39,18 +40,18 @@ public:
/// Blockchain.
//@{
/// Value of `this` address.
Expression thisAddress();
smtutil::Expression thisAddress();
/// @returns the symbolic balance of address `this`.
Expression balance();
smtutil::Expression balance();
/// @returns the symbolic balance of an address.
Expression balance(Expression _address);
smtutil::Expression balance(smtutil::Expression _address);
/// Transfer _value from _from to _to.
void transfer(Expression _from, Expression _to, Expression _value);
void transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value);
//@}
private:
/// Adds _value to _account's balance.
void addBalance(Expression _account, Expression _value);
void addBalance(smtutil::Expression _account, smtutil::Expression _value);
EncodingContext& m_context;
@ -62,7 +63,7 @@ private:
/// Symbolic balances.
SymbolicArrayVariable m_balances{
std::make_shared<ArraySort>(SortProvider::intSort, SortProvider::intSort),
std::make_shared<smtutil::ArraySort>(smtutil::SortProvider::intSort, smtutil::SortProvider::intSort),
"balances",
m_context
};

32
libsolidity/formal/SymbolicTypes.cpp
View File

@ -24,6 +24,7 @@
#include <vector>
using namespace std;
using namespace solidity::smtutil;
namespace solidity::frontend::smt
{
@ -334,14 +335,14 @@ bool isStringLiteral(frontend::Type::Category _category)
return _category == frontend::Type::Category::StringLiteral;
}
Expression minValue(frontend::IntegerType const& _type)
smtutil::Expression minValue(frontend::IntegerType const& _type)
{
return Expression(_type.minValue());
return smtutil::Expression(_type.minValue());
}
Expression maxValue(frontend::IntegerType const& _type)
smtutil::Expression maxValue(frontend::IntegerType const& _type)
{
return Expression(_type.maxValue());
return smtutil::Expression(_type.maxValue());
}
void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _context)
@ -349,13 +350,13 @@ void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _c
setSymbolicZeroValue(_variable.currentValue(), _variable.type(), _context);
}
void setSymbolicZeroValue(Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context)
void setSymbolicZeroValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context)
{
solAssert(_type, "");
_context.addAssertion(_expr == zeroValue(_type));
}
Expression zeroValue(frontend::TypePointer const& _type)
smtutil::Expression zeroValue(frontend::TypePointer const& _type)
{
solAssert(_type, "");
if (isSupportedType(_type->category()))
@ -363,28 +364,31 @@ Expression zeroValue(frontend::TypePointer const& _type)
if (isNumber(_type->category()))
return 0;
if (isBool(_type->category()))
return Expression(false);
return smtutil::Expression(false);
if (isArray(_type->category()) || isMapping(_type->category()))
{
auto tupleSort = dynamic_pointer_cast<TupleSort>(smtSort(*_type));
solAssert(tupleSort, "");
auto sortSort = make_shared<SortSort>(tupleSort->components.front());
std::optional<Expression> zeroArray;
std::optional<smtutil::Expression> zeroArray;
auto length = bigint(0);
if (auto arrayType = dynamic_cast<ArrayType const*>(_type))
{
zeroArray = Expression::const_array(Expression(sortSort), zeroValue(arrayType->baseType()));
zeroArray = smtutil::Expression::const_array(smtutil::Expression(sortSort), zeroValue(arrayType->baseType()));
if (!arrayType->isDynamicallySized())
length = bigint(arrayType->length());
}
else if (auto mappingType = dynamic_cast<MappingType const*>(_type))
zeroArray = Expression::const_array(Expression(sortSort), zeroValue(mappingType->valueType()));
zeroArray = smtutil::Expression::const_array(smtutil::Expression(sortSort), zeroValue(mappingType->valueType()));
else
solAssert(false, "");
solAssert(zeroArray, "");
return Expression::tuple_constructor(Expression(_type), vector<Expression>{*zeroArray, length});
return smtutil::Expression::tuple_constructor(
smtutil::Expression(std::make_shared<SortSort>(smtSort(*_type)), _type->toString(true)),
vector<smtutil::Expression>{*zeroArray, length}
);
}
solAssert(false, "");
@ -398,7 +402,7 @@ void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext&
setSymbolicUnknownValue(_variable.currentValue(), _variable.type(), _context);
}
void setSymbolicUnknownValue(Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context)
void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context)
{
solAssert(_type, "");
if (isEnum(_type->category()))
@ -417,7 +421,7 @@ void setSymbolicUnknownValue(Expression _expr, frontend::TypePointer const& _typ
}
}
optional<Expression> symbolicTypeConversion(TypePointer _from, TypePointer _to)
optional<smtutil::Expression> symbolicTypeConversion(TypePointer _from, TypePointer _to)
{
if (_to && _from)
// StringLiterals are encoded as SMT arrays in the generic case,
@ -425,7 +429,7 @@ optional<Expression> symbolicTypeConversion(TypePointer _from, TypePointer _to)
// case they'd need to be encoded as numbers.
if (auto strType = dynamic_cast<StringLiteralType const*>(_from))
if (_to->category() == frontend::Type::Category::FixedBytes)
return smt::Expression(u256(toHex(util::asBytes(strType->value()), util::HexPrefix::Add)));
return smtutil::Expression(u256(toHex(util::asBytes(strType->value()), util::HexPrefix::Add)));
return std::nullopt;
}

22
libsolidity/formal/SymbolicTypes.h
View File

@ -26,14 +26,14 @@ namespace solidity::frontend::smt
{
/// Returns the SMT sort that models the Solidity type _type.
SortPointer smtSort(frontend::Type const& _type);
std::vector<SortPointer> smtSort(std::vector<frontend::TypePointer> const& _types);
smtutil::SortPointer smtSort(frontend::Type const& _type);
std::vector<smtutil::SortPointer> smtSort(std::vector<frontend::TypePointer> const& _types);
/// If _type has type Function, abstract it to Integer.
/// Otherwise return smtSort(_type).
SortPointer smtSortAbstractFunction(frontend::Type const& _type);
std::vector<SortPointer> smtSortAbstractFunction(std::vector<frontend::TypePointer> const& _types);
smtutil::SortPointer smtSortAbstractFunction(frontend::Type const& _type);
std::vector<smtutil::SortPointer> smtSortAbstractFunction(std::vector<frontend::TypePointer> const& _types);
/// Returns the SMT kind that models the Solidity type type category _category.
Kind smtKind(frontend::Type::Category _category);
smtutil::Kind smtKind(frontend::Type::Category _category);
/// Returns true if type is fully supported (declaration and operations).
bool isSupportedType(frontend::Type::Category _category);
@ -61,14 +61,14 @@ bool isStringLiteral(frontend::Type::Category _category);
/// which is true for unsupported types.
std::pair<bool, std::shared_ptr<SymbolicVariable>> newSymbolicVariable(frontend::Type const& _type, std::string const& _uniqueName, EncodingContext& _context);
Expression minValue(frontend::IntegerType const& _type);
Expression maxValue(frontend::IntegerType const& _type);
Expression zeroValue(frontend::TypePointer const& _type);
smtutil::Expression minValue(frontend::IntegerType const& _type);
smtutil::Expression maxValue(frontend::IntegerType const& _type);
smtutil::Expression zeroValue(frontend::TypePointer const& _type);
void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _context);
void setSymbolicZeroValue(Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context);
void setSymbolicZeroValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context);
void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext& _context);
void setSymbolicUnknownValue(Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context);
void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context);
std::optional<Expression> symbolicTypeConversion(TypePointer _from, TypePointer _to);
std::optional<smtutil::Expression> symbolicTypeConversion(TypePointer _from, TypePointer _to);
}

43
libsolidity/formal/SymbolicVariables.cpp
View File

@ -22,6 +22,7 @@
using namespace std;
using namespace solidity;
using namespace solidity::smtutil;
using namespace solidity::frontend;
using namespace solidity::frontend::smt;
@ -55,7 +56,7 @@ SymbolicVariable::SymbolicVariable(
solAssert(m_sort, "");
}
smt::Expression SymbolicVariable::currentValue(frontend::TypePointer const&) const
smtutil::Expression SymbolicVariable::currentValue(frontend::TypePointer const&) const
{
return valueAtIndex(m_ssa->index());
}
@ -65,7 +66,7 @@ string SymbolicVariable::currentName() const
return uniqueSymbol(m_ssa->index());
}
smt::Expression SymbolicVariable::valueAtIndex(int _index) const
smtutil::Expression SymbolicVariable::valueAtIndex(int _index) const
{
return m_context.newVariable(uniqueSymbol(_index), m_sort);
}
@ -80,19 +81,19 @@ string SymbolicVariable::uniqueSymbol(unsigned _index) const
return m_uniqueName + "_" + to_string(_index);
}
smt::Expression SymbolicVariable::resetIndex()
smtutil::Expression SymbolicVariable::resetIndex()
{
m_ssa->resetIndex();
return currentValue();
}
smt::Expression SymbolicVariable::setIndex(unsigned _index)
smtutil::Expression SymbolicVariable::setIndex(unsigned _index)
{
m_ssa->setIndex(_index);
return currentValue();
}
smt::Expression SymbolicVariable::increaseIndex()
smtutil::Expression SymbolicVariable::increaseIndex()
{
++(*m_ssa);
return currentValue();
@ -159,39 +160,39 @@ SymbolicFunctionVariable::SymbolicFunctionVariable(
solAssert(m_sort->kind == Kind::Function, "");
}
smt::Expression SymbolicFunctionVariable::currentValue(frontend::TypePointer const& _targetType) const
smtutil::Expression SymbolicFunctionVariable::currentValue(frontend::TypePointer const& _targetType) const
{
return m_abstract.currentValue(_targetType);
}
smt::Expression SymbolicFunctionVariable::currentFunctionValue() const
smtutil::Expression SymbolicFunctionVariable::currentFunctionValue() const
{
return m_declaration;
}
smt::Expression SymbolicFunctionVariable::valueAtIndex(int _index) const
smtutil::Expression SymbolicFunctionVariable::valueAtIndex(int _index) const
{
return m_abstract.valueAtIndex(_index);
}
smt::Expression SymbolicFunctionVariable::functionValueAtIndex(int _index) const
smtutil::Expression SymbolicFunctionVariable::functionValueAtIndex(int _index) const
{
return SymbolicVariable::valueAtIndex(_index);
}
smt::Expression SymbolicFunctionVariable::resetIndex()
smtutil::Expression SymbolicFunctionVariable::resetIndex()
{
SymbolicVariable::resetIndex();
return m_abstract.resetIndex();
}
smt::Expression SymbolicFunctionVariable::setIndex(unsigned _index)
smtutil::Expression SymbolicFunctionVariable::setIndex(unsigned _index)
{
SymbolicVariable::setIndex(_index);
return m_abstract.setIndex(_index);
}
smt::Expression SymbolicFunctionVariable::increaseIndex()
smtutil::Expression SymbolicFunctionVariable::increaseIndex()
{
++(*m_ssa);
resetDeclaration();
@ -199,7 +200,7 @@ smt::Expression SymbolicFunctionVariable::increaseIndex()
return m_abstract.currentValue();
}
smt::Expression SymbolicFunctionVariable::operator()(vector<smt::Expression> _arguments) const
smtutil::Expression SymbolicFunctionVariable::operator()(vector<smtutil::Expression> _arguments) const
{
return m_declaration(_arguments);
}
@ -246,17 +247,17 @@ vector<SortPointer> const& SymbolicTupleVariable::components()
return tupleSort->components;
}
smt::Expression SymbolicTupleVariable::component(
smtutil::Expression SymbolicTupleVariable::component(
size_t _index,
TypePointer _fromType,
TypePointer _toType
)
{
optional<smt::Expression> conversion = symbolicTypeConversion(_fromType, _toType);
optional<smtutil::Expression> conversion = symbolicTypeConversion(_fromType, _toType);
if (conversion)
return *conversion;
return smt::Expression::tuple_get(currentValue(), _index);
return smtutil::Expression::tuple_get(currentValue(), _index);
}
SymbolicArrayVariable::SymbolicArrayVariable(
@ -294,26 +295,26 @@ SymbolicArrayVariable::SymbolicArrayVariable(
solAssert(m_sort->kind == Kind::Array, "");
}
smt::Expression SymbolicArrayVariable::currentValue(frontend::TypePointer const& _targetType) const
smtutil::Expression SymbolicArrayVariable::currentValue(frontend::TypePointer const& _targetType) const
{
optional<smt::Expression> conversion = symbolicTypeConversion(m_originalType, _targetType);
optional<smtutil::Expression> conversion = symbolicTypeConversion(m_originalType, _targetType);
if (conversion)
return *conversion;
return m_pair.currentValue();
}
smt::Expression SymbolicArrayVariable::valueAtIndex(int _index) const
smtutil::Expression SymbolicArrayVariable::valueAtIndex(int _index) const
{
return m_pair.valueAtIndex(_index);
}
smt::Expression SymbolicArrayVariable::elements()
smtutil::Expression SymbolicArrayVariable::elements()
{
return m_pair.component(0);
}
smt::Expression SymbolicArrayVariable::length()
smtutil::Expression SymbolicArrayVariable::length()
{
return m_pair.component(1);
}

65
libsolidity/formal/SymbolicVariables.h
View File

@ -17,10 +17,11 @@
#pragma once
#include <libsolidity/formal/SolverInterface.h>
#include <libsolidity/formal/SSAVariable.h>
#include <libsolidity/ast/Types.h>
#include <libsolidity/ast/TypeProvider.h>
#include <libsmtutil/SolverInterface.h>
#include <memory>
namespace solidity::frontend::smt
@ -42,7 +43,7 @@ public:
EncodingContext& _context
);
SymbolicVariable(
SortPointer _sort,
smtutil::SortPointer _sort,
std::string _uniqueName,
EncodingContext& _context
);
@ -51,14 +52,14 @@ public:
virtual ~SymbolicVariable() = default;
virtual Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const;
virtual smtutil::Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const;
std::string currentName() const;
virtual Expression valueAtIndex(int _index) const;
virtual smtutil::Expression valueAtIndex(int _index) const;
virtual std::string nameAtIndex(int _index) const;
virtual Expression resetIndex();
virtual Expression setIndex(unsigned _index);
virtual Expression increaseIndex();
virtual Expression operator()(std::vector<Expression> /*_arguments*/) const
virtual smtutil::Expression resetIndex();
virtual smtutil::Expression setIndex(unsigned _index);
virtual smtutil::Expression increaseIndex();
virtual smtutil::Expression operator()(std::vector<smtutil::Expression> /*_arguments*/) const
{
solAssert(false, "Function application to non-function.");
}
@ -66,7 +67,7 @@ public:
unsigned index() const { return m_ssa->index(); }
unsigned& index() { return m_ssa->index(); }
SortPointer const& sort() const { return m_sort; }
smtutil::SortPointer const& sort() const { return m_sort; }
frontend::TypePointer const& type() const { return m_type; }
frontend::TypePointer const& originalType() const { return m_originalType; }
@ -74,7 +75,7 @@ protected:
std::string uniqueSymbol(unsigned _index) const;
/// SMT sort.
SortPointer m_sort;
smtutil::SortPointer m_sort;
/// Solidity type, used for size and range in number types.
frontend::TypePointer m_type;
/// Solidity original type, used for type conversion if necessary.
@ -154,33 +155,33 @@ public:
EncodingContext& _context
);
SymbolicFunctionVariable(
SortPointer _sort,
smtutil::SortPointer _sort,
std::string _uniqueName,
EncodingContext& _context
);
Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
smtutil::Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
// Explicit request the function declaration.
Expression currentFunctionValue() const;
smtutil::Expression currentFunctionValue() const;
Expression valueAtIndex(int _index) const override;
smtutil::Expression valueAtIndex(int _index) const override;
// Explicit request the function declaration.
Expression functionValueAtIndex(int _index) const;
smtutil::Expression functionValueAtIndex(int _index) const;
Expression resetIndex() override;
Expression setIndex(unsigned _index) override;
Expression increaseIndex() override;
smtutil::Expression resetIndex() override;
smtutil::Expression setIndex(unsigned _index) override;
smtutil::Expression increaseIndex() override;
Expression operator()(std::vector<Expression> _arguments) const override;
smtutil::Expression operator()(std::vector<smtutil::Expression> _arguments) const override;
private:
/// Creates a new function declaration.
void resetDeclaration();
/// Stores the current function declaration.
Expression m_declaration;
smtutil::Expression m_declaration;
/// Abstract representation.
SymbolicIntVariable m_abstract{
@ -216,13 +217,13 @@ public:
EncodingContext& _context
);
SymbolicTupleVariable(
SortPointer _sort,
smtutil::SortPointer _sort,
std::string _uniqueName,
EncodingContext& _context
);
std::vector<SortPointer> const& components();
Expression component(
std::vector<smtutil::SortPointer> const& components();
smtutil::Expression component(
size_t _index,
TypePointer _fromType = nullptr,
TypePointer _toType = nullptr
@ -242,22 +243,22 @@ public:
EncodingContext& _context
);
SymbolicArrayVariable(
SortPointer _sort,
smtutil::SortPointer _sort,
std::string _uniqueName,
EncodingContext& _context
);
SymbolicArrayVariable(SymbolicArrayVariable&&) = default;
Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
Expression valueAtIndex(int _index) const override;
Expression resetIndex() override { SymbolicVariable::resetIndex(); return m_pair.resetIndex(); }
Expression setIndex(unsigned _index) override { SymbolicVariable::setIndex(_index); return m_pair.setIndex(_index); }
Expression increaseIndex() override { SymbolicVariable::increaseIndex(); return m_pair.increaseIndex(); }
Expression elements();
Expression length();
smtutil::Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
smtutil::Expression valueAtIndex(int _index) const override;
smtutil::Expression resetIndex() override { SymbolicVariable::resetIndex(); return m_pair.resetIndex(); }
smtutil::Expression setIndex(unsigned _index) override { SymbolicVariable::setIndex(_index); return m_pair.setIndex(_index); }
smtutil::Expression increaseIndex() override { SymbolicVariable::increaseIndex(); return m_pair.increaseIndex(); }
smtutil::Expression elements();
smtutil::Expression length();
SortPointer tupleSort() { return m_pair.sort(); }
smtutil::SortPointer tupleSort() { return m_pair.sort(); }
private:
SymbolicTupleVariable m_pair;

6
libsolidity/interface/CompilerStack.cpp
View File

@ -82,7 +82,7 @@ static int g_compilerStackCounts = 0;
CompilerStack::CompilerStack(ReadCallback::Callback _readFile):
m_readFile{std::move(_readFile)},
m_enabledSMTSolvers{smt::SMTSolverChoice::All()},
m_enabledSMTSolvers{smtutil::SMTSolverChoice::All()},
m_generateIR{false},
m_generateEwasm{false},
m_errorList{},
@ -136,7 +136,7 @@ void CompilerStack::setEVMVersion(langutil::EVMVersion _version)
m_evmVersion = _version;
}
void CompilerStack::setSMTSolverChoice(smt::SMTSolverChoice _enabledSMTSolvers)
void CompilerStack::setSMTSolverChoice(smtutil::SMTSolverChoice _enabledSMTSolvers)
{
if (m_stackState >= ParsingPerformed)
BOOST_THROW_EXCEPTION(CompilerError() << errinfo_comment("Must set enabled SMT solvers before parsing."));
@ -205,7 +205,7 @@ void CompilerStack::reset(bool _keepSettings)
m_remappings.clear();
m_libraries.clear();
m_evmVersion = langutil::EVMVersion();
m_enabledSMTSolvers = smt::SMTSolverChoice::All();
m_enabledSMTSolvers = smtutil::SMTSolverChoice::All();
m_generateIR = false;
m_generateEwasm = false;
m_revertStrings = RevertStrings::Default;

7
libsolidity/interface/CompilerStack.h
View File

@ -27,7 +27,8 @@
#include <libsolidity/interface/OptimiserSettings.h>
#include <libsolidity/interface/Version.h>
#include <libsolidity/interface/DebugSettings.h>
#include <libsolidity/formal/SolverInterface.h>
#include <libsmtutil/SolverInterface.h>
#include <liblangutil/ErrorReporter.h>
#include <liblangutil/EVMVersion.h>
@ -163,7 +164,7 @@ public:
void setEVMVersion(langutil::EVMVersion _version = langutil::EVMVersion{});
/// Set which SMT solvers should be enabled.
void setSMTSolverChoice(smt::SMTSolverChoice _enabledSolvers);
void setSMTSolverChoice(smtutil::SMTSolverChoice _enabledSolvers);
/// Sets the requested contract names by source.
/// If empty, no filtering is performed and every contract
@ -433,7 +434,7 @@ private:
OptimiserSettings m_optimiserSettings;
RevertStrings m_revertStrings = RevertStrings::Default;
langutil::EVMVersion m_evmVersion;
smt::SMTSolverChoice m_enabledSMTSolvers;
smtutil::SMTSolverChoice m_enabledSMTSolvers;
std::map<std::string, std::set<std::string>> m_requestedContractNames;
bool m_generateIR;
bool m_generateEwasm;

11
libsolidity/interface/StandardCompiler.cpp
View File

@ -28,6 +28,7 @@
#include <libyul/optimiser/Suite.h>
#include <liblangutil/SourceReferenceFormatter.h>
#include <libevmasm/Instruction.h>
#include <libsmtutil/Exceptions.h>
#include <libsolutil/JSON.h>
#include <libsolutil/Keccak256.h>
#include <libsolutil/CommonData.h>
@ -921,6 +922,16 @@ Json::Value StandardCompiler::compileSolidity(StandardCompiler::InputsAndSetting
"Yul exception"
));
}
catch (smtutil::SMTLogicError const& _exception)
{
errors.append(formatErrorWithException(
_exception,
false,
"SMTLogicException",
"general",
"SMT logic exception"
));
}
catch (util::Exception const& _exception)
{
errors.append(formatError(

10
solc/CommandLineInterface.cpp
View File

@ -47,6 +47,8 @@
#include <liblangutil/SourceReferenceFormatter.h>
#include <liblangutil/SourceReferenceFormatterHuman.h>
#include <libsmtutil/Exceptions.h>
#include <libsolutil/Common.h>
#include <libsolutil/CommonData.h>
#include <libsolutil/CommonIO.h>
@ -1295,6 +1297,14 @@ bool CommandLineInterface::processInput()
boost::diagnostic_information(_exception);
return false;
}
catch (smtutil::SMTLogicError const& _exception)
{
serr() <<
"SMT logic error during analysis:" <<
endl <<
boost::diagnostic_information(_exception);
return false;
}
catch (Error const& _error)
{
if (_error.type() == Error::Type::DocstringParsingError)

2
test/CMakeLists.txt
View File

@ -188,7 +188,7 @@ add_executable(soltest ${sources}
${libsolidity_util_sources}
${yul_phaser_sources}
)
target_link_libraries(soltest PRIVATE libsolc yul solidity yulInterpreter evmasm solutil Boost::boost Boost::filesystem Boost::program_options Boost::unit_test_framework evmc)
target_link_libraries(soltest PRIVATE libsolc yul solidity smtutil solutil Boost::boost yulInterpreter evmasm Boost::filesystem Boost::program_options Boost::unit_test_framework evmc)
# Special compilation flag for Visual Studio (version 2019 at least affected)

8
test/libsolidity/SMTCheckerTest.cpp
View File

@ -30,13 +30,13 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename, langutil::EVMVersion _ev
{
auto const& choice = m_reader.stringSetting("SMTSolvers", "any");
if (choice == "any")
m_enabledSolvers = smt::SMTSolverChoice::All();
m_enabledSolvers = smtutil::SMTSolverChoice::All();
else if (choice == "z3")
m_enabledSolvers = smt::SMTSolverChoice::Z3();
m_enabledSolvers = smtutil::SMTSolverChoice::Z3();
else if (choice == "cvc4")
m_enabledSolvers = smt::SMTSolverChoice::CVC4();
m_enabledSolvers = smtutil::SMTSolverChoice::CVC4();
else if (choice == "none")
m_enabledSolvers = smt::SMTSolverChoice::None();
m_enabledSolvers = smtutil::SMTSolverChoice::None();
else
BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT solver choice."));

4
test/libsolidity/SMTCheckerTest.h
View File

@ -19,7 +19,7 @@
#include <test/libsolidity/SyntaxTest.h>
#include <libsolidity/formal/SolverInterface.h>
#include <libsmtutil/SolverInterface.h>
#include <string>
@ -41,7 +41,7 @@ protected:
/// This is set via option SMTSolvers in the test.
/// The possible options are `all`, `z3`, `cvc4`, `none`,
/// where if none is given the default used option is `all`.
smt::SMTSolverChoice m_enabledSolvers;
smtutil::SMTSolverChoice m_enabledSolvers;
};
}