From 55cd213383be3ee7ab216ff0352444756f07e34d Mon Sep 17 00:00:00 2001 From: fruffy Date: Sat, 6 Jan 2024 09:57:04 +0100 Subject: [PATCH] Open up the Z3 api. --- backends/p4tools/common/core/z3_solver.cpp | 187 +++++++-------------- backends/p4tools/common/core/z3_solver.h | 114 ++++++++++++- 2 files changed, 172 insertions(+), 129 deletions(-) diff --git a/backends/p4tools/common/core/z3_solver.cpp b/backends/p4tools/common/core/z3_solver.cpp index ff67f2c876..773977e889 100644 --- a/backends/p4tools/common/core/z3_solver.cpp +++ b/backends/p4tools/common/core/z3_solver.cpp @@ -1,5 +1,6 @@ #include "backends/p4tools/common/core/z3_solver.h" +#include #include #include @@ -49,101 +50,6 @@ const char *toString(z3::model m) { return Z3_model_to_string(m.ctx(), m); } #define Z3_LOG(...) #endif // NDEBUG -/// Translates P4 expressions into Z3. Any variables encountered are declared to a Z3 instance. -class Z3Translator : public virtual Inspector { - public: - /// Creates a Z3 translator. Any variables encountered during translation will be declared to - /// the Z3 instance encapsulated within the given solver. - explicit Z3Translator(Z3Solver &solver); - - /// Handles unexpected nodes. - bool preorder(const IR::Node *node) override; - - /// Translates casts. - bool preorder(const IR::Cast *cast) override; - - /// Translates constants. - bool preorder(const IR::Constant *constant) override; - bool preorder(const IR::BoolLiteral *boolLiteral) override; - bool preorder(const IR::StringLiteral *stringLiteral) override; - - /// Translates variables. - bool preorder(const IR::SymbolicVariable *var) override; - - // Translations for unary operations. - bool preorder(const IR::Neg *op) override; - bool preorder(const IR::Cmpl *op) override; - bool preorder(const IR::LNot *op) override; - - // Translations for binary operations. - bool preorder(const IR::Equ *op) override; - bool preorder(const IR::Neq *op) override; - bool preorder(const IR::Lss *op) override; - bool preorder(const IR::Leq *op) override; - bool preorder(const IR::Grt *op) override; - bool preorder(const IR::Geq *op) override; - bool preorder(const IR::Mod *op) override; - bool preorder(const IR::Add *op) override; - bool preorder(const IR::Sub *op) override; - bool preorder(const IR::Mul *op) override; - bool preorder(const IR::Div *op) override; - bool preorder(const IR::Shl *op) override; - bool preorder(const IR::Shr *op) override; - bool preorder(const IR::BAnd *op) override; - bool preorder(const IR::BOr *op) override; - bool preorder(const IR::BXor *op) override; - bool preorder(const IR::LAnd *op) override; - bool preorder(const IR::LOr *op) override; - bool preorder(const IR::Concat *op) override; - - // Translations for ternary operations. - bool preorder(const IR::Mux *op) override; - bool preorder(const IR::Slice *op) override; - - /// @returns the result of the translation. - z3::expr getResult() { return result; } - - private: - /// Function type for a unary operator. - using Z3UnaryOp = z3::expr (*)(const z3::expr &); - - /// Function type for a binary operator. - using Z3BinaryOp = z3::expr (*)(const z3::expr &, const z3::expr &); - - /// Function type for a ternary operator. - using Z3TernaryOp = z3::expr (*)(const z3::expr &, const z3::expr &, const z3::expr &); - - /// Handles recursion into unary operations. - /// - /// @returns false. - bool recurseUnary(const IR::Operation_Unary *unary, Z3UnaryOp f); - - /// Handles recursion into binary operations. - /// - /// @returns false. - bool recurseBinary(const IR::Operation_Binary *binary, Z3BinaryOp f); - - /// Handles recursion into ternary operations. - /// - /// @returns false. - bool recurseTernary(const IR::Operation_Ternary *ternary, Z3TernaryOp f); - - /// Rewrites a shift operation so that the type of the shift amount matches that of the number - /// being shifted. - /// - /// P4 allows shift operands to have different types: when the number being shifted is a bit - /// vector, the shift amount can be an infinite-precision integer. This rewrites such - /// expressions so that the shift amount is a bit vector. - template - const ShiftType *rewriteShift(const ShiftType *shift) const; - - /// The output of the translation. - z3::expr result; - - /// The Z3 solver instance, to which variables will be declared as they are encountered. - Z3Solver &solver; -}; - z3::sort Z3Solver::toSort(const IR::Type *type) { BUG_CHECK(type, "Z3Solver::toSort with empty pointer"); @@ -262,6 +168,31 @@ void Z3Solver::timeout(unsigned tm) { timeout_ = tm; } +std::optional Z3Solver::interpretSolverResult(z3::check_result result) { + switch (result) { + case z3::sat: + Z3_LOG("result:%s", "sat"); + return true; + case z3::unsat: + Z3_LOG("result:%s", "unsat"); + return false; + + default: // unknown + Z3_LOG("result:%s", "unknown"); + return std::nullopt; + } +} + +std::optional Z3Solver::checkSat() { + Util::ScopedTimer ctCheckSat("checkSat"); + return interpretSolverResult(z3solver.check()); +} + +std::optional Z3Solver::checkSat(const z3::expr_vector &asserts) { + Util::ScopedTimer ctCheckSat("checkSat"); + return interpretSolverResult(z3solver.check(asserts)); +} + std::optional Z3Solver::checkSat(const std::vector &asserts) { Util::ScopedTimer ctZ3("z3"); if (isIncremental) { @@ -285,38 +216,27 @@ std::optional Z3Solver::checkSat(const std::vector &as } Z3_LOG("checking satisfiability for %d assertions", isIncremental ? z3solver.assertions().size() : z3Assertions.size()); - Util::ScopedTimer ctCheckSat("checkSat"); - z3::check_result result = isIncremental ? z3solver.check() : z3solver.check(z3Assertions); - switch (result) { - case z3::sat: - Z3_LOG("result:%s", "sat"); - return true; - case z3::unsat: - Z3_LOG("result:%s", "unsat"); - return false; - - default: // unknown - Z3_LOG("result:%s", "unknown"); - return std::nullopt; - } + return isIncremental ? checkSat() : checkSat(z3Assertions); } void Z3Solver::asrt(const Constraint *assertion) { CHECK_NULL(assertion); - try { - Z3Translator z3translator(*this); - assertion->apply(z3translator); - auto expr = z3translator.getResult(); + Z3Translator z3translator(*this); + auto expr = z3translator.translate(assertion); + asrt(expr); + p4Assertions.push_back(assertion); + BUG_CHECK(isIncremental || z3Assertions.size() == p4Assertions.size(), + "Number of assertion in P4 and Z3 formats aren't equal"); +} - Z3_LOG("add assertion '%s'", toString(expr)); +void Z3Solver::asrt(const z3::expr &assertion) { + try { + Z3_LOG("add assertion '%s'", toString(assertion)); if (isIncremental) { - z3solver.add(expr); + z3solver.add(assertion); } else { - z3Assertions.push_back(expr); + z3Assertions.push_back(assertion); } - p4Assertions.push_back(assertion); - BUG_CHECK(isIncremental || z3Assertions.size() == p4Assertions.size(), - "Number of assertion in P4 and Z3 formats aren't equal"); } catch (z3::exception &e) { BUG("Z3Solver: Z3 exception: %1%\nAssertion %2%", e.msg(), assertion); } @@ -471,8 +391,8 @@ bool Z3Translator::preorder(const IR::Cast *cast) { exprSize = exprType->width_bits(); } else if (castExtrType->is()) { exprSize = 1; - auto trueVal = solver.ctx().bv_val(1, exprSize); - auto falseVal = solver.ctx().bv_val(0, exprSize); + auto trueVal = solver.get().ctx().bv_val(1, exprSize); + auto falseVal = solver.get().ctx().bv_val(0, exprSize); castExpr = z3::ite(castExpr, trueVal, falseVal); } else if (const auto *exprType = castExtrType->to()) { exprSize = exprType->width_bits(); @@ -496,7 +416,7 @@ bool Z3Translator::preorder(const IR::Cast *cast) { if (cast->destType->is()) { if (const auto *exprType = castExtrType->to()) { if (exprType->width_bits() == 1) { - castExpr = z3::operator==(castExpr, solver.ctx().bv_val(1, 1)); + castExpr = z3::operator==(castExpr, solver.get().ctx().bv_val(1, 1)); } else { BUG("Cast expression type %1% is not bit<1> : %2%", exprType, castExpr); } @@ -514,18 +434,18 @@ bool Z3Translator::preorder(const IR::Cast *cast) { bool Z3Translator::preorder(const IR::Constant *constant) { // Handle infinite-integer constants. if (constant->type->is()) { - result = solver.ctx().int_val(constant->value.str().c_str()); + result = solver.get().ctx().int_val(constant->value.str().c_str()); return false; } // Handle bit constants. if (const auto *bits = constant->type->to()) { - result = solver.ctx().bv_val(constant->value.str().c_str(), bits->size); + result = solver.get().ctx().bv_val(constant->value.str().c_str(), bits->size); return false; } if (const auto *bits = constant->type->to()) { - result = solver.ctx().bv_val(constant->value.str().c_str(), bits->width_bits()); + result = solver.get().ctx().bv_val(constant->value.str().c_str(), bits->width_bits()); return false; } @@ -533,17 +453,17 @@ bool Z3Translator::preorder(const IR::Constant *constant) { } bool Z3Translator::preorder(const IR::BoolLiteral *boolLiteral) { - result = solver.ctx().bool_val(boolLiteral->value); + result = solver.get().ctx().bool_val(boolLiteral->value); return false; } bool Z3Translator::preorder(const IR::StringLiteral *stringLiteral) { - result = solver.ctx().string_val(stringLiteral->value); + result = solver.get().ctx().string_val(stringLiteral->value); return false; } bool Z3Translator::preorder(const IR::SymbolicVariable *var) { - result = solver.declareVar(*var); + result = solver.get().declareVar(*var); return false; } @@ -694,4 +614,15 @@ bool Z3Translator::recurseTernary(const IR::Operation_Ternary *ternary, Z3Ternar return false; } +z3::expr Z3Translator::getResult() { return result; } + +z3::expr Z3Translator::translate(const IR::Expression *expression) { + try { + expression->apply(*this); + } catch (z3::exception &e) { + BUG("Z3Translator: Z3 exception: %1%\nExpression %2%", e.msg(), expression); + } + return result; +} + } // namespace P4Tools diff --git a/backends/p4tools/common/core/z3_solver.h b/backends/p4tools/common/core/z3_solver.h index b406d82b26..5f73a2493d 100644 --- a/backends/p4tools/common/core/z3_solver.h +++ b/backends/p4tools/common/core/z3_solver.h @@ -44,6 +44,14 @@ class Z3Solver : public AbstractSolver { std::optional checkSat(const std::vector &asserts) override; + /// Z3Solver specific checkSat function. Calls check on the input z3::expr_vector. + /// Only relies on the incrementality mode of the Z3 solver. + std::optional checkSat(const z3::expr_vector &asserts); + + /// Z3Solver specific checkSat function. Calls check on the solver. + /// Only useful in incremental mode. + std::optional checkSat(); + [[nodiscard]] const SymbolicMapping &getSymbolicMapping() const override; void toJSON(JSONGenerator & /*json*/) const override; @@ -73,10 +81,13 @@ class Z3Solver : public AbstractSolver { /// In incremental state, all active assertions are reapplied after resetting. void clearMemory(); - private: + /// Adds a Z3 assertion to the solver context. + void asrt(const z3::expr &assert); + /// Inserts an assertion into the topmost solver context. void asrt(const Constraint *assertion); + private: /// Converts a P4 type to a Z3 sort. z3::sort toSort(const IR::Type *type); @@ -102,6 +113,9 @@ class Z3Solver : public AbstractSolver { /// Helps to restore a state of incremental solver in a constructor. void addZ3Pushes(size_t &chkIndex, size_t asrtIndex); + /// Helper function which converts a z3::check_result to a std::optional. + static std::optional interpretSolverResult(z3::check_result result); + /// The underlying Z3 instance. z3::solver z3solver; @@ -132,6 +146,104 @@ class Z3Solver : public AbstractSolver { DECLARE_TYPEINFO(Z3Solver, AbstractSolver); }; +/// Translates P4 expressions into Z3. Any variables encountered are declared to a Z3 instance. +class Z3Translator : public virtual Inspector { + public: + /// Creates a Z3 translator. Any variables encountered during translation will be declared to + /// the Z3 instance encapsulated within the given solver. + explicit Z3Translator(Z3Solver &solver); + + /// Handles unexpected nodes. + bool preorder(const IR::Node *node) override; + + /// Translates casts. + bool preorder(const IR::Cast *cast) override; + + /// Translates constants. + bool preorder(const IR::Constant *constant) override; + bool preorder(const IR::BoolLiteral *boolLiteral) override; + bool preorder(const IR::StringLiteral *stringLiteral) override; + + /// Translates variables. + bool preorder(const IR::SymbolicVariable *var) override; + + // Translations for unary operations. + bool preorder(const IR::Neg *op) override; + bool preorder(const IR::Cmpl *op) override; + bool preorder(const IR::LNot *op) override; + + // Translations for binary operations. + bool preorder(const IR::Equ *op) override; + bool preorder(const IR::Neq *op) override; + bool preorder(const IR::Lss *op) override; + bool preorder(const IR::Leq *op) override; + bool preorder(const IR::Grt *op) override; + bool preorder(const IR::Geq *op) override; + bool preorder(const IR::Mod *op) override; + bool preorder(const IR::Add *op) override; + bool preorder(const IR::Sub *op) override; + bool preorder(const IR::Mul *op) override; + bool preorder(const IR::Div *op) override; + bool preorder(const IR::Shl *op) override; + bool preorder(const IR::Shr *op) override; + bool preorder(const IR::BAnd *op) override; + bool preorder(const IR::BOr *op) override; + bool preorder(const IR::BXor *op) override; + bool preorder(const IR::LAnd *op) override; + bool preorder(const IR::LOr *op) override; + bool preorder(const IR::Concat *op) override; + + // Translations for ternary operations. + bool preorder(const IR::Mux *op) override; + bool preorder(const IR::Slice *op) override; + + /// @returns the result of the translation. + z3::expr getResult(); + + /// Translate an P4C IR expression and return the Z3 equivalent. + z3::expr translate(const IR::Expression *expression); + + private: + /// Function type for a unary operator. + using Z3UnaryOp = z3::expr (*)(const z3::expr &); + + /// Function type for a binary operator. + using Z3BinaryOp = z3::expr (*)(const z3::expr &, const z3::expr &); + + /// Function type for a ternary operator. + using Z3TernaryOp = z3::expr (*)(const z3::expr &, const z3::expr &, const z3::expr &); + + /// Handles recursion into unary operations. + /// + /// @returns false. + bool recurseUnary(const IR::Operation_Unary *unary, Z3UnaryOp f); + + /// Handles recursion into binary operations. + /// + /// @returns false. + bool recurseBinary(const IR::Operation_Binary *binary, Z3BinaryOp f); + + /// Handles recursion into ternary operations. + /// + /// @returns false. + bool recurseTernary(const IR::Operation_Ternary *ternary, Z3TernaryOp f); + + /// Rewrites a shift operation so that the type of the shift amount matches that of the number + /// being shifted. + /// + /// P4 allows shift operands to have different types: when the number being shifted is a bit + /// vector, the shift amount can be an infinite-precision integer. This rewrites such + /// expressions so that the shift amount is a bit vector. + template + const ShiftType *rewriteShift(const ShiftType *shift) const; + + /// The output of the translation. + z3::expr result; + + /// The Z3 solver instance, to which variables will be declared as they are encountered. + std::reference_wrapper solver; +}; + } // namespace P4Tools #endif /* BACKENDS_P4TOOLS_COMMON_CORE_Z3_SOLVER_H_ */