Do not erase knowledge about storage pointers when another pointer is assigned

This commit is contained in:
Leonardo Alt 2019-07-30 20:32:49 +02:00
parent 967ee944a5
commit 7b5863e583
9 changed files with 144 additions and 2 deletions

View File

@ -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.

View File

@ -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 (

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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