cerc-io/solidity
11
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

[SMTChecker] Support bitwise or, xor and not.

Browse Source
This commit is contained in:
Djordje Mijovic
2020-08-26 11:06:56 +02:00
parent bff0f9bda7
commit 11a7763f49
18 changed files with 203 additions and 22 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTEncoder.cpp
+18 -21
View File
@@ -456,6 +456,8 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
void SMTEncoder::endVisit(UnaryOperation const& _op)
{
if (TokenTraits::isBitOp(_op.getOperator()))
return bitwiseNotOperation(_op);
if (_op.annotation().type->category() == Type::Category::RationalNumber)
return;
@@ -1406,20 +1408,7 @@ void SMTEncoder::bitwiseOperation(BinaryOperation const& _op)
auto commonType = _op.annotation().commonType;
solAssert(commonType, "");
unsigned bvSize = 256;
bool isSigned = false;
if (auto const* intType = dynamic_cast<IntegerType const*>(commonType))
{
bvSize = intType->numBits();
isSigned = intType->isSigned();
}
else if (auto const* fixedType = dynamic_cast<FixedPointType const*>(commonType))
{
bvSize = fixedType->numBits();
isSigned = fixedType->isSigned();
}
else if (auto const* fixedBytesType = dynamic_cast<FixedBytesType const*>(commonType))
bvSize = fixedBytesType->numBytes() * 8;
auto [bvSize, isSigned] = smt::typeBvSizeAndSignedness(commonType);
auto bvLeft = smtutil::Expression::int2bv(expr(_op.leftExpression(), commonType), bvSize);
auto bvRight = smtutil::Expression::int2bv(expr(_op.rightExpression(), commonType), bvSize);
@@ -1427,18 +1416,26 @@ void SMTEncoder::bitwiseOperation(BinaryOperation const& _op)
optional<smtutil::Expression> result;
if (_op.getOperator() == Token::BitAnd)
result = bvLeft & bvRight;
// TODO implement the other operators
else
m_errorReporter.warning(
1093_error,
_op.location(),
"Assertion checker does not yet implement this bitwise operator."
);
else if (_op.getOperator() == Token::BitOr)
result = bvLeft | bvRight;
else if (_op.getOperator() == Token::BitXor)
result = bvLeft ^ bvRight;
solAssert(result, "");
if (result)
defineExpr(_op, smtutil::Expression::bv2int(*result, isSigned));
}
void SMTEncoder::bitwiseNotOperation(UnaryOperation const& _op)
{
solAssert(_op.getOperator() == Token::BitNot, "");
auto [bvSize, isSigned] = smt::typeBvSizeAndSignedness(_op.annotation().type);
auto bvOperand = smtutil::Expression::int2bv(expr(_op.subExpression(), _op.annotation().type), bvSize);
defineExpr(_op, smtutil::Expression::bv2int(~bvOperand, isSigned));
}
smtutil::Expression SMTEncoder::division(smtutil::Expression _left, smtutil::Expression _right, IntegerType const& _type)
{
// Signed division in SMTLIB2 rounds differently for negative division.