Add stop metrics for P4Testgen. Sanitize some P4Testgen options. (p4l…

…ang#3829)
kamleshbhalui · Jan 16, 2023 · 9f59c7b · 9f59c7b
1 parent 64cece3
commit 9f59c7b
Show file tree

Hide file tree

Showing 13 changed files with 272 additions and 156 deletions.
diff --git a/backends/p4tools/common/lib/util.h b/backends/p4tools/common/lib/util.h
@@ -144,6 +144,24 @@ class Utils {
         std::advance(start, random);
         return start;
     }
+
+    /// Convert a container type (array, set, vector, etc.) into a well-formed [val1, val2, ...]
+    /// representation. This function is used for debugging output.
+    template <typename ContainerType>
+    static std::string containerToString(const ContainerType& container) {
+        std::stringstream stringStream;
+
+        stringStream << '[';
+        auto val = container.cbegin();
+        if (val != container.cend()) {
+            stringStream << *val++;
+            while (val != container.cend()) {
+                stringStream << ", " << *val++;
+            }
+        }
+        stringStream << ']';
+        return stringStream.str();
+    }
 };
 
 }  // namespace P4Tools

diff --git a/backends/p4tools/common/options.cpp b/backends/p4tools/common/options.cpp
@@ -123,47 +123,6 @@ AbstractP4cToolOptions::AbstractP4cToolOptions(cstring message) : Options(messag
         },
         "Prints version information and exits");
 
-    registerOption(
-        "--packet-size-range", "packetSizeRange",
-        [this](const char* arg) {
-            auto rangeStr = std::string(arg);
-            size_t packetLenStr = rangeStr.find_first_of(':');
-            try {
-                auto minPacketLenStr = rangeStr.substr(0, packetLenStr);
-                minPktSize = std::stoi(minPacketLenStr);
-                if (minPktSize < 0) {
-                    ::error(
-                        "Invalid minimum packet size %1%. Minimum packet size must be at least 0.",
-                        minPktSize);
-                }
-                auto maxPacketLenStr = rangeStr.substr(packetLenStr + 1);
-                maxPktSize = std::stoi(maxPacketLenStr);
-                if (maxPktSize < minPktSize) {
-                    ::error(
-                        "Invalid packet size range %1%:%2%.  The maximum packet size must be at "
-                        "least the size of the minimum packet size.",
-                        minPktSize, maxPktSize);
-                }
-            } catch (std::invalid_argument&) {
-                ::error(
-                    "Invalid packet size range %1%. Expected format is [min]:[max], where [min] "
-                    "and [max] are integers.",
-                    arg);
-                return false;
-            }
-            return true;
-        },
-        "Specify the possible range of the input packet size in bits. The format is [min]:[max]. "
-        "The default values are \"0:72000\". The maximum is set to jumbo frame size (9000 bytes).");
-
-    registerOption(
-        "--seed", "seed",
-        [this](const char* arg) {
-            seed = std::stoul(arg);
-            return true;
-        },
-        "Provides a randomization seed");
-
     // Inherit some compiler options, setting them up to be forwarded to the compiler.
     std::vector<InheritedCompilerOptionSpec> inheritedCompilerOptions = {
         {"-I", "path", "Adds the given path to the preprocessor include path", {}},
@@ -207,6 +166,14 @@ AbstractP4cToolOptions::AbstractP4cToolOptions(cstring message) : Options(messag
         {"-v", nullptr, "Increase verbosity level (can be repeated)", {}},
     };
 
+    registerOption(
+        "--seed", "seed",
+        [this](const char* arg) {
+            seed = std::stoul(arg);
+            return true;
+        },
+        "Provides a randomization seed");
+
     for (const auto& optionSpec : inheritedCompilerOptions) {
         registerOption(
             optionSpec.option, optionSpec.argName,

diff --git a/backends/p4tools/modules/testgen/README.md b/backends/p4tools/modules/testgen/README.md
@@ -1,6 +1,6 @@
 # P4Testgen - Generating Tests for P4 Targets
 
-The P4Testgen tool uses symbolic execution to automatically generate input-output tests for a given P4 program. P4Testgen attempts to generate a set of tests of all reachable paths within the program. Each test consists of an input packet, the control-plane commands to populate match-action tables, and a predicate on the output packet. Each generated test also has a human-readable trace that indicates the path through the program being exercised by that test.
+P4Testgen uses symbolic execution to automatically generate input-output tests for a given P4 program. P4Testgen attempts to generate a set of tests of all reachable paths within the program. Each test consists of an input packet, the control-plane commands to populate match-action tables, and a predicate on the output packet. Each generated test also has a human-readable trace that indicates the path through the program being exercised by that test.
 
 ## Directory Structure
 
@@ -20,40 +20,52 @@ testgen
 ## Usage
 The main binary can be found in `build/p4testgen`.
 
-To generate tests for a particular target and P4 architecture, run `p4testgen –target [TARGET] –arch [ARCH] –max-tests 10 –out-dir [OUT] prog.p4`
-`p4testgen` specifies that the p4testgen tool should be used. In the future, other tools may be supported, for example random program generation or translation validators.
+To generate 10 tests for a particular target and P4 architecture, run `p4testgen –target [TARGET] –arch [ARCH] –max-tests 10 –out-dir [OUT] prog.p4`
+`p4testgen` specifies that P4Testgen should be used. In the future, other tools may be supported, for example random program generation or translation validators.
 These are the current usage flags:
 
 ```
-./p4testgen: Generate packet tests for a P4 program
---help                     Shows this help message and exits
---version                  Prints version information and exits
---seed seed                Provides a randomization seed
--I path                    Adds the given path to the preprocessor include path
--D arg=value               Defines a preprocessor symbol
--U arg                     Undefines a preprocessor symbol
--E                         Preprocess only. Prints preprocessed program on stdout.
---nocpp                    Skips the preprocessor; assumes the input file is already preprocessed.
---std {p4-14|p4-16}        Specifies source language version.
--T loglevel                Adjusts logging level per file.
---target target            Specifies the device targeted by the program.
---arch arch                Specifies the architecture targeted by the program.
---top4 pass1[,pass2]       Dump the P4 representation after
-                           passes whose name contains one of `passX' substrings.
-                           When '-v' is used this will include the compiler IR.
---dump folder              Folder where P4 programs are dumped.
--v                         Increase verbosity level (can be repeated)
---input-packet-only        Only produce the input packet for each test
--- packet-size-range       Specify the possible range of the input packet size in bits. The format is [min]:[max]. The default values are "0:72000". The maximum is set to jumbo frame size (9000 bytes).
---max-tests maxTests       Sets the maximum number of tests to be generated
---out-dir outputDir        Directory for generated tests
---test-backend             Select a test back end. Available test back ends are defined by the respective target.
---packet-size packetSize   If enabled, sets all input packets to a fixed size in bits (from 1 to 12000 bits). 0 implies no packet sizing.
---exploration-strategy     Selects a specific exploration strategy for test generation. Options are: randomAccessStack, linearEnumeration, maxCoverage. Defaults to incrementalStack.
---pop-level                This is the fraction of unexploredBranches we select on randomAccessStack. Defaults to 3.
---linear-enumeration       Max bound for LinearEnumeration strategy. Defaults to 2. **Experimental feature**.
---saddle-point             To be used with randomAccessMaxCoverage. Specifies when to randomly explore the map after a saddle point in the coverage of the test generation.
---with-output-packet       Produced tests must have an output packet.
+./p4testgen: Generate packet tests for a P4 program.
+--help                                       Shows this help message and exits
+--version                                    Prints version information and exits
+--seed seed                                  Provides a randomization seed
+-I path                                      Adds the given path to the preprocessor include path
+--Wwarn diagnostic                           Report a warning for a compiler diagnostic, or treat all warnings as warnings (the default) if no diagnostic is specified.
+-D arg=value                                 Defines a preprocessor symbol
+-U arg                                       Undefines a preprocessor symbol
+-E                                           Preprocess only. Prints preprocessed program on stdout.
+--nocpp                                      Skips the preprocessor; assumes the input file is already preprocessed.
+--std {p4-14|p4-16}                          Specifies source language version.
+-T loglevel                                  Adjusts logging level per file.
+--target target                              Specifies the device targeted by the program.
+--arch arch                                  Specifies the architecture targeted by the program.
+--top4 pass1[,pass2]                         Dump the P4 representation after
+                                             passes whose name contains one of `passX' substrings.
+                                             When '-v' is used this will include the compiler IR.
+--dump folder                                Folder where P4 programs are dumped.
+-v                                           Increase verbosity level (can be repeated)
+--strict                                     Fail on unimplemented features instead of trying the next branch.
+--input-packet-only                          Only produce the input packet for each test.
+--max-tests maxTests                         Sets the maximum number of tests to be generated [default: 1]. Setting the value to 0 will generate tests until no more paths can be found.
+--stop-metric stopMetric                     Stops generating tests when a particular metric is satisifed. Currently supported options are:
+                                             "MAX_STATEMENT_COVERAGE".
+--packet-size-range packetSizeRange          Specify the possible range of the input packet size in bits. The format is [min]:[max]. The default values are "0:72000". The maximum is set to jumbo frame size (9000 bytes).
+--out-dir outputDir                          The output directory for the generated tests. The directory will be created, if it does not exist.
+--test-backend testBackend                   Select the test back end. P4Testgen will produce tests that correspond to the input format of this test back end.
+--input-branches selectedBranches            List of the selected branches which should be chosen for selection.
+--track-branches                             Track the branches that are chosen in the symbolic executor. This can be used for deterministic replay.
+--with-output-packet                         Produced tests must have an output packet.
+--exploration-strategy explorationStrategy   Selects a specific exploration strategy for test generation. Options are: INCREMENTAL_STACK, RANDOM_ACCESS_STACK, LINEAR_ENUMERATION, MAX_COVERAGE, and RANDOM_ACCESS_MAX_COVERAGE. Defaults to INCREMENTAL_STACK.
+--pop-level popLevel                         Sets the fraction for multiPop exploration; default is 3 when meaningful strategy is activated.
+--linear-enumeration linearEnumeration       Max bound for vector size in LINEAR_ENUMERATION; defaults to 2.
+--saddle-point saddlePoint                   Threshold to invoke multiPop on RANDOM_ACCESS_MAX_COVERAGE.
+--print-traces                               Print the associated traces and test information for each generated test.
+--print-steps                                Print the representation of each program node while the stepper steps through the program.
+--print-coverage                             Print detailed statement coverage statistics the interpreter collects while stepping through the program.
+--print-performance-report                   Print timing report summary at the end of the program.
+--dcg DCG                                    Build a DCG for input graph. This control flow graph directed cyclic graph can be used
+                                                     for statement reachability analysis.
+--pattern pattern                            List of the selected branches which should be chosen for selection.
 ```
 
 Once P4Testgen has generated tests, the tests can be executed by either the P4Runtime or STF test back ends.

diff --git a/backends/p4tools/modules/testgen/core/exploration_strategy/linear_enumeration.cpp b/backends/p4tools/modules/testgen/core/exploration_strategy/linear_enumeration.cpp
@@ -55,8 +55,8 @@ void LinearEnumeration::run(const Callback& callback) {
 }
 
 LinearEnumeration::LinearEnumeration(AbstractSolver& solver, const ProgramInfo& programInfo,
-                                     boost::optional<uint32_t> seed, int linearEnumeration)
-    : ExplorationStrategy(solver, programInfo, seed), maxBound(linearEnumeration) {
+                                     boost::optional<uint32_t> seed, uint64_t maxBound)
+    : ExplorationStrategy(solver, programInfo, seed), maxBound(maxBound) {
     // The constructor populates the initial vector of branches holding a terminal state.
     // It fill the vector with a recursive call to mapBranch and stops at maxBound.
     StepResult initialSuccessors = step(*executionState);

diff --git a/backends/p4tools/modules/testgen/core/exploration_strategy/linear_enumeration.h b/backends/p4tools/modules/testgen/core/exploration_strategy/linear_enumeration.h
@@ -28,7 +28,7 @@ class LinearEnumeration : public ExplorationStrategy {
 
     /// Constructor for this strategy, considering inheritance.
     LinearEnumeration(AbstractSolver& solver, const ProgramInfo& programInfo,
-                      boost::optional<uint32_t> seed, int linearEnumeration);
+                      boost::optional<uint32_t> seed, uint64_t maxBound);
 
  protected:
     /// The max size for the exploredBranches vector.

diff --git a/backends/p4tools/modules/testgen/core/exploration_strategy/rnd_access_max_coverage.cpp b/backends/p4tools/modules/testgen/core/exploration_strategy/rnd_access_max_coverage.cpp
@@ -90,7 +90,7 @@ void RandomAccessMaxCoverage::run(const Callback& callback) {
                 bufferUnexploredBranches.erase(coverageKey);
                 next = chooseBranch(successors, guaranteeViability);
             } else {
-                // If we are stuck in a sadlle point for too long,
+                // If we are stuck in a saddle point for too long,
                 // trust in the lookahead and take the higher ranks.
                 if (coverageSaddleTrack.second >= (2 * saddlePoint)) {
                     // Empty unexploredBranches.
@@ -144,6 +144,7 @@ void RandomAccessMaxCoverage::run(const Callback& callback) {
 uint64_t RandomAccessMaxCoverage::getRandomUnexploredMapEntry() {
     // Collect all the keys and select a random one.
     std::vector<uint64_t> unexploredCoverageKeys;
+    unexploredCoverageKeys.reserve(bufferUnexploredBranches.size());
     for (auto const& unexplored : bufferUnexploredBranches) {
         unexploredCoverageKeys.push_back(unexplored.first);
     }
@@ -157,6 +158,7 @@ uint64_t RandomAccessMaxCoverage::getRandomUnexploredMapEntry() {
 void RandomAccessMaxCoverage::updateBufferRankings() {
     // Collect all the keys
     std::vector<uint64_t> unexploredCoverageKeys;
+    unexploredCoverageKeys.reserve(bufferUnexploredBranches.size());
     for (auto const& unexplored : bufferUnexploredBranches) {
         unexploredCoverageKeys.push_back(unexplored.first);
     }
@@ -169,12 +171,11 @@ void RandomAccessMaxCoverage::updateBufferRankings() {
 
 void RandomAccessMaxCoverage::sortBranchesByCoverage(std::vector<Branch>& branches) {
     // Transfers branches to rankedBranches and sorts them by coverage
-    for (uint64_t i = 0; i < branches.size(); i++) {
-        auto localBranch = branches.at(i);
+    for (const auto& localBranch : branches) {
         ExecutionState* branchState = localBranch.nextState;
         // Calculate coverage for each branch:
         uint64_t coverage = 0;
-        if (branchState) {
+        if (branchState != nullptr) {
             uint64_t lookAheadCoverage = 0;
             for (const auto& stmt : branchState->getVisited()) {
                 // We need to take into account the set of visitedStatements.
@@ -246,7 +247,7 @@ ExecutionState* RandomAccessMaxCoverage::chooseBranch(std::vector<Branch>& branc
             }
         }
         // Push the new set of branches if the remaining vector is not empty.
-        if (branches.size() > 0) {
+        if (!branches.empty()) {
             unexploredBranches.push_back(branches);
         }
 

diff --git a/backends/p4tools/modules/testgen/lib/test_backend.cpp b/backends/p4tools/modules/testgen/lib/test_backend.cpp
@@ -116,7 +116,7 @@ bool TestBackEnd::run(const FinalState& state) {
             auto outputPacketSize = executionState->getPacketBufferSize();
             bool packetIsDropped = executionState->getProperty<bool>("drop");
             if (outputPacketSize <= 0 || packetIsDropped) {
-                return testCount > maxTests - 1;
+                return needsToTerminate(testCount);
             }
         }
 
@@ -127,7 +127,7 @@ bool TestBackEnd::run(const FinalState& state) {
             testCount++;
             P4::Coverage::coverageReportFinal(allStatements, visitedStatements);
             printPerformanceReport();
-            return testCount > maxTests - 1;
+            return needsToTerminate(testCount);
         }
         completedModel = concolicModel;
 
@@ -141,17 +141,16 @@ bool TestBackEnd::run(const FinalState& state) {
             symbex.printCurrentTraceAndBranches(selectedBranches);
         }
 
-        abort = printTestInfo(executionState, testInfo, testCount, outputPortExpr);
+        abort = printTestInfo(executionState, testInfo, outputPortExpr);
         if (abort) {
             testCount++;
             P4::Coverage::coverageReportFinal(allStatements, visitedStatements);
             printPerformanceReport();
-            return testCount > maxTests - 1;
+            return needsToTerminate(testCount);
         }
-
         const auto* testSpec = createTestSpec(executionState, completedModel, testInfo);
-
         float coverage = static_cast<float>(visitedStatements.size()) / allStatements.size();
+
         printFeature("test_info", 4,
                      "============ Test %1%: Statements covered: %2% (%3%/%4%) ============",
                      testCount, coverage, visitedStatements.size(), allStatements.size());
@@ -166,7 +165,12 @@ bool TestBackEnd::run(const FinalState& state) {
         testCount++;
         P4::Coverage::coverageReportFinal(allStatements, visitedStatements);
         printPerformanceReport();
-        return testCount > maxTests - 1;
+
+        // If MAX_STATEMENT_COVERAGE is enabled, terminate early if we hit max coverage already.
+        if (TestgenOptions::get().stopMetric == "MAX_STATEMENT_COVERAGE" && coverage == 1.0) {
+            return true;
+        }
+        return needsToTerminate(testCount);
     }
 }
 
@@ -219,7 +223,7 @@ TestBackEnd::TestInfo TestBackEnd::produceTestInfo(
 }
 
 bool TestBackEnd::printTestInfo(const ExecutionState* executionState, const TestInfo& testInfo,
-                                int testCount, const IR::Expression* outputPortExpr) {
+                                const IR::Expression* outputPortExpr) {
     // Print all the important variables and properties of this test.
     printTraces("============ Program trace for Test %1% ============\n", testCount);
     for (const auto& event : testInfo.programTraces) {
@@ -278,7 +282,7 @@ void TestBackEnd::printPerformanceReport() {
     }
 }
 
-int TestBackEnd::getTestCount() { return testCount; }
+int64_t TestBackEnd::getTestCount() const { return testCount; }
 
 }  // namespace P4Testgen