Introduce a configuration structure for the test back ends.

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

@@ -40,9 +40,10 @@ const ProgramInfo *TestgenTarget::produceProgramInfoImpl(
 
 const TestgenTarget &TestgenTarget::get() { return Target::get<TestgenTarget>("testgen"); }
 
-TestBackEnd *TestgenTarget::getTestBackend(const ProgramInfo &programInfo, SymbolicExecutor &symbex,
-                                           const std::filesystem::path &testPath) {
-    return get().getTestBackendImpl(programInfo, symbex, testPath);
+TestBackEnd *TestgenTarget::getTestBackend(const ProgramInfo &programInfo,
+                                           const TestBackendConfiguration &testBackendConfiguration,
+                                           SymbolicExecutor &symbex) {
+    return get().getTestBackendImpl(programInfo, testBackendConfiguration, symbex);
 }
 
 const ProgramInfo *TestgenTarget::produceProgramInfo(const CompilerResult &compilerResult) {

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

@@ -30,8 +30,9 @@ class TestgenTarget : public Target {
     static const ProgramInfo *produceProgramInfo(const CompilerResult &compilerResult);
 
     /// Returns the test back end associated with this P4Testgen target.
-    static TestBackEnd *getTestBackend(const ProgramInfo &programInfo, SymbolicExecutor &symbex,
-                                       const std::filesystem::path &testPath);
+    static TestBackEnd *getTestBackend(const ProgramInfo &programInfo,
+                                       const TestBackendConfiguration &testBackendConfiguration,
+                                       SymbolicExecutor &symbex);
 
     /// Provides a CmdStepper implementation for this target.
     static CmdStepper *getCmdStepper(ExecutionState &state, AbstractSolver &solver,
@@ -51,9 +52,9 @@ class TestgenTarget : public Target {
         const CompilerResult &compilerResult, const IR::Declaration_Instance *mainDecl) const = 0;
 
     /// @see getTestBackend.
-    virtual TestBackEnd *getTestBackendImpl(const ProgramInfo &programInfo,
-                                            SymbolicExecutor &symbex,
-                                            const std::filesystem::path &testPath) const = 0;
+    virtual TestBackEnd *getTestBackendImpl(
+        const ProgramInfo &programInfo, const TestBackendConfiguration &testBackendConfiguration,
+        SymbolicExecutor &symbex) const = 0;
 
     /// @see getCmdStepper.
     virtual CmdStepper *getCmdStepperImpl(ExecutionState &state, AbstractSolver &solver,

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

@@ -32,8 +32,8 @@ 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 *outputPortExpr = executionState->get(programInfo.getTargetOutputPortVar());
-        const auto &coverableNodes = programInfo.getCoverableNodes();
+        const auto *outputPortExpr = executionState->get(getProgramInfo().getTargetOutputPortVar());
+        const auto &coverableNodes = getProgramInfo().getCoverableNodes();
         const auto *programTraces = state.getTraces();
         const auto &testgenOptions = TestgenOptions::get();
 
@@ -69,7 +69,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(state.getFinalModel(), *executionState,
-                                                 *programInfo.getConcolicMethodImpls());
+                                                 *getProgramInfo().getConcolicMethodImpls());
 
         outputPacketExpr->apply(concolicResolver);
         outputPortExpr->apply(concolicResolver);
@@ -91,7 +91,7 @@ bool TestBackEnd::run(const FinalState &state) {
         executionState = replacedState.getExecutionState();
         outputPacketExpr = executionState->getPacketBuffer();
         const auto &finalModel = replacedState.getFinalModel();
-        outputPortExpr = executionState->get(programInfo.getTargetOutputPortVar());
+        outputPortExpr = executionState->get(getProgramInfo().getTargetOutputPortVar());
 
         auto testInfo = produceTestInfo(executionState, &finalModel, outputPacketExpr,
                                         outputPortExpr, programTraces);
@@ -178,7 +178,7 @@ TestBackEnd::TestInfo TestBackEnd::produceTestInfo(
     const auto *inputPacket = finalModel->evaluate(inputPacketExpr, true);
     const auto *outputPacket = finalModel->evaluate(outputPacketExpr, true);
     const auto *inputPort =
-        finalModel->evaluate(executionState->get(programInfo.getTargetInputPortVar()), true);
+        finalModel->evaluate(executionState->get(getProgramInfo().getTargetInputPortVar()), true);
 
     const auto *outputPortVar = finalModel->evaluate(outputPortExpr, true);
     // Build the taint mask by dissecting the program packet variable
@@ -246,4 +246,10 @@ int64_t TestBackEnd::getTestCount() const { return testCount; }
 
 float TestBackEnd::getCoverage() const { return coverage; }
 
+const ProgramInfo &TestBackEnd::getProgramInfo() const { return programInfo; }
+
+const TestBackendConfiguration &TestBackEnd::getTestBackendConfiguration() const {
+    return testBackendConfiguration;
+}
+
 }  // namespace P4Tools::P4Testgen

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

@@ -28,15 +28,18 @@ class TestBackEnd {
     /// Indicates the number of generated tests after which we reset memory.
     static const int64_t RESET_THRESHOLD = 10000;
 
- protected:
     /// ProgramInfo is used to access some target specific information for test generation.
-    const ProgramInfo &programInfo;
+    std::reference_wrapper<const ProgramInfo> programInfo;
+
+    /// Configuration options for the test back end.
+    std::reference_wrapper<const TestBackendConfiguration> testBackendConfiguration;
 
+ protected:
     /// Writes the tests out to a file.
     TestFramework *testWriter = nullptr;
 
     /// Pointer to the symbolic executor.
-    /// TODO: Remove this.
+    /// TODO: Remove this. We only need to update coverage tracking.
     SymbolicExecutor &symbex;
 
     /// Test maximum number of tests that are to be produced.
@@ -45,8 +48,13 @@ class TestBackEnd {
     /// The accumulated coverage of all finished test cases. Number in range [0, 1].
     float coverage = 0;
 
-    explicit TestBackEnd(const ProgramInfo &programInfo, SymbolicExecutor &symbex)
-        : programInfo(programInfo), symbex(symbex), maxTests(TestgenOptions::get().maxTests) {
+    explicit TestBackEnd(const ProgramInfo &programInfo,
+                         const TestBackendConfiguration &testBackendConfiguration,
+                         SymbolicExecutor &symbex)
+        : programInfo(programInfo),
+          testBackendConfiguration(testBackendConfiguration),
+          symbex(symbex),
+          maxTests(TestgenOptions::get().maxTests) {
         // If we select a specific branch, the number of tests should be 1.
         if (!TestgenOptions::get().selectedBranches.empty()) {
             maxTests = 1;
@@ -119,6 +127,12 @@ class TestBackEnd {
 
     /// Returns coverage achieved by all the processed tests.
     [[nodiscard]] float getCoverage() const;
+
+    /// Returns the program info.
+    [[nodiscard]] const ProgramInfo &getProgramInfo() const;
+
+    /// Returns the configuration options for the test back end.
+    [[nodiscard]] const TestBackendConfiguration &getTestBackendConfiguration() const;
 };
 
 }  // namespace P4Tools::P4Testgen

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

@@ -0,0 +1,33 @@
+#ifndef BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_TEST_BACKEND_CONFIGURATION_H_
+#define BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_TEST_BACKEND_CONFIGURATION_H_
+
+#include <filesystem>
+#include <optional>
+
+#include "lib/cstring.h"
+
+namespace P4Tools::P4Testgen {
+
+/// A file path which may not be set.
+using OptionalFilePath = std::optional<std::filesystem::path>;
+
+/// Configuration parameters for P4Testgen test back ends.
+/// These parameters may influence how tests are generated.
+struct TestBackendConfiguration {
+    /// The base name of the test.
+    cstring testName;
+
+    /// The maximum number of tests to produce. Defaults to one test.
+    int64_t maxTests = 1;
+
+    /// The base path to be used when writing out tests.
+    /// May not be set, which means no tests are written to file.
+    OptionalFilePath fileBasePath;
+
+    /// The initial seed used to generate tests. If it is not set, no seed was used.
+    std::optional<unsigned int> seed;
+};
+
+}  // namespace P4Tools::P4Testgen
+
+#endif /* BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_TEST_BACKEND_CONFIGURATION_H_ */

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

@@ -1,12 +1,11 @@
 #include "backends/p4tools/modules/testgen/lib/test_framework.h"
 
-#include <optional>
-#include <utility>
-
 namespace P4Tools::P4Testgen {
 
-TestFramework::TestFramework(std::filesystem::path basePath,
-                             std::optional<unsigned int> seed = std::nullopt)
-    : basePath(std::move(basePath)), seed(seed) {}
+TestFramework::TestFramework(const TestBackendConfiguration &testBackendConfiguration)
+    : testBackendConfiguration(testBackendConfiguration) {}
 
+const TestBackendConfiguration &TestFramework::getTestBackendConfiguration() const {
+    return testBackendConfiguration.get();
+}
 }  // namespace P4Tools::P4Testgen

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

@@ -2,10 +2,8 @@
 #define BACKENDS_P4TOOLS_MODULES_TESTGEN_LIB_TEST_FRAMEWORK_H_
 
 #include <cstddef>
-#include <filesystem>
 #include <iosfwd>
 #include <map>
-#include <optional>
 #include <string>
 #include <utility>
 
@@ -15,6 +13,7 @@
 #include "backends/p4tools/common/lib/trace_event.h"
 #include "lib/cstring.h"
 
+#include "backends/p4tools/modules/testgen/lib/test_backend_configuration.h"
 #include "backends/p4tools/modules/testgen/lib/test_object.h"
 #include "backends/p4tools/modules/testgen/lib/test_spec.h"
 
@@ -23,15 +22,13 @@ namespace P4Tools::P4Testgen {
 /// THe default base class for the various test frameworks. Every test framework has a test
 /// name and a seed associated with it. Also contains a variety of common utility functions.
 class TestFramework {
- protected:
-    /// The @basePath to be used in test case generation.
-    std::filesystem::path basePath;
-
-    /// The seed used by the testgen.
-    std::optional<unsigned int> seed;
+ private:
+    /// Configuration options for the test back end.
+    std::reference_wrapper<const TestBackendConfiguration> testBackendConfiguration;
 
+ protected:
     /// Creates a generic test framework.
-    TestFramework(std::filesystem::path basePath, std::optional<unsigned int> seed);
+    explicit TestFramework(const TestBackendConfiguration &testBackendConfiguration);
 
     /// Converts the traces of this test into a string representation and Inja object.
     static inja::json getTrace(const TestSpec *testSpec) {
@@ -131,7 +128,12 @@ class TestFramework {
         }
     }
 
+    /// Returns the configuration options for the test back end.
+    [[nodiscard]] const TestBackendConfiguration &getTestBackendConfiguration() const;
+
  public:
+    virtual ~TestFramework() = default;
+
     /// The method used to output the test case to be implemented by
     /// all the test frameworks (eg. STF, PTF, etc.).
     /// @param spec the testcase specification to be outputted

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

@@ -71,9 +71,10 @@ const Bmv2V1ModelProgramInfo *Bmv2V1ModelTestgenTarget::produceProgramInfoImpl(
 }
 
 Bmv2TestBackend *Bmv2V1ModelTestgenTarget::getTestBackendImpl(
-    const ProgramInfo &programInfo, SymbolicExecutor &symbex,
-    const std::filesystem::path &testPath) const {
-    return new Bmv2TestBackend(*programInfo.checkedTo<Bmv2V1ModelProgramInfo>(), symbex, testPath);
+    const ProgramInfo &programInfo, const TestBackendConfiguration &testBackendConfiguration,
+    SymbolicExecutor &symbex) const {
+    return new Bmv2TestBackend(*programInfo.checkedTo<Bmv2V1ModelProgramInfo>(),
+                               testBackendConfiguration, symbex);
 }
 
 Bmv2V1ModelCmdStepper *Bmv2V1ModelTestgenTarget::getCmdStepperImpl(

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

@@ -30,8 +30,9 @@ class Bmv2V1ModelTestgenTarget : public TestgenTarget {
         const CompilerResult &compilerResult,
         const IR::Declaration_Instance *mainDecl) const override;
 
-    Bmv2TestBackend *getTestBackendImpl(const ProgramInfo &programInfo, SymbolicExecutor &symbex,
-                                        const std::filesystem::path &testPath) const override;
+    Bmv2TestBackend *getTestBackendImpl(const ProgramInfo &programInfo,
+                                        const TestBackendConfiguration &testBackendConfiguration,
+                                        SymbolicExecutor &symbex) const override;
 
     Bmv2V1ModelCmdStepper *getCmdStepperImpl(ExecutionState &state, AbstractSolver &solver,
                                              const ProgramInfo &programInfo) const override;

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

@@ -81,7 +81,8 @@ TEST_F(PTFTest, Ptf01) {
     auto testSpec = TestSpec(ingressPacket, egressPacket, {});
     testSpec.addTestObject("tables", "SwitchIngress.forward", &fwdConfig);
 
-    auto testWriter = PTF("test01", 1);
+    TestBackendConfiguration testBackendConfiguration{"test01", 1, "test01", 1};
+    auto testWriter = PTF(testBackendConfiguration);
     testWriter.outputTest(&testSpec, "", 1, 0);
 }
 
@@ -111,7 +112,8 @@ TEST_F(PTFTest, Ptf02) {
     testSpec.addTestObject("tables", "SwitchIngress.forward", &fwdConfig);
     testSpec.addTestObject("tables", "SwitchIngress.ipRoute", &ipRouteConfig);
 
-    auto testWriter = PTF("test02", 2);
+    TestBackendConfiguration testBackendConfiguration{"test02", 1, "test02", 2};
+    auto testWriter = PTF(testBackendConfiguration);
     testWriter.outputTest(&testSpec, "", 2, 0);
 }
 
@@ -155,7 +157,8 @@ TEST_F(PTFTest, Ptf03) {
     auto testSpec = TestSpec(ingressPacket, egressPacket, {});
     testSpec.addTestObject("tables", "test1", &test1Config);
 
-    auto testWriter = PTF("test03", 3);
+    TestBackendConfiguration testBackendConfiguration{"test03", 1, "test03", 3};
+    auto testWriter = PTF(testBackendConfiguration);
     try {
         testWriter.outputTest(&testSpec, "", 3, 0);
     } catch (const Util::CompilerBug &e) {
@@ -222,7 +225,8 @@ TEST_F(PTFTest, Ptf04) {
     auto testSpec = TestSpec(ingressPacket, egressPacket, {});
     testSpec.addTestObject("tables", "test1", &test1Config);
 
-    auto testWriter = PTF("test04", 4);
+    TestBackendConfiguration testBackendConfiguration{"test04", 1, "test04", 4};
+    auto testWriter = PTF(testBackendConfiguration);
     try {
         testWriter.outputTest(&testSpec, "", 4, 0);
     } catch (const Util::CompilerBug &e) {

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

@@ -6,6 +6,7 @@
 
 namespace Test {
 
+using TestBackendConfiguration = P4Tools::P4Testgen::TestBackendConfiguration;
 using Packet = P4Tools::P4Testgen::Packet;
 using ActionArg = P4Tools::P4Testgen::ActionArg;
 using ActionCall = P4Tools::P4Testgen::ActionCall;

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

@@ -81,7 +81,8 @@ TEST_F(STFTest, Stf01) {
     auto testSpec = TestSpec(ingressPacket, egressPacket, {});
     testSpec.addTestObject("tables", "SwitchIngress.forward", &fwdConfig);
 
-    auto testWriter = STF("test01", 1);
+    TestBackendConfiguration testBackendConfiguration{"test01", 1, "test01", 1};
+    auto testWriter = STF(testBackendConfiguration);
     testWriter.outputTest(&testSpec, "", 1, 0);
 }
 
@@ -111,7 +112,8 @@ TEST_F(STFTest, Stf02) {
     testSpec.addTestObject("tables", "SwitchIngress.forward", &fwdConfig);
     testSpec.addTestObject("tables", "SwitchIngress.ipRoute", &ipRouteConfig);
 
-    auto testWriter = STF("test02", 2);
+    TestBackendConfiguration testBackendConfiguration{"test02", 1, "test02", 2};
+    auto testWriter = STF(testBackendConfiguration);
     testWriter.outputTest(&testSpec, "", 2, 0);
 }
 
@@ -155,7 +157,8 @@ TEST_F(STFTest, Stf03) {
     auto testSpec = TestSpec(ingressPacket, egressPacket, {});
     testSpec.addTestObject("tables", "test1", &test1Config);
 
-    auto testWriter = STF("test03", 3);
+    TestBackendConfiguration testBackendConfiguration{"test03", 1, "test03", 3};
+    auto testWriter = STF(testBackendConfiguration);
     try {
         testWriter.outputTest(&testSpec, "", 3, 0);
     } catch (const Util::CompilerBug &e) {
@@ -222,7 +225,8 @@ TEST_F(STFTest, Stf04) {
     auto testSpec = TestSpec(ingressPacket, egressPacket, {});
     testSpec.addTestObject("tables", "test1", &test1Config);
 
-    auto testWriter = STF("test04", 4);
+    TestBackendConfiguration testBackendConfiguration{"test04", 1, "test04", 4};
+    auto testWriter = STF(testBackendConfiguration);
     try {
         testWriter.outputTest(&testSpec, "", 4, 0);
     } catch (const Util::CompilerBug &e) {

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

@@ -6,6 +6,7 @@
 
 namespace Test {
 
+using TestBackendConfiguration = P4Tools::P4Testgen::TestBackendConfiguration;
 using Packet = P4Tools::P4Testgen::Packet;
 using ActionArg = P4Tools::P4Testgen::ActionArg;
 using ActionCall = P4Tools::P4Testgen::ActionCall;