From 80e85b772be4d9366675ba2f5ee07ee2e3325796 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 16 Dec 2020 11:27:56 +0100 Subject: [PATCH] [SMTChecker] Apply const eval to arithmetic binary expressions --- Changelog.md | 1 + libsolidity/formal/SMTEncoder.cpp | 43 +++++++++++++------ libsolidity/formal/SMTEncoder.h | 4 ++ .../complex/slither/const_state_variables.sol | 4 +- .../smtCheckerTests/operators/const_exp_1.sol | 15 +++++++ .../operators/constant_propagation_1.sol | 13 ++++++ 6 files changed, 67 insertions(+), 13 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/operators/const_exp_1.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/constant_propagation_1.sol diff --git a/Changelog.md b/Changelog.md index 27c5451bb..0b8805939 100644 --- a/Changelog.md +++ b/Changelog.md @@ -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. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index bd0746550..89727c6a6 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -22,6 +22,8 @@ #include #include +#include + #include #include @@ -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(_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(*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>> 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); diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 4f08aae7e..b6f65bcd7 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -83,6 +83,10 @@ public: /// @returns the arguments for each base constructor call in the hierarchy of @a _contract. std::map>> 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 diff --git a/test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol b/test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol index 280632f1f..92a45e5ac 100644 --- a/test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol +++ b/test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/operators/const_exp_1.sol b/test/libsolidity/smtCheckerTests/operators/const_exp_1.sol new file mode 100644 index 000000000..d156b9ab3 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/const_exp_1.sol @@ -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() diff --git a/test/libsolidity/smtCheckerTests/operators/constant_propagation_1.sol b/test/libsolidity/smtCheckerTests/operators/constant_propagation_1.sol new file mode 100644 index 000000000..536f43768 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/constant_propagation_1.sol @@ -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()