diff --git a/Changelog.md b/Changelog.md index 3ff3c2cd0..b55713488 100644 --- a/Changelog.md +++ b/Changelog.md @@ -4,6 +4,7 @@ Language Features: Compiler Features: + * SMTChecker: Support one-dimensional arrays. Bugfixes: diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 1f6e85356..679cf7dd3 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -535,13 +535,6 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall) m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1)); } -void SMTChecker::eraseArrayKnowledge() -{ - for (auto const& var: m_variables) - if (var.first->annotation().type->category() == Type::Category::Mapping) - newValue(*var.first); -} - void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall) { FunctionDefinition const* _funDef = nullptr; @@ -698,17 +691,26 @@ void SMTChecker::endVisit(Literal const& _literal) solAssert(_literal.annotation().type, "Expected type for AST node"); Type const& type = *_literal.annotation().type; if (isNumber(type.category())) - defineExpr(_literal, smt::Expression(type.literalValue(&_literal))); else if (isBool(type.category())) defineExpr(_literal, smt::Expression(_literal.token() == Token::TrueLiteral ? true : false)); else + { + if (type.category() == Type::Category::StringLiteral) + { + auto stringType = make_shared(DataLocation::Memory, true); + auto stringLit = dynamic_cast(_literal.annotation().type.get()); + solAssert(stringLit, ""); + auto result = newSymbolicVariable(*stringType, stringLit->richIdentifier(), *m_interface); + m_expressions.emplace(&_literal, result.second); + } m_errorReporter.warning( _literal.location(), "Assertion checker does not yet support the type of this literal (" + _literal.annotation().type->toString() + ")." ); + } } void SMTChecker::endVisit(Return const& _return) @@ -796,7 +798,6 @@ void SMTChecker::endVisit(IndexAccess const& _indexAccess) void SMTChecker::arrayAssignment() { m_arrayAssignmentHappened = true; - eraseArrayKnowledge(); } void SMTChecker::arrayIndexAssignment(Assignment const& _assignment) @@ -806,12 +807,48 @@ void SMTChecker::arrayIndexAssignment(Assignment const& _assignment) { auto const& varDecl = dynamic_cast(*id->annotation().referencedDeclaration); solAssert(knownVariable(varDecl), ""); + + if (varDecl.hasReferenceOrMappingType()) + resetVariables([&](VariableDeclaration const& _var) { + if (_var == varDecl) + return false; + TypePointer prefix = _var.type(); + TypePointer originalType = typeWithoutPointer(varDecl.type()); + while ( + prefix->category() == Type::Category::Mapping || + prefix->category() == Type::Category::Array + ) + { + if (*originalType == *typeWithoutPointer(prefix)) + return true; + if (prefix->category() == Type::Category::Mapping) + { + auto mapPrefix = dynamic_cast(prefix.get()); + solAssert(mapPrefix, ""); + prefix = mapPrefix->valueType(); + } + else + { + auto arrayPrefix = dynamic_cast(prefix.get()); + solAssert(arrayPrefix, ""); + prefix = arrayPrefix->baseType(); + } + } + return false; + }); + smt::Expression store = smt::Expression::store( m_variables[&varDecl]->currentValue(), expr(*indexAccess.indexExpression()), expr(_assignment.rightHandSide()) ); m_interface->addAssertion(newValue(varDecl) == store); + // Update the SMT select value after the assignment, + // necessary for sound models. + defineExpr(indexAccess, smt::Expression::select( + m_variables[&varDecl]->currentValue(), + expr(*indexAccess.indexExpression()) + )); } else if (dynamic_cast(&indexAccess.baseExpression())) m_errorReporter.warning( @@ -1310,6 +1347,13 @@ void SMTChecker::resetVariables(function const }); } +TypePointer SMTChecker::typeWithoutPointer(TypePointer const& _type) +{ + if (auto refType = dynamic_cast(_type.get())) + return ReferenceType::copyForLocationIfReference(refType->location(), _type); + return _type; +} + void SMTChecker::mergeVariables(vector const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse) { set uniqueVars(_variables.begin(), _variables.end()); diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index ccb7e1e4d..f11f156e7 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -103,8 +103,6 @@ private: void arrayAssignment(); /// Handles assignment to SMT array index. void arrayIndexAssignment(Assignment const& _assignment); - /// Erases information about SMT arrays. - void eraseArrayKnowledge(); /// Division expression in the given type. Requires special treatment because /// of rounding for signed division. @@ -177,6 +175,9 @@ private: void resetStorageReferences(); void resetVariables(std::vector _variables); void resetVariables(std::function const& _filter); + /// @returns the type without storage pointer information if it has it. + TypePointer typeWithoutPointer(TypePointer const& _type); + /// Given two different branches and the touched variables, /// merge the touched variables into after-branch ite variables /// using the branch condition as guard. diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index 269bff738..9ee4f726a 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -57,8 +57,13 @@ smt::SortPointer dev::solidity::smtSort(Type const& _type) solAssert(mapType, ""); return make_shared(smtSort(*mapType->keyType()), smtSort(*mapType->valueType())); } - // TODO Solidity array - return make_shared(smt::Kind::Int); + else + { + solAssert(isArray(_type.category()), ""); + auto arrayType = dynamic_cast(&_type); + solAssert(arrayType, ""); + return make_shared(make_shared(smt::Kind::Int), smtSort(*arrayType->baseType())); + } } default: // Abstract case. @@ -82,7 +87,7 @@ smt::Kind dev::solidity::smtKind(Type::Category _category) return smt::Kind::Bool; else if (isFunction(_category)) return smt::Kind::Function; - else if (isMapping(_category)) + else if (isMapping(_category) || isArray(_category)) return smt::Kind::Array; // Abstract case. return smt::Kind::Int; @@ -92,7 +97,8 @@ bool dev::solidity::isSupportedType(Type::Category _category) { return isNumber(_category) || isBool(_category) || - isMapping(_category); + isMapping(_category) || + isArray(_category); } bool dev::solidity::isSupportedTypeDeclaration(Type::Category _category) @@ -140,6 +146,8 @@ pair> dev::solidity::newSymbolicVariable( } else if (isMapping(_type.category())) var = make_shared(type, _uniqueName, _solver); + else if (isArray(_type.category())) + var = make_shared(type, _uniqueName, _solver); else solAssert(false, ""); return make_pair(abstract, var); @@ -198,6 +206,11 @@ bool dev::solidity::isMapping(Type::Category _category) return _category == Type::Category::Mapping; } +bool dev::solidity::isArray(Type::Category _category) +{ + return _category == Type::Category::Array; +} + smt::Expression dev::solidity::minValue(IntegerType const& _type) { return smt::Expression(_type.minValue()); diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h index 35c7bb8df..72f6232da 100644 --- a/libsolidity/formal/SymbolicTypes.h +++ b/libsolidity/formal/SymbolicTypes.h @@ -48,6 +48,7 @@ bool isNumber(Type::Category _category); bool isBool(Type::Category _category); bool isFunction(Type::Category _category); bool isMapping(Type::Category _category); +bool isArray(Type::Category _category); /// Returns a new symbolic variable, according to _type. /// Also returns whether the type is abstract or not, diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp index 57921558c..a0a4fcefb 100644 --- a/libsolidity/formal/SymbolicVariables.cpp +++ b/libsolidity/formal/SymbolicVariables.cpp @@ -136,3 +136,13 @@ SymbolicMappingVariable::SymbolicMappingVariable( { solAssert(isMapping(m_type->category()), ""); } + +SymbolicArrayVariable::SymbolicArrayVariable( + TypePointer _type, + string const& _uniqueName, + smt::SolverInterface& _interface +): + SymbolicVariable(move(_type), _uniqueName, _interface) +{ + solAssert(isArray(m_type->category()), ""); +} diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h index 86abf4f19..9397865ec 100644 --- a/libsolidity/formal/SymbolicVariables.h +++ b/libsolidity/formal/SymbolicVariables.h @@ -153,5 +153,18 @@ public: ); }; +/** + * Specialization of SymbolicVariable for Array + */ +class SymbolicArrayVariable: public SymbolicVariable +{ +public: + SymbolicArrayVariable( + TypePointer _type, + std::string const& _uniqueName, + smt::SolverInterface& _interface + ); +}; + } } diff --git a/test/libsolidity/smtCheckerTests/simple/static_array.sol b/test/libsolidity/smtCheckerTests/simple/static_array.sol index be49ab7fe..be114fbb5 100644 --- a/test/libsolidity/smtCheckerTests/simple/static_array.sol +++ b/test/libsolidity/smtCheckerTests/simple/static_array.sol @@ -7,6 +7,4 @@ contract C int[3*1] x; } // ---- -// Warning: (92-100): Assertion checker does not yet support the type of this variable. -// Warning: (149-159): Assertion checker does not yet support the type of this variable. // Warning: (153-156): Assertion checker does not yet implement this operator on non-integer types. diff --git a/test/libsolidity/smtCheckerTests/special/msg_data.sol b/test/libsolidity/smtCheckerTests/special/msg_data.sol index b667f971d..75bc8e2ba 100644 --- a/test/libsolidity/smtCheckerTests/special/msg_data.sol +++ b/test/libsolidity/smtCheckerTests/special/msg_data.sol @@ -8,6 +8,5 @@ contract C } // ---- // Warning: (86-101): Assertion checker does not yet support this expression. -// Warning: (86-94): Assertion checker does not yet support this global variable. // Warning: (86-101): Internal error: Expression undefined for SMT solver. // Warning: (79-106): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_1.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_1.sol new file mode 100644 index 000000000..8cd468652 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_1.sol @@ -0,0 +1,31 @@ +pragma experimental SMTChecker; + +contract C +{ + function f( + uint[] memory a, + uint[] memory b, + uint[][] memory cc, + uint8[][] memory dd, + uint[][][] memory eee + ) internal pure { + require(a[0] == 2); + require(cc[0][0] == 50); + require(dd[0][0] == 10); + require(eee[0][0][0] == 50); + b[0] = 1; + // Fails because b == a is possible. + assert(a[0] == 2); + // Fails because b == cc[0] is possible. + assert(cc[0][0] == 50); + // Should not fail since knowledge is erased only for uint[]. + assert(dd[0][0] == 10); + // Fails because b == ee[0][0] is possible. + assert(eee[0][0][0] == 50); + assert(b[0] == 1); + } +} +// ---- +// Warning: (345-362): Assertion violation happens here +// Warning: (409-431): Assertion violation happens here +// Warning: (571-597): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_2.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_2.sol new file mode 100644 index 000000000..d015d1471 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_2.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract C +{ + uint[] array; + function f(uint[] memory a, uint[] memory b) internal view { + require(array[0] == 42); + require(a[0] == 2); + b[0] = 1; + // Erasing knowledge about memory references should not + // erase knowledge about state variables. + assert(array[0] == 42); + assert(a[0] == 2); + assert(b[0] == 1); + } +} +// ---- +// Warning: (314-331): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_3.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_3.sol new file mode 100644 index 000000000..f6d6b1977 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_aliasing_memory_3.sol @@ -0,0 +1,22 @@ +pragma experimental SMTChecker; + +contract C +{ + uint[] array; + function f(uint[] memory a, uint[] memory b) internal view { + require(array[0] == 42); + uint[] storage c = array; + require(a[0] == 2); + b[0] = 1; + // Erasing knowledge about memory references should not + // erase knowledge about state variables. + assert(array[0] == 42); + // Erasing knowledge about memory references should not + // erase knowledge about storage references. + assert(c[0] == 42); + assert(a[0] == 2); + assert(b[0] == 1); + } +} +// ---- +// Warning: (469-486): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_1.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_1.sol new file mode 100644 index 000000000..6461634e1 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_1.sol @@ -0,0 +1,45 @@ +pragma experimental SMTChecker; + +contract C +{ + uint[] array; + uint[][] array2d; + uint8[] tinyArray; + function f( + uint[] storage a, + uint[] storage b, + uint[][] storage cc, + uint8[][] storage dd, + uint[][][] storage eee + ) internal { + require(a[0] == 2); + require(array[0] == 42); + require(array2d[0][0] == 42); + require(tinyArray[0] == 42); + require(cc[0][0] == 42); + require(dd[0][0] == 42); + require(eee[0][0][0] == 42); + b[0] = 1; + // Fails because b == a is possible. + assert(a[0] == 2); + // Fails because b == array is possible. + assert(array[0] == 42); + // Fails because b == array2d[0] is possible. + assert(array2d[0][0] == 42); + // Should not fail since knowledge is erased only for uint[]. + assert(tinyArray[0] == 42); + // Fails because b == cc[0] is possible. + assert(cc[0][0] == 42); + // Should not fail since knowledge is erased only for uint[]. + assert(dd[0][0] == 42); + // Fails because b == ee[0][0] is possible. + assert(eee[0][0][0] == 42); + assert(b[0] == 1); + } +} +// ---- +// Warning: (489-506): Assertion violation happens here +// Warning: (553-575): Assertion violation happens here +// Warning: (627-654): Assertion violation happens here +// Warning: (795-817): Assertion violation happens here +// Warning: (957-983): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_2.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_2.sol new file mode 100644 index 000000000..4b134e58e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_2.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint[] storage a, uint[] storage b, uint[] memory c) internal { + require(c[0] == 42); + require(a[0] == 2); + b[0] = 1; + // Erasing knowledge about storage references should not + // erase knowledge about memory references. + assert(c[0] == 42); + // Fails because b == a is possible. + assert(a[0] == 2); + assert(b[0] == 1); + } +} +// ---- +// Warning: (347-364): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_3.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_3.sol new file mode 100644 index 000000000..d70cc18bb --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_3.sol @@ -0,0 +1,22 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint[] storage a, uint[] storage b, uint[] memory c) internal { + uint[] memory d = c; + require(c[0] == 42); + require(a[0] == 2); + b[0] = 1; + // Erasing knowledge about storage references should not + // erase knowledge about memory references. + assert(c[0] == 42); + // Erasing knowledge about storage references should not + // erase knowledge about memory references. + assert(d[0] == 42); + // Fails because b == a is possible. + assert(a[0] == 2); + assert(b[0] == 1); + } +} +// ---- +// Warning: (497-514): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_4.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_4.sol new file mode 100644 index 000000000..13dc6fcc2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_4.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; + +contract C +{ + uint[] array; + function f(uint[] storage a, uint[] storage b) internal { + require(a[0] == 2); + require(b[0] == 42); + array[0] = 1; + // Fails because array == a is possible. + assert(a[0] == 2); + // Fails because array == b is possible. + assert(b[0] == 42); + assert(array[0] == 1); + } +} +// ---- +// Warning: (226-243): Assertion violation happens here +// Warning: (290-308): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_dynamic_1.sol b/test/libsolidity/smtCheckerTests/types/array_dynamic_1.sol new file mode 100644 index 000000000..39d028eff --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_dynamic_1.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; + +contract C +{ + uint[] array; + function f(uint x, uint y) public { + array[x] = 200; + require(x == y); + assert(array[y] > 100); + } +} diff --git a/test/libsolidity/smtCheckerTests/types/array_dynamic_1_fail.sol b/test/libsolidity/smtCheckerTests/types/array_dynamic_1_fail.sol new file mode 100644 index 000000000..79864d35a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_dynamic_1_fail.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C +{ + uint[] array; + function f(uint x, uint y) public { + array[x] = 200; + require(x == y); + assert(array[y] > 300); + } +} +// ---- +// Warning: (137-159): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_dynamic_2.sol b/test/libsolidity/smtCheckerTests/types/array_dynamic_2.sol new file mode 100644 index 000000000..e1a02a797 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_dynamic_2.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; + +contract C +{ + uint[][] array; + function f(uint x, uint y, uint z, uint t) public view { + require(array[x][y] == 200); + require(x == z && y == t); + assert(array[z][t] > 100); + } +} diff --git a/test/libsolidity/smtCheckerTests/types/array_dynamic_2_fail.sol b/test/libsolidity/smtCheckerTests/types/array_dynamic_2_fail.sol new file mode 100644 index 000000000..725e51ba2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_dynamic_2_fail.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C +{ + uint[][] array; + function f(uint x, uint y, uint z, uint t) public view { + require(array[x][y] == 200); + require(x == z && y == t); + assert(array[z][t] > 300); + } +} +// ---- +// Warning: (183-208): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_dynamic_3.sol b/test/libsolidity/smtCheckerTests/types/array_dynamic_3.sol new file mode 100644 index 000000000..b76f23bed --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_dynamic_3.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; + +contract C +{ + uint[][][] array; + function f(uint x, uint y, uint z, uint t, uint w, uint v) public view { + require(array[x][y][z] == 200); + require(x == t && y == w && z == v); + assert(array[t][w][v] > 100); + } +} diff --git a/test/libsolidity/smtCheckerTests/types/array_dynamic_3_fail.sol b/test/libsolidity/smtCheckerTests/types/array_dynamic_3_fail.sol new file mode 100644 index 000000000..3a34ce5dd --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_dynamic_3_fail.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C +{ + uint[][][] array; + function f(uint x, uint y, uint z, uint t, uint w, uint v) public view { + require(array[x][y][z] == 200); + require(x == t && y == w && z == v); + assert(array[t][w][v] > 300); + } +} +// ---- +// Warning: (214-242): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_dynamic_parameter_1.sol b/test/libsolidity/smtCheckerTests/types/array_dynamic_parameter_1.sol new file mode 100644 index 000000000..83d25dcb5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_dynamic_parameter_1.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint[] memory array, uint x, uint y) public pure { + array[x] = 200; + require(x == y); + assert(array[y] > 100); + } +} diff --git a/test/libsolidity/smtCheckerTests/types/array_dynamic_parameter_1_fail.sol b/test/libsolidity/smtCheckerTests/types/array_dynamic_parameter_1_fail.sol new file mode 100644 index 000000000..a9754b611 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_dynamic_parameter_1_fail.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint[] memory array, uint x, uint y) public pure { + array[x] = 200; + require(x == y); + assert(array[y] > 300); + } +} +// ---- +// Warning: (148-170): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_literal_1.sol b/test/libsolidity/smtCheckerTests/types/array_literal_1.sol new file mode 100644 index 000000000..5c0d31b5b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_literal_1.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public pure { + uint[3] memory array = [uint(1), 2, 3]; + } +} +// ---- +// Warning: (76-96): Unused local variable. +// Warning: (99-114): Assertion checker does not yet implement tuples and inline arrays. +// Warning: (99-114): Internal error: Expression undefined for SMT solver. diff --git a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol new file mode 100644 index 000000000..decffbc0b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol @@ -0,0 +1,24 @@ +pragma experimental SMTChecker; + +contract C +{ + mapping (uint => uint) singleMap; + mapping (uint => uint)[] severalMaps; + mapping (uint => uint8)[] severalMaps8; + mapping (uint => uint)[][] severalMaps3d; + function f(mapping (uint => uint) storage map) internal { + require(severalMaps[0][0] == 42); + require(severalMaps8[0][0] == 42); + require(severalMaps3d[0][0][0] == 42); + map[0] = 2; + // Should fail since map == severalMaps[0] is possible. + assert(severalMaps[0][0] == 42); + // Should not fail since knowledge is erase only for mapping (uint => uint). + assert(severalMaps8[0][0] == 42); + // Should fail since map == severalMaps3d[0][0] is possible. + assert(severalMaps3d[0][0][0] == 42); + } +} +// ---- +// Warning: (451-482): Assertion violation happens here +// Warning: (664-700): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_static_1.sol b/test/libsolidity/smtCheckerTests/types/array_static_1.sol new file mode 100644 index 000000000..2d7dc7250 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_static_1.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; + +contract C +{ + uint[10] array; + function f(uint x, uint y) public { + array[x] = 200; + require(x == y); + assert(array[y] > 100); + } +} diff --git a/test/libsolidity/smtCheckerTests/types/array_static_1_fail.sol b/test/libsolidity/smtCheckerTests/types/array_static_1_fail.sol new file mode 100644 index 000000000..017df8f29 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_static_1_fail.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C +{ + uint[10] array; + function f(uint x, uint y) public { + array[x] = 200; + require(x == y); + assert(array[y] > 300); + } +} +// ---- +// Warning: (139-161): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_static_2.sol b/test/libsolidity/smtCheckerTests/types/array_static_2.sol new file mode 100644 index 000000000..5d5242938 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_static_2.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; + +contract C +{ + uint[10][20] array; + function f(uint x, uint y, uint z, uint t) public view { + require(array[x][y] == 200); + require(x == z && y == t); + assert(array[z][t] > 100); + } +} diff --git a/test/libsolidity/smtCheckerTests/types/array_static_2_fail.sol b/test/libsolidity/smtCheckerTests/types/array_static_2_fail.sol new file mode 100644 index 000000000..789308c57 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_static_2_fail.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C +{ + uint[10][20] array; + function f(uint x, uint y, uint z, uint t) public view { + require(array[x][y] == 200); + require(x == z && y == t); + assert(array[z][t] > 300); + } +} +// ---- +// Warning: (187-212): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_static_3.sol b/test/libsolidity/smtCheckerTests/types/array_static_3.sol new file mode 100644 index 000000000..516291219 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_static_3.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; + +contract C +{ + uint[10][20][30] array; + function f(uint x, uint y, uint z, uint t, uint w, uint v) public view { + require(array[x][y][z] == 200); + require(x == t && y == w && z == v); + assert(array[t][w][v] > 100); + } +} diff --git a/test/libsolidity/smtCheckerTests/types/array_static_3_fail.sol b/test/libsolidity/smtCheckerTests/types/array_static_3_fail.sol new file mode 100644 index 000000000..240a11067 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_static_3_fail.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C +{ + uint[10][20][30] array; + function f(uint x, uint y, uint z, uint t, uint w, uint v) public view { + require(array[x][y][z] == 200); + require(x == t && y == w && z == v); + assert(array[t][w][v] > 300); + } +} +// ---- +// Warning: (220-248): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/bytes_1.sol b/test/libsolidity/smtCheckerTests/types/bytes_1.sol index fb9574213..92a616d43 100644 --- a/test/libsolidity/smtCheckerTests/types/bytes_1.sol +++ b/test/libsolidity/smtCheckerTests/types/bytes_1.sol @@ -9,8 +9,3 @@ contract C } // ---- // Warning: (113-127): Unused local variable. -// Warning: (113-127): Assertion checker does not yet support the type of this variable. -// Warning: (58-72): Assertion checker does not yet support the type of this variable. -// Warning: (95-107): Assertion checker does not yet support the type of this variable. -// Warning: (130-131): Internal error: Expression undefined for SMT solver. -// Warning: (130-131): Assertion checker does not yet implement this type. diff --git a/test/libsolidity/smtCheckerTests/types/bytes_2.sol b/test/libsolidity/smtCheckerTests/types/bytes_2.sol new file mode 100644 index 000000000..dc41aa423 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/bytes_2.sol @@ -0,0 +1,9 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(bytes memory b1, bytes memory b2) public pure { + b1 = b2; + assert(b1[1] == b2[1]); + } +} diff --git a/test/libsolidity/smtCheckerTests/types/bytes_2_fail.sol b/test/libsolidity/smtCheckerTests/types/bytes_2_fail.sol new file mode 100644 index 000000000..e5f1b3a80 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/bytes_2_fail.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(bytes memory b1, bytes memory b2) public pure { + b1 = b2; + assert(b1[1] == b2[2]); + } +} +// ---- +// Warning: (119-141): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/mapping_aliasing_2.sol new file mode 100644 index 000000000..86af187ad --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/mapping_aliasing_2.sol @@ -0,0 +1,28 @@ +pragma experimental SMTChecker; + +contract C +{ + mapping (uint => uint) a; + mapping (uint => mapping (uint => uint)) maps; + mapping (uint => mapping (uint => uint8)) maps8; + function f(mapping (uint => uint) storage map1, mapping (uint => uint) storage map2) internal { + require(map1[0] == 2); + require(a[0] == 42); + require(maps[0][0] == 42); + require(maps8[0][0] == 42); + map2[0] = 1; + // Fails because map2 == map1 is possible. + assert(map1[0] == 2); + // Fails because map2 == a is possible. + assert(a[0] == 42); + // Fails because map2 == maps[0] is possible. + assert(maps[0][0] == 42); + // Should not fail since knowledge is erased only for mapping (uint => uint). + assert(maps8[0][0] == 42); + assert(map2[0] == 1); + } +} +// ---- +// Warning: (437-457): Assertion violation happens here +// Warning: (503-521): Assertion violation happens here +// Warning: (573-597): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/mapping_unsupported_key_type_1.sol b/test/libsolidity/smtCheckerTests/types/mapping_unsupported_key_type_1.sol index f4e3a65fe..d524a0da5 100644 --- a/test/libsolidity/smtCheckerTests/types/mapping_unsupported_key_type_1.sol +++ b/test/libsolidity/smtCheckerTests/types/mapping_unsupported_key_type_1.sol @@ -9,9 +9,3 @@ contract C } } // ---- -// Warning: (89-104): Assertion checker does not yet support the type of this variable. -// Warning: (129-130): Internal error: Expression undefined for SMT solver. -// Warning: (129-130): Assertion checker does not yet implement this type. -// Warning: (155-156): Internal error: Expression undefined for SMT solver. -// Warning: (155-156): Assertion checker does not yet implement this type. -// Warning: (139-158): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/string_1.sol b/test/libsolidity/smtCheckerTests/types/string_1.sol new file mode 100644 index 000000000..0ac635c6c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/string_1.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(string memory s1, string memory s2) public pure { + assert(bytes(s1).length == bytes(s2).length); + } +} +// ---- +// Warning: (117-133): Assertion checker does not yet support this expression. +// Warning: (137-153): Assertion checker does not yet support this expression. +// Warning: (117-133): Internal error: Expression undefined for SMT solver. +// Warning: (137-153): Internal error: Expression undefined for SMT solver. +// Warning: (110-154): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/string_2.sol b/test/libsolidity/smtCheckerTests/types/string_2.sol new file mode 100644 index 000000000..68f6861b4 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/string_2.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public pure { + string memory s = "Hello World"; + } +} +// ---- +// Warning: (76-91): Unused local variable. +// Warning: (94-107): Assertion checker does not yet support the type of this literal (literal_string "Hello World").