Fix soundness of storage/memory pointers that were not erasing enough knowledge

This commit is contained in:
Leo Alt 2021-12-13 22:27:04 +01:00
parent 248bc387cd
commit 316be7206f
11 changed files with 202 additions and 23 deletions

View File

@ -9,6 +9,7 @@ Compiler Features:
Bugfixes: Bugfixes:
* Code Generator: Fix a crash when using ``@use-src`` and compiling from Yul to ewasm. * Code Generator: Fix a crash when using ``@use-src`` and compiling from Yul to ewasm.
* SMTChecker: Fix internal error when an unsafe target is solved more than once and the counterexample messages are different. * SMTChecker: Fix internal error when an unsafe target is solved more than once and the counterexample messages are different.
* SMTChecker: Fix soundness of assigned storage/memory local pointers that were not erasing enough knowledge.
* Fix internal error when a function has a calldata struct argument with an internal type inside. * Fix internal error when a function has a calldata struct argument with an internal type inside.

View File

@ -32,6 +32,8 @@
#include <liblangutil/CharStreamProvider.h> #include <liblangutil/CharStreamProvider.h>
#include <libsolutil/Algorithms.h>
#include <range/v3/view.hpp> #include <range/v3/view.hpp>
#include <limits> #include <limits>
@ -2371,28 +2373,25 @@ void SMTEncoder::resetReferences(Type const* _type)
bool SMTEncoder::sameTypeOrSubtype(Type const* _a, Type const* _b) bool SMTEncoder::sameTypeOrSubtype(Type const* _a, Type const* _b)
{ {
Type const* prefix = _a; bool foundSame = false;
while (
prefix->category() == Type::Category::Mapping || solidity::util::BreadthFirstSearch<Type const*> bfs{{_a}};
prefix->category() == Type::Category::Array bfs.run([&](auto _type, auto&& _addChild) {
) if (*typeWithoutPointer(_b) == *typeWithoutPointer(_type))
{
if (*typeWithoutPointer(_b) == *typeWithoutPointer(prefix))
return true;
if (prefix->category() == Type::Category::Mapping)
{ {
auto mapPrefix = dynamic_cast<MappingType const*>(prefix); foundSame = true;
solAssert(mapPrefix, ""); bfs.abort();
prefix = mapPrefix->valueType();
} }
else if (auto const* mapType = dynamic_cast<MappingType const*>(_type))
{ _addChild(mapType->valueType());
auto arrayPrefix = dynamic_cast<ArrayType const*>(prefix); else if (auto const* arrayType = dynamic_cast<ArrayType const*>(_type))
solAssert(arrayPrefix, ""); _addChild(arrayType->baseType());
prefix = arrayPrefix->baseType(); else if (auto const* structType = dynamic_cast<StructType const*>(_type))
} for (auto const& member: structType->nativeMembers(nullptr))
} _addChild(member.type);
return false; });
return foundSame;
} }
bool SMTEncoder::isSupportedType(Type const& _type) const bool SMTEncoder::isSupportedType(Type const& _type) const

View File

@ -22,5 +22,5 @@ contract C {
// ==== // ====
// SMTEngine: all // SMTEngine: all
// ---- // ----
// Warning 6328: (B:238-252): CHC: Assertion violation happens here.\nCounterexample:\ndata = {x: 0}\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: data = {x: 0}\nC.g()\n C.f(7) -- internal call\n A:set({x: 0}, 7) -- internal call\n A:set({x: 0}, 8) -- internal call // Warning 6328: (B:238-252): CHC: Assertion violation happens here.\nCounterexample:\ndata = {x: 21238}\nx = 8\ny = 21238\n\nTransaction trace:\nC.constructor()\nState: data = {x: 0}\nC.g()\n C.f(7) -- internal call\n A:set({x: 0}, 7) -- internal call\n A:set({x: 8}, 8) -- internal call
// Warning 6328: (B:308-322): CHC: Assertion violation happens here.\nCounterexample:\ndata = {x: 0}\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: data = {x: 0}\nC.g()\n C.f(7) -- internal call\n A:set({x: 0}, 7) -- internal call\n A:set({x: 0}, 8) -- internal call // Warning 6328: (B:308-322): CHC: Assertion violation happens here.\nCounterexample:\ndata = {x: 6}\nx = 0\ny = 6\n\nTransaction trace:\nC.constructor()\nState: data = {x: 0}\nC.g()\n C.f(7) -- internal call\n A:set({x: 0}, 7) -- internal call\n A:set({x: 0}, 8) -- internal call

View File

@ -0,0 +1,21 @@
contract C {
struct S {
uint sum;
uint[] a;
}
function f(S memory m, uint v) internal pure {
m.sum = v;
m.a = new uint[](2);
}
constructor(uint amt) {
S memory s;
f(s, amt);
assert(s.a.length == 2); // should hold but no aliasing support means it fails for now
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (201-224): CHC: Assertion violation happens here.\nCounterexample:\n\namt = 0\ns = {sum: 0, a: []}\n\nTransaction trace:\nC.constructor(0)

View File

@ -0,0 +1,26 @@
contract C {
struct S {
uint sum;
uint[] a;
}
struct T {
S s;
uint x;
}
function f(S memory m, uint v) internal pure {
m.sum = v;
m.a = new uint[](2);
}
constructor(uint amt) {
T memory t;
f(t.s, amt);
assert(t.s.a.length == 2); // should hold but no aliasing support means it fails for now
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (236-261): CHC: Assertion violation happens here.\nCounterexample:\n\namt = 0\nt = {s: {sum: 0, a: []}, x: 0}\n\nTransaction trace:\nC.constructor(0)

View File

@ -0,0 +1,26 @@
contract C {
struct S {
uint sum;
uint[] a;
}
struct T {
S s;
uint x;
}
function f(T memory m, uint v) internal pure {
m.s.sum = v;
m.s.a = new uint[](2);
}
constructor(uint amt) {
T memory t;
f(t, amt);
assert(t.s.a.length == 2); // should hold but no aliasing support means it fails for now
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (238-263): CHC: Assertion violation happens here.\nCounterexample:\n\namt = 0\nt = {s: {sum: 0, a: []}, x: 0}\n\nTransaction trace:\nC.constructor(0)

View File

@ -0,0 +1,24 @@
contract C {
struct S {
mapping(address => uint) innerM;
uint sum;
}
function f(S storage m, address i, uint v) internal {
m.innerM[i] = v;
m.sum += v;
}
S s;
constructor(uint amt) {
f(s, msg.sender, amt);
}
function g() public view {
assert(s.sum == 0); // should hold but no aliasing support means it fails for now
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (270-288): CHC: Assertion violation happens here.\nCounterexample:\ns = {innerM, sum: 21239}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: s = {innerM, sum: 21239}\nC.g()

View File

@ -0,0 +1,23 @@
contract C {
struct S {
mapping(address => uint) innerM;
uint sum;
}
function f(mapping(address => uint) storage innerM, address i, uint v) internal {
innerM[i] = v;
}
S s;
constructor(uint amt) {
f(s.innerM, msg.sender, amt);
}
function g() public view {
assert(s.innerM[msg.sender] == 0); // should hold but no aliasing support means it fails for now
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (289-322): CHC: Assertion violation happens here.\nCounterexample:\ns = {innerM, sum: 10}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: s = {innerM, sum: 10}\nC.g(){ msg.sender: 0x0985 }

View File

@ -0,0 +1,29 @@
contract C {
struct S {
mapping(address => uint) innerM;
uint sum;
}
struct T {
uint x;
S s;
}
function f(T storage m, address i, uint v) internal {
m.s.innerM[i] = v;
m.s.sum += v;
}
T t;
constructor(uint amt) {
f(t, msg.sender, amt);
}
function g() public view {
assert(t.s.sum == 0); // should hold but no aliasing support means it fails for now
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (307-327): CHC: Assertion violation happens here.\nCounterexample:\nt = {x: 10, s: {innerM, sum: 21239}}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: t = {x: 10, s: {innerM, sum: 21239}}\nC.g()

View File

@ -0,0 +1,29 @@
contract C {
struct S {
mapping(address => uint) innerM;
uint sum;
}
struct T {
uint x;
S s;
}
function f(S storage m, address i, uint v) internal {
m.innerM[i] = v;
m.sum += v;
}
T t;
constructor(uint amt) {
f(t.s, msg.sender, amt);
}
function g() public view {
assert(t.s.sum == 0); // should hold but no aliasing support means it fails for now
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (305-325): CHC: Assertion violation happens here.\nCounterexample:\nt = {x: 10, s: {innerM, sum: 21239}}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: t = {x: 10, s: {innerM, sum: 21239}}\nC.g()

View File

@ -25,5 +25,6 @@ contract C {
} }
// ==== // ====
// SMTEngine: all // SMTEngine: all
// SMTIgnoreCex: yes
// ---- // ----
// Warning 6328: (369-405): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 0, a: []}, s2 = {x: 0, a: []}\nb = false\ns3 = {x: 42, a: []}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, a: []}, s2 = {x: 0, a: []}\nC.f(false) // Warning 6328: (369-405): CHC: Assertion violation happens here.