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 #9798 from ethereum/smt-log

Browse Source 
[SMTChecker] Support events and low-level logs
This commit is contained in:
Alex Beregszaszi 2020-09-16 12:26:27 +01:00 committed by GitHub
commit a187a1c4c4
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 76 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -5,6 +5,7 @@ Language Features:
Compiler Features: Compiler Features:
* Export compiler-generated utility sources via standard-json or combined-json. * Export compiler-generated utility sources via standard-json or combined-json.
* SMTChecker: Support events and low-level logs.
* SMTChecker: Support ``revert()``. * SMTChecker: Support ``revert()``.
* SMTChecker: Support shifts. * SMTChecker: Support shifts.
* SMTChecker: Support structs. * SMTChecker: Support structs.

8
libsolidity/formal/SMTEncoder.cpp
View File

@ -676,6 +676,14 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
case FunctionType::Kind::ArrayPop: case FunctionType::Kind::ArrayPop:
arrayPop(_funCall); arrayPop(_funCall);
break; break;
case FunctionType::Kind::Log0:
case FunctionType::Kind::Log1:
case FunctionType::Kind::Log2:
case FunctionType::Kind::Log3:
case FunctionType::Kind::Log4:
case FunctionType::Kind::Event:
// These can be safely ignored.
break;
default: default:
m_errorReporter.warning( m_errorReporter.warning(
4588_error, 4588_error,

28
test/libsolidity/smtCheckerTests/special/event.sol Normal file
View File

@ -0,0 +1,28 @@
pragma experimental SMTChecker;
contract C {
event Nudge();
event SomeArgs(uint, uint);
event Caller(address, uint);
function f() payable external {
emit Nudge();
emit SomeArgs(134, 567);
emit Caller(msg.sender, msg.value);
}
function g_data() pure internal returns (uint) {
assert(true);
}
function g() external {
emit SomeArgs(g_data(), g_data());
}
bool x = true;
function h_data() view internal returns (uint) {
assert(x);
}
function h() external {
x = false;
emit SomeArgs(h_data(), h_data());
}
}
// ----
// Warning 6328: (440-449): Assertion violation happens here.

39
test/libsolidity/smtCheckerTests/special/log.sol Normal file
View File

@ -0,0 +1,39 @@
pragma experimental SMTChecker;
contract C {
function f() external {
bytes32 t1 = bytes32(uint256(0x1234));
log0(t1);
log1(t1, t1);
log2(t1, t1, t1);
log3(t1, t1, t1, t1);
log4(t1, t1, t1, t1, t1);
}
function g_data() pure internal returns (bytes32) {
assert(true);
return bytes32(uint256(0x5678));
}
function g() external {
// To test that the function call is actually visited.
log0(g_data());
log1(g_data(), g_data());
log2(g_data(), g_data(), g_data());
log3(g_data(), g_data(), g_data(), g_data());
log4(g_data(), g_data(), g_data(), g_data(), g_data());
}
bool x = true;
function h_data() view internal returns (bytes32) {
assert(x);
}
function h() external {
// To test that the function call is actually visited.
x = false;
log0(h_data());
log1(h_data(), h_data());
log2(h_data(), h_data(), h_data());
log3(h_data(), h_data(), h_data(), h_data());
log4(h_data(), h_data(), h_data(), h_data(), h_data());
}
}
// ----
// Warning 6328: (668-677): Assertion violation happens here.