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

Warn about missing user-defined operator support in SMTChecker

Browse Source
This commit is contained in:
Kamil Śliwak 2023-01-28 03:20:43 +01:00
parent 2e8d50eca2
commit 5b5e853ea0
1 changed files with 31 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
libsolidity/formal/SMTEncoder.cpp
View File

@ -449,11 +449,25 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
if (_op.annotation().type->category() == Type::Category::RationalNumber) if (_op.annotation().type->category() == Type::Category::RationalNumber)
return; return;
if (TokenTraits::isBitOp(_op.getOperator())) if (TokenTraits::isBitOp(_op.getOperator()) && !*_op.annotation().userDefinedFunction)
return bitwiseNotOperation(_op); return bitwiseNotOperation(_op);
createExpr(_op); createExpr(_op);
// User-defined operators are essentially function calls.
if (*_op.annotation().userDefinedFunction)
{
// TODO: Implement user-defined operators properly.
m_errorReporter.warning(
6156_error,
_op.location(),
"User-defined operators are not yet supported by SMTChecker. "s +
"This invocation of operator " + TokenTraits::friendlyName(_op.getOperator()) +
" has been ignored, which may lead to incorrect results."
);
return;
}
auto const* subExpr = innermostTuple(_op.subExpression()); auto const* subExpr = innermostTuple(_op.subExpression());
auto type = _op.annotation().type; auto type = _op.annotation().type;
switch (_op.getOperator()) switch (_op.getOperator())
@ -524,7 +538,7 @@ bool SMTEncoder::visit(BinaryOperation const& _op)
{ {
if (shortcutRationalNumber(_op)) if (shortcutRationalNumber(_op))
return false; return false;
if (TokenTraits::isBooleanOp(_op.getOperator())) if (TokenTraits::isBooleanOp(_op.getOperator()) && !*_op.annotation().userDefinedFunction)
{ {
booleanOperation(_op); booleanOperation(_op);
return false; return false;
@ -537,11 +551,25 @@ void SMTEncoder::endVisit(BinaryOperation const& _op)
/// If _op is const evaluated the RationalNumber shortcut was taken. /// If _op is const evaluated the RationalNumber shortcut was taken.
if (isConstant(_op)) if (isConstant(_op))
return; return;
if (TokenTraits::isBooleanOp(_op.getOperator())) if (TokenTraits::isBooleanOp(_op.getOperator()) && !*_op.annotation().userDefinedFunction)
return; return;
createExpr(_op); createExpr(_op);
// User-defined operators are essentially function calls.
if (*_op.annotation().userDefinedFunction)
{
// TODO: Implement user-defined operators properly.
m_errorReporter.warning(
6756_error,
_op.location(),
"User-defined operators are not yet supported by SMTChecker. "s +
"This invocation of operator " + TokenTraits::friendlyName(_op.getOperator()) +
" has been ignored, which may lead to incorrect results."
);
return;
}
if (TokenTraits::isArithmeticOp(_op.getOperator())) if (TokenTraits::isArithmeticOp(_op.getOperator()))
arithmeticOperation(_op); arithmeticOperation(_op);
else if (TokenTraits::isCompareOp(_op.getOperator())) else if (TokenTraits::isCompareOp(_op.getOperator()))