cerc-io/solidity
11
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Support deployment

Browse Source
This commit is contained in:
Leo Alt 2021-10-12 11:21:09 +02:00
parent 287ea63cde
commit e0cda47603
5 changed files with 171 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

139
libsolidity/formal/CHC.cpp
View File

@ -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);
@ -174,15 +174,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
@ -219,6 +234,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));
@ -549,10 +567,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;
@ -725,6 +745,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, "");
@ -1120,6 +1200,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))
@ -1293,28 +1378,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, "");
@ -2087,3 +2172,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));
}

19
libsolidity/formal/CHC.h
View File

@ -111,6 +111,7 @@ private:
void visitAssert(FunctionCall const& _funCall);
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);
@ -148,6 +149,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 +315,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.

11
libsolidity/formal/PredicateInstance.cpp
View File

@ -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(); });

12
libsolidity/formal/PredicateInstance.h
View File

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

12
libsolidity/formal/SMTEncoder.cpp
View File

@ -705,10 +705,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,
@ -1063,7 +1071,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)