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

Fix constant evaluation build

Browse Source
This commit is contained in:
Leonardo Alt 2020-12-16 17:58:49 +01:00
parent b252ab08a9
commit f5c96ea6da
3 changed files with 26 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
libsolidity/formal/SMTEncoder.cpp
View File

@ -1626,16 +1626,14 @@ void SMTEncoder::defineGlobalVariable(string const& _name, Expression const& _ex
bool SMTEncoder::shortcutRationalNumber(Expression const& _expr) bool SMTEncoder::shortcutRationalNumber(Expression const& _expr)
{ {
auto type = isConstant(_expr); RationalNumberType const* rationalType = isConstant(_expr);
if (!type) if (!rationalType)
return false; return false;
solAssert(type->category() == Type::Category::RationalNumber, ""); if (rationalType->isNegative())
auto const& rationalType = dynamic_cast<RationalNumberType const&>(*type); defineExpr(_expr, smtutil::Expression(u2s(rationalType->literalValue(nullptr))));
if (rationalType.isNegative())
defineExpr(_expr, smtutil::Expression(u2s(rationalType.literalValue(nullptr))));
else else
defineExpr(_expr, smtutil::Expression(rationalType.literalValue(nullptr))); defineExpr(_expr, smtutil::Expression(rationalType->literalValue(nullptr)));
return true; return true;
} }
@ -2658,12 +2656,9 @@ map<ContractDefinition const*, vector<ASTPointer<frontend::Expression>>> SMTEnco
return baseArgs; return baseArgs;
} }
TypePointer SMTEncoder::isConstant(Expression const& _expr) RationalNumberType const* SMTEncoder::isConstant(Expression const& _expr)
{ {
if ( if (auto type = dynamic_cast<RationalNumberType const*>(_expr.annotation().type))
auto type = _expr.annotation().type;
type->category() == Type::Category::RationalNumber
)
return type; return type;
// _expr may not be constant evaluable. // _expr may not be constant evaluable.
@ -2671,7 +2666,10 @@ TypePointer SMTEncoder::isConstant(Expression const& _expr)
// as it will return nullptr in case of failure. // as it will return nullptr in case of failure.
ErrorList l; ErrorList l;
ErrorReporter e(l); ErrorReporter e(l);
return ConstantEvaluator(e).evaluate(_expr); if (auto t = ConstantEvaluator::evaluate(e, _expr))
return TypeProvider::rationalNumber(t->value);
return nullptr;
} }
void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall) void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)

2
libsolidity/formal/SMTEncoder.h
View File

@ -85,7 +85,7 @@ public:
/// @returns a valid RationalNumberType pointer if _expr has type /// @returns a valid RationalNumberType pointer if _expr has type
/// RationalNumberType or can be const evaluated, and nullptr otherwise. /// RationalNumberType or can be const evaluated, and nullptr otherwise.
static TypePointer isConstant(Expression const& _expr); static RationalNumberType const* isConstant(Expression const& _expr);
protected: protected:
// TODO: Check that we do not have concurrent reads and writes to a variable, // TODO: Check that we do not have concurrent reads and writes to a variable,

14
test/libsolidity/smtCheckerTests/operators/constant_propagation_2.sol Normal file
View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C {
uint constant x = 7;
uint constant y = 3;
uint constant z = x / y;
function f() public pure {
assert(z == 2);
assert(z == x / 3);
assert(z == 7 / y);
assert(z * 3 != 7);
}
}