diff --git a/Changelog.md b/Changelog.md index 79f88b658..516f20b33 100644 --- a/Changelog.md +++ b/Changelog.md @@ -13,6 +13,7 @@ Compiler Features: * SMTChecker: Support low level ``call`` as external calls to unknown code. * SMTChecker: Add constraints to better correlate ``address(this).balance`` and ``msg.value``. * SMTChecker: Support the ``value`` option for external function calls. + * SMTChecker: Support constants via modules. Bugfixes: diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index fdf5db5ca..e0c440919 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -870,21 +870,7 @@ void SMTEncoder::endVisit(Identifier const& _identifier) if (auto decl = identifierToVariable(_identifier)) { if (decl->isConstant()) - { - if (RationalNumberType const* rationalType = isConstant(_identifier)) - { - if (rationalType->isNegative()) - defineExpr(_identifier, smtutil::Expression(u2s(rationalType->literalValue(nullptr)))); - else - defineExpr(_identifier, smtutil::Expression(rationalType->literalValue(nullptr))); - } - else - { - solAssert(decl->value(), ""); - decl->value()->accept(*this); - defineExpr(_identifier, expr(*decl->value(), _identifier.annotation().type)); - } - } + defineExpr(_identifier, constantExpr(_identifier, *decl)); else defineExpr(_identifier, currentValue(*decl)); } @@ -900,6 +886,9 @@ void SMTEncoder::endVisit(Identifier const& _identifier) // Ignore type identifiers else if (dynamic_cast(_identifier.annotation().type)) return; + // Ignore module identifiers + else if (dynamic_cast(_identifier.annotation().type)) + return; // Ignore the builtin abi, it is handled in FunctionCall. // TODO: ignore MagicType in general (abi, block, msg, tx, type) else if (auto magicType = dynamic_cast(_identifier.annotation().type); magicType && magicType->kind() == MagicType::Kind::ABI) @@ -1287,11 +1276,13 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) createExpr(_memberAccess); - auto const& exprType = _memberAccess.expression().annotation().type; + Expression const* memberExpr = innermostTuple(_memberAccess.expression()); + + auto const& exprType = memberExpr->annotation().type; solAssert(exprType, ""); if (exprType->category() == Type::Category::Magic) { - if (auto const* identifier = dynamic_cast(&_memberAccess.expression())) + if (auto const* identifier = dynamic_cast(memberExpr)) { auto const& name = identifier->name(); solAssert(name == "block" || name == "msg" || name == "tx", ""); @@ -1328,14 +1319,14 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) } else if (smt::isNonRecursiveStruct(*exprType)) { - _memberAccess.expression().accept(*this); - auto const& symbStruct = dynamic_pointer_cast(m_context.expression(_memberAccess.expression())); + memberExpr->accept(*this); + auto const& symbStruct = dynamic_pointer_cast(m_context.expression(*memberExpr)); defineExpr(_memberAccess, symbStruct->member(_memberAccess.memberName())); return false; } else if (exprType->category() == Type::Category::TypeType) { - auto const* decl = expressionToDeclaration(_memberAccess.expression()); + auto const* decl = expressionToDeclaration(*memberExpr); if (dynamic_cast(decl)) { auto enumType = dynamic_cast(accessType); @@ -1355,10 +1346,10 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) } else if (exprType->category() == Type::Category::Address) { - _memberAccess.expression().accept(*this); + memberExpr->accept(*this); if (_memberAccess.memberName() == "balance") { - defineExpr(_memberAccess, state().balance(expr(_memberAccess.expression()))); + defineExpr(_memberAccess, state().balance(expr(*memberExpr))); setSymbolicUnknownValue(*m_context.expression(_memberAccess), m_context); m_uninterpretedTerms.insert(&_memberAccess); return false; @@ -1366,10 +1357,10 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) } else if (exprType->category() == Type::Category::Array) { - _memberAccess.expression().accept(*this); + memberExpr->accept(*this); if (_memberAccess.memberName() == "length") { - auto symbArray = dynamic_pointer_cast(m_context.expression(_memberAccess.expression())); + auto symbArray = dynamic_pointer_cast(m_context.expression(*memberExpr)); solAssert(symbArray, ""); defineExpr(_memberAccess, symbArray->length()); m_uninterpretedTerms.insert(&_memberAccess); @@ -1391,6 +1382,15 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) defineExpr(_memberAccess, functionType->externalIdentifier()); return false; } + else if (exprType->category() == Type::Category::Module) + { + if (auto const* var = dynamic_cast(_memberAccess.annotation().referencedDeclaration)) + { + solAssert(var->isConstant(), ""); + defineExpr(_memberAccess, constantExpr(_memberAccess, *var)); + return false; + } + } else m_errorReporter.warning( 7650_error, @@ -3050,6 +3050,24 @@ vector SMTEncoder::symbolicArguments(FunctionCall const& _f return args; } +smtutil::Expression SMTEncoder::constantExpr(Expression const& _expr, VariableDeclaration const& _var) +{ + if (RationalNumberType const* rationalType = isConstant(_expr)) + { + if (rationalType->isNegative()) + return smtutil::Expression(u2s(rationalType->literalValue(nullptr))); + else + return smtutil::Expression(rationalType->literalValue(nullptr)); + } + else + { + solAssert(_var.value(), ""); + _var.value()->accept(*this); + return expr(*_var.value(), _expr.annotation().type); + } + solAssert(false, ""); +} + void SMTEncoder::collectFreeFunctions(set const& _sources) { for (auto source: _sources) diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index a567a0fbf..4852c6831 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -393,6 +393,8 @@ protected: /// type conversion. std::vector symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contextContract); + smtutil::Expression constantExpr(Expression const& _expr, VariableDeclaration const& _var); + /// Traverses all source units available collecting free functions /// and internal library functions in m_freeFunctions. void collectFreeFunctions(std::set const& _sources); diff --git a/test/libsolidity/smtCheckerTests/file_level/file_level_call_via_module.sol b/test/libsolidity/smtCheckerTests/file_level/file_level_call_via_module.sol index 2392db620..9cea98f6b 100644 --- a/test/libsolidity/smtCheckerTests/file_level/file_level_call_via_module.sol +++ b/test/libsolidity/smtCheckerTests/file_level/file_level_call_via_module.sol @@ -18,7 +18,5 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 8364: (b.sol:95-96): Assertion checker does not yet implement type module "a.sol" -// Warning 8364: (b.sol:103-104): Assertion checker does not yet implement type module "a.sol" // Warning 6328: (b.sol:208-222): CHC: Assertion violation happens here.\nCounterexample:\n\na = 7\nb = 3\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call\n a.sol:f(2) -- internal call\n a.sol:f([97, 98, 99]) -- internal call // Warning 6328: (b.sol:274-288): CHC: Assertion violation happens here.\nCounterexample:\n\na = 7\nb = 3\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call\n a.sol:f(2) -- internal call\n a.sol:f([97, 98, 99]) -- internal call diff --git a/test/libsolidity/smtCheckerTests/file_level/import.sol b/test/libsolidity/smtCheckerTests/file_level/import.sol index 536e38fb1..a67ee4eb6 100644 --- a/test/libsolidity/smtCheckerTests/file_level/import.sol +++ b/test/libsolidity/smtCheckerTests/file_level/import.sol @@ -22,6 +22,5 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 8364: (B:115-116): Assertion checker does not yet implement type module "A" // Warning 6328: (B:238-252): CHC: Assertion violation happens here.\nCounterexample:\ndata = {x: 0}\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: data = {x: 0}\nC.g()\n C.f(7) -- internal call\n A:set({x: 0}, 7) -- internal call\n A:set({x: 0}, 8) -- internal call // Warning 6328: (B:308-322): CHC: Assertion violation happens here.\nCounterexample:\ndata = {x: 0}\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: data = {x: 0}\nC.g()\n C.f(7) -- internal call\n A:set({x: 0}, 7) -- internal call\n A:set({x: 0}, 8) -- internal call diff --git a/test/libsolidity/smtCheckerTests/file_level/module_constants_1.sol b/test/libsolidity/smtCheckerTests/file_level/module_constants_1.sol new file mode 100644 index 000000000..5993f5e94 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/file_level/module_constants_1.sol @@ -0,0 +1,26 @@ +==== Source: s1.sol ==== +uint constant a = 89; +==== Source: s2.sol ==== +uint constant a = 88; + +==== Source: s3.sol ==== +import "s1.sol" as M; +import "s2.sol" as N; + +contract C { + function f() internal pure returns (uint, uint) { + return (M.a, N.a); + } + function p() public pure { + (uint x, uint y) = f(); + assert(x == 89); // should hold + assert(x == 88); // should fail + assert(y == 88); // should hold + assert(y == 89); // should fail + } +} +// ==== +// SMTEngine: chc +// ---- +// Warning 6328: (s3.sol:223-238): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 89\ny = 88\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call +// Warning 6328: (s3.sol:291-306): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 89\ny = 88\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call diff --git a/test/libsolidity/smtCheckerTests/file_level/module_constants_functions_1.sol b/test/libsolidity/smtCheckerTests/file_level/module_constants_functions_1.sol new file mode 100644 index 000000000..d3b0e4c6b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/file_level/module_constants_functions_1.sol @@ -0,0 +1,46 @@ +==== Source: s1.sol ==== +uint constant a = 89; + +function fre() pure returns (uint) { + return a; +} + +==== Source: s2.sol ==== +function foo() pure returns (uint) { + return 42; +} + +==== Source: s3.sol ==== +import {fre as foo} from "s1.sol"; +import "s1.sol" as M; +import "s2.sol" as N; + +uint256 constant a = 13; + +contract C { + function f() internal pure returns (uint, uint, uint, uint) { + return (a, foo(), N.foo(), M.a); + } + function p() public pure { + (uint x, uint y, uint z, uint t) = f(); + + assert(x == 13); // should hold + assert(x == 89); // should fail + + assert(y == 89); // should hold + assert(y == 42); // should fail + + assert(z == 42); // should hold + assert(z == 89); // should fail + + assert(t == 89); // should hold + assert(t == 13); // should fail + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (s3.sol:327-342): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 13\ny = 89\nz = 42\nt = 89\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call\n s1.sol:fre() -- internal call\n s2.sol:foo() -- internal call +// Warning 6328: (s3.sol:396-411): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 13\ny = 89\nz = 42\nt = 89\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call\n s1.sol:fre() -- internal call\n s2.sol:foo() -- internal call +// Warning 6328: (s3.sol:465-480): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 13\ny = 89\nz = 42\nt = 89\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call\n s1.sol:fre() -- internal call\n s2.sol:foo() -- internal call +// Warning 6328: (s3.sol:534-549): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 13\ny = 89\nz = 42\nt = 89\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call\n s1.sol:fre() -- internal call\n s2.sol:foo() -- internal call diff --git a/test/libsolidity/smtCheckerTests/file_level/same_constants_different_files.sol b/test/libsolidity/smtCheckerTests/file_level/same_constants_different_files.sol index 1d7760f25..948baf198 100644 --- a/test/libsolidity/smtCheckerTests/file_level/same_constants_different_files.sol +++ b/test/libsolidity/smtCheckerTests/file_level/same_constants_different_files.sol @@ -22,13 +22,10 @@ contract C { (uint x, uint y, uint z, uint t) = f(); assert(x == 13); // should hold assert(y == 89); // should hold - assert(z == 89); // should hold but the SMTChecker does not implement module access + assert(z == 89); // should hold assert(t == 89); // should hold } } // ==== // SMTEngine: all // ---- -// Warning 7650: (s2.sol:182-185): Assertion checker does not yet support this expression. -// Warning 8364: (s2.sol:182-183): Assertion checker does not yet implement type module "s1.sol" -// Warning 6328: (s2.sol:334-349): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 13\ny = 89\nz = 0\nt = 89\n\nTransaction trace:\nC.constructor()\nC.p()\n C.f() -- internal call\n s1.sol:fre() -- internal call diff --git a/test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol b/test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol index 7f109df23..8ddef2da9 100644 --- a/test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol +++ b/test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol @@ -18,7 +18,5 @@ function f(uint _x) pure { // ==== // SMTEngine: all // ---- -// Warning 8364: (A:118-119): Assertion checker does not yet implement type module "s1.sol" -// Warning 8364: (A:145-146): Assertion checker does not yet implement type module "s1.sol" // Warning 6328: (A:50-64): CHC: Assertion violation happens here.\nCounterexample:\n\n_y = 0\n\nTransaction trace:\nD.constructor()\nD.g(0)\n s1.sol:f(200) -- internal call\n s1.sol:f(0) -- internal call\n A:f(10) -- internal call\n A:f(0) -- internal call // Warning 6328: (s1.sol:28-44): CHC: Assertion violation happens here.\nCounterexample:\n\n_y = 0\n\nTransaction trace:\nD.constructor()\nD.g(0)\n s1.sol:f(200) -- internal call\n s1.sol:f(0) -- internal call