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 Nov 22, 2023
1 parent 58811f1 commit 9e713cb
Show file tree
Hide file tree
Showing 11 changed files with 305 additions and 36 deletions.
2 changes: 1 addition & 1 deletion Changelog.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ Language Features:


Compiler Features:

* SMTChecker: Support `bytes.concat` function with an exception of string literals provided as an argument to `bytes.concat` call.

Bugfixes:

Expand Down
8 changes: 4 additions & 4 deletions libsolidity/formal/CHC.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -950,7 +950,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{error, address, state().abi(), state().bytesConcat(), state().crypto()};

auto nondet = (*m_nondetInterfaces.at(&_contract))(stateExprs + preCallState + postCallState);
auto nondetCall = callPredicate(stateExprs + preCallState + postCallState);
Expand Down Expand Up @@ -1033,7 +1033,7 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
&_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{error, state().thisAddress(), state().abi(), state().bytesConcat(), state().crypto()};

auto nondet = (*m_nondetInterfaces.at(m_currentContract))(stateExprs + preCallState + postCallState);
auto nondetCall = callPredicate(stateExprs + preCallState + postCallState);
Expand Down Expand Up @@ -1464,7 +1464,7 @@ 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{errorPost, state().thisAddress(), state().abi(), state().bytesConcat(), state().crypto(), 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 +1829,7 @@ 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{errorFlag().currentValue(), _contractAddressValue, state().abi(), state().bytesConcat(), state().crypto(), state().tx(), state().state()};

auto const* contract = _funDef->annotation().contract;
auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
Expand Down
34 changes: 17 additions & 17 deletions libsolidity/formal/Predicate.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -229,7 +229,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, 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 +285,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(5));
std::vector<std::string> values;
for (auto const& _var: txVars)
if (auto v = txValues.at(_var))
Expand All @@ -303,7 +303,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() + 7 + 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 +337,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, 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, bytesConcatFunctions, cryptoFunctions, txData, preBlockchainState, postBlockchainState, preStateVars, postStateVars).
/// Here we are interested in postStateVars.
auto stateVars = stateVariables();
solAssert(stateVars.has_value(), "");
Expand All @@ -347,12 +347,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() + 7 + 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() + 8 + static_cast<int>(stateVars->size());
stateLast = stateFirst + static_cast<int>(stateVars->size());
}
else if (programVariable())
Expand All @@ -371,7 +371,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, 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 +381,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() + 7 + 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 +395,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, 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 +405,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() + 7 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;

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

Expand All @@ -418,7 +418,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, 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 +452,19 @@ 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, bytesConcatFunctions, cryptoFunctions, blockchainState, stateVariables).
// An invariant for an interface predicate is a contract
// invariant over its state, for example `x <= 0`.
if (isInterface())
{
solAssert(starts_with(predName, "interface"), "");
subst[_predExpr.arguments.at(0).name] = "address(this)";
solAssert(nArgs == stateVars.size() + 4, "");
solAssert(nArgs == stateVars.size() + 5, "");
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 - 5)->name();
}
// The signature of a nondet interface predicate is
// nondet_interface(error, this, abiFunctions, cryptoFunctions, blockchainState, stateVariables, blockchainState', stateVariables').
// nondet_interface(error, this, abiFunctions, 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 +475,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 + 7, "");
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
19 changes: 12 additions & 7 deletions libsolidity/formal/PredicateInstance.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,14 +29,16 @@ namespace solidity::frontend::smt
smtutil::Expression interfacePre(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
{
auto& state = _context.state();
std::vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.abi(0), state.crypto(0), state.state(0)};
std::vector<smtutil::Expression> stateExprs{state.thisAddress(0),
state.abi(0), state.bytesConcat(0), state.crypto(0), state.state(0)};
return _pred(stateExprs + initialStateVariables(_contract, _context));
}

smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
{
auto const& state = _context.state();
std::vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.abi(0), state.crypto(0), state.state()};
std::vector<smtutil::Expression> stateExprs{state.thisAddress(0),
state.abi(0), state.bytesConcat(0), state.crypto(0), state.state()};
return _pred(stateExprs + currentStateVariables(_contract, _context));
}

Expand All @@ -48,7 +50,8 @@ smtutil::Expression nondetInterface(
unsigned _postIdx)
{
auto const& state = _context.state();
std::vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(), state.abi(), state.crypto()};
std::vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(),
state.abi(), state.bytesConcat(0), state.crypto()};
return _pred(
stateExprs +
std::vector<smtutil::Expression>{_context.state().state(_preIdx)} +
Expand All @@ -65,7 +68,7 @@ smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _contex
return _pred(currentFunctionVariablesForDefinition(*constructor, &contract, _context));

auto& state = _context.state();
std::vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state(0), state.state()};
std::vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.bytesConcat(0), state.crypto(0), state.tx(0), state.state(0), state.state()};
return _pred(stateExprs + initialStateVariables(contract, _context) + currentStateVariables(contract, _context));
}

Expand All @@ -76,7 +79,7 @@ smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _co
return _pred(currentFunctionVariablesForCall(*constructor, &contract, _context, _internal));

auto& state = _context.state();
std::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()};
std::vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), _internal ? state.thisAddress(0) : state.thisAddress(), state.abi(0), state.bytesConcat(0), state.crypto(0), _internal ? state.tx(0) : state.tx(), state.state()};
state.newState();
stateExprs += std::vector<smtutil::Expression>{state.state()};
stateExprs += currentStateVariables(contract, _context);
Expand Down Expand Up @@ -152,7 +155,8 @@ std::vector<smtutil::Expression> currentFunctionVariablesForDefinition(
)
{
auto& state = _context.state();
std::vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state(0)};
std::vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0),
state.abi(0), state.bytesConcat(0), state.crypto(0), state.tx(0), state.state(0)};
exprs += _contract ? initialStateVariables(*_contract, _context) : std::vector<smtutil::Expression>{};
exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->valueAtIndex(0); });
exprs += std::vector<smtutil::Expression>{state.state()};
Expand All @@ -170,7 +174,8 @@ std::vector<smtutil::Expression> currentFunctionVariablesForCall(
)
{
auto& state = _context.state();
std::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()};
std::vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), _internal ? state.thisAddress(0) : state.thisAddress(),
state.abi(0), state.bytesConcat(0), state.crypto(0), _internal ? state.tx(0) : state.tx(), state.state()};
exprs += _contract ? currentStateVariables(*_contract, _context) : std::vector<smtutil::Expression>{};
exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });

Expand Down
8 changes: 4 additions & 4 deletions libsolidity/formal/PredicateSort.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ namespace solidity::frontend::smt
SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _state)
{
return std::make_shared<FunctionSort>(
std::vector<SortPointer>{_state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.stateSort()} + stateSorts(_contract),
std::vector<SortPointer>{_state.thisAddressSort(), _state.abiSort(), _state.bytesConcatSort(), _state.cryptoSort(), _state.stateSort()} + stateSorts(_contract),
SortProvider::boolSort
);
}
Expand All @@ -40,7 +40,7 @@ SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicSta
auto varSorts = stateSorts(_contract);
std::vector<SortPointer> stateSort{_state.stateSort()};
return std::make_shared<FunctionSort>(
std::vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort()} +
std::vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.bytesConcatSort(), _state.cryptoSort()} +
stateSort +
varSorts +
stateSort +
Expand All @@ -57,7 +57,7 @@ SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState&
auto varSorts = stateSorts(_contract);
std::vector<SortPointer> stateSort{_state.stateSort()};
return std::make_shared<FunctionSort>(
std::vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + varSorts + varSorts,
std::vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.bytesConcatSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + varSorts + varSorts,
SortProvider::boolSort
);
}
Expand All @@ -69,7 +69,7 @@ SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition
auto inputSorts = applyMap(_function.parameters(), smtSort);
auto outputSorts = applyMap(_function.returnParameters(), smtSort);
return std::make_shared<FunctionSort>(
std::vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()} +
std::vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.bytesConcatSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()} +
varSorts +
inputSorts +
std::vector<SortPointer>{_state.stateSort()} +
Expand Down
Loading

0 comments on commit 9e713cb

Please sign in to comment.