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

[SMTChecker] Implementing compound bitwise And/Or/Xor operators

Browse Source
This commit is contained in:
Djordje Mijovic 2020-09-21 16:54:58 +02:00
parent 700cc4c9d3
commit 773e000227
3 changed files with 88 additions and 35 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -8,6 +8,7 @@ Compiler Features:
* SMTChecker: Support events and low-level logs.
* SMTChecker: Support ``revert()``.
* SMTChecker: Support shifts.
* SMTChecker: Support compound and, or, and xor operators.
* SMTChecker: Support structs.
* SMTChecker: Support ``type(T).min``, ``type(T).max``, and ``type(I).interfaceId``.
* Yul Optimizer: Prune unused parameters in functions.

114
libsolidity/formal/SMTEncoder.cpp
View File

@ -357,7 +357,10 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
Token::AssignSub,
Token::AssignMul,
Token::AssignDiv,
Token::AssignMod
Token::AssignMod,
Token::AssignBitAnd,
Token::AssignBitOr,
Token::AssignBitXor
};
Token op = _assignment.assignmentOperator();
if (op != Token::Assign && !compoundOps.count(op))
@ -1381,6 +1384,59 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
return {value, valueUnbounded};
}
smtutil::Expression SMTEncoder::bitwiseOperation(
Token _op,
smtutil::Expression const& _left,
smtutil::Expression const& _right,
TypePointer const& _commonType
)
{
static set<Token> validOperators{
Token::BitAnd,
Token::BitOr,
Token::BitXor,
Token::SHL,
Token::SHR,
Token::SAR
};
solAssert(validOperators.count(_op), "");
solAssert(_commonType, "");
auto [bvSize, isSigned] = smt::typeBvSizeAndSignedness(_commonType);
auto bvLeft = smtutil::Expression::int2bv(_left, bvSize);
auto bvRight = smtutil::Expression::int2bv(_right, bvSize);
optional<smtutil::Expression> result;
switch (_op)
{
case Token::BitAnd:
result = bvLeft & bvRight;
break;
case Token::BitOr:
result = bvLeft | bvRight;
break;
case Token::BitXor:
result = bvLeft ^ bvRight;
break;
case Token::SHL:
result = bvLeft << bvRight;
break;
case Token::SHR:
solAssert(false, "");
case Token::SAR:
result = isSigned ?
smtutil::Expression::ashr(bvLeft, bvRight) :
bvLeft >> bvRight;
break;
default:
solAssert(false, "");
}
solAssert(result.has_value(), "");
return smtutil::Expression::bv2int(*result, isSigned);
}
void SMTEncoder::compareOperation(BinaryOperation const& _op)
{
auto const& commonType = _op.annotation().commonType;
@ -1457,39 +1513,12 @@ void SMTEncoder::bitwiseOperation(BinaryOperation const& _op)
auto commonType = _op.annotation().commonType;
solAssert(commonType, "");
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);
optional<smtutil::Expression> result;
switch (op)
{
case Token::BitAnd:
result = bvLeft & bvRight;
break;
case Token::BitOr:
result = bvLeft | bvRight;
break;
case Token::BitXor:
result = bvLeft ^ bvRight;
break;
case Token::SHL:
result = bvLeft << bvRight;
break;
case Token::SHR:
solAssert(false, "");
case Token::SAR:
result = isSigned ?
smtutil::Expression::ashr(bvLeft, bvRight) :
bvLeft >> bvRight;
break;
default:
solAssert(false, "");
}
solAssert(result, "");
defineExpr(_op, smtutil::Expression::bv2int(*result, isSigned));
defineExpr(_op, bitwiseOperation(
_op.getOperator(),
expr(_op.leftExpression(), commonType),
expr(_op.rightExpression(), commonType),
commonType
));
}
void SMTEncoder::bitwiseNotOperation(UnaryOperation const& _op)
@ -1597,9 +1626,24 @@ smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment
{Token::AssignDiv, Token::Div},
{Token::AssignMod, Token::Mod}
};
static map<Token, Token> const compoundToBitwise{
{Token::AssignBitAnd, Token::BitAnd},
{Token::AssignBitOr, Token::BitOr},
{Token::AssignBitXor, Token::BitXor}
};
Token op = _assignment.assignmentOperator();
solAssert(compoundToArithmetic.count(op), "");
solAssert(compoundToArithmetic.count(op) || compoundToBitwise.count(op), "");
auto decl = identifierToVariable(_assignment.leftHandSide());
if (compoundToBitwise.count(op))
return bitwiseOperation(
compoundToBitwise.at(op),
decl ? currentValue(*decl) : expr(_assignment.leftHandSide()),
expr(_assignment.rightHandSide()),
_assignment.annotation().type
);
auto values = arithmeticOperation(
compoundToArithmetic.at(op),
decl ? currentValue(*decl) : expr(_assignment.leftHandSide()),

8
libsolidity/formal/SMTEncoder.h
View File

@ -119,6 +119,14 @@ protected:
TypePointer const& _commonType,
Expression const& _expression
);
smtutil::Expression bitwiseOperation(
Token _op,
smtutil::Expression const& _left,
smtutil::Expression const& _right,
TypePointer const& _commonType
);
void compareOperation(BinaryOperation const& _op);
void booleanOperation(BinaryOperation const& _op);
void bitwiseOperation(BinaryOperation const& _op);