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

Support user defined operators in SMT

Browse Source
This commit is contained in:
Pawel Gebal 2023-08-08 17:48:38 +02:00
parent 72671d6c88
commit 6a9a0a4bea
14 changed files with 267 additions and 245 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -6,6 +6,7 @@ Language Features:
Compiler Features:
* Parser: Remove the experimental error recovery mode (``--error-recovery`` / ``settings.parserErrorRecovery``).
* SMTChecker: Support user-defined operators.
* Yul Optimizer: If ``PUSH0`` is supported, favor zero literals over storing zero values in variables.
* Yul Optimizer: Run the ``Rematerializer`` and ``UnusedPruner`` steps at the end of the default clean-up sequence.

3
libsolidity/ast/AST.h
View File

@ -2111,6 +2111,7 @@ public:
Token getOperator() const { return m_operator; }
bool isPrefixOperation() const { return m_isPrefix; }
Expression const& subExpression() const { return *m_subExpression; }
ASTPointer<Expression> const& argument() const { return m_subExpression; }
FunctionType const* userDefinedFunctionType() const;
@ -2145,6 +2146,8 @@ public:
Expression const& leftExpression() const { return *m_left; }
Expression const& rightExpression() const { return *m_right; }
ASTPointer<Expression> leftArgument() const { return m_left; }
ASTPointer<Expression> rightArgument() const { return m_right; }
Token getOperator() const { return m_operator; }
FunctionType const* userDefinedFunctionType() const;

62
libsolidity/formal/BMC.cpp
View File

@ -551,6 +551,15 @@ void BMC::endVisit(UnaryOperation const& _op)
{
SMTEncoder::endVisit(_op);
// User-defined operators are essentially function calls.
if (auto funDef = *_op.annotation().userDefinedFunction)
{
std::vector<ASTPointer<Expression const>> arguments;
arguments.push_back(_op.argument());
inlineFunctionCall(funDef, _op, &_op, _op.userDefinedFunctionType(), arguments);
return;
}
if (
_op.annotation().type->category() == Type::Category::RationalNumber ||
_op.annotation().type->category() == Type::Category::FixedPoint
@ -565,6 +574,19 @@ void BMC::endVisit(UnaryOperation const& _op)
);
}
void BMC::endVisit(BinaryOperation const& _op)
{
SMTEncoder::endVisit(_op);
if (auto funDef = *_op.annotation().userDefinedFunction)
{
std::vector<ASTPointer<Expression const>> arguments;
arguments.push_back(_op.leftArgument());
arguments.push_back(_op.rightArgument());
inlineFunctionCall(funDef, _op, &_op, _op.userDefinedFunctionType(), arguments);
}
}
void BMC::endVisit(FunctionCall const& _funCall)
{
auto functionCallKind = *_funCall.annotation().kind;
@ -674,15 +696,21 @@ void BMC::visitAddMulMod(FunctionCall const& _funCall)
SMTEncoder::visitAddMulMod(_funCall);
}
void BMC::inlineFunctionCall(FunctionCall const& _funCall)
void BMC::inlineFunctionCall(
FunctionDefinition const* _funDef,
Expression const& _callStackExpr,
Expression const* _calledExpr,
FunctionType const* _funType,
std::vector<ASTPointer<Expression const>> const& _arguments
)
{
solAssert(shouldInlineFunctionCall(_funCall, currentScopeContract(), m_currentContract), "");
auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
solAssert(funDef, "");
solAssert(_funDef, "");
solAssert(_funType, "");
solAssert(_calledExpr, "");
if (visitedFunction(funDef))
if (visitedFunction(_funDef))
{
auto const& returnParams = funDef->returnParameters();
auto const& returnParams = _funDef->returnParameters();
for (auto param: returnParams)
{
m_context.newValue(*param);
@ -691,19 +719,31 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
}
else
{
initializeFunctionCallParameters(*funDef, symbolicArguments(_funCall, m_currentContract));
initializeFunctionCallParameters(*_funDef, symbolicArguments(_funDef, _calledExpr, _funType, _arguments));
// The reason why we need to pushCallStack here instead of visit(FunctionDefinition)
// is that there we don't have `_funCall`.
pushCallStack({funDef, &_funCall});
// is that there we don't have `_callStackExpr`.
pushCallStack({_funDef, &_callStackExpr});
pushPathCondition(currentPathConditions());
auto oldChecked = std::exchange(m_checked, true);
funDef->accept(*this);
_funDef->accept(*this);
m_checked = oldChecked;
popPathCondition();
}
createReturnedExpressions(_funCall, m_currentContract);
createReturnedExpressions(_funDef, _callStackExpr);
}
void BMC::inlineFunctionCall(FunctionCall const& _funCall)
{
solAssert(shouldInlineFunctionCall(_funCall, currentScopeContract(), m_currentContract), "");
auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
Expression const* calledExpr = &_funCall.expression();
auto funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
std::vector<ASTPointer<Expression const>> arguments = _funCall.sortedArguments();
inlineFunctionCall(funDef, _funCall, calledExpr, funType, arguments);
}
void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)

8
libsolidity/formal/BMC.h
View File

@ -97,6 +97,7 @@ private:
bool visit(WhileStatement const& _node) override;
bool visit(ForStatement const& _node) override;
void endVisit(UnaryOperation const& _node) override;
void endVisit(BinaryOperation const& _node) override;
void endVisit(FunctionCall const& _node) override;
void endVisit(Return const& _node) override;
bool visit(TryStatement const& _node) override;
@ -113,6 +114,13 @@ private:
/// Visits the FunctionDefinition of the called function
/// if available and inlines the return value.
void inlineFunctionCall(FunctionCall const& _funCall);
void inlineFunctionCall(
FunctionDefinition const* _funDef,
Expression const& _callStackExpr,
Expression const* _calledExpr,
FunctionType const* _funType,
std::vector<ASTPointer<Expression const>> const& _arguments
);
/// Inlines if the function call is internal or external to `this`.
/// Erases knowledge about state variables if external.
void internalOrExternalFunctionCall(FunctionCall const& _funCall);

136
libsolidity/formal/CHC.cpp
View File

@ -543,6 +543,35 @@ void CHC::endVisit(ForStatement const& _for)
m_scopes.pop_back();
}
void CHC::endVisit(UnaryOperation const& _op)
{
SMTEncoder::endVisit(_op);
if (auto funDef = *_op.annotation().userDefinedFunction)
{
std::vector<ASTPointer<Expression const>> arguments;
arguments.push_back(_op.argument());
internalFunctionCall(funDef, &_op, _op.userDefinedFunctionType(), arguments, state().thisAddress());
createReturnedExpressions(funDef, _op);
}
}
void CHC::endVisit(BinaryOperation const& _op)
{
SMTEncoder::endVisit(_op);
if (auto funDef = *_op.annotation().userDefinedFunction)
{
std::vector<ASTPointer<Expression const>> arguments;
arguments.push_back(_op.leftArgument());
arguments.push_back(_op.rightArgument());
internalFunctionCall(funDef, &_op, _op.userDefinedFunctionType(), arguments, state().thisAddress());
createReturnedExpressions(funDef, _op);
}
}
void CHC::endVisit(FunctionCall const& _funCall)
{
auto functionCallKind = *_funCall.annotation().kind;
@ -593,8 +622,8 @@ void CHC::endVisit(FunctionCall const& _funCall)
break;
}
createReturnedExpressions(_funCall, m_currentContract);
auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
createReturnedExpressions(funDef, _funCall);
}
void CHC::endVisit(Break const& _break)
@ -820,20 +849,27 @@ void CHC::visitDeployment(FunctionCall const& _funCall)
defineExpr(_funCall, newAddr);
}
void CHC::internalFunctionCall(FunctionCall const& _funCall)
void CHC::internalFunctionCall(
FunctionDefinition const* _funDef,
Expression const* _calledExpr,
FunctionType const* _funType,
std::vector<ASTPointer<Expression const>> const& _arguments,
smtutil::Expression _contractAddressValue
)
{
solAssert(m_currentContract, "");
solAssert(_calledExpr, "");
solAssert(_funType, "");
auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
if (function)
if (_funDef)
{
if (m_currentFunction && !m_currentFunction->isConstructor())
m_callGraph[m_currentFunction].insert(function);
m_callGraph[m_currentFunction].insert(_funDef);
else
m_callGraph[m_currentContract].insert(function);
m_callGraph[m_currentContract].insert(_funDef);
}
m_context.addAssertion(predicate(_funCall));
m_context.addAssertion(predicate(_funDef, _calledExpr, _funType, _arguments, _contractAddressValue));
solAssert(m_errorDest, "");
connectBlocks(
@ -845,6 +881,37 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
m_context.addAssertion(errorFlag().increaseIndex() == 0);
}
void CHC::internalFunctionCall(FunctionCall const& _funCall)
{
solAssert(m_currentContract, "");
auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
if (funDef)
{
if (m_currentFunction && !m_currentFunction->isConstructor())
m_callGraph[m_currentFunction].insert(funDef);
else
m_callGraph[m_currentContract].insert(funDef);
}
Expression const* calledExpr = &_funCall.expression();
auto funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
std::vector<ASTPointer<Expression const>> arguments = _funCall.sortedArguments();
auto contractAddressValue = [this](FunctionCall const& _f) {
auto [callExpr, callOptions] = functionCallExpression(_f);
FunctionType const& funType = dynamic_cast<FunctionType const&>(*callExpr->annotation().type);
if (funType.kind() == FunctionType::Kind::Internal)
return state().thisAddress();
if (MemberAccess const* callBase = dynamic_cast<MemberAccess const*>(callExpr))
return expr(callBase->expression());
solAssert(false, "Unreachable!");
};
internalFunctionCall(funDef, calledExpr, funType, arguments, contractAddressValue(_funCall));
}
void CHC::addNondetCalls(ContractDefinition const& _contract)
{
for (auto var: _contract.stateVariables())
@ -1028,7 +1095,7 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
state().readStateVars(*function->annotation().contract, contractAddressValue(_funCall));
}
smtutil::Expression pred = predicate(_funCall);
smtutil::Expression pred = predicate(function, callExpr, &funType, _funCall.sortedArguments(), calledAddress);
auto txConstraints = state().txTypeConstraints() && state().txFunctionConstraints(*function);
m_context.addAssertion(pred && txConstraints);
@ -1264,6 +1331,12 @@ std::set<unsigned> CHC::transactionVerificationTargetsIds(ASTNode const* _txRoot
return verificationTargetsIds;
}
bool CHC::usesStaticCall(FunctionDefinition const* _funDef, FunctionType const* _funType)
{
auto kind = _funType->kind();
return (_funDef && (_funDef->stateMutability() == StateMutability::Pure || _funDef->stateMutability() == StateMutability::View)) || kind == FunctionType::Kind::BareStaticCall;
}
bool CHC::usesStaticCall(FunctionCall const& _funCall)
{
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
@ -1733,40 +1806,35 @@ smtutil::Expression CHC::predicate(Predicate const& _block)
solAssert(false, "");
}
smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
smtutil::Expression CHC::predicate(
FunctionDefinition const* _funDef,
Expression const* _calledExpr,
FunctionType const* _funType,
std::vector<ASTPointer<Expression const>> _arguments,
smtutil::Expression _contractAddressValue
)
{
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
auto kind = funType.kind();
solAssert(_calledExpr, "");
solAssert(_funType, "");
auto kind = _funType->kind();
solAssert(kind == FunctionType::Kind::Internal || kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
solAssert(m_currentContract, "");
auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
if (!function)
if (!_funDef)
return smtutil::Expression(true);
auto contractAddressValue = [this](FunctionCall const& _f) {
auto [callExpr, callOptions] = functionCallExpression(_f);
FunctionType const& funType = dynamic_cast<FunctionType const&>(*callExpr->annotation().type);
if (funType.kind() == FunctionType::Kind::Internal)
return state().thisAddress();
if (MemberAccess const* callBase = dynamic_cast<MemberAccess const*>(callExpr))
return expr(callBase->expression());
solAssert(false, "Unreachable!");
};
errorFlag().increaseIndex();
std::vector<smtutil::Expression> args{errorFlag().currentValue(), contractAddressValue(_funCall), state().abi(), state().crypto(), state().tx(), state().state()};
auto const* contract = function->annotation().contract;
std::vector<smtutil::Expression> args{errorFlag().currentValue(), _contractAddressValue, state().abi(), state().crypto(), state().tx(), state().state()};
auto const* contract = _funDef->annotation().contract;
auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
solAssert(kind != FunctionType::Kind::Internal || function->isFree() || (contract && contract->isLibrary()) || util::contains(hierarchy, contract), "");
solAssert(kind != FunctionType::Kind::Internal || _funDef->isFree() || (contract && contract->isLibrary()) || util::contains(hierarchy, contract), "");
if (kind == FunctionType::Kind::Internal)
contract = m_currentContract;
args += currentStateVariables(*contract);
args += symbolicArguments(_funCall, contract);
if (!usesStaticCall(_funCall))
args += symbolicArguments(_funDef, _calledExpr, _funType, _arguments);
if (!usesStaticCall(_funDef, _funType))
{
state().newState();
for (auto const& var: stateVariablesIncludingInheritedAndPrivate(*contract))
@ -1775,7 +1843,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
args += std::vector<smtutil::Expression>{state().state()};
args += currentStateVariables(*contract);
for (auto var: function->parameters() + function->returnParameters())
for (auto var: _funDef->parameters() + _funDef->returnParameters())
{
if (m_context.knownVariable(*var))
m_context.variable(*var)->increaseIndex();
@ -1784,10 +1852,10 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
args.push_back(currentValue(*var));
}
Predicate const& summary = *m_summaries.at(contract).at(function);
Predicate const& summary = *m_summaries.at(contract).at(_funDef);
auto from = smt::function(summary, contract, m_context);
Predicate const& callPredicate = *createSummaryBlock(
*function,
*_funDef,
*contract,
kind == FunctionType::Kind::Internal ? PredicateType::InternalCall : PredicateType::ExternalCallTrusted
);

18
libsolidity/formal/CHC.h
View File

@ -111,6 +111,8 @@ private:
bool visit(ForStatement const&) override;
void endVisit(ForStatement const&) override;
void endVisit(FunctionCall const& _node) override;
void endVisit(BinaryOperation const& _op) override;
void endVisit(UnaryOperation const& _op) override;
void endVisit(Break const& _node) override;
void endVisit(Continue const& _node) override;
void endVisit(IndexRangeAccess const& _node) override;
@ -127,6 +129,13 @@ private:
void visitAddMulMod(FunctionCall const& _funCall) override;
void visitDeployment(FunctionCall const& _funCall);
void internalFunctionCall(FunctionCall const& _funCall);
void internalFunctionCall(
FunctionDefinition const* _funDef,
Expression const* _calledExpr,
FunctionType const* _funType,
std::vector<ASTPointer<Expression const>> const& _arguments,
smtutil::Expression _contractAddressValue
);
void externalFunctionCall(FunctionCall const& _funCall);
void externalFunctionCallToTrustedCode(FunctionCall const& _funCall);
void addNondetCalls(ContractDefinition const& _contract);
@ -152,6 +161,7 @@ private:
void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override;
void setCurrentBlock(Predicate const& _block);
std::set<unsigned> transactionVerificationTargetsIds(ASTNode const* _txRoot);
bool usesStaticCall(FunctionDefinition const* _funDef, FunctionType const* _funType);
bool usesStaticCall(FunctionCall const& _funCall);
//@}
@ -246,7 +256,13 @@ private:
/// @returns a predicate application after checking the predicate's type.
smtutil::Expression predicate(Predicate const& _block);
/// @returns the summary predicate for the called function.
smtutil::Expression predicate(FunctionCall const& _funCall);
smtutil::Expression predicate(
FunctionDefinition const* _funDef,
Expression const* _calledExpr,
FunctionType const* _funType,
std::vector<ASTPointer<Expression const>> _arguments,
smtutil::Expression _contractAddressValue
);
/// @returns a predicate that defines a contract initializer for _contract in the context of _contractContext.
smtutil::Expression initializer(ContractDefinition const& _contract, ContractDefinition const& _contractContext);
/// @returns a predicate that defines a constructor summary.

58
libsolidity/formal/SMTEncoder.cpp
View File

@ -459,17 +459,7 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
// User-defined operators are essentially function calls.
if (*_op.annotation().userDefinedFunction)
{
// TODO: Implement user-defined operators properly.
m_unsupportedErrors.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 type = _op.annotation().type;
@ -561,17 +551,7 @@ void SMTEncoder::endVisit(BinaryOperation const& _op)
// User-defined operators are essentially function calls.
if (*_op.annotation().userDefinedFunction)
{
// TODO: Implement user-defined operators properly.
m_unsupportedErrors.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()))
arithmeticOperation(_op);
@ -3141,47 +3121,45 @@ std::set<SourceUnit const*, ASTNode::CompareByID> SMTEncoder::sourceDependencies
return sources;
}
void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall, ContractDefinition const* _contextContract)
void SMTEncoder::createReturnedExpressions(FunctionDefinition const* _funDef, Expression const& _callStackExpr)
{
auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), _contextContract);
if (!funDef)
if (!_funDef)
return;
auto const& returnParams = funDef->returnParameters();
auto const& returnParams = _funDef->returnParameters();
for (auto param: returnParams)
createVariable(*param);
auto returnValues = applyMap(returnParams, [this](auto const& param) -> std::optional<smtutil::Expression> {
solAssert(param && m_context.knownVariable(*param), "");
return currentValue(*param);
});
defineExpr(_funCall, returnValues);
defineExpr(_callStackExpr, returnValues);
}
std::vector<smtutil::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contextContract)
std::vector<smtutil::Expression> SMTEncoder::symbolicArguments(
FunctionDefinition const* _funDef,
Expression const* _calledExpr,
FunctionType const* _funType,
std::vector<ASTPointer<Expression const>> const& _arguments)
{
auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), _contextContract);
solAssert(funDef, "");
solAssert(_funDef, "");
solAssert(_funType, "");
std::vector<smtutil::Expression> args;
Expression const* calledExpr = &_funCall.expression();
auto funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
solAssert(funType, "");
std::vector<ASTPointer<Expression const>> arguments = _funCall.sortedArguments();
auto functionParams = funDef->parameters();
auto functionParams = _funDef->parameters();
unsigned firstParam = 0;
if (funType->hasBoundFirstArgument())
if (_funType->hasBoundFirstArgument())
{
calledExpr = innermostTuple(*calledExpr);
auto const& attachedFunction = dynamic_cast<MemberAccess const*>(calledExpr);
_calledExpr = innermostTuple(*_calledExpr);
auto const& attachedFunction = dynamic_cast<MemberAccess const*>(_calledExpr);
solAssert(attachedFunction, "");
args.push_back(expr(attachedFunction->expression(), functionParams.front()->type()));
firstParam = 1;
}
solAssert((arguments.size() + firstParam) == functionParams.size(), "");
for (unsigned i = 0; i < arguments.size(); ++i)
args.push_back(expr(*arguments.at(i), functionParams.at(i + firstParam)->type()));
solAssert((_arguments.size() + firstParam) == functionParams.size(), "");
for (unsigned i = 0; i < _arguments.size(); ++i)
args.push_back(expr(*_arguments.at(i), functionParams.at(i + firstParam)->type()));
return args;
}

9
libsolidity/formal/SMTEncoder.h
View File

@ -403,12 +403,17 @@ protected:
/// Creates symbolic expressions for the returned values
/// and set them as the components of the symbolic tuple.
void createReturnedExpressions(FunctionCall const& _funCall, ContractDefinition const* _contextContract);
void createReturnedExpressions(FunctionDefinition const* _funDef, Expression const& _calledExpr);
/// @returns the symbolic arguments for a function call,
/// taking into account attached functions and
/// type conversion.
std::vector<smtutil::Expression> symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contextContract);
std::vector<smtutil::Expression> symbolicArguments(
FunctionDefinition const* _funDef,
Expression const* _calledExpr,
FunctionType const* _funType,
std::vector<ASTPointer<Expression const>> const& _arguments
);
smtutil::Expression constantExpr(Expression const& _expr, VariableDeclaration const& _var);

6
test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_division_same_as_builtin.sol
View File

@ -2,15 +2,15 @@ type U is uint;
using {div as /} for U global;
function div(U x, U y) pure returns (U) {
return U.wrap(U.unwrap(x) / U.unwrap(y));
return U.wrap(U.unwrap(x) / U.unwrap(y)); // detects division by zero
}
contract C {
function f(U x, U y) public pure returns (U) {
return x / y; // FIXME: should detect div by zero
return x / y; // reports division by zero in the implementation
}
}
// ====
// SMTEngine: all
// ----
// Warning 6756: (218-223): User-defined operators are not yet supported by SMTChecker. This invocation of operator / has been ignored, which may lead to incorrect results.
// Warning 4281: (108-133): CHC: Division by zero happens here.

2
test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_division_with_safe_division_by_zero.sol
View File

@ -16,4 +16,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6756: (271-276): User-defined operators are not yet supported by SMTChecker. This invocation of operator / has been ignored, which may lead to incorrect results.
// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

76
test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operations_on_constants.sol
View File

@ -33,72 +33,32 @@ contract C {
I16 constant FOUR = I16.wrap(4);
function testBitwise() public pure {
assert(ONE | TWO == THREE); // FIXME: should hold
assert(ONE & THREE == ZERO); // FIXME: should hold
assert(TWO ^ TWO == ZERO); // FIXME: should hold
assert(~ONE == MINUS_TWO); // FIXME: should hold
assert(ONE | TWO == THREE);
assert(ONE & THREE == ONE);
assert(TWO ^ TWO == ZERO);
assert(~ONE == MINUS_TWO);
}
function testArithmetic() public pure {
assert(TWO + TWO == FOUR); // FIXME: should hold
assert(TWO - TWO == ZERO); // FIXME: should hold
assert(-TWO == MINUS_TWO); // FIXME: should hold
assert(TWO * TWO == FOUR); // FIXME: should hold
assert(TWO / TWO == ONE); // FIXME: should hold
assert(TWO % TWO == ZERO); // FIXME: should hold
assert(TWO + TWO == FOUR);
assert(TWO - TWO == ZERO);
assert(-TWO == MINUS_TWO);
assert(TWO * TWO == FOUR);
assert(TWO / TWO == ONE);
assert(TWO % TWO == ZERO);
}
function testComparison() public pure {
assert(TWO == TWO); // FIXME: should hold
assert(!(TWO != TWO)); // FIXME: should hold
assert(!(TWO < TWO)); // FIXME: should hold
assert(!(TWO > TWO)); // FIXME: should hold
assert(TWO <= TWO); // FIXME: should hold
assert(TWO >= TWO); // FIXME: should hold
assert(TWO == TWO);
assert(!(TWO != TWO));
assert(!(TWO < TWO));
assert(!(TWO > TWO));
assert(TWO <= TWO);
assert(TWO >= TWO);
}
}
// ====
// SMTEngine: all
// ----
// Warning 6756: (2019-2028): User-defined operators are not yet supported by SMTChecker. This invocation of operator | has been ignored, which may lead to incorrect results.
// Warning 6756: (2019-2037): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2077-2088): User-defined operators are not yet supported by SMTChecker. This invocation of operator & has been ignored, which may lead to incorrect results.
// Warning 6756: (2077-2096): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2136-2145): User-defined operators are not yet supported by SMTChecker. This invocation of operator ^ has been ignored, which may lead to incorrect results.
// Warning 6756: (2136-2153): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6156: (2193-2197): User-defined operators are not yet supported by SMTChecker. This invocation of operator ~ has been ignored, which may lead to incorrect results.
// Warning 6756: (2193-2210): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2301-2310): User-defined operators are not yet supported by SMTChecker. This invocation of operator + has been ignored, which may lead to incorrect results.
// Warning 6756: (2301-2318): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2358-2367): User-defined operators are not yet supported by SMTChecker. This invocation of operator - has been ignored, which may lead to incorrect results.
// Warning 6756: (2358-2375): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6156: (2415-2419): User-defined operators are not yet supported by SMTChecker. This invocation of operator - has been ignored, which may lead to incorrect results.
// Warning 6756: (2415-2432): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2472-2481): User-defined operators are not yet supported by SMTChecker. This invocation of operator * has been ignored, which may lead to incorrect results.
// Warning 6756: (2472-2489): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2529-2538): User-defined operators are not yet supported by SMTChecker. This invocation of operator / has been ignored, which may lead to incorrect results.
// Warning 6756: (2529-2545): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2585-2594): User-defined operators are not yet supported by SMTChecker. This invocation of operator % has been ignored, which may lead to incorrect results.
// Warning 6756: (2585-2602): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2693-2703): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2745-2755): User-defined operators are not yet supported by SMTChecker. This invocation of operator != has been ignored, which may lead to incorrect results.
// Warning 6756: (2798-2807): User-defined operators are not yet supported by SMTChecker. This invocation of operator < has been ignored, which may lead to incorrect results.
// Warning 6756: (2850-2859): User-defined operators are not yet supported by SMTChecker. This invocation of operator > has been ignored, which may lead to incorrect results.
// Warning 6756: (2900-2910): User-defined operators are not yet supported by SMTChecker. This invocation of operator <= has been ignored, which may lead to incorrect results.
// Warning 6756: (2950-2960): User-defined operators are not yet supported by SMTChecker. This invocation of operator >= has been ignored, which may lead to incorrect results.
// Warning 6328: (2012-2038): CHC: Assertion violation happens here.
// Warning 6328: (2070-2097): CHC: Assertion violation happens here.
// Warning 6328: (2129-2154): CHC: Assertion violation happens here.
// Warning 6328: (2186-2211): CHC: Assertion violation happens here.
// Warning 6328: (2294-2319): CHC: Assertion violation happens here.
// Warning 6328: (2351-2376): CHC: Assertion violation happens here.
// Warning 6328: (2408-2433): CHC: Assertion violation happens here.
// Warning 6328: (2465-2490): CHC: Assertion violation happens here.
// Warning 6328: (2522-2546): CHC: Assertion violation happens here.
// Warning 6328: (2578-2603): CHC: Assertion violation happens here.
// Warning 6328: (2686-2704): CHC: Assertion violation happens here.
// Warning 6328: (2736-2757): CHC: Assertion violation happens here.
// Warning 6328: (2789-2809): CHC: Assertion violation happens here.
// Warning 6328: (2841-2861): CHC: Assertion violation happens here.
// Warning 6328: (2893-2911): CHC: Assertion violation happens here.
// Warning 6328: (2943-2961): CHC: Assertion violation happens here.
// Info 1391: CHC: 21 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

27
test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operations_on_constants_fail.sol
View File

@ -60,32 +60,6 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6756: (2019-2028): User-defined operators are not yet supported by SMTChecker. This invocation of operator | has been ignored, which may lead to incorrect results.
// Warning 6756: (2019-2036): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2069-2080): User-defined operators are not yet supported by SMTChecker. This invocation of operator & has been ignored, which may lead to incorrect results.
// Warning 6756: (2069-2088): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2121-2130): User-defined operators are not yet supported by SMTChecker. This invocation of operator ^ has been ignored, which may lead to incorrect results.
// Warning 6756: (2121-2138): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6156: (2171-2175): User-defined operators are not yet supported by SMTChecker. This invocation of operator ~ has been ignored, which may lead to incorrect results.
// Warning 6756: (2171-2183): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2267-2278): User-defined operators are not yet supported by SMTChecker. This invocation of operator + has been ignored, which may lead to incorrect results.
// Warning 6756: (2267-2286): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2319-2328): User-defined operators are not yet supported by SMTChecker. This invocation of operator - has been ignored, which may lead to incorrect results.
// Warning 6756: (2319-2336): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6156: (2369-2373): User-defined operators are not yet supported by SMTChecker. This invocation of operator - has been ignored, which may lead to incorrect results.
// Warning 6756: (2369-2381): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2414-2425): User-defined operators are not yet supported by SMTChecker. This invocation of operator * has been ignored, which may lead to incorrect results.
// Warning 6756: (2414-2433): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2466-2475): User-defined operators are not yet supported by SMTChecker. This invocation of operator / has been ignored, which may lead to incorrect results.
// Warning 6756: (2466-2483): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2516-2525): User-defined operators are not yet supported by SMTChecker. This invocation of operator % has been ignored, which may lead to incorrect results.
// Warning 6756: (2516-2533): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2619-2629): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2663-2673): User-defined operators are not yet supported by SMTChecker. This invocation of operator != has been ignored, which may lead to incorrect results.
// Warning 6756: (2706-2715): User-defined operators are not yet supported by SMTChecker. This invocation of operator < has been ignored, which may lead to incorrect results.
// Warning 6756: (2748-2757): User-defined operators are not yet supported by SMTChecker. This invocation of operator > has been ignored, which may lead to incorrect results.
// Warning 6756: (2792-2802): User-defined operators are not yet supported by SMTChecker. This invocation of operator <= has been ignored, which may lead to incorrect results.
// Warning 6756: (2838-2848): User-defined operators are not yet supported by SMTChecker. This invocation of operator >= has been ignored, which may lead to incorrect results.
// Warning 6328: (2012-2037): CHC: Assertion violation happens here.
// Warning 6328: (2062-2089): CHC: Assertion violation happens here.
// Warning 6328: (2114-2139): CHC: Assertion violation happens here.
@ -102,3 +76,4 @@ contract C {
// Warning 6328: (2741-2758): CHC: Assertion violation happens here.
// Warning 6328: (2783-2804): CHC: Assertion violation happens here.
// Warning 6328: (2829-2850): CHC: Assertion violation happens here.
// Info 1391: CHC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

98
test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_operator_matches_equivalent_function_call.sol
View File

@ -17,6 +17,7 @@ function mul(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) *
function div(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) / I16.unwrap(y)); }
function mod(I16 x, I16 y) pure returns (I16) { return I16.wrap(I16.unwrap(x) % I16.unwrap(y)); }
function eq(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) == I16.unwrap(y); }
function noteq(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) != I16.unwrap(y); }
function lt(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) < I16.unwrap(y); }
@ -26,81 +27,48 @@ function geq(I16 x, I16 y) pure returns (bool) { return I16.unwrap(x) >= I16.unw
contract C {
function testBitwise(I16 x, I16 y) public pure {
assert(x | y == bitor(x, y)); // FIXME: should hold
assert(x & y == bitand(x, y)); // FIXME: should hold
assert(x ^ y == bitxor(x, y)); // FIXME: should hold
assert(~x == bitnot(x)); // FIXME: should hold
assert(x | y == bitor(x, y)); // should hold
assert(x & y == bitand(x, y)); // should hold
assert(x ^ y == bitxor(x, y)); // should hold
assert(~x == bitnot(x)); // should hold
}
function testArithmetic(I16 x, I16 y) public pure {
assert(x + y == add(x, y)); // FIXME: should hold
assert(x - y == sub(x, y)); // FIXME: should hold
assert(-x == unsub(x)); // FIXME: should hold
assert(x * y == mul(x, y)); // FIXME: should hold
assert(x / y == div(x, y)); // FIXME: should hold
assert(x % y == mod(x, y)); // FIXME: should hold
assert(x + y == add(x, y));
assert(x - y == sub(x, y));
assert(-x == unsub(x));
assert(x * y == mul(x, y));
assert(x / y == div(x, y));
assert(x % y == mod(x, y));
}
function testComparison(I16 x, I16 y) public pure {
assert((x == y) == eq(x, y)); // FIXME: should hold
assert((x != y) == noteq(x, y)); // FIXME: should hold
assert((x < y) == lt(x, y)); // FIXME: should hold
assert((x > y) == gt(x, y)); // FIXME: should hold
assert((x <= y) == leq(x, y)); // FIXME: should hold
assert((x >= y) == geq(x, y)); // FIXME: should hold
assert((x == y) == eq(x, y)); // should hold
assert((x != y) == noteq(x, y)); // should hold
assert((x < y) == lt(x, y)); // should hold
assert((x > y) == gt(x, y)); // should hold
assert((x <= y) == leq(x, y)); // should hold
assert((x >= y) == geq(x, y)); // should hold
}
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// ----
// Warning 6756: (1803-1808): User-defined operators are not yet supported by SMTChecker. This invocation of operator | has been ignored, which may lead to incorrect results.
// Warning 6756: (1803-1823): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (1863-1868): User-defined operators are not yet supported by SMTChecker. This invocation of operator & has been ignored, which may lead to incorrect results.
// Warning 6756: (1863-1884): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (1924-1929): User-defined operators are not yet supported by SMTChecker. This invocation of operator ^ has been ignored, which may lead to incorrect results.
// Warning 6756: (1924-1945): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6156: (1985-1987): User-defined operators are not yet supported by SMTChecker. This invocation of operator ~ has been ignored, which may lead to incorrect results.
// Warning 6756: (1985-2000): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2103-2108): User-defined operators are not yet supported by SMTChecker. This invocation of operator + has been ignored, which may lead to incorrect results.
// Warning 6756: (2103-2121): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2161-2166): User-defined operators are not yet supported by SMTChecker. This invocation of operator - has been ignored, which may lead to incorrect results.
// Warning 6756: (2161-2179): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6156: (2219-2221): User-defined operators are not yet supported by SMTChecker. This invocation of operator - has been ignored, which may lead to incorrect results.
// Warning 6756: (2219-2233): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2273-2278): User-defined operators are not yet supported by SMTChecker. This invocation of operator * has been ignored, which may lead to incorrect results.
// Warning 6756: (2273-2291): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2331-2336): User-defined operators are not yet supported by SMTChecker. This invocation of operator / has been ignored, which may lead to incorrect results.
// Warning 6756: (2331-2349): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2389-2394): User-defined operators are not yet supported by SMTChecker. This invocation of operator % has been ignored, which may lead to incorrect results.
// Warning 6756: (2389-2407): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2511-2517): User-defined operators are not yet supported by SMTChecker. This invocation of operator == has been ignored, which may lead to incorrect results.
// Warning 6756: (2571-2577): User-defined operators are not yet supported by SMTChecker. This invocation of operator != has been ignored, which may lead to incorrect results.
// Warning 6756: (2634-2639): User-defined operators are not yet supported by SMTChecker. This invocation of operator < has been ignored, which may lead to incorrect results.
// Warning 6756: (2693-2698): User-defined operators are not yet supported by SMTChecker. This invocation of operator > has been ignored, which may lead to incorrect results.
// Warning 6756: (2752-2758): User-defined operators are not yet supported by SMTChecker. This invocation of operator <= has been ignored, which may lead to incorrect results.
// Warning 6756: (2813-2819): User-defined operators are not yet supported by SMTChecker. This invocation of operator >= has been ignored, which may lead to incorrect results.
// Warning 3944: (679-708): CHC: Underflow (resulting value less than -32768) happens here.
// Warning 4984: (679-708): CHC: Overflow (resulting value larger than 32767) happens here.
// Warning 3944: (679-708): CHC: Underflow (resulting value less than -32768) might happen here.
// Warning 4984: (679-708): CHC: Overflow (resulting value larger than 32767) might happen here.
// Warning 3944: (777-806): CHC: Underflow (resulting value less than -32768) happens here.
// Warning 4984: (777-806): CHC: Overflow (resulting value larger than 32767) happens here.
// Warning 3944: (953-982): CHC: Underflow (resulting value less than -32768) happens here.
// Warning 4984: (953-982): CHC: Overflow (resulting value larger than 32767) happens here.
// Warning 4281: (1051-1080): CHC: Division by zero happens here.
// Warning 4984: (777-806): CHC: Overflow (resulting value larger than 32767) might happen here.
// Warning 3944: (953-982): CHC: Underflow (resulting value less than -32768) might happen here.
// Warning 4984: (953-982): CHC: Overflow (resulting value larger than 32767) might happen here.
// Warning 4984: (1051-1080): CHC: Overflow (resulting value larger than 32767) might happen here.
// Warning 4281: (1051-1080): CHC: Division by zero might happen here.
// Warning 4281: (1149-1178): CHC: Division by zero happens here.
// Warning 6328: (1796-1824): CHC: Assertion violation happens here.
// Warning 6328: (1856-1885): CHC: Assertion violation happens here.
// Warning 6328: (1917-1946): CHC: Assertion violation happens here.
// Warning 6328: (1978-2001): CHC: Assertion violation happens here.
// Warning 6328: (2096-2122): CHC: Assertion violation happens here.
// Warning 6328: (2154-2180): CHC: Assertion violation happens here.
// Warning 6328: (2212-2234): CHC: Assertion violation happens here.
// Warning 6328: (2266-2292): CHC: Assertion violation happens here.
// Warning 6328: (2324-2350): CHC: Assertion violation happens here.
// Warning 6328: (2382-2408): CHC: Assertion violation happens here.
// Warning 6328: (2503-2531): CHC: Assertion violation happens here.
// Warning 6328: (2563-2594): CHC: Assertion violation happens here.
// Warning 6328: (2626-2653): CHC: Assertion violation happens here.
// Warning 6328: (2685-2712): CHC: Assertion violation happens here.
// Warning 6328: (2744-2773): CHC: Assertion violation happens here.
// Warning 6328: (2805-2834): CHC: Assertion violation happens here.
// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
// Warning 6328: (2105-2131): CHC: Assertion violation might happen here.
// Warning 6328: (2141-2163): CHC: Assertion violation might happen here.
// Warning 6328: (2209-2235): CHC: Assertion violation might happen here.
// Warning 6328: (2245-2271): CHC: Assertion violation might happen here.
// Info 1391: CHC: 12 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
// Warning 3046: (1051-1080): BMC: Division by zero happens here.
// Warning 7812: (2245-2271): BMC: Assertion violation might happen here.
// Info 6002: BMC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

8
test/libsolidity/smtCheckerTests/operators/userDefined/user_defined_overflow.sol
View File

@ -2,14 +2,14 @@ type U8 is uint8;
using {add as +} for U8 global;
function add(U8 x, U8 y) pure returns (U8) {
return U8.wrap(U8.unwrap(x) + U8.unwrap(y)); // FIXME: should detect possible overflow here
return U8.wrap(U8.unwrap(x) + U8.unwrap(y)); // overflow detected
}
contract C {
U8 x = U8.wrap(254);
U8 x = U8.wrap(255);
function inc() public {
x = x + U8.wrap(1); // FIXME: should detect possible overflow here
x = x + U8.wrap(1);
}
function check() view public {
@ -20,5 +20,5 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6756: (274-288): User-defined operators are not yet supported by SMTChecker. This invocation of operator + has been ignored, which may lead to incorrect results.
// Warning 4984: (115-142): CHC: Overflow (resulting value larger than 255) happens here.
// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.