z3_solver.h

#ifndef BACKENDS_P4TOOLS_COMMON_CORE_Z3_SOLVER_H_
#define BACKENDS_P4TOOLS_COMMON_CORE_Z3_SOLVER_H_
 
#include <z3++.h>
#include <z3.h>
 
#include <cstddef>
#include <iosfwd>
#include <optional>
#include <string>
#include <vector>
 
#include "ir/ir.h"
#include "ir/json_generator.h"
#include "ir/solver.h"
#include "lib/cstring.h"
#include "lib/ordered_map.h"
#include "lib/rtti.h"
#include "lib/safe_vector.h"
 
namespace P4::P4Tools {
 
using Z3DeclaredVariablesMap = std::vector<ordered_map<unsigned, const IR::SymbolicVariable *>>;
 
class Z3Solver : public AbstractSolver {
    friend class Z3Translator;
    friend class Z3JSON;
    friend class Z3SolverAccessor;
 
 public:
    ~Z3Solver() override = default;
 
    explicit Z3Solver(bool isIncremental = true,
                      std::optional<std::istream *> inOpt = std::nullopt);
 
    void comment(cstring comment) override;
 
    void seed(unsigned seed) override;
 
    void timeout(unsigned tm) override;
 
    std::optional<bool> checkSat(const std::vector<const Constraint *> &asserts) override;
 
    std::optional<bool> checkSat(const z3::expr_vector &asserts);
 
    std::optional<bool> checkSat();
 
    [[nodiscard]] const SymbolicMapping &getSymbolicMapping() const override;
 
    void toJSON(JSONGenerator & /*json*/) const override;
 
    [[nodiscard]] bool isInIncrementalMode() const override;
 
    [[nodiscard]] const z3::solver &getZ3Solver() const;
 
    [[nodiscard]] const z3::context &getZ3Ctx() const;
 
    [[nodiscard]] safe_vector<const Constraint *> getAssertions() const;
 
    void reset();
 
    void push();
 
    void pop();
 
    void clearMemory();
 
    void asrt(const z3::expr &assert);
 
    void asrt(const Constraint *assertion);
 
 private:
    z3::sort toSort(const IR::Type *type);
 
    [[nodiscard]] z3::context &ctx() const;
 
    z3::expr declareVar(const IR::SymbolicVariable &var);
 
    [[nodiscard]] static std::string generateName(const IR::SymbolicVariable &var);
 
    static const IR::Literal *toLiteral(const z3::expr &e, const IR::Type *type);
 
    //             that is greater than or equal to @asrtIndex.
    void addZ3Pushes(size_t &chkIndex, size_t asrtIndex);
 
    static std::optional<bool> interpretSolverResult(z3::check_result result);
 
    z3::solver z3solver;
 
    Z3DeclaredVariablesMap declaredVarsById;
 
    safe_vector<const Constraint *> p4Assertions;
 
    bool isIncremental;
 
    std::vector<size_t> checkpoints;
 
    z3::expr_vector z3Assertions;
 
    std::optional<unsigned> seed_;
 
    std::optional<unsigned> timeout_;
 
    DECLARE_TYPEINFO(Z3Solver, AbstractSolver);
};
 
class Z3Translator : public virtual Inspector {
 public:
    explicit Z3Translator(Z3Solver &solver);
 
    bool preorder(const IR::Node *node) override;
 
    bool preorder(const IR::Cast *cast) override;
 
    bool preorder(const IR::Constant *constant) override;
    bool preorder(const IR::BoolLiteral *boolLiteral) override;
    bool preorder(const IR::StringLiteral *stringLiteral) override;
 
    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;
 
    z3::expr getResult();
 
    z3::expr translate(const IR::Expression *expression);
 
 private:
    using Z3UnaryOp = z3::expr (*)(const z3::expr &);
 
    using Z3BinaryOp = z3::expr (*)(const z3::expr &, const z3::expr &);
 
    using Z3TernaryOp = z3::expr (*)(const z3::expr &, const z3::expr &, const z3::expr &);
 
    bool recurseUnary(const IR::Operation_Unary *unary, Z3UnaryOp f);
 
    bool recurseBinary(const IR::Operation_Binary *binary, Z3BinaryOp f);
 
    bool recurseTernary(const IR::Operation_Ternary *ternary, Z3TernaryOp f);
 
    template <class ShiftType>
    const ShiftType *rewriteShift(const ShiftType *shift) const;
 
    z3::expr result;
 
    std::reference_wrapper<Z3Solver> solver;
};
 
}  // namespace P4::P4Tools
 
#endif /* BACKENDS_P4TOOLS_COMMON_CORE_Z3_SOLVER_H_ */