diff --git a/Changelog.md b/Changelog.md index 197baad7e..9f197b748 100644 --- a/Changelog.md +++ b/Changelog.md @@ -13,6 +13,7 @@ Compiler Features: * Metadata: Update the swarm hash, changes ``bzzr0`` to ``bzzr1`` and urls to use ``bzz-raw://``. * Standard JSON Interface: Compile only selected sources and contracts. * Standard JSON Interface: Provide secondary error locations (e.g. the source position of other conflicting declarations). + * SMTChecker: Do not erase knowledge about storage pointers if another storage pointer is assigned. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index b7d827a05..e64992838 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -759,6 +759,11 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression c m_context.resetVariables([&](VariableDeclaration const& _var) { if (_var == *varDecl) return false; + + // If both are state variables no need to clear knowledge. + if (_var.isStateVariable() && varDecl->isStateVariable()) + return false; + TypePointer prefix = _var.type(); TypePointer originalType = typeWithoutPointer(varDecl->type()); while ( diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol new file mode 100644 index 000000000..ff47cc0e4 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol @@ -0,0 +1,23 @@ +pragma experimental SMTChecker; + +contract C +{ + uint[] b; + uint[] d; + function f(uint[] storage a, uint[] memory c) internal { + require(d[0] == 42); + require(c[0] == 42); + require(a[0] == 2); + b[0] = 1; + // Erasing knowledge about storage variables should not + // erase knowledge about memory references. + assert(c[0] == 42); + // Should not fail since b == d is not possible. + assert(d[0] == 42); + // Fails because b == a is possible. + assert(a[0] == 2); + assert(b[0] == 1); + } +} +// ---- +// Warning: (446-463): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol index decffbc0b..062e9776d 100644 --- a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol +++ b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol @@ -13,7 +13,7 @@ contract C 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). + // Should not fail since knowledge is erased 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); @@ -21,4 +21,4 @@ contract C } // ---- // Warning: (451-482): Assertion violation happens here -// Warning: (664-700): Assertion violation happens here +// Warning: (665-701): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol new file mode 100644 index 000000000..1d5ab2687 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol @@ -0,0 +1,26 @@ +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 { + map[0] = 42; + require(severalMaps[0][0] == 42); + require(severalMaps8[0][0] == 42); + require(severalMaps3d[0][0][0] == 42); + singleMap[0] = 2; + // Should not fail since singleMap == severalMaps[0] is not possible. + assert(severalMaps[0][0] == 42); + // Should not fail since knowledge is erased only for mapping (uint => uint). + assert(severalMaps8[0][0] == 42); + // Should not fail since singleMap == severalMaps3d[0][0] is not possible. + assert(severalMaps3d[0][0][0] == 42); + // Should fail since singleMap == map is possible. + assert(map[0] == 42); + } +} +// ---- +// Warning: (807-827): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_static_aliasing_memory_5.sol b/test/libsolidity/smtCheckerTests/types/array_static_aliasing_memory_5.sol new file mode 100644 index 000000000..99e993032 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_static_aliasing_memory_5.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint[2] memory a, uint[2] memory b, uint[2] memory c) internal pure { + require(c[0] == 42); + require(a[0] == 2); + b[0] = 1; + // Should fail since b == c is possible. + assert(c[0] == 42); + // Should fail since b == a is possible. + assert(a[0] == 2); + assert(b[0] == 1); + } +} +// ---- +// Warning: (230-248): Assertion violation happens here +// Warning: (295-312): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_static_aliasing_storage_5.sol b/test/libsolidity/smtCheckerTests/types/array_static_aliasing_storage_5.sol new file mode 100644 index 000000000..fa0c5eae1 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_static_aliasing_storage_5.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; + +contract C +{ + uint[2] b; + function f(uint[2] storage a, uint[2] memory c) internal { + require(c[0] == 42); + require(a[0] == 2); + b[0] = 1; + // Erasing knowledge about storage variables 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: (342-359): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol new file mode 100644 index 000000000..a675c29e2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol @@ -0,0 +1,24 @@ +pragma experimental SMTChecker; + +contract C +{ + mapping (uint => uint) singleMap; + mapping (uint => uint)[2] severalMaps; + mapping (uint => uint8)[2] severalMaps8; + mapping (uint => uint)[2][2] 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 erased 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: (455-486): Assertion violation happens here +// Warning: (669-705): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol new file mode 100644 index 000000000..c9c96a0a7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol @@ -0,0 +1,26 @@ +pragma experimental SMTChecker; + +contract C +{ + mapping (uint => uint) singleMap; + mapping (uint => uint)[2] severalMaps; + mapping (uint => uint8)[2] severalMaps8; + mapping (uint => uint)[2][2] severalMaps3d; + function f(mapping (uint => uint) storage map) internal { + map[0] = 42; + require(severalMaps[0][0] == 42); + require(severalMaps8[0][0] == 42); + require(severalMaps3d[0][0][0] == 42); + singleMap[0] = 2; + // Should not fail since singleMap == severalMaps[0] is not possible. + assert(severalMaps[0][0] == 42); + // Should not fail since knowledge is erased only for mapping (uint => uint). + assert(severalMaps8[0][0] == 42); + // Should not fail since singleMap == severalMaps3d[0][0] is not possible. + assert(severalMaps3d[0][0][0] == 42); + // Should fail since singleMap == map is possible. + assert(map[0] == 42); + } +} +// ---- +// Warning: (811-831): Assertion violation happens here