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

Merge pull request #10222 from ethereum/smt_remove_nondet

Browse Source 
[SMTChecker] Decrease nondeterminism
This commit is contained in:
Leonardo 2020-11-06 13:27:29 +00:00 committed by GitHub
commit 6309d78762
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 29 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolidity/formal/CHC.cpp
View File

@ -71,7 +71,7 @@ void CHC::analyze(SourceUnit const& _source)
resetSourceAnalysis();
set<SourceUnit const*, IdCompare> sources;
set<SourceUnit const*, EncodingContext::IdCompare> sources;
sources.insert(&_source);
for (auto const& source: _source.referencedSourceUnits(true))
sources.insert(source);

14
libsolidity/formal/CHC.h
View File

@ -100,14 +100,6 @@ private:
) override;
//@}
struct IdCompare
{
bool operator()(ASTNode const* lhs, ASTNode const* rhs) const
{
return lhs->id() < rhs->id();
}
};
/// Helpers.
//@{
void resetSourceAnalysis();
@ -287,12 +279,12 @@ private:
/// Query placeholders for constructors, if the key has type ContractDefinition*,
/// or external functions, if the key has type FunctionDefinition*.
/// A placeholder is created for each possible context of a function (e.g. multiple contracts in contract inheritance hierarchy).
std::map<ASTNode const*, std::vector<CHCQueryPlaceholder>, IdCompare> m_queryPlaceholders;
std::map<ASTNode const*, std::vector<CHCQueryPlaceholder>, smt::EncodingContext::IdCompare> m_queryPlaceholders;
/// Records verification conditions IDs per function encountered during an analysis of that function.
/// The key is the ASTNode of the function where the verification condition has been encountered,
/// or the ASTNode of the contract if the verification condition happens inside an implicit constructor.
std::map<ASTNode const*, std::vector<unsigned>, IdCompare> m_functionTargetIds;
std::map<ASTNode const*, std::vector<unsigned>, smt::EncodingContext::IdCompare> m_functionTargetIds;
/// Helper mapping unique IDs to actual verification targets.
std::map<unsigned, CHCVerificationTarget> m_verificationTargets;
@ -306,7 +298,7 @@ private:
//@{
FunctionDefinition const* m_currentFunction = nullptr;
std::map<ASTNode const*, std::set<ASTNode const*, IdCompare>, IdCompare> m_callGraph;
std::map<ASTNode const*, std::set<ASTNode const*, smt::EncodingContext::IdCompare>, smt::EncodingContext::IdCompare> m_callGraph;
/// The current block.
smtutil::Expression m_currentBlock = smtutil::Expression(true);

23
libsolidity/formal/EncodingContext.h
View File

@ -23,8 +23,7 @@
#include <libsmtutil/SolverInterface.h>
#include <unordered_map>
#include <set>
#include <map>
namespace solidity::frontend::smt
{
@ -67,12 +66,20 @@ public:
return m_solver->newVariable(move(_name), move(_sort));
}
struct IdCompare
{
bool operator()(ASTNode const* lhs, ASTNode const* rhs) const
{
return lhs->id() < rhs->id();
}
};
/// Variables.
//@{
/// @returns the symbolic representation of a program variable.
std::shared_ptr<SymbolicVariable> variable(frontend::VariableDeclaration const& _varDecl);
/// @returns all symbolic variables.
std::unordered_map<frontend::VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> const& variables() const { return m_variables; }
std::map<frontend::VariableDeclaration const*, std::shared_ptr<SymbolicVariable>, IdCompare> const& variables() const { return m_variables; }
/// Creates a symbolic variable and
/// @returns true if a variable's type is not supported and is therefore abstract.
@ -105,7 +112,7 @@ public:
/// @returns the symbolic representation of an AST node expression.
std::shared_ptr<SymbolicVariable> expression(frontend::Expression const& _e);
/// @returns all symbolic expressions.
std::unordered_map<frontend::Expression const*, std::shared_ptr<SymbolicVariable>> const& expressions() const { return m_expressions; }
std::map<frontend::Expression const*, std::shared_ptr<SymbolicVariable>, IdCompare> const& expressions() const { return m_expressions; }
/// Creates the expression (value can be arbitrary).
/// @returns true if type is not supported.
@ -119,7 +126,7 @@ public:
/// Global variables and functions.
std::shared_ptr<SymbolicVariable> globalSymbol(std::string const& _name);
/// @returns all symbolic globals.
std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> const& globalSymbols() const { return m_globalContext; }
std::map<std::string, std::shared_ptr<SymbolicVariable>> const& globalSymbols() const { return m_globalContext; }
/// Defines a new global variable or function
/// and @returns true if type was abstracted.
@ -149,14 +156,14 @@ private:
/// Symbolic expressions.
//{@
/// Symbolic variables.
std::unordered_map<frontend::VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables;
std::map<frontend::VariableDeclaration const*, std::shared_ptr<SymbolicVariable>, IdCompare> m_variables;
/// Symbolic expressions.
std::unordered_map<frontend::Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions;
std::map<frontend::Expression const*, std::shared_ptr<SymbolicVariable>, IdCompare> m_expressions;
/// Symbolic representation of global symbols including
/// variables and functions.
std::unordered_map<std::string, std::shared_ptr<smt::SymbolicVariable>> m_globalContext;
std::map<std::string, std::shared_ptr<smt::SymbolicVariable>> m_globalContext;
/// Symbolic representation of the blockchain state.
SymbolicState m_state;

18
libsolidity/formal/SMTEncoder.cpp
View File

@ -1804,23 +1804,25 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::divModWithSlacks(
{
IntegerType const* intType = &_type;
string suffix = "div_mod_" + to_string(m_context.newUniqueId());
smt::SymbolicIntVariable d(intType, intType, "d_" + suffix, m_context);
smt::SymbolicIntVariable r(intType, intType, "r_" + suffix, m_context);
smt::SymbolicIntVariable dSymb(intType, intType, "d_" + suffix, m_context);
smt::SymbolicIntVariable rSymb(intType, intType, "r_" + suffix, m_context);
auto d = dSymb.currentValue();
auto r = rSymb.currentValue();
// x / y = d and x % y = r iff d * y + r = x and
// either x >= 0 and 0 <= r < abs(y) (or just 0 <= r < y for unsigned)
// or x < 0 and -abs(y) < r <= 0
m_context.addAssertion(((d.currentValue() * _right) + r.currentValue()) == _left);
m_context.addAssertion(((d * _right) + r) == _left);
if (_type.isSigned())
m_context.addAssertion(
(_left >= 0 && 0 <= r.currentValue() && (_right == 0 || r.currentValue() < smtutil::abs(_right))) ||
(_left < 0 && ((_right == 0 || 0 - smtutil::abs(_right) < r.currentValue()) && r.currentValue() <= 0))
(_left >= 0 && 0 <= r && (_right == 0 || r < smtutil::abs(_right))) ||
(_left < 0 && ((_right == 0 || 0 - smtutil::abs(_right) < r) && r <= 0))
);
else // unsigned version
m_context.addAssertion(0 <= r.currentValue() && (_right == 0 || r.currentValue() < _right));
m_context.addAssertion(0 <= r && (_right == 0 || r < _right));
auto divResult = smtutil::Expression::ite(_right == 0, 0, d.currentValue());
auto modResult = smtutil::Expression::ite(_right == 0, 0, r.currentValue());
auto divResult = smtutil::Expression::ite(_right == 0, 0, d);
auto modResult = smtutil::Expression::ite(_right == 0, 0, r);
return {divResult, modResult};
}