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

Use Expression instead of plain strings for counterexamples

Browse Source
This commit is contained in:
Leonardo Alt 2020-10-19 12:21:05 +01:00
parent 72b052eae7
commit 446e46fe06
6 changed files with 92 additions and 37 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
libsmtutil/CHCSolverInterface.h
View File

@ -44,9 +44,7 @@ public:
/// Needs to bound all vars as universally quantified.
virtual void addRule(Expression const& _expr, std::string const& _name) = 0;
/// first: predicate name
/// second: predicate arguments
using CexNode = std::pair<std::string, std::vector<std::string>>;
using CexNode = Expression;
struct CexGraph
{
std::map<unsigned, CexNode> nodes;

4
libsmtutil/Z3CHCInterface.cpp
View File

@ -161,7 +161,7 @@ CHCSolverInterface::CexGraph Z3CHCInterface::cexGraph(z3::expr const& _proof)
proofStack.push(_proof.arg(0));
auto const& root = proofStack.top();
graph.nodes[root.id()] = {name(fact(root)), arguments(fact(root))};
graph.nodes.emplace(root.id(), m_z3Interface->fromZ3Expr(fact(root)));
set<unsigned> visited;
visited.insert(root.id());
@ -186,7 +186,7 @@ CHCSolverInterface::CexGraph Z3CHCInterface::cexGraph(z3::expr const& _proof)
if (!graph.nodes.count(child.id()))
{
graph.nodes[child.id()] = {name(fact(child)), arguments(fact(child))};
graph.nodes.emplace(child.id(), m_z3Interface->fromZ3Expr(fact(child)));
graph.edges[child.id()] = {};
}

21
libsolidity/formal/CHC.cpp
View File

@ -1306,7 +1306,7 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
{
optional<unsigned> rootId;
for (auto const& [id, node]: _graph.nodes)
if (node.first == _root)
if (node.name == _root)
{
rootId = id;
break;
@ -1330,18 +1330,18 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
if (edges.size() == 2)
{
interfaceId = edges.at(1);
if (!Predicate::predicate(_graph.nodes.at(summaryId).first)->isSummary())
if (!Predicate::predicate(_graph.nodes.at(summaryId).name)->isSummary())
swap(summaryId, *interfaceId);
auto interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).first);
auto interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).name);
solAssert(interfacePredicate && interfacePredicate->isInterface(), "");
}
/// The children are unordered, so we need to check which is the summary and
/// which is the interface.
Predicate const* summaryPredicate = Predicate::predicate(_graph.nodes.at(summaryId).first);
Predicate const* summaryPredicate = Predicate::predicate(_graph.nodes.at(summaryId).name);
solAssert(summaryPredicate && summaryPredicate->isSummary(), "");
/// At this point property 2 from the function description is verified for this node.
auto summaryArgs = _graph.nodes.at(summaryId).second;
vector<smtutil::Expression> summaryArgs = _graph.nodes.at(summaryId).arguments;
FunctionDefinition const* calledFun = summaryPredicate->programFunction();
ContractDefinition const* calledContract = summaryPredicate->programContract();
@ -1387,7 +1387,7 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
/// or stop.
if (interfaceId)
{
Predicate const* interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).first);
Predicate const* interfacePredicate = Predicate::predicate(_graph.nodes.at(*interfaceId).name);
solAssert(interfacePredicate && interfacePredicate->isInterface(), "");
node = *interfaceId;
}
@ -1403,7 +1403,14 @@ string CHC::cex2dot(CHCSolverInterface::CexGraph const& _cex)
string dot = "digraph {\n";
auto pred = [&](CHCSolverInterface::CexNode const& _node) {
return "\"" + _node.first + "(" + boost::algorithm::join(_node.second, ", ") + ")\"";
vector<string> args = applyMap(
_node.arguments,
[&](auto const& arg) {
solAssert(arg.arguments.empty(), "");
return arg.name;
}
);
return "\"" + _node.name + "(" + boost::algorithm::join(args, ", ") + ")\"";
};
for (auto const& [u, vs]: _cex.edges)

7
libsolidity/formal/CHC.h
View File

@ -203,7 +203,7 @@ private:
/// @returns a set of pairs _var = _value separated by _separator.
template <typename T>
std::string formatVariableModel(std::vector<T> const& _variables, std::vector<std::string> const& _values, std::string const& _separator) const
std::string formatVariableModel(std::vector<T> const& _variables, std::vector<std::optional<std::string>> const& _values, std::string const& _separator) const
{
solAssert(_variables.size() == _values.size(), "");
@ -212,7 +212,10 @@ private:
{
auto var = _variables.at(i);
if (var && var->type()->isValueType())
assignments.emplace_back(var->name() + " = " + _values.at(i));
{
solAssert(_values.at(i), "");
assignments.emplace_back(var->name() + " = " + *_values.at(i));
}
}
return boost::algorithm::join(assignments, _separator);

79
libsolidity/formal/Predicate.cpp
View File

@ -149,7 +149,7 @@ bool Predicate::isInterface() const
return functor().name.rfind("interface", 0) == 0;
}
string Predicate::formatSummaryCall(vector<string> const& _args) const
string Predicate::formatSummaryCall(vector<smtutil::Expression> const& _args) const
{
if (programContract())
return "constructor()";
@ -163,18 +163,22 @@ string Predicate::formatSummaryCall(vector<string> const& _args) const
/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// Here we are interested in preInputVars.
vector<string>::const_iterator first = _args.begin() + 5 + static_cast<int>(stateVars->size());
vector<string>::const_iterator last = first + static_cast<int>(fun->parameters().size());
auto first = _args.begin() + 5 + 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(), "");
vector<string> functionArgsCex(first, last);
auto inTypes = FunctionType(*fun).parameterTypes();
vector<optional<string>> functionArgsCex = formatExpressions(vector<smtutil::Expression>(first, last), inTypes);
vector<string> functionArgs;
auto const& params = fun->parameters();
solAssert(params.size() == functionArgsCex.size(), "");
for (unsigned i = 0; i < params.size(); ++i)
if (params[i]->type()->isValueType())
functionArgs.emplace_back(functionArgsCex[i]);
{
solAssert(functionArgsCex.at(i), "");
functionArgs.emplace_back(*functionArgsCex.at(i));
}
else
functionArgs.emplace_back(params[i]->name());
@ -186,7 +190,7 @@ string Predicate::formatSummaryCall(vector<string> const& _args) const
}
vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
vector<optional<string>> Predicate::summaryStateValues(vector<smtutil::Expression> const& _args) const
{
/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// The signature of an implicit constructor summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, postBlockchainState, postStateVars).
@ -194,8 +198,8 @@ vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
auto stateVars = stateVariables();
solAssert(stateVars.has_value(), "");
vector<string>::const_iterator stateFirst;
vector<string>::const_iterator stateLast;
vector<smtutil::Expression>::const_iterator stateFirst;
vector<smtutil::Expression>::const_iterator stateLast;
if (auto const* function = programFunction())
{
stateFirst = _args.begin() + 5 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size()) + 1;
@ -212,12 +216,13 @@ vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
solAssert(stateFirst >= _args.begin() && stateFirst <= _args.end(), "");
solAssert(stateLast >= _args.begin() && stateLast <= _args.end(), "");
vector<string> stateArgs(stateFirst, stateLast);
vector<smtutil::Expression> stateArgs(stateFirst, stateLast);
solAssert(stateArgs.size() == stateVars->size(), "");
return stateArgs;
auto stateTypes = applyMap(*stateVars, [&](auto const& _var) { return _var->type(); });
return formatExpressions(stateArgs, stateTypes);
}
vector<string> Predicate::summaryPostInputValues(vector<string> const& _args) const
vector<optional<string>> Predicate::summaryPostInputValues(vector<smtutil::Expression> const& _args) const
{
/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// Here we are interested in postInputVars.
@ -229,18 +234,19 @@ vector<string> Predicate::summaryPostInputValues(vector<string> const& _args) co
auto const& inParams = function->parameters();
vector<string>::const_iterator first = _args.begin() + 5 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
vector<string>::const_iterator last = first + static_cast<int>(inParams.size());
auto first = _args.begin() + 5 + 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(), "");
solAssert(last >= _args.begin() && last <= _args.end(), "");
vector<string> inValues(first, last);
vector<smtutil::Expression> inValues(first, last);
solAssert(inValues.size() == inParams.size(), "");
return inValues;
auto inTypes = FunctionType(*function).parameterTypes();
return formatExpressions(inValues, inTypes);
}
vector<string> Predicate::summaryPostOutputValues(vector<string> const& _args) const
vector<optional<string>> Predicate::summaryPostOutputValues(vector<smtutil::Expression> const& _args) const
{
/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// Here we are interested in outputVars.
@ -252,11 +258,46 @@ vector<string> Predicate::summaryPostOutputValues(vector<string> const& _args) c
auto const& inParams = function->parameters();
vector<string>::const_iterator first = _args.begin() + 5 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;
auto first = _args.begin() + 5 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;
solAssert(first >= _args.begin() && first <= _args.end(), "");
vector<string> outValues(first, _args.end());
vector<smtutil::Expression> outValues(first, _args.end());
solAssert(outValues.size() == function->returnParameters().size(), "");
return outValues;
auto outTypes = FunctionType(*function).returnParameterTypes();
return formatExpressions(outValues, outTypes);
}
vector<optional<string>> Predicate::formatExpressions(vector<smtutil::Expression> const& _exprs, vector<TypePointer> const& _types) const
{
solAssert(_exprs.size() == _types.size(), "");
vector<optional<string>> strExprs;
for (unsigned i = 0; i < _exprs.size(); ++i)
strExprs.push_back(expressionToString(_exprs.at(i), _types.at(i)));
return strExprs;
}
optional<string> Predicate::expressionToString(smtutil::Expression const& _expr, TypePointer _type) const
{
if (smt::isNumber(*_type))
{
solAssert(_expr.sort->kind == Kind::Int, "");
solAssert(_expr.arguments.empty(), "");
// TODO assert that _expr.name is a number.
return _expr.name;
}
if (smt::isBool(*_type))
{
solAssert(_expr.sort->kind == Kind::Bool, "");
solAssert(_expr.arguments.empty(), "");
solAssert(_expr.name == "true" || _expr.name == "false", "");
return _expr.name;
}
if (smt::isFunction(*_type))
{
solAssert(_expr.arguments.empty(), "");
return _expr.name;
}
return {};
}

14
libsolidity/formal/Predicate.h
View File

@ -107,21 +107,27 @@ public:
/// @returns a formatted string representing a call to this predicate
/// with _args.
std::string formatSummaryCall(std::vector<std::string> const& _args) const;
std::string formatSummaryCall(std::vector<smtutil::Expression> 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;
std::vector<std::optional<std::string>> summaryStateValues(std::vector<smtutil::Expression> const& _args) const;
/// @returns the values of the function input variables from _args at the point
/// where this summary was reached.
std::vector<std::string> summaryPostInputValues(std::vector<std::string> const& _args) const;
std::vector<std::optional<std::string>> summaryPostInputValues(std::vector<smtutil::Expression> const& _args) const;
/// @returns the values of the function output variables from _args at the point
/// where this summary was reached.
std::vector<std::string> summaryPostOutputValues(std::vector<std::string> const& _args) const;
std::vector<std::optional<std::string>> summaryPostOutputValues(std::vector<smtutil::Expression> const& _args) const;
private:
/// @returns the formatted version of the given SMT expressions. Those expressions must be SMT constants.
std::vector<std::optional<std::string>> formatExpressions(std::vector<smtutil::Expression> const& _exprs, std::vector<TypePointer> const& _types) const;
/// @returns a string representation of the SMT expression based on a Solidity type.
std::optional<std::string> expressionToString(smtutil::Expression const& _expr, TypePointer _type) const;
/// The actual SMT expression.
smt::SymbolicFunctionVariable m_predicate;