mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
[SMTChecker] Apply const eval to arithmetic binary expressions
This commit is contained in:
parent
e347545597
commit
80e85b772b
@ -11,6 +11,7 @@ Language Features:
|
||||
Compiler Features:
|
||||
* Build System: Optionally support dynamic loading of Z3 and use that mechanism for Linux release builds.
|
||||
* Code Generator: Avoid memory allocation for default value if it is not used.
|
||||
* SMTChecker: Apply constant evaluation on binary arithmetic expressions.
|
||||
* SMTChecker: Create underflow and overflow verification targets for increment/decrement in the CHC engine.
|
||||
* SMTChecker: Report struct values in counterexamples from CHC engine.
|
||||
* SMTChecker: Support early returns in the CHC engine.
|
||||
|
@ -22,6 +22,8 @@
|
||||
#include <libsolidity/formal/SymbolicState.h>
|
||||
#include <libsolidity/formal/SymbolicTypes.h>
|
||||
|
||||
#include <libsolidity/analysis/ConstantEvaluator.h>
|
||||
|
||||
#include <libsmtutil/SMTPortfolio.h>
|
||||
#include <libsmtutil/Helpers.h>
|
||||
|
||||
@ -600,7 +602,8 @@ bool SMTEncoder::visit(BinaryOperation const& _op)
|
||||
|
||||
void SMTEncoder::endVisit(BinaryOperation const& _op)
|
||||
{
|
||||
if (_op.annotation().type->category() == Type::Category::RationalNumber)
|
||||
/// If _op is const evaluated the RationalNumber shortcut was taken.
|
||||
if (isConstant(_op))
|
||||
return;
|
||||
if (TokenTraits::isBooleanOp(_op.getOperator()))
|
||||
return;
|
||||
@ -1628,17 +1631,17 @@ void SMTEncoder::defineGlobalVariable(string const& _name, Expression const& _ex
|
||||
|
||||
bool SMTEncoder::shortcutRationalNumber(Expression const& _expr)
|
||||
{
|
||||
if (_expr.annotation().type->category() == Type::Category::RationalNumber)
|
||||
{
|
||||
auto rationalType = dynamic_cast<RationalNumberType const*>(_expr.annotation().type);
|
||||
solAssert(rationalType, "");
|
||||
if (rationalType->isNegative())
|
||||
defineExpr(_expr, smtutil::Expression(u2s(rationalType->literalValue(nullptr))));
|
||||
else
|
||||
defineExpr(_expr, smtutil::Expression(rationalType->literalValue(nullptr)));
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
auto type = isConstant(_expr);
|
||||
if (!type)
|
||||
return false;
|
||||
|
||||
solAssert(type->category() == Type::Category::RationalNumber, "");
|
||||
auto const& rationalType = dynamic_cast<RationalNumberType const&>(*type);
|
||||
if (rationalType.isNegative())
|
||||
defineExpr(_expr, smtutil::Expression(u2s(rationalType.literalValue(nullptr))));
|
||||
else
|
||||
defineExpr(_expr, smtutil::Expression(rationalType.literalValue(nullptr)));
|
||||
return true;
|
||||
}
|
||||
|
||||
void SMTEncoder::arithmeticOperation(BinaryOperation const& _op)
|
||||
@ -2660,6 +2663,22 @@ map<ContractDefinition const*, vector<ASTPointer<frontend::Expression>>> SMTEnco
|
||||
return baseArgs;
|
||||
}
|
||||
|
||||
TypePointer SMTEncoder::isConstant(Expression const& _expr)
|
||||
{
|
||||
if (
|
||||
auto type = _expr.annotation().type;
|
||||
type->category() == Type::Category::RationalNumber
|
||||
)
|
||||
return type;
|
||||
|
||||
// _expr may not be constant evaluable.
|
||||
// In that case we ignore any warnings emitted by the constant evaluator,
|
||||
// as it will return nullptr in case of failure.
|
||||
ErrorList l;
|
||||
ErrorReporter e(l);
|
||||
return ConstantEvaluator(e).evaluate(_expr);
|
||||
}
|
||||
|
||||
void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
|
||||
{
|
||||
FunctionDefinition const* funDef = functionCallToDefinition(_funCall);
|
||||
|
@ -83,6 +83,10 @@ public:
|
||||
/// @returns the arguments for each base constructor call in the hierarchy of @a _contract.
|
||||
std::map<ContractDefinition const*, std::vector<ASTPointer<frontend::Expression>>> baseArguments(ContractDefinition const& _contract);
|
||||
|
||||
/// @returns a valid RationalNumberType pointer if _expr has type
|
||||
/// RationalNumberType or can be const evaluated, and nullptr otherwise.
|
||||
static TypePointer isConstant(Expression const& _expr);
|
||||
|
||||
protected:
|
||||
// TODO: Check that we do not have concurrent reads and writes to a variable,
|
||||
// because the order of expression evaluation is undefined
|
||||
|
@ -50,7 +50,9 @@ contract MyConc{
|
||||
}
|
||||
|
||||
}
|
||||
// ====
|
||||
// SMTIgnoreCex: yes
|
||||
// ----
|
||||
// Warning 2519: (773-792): This declaration shadows an existing declaration.
|
||||
// Warning 2018: (1009-1086): Function state mutability can be restricted to view
|
||||
// Warning 4984: (985-1002): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nA = 1, should_be_constant = 0, should_be_constant_2 = 2, not_constant = 0, not_constant_2 = 115792089237316195423570985008687907853269984665640564039457584007913129639926, not_constant_3 = 0\n\nTransaction trace:\nconstructor()
|
||||
// Warning 4984: (985-1002): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
|
||||
|
15
test/libsolidity/smtCheckerTests/operators/const_exp_1.sol
Normal file
15
test/libsolidity/smtCheckerTests/operators/const_exp_1.sol
Normal file
@ -0,0 +1,15 @@
|
||||
pragma experimental SMTChecker;
|
||||
|
||||
contract C {
|
||||
uint constant x = 2;
|
||||
uint constant y = x ** 10;
|
||||
|
||||
function f() public view {
|
||||
assert(y == 2 ** 10);
|
||||
assert(y == 1024);
|
||||
assert(y == 14); // should fail
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 2018: (98-206): Function state mutability can be restricted to pure
|
||||
// Warning 6328: (172-187): CHC: Assertion violation happens here.\nCounterexample:\nx = 2, y = 1024\n\n\n\nTransaction trace:\nconstructor()\nState: x = 2, y = 1024\nf()
|
@ -0,0 +1,13 @@
|
||||
pragma experimental SMTChecker;
|
||||
|
||||
contract C {
|
||||
uint constant DEPOSIT_CONTRACT_TREE_DEPTH = 32;
|
||||
uint constant MAX_DEPOSIT_COUNT = 2**DEPOSIT_CONTRACT_TREE_DEPTH - 1;
|
||||
function f() public pure {
|
||||
assert(DEPOSIT_CONTRACT_TREE_DEPTH == 32);
|
||||
assert(MAX_DEPOSIT_COUNT == 4294967295);
|
||||
assert(MAX_DEPOSIT_COUNT == 2); // should fail
|
||||
}
|
||||
}
|
||||
// ----
|
||||
// Warning 6328: (284-314): CHC: Assertion violation happens here.\nCounterexample:\nDEPOSIT_CONTRACT_TREE_DEPTH = 32, MAX_DEPOSIT_COUNT = 4294967295\n\n\n\nTransaction trace:\nconstructor()\nState: DEPOSIT_CONTRACT_TREE_DEPTH = 32, MAX_DEPOSIT_COUNT = 4294967295\nf()
|
Loading…
Reference in New Issue
Block a user