diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 267ea9269..28026ec6f 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -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(callExpr->annotation().type); + ContractDefinition const* contract = + &dynamic_cast(*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(_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)); +} diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index fd54db6c2..9524d86dc 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -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. diff --git a/libsolidity/formal/PredicateInstance.cpp b/libsolidity/formal/PredicateInstance.cpp index aff6aa19b..5e057efe3 100644 --- a/libsolidity/formal/PredicateInstance.cpp +++ b/libsolidity/formal/PredicateInstance.cpp @@ -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(*_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 stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state()}; + vector 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{state.state()}; stateExprs += currentStateVariables(contract, _context); @@ -166,11 +166,12 @@ vector currentFunctionVariablesForDefinition( vector currentFunctionVariablesForCall( FunctionDefinition const& _function, ContractDefinition const* _contract, - EncodingContext& _context + EncodingContext& _context, + bool _internal ) { auto& state = _context.state(); - vector exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state()}; + vector 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{}; exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); }); diff --git a/libsolidity/formal/PredicateInstance.h b/libsolidity/formal/PredicateInstance.h index 2f6c77381..42a9e2040 100644 --- a/libsolidity/formal/PredicateInstance.h +++ b/libsolidity/formal/PredicateInstance.h @@ -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 currentFunctionVariablesForDefinition( std::vector currentFunctionVariablesForCall( FunctionDefinition const& _function, ContractDefinition const* _contract, - EncodingContext& _context + EncodingContext& _context, + bool _internal = true ); std::vector currentBlockVariables( diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 4e8fded22..e2e9f4ffb 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -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)