diff --git a/Changelog.md b/Changelog.md index 6793285dc..483c4f1d5 100644 --- a/Changelog.md +++ b/Changelog.md @@ -45,6 +45,7 @@ Bugfixes: * SMTChecker: Fix internal error on lvalue unary operators with tuples. * SMTChecker: Fix internal error on tuple assignment. * SMTChecker: Fix internal error on tuples of one element that have tuple type. + * SMTChecker: Fix internal error when using imported code. * SMTChecker: Fix soundness of array ``pop``. * Type Checker: Disallow ``using for`` directive inside interfaces. * Type Checker: Disallow signed literals as exponent in exponentiation operator. diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp index cc30c127b..bc3d1c6d9 100644 --- a/libsmtutil/CHCSmtLib2Interface.cpp +++ b/libsmtutil/CHCSmtLib2Interface.cpp @@ -50,6 +50,7 @@ void CHCSmtLib2Interface::reset() { m_accumulatedOutput.clear(); m_variables.clear(); + m_unhandledQueries.clear(); } void CHCSmtLib2Interface::registerRelation(Expression const& _expr) diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index fb63c4536..39b7ae593 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -43,19 +43,19 @@ using namespace solidity::frontend; CHC::CHC( smt::EncodingContext& _context, ErrorReporter& _errorReporter, - map const& _smtlib2Responses, - ReadCallback::Callback const& _smtCallback, - [[maybe_unused]] smtutil::SMTSolverChoice _enabledSolvers + [[maybe_unused]] map const& _smtlib2Responses, + [[maybe_unused]] ReadCallback::Callback const& _smtCallback, + smtutil::SMTSolverChoice _enabledSolvers ): SMTEncoder(_context), m_outerErrorReporter(_errorReporter), m_enabledSolvers(_enabledSolvers) { -#ifdef HAVE_Z3 - if (_enabledSolvers.z3) - m_interface = make_unique(); + bool usesZ3 = _enabledSolvers.z3; +#ifndef HAVE_Z3 + usesZ3 = false; #endif - if (!m_interface) + if (!usesZ3) m_interface = make_unique(_smtlib2Responses, _smtCallback); } @@ -63,30 +63,8 @@ void CHC::analyze(SourceUnit const& _source) { solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), ""); - bool usesZ3 = false; -#ifdef HAVE_Z3 - usesZ3 = m_enabledSolvers.z3; - if (usesZ3) - { - auto z3Interface = dynamic_cast(m_interface.get()); - solAssert(z3Interface, ""); - m_context.setSolver(z3Interface->z3Interface()); - } -#endif - if (!usesZ3) - { - auto smtlib2Interface = dynamic_cast(m_interface.get()); - solAssert(smtlib2Interface, ""); - m_context.setSolver(smtlib2Interface->smtlib2Interface()); - } - m_context.clear(); - m_context.setAssertionAccumulation(false); - resetSourceAnalysis(); - m_genesisPredicate = createSymbolicBlock(arity0FunctionSort(), "genesis"); - addRule(genesis(), "genesis"); - set sources; sources.insert(&_source); for (auto const& source: _source.referencedSourceUnits(true)) @@ -131,7 +109,7 @@ bool CHC::visit(ContractDefinition const& _contract) void CHC::endVisit(ContractDefinition const& _contract) { auto implicitConstructor = (*m_implicitConstructorPredicate)({}); - connectBlocks(genesis(), implicitConstructor); + addRule(implicitConstructor, implicitConstructor.name); m_currentBlock = implicitConstructor; m_context.addAssertion(m_error.currentValue() == 0); @@ -156,7 +134,7 @@ bool CHC::visit(FunctionDefinition const& _function) { if (!_function.isImplemented()) { - connectBlocks(genesis(), summary(_function)); + addRule(summary(_function), "summary_function_" + to_string(_function.id())); return false; } @@ -184,7 +162,7 @@ bool CHC::visit(FunctionDefinition const& _function) if (_function.isConstructor()) connectBlocks(m_currentBlock, functionPred); else - connectBlocks(genesis(), functionPred); + addRule(functionPred, functionPred.name); m_context.addAssertion(m_error.currentValue() == 0); for (auto const* var: m_stateVariables) @@ -676,6 +654,30 @@ void CHC::resetSourceAnalysis() m_interfaces.clear(); m_nondetInterfaces.clear(); Predicate::reset(); + m_blockCounter = 0; + + bool usesZ3 = false; +#ifdef HAVE_Z3 + usesZ3 = m_enabledSolvers.z3; + if (usesZ3) + { + /// z3::fixedpoint does not have a reset mechanism, so we need to create another. + m_interface.reset(new smtutil::Z3CHCInterface()); + auto z3Interface = dynamic_cast(m_interface.get()); + solAssert(z3Interface, ""); + m_context.setSolver(z3Interface->z3Interface()); + } +#endif + if (!usesZ3) + { + auto smtlib2Interface = dynamic_cast(m_interface.get()); + smtlib2Interface->reset(); + solAssert(smtlib2Interface, ""); + m_context.setSolver(smtlib2Interface->smtlib2Interface()); + } + + m_context.clear(); + m_context.setAssertionAccumulation(false); } void CHC::resetContractAnalysis() @@ -861,27 +863,23 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) { for (auto const& node: _source.nodes()) if (auto const* contract = dynamic_cast(node.get())) + { + string suffix = contract->name() + "_" + to_string(contract->id()); + m_interfaces[contract] = createSymbolicBlock(interfaceSort(*contract), "interface_" + suffix); + m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract), "nondet_interface_" + suffix); + + for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*contract)) + if (!m_context.knownVariable(*var)) + createVariable(*var); + + /// Base nondeterministic interface that allows + /// 0 steps to be taken, used as base for the inductive + /// rule for each function. + auto const& iface = *m_nondetInterfaces.at(contract); + auto state0 = stateVariablesAtIndex(0, *contract); + addRule(iface(state0 + state0), "base_nondet"); + for (auto const* base: contract->annotation().linearizedBaseContracts) - { - for (auto const* var: SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*base)) - if (!m_context.knownVariable(*var)) - createVariable(*var); - - if (!m_interfaces.count(base)) - { - solAssert(!m_nondetInterfaces.count(base), ""); - string suffix = base->name() + "_" + to_string(base->id()); - m_interfaces.emplace(base, createSymbolicBlock(interfaceSort(*base), "interface_" + suffix, base)); - m_nondetInterfaces.emplace(base, createSymbolicBlock(nondetInterfaceSort(*base), "nondet_interface_" + suffix, base)); - - /// Base nondeterministic interface that allows - /// 0 steps to be taken, used as base for the inductive - /// rule for each function. - auto const* iface = m_nondetInterfaces.at(base); - auto state0 = stateVariablesAtIndex(0, *base); - addRule((*iface)(state0 + state0), "base_nondet"); - } - for (auto const* function: base->definedFunctions()) { for (auto var: function->parameters()) @@ -900,13 +898,11 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) !base->isInterface() ) { - auto state1 = stateVariablesAtIndex(1, *base); - auto state2 = stateVariablesAtIndex(2, *base); + auto state1 = stateVariablesAtIndex(1, *contract); + auto state2 = stateVariablesAtIndex(2, *contract); - auto const* iface = m_nondetInterfaces.at(base); - auto state0 = stateVariablesAtIndex(0, *base); - auto nondetPre = (*iface)(state0 + state1); - auto nondetPost = (*iface)(state0 + state2); + auto nondetPre = iface(state0 + state1); + auto nondetPost = iface(state0 + state2); vector args{m_error.currentValue()}; args += state1 + @@ -915,10 +911,10 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }) + applyMap(function->returnParameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }); - connectBlocks(nondetPre, nondetPost, (*m_summaries.at(base).at(function))(args)); + connectBlocks(nondetPre, nondetPost, (*m_summaries.at(contract).at(function))(args)); } - } } + } } smtutil::Expression CHC::interface() @@ -1210,6 +1206,16 @@ void CHC::addVerificationTarget( smtutil::Expression _errorId ) { + solAssert(m_currentContract || m_currentFunction, ""); + SourceUnit const* source = nullptr; + if (m_currentContract) + source = sourceUnitContaining(*m_currentContract); + else + source = sourceUnitContaining(*m_currentFunction); + solAssert(source, ""); + if (!source->annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker)) + return; + m_verificationTargets.emplace(_scope, CHCVerificationTarget{{_type, _from, _constraints}, _errorId}); } @@ -1459,7 +1465,11 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& /// Recurse on the next interface node which represents the previous transaction /// or stop. if (interfaceId) + { + Predicate const* interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).first); + solAssert(interfacePredicate && interfacePredicate->isInterface(), ""); node = *interfaceId; + } else break; } diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index d555f19e7..769c91aa4 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -141,8 +141,6 @@ private: /// in a given _source. void defineInterfacesAndSummaries(SourceUnit const& _source); - /// Genesis predicate. - smtutil::Expression genesis() { return (*m_genesisPredicate)({}); } /// Interface predicate over current variables. smtutil::Expression interface(); smtutil::Expression interface(ContractDefinition const& _contract); @@ -259,9 +257,6 @@ private: /// Predicates. //@{ - /// Genesis predicate. - Predicate const* m_genesisPredicate = nullptr; - /// Implicit constructor predicate. /// Explicit constructors are handled as functions. Predicate const* m_implicitConstructorPredicate = nullptr; @@ -293,9 +288,6 @@ private: "error", m_context }; - - /// Maps predicate names to the ASTNodes they came from. - std::map m_symbolFunction; //@} /// Variables. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index b6bb770af..1cd3264e8 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -133,10 +133,7 @@ bool SMTEncoder::visit(FunctionDefinition const& _function) if (_function.isConstructor()) inlineConstructorHierarchy(dynamic_cast(*_function.scope())); - // Base constructors' parameters should be set by explicit calls, - // but the most derived one needs to be initialized. - if (_function.scope() == m_currentContract) - initializeLocalVariables(_function); + initializeLocalVariables(_function); _function.parameterList().accept(*this); if (_function.returnParameterList()) @@ -2055,6 +2052,14 @@ vector SMTEncoder::stateVariablesIncludingInheritedA return stateVariablesIncludingInheritedAndPrivate(dynamic_cast(*_function.scope())); } +SourceUnit const* SMTEncoder::sourceUnitContaining(Scopable const& _scopable) +{ + for (auto const* s = &_scopable; s; s = dynamic_cast(s->scope())) + if (auto const* source = dynamic_cast(s->scope())) + return source; + solAssert(false, ""); +} + void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall) { FunctionDefinition const* funDef = functionCallToDefinition(_funCall); diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index a87af642f..9bb7b81ce 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -65,6 +65,9 @@ public: static std::vector stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract); static std::vector stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function); + /// @returns the SourceUnit that contains _scopable. + static SourceUnit const* sourceUnitContaining(Scopable const& _scopable); + protected: // TODO: Check that we do not have concurrent reads and writes to a variable, // because the order of expression evaluation is undefined diff --git a/test/externalTests/solc-js/solc-js.sh b/test/externalTests/solc-js/solc-js.sh index 907061f5c..db01a2ae7 100755 --- a/test/externalTests/solc-js/solc-js.sh +++ b/test/externalTests/solc-js/solc-js.sh @@ -48,6 +48,7 @@ function solcjs_test printLog "Copying SMTChecker tests..." cp -Rf "$TEST_DIR"/test/libsolidity/smtCheckerTests test/ + rm -rf test/smtCheckerTests/imports # Update version (needed for some tests) echo "Updating package.json to version $VERSION" diff --git a/test/libsolidity/smtCheckerTests/imports/imported_fail_1.sol b/test/libsolidity/smtCheckerTests/imports/imported_fail_1.sol new file mode 100644 index 000000000..fce98af06 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/imports/imported_fail_1.sol @@ -0,0 +1,25 @@ +==== Source: ==== +import "B.sol"; +pragma experimental SMTChecker; +contract C is B { + function h(uint _x) public view { + assert(_x < x); + } +} +==== Source: A.sol ==== +contract A { + uint x; + function f(uint _x) public { + x = _x; + } +} +==== Source: B.sol ==== +import "A.sol"; +contract B is A { + function g(uint _x) public view { + assert(_x > x); + } +} +// ---- +// Warning 6328: (103-117): Assertion violation happens here. +// Warning 6328: (B.sol:71-85): Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/imports/imported_fail_2.sol b/test/libsolidity/smtCheckerTests/imports/imported_fail_2.sol new file mode 100644 index 000000000..715af1b7c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/imports/imported_fail_2.sol @@ -0,0 +1,27 @@ +==== Source: ==== +import "B.sol"; +pragma experimental SMTChecker; +contract C is B { + function h(uint _x) public view { + assert(_x < x); + } +} +==== Source: A.sol ==== +contract A { + uint x; + function f(uint _x) public { + x = _x; + } +} +==== Source: B.sol ==== +import "A.sol"; +pragma experimental SMTChecker; +contract B is A { + function g(uint _x) public view { + assert(_x > x); + } +} +// ---- +// Warning 6328: (B.sol:103-117): Assertion violation happens here. +// Warning 6328: (103-117): Assertion violation happens here. +// Warning 6328: (B.sol:103-117): Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/imports/imported_fail_3.sol b/test/libsolidity/smtCheckerTests/imports/imported_fail_3.sol new file mode 100644 index 000000000..d4c180451 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/imports/imported_fail_3.sol @@ -0,0 +1,26 @@ +==== Source: ==== +import "A.sol"; +pragma experimental SMTChecker; +contract C is A { + function h(uint _x) public view { + assert(_x < x); + } +} +==== Source: A.sol ==== +contract A { + uint x; + function f(uint _x) public { + x = _x; + } +} +==== Source: B.sol ==== +import "A.sol"; +pragma experimental SMTChecker; +contract B is A { + function g(uint _x) public view { + assert(_x > x); + } +} +// ---- +// Warning 6328: (103-117): Assertion violation happens here. +// Warning 6328: (B.sol:103-117): Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/imports/simple.sol b/test/libsolidity/smtCheckerTests/imports/simple.sol new file mode 100644 index 000000000..5bae07210 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/imports/simple.sol @@ -0,0 +1,6 @@ +==== Source: A.sol ==== +contract A { function f() public {} } +==== Source:==== +import "A.sol"; +pragma experimental SMTChecker; +contract C is A {} diff --git a/test/libsolidity/smtCheckerTests/imports/simple_imported_fail_no_pragma.sol b/test/libsolidity/smtCheckerTests/imports/simple_imported_fail_no_pragma.sol new file mode 100644 index 000000000..415553385 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/imports/simple_imported_fail_no_pragma.sol @@ -0,0 +1,12 @@ +==== Source: ==== +import "A.sol"; +pragma experimental SMTChecker; +contract C is A {} +==== Source: A.sol ==== +contract A { + function f(uint x) public pure { + assert(x > 0); + } +} +// ---- +// Warning 6328: (A.sol:49-62): Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/imports/simple_imported_fail_two_pragmas.sol b/test/libsolidity/smtCheckerTests/imports/simple_imported_fail_two_pragmas.sol new file mode 100644 index 000000000..db650beec --- /dev/null +++ b/test/libsolidity/smtCheckerTests/imports/simple_imported_fail_two_pragmas.sol @@ -0,0 +1,14 @@ +==== Source: ==== +import "A.sol"; +pragma experimental SMTChecker; +contract C is A {} +==== Source: A.sol ==== +pragma experimental SMTChecker; +contract A { + function f(uint x) public pure { + assert(x > 0); + } +} +// ---- +// Warning 6328: (A.sol:81-94): Assertion violation happens here. +// Warning 6328: (A.sol:81-94): Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/shifts/shift_right_uint8.sol b/test/libsolidity/smtCheckerTests/operators/shifts/shift_right_uint8.sol deleted file mode 100644 index 24cc9b023..000000000 --- a/test/libsolidity/smtCheckerTests/operators/shifts/shift_right_uint8.sol +++ /dev/null @@ -1,19 +0,0 @@ -pragma experimental SMTChecker; - -contract C { - function f(uint8 a, uint8 b) internal pure returns (uint256) { - return a >> b; - } - function t() public pure { - assert(f(0x66, 0) == 0x66); - // Fails because the above is true. - assert(f(0x66, 0) == 0x6); - - assert(f(0x66, 8) == 0); - // Fails because the above is true. - assert(f(0x66, 8) == 1); - } -} -// ---- -// Warning 6328: (240-265): Assertion violation happens here. -// Warning 6328: (335-358): Assertion violation happens here.