backends/p4tools/common/lib/model.h

#ifndef BACKENDS_P4TOOLS_COMMON_LIB_MODEL_H_
#define BACKENDS_P4TOOLS_COMMON_LIB_MODEL_H_
 
#include <map>
#include <utility>
 
#include "ir/ir.h"
#include "ir/solver.h"
#include "ir/visitor.h"
 
namespace P4::P4Tools {
 
using SymbolicMapType = P4::flat_map<IR::StateVariable, const IR::Expression *>;
 
class Model {
 private:
    SymbolicMapping symbolicMap;
 
    // A visitor that iterates over an input expression and visits all the variables in the input
    // expression. These variables correspond to variables that were used for constraints in model
    // generated by the SMT solver. A variable needs to be
    class SubstVisitor : public Transform {
        const Model &self;
 
        bool doComplete;
 
     public:
        const IR::Literal *preorder(IR::StateVariable *var) override;
        const IR::Literal *preorder(IR::SymbolicVariable *var) override;
        const IR::Literal *preorder(IR::TaintExpression *var) override;
 
        explicit SubstVisitor(const Model &model, bool doComplete);
    };
 
 public:
    // Maps an expression to its value in the model.
    using ExpressionMap = std::map<const IR::Expression *, const IR::Literal *>;
 
    explicit Model(SymbolicMapping symbolicMap) : symbolicMap(std::move(symbolicMap)) {}
 
    Model(const Model &) = default;
    Model(Model &&) = default;
    Model &operator=(const Model &) = default;
    Model &operator=(Model &&) = default;
    ~Model() = default;
 
    const IR::Literal *evaluate(const IR::Expression *expr, bool doComplete,
                                ExpressionMap *resolvedExpressions = nullptr) const;
 
    // Evaluates a P4 StructExpression in the context of this model. Recursively calls into
    // @evaluate and substitutes all members of this list with a Value type.
    const IR::StructExpression *evaluateStructExpr(
        const IR::StructExpression *structExpr, bool doComplete,
        ExpressionMap *resolvedExpressions = nullptr) const;
 
    // Evaluates a P4 BaseListExpression in the context of this model. Recursively calls into
    // @evaluate and substitutes all members of this list with a Value type.
    const IR::BaseListExpression *evaluateListExpr(
        const IR::BaseListExpression *listExpr, bool doComplete,
        ExpressionMap *resolvedExpressions = nullptr) const;
 
    [[nodiscard]] const IR::Expression *get(const IR::SymbolicVariable *var, bool checked) const;
 
    void set(const IR::SymbolicVariable *var, const IR::Expression *val);
 
    void mergeMap(const SymbolicMapping &sourceMap);
 
    [[nodiscard]] const SymbolicMapping &getSymbolicMap() const;
};
 
}  // namespace P4::P4Tools
 
#endif /* BACKENDS_P4TOOLS_COMMON_LIB_MODEL_H_ */