Skip to content

Commit

Permalink
Support bytes concat
Browse files Browse the repository at this point in the history
  • Loading branch information
@pgebal
pgebal committed Jan 23, 2024
1 parent 01cb85f commit a8d6a44
Show file tree
Hide file tree
Showing 21 changed files with 460 additions and 80 deletions.
3 changes: 2 additions & 1 deletion Changelog.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,8 @@ Language Features:
* Yul: Introduce builtin ``blobhash()`` for retrieving versioned hashes of blobs associated with the transaction.

Compiler Features:
* EVM: Support for the EVM Version "Cancun".
* EVM: Support for the EVM Version "Cancun".
* SMTChecker: Support `bytes.concat` except when string literals are passed as arguments.

Bugfixes:
* AST import: Fix bug when importing inline assembly with empty ``let`` variable declaration.
Expand Down
24 changes: 15 additions & 9 deletions libsolidity/formal/CHC.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -940,8 +940,6 @@ void CHC::nondetCall(ContractDefinition const& _contract, VariableDeclaration co
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(),
Expand All @@ -950,7 +948,7 @@ void CHC::nondetCall(ContractDefinition const& _contract, VariableDeclaration co
m_currentContract
);
auto postCallState = std::vector<smtutil::Expression>{state().state()} + currentStateVariables(_contract);
std::vector<smtutil::Expression> stateExprs{error, address, state().abi(), state().crypto()};
std::vector<smtutil::Expression> stateExprs = commonStateExpressions(errorFlag().increaseIndex(), address);

auto nondet = (*m_nondetInterfaces.at(&_contract))(stateExprs + preCallState + postCallState);
auto nondetCall = callPredicate(stateExprs + preCallState + postCallState);
Expand Down Expand Up @@ -1024,16 +1022,14 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
m_context.variable(*var)->increaseIndex();
}

auto error = errorFlag().increaseIndex();

Predicate const& callPredicate = *createSymbolicBlock(
nondetInterfaceSort(*m_currentContract, state()),
"nondet_call_" + uniquePrefix(),
PredicateType::ExternalCallUntrusted,
&_funCall
);
auto postCallState = std::vector<smtutil::Expression>{state().state()} + currentStateVariables();
std::vector<smtutil::Expression> stateExprs{error, state().thisAddress(), state().abi(), state().crypto()};
std::vector<smtutil::Expression> stateExprs = commonStateExpressions(errorFlag().increaseIndex(), state().thisAddress());

auto nondet = (*m_nondetInterfaces.at(m_currentContract))(stateExprs + preCallState + postCallState);
auto nondetCall = callPredicate(stateExprs + preCallState + postCallState);
Expand Down Expand Up @@ -1464,7 +1460,9 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
auto errorPost = errorFlag().increaseIndex();
auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2);

std::vector<smtutil::Expression> args{errorPost, state().thisAddress(), state().abi(), state().crypto(), state().tx(), state().state(1)};
std::vector<smtutil::Expression> args =
commonStateExpressions(errorPost, state().thisAddress()) +
std::vector<smtutil::Expression>{state().tx(), state().state(1)};
args += state1 +
applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) +
std::vector<smtutil::Expression>{state().state(2)} +
Expand Down Expand Up @@ -1829,7 +1827,9 @@ smtutil::Expression CHC::predicate(

errorFlag().increaseIndex();

std::vector<smtutil::Expression> args{errorFlag().currentValue(), _contractAddressValue, state().abi(), state().crypto(), state().tx(), state().state()};
std::vector<smtutil::Expression> args =
commonStateExpressions(errorFlag().currentValue(), _contractAddressValue) +
std::vector<smtutil::Expression>{state().tx(), state().state()};

auto const* contract = _funDef->annotation().contract;
auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
Expand Down Expand Up @@ -2311,7 +2311,6 @@ std::optional<std::string> CHC::generateCounterexample(CHCSolverInterface::CexGr
path.emplace_back("State: " + modelMsg);
}
}

std::string txCex = summaryPredicate->formatSummaryCall(summaryArgs, m_charStreamProvider);

std::list<std::string> calls;
Expand Down Expand Up @@ -2486,3 +2485,10 @@ void CHC::decreaseBalanceFromOptionsValue(Expression const& _value)
{
state().addBalance(state().thisAddress(), 0 - expr(_value));
}

std::vector<smtutil::Expression> CHC::commonStateExpressions(smtutil::Expression const& error, smtutil::Expression const& address)
{
if (state().hasBytesConcatFunction())
return {error, address, state().abi(), state().bytesConcat(), state().crypto()};
return {error, address, state().abi(), state().crypto()};
}
2 changes: 2 additions & 0 deletions libsolidity/formal/CHC.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -362,6 +362,8 @@ class CHC: public SMTEncoder

/// Adds constraints that decrease the balance of the caller by _value.
void decreaseBalanceFromOptionsValue(Expression const& _value);

std::vector<smtutil::Expression> commonStateExpressions(smtutil::Expression const& error, smtutil::Expression const& address);
//@}

/// Predicates.
Expand Down
42 changes: 23 additions & 19 deletions libsolidity/formal/Predicate.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,13 +55,15 @@ Predicate const* Predicate::create(
return &m_predicates.emplace(
std::piecewise_construct,
std::forward_as_tuple(functorName),
std::forward_as_tuple(std::move(predicate), _type, _node, _contractContext, std::move(_scopeStack))
std::forward_as_tuple(std::move(predicate), _type, _context.state().hasBytesConcatFunction(),
_node, _contractContext, std::move(_scopeStack))
).first->second;
}

Predicate::Predicate(
smt::SymbolicFunctionVariable&& _predicate,
PredicateType _type,
bool _bytesConcatFunctionInContext,
ASTNode const* _node,
ContractDefinition const* _contractContext,
std::vector<ScopeOpener const*> _scopeStack
Expand All @@ -70,7 +72,8 @@ Predicate::Predicate(
m_type(_type),
m_node(_node),
m_contractContext(_contractContext),
m_scopeStack(_scopeStack)
m_scopeStack(_scopeStack),
m_bytesConcatFunctionInContext(_bytesConcatFunctionInContext)
{
}

Expand Down Expand Up @@ -229,7 +232,7 @@ std::string Predicate::formatSummaryCall(
return {};
}

/// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// The signature of a function summary predicate is: summary(error, this, abiFunctions, (optionally) bytesConcatFunctions, cryptoFunctions, txData, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// Here we are interested in preInputVars to format the function call.

std::string txModel;
Expand Down Expand Up @@ -285,7 +288,7 @@ std::string Predicate::formatSummaryCall(
}

// Here we are interested in txData from the summary predicate.
auto txValues = readTxVars(_args.at(4));
auto txValues = readTxVars(_args.at(txValuesIndex()));
std::vector<std::string> values;
for (auto const& _var: txVars)
if (auto v = txValues.at(_var))
Expand All @@ -303,7 +306,7 @@ std::string Predicate::formatSummaryCall(
auto const* fun = programFunction();
solAssert(fun, "");

auto first = _args.begin() + 6 + static_cast<int>(stateVars->size());
auto first = _args.begin() + static_cast<int>(firstArgIndex()) + static_cast<int>(stateVars->size());
auto last = first + static_cast<int>(fun->parameters().size());
solAssert(first >= _args.begin() && first <= _args.end(), "");
solAssert(last >= _args.begin() && last <= _args.end(), "");
Expand Down Expand Up @@ -337,8 +340,8 @@ std::string Predicate::formatSummaryCall(

std::vector<std::optional<std::string>> Predicate::summaryStateValues(std::vector<smtutil::Expression> const& _args) const
{
/// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// The signature of the summary predicate of a contract without constructor is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, postBlockchainState, preStateVars, postStateVars).
/// The signature of a function summary predicate is: summary(error, this, abiFunctions, (optionally) bytesConcatFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// The signature of the summary predicate of a contract without constructor is: summary(error, this, abiFunctions, (optionally) bytesConcatFunctions, cryptoFunctions, txData, preBlockchainState, postBlockchainState, preStateVars, postStateVars).
/// Here we are interested in postStateVars.
auto stateVars = stateVariables();
solAssert(stateVars.has_value(), "");
Expand All @@ -347,12 +350,12 @@ std::vector<std::optional<std::string>> Predicate::summaryStateValues(std::vecto
std::vector<smtutil::Expression>::const_iterator stateLast;
if (auto const* function = programFunction())
{
stateFirst = _args.begin() + 6 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size()) + 1;
stateFirst = _args.begin() + static_cast<int>(firstArgIndex()) + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size()) + 1;
stateLast = stateFirst + static_cast<int>(stateVars->size());
}
else if (programContract())
{
stateFirst = _args.begin() + 7 + static_cast<int>(stateVars->size());
stateFirst = _args.begin() + static_cast<int>(firstStateVarIndex()) + static_cast<int>(stateVars->size());
stateLast = stateFirst + static_cast<int>(stateVars->size());
}
else if (programVariable())
Expand All @@ -371,7 +374,7 @@ std::vector<std::optional<std::string>> Predicate::summaryStateValues(std::vecto

std::vector<std::optional<std::string>> Predicate::summaryPostInputValues(std::vector<smtutil::Expression> const& _args) const
{
/// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// The signature of a function summary predicate is: summary(error, this, abiFunctions, (optionally) bytesConcatFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// Here we are interested in postInputVars.
auto const* function = programFunction();
solAssert(function, "");
Expand All @@ -381,7 +384,7 @@ std::vector<std::optional<std::string>> Predicate::summaryPostInputValues(std::v

auto const& inParams = function->parameters();

auto first = _args.begin() + 6 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
auto first = _args.begin() + static_cast<int>(firstArgIndex()) + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
auto last = first + static_cast<int>(inParams.size());

solAssert(first >= _args.begin() && first <= _args.end(), "");
Expand All @@ -395,7 +398,7 @@ std::vector<std::optional<std::string>> Predicate::summaryPostInputValues(std::v

std::vector<std::optional<std::string>> Predicate::summaryPostOutputValues(std::vector<smtutil::Expression> const& _args) const
{
/// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// The signature of a function summary predicate is: summary(error, this, abiFunctions, (optionally) bytesConcatFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// Here we are interested in outputVars.
auto const* function = programFunction();
solAssert(function, "");
Expand All @@ -405,7 +408,7 @@ std::vector<std::optional<std::string>> Predicate::summaryPostOutputValues(std::

auto const& inParams = function->parameters();

auto first = _args.begin() + 6 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;
auto first = _args.begin() + static_cast<int>(firstArgIndex()) + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;

solAssert(first >= _args.begin() && first <= _args.end(), "");

Expand All @@ -418,7 +421,7 @@ std::vector<std::optional<std::string>> Predicate::summaryPostOutputValues(std::
std::pair<std::vector<std::optional<std::string>>, std::vector<VariableDeclaration const*>> Predicate::localVariableValues(std::vector<smtutil::Expression> const& _args) const
{
/// The signature of a local block predicate is:
/// block(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars, localVars).
/// block(error, this, abiFunctions, (optionally) bytesConcatFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars, localVars).
/// Here we are interested in localVars.
auto const* function = programFunction();
solAssert(function, "");
Expand Down Expand Up @@ -452,19 +455,20 @@ std::map<std::string, std::string> Predicate::expressionSubstitution(smtutil::Ex
auto nArgs = _predExpr.arguments.size();

// The signature of an interface predicate is
// interface(this, abiFunctions, cryptoFunctions, blockchainState, stateVariables).
// interface(this, abiFunctions, (optionally) bytesConcatFunctions, cryptoFunctions, blockchainState, stateVariables).
// An invariant for an interface predicate is a contract
// invariant over its state, for example `x <= 0`.
if (isInterface())
{
size_t shift = txValuesIndex();
solAssert(starts_with(predName, "interface"), "");
subst[_predExpr.arguments.at(0).name] = "address(this)";
solAssert(nArgs == stateVars.size() + 4, "");
solAssert(nArgs == stateVars.size() + shift, "");
for (size_t i = nArgs - stateVars.size(); i < nArgs; ++i)
subst[_predExpr.arguments.at(i).name] = stateVars.at(i - 4)->name();
subst[_predExpr.arguments.at(i).name] = stateVars.at(i - shift)->name();
}
// The signature of a nondet interface predicate is
// nondet_interface(error, this, abiFunctions, cryptoFunctions, blockchainState, stateVariables, blockchainState', stateVariables').
// nondet_interface(error, this, abiFunctions, (optionally) bytesConcatFunctions, cryptoFunctions, blockchainState, stateVariables, blockchainState', stateVariables').
// An invariant for a nondet interface predicate is a reentrancy property
// over the pre and post state variables of a contract, where pre state vars
// are represented by the variable's name and post state vars are represented
Expand All @@ -475,7 +479,7 @@ std::map<std::string, std::string> Predicate::expressionSubstitution(smtutil::Ex
solAssert(starts_with(predName, "nondet_interface"), "");
subst[_predExpr.arguments.at(0).name] = "<errorCode>";
subst[_predExpr.arguments.at(1).name] = "address(this)";
solAssert(nArgs == stateVars.size() * 2 + 6, "");
solAssert(nArgs == stateVars.size() * 2 + firstArgIndex(), "");
for (size_t i = nArgs - stateVars.size(), s = 0; i < nArgs; ++i, ++s)
subst[_predExpr.arguments.at(i).name] = stateVars.at(s)->name() + "'";
for (size_t i = nArgs - (stateVars.size() * 2 + 1), s = 0; i < nArgs - (stateVars.size() + 1); ++i, ++s)
Expand Down
13 changes: 12 additions & 1 deletion libsolidity/formal/Predicate.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,6 +71,7 @@ class Predicate
Predicate(
smt::SymbolicFunctionVariable&& _predicate,
PredicateType _type,
bool _bytesConcatFunctionInContext,
ASTNode const* _node = nullptr,
ContractDefinition const* _contractContext = nullptr,
std::vector<ScopeOpener const*> _scopeStack = {}
Expand Down Expand Up @@ -179,7 +180,7 @@ class Predicate

/// @returns a substitution map from the arguments of _predExpr
/// to a Solidity-like expression.
std::map<std::string, std::string> expressionSubstitution(smtutil::Expression const& _predExpr) const;
std::map<std::string, std::string> expressionSubstitution(smtutil::Expression const& _predExprs) const;

private:
/// @returns the formatted version of the given SMT expressions. Those expressions must be SMT constants.
Expand All @@ -196,6 +197,13 @@ class Predicate

std::map<std::string, std::optional<std::string>> readTxVars(smtutil::Expression const& _tx) const;

/// @returns index at which transaction values start in args list
size_t txValuesIndex() const { return m_bytesConcatFunctionInContext ? 5 : 4; }
/// @returns index at which function arguments start in args list
size_t firstArgIndex() const { return m_bytesConcatFunctionInContext ? 7 : 6; }
/// @returns index at which state variables values start in args list
size_t firstStateVarIndex() const { return m_bytesConcatFunctionInContext ? 8 : 7; }

/// The actual SMT expression.
smt::SymbolicFunctionVariable m_predicate;

Expand All @@ -219,6 +227,9 @@ class Predicate
/// The scope stack when the predicate was created.
/// Used to identify the subset of variables in scope.
std::vector<ScopeOpener const*> const m_scopeStack;

/// True iff there is a bytes concat function in contract scope
bool m_bytesConcatFunctionInContext;
};

struct PredicateCompare
Expand Down

0 comments on commit a8d6a44

Please sign in to comment.