diff options
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 18 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 4 |
2 files changed, 20 insertions, 2 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 9e2cf908..c20c63c6 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -401,13 +401,14 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op) { solAssert(_op.annotation().commonType, ""); solAssert(_op.annotation().commonType->category() == Type::Category::Integer, ""); + auto const& intType = dynamic_cast<IntegerType const&>(*_op.annotation().commonType); smt::Expression left(expr(_op.leftExpression())); smt::Expression right(expr(_op.rightExpression())); Token::Value op = _op.getOperator(); smt::Expression value( op == Token::Add ? left + right : op == Token::Sub ? left - right : - op == Token::Div ? left / right : + op == Token::Div ? division(left, right, intType) : /*op == Token::Mul*/ left * right ); @@ -417,7 +418,7 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op) m_interface->addAssertion(right != 0); } - checkUnderOverflow(value, dynamic_cast<IntegerType const&>(*_op.annotation().commonType), _op.location()); + checkUnderOverflow(value, intType, _op.location()); defineExpr(_op, value); break; @@ -475,6 +476,19 @@ void SMTChecker::booleanOperation(BinaryOperation const& _op) ); } +smt::Expression SMTChecker::division(smt::Expression _left, smt::Expression _right, IntegerType const& _type) +{ + // Signed division in SMTLIB2 rounds differently for negative division. + if (_type.isSigned()) + return (smt::Expression::ite( + _left >= 0, + smt::Expression::ite(_right >= 0, _left / _right, 0 - (_left / (0 - _right))), + smt::Expression::ite(_right >= 0, 0 - ((0 - _left) / _right), (0 - _left) / (0 - _right)) + )); + else + return _left / _right; +} + void SMTChecker::assignment(Declaration const& _variable, Expression const& _value, SourceLocation const& _location) { assignment(_variable, expr(_value), _location); diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index cc3aca81..e7481cca 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -67,6 +67,10 @@ private: void compareOperation(BinaryOperation const& _op); void booleanOperation(BinaryOperation const& _op); + /// Division expression in the given type. Requires special treatment because + /// of rounding for signed division. + smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type); + void assignment(Declaration const& _variable, Expression const& _value, SourceLocation const& _location); void assignment(Declaration const& _variable, smt::Expression const& _value, SourceLocation const& _location); |