action_constraint_solver.h

 
#ifndef BF_P4C_PHV_SOLVER_ACTION_CONSTRAINT_SOLVER_H_
#define BF_P4C_PHV_SOLVER_ACTION_CONSTRAINT_SOLVER_H_
 
#include <optional>
#include <vector>
 
#include "backends/tofino/bf-p4c/ir/bitrange.h"
#include "backends/tofino/bf-p4c/phv/solver/symbolic_bitvec.h"
#include "lib/bitvec.h"
#include "lib/cstring.h"
#include "lib/ordered_map.h"
 
namespace solver {
 
using namespace P4::literals;
using namespace P4;
 
using ContainerID = cstring;
 
class Instruction {
 public:
    virtual cstring name() const = 0;
    virtual cstring to_cstring() const = 0;
};
 
class DepositField : public Instruction {
 public:
    ContainerID dest;
    ContainerID src1;
    int left_rotate;
    bitvec mask;
    ContainerID src2;
    DepositField(ContainerID dest, ContainerID src1, int left_rotate, bitvec mask, ContainerID src2)
        : dest(dest), src1(src1), left_rotate(left_rotate), mask(mask), src2(src2) {}
    cstring name() const override { return "deposit-field"_cs; };
    cstring to_cstring() const override;
};
 
class BitmaskedSet : public Instruction {
 public:
    ContainerID dest;
    ContainerID src1;
    ContainerID src2;
    bitvec mask;
    BitmaskedSet(ContainerID dest, ContainerID src1, ContainerID src2, bitvec mask)
        : dest(dest), src1(src1), src2(src2), mask(mask) {}
    cstring name() const override { return "bitmasked-set"_cs; };
    cstring to_cstring() const override;
};
 
class ByteRotateMerge : public Instruction {
 public:
    ContainerID dest;
    ContainerID src1;
    int shift1;
    ContainerID src2;
    int shift2;
    bitvec mask;
    ByteRotateMerge(ContainerID dest, ContainerID src1, int shift1, ContainerID src2, int shift2,
                    bitvec mask)
        : dest(dest), src1(src1), shift1(shift1), src2(src2), shift2(shift2), mask(mask) {}
    cstring name() const override { return "byte-rotate-merge"_cs; };
    cstring to_cstring() const override;
};
 
class ContainerSet : public Instruction {
 public:
    ContainerID dest;
    ContainerID src;
    ContainerSet(ContainerID dest, ContainerID src) : dest(dest), src(src) {}
    cstring name() const override { return "set"_cs; };
    cstring to_cstring() const override;
};
 
enum class ErrorCode {
    unsat = 1,
    invalid_input = 2,
    too_many_container_sources = 3,
    too_many_unaligned_sources = 4,
    invalid_for_deposit_field = 5,
    smt_sovler_unknown = 6,
    deposit_src2_must_be_dest = 7,
    non_rot_aligned_and_non_byte_shiftable = 8,
    invalid_whole_container_write = 9,
    dark_container_ad_or_const_source = 10,
};
 
struct Error {
    ErrorCode code;
    cstring msg;
    Error(ErrorCode code, cstring msg) : code(code), msg(msg){};
};
 
struct ContainerSpec {
    int size;
    bitvec live;
};
 
struct Result {
    std::optional<Error> err;
    std::vector<const Instruction *> instructions;
    Result() {}
    explicit Result(const Error &err) : err(err) {}
    explicit Result(const Instruction *inst) : instructions({inst}) {}
    explicit Result(const std::vector<const Instruction *> &instructions)
        : instructions(instructions) {}
    bool ok() { return !err; }
};
 
struct Operand {
    bool is_ad_or_const;
    ContainerID container;
    le_bitrange range;
    bool operator==(const Operand &b) const {
        return is_ad_or_const == b.is_ad_or_const && container == b.container && range == b.range;
    }
    bool operator!=(const Operand &b) const { return !(*this == b); }
};
std::ostream &operator<<(std::ostream &s, const Operand &);
 
Operand make_ad_or_const_operand();
Operand make_container_operand(ContainerID c, le_bitrange r);
 
struct Assign {
    Operand dst;
    Operand src;
};
std::ostream &operator<<(std::ostream &s, const Assign &);
std::ostream &operator<<(std::ostream &s, const std::vector<Assign> &);
 
using RotateClassifiedAssigns = std::map<int, std::vector<Assign>>;
 
class ActionSolverBase {
 protected:
    ordered_map<ContainerID, RotateClassifiedAssigns> dest_assigns_i;
    ordered_map<ContainerID, ContainerSpec> specs_i;
    ordered_map<ContainerID, bitvec> src_unallocated_bits;
    bool enable_bitmasked_set_i = true;
 
 protected:
    std::optional<Error> validate_input() const;
 
    Result try_container_set(const ContainerID dest,
                             const RotateClassifiedAssigns &offset_assigns) const;
 
    std::optional<Error> check_whole_container_set_with_none_source_allocated() const;
 
 public:
    void enable_bitmasked_set(bool enable) { enable_bitmasked_set_i = enable; }
 
    virtual void add_assign(const Operand &dst, Operand src);
 
    virtual void add_src_unallocated_assign(const ContainerID &c, const le_bitrange &range);
 
    virtual void set_container_spec(ContainerID id, int size, bitvec live);
 
    virtual Result solve() = 0;
 
    virtual void clear() {
        dest_assigns_i.clear();
        specs_i.clear();
        src_unallocated_bits.clear();
        enable_bitmasked_set_i = true;
    }
};
 
class ActionMoveSolver : public ActionSolverBase {
 private:
    // check whether @p bv_dest satifies all assignments.
    std::optional<Error> dest_meet_expectation(const ContainerID dest,
                                               const std::vector<Assign> &src1,
                                               const std::vector<Assign> &src2,
                                               const symbolic_bitvec::BitVec &bv_dest,
                                               const symbolic_bitvec::BitVec &bv_src1,
                                               const symbolic_bitvec::BitVec &bv_src2) const;
 
    Result run_deposit_field_symbolic_bitvec_solver(const ContainerID dest,
                                                    const std::vector<Assign> &src1,
                                                    const std::vector<Assign> &src2) const;
 
    Result run_deposit_field_solver(const ContainerID dest, const std::vector<Assign> &src1,
                                    const std::vector<Assign> &src2) const;
 
    Result try_deposit_field(const ContainerID dest, const RotateClassifiedAssigns &assigns) const;
 
    Result run_byte_rotate_merge_symbolic_bitvec_solver(const ContainerID dest,
                                                        const std::vector<Assign> &src1,
                                                        const std::vector<Assign> &src2) const;
 
    Result run_byte_rotate_merge_solver(const ContainerID dest, const std::vector<Assign> &src1,
                                        const std::vector<Assign> &src2) const;
 
    Result try_byte_rotate_merge(const ContainerID dest,
                                 const RotateClassifiedAssigns &assigns) const;
 
    Result try_bitmasked_set(const ContainerID dest, const RotateClassifiedAssigns &assigns) const;
 
    const RotateClassifiedAssigns *apply_unallocated_src_optimization(
        const ContainerID dest, const RotateClassifiedAssigns &offset_assigns);
 
 public:
    Result solve() override;
};
 
class ActionMochaSolver : public ActionSolverBase {
 public:
    ActionMochaSolver(){};
    Result solve() override;
};
 
class ActionDarkSolver : public ActionSolverBase {
 public:
    ActionDarkSolver(){};
    Result solve() override;
};
 
}  // namespace solver
 
#endif /* BF_P4C_PHV_SOLVER_ACTION_CONSTRAINT_SOLVER_H_ */