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] Support user types

Browse Source
This commit is contained in:
Leo Alt 2021-09-17 21:28:07 +02:00
parent 659498ff50
commit e74f853c6b
23 changed files with 462 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -14,6 +14,7 @@ Compiler Features:
* SMTChecker: Add constraints to better correlate ``address(this).balance`` and ``msg.value``.
* SMTChecker: Support the ``value`` option for external function calls.
* SMTChecker: Support constants via modules.
* SMTChecker: Support user defined value types.
Bugfixes:

2
libsolidity/formal/BMC.cpp
View File

@ -483,6 +483,8 @@ void BMC::endVisit(FunctionCall const& _funCall)
case FunctionType::Kind::BlockHash:
case FunctionType::Kind::AddMod:
case FunctionType::Kind::MulMod:
case FunctionType::Kind::Unwrap:
case FunctionType::Kind::Wrap:
[[fallthrough]];
default:
SMTEncoder::endVisit(_funCall);

2
libsolidity/formal/CHC.cpp
View File

@ -553,6 +553,8 @@ void CHC::endVisit(FunctionCall const& _funCall)
case FunctionType::Kind::BlockHash:
case FunctionType::Kind::AddMod:
case FunctionType::Kind::MulMod:
case FunctionType::Kind::Unwrap:
case FunctionType::Kind::Wrap:
[[fallthrough]];
default:
SMTEncoder::endVisit(_funCall);

6
libsolidity/formal/Predicate.cpp
View File

@ -237,7 +237,7 @@ string Predicate::formatSummaryCall(
auto last = first + static_cast<int>(fun->parameters().size());
solAssert(first >= _args.begin() && first <= _args.end(), "");
solAssert(last >= _args.begin() && last <= _args.end(), "");
auto inTypes = FunctionType(*fun).parameterTypes();
auto inTypes = SMTEncoder::replaceUserTypes(FunctionType(*fun).parameterTypes());
vector<optional<string>> functionArgsCex = formatExpressions(vector<smtutil::Expression>(first, last), inTypes);
vector<string> functionArgs;
@ -317,7 +317,7 @@ vector<optional<string>> Predicate::summaryPostInputValues(vector<smtutil::Expre
vector<smtutil::Expression> inValues(first, last);
solAssert(inValues.size() == inParams.size(), "");
auto inTypes = FunctionType(*function).parameterTypes();
auto inTypes = SMTEncoder::replaceUserTypes(FunctionType(*function).parameterTypes());
return formatExpressions(inValues, inTypes);
}
@ -339,7 +339,7 @@ vector<optional<string>> Predicate::summaryPostOutputValues(vector<smtutil::Expr
vector<smtutil::Expression> outValues(first, _args.end());
solAssert(outValues.size() == function->returnParameters().size(), "");
auto outTypes = FunctionType(*function).returnParameterTypes();
auto outTypes = SMTEncoder::replaceUserTypes(FunctionType(*function).returnParameterTypes());
return formatExpressions(outValues, outTypes);
}

68
libsolidity/formal/SMTEncoder.cpp
View File

@ -370,7 +370,7 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
Token op = _assignment.assignmentOperator();
solAssert(TokenTraits::isAssignmentOp(op), "");
if (!smt::isSupportedType(*_assignment.annotation().type))
if (!isSupportedType(*_assignment.annotation().type))
{
// Give it a new index anyway to keep the SSA scheme sound.
@ -406,6 +406,9 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
if (_tuple.annotation().type->category() == Type::Category::Function)
return;
if (_tuple.annotation().type->category() == Type::Category::TypeType)
return;
createExpr(_tuple);
if (_tuple.isInlineArray())
@ -575,6 +578,17 @@ bool SMTEncoder::visit(FunctionCall const& _funCall)
arg->accept(*this);
return false;
}
// We do not really need to visit the expression in a wrap/unwrap no-op call,
// so we just ignore the function call expression to avoid "unsupported" warnings.
else if (
funType.kind() == FunctionType::Kind::Wrap ||
funType.kind() == FunctionType::Kind::Unwrap
)
{
if (auto arg = _funCall.arguments().front())
arg->accept(*this);
return false;
}
return true;
}
@ -641,6 +655,10 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
case FunctionType::Kind::MulMod:
visitAddMulMod(_funCall);
break;
case FunctionType::Kind::Unwrap:
case FunctionType::Kind::Wrap:
visitWrapUnwrap(_funCall);
break;
case FunctionType::Kind::Send:
case FunctionType::Kind::Transfer:
{
@ -846,6 +864,13 @@ void SMTEncoder::visitAddMulMod(FunctionCall const& _funCall)
defineExpr(_funCall, divModWithSlacks(x * y, k, intType).second);
}
void SMTEncoder::visitWrapUnwrap(FunctionCall const& _funCall)
{
auto const& args = _funCall.arguments();
solAssert(args.size() == 1, "");
defineExpr(_funCall, expr(*args.front()));
}
void SMTEncoder::visitObjectCreation(FunctionCall const& _funCall)
{
auto const& args = _funCall.arguments();
@ -889,6 +914,9 @@ void SMTEncoder::endVisit(Identifier const& _identifier)
// Ignore module identifiers
else if (dynamic_cast<ModuleType const*>(_identifier.annotation().type))
return;
// Ignore user defined value type identifiers
else if (dynamic_cast<UserDefinedValueType const*>(_identifier.annotation().type))
return;
// Ignore the builtin abi, it is handled in FunctionCall.
// TODO: ignore MagicType in general (abi, block, msg, tx, type)
else if (auto magicType = dynamic_cast<MagicType const*>(_identifier.annotation().type); magicType && magicType->kind() == MagicType::Kind::ABI)
@ -944,7 +972,7 @@ void SMTEncoder::visitPublicGetter(FunctionCall const& _funCall)
auto var = dynamic_cast<VariableDeclaration const*>(access.annotation().referencedDeclaration);
solAssert(var, "");
solAssert(m_context.knownExpression(_funCall), "");
auto paramExpectedTypes = FunctionType(*var).parameterTypes();
auto paramExpectedTypes = replaceUserTypes(FunctionType(*var).parameterTypes());
auto actualArguments = _funCall.arguments();
solAssert(actualArguments.size() == paramExpectedTypes.size(), "");
deque<smtutil::Expression> symbArguments;
@ -1164,7 +1192,7 @@ void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
void SMTEncoder::visitFunctionIdentifier(Identifier const& _identifier)
{
auto const& fType = dynamic_cast<FunctionType const&>(*_identifier.annotation().type);
if (fType.returnParameterTypes().size() == 1)
if (replaceUserTypes(fType.returnParameterTypes()).size() == 1)
{
defineGlobalVariable(fType.identifier(), _identifier);
m_context.createExpression(_identifier, m_context.globalSymbol(fType.identifier()));
@ -1647,7 +1675,7 @@ void SMTEncoder::defineGlobalVariable(string const& _name, Expression const& _ex
m_context.globalSymbol(_name)->increaseIndex();
// The default behavior is not to increase the index since
// most of the global values stay the same throughout a tx.
if (smt::isSupportedType(*_expr.annotation().type))
if (isSupportedType(*_expr.annotation().type))
defineExpr(_expr, m_context.globalSymbol(_name)->currentValue());
}
@ -1843,9 +1871,10 @@ smtutil::Expression SMTEncoder::bitwiseOperation(
void SMTEncoder::compareOperation(BinaryOperation const& _op)
{
auto const& commonType = _op.annotation().commonType;
auto commonType = _op.annotation().commonType;
solAssert(commonType, "");
if (smt::isSupportedType(*commonType))
if (isSupportedType(*commonType))
{
smtutil::Expression left(expr(_op.leftExpression(), commonType));
smtutil::Expression right(expr(_op.rightExpression(), commonType));
@ -1978,7 +2007,7 @@ void SMTEncoder::assignment(
Expression const* left = cleanExpression(_left);
if (!smt::isSupportedType(*_type))
if (!isSupportedType(*_type))
{
// Give it a new index anyway to keep the SSA scheme sound.
if (auto varDecl = identifierToVariable(*left))
@ -2019,7 +2048,7 @@ void SMTEncoder::assignment(
}
else if (funType->kind() == FunctionType::Kind::Internal)
{
for (auto type: funType->returnParameterTypes())
for (auto type: replaceUserTypes(funType->returnParameterTypes()))
if (type->category() == Type::Category::Mapping || dynamic_cast<ReferenceType const*>(type))
resetReferences(type);
}
@ -2356,6 +2385,11 @@ bool SMTEncoder::sameTypeOrSubtype(Type const* _a, Type const* _b)
return false;
}
bool SMTEncoder::isSupportedType(Type const& _type) const
{
return smt::isSupportedType(*underlyingType(&_type));
}
Type const* SMTEncoder::typeWithoutPointer(Type const* _type)
{
if (auto refType = dynamic_cast<ReferenceType const*>(_type))
@ -2417,7 +2451,7 @@ smtutil::Expression SMTEncoder::expr(Expression const& _e, Type const* _targetTy
createExpr(_e);
}
return m_context.expression(_e)->currentValue(_targetType);
return m_context.expression(_e)->currentValue(underlyingType(_targetType));
}
void SMTEncoder::createExpr(Expression const& _e)
@ -2608,6 +2642,22 @@ Expression const* SMTEncoder::innermostTuple(Expression const& _expr)
return expr;
}
Type const* SMTEncoder::underlyingType(Type const* _type)
{
if (auto userType = dynamic_cast<UserDefinedValueType const*>(_type))
_type = &userType->underlyingType();
return _type;
}
TypePointers SMTEncoder::replaceUserTypes(TypePointers const& _types)
{
return applyMap(_types, [](auto _type) {
if (auto userType = dynamic_cast<UserDefinedValueType const*>(_type))
return &userType->underlyingType();
return _type;
});
}
pair<Expression const*, FunctionCallOptions const*> SMTEncoder::functionCallExpression(FunctionCall const& _funCall)
{
Expression const* callExpr = &_funCall.expression();

9
libsolidity/formal/SMTEncoder.h
View File

@ -71,6 +71,12 @@ public:
/// otherwise _expr.
static Expression const* innermostTuple(Expression const& _expr);
/// @returns the underlying type if _type is UserDefinedValueType,
/// and _type otherwise.
static Type const* underlyingType(Type const* _type);
static TypePointers replaceUserTypes(TypePointers const& _types);
/// @returns {_funCall.expression(), nullptr} if function call option values are not given, and
/// {_funCall.expression().expression(), _funCall.expression()} if they are.
static std::pair<Expression const*, FunctionCallOptions const*> functionCallExpression(FunctionCall const& _funCall);
@ -207,6 +213,7 @@ protected:
void visitCryptoFunction(FunctionCall const& _funCall);
void visitGasLeft(FunctionCall const& _funCall);
virtual void visitAddMulMod(FunctionCall const& _funCall);
void visitWrapUnwrap(FunctionCall const& _funCall);
void visitObjectCreation(FunctionCall const& _funCall);
void visitTypeConversion(FunctionCall const& _funCall);
void visitStructConstructorCall(FunctionCall const& _funCall);
@ -319,6 +326,8 @@ protected:
/// @returns whether _a or a subtype of _a is the same as _b.
bool sameTypeOrSubtype(Type const* _a, Type const* _b);
bool isSupportedType(Type const& _type) const;
/// Given the state of the symbolic variables at the end of two different branches,
/// create a merged state using the given branch condition.
void mergeVariables(smtutil::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse);

2
libsolidity/formal/SymbolicState.cpp
View File

@ -270,6 +270,8 @@ void SymbolicState::buildABIFunctions(set<FunctionCall const*> const& _abiFuncti
t = TypeProvider::uint256();
else if (t->category() == frontend::Type::Category::StringLiteral)
t = TypeProvider::bytesMemory();
else if (auto userType = dynamic_cast<UserDefinedValueType const*>(t))
t = &userType->underlyingType();
};
replaceTypes(inTypes);
replaceTypes(outTypes);

4
libsolidity/formal/SymbolicTypes.cpp
View File

@ -233,6 +233,10 @@ pair<bool, shared_ptr<SymbolicVariable>> newSymbolicVariable(
bool abstract = false;
shared_ptr<SymbolicVariable> var;
frontend::Type const* type = &_type;
if (auto userType = dynamic_cast<UserDefinedValueType const*>(type))
return newSymbolicVariable(userType->underlyingType(), _uniqueName, _context);
if (!isSupportedTypeDeclaration(_type))
{
abstract = true;

1
test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_2d.sol
View File

@ -9,4 +9,3 @@ function f() public pure { (int[][]); }
// Warning 6133: (41-50): Statement has no effect.
// Warning 8364: (42-47): Assertion checker does not yet implement type type(int256[] memory)
// Warning 8364: (42-49): Assertion checker does not yet implement type type(int256[] memory[] memory)
// Warning 8364: (41-50): Assertion checker does not yet implement type type(int256[] memory[] memory)

1
test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_3d.sol
View File

@ -10,4 +10,3 @@ function f() public pure { (int[][][]); }
// Warning 8364: (42-47): Assertion checker does not yet implement type type(int256[] memory)
// Warning 8364: (42-49): Assertion checker does not yet implement type type(int256[] memory[] memory)
// Warning 8364: (42-51): Assertion checker does not yet implement type type(int256[] memory[] memory[] memory)
// Warning 8364: (41-52): Assertion checker does not yet implement type type(int256[] memory[] memory[] memory)

18
test/libsolidity/smtCheckerTests/userTypes/constant.sol Normal file
View File

@ -0,0 +1,18 @@
type T is int224;
pragma solidity >= 0.0.0;
contract C {
T constant public s = T.wrap(int224(165521356710917456517261742455526507355687727119203895813322792776));
T constant public t = s;
int224 constant public u = T.unwrap(t);
function f() public pure {
assert(T.unwrap(s) == 165521356710917456517261742455526507355687727119203895813322792776);
assert(T.unwrap(t) == 165521356710917456517261742455526507355687727119203895813322792776);
assert(u == 165521356710917456517261742455526507355687727119203895813322792776);
assert(T.unwrap(s) == 0); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (531-555): CHC: Assertion violation happens here.\nCounterexample:\nu = 165521356710917456517261742455526507355687727119203895813322792776\n\nTransaction trace:\nC.constructor()\nState: u = 165521356710917456517261742455526507355687727119203895813322792776\nC.f()

87
test/libsolidity/smtCheckerTests/userTypes/conversion.sol Normal file
View File

@ -0,0 +1,87 @@
pragma abicoder v2;
type MyUInt8 is uint8;
type MyInt8 is int8;
type MyUInt16 is uint16;
contract C {
function f(uint a) internal pure returns(MyUInt8) {
return MyUInt8.wrap(uint8(a));
}
function g(uint a) internal pure returns(MyInt8) {
return MyInt8.wrap(int8(int(a)));
}
function h(MyUInt8 a) internal pure returns (MyInt8) {
return MyInt8.wrap(int8(MyUInt8.unwrap(a)));
}
function i(MyUInt8 a) internal pure returns(MyUInt16) {
return MyUInt16.wrap(MyUInt8.unwrap(a));
}
function j(MyUInt8 a) internal pure returns (uint) {
return MyUInt8.unwrap(a);
}
function k(MyUInt8 a) internal pure returns (MyUInt16) {
return MyUInt16.wrap(MyUInt8.unwrap(a));
}
function m(MyUInt16 a) internal pure returns (MyUInt8) {
return MyUInt8.wrap(uint8(MyUInt16.unwrap(a)));
}
function p() public pure {
assert(MyUInt8.unwrap(f(1)) == 1);
assert(MyUInt8.unwrap(f(2)) == 2);
assert(MyUInt8.unwrap(f(257)) == 1);
assert(MyUInt8.unwrap(f(257)) == 257); // should fail
}
function q() public pure {
assert(MyInt8.unwrap(g(1)) == 1);
assert(MyInt8.unwrap(g(2)) == 2);
assert(MyInt8.unwrap(g(255)) == -1);
assert(MyInt8.unwrap(g(257)) == 1);
assert(MyInt8.unwrap(g(257)) == -1); // should fail
}
function r() public pure {
assert(MyInt8.unwrap(h(MyUInt8.wrap(1))) == 1);
assert(MyInt8.unwrap(h(MyUInt8.wrap(2))) == 2);
assert(MyInt8.unwrap(h(MyUInt8.wrap(255))) == -1);
assert(MyInt8.unwrap(h(MyUInt8.wrap(255))) == 1); // should fail
}
function s() public pure {
assert(MyUInt16.unwrap(i(MyUInt8.wrap(250))) == 250);
assert(MyUInt16.unwrap(i(MyUInt8.wrap(250))) == 0); // should fail
}
function t() public pure {
assert(j(MyUInt8.wrap(1)) == 1);
assert(j(MyUInt8.wrap(2)) == 2);
assert(j(MyUInt8.wrap(255)) == 0xff);
assert(j(MyUInt8.wrap(255)) == 1); // should fail
}
function v() public pure {
assert(MyUInt16.unwrap(k(MyUInt8.wrap(1))) == 1);
assert(MyUInt16.unwrap(k(MyUInt8.wrap(2))) == 2);
assert(MyUInt16.unwrap(k(MyUInt8.wrap(255))) == 0xff);
assert(MyUInt16.unwrap(k(MyUInt8.wrap(255))) == 1); // should fail
}
function w() public pure {
assert(MyUInt8.unwrap(m(MyUInt16.wrap(1))) == 1);
assert(MyUInt8.unwrap(m(MyUInt16.wrap(2))) == 2);
assert(MyUInt8.unwrap(m(MyUInt16.wrap(255))) == 0xff);
assert(MyUInt8.unwrap(m(MyUInt16.wrap(255))) == 1); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (937-974): CHC: Assertion violation happens here.
// Warning 6328: (1174-1209): CHC: Assertion violation happens here.
// Warning 6328: (1413-1461): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.r()\n C.h(1) -- internal call\n C.h(2) -- internal call\n C.h(255) -- internal call\n C.h(255) -- internal call
// Warning 6328: (1568-1618): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.s()\n C.i(250) -- internal call\n C.i(250) -- internal call
// Warning 6328: (1779-1812): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.t()\n C.j(1) -- internal call\n C.j(2) -- internal call\n C.j(255) -- internal call\n C.j(255) -- internal call
// Warning 6328: (2024-2074): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.v()\n C.k(1) -- internal call\n C.k(2) -- internal call\n C.k(255) -- internal call\n C.k(255) -- internal call
// Warning 6328: (2286-2336): CHC: Assertion violation happens here.

74
test/libsolidity/smtCheckerTests/userTypes/fixedpoint.sol Normal file
View File

@ -0,0 +1,74 @@
// Represent a 18 decimal, 256 bit wide fixed point type using a user defined value type.
type UFixed256x18 is uint256;
/// A minimal library to do fixed point operations on UFixed256x18.
library FixedMath {
uint constant multiplier = 10**18;
/// Adds two UFixed256x18 numbers. Reverts on overflow, relying on checked arithmetic on
/// uint256.
function add(UFixed256x18 a, UFixed256x18 b) internal pure returns (UFixed256x18) {
return UFixed256x18.wrap(UFixed256x18.unwrap(a) + UFixed256x18.unwrap(b));
}
/// Multiplies UFixed256x18 and uint256. Reverts on overflow, relying on checked arithmetic on
/// uint256.
function mul(UFixed256x18 a, uint256 b) internal pure returns (UFixed256x18) {
return UFixed256x18.wrap(UFixed256x18.unwrap(a) * b);
}
/// Take the floor of a UFixed256x18 number.
/// @return the largest integer that does not exceed `a`.
function floor(UFixed256x18 a) internal pure returns (uint256) {
return UFixed256x18.unwrap(a) / multiplier;
}
/// Turns a uint256 into a UFixed256x18 of the same value.
/// Reverts if the integer is too large.
function toUFixed256x18(uint256 a) internal pure returns (UFixed256x18) {
return UFixed256x18.wrap(a * multiplier);
}
}
contract TestFixedMath {
function add(UFixed256x18 a, UFixed256x18 b) internal pure returns (UFixed256x18) {
return FixedMath.add(a, b);
}
function mul(UFixed256x18 a, uint256 b) internal pure returns (UFixed256x18) {
return FixedMath.mul(a, b);
}
function floor(UFixed256x18 a) internal pure returns (uint256) {
return FixedMath.floor(a);
}
function toUFixed256x18(uint256 a) internal pure returns (UFixed256x18) {
return FixedMath.toUFixed256x18(a);
}
function f() public pure {
assert(UFixed256x18.unwrap(add(UFixed256x18.wrap(0), UFixed256x18.wrap(0))) == 0);
assert(UFixed256x18.unwrap(add(UFixed256x18.wrap(25), UFixed256x18.wrap(45))) == 0x46);
assert(UFixed256x18.unwrap(add(UFixed256x18.wrap(25), UFixed256x18.wrap(45))) == 46); // should fail
}
function g() public pure {
assert(UFixed256x18.unwrap(mul(UFixed256x18.wrap(340282366920938463463374607431768211456), 20)) == 6805647338418769269267492148635364229120);
assert(UFixed256x18.unwrap(mul(UFixed256x18.wrap(340282366920938463463374607431768211456), 20)) == 0); // should fail
}
function h() public pure {
assert(floor(UFixed256x18.wrap(11579208923731619542357098500868790785326998665640564039457584007913129639930)) == 11579208923731619542357098500868790785326998665640564039457);
assert(floor(UFixed256x18.wrap(115792089237316195423570985008687907853269984665640564039457584007913129639935)) == 115792089237316195423570985008687907853269984665640564039457);
assert(floor(UFixed256x18.wrap(11579208923731619542357098500868790785326998665640564039457584007913129639930)) == 0); // should fail
}
function i() public pure {
assert(UFixed256x18.unwrap(toUFixed256x18(0)) == 0);
assert(UFixed256x18.unwrap(toUFixed256x18(5)) == 5000000000000000000);
assert(UFixed256x18.unwrap(toUFixed256x18(115792089237316195423570985008687907853269984665640564039457)) == 115792089237316195423570985008687907853269984665640564039457000000000000000000);
assert(UFixed256x18.unwrap(toUFixed256x18(5)) == 5); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (1886-1970): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nTestFixedMath.constructor()\nTestFixedMath.f()\n TestFixedMath.add(0, 0) -- internal call\n FixedMath.add(0, 0) -- internal call\n TestFixedMath.add(25, 45) -- internal call\n FixedMath.add(25, 45) -- internal call\n TestFixedMath.add(25, 45) -- internal call\n FixedMath.add(25, 45) -- internal call
// Warning 6328: (2165-2266): CHC: Assertion violation happens here.
// Warning 6328: (2675-2791): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nTestFixedMath.constructor()\nTestFixedMath.h()\n TestFixedMath.floor(11579208923731619542357098500868790785326998665640564039457584007913129639930) -- internal call\n FixedMath.floor(11579208923731619542357098500868790785326998665640564039457584007913129639930) -- internal call\n TestFixedMath.floor(115792089237316195423570985008687907853269984665640564039457584007913129639935) -- internal call\n FixedMath.floor(115792089237316195423570985008687907853269984665640564039457584007913129639935) -- internal call\n TestFixedMath.floor(11579208923731619542357098500868790785326998665640564039457584007913129639930) -- internal call\n FixedMath.floor(11579208923731619542357098500868790785326998665640564039457584007913129639930) -- internal call
// Warning 6328: (3161-3212): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nTestFixedMath.constructor()\nTestFixedMath.i()\n TestFixedMath.toUFixed256x18(0) -- internal call\n FixedMath.toUFixed256x18(0) -- internal call\n TestFixedMath.toUFixed256x18(5) -- internal call\n FixedMath.toUFixed256x18(5) -- internal call\n TestFixedMath.toUFixed256x18(115792089237316195423570985008687907853269984665640564039457) -- internal call\n FixedMath.toUFixed256x18(115792089237316195423570985008687907853269984665640564039457) -- internal call\n TestFixedMath.toUFixed256x18(5) -- internal call\n FixedMath.toUFixed256x18(5) -- internal call

19
test/libsolidity/smtCheckerTests/userTypes/in_parenthesis.sol Normal file
View File

@ -0,0 +1,19 @@
type MyInt is int;
contract C {
function f() public pure returns (MyInt a) {
a = MyInt.wrap(5);
assert(MyInt.unwrap(a) == 5);
assert(MyInt.unwrap(a) == 6); // should fail
}
function g() public pure {
MyInt x = f();
assert(MyInt.unwrap(x) == 5);
assert(MyInt.unwrap(x) == 6); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (133-161): CHC: Assertion violation happens here.\nCounterexample:\n\na = 5\n\nTransaction trace:\nC.constructor()\nC.f()
// Warning 6328: (261-289): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call

26
test/libsolidity/smtCheckerTests/userTypes/in_parenthesis_2.sol Normal file
View File

@ -0,0 +1,26 @@
type MyInt is int;
contract C {
function f() public pure returns (MyInt a, int b) {
(MyInt).wrap;
a = (MyInt).wrap(5);
(MyInt).unwrap;
b = (MyInt).unwrap((MyInt).wrap(10));
}
function g() public pure {
(MyInt x, int y) = f();
assert(MyInt.unwrap(x) == 5);
assert(MyInt.unwrap(x) == 6); // should fail
assert(y == 10);
assert(y == 11); // should fail
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6133: (87-99): Statement has no effect.
// Warning 6133: (126-140): Statement has no effect.
// Warning 6328: (274-302): CHC: Assertion violation happens here.
// Warning 6328: (340-355): CHC: Assertion violation happens here.

10
test/libsolidity/smtCheckerTests/userTypes/mapping_1.sol Normal file
View File

@ -0,0 +1,10 @@
type MyInt is int;
contract C {
mapping(MyInt => int) m;
function f(MyInt a) public view {
assert(m[a] == 0); // should hold
assert(m[a] != 0); // should fail
}
}
// ----
// Warning 6328: (134-151): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\n\nTransaction trace:\nC.constructor()\nC.f(0)

18
test/libsolidity/smtCheckerTests/userTypes/modifier_1.sol Normal file
View File

@ -0,0 +1,18 @@
type T1 is uint;
type T2 is uint;
contract C {
modifier m(T1 x, T2 y) {
require(T1.unwrap(x) == T2.unwrap(y));
_;
}
function f(uint x, uint y) m(T1.wrap(x), T2.wrap(y)) public pure {
assert(x == y);
assert(x != y); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (212-226): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 0)

21
test/libsolidity/smtCheckerTests/userTypes/multisource.sol Normal file
View File

@ -0,0 +1,21 @@
==== Source: A ====
type MyInt is int;
type MyAddress is address;
==== Source: B ====
import {MyInt, MyAddress as OurAddress} from "A";
contract A {
function f(int x) internal pure returns(MyInt) { return MyInt.wrap(x); }
function f(address x) internal pure returns(OurAddress) { return OurAddress.wrap(x); }
function g() public pure {
assert(MyInt.unwrap(f(int(5))) == 5);
assert(MyInt.unwrap(f(int(5))) == 0); // should fail
assert(OurAddress.unwrap(f(address(5))) == address(5));
assert(OurAddress.unwrap(f(address(5))) == address(0)); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (B:296-332): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nA.constructor()\nA.g()\n A.f(5) -- internal call\n A.f(5) -- internal call
// Warning 6328: (B:409-463): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nA.constructor()\nA.g()\n A.f(5) -- internal call\n A.f(5) -- internal call\n A.f(5) -- internal call\n A.f(5) -- internal call

20
test/libsolidity/smtCheckerTests/userTypes/multisource_module.sol Normal file
View File

@ -0,0 +1,20 @@
==== Source: s1.sol ====
type MyInt is int;
==== Source: s2.sol ====
import "s1.sol" as M;
contract C {
function f(int x) public pure returns (M.MyInt) { return M.MyInt.wrap(x); }
function g(M.MyInt x) public pure returns (int) { return M.MyInt.unwrap(x); }
function h() public pure {
assert(M.MyInt.unwrap(f(5)) == 5);
assert(M.MyInt.unwrap(f(5)) == 6); // should fail
assert(g(M.MyInt.wrap(1)) == 1);
assert(g(M.MyInt.wrap(1)) == 0); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (s2.sol:259-292): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.h()\n C.f(5) -- internal call\n C.f(5) -- internal call
// Warning 6328: (s2.sol:346-377): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.h()\n C.f(5) -- internal call\n C.f(5) -- internal call\n C.g(1) -- internal call\n C.g(1) -- internal call

23
test/libsolidity/smtCheckerTests/userTypes/simple.sol Normal file
View File

@ -0,0 +1,23 @@
type MyInt is int;
contract C {
function f() internal pure returns (MyInt a) {
}
function g() internal pure returns (MyInt b, MyInt c) {
b = MyInt.wrap(int(1));
c = MyInt.wrap(1);
}
function h() public pure {
assert(MyInt.unwrap(f()) == 0);
assert(MyInt.unwrap(f()) == 1); // should fail
(MyInt x, MyInt y) = g();
assert(MyInt.unwrap(x) == 1);
assert(MyInt.unwrap(x) == 0); // should fail
assert(MyInt.unwrap(y) == 1);
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (255-285): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.h()\n C.f() -- internal call\n C.f() -- internal call
// Warning 6328: (364-392): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.h()\n C.f() -- internal call\n C.f() -- internal call\n C.g() -- internal call

14
test/libsolidity/smtCheckerTests/userTypes/user_abi_1.sol Normal file
View File

@ -0,0 +1,14 @@
type T is uint;
contract C {
function f(bytes memory data) public pure {
T x = abi.decode(data, (T));
uint y = abi.decode(data, (uint));
assert(T.unwrap(x) == y); // should hold
assert(T.unwrap(x) != y); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (188-212): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 2437\n\nTransaction trace:\nC.constructor()\nC.f(data)

14
test/libsolidity/smtCheckerTests/userTypes/user_abi_2.sol Normal file
View File

@ -0,0 +1,14 @@
type T is uint;
contract C {
function f(bytes memory data) public pure {
T x = abi.decode(data, (T));
T y = abi.decode(data, (T));
assert(T.unwrap(x) == T.unwrap(y)); // should hold
assert(T.unwrap(x) != T.unwrap(y)); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (192-226): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(data)

36
test/libsolidity/smtCheckerTests/userTypes/wrap_unwrap_via_contract_name.sol Normal file
View File

@ -0,0 +1,36 @@
contract C {
type T is uint;
}
contract D {
function f(C.T x) internal pure returns(uint) {
return C.T.unwrap(x);
}
function g(uint x) internal pure returns(C.T) {
return C.T.wrap(x);
}
function h(uint x) internal pure returns(uint) {
return f(g(x));
}
function i(C.T x) internal pure returns(C.T) {
return g(f(x));
}
function m() public pure {
assert(f(C.T.wrap(0x42)) == 0x42);
assert(f(C.T.wrap(0x42)) == 0x43); // should fail
assert(C.T.unwrap(g(0x42)) == 0x42);
assert(C.T.unwrap(g(0x42)) == 0x43); // should fail
assert(h(0x42) == 0x42);
assert(h(0x42) == 0x43); // should fail
assert(C.T.unwrap(i(C.T.wrap(0x42))) == 0x42);
assert(C.T.unwrap(i(C.T.wrap(0x42))) == 0x43); // should fail
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (403-436): CHC: Assertion violation happens here.
// Warning 6328: (494-529): CHC: Assertion violation happens here.
// Warning 6328: (575-598): CHC: Assertion violation happens here.
// Warning 6328: (666-711): CHC: Assertion violation happens here.