cerc-io/solidity
16
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

Move state model filtering from CHC to Predicate

Browse Source
This commit is contained in:
Leonardo Alt 2020-08-19 18:38:56 +02:00
parent e3a8c94ace
commit 2e2e96cc93
4 changed files with 45 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

33
libsolidity/formal/CHC.cpp
View File

@ -1429,6 +1429,8 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
solAssert((calledFun && !calledContract) || (!calledFun && calledContract), "");
auto stateVars = summaryPredicate->stateVariables();
solAssert(stateVars.has_value(), "");
auto stateValues = summaryPredicate->summaryStateValues(summaryNode.second);
solAssert(stateValues.size() == stateVars->size(), "");
/// This summary node is the end of a tx.
/// If it is the first summary node seen in this loop, it is the summary
@ -1438,7 +1440,7 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
{
lastTxSeen = true;
/// Generate counterexample message local to the failed target.
localState = formatStateCounterexample(*stateVars, calledFun, summaryNode.second) + "\n";
localState = formatStateCounterexample(*stateVars, stateValues) + "\n";
if (calledFun)
{
/// The signature of a summary predicate is: summary(error, preStateVars, preInputVars, postInputVars, outputVars).
@ -1465,7 +1467,7 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
else
/// We report the state after every tx in the trace except for the last, which is reported
/// first in the code above.
path.emplace_back("State: " + formatStateCounterexample(*stateVars, calledFun, summaryNode.second));
path.emplace_back("State: " + formatStateCounterexample(*stateVars, stateValues));
string txCex = summaryPredicate->formatSummaryCall(summaryNode.second);
path.emplace_back(txCex);
@ -1481,35 +1483,16 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
return localState + "\nTransaction trace:\n" + boost::algorithm::join(boost::adaptors::reverse(path), "\n");
}
string CHC::formatStateCounterexample(vector<VariableDeclaration const*> const& _stateVars, FunctionDefinition const* _function, vector<string> const& _summaryValues)
string CHC::formatStateCounterexample(vector<VariableDeclaration const*> const& _stateVars, vector<string> const& _values)
{
/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postInputVars, outputVars).
/// The signature of an implicit constructor summary predicate is: summary(error, postStateVars).
/// Here we are interested in postStateVars.
vector<string>::const_iterator stateFirst;
vector<string>::const_iterator stateLast;
if (_function)
{
stateFirst = _summaryValues.begin() + 1 + static_cast<int>(_stateVars.size()) + static_cast<int>(_function->parameters().size());
stateLast = stateFirst + static_cast<int>(_stateVars.size());
}
else
{
stateFirst = _summaryValues.begin() + 1;
stateLast = stateFirst + static_cast<int>(_stateVars.size());
}
solAssert(stateFirst >= _summaryValues.begin() && stateFirst <= _summaryValues.end(), "");
solAssert(stateLast >= _summaryValues.begin() && stateLast <= _summaryValues.end(), "");
vector<string> stateArgs(stateFirst, stateLast);
solAssert(stateArgs.size() == _stateVars.size(), "");
solAssert(_stateVars.size() == _values.size(), "");
vector<string> stateCex;
for (unsigned i = 0; i < stateArgs.size(); ++i)
for (unsigned i = 0; i < _values.size(); ++i)
{
auto var = _stateVars.at(i);
if (var->type()->isValueType())
stateCex.emplace_back(var->name() + " = " + stateArgs.at(i));
stateCex.emplace_back(var->name() + " = " + _values.at(i));
}
return boost::algorithm::join(stateCex, ", ");

2
libsolidity/formal/CHC.h
View File

@ -225,7 +225,7 @@ private:
/// _function was executed.
/// _function = nullptr means the transaction was the deployment of a
/// contract without an explicit constructor.
std::string formatStateCounterexample(std::vector<VariableDeclaration const*> const& _stateVariables, FunctionDefinition const* _function, std::vector<std::string> const& _summaryValues);
std::string formatStateCounterexample(std::vector<VariableDeclaration const*> const& _stateVariables, std::vector<std::string> const& _values);
/// @returns a DAG in the dot format.
/// Used for debugging purposes.

32
libsolidity/formal/Predicate.cpp
View File

@ -182,3 +182,35 @@ string Predicate::formatSummaryCall(vector<string> const& _args) const
return fName + "(" + boost::algorithm::join(functionArgs, ", ") + ")";
}
vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
{
/// The signature of a function summary predicate is: summary(error, preStateVars, preInputVars, postStateVars, postInputVars, outputVars).
/// The signature of an implicit constructor summary predicate is: summary(error, postStateVars).
/// Here we are interested in postStateVars.
auto stateVars = stateVariables();
solAssert(stateVars.has_value(), "");
vector<string>::const_iterator stateFirst;
vector<string>::const_iterator stateLast;
if (auto const* function = programFunction())
{
stateFirst = _args.begin() + 1 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size());
stateLast = stateFirst + static_cast<int>(stateVars->size());
}
else if (programContract())
{
stateFirst = _args.begin() + 1;
stateLast = stateFirst + static_cast<int>(stateVars->size());
}
else
solAssert(false, "");
solAssert(stateFirst >= _args.begin() && stateFirst <= _args.end(), "");
solAssert(stateLast >= _args.begin() && stateLast <= _args.end(), "");
vector<string> stateArgs(stateFirst, stateLast);
solAssert(stateArgs.size() == stateVars->size(), "");
return stateArgs;
}

4
libsolidity/formal/Predicate.h
View File

@ -92,6 +92,10 @@ public:
/// with _args.
std::string formatSummaryCall(std::vector<std::string> const& _args) const;
/// @returns the values of the state variables from _args at the point
/// where this summary was reached.
std::vector<std::string> summaryStateValues(std::vector<std::string> const& _args) const;
private:
/// The actual SMT expression.
smt::SymbolicFunctionVariable m_predicate;