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

Merge pull request #7022 from ethereum/smt_create_expr

Browse Source 
[SMTChecker] Always create symbolic expression
This commit is contained in:
chriseth 2019-07-02 14:07:24 +02:00 committed by GitHub
commit e542e46163
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
14 changed files with 61 additions and 41 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

50
libsolidity/formal/SMTEncoder.cpp
View File

@ -204,6 +204,8 @@ void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl)
void SMTEncoder::endVisit(Assignment const& _assignment)
{
createExpr(_assignment);
static set<Token> 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<shared_ptr<smt::SymbolicVariable>> 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<Identifier const*>(&_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<smt::SymbolicVariable> array;
if (auto const& id = dynamic_cast<Identifier const*>(&_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()
);
}

8
test/libsolidity/smtCheckerTests/complex/slither/data_dependency.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/complex/slither/external_function.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/complex/warn_on_struct.sol
View File

@ -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.

3
test/libsolidity/smtCheckerTests/operators/delete_struct.sol
View File

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

1
test/libsolidity/smtCheckerTests/types/array_literal_1.sol
View File

@ -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.

8
test/libsolidity/smtCheckerTests/types/array_struct_array_branches_2d.sol
View File

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

2
test/libsolidity/smtCheckerTests/types/enum_in_struct.sol
View File

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

6
test/libsolidity/smtCheckerTests/types/struct_1.sol
View File

@ -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.

4
test/libsolidity/smtCheckerTests/types/struct_array_branches_1d.sol
View File

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

4
test/libsolidity/smtCheckerTests/types/struct_array_branches_2d.sol
View File

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

4
test/libsolidity/smtCheckerTests/types/struct_array_branches_3d.sol
View File

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

6
test/libsolidity/smtCheckerTestsJSON/multi.json
View File

@ -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"
}
}
}

2
test/libsolidity/smtCheckerTestsJSON/simple.json
View File

@ -3,7 +3,7 @@
{
"smtlib2responses":
{
"0xf38a3b8e5fd03ea30ca7df1b566b1f76a5d6e0b8c46f58ff7bf576f537a4c366": "sat\n((|EVALEXPR_0| 0))\n"
"0xc1ec66473d8e3b43cd320f847166c54f779e5e905085a837418d211233144dab": "sat\n((|EVALEXPR_0| 0))\n"
}
}
}