mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Support the external call option
This commit is contained in:
parent
29cc7aa951
commit
106c591dde
@ -10,6 +10,7 @@ Compiler Features:
|
||||
* Immutable variables can be read at construction time once they are initialized.
|
||||
* SMTChecker: Support low level ``call`` as external calls to unknown code.
|
||||
* SMTChecker: Add constraints to better correlate ``address(this).balance`` and ``msg.value``.
|
||||
* SMTChecker: Support the ``value`` option for external function calls.
|
||||
* Commandline Interface: Disallowed the ``--experimental-via-ir`` option to be used with Standard Json, Assembler and Linker modes.
|
||||
|
||||
|
||||
|
@ -34,6 +34,7 @@
|
||||
|
||||
#include <range/v3/algorithm/for_each.hpp>
|
||||
|
||||
#include <range/v3/view/enumerate.hpp>
|
||||
#include <range/v3/view/reverse.hpp>
|
||||
|
||||
#ifdef HAVE_Z3_DLOPEN
|
||||
@ -743,13 +744,15 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
|
||||
/// so we just add the nondet_interface predicate.
|
||||
|
||||
solAssert(m_currentContract, "");
|
||||
if (isTrustedExternalCall(&_funCall.expression()))
|
||||
auto [callExpr, callOptions] = functionCallExpression(_funCall);
|
||||
|
||||
if (isTrustedExternalCall(callExpr))
|
||||
{
|
||||
externalFunctionCallToTrustedCode(_funCall);
|
||||
return;
|
||||
}
|
||||
|
||||
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
|
||||
FunctionType const& funType = dynamic_cast<FunctionType const&>(*callExpr->annotation().type);
|
||||
auto kind = funType.kind();
|
||||
solAssert(
|
||||
kind == FunctionType::Kind::External ||
|
||||
@ -773,6 +776,19 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
|
||||
if (!m_currentFunction || m_currentFunction->isConstructor())
|
||||
return;
|
||||
|
||||
if (callOptions)
|
||||
{
|
||||
optional<unsigned> valueIndex;
|
||||
for (auto&& [i, name]: callOptions->names() | ranges::views::enumerate)
|
||||
if (name && *name == "value")
|
||||
{
|
||||
valueIndex = i;
|
||||
break;
|
||||
}
|
||||
solAssert(valueIndex, "");
|
||||
state().addBalance(state().thisAddress(), 0 - expr(*callOptions->options().at(*valueIndex)));
|
||||
}
|
||||
|
||||
auto preCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables();
|
||||
|
||||
if (!usesStaticCall)
|
||||
@ -829,6 +845,8 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
|
||||
state().newTx();
|
||||
// set the transaction sender as this contract
|
||||
m_context.addAssertion(state().txMember("msg.sender") == state().thisAddress());
|
||||
// set the transaction value as 0
|
||||
m_context.addAssertion(state().txMember("msg.value") == 0);
|
||||
// set the origin to be the current transaction origin
|
||||
m_context.addAssertion(state().txMember("tx.origin") == txOrigin);
|
||||
|
||||
@ -1451,10 +1469,12 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
|
||||
return smtutil::Expression(true);
|
||||
|
||||
auto contractAddressValue = [this](FunctionCall const& _f) {
|
||||
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_f.expression().annotation().type);
|
||||
auto [callExpr, callOptions] = functionCallExpression(_f);
|
||||
|
||||
FunctionType const& funType = dynamic_cast<FunctionType const&>(*callExpr->annotation().type);
|
||||
if (funType.kind() == FunctionType::Kind::Internal)
|
||||
return state().thisAddress();
|
||||
if (MemberAccess const* callBase = dynamic_cast<MemberAccess const*>(&_f.expression()))
|
||||
if (MemberAccess const* callBase = dynamic_cast<MemberAccess const*>(callExpr))
|
||||
return expr(callBase->expression());
|
||||
solAssert(false, "Unreachable!");
|
||||
};
|
||||
|
@ -2590,6 +2590,16 @@ Expression const* SMTEncoder::innermostTuple(Expression const& _expr)
|
||||
return expr;
|
||||
}
|
||||
|
||||
pair<Expression const*, FunctionCallOptions const*> SMTEncoder::functionCallExpression(FunctionCall const& _funCall)
|
||||
{
|
||||
Expression const* callExpr = &_funCall.expression();
|
||||
auto const* callOptions = dynamic_cast<FunctionCallOptions const*>(callExpr);
|
||||
if (callOptions)
|
||||
callExpr = &callOptions->expression();
|
||||
|
||||
return {callExpr, callOptions};
|
||||
}
|
||||
|
||||
Expression const* SMTEncoder::cleanExpression(Expression const& _expr)
|
||||
{
|
||||
auto const* expr = &_expr;
|
||||
@ -2713,7 +2723,8 @@ FunctionDefinition const* SMTEncoder::functionCallToDefinition(
|
||||
if (*_funCall.annotation().kind != FunctionCallKind::FunctionCall)
|
||||
return {};
|
||||
|
||||
Expression const* calledExpr = &_funCall.expression();
|
||||
auto [calledExpr, callOptions] = functionCallExpression(_funCall);
|
||||
|
||||
if (TupleExpression const* fun = dynamic_cast<TupleExpression const*>(calledExpr))
|
||||
{
|
||||
solAssert(fun->components().size() == 1, "");
|
||||
|
@ -71,6 +71,10 @@ public:
|
||||
/// otherwise _expr.
|
||||
static Expression const* innermostTuple(Expression const& _expr);
|
||||
|
||||
/// @returns {_funCall.expression(), nullptr} if function call option values are not given, and
|
||||
/// {_funCall.expression().expression(), _funCall.expression()} if they are.
|
||||
static std::pair<Expression const*, FunctionCallOptions const*> functionCallExpression(FunctionCall const& _funCall);
|
||||
|
||||
/// @returns the expression after stripping redundant syntactic sugar.
|
||||
/// Currently supports stripping:
|
||||
/// 1. 1-tuple; i.e. ((x)) -> x
|
||||
|
@ -0,0 +1,14 @@
|
||||
contract C {
|
||||
function g(address payable i) public {
|
||||
require(address(this).balance == 100);
|
||||
i.call{value: 10}("");
|
||||
// Disabled due to Spacer nondeterminism
|
||||
//assert(address(this).balance == 90); // should hold
|
||||
// Disabled due to Spacer nondeterminism
|
||||
//assert(address(this).balance == 100); // should fail
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: all
|
||||
// ----
|
||||
// Warning 9302: (96-117): Return value of low-level calls not used.
|
@ -0,0 +1,15 @@
|
||||
contract C {
|
||||
function g(address payable i) public {
|
||||
require(address(this).balance == 100);
|
||||
i.call{value: 0}("");
|
||||
assert(address(this).balance == 100); // should hold
|
||||
assert(address(this).balance == 20); // should fail
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: all
|
||||
// ----
|
||||
// Warning 9302: (96-116): Return value of low-level calls not used.
|
||||
// Warning 6328: (120-156): CHC: Assertion violation might happen here.
|
||||
// Warning 6328: (175-210): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n i.call{value: 0}("") -- untrusted external call
|
||||
// Warning 4661: (120-156): BMC: Assertion violation happens here.
|
@ -0,0 +1,15 @@
|
||||
contract C {
|
||||
function g(address payable i) public {
|
||||
require(address(this).balance > 100);
|
||||
i.call{value: 20}("");
|
||||
assert(address(this).balance > 0); // should hold
|
||||
// Disabled due to Spacer nondeterminism
|
||||
//assert(address(this).balance == 0); // should fail
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: all
|
||||
// ----
|
||||
// Warning 9302: (95-116): Return value of low-level calls not used.
|
||||
// Warning 6328: (120-153): CHC: Assertion violation might happen here.
|
||||
// Warning 4661: (120-153): BMC: Assertion violation happens here.
|
@ -0,0 +1,14 @@
|
||||
contract C {
|
||||
function g() public {
|
||||
require(address(this).balance == 100);
|
||||
this.h{value: 10}();
|
||||
assert(address(this).balance == 100); // should hold
|
||||
assert(address(this).balance == 90); // should fail
|
||||
}
|
||||
|
||||
function h() external payable {}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: all
|
||||
// ----
|
||||
// Warning 6328: (157-192): CHC: Assertion violation happens here.
|
@ -0,0 +1,15 @@
|
||||
contract C {
|
||||
function g(uint i) public {
|
||||
require(address(this).balance == 100);
|
||||
this.h{value: i}();
|
||||
assert(address(this).balance == 100); // should hold
|
||||
assert(address(this).balance == 90); // should fail
|
||||
}
|
||||
|
||||
function h() external payable {}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: all
|
||||
// SMTIgnoreCex: yes
|
||||
// ----
|
||||
// Warning 6328: (162-197): CHC: Assertion violation happens here.
|
@ -0,0 +1,18 @@
|
||||
interface I {
|
||||
function f() external payable;
|
||||
}
|
||||
|
||||
contract C {
|
||||
function g(I i) public {
|
||||
require(address(this).balance == 100);
|
||||
i.f{value: 10}();
|
||||
assert(address(this).balance == 90); // should hold
|
||||
// Disabled due to Spacer nondeterminism
|
||||
//assert(address(this).balance == 100); // should fail
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: all
|
||||
// ----
|
||||
// Warning 6328: (151-186): CHC: Assertion violation might happen here.
|
||||
// Warning 4661: (151-186): BMC: Assertion violation happens here.
|
@ -0,0 +1,18 @@
|
||||
interface I {
|
||||
function f() external payable;
|
||||
}
|
||||
|
||||
contract C {
|
||||
function g(I i) public {
|
||||
require(address(this).balance == 100);
|
||||
i.f{value: 0}();
|
||||
assert(address(this).balance == 100); // should hold
|
||||
assert(address(this).balance == 90); // should fail
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: all
|
||||
// ----
|
||||
// Warning 6328: (150-186): CHC: Assertion violation might happen here.
|
||||
// Warning 6328: (205-240): CHC: Assertion violation happens here.
|
||||
// Warning 4661: (150-186): BMC: Assertion violation happens here.
|
@ -0,0 +1,18 @@
|
||||
interface I {
|
||||
function f() external payable;
|
||||
}
|
||||
|
||||
contract C {
|
||||
function g(I i) public {
|
||||
require(address(this).balance > 100);
|
||||
i.f{value: 20}();
|
||||
assert(address(this).balance > 0); // should hold
|
||||
assert(address(this).balance == 0); // should fail
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: all
|
||||
// ----
|
||||
// Warning 6328: (150-183): CHC: Assertion violation might happen here.
|
||||
// Warning 6328: (202-236): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n i.f{value: 20}() -- untrusted external call
|
||||
// Warning 4661: (150-183): BMC: Assertion violation happens here.
|
Loading…
Reference in New Issue
Block a user