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

Rename namespace

Browse Source
This commit is contained in:
Leonardo Alt 2020-05-19 14:14:46 +02:00
parent 802d66244d
commit 45eba27424
36 changed files with 444 additions and 441 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
libsmtutil/CHCSmtLib2Interface.cpp
View File

@ -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, "");
solAssert(_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);
@ -125,7 +125,7 @@ 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, "");
solAssert(_sort->kind == Kind::Function, "");
// TODO Use domain and codomain as key as well
if (!m_variables.count(_name))
{

6
libsmtutil/CHCSmtLib2Interface.h
View File

@ -25,7 +25,7 @@
#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;
};
}

2
libsmtutil/CHCSolverInterface.h
View File

@ -23,7 +23,7 @@
#include <libsmtutil/SolverInterface.h>
namespace solidity::frontend::smt
namespace solidity::smtutil
{
class CHCSolverInterface

2
libsmtutil/CVC4Interface.cpp
View File

@ -23,7 +23,7 @@
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)

6
libsmtutil/CVC4Interface.h
View File

@ -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;

12
libsmtutil/SMTLib2Interface.cpp
View File

@ -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,
@ -82,7 +82,7 @@ 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, "");
solAssert(_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;
@ -224,7 +224,7 @@ void SMTLib2Interface::write(string _data)
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())

14
libsmtutil/SMTLib2Interface.h
View File

@ -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;
};
}

16
libsmtutil/SMTPortfolio.cpp
View File

@ -29,22 +29,22 @@ 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
}
@ -73,7 +73,7 @@ void SMTPortfolio::declareVariable(string const& _name, SortPointer const& _sort
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;
@ -142,7 +142,7 @@ 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()), "");
solAssert(dynamic_cast<SMTLib2Interface*>(m_solvers.front().get()), "");
return m_solvers.front()->unhandledQueries();
}

12
libsmtutil/SMTPortfolio.h
View File

@ -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;
};
}

5
libsmtutil/SolverInterface.h
View File

@ -20,7 +20,6 @@
#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>
@ -32,7 +31,7 @@
#include <string>
#include <vector>
namespace solidity::frontend::smt
namespace solidity::smtutil
{
struct SMTSolverChoice
@ -56,7 +55,7 @@ enum class CheckResult
};
// Forward declaration.
SortPointer smtSort(Type const& _type);
SortPointer smtSort(frontend::Type const& _type);
/// C++ representation of an SMTLIB2 expression.
class Expression

2
libsmtutil/Sorts.cpp
View File

@ -20,7 +20,7 @@
using namespace std;
namespace solidity::frontend::smt
namespace solidity::smtutil
{
shared_ptr<Sort> const SortProvider::boolSort{make_shared<Sort>(Kind::Bool)};

2
libsmtutil/Sorts.h
View File

@ -24,7 +24,7 @@
#include <memory>
#include <vector>
namespace solidity::frontend::smt
namespace solidity::smtutil
{
enum class Kind

2
libsmtutil/Z3CHCInterface.cpp
View File

@ -22,7 +22,7 @@
using namespace std;
using namespace solidity;
using namespace solidity::frontend::smt;
using namespace solidity::smtutil;
Z3CHCInterface::Z3CHCInterface():
m_z3Interface(make_unique<Z3Interface>()),

2
libsmtutil/Z3CHCInterface.h
View File

@ -24,7 +24,7 @@
#include <libsmtutil/CHCSolverInterface.h>
#include <libsmtutil/Z3Interface.h>
namespace solidity::frontend::smt
namespace solidity::smtutil
{
class Z3CHCInterface: public CHCSolverInterface

4
libsmtutil/Z3Interface.cpp
View File

@ -21,7 +21,7 @@
#include <libsolutil/CommonIO.h>
using namespace std;
using namespace solidity::frontend::smt;
using namespace solidity::smtutil;
Z3Interface::Z3Interface():
m_solver(m_context)
@ -61,7 +61,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, "");
solAssert(_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));

6
libsmtutil/Z3Interface.h
View File

@ -21,7 +21,7 @@
#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;

90
libsolidity/formal/BMC.cpp
View File

@ -33,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)
@ -133,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();
}
@ -167,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();
}
@ -294,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;
@ -381,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,
@ -453,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));
@ -480,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
)
@ -516,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())
@ -531,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());
@ -550,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)
{
@ -597,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 ||
@ -619,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 ||
@ -689,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
)
{
@ -712,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())
@ -735,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);
@ -756,7 +756,7 @@ void BMC::checkCondition(
switch (result)
{
case smt::CheckResult::SATISFIABLE:
case smtutil::CheckResult::SATISFIABLE:
{
std::ostringstream message;
message << _description << " happens here";
@ -788,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;
}
@ -806,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
)
{
@ -825,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(
@ -862,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)
@ -893,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;
}

40
libsolidity/formal/BMC.h
View File

@ -60,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);
@ -103,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;
@ -114,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.
@ -123,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
);
//@}
@ -145,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;

175
libsolidity/formal/CHC.cpp
View File

@ -32,6 +32,7 @@ using namespace std;
using namespace solidity;
using namespace solidity::util;
using namespace solidity::langutil;
using namespace solidity::smtutil;
using namespace solidity::frontend;
CHC::CHC(
@ -39,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),
@ -47,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)
@ -62,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());
}
@ -79,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");
@ -107,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);
}
}
@ -119,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.";
@ -141,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 {};
@ -181,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);
@ -264,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
@ -416,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);
@ -655,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)
@ -669,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) {
@ -689,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),
@ -697,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
);
}
@ -740,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);
@ -774,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,
@ -807,7 +808,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
}
}
smt::Expression CHC::interface()
smtutil::Expression CHC::interface()
{
auto paramExprs = applyMap(
m_stateVariables,
@ -816,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); });
@ -876,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),
@ -904,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() +
@ -928,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); });
@ -953,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();
@ -997,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;
}
@ -1028,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());

76
libsolidity/formal/CHC.h
View File

@ -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);

16
libsolidity/formal/EncodingContext.h
View File

@ -46,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;
@ -56,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));
@ -86,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);
@ -126,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;
@ -160,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

4
libsolidity/formal/ModelChecker.h
View File

@ -49,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);
@ -60,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.

112
libsolidity/formal/SMTEncoder.cpp
View File

@ -181,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();
@ -367,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()));
@ -641,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));
@ -779,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)
@ -810,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
@ -965,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())
));
@ -992,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);
@ -1039,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
@ -1050,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())
));
@ -1061,9 +1061,9 @@ 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()}
toStore = smtutil::Expression::tuple_constructor(
smtutil::Expression(base->annotation().type),
{smtutil::Expression::store(symbArray->elements(), expr(*indexAccess->indexExpression()), toStore), symbArray->length()}
);
indexAccess = base;
}
@ -1092,10 +1092,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
@ -1125,7 +1125,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
@ -1135,7 +1135,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))
{
@ -1176,9 +1176,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;
@ -1224,10 +1224,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&
)
@ -1244,7 +1244,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) :
@ -1255,11 +1255,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
@ -1267,7 +1267,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
@ -1282,13 +1282,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) :
@ -1300,7 +1300,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)
);
@ -1345,14 +1345,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;
@ -1360,7 +1360,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
)
@ -1406,7 +1406,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},
@ -1440,7 +1440,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)
@ -1448,12 +1448,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)
@ -1466,7 +1466,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(), "");
@ -1563,7 +1563,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();
@ -1590,7 +1590,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))
@ -1598,13 +1598,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);
@ -1627,7 +1627,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))
{
@ -1649,10 +1649,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);
}
@ -1662,15 +1662,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();
}
@ -1698,9 +1698,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()
@ -1836,12 +1836,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)

12
libsolidity/formal/SymbolicState.h
View File

@ -40,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;
@ -63,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
};

29
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,28 @@ 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(_type), vector<smtutil::Expression>{*zeroArray, length});
}
solAssert(false, "");
@ -398,7 +399,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 +418,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 +426,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);
}

62
libsolidity/formal/SymbolicVariables.h
View File

@ -43,7 +43,7 @@ public:
EncodingContext& _context
);
SymbolicVariable(
SortPointer _sort,
smtutil::SortPointer _sort,
std::string _uniqueName,
EncodingContext& _context
);
@ -52,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.");
}
@ -67,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; }
@ -75,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.
@ -155,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{
@ -217,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
@ -243,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;

4
libsolidity/interface/CompilerStack.h
View File

@ -164,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
@ -434,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;

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."));

2
test/libsolidity/SMTCheckerTest.h
View File

@ -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;
};
}