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

EncodingContext's solver needs to be set dynamically

Browse Source
This commit is contained in:
Leonardo Alt 2019-07-04 15:27:45 +02:00
parent 035fde2932
commit 01570bbc8c
4 changed files with 20 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
libsolidity/formal/BMC.cpp
View File

@ -49,6 +49,7 @@ void BMC::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner
m_scanner = _scanner; m_scanner = _scanner;
m_context.setSolver(m_interface);
m_context.clear(); m_context.clear();
_source.accept(*this); _source.accept(*this);

9
libsolidity/formal/EncodingContext.cpp
View File

@ -23,9 +23,8 @@ using namespace std;
using namespace dev; using namespace dev;
using namespace dev::solidity::smt; using namespace dev::solidity::smt;
EncodingContext::EncodingContext(std::shared_ptr<SolverInterface> _solver): EncodingContext::EncodingContext():
m_thisAddress(make_unique<SymbolicAddressVariable>("this", *this)), m_thisAddress(make_unique<SymbolicAddressVariable>("this", *this))
m_solver(_solver)
{ {
auto sort = make_shared<ArraySort>( auto sort = make_shared<ArraySort>(
make_shared<Sort>(Kind::Int), make_shared<Sort>(Kind::Int),
@ -214,7 +213,7 @@ void EncodingContext::transfer(Expression _from, Expression _to, Expression _val
m_balances->valueAtIndex(indexBefore), m_balances->valueAtIndex(indexBefore),
m_balances->valueAtIndex(indexAfter) m_balances->valueAtIndex(indexAfter)
); );
m_solver->addAssertion(m_balances->currentValue() == newBalances); addAssertion(m_balances->currentValue() == newBalances);
} }
/// Solver. /// Solver.
@ -256,5 +255,5 @@ void EncodingContext::addBalance(Expression _address, Expression _value)
balance(_address) + move(_value) balance(_address) + move(_value)
); );
m_balances->increaseIndex(); m_balances->increaseIndex();
m_solver->addAssertion(newBalances == m_balances->currentValue()); addAssertion(newBalances == m_balances->currentValue());
} }

16
libsolidity/formal/EncodingContext.h
View File

@ -36,7 +36,7 @@ namespace smt
class EncodingContext class EncodingContext
{ {
public: public:
EncodingContext(std::shared_ptr<SolverInterface> _solver); EncodingContext();
/// Resets the entire context except for symbolic variables which stay /// Resets the entire context except for symbolic variables which stay
/// alive because of state variables and inlined function calls. /// alive because of state variables and inlined function calls.
@ -46,6 +46,14 @@ public:
/// To be used before a model checking engine starts. /// To be used before a model checking engine starts.
void clear(); void clear();
/// Sets the current solver used by the current engine for
/// SMT variable declaration.
void setSolver(std::shared_ptr<SolverInterface> _solver)
{
solAssert(_solver, "");
m_solver = _solver;
}
/// Forwards variable creation to the solver. /// Forwards variable creation to the solver.
Expression newVariable(std::string _name, SortPointer _sort) Expression newVariable(std::string _name, SortPointer _sort)
{ {
@ -133,7 +141,11 @@ public:
void pushSolver(); void pushSolver();
void popSolver(); void popSolver();
void addAssertion(Expression const& _e); void addAssertion(Expression const& _e);
std::shared_ptr<SolverInterface> solver() { return m_solver; } std::shared_ptr<SolverInterface> solver()
{
solAssert(m_solver, "");
return m_solver;
}
//@} //@}
private: private:

2
libsolidity/formal/ModelChecker.cpp
View File

@ -24,7 +24,7 @@ using namespace dev::solidity;
ModelChecker::ModelChecker(ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses): ModelChecker::ModelChecker(ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
m_bmc(m_context, _errorReporter, _smtlib2Responses), m_bmc(m_context, _errorReporter, _smtlib2Responses),
m_context(m_bmc.solver()) m_context()
{ {
} }