From 095d33714086880ded0f2ce2c7a8e4493e379613 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 7 Apr 2021 18:53:56 +0200 Subject: [PATCH] Basic support to free constants --- libsolidity/formal/BMC.cpp | 3 +- libsolidity/formal/CHC.cpp | 11 ++-- libsolidity/formal/SMTEncoder.cpp | 51 +++++++++---------- libsolidity/formal/SMTEncoder.h | 6 +++ .../file_level/free_constant_1.sol | 3 +- .../file_level/free_constant_2.sol | 8 +-- .../free_function_and_constant_1.sol | 5 +- 7 files changed, 39 insertions(+), 48 deletions(-) diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 8c225975d..27120403a 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -61,8 +61,6 @@ BMC::BMC( void BMC::analyze(SourceUnit const& _source, map> _solvedTargets) { - /// This is currently used to abort analysis of SourceUnits - /// containing file level functions or constants. if (SMTEncoder::analyze(_source)) { m_solvedTargets = move(_solvedTargets); @@ -70,6 +68,7 @@ void BMC::analyze(SourceUnit const& _source, map sources; - sources.insert(&_source); - for (auto const& source: _source.referencedSourceUnits(true)) - sources.insert(source); + auto sources = sourceDependencies(_source); collectFreeFunctions(sources); + createFreeConstants(sources); for (auto const* source: sources) defineInterfacesAndSummaries(*source); for (auto const* source: sources) @@ -1422,7 +1418,8 @@ void CHC::verificationTargetEncountered( if (!m_settings.targets.has(_type)) return; - solAssert(m_currentContract || m_currentFunction, ""); + if (!(m_currentContract || m_currentFunction)) + return; bool scopeIsFunction = m_currentFunction && !m_currentFunction->isConstructor(); auto errorId = newErrorId(); diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 301157233..8204ae98b 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -51,27 +51,6 @@ SMTEncoder::SMTEncoder(smt::EncodingContext& _context): bool SMTEncoder::analyze(SourceUnit const& _source) { - set sources; - sources.insert(&_source); - for (auto const& source: _source.referencedSourceUnits(true)) - sources.insert(source); - - bool analysis = true; - for (auto source: sources) - for (auto node: source->nodes()) - if (auto var = dynamic_pointer_cast(node)) - { - m_errorReporter.warning( - 8195_error, - var->location(), - "Model checker analysis was not possible because file level constants are not supported." - ); - analysis = false; - } - - if (!analysis) - return false; - state().prepareForSourceUnit(_source); return true; @@ -437,14 +416,9 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple) auto values = applyMap(_tuple.components(), [this](auto const& component) -> optional { if (component) { - if (auto varDecl = identifierToVariable(*component)) - return currentValue(*varDecl); - else - { - if (!m_context.knownExpression(*component)) + if (!m_context.knownExpression(*component)) createExpr(*component); - return expr(*component); - } + return expr(*component); } return {}; }); @@ -1395,6 +1369,9 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess) auto varDecl = identifierToVariable(*id); solAssert(varDecl, ""); array = m_context.variable(*varDecl); + + if (varDecl && varDecl->isConstant()) + m_context.addAssertion(currentValue(*varDecl) == expr(*id)); } else { @@ -2599,6 +2576,7 @@ VariableDeclaration const* SMTEncoder::identifierToVariable(Expression const& _e solAssert(m_context.knownVariable(*varDecl), ""); return varDecl; } + return nullptr; } @@ -2913,6 +2891,15 @@ set SMTEncoder::collectABICalls(ASTNode const* _node) return ABIFunctions(_node).abiCalls; } +set SMTEncoder::sourceDependencies(SourceUnit const& _source) +{ + set sources; + sources.insert(&_source); + for (auto const& source: _source.referencedSourceUnits(true)) + sources.insert(source); + return sources; +} + void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall, ContractDefinition const* _contextContract) { auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), _contextContract); @@ -2978,6 +2965,14 @@ void SMTEncoder::collectFreeFunctions(set const& _sources) +{ + for (auto source: _sources) + for (auto node: source->nodes()) + if (auto var = dynamic_cast(node.get())) + createVariable(*var); +} + smt::SymbolicState& SMTEncoder::state() { return m_context.state(); diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 0bdd0a679..45cdc80c2 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -112,6 +112,10 @@ public: static std::set collectABICalls(ASTNode const* _node); + /// @returns all the sources that @param _source depends on, + /// including itself. + static std::set sourceDependencies(SourceUnit const& _source); + protected: // TODO: Check that we do not have concurrent reads and writes to a variable, // because the order of expression evaluation is undefined @@ -373,6 +377,8 @@ protected: /// and internal library functions in m_freeFunctions. void collectFreeFunctions(std::set const& _sources); std::set const& allFreeFunctions() const { return m_freeFunctions; } + /// Create symbolic variables for the free constants in all @param _sources. + void createFreeConstants(std::set const& _sources); /// @returns a note to be added to warnings. std::string extraComment(); diff --git a/test/libsolidity/smtCheckerTests/file_level/free_constant_1.sol b/test/libsolidity/smtCheckerTests/file_level/free_constant_1.sol index 243d112da..11c4428b0 100644 --- a/test/libsolidity/smtCheckerTests/file_level/free_constant_1.sol +++ b/test/libsolidity/smtCheckerTests/file_level/free_constant_1.sol @@ -7,5 +7,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 8195: (0-20): Model checker analysis was not possible because file level constants are not supported. -// Warning 8195: (0-20): Model checker analysis was not possible because file level constants are not supported. +// Warning 4984: (125-130): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639894\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(115792089237316195423570985008687907853269984665640564039457584007913129639894) diff --git a/test/libsolidity/smtCheckerTests/file_level/free_constant_2.sol b/test/libsolidity/smtCheckerTests/file_level/free_constant_2.sol index 9f60fb374..1e937c303 100644 --- a/test/libsolidity/smtCheckerTests/file_level/free_constant_2.sol +++ b/test/libsolidity/smtCheckerTests/file_level/free_constant_2.sol @@ -10,10 +10,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 2018: (188-278): Function state mutability can be restricted to pure -// Warning 8195: (0-23): Model checker analysis was not possible because file level constants are not supported. -// Warning 8195: (79-133): Model checker analysis was not possible because file level constants are not supported. -// Warning 8195: (135-172): Model checker analysis was not possible because file level constants are not supported. -// Warning 8195: (0-23): Model checker analysis was not possible because file level constants are not supported. -// Warning 8195: (79-133): Model checker analysis was not possible because file level constants are not supported. -// Warning 8195: (135-172): Model checker analysis was not possible because file level constants are not supported. +// Warning 2018: (220-310): Function state mutability can be restricted to pure diff --git a/test/libsolidity/smtCheckerTests/file_level/free_function_and_constant_1.sol b/test/libsolidity/smtCheckerTests/file_level/free_function_and_constant_1.sol index 7c4f1099f..2ac197bbe 100644 --- a/test/libsolidity/smtCheckerTests/file_level/free_function_and_constant_1.sol +++ b/test/libsolidity/smtCheckerTests/file_level/free_function_and_constant_1.sol @@ -12,5 +12,6 @@ function fun(uint[] calldata _x, uint[] storage _y) view returns (uint, uint[] // ==== // SMTEngine: all // ---- -// Warning 8195: (32-52): Model checker analysis was not possible because file level constants are not supported. -// Warning 8195: (32-52): Model checker analysis was not possible because file level constants are not supported. +// Warning 4984: (222-234): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\ndata = []\nx = 1\n = 0\n = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(1, input)\n ::fun(_x, []) -- internal call +// Warning 4984: (222-238): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\ndata = []\nx = 115792089237316195423570985008687907853269984665640564039457584007913129632175\n = 0\n = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(115792089237316195423570985008687907853269984665640564039457584007913129632175, input)\n ::fun(_x, []) -- internal call +// Warning 6368: (347-352): CHC: Out of bounds access happens here.\nCounterexample:\ndata = []\nx = 0\ninput = [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 14, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5]\n = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(0, [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 14, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5])\n ::fun([5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 14, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5], []) -- internal call