From 19e067465a058ca9f40238cb3a928a1113531c9d Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 5 Oct 2017 15:23:25 +0200 Subject: Unary operators and division. --- libsolidity/analysis/TypeChecker.cpp | 2 +- libsolidity/formal/SMTChecker.cpp | 191 +++++++++++++++++++++++++---------- libsolidity/formal/SMTChecker.h | 14 ++- libsolidity/formal/SolverInterface.h | 4 + libsolidity/formal/Z3Interface.cpp | 5 +- 5 files changed, 155 insertions(+), 61 deletions(-) (limited to 'libsolidity') diff --git a/libsolidity/analysis/TypeChecker.cpp b/libsolidity/analysis/TypeChecker.cpp index 73047e76..96160a75 100644 --- a/libsolidity/analysis/TypeChecker.cpp +++ b/libsolidity/analysis/TypeChecker.cpp @@ -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, ""); diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 1050621e..9e2cf908 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -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,7 @@ 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()); else m_errorReporter.warning( _assignment.location(), @@ -230,7 +229,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(&_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(_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 +347,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 +361,7 @@ void SMTChecker::endVisit(Identifier const& _identifier) // Will be translated as part of the node that requested the lvalue. } else if (dynamic_cast(_identifier.annotation().type.get())) - m_interface->addAssertion(expr(_identifier) == currentValue(*decl)); + defineExpr(_identifier, currentValue(*decl)); else if (FunctionType const* fun = dynamic_cast(_identifier.annotation().type.get())) { if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require) @@ -306,10 +377,10 @@ void SMTChecker::endVisit(Literal const& _literal) if (RationalNumberType const* rational = dynamic_cast(&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,6 +397,7 @@ 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, ""); @@ -335,27 +407,19 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op) smt::Expression value( op == Token::Add ? left + right : op == Token::Sub ? left - right : + op == Token::Div ? left / right : /*op == Token::Mul*/ left * right ); - // Overflow check - auto const& intType = dynamic_cast(*_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); + } + + checkUnderOverflow(value, dynamic_cast(*_op.annotation().commonType), _op.location()); - m_interface->addAssertion(expr(_op) == value); + defineExpr(_op, value); break; } default: @@ -383,7 +447,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 +464,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 +475,17 @@ void SMTChecker::booleanOperation(BinaryOperation const& _op) ); } -void SMTChecker::assignment(Declaration const& _variable, Expression const& _value) +void SMTChecker::assignment(Declaration const& _variable, Expression const& _value, SourceLocation const& _location) { - // TODO more checks? - // TODO add restrictions about type (might be assignment from smaller type) - m_interface->addAssertion(newValue(_variable) == expr(_value)); + 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(type.get())) + checkUnderOverflow(_value, *intType, _location); + m_interface->addAssertion(newValue(_variable) == _value); } void SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition) @@ -694,29 +764,38 @@ smt::Expression SMTChecker::maxValue(IntegerType const& _t) smt::Expression SMTChecker::expr(Expression const& _e) { - if (!m_expressions.count(&_e)) + solAssert(m_expressions.count(&_e), ""); + return m_expressions.at(&_e); +} + +void SMTChecker::createExpr(Expression const& _e) +{ + solAssert(!m_expressions.count(&_e), ""); + solAssert(_e.annotation().type, ""); + switch (_e.annotation().type->category()) { - solAssert(_e.annotation().type, ""); - switch (_e.annotation().type->category()) - { - case Type::Category::RationalNumber: - { - if (RationalNumberType const* rational = dynamic_cast(_e.annotation().type.get())) - solAssert(!rational->isFractional(), ""); - m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); - break; - } - case Type::Category::Integer: - m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); - break; - case Type::Category::Bool: - m_expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e))); - break; - default: - solAssert(false, "Type not implemented."); - } + case Type::Category::RationalNumber: + { + if (RationalNumberType const* rational = dynamic_cast(_e.annotation().type.get())) + solAssert(!rational->isFractional(), ""); + m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); + break; } - return m_expressions.at(&_e); + case Type::Category::Integer: + m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); + break; + case Type::Category::Bool: + m_expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e))); + break; + default: + solAssert(false, "Type not implemented."); + } +} + +void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value) +{ + createExpr(_e); + m_interface->addAssertion(expr(_e) == _value); } smt::Expression SMTChecker::var(Declaration const& _decl) diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 8e07d74d..cc3aca81 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -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,8 @@ private: void compareOperation(BinaryOperation const& _op); void booleanOperation(BinaryOperation const& _op); - void assignment(Declaration const& _variable, Expression const& _value); + 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 +90,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> checkSatisifableAndGenerateModel(std::vector const& _expressionsToEvaluate); @@ -126,9 +131,12 @@ private: using VariableSequenceCounters = std::map; - /// 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); diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h index c9adf863..74c993e8 100644 --- a/libsolidity/formal/SolverInterface.h +++ b/libsolidity/formal/SolverInterface.h @@ -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( diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp index e5c1aef4..769e6edb 100644 --- a/libsolidity/formal/Z3Interface.cpp +++ b/libsolidity/formal/Z3Interface.cpp @@ -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]; -- cgit v1.2.3 From d160ec8595171e16dd404e9b859aa37aed2fe0a4 Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 5 Oct 2017 19:20:46 +0200 Subject: Fix signed division. --- libsolidity/formal/SMTChecker.cpp | 18 ++++++++++++++++-- libsolidity/formal/SMTChecker.h | 4 ++++ 2 files changed, 20 insertions(+), 2 deletions(-) (limited to 'libsolidity') 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(*_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(*_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); -- cgit v1.2.3 From a2569833203a952f265acc3511ace52cd9cec4c0 Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 5 Oct 2017 19:39:29 +0200 Subject: Fix expression creation problems. --- libsolidity/formal/SMTChecker.cpp | 49 ++++++++++++++++++++++++--------------- 1 file changed, 30 insertions(+), 19 deletions(-) (limited to 'libsolidity') diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index c20c63c6..a22e35d6 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -207,7 +207,10 @@ void SMTChecker::endVisit(Assignment const& _assignment) { Declaration const* decl = identifier->annotation().referencedDeclaration; if (knownVariable(*decl)) + { assignment(*decl, _assignment.rightHandSide(), _assignment.location()); + defineExpr(_assignment, expr(_assignment.rightHandSide())); + } else m_errorReporter.warning( _assignment.location(), @@ -778,31 +781,39 @@ smt::Expression SMTChecker::maxValue(IntegerType const& _t) smt::Expression SMTChecker::expr(Expression const& _e) { - solAssert(m_expressions.count(&_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) { - solAssert(!m_expressions.count(&_e), ""); - solAssert(_e.annotation().type, ""); - switch (_e.annotation().type->category()) - { - case Type::Category::RationalNumber: + if (m_expressions.count(&_e)) + m_errorReporter.warning(_e.location(), "Internal error: Expression created twice in SMT solver." ); + else { - if (RationalNumberType const* rational = dynamic_cast(_e.annotation().type.get())) - solAssert(!rational->isFractional(), ""); - m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); - break; - } - case Type::Category::Integer: - m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); - break; - case Type::Category::Bool: - m_expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e))); - break; - default: - solAssert(false, "Type not implemented."); + solAssert(_e.annotation().type, ""); + switch (_e.annotation().type->category()) + { + case Type::Category::RationalNumber: + { + if (RationalNumberType const* rational = dynamic_cast(_e.annotation().type.get())) + solAssert(!rational->isFractional(), ""); + m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); + break; + } + case Type::Category::Integer: + m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); + break; + case Type::Category::Bool: + m_expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e))); + break; + default: + solAssert(false, "Type not implemented."); + } } } -- cgit v1.2.3