From fb3c85633bf19413a446d15a231a59536e904e35 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 1 Jul 2019 16:25:33 +0200 Subject: [PATCH] Always create symbolic expression --- libsolidity/formal/SMTEncoder.cpp | 50 ++++++++++--------- .../complex/slither/data_dependency.sol | 8 ++- .../complex/slither/external_function.sol | 2 - .../complex/warn_on_struct.sol | 2 +- .../operators/delete_struct.sol | 3 ++ .../smtCheckerTests/types/array_literal_1.sol | 1 - .../types/array_struct_array_branches_2d.sol | 8 +-- .../smtCheckerTests/types/enum_in_struct.sol | 2 + .../smtCheckerTests/types/struct_1.sol | 6 +-- .../types/struct_array_branches_1d.sol | 4 ++ .../types/struct_array_branches_2d.sol | 4 ++ .../types/struct_array_branches_3d.sol | 4 ++ .../smtCheckerTestsJSON/multi.json | 6 +-- .../smtCheckerTestsJSON/simple.json | 2 +- 14 files changed, 61 insertions(+), 41 deletions(-) diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 30aa95226..ce5860efd 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -204,6 +204,8 @@ void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl) void SMTEncoder::endVisit(Assignment const& _assignment) { + createExpr(_assignment); + static set const compoundOps{ Token::AssignAdd, Token::AssignSub, @@ -219,10 +221,6 @@ void SMTEncoder::endVisit(Assignment const& _assignment) ); else if (!smt::isSupportedType(_assignment.annotation().type->category())) { - m_errorReporter.warning( - _assignment.location(), - "Assertion checker does not yet implement type " + _assignment.annotation().type->toString() - ); // Give it a new index anyway to keep the SSA scheme sound. if (auto varDecl = identifierToVariable(_assignment.leftHandSide())) m_context.newValue(*varDecl); @@ -260,6 +258,8 @@ void SMTEncoder::endVisit(Assignment const& _assignment) void SMTEncoder::endVisit(TupleExpression const& _tuple) { + createExpr(_tuple); + if (_tuple.isInlineArray()) m_errorReporter.warning( _tuple.location(), @@ -267,7 +267,6 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple) ); else if (_tuple.annotation().type->category() == Type::Category::Tuple) { - createExpr(_tuple); vector> components; for (auto const& component: _tuple.components()) if (component) @@ -302,6 +301,8 @@ void SMTEncoder::endVisit(UnaryOperation const& _op) if (_op.annotation().type->category() == Type::Category::RationalNumber) return; + createExpr(_op); + switch (_op.getOperator()) { case Token::Not: // ! @@ -401,6 +402,8 @@ void SMTEncoder::endVisit(BinaryOperation const& _op) if (TokenTraits::isBooleanOp(_op.getOperator())) return; + createExpr(_op); + if (TokenTraits::isArithmeticOp(_op.getOperator())) arithmeticOperation(_op); else if (TokenTraits::isCompareOp(_op.getOperator())) @@ -535,24 +538,21 @@ void SMTEncoder::endVisit(Identifier const& _identifier) } else if (_identifier.annotation().type->category() == Type::Category::Function) visitFunctionIdentifier(_identifier); - else if (smt::isSupportedType(_identifier.annotation().type->category())) + else if (auto decl = identifierToVariable(_identifier)) + defineExpr(_identifier, currentValue(*decl)); + else if (_identifier.name() == "now") + defineGlobalVariable(_identifier.name(), _identifier); + else if (_identifier.name() == "this") { - if (auto decl = identifierToVariable(_identifier)) - defineExpr(_identifier, currentValue(*decl)); - else if (_identifier.name() == "now") - defineGlobalVariable(_identifier.name(), _identifier); - else if (_identifier.name() == "this") - { - defineExpr(_identifier, m_context.thisAddress()); - m_uninterpretedTerms.insert(&_identifier); - } - else - // TODO: handle MagicVariableDeclaration here - m_errorReporter.warning( - _identifier.location(), - "Assertion checker does not yet support the type of this variable." - ); + defineExpr(_identifier, m_context.thisAddress()); + m_uninterpretedTerms.insert(&_identifier); } + else if (smt::isSupportedType(_identifier.annotation().type->category())) + // TODO: handle MagicVariableDeclaration here + m_errorReporter.warning( + _identifier.location(), + "Assertion checker does not yet support the type of this variable." + ); } void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall) @@ -654,6 +654,8 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) if (accessType->category() == Type::Category::Function) return true; + createExpr(_memberAccess); + auto const& exprType = _memberAccess.expression().annotation().type; solAssert(exprType, ""); auto identifier = dynamic_cast(&_memberAccess.expression()); @@ -697,12 +699,13 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) "Assertion checker does not yet support this expression." ); - createExpr(_memberAccess); return true; } void SMTEncoder::endVisit(IndexAccess const& _indexAccess) { + createExpr(_indexAccess); + shared_ptr array; if (auto const& id = dynamic_cast(&_indexAccess.baseExpression())) { @@ -717,7 +720,6 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess) } else { - createExpr(_indexAccess); m_errorReporter.warning( _indexAccess.location(), "Assertion checker does not yet implement this expression." @@ -1227,7 +1229,7 @@ void SMTEncoder::createExpr(Expression const& _e) if (abstract) m_errorReporter.warning( _e.location(), - "Assertion checker does not yet implement this type." + "Assertion checker does not yet implement type " + _e.annotation().type->toString() ); } diff --git a/test/libsolidity/smtCheckerTests/complex/slither/data_dependency.sol b/test/libsolidity/smtCheckerTests/complex/slither/data_dependency.sol index 89c38a4cd..2053fff48 100644 --- a/test/libsolidity/smtCheckerTests/complex/slither/data_dependency.sol +++ b/test/libsolidity/smtCheckerTests/complex/slither/data_dependency.sol @@ -123,14 +123,18 @@ contract PropagateThroughReturnValue { // Warning: (353-378): Assertion checker does not yet support the type of this variable. // Warning: (384-409): Assertion checker does not yet support the type of this variable. // Warning: (464-479): Assertion checker does not yet support this expression. +// Warning: (464-475): Assertion checker does not yet implement type struct Reference.St storage ref // Warning: (464-494): Assertion checker does not yet implement such assignments. // Warning: (539-554): Assertion checker does not yet support this expression. +// Warning: (539-550): Assertion checker does not yet implement type struct Reference.St storage ref // Warning: (557-567): Assertion checker does not yet support this expression. +// Warning: (557-563): Assertion checker does not yet implement type struct Reference.St storage ref // Warning: (539-567): Assertion checker does not yet implement such assignments. // Warning: (629-643): Assertion checker does not yet support the type of this variable. -// Warning: (646-668): Internal error: Expression undefined for SMT solver. -// Warning: (646-668): Assertion checker does not yet implement this type. +// Warning: (646-668): Assertion checker does not yet implement type struct Reference.St storage ref +// Warning: (706-728): Assertion checker does not yet implement type struct Reference.St storage ref // Warning: (700-728): Assertion checker does not yet implement type struct Reference.St storage pointer // Warning: (748-755): Assertion checker does not yet support this expression. +// Warning: (748-751): Assertion checker does not yet implement type struct Reference.St storage pointer // Warning: (748-770): Assertion checker does not yet implement such assignments. // Warning: (849-905): Assertion checker does not yet support constructors. diff --git a/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol b/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol index ece92ee0c..a3ac97dba 100644 --- a/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol +++ b/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol @@ -87,6 +87,4 @@ contract InternalCall { // Warning: (782-813): Type conversion is not yet fully supported and might yield false positives. // Warning: (771-814): Assertion checker does not yet implement this type of function call. // Warning: (825-830): Assertion checker does not yet support the type of this variable. -// Warning: (1057-1068): Assertion checker does not yet implement type function () returns (uint256) -// Warning: (1120-1131): Assertion checker does not yet implement type function () returns (uint256) // Warning: (1403-1408): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol b/test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol index 861602bad..f6c6f89c2 100644 --- a/test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol +++ b/test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol @@ -9,5 +9,5 @@ contract C { // ---- // Warning: (133-143): Unused local variable. // Warning: (133-143): Assertion checker does not yet support the type of this variable. -// Warning: (146-163): Assertion checker does not yet implement this type. +// Warning: (146-163): Assertion checker does not yet implement type struct C.A memory // Warning: (146-163): Assertion checker does not yet implement this expression. diff --git a/test/libsolidity/smtCheckerTests/operators/delete_struct.sol b/test/libsolidity/smtCheckerTests/operators/delete_struct.sol index e0583602a..57a10c1eb 100644 --- a/test/libsolidity/smtCheckerTests/operators/delete_struct.sol +++ b/test/libsolidity/smtCheckerTests/operators/delete_struct.sol @@ -20,8 +20,11 @@ contract C // Warning: (73-192): Function state mutability can be restricted to pure // Warning: (103-113): Assertion checker does not yet support the type of this variable. // Warning: (117-120): Assertion checker does not yet support this expression. +// Warning: (117-118): Assertion checker does not yet implement type struct C.S memory // Warning: (117-124): Assertion checker does not yet implement such assignments. // Warning: (165-168): Assertion checker does not yet support this expression. +// Warning: (165-166): Assertion checker does not yet implement type struct C.S memory // Warning: (158-168): Assertion checker does not yet implement "delete" for this expression. // Warning: (179-182): Assertion checker does not yet support this expression. +// Warning: (179-180): Assertion checker does not yet implement type struct C.S memory // Warning: (172-188): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_literal_1.sol b/test/libsolidity/smtCheckerTests/types/array_literal_1.sol index 0380f673c..99e350ba0 100644 --- a/test/libsolidity/smtCheckerTests/types/array_literal_1.sol +++ b/test/libsolidity/smtCheckerTests/types/array_literal_1.sol @@ -9,4 +9,3 @@ contract C // ---- // Warning: (76-96): Unused local variable. // Warning: (99-114): Assertion checker does not yet implement inline arrays. -// Warning: (99-114): Internal error: Expression undefined for SMT solver. diff --git a/test/libsolidity/smtCheckerTests/types/array_struct_array_branches_2d.sol b/test/libsolidity/smtCheckerTests/types/array_struct_array_branches_2d.sol index 99568e432..725cecc86 100644 --- a/test/libsolidity/smtCheckerTests/types/array_struct_array_branches_2d.sol +++ b/test/libsolidity/smtCheckerTests/types/array_struct_array_branches_2d.sol @@ -15,18 +15,18 @@ contract C } // ---- // Warning: (124-130): Assertion checker does not yet support this expression. -// Warning: (124-128): Assertion checker does not yet implement this type. +// Warning: (124-128): Assertion checker does not yet implement type struct C.S memory // Warning: (124-133): Assertion checker does not yet implement this expression. // Warning: (124-136): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays. // Warning: (154-160): Assertion checker does not yet support this expression. -// Warning: (154-158): Assertion checker does not yet implement this type. +// Warning: (154-158): Assertion checker does not yet implement type struct C.S memory // Warning: (154-163): Assertion checker does not yet implement this expression. // Warning: (154-166): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays. // Warning: (182-188): Assertion checker does not yet support this expression. -// Warning: (182-186): Assertion checker does not yet implement this type. +// Warning: (182-186): Assertion checker does not yet implement type struct C.S memory // Warning: (182-191): Assertion checker does not yet implement this expression. // Warning: (182-194): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays. // Warning: (209-215): Assertion checker does not yet support this expression. -// Warning: (209-213): Assertion checker does not yet implement this type. +// Warning: (209-213): Assertion checker does not yet implement type struct C.S memory // Warning: (209-218): Assertion checker does not yet implement this expression. // Warning: (202-226): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/enum_in_struct.sol b/test/libsolidity/smtCheckerTests/types/enum_in_struct.sol index 5218683f4..47bdd0c66 100644 --- a/test/libsolidity/smtCheckerTests/types/enum_in_struct.sol +++ b/test/libsolidity/smtCheckerTests/types/enum_in_struct.sol @@ -12,6 +12,8 @@ contract C // ---- // Warning: (109-119): Assertion checker does not yet support the type of this variable. // Warning: (139-142): Assertion checker does not yet support this expression. +// Warning: (139-140): Assertion checker does not yet implement type struct C.S memory // Warning: (139-151): Assertion checker does not yet implement such assignments. // Warning: (162-165): Assertion checker does not yet support this expression. +// Warning: (162-163): Assertion checker does not yet implement type struct C.S memory // Warning: (155-176): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/struct_1.sol b/test/libsolidity/smtCheckerTests/types/struct_1.sol index 936910a74..38aa311a6 100644 --- a/test/libsolidity/smtCheckerTests/types/struct_1.sol +++ b/test/libsolidity/smtCheckerTests/types/struct_1.sol @@ -16,9 +16,9 @@ contract C // ---- // Warning: (157-170): Unused local variable. // Warning: (157-170): Assertion checker does not yet support the type of this variable. -// Warning: (139-146): Assertion checker does not yet implement this type. -// Warning: (149-153): Assertion checker does not yet implement this type. +// Warning: (139-146): Assertion checker does not yet implement type struct C.S storage ref +// Warning: (149-153): Assertion checker does not yet implement type struct C.S memory // Warning: (149-153): Assertion checker does not yet implement this expression. // Warning: (139-153): Assertion checker does not yet implement type struct C.S storage ref -// Warning: (173-177): Assertion checker does not yet implement this type. +// Warning: (173-177): Assertion checker does not yet implement type struct C.S memory // Warning: (173-177): Assertion checker does not yet implement this expression. diff --git a/test/libsolidity/smtCheckerTests/types/struct_array_branches_1d.sol b/test/libsolidity/smtCheckerTests/types/struct_array_branches_1d.sol index b35bc2612..295e98788 100644 --- a/test/libsolidity/smtCheckerTests/types/struct_array_branches_1d.sol +++ b/test/libsolidity/smtCheckerTests/types/struct_array_branches_1d.sol @@ -17,14 +17,18 @@ contract C // Warning: (71-197): Function state mutability can be restricted to pure // Warning: (101-111): Assertion checker does not yet support the type of this variable. // Warning: (115-118): Assertion checker does not yet support this expression. +// Warning: (115-116): Assertion checker does not yet implement type struct C.S memory // Warning: (115-121): Assertion checker does not yet implement this expression. // Warning: (115-121): Assertion checker does not yet implement this expression. // Warning: (139-142): Assertion checker does not yet support this expression. +// Warning: (139-140): Assertion checker does not yet implement type struct C.S memory // Warning: (139-145): Assertion checker does not yet implement this expression. // Warning: (139-145): Assertion checker does not yet implement this expression. // Warning: (161-164): Assertion checker does not yet support this expression. +// Warning: (161-162): Assertion checker does not yet implement type struct C.S memory // Warning: (161-167): Assertion checker does not yet implement this expression. // Warning: (161-167): Assertion checker does not yet implement this expression. // Warning: (182-185): Assertion checker does not yet support this expression. +// Warning: (182-183): Assertion checker does not yet implement type struct C.S memory // Warning: (182-188): Assertion checker does not yet implement this expression. // Warning: (175-193): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/struct_array_branches_2d.sol b/test/libsolidity/smtCheckerTests/types/struct_array_branches_2d.sol index a50150c35..e8fbd3d15 100644 --- a/test/libsolidity/smtCheckerTests/types/struct_array_branches_2d.sol +++ b/test/libsolidity/smtCheckerTests/types/struct_array_branches_2d.sol @@ -17,14 +17,18 @@ contract C // Warning: (73-211): Function state mutability can be restricted to pure // Warning: (103-113): Assertion checker does not yet support the type of this variable. // Warning: (117-120): Assertion checker does not yet support this expression. +// Warning: (117-118): Assertion checker does not yet implement type struct C.S memory // Warning: (117-123): Assertion checker does not yet implement this expression. // Warning: (117-126): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays. // Warning: (144-147): Assertion checker does not yet support this expression. +// Warning: (144-145): Assertion checker does not yet implement type struct C.S memory // Warning: (144-150): Assertion checker does not yet implement this expression. // Warning: (144-153): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays. // Warning: (169-172): Assertion checker does not yet support this expression. +// Warning: (169-170): Assertion checker does not yet implement type struct C.S memory // Warning: (169-175): Assertion checker does not yet implement this expression. // Warning: (169-178): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays. // Warning: (193-196): Assertion checker does not yet support this expression. +// Warning: (193-194): Assertion checker does not yet implement type struct C.S memory // Warning: (193-199): Assertion checker does not yet implement this expression. // Warning: (186-207): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/struct_array_branches_3d.sol b/test/libsolidity/smtCheckerTests/types/struct_array_branches_3d.sol index 80e25b142..2ba32209e 100644 --- a/test/libsolidity/smtCheckerTests/types/struct_array_branches_3d.sol +++ b/test/libsolidity/smtCheckerTests/types/struct_array_branches_3d.sol @@ -16,14 +16,18 @@ contract C // ---- // Warning: (110-120): Assertion checker does not yet support the type of this variable. // Warning: (124-127): Assertion checker does not yet support this expression. +// Warning: (124-125): Assertion checker does not yet implement type struct C.S memory // Warning: (124-130): Assertion checker does not yet implement this expression. // Warning: (124-136): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays. // Warning: (154-157): Assertion checker does not yet support this expression. +// Warning: (154-155): Assertion checker does not yet implement type struct C.S memory // Warning: (154-160): Assertion checker does not yet implement this expression. // Warning: (154-166): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays. // Warning: (182-185): Assertion checker does not yet support this expression. +// Warning: (182-183): Assertion checker does not yet implement type struct C.S memory // Warning: (182-188): Assertion checker does not yet implement this expression. // Warning: (182-194): Assertion checker does not yet implement assignments to multi-dimensional mappings or arrays. // Warning: (209-212): Assertion checker does not yet support this expression. +// Warning: (209-210): Assertion checker does not yet implement type struct C.S memory // Warning: (209-215): Assertion checker does not yet implement this expression. // Warning: (202-226): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTestsJSON/multi.json b/test/libsolidity/smtCheckerTestsJSON/multi.json index 166a6b3c5..a5e1990f5 100644 --- a/test/libsolidity/smtCheckerTestsJSON/multi.json +++ b/test/libsolidity/smtCheckerTestsJSON/multi.json @@ -3,9 +3,9 @@ { "smtlib2responses": { - "0x5c4a8addfb72cd6eedbd143f0d402faa2833363b9c8c3f4ed5d9b01ff8fdeee0": "unsat\n", - "0xf04f3df4fcb1dcab2a20ff50621679f88608a48addeedfd3792fd652e7115d2f": "sat\n((|EVALEXPR_0| 0))\n", - "0xf7f1fe2ee1dced3b4ee90b7f1babcfb9ca520344b39c592f4a378761775705bd": "sat\n((|EVALEXPR_0| 1))\n" + "0x399638a49c613bd393612f518a0bc22e9c7801791f0fa10a760b53c88686763c": "unsat\n", + "0x91c1bd0064608eae1120536e6e62864766bc370782e162d70f05d94a9f184ffc": "sat\n((|EVALEXPR_0| 1))\n", + "0x980a3db3305233a5417ea16e6253211d98818fcaa2ce7d0858f95080160092ef": "sat\n((|EVALEXPR_0| 0))\n" } } } diff --git a/test/libsolidity/smtCheckerTestsJSON/simple.json b/test/libsolidity/smtCheckerTestsJSON/simple.json index be0911777..c085044c6 100644 --- a/test/libsolidity/smtCheckerTestsJSON/simple.json +++ b/test/libsolidity/smtCheckerTestsJSON/simple.json @@ -3,7 +3,7 @@ { "smtlib2responses": { - "0xf38a3b8e5fd03ea30ca7df1b566b1f76a5d6e0b8c46f58ff7bf576f537a4c366": "sat\n((|EVALEXPR_0| 0))\n" + "0xc1ec66473d8e3b43cd320f847166c54f779e5e905085a837418d211233144dab": "sat\n((|EVALEXPR_0| 0))\n" } } }