mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Merge pull request #11559 from ethereum/smt_trusted
[SMTChecker] Trusted mode for external calls
This commit is contained in:
Leo
GitHub
commit
7176925a87
@ -4,6 +4,7 @@ Language Features:
|
||||
|
||||
|
||||
Compiler Features:
|
||||
* SMTChecker: New trusted mode that assumes that any compile-time available code is the actual used code even in external calls. This can be used via the CLI option ``--model-checker-ext-calls trusted`` or the JSON field ``settings.modelChecker.extCalls: "trusted"``.
|
||||
|
||||
|
||||
Bugfixes:
|
||||
|
||||
@ -518,6 +518,188 @@ which has the following form:
|
||||
"source2.sol": ["contract2", "contract3"]
|
||||
}
|
||||
|
||||
Trusted External Calls
|
||||
======================
|
||||
|
||||
By default, the SMTChecker does not assume that compile-time available code
|
||||
is the same as the runtime code for external calls. Take the following contracts
|
||||
as an example:
|
||||
|
||||
.. code-block:: solidity
|
||||
|
||||
// SPDX-License-Identifier: GPL-3.0
|
||||
pragma solidity >=0.8.0;
|
||||
|
||||
contract Ext {
|
||||
uint public x;
|
||||
function setX(uint _x) public { x = _x; }
|
||||
}
|
||||
contract MyContract {
|
||||
function callExt(Ext _e) public {
|
||||
_e.setX(42);
|
||||
assert(_e.x() == 42);
|
||||
}
|
||||
}
|
||||
|
||||
When ``MyContract.callExt`` is called, an address is given as the argument.
|
||||
At deployment time, we cannot know for sure that address ``_e`` actually
|
||||
contains a deployment of contract ``Ext``.
|
||||
Therefore, the SMTChecker will warn that the assertion above can be violated,
|
||||
which is true, if ``_e`` contains another contract than ``Ext``.
|
||||
|
||||
However, it can be useful to treat these external calls as trusted, for example,
|
||||
to test that different implementations of an interface conform to the same property.
|
||||
This means assuming that address ``_e`` indeed was deployed as contract ``Ext``.
|
||||
This mode can be enabled via the CLI option ``--model-checker-ext-calls=trusted``
|
||||
or the JSON field ``settings.modelChecker.extCalls: "trusted"``.
|
||||
|
||||
Please be aware that enabling this mode can make the SMTChecker analysis much more
|
||||
computationally costly.
|
||||
|
||||
An important part of this mode is that it is applied to contract types and high
|
||||
level external calls to contracts, and not low level calls such as ``call`` and
|
||||
``delegatecall``. The storage of an address is stored per contract type, and
|
||||
the SMTChecker assumes that an externally called contract has the type of the
|
||||
caller expression. Therefore, casting an ``address`` or a contract to
|
||||
different contract types will yield different storage values and can give
|
||||
unsound results if the assumptions are inconsistent, such as the example below:
|
||||
|
||||
.. code-block:: solidity
|
||||
|
||||
// SPDX-License-Identifier: GPL-3.0
|
||||
pragma solidity >=0.8.0;
|
||||
|
||||
contract D {
|
||||
constructor(uint _x) { x = _x; }
|
||||
uint public x;
|
||||
function setX(uint _x) public { x = _x; }
|
||||
}
|
||||
|
||||
contract E {
|
||||
constructor() { x = 2; }
|
||||
uint public x;
|
||||
function setX(uint _x) public { x = _x; }
|
||||
}
|
||||
|
||||
contract C {
|
||||
function f() public {
|
||||
address d = address(new D(42));
|
||||
|
||||
// `d` was deployed as `D`, so its `x` should be 42 now.
|
||||
assert(D(d).x() == 42); // should hold
|
||||
assert(D(d).x() == 43); // should fail
|
||||
|
||||
// E and D have the same interface, so the following
|
||||
// call would also work at runtime.
|
||||
// However, the change to `E(d)` is not reflected in `D(d)`.
|
||||
E(d).setX(1024);
|
||||
|
||||
// Reading from `D(d)` now will show old values.
|
||||
// The assertion below should fail at runtime,
|
||||
// but succeeds in this mode's analysis (unsound).
|
||||
assert(D(d).x() == 42);
|
||||
// The assertion below should succeed at runtime,
|
||||
// but fails in this mode's analysis (false positive).
|
||||
assert(D(d).x() == 1024);
|
||||
}
|
||||
}
|
||||
|
||||
Due to the above, make sure that the trusted external calls to a certain
|
||||
variable of ``address`` or ``contract`` type always have the same caller
|
||||
expression type.
|
||||
|
||||
It is also helpful to cast the called contract's variable as the type of the
|
||||
most derived type in case of inheritance.
|
||||
|
||||
.. code-block:: solidity
|
||||
|
||||
// SPDX-License-Identifier: GPL-3.0
|
||||
pragma solidity >=0.8.0;
|
||||
|
||||
interface Token {
|
||||
function balanceOf(address _a) external view returns (uint);
|
||||
function transfer(address _to, uint _amt) external;
|
||||
}
|
||||
|
||||
contract TokenCorrect is Token {
|
||||
mapping (address => uint) balance;
|
||||
constructor(address _a, uint _b) {
|
||||
balance[_a] = _b;
|
||||
}
|
||||
function balanceOf(address _a) public view override returns (uint) {
|
||||
return balance[_a];
|
||||
}
|
||||
function transfer(address _to, uint _amt) public override {
|
||||
require(balance[msg.sender] >= _amt);
|
||||
balance[msg.sender] -= _amt;
|
||||
balance[_to] += _amt;
|
||||
}
|
||||
}
|
||||
|
||||
contract Test {
|
||||
function property_transfer(address _token, address _to, uint _amt) public {
|
||||
require(_to != address(this));
|
||||
|
||||
TokenCorrect t = TokenCorrect(_token);
|
||||
|
||||
uint xPre = t.balanceOf(address(this));
|
||||
require(xPre >= _amt);
|
||||
uint yPre = t.balanceOf(_to);
|
||||
|
||||
t.transfer(_to, _amt);
|
||||
uint xPost = t.balanceOf(address(this));
|
||||
uint yPost = t.balanceOf(_to);
|
||||
|
||||
assert(xPost == xPre - _amt);
|
||||
assert(yPost == yPre + _amt);
|
||||
}
|
||||
}
|
||||
|
||||
Note that in function ``property_transfer``, the external calls are
|
||||
performed on variable ``t``
|
||||
|
||||
Another caveat of this mode are calls to state variables of contract type
|
||||
outside the analyzed contract. In the code below, even though ``B`` deploys
|
||||
``A``, it is also possible for the address stored in ``B.a`` to be called by
|
||||
anyone outside of ``B`` in between transactions to ``B`` itself. To reflect the
|
||||
possible changes to ``B.a``, the encoding allows an unbounded number of calls
|
||||
to be made to ``B.a`` externally. The encoding will keep track of ``B.a``'s
|
||||
storage, therefore assertion (2) should hold. However, currently the encoding
|
||||
allows such calls to be made from ``B`` conceptually, therefore assertion (3)
|
||||
fails. Making the encoding stronger logically is an extension of the trusted
|
||||
mode and is under development. Note that the encoding does not keep track of
|
||||
storage for ``address`` variables, therefore if ``B.a`` had type ``address``
|
||||
the encoding would assume that its storage does not change in between
|
||||
transactions to ``B``.
|
||||
|
||||
.. code-block:: solidity
|
||||
|
||||
pragma solidity >=0.8.0;
|
||||
|
||||
contract A {
|
||||
uint public x;
|
||||
address immutable public owner;
|
||||
constructor() {
|
||||
owner = msg.sender;
|
||||
}
|
||||
function setX(uint _x) public {
|
||||
require(msg.sender == owner);
|
||||
x = _x;
|
||||
}
|
||||
}
|
||||
|
||||
contract B {
|
||||
A a;
|
||||
constructor() {
|
||||
a = new A();
|
||||
assert(a.x() == 0); // (1) should hold
|
||||
}
|
||||
function g() public view {
|
||||
assert(a.owner() == address(this)); // (2) should hold
|
||||
assert(a.x() == 0); // (3) should hold, but fails due to a false positive
|
||||
}
|
||||
}
|
||||
|
||||
Reported Inferred Inductive Invariants
|
||||
======================================
|
||||
|
||||
|
||||
@ -433,6 +433,10 @@ Input Description
|
||||
"divModNoSlacks": false,
|
||||
// Choose which model checker engine to use: all (default), bmc, chc, none.
|
||||
"engine": "chc",
|
||||
// Choose whether external calls should be considered trusted in case the
|
||||
// code of the called function is available at compile-time.
|
||||
// For details see the SMTChecker section.
|
||||
"extCalls": "trusted",
|
||||
// Choose which types of invariants should be reported to the user: contract, reentrancy.
|
||||
"invariants": ["contract", "reentrancy"],
|
||||
// Choose whether to output all unproved targets. The default is `false`.
|
||||
|
||||
@ -82,7 +82,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
|
||||
m_context.setAssertionAccumulation(true);
|
||||
m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
|
||||
createFreeConstants(sourceDependencies(_source));
|
||||
state().prepareForSourceUnit(_source);
|
||||
state().prepareForSourceUnit(_source, false);
|
||||
m_unprovedAmt = 0;
|
||||
|
||||
_source.accept(*this);
|
||||
@ -130,7 +130,7 @@ bool BMC::shouldInlineFunctionCall(
|
||||
|
||||
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
|
||||
if (funType.kind() == FunctionType::Kind::External)
|
||||
return isTrustedExternalCall(&_funCall.expression());
|
||||
return isExternalCallToThis(&_funCall.expression());
|
||||
else if (funType.kind() != FunctionType::Kind::Internal)
|
||||
return false;
|
||||
|
||||
@ -567,7 +567,7 @@ void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
|
||||
auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
|
||||
if (shouldInlineFunctionCall(_funCall, currentScopeContract(), m_currentContract))
|
||||
inlineFunctionCall(_funCall);
|
||||
else if (isPublicGetter(_funCall.expression()))
|
||||
else if (publicGetter(_funCall.expression()))
|
||||
{
|
||||
// Do nothing here.
|
||||
// The processing happens in SMT Encoder, but we need to prevent the resetting of the state variables.
|
||||
|
||||
@ -104,7 +104,7 @@ void CHC::analyze(SourceUnit const& _source)
|
||||
auto sources = sourceDependencies(_source);
|
||||
collectFreeFunctions(sources);
|
||||
createFreeConstants(sources);
|
||||
state().prepareForSourceUnit(_source);
|
||||
state().prepareForSourceUnit(_source, encodeExternalCallsAsTrusted());
|
||||
|
||||
for (auto const* source: sources)
|
||||
defineInterfacesAndSummaries(*source);
|
||||
@ -175,15 +175,30 @@ void CHC::endVisit(ContractDefinition const& _contract)
|
||||
smtutil::Expression zeroes(true);
|
||||
for (auto var: stateVariablesIncludingInheritedAndPrivate(_contract))
|
||||
zeroes = zeroes && currentValue(*var) == smt::zeroValue(var->type());
|
||||
|
||||
smtutil::Expression newAddress = encodeExternalCallsAsTrusted() ?
|
||||
!state().addressActive(state().thisAddress()) :
|
||||
smtutil::Expression(true);
|
||||
|
||||
// The contract's address might already have funds before deployment,
|
||||
// so the balance must be at least `msg.value`, but not equals.
|
||||
auto initialBalanceConstraint = state().balance(state().thisAddress()) >= state().txMember("msg.value");
|
||||
addRule(smtutil::Expression::implies(
|
||||
initialConstraints(_contract) && zeroes && initialBalanceConstraint,
|
||||
initialConstraints(_contract) && zeroes && newAddress && initialBalanceConstraint,
|
||||
predicate(entry)
|
||||
), entry.functor().name);
|
||||
|
||||
setCurrentBlock(entry);
|
||||
|
||||
if (encodeExternalCallsAsTrusted())
|
||||
{
|
||||
auto const& entryAfterAddress = *createConstructorBlock(_contract, "implicit_constructor_entry_after_address");
|
||||
state().setAddressActive(state().thisAddress(), true);
|
||||
|
||||
connectBlocks(m_currentBlock, predicate(entryAfterAddress));
|
||||
setCurrentBlock(entryAfterAddress);
|
||||
}
|
||||
|
||||
solAssert(!m_errorDest, "");
|
||||
m_errorDest = m_constructorSummaries.at(&_contract);
|
||||
// We need to evaluate the base constructor calls (arguments) from derived -> base
|
||||
@ -220,6 +235,9 @@ void CHC::endVisit(ContractDefinition const& _contract)
|
||||
m_context.addAssertion(errorFlag().currentValue() == 0);
|
||||
}
|
||||
|
||||
if (encodeExternalCallsAsTrusted())
|
||||
state().writeStateVars(_contract, state().thisAddress());
|
||||
|
||||
connectBlocks(m_currentBlock, summary(_contract));
|
||||
|
||||
setCurrentBlock(*m_constructorSummaries.at(&_contract));
|
||||
@ -550,10 +568,12 @@ void CHC::endVisit(FunctionCall const& _funCall)
|
||||
externalFunctionCall(_funCall);
|
||||
SMTEncoder::endVisit(_funCall);
|
||||
break;
|
||||
case FunctionType::Kind::Creation:
|
||||
visitDeployment(_funCall);
|
||||
break;
|
||||
case FunctionType::Kind::DelegateCall:
|
||||
case FunctionType::Kind::BareCallCode:
|
||||
case FunctionType::Kind::BareDelegateCall:
|
||||
case FunctionType::Kind::Creation:
|
||||
SMTEncoder::endVisit(_funCall);
|
||||
unknownFunctionCall(_funCall);
|
||||
break;
|
||||
@ -717,6 +737,19 @@ void CHC::visitAssert(FunctionCall const& _funCall)
|
||||
verificationTargetEncountered(&_funCall, VerificationTargetType::Assert, errorCondition);
|
||||
}
|
||||
|
||||
void CHC::visitPublicGetter(FunctionCall const& _funCall)
|
||||
{
|
||||
createExpr(_funCall);
|
||||
if (encodeExternalCallsAsTrusted())
|
||||
{
|
||||
auto const& access = dynamic_cast<MemberAccess const&>(_funCall.expression());
|
||||
auto const& contractType = dynamic_cast<ContractType const&>(*access.expression().annotation().type);
|
||||
state().writeStateVars(*m_currentContract, state().thisAddress());
|
||||
state().readStateVars(contractType.contractDefinition(), expr(access.expression()));
|
||||
}
|
||||
SMTEncoder::visitPublicGetter(_funCall);
|
||||
}
|
||||
|
||||
void CHC::visitAddMulMod(FunctionCall const& _funCall)
|
||||
{
|
||||
solAssert(_funCall.arguments().at(2), "");
|
||||
@ -726,6 +759,66 @@ void CHC::visitAddMulMod(FunctionCall const& _funCall)
|
||||
SMTEncoder::visitAddMulMod(_funCall);
|
||||
}
|
||||
|
||||
void CHC::visitDeployment(FunctionCall const& _funCall)
|
||||
{
|
||||
if (!encodeExternalCallsAsTrusted())
|
||||
{
|
||||
SMTEncoder::endVisit(_funCall);
|
||||
unknownFunctionCall(_funCall);
|
||||
return;
|
||||
}
|
||||
|
||||
auto [callExpr, callOptions] = functionCallExpression(_funCall);
|
||||
auto funType = dynamic_cast<FunctionType const*>(callExpr->annotation().type);
|
||||
ContractDefinition const* contract =
|
||||
&dynamic_cast<ContractType const&>(*funType->returnParameterTypes().front()).contractDefinition();
|
||||
|
||||
// copy state variables from m_currentContract to state.storage.
|
||||
state().writeStateVars(*m_currentContract, state().thisAddress());
|
||||
errorFlag().increaseIndex();
|
||||
|
||||
Expression const* value = valueOption(callOptions);
|
||||
if (value)
|
||||
decreaseBalanceFromOptionsValue(*value);
|
||||
|
||||
auto originalTx = state().tx();
|
||||
newTxConstraints(value);
|
||||
|
||||
auto prevThisAddr = state().thisAddress();
|
||||
auto newAddr = state().newThisAddress();
|
||||
|
||||
if (auto constructor = contract->constructor())
|
||||
{
|
||||
auto const& args = _funCall.sortedArguments();
|
||||
auto const& params = constructor->parameters();
|
||||
solAssert(args.size() == params.size(), "");
|
||||
for (auto [arg, param]: ranges::zip_view(args, params))
|
||||
m_context.addAssertion(expr(*arg) == m_context.variable(*param)->currentValue());
|
||||
}
|
||||
for (auto var: stateVariablesIncludingInheritedAndPrivate(*contract))
|
||||
m_context.variable(*var)->increaseIndex();
|
||||
Predicate const& constructorSummary = *m_constructorSummaries.at(contract);
|
||||
m_context.addAssertion(smt::constructorCall(constructorSummary, m_context, false));
|
||||
|
||||
solAssert(m_errorDest, "");
|
||||
connectBlocks(
|
||||
m_currentBlock,
|
||||
predicate(*m_errorDest),
|
||||
errorFlag().currentValue() > 0
|
||||
);
|
||||
m_context.addAssertion(errorFlag().currentValue() == 0);
|
||||
|
||||
m_context.addAssertion(state().newThisAddress() == prevThisAddr);
|
||||
|
||||
// copy state variables from state.storage to m_currentContract.
|
||||
state().readStateVars(*m_currentContract, state().thisAddress());
|
||||
|
||||
state().newTx();
|
||||
m_context.addAssertion(originalTx == state().tx());
|
||||
|
||||
defineExpr(_funCall, newAddr);
|
||||
}
|
||||
|
||||
void CHC::internalFunctionCall(FunctionCall const& _funCall)
|
||||
{
|
||||
solAssert(m_currentContract, "");
|
||||
@ -750,6 +843,53 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
|
||||
m_context.addAssertion(errorFlag().currentValue() == 0);
|
||||
}
|
||||
|
||||
void CHC::addNondetCalls(ContractDefinition const& _contract)
|
||||
{
|
||||
for (auto var: _contract.stateVariables())
|
||||
if (auto contractType = dynamic_cast<ContractType const*>(var->type()))
|
||||
{
|
||||
auto const& symbVar = m_context.variable(*var);
|
||||
m_context.addAssertion(symbVar->currentValue() == symbVar->valueAtIndex(0));
|
||||
nondetCall(contractType->contractDefinition(), *var);
|
||||
}
|
||||
}
|
||||
|
||||
void CHC::nondetCall(ContractDefinition const& _contract, VariableDeclaration const& _var)
|
||||
{
|
||||
auto address = m_context.variable(_var)->currentValue();
|
||||
// Load the called contract's state variables from the global state.
|
||||
state().readStateVars(_contract, address);
|
||||
|
||||
m_context.addAssertion(state().state() == state().state(0));
|
||||
auto preCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables(_contract);
|
||||
|
||||
state().newState();
|
||||
for (auto const* var: _contract.stateVariables())
|
||||
m_context.variable(*var)->increaseIndex();
|
||||
|
||||
auto error = errorFlag().increaseIndex();
|
||||
|
||||
Predicate const& callPredicate = *createSymbolicBlock(
|
||||
nondetInterfaceSort(_contract, state()),
|
||||
"nondet_call_" + uniquePrefix(),
|
||||
PredicateType::FunctionSummary,
|
||||
&_var,
|
||||
m_currentContract
|
||||
);
|
||||
auto postCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables(_contract);
|
||||
vector<smtutil::Expression> stateExprs{error, address, state().abi(), state().crypto()};
|
||||
|
||||
auto nondet = (*m_nondetInterfaces.at(&_contract))(stateExprs + preCallState + postCallState);
|
||||
auto nondetCall = callPredicate(stateExprs + preCallState + postCallState);
|
||||
|
||||
addRule(smtutil::Expression::implies(nondet, nondetCall), nondetCall.name);
|
||||
|
||||
m_context.addAssertion(nondetCall);
|
||||
|
||||
// Load the called contract's state variables into the global state.
|
||||
state().writeStateVars(_contract, address);
|
||||
}
|
||||
|
||||
void CHC::externalFunctionCall(FunctionCall const& _funCall)
|
||||
{
|
||||
/// In external function calls we do not add a "predicate call"
|
||||
@ -757,15 +897,10 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
|
||||
/// so we just add the nondet_interface predicate.
|
||||
|
||||
solAssert(m_currentContract, "");
|
||||
|
||||
auto [callExpr, callOptions] = functionCallExpression(_funCall);
|
||||
|
||||
if (isTrustedExternalCall(callExpr))
|
||||
{
|
||||
externalFunctionCallToTrustedCode(_funCall);
|
||||
return;
|
||||
}
|
||||
|
||||
FunctionType const& funType = dynamic_cast<FunctionType const&>(*callExpr->annotation().type);
|
||||
|
||||
auto kind = funType.kind();
|
||||
solAssert(
|
||||
kind == FunctionType::Kind::External ||
|
||||
@ -774,37 +909,42 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
|
||||
""
|
||||
);
|
||||
|
||||
bool usesStaticCall = kind == FunctionType::Kind::BareStaticCall;
|
||||
|
||||
solAssert(m_currentContract, "");
|
||||
auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
|
||||
if (function)
|
||||
// Only consider high level external calls in trusted mode.
|
||||
if (
|
||||
kind == FunctionType::Kind::External &&
|
||||
(encodeExternalCallsAsTrusted() || isExternalCallToThis(callExpr))
|
||||
)
|
||||
{
|
||||
usesStaticCall |= function->stateMutability() == StateMutability::Pure ||
|
||||
function->stateMutability() == StateMutability::View;
|
||||
for (auto var: function->returnParameters())
|
||||
m_context.variable(*var)->increaseIndex();
|
||||
externalFunctionCallToTrustedCode(_funCall);
|
||||
return;
|
||||
}
|
||||
|
||||
// Low level calls are still encoded nondeterministically.
|
||||
|
||||
auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
|
||||
if (function)
|
||||
for (auto var: function->returnParameters())
|
||||
m_context.variable(*var)->increaseIndex();
|
||||
|
||||
// If we see a low level call in trusted mode,
|
||||
// we need to havoc the global state.
|
||||
if (
|
||||
kind == FunctionType::Kind::BareCall &&
|
||||
encodeExternalCallsAsTrusted()
|
||||
)
|
||||
state().newStorage();
|
||||
|
||||
// No reentrancy from constructor calls.
|
||||
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;
|
||||
}
|
||||
if (valueIndex)
|
||||
state().addBalance(state().thisAddress(), 0 - expr(*callOptions->options().at(*valueIndex)));
|
||||
}
|
||||
if (Expression const* value = valueOption(callOptions))
|
||||
decreaseBalanceFromOptionsValue(*value);
|
||||
|
||||
auto preCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables();
|
||||
|
||||
if (!usesStaticCall)
|
||||
if (!usesStaticCall(_funCall))
|
||||
{
|
||||
state().newState();
|
||||
for (auto const* var: m_stateVariables)
|
||||
@ -843,8 +983,14 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
|
||||
|
||||
void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
|
||||
{
|
||||
if (publicGetter(_funCall.expression()))
|
||||
visitPublicGetter(_funCall);
|
||||
|
||||
solAssert(m_currentContract, "");
|
||||
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
|
||||
|
||||
auto [callExpr, callOptions] = functionCallExpression(_funCall);
|
||||
FunctionType const& funType = dynamic_cast<FunctionType const&>(*callExpr->annotation().type);
|
||||
|
||||
auto kind = funType.kind();
|
||||
solAssert(kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
|
||||
|
||||
@ -854,14 +1000,25 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
|
||||
|
||||
// External call creates a new transaction.
|
||||
auto originalTx = state().tx();
|
||||
auto txOrigin = state().txMember("tx.origin");
|
||||
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);
|
||||
Expression const* value = valueOption(callOptions);
|
||||
newTxConstraints(value);
|
||||
|
||||
auto calledAddress = contractAddressValue(_funCall);
|
||||
if (value)
|
||||
{
|
||||
decreaseBalanceFromOptionsValue(*value);
|
||||
state().addBalance(calledAddress, expr(*value));
|
||||
}
|
||||
|
||||
if (encodeExternalCallsAsTrusted())
|
||||
{
|
||||
// The order here is important!! Write should go first.
|
||||
|
||||
// Load the caller contract's state variables into the global state.
|
||||
state().writeStateVars(*m_currentContract, state().thisAddress());
|
||||
// Load the called contract's state variables from the global state.
|
||||
state().readStateVars(*function->annotation().contract, contractAddressValue(_funCall));
|
||||
}
|
||||
|
||||
smtutil::Expression pred = predicate(_funCall);
|
||||
|
||||
@ -878,6 +1035,17 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
|
||||
(errorFlag().currentValue() > 0)
|
||||
);
|
||||
m_context.addAssertion(errorFlag().currentValue() == 0);
|
||||
|
||||
if (!usesStaticCall(_funCall))
|
||||
if (encodeExternalCallsAsTrusted())
|
||||
{
|
||||
// The order here is important!! Write should go first.
|
||||
|
||||
// Load the called contract's state variables into the global state.
|
||||
state().writeStateVars(*function->annotation().contract, contractAddressValue(_funCall));
|
||||
// Load the caller contract's state variables from the global state.
|
||||
state().readStateVars(*m_currentContract, state().thisAddress());
|
||||
}
|
||||
}
|
||||
|
||||
void CHC::unknownFunctionCall(FunctionCall const&)
|
||||
@ -1088,6 +1256,14 @@ set<unsigned> CHC::transactionVerificationTargetsIds(ASTNode const* _txRoot)
|
||||
return verificationTargetsIds;
|
||||
}
|
||||
|
||||
bool CHC::usesStaticCall(FunctionCall const& _funCall)
|
||||
{
|
||||
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
|
||||
auto kind = funType.kind();
|
||||
auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
|
||||
return (function && (function->stateMutability() == StateMutability::Pure || function->stateMutability() == StateMutability::View)) || kind == FunctionType::Kind::BareStaticCall;
|
||||
}
|
||||
|
||||
optional<CHC::CHCNatspecOption> CHC::natspecOptionFromString(string const& _option)
|
||||
{
|
||||
static map<string, CHCNatspecOption> options{
|
||||
@ -1128,6 +1304,11 @@ SortPointer CHC::sort(FunctionDefinition const& _function)
|
||||
return functionBodySort(_function, m_currentContract, state());
|
||||
}
|
||||
|
||||
bool CHC::encodeExternalCallsAsTrusted()
|
||||
{
|
||||
return m_settings.externalCalls.isTrusted();
|
||||
}
|
||||
|
||||
SortPointer CHC::sort(ASTNode const* _node)
|
||||
{
|
||||
if (auto funDef = dynamic_cast<FunctionDefinition const*>(_node))
|
||||
@ -1232,6 +1413,62 @@ void CHC::defineExternalFunctionInterface(FunctionDefinition const& _function, C
|
||||
m_context.addAssertion(smt::symbolicUnknownConstraints(state().balance(state().thisAddress()) + k.currentValue(), TypeProvider::uint256()));
|
||||
state().addBalance(state().thisAddress(), k.currentValue());
|
||||
|
||||
if (encodeExternalCallsAsTrusted())
|
||||
{
|
||||
// If the contract has state variables that are addresses to other contracts,
|
||||
// we need to encode the fact that those contracts may have been called in between
|
||||
// transactions to _contract.
|
||||
//
|
||||
// We do that by adding nondet_interface constraints for those contracts,
|
||||
// in the last line of this if block.
|
||||
//
|
||||
// If there are state variables of container types like structs or arrays
|
||||
// that indirectly contain contract types, we havoc the state for simplicity,
|
||||
// in the first part of this block.
|
||||
// TODO: This could actually be supported.
|
||||
// For structs: simply collect the SMT expressions of all the indirect contract type members.
|
||||
// For arrays: more involved, needs to traverse the array symbolically and do the same for each contract.
|
||||
// For mappings: way more complicated if the element type is a contract.
|
||||
auto hasContractOrAddressSubType = [&](VariableDeclaration const* _var) -> bool {
|
||||
bool foundContract = false;
|
||||
solidity::util::BreadthFirstSearch<Type const*> bfs{{_var->type()}};
|
||||
bfs.run([&](auto _type, auto&& _addChild) {
|
||||
if (
|
||||
_type->category() == Type::Category::Address ||
|
||||
_type->category() == Type::Category::Contract
|
||||
)
|
||||
{
|
||||
foundContract = true;
|
||||
bfs.abort();
|
||||
}
|
||||
if (auto const* mapType = dynamic_cast<MappingType const*>(_type))
|
||||
_addChild(mapType->valueType());
|
||||
else if (auto const* arrayType = dynamic_cast<ArrayType const*>(_type))
|
||||
_addChild(arrayType->baseType());
|
||||
else if (auto const* structType = dynamic_cast<StructType const*>(_type))
|
||||
for (auto const& member: structType->nativeMembers(nullptr))
|
||||
_addChild(member.type);
|
||||
});
|
||||
return foundContract;
|
||||
};
|
||||
bool found = false;
|
||||
for (auto var: m_currentContract->stateVariables())
|
||||
if (
|
||||
var->type()->category() != Type::Category::Address &&
|
||||
var->type()->category() != Type::Category::Contract &&
|
||||
hasContractOrAddressSubType(var)
|
||||
)
|
||||
{
|
||||
found = true;
|
||||
break;
|
||||
}
|
||||
|
||||
if (found)
|
||||
state().newStorage();
|
||||
else
|
||||
addNondetCalls(*m_currentContract);
|
||||
}
|
||||
|
||||
errorFlag().increaseIndex();
|
||||
m_context.addAssertion(summaryCall(_function));
|
||||
|
||||
@ -1308,28 +1545,28 @@ smtutil::Expression CHC::summary(FunctionDefinition const& _function, ContractDe
|
||||
return smt::function(*m_summaries.at(&_contract).at(&_function), &_contract, m_context);
|
||||
}
|
||||
|
||||
smtutil::Expression CHC::summaryCall(FunctionDefinition const& _function, ContractDefinition const& _contract)
|
||||
{
|
||||
return smt::functionCall(*m_summaries.at(&_contract).at(&_function), &_contract, m_context);
|
||||
}
|
||||
|
||||
smtutil::Expression CHC::externalSummary(FunctionDefinition const& _function, ContractDefinition const& _contract)
|
||||
{
|
||||
return smt::function(*m_externalSummaries.at(&_contract).at(&_function), &_contract, m_context);
|
||||
}
|
||||
|
||||
smtutil::Expression CHC::summary(FunctionDefinition const& _function)
|
||||
{
|
||||
solAssert(m_currentContract, "");
|
||||
return summary(_function, *m_currentContract);
|
||||
}
|
||||
|
||||
smtutil::Expression CHC::summaryCall(FunctionDefinition const& _function, ContractDefinition const& _contract)
|
||||
{
|
||||
return smt::functionCall(*m_summaries.at(&_contract).at(&_function), &_contract, m_context);
|
||||
}
|
||||
|
||||
smtutil::Expression CHC::summaryCall(FunctionDefinition const& _function)
|
||||
{
|
||||
solAssert(m_currentContract, "");
|
||||
return summaryCall(_function, *m_currentContract);
|
||||
}
|
||||
|
||||
smtutil::Expression CHC::externalSummary(FunctionDefinition const& _function, ContractDefinition const& _contract)
|
||||
{
|
||||
return smt::function(*m_externalSummaries.at(&_contract).at(&_function), &_contract, m_context);
|
||||
}
|
||||
|
||||
smtutil::Expression CHC::externalSummary(FunctionDefinition const& _function)
|
||||
{
|
||||
solAssert(m_currentContract, "");
|
||||
@ -1516,18 +1753,19 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
|
||||
auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
|
||||
solAssert(kind != FunctionType::Kind::Internal || function->isFree() || (contract && contract->isLibrary()) || util::contains(hierarchy, contract), "");
|
||||
|
||||
bool usesStaticCall = function->stateMutability() == StateMutability::Pure || function->stateMutability() == StateMutability::View;
|
||||
if (kind == FunctionType::Kind::Internal)
|
||||
contract = m_currentContract;
|
||||
|
||||
args += currentStateVariables(*m_currentContract);
|
||||
args += symbolicArguments(_funCall, m_currentContract);
|
||||
if (!m_currentContract->isLibrary() && !usesStaticCall)
|
||||
args += currentStateVariables(*contract);
|
||||
args += symbolicArguments(_funCall, contract);
|
||||
if (!usesStaticCall(_funCall))
|
||||
{
|
||||
state().newState();
|
||||
for (auto const& var: m_stateVariables)
|
||||
for (auto const& var: stateVariablesIncludingInheritedAndPrivate(*contract))
|
||||
m_context.variable(*var)->increaseIndex();
|
||||
}
|
||||
args += vector<smtutil::Expression>{state().state()};
|
||||
args += currentStateVariables(*m_currentContract);
|
||||
args += currentStateVariables(*contract);
|
||||
|
||||
for (auto var: function->parameters() + function->returnParameters())
|
||||
{
|
||||
@ -1538,14 +1776,14 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
|
||||
args.push_back(currentValue(*var));
|
||||
}
|
||||
|
||||
Predicate const& summary = *m_summaries.at(m_currentContract).at(function);
|
||||
auto from = smt::function(summary, m_currentContract, m_context);
|
||||
Predicate const& summary = *m_summaries.at(contract).at(function);
|
||||
auto from = smt::function(summary, contract, m_context);
|
||||
Predicate const& callPredicate = *createSummaryBlock(
|
||||
*function,
|
||||
*m_currentContract,
|
||||
*contract,
|
||||
kind == FunctionType::Kind::Internal ? PredicateType::InternalCall : PredicateType::ExternalCallTrusted
|
||||
);
|
||||
auto to = smt::function(callPredicate, m_currentContract, m_context);
|
||||
auto to = smt::function(callPredicate, contract, m_context);
|
||||
addRule(smtutil::Expression::implies(from, to), to.name);
|
||||
|
||||
return callPredicate(args);
|
||||
@ -1910,60 +2148,63 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
|
||||
Predicate const* summaryPredicate = Predicate::predicate(summaryNode.name);
|
||||
auto const& summaryArgs = summaryNode.arguments;
|
||||
|
||||
auto stateVars = summaryPredicate->stateVariables();
|
||||
solAssert(stateVars.has_value(), "");
|
||||
auto stateValues = summaryPredicate->summaryStateValues(summaryArgs);
|
||||
solAssert(stateValues.size() == stateVars->size(), "");
|
||||
|
||||
if (first)
|
||||
if (!summaryPredicate->programVariable())
|
||||
{
|
||||
first = false;
|
||||
/// Generate counterexample message local to the failed target.
|
||||
localState = formatVariableModel(*stateVars, stateValues, ", ") + "\n";
|
||||
auto stateVars = summaryPredicate->stateVariables();
|
||||
solAssert(stateVars.has_value(), "");
|
||||
auto stateValues = summaryPredicate->summaryStateValues(summaryArgs);
|
||||
solAssert(stateValues.size() == stateVars->size(), "");
|
||||
|
||||
if (auto calledFun = summaryPredicate->programFunction())
|
||||
if (first)
|
||||
{
|
||||
auto inValues = summaryPredicate->summaryPostInputValues(summaryArgs);
|
||||
auto const& inParams = calledFun->parameters();
|
||||
if (auto inStr = formatVariableModel(inParams, inValues, "\n"); !inStr.empty())
|
||||
localState += inStr + "\n";
|
||||
auto outValues = summaryPredicate->summaryPostOutputValues(summaryArgs);
|
||||
auto const& outParams = calledFun->returnParameters();
|
||||
if (auto outStr = formatVariableModel(outParams, outValues, "\n"); !outStr.empty())
|
||||
localState += outStr + "\n";
|
||||
first = false;
|
||||
/// Generate counterexample message local to the failed target.
|
||||
localState = formatVariableModel(*stateVars, stateValues, ", ") + "\n";
|
||||
|
||||
optional<unsigned> localErrorId;
|
||||
solidity::util::BreadthFirstSearch<unsigned> bfs{{summaryId}};
|
||||
bfs.run([&](auto _nodeId, auto&& _addChild) {
|
||||
auto const& children = _graph.edges.at(_nodeId);
|
||||
if (
|
||||
children.size() == 1 &&
|
||||
nodePred(children.front())->isFunctionErrorBlock()
|
||||
)
|
||||
{
|
||||
localErrorId = children.front();
|
||||
bfs.abort();
|
||||
}
|
||||
ranges::for_each(children, _addChild);
|
||||
});
|
||||
|
||||
if (localErrorId.has_value())
|
||||
if (auto calledFun = summaryPredicate->programFunction())
|
||||
{
|
||||
auto const* localError = nodePred(*localErrorId);
|
||||
solAssert(localError && localError->isFunctionErrorBlock(), "");
|
||||
auto const [localValues, localVars] = localError->localVariableValues(nodeArgs(*localErrorId));
|
||||
if (auto localStr = formatVariableModel(localVars, localValues, "\n"); !localStr.empty())
|
||||
localState += localStr + "\n";
|
||||
auto inValues = summaryPredicate->summaryPostInputValues(summaryArgs);
|
||||
auto const& inParams = calledFun->parameters();
|
||||
if (auto inStr = formatVariableModel(inParams, inValues, "\n"); !inStr.empty())
|
||||
localState += inStr + "\n";
|
||||
auto outValues = summaryPredicate->summaryPostOutputValues(summaryArgs);
|
||||
auto const& outParams = calledFun->returnParameters();
|
||||
if (auto outStr = formatVariableModel(outParams, outValues, "\n"); !outStr.empty())
|
||||
localState += outStr + "\n";
|
||||
|
||||
optional<unsigned> localErrorId;
|
||||
solidity::util::BreadthFirstSearch<unsigned> bfs{{summaryId}};
|
||||
bfs.run([&](auto _nodeId, auto&& _addChild) {
|
||||
auto const& children = _graph.edges.at(_nodeId);
|
||||
if (
|
||||
children.size() == 1 &&
|
||||
nodePred(children.front())->isFunctionErrorBlock()
|
||||
)
|
||||
{
|
||||
localErrorId = children.front();
|
||||
bfs.abort();
|
||||
}
|
||||
ranges::for_each(children, _addChild);
|
||||
});
|
||||
|
||||
if (localErrorId.has_value())
|
||||
{
|
||||
auto const* localError = nodePred(*localErrorId);
|
||||
solAssert(localError && localError->isFunctionErrorBlock(), "");
|
||||
auto const [localValues, localVars] = localError->localVariableValues(nodeArgs(*localErrorId));
|
||||
if (auto localStr = formatVariableModel(localVars, localValues, "\n"); !localStr.empty())
|
||||
localState += localStr + "\n";
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
auto modelMsg = formatVariableModel(*stateVars, stateValues, ", ");
|
||||
/// We report the state after every tx in the trace except for the last, which is reported
|
||||
/// first in the code above.
|
||||
if (!modelMsg.empty())
|
||||
path.emplace_back("State: " + modelMsg);
|
||||
else
|
||||
{
|
||||
auto modelMsg = formatVariableModel(*stateVars, stateValues, ", ");
|
||||
/// We report the state after every tx in the trace except for the last, which is reported
|
||||
/// first in the code above.
|
||||
if (!modelMsg.empty())
|
||||
path.emplace_back("State: " + modelMsg);
|
||||
}
|
||||
}
|
||||
|
||||
string txCex = summaryPredicate->formatSummaryCall(summaryArgs, m_charStreamProvider);
|
||||
@ -1992,6 +2233,12 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
|
||||
if (calls.size() > callTraceSize + 1)
|
||||
calls.front() += ", synthesized as:";
|
||||
}
|
||||
else if (pred->programVariable())
|
||||
{
|
||||
calls.front() += "-- action on external contract in state variable \"" + pred->programVariable()->name() + "\"";
|
||||
if (calls.size() > callTraceSize + 1)
|
||||
calls.front() += ", synthesized as:";
|
||||
}
|
||||
else if (pred->isFunctionSummary() && parentPred->isExternalCallUntrusted())
|
||||
calls.front() += " -- reentrant call";
|
||||
};
|
||||
@ -2047,7 +2294,8 @@ map<unsigned, vector<unsigned>> CHC::summaryCalls(CHCSolverInterface::CexGraph c
|
||||
nodePred->isInternalCall() ||
|
||||
nodePred->isExternalCallTrusted() ||
|
||||
nodePred->isExternalCallUntrusted() ||
|
||||
rootPred->isExternalCallUntrusted()
|
||||
rootPred->isExternalCallUntrusted() ||
|
||||
rootPred->programVariable()
|
||||
))
|
||||
{
|
||||
calls[root].push_back(node);
|
||||
@ -2105,3 +2353,31 @@ SymbolicIntVariable& CHC::errorFlag()
|
||||
{
|
||||
return state().errorFlag();
|
||||
}
|
||||
|
||||
void CHC::newTxConstraints(Expression const* _value)
|
||||
{
|
||||
auto txOrigin = state().txMember("tx.origin");
|
||||
state().newTx();
|
||||
// set the transaction sender as this contract
|
||||
m_context.addAssertion(state().txMember("msg.sender") == state().thisAddress());
|
||||
// set the origin to be the current transaction origin
|
||||
m_context.addAssertion(state().txMember("tx.origin") == txOrigin);
|
||||
|
||||
if (_value)
|
||||
// set the msg value
|
||||
m_context.addAssertion(state().txMember("msg.value") == expr(*_value));
|
||||
}
|
||||
|
||||
frontend::Expression const* CHC::valueOption(FunctionCallOptions const* _options)
|
||||
{
|
||||
if (_options)
|
||||
for (auto&& [i, name]: _options->names() | ranges::views::enumerate)
|
||||
if (name && *name == "value")
|
||||
return _options->options().at(i).get();
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
void CHC::decreaseBalanceFromOptionsValue(Expression const& _value)
|
||||
{
|
||||
state().addBalance(state().thisAddress(), 0 - expr(_value));
|
||||
}
|
||||
|
||||
@ -110,10 +110,14 @@ private:
|
||||
void popInlineFrame(CallableDeclaration const& _callable) override;
|
||||
|
||||
void visitAssert(FunctionCall const& _funCall);
|
||||
void visitPublicGetter(FunctionCall const& _funCall) override;
|
||||
void visitAddMulMod(FunctionCall const& _funCall) override;
|
||||
void visitDeployment(FunctionCall const& _funCall);
|
||||
void internalFunctionCall(FunctionCall const& _funCall);
|
||||
void externalFunctionCall(FunctionCall const& _funCall);
|
||||
void externalFunctionCallToTrustedCode(FunctionCall const& _funCall);
|
||||
void addNondetCalls(ContractDefinition const& _contract);
|
||||
void nondetCall(ContractDefinition const& _contract, VariableDeclaration const& _var);
|
||||
void unknownFunctionCall(FunctionCall const& _funCall);
|
||||
void makeArrayPopVerificationTarget(FunctionCall const& _arrayPop) override;
|
||||
void makeOutOfBoundsVerificationTarget(IndexAccess const& _access) override;
|
||||
@ -135,6 +139,7 @@ private:
|
||||
void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override;
|
||||
void setCurrentBlock(Predicate const& _block);
|
||||
std::set<unsigned> transactionVerificationTargetsIds(ASTNode const* _txRoot);
|
||||
bool usesStaticCall(FunctionCall const& _funCall);
|
||||
//@}
|
||||
|
||||
/// SMT Natspec and abstraction helpers.
|
||||
@ -148,6 +153,10 @@ private:
|
||||
/// @returns true if _function is Natspec annotated to be abstracted by
|
||||
/// nondeterministic values.
|
||||
bool abstractAsNondet(FunctionDefinition const& _function);
|
||||
|
||||
/// @returns true if external calls should be considered trusted.
|
||||
/// If that's the case, their code is used if available at compile time.
|
||||
bool encodeExternalCallsAsTrusted();
|
||||
//@}
|
||||
|
||||
/// Sort helpers.
|
||||
@ -310,6 +319,20 @@ private:
|
||||
unsigned newErrorId();
|
||||
|
||||
smt::SymbolicIntVariable& errorFlag();
|
||||
|
||||
/// Adds to the solver constraints that
|
||||
/// - propagate tx.origin
|
||||
/// - set the current contract as msg.sender
|
||||
/// - set the msg.value as _value, if not nullptr
|
||||
void newTxConstraints(Expression const* _value);
|
||||
|
||||
/// @returns the expression representing the value sent in
|
||||
/// an external call if present,
|
||||
/// and nullptr otherwise.
|
||||
frontend::Expression const* valueOption(FunctionCallOptions const* _options);
|
||||
|
||||
/// Adds constraints that decrease the balance of the caller by _value.
|
||||
void decreaseBalanceFromOptionsValue(Expression const& _value);
|
||||
//@}
|
||||
|
||||
/// Predicates.
|
||||
|
||||
@ -130,3 +130,12 @@ std::optional<ModelCheckerContracts> ModelCheckerContracts::fromString(string co
|
||||
|
||||
return ModelCheckerContracts{chosen};
|
||||
}
|
||||
|
||||
std::optional<ModelCheckerExtCalls> ModelCheckerExtCalls::fromString(string const& _mode)
|
||||
{
|
||||
if (_mode == "untrusted")
|
||||
return ModelCheckerExtCalls{Mode::UNTRUSTED};
|
||||
if (_mode == "trusted")
|
||||
return ModelCheckerExtCalls{Mode::TRUSTED};
|
||||
return {};
|
||||
}
|
||||
|
||||
@ -140,6 +140,21 @@ struct ModelCheckerTargets
|
||||
std::set<VerificationTargetType> targets;
|
||||
};
|
||||
|
||||
struct ModelCheckerExtCalls
|
||||
{
|
||||
enum class Mode
|
||||
{
|
||||
UNTRUSTED,
|
||||
TRUSTED
|
||||
};
|
||||
|
||||
Mode mode = Mode::UNTRUSTED;
|
||||
|
||||
static std::optional<ModelCheckerExtCalls> fromString(std::string const& _mode);
|
||||
|
||||
bool isTrusted() const { return mode == Mode::TRUSTED; }
|
||||
};
|
||||
|
||||
struct ModelCheckerSettings
|
||||
{
|
||||
ModelCheckerContracts contracts = ModelCheckerContracts::Default();
|
||||
@ -151,6 +166,7 @@ struct ModelCheckerSettings
|
||||
/// might prefer the precise encoding.
|
||||
bool divModNoSlacks = false;
|
||||
ModelCheckerEngine engine = ModelCheckerEngine::None();
|
||||
ModelCheckerExtCalls externalCalls = {};
|
||||
ModelCheckerInvariants invariants = ModelCheckerInvariants::Default();
|
||||
bool showUnproved = false;
|
||||
smtutil::SMTSolverChoice solvers = smtutil::SMTSolverChoice::Z3();
|
||||
@ -164,6 +180,7 @@ struct ModelCheckerSettings
|
||||
contracts == _other.contracts &&
|
||||
divModNoSlacks == _other.divModNoSlacks &&
|
||||
engine == _other.engine &&
|
||||
externalCalls.mode == _other.externalCalls.mode &&
|
||||
invariants == _other.invariants &&
|
||||
showUnproved == _other.showUnproved &&
|
||||
solvers == _other.solvers &&
|
||||
|
||||
@ -144,6 +144,11 @@ FunctionCall const* Predicate::programFunctionCall() const
|
||||
return dynamic_cast<FunctionCall const*>(m_node);
|
||||
}
|
||||
|
||||
VariableDeclaration const* Predicate::programVariable() const
|
||||
{
|
||||
return dynamic_cast<VariableDeclaration const*>(m_node);
|
||||
}
|
||||
|
||||
optional<vector<VariableDeclaration const*>> Predicate::stateVariables() const
|
||||
{
|
||||
if (m_contractContext)
|
||||
@ -214,6 +219,9 @@ string Predicate::formatSummaryCall(
|
||||
{
|
||||
solAssert(isSummary(), "");
|
||||
|
||||
if (programVariable())
|
||||
return {};
|
||||
|
||||
if (auto funCall = programFunctionCall())
|
||||
{
|
||||
if (funCall->location().hasText())
|
||||
@ -348,6 +356,8 @@ vector<optional<string>> Predicate::summaryStateValues(vector<smtutil::Expressio
|
||||
stateFirst = _args.begin() + 7 + static_cast<int>(stateVars->size());
|
||||
stateLast = stateFirst + static_cast<int>(stateVars->size());
|
||||
}
|
||||
else if (programVariable())
|
||||
return {};
|
||||
else
|
||||
solAssert(false, "");
|
||||
|
||||
|
||||
@ -115,6 +115,10 @@ public:
|
||||
/// or nullptr otherwise.
|
||||
FunctionCall const* programFunctionCall() const;
|
||||
|
||||
/// @returns the VariableDeclaration that this predicate represents
|
||||
/// or nullptr otherwise.
|
||||
VariableDeclaration const* programVariable() const;
|
||||
|
||||
/// @returns the program state variables in the scope of this predicate.
|
||||
std::optional<std::vector<VariableDeclaration const*>> stateVariables() const;
|
||||
|
||||
|
||||
@ -70,14 +70,14 @@ smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _contex
|
||||
return _pred(stateExprs + initialStateVariables(contract, _context) + currentStateVariables(contract, _context));
|
||||
}
|
||||
|
||||
smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _context)
|
||||
smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _context, bool _internal)
|
||||
{
|
||||
auto const& contract = dynamic_cast<ContractDefinition const&>(*_pred.programNode());
|
||||
if (auto const* constructor = contract.constructor())
|
||||
return _pred(currentFunctionVariablesForCall(*constructor, &contract, _context));
|
||||
return _pred(currentFunctionVariablesForCall(*constructor, &contract, _context, _internal));
|
||||
|
||||
auto& state = _context.state();
|
||||
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state()};
|
||||
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), _internal ? state.thisAddress(0) : state.thisAddress(), state.abi(0), state.crypto(0), _internal ? state.tx(0) : state.tx(), state.state()};
|
||||
state.newState();
|
||||
stateExprs += vector<smtutil::Expression>{state.state()};
|
||||
stateExprs += currentStateVariables(contract, _context);
|
||||
@ -166,11 +166,12 @@ vector<smtutil::Expression> currentFunctionVariablesForDefinition(
|
||||
vector<smtutil::Expression> currentFunctionVariablesForCall(
|
||||
FunctionDefinition const& _function,
|
||||
ContractDefinition const* _contract,
|
||||
EncodingContext& _context
|
||||
EncodingContext& _context,
|
||||
bool _internal
|
||||
)
|
||||
{
|
||||
auto& state = _context.state();
|
||||
vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state()};
|
||||
vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), _internal ? state.thisAddress(0) : state.thisAddress(), state.abi(0), state.crypto(0), _internal ? state.tx(0) : state.tx(), state.state()};
|
||||
exprs += _contract ? currentStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
|
||||
exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });
|
||||
|
||||
|
||||
@ -37,7 +37,14 @@ smtutil::Expression interface(Predicate const& _pred, ContractDefinition const&
|
||||
smtutil::Expression nondetInterface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context, unsigned _preIdx, unsigned _postIdx);
|
||||
|
||||
smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _context);
|
||||
smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _context);
|
||||
/// The encoding of the deployment procedure includes adding constraints
|
||||
/// for base constructors if inheritance is used.
|
||||
/// From the predicate point of view this is not different,
|
||||
/// but some of the arguments are different.
|
||||
/// @param _internal = true means that this constructor call is used in the
|
||||
/// deployment procedure, whereas false means it is used in the deployment
|
||||
/// of a contract.
|
||||
smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _context, bool _internal = true);
|
||||
|
||||
smtutil::Expression function(
|
||||
Predicate const& _pred,
|
||||
@ -77,7 +84,8 @@ std::vector<smtutil::Expression> currentFunctionVariablesForDefinition(
|
||||
std::vector<smtutil::Expression> currentFunctionVariablesForCall(
|
||||
FunctionDefinition const& _function,
|
||||
ContractDefinition const* _contract,
|
||||
EncodingContext& _context
|
||||
EncodingContext& _context,
|
||||
bool _internal = true
|
||||
);
|
||||
|
||||
std::vector<smtutil::Expression> currentBlockVariables(
|
||||
|
||||
@ -637,7 +637,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
|
||||
visitGasLeft(_funCall);
|
||||
break;
|
||||
case FunctionType::Kind::External:
|
||||
if (isPublicGetter(_funCall.expression()))
|
||||
if (publicGetter(_funCall.expression()))
|
||||
visitPublicGetter(_funCall);
|
||||
break;
|
||||
case FunctionType::Kind::ABIDecode:
|
||||
@ -696,10 +696,18 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
|
||||
case FunctionType::Kind::ObjectCreation:
|
||||
visitObjectCreation(_funCall);
|
||||
return;
|
||||
case FunctionType::Kind::Creation:
|
||||
if (!m_settings.engine.chc || !m_settings.externalCalls.isTrusted())
|
||||
m_errorReporter.warning(
|
||||
8729_error,
|
||||
_funCall.location(),
|
||||
"Contract deployment is only supported in the trusted mode for external calls"
|
||||
" with the CHC engine."
|
||||
);
|
||||
break;
|
||||
case FunctionType::Kind::DelegateCall:
|
||||
case FunctionType::Kind::BareCallCode:
|
||||
case FunctionType::Kind::BareDelegateCall:
|
||||
case FunctionType::Kind::Creation:
|
||||
default:
|
||||
m_errorReporter.warning(
|
||||
4588_error,
|
||||
@ -978,9 +986,8 @@ vector<string> structGetterReturnedMembers(StructType const& _structType)
|
||||
|
||||
void SMTEncoder::visitPublicGetter(FunctionCall const& _funCall)
|
||||
{
|
||||
MemberAccess const& access = dynamic_cast<MemberAccess const&>(_funCall.expression());
|
||||
auto var = dynamic_cast<VariableDeclaration const*>(access.annotation().referencedDeclaration);
|
||||
solAssert(var, "");
|
||||
auto var = publicGetter(_funCall.expression());
|
||||
solAssert(var && var->isStateVariable(), "");
|
||||
solAssert(m_context.knownExpression(_funCall), "");
|
||||
auto paramExpectedTypes = replaceUserTypes(FunctionType(*var).parameterTypes());
|
||||
auto actualArguments = _funCall.arguments();
|
||||
@ -1054,7 +1061,7 @@ bool SMTEncoder::shouldAnalyze(ContractDefinition const& _contract) const
|
||||
return false;
|
||||
|
||||
return m_settings.contracts.isDefault() ||
|
||||
m_settings.contracts.has(_contract.sourceUnitName(), _contract.name());
|
||||
m_settings.contracts.has(_contract.sourceUnitName());
|
||||
}
|
||||
|
||||
void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
|
||||
@ -2789,16 +2796,24 @@ MemberAccess const* SMTEncoder::isEmptyPush(Expression const& _expr) const
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
bool SMTEncoder::isPublicGetter(Expression const& _expr) {
|
||||
if (!isTrustedExternalCall(&_expr))
|
||||
return false;
|
||||
auto varDecl = dynamic_cast<VariableDeclaration const*>(
|
||||
dynamic_cast<MemberAccess const&>(_expr).annotation().referencedDeclaration
|
||||
);
|
||||
return varDecl != nullptr;
|
||||
smtutil::Expression SMTEncoder::contractAddressValue(FunctionCall const& _f)
|
||||
{
|
||||
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_f.expression().annotation().type);
|
||||
if (funType.kind() == FunctionType::Kind::Internal)
|
||||
return state().thisAddress();
|
||||
auto [funExpr, funOptions] = functionCallExpression(_f);
|
||||
if (MemberAccess const* callBase = dynamic_cast<MemberAccess const*>(funExpr))
|
||||
return expr(callBase->expression());
|
||||
solAssert(false, "Unreachable!");
|
||||
}
|
||||
|
||||
bool SMTEncoder::isTrustedExternalCall(Expression const* _expr) {
|
||||
VariableDeclaration const* SMTEncoder::publicGetter(Expression const& _expr) const {
|
||||
if (auto memberAccess = dynamic_cast<MemberAccess const*>(&_expr))
|
||||
return dynamic_cast<VariableDeclaration const*>(memberAccess->annotation().referencedDeclaration);
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
bool SMTEncoder::isExternalCallToThis(Expression const* _expr) {
|
||||
auto memberAccess = dynamic_cast<MemberAccess const*>(_expr);
|
||||
if (!memberAccess)
|
||||
return false;
|
||||
@ -3060,7 +3075,7 @@ RationalNumberType const* SMTEncoder::isConstant(Expression const& _expr)
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
set<FunctionCall const*> SMTEncoder::collectABICalls(ASTNode const* _node)
|
||||
set<FunctionCall const*, ASTCompareByID<FunctionCall>> SMTEncoder::collectABICalls(ASTNode const* _node)
|
||||
{
|
||||
struct ABIFunctions: public ASTConstVisitor
|
||||
{
|
||||
@ -3082,7 +3097,7 @@ set<FunctionCall const*> SMTEncoder::collectABICalls(ASTNode const* _node)
|
||||
}
|
||||
}
|
||||
|
||||
set<FunctionCall const*> abiCalls;
|
||||
set<FunctionCall const*, ASTCompareByID<FunctionCall>> abiCalls;
|
||||
};
|
||||
|
||||
return ABIFunctions(_node).abiCalls;
|
||||
|
||||
@ -123,7 +123,7 @@ public:
|
||||
/// RationalNumberType or can be const evaluated, and nullptr otherwise.
|
||||
static RationalNumberType const* isConstant(Expression const& _expr);
|
||||
|
||||
static std::set<FunctionCall const*> collectABICalls(ASTNode const* _node);
|
||||
static std::set<FunctionCall const*, ASTCompareByID<FunctionCall>> collectABICalls(ASTNode const* _node);
|
||||
|
||||
/// @returns all the sources that @param _source depends on,
|
||||
/// including itself.
|
||||
@ -219,7 +219,7 @@ protected:
|
||||
void visitTypeConversion(FunctionCall const& _funCall);
|
||||
void visitStructConstructorCall(FunctionCall const& _funCall);
|
||||
void visitFunctionIdentifier(Identifier const& _identifier);
|
||||
void visitPublicGetter(FunctionCall const& _funCall);
|
||||
virtual void visitPublicGetter(FunctionCall const& _funCall);
|
||||
|
||||
/// @returns true if @param _contract is set for analysis in the settings
|
||||
/// and it is not abstract.
|
||||
@ -227,7 +227,12 @@ protected:
|
||||
/// @returns true if @param _source is set for analysis in the settings.
|
||||
bool shouldAnalyze(SourceUnit const& _source) const;
|
||||
|
||||
bool isPublicGetter(Expression const& _expr);
|
||||
/// @returns the state variable returned by a public getter if
|
||||
/// @a _expr is a call to a public getter,
|
||||
/// otherwise nullptr.
|
||||
VariableDeclaration const* publicGetter(Expression const& _expr) const;
|
||||
|
||||
smtutil::Expression contractAddressValue(FunctionCall const& _f);
|
||||
|
||||
/// Encodes a modifier or function body according to the modifier
|
||||
/// visit depth.
|
||||
@ -392,9 +397,9 @@ protected:
|
||||
/// otherwise nullptr.
|
||||
MemberAccess const* isEmptyPush(Expression const& _expr) const;
|
||||
|
||||
/// @returns true if the given identifier is a contract which is known and trusted.
|
||||
/// @returns true if the given expression is `this`.
|
||||
/// This means we don't have to abstract away effects of external function calls to this contract.
|
||||
static bool isTrustedExternalCall(Expression const* _expr);
|
||||
static bool isExternalCallToThis(Expression const* _expr);
|
||||
|
||||
/// Creates symbolic expressions for the returned values
|
||||
/// and set them as the components of the symbolic tuple.
|
||||
|
||||
@ -22,8 +22,13 @@
|
||||
#include <libsolidity/formal/EncodingContext.h>
|
||||
#include <libsolidity/formal/SMTEncoder.h>
|
||||
|
||||
#include <libsmtutil/Sorts.h>
|
||||
|
||||
#include <range/v3/view.hpp>
|
||||
|
||||
using namespace std;
|
||||
using namespace solidity;
|
||||
using namespace solidity::util;
|
||||
using namespace solidity::smtutil;
|
||||
using namespace solidity::frontend::smt;
|
||||
|
||||
@ -58,16 +63,8 @@ smtutil::Expression BlockchainVariable::member(string const& _member) const
|
||||
|
||||
smtutil::Expression BlockchainVariable::assignMember(string const& _member, smtutil::Expression const& _value)
|
||||
{
|
||||
vector<smtutil::Expression> args;
|
||||
for (auto const& m: m_members)
|
||||
if (m.first == _member)
|
||||
args.emplace_back(_value);
|
||||
else
|
||||
args.emplace_back(member(m.first));
|
||||
m_tuple->increaseIndex();
|
||||
auto tuple = m_tuple->currentValue();
|
||||
auto sortExpr = smtutil::Expression(make_shared<smtutil::SortSort>(tuple.sort), tuple.name);
|
||||
m_context.addAssertion(tuple == smtutil::Expression::tuple_constructor(sortExpr, args));
|
||||
smtutil::Expression newTuple = smt::assignMember(m_tuple->currentValue(), {{_member, _value}});
|
||||
m_context.addAssertion(m_tuple->increaseIndex() == newTuple);
|
||||
return m_tuple->currentValue();
|
||||
}
|
||||
|
||||
@ -75,16 +72,19 @@ void SymbolicState::reset()
|
||||
{
|
||||
m_error.resetIndex();
|
||||
m_thisAddress.resetIndex();
|
||||
m_state.reset();
|
||||
m_tx.reset();
|
||||
m_crypto.reset();
|
||||
if (m_abi)
|
||||
m_abi->reset();
|
||||
/// We don't reset nor clear these pointers on purpose,
|
||||
/// since it only helps to keep the already generated types.
|
||||
if (m_state)
|
||||
m_state->reset();
|
||||
}
|
||||
|
||||
smtutil::Expression SymbolicState::balances() const
|
||||
{
|
||||
return m_state.member("balances");
|
||||
return m_state->member("balances");
|
||||
}
|
||||
|
||||
smtutil::Expression SymbolicState::balance() const
|
||||
@ -107,24 +107,94 @@ void SymbolicState::newBalances()
|
||||
auto tupleSort = dynamic_pointer_cast<TupleSort>(stateSort());
|
||||
auto balanceSort = tupleSort->components.at(tupleSort->memberToIndex.at("balances"));
|
||||
SymbolicVariable newBalances(balanceSort, "fresh_balances_" + to_string(m_context.newUniqueId()), m_context);
|
||||
m_state.assignMember("balances", newBalances.currentValue());
|
||||
m_state->assignMember("balances", newBalances.currentValue());
|
||||
}
|
||||
|
||||
void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value)
|
||||
{
|
||||
unsigned indexBefore = m_state.index();
|
||||
unsigned indexBefore = m_state->index();
|
||||
addBalance(_from, 0 - _value);
|
||||
addBalance(_to, std::move(_value));
|
||||
unsigned indexAfter = m_state.index();
|
||||
unsigned indexAfter = m_state->index();
|
||||
solAssert(indexAfter > indexBefore, "");
|
||||
m_state.newVar();
|
||||
m_state->newVar();
|
||||
/// Do not apply the transfer operation if _from == _to.
|
||||
auto newState = smtutil::Expression::ite(
|
||||
std::move(_from) == std::move(_to),
|
||||
m_state.value(indexBefore),
|
||||
m_state.value(indexAfter)
|
||||
m_state->value(indexBefore),
|
||||
m_state->value(indexAfter)
|
||||
);
|
||||
m_context.addAssertion(m_state.value() == newState);
|
||||
m_context.addAssertion(m_state->value() == newState);
|
||||
}
|
||||
|
||||
smtutil::Expression SymbolicState::storage(ContractDefinition const& _contract) const
|
||||
{
|
||||
return smt::member(m_state->member("storage"), contractStorageKey(_contract));
|
||||
}
|
||||
|
||||
smtutil::Expression SymbolicState::storage(ContractDefinition const& _contract, smtutil::Expression _address) const
|
||||
{
|
||||
return smtutil::Expression::select(storage(_contract), std::move(_address));
|
||||
}
|
||||
|
||||
smtutil::Expression SymbolicState::addressActive(smtutil::Expression _address) const
|
||||
{
|
||||
return smtutil::Expression::select(m_state->member("isActive"), std::move(_address));
|
||||
}
|
||||
|
||||
void SymbolicState::setAddressActive(
|
||||
smtutil::Expression _address,
|
||||
bool _active
|
||||
)
|
||||
{
|
||||
m_state->assignMember("isActive", smtutil::Expression::store(
|
||||
m_state->member("isActive"),
|
||||
std::move(_address),
|
||||
smtutil::Expression(_active))
|
||||
);
|
||||
}
|
||||
|
||||
void SymbolicState::newStorage()
|
||||
{
|
||||
auto newStorageVar = SymbolicTupleVariable(
|
||||
m_state->member("storage").sort,
|
||||
"havoc_storage_" + to_string(m_context.newUniqueId()),
|
||||
m_context
|
||||
);
|
||||
m_state->assignMember("storage", newStorageVar.currentValue());
|
||||
}
|
||||
|
||||
void SymbolicState::writeStateVars(ContractDefinition const& _contract, smtutil::Expression _address)
|
||||
{
|
||||
auto stateVars = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract);
|
||||
if (stateVars.empty())
|
||||
return;
|
||||
|
||||
map<string, smtutil::Expression> values;
|
||||
for (auto var: stateVars)
|
||||
values.emplace(stateVarStorageKey(*var, _contract), m_context.variable(*var)->currentValue());
|
||||
|
||||
smtutil::Expression thisStorage = storage(_contract, _address);
|
||||
smtutil::Expression newStorage = smt::assignMember(thisStorage, values);
|
||||
auto newContractStorage = smtutil::Expression::store(
|
||||
storage(_contract), std::move(_address), newStorage
|
||||
);
|
||||
smtutil::Expression newAllStorage = smt::assignMember(m_state->member("storage"), {{contractStorageKey(_contract), newContractStorage}});
|
||||
m_state->assignMember("storage", newAllStorage);
|
||||
}
|
||||
|
||||
void SymbolicState::readStateVars(ContractDefinition const& _contract, smtutil::Expression _address)
|
||||
{
|
||||
auto stateVars = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract);
|
||||
if (stateVars.empty())
|
||||
return;
|
||||
|
||||
auto contractStorage = storage(_contract, std::move(_address));
|
||||
for (auto var: stateVars)
|
||||
m_context.addAssertion(
|
||||
m_context.variable(*var)->increaseIndex() ==
|
||||
smt::member(contractStorage, stateVarStorageKey(*var, _contract))
|
||||
);
|
||||
}
|
||||
|
||||
void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression _value)
|
||||
@ -134,7 +204,7 @@ void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression
|
||||
_address,
|
||||
balance(_address) + std::move(_value)
|
||||
);
|
||||
m_state.assignMember("balances", newBalances);
|
||||
m_state->assignMember("balances", newBalances);
|
||||
}
|
||||
|
||||
smtutil::Expression SymbolicState::txMember(string const& _member) const
|
||||
@ -194,17 +264,99 @@ smtutil::Expression SymbolicState::txFunctionConstraints(FunctionDefinition cons
|
||||
return conj;
|
||||
}
|
||||
|
||||
void SymbolicState::prepareForSourceUnit(SourceUnit const& _source)
|
||||
void SymbolicState::prepareForSourceUnit(SourceUnit const& _source, bool _storage)
|
||||
{
|
||||
set<FunctionCall const*> abiCalls = SMTEncoder::collectABICalls(&_source);
|
||||
for (auto const& source: _source.referencedSourceUnits(true))
|
||||
auto allSources = _source.referencedSourceUnits(true);
|
||||
allSources.insert(&_source);
|
||||
set<FunctionCall const*, ASTCompareByID<FunctionCall>> abiCalls;
|
||||
set<ContractDefinition const*, ASTCompareByID<ContractDefinition>> contracts;
|
||||
for (auto const& source: allSources)
|
||||
{
|
||||
abiCalls += SMTEncoder::collectABICalls(source);
|
||||
for (auto node: source->nodes())
|
||||
if (auto contract = dynamic_cast<ContractDefinition const*>(node.get()))
|
||||
contracts.insert(contract);
|
||||
}
|
||||
buildState(contracts, _storage);
|
||||
buildABIFunctions(abiCalls);
|
||||
}
|
||||
|
||||
/// Private helpers.
|
||||
|
||||
void SymbolicState::buildABIFunctions(set<FunctionCall const*> const& _abiFunctions)
|
||||
string SymbolicState::contractSuffix(ContractDefinition const& _contract) const
|
||||
{
|
||||
return "_" + _contract.name() + "_" + to_string(_contract.id());
|
||||
}
|
||||
|
||||
string SymbolicState::contractStorageKey(ContractDefinition const& _contract) const
|
||||
{
|
||||
return "storage" + contractSuffix(_contract);
|
||||
}
|
||||
|
||||
string SymbolicState::stateVarStorageKey(VariableDeclaration const& _var, ContractDefinition const& _contract) const
|
||||
{
|
||||
return _var.name() + "_" + to_string(_var.id()) + contractSuffix(_contract);
|
||||
}
|
||||
|
||||
void SymbolicState::buildState(set<ContractDefinition const*, ASTCompareByID<ContractDefinition>> const& _contracts, bool _allStorages)
|
||||
{
|
||||
map<string, SortPointer> stateMembers{
|
||||
{"balances", make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)}
|
||||
};
|
||||
|
||||
if (_allStorages)
|
||||
{
|
||||
vector<string> memberNames;
|
||||
vector<SortPointer> memberSorts;
|
||||
for (auto contract: _contracts)
|
||||
{
|
||||
string suffix = contractSuffix(*contract);
|
||||
|
||||
// z3 doesn't like empty tuples, so if the contract has 0
|
||||
// state vars we can't put it there.
|
||||
auto stateVars = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*contract);
|
||||
if (stateVars.empty())
|
||||
continue;
|
||||
|
||||
auto names = applyMap(stateVars, [&](auto var) {
|
||||
return var->name() + "_" + to_string(var->id()) + suffix;
|
||||
});
|
||||
auto sorts = applyMap(stateVars, [](auto var) { return smtSortAbstractFunction(*var->type()); });
|
||||
|
||||
string name = "storage" + suffix;
|
||||
auto storageTuple = make_shared<smtutil::TupleSort>(
|
||||
name + "_type", names, sorts
|
||||
);
|
||||
|
||||
auto storageSort = make_shared<smtutil::ArraySort>(
|
||||
smtSort(*TypeProvider::address()),
|
||||
storageTuple
|
||||
);
|
||||
|
||||
memberNames.emplace_back(name);
|
||||
memberSorts.emplace_back(storageSort);
|
||||
}
|
||||
|
||||
stateMembers.emplace(
|
||||
"isActive",
|
||||
make_shared<smtutil::ArraySort>(smtSort(*TypeProvider::address()), smtutil::SortProvider::boolSort)
|
||||
);
|
||||
stateMembers.emplace(
|
||||
"storage",
|
||||
make_shared<smtutil::TupleSort>(
|
||||
"storage_type", memberNames, memberSorts
|
||||
)
|
||||
);
|
||||
}
|
||||
|
||||
m_state = make_unique<BlockchainVariable>(
|
||||
"state",
|
||||
std::move(stateMembers),
|
||||
m_context
|
||||
);
|
||||
}
|
||||
|
||||
void SymbolicState::buildABIFunctions(set<FunctionCall const*, ASTCompareByID<FunctionCall>> const& _abiFunctions)
|
||||
{
|
||||
map<string, SortPointer> functions;
|
||||
|
||||
|
||||
@ -62,7 +62,8 @@ private:
|
||||
* - this (the address of the currently executing contract)
|
||||
* - state, represented as a tuple of:
|
||||
* - balances
|
||||
* - TODO: potentially storage of contracts
|
||||
* - array of address => bool representing whether an address is used by a contract
|
||||
* - storage of contracts
|
||||
* - block and transaction properties, represented as a tuple of:
|
||||
* - blockhash
|
||||
* - block basefee
|
||||
@ -99,29 +100,41 @@ public:
|
||||
/// @returns the symbolic value of the currently executing contract's address.
|
||||
smtutil::Expression thisAddress() const { return m_thisAddress.currentValue(); }
|
||||
smtutil::Expression thisAddress(unsigned _idx) const { return m_thisAddress.valueAtIndex(_idx); }
|
||||
smtutil::Expression newThisAddress() { return m_thisAddress.increaseIndex(); }
|
||||
smtutil::SortPointer const& thisAddressSort() const { return m_thisAddress.sort(); }
|
||||
//@}
|
||||
|
||||
/// Blockchain state.
|
||||
//@{
|
||||
smtutil::Expression state() const { return m_state.value(); }
|
||||
smtutil::Expression state(unsigned _idx) const { return m_state.value(_idx); }
|
||||
smtutil::SortPointer const& stateSort() const { return m_state.sort(); }
|
||||
void newState() { m_state.newVar(); }
|
||||
smtutil::Expression state() const { solAssert(m_state, ""); return m_state->value(); }
|
||||
smtutil::Expression state(unsigned _idx) const { solAssert(m_state, ""); return m_state->value(_idx); }
|
||||
smtutil::SortPointer const& stateSort() const { solAssert(m_state, ""); return m_state->sort(); }
|
||||
void newState() { solAssert(m_state, ""); m_state->newVar(); }
|
||||
|
||||
void newBalances();
|
||||
|
||||
/// Balance.
|
||||
/// @returns the symbolic balances.
|
||||
smtutil::Expression balances() const;
|
||||
/// @returns the symbolic balance of address `this`.
|
||||
smtutil::Expression balance() const;
|
||||
/// @returns the symbolic balance of an address.
|
||||
smtutil::Expression balance(smtutil::Expression _address) const;
|
||||
|
||||
/// Transfer _value from _from to _to.
|
||||
void transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value);
|
||||
|
||||
/// Adds _value to _account's balance.
|
||||
void addBalance(smtutil::Expression _account, smtutil::Expression _value);
|
||||
|
||||
/// Storage.
|
||||
smtutil::Expression storage(ContractDefinition const& _contract) const;
|
||||
smtutil::Expression storage(ContractDefinition const& _contract, smtutil::Expression _address) const;
|
||||
smtutil::Expression addressActive(smtutil::Expression _address) const;
|
||||
void setAddressActive(smtutil::Expression _address, bool _active);
|
||||
|
||||
void newStorage();
|
||||
void writeStateVars(ContractDefinition const& _contract, smtutil::Expression _address);
|
||||
void readStateVars(ContractDefinition const& _contract, smtutil::Expression _address);
|
||||
//@}
|
||||
|
||||
/// Transaction data.
|
||||
@ -149,11 +162,15 @@ public:
|
||||
smtutil::Expression cryptoFunction(std::string const& _member) const { return m_crypto.member(_member); }
|
||||
//@}
|
||||
|
||||
/// Calls the internal methods that build
|
||||
/// - the symbolic ABI functions based on the abi.* calls
|
||||
/// in _source and referenced sources.
|
||||
/// - the symbolic storages for all contracts in _source and
|
||||
/// referenced sources.
|
||||
void prepareForSourceUnit(SourceUnit const& _source, bool _storage);
|
||||
|
||||
/// ABI functions.
|
||||
//@{
|
||||
/// Calls the internal methods that build the symbolic ABI functions
|
||||
/// based on the abi.* calls in _source and referenced sources.
|
||||
void prepareForSourceUnit(SourceUnit const& _source);
|
||||
smtutil::Expression abiFunction(FunctionCall const* _funCall);
|
||||
using SymbolicABIFunction = std::tuple<
|
||||
std::string,
|
||||
@ -169,8 +186,15 @@ public:
|
||||
//@}
|
||||
|
||||
private:
|
||||
std::string contractSuffix(ContractDefinition const& _contract) const;
|
||||
std::string contractStorageKey(ContractDefinition const& _contract) const;
|
||||
std::string stateVarStorageKey(VariableDeclaration const& _var, ContractDefinition const& _contract) const;
|
||||
|
||||
/// Builds state.storage based on _contracts.
|
||||
void buildState(std::set<ContractDefinition const*, ASTCompareByID<ContractDefinition>> const& _contracts, bool _allStorages);
|
||||
|
||||
/// Builds m_abi based on the abi.* calls _abiFunctions.
|
||||
void buildABIFunctions(std::set<FunctionCall const*> const& _abiFunctions);
|
||||
void buildABIFunctions(std::set<FunctionCall const*, ASTCompareByID<FunctionCall>> const& _abiFunctions);
|
||||
|
||||
EncodingContext& m_context;
|
||||
|
||||
@ -186,11 +210,14 @@ private:
|
||||
m_context
|
||||
};
|
||||
|
||||
BlockchainVariable m_state{
|
||||
"state",
|
||||
{{"balances", std::make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)}},
|
||||
m_context
|
||||
};
|
||||
/// m_state is a tuple of
|
||||
/// - balances: array of address to balance of address.
|
||||
/// - isActive: array of address to Boolean, where element is true iff address is used.
|
||||
/// - storage: tuple containing the storage of every contract, where
|
||||
/// each element of the tuple represents a contract,
|
||||
/// and is defined by an array where the index is the contract's address
|
||||
/// and the element is a tuple containing the state variables of that contract.
|
||||
std::unique_ptr<BlockchainVariable> m_state;
|
||||
|
||||
BlockchainVariable m_tx{
|
||||
"tx",
|
||||
|
||||
@ -618,4 +618,26 @@ optional<smtutil::Expression> symbolicTypeConversion(frontend::Type const* _from
|
||||
return std::nullopt;
|
||||
}
|
||||
|
||||
smtutil::Expression member(smtutil::Expression const& _tuple, string const& _member)
|
||||
{
|
||||
TupleSort const& _sort = dynamic_cast<TupleSort const&>(*_tuple.sort);
|
||||
return smtutil::Expression::tuple_get(
|
||||
_tuple,
|
||||
_sort.memberToIndex.at(_member)
|
||||
);
|
||||
}
|
||||
|
||||
smtutil::Expression assignMember(smtutil::Expression const _tuple, map<string, smtutil::Expression> const& _values)
|
||||
{
|
||||
TupleSort const& _sort = dynamic_cast<TupleSort const&>(*_tuple.sort);
|
||||
vector<smtutil::Expression> args;
|
||||
for (auto const& m: _sort.members)
|
||||
if (auto* value = util::valueOrNullptr(_values, m))
|
||||
args.emplace_back(*value);
|
||||
else
|
||||
args.emplace_back(member(_tuple, m));
|
||||
auto sortExpr = smtutil::Expression(make_shared<smtutil::SortSort>(_tuple.sort), _tuple.name);
|
||||
return smtutil::Expression::tuple_constructor(sortExpr, args);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
@ -82,4 +82,8 @@ void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::Type const* _t
|
||||
smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, frontend::Type const* _type);
|
||||
|
||||
std::optional<smtutil::Expression> symbolicTypeConversion(frontend::Type const* _from, frontend::Type const* _to);
|
||||
|
||||
smtutil::Expression member(smtutil::Expression const& _tuple, std::string const& _member);
|
||||
smtutil::Expression assignMember(smtutil::Expression const _tuple, std::map<std::string, smtutil::Expression> const& _values);
|
||||
|
||||
}
|
||||
|
||||
@ -445,7 +445,7 @@ std::optional<Json::Value> checkSettingsKeys(Json::Value const& _input)
|
||||
|
||||
std::optional<Json::Value> checkModelCheckerSettingsKeys(Json::Value const& _input)
|
||||
{
|
||||
static set<string> keys{"contracts", "divModNoSlacks", "engine", "invariants", "showUnproved", "solvers", "targets", "timeout"};
|
||||
static set<string> keys{"contracts", "divModNoSlacks", "engine", "extCalls", "invariants", "showUnproved", "solvers", "targets", "timeout"};
|
||||
return checkKeys(_input, keys, "modelChecker");
|
||||
}
|
||||
|
||||
@ -1016,6 +1016,16 @@ std::variant<StandardCompiler::InputsAndSettings, Json::Value> StandardCompiler:
|
||||
ret.modelCheckerSettings.engine = *engine;
|
||||
}
|
||||
|
||||
if (modelCheckerSettings.isMember("extCalls"))
|
||||
{
|
||||
if (!modelCheckerSettings["extCalls"].isString())
|
||||
return formatFatalError(Error::Type::JSONError, "settings.modelChecker.extCalls must be a string.");
|
||||
std::optional<ModelCheckerExtCalls> extCalls = ModelCheckerExtCalls::fromString(modelCheckerSettings["extCalls"].asString());
|
||||
if (!extCalls)
|
||||
return formatFatalError(Error::Type::JSONError, "Invalid model checker extCalls requested.");
|
||||
ret.modelCheckerSettings.externalCalls = *extCalls;
|
||||
}
|
||||
|
||||
if (modelCheckerSettings.isMember("invariants"))
|
||||
{
|
||||
auto const& invariantsArray = modelCheckerSettings["invariants"];
|
||||
|
||||
@ -69,6 +69,7 @@ static string const g_strMetadataLiteral = "metadata-literal";
|
||||
static string const g_strModelCheckerContracts = "model-checker-contracts";
|
||||
static string const g_strModelCheckerDivModNoSlacks = "model-checker-div-mod-no-slacks";
|
||||
static string const g_strModelCheckerEngine = "model-checker-engine";
|
||||
static string const g_strModelCheckerExtCalls = "model-checker-ext-calls";
|
||||
static string const g_strModelCheckerInvariants = "model-checker-invariants";
|
||||
static string const g_strModelCheckerShowUnproved = "model-checker-show-unproved";
|
||||
static string const g_strModelCheckerSolvers = "model-checker-solvers";
|
||||
@ -831,6 +832,12 @@ General Information)").c_str(),
|
||||
po::value<string>()->value_name("all,bmc,chc,none")->default_value("none"),
|
||||
"Select model checker engine."
|
||||
)
|
||||
(
|
||||
g_strModelCheckerExtCalls.c_str(),
|
||||
po::value<string>()->value_name("untrusted,trusted")->default_value("untrusted"),
|
||||
"Select whether to assume (trusted) that external calls always invoke"
|
||||
" the code given by the type of the contract, if that code is available."
|
||||
)
|
||||
(
|
||||
g_strModelCheckerInvariants.c_str(),
|
||||
po::value<string>()->value_name("default,all,contract,reentrancy")->default_value("default"),
|
||||
@ -1289,6 +1296,15 @@ void CommandLineParser::processArgs()
|
||||
m_options.modelChecker.settings.engine = *engine;
|
||||
}
|
||||
|
||||
if (m_args.count(g_strModelCheckerExtCalls))
|
||||
{
|
||||
string mode = m_args[g_strModelCheckerExtCalls].as<string>();
|
||||
optional<ModelCheckerExtCalls> extCallsMode = ModelCheckerExtCalls::fromString(mode);
|
||||
if (!extCallsMode)
|
||||
solThrow(CommandLineValidationError, "Invalid option for --" + g_strModelCheckerExtCalls + ": " + mode);
|
||||
m_options.modelChecker.settings.externalCalls = *extCallsMode;
|
||||
}
|
||||
|
||||
if (m_args.count(g_strModelCheckerInvariants))
|
||||
{
|
||||
string invsStr = m_args[g_strModelCheckerInvariants].as<string>();
|
||||
@ -1327,6 +1343,7 @@ void CommandLineParser::processArgs()
|
||||
m_args.count(g_strModelCheckerContracts) ||
|
||||
m_args.count(g_strModelCheckerDivModNoSlacks) ||
|
||||
m_args.count(g_strModelCheckerEngine) ||
|
||||
m_args.count(g_strModelCheckerExtCalls) ||
|
||||
m_args.count(g_strModelCheckerInvariants) ||
|
||||
m_args.count(g_strModelCheckerShowUnproved) ||
|
||||
m_args.count(g_strModelCheckerSolvers) ||
|
||||
|
||||
@ -1 +1,27 @@
|
||||
Warning: Requested contract "C" does not exist in source "model_checker_contracts_inexistent_contract/input.sol".
|
||||
|
||||
Warning: CHC: Assertion violation happens here.
|
||||
Counterexample:
|
||||
|
||||
x = 0
|
||||
|
||||
Transaction trace:
|
||||
B.constructor()
|
||||
B.f(0)
|
||||
--> model_checker_contracts_inexistent_contract/input.sol:5:3:
|
||||
|
|
||||
5 | assert(x > 0);
|
||||
| ^^^^^^^^^^^^^
|
||||
|
||||
Warning: CHC: Assertion violation happens here.
|
||||
Counterexample:
|
||||
|
||||
y = 0
|
||||
|
||||
Transaction trace:
|
||||
A.constructor()
|
||||
A.g(0)
|
||||
--> model_checker_contracts_inexistent_contract/input.sol:10:3:
|
||||
|
|
||||
10 | assert(y > 0);
|
||||
| ^^^^^^^^^^^^^
|
||||
|
||||
@ -4,7 +4,7 @@ Counterexample:
|
||||
x = 0
|
||||
|
||||
Transaction trace:
|
||||
A.constructor()
|
||||
B.constructor()
|
||||
B.f(0)
|
||||
--> model_checker_contracts_only_one/input.sol:5:3:
|
||||
|
|
||||
|
||||
1
test/cmdlineTests/model_checker_ext_calls_empty_arg/args
Normal file
1
test/cmdlineTests/model_checker_ext_calls_empty_arg/args
Normal file
@ -0,0 +1 @@
|
||||
--model-checker-engine chc --model-checker-ext-calls
|
||||
1
test/cmdlineTests/model_checker_ext_calls_empty_arg/err
Normal file
1
test/cmdlineTests/model_checker_ext_calls_empty_arg/err
Normal file
@ -0,0 +1 @@
|
||||
No input files given. If you wish to use the standard input please specify "-" explicitly.
|
||||
1
test/cmdlineTests/model_checker_ext_calls_empty_arg/exit
Normal file
1
test/cmdlineTests/model_checker_ext_calls_empty_arg/exit
Normal file
@ -0,0 +1 @@
|
||||
1
|
||||
@ -0,0 +1,15 @@
|
||||
// SPDX-License-Identifier: GPL-3.0
|
||||
pragma solidity >=0.0;
|
||||
|
||||
contract Ext {
|
||||
function f() public view returns (uint) {
|
||||
return 42;
|
||||
}
|
||||
}
|
||||
|
||||
contract test {
|
||||
function g(Ext e) public view {
|
||||
uint x = e.f();
|
||||
assert(x == 42);
|
||||
}
|
||||
}
|
||||
@ -0,0 +1 @@
|
||||
--model-checker-engine chc --model-checker-ext-calls trusted
|
||||
@ -0,0 +1,5 @@
|
||||
Warning: Function state mutability can be restricted to pure
|
||||
--> model_checker_ext_calls_trusted_chc/input.sol:5:2:
|
||||
|
|
||||
5 | function f() public view returns (uint) {
|
||||
| ^ (Relevant source part starts here and spans across multiple lines).
|
||||
@ -0,0 +1,15 @@
|
||||
// SPDX-License-Identifier: GPL-3.0
|
||||
pragma solidity >=0.0;
|
||||
|
||||
contract Ext {
|
||||
function f() public view returns (uint) {
|
||||
return 42;
|
||||
}
|
||||
}
|
||||
|
||||
contract test {
|
||||
function g(Ext e) public view {
|
||||
uint x = e.f();
|
||||
assert(x == 42);
|
||||
}
|
||||
}
|
||||
@ -0,0 +1 @@
|
||||
--model-checker-engine chc --model-checker-ext-calls untrusted
|
||||
14
test/cmdlineTests/model_checker_ext_calls_untrusted_chc/err
Normal file
14
test/cmdlineTests/model_checker_ext_calls_untrusted_chc/err
Normal file
@ -0,0 +1,14 @@
|
||||
Warning: CHC: Assertion violation happens here.
|
||||
Counterexample:
|
||||
|
||||
e = 0
|
||||
x = 1
|
||||
|
||||
Transaction trace:
|
||||
test.constructor()
|
||||
test.g(0)
|
||||
e.f() -- untrusted external call
|
||||
--> model_checker_ext_calls_untrusted_chc/input.sol:11:3:
|
||||
|
|
||||
11 | assert(x == 0);
|
||||
| ^^^^^^^^^^^^^^
|
||||
@ -0,0 +1,13 @@
|
||||
// SPDX-License-Identifier: GPL-3.0
|
||||
pragma solidity >=0.0;
|
||||
|
||||
abstract contract Ext {
|
||||
function f() virtual public view returns (uint);
|
||||
}
|
||||
|
||||
contract test {
|
||||
function g(Ext e) public view {
|
||||
uint x = e.f();
|
||||
assert(x == 0);
|
||||
}
|
||||
}
|
||||
1
test/cmdlineTests/model_checker_ext_calls_wrong_arg/args
Normal file
1
test/cmdlineTests/model_checker_ext_calls_wrong_arg/args
Normal file
@ -0,0 +1 @@
|
||||
--model-checker-engine chc --model-checker-ext-calls what
|
||||
1
test/cmdlineTests/model_checker_ext_calls_wrong_arg/err
Normal file
1
test/cmdlineTests/model_checker_ext_calls_wrong_arg/err
Normal file
@ -0,0 +1 @@
|
||||
Invalid option for --model-checker-ext-calls: what
|
||||
1
test/cmdlineTests/model_checker_ext_calls_wrong_arg/exit
Normal file
1
test/cmdlineTests/model_checker_ext_calls_wrong_arg/exit
Normal file
@ -0,0 +1 @@
|
||||
1
|
||||
@ -0,0 +1,15 @@
|
||||
// SPDX-License-Identifier: GPL-3.0
|
||||
pragma solidity >=0.0;
|
||||
|
||||
contract Ext {
|
||||
function f() public view returns (uint) {
|
||||
return 42;
|
||||
}
|
||||
}
|
||||
|
||||
contract test {
|
||||
function g(Ext e) public view {
|
||||
uint x = e.f();
|
||||
assert(x == 42);
|
||||
}
|
||||
}
|
||||
@ -10,6 +10,74 @@
|
||||
"message": "Requested contract \"C\" does not exist in source \"Source\".",
|
||||
"severity": "warning",
|
||||
"type": "Warning"
|
||||
},
|
||||
{
|
||||
"component": "general",
|
||||
"errorCode": "6328",
|
||||
"formattedMessage": "Warning: CHC: Assertion violation happens here.
|
||||
Counterexample:
|
||||
|
||||
y = 0
|
||||
|
||||
Transaction trace:
|
||||
B.constructor()
|
||||
B.g(0)
|
||||
--> Source:5:7:
|
||||
|
|
||||
5 | \t\t\t\t\t\tassert(y > 0);
|
||||
| \t\t\t\t\t\t^^^^^^^^^^^^^
|
||||
|
||||
",
|
||||
"message": "CHC: Assertion violation happens here.
|
||||
Counterexample:
|
||||
|
||||
y = 0
|
||||
|
||||
Transaction trace:
|
||||
B.constructor()
|
||||
B.g(0)",
|
||||
"severity": "warning",
|
||||
"sourceLocation":
|
||||
{
|
||||
"end": 137,
|
||||
"file": "Source",
|
||||
"start": 124
|
||||
},
|
||||
"type": "Warning"
|
||||
},
|
||||
{
|
||||
"component": "general",
|
||||
"errorCode": "6328",
|
||||
"formattedMessage": "Warning: CHC: Assertion violation happens here.
|
||||
Counterexample:
|
||||
|
||||
x = 0
|
||||
|
||||
Transaction trace:
|
||||
A.constructor()
|
||||
A.f(0)
|
||||
--> Source:10:7:
|
||||
|
|
||||
10 | \t\t\t\t\t\tassert(x > 0);
|
||||
| \t\t\t\t\t\t^^^^^^^^^^^^^
|
||||
|
||||
",
|
||||
"message": "CHC: Assertion violation happens here.
|
||||
Counterexample:
|
||||
|
||||
x = 0
|
||||
|
||||
Transaction trace:
|
||||
A.constructor()
|
||||
A.f(0)",
|
||||
"severity": "warning",
|
||||
"sourceLocation":
|
||||
{
|
||||
"end": 231,
|
||||
"file": "Source",
|
||||
"start": 218
|
||||
},
|
||||
"type": "Warning"
|
||||
}
|
||||
],
|
||||
"sources":
|
||||
|
||||
@ -10,7 +10,7 @@ Counterexample:
|
||||
y = 0
|
||||
|
||||
Transaction trace:
|
||||
A.constructor()
|
||||
B.constructor()
|
||||
B.g(0)
|
||||
--> Source:5:7:
|
||||
|
|
||||
@ -24,7 +24,7 @@ Counterexample:
|
||||
y = 0
|
||||
|
||||
Transaction trace:
|
||||
A.constructor()
|
||||
B.constructor()
|
||||
B.g(0)",
|
||||
"severity": "warning",
|
||||
"sourceLocation":
|
||||
|
||||
@ -10,7 +10,7 @@ Counterexample:
|
||||
y = 0
|
||||
|
||||
Transaction trace:
|
||||
A.constructor()
|
||||
B.constructor()
|
||||
B.g(0)
|
||||
--> Source:5:7:
|
||||
|
|
||||
@ -24,7 +24,7 @@ Counterexample:
|
||||
y = 0
|
||||
|
||||
Transaction trace:
|
||||
A.constructor()
|
||||
B.constructor()
|
||||
B.g(0)",
|
||||
"severity": "warning",
|
||||
"sourceLocation":
|
||||
|
||||
@ -0,0 +1,30 @@
|
||||
{
|
||||
"language": "Solidity",
|
||||
"sources":
|
||||
{
|
||||
"A":
|
||||
{
|
||||
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;
|
||||
contract Ext {
|
||||
function f() public view returns (uint) {
|
||||
return 42;
|
||||
}
|
||||
}
|
||||
|
||||
contract test {
|
||||
function g(Ext e) public view {
|
||||
uint x = e.f();
|
||||
assert(x == 42);
|
||||
}
|
||||
}"
|
||||
}
|
||||
},
|
||||
"settings":
|
||||
{
|
||||
"modelChecker":
|
||||
{
|
||||
"engine": "chc",
|
||||
"extCalls": ""
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,12 @@
|
||||
{
|
||||
"errors":
|
||||
[
|
||||
{
|
||||
"component": "general",
|
||||
"formattedMessage": "Invalid model checker extCalls requested.",
|
||||
"message": "Invalid model checker extCalls requested.",
|
||||
"severity": "error",
|
||||
"type": "JSONError"
|
||||
}
|
||||
]
|
||||
}
|
||||
@ -0,0 +1,30 @@
|
||||
{
|
||||
"language": "Solidity",
|
||||
"sources":
|
||||
{
|
||||
"A":
|
||||
{
|
||||
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;
|
||||
contract Ext {
|
||||
function f() public view returns (uint) {
|
||||
return 42;
|
||||
}
|
||||
}
|
||||
|
||||
contract test {
|
||||
function g(Ext e) public view {
|
||||
uint x = e.f();
|
||||
assert(x == 42);
|
||||
}
|
||||
}"
|
||||
}
|
||||
},
|
||||
"settings":
|
||||
{
|
||||
"modelChecker":
|
||||
{
|
||||
"engine": "chc",
|
||||
"extCalls": "trusted"
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,32 @@
|
||||
{
|
||||
"errors":
|
||||
[
|
||||
{
|
||||
"component": "general",
|
||||
"errorCode": "2018",
|
||||
"formattedMessage": "Warning: Function state mutability can be restricted to pure
|
||||
--> A:4:7:
|
||||
|
|
||||
4 | \t\t\t\t\t\tfunction f() public view returns (uint) {
|
||||
| \t\t\t\t\t\t^ (Relevant source part starts here and spans across multiple lines).
|
||||
|
||||
",
|
||||
"message": "Function state mutability can be restricted to pure",
|
||||
"severity": "warning",
|
||||
"sourceLocation":
|
||||
{
|
||||
"end": 152,
|
||||
"file": "A",
|
||||
"start": 85
|
||||
},
|
||||
"type": "Warning"
|
||||
}
|
||||
],
|
||||
"sources":
|
||||
{
|
||||
"A":
|
||||
{
|
||||
"id": 0
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,28 @@
|
||||
{
|
||||
"language": "Solidity",
|
||||
"sources":
|
||||
{
|
||||
"A":
|
||||
{
|
||||
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;
|
||||
abstract contract Ext {
|
||||
function f() virtual public view returns (uint);
|
||||
}
|
||||
|
||||
contract test {
|
||||
function g(Ext e) public view {
|
||||
uint x = e.f();
|
||||
assert(x == 0);
|
||||
}
|
||||
}"
|
||||
}
|
||||
},
|
||||
"settings":
|
||||
{
|
||||
"modelChecker":
|
||||
{
|
||||
"engine": "chc",
|
||||
"extCalls": "untrusted"
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,50 @@
|
||||
{
|
||||
"errors":
|
||||
[
|
||||
{
|
||||
"component": "general",
|
||||
"errorCode": "6328",
|
||||
"formattedMessage": "Warning: CHC: Assertion violation happens here.
|
||||
Counterexample:
|
||||
|
||||
e = 0
|
||||
x = 1
|
||||
|
||||
Transaction trace:
|
||||
test.constructor()
|
||||
test.g(0)
|
||||
e.f() -- untrusted external call
|
||||
--> A:10:8:
|
||||
|
|
||||
10 | \t\t\t\t\t\t\tassert(x == 0);
|
||||
| \t\t\t\t\t\t\t^^^^^^^^^^^^^^
|
||||
|
||||
",
|
||||
"message": "CHC: Assertion violation happens here.
|
||||
Counterexample:
|
||||
|
||||
e = 0
|
||||
x = 1
|
||||
|
||||
Transaction trace:
|
||||
test.constructor()
|
||||
test.g(0)
|
||||
e.f() -- untrusted external call",
|
||||
"severity": "warning",
|
||||
"sourceLocation":
|
||||
{
|
||||
"end": 254,
|
||||
"file": "A",
|
||||
"start": 240
|
||||
},
|
||||
"type": "Warning"
|
||||
}
|
||||
],
|
||||
"sources":
|
||||
{
|
||||
"A":
|
||||
{
|
||||
"id": 0
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,30 @@
|
||||
{
|
||||
"language": "Solidity",
|
||||
"sources":
|
||||
{
|
||||
"A":
|
||||
{
|
||||
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;
|
||||
contract Ext {
|
||||
function f() public view returns (uint) {
|
||||
return 42;
|
||||
}
|
||||
}
|
||||
|
||||
contract test {
|
||||
function g(Ext e) public view {
|
||||
uint x = e.f();
|
||||
assert(x == 42);
|
||||
}
|
||||
}"
|
||||
}
|
||||
},
|
||||
"settings":
|
||||
{
|
||||
"modelChecker":
|
||||
{
|
||||
"engine": "chc",
|
||||
"extCalls": "what"
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,12 @@
|
||||
{
|
||||
"errors":
|
||||
[
|
||||
{
|
||||
"component": "general",
|
||||
"formattedMessage": "Invalid model checker extCalls requested.",
|
||||
"message": "Invalid model checker extCalls requested.",
|
||||
"severity": "error",
|
||||
"type": "JSONError"
|
||||
}
|
||||
]
|
||||
}
|
||||
@ -0,0 +1,30 @@
|
||||
{
|
||||
"language": "Solidity",
|
||||
"sources":
|
||||
{
|
||||
"A":
|
||||
{
|
||||
"content": "// SPDX-License-Identifier: GPL-3.0\npragma solidity >=0.0;
|
||||
contract Ext {
|
||||
function f() public view returns (uint) {
|
||||
return 42;
|
||||
}
|
||||
}
|
||||
|
||||
contract test {
|
||||
function g(Ext e) public view {
|
||||
uint x = e.f();
|
||||
assert(x == 42);
|
||||
}
|
||||
}"
|
||||
}
|
||||
},
|
||||
"settings":
|
||||
{
|
||||
"modelChecker":
|
||||
{
|
||||
"engine": "chc",
|
||||
"extCalls": 2
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -0,0 +1,12 @@
|
||||
{
|
||||
"errors":
|
||||
[
|
||||
{
|
||||
"component": "general",
|
||||
"formattedMessage": "settings.modelChecker.extCalls must be a string.",
|
||||
"message": "settings.modelChecker.extCalls must be a string.",
|
||||
"severity": "error",
|
||||
"type": "JSONError"
|
||||
}
|
||||
]
|
||||
}
|
||||
@ -3,14 +3,41 @@
|
||||
{
|
||||
"smtlib2queries":
|
||||
{
|
||||
"0x0ebc730de380833af1e52ed063befb32994bc637929c942b7fd089b7cd3ba64e": "(set-logic HORN)
|
||||
|
||||
"0x75b95497d56c30e254a59358d72ddd4e78f9e90db621cfe677e85d05b2252411": "(set-option :produce-models true)
|
||||
(set-logic ALL)
|
||||
(declare-fun |x_3_3| () Int)
|
||||
(declare-fun |error_0| () Int)
|
||||
(declare-fun |this_0| () Int)
|
||||
(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
|
||||
(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.prevrandao| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
|
||||
(declare-fun |tx_0| () |tx_type|)
|
||||
(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
|
||||
(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
|
||||
(declare-fun |crypto_0| () |crypto_type|)
|
||||
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
|
||||
(declare-fun |abi_0| () |abi_type|)
|
||||
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
|
||||
(declare-fun |state_0| () |state_type|)
|
||||
(declare-fun |x_3_4| () Int)
|
||||
(declare-fun |x_3_0| () Int)
|
||||
(declare-fun |expr_7_0| () Int)
|
||||
(declare-fun |expr_8_0| () Int)
|
||||
(declare-fun |expr_9_1| () Bool)
|
||||
|
||||
(assert (and (and (and true true) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> (and true true) true) (and (= expr_8_0 0) (and (=> (and true true) (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_0) (and (and (>= x_3_0 0) (<= x_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (> (|block.prevrandao| tx_0) 18446744073709551616) (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.prevrandao| tx_0) 0) (<= (|block.prevrandao| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))) (not expr_9_1)))
|
||||
(declare-const |EVALEXPR_0| Int)
|
||||
(assert (= |EVALEXPR_0| x_3_0))
|
||||
(check-sat)
|
||||
(get-value (|EVALEXPR_0| ))
|
||||
",
|
||||
"0xfb06d3f02a20bd362abded9ab80638bdc9dd43ccbf644517f3006206c0c47f67": "(set-logic HORN)
|
||||
|
||||
(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
|
||||
(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.prevrandao| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
|
||||
(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
|
||||
(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
|
||||
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
|
||||
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
|
||||
(declare-fun |interface_0_C_14_0| (Int |abi_type| |crypto_type| |state_type| ) Bool)
|
||||
(declare-fun |nondet_interface_1_C_14_0| (Int Int |abi_type| |crypto_type| |state_type| |state_type| ) Bool)
|
||||
(declare-fun |summary_constructor_2_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool)
|
||||
@ -97,7 +124,7 @@
|
||||
(declare-fun |implicit_constructor_entry_13_C_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool)
|
||||
(assert
|
||||
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
|
||||
(=> (and (and (and (and (= state_1 state_0) (= error_0 0)) true) true) (>= (select (|balances| state_1) this_0) (|msg.value| tx_0))) (implicit_constructor_entry_13_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1))))
|
||||
(=> (and (and (and (and (and (= state_1 state_0) (= error_0 0)) true) true) true) (>= (select (|balances| state_1) this_0) (|msg.value| tx_0))) (implicit_constructor_entry_13_C_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1))))
|
||||
|
||||
|
||||
(assert
|
||||
@ -124,34 +151,7 @@
|
||||
(assert
|
||||
(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
|
||||
(=> error_target_3_0 false)))
|
||||
(check-sat)",
|
||||
"0xcb822e6220a39244d26887a0fa6f62b06718359056555679fb06dd7dff18bb86": "(set-option :produce-models true)
|
||||
(set-logic ALL)
|
||||
(declare-fun |x_3_3| () Int)
|
||||
(declare-fun |error_0| () Int)
|
||||
(declare-fun |this_0| () Int)
|
||||
(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
|
||||
(declare-fun |state_0| () |state_type|)
|
||||
(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
|
||||
(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.prevrandao| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
|
||||
(declare-fun |tx_0| () |tx_type|)
|
||||
(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
|
||||
(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
|
||||
(declare-fun |crypto_0| () |crypto_type|)
|
||||
(declare-datatypes ((|abi_type| 0)) (((|abi_type|))))
|
||||
(declare-fun |abi_0| () |abi_type|)
|
||||
(declare-fun |x_3_4| () Int)
|
||||
(declare-fun |x_3_0| () Int)
|
||||
(declare-fun |expr_7_0| () Int)
|
||||
(declare-fun |expr_8_0| () Int)
|
||||
(declare-fun |expr_9_1| () Bool)
|
||||
|
||||
(assert (and (and (and true true) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> (and true true) true) (and (= expr_8_0 0) (and (=> (and true true) (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_0) (and (and (>= x_3_0 0) (<= x_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (> (|block.prevrandao| tx_0) 18446744073709551616) (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.prevrandao| tx_0) 0) (<= (|block.prevrandao| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3017696395)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 179)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 222)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 100)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 139)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))) (not expr_9_1)))
|
||||
(declare-const |EVALEXPR_0| Int)
|
||||
(assert (= |EVALEXPR_0| x_3_0))
|
||||
(check-sat)
|
||||
(get-value (|EVALEXPR_0| ))
|
||||
"
|
||||
(check-sat)"
|
||||
}
|
||||
},
|
||||
"errors":
|
||||
|
||||
@ -33,6 +33,12 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E
|
||||
if (!contract.empty())
|
||||
m_modelCheckerSettings.contracts.contracts[""] = {contract};
|
||||
|
||||
auto extCallsMode = ModelCheckerExtCalls::fromString(m_reader.stringSetting("SMTExtCalls", "untrusted"));
|
||||
if (extCallsMode)
|
||||
m_modelCheckerSettings.externalCalls = *extCallsMode;
|
||||
else
|
||||
BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT external calls mode."));
|
||||
|
||||
auto const& showUnproved = m_reader.stringSetting("SMTShowUnproved", "yes");
|
||||
if (showUnproved == "no")
|
||||
m_modelCheckerSettings.showUnproved = false;
|
||||
@ -51,8 +57,13 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E
|
||||
m_modelCheckerSettings.solvers &= ModelChecker::availableSolvers();
|
||||
|
||||
/// Underflow and Overflow are not enabled by default for Solidity >=0.8.7,
|
||||
/// so we explicitly enable all targets for the tests.
|
||||
m_modelCheckerSettings.targets = ModelCheckerTargets::All();
|
||||
/// so we explicitly enable all targets for the tests,
|
||||
/// if the targets were not explicitly set by the test.
|
||||
auto targets = ModelCheckerTargets::fromString(m_reader.stringSetting("SMTTargets", "all"));
|
||||
if (targets)
|
||||
m_modelCheckerSettings.targets = *targets;
|
||||
else
|
||||
BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT targets."));
|
||||
|
||||
auto engine = ModelCheckerEngine::fromString(m_reader.stringSetting("SMTEngine", "all"));
|
||||
if (engine)
|
||||
|
||||
@ -22,4 +22,4 @@ contract C {
|
||||
// SMTEngine: all
|
||||
// SMTIgnoreOS: macos
|
||||
// ----
|
||||
// Info 1180: Contract invariant(s) for :C:\n!(s1.arr.length <= 0)\n!(s2.arr.length <= 0)\n(((s2.arr[0].length + ((- 1) * s1.arr[0].length)) <= 0) && ((s1.arr[0].length + ((- 1) * s2.arr[0].length)) <= 0))\n
|
||||
// Info 1180: Contract invariant(s) for :C:\n!(s1.arr.length <= 0)\n!(s2.arr.length <= 0)\n(((s1.arr[0].length + ((- 1) * s2.arr[0].length)) <= 0) && ((s2.arr[0].length + ((- 1) * s1.arr[0].length)) <= 0))\n
|
||||
|
||||
@ -31,4 +31,4 @@ contract C {
|
||||
// Warning 6328: (349-375): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
|
||||
// Warning 6328: (379-402): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
|
||||
// Warning 6328: (406-432): CHC: Assertion violation happens here.\nCounterexample:\narr = [[], [], [], [], [], [], [], [], []]\nx = 0\ny = 0\nz = 9\nt = 0\n\nTransaction trace:\nC.constructor()\nState: arr = [[], [], [], [], [], [], [], [], []]\nC.f()
|
||||
// Info 1180: Contract invariant(s) for :C:\n!(arr.length <= 7)\n!(arr.length <= 8)\n
|
||||
// Info 1180: Contract invariant(s) for :C:\n!(arr.length <= 5)\n!(arr.length <= 7)\n!(arr.length <= 8)\n
|
||||
|
||||
@ -18,5 +18,6 @@ contract C {
|
||||
// ====
|
||||
// SMTEngine: all
|
||||
// SMTIgnoreOS: macos
|
||||
// SMTIgnoreCex: yes
|
||||
// ----
|
||||
// Warning 6328: (199-229): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.g()
|
||||
|
||||
@ -20,5 +20,6 @@ contract C {
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: all
|
||||
// SMTIgnoreCex: yes
|
||||
// ----
|
||||
// Warning 6328: (362-420): CHC: Assertion violation happens here.
|
||||
|
||||
@ -83,6 +83,6 @@ contract InternalCall {
|
||||
// Warning 2018: (1111-1173): Function state mutability can be restricted to pure
|
||||
// Warning 2018: (1179-1241): Function state mutability can be restricted to pure
|
||||
// Warning 2018: (1247-1309): Function state mutability can be restricted to pure
|
||||
// Warning 4588: (681-716): Assertion checker does not yet implement this type of function call.
|
||||
// Warning 4588: (854-886): Assertion checker does not yet implement this type of function call.
|
||||
// Warning 8729: (681-716): Contract deployment is only supported in the trusted mode for external calls with the CHC engine.
|
||||
// Warning 8729: (854-886): Contract deployment is only supported in the trusted mode for external calls with the CHC engine.
|
||||
// Warning 5729: (1370-1375): BMC does not yet implement this type of function call.
|
||||
|
||||
@ -0,0 +1,18 @@
|
||||
contract D {
|
||||
uint x;
|
||||
function f() public view returns (uint) { return x; }
|
||||
}
|
||||
|
||||
contract C {
|
||||
function g() public {
|
||||
D d = new D();
|
||||
uint y = d.f();
|
||||
assert(y == 0); // should fail in BMC
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: bmc
|
||||
// SMTExtCalls: trusted
|
||||
// ----
|
||||
// Warning 8729: (124-131): Contract deployment is only supported in the trusted mode for external calls with the CHC engine.
|
||||
// Warning 4661: (153-167): BMC: Assertion violation happens here.
|
||||
@ -0,0 +1,17 @@
|
||||
contract D {
|
||||
uint x;
|
||||
function f() public view returns (uint) { return x; }
|
||||
}
|
||||
|
||||
contract C {
|
||||
function g() public {
|
||||
D d = new D();
|
||||
uint y = d.f();
|
||||
assert(y == 0); // should fail in ext calls untrusted mode
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: bmc
|
||||
// ----
|
||||
// Warning 8729: (124-131): Contract deployment is only supported in the trusted mode for external calls with the CHC engine.
|
||||
// Warning 4661: (153-167): BMC: Assertion violation happens here.
|
||||
@ -0,0 +1,16 @@
|
||||
contract D {
|
||||
uint x;
|
||||
function f() public view returns (uint) { return x; }
|
||||
}
|
||||
|
||||
contract C {
|
||||
function g() public {
|
||||
D d = new D();
|
||||
uint y = d.f();
|
||||
assert(y == 0); // should hold in ext calls trusted mode
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: all
|
||||
// SMTExtCalls: trusted
|
||||
// ----
|
||||
@ -0,0 +1,19 @@
|
||||
contract D {
|
||||
uint x;
|
||||
}
|
||||
|
||||
contract C {
|
||||
function f() public {
|
||||
D d1 = new D();
|
||||
D d2 = new D();
|
||||
|
||||
assert(d1 != d2); // should hold in ext calls trusted mode
|
||||
assert(address(this) != address(d1)); // should hold in ext calls trusted mode
|
||||
assert(address(this) != address(d2)); // should hold in ext calls trusted mode
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: all
|
||||
// SMTExtCalls: trusted
|
||||
// ----
|
||||
// Info 1180: Contract invariant(s) for :C:\n(:var 0).isActive[address(this)]\n
|
||||
@ -0,0 +1,32 @@
|
||||
contract D {
|
||||
uint x;
|
||||
function inc() public { ++x; }
|
||||
function f() public view returns (uint) { return x; }
|
||||
}
|
||||
|
||||
contract C {
|
||||
function f() public {
|
||||
D d = new D();
|
||||
assert(d.f() == 0); // should hold
|
||||
d.inc();
|
||||
assert(d.f() == 1); // should hold
|
||||
d = new D();
|
||||
assert(d.f() == 0); // should hold
|
||||
assert(d.f() == 1); // should fail
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: all
|
||||
// SMTExtCalls: trusted
|
||||
// SMTIgnoreOS: macos
|
||||
// ----
|
||||
// Warning 4984: (47-50): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
|
||||
// Warning 6328: (167-185): CHC: Assertion violation might happen here.
|
||||
// Warning 6328: (215-233): CHC: Assertion violation might happen here.
|
||||
// Warning 6328: (267-285): CHC: Assertion violation might happen here.
|
||||
// Warning 6328: (304-322): CHC: Assertion violation might happen here.
|
||||
// Warning 2661: (47-50): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
|
||||
// Warning 4661: (167-185): BMC: Assertion violation happens here.
|
||||
// Warning 4661: (215-233): BMC: Assertion violation happens here.
|
||||
// Warning 4661: (267-285): BMC: Assertion violation happens here.
|
||||
// Warning 4661: (304-322): BMC: Assertion violation happens here.
|
||||
@ -0,0 +1,17 @@
|
||||
contract D {
|
||||
uint x;
|
||||
}
|
||||
|
||||
contract C {
|
||||
uint y;
|
||||
function g() public {
|
||||
D d = new D();
|
||||
assert(y == 0); // should hold
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: all
|
||||
// SMTExtCalls: trusted
|
||||
// ----
|
||||
// Warning 2072: (72-75): Unused local variable.
|
||||
// Info 1180: Contract invariant(s) for :C:\n(y <= 0)\n
|
||||
@ -0,0 +1,24 @@
|
||||
contract D {
|
||||
uint x;
|
||||
function inc() public { ++x; }
|
||||
function f() public view returns (uint) { return x; }
|
||||
}
|
||||
|
||||
contract C {
|
||||
D d;
|
||||
constructor() {
|
||||
d = new D();
|
||||
assert(d.f() == 0); // should hold
|
||||
}
|
||||
function g() public view {
|
||||
assert(d.f() == 0); // should fail
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: all
|
||||
// SMTExtCalls: trusted
|
||||
// SMTIgnoreOS: macos
|
||||
// ----
|
||||
// Warning 4984: (47-50): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
|
||||
// Warning 6328: (233-251): CHC: Assertion violation happens here.
|
||||
// Warning 2661: (47-50): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
|
||||
@ -0,0 +1,20 @@
|
||||
contract D {
|
||||
uint x;
|
||||
function f() public view returns (uint) { return x; }
|
||||
}
|
||||
|
||||
contract C {
|
||||
D d;
|
||||
constructor() {
|
||||
d = new D();
|
||||
assert(d.f() == 0); // should hold
|
||||
}
|
||||
function g() public view {
|
||||
assert(d.f() == 0); // should hold
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: all
|
||||
// SMTExtCalls: trusted
|
||||
// ----
|
||||
// Info 1180: Contract invariant(s) for :C:\n((:var 1).storage.storage_D_12[d].x_3_D_12 <= 0)\nReentrancy property(ies) for :D:\n((x' <= 0) || !(x <= 0))\n
|
||||
@ -0,0 +1,21 @@
|
||||
contract D {
|
||||
uint x;
|
||||
function s(uint _x) public { x = _x; }
|
||||
function f() public view returns (uint) { return x; }
|
||||
}
|
||||
|
||||
contract C {
|
||||
D d;
|
||||
constructor() {
|
||||
d = new D();
|
||||
}
|
||||
function g() public view {
|
||||
assert(d.f() == 0); // should fail
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTContract: C
|
||||
// SMTEngine: all
|
||||
// SMTExtCalls: trusted
|
||||
// ----
|
||||
// Warning 6328: (204-222): CHC: Assertion violation happens here.
|
||||
@ -0,0 +1,20 @@
|
||||
contract D {
|
||||
bool b;
|
||||
function s() public { b = true; }
|
||||
function f() public view returns (bool) { return b; }
|
||||
}
|
||||
|
||||
contract C {
|
||||
D d;
|
||||
constructor() {
|
||||
d = new D();
|
||||
}
|
||||
function g() public view {
|
||||
assert(d.f()); // should fail
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: all
|
||||
// SMTExtCalls: trusted
|
||||
// ----
|
||||
// Warning 6328: (199-212): CHC: Assertion violation happens here.\nCounterexample:\nd = (- 1)\n\nTransaction trace:\nC.constructor()\nState: d = (- 1)\nC.g()\n D.f() -- trusted external call
|
||||
@ -0,0 +1,17 @@
|
||||
contract D {
|
||||
uint x;
|
||||
function f() public view returns (uint) { return x; }
|
||||
}
|
||||
|
||||
contract C {
|
||||
function g() public {
|
||||
D d = new D();
|
||||
uint y = d.f();
|
||||
assert(y == 0); // should fail in ext calls untrusted mode
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: all
|
||||
// ----
|
||||
// Warning 8729: (124-131): Contract deployment is only supported in the trusted mode for external calls with the CHC engine.
|
||||
// Warning 6328: (153-167): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0\ny = 1\n\nTransaction trace:\nC.constructor()\nC.g()\n d.f() -- untrusted external call
|
||||
@ -0,0 +1,22 @@
|
||||
contract D {
|
||||
uint x;
|
||||
}
|
||||
|
||||
contract C {
|
||||
function f() public {
|
||||
D d1 = new D();
|
||||
D d2 = new D();
|
||||
|
||||
assert(d1 != d2); // should fail in ext calls untrusted mode
|
||||
assert(address(this) != address(d1)); // should fail in ext calls untrusted mode
|
||||
assert(address(this) != address(d2)); // should fail in ext calls untrusted mode
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: all
|
||||
// ----
|
||||
// Warning 8729: (70-77): Contract deployment is only supported in the trusted mode for external calls with the CHC engine.
|
||||
// Warning 8729: (88-95): Contract deployment is only supported in the trusted mode for external calls with the CHC engine.
|
||||
// Warning 6328: (100-116): CHC: Assertion violation happens here.\nCounterexample:\n\nd1 = 0\nd2 = 0\n\nTransaction trace:\nC.constructor()\nC.f()
|
||||
// Warning 6328: (163-199): CHC: Assertion violation happens here.\nCounterexample:\n\nd1 = 21238\nd2 = 21238\n\nTransaction trace:\nC.constructor()\nC.f()
|
||||
// Warning 6328: (246-282): CHC: Assertion violation happens here.\nCounterexample:\n\nd1 = 21238\nd2 = 21238\n\nTransaction trace:\nC.constructor()\nC.f()
|
||||
@ -0,0 +1,17 @@
|
||||
contract D {
|
||||
uint x;
|
||||
}
|
||||
|
||||
contract C {
|
||||
uint y;
|
||||
function g() public {
|
||||
D d = new D();
|
||||
assert(y == 0); // should fail in ext calls untrusted mode
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: all
|
||||
// ----
|
||||
// Warning 2072: (72-75): Unused local variable.
|
||||
// Warning 8729: (78-85): Contract deployment is only supported in the trusted mode for external calls with the CHC engine.
|
||||
// Warning 6328: (89-103): CHC: Assertion violation happens here.\nCounterexample:\ny = 1\nd = 0\n\nTransaction trace:\nC.constructor()\nState: y = 0\nC.g()
|
||||
@ -0,0 +1,20 @@
|
||||
contract A {
|
||||
constructor() payable {}
|
||||
}
|
||||
|
||||
contract B {
|
||||
function f() public payable {
|
||||
require(address(this).balance == 100);
|
||||
A a = new A{value: 50}();
|
||||
assert(address(this).balance == 50); // should hold
|
||||
assert(address(this).balance == 60); // should fail
|
||||
assert(address(a).balance >= 50); // should hold
|
||||
assert(address(a).balance == 50); // should fail
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// ----
|
||||
// Warning 6328: (211-246): CHC: Assertion violation happens here.
|
||||
// Warning 6328: (316-348): CHC: Assertion violation happens here.
|
||||
@ -0,0 +1,28 @@
|
||||
contract D {
|
||||
constructor(uint _x) { x = _x; }
|
||||
uint public x;
|
||||
}
|
||||
|
||||
contract E {
|
||||
constructor() { x = 2; }
|
||||
uint public x;
|
||||
}
|
||||
|
||||
contract C {
|
||||
constructor() {
|
||||
address d = address(new D(42));
|
||||
assert(D(d).x() == 42); // should hold
|
||||
assert(D(d).x() == 43); // should fail
|
||||
uint y = E(d).x();
|
||||
assert(y == 2); // should fail, it would still call D.x() == 42
|
||||
assert(y == 42); // should hold, but fails due to false positive
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// SMTIgnoreCex: yes
|
||||
// ----
|
||||
// Warning 6328: (231-253): CHC: Assertion violation happens here.
|
||||
// Warning 6328: (293-307): CHC: Assertion violation happens here.
|
||||
// Warning 6328: (359-374): CHC: Assertion violation happens here.
|
||||
@ -0,0 +1,25 @@
|
||||
contract D {
|
||||
constructor(uint _x) { x = _x; }
|
||||
function setD(uint _x) public { x = _x; }
|
||||
uint public x;
|
||||
}
|
||||
|
||||
contract C {
|
||||
constructor() {
|
||||
address d = address(new D(42));
|
||||
assert(D(d).x() == 42); // should hold
|
||||
assert(D(d).x() == 21); // should fail
|
||||
d.call(abi.encodeCall(D.setD, (21)));
|
||||
assert(D(d).x() == 21); // should hold, but false positive cus low level calls are not handled precisely
|
||||
assert(D(d).x() == 42); // should fail
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// SMTIgnoreCex: yes
|
||||
// ----
|
||||
// Warning 9302: (257-293): Return value of low-level calls not used.
|
||||
// Warning 6328: (216-238): CHC: Assertion violation happens here.
|
||||
// Warning 6328: (297-319): CHC: Assertion violation happens here.
|
||||
// Warning 6328: (404-426): CHC: Assertion violation happens here.
|
||||
@ -0,0 +1,28 @@
|
||||
contract D {
|
||||
constructor(uint _x) { x = _x; }
|
||||
uint public x;
|
||||
}
|
||||
|
||||
contract E {
|
||||
constructor() { x = 2; }
|
||||
uint public x;
|
||||
}
|
||||
|
||||
contract C {
|
||||
function f() public {
|
||||
address d = address(new D(42));
|
||||
assert(D(d).x() == 42); // should hold
|
||||
assert(D(d).x() == 43); // should fail
|
||||
uint y = E(d).x();
|
||||
assert(y == 2); // should fail, it would still call D.x() == 42
|
||||
assert(y == 42); // should hold, but fails due to false positive
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// SMTIgnoreCex: yes
|
||||
// ----
|
||||
// Warning 6328: (237-259): CHC: Assertion violation happens here.
|
||||
// Warning 6328: (299-313): CHC: Assertion violation happens here.
|
||||
// Warning 6328: (365-380): CHC: Assertion violation happens here.
|
||||
@ -0,0 +1,25 @@
|
||||
contract D {
|
||||
constructor(uint _x) { x = _x; }
|
||||
function setD(uint _x) public { x = _x; }
|
||||
uint public x;
|
||||
}
|
||||
|
||||
contract C {
|
||||
function f() public {
|
||||
address d = address(new D(42));
|
||||
assert(D(d).x() == 42); // should hold
|
||||
assert(D(d).x() == 21); // should fail
|
||||
d.call(abi.encodeCall(D.setD, (21)));
|
||||
assert(D(d).x() == 21); // should hold, but false positive cus low level calls are not handled precisely
|
||||
assert(D(d).x() == 42); // should fail
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// SMTIgnoreCex: yes
|
||||
// ----
|
||||
// Warning 9302: (263-299): Return value of low-level calls not used.
|
||||
// Warning 6328: (222-244): CHC: Assertion violation happens here.
|
||||
// Warning 6328: (303-325): CHC: Assertion violation happens here.
|
||||
// Warning 6328: (410-432): CHC: Assertion violation happens here.
|
||||
@ -0,0 +1,29 @@
|
||||
contract D {
|
||||
constructor(uint _x) { x = _x; }
|
||||
function setD(uint _x) public { x = _x; }
|
||||
uint public x;
|
||||
}
|
||||
|
||||
contract C {
|
||||
uint x;
|
||||
|
||||
function f() public {
|
||||
x = 666;
|
||||
address d = address(new D(42));
|
||||
assert(D(d).x() == 42); // should hold
|
||||
assert(D(d).x() == 21); // should fail
|
||||
d.call(abi.encodeCall(D.setD, (21)));
|
||||
assert(D(d).x() == 21); // should hold, but false positive cus low level calls are not handled precisely
|
||||
assert(D(d).x() == 42); // should fail
|
||||
assert(x == 666); // should hold, C's storage should not have been havoced
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// SMTIgnoreCex: yes
|
||||
// ----
|
||||
// Warning 9302: (284-320): Return value of low-level calls not used.
|
||||
// Warning 6328: (243-265): CHC: Assertion violation happens here.
|
||||
// Warning 6328: (324-346): CHC: Assertion violation happens here.
|
||||
// Warning 6328: (431-453): CHC: Assertion violation happens here.
|
||||
@ -15,4 +15,4 @@ contract C {
|
||||
// Warning 2519: (106-112): This declaration shadows an existing declaration.
|
||||
// Warning 2072: (106-112): Unused local variable.
|
||||
// Warning 2072: (114-131): Unused local variable.
|
||||
// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\nReentrancy property(ies) for :C:\n((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 0)\n
|
||||
// Info 1180: Contract invariant(s) for :C:\n(x <= 0)\nReentrancy property(ies) for :C:\n((!(x <= 0) || (x' <= 0)) && ((<errorCode> <= 0) || !(x <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 0)\n
|
||||
|
||||
@ -0,0 +1,21 @@
|
||||
contract State {
|
||||
function f(uint _x) public pure returns (uint) {
|
||||
assert(_x < 100); // should fail
|
||||
return _x;
|
||||
}
|
||||
}
|
||||
contract C {
|
||||
State s;
|
||||
uint z = s.f(2);
|
||||
|
||||
function f() public view {
|
||||
assert(z == 2); // should hold in trusted mode
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTContract: C
|
||||
// SMTEngine: all
|
||||
// SMTExtCalls: trusted
|
||||
// SMTIgnoreInv: yes
|
||||
// ----
|
||||
// Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100)
|
||||
@ -0,0 +1,17 @@
|
||||
contract C {
|
||||
uint z = this.g(2);
|
||||
|
||||
function g(uint _x) public pure returns (uint) {
|
||||
assert(_x > 0); // should fail
|
||||
return _x;
|
||||
}
|
||||
|
||||
function f() public view {
|
||||
assert(z == 2); // should hold
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: all
|
||||
// ----
|
||||
// Warning 6328: (87-101): CHC: Assertion violation happens here.\nCounterexample:\nz = 2\n_x = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: z = 2\nC.g(0)
|
||||
// Info 1180: Contract invariant(s) for :C:\n(!(z >= 3) && !(z <= 1))\n
|
||||
@ -0,0 +1,25 @@
|
||||
contract State {
|
||||
function f(uint _x) public pure returns (uint) {
|
||||
assert(_x < 100); // should fail
|
||||
return _x;
|
||||
}
|
||||
}
|
||||
contract C {
|
||||
State s;
|
||||
uint z;
|
||||
|
||||
constructor() {
|
||||
z = s.f(2);
|
||||
}
|
||||
|
||||
function f() public view {
|
||||
assert(z == 2); // should hold in trusted mode
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTContract: C
|
||||
// SMTEngine: all
|
||||
// SMTExtCalls: trusted
|
||||
// ----
|
||||
// Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100)
|
||||
// Info 1180: Contract invariant(s) for :C:\n(!(z >= 3) && !(z <= 1))\n
|
||||
@ -0,0 +1,41 @@
|
||||
contract A {
|
||||
uint x;
|
||||
function setX(uint _x) public {
|
||||
x = _x;
|
||||
}
|
||||
function getX() public view returns (uint) {
|
||||
return x;
|
||||
}
|
||||
}
|
||||
|
||||
contract B {
|
||||
A a;
|
||||
constructor() {
|
||||
a = new A();
|
||||
assert(a.getX() == 0); // should hold
|
||||
}
|
||||
function g() public view {
|
||||
assert(a.getX() == 0); // should fail because A.setX() can be called without B
|
||||
}
|
||||
function getX() public view returns (uint) {
|
||||
return a.getX();
|
||||
}
|
||||
}
|
||||
|
||||
contract C {
|
||||
B b;
|
||||
constructor() {
|
||||
b = new B();
|
||||
assert(b.getX() == 0); // should hold
|
||||
}
|
||||
function f() public view {
|
||||
assert(b.getX() == 0); // should fail because A.setX() can be called without A
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// SMTIgnoreOS: macos
|
||||
// ----
|
||||
// Warning 6328: (256-277): CHC: Assertion violation happens here.
|
||||
// Warning 6328: (533-554): CHC: Assertion violation might happen here.
|
||||
@ -0,0 +1,52 @@
|
||||
contract A {
|
||||
uint x;
|
||||
address immutable owner;
|
||||
constructor() {
|
||||
owner = msg.sender;
|
||||
}
|
||||
function setX(uint _x) public {
|
||||
require(msg.sender == owner);
|
||||
x = _x;
|
||||
}
|
||||
function getX() public view returns (uint) {
|
||||
return x;
|
||||
}
|
||||
}
|
||||
|
||||
contract B {
|
||||
A a;
|
||||
constructor() {
|
||||
a = new A();
|
||||
assert(a.getX() == 0); // should hold
|
||||
}
|
||||
function g() public view {
|
||||
assert(a.getX() == 0); // should hold, but fails because
|
||||
// the nondet_interface constraint added for `A a` in between
|
||||
// txs of `B` does not have the constraint that `msg.sender != address(this)`
|
||||
// so `A.setX` is allowed with `msg.sender = address(this)` inside
|
||||
// the current rules defining nondet_interface.
|
||||
// If we want to support that, we likely need a new type of nondet_interface
|
||||
// `nondet_interface_with_tx` that contains tx data as well as restricts
|
||||
// every further `nondet_interface_with_tx` to not have that `msg.sender`.
|
||||
}
|
||||
function getX() public view returns (uint) {
|
||||
return a.getX();
|
||||
}
|
||||
}
|
||||
|
||||
contract C {
|
||||
B b;
|
||||
constructor() {
|
||||
b = new B();
|
||||
assert(b.getX() == 0); // should hold
|
||||
}
|
||||
function f() public view {
|
||||
assert(b.getX() == 0); // should hold
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// ----
|
||||
// Warning 6328: (434-455): CHC: Assertion violation happens here.
|
||||
// Warning 6328: (1270-1291): CHC: Assertion violation might happen here.
|
||||
@ -0,0 +1,45 @@
|
||||
contract A {
|
||||
uint x;
|
||||
address immutable owner;
|
||||
constructor() {
|
||||
owner = msg.sender;
|
||||
}
|
||||
function setX(uint _x) public {
|
||||
require(msg.sender == owner);
|
||||
x = _x;
|
||||
}
|
||||
function getX() public view returns (uint) {
|
||||
return x;
|
||||
}
|
||||
}
|
||||
|
||||
contract B {
|
||||
A a;
|
||||
constructor() {
|
||||
a = new A();
|
||||
assert(a.getX() == 0); // should hold
|
||||
}
|
||||
function g() public {
|
||||
a.setX(42);
|
||||
}
|
||||
function getX() public view returns (uint) {
|
||||
return a.getX();
|
||||
}
|
||||
}
|
||||
|
||||
contract C {
|
||||
B b;
|
||||
constructor() {
|
||||
b = new B();
|
||||
assert(b.getX() == 0); // should hold
|
||||
}
|
||||
function f() public view {
|
||||
assert(b.getX() == 0); // should fail
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// SMTIgnoreOS: macos
|
||||
// ----
|
||||
// Warning 6328: (561-582): CHC: Assertion violation might happen here.
|
||||
@ -0,0 +1,48 @@
|
||||
contract A {
|
||||
uint x;
|
||||
address immutable owner;
|
||||
constructor() {
|
||||
owner = msg.sender;
|
||||
}
|
||||
function setX(uint _x) public {
|
||||
require(msg.sender == owner);
|
||||
x = _x;
|
||||
}
|
||||
function getX() public view returns (uint) {
|
||||
return x;
|
||||
}
|
||||
}
|
||||
|
||||
contract B {
|
||||
A a;
|
||||
address immutable owner;
|
||||
constructor() {
|
||||
owner = msg.sender;
|
||||
a = new A();
|
||||
assert(a.getX() == 0); // should hold
|
||||
}
|
||||
function g() public {
|
||||
require(msg.sender == owner);
|
||||
a.setX(42);
|
||||
}
|
||||
function getX() public view returns (uint) {
|
||||
return a.getX();
|
||||
}
|
||||
}
|
||||
|
||||
contract C {
|
||||
B b;
|
||||
constructor() {
|
||||
b = new B();
|
||||
assert(b.getX() == 0); // should hold
|
||||
}
|
||||
function f() public view {
|
||||
assert(b.getX() == 0); // should hold
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// SMTIgnoreOS: macos
|
||||
// ----
|
||||
// Warning 6328: (641-662): CHC: Assertion violation might happen here.
|
||||
@ -0,0 +1,50 @@
|
||||
contract A {
|
||||
uint x;
|
||||
address immutable owner;
|
||||
constructor() {
|
||||
owner = msg.sender;
|
||||
}
|
||||
function setX(uint _x) public {
|
||||
require(msg.sender == owner);
|
||||
x = _x;
|
||||
}
|
||||
function getX() public view returns (uint) {
|
||||
return x;
|
||||
}
|
||||
}
|
||||
|
||||
contract B {
|
||||
A a;
|
||||
address immutable owner;
|
||||
constructor() {
|
||||
owner = msg.sender;
|
||||
a = new A();
|
||||
}
|
||||
function g() public {
|
||||
require(msg.sender == owner);
|
||||
a.setX(42);
|
||||
}
|
||||
function getX() public view returns (uint) {
|
||||
return a.getX();
|
||||
}
|
||||
}
|
||||
|
||||
contract C {
|
||||
B b;
|
||||
constructor() {
|
||||
b = new B();
|
||||
assert(b.getX() == 0); // should hold
|
||||
}
|
||||
function f() public view {
|
||||
assert(b.getX() == 0); // should fail
|
||||
}
|
||||
function h() public {
|
||||
b.g();
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTContract: C
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// ----
|
||||
// Warning 6328: (601-622): CHC: Assertion violation might happen here.
|
||||
@ -0,0 +1,17 @@
|
||||
contract C {
|
||||
uint x;
|
||||
function i() public { ++x; }
|
||||
function f() public {
|
||||
x = 0;
|
||||
this.i();
|
||||
assert(x == 1); // should hold in trusted mode
|
||||
assert(x != 1); // should fail
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// SMTTargets: assert
|
||||
// SMTIgnoreCex: yes
|
||||
// ----
|
||||
// Warning 6328: (147-161): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()\n C.i() -- trusted external call
|
||||
@ -0,0 +1,16 @@
|
||||
contract C {
|
||||
uint x;
|
||||
function i() public { ++x; }
|
||||
function f() public {
|
||||
x = 0;
|
||||
((this)).i();
|
||||
assert(x == 1); // should hold in trusted mode
|
||||
assert(x != 1); // should fail
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// SMTTargets: assert
|
||||
// ----
|
||||
// Warning 6328: (151-165): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()\n C.i() -- trusted external call
|
||||
@ -0,0 +1,17 @@
|
||||
contract C {
|
||||
uint x;
|
||||
function i() public { ++x; }
|
||||
function f() public {
|
||||
x = 0;
|
||||
C c = this;
|
||||
c.i();
|
||||
assert(x == 1); // should hold in trusted mode
|
||||
assert(x != 1); // should fail
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// SMTTargets: assert
|
||||
// ----
|
||||
// Warning 6328: (158-172): CHC: Assertion violation happens here.
|
||||
@ -0,0 +1,23 @@
|
||||
contract D {
|
||||
uint public x;
|
||||
}
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
address d;
|
||||
}
|
||||
S[] ss;
|
||||
constructor() {
|
||||
ss.push(S(address(new D())));
|
||||
assert(D(ss[0].d).x() == 0); // should hold
|
||||
}
|
||||
function f() public view {
|
||||
assert(D(ss[0].d).x() == 0); // should hold, but fails because we havoc the state
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// SMTTargets: assert
|
||||
// ----
|
||||
// Warning 6328: (210-237): CHC: Assertion violation happens here.
|
||||
@ -0,0 +1,24 @@
|
||||
contract D {
|
||||
uint public x;
|
||||
function setD(uint _x) public { x = _x; }
|
||||
}
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
address d;
|
||||
}
|
||||
S[] ss;
|
||||
constructor() {
|
||||
ss.push(S(address(new D())));
|
||||
assert(D(ss[0].d).x() == 0); // should hold
|
||||
}
|
||||
function f() public view {
|
||||
assert(D(ss[0].d).x() == 0); // should fail
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// SMTTargets: assert
|
||||
// ----
|
||||
// Warning 6328: (253-280): CHC: Assertion violation happens here.\nCounterexample:\nss = [{d: 0x4706}]\n\nTransaction trace:\nC.constructor()\nState: ss = [{d: 0x4706}]\nC.f()
|
||||
@ -0,0 +1,21 @@
|
||||
contract D {
|
||||
uint public x;
|
||||
function setD(uint _x) public { x = _x; }
|
||||
}
|
||||
|
||||
contract C {
|
||||
address[] ds;
|
||||
constructor() {
|
||||
ds.push(address(new D()));
|
||||
assert(D(ds[0]).x() == 0); // should hold
|
||||
}
|
||||
function f() public view {
|
||||
assert(D(ds[0]).x() == 0); // should fail
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// SMTTargets: assert
|
||||
// ----
|
||||
// Warning 6328: (226-251): CHC: Assertion violation happens here.\nCounterexample:\nds = [0x0]\n\nTransaction trace:\nC.constructor()\nState: ds = [0x0]\nC.f()
|
||||
@ -0,0 +1,20 @@
|
||||
contract D {
|
||||
uint public x;
|
||||
}
|
||||
|
||||
contract C {
|
||||
address[] ds;
|
||||
constructor() {
|
||||
ds.push(address(new D()));
|
||||
assert(D(ds[0]).x() == 0); // should hold
|
||||
}
|
||||
function f() public view {
|
||||
assert(D(ds[0]).x() == 0); // should hold, but fails because we havoc the state
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// SMTTargets: assert
|
||||
// ----
|
||||
// Warning 6328: (183-208): CHC: Assertion violation happens here.\nCounterexample:\nds = [0x25]\n\nTransaction trace:\nC.constructor()\nState: ds = [0x25]\nC.f()
|
||||
@ -0,0 +1,24 @@
|
||||
contract D {
|
||||
uint public x;
|
||||
function setD(uint _x) public { x = _x; }
|
||||
}
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
address d;
|
||||
}
|
||||
S s;
|
||||
constructor() {
|
||||
s.d = address(new D());
|
||||
assert(D(s.d).x() == 0); // should hold
|
||||
}
|
||||
function f() public view {
|
||||
assert(D(s.d).x() == 0); // should fail
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// SMTTargets: assert
|
||||
// ----
|
||||
// Warning 6328: (240-263): CHC: Assertion violation happens here.\nCounterexample:\ns = {d: 0x5039}\n\nTransaction trace:\nC.constructor()\nState: s = {d: 0x5039}\nC.f()
|
||||
@ -0,0 +1,23 @@
|
||||
contract D {
|
||||
uint public x;
|
||||
}
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
address d;
|
||||
}
|
||||
S s;
|
||||
constructor() {
|
||||
s.d = address(new D());
|
||||
assert(D(s.d).x() == 0); // should hold
|
||||
}
|
||||
function f() public view {
|
||||
assert(D(s.d).x() == 0); // should hold, but fails because we havoc the state
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// SMTTargets: assert
|
||||
// ----
|
||||
// Warning 6328: (197-220): CHC: Assertion violation happens here.\nCounterexample:\ns = {d: 0x5039}\n\nTransaction trace:\nC.constructor()\nState: s = {d: 0x5039}\nC.f()
|
||||
@ -0,0 +1,26 @@
|
||||
contract D {
|
||||
uint public x;
|
||||
}
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
address d;
|
||||
}
|
||||
struct T {
|
||||
S s;
|
||||
}
|
||||
T t;
|
||||
constructor() {
|
||||
t.s.d = address(new D());
|
||||
assert(D(t.s.d).x() == 0); // should hold
|
||||
}
|
||||
function f() public view {
|
||||
assert(D(t.s.d).x() == 0); // should hold, but fails because we havoc the state
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// SMTTargets: assert
|
||||
// ----
|
||||
// Warning 6328: (223-248): CHC: Assertion violation happens here.\nCounterexample:\nt = {s: {d: 0x5039}}\n\nTransaction trace:\nC.constructor()\nState: t = {s: {d: 0x5039}}\nC.f()
|
||||
@ -0,0 +1,27 @@
|
||||
contract D {
|
||||
uint public x;
|
||||
function setD(uint _x) public { x = _x; }
|
||||
}
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
address d;
|
||||
}
|
||||
struct T {
|
||||
S s;
|
||||
}
|
||||
T t;
|
||||
constructor() {
|
||||
t.s.d = address(new D());
|
||||
assert(D(t.s.d).x() == 0); // should hold
|
||||
}
|
||||
function f() public view {
|
||||
assert(D(t.s.d).x() == 0); // should fail
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// SMTTargets: assert
|
||||
// ----
|
||||
// Warning 6328: (266-291): CHC: Assertion violation happens here.\nCounterexample:\nt = {s: {d: 0x5039}}\n\nTransaction trace:\nC.constructor()\nState: t = {s: {d: 0x5039}}\nC.f()
|
||||
@ -0,0 +1,23 @@
|
||||
contract D {
|
||||
uint public x;
|
||||
}
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
D d;
|
||||
}
|
||||
S[] ss;
|
||||
constructor() {
|
||||
ss.push(S(new D()));
|
||||
assert(ss[0].d.x() == 0); // should hold
|
||||
}
|
||||
function f() public view {
|
||||
assert(ss[0].d.x() == 0); // should hold, but fails because we havoc the state
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// SMTTargets: assert
|
||||
// ----
|
||||
// Warning 6328: (192-216): CHC: Assertion violation happens here.
|
||||
@ -0,0 +1,24 @@
|
||||
contract D {
|
||||
uint public x;
|
||||
function setD(uint _x) public { x = _x; }
|
||||
}
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
D d;
|
||||
}
|
||||
S[] ss;
|
||||
constructor() {
|
||||
ss.push(S(new D()));
|
||||
assert(ss[0].d.x() == 0); // should hold
|
||||
}
|
||||
function f() public view {
|
||||
assert(ss[0].d.x() == 0); // should fail
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// SMTTargets: assert
|
||||
// ----
|
||||
// Warning 6328: (235-259): CHC: Assertion violation happens here.\nCounterexample:\nss = [{d: 20819}]\n\nTransaction trace:\nC.constructor()\nState: ss = [{d: 20819}]\nC.f()
|
||||
@ -0,0 +1,21 @@
|
||||
contract D {
|
||||
uint public x;
|
||||
function setD(uint _x) public { x = _x; }
|
||||
}
|
||||
|
||||
contract C {
|
||||
D[] ds;
|
||||
constructor() {
|
||||
ds.push(new D());
|
||||
assert(ds[0].x() == 0); // should hold
|
||||
}
|
||||
function f() public view {
|
||||
assert(ds[0].x() == 0); // should fail
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// SMTTargets: assert
|
||||
// ----
|
||||
// Warning 6328: (208-230): CHC: Assertion violation happens here.\nCounterexample:\nds = [39]\n\nTransaction trace:\nC.constructor()\nState: ds = [39]\nC.f()
|
||||
@ -0,0 +1,21 @@
|
||||
contract D {
|
||||
uint public x;
|
||||
}
|
||||
|
||||
contract C {
|
||||
D[] ds;
|
||||
constructor() {
|
||||
ds.push(new D());
|
||||
assert(ds[0].x() == 0); // should hold
|
||||
}
|
||||
function f() public view {
|
||||
assert(ds[0].x() == 0); // should hold, but fails because we havoc the state
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// SMTTargets: assert
|
||||
// SMTIgnoreCex: yes
|
||||
// ----
|
||||
// Warning 6328: (165-187): CHC: Assertion violation happens here.
|
||||
@ -0,0 +1,24 @@
|
||||
contract D {
|
||||
uint public x;
|
||||
function setD(uint _x) public { x = _x; }
|
||||
}
|
||||
|
||||
contract C {
|
||||
struct S {
|
||||
D d;
|
||||
}
|
||||
S s;
|
||||
constructor() {
|
||||
s.d = new D();
|
||||
assert(s.d.x() == 0); // should hold
|
||||
}
|
||||
function f() public view {
|
||||
assert(s.d.x() == 0); // should fail
|
||||
}
|
||||
}
|
||||
// ====
|
||||
// SMTEngine: chc
|
||||
// SMTExtCalls: trusted
|
||||
// SMTTargets: assert
|
||||
// ----
|
||||
// Warning 6328: (222-242): CHC: Assertion violation happens here.\nCounterexample:\ns = {d: 20819}\n\nTransaction trace:\nC.constructor()\nState: s = {d: 20819}\nC.f()
|
||||
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue
Block a user