mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Merge pull request #10068 from ethereum/smt_from_z3_expr
Refactor SMT cex graph
This commit is contained in:
Leonardo
GitHub
commit
f1ed510045
@ -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;
|
||||
|
||||
@ -60,6 +60,8 @@ class Expression
|
||||
public:
|
||||
explicit Expression(bool _v): Expression(_v ? "true" : "false", Kind::Bool) {}
|
||||
explicit Expression(std::shared_ptr<SortSort> _sort, std::string _name = ""): Expression(std::move(_name), {}, _sort) {}
|
||||
explicit Expression(std::string _name, std::vector<Expression> _arguments, SortPointer _sort):
|
||||
name(std::move(_name)), arguments(std::move(_arguments)), sort(std::move(_sort)) {}
|
||||
Expression(size_t _number): Expression(std::to_string(_number), {}, SortProvider::sintSort) {}
|
||||
Expression(u256 const& _number): Expression(_number.str(), {}, SortProvider::sintSort) {}
|
||||
Expression(s256 const& _number): Expression(_number.str(), {}, SortProvider::sintSort) {}
|
||||
@ -233,14 +235,26 @@ public:
|
||||
|
||||
friend Expression operator!(Expression _a)
|
||||
{
|
||||
if (_a.sort->kind == Kind::BitVector)
|
||||
return ~_a;
|
||||
return Expression("not", std::move(_a), Kind::Bool);
|
||||
}
|
||||
friend Expression operator&&(Expression _a, Expression _b)
|
||||
{
|
||||
if (_a.sort->kind == Kind::BitVector)
|
||||
{
|
||||
smtAssert(_b.sort->kind == Kind::BitVector, "");
|
||||
return _a & _b;
|
||||
}
|
||||
return Expression("and", std::move(_a), std::move(_b), Kind::Bool);
|
||||
}
|
||||
friend Expression operator||(Expression _a, Expression _b)
|
||||
{
|
||||
if (_a.sort->kind == Kind::BitVector)
|
||||
{
|
||||
smtAssert(_b.sort->kind == Kind::BitVector, "");
|
||||
return _a | _b;
|
||||
}
|
||||
return Expression("or", std::move(_a), std::move(_b), Kind::Bool);
|
||||
}
|
||||
friend Expression operator==(Expression _a, Expression _b)
|
||||
@ -344,8 +358,6 @@ public:
|
||||
|
||||
private:
|
||||
/// Manual constructors, should only be used by SolverInterface and this class itself.
|
||||
Expression(std::string _name, std::vector<Expression> _arguments, SortPointer _sort):
|
||||
name(std::move(_name)), arguments(std::move(_arguments)), sort(std::move(_sort)) {}
|
||||
Expression(std::string _name, std::vector<Expression> _arguments, Kind _kind):
|
||||
Expression(std::move(_name), std::move(_arguments), std::make_shared<Sort>(_kind)) {}
|
||||
|
||||
|
||||
@ -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()] = {};
|
||||
}
|
||||
|
||||
|
||||
@ -18,10 +18,14 @@
|
||||
|
||||
#include <libsmtutil/Z3Interface.h>
|
||||
|
||||
#include <libsolutil/CommonData.h>
|
||||
#include <libsolutil/CommonIO.h>
|
||||
|
||||
#include <z3_api.h>
|
||||
|
||||
using namespace std;
|
||||
using namespace solidity::smtutil;
|
||||
using namespace solidity::util;
|
||||
|
||||
Z3Interface::Z3Interface():
|
||||
m_solver(m_context)
|
||||
@ -243,6 +247,82 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
|
||||
smtAssert(false, "");
|
||||
}
|
||||
|
||||
Expression Z3Interface::fromZ3Expr(z3::expr const& _expr)
|
||||
{
|
||||
auto sort = fromZ3Sort(_expr.get_sort());
|
||||
if (_expr.is_const() || _expr.is_var())
|
||||
return Expression(_expr.to_string(), {}, sort);
|
||||
|
||||
smtAssert(_expr.is_app(), "");
|
||||
vector<Expression> arguments;
|
||||
for (unsigned i = 0; i < _expr.num_args(); ++i)
|
||||
arguments.push_back(fromZ3Expr(_expr.arg(i)));
|
||||
|
||||
auto kind = _expr.decl().decl_kind();
|
||||
if (_expr.is_ite())
|
||||
return Expression::ite(arguments[0], arguments[1], arguments[2]);
|
||||
else if (_expr.is_not())
|
||||
return !arguments[0];
|
||||
else if (_expr.is_and())
|
||||
return arguments[0] && arguments[1];
|
||||
else if (_expr.is_or())
|
||||
return arguments[0] || arguments[1];
|
||||
else if (_expr.is_implies())
|
||||
return Expression::implies(arguments[0], arguments[1]);
|
||||
else if (_expr.is_eq())
|
||||
return arguments[0] == arguments[1];
|
||||
else if (kind == Z3_OP_ULT || kind == Z3_OP_SLT)
|
||||
return arguments[0] < arguments[1];
|
||||
else if (kind == Z3_OP_ULEQ || kind == Z3_OP_SLEQ)
|
||||
return arguments[0] <= arguments[1];
|
||||
else if (kind == Z3_OP_GT || kind == Z3_OP_SGT)
|
||||
return arguments[0] > arguments[1];
|
||||
else if (kind == Z3_OP_UGEQ || kind == Z3_OP_SGEQ)
|
||||
return arguments[0] >= arguments[1];
|
||||
else if (kind == Z3_OP_ADD)
|
||||
return arguments[0] + arguments[1];
|
||||
else if (kind == Z3_OP_SUB)
|
||||
return arguments[0] - arguments[1];
|
||||
else if (kind == Z3_OP_MUL)
|
||||
return arguments[0] * arguments[1];
|
||||
else if (kind == Z3_OP_DIV)
|
||||
return arguments[0] / arguments[1];
|
||||
else if (kind == Z3_OP_MOD)
|
||||
return arguments[0] % arguments[1];
|
||||
else if (kind == Z3_OP_XOR)
|
||||
return arguments[0] ^ arguments[1];
|
||||
else if (kind == Z3_OP_BSHL)
|
||||
return arguments[0] << arguments[1];
|
||||
else if (kind == Z3_OP_BLSHR)
|
||||
return arguments[0] >> arguments[1];
|
||||
else if (kind == Z3_OP_BASHR)
|
||||
return Expression::ashr(arguments[0], arguments[1]);
|
||||
else if (kind == Z3_OP_INT2BV)
|
||||
smtAssert(false, "");
|
||||
else if (kind == Z3_OP_BV2INT)
|
||||
smtAssert(false, "");
|
||||
else if (kind == Z3_OP_SELECT)
|
||||
return Expression::select(arguments[0], arguments[1]);
|
||||
else if (kind == Z3_OP_STORE)
|
||||
return Expression::store(arguments[0], arguments[1], arguments[2]);
|
||||
else if (kind == Z3_OP_CONST_ARRAY)
|
||||
{
|
||||
auto sortSort = make_shared<SortSort>(fromZ3Sort(_expr.get_sort()));
|
||||
return Expression::const_array(Expression(sortSort), arguments[0]);
|
||||
}
|
||||
else if (kind == Z3_OP_DT_CONSTRUCTOR)
|
||||
{
|
||||
auto sortSort = make_shared<SortSort>(fromZ3Sort(_expr.get_sort()));
|
||||
return Expression::tuple_constructor(Expression(sortSort), arguments);
|
||||
}
|
||||
else if (kind == Z3_OP_DT_ACCESSOR)
|
||||
smtAssert(false, "");
|
||||
else if (kind == Z3_OP_UNINTERPRETED)
|
||||
return Expression(_expr.decl().name().str(), arguments, fromZ3Sort(_expr.get_sort()));
|
||||
|
||||
smtAssert(false, "");
|
||||
}
|
||||
|
||||
z3::sort Z3Interface::z3Sort(Sort const& _sort)
|
||||
{
|
||||
switch (_sort.kind)
|
||||
@ -295,3 +375,35 @@ z3::sort_vector Z3Interface::z3Sort(vector<SortPointer> const& _sorts)
|
||||
z3Sorts.push_back(z3Sort(*_sort));
|
||||
return z3Sorts;
|
||||
}
|
||||
|
||||
SortPointer Z3Interface::fromZ3Sort(z3::sort const& _sort)
|
||||
{
|
||||
if (_sort.is_bool())
|
||||
return SortProvider::boolSort;
|
||||
if (_sort.is_int())
|
||||
return SortProvider::sintSort;
|
||||
if (_sort.is_bv())
|
||||
return make_shared<BitVectorSort>(_sort.bv_size());
|
||||
if (_sort.is_array())
|
||||
return make_shared<ArraySort>(fromZ3Sort(_sort.array_domain()), fromZ3Sort(_sort.array_range()));
|
||||
if (_sort.is_datatype())
|
||||
{
|
||||
auto name = _sort.name().str();
|
||||
auto constructor = z3::func_decl(m_context, Z3_get_tuple_sort_mk_decl(m_context, _sort));
|
||||
vector<string> memberNames;
|
||||
vector<SortPointer> memberSorts;
|
||||
for (unsigned i = 0; i < constructor.arity(); ++i)
|
||||
{
|
||||
auto accessor = z3::func_decl(m_context, Z3_get_tuple_sort_field_decl(m_context, _sort, i));
|
||||
memberNames.push_back(accessor.name().str());
|
||||
memberSorts.push_back(fromZ3Sort(accessor.range()));
|
||||
}
|
||||
return make_shared<TupleSort>(name, memberNames, memberSorts);
|
||||
}
|
||||
smtAssert(false, "");
|
||||
}
|
||||
|
||||
vector<SortPointer> Z3Interface::fromZ3Sort(z3::sort_vector const& _sorts)
|
||||
{
|
||||
return applyMap(_sorts, [this](auto const& sort) { return fromZ3Sort(sort); });
|
||||
}
|
||||
|
||||
@ -41,6 +41,7 @@ public:
|
||||
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
|
||||
|
||||
z3::expr toZ3Expr(Expression const& _expr);
|
||||
smtutil::Expression fromZ3Expr(z3::expr const& _expr);
|
||||
|
||||
std::map<std::string, z3::expr> constants() const { return m_constants; }
|
||||
std::map<std::string, z3::func_decl> functions() const { return m_functions; }
|
||||
@ -56,6 +57,8 @@ private:
|
||||
|
||||
z3::sort z3Sort(Sort const& _sort);
|
||||
z3::sort_vector z3Sort(std::vector<SortPointer> const& _sorts);
|
||||
smtutil::SortPointer fromZ3Sort(z3::sort const& _sort);
|
||||
std::vector<smtutil::SortPointer> fromZ3Sort(z3::sort_vector const& _sorts);
|
||||
|
||||
z3::context m_context;
|
||||
z3::solver m_solver;
|
||||
|
||||
@ -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)
|
||||
|
||||
@ -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);
|
||||
|
||||
@ -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 {};
|
||||
}
|
||||
|
||||
@ -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;
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user