diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 01c4544f0..a4044bdea 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -318,18 +318,12 @@ void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl) assignment(*declarations.at(i), symbTuple->component(i, components.at(i), declarations.at(i)->type())); } } - else if (m_context.knownVariable(*_varDecl.declarations().front())) + else { + solAssert(m_context.knownVariable(*_varDecl.declarations().front()), ""); if (_varDecl.initialValue()) assignment(*_varDecl.declarations().front(), *_varDecl.initialValue()); } - else - m_errorReporter.warning( - 7186_error, - _varDecl.location(), - "Assertion checker does not yet implement such variable declarations." - ); - } bool SMTEncoder::visit(Assignment const& _assignment) @@ -492,11 +486,7 @@ void SMTEncoder::endVisit(UnaryOperation const& _op) indexOrMemberAssignment(*subExpr, newValue); } else - m_errorReporter.warning( - 1950_error, - _op.location(), - "Assertion checker does not yet implement such increments / decrements." - ); + solAssert(false, ""); break; } @@ -530,11 +520,7 @@ void SMTEncoder::endVisit(UnaryOperation const& _op) break; } default: - m_errorReporter.warning( - 3682_error, - _op.location(), - "Assertion checker does not yet implement this operator." - ); + solAssert(false, ""); } } @@ -571,11 +557,7 @@ void SMTEncoder::endVisit(BinaryOperation const& _op) else if (TokenTraits::isBitOp(_op.getOperator()) || TokenTraits::isShiftOp(_op.getOperator())) bitwiseOperation(_op); else - m_errorReporter.warning( - 3876_error, - _op.location(), - "Assertion checker does not yet implement this operator." - ); + solAssert(false, ""); } bool SMTEncoder::visit(Conditional const& _op) @@ -1125,15 +1107,7 @@ void SMTEncoder::endVisit(Literal const& _literal) ); } else - { - m_errorReporter.warning( - 7885_error, - _literal.location(), - "Assertion checker does not yet support the type of this literal (" + - _literal.annotation().type->toString() + - ")." - ); - } + solAssert(false, ""); } void SMTEncoder::addArrayLiteralAssertions( @@ -1211,11 +1185,8 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) ); } else - m_errorReporter.warning( - 9551_error, - _memberAccess.location(), - "Assertion checker does not yet support this expression." - ); + solUnimplementedAssert(false, ""); + return false; } else if (smt::isNonRecursiveStruct(*exprType)) @@ -1605,40 +1576,32 @@ void SMTEncoder::arithmeticOperation(BinaryOperation const& _op) { auto type = _op.annotation().commonType; solAssert(type, ""); - if (type->category() == Type::Category::Integer || type->category() == Type::Category::FixedPoint) + solAssert(type->category() == Type::Category::Integer || type->category() == Type::Category::FixedPoint, ""); + switch (_op.getOperator()) { - switch (_op.getOperator()) - { - case Token::Add: - case Token::Sub: - case Token::Mul: - case Token::Div: - case Token::Mod: - { - auto values = arithmeticOperation( - _op.getOperator(), - expr(_op.leftExpression()), - expr(_op.rightExpression()), - _op.annotation().commonType, - _op - ); - defineExpr(_op, values.first); - break; - } - default: - m_errorReporter.warning( - 5188_error, - _op.location(), - "Assertion checker does not yet implement this operator." - ); - } - } - else - m_errorReporter.warning( - 9011_error, - _op.location(), - "Assertion checker does not yet implement this operator for type " + type->richIdentifier() + "." + case Token::Add: + case Token::Sub: + case Token::Mul: + case Token::Div: + case Token::Mod: + { + auto values = arithmeticOperation( + _op.getOperator(), + expr(_op.leftExpression()), + expr(_op.rightExpression()), + _op.annotation().commonType, + _op ); + defineExpr(_op, values.first); + break; + } + default: + m_errorReporter.warning( + 5188_error, + _op.location(), + "Assertion checker does not yet implement this operator." + ); + } } pair SMTEncoder::arithmeticOperation( @@ -1827,29 +1790,21 @@ void SMTEncoder::booleanOperation(BinaryOperation const& _op) { solAssert(_op.getOperator() == Token::And || _op.getOperator() == Token::Or, ""); solAssert(_op.annotation().commonType, ""); - if (_op.annotation().commonType->category() == Type::Category::Bool) + solAssert(_op.annotation().commonType->category() == Type::Category::Bool, ""); + // @TODO check that both of them are not constant + _op.leftExpression().accept(*this); + if (_op.getOperator() == Token::And) { - // @TODO check that both of them are not constant - _op.leftExpression().accept(*this); - if (_op.getOperator() == Token::And) - { - auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression())).first; - mergeVariables(touchedVariables(_op.rightExpression()), !expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond); - defineExpr(_op, expr(_op.leftExpression()) && expr(_op.rightExpression())); - } - else - { - auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression())).first; - mergeVariables(touchedVariables(_op.rightExpression()), expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond); - defineExpr(_op, expr(_op.leftExpression()) || expr(_op.rightExpression())); - } + auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression())).first; + mergeVariables(touchedVariables(_op.rightExpression()), !expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond); + defineExpr(_op, expr(_op.leftExpression()) && expr(_op.rightExpression())); } else - m_errorReporter.warning( - 3263_error, - _op.location(), - "Assertion checker does not yet implement the type " + _op.annotation().commonType->toString() + " for boolean operations" - ); + { + auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression())).first; + mergeVariables(touchedVariables(_op.rightExpression()), expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond); + defineExpr(_op, expr(_op.leftExpression()) || expr(_op.rightExpression())); + } } void SMTEncoder::bitwiseOperation(BinaryOperation const& _op) diff --git a/scripts/error_codes.py b/scripts/error_codes.py index 5ae990059..23c1657a7 100755 --- a/scripts/error_codes.py +++ b/scripts/error_codes.py @@ -220,15 +220,12 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False): return False old_source_only_ids = { - "1123", "1220", "1584", "1823", "1950", - "1988", "2657", "2800", - "3263", "3356", "3682", "3876", + "1123", "1220", "1584", "1823", + "1988", "2657", "2800", "3356", "3893", "3996", "4010", "4802", - "5073", "5188", "5272", - "5622", "6272", "7128", "7186", - "7589", "7593", "7653", "7885", "8065", "8084", "8140", - "8312", "8592", "9011", - "9085", "9390", "9551", + "5073", "5272", "5622", "6272", "7128", + "7589", "7593", "7653", "8065", "8084", "8140", + "8312", "8592", "9085", "9390" } new_source_only_ids = source_only_ids - old_source_only_ids diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol index 8682973cd..0e6e1642c 100644 --- a/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol +++ b/test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol @@ -1,7 +1,12 @@ pragma experimental SMTChecker; + contract C { - function f() public pure returns (byte) { - return (~byte(0xFF)); - } + function f() public pure { + // ffff0000 in bytes4 + bytes4 x = ~bytes4(hex"ffff"); + assert(x == 0xffff0000); // should fail + assert(x == 0x0000ffff); // should hold + } } // ---- +// Warning 6328: (175-198): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/exp.sol b/test/libsolidity/smtCheckerTests/operators/exp.sol new file mode 100644 index 000000000..3070f9649 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/exp.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; +contract D { + function f(uint x) public pure { + assert(x**2 == 4); + } +} +// ---- +// Warning 5188: (88-92): Assertion checker does not yet implement this operator. +// Warning 6328: (81-98): CHC: Assertion violation happens here. +// Warning 5188: (88-92): Assertion checker does not yet implement this operator. diff --git a/test/libsolidity/smtCheckerTests/special/ether_units.sol b/test/libsolidity/smtCheckerTests/special/ether_units.sol new file mode 100644 index 000000000..ccb0cee20 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/ether_units.sol @@ -0,0 +1,15 @@ +pragma experimental SMTChecker; +contract D { + function f() public pure { + assert(1000000000000000000 wei == 1 ether); + assert(100000000000000000 wei == 1 ether); + assert(1000000000 wei == 1 gwei); + assert(100000000 wei == 1 gwei); + assert(1000000000 gwei == 1 ether); + assert(100000000 gwei == 1 ether); + } +} +// ---- +// Warning 6328: (121-162): CHC: Assertion violation happens here. +// Warning 6328: (202-233): CHC: Assertion violation happens here. +// Warning 6328: (275-308): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/special/time_units.sol b/test/libsolidity/smtCheckerTests/special/time_units.sol new file mode 100644 index 000000000..59bb004b9 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/time_units.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; +contract D { + function f() public pure { + assert(1 == 1 seconds); + assert(2 == 1 seconds); + assert(2 minutes == 120 seconds); + assert(3 minutes == 120 seconds); + assert(2 hours == 120 minutes); + assert(3 hours == 120 minutes); + assert(2 days == 48 hours); + assert(4 days == 48 hours); + assert(2 weeks == 14 days); + assert(25 weeks == 14 days); + } +} +// ---- +// Warning 6328: (101-123): CHC: Assertion violation happens here. +// Warning 6328: (163-195): CHC: Assertion violation happens here. +// Warning 6328: (233-263): CHC: Assertion violation happens here. +// Warning 6328: (297-323): CHC: Assertion violation happens here. +// Warning 6328: (357-384): CHC: Assertion violation happens here.