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 signed division.

Browse Source
This commit is contained in:
chriseth 2017-10-05 19:20:46 +02:00
parent 19e067465a
commit d160ec8595
2 changed files with 20 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
libsolidity/formal/SMTChecker.cpp
View File

@ -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);

4
libsolidity/formal/SMTChecker.h
View File

@ -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);