cerc-io/solidity
10
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

Merge pull request #3032 from ethereum/division

Browse Source 
Division and unary operators for SMT checker
This commit is contained in:
chriseth 2017-12-05 13:59:01 +01:00 committed by GitHub
commit b47e023df1
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
6 changed files with 260 additions and 43 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolidity/analysis/TypeChecker.cpp
View File

@ -1060,7 +1060,7 @@ bool TypeChecker::visit(VariableDeclarationStatement const& _statement)
_statement.initialValue()->location(),
"Invalid rational " +
valueComponentType->toString() +
" (absolute value too large or divison by zero)."
" (absolute value too large or division by zero)."
);
else
solAssert(false, "");

176
libsolidity/formal/SMTChecker.cpp
View File

@ -55,7 +55,7 @@ void SMTChecker::analyze(SourceUnit const& _source)
void SMTChecker::endVisit(VariableDeclaration const& _varDecl)
{
if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value())
assignment(_varDecl, *_varDecl.value());
assignment(_varDecl, *_varDecl.value(), _varDecl.location());
}
bool SMTChecker::visit(FunctionDefinition const& _function)
@ -178,8 +178,7 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl)
else if (knownVariable(*_varDecl.declarations()[0]))
{
if (_varDecl.initialValue())
// TODO more checks?
assignment(*_varDecl.declarations()[0], *_varDecl.initialValue());
assignment(*_varDecl.declarations()[0], *_varDecl.initialValue(), _varDecl.location());
}
else
m_errorReporter.warning(
@ -208,7 +207,10 @@ void SMTChecker::endVisit(Assignment const& _assignment)
{
Declaration const* decl = identifier->annotation().referencedDeclaration;
if (knownVariable(*decl))
assignment(*decl, _assignment.rightHandSide());
{
assignment(*decl, _assignment.rightHandSide(), _assignment.location());
defineExpr(_assignment, expr(_assignment.rightHandSide()));
}
else
m_errorReporter.warning(
_assignment.location(),
@ -230,7 +232,81 @@ void SMTChecker::endVisit(TupleExpression const& _tuple)
"Assertion checker does not yet implement tules and inline arrays."
);
else
m_interface->addAssertion(expr(_tuple) == expr(*_tuple.components()[0]));
defineExpr(_tuple, expr(*_tuple.components()[0]));
}
void SMTChecker::checkUnderOverflow(smt::Expression _value, IntegerType const& _type, SourceLocation const& _location)
{
checkCondition(
_value < minValue(_type),
_location,
"Underflow (resulting value less than " + formatNumber(_type.minValue()) + ")",
"value",
&_value
);
checkCondition(
_value > maxValue(_type),
_location,
"Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")",
"value",
&_value
);
}
void SMTChecker::endVisit(UnaryOperation const& _op)
{
switch (_op.getOperator())
{
case Token::Not: // !
{
solAssert(_op.annotation().type->category() == Type::Category::Bool, "");
defineExpr(_op, !expr(_op.subExpression()));
break;
}
case Token::Inc: // ++ (pre- or postfix)
case Token::Dec: // -- (pre- or postfix)
{
solAssert(_op.annotation().type->category() == Type::Category::Integer, "");
solAssert(_op.subExpression().annotation().lValueRequested, "");
if (Identifier const* identifier = dynamic_cast<Identifier const*>(&_op.subExpression()))
{
Declaration const* decl = identifier->annotation().referencedDeclaration;
if (knownVariable(*decl))
{
auto innerValue = currentValue(*decl);
auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1;
assignment(*decl, newValue, _op.location());
defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue);
}
else
m_errorReporter.warning(
_op.location(),
"Assertion checker does not yet implement such assignments."
);
}
else
m_errorReporter.warning(
_op.location(),
"Assertion checker does not yet implement such increments / decrements."
);
break;
}
case Token::Add: // +
defineExpr(_op, expr(_op.subExpression()));
break;
case Token::Sub: // -
{
defineExpr(_op, 0 - expr(_op.subExpression()));
if (auto intType = dynamic_cast<IntegerType const*>(_op.annotation().type.get()))
checkUnderOverflow(expr(_op), *intType, _op.location());
break;
}
default:
m_errorReporter.warning(
_op.location(),
"Assertion checker does not yet implement this operator."
);
}
}
void SMTChecker::endVisit(BinaryOperation const& _op)
@ -274,10 +350,8 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
{
solAssert(args.size() == 1, "");
solAssert(args[0]->annotation().type->category() == Type::Category::Bool, "");
checkBooleanNotConstant(*args[0], "Condition is always $VALUE.");
m_interface->addAssertion(expr(*args[0]));
checkCondition(!(expr(*args[0])), _funCall.location(), "Unreachable code");
// TODO is there something meaningful we can check here?
// We can check whether the condition is always fulfilled or never fulfilled.
}
}
@ -290,7 +364,7 @@ void SMTChecker::endVisit(Identifier const& _identifier)
// Will be translated as part of the node that requested the lvalue.
}
else if (dynamic_cast<IntegerType const*>(_identifier.annotation().type.get()))
m_interface->addAssertion(expr(_identifier) == currentValue(*decl));
defineExpr(_identifier, currentValue(*decl));
else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
{
if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require)
@ -306,10 +380,10 @@ void SMTChecker::endVisit(Literal const& _literal)
if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(&type))
solAssert(!rational->isFractional(), "");
m_interface->addAssertion(expr(_literal) == smt::Expression(type.literalValue(&_literal)));
defineExpr(_literal, smt::Expression(type.literalValue(&_literal)));
}
else if (type.category() == Type::Category::Bool)
m_interface->addAssertion(expr(_literal) == smt::Expression(_literal.token() == Token::TrueLiteral ? true : false));
defineExpr(_literal, smt::Expression(_literal.token() == Token::TrueLiteral ? true : false));
else
m_errorReporter.warning(
_literal.location(),
@ -326,36 +400,30 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
case Token::Add:
case Token::Sub:
case Token::Mul:
case Token::Div:
{
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 ? division(left, right, intType) :
/*op == Token::Mul*/ left * right
);
// Overflow check
auto const& intType = dynamic_cast<IntegerType const&>(*_op.annotation().commonType);
checkCondition(
value < minValue(intType),
_op.location(),
"Underflow (resulting value less than " + formatNumber(intType.minValue()) + ")",
"value",
&value
);
checkCondition(
value > maxValue(intType),
_op.location(),
"Overflow (resulting value larger than " + formatNumber(intType.maxValue()) + ")",
"value",
&value
);
if (_op.getOperator() == Token::Div)
{
checkCondition(right == 0, _op.location(), "Division by zero", "value", &right);
m_interface->addAssertion(right != 0);
}
m_interface->addAssertion(expr(_op) == value);
checkUnderOverflow(value, intType, _op.location());
defineExpr(_op, value);
break;
}
default:
@ -383,7 +451,7 @@ void SMTChecker::compareOperation(BinaryOperation const& _op)
/*op == Token::GreaterThanOrEqual*/ (left >= right)
);
// TODO: check that other values for op are not possible.
m_interface->addAssertion(expr(_op) == value);
defineExpr(_op, value);
}
else
m_errorReporter.warning(
@ -400,9 +468,9 @@ void SMTChecker::booleanOperation(BinaryOperation const& _op)
{
// @TODO check that both of them are not constant
if (_op.getOperator() == Token::And)
m_interface->addAssertion(expr(_op) == expr(_op.leftExpression()) && expr(_op.rightExpression()));
defineExpr(_op, expr(_op.leftExpression()) && expr(_op.rightExpression()));
else
m_interface->addAssertion(expr(_op) == expr(_op.leftExpression()) || expr(_op.rightExpression()));
defineExpr(_op, expr(_op.leftExpression()) || expr(_op.rightExpression()));
}
else
m_errorReporter.warning(
@ -411,11 +479,30 @@ void SMTChecker::booleanOperation(BinaryOperation const& _op)
);
}
void SMTChecker::assignment(Declaration const& _variable, Expression const& _value)
smt::Expression SMTChecker::division(smt::Expression _left, smt::Expression _right, IntegerType const& _type)
{
// TODO more checks?
// TODO add restrictions about type (might be assignment from smaller type)
m_interface->addAssertion(newValue(_variable) == expr(_value));
// 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);
}
void SMTChecker::assignment(Declaration const& _variable, smt::Expression const& _value, SourceLocation const& _location)
{
TypePointer type = _variable.type();
if (auto const* intType = dynamic_cast<IntegerType const*>(type.get()))
checkUnderOverflow(_value, *intType, _location);
m_interface->addAssertion(newValue(_variable) == _value);
}
void SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition)
@ -695,6 +782,18 @@ smt::Expression SMTChecker::maxValue(IntegerType const& _t)
smt::Expression SMTChecker::expr(Expression const& _e)
{
if (!m_expressions.count(&_e))
{
m_errorReporter.warning(_e.location(), "Internal error: Expression undefined for SMT solver." );
createExpr(_e);
}
return m_expressions.at(&_e);
}
void SMTChecker::createExpr(Expression const& _e)
{
if (m_expressions.count(&_e))
m_errorReporter.warning(_e.location(), "Internal error: Expression created twice in SMT solver." );
else
{
solAssert(_e.annotation().type, "");
switch (_e.annotation().type->category())
@ -716,7 +815,12 @@ smt::Expression SMTChecker::expr(Expression const& _e)
solAssert(false, "Type not implemented.");
}
}
return m_expressions.at(&_e);
}
void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value)
{
createExpr(_e);
m_interface->addAssertion(expr(_e) == _value);
}
smt::Expression SMTChecker::var(Declaration const& _decl)

18
libsolidity/formal/SMTChecker.h
View File

@ -57,6 +57,7 @@ private:
virtual void endVisit(ExpressionStatement const& _node) override;
virtual void endVisit(Assignment const& _node) override;
virtual void endVisit(TupleExpression const& _node) override;
virtual void endVisit(UnaryOperation const& _node) override;
virtual void endVisit(BinaryOperation const& _node) override;
virtual void endVisit(FunctionCall const& _node) override;
virtual void endVisit(Identifier const& _node) override;
@ -66,7 +67,12 @@ private:
void compareOperation(BinaryOperation const& _op);
void booleanOperation(BinaryOperation const& _op);
void assignment(Declaration const& _variable, Expression const& _value);
/// 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);
// Visits the branch given by the statement, pushes and pops the SMT checker.
// @param _condition if present, asserts that this condition is true within the branch.
@ -88,6 +94,9 @@ private:
Expression const& _condition,
std::string const& _description
);
/// Checks that the value is in the range given by the type.
void checkUnderOverflow(smt::Expression _value, IntegerType const& _Type, SourceLocation const& _location);
std::pair<smt::CheckResult, std::vector<std::string>>
checkSatisifableAndGenerateModel(std::vector<smt::Expression> const& _expressionsToEvaluate);
@ -126,9 +135,12 @@ private:
using VariableSequenceCounters = std::map<Declaration const*, int>;
/// Returns the expression corresponding to the AST node. Creates a new expression
/// if it does not exist yet.
/// Returns the expression corresponding to the AST node. Throws if the expression does not exist.
smt::Expression expr(Expression const& _e);
/// Creates the expression (value can be arbitrary)
void createExpr(Expression const& _e);
/// Creates the expression and sets its value.
void defineExpr(Expression const& _e, smt::Expression _value);
/// Returns the function declaration corresponding to the given variable.
/// The function takes one argument which is the "sequence number".
smt::Expression var(Declaration const& _decl);

4
libsolidity/formal/SolverInterface.h
View File

@ -120,6 +120,10 @@ public:
{
return Expression("*", std::move(_a), std::move(_b), Sort::Int);
}
friend Expression operator/(Expression _a, Expression _b)
{
return Expression("/", std::move(_a), std::move(_b), Sort::Int);
}
Expression operator()(Expression _a) const
{
solAssert(

5
libsolidity/formal/Z3Interface.cpp
View File

@ -127,7 +127,8 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
{">=", 2},
{"+", 2},
{"-", 2},
{"*", 2}
{"*", 2},
{"/", 2}
};
string const& n = _expr.name;
if (m_functions.count(n))
@ -173,6 +174,8 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
return arguments[0] - arguments[1];
else if (n == "*")
return arguments[0] * arguments[1];
else if (n == "/")
return arguments[0] / arguments[1];
// Cannot reach here.
solAssert(false, "");
return arguments[0];

98
test/libsolidity/SMTChecker.cpp
View File

@ -351,9 +351,9 @@ BOOST_AUTO_TEST_CASE(while_loop_simple)
// Check that side-effects of condition are taken into account
text = R"(
contract C {
function f(uint x) public pure {
function f(uint x, uint y) public pure {
x = 7;
while ((x = 5) > 0) {
while ((x = y) > 0) {
}
assert(x == 7);
}
@ -458,6 +458,100 @@ BOOST_AUTO_TEST_CASE(for_loop)
CHECK_WARNING(text, "Assertion violation");
}
BOOST_AUTO_TEST_CASE(division)
{
string text = R"(
contract C {
function f(uint x, uint y) public pure returns (uint) {
return x / y;
}
}
)";
CHECK_WARNING(text, "Division by zero");
text = R"(
contract C {
function f(uint x, uint y) public pure returns (uint) {
require(y != 0);
return x / y;
}
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
text = R"(
contract C {
function f(int x, int y) public pure returns (int) {
require(y != 0);
return x / y;
}
}
)";
CHECK_WARNING(text, "Overflow");
text = R"(
contract C {
function f(int x, int y) public pure returns (int) {
require(y != 0);
require(y != -1);
return x / y;
}
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
}
BOOST_AUTO_TEST_CASE(division_truncates_correctly)
{
string text = R"(
contract C {
function f(uint x, uint y) public pure {
x = 7;
y = 2;
assert(x / y == 3);
}
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
text = R"(
contract C {
function f(int x, int y) public pure {
x = 7;
y = 2;
assert(x / y == 3);
}
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
text = R"(
contract C {
function f(int x, int y) public pure {
x = -7;
y = 2;
assert(x / y == -3);
}
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
text = R"(
contract C {
function f(int x, int y) public pure {
x = 7;
y = -2;
assert(x / y == -3);
}
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
text = R"(
contract C {
function f(int x, int y) public pure {
x = -7;
y = -2;
assert(x / y == 3);
}
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
}
BOOST_AUTO_TEST_SUITE_END()
}