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 #10207 from ethereum/smt_tests_asserts

Browse Source 
[SMTChecker] Add uncovered test and replace uncovered tests by asserts
This commit is contained in:
Leonardo 2020-12-03 08:59:48 +01:00 committed by GitHub
commit 088b694f0b
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
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()));
}
}
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<smtutil::Expression, smtutil::Expression> 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)

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

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

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

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.