diff --git a/Changelog.md b/Changelog.md index 2acf382ee..97935a9c4 100644 --- a/Changelog.md +++ b/Changelog.md @@ -28,6 +28,7 @@ Bugfixes: * SMTChecker: Fix internal error when using compound bitwise assignment operators inside branches. * SMTChecker: Fix internal error when inlining a function that returns a tuple containing an unsupported type inside a branch. * SMTChecker: Fix internal error when inlining functions that use state variables and belong to a different source. + * SMTChecker: Fix internal error when reporting counterexamples concerning state variables from different source files. * View/Pure Checker: Properly detect state variable access through base class. * Yul analyzer: Check availability of data objects already in analysis phase. * Yul Optimizer: Fix an issue where memory-accessing code was removed even though ``msize`` was used in the program. diff --git a/liblangutil/SourceLocation.h b/liblangutil/SourceLocation.h index cf5308e02..7aafd03da 100644 --- a/liblangutil/SourceLocation.h +++ b/liblangutil/SourceLocation.h @@ -22,7 +22,9 @@ #pragma once +#include #include // defines noexcept macro for MSVC +#include #include #include #include @@ -31,6 +33,7 @@ namespace langutil { +struct SourceLocationError: virtual dev::Exception {}; /** * Representation of an interval of source positions. @@ -49,6 +52,15 @@ struct SourceLocation bool isEmpty() const { return start == -1 && end == -1; } + std::string text() const + { + assertThrow(source, SourceLocationError, "Requested text from null source."); + assertThrow(!isEmpty(), SourceLocationError, "Requested text from empty source location."); + assertThrow(start <= end, SourceLocationError, "Invalid source location."); + assertThrow(end <= int(source->source().length()), SourceLocationError, "Invalid source location."); + return source->source().substr(start, end - start); + } + /// @returns the smallest SourceLocation that contains both @param _a and @param _b. /// Assumes that @param _a and @param _b refer to the same source (exception: if the source of either one /// is unset, the source of the other will be used for the result, even if that is unset as well). diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 8b83e62fe..0fcccdd75 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -43,12 +43,10 @@ BMC::BMC(smt::EncodingContext& _context, ErrorReporter& _errorReporter, map const& _scanner, set _safeAssertions) +void BMC::analyze(SourceUnit const& _source, set _safeAssertions) { solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), ""); - m_scanner = _scanner; - m_safeAssertions += move(_safeAssertions); m_context.setSolver(m_interface); m_context.clear(); @@ -542,7 +540,7 @@ pair, vector> BMC::modelExpressions() if (uf->annotation().type->isValueType()) { expressionsToEvaluate.emplace_back(expr(*uf)); - expressionNames.push_back(m_scanner->sourceAt(uf->location())); + expressionNames.push_back(uf->location().text()); } return {expressionsToEvaluate, expressionNames}; @@ -717,14 +715,11 @@ void BMC::checkCondition( vector expressionNames; tie(expressionsToEvaluate, expressionNames) = _modelExpressions; if (callStack.size()) - { - solAssert(m_scanner, ""); if (_additionalValue) { expressionsToEvaluate.emplace_back(*_additionalValue); expressionNames.push_back(_additionalValueName); } - } smt::CheckResult result; vector values; tie(result, values) = checkSatisfiableAndGenerateModel(expressionsToEvaluate); diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h index 937733574..432050e78 100644 --- a/libsolidity/formal/BMC.h +++ b/libsolidity/formal/BMC.h @@ -34,7 +34,6 @@ #include #include -#include #include #include @@ -56,7 +55,7 @@ class BMC: public SMTEncoder public: BMC(smt::EncodingContext& _context, langutil::ErrorReporter& _errorReporter, std::map const& _smtlib2Responses); - void analyze(SourceUnit const& _sources, std::shared_ptr const& _scanner, std::set _safeAssertions); + void analyze(SourceUnit const& _sources, std::set _safeAssertions); /// This is used if the SMT solver is not directly linked into this binary. /// @returns a list of inputs to the SMT solver that were not part of the argument to diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 337967b62..e12737253 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -39,12 +39,10 @@ CHC::CHC(smt::EncodingContext& _context, ErrorReporter& _errorReporter): { } -void CHC::analyze(SourceUnit const& _source, shared_ptr const& _scanner) +void CHC::analyze(SourceUnit const& _source) { solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), ""); - m_scanner = _scanner; - #ifdef HAVE_Z3 auto z3Interface = dynamic_pointer_cast(m_interface); solAssert(z3Interface, ""); diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index ffbc8cd19..e590f43e2 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -46,7 +46,7 @@ class CHC: public SMTEncoder public: CHC(smt::EncodingContext& _context, langutil::ErrorReporter& _errorReporter); - void analyze(SourceUnit const& _sources, std::shared_ptr const& _scanner); + void analyze(SourceUnit const& _sources); std::set const& safeAssertions() const { return m_safeAssertions; } diff --git a/libsolidity/formal/ModelChecker.cpp b/libsolidity/formal/ModelChecker.cpp index e4b0ba35d..265d0f991 100644 --- a/libsolidity/formal/ModelChecker.cpp +++ b/libsolidity/formal/ModelChecker.cpp @@ -29,13 +29,13 @@ ModelChecker::ModelChecker(ErrorReporter& _errorReporter, map cons { } -void ModelChecker::analyze(SourceUnit const& _source, shared_ptr const& _scanner) +void ModelChecker::analyze(SourceUnit const& _source) { if (!_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker)) return; - m_chc.analyze(_source, _scanner); - m_bmc.analyze(_source, _scanner, m_chc.safeAssertions()); + m_chc.analyze(_source); + m_bmc.analyze(_source, m_chc.safeAssertions()); } vector ModelChecker::unhandledQueries() diff --git a/libsolidity/formal/ModelChecker.h b/libsolidity/formal/ModelChecker.h index f9ad23e5f..349ed76d4 100644 --- a/libsolidity/formal/ModelChecker.h +++ b/libsolidity/formal/ModelChecker.h @@ -28,7 +28,6 @@ #include #include -#include namespace langutil { @@ -46,7 +45,7 @@ class ModelChecker public: ModelChecker(langutil::ErrorReporter& _errorReporter, std::map const& _smtlib2Responses); - void analyze(SourceUnit const& _sources, std::shared_ptr const& _scanner); + void analyze(SourceUnit const& _sources); /// This is used if the SMT solver is not directly linked into this binary. /// @returns a list of inputs to the SMT solver that were not part of the argument to diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 46fdac831..6342ca617 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -30,7 +30,6 @@ #include #include #include -#include #include #include @@ -231,7 +230,6 @@ protected: /// warning before the others in case it's needed. langutil::ErrorReporter m_errorReporter; langutil::ErrorList m_smtErrors; - std::shared_ptr m_scanner; /// Stores the current function/modifier call/invocation path. std::vector m_callStack; diff --git a/libsolidity/interface/CompilerStack.cpp b/libsolidity/interface/CompilerStack.cpp index 3884e13f6..7df52ca23 100644 --- a/libsolidity/interface/CompilerStack.cpp +++ b/libsolidity/interface/CompilerStack.cpp @@ -373,7 +373,7 @@ bool CompilerStack::analyze() { ModelChecker modelChecker(m_errorReporter, m_smtlib2Responses); for (Source const* source: m_sourceOrder) - modelChecker.analyze(*source->ast, source->scanner); + modelChecker.analyze(*source->ast); m_unhandledSMTLib2Queries += modelChecker.unhandledQueries(); } } diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index 99ae85aaf..88a632f7e 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -257,8 +257,11 @@ BOOST_AUTO_TEST_CASE(import_base) pragma solidity >=0.0; contract Base { uint x; - function f() internal { + address a; + function f() internal returns (uint) { + a = address(this); ++x; + return 2; } } )"}, @@ -268,7 +271,7 @@ BOOST_AUTO_TEST_CASE(import_base) import "base"; contract Der is Base { function g(uint y) public { - f(); + x += f(); assert(y > x); } } @@ -328,6 +331,7 @@ BOOST_AUTO_TEST_CASE(import_library) } + BOOST_AUTO_TEST_SUITE_END() }