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

Add uncovered test and replace uncovered tests by asserts

Browse Source
This commit is contained in:
Leonardo Alt 2020-11-05 13:25:15 +00:00
parent 7e7a42c6ad
commit fa561dbd0e
6 changed files with 103 additions and 100 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

133
libsolidity/formal/SMTEncoder.cpp
View File

@ -318,18 +318,12 @@ void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl)
assignment(*declarations.at(i), symbTuple->component(i, components.at(i), declarations.at(i)->type())); 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()) if (_varDecl.initialValue())
assignment(*_varDecl.declarations().front(), *_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) bool SMTEncoder::visit(Assignment const& _assignment)
@ -492,11 +486,7 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
indexOrMemberAssignment(*subExpr, newValue); indexOrMemberAssignment(*subExpr, newValue);
} }
else else
m_errorReporter.warning( solAssert(false, "");
1950_error,
_op.location(),
"Assertion checker does not yet implement such increments / decrements."
);
break; break;
} }
@ -530,11 +520,7 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
break; break;
} }
default: default:
m_errorReporter.warning( solAssert(false, "");
3682_error,
_op.location(),
"Assertion checker does not yet implement this operator."
);
} }
} }
@ -571,11 +557,7 @@ void SMTEncoder::endVisit(BinaryOperation const& _op)
else if (TokenTraits::isBitOp(_op.getOperator()) || TokenTraits::isShiftOp(_op.getOperator())) else if (TokenTraits::isBitOp(_op.getOperator()) || TokenTraits::isShiftOp(_op.getOperator()))
bitwiseOperation(_op); bitwiseOperation(_op);
else else
m_errorReporter.warning( solAssert(false, "");
3876_error,
_op.location(),
"Assertion checker does not yet implement this operator."
);
} }
bool SMTEncoder::visit(Conditional const& _op) bool SMTEncoder::visit(Conditional const& _op)
@ -1030,15 +1012,7 @@ void SMTEncoder::endVisit(Literal const& _literal)
); );
} }
else else
{ solAssert(false, "");
m_errorReporter.warning(
7885_error,
_literal.location(),
"Assertion checker does not yet support the type of this literal (" +
_literal.annotation().type->toString() +
")."
);
}
} }
void SMTEncoder::addArrayLiteralAssertions( void SMTEncoder::addArrayLiteralAssertions(
@ -1116,11 +1090,8 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
); );
} }
else else
m_errorReporter.warning( solUnimplementedAssert(false, "");
9551_error,
_memberAccess.location(),
"Assertion checker does not yet support this expression."
);
return false; return false;
} }
else if (smt::isNonRecursiveStruct(*exprType)) else if (smt::isNonRecursiveStruct(*exprType))
@ -1510,40 +1481,32 @@ void SMTEncoder::arithmeticOperation(BinaryOperation const& _op)
{ {
auto type = _op.annotation().commonType; auto type = _op.annotation().commonType;
solAssert(type, ""); 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::Add: case Token::Mul:
case Token::Sub: case Token::Div:
case Token::Mul: case Token::Mod:
case Token::Div: {
case Token::Mod: auto values = arithmeticOperation(
{ _op.getOperator(),
auto values = arithmeticOperation( expr(_op.leftExpression()),
_op.getOperator(), expr(_op.rightExpression()),
expr(_op.leftExpression()), _op.annotation().commonType,
expr(_op.rightExpression()), _op
_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() + "."
); );
defineExpr(_op, values.first);
break;
}
default:
m_errorReporter.warning(
5188_error,
_op.location(),
"Assertion checker does not yet implement this operator."
);
}
} }
pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation( pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
@ -1732,29 +1695,21 @@ void SMTEncoder::booleanOperation(BinaryOperation const& _op)
{ {
solAssert(_op.getOperator() == Token::And || _op.getOperator() == Token::Or, ""); solAssert(_op.getOperator() == Token::And || _op.getOperator() == Token::Or, "");
solAssert(_op.annotation().commonType, ""); 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 auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression())).first;
_op.leftExpression().accept(*this); mergeVariables(touchedVariables(_op.rightExpression()), !expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
if (_op.getOperator() == Token::And) 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
{
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 else
m_errorReporter.warning( {
3263_error, auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression())).first;
_op.location(), mergeVariables(touchedVariables(_op.rightExpression()), expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
"Assertion checker does not yet implement the type " + _op.annotation().commonType->toString() + " for boolean operations" defineExpr(_op, expr(_op.leftExpression()) || expr(_op.rightExpression()));
); }
} }
void SMTEncoder::bitwiseOperation(BinaryOperation const& _op) void SMTEncoder::bitwiseOperation(BinaryOperation const& _op)

13
scripts/error_codes.py
View File

@ -220,15 +220,12 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False):
return False return False
old_source_only_ids = { old_source_only_ids = {
"1123", "1220", "1584", "1823", "1950", "1123", "1220", "1584", "1823",
"1988", "2657", "2800", "1988", "2657", "2800", "3356",
"3263", "3356", "3682", "3876",
"3893", "3996", "4010", "4802", "3893", "3996", "4010", "4802",
"5073", "5188", "5272", "5073", "5272", "5622", "6272", "7128",
"5622", "6272", "7128", "7186", "7589", "7593", "7653", "8065", "8084", "8140",
"7589", "7593", "7653", "7885", "8065", "8084", "8140", "8312", "8592", "9085", "9390"
"8312", "8592", "9011",
"9085", "9390", "9551",
} }
new_source_only_ids = source_only_ids - old_source_only_ids new_source_only_ids = source_only_ids - old_source_only_ids

11
test/libsolidity/smtCheckerTests/operators/bitwise_not_fixed_bytes.sol
View File

@ -1,7 +1,12 @@
pragma experimental SMTChecker; pragma experimental SMTChecker;
contract C { contract C {
function f() public pure returns (byte) { function f() public pure {
return (~byte(0xFF)); // 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.

10
test/libsolidity/smtCheckerTests/operators/exp.sol Normal file
View File

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

15
test/libsolidity/smtCheckerTests/special/ether_units.sol Normal file
View File

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

21
test/libsolidity/smtCheckerTests/special/time_units.sol Normal file
View File

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