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

Merge pull request #7132 from ethereum/smt_acc_solver

Browse Source 
[SMTChecker] EncodingContext config flag to accumulate assertions
This commit is contained in:
chriseth 2019-08-01 13:04:37 +02:00 committed by GitHub
commit 04f298fd0e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 12 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
libsolidity/formal/BMC.cpp
View File

@ -52,6 +52,7 @@ void BMC::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner
m_safeAssertions += move(_safeAssertions); m_safeAssertions += move(_safeAssertions);
m_context.setSolver(m_interface); m_context.setSolver(m_interface);
m_context.clear(); m_context.clear();
m_context.setAssertionAccumulation(true);
m_variableUsage.setFunctionInlining(true); m_variableUsage.setFunctionInlining(true);
_source.accept(*this); _source.accept(*this);

1
libsolidity/formal/CHC.cpp
View File

@ -50,6 +50,7 @@ void CHC::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner
solAssert(z3Interface, ""); solAssert(z3Interface, "");
m_context.setSolver(z3Interface->z3Interface()); m_context.setSolver(z3Interface->z3Interface());
m_context.clear(); m_context.clear();
m_context.setAssertionAccumulation(false);
m_variableUsage.setFunctionInlining(false); m_variableUsage.setFunctionInlining(false);
_source.accept(*this); _source.accept(*this);

5
libsolidity/formal/EncodingContext.cpp
View File

@ -228,7 +228,10 @@ Expression EncodingContext::assertions()
void EncodingContext::pushSolver() void EncodingContext::pushSolver()
{ {
m_assertions.push_back(assertions()); if (m_accumulateAssertions)
m_assertions.push_back(assertions());
else
m_assertions.push_back(smt::Expression(true));
} }
void EncodingContext::popSolver() void EncodingContext::popSolver()

6
libsolidity/formal/EncodingContext.h
View File

@ -54,6 +54,9 @@ public:
m_solver = _solver; m_solver = _solver;
} }
/// Sets whether the context should conjoin assertions in the assertion stack.
void setAssertionAccumulation(bool _acc) { m_accumulateAssertions = _acc; }
/// 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)
{ {
@ -178,6 +181,9 @@ private:
/// Assertion stack. /// Assertion stack.
std::vector<Expression> m_assertions; std::vector<Expression> m_assertions;
/// Whether to conjoin assertions in the assertion stack.
bool m_accumulateAssertions = true;
//@} //@}
}; };