Erase balances when delegatecall is seen

This commit is contained in:
Leo Alt 2021-08-25 11:29:42 +02:00
parent 7a0295ec6c
commit a55685c04f
12 changed files with 203 additions and 0 deletions

View File

@ -591,6 +591,7 @@ void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
{
m_externalFunctionCallHappened = true;
resetStorageVariables();
resetBalances();
}
}

View File

@ -995,6 +995,7 @@ void CHC::resetContractAnalysis()
void CHC::eraseKnowledge()
{
resetStorageVariables();
resetBalances();
}
void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function)

View File

@ -2281,6 +2281,13 @@ void SMTEncoder::resetStorageVariables()
});
}
void SMTEncoder::resetBalances()
{
// TODO this should be changed to `balances` only
// when `state` gets more members.
state().newState();
}
void SMTEncoder::resetReferences(VariableDeclaration const& _varDecl)
{
m_context.resetVariables([&](VariableDeclaration const& _var) {

View File

@ -303,6 +303,7 @@ protected:
void resetStateVariables();
void resetStorageVariables();
void resetMemoryVariables();
void resetBalances();
/// Resets all references/pointers that have the same type or have
/// a subexpression of the same type as _varDecl.
void resetReferences(VariableDeclaration const& _varDecl);

View File

@ -0,0 +1,15 @@
function l(address payable a) {}
contract C {
uint x;
function f(address payable a) public payable {
require(msg.value > 1);
uint b1 = address(this).balance;
l(a);
uint b2 = address(this).balance;
assert(b1 == b2); // should hold
assert(x == 0); // should hold
}
}
// ====
// SMTEngine: all

View File

@ -0,0 +1,24 @@
function l(address payable a) {
a.transfer(1);
}
contract C {
uint x;
function f(address payable a) public payable {
require(msg.value > 1);
uint b1 = address(this).balance;
l(a);
uint b2 = address(this).balance;
assert(b1 == b2); // should fail
assert(b1 == b2 - 1); // should hold but we don't keep track of balances with msg.value yet
assert(x == 0); // should hold
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 6328: (227-243): CHC: Assertion violation happens here.
// Warning 3944: (275-281): CHC: Underflow (resulting value less than 0) happens here.
// Warning 6328: (262-282): CHC: Assertion violation happens here.
// Warning 1236: (33-46): BMC: Insufficient funds happens here.

View File

@ -0,0 +1,18 @@
library L {
function l(address payable a) internal {}
}
contract C {
using L for address payable;
uint x;
function f(address payable a) public payable {
require(msg.value > 1);
uint b1 = address(this).balance;
a.l();
uint b2 = address(this).balance;
assert(b1 == b2); // should hold
assert(x == 0); // should hold
}
}
// ====
// SMTEngine: all

View File

@ -0,0 +1,27 @@
library L {
function l(address payable a) internal {
a.transfer(1);
}
}
contract C {
using L for address payable;
uint x;
function f(address payable a) public payable {
require(msg.value > 1);
uint b1 = address(this).balance;
a.l();
uint b2 = address(this).balance;
assert(b1 == b2); // should fail
assert(b1 == b2 - 1); // should hold but we don't keep track of balances with msg.value yet
assert(x == 0); // should hold
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (284-300): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 21238\nb1 = 8856\nb2 = 8855\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(21238){ value: 11799 }\n L.l(21238){ value: 11799 } -- internal call
// Warning 3944: (332-338): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\nx = 0\na = 38\nb1 = 1\nb2 = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(38){ value: 21240 }\n L.l(38){ value: 21240 } -- internal call
// Warning 6328: (319-339): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 21238\nb1 = 40\nb2 = 39\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(21238){ value: 8857 }\n L.l(21238){ value: 8857 } -- internal call
// Warning 1236: (56-69): BMC: Insufficient funds happens here.
// Warning 1236: (56-69): BMC: Insufficient funds happens here.

View File

@ -0,0 +1,23 @@
library L {
function l(address payable a) public {}
}
contract C {
using L for address payable;
uint x;
function f(address payable a) public payable {
require(msg.value > 1);
uint b1 = address(this).balance;
a.l();
uint b2 = address(this).balance;
assert(b1 == b2); // should fail because the called library can transfer with `this`s balance
assert(x == 0); // should fail because of `delegatecall`
}
}
// ====
// SMTEngine: all
// ----
// Warning 4588: (219-224): Assertion checker does not yet implement this type of function call.
// Warning 6328: (263-279): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\nb1 = 7720\nb2 = 7719\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0){ value: 5855 }
// Warning 6328: (359-373): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\nb1 = 39\nb2 = 38\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0){ value: 21240 }
// Warning 4588: (219-224): Assertion checker does not yet implement this type of function call.

View File

@ -0,0 +1,27 @@
library L {
function l(address payable a) public {
a.transfer(1);
}
}
contract C {
using L for address payable;
uint x;
function f(address payable a) public payable {
require(msg.value > 1);
uint b1 = address(this).balance;
a.l();
uint b2 = address(this).balance;
assert(b1 == b2); // should fail
assert(x == 0); // should fail because of `delegatecall`
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 4588: (238-243): Assertion checker does not yet implement this type of function call.
// Warning 6328: (282-298): CHC: Assertion violation happens here.
// Warning 6328: (317-331): CHC: Assertion violation happens here.
// Warning 1236: (54-67): BMC: Insufficient funds happens here.
// Warning 4588: (238-243): Assertion checker does not yet implement this type of function call.

View File

@ -0,0 +1,29 @@
library L {
function l(address payable a) public returns (uint) {
return msg.value;
}
}
contract C {
using L for address payable;
uint x;
function f(address payable a) public payable {
require(msg.value > 1);
uint b1 = address(this).balance;
uint v = a.l();
uint b2 = address(this).balance;
assert(b1 == b2); // should fail because the called library can transfer with `this`s balance
assert(x == 0); // should fail because of `delegatecall`
assert(v == msg.value); // should hold but we don't support `delegatecall` properly yet.
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 5667: (24-41): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 4588: (265-270): Assertion checker does not yet implement this type of function call.
// Warning 6328: (309-325): CHC: Assertion violation happens here.
// Warning 6328: (405-419): CHC: Assertion violation happens here.
// Warning 6328: (464-486): CHC: Assertion violation happens here.
// Warning 4588: (265-270): Assertion checker does not yet implement this type of function call.

View File

@ -0,0 +1,30 @@
library L {
function l(address payable a) public returns (address) {
return msg.sender;
}
}
contract C {
using L for address payable;
uint x;
function f(address payable a) public payable {
require(msg.value > 1);
uint b1 = address(this).balance;
address v = a.l();
uint b2 = address(this).balance;
assert(b1 == b2); // should fail because the called library can transfer with `this`s balance
assert(x == 0); // should fail because of `delegatecall`
assert(v == msg.sender); // should hold but we don't support `delegatecall` properly yet.
}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// ----
// Warning 5667: (24-41): Unused function parameter. Remove or comment out the variable name to silence this warning.
// Warning 2018: (13-93): Function state mutability can be restricted to view
// Warning 4588: (272-277): Assertion checker does not yet implement this type of function call.
// Warning 6328: (316-332): CHC: Assertion violation happens here.
// Warning 6328: (412-426): CHC: Assertion violation happens here.
// Warning 6328: (471-494): CHC: Assertion violation happens here.
// Warning 4588: (272-277): Assertion checker does not yet implement this type of function call.