backends/p4tools/common/lib/model.h

/*
 * SPDX-FileCopyrightText: 2022 The P4 Language Consortium
 *
 * SPDX-License-Identifier: Apache-2.0
 */
 
#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_ */