[P4Testgen] Open up P4Testgen interface. (#4014)

* Open up the P4Testgen interface.

* Remove getPortNumWidthBits from the target and replace it with target-specific constants.

* Clean up library management and namespaces and make sure that the final state class can be moved.

.github/CODEOWNERS

@@ -1,3 +1,3 @@
 # The P4Tools repository is owned by the following maintainers.
-backends/p4tools @fruffy @pkotikal @jnfoster @mbudiu-vmw
+backends/p4tools @fruffy @pkotikal @jnfoster
 

backends/p4tools/modules/testgen/CMakeLists.txt

@@ -77,8 +77,8 @@ FetchContent_MakeAvailable(inja)
 # Testgen libraries.
 set(
   TESTGEN_LIBS
-  p4tools-common
-  inja
+  PRIVATE p4tools-common
+  PUBLIC inja
 )
 
 file(GLOB testgen_targets RELATIVE ${CMAKE_CURRENT_SOURCE_DIR}/targets ${CMAKE_CURRENT_SOURCE_DIR}/targets/*)
@@ -114,15 +114,17 @@ configure_file(register.h.in register.h)
 # The library.
 add_p4tools_library(testgen ${TESTGEN_SOURCES})
 # Make sure the testgen library and anything that links to it see both the Z3 and Inja includes.
-# also links to Z3 and inja
 target_link_libraries(testgen PUBLIC p4tools-common inja)
 
 # The executable.
 add_p4tools_executable(p4testgen main.cpp)
 target_link_libraries(
   p4testgen
-  testgen
+  PRIVATE testgen
   ${TESTGEN_LIBS}
+  ${P4C_LIBRARIES}
+  ${P4C_LIB_DEPS}
+  ${CMAKE_THREAD_LIBS_INIT}
 )
 
 add_custom_target(
@@ -148,6 +150,9 @@ if(ENABLE_GTESTS)
     PRIVATE testgen
     PRIVATE gtest
     ${TESTGEN_LIBS}
+    ${P4C_LIBRARIES}
+    ${P4C_LIB_DEPS}
+    ${CMAKE_THREAD_LIBS_INIT}
   )
 
   if(ENABLE_TESTING)

backends/p4tools/modules/testgen/core/target.cpp

@@ -38,12 +38,9 @@ const ProgramInfo *TestgenTarget::initProgramImpl(const IR::P4Program *program)
 
 const TestgenTarget &TestgenTarget::get() { return Target::get<TestgenTarget>("testgen"); }
 
-int TestgenTarget::getPortNumWidthBits() { return get().getPortNumWidthBitsImpl(); }
-
 TestBackEnd *TestgenTarget::getTestBackend(const ProgramInfo &programInfo, SymbolicExecutor &symbex,
-                                           const std::filesystem::path &testPath,
-                                           std::optional<uint32_t> seed) {
-    return get().getTestBackendImpl(programInfo, symbex, testPath, seed);
+                                           const std::filesystem::path &testPath) {
+    return get().getTestBackendImpl(programInfo, symbex, testPath);
 }
 
 const ProgramInfo *TestgenTarget::initProgram(const IR::P4Program *program) {

backends/p4tools/modules/testgen/core/target.h

@@ -34,11 +34,7 @@ class TestgenTarget : public Target {
 
     /// Returns the test back end associated with this P4Testgen target.
     static TestBackEnd *getTestBackend(const ProgramInfo &programInfo, SymbolicExecutor &symbex,
-                                       const std::filesystem::path &testPath,
-                                       std::optional<uint32_t> seed);
-
-    /// The width of a port number, in bits.
-    static int getPortNumWidthBits();
+                                       const std::filesystem::path &testPath);
 
     /// Provides a CmdStepper implementation for this target.
     static CmdStepper *getCmdStepper(ExecutionState &state, AbstractSolver &solver,
@@ -63,14 +59,10 @@ class TestgenTarget : public Target {
     virtual const ProgramInfo *initProgramImpl(const IR::P4Program *program,
                                                const IR::Declaration_Instance *mainDecl) const = 0;
 
-    /// @see getPortNumWidthBits.
-    [[nodiscard]] virtual int getPortNumWidthBitsImpl() const = 0;
-
     /// @see getTestBackend.
     virtual TestBackEnd *getTestBackendImpl(const ProgramInfo &programInfo,
                                             SymbolicExecutor &symbex,
-                                            const std::filesystem::path &testPath,
-                                            std::optional<uint32_t> seed) const = 0;
+                                            const std::filesystem::path &testPath) const = 0;
 
     /// @see getCmdStepper.
     virtual CmdStepper *getCmdStepperImpl(ExecutionState &state, AbstractSolver &solver,
@@ -86,7 +78,6 @@ class TestgenTarget : public Target {
     /// Utility function. Converts the list of arguments @inputArgs to a list of type declarations
     ///  and appends the result to @v. Any names appearing in the arguments are
     /// resolved with @ns.
-    //
     static void argumentsToTypeDeclarations(const IR::IGeneralNamespace *ns,
                                             const IR::Vector<IR::Argument> *inputArgs,
                                             std::vector<const IR::Type_Declaration *> &resultDecls);

backends/p4tools/modules/testgen/lib/final_state.cpp

@@ -118,13 +118,13 @@ std::optional<std::reference_wrapper<const FinalState>> FinalState::computeConco
     auto &model = completeModel(state, new Model(solver.get().getSymbolicMapping()), false);
     /// Transfer any derived variables from that are missing  in this model.
     /// Do NOT update any variables that already exist.
-    for (const auto &varTuple : completedModel) {
+    for (const auto &varTuple : completedModel.get()) {
         model.emplace(varTuple.first, varTuple.second);
     }
     return *new FinalState(solver, state, model);
 }
 
-const Model *FinalState::getCompletedModel() const { return &completedModel; }
+const Model &FinalState::getCompletedModel() const { return completedModel; }
 
 AbstractSolver &FinalState::getSolver() const { return solver; }
 

backends/p4tools/modules/testgen/lib/final_state.h

@@ -26,7 +26,7 @@ class FinalState {
     std::reference_wrapper<const ExecutionState> state;
 
     /// The final model which has been augmented with environment completions.
-    const Model &completedModel;
+    std::reference_wrapper<const Model> completedModel;
 
     /// The final program trace.
     std::vector<std::reference_wrapper<const TraceEvent>> trace;
@@ -61,7 +61,7 @@ class FinalState {
         const ConcolicVariableMap &resolvedConcolicVariables) const;
 
     /// @returns the model after it was augmented by completions from the symbolic environment.
-    [[nodiscard]] const Model *getCompletedModel() const;
+    [[nodiscard]] const Model &getCompletedModel() const;
 
     /// @returns the solver associated with this final state.
     [[nodiscard]] AbstractSolver &getSolver() const;

backends/p4tools/modules/testgen/lib/test_backend.cpp

@@ -35,7 +35,6 @@ bool TestBackEnd::run(const FinalState &state) {
         // Evaluate the model and extract the input and output packets.
         const auto *executionState = state.getExecutionState();
         const auto *outputPacketExpr = executionState->getPacketBuffer();
-        const auto *completedModel = state.getCompletedModel();
         const auto *outputPortExpr = executionState->get(programInfo.getTargetOutputPortVar());
         const auto &coverableNodes = programInfo.getCoverableNodes();
         const auto *programTraces = state.getTraces();
@@ -63,7 +62,7 @@ bool TestBackEnd::run(const FinalState &state) {
 
         // Execute concolic functions that may occur in the output packet, the output port,
         // or any path conditions.
-        auto concolicResolver = ConcolicResolver(*completedModel, *executionState,
+        auto concolicResolver = ConcolicResolver(state.getCompletedModel(), *executionState,
                                                  *programInfo.getConcolicMethodImpls());
 
         outputPacketExpr->apply(concolicResolver);
@@ -85,10 +84,10 @@ bool TestBackEnd::run(const FinalState &state) {
         auto replacedState = concolicOptState.value().get();
         executionState = replacedState.getExecutionState();
         outputPacketExpr = executionState->getPacketBuffer();
-        completedModel = replacedState.getCompletedModel();
+        const auto &completedModel = replacedState.getCompletedModel();
         outputPortExpr = executionState->get(programInfo.getTargetOutputPortVar());
 
-        auto testInfo = produceTestInfo(executionState, completedModel, outputPacketExpr,
+        auto testInfo = produceTestInfo(executionState, &completedModel, outputPacketExpr,
                                         outputPortExpr, programTraces);
 
         // Add a list of tracked branches to the test output, too.
@@ -103,7 +102,7 @@ bool TestBackEnd::run(const FinalState &state) {
             printPerformanceReport(false);
             return needsToTerminate(testCount);
         }
-        const auto *testSpec = createTestSpec(executionState, completedModel, testInfo);
+        const auto *testSpec = createTestSpec(executionState, &completedModel, testInfo);
 
         // Commit an update to the visited statements.
         // Only do this once we are sure we are generating a test.

backends/p4tools/modules/testgen/lib/test_backend.h

@@ -1,8 +1,7 @@
 #ifndef BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_TEST_BACKEND_H_
 #define BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_TEST_BACKEND_H_
 
-#include <stdint.h>
-
+#include <cstdint>
 #include <functional>
 #include <optional>
 #include <vector>

backends/p4tools/modules/testgen/options.cpp

@@ -16,7 +16,7 @@
 
 #include "backends/p4tools/modules/testgen/lib/logging.h"
 
-namespace P4Tools {
+namespace P4Tools::P4Testgen {
 
 TestgenOptions &TestgenOptions::get() {
     static TestgenOptions INSTANCE;
@@ -327,4 +327,4 @@ TestgenOptions::TestgenOptions()
         "produce no tests or only tests that contain counter examples.");
 }
 
-}  // namespace P4Tools
+}  // namespace P4Tools::P4Testgen

backends/p4tools/modules/testgen/options.h

@@ -11,7 +11,7 @@
 
 #include "backends/p4tools/modules/testgen/core/symbolic_executor/path_selection.h"
 
-namespace P4Tools {
+namespace P4Tools::P4Testgen {
 
 /// Encapsulates and processes command-line options for P4Testgen.
 class TestgenOptions : public AbstractP4cToolOptions {
@@ -84,6 +84,6 @@ class TestgenOptions : public AbstractP4cToolOptions {
     TestgenOptions();
 };
 
-}  // namespace P4Tools
+}  // namespace P4Tools::P4Testgen
 
 #endif /* BACKENDS_P4TOOLS_MODULES_TESTGEN_OPTIONS_H_ */

backends/p4tools/modules/testgen/targets/bmv2/CMakeLists.txt

@@ -34,8 +34,5 @@ execute_process(COMMAND ln -sfn ${P4C_SOURCE_DIR}/backends/bmv2/run-bmv2-test.py
 
 set(
   TESTGEN_LIBS ${TESTGEN_LIBS}
-  ${P4C_LIBRARIES}
-  ${P4C_LIB_DEPS}
-  ${CMAKE_THREAD_LIBS_INIT}
   PARENT_SCOPE
 )

backends/p4tools/modules/testgen/targets/bmv2/constants.h

@@ -34,6 +34,8 @@ class BMv2Constants {
     enum CloneType { I2E = 0, E2E = 1 };
     /// Meter colors are defined in v1model.p4
     enum METER_COLOR { GREEN = 0, YELLOW = 1, RED = 2 };
+    /// Port width in bits.
+    static constexpr int PORT_BIT_WIDTH = 9;
 
     /// Other useful constants
     static constexpr int STF_MIN_PKT_SIZE = 22;

backends/p4tools/modules/testgen/targets/bmv2/expr_stepper.cpp

@@ -357,8 +357,7 @@ void Bmv2V1ModelExprStepper::evalExternMethodCall(const IR::MethodCallExpression
             IR::ID & /*methodName*/, const IR::Vector<IR::Argument> *args,
             const ExecutionState &state, SmallStepEvaluator::Result &result) {
              auto &nextState = state.clone();
-             const auto *nineBitType =
-                 IR::getBitType(Bmv2V1ModelTestgenTarget::getPortNumWidthBits());
+             const auto *nineBitType = IR::getBitType(BMv2Constants::PORT_BIT_WIDTH);
              const auto *metadataLabel = args->at(0)->expression;
              if (!(metadataLabel->is<IR::Member>() || metadataLabel->is<IR::PathExpression>())) {
                  TESTGEN_UNIMPLEMENTED("Drop input %1% of type %2% not supported", metadataLabel,

backends/p4tools/modules/testgen/targets/bmv2/program_info.cpp

@@ -153,7 +153,7 @@ std::vector<Continuation::Command> Bmv2V1ModelProgramInfo::processDeclaration(
     // processing. For example, the egress port.
     if ((archMember->blockName == "Ingress")) {
         auto *egressPortVar =
-            new IR::Member(IR::getBitType(TestgenTarget::getPortNumWidthBits()),
+            new IR::Member(IR::getBitType(BMv2Constants::PORT_BIT_WIDTH),
                            new IR::PathExpression("*standard_metadata"), "egress_port");
         auto *portStmt = new IR::AssignmentStatement(egressPortVar, getTargetOutputPortVar());
         cmds.emplace_back(portStmt);
@@ -187,9 +187,9 @@ std::vector<Continuation::Command> Bmv2V1ModelProgramInfo::processDeclaration(
 }
 
 const IR::StateVariable &Bmv2V1ModelProgramInfo::getTargetInputPortVar() const {
-    return *new IR::StateVariable(
-        new IR::Member(IR::getBitType(TestgenTarget::getPortNumWidthBits()),
-                       new IR::PathExpression("*standard_metadata"), "ingress_port"));
+    return *new IR::StateVariable(new IR::Member(IR::getBitType(BMv2Constants::PORT_BIT_WIDTH),
+                                                 new IR::PathExpression("*standard_metadata"),
+                                                 "ingress_port"));
 }
 
 const IR::Expression *Bmv2V1ModelProgramInfo::getPortConstraint(const IR::StateVariable &portVar) {
@@ -200,9 +200,9 @@ const IR::Expression *Bmv2V1ModelProgramInfo::getPortConstraint(const IR::StateV
 }
 
 const IR::StateVariable &Bmv2V1ModelProgramInfo::getTargetOutputPortVar() const {
-    return *new IR::StateVariable(
-        new IR::Member(IR::getBitType(TestgenTarget::getPortNumWidthBits()),
-                       new IR::PathExpression("*standard_metadata"), "egress_spec"));
+    return *new IR::StateVariable(new IR::Member(IR::getBitType(BMv2Constants::PORT_BIT_WIDTH),
+                                                 new IR::PathExpression("*standard_metadata"),
+                                                 "egress_spec"));
 }
 
 const IR::Expression *Bmv2V1ModelProgramInfo::dropIsActive() const {

backends/p4tools/modules/testgen/targets/bmv2/target.cpp

@@ -67,15 +67,12 @@ const Bmv2V1ModelProgramInfo *Bmv2V1ModelTestgenTarget::initProgramImpl(
     return new Bmv2V1ModelProgramInfo(program, programmableBlocks, declIdToGress);
 }
 
-Bmv2TestBackend *Bmv2V1ModelTestgenTarget::getTestBackendImpl(const ProgramInfo &programInfo,
-                                                              SymbolicExecutor &symbex,
-                                                              const std::filesystem::path &testPath,
-                                                              std::optional<uint32_t> seed) const {
-    return new Bmv2TestBackend(programInfo, symbex, testPath, seed);
+Bmv2TestBackend *Bmv2V1ModelTestgenTarget::getTestBackendImpl(
+    const ProgramInfo &programInfo, SymbolicExecutor &symbex,
+    const std::filesystem::path &testPath) const {
+    return new Bmv2TestBackend(programInfo, symbex, testPath);
 }
 
-int Bmv2V1ModelTestgenTarget::getPortNumWidthBitsImpl() const { return 9; }
-
 Bmv2V1ModelCmdStepper *Bmv2V1ModelTestgenTarget::getCmdStepperImpl(
     ExecutionState &state, AbstractSolver &solver, const ProgramInfo &programInfo) const {
     return new Bmv2V1ModelCmdStepper(state, solver, programInfo);

backends/p4tools/modules/testgen/targets/bmv2/target.h

@@ -29,11 +29,8 @@ class Bmv2V1ModelTestgenTarget : public TestgenTarget {
     const Bmv2V1ModelProgramInfo *initProgramImpl(
         const IR::P4Program *program, const IR::Declaration_Instance *mainDecl) const override;
 
-    [[nodiscard]] int getPortNumWidthBitsImpl() const override;
-
     Bmv2TestBackend *getTestBackendImpl(const ProgramInfo &programInfo, SymbolicExecutor &symbex,
-                                        const std::filesystem::path &testPath,
-                                        std::optional<uint32_t> seed) const override;
+                                        const std::filesystem::path &testPath) const override;
 
     Bmv2V1ModelCmdStepper *getCmdStepperImpl(ExecutionState &state, AbstractSolver &solver,
                                              const ProgramInfo &programInfo) const override;

backends/p4tools/modules/testgen/targets/bmv2/test_backend.cpp

@@ -39,8 +39,7 @@ const std::set<std::string> Bmv2TestBackend::SUPPORTED_BACKENDS = {"PTF", "STF",
                                                                    "METADATA"};
 
 Bmv2TestBackend::Bmv2TestBackend(const ProgramInfo &programInfo, SymbolicExecutor &symbex,
-                                 const std::filesystem::path &testPath,
-                                 std::optional<uint32_t> seed)
+                                 const std::filesystem::path &testPath)
     : TestBackEnd(programInfo, symbex) {
     cstring testBackendString = TestgenOptions::get().testBackend;
     if (testBackendString.isNullOrEmpty()) {
@@ -50,6 +49,7 @@ Bmv2TestBackend::Bmv2TestBackend(const ProgramInfo &programInfo, SymbolicExecuto
         exit(EXIT_FAILURE);
     }
 
+    auto seed = TestgenOptions::get().seed;
     if (testBackendString == "PTF") {
         testWriter = new PTF(testPath, seed);
     } else if (testBackendString == "STF") {

backends/p4tools/modules/testgen/targets/bmv2/test_backend.h

@@ -36,7 +36,7 @@ class Bmv2TestBackend : public TestBackEnd {
 
  public:
     explicit Bmv2TestBackend(const ProgramInfo &programInfo, SymbolicExecutor &symbex,
-                             const std::filesystem::path &testPath, std::optional<uint32_t> seed);
+                             const std::filesystem::path &testPath);
 
     TestBackEnd::TestInfo produceTestInfo(
         const ExecutionState *executionState, const Model *completedModel,

backends/p4tools/modules/testgen/targets/ebpf/CMakeLists.txt

@@ -27,8 +27,5 @@ execute_process(COMMAND ln -sfn ${P4C_SOURCE_DIR}/backends/ebpf/run-ebpf-test.py
 
 set(
   TESTGEN_LIBS ${TESTGEN_LIBS}
-  ${P4C_LIBRARIES}
-  ${P4C_LIB_DEPS}
-  ${CMAKE_THREAD_LIBS_INIT}
   PARENT_SCOPE
 )

backends/p4tools/modules/testgen/targets/ebpf/constants.h

@@ -9,6 +9,8 @@ class EBPFConstants {
  public:
     /// eBPF-internal drop variable.
     static const IR::PathExpression ACCEPT_VAR;
+    /// Port width in bits.
+    static constexpr int PORT_BIT_WIDTH = 9;
 };
 
 }  // namespace P4Tools::P4Testgen::EBPF

backends/p4tools/modules/testgen/targets/ebpf/program_info.cpp

@@ -106,15 +106,13 @@ std::vector<Continuation::Command> EBPFProgramInfo::processDeclaration(
 }
 
 const IR::StateVariable &EBPFProgramInfo::getTargetInputPortVar() const {
-    return *new IR::StateVariable(
-        new IR::Member(IR::getBitType(TestgenTarget::getPortNumWidthBits()),
-                       new IR::PathExpression("*"), "input_port"));
+    return *new IR::StateVariable(new IR::Member(IR::getBitType(EBPFConstants::PORT_BIT_WIDTH),
+                                                 new IR::PathExpression("*"), "input_port"));
 }
 
 const IR::StateVariable &EBPFProgramInfo::getTargetOutputPortVar() const {
-    return *new IR::StateVariable(
-        new IR::Member(IR::getBitType(TestgenTarget::getPortNumWidthBits()),
-                       new IR::PathExpression("*"), "output_port"));
+    return *new IR::StateVariable(new IR::Member(IR::getBitType(EBPFConstants::PORT_BIT_WIDTH),
+                                                 new IR::PathExpression("*"), "output_port"));
 }
 
 const IR::Expression *EBPFProgramInfo::dropIsActive() const {

backends/p4tools/modules/testgen/targets/ebpf/target.cpp

@@ -67,15 +67,12 @@ const EBPFProgramInfo *EBPFTestgenTarget::initProgramImpl(
     return new EBPFProgramInfo(program, programmableBlocks);
 }
 
-EBPFTestBackend *EBPFTestgenTarget::getTestBackendImpl(const ProgramInfo &programInfo,
-                                                       SymbolicExecutor &symbex,
-                                                       const std::filesystem::path &testPath,
-                                                       std::optional<uint32_t> seed) const {
-    return new EBPFTestBackend(programInfo, symbex, testPath, seed);
+EBPFTestBackend *EBPFTestgenTarget::getTestBackendImpl(
+    const ProgramInfo &programInfo, SymbolicExecutor &symbex,
+    const std::filesystem::path &testPath) const {
+    return new EBPFTestBackend(programInfo, symbex, testPath);
 }
 
-int EBPFTestgenTarget::getPortNumWidthBitsImpl() const { return 9; }
-
 EBPFCmdStepper *EBPFTestgenTarget::getCmdStepperImpl(ExecutionState &state, AbstractSolver &solver,
                                                      const ProgramInfo &programInfo) const {
     return new EBPFCmdStepper(state, solver, programInfo);