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 #12036 from ethereum/smt_fix_magic

Browse Source 
[SMTChecker] Fix magic access
This commit is contained in:
chriseth 2021-10-04 11:01:39 +02:00 committed by GitHub
commit 529087be6c
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 50 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -7,6 +7,7 @@ Compiler Features:
Bugfixes:
* SMTChecker: Fix internal error in magic type access (``block``, ``msg``, ``tx``).

64
libsolidity/formal/SMTEncoder.cpp
View File

@ -1316,32 +1316,42 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
solAssert(name == "block" || name == "msg" || name == "tx", "");
defineExpr(_memberAccess, state().txMember(name + "." + _memberAccess.memberName()));
}
else if (auto magicType = dynamic_cast<MagicType const*>(exprType); magicType->kind() == MagicType::Kind::MetaType)
else if (auto magicType = dynamic_cast<MagicType const*>(exprType))
{
auto const& memberName = _memberAccess.memberName();
if (memberName == "min" || memberName == "max")
if (magicType->kind() == MagicType::Kind::Block)
defineExpr(_memberAccess, state().txMember("block." + _memberAccess.memberName()));
else if (magicType->kind() == MagicType::Kind::Message)
defineExpr(_memberAccess, state().txMember("msg." + _memberAccess.memberName()));
else if (magicType->kind() == MagicType::Kind::Transaction)
defineExpr(_memberAccess, state().txMember("tx." + _memberAccess.memberName()));
else if (magicType->kind() == MagicType::Kind::MetaType)
{
if (IntegerType const* integerType = dynamic_cast<IntegerType const*>(magicType->typeArgument()))
defineExpr(_memberAccess, memberName == "min" ? integerType->minValue() : integerType->maxValue());
else if (EnumType const* enumType = dynamic_cast<EnumType const*>(magicType->typeArgument()))
defineExpr(_memberAccess, memberName == "min" ? enumType->minValue() : enumType->maxValue());
auto const& memberName = _memberAccess.memberName();
if (memberName == "min" || memberName == "max")
{
if (IntegerType const* integerType = dynamic_cast<IntegerType const*>(magicType->typeArgument()))
defineExpr(_memberAccess, memberName == "min" ? integerType->minValue() : integerType->maxValue());
else if (EnumType const* enumType = dynamic_cast<EnumType const*>(magicType->typeArgument()))
defineExpr(_memberAccess, memberName == "min" ? enumType->minValue() : enumType->maxValue());
}
else if (memberName == "interfaceId")
{
ContractDefinition const& contract = dynamic_cast<ContractType const&>(*magicType->typeArgument()).contractDefinition();
defineExpr(_memberAccess, contract.interfaceId());
}
else
// NOTE: supporting name, creationCode, runtimeCode would be easy enough, but the bytes/string they return are not
// at all usable in the SMT checker currently
m_errorReporter.warning(
7507_error,
_memberAccess.location(),
"Assertion checker does not yet support this expression."
);
}
else if (memberName == "interfaceId")
{
ContractDefinition const& contract = dynamic_cast<ContractType const&>(*magicType->typeArgument()).contractDefinition();
defineExpr(_memberAccess, contract.interfaceId());
}
else
// NOTE: supporting name, creationCode, runtimeCode would be easy enough, but the bytes/string they return are not
// at all usable in the SMT checker currently
m_errorReporter.warning(
7507_error,
_memberAccess.location(),
"Assertion checker does not yet support this expression."
);
}
else
solUnimplementedAssert(false, "");
solAssert(false, "");
return false;
}
@ -1419,12 +1429,12 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
return false;
}
}
else
m_errorReporter.warning(
7650_error,
_memberAccess.location(),
"Assertion checker does not yet support this expression."
);
m_errorReporter.warning(
7650_error,
_memberAccess.location(),
"Assertion checker does not yet support this expression."
);
return true;
}

12
test/libsolidity/smtCheckerTests/special/msg_parens_1.sol Normal file
View File

@ -0,0 +1,12 @@
contract C {
function f() public payable {
assert((msg).value == 10);
assert((true ? msg : msg).value == 12);
}
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6328: (46-71): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(){ value: 11 }
// Warning 6328: (75-113): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()