Merge pull request from ethereum/smt-revert

[SMTChecker] Support revert()
This commit is contained in:
Alex Beregszaszi 2020-09-15 13:26:19 +01:00 committed by GitHub
commit 5355e85639
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
8 changed files with 91 additions and 3 deletions

View File

@ -5,6 +5,7 @@ Language Features:
Compiler Features:
* Export compiler-generated utility sources via standard-json or combined-json.
* SMTChecker: Support ``revert()``.
* SMTChecker: Support shifts.
* SMTChecker: Support structs.
* SMTChecker: Support ``type(T).min``, ``type(T).max``, and ``type(I).interfaceId``.

View File

@ -631,6 +631,10 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
case FunctionType::Kind::Require:
visitRequire(_funCall);
break;
case FunctionType::Kind::Revert:
// Revert is a special case of require and equals to `require(false)`
addPathImpliedExpression(smtutil::Expression(false));
break;
case FunctionType::Kind::GasLeft:
visitGasLeft(_funCall);
break;

View File

@ -0,0 +1,33 @@
pragma experimental SMTChecker;
contract C {
function f() pure public {
require(false);
// This is not reachable.
assert(false);
}
function g() pure public {
require(false, "require message");
// This is not reachable.
assert(false);
}
function h(bool b) pure public {
if (b)
require(false);
assert(!b);
}
// Check that arguments are evaluated.
bool x = false;
function m() view internal returns (string memory) {
assert(x != true);
}
function i() public {
x = true;
require(false, m());
}
}
// ----
// Warning 6328: (448-465): Assertion violation happens here.

View File

@ -0,0 +1,35 @@
pragma experimental SMTChecker;
contract C {
function f() pure public {
revert();
// This is not reachable.
assert(false);
}
function g() pure public {
revert("revert message");
// This is not reachable.
assert(false);
}
function h(bool b) pure public {
if (b)
revert();
assert(!b);
}
// Check that arguments are evaluated.
bool x = false;
function m() view internal returns (string memory) {
assert(x != true);
}
function i() public {
x = true;
revert(m());
}
}
// ----
// Warning 5740: (116-129): Unreachable code.
// Warning 5740: (221-234): Unreachable code.
// Warning 6328: (427-444): Assertion violation happens here.

View File

@ -0,0 +1,18 @@
pragma experimental SMTChecker;
contract C {
function f(bool b, uint a) pure public {
require(a <= 256);
if (b)
revert();
uint c = a + 1;
if (b)
c--;
else
c++;
assert(c == a);
}
}
// ----
// Warning 6328: (183-197): Assertion violation happens here.
// Warning 6838: (155-156): Condition is always false.

View File

@ -6,4 +6,3 @@ contract C {
}
// ----
// Warning 6838: (94-100): Condition is always true.
// Warning 4588: (104-112): Assertion checker does not yet implement this type of function call.

View File

@ -6,4 +6,3 @@ contract C {
}
// ----
// Warning 6838: (109-115): Condition is always false.
// Warning 4588: (119-127): Assertion checker does not yet implement this type of function call.

View File

@ -6,4 +6,3 @@ contract C {
}
}
// ----
// Warning 4588: (136-144): Assertion checker does not yet implement this type of function call.