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 #11945 from ethereum/smt_modules

Browse Source 
[SMTChecker] Support constants via modules
This commit is contained in:
chriseth 2021-09-16 15:18:15 +02:00 committed by GitHub
commit 9d29b1ed9c
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
9 changed files with 118 additions and 33 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -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:

66
libsolidity/formal/SMTEncoder.cpp
View File

@ -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<TypeType const*>(_identifier.annotation().type))
return;
// Ignore module identifiers
else if (dynamic_cast<ModuleType const*>(_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<MagicType const*>(_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<Identifier const*>(&_memberAccess.expression()))
if (auto const* identifier = dynamic_cast<Identifier const*>(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<smt::SymbolicStructVariable>(m_context.expression(_memberAccess.expression()));
memberExpr->accept(*this);
auto const& symbStruct = dynamic_pointer_cast<smt::SymbolicStructVariable>(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<EnumDefinition const*>(decl))
{
auto enumType = dynamic_cast<EnumType const*>(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<smt::SymbolicArrayVariable>(m_context.expression(_memberAccess.expression()));
auto symbArray = dynamic_pointer_cast<smt::SymbolicArrayVariable>(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<VariableDeclaration const*>(_memberAccess.annotation().referencedDeclaration))
{
solAssert(var->isConstant(), "");
defineExpr(_memberAccess, constantExpr(_memberAccess, *var));
return false;
}
}
else
m_errorReporter.warning(
7650_error,
@ -3050,6 +3050,24 @@ vector<smtutil::Expression> 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<SourceUnit const*, ASTNode::CompareByID> const& _sources)
{
for (auto source: _sources)

2
libsolidity/formal/SMTEncoder.h
View File

@ -393,6 +393,8 @@ protected:
/// type conversion.
std::vector<smtutil::Expression> 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<SourceUnit const*, ASTNode::CompareByID> const& _sources);

2
test/libsolidity/smtCheckerTests/file_level/file_level_call_via_module.sol
View File

@ -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

1
test/libsolidity/smtCheckerTests/file_level/import.sol
View File

@ -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

26
test/libsolidity/smtCheckerTests/file_level/module_constants_1.sol Normal file
View File

@ -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

46
test/libsolidity/smtCheckerTests/file_level/module_constants_functions_1.sol Normal file
View File

@ -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

5
test/libsolidity/smtCheckerTests/file_level/same_constants_different_files.sol
View File

@ -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

2
test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol
View File

@ -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