cerc-io/solidity
15
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 #11400 from blishko/smt-struct-constructor-fix

Browse Source 
SMTChecker: Fix struct constructor where fixed-bytes member is initialized with a string literal
This commit is contained in:
Harikrishnan Mulackal 2021-05-17 14:32:17 +02:00 committed by GitHub
commit 72b071c3c3
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 24 additions and 1 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:
Bugfixes:
* AST: Do not output value of Yul literal if it is not a valid UTF-8 string.
* SMTChecker: Fix internal error on struct constructor with fixed bytes member initialized with string literal.
AST Changes:

10
libsolidity/formal/SMTEncoder.cpp
View File

@ -1158,7 +1158,15 @@ void SMTEncoder::visitStructConstructorCall(FunctionCall const& _funCall)
if (smt::isNonRecursiveStruct(*_funCall.annotation().type))
{
auto& structSymbolicVar = dynamic_cast<smt::SymbolicStructVariable&>(*m_context.expression(_funCall));
structSymbolicVar.assignAllMembers(applyMap(_funCall.sortedArguments(), [this](auto const& arg) { return expr(*arg); }));
auto structType = dynamic_cast<StructType const*>(structSymbolicVar.type());
solAssert(structType, "");
auto const& structMembers = structType->structDefinition().members();
solAssert(structMembers.size() == _funCall.sortedArguments().size(), "");
auto args = _funCall.sortedArguments();
structSymbolicVar.assignAllMembers(applyMap(
ranges::views::zip(args, structMembers),
[this] (auto const& argMemberPair) { return expr(*argMemberPair.first, argMemberPair.second->type()); }
));
}
}

14
test/libsolidity/smtCheckerTests/types/struct/struct_constructor_fixed_bytes_from_string_1.sol Normal file
View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C {
struct S {
int a;
bytes5 b;
}
function f() public pure {
assert(S({a:2, b:""}).b == bytes5(0)); // should hold
assert(S({a:2, b:""}).a == 0); // should fail
}
}
// ----
// Warning 5523: (0-31): The SMTChecker pragma has been deprecated and will be removed in the future. Please use the "model checker engine" compiler setting to activate the SMTChecker instead. If the pragma is enabled, all engines will be used.
// Warning 6328: (178-207): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()