diff --git a/libsmtutil/CHCSolverInterface.h b/libsmtutil/CHCSolverInterface.h index 1fe279a8b..c088f3d0f 100644 --- a/libsmtutil/CHCSolverInterface.h +++ b/libsmtutil/CHCSolverInterface.h @@ -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>; + using CexNode = Expression; struct CexGraph { std::map nodes; diff --git a/libsmtutil/SolverInterface.h b/libsmtutil/SolverInterface.h index 314039260..8ea0c5250 100644 --- a/libsmtutil/SolverInterface.h +++ b/libsmtutil/SolverInterface.h @@ -60,6 +60,8 @@ class Expression public: explicit Expression(bool _v): Expression(_v ? "true" : "false", Kind::Bool) {} explicit Expression(std::shared_ptr _sort, std::string _name = ""): Expression(std::move(_name), {}, _sort) {} + explicit Expression(std::string _name, std::vector _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 _arguments, SortPointer _sort): - name(std::move(_name)), arguments(std::move(_arguments)), sort(std::move(_sort)) {} Expression(std::string _name, std::vector _arguments, Kind _kind): Expression(std::move(_name), std::move(_arguments), std::make_shared(_kind)) {} diff --git a/libsmtutil/Z3CHCInterface.cpp b/libsmtutil/Z3CHCInterface.cpp index 35b3556d9..e2b933b68 100644 --- a/libsmtutil/Z3CHCInterface.cpp +++ b/libsmtutil/Z3CHCInterface.cpp @@ -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 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()] = {}; } diff --git a/libsmtutil/Z3Interface.cpp b/libsmtutil/Z3Interface.cpp index 89d378fe1..cfef7db72 100644 --- a/libsmtutil/Z3Interface.cpp +++ b/libsmtutil/Z3Interface.cpp @@ -18,10 +18,14 @@ #include +#include #include +#include + 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 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(fromZ3Sort(_expr.get_sort())); + return Expression::const_array(Expression(sortSort), arguments[0]); + } + else if (kind == Z3_OP_DT_CONSTRUCTOR) + { + auto sortSort = make_shared(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 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(_sort.bv_size()); + if (_sort.is_array()) + return make_shared(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 memberNames; + vector 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(name, memberNames, memberSorts); + } + smtAssert(false, ""); +} + +vector Z3Interface::fromZ3Sort(z3::sort_vector const& _sorts) +{ + return applyMap(_sorts, [this](auto const& sort) { return fromZ3Sort(sort); }); +} diff --git a/libsmtutil/Z3Interface.h b/libsmtutil/Z3Interface.h index a44bfafcd..487723416 100644 --- a/libsmtutil/Z3Interface.h +++ b/libsmtutil/Z3Interface.h @@ -41,6 +41,7 @@ public: std::pair> check(std::vector const& _expressionsToEvaluate) override; z3::expr toZ3Expr(Expression const& _expr); + smtutil::Expression fromZ3Expr(z3::expr const& _expr); std::map constants() const { return m_constants; } std::map functions() const { return m_functions; } @@ -56,6 +57,8 @@ private: z3::sort z3Sort(Sort const& _sort); z3::sort_vector z3Sort(std::vector const& _sorts); + smtutil::SortPointer fromZ3Sort(z3::sort const& _sort); + std::vector fromZ3Sort(z3::sort_vector const& _sorts); z3::context m_context; z3::solver m_solver; diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 7bedc8a65..e10785093 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -1306,7 +1306,7 @@ optional CHC::generateCounterexample(CHCSolverInterface::CexGraph const& { optional rootId; for (auto const& [id, node]: _graph.nodes) - if (node.first == _root) + if (node.name == _root) { rootId = id; break; @@ -1330,18 +1330,18 @@ optional 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 summaryArgs = _graph.nodes.at(summaryId).arguments; FunctionDefinition const* calledFun = summaryPredicate->programFunction(); ContractDefinition const* calledContract = summaryPredicate->programContract(); @@ -1387,7 +1387,7 @@ optional 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 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) diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 0bae37084..8d801ccb8 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -203,7 +203,7 @@ private: /// @returns a set of pairs _var = _value separated by _separator. template - std::string formatVariableModel(std::vector const& _variables, std::vector const& _values, std::string const& _separator) const + std::string formatVariableModel(std::vector const& _variables, std::vector> 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); diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp index b1fa9b19d..d3deaa141 100644 --- a/libsolidity/formal/Predicate.cpp +++ b/libsolidity/formal/Predicate.cpp @@ -149,7 +149,7 @@ bool Predicate::isInterface() const return functor().name.rfind("interface", 0) == 0; } -string Predicate::formatSummaryCall(vector const& _args) const +string Predicate::formatSummaryCall(vector const& _args) const { if (programContract()) return "constructor()"; @@ -163,18 +163,22 @@ string Predicate::formatSummaryCall(vector 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::const_iterator first = _args.begin() + 5 + static_cast(stateVars->size()); - vector::const_iterator last = first + static_cast(fun->parameters().size()); + auto first = _args.begin() + 5 + static_cast(stateVars->size()); + auto last = first + static_cast(fun->parameters().size()); solAssert(first >= _args.begin() && first <= _args.end(), ""); solAssert(last >= _args.begin() && last <= _args.end(), ""); - vector functionArgsCex(first, last); + auto inTypes = FunctionType(*fun).parameterTypes(); + vector> functionArgsCex = formatExpressions(vector(first, last), inTypes); vector 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 const& _args) const } -vector Predicate::summaryStateValues(vector const& _args) const +vector> Predicate::summaryStateValues(vector 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 Predicate::summaryStateValues(vector const& _args) const auto stateVars = stateVariables(); solAssert(stateVars.has_value(), ""); - vector::const_iterator stateFirst; - vector::const_iterator stateLast; + vector::const_iterator stateFirst; + vector::const_iterator stateLast; if (auto const* function = programFunction()) { stateFirst = _args.begin() + 5 + static_cast(stateVars->size()) + static_cast(function->parameters().size()) + 1; @@ -212,12 +216,13 @@ vector Predicate::summaryStateValues(vector const& _args) const solAssert(stateFirst >= _args.begin() && stateFirst <= _args.end(), ""); solAssert(stateLast >= _args.begin() && stateLast <= _args.end(), ""); - vector stateArgs(stateFirst, stateLast); + vector 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 Predicate::summaryPostInputValues(vector const& _args) const +vector> Predicate::summaryPostInputValues(vector 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 Predicate::summaryPostInputValues(vector const& _args) co auto const& inParams = function->parameters(); - vector::const_iterator first = _args.begin() + 5 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) + 1; - vector::const_iterator last = first + static_cast(inParams.size()); + auto first = _args.begin() + 5 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) + 1; + auto last = first + static_cast(inParams.size()); solAssert(first >= _args.begin() && first <= _args.end(), ""); solAssert(last >= _args.begin() && last <= _args.end(), ""); - vector inValues(first, last); + vector inValues(first, last); solAssert(inValues.size() == inParams.size(), ""); - return inValues; + auto inTypes = FunctionType(*function).parameterTypes(); + return formatExpressions(inValues, inTypes); } -vector Predicate::summaryPostOutputValues(vector const& _args) const +vector> Predicate::summaryPostOutputValues(vector 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 Predicate::summaryPostOutputValues(vector const& _args) c auto const& inParams = function->parameters(); - vector::const_iterator first = _args.begin() + 5 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) * 2 + 1; + auto first = _args.begin() + 5 + static_cast(stateVars->size()) * 2 + static_cast(inParams.size()) * 2 + 1; solAssert(first >= _args.begin() && first <= _args.end(), ""); - vector outValues(first, _args.end()); + vector outValues(first, _args.end()); solAssert(outValues.size() == function->returnParameters().size(), ""); - return outValues; + auto outTypes = FunctionType(*function).returnParameterTypes(); + return formatExpressions(outValues, outTypes); +} + +vector> Predicate::formatExpressions(vector const& _exprs, vector const& _types) const +{ + solAssert(_exprs.size() == _types.size(), ""); + vector> strExprs; + for (unsigned i = 0; i < _exprs.size(); ++i) + strExprs.push_back(expressionToString(_exprs.at(i), _types.at(i))); + return strExprs; +} + +optional 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 {}; } diff --git a/libsolidity/formal/Predicate.h b/libsolidity/formal/Predicate.h index a87e81afa..9a05c3008 100644 --- a/libsolidity/formal/Predicate.h +++ b/libsolidity/formal/Predicate.h @@ -107,21 +107,27 @@ public: /// @returns a formatted string representing a call to this predicate /// with _args. - std::string formatSummaryCall(std::vector const& _args) const; + std::string formatSummaryCall(std::vector const& _args) const; /// @returns the values of the state variables from _args at the point /// where this summary was reached. - std::vector summaryStateValues(std::vector const& _args) const; + std::vector> summaryStateValues(std::vector const& _args) const; /// @returns the values of the function input variables from _args at the point /// where this summary was reached. - std::vector summaryPostInputValues(std::vector const& _args) const; + std::vector> summaryPostInputValues(std::vector const& _args) const; /// @returns the values of the function output variables from _args at the point /// where this summary was reached. - std::vector summaryPostOutputValues(std::vector const& _args) const; + std::vector> summaryPostOutputValues(std::vector const& _args) const; private: + /// @returns the formatted version of the given SMT expressions. Those expressions must be SMT constants. + std::vector> formatExpressions(std::vector const& _exprs, std::vector const& _types) const; + + /// @returns a string representation of the SMT expression based on a Solidity type. + std::optional expressionToString(smtutil::Expression const& _expr, TypePointer _type) const; + /// The actual SMT expression. smt::SymbolicFunctionVariable m_predicate;