targets/bmv2/concolic.h

#ifndef BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_BMV2_CONCOLIC_H_
#define BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_BMV2_CONCOLIC_H_
 
#include <cstddef>
#include <functional>
#include <vector>
 
#include "backends/p4tools/common/lib/model.h"
#include "ir/ir.h"
#include "lib/big_int_util.h"
 
#include "backends/p4tools/modules/testgen/lib/concolic.h"
 
namespace P4::P4Tools::P4Testgen::Bmv2 {
 
enum class Bmv2HashAlgorithm {
    crc32,
    crc32_custom,
    crc16,
    crc16_custom,
    random,
    identity,
    csum16,
    xor16
};
 
std::ostream &operator<<(std::ostream &os, Bmv2HashAlgorithm algo);
 
class Bmv2Concolic : public Concolic {
 private:
    static constexpr int CHUNK_SIZE = 8;

    static const ConcolicMethodImpls::ImplList BMV2_CONCOLIC_METHOD_IMPLS;

    static big_int computeChecksum(const std::vector<const IR::Expression *> &exprList,
                                   const Model &finalModel, Bmv2HashAlgorithm algo,
                                   Model::ExpressionMap *resolvedExpressions);

    static const IR::Expression *setAndComputePayload(
        const Model &finalModel, ConcolicVariableMap *resolvedConcolicVariables, int payloadSize);
 
 public:
    static const ConcolicMethodImpls::ImplList *getBmv2ConcolicMethodImpls();
};
 
}  // namespace P4::P4Tools::P4Testgen::Bmv2
 
#endif /* BACKENDS_P4TOOLS_MODULES_TESTGEN_TARGETS_BMV2_CONCOLIC_H_ */