Remove nondeterminism in P4Testgen.

backends/p4tools/common/core/z3_solver.cpp

@@ -248,7 +248,6 @@ void Z3Solver::seed(unsigned seed) {
     z3::params param(z3context);
     param.set("phase_selection", 5U);
     param.set("random_seed", seed);
-    param.set("arith.random_initial_value", true);
     z3solver.set(param);
     seed_ = seed;
 }

backends/p4tools/common/lib/util.cpp

@@ -36,7 +36,7 @@ namespace P4Tools {
 
 boost::optional<uint32_t> Utils::currentSeed = boost::none;
 
-boost::random::mt19937 Utils::rng;
+boost::random::mt19937 Utils::rng(0);
 
 std::string Utils::getTimeStamp() {
     // get current time
@@ -56,6 +56,9 @@ std::string Utils::getTimeStamp() {
 }
 
 void Utils::setRandomSeed(int seed) {
+    if (currentSeed) {
+        BUG("Seed already initialized with %1%.", currentSeed.get());
+    }
     currentSeed = seed;
     rng.seed(seed);
 }

backends/p4tools/common/options.cpp

@@ -10,6 +10,7 @@
 
 #include "backends/p4tools/common/compiler/compiler_target.h"
 #include "backends/p4tools/common/core/target.h"
+#include "backends/p4tools/common/lib/util.h"
 #include "backends/p4tools/common/version.h"
 #include "frontends/common/parser_options.h"
 #include "lib/error.h"
@@ -170,6 +171,8 @@ AbstractP4cToolOptions::AbstractP4cToolOptions(cstring message) : Options(messag
         "--seed", "seed",
         [this](const char* arg) {
             seed = std::stoul(arg);
+            // Initialize the global seed for randomness.
+            Utils::setRandomSeed(*seed);
             return true;
         },
         "Provides a randomization seed");

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

@@ -98,13 +98,13 @@ bool ExplorationStrategy::handleTerminalState(const Callback& callback,
     return callback(finalState);
 }
 
-ExplorationStrategy::ExplorationStrategy(AbstractSolver& solver, const ProgramInfo& programInfo,
-                                         boost::optional<uint32_t> seed)
+ExplorationStrategy::ExplorationStrategy(AbstractSolver& solver, const ProgramInfo& programInfo)
     : programInfo(programInfo),
       solver(solver),
       allStatements(programInfo.getAllStatements()),
       evaluator(solver, programInfo) {
     // If there is no seed provided, do not randomize the solver.
+    auto seed = Utils::getCurrentSeed();
     if (seed != boost::none) {
         this->solver.seed(*seed);
     }

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

@@ -49,8 +49,7 @@ class ExplorationStrategy {
     /// TODO there is a lot of code repetition in subclasses. Refactor and extract duplicates.
     virtual void run(const Callback& callBack) = 0;
 
-    explicit ExplorationStrategy(AbstractSolver& solver, const ProgramInfo& programInfo,
-                                 boost::optional<uint32_t> seed);
+    explicit ExplorationStrategy(AbstractSolver& solver, const ProgramInfo& programInfo);
 
     /// Writes a list of the selected branches into @param out.
     void printCurrentTraceAndBranches(std::ostream& out);

backends/p4tools/modules/testgen/core/exploration_strategy/inc_max_coverage_stack.cpp

@@ -82,18 +82,16 @@ void IncrementalMaxCoverageStack::run(const Callback& callback) {
 }
 
 IncrementalMaxCoverageStack::IncrementalMaxCoverageStack(AbstractSolver& solver,
-                                                         const ProgramInfo& programInfo,
-                                                         boost::optional<uint32_t> seed)
-    : ExplorationStrategy(solver, programInfo, seed) {}
+                                                         const ProgramInfo& programInfo)
+    : ExplorationStrategy(solver, programInfo) {}
 
 void IncrementalMaxCoverageStack::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.
@@ -178,7 +176,7 @@ ExecutionState* IncrementalMaxCoverageStack::chooseBranch(std::vector<Branch>& b
             }
         }
         // Push the new set of branches if the remaining vector is not empty.
-        if (branches.size() > 0) {
+        if (!branches.empty()) {
             auto coverageKey = unexploredBranches.find(localCoverage);
             coverageKey->second = branches;
         } else {

backends/p4tools/modules/testgen/core/exploration_strategy/inc_max_coverage_stack.h

@@ -39,14 +39,13 @@ class IncrementalMaxCoverageStack : public ExplorationStrategy {
     void run(const Callback& callBack) override;
 
     /// Constructor for this strategy, considering inheritance.
-    IncrementalMaxCoverageStack(AbstractSolver& solver, const ProgramInfo& programInfo,
-                                boost::optional<uint32_t> seed);
+    IncrementalMaxCoverageStack(AbstractSolver& solver, const ProgramInfo& programInfo);
 
  protected:
     /// The main datastructure for exploration in this strategy. It is a map
     /// of pairs, and each pair carries the potential coverage and a vector of
     /// branches with that same coverage.
-    std::map<uint64_t, std::vector<Branch>> unexploredBranches;
+    ordered_map<uint64_t, std::vector<Branch>> unexploredBranches;
 
     /// Chooses a branch to take, sets the current execution state to be that branch, and asserts
     /// the corresponding path constraint to the solver.

backends/p4tools/modules/testgen/core/exploration_strategy/incremental_stack.cpp

@@ -72,9 +72,8 @@ void IncrementalStack::run(const Callback& callback) {
     }
 }
 
-IncrementalStack::IncrementalStack(AbstractSolver& solver, const ProgramInfo& programInfo,
-                                   boost::optional<uint32_t> seed)
-    : ExplorationStrategy(solver, programInfo, seed) {}
+IncrementalStack::IncrementalStack(AbstractSolver& solver, const ProgramInfo& programInfo)
+    : ExplorationStrategy(solver, programInfo) {}
 
 ExecutionState* IncrementalStack::chooseBranch(std::vector<Branch>& branches,
                                                bool guaranteeViability) {

backends/p4tools/modules/testgen/core/exploration_strategy/incremental_stack.h

@@ -30,16 +30,15 @@ class IncrementalStack : public ExplorationStrategy {
     void run(const Callback& callBack) override;
 
     /// Constructor for this strategy, considering inheritance
-    IncrementalStack(AbstractSolver& solver, const ProgramInfo& programInfo,
-                     boost::optional<uint32_t> seed);
+    IncrementalStack(AbstractSolver& solver, const ProgramInfo& programInfo);
 
  protected:
     /// Encapsulates a stack of unexplored branches. This exists to help enforce the invariant that
     /// any push or pop operation on this stack should be paired with a corresponding push/pop
     /// operation on the solver.
     class UnexploredBranches {
      public:
-        bool empty() const;
+        [[nodiscard]] bool empty() const;
         void push(StepResult branches);
         StepResult pop();
         size_t size();

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, uint64_t maxBound)
-    : ExplorationStrategy(solver, programInfo, seed), maxBound(maxBound) {
+                                     uint64_t maxBound)
+    : ExplorationStrategy(solver, programInfo), 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);

backends/p4tools/modules/testgen/core/exploration_strategy/linear_enumeration.h

@@ -27,8 +27,7 @@ class LinearEnumeration : public ExplorationStrategy {
     void run(const Callback& callBack) override;
 
     /// Constructor for this strategy, considering inheritance.
-    LinearEnumeration(AbstractSolver& solver, const ProgramInfo& programInfo,
-                      boost::optional<uint32_t> seed, uint64_t maxBound);
+    LinearEnumeration(AbstractSolver& solver, const ProgramInfo& programInfo, uint64_t maxBound);
 
  protected:
     /// The max size for the exploredBranches vector.

backends/p4tools/modules/testgen/core/exploration_strategy/random_access_stack.cpp

@@ -82,14 +82,14 @@ void RandomAccessStack::run(const Callback& callback) {
 }
 
 RandomAccessStack::RandomAccessStack(AbstractSolver& solver, const ProgramInfo& programInfo,
-                                     boost::optional<uint32_t> seed, int popLevel)
-    : IncrementalStack(solver, programInfo, seed), popLevel(popLevel) {}
+                                     uint64_t popLevel)
+    : IncrementalStack(solver, programInfo), popLevel(popLevel) {}
 
 RandomAccessStack::StepResult RandomAccessStack::multiPop(
     IncrementalStack::UnexploredBranches& unexploredBranches) {
     // A good spot seems to be 10 per cent of the paths. Needs better stats.
-    size_t unexploredRange = unexploredBranches.size() / popLevel;
-    uint64_t popLevels = Utils::getRandInt(unexploredRange) + 1;
+    auto unexploredRange = unexploredBranches.size() / popLevel;
+    auto popLevels = Utils::getRandInt(unexploredRange) + 1;
     // Saves unexploredBranches in the buffer if we are popping more
     // than one level to revist them later.
     if (popLevels == 1) {

backends/p4tools/modules/testgen/core/exploration_strategy/random_access_stack.h

@@ -25,16 +25,15 @@ class RandomAccessStack : public IncrementalStack {
     /// Executes the P4 program along a randomly chosen path. When the program terminates, the
     /// given callback is invoked. If the callback returns true, then the executor terminates.
     /// Otherwise, execution of the P4 program continues on a different random path.
-    void run(const Callback& callBack);
+    void run(const Callback& callBack) override;
 
     /// Constructor for this strategy, considering inheritance
-    RandomAccessStack(AbstractSolver& solver, const ProgramInfo& programInfo,
-                      boost::optional<uint32_t> seed, int popLevel);
+    RandomAccessStack(AbstractSolver& solver, const ProgramInfo& programInfo, uint64_t popLevel);
 
  private:
     // The fraction in which we'll explore the depth of the stack. The higher the
     // number, the smaller the step.
-    int popLevel;
+    uint64_t popLevel;
 
     // Buffer of unexploredBranches. It saves the unexplored branches,
     // so we can restore them if multiPop empties the current unexploredBranches

backends/p4tools/modules/testgen/core/exploration_strategy/rnd_access_max_coverage.cpp

@@ -205,7 +205,7 @@ void RandomAccessMaxCoverage::sortBranchesByCoverage(std::vector<Branch>& branch
         }
     }
 
-    // Clear branches and reinsert information from rankedBranches
+    // Clear branches and reinsert information from rankedBranches.
     branches.clear();
 }
 
@@ -257,9 +257,8 @@ ExecutionState* RandomAccessMaxCoverage::chooseBranch(std::vector<Branch>& branc
 
 RandomAccessMaxCoverage::RandomAccessMaxCoverage(AbstractSolver& solver,
                                                  const ProgramInfo& programInfo,
-                                                 boost::optional<uint32_t> seed,
                                                  uint64_t saddlePoint)
-    : IncrementalMaxCoverageStack(solver, programInfo, seed), saddlePoint(saddlePoint) {}
+    : IncrementalMaxCoverageStack(solver, programInfo), saddlePoint(saddlePoint) {}
 
 }  // namespace P4Testgen
 

backends/p4tools/modules/testgen/core/exploration_strategy/rnd_access_max_coverage.h

@@ -35,7 +35,7 @@ class RandomAccessMaxCoverage : public IncrementalMaxCoverageStack {
 
     /// Constructor for this strategy, considering inheritance.
     RandomAccessMaxCoverage(AbstractSolver& solver, const ProgramInfo& programInfo,
-                            boost::optional<uint32_t> seed, uint64_t saddlePoint);
+                            uint64_t saddlePoint);
 
  protected:
     // Saddle point indicates when we get stuck into a coverage and decides to take
@@ -57,7 +57,7 @@ class RandomAccessMaxCoverage : public IncrementalMaxCoverageStack {
     // Buffer of unexploredBranches. It saves the unexplored branches,
     // so we can restore them if getRandomUnexploredMapEntry finishes a path
     // in unexploredBranches.
-    std::map<uint64_t, std::vector<Branch>> bufferUnexploredBranches;
+    ordered_map<uint64_t, std::vector<Branch>> bufferUnexploredBranches;
 
     /// Chooses a branch to take, sets the current execution state to be that branch, and asserts
     /// the corresponding path constraint to the solver.

backends/p4tools/modules/testgen/core/exploration_strategy/selected_branches.cpp

@@ -62,8 +62,8 @@ uint64_t getNumeric(const std::string& str) {
 }
 
 SelectedBranches::SelectedBranches(AbstractSolver& solver, const ProgramInfo& programInfo,
-                                   boost::optional<uint32_t> seed, std::string selectedBranchesStr)
-    : ExplorationStrategy(solver, programInfo, seed) {
+                                   std::string selectedBranchesStr)
+    : ExplorationStrategy(solver, programInfo) {
     size_t n = 0;
     auto str = std::move(selectedBranchesStr);
     while ((n = str.find(',')) != std::string::npos) {

backends/p4tools/modules/testgen/core/exploration_strategy/selected_branches.h

@@ -28,7 +28,7 @@ class SelectedBranches : public ExplorationStrategy {
 
     /// Constructor for this strategy, considering inheritance
     SelectedBranches(AbstractSolver& solver, const ProgramInfo& programInfo,
-                     boost::optional<uint32_t> seed, std::string selectedBranchesStr);
+                     std::string selectedBranchesStr);
 
  private:
     /// Chooses a branch corresponding to a given branch identifier.

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

@@ -29,10 +29,10 @@ namespace P4Testgen {
 /// TODO: This is a very ugly data structure. Essentially, you can store both state variables and
 /// entire expression as keys. State variables can actually compared, expressions are always unique
 /// keys. Using this map, you can look up particular state variables and check whether they actually
-/// are present, but not expressions. The reason expressions need to be keys is that some times
+/// are present, but not expressions. The reason expressions need to be keys is that sometimes
 /// entire expressions are mapped to a particular constant.
 using ConcolicVariableMap =
-    std::map<boost::variant<const StateVariable, const IR::Expression*>, const IR::Expression*>;
+    ordered_map<boost::variant<const StateVariable, const IR::Expression*>, const IR::Expression*>;
 
 /// Encapsulates a set of concolic method implementations.
 class ConcolicMethodImpls {
@@ -41,7 +41,8 @@ class ConcolicMethodImpls {
         cstring concolicMethodName, const IR::ConcolicVariable* var, const ExecutionState& state,
         const Model* completedModel, ConcolicVariableMap* resolvedConcolicVariables)>;
 
-    std::map<cstring, std::map<uint, std::list<std::pair<std::vector<cstring>, MethodImpl>>>> impls;
+    ordered_map<cstring, ordered_map<uint, std::list<std::pair<std::vector<cstring>, MethodImpl>>>>
+        impls;
 
     static bool matches(const std::vector<cstring>& paramNames,
                         const IR::Vector<IR::Argument>* args);

backends/p4tools/modules/testgen/targets/bmv2/test/BMV2Xfail.cmake

@@ -90,8 +90,6 @@ p4tools_add_xfail_reason(
 p4tools_add_xfail_reason(
   "testgen-p4c-bmv2"
   "differs|Expected ([0-9]+) packets on port ([0-9]+) got ([0-9]+)"
-  # Difficult to reproduce bug in the checksum calculation.
-  checksum-l4-bmv2.p4
 )
 
 p4tools_add_xfail_reason(

backends/p4tools/modules/testgen/testgen.cpp

@@ -65,7 +65,10 @@ int Testgen::mainImpl(const IR::P4Program* program) {
     auto const inputFile = P4CContext::get().options().file;
     const auto& testgenOptions = TestgenOptions::get();
     cstring testDirStr = testgenOptions.outputDir;
-    auto seed = testgenOptions.seed;
+    auto seed = Utils::getCurrentSeed();
+    if (seed) {
+        printFeature("test_info", 4, "============ Program seed %1% =============\n", *seed);
+    }
 
     // Get the basename of the input file and remove the extension
     // This assumes that inputFile is not null.
@@ -78,15 +81,9 @@ int Testgen::mainImpl(const IR::P4Program* program) {
         testPath = fs::path(testDir) / testPath;
     }
 
-    if (seed != boost::none) {
-        // Initialize the global seed for randomness.
-        Utils::setRandomSeed(*seed);
-        printFeature("test_info", 4, "============ Program seed %1% =============\n", *seed);
-    }
-
     Z3Solver solver;
 
-    auto* symExec = [&solver, &programInfo, seed, &testgenOptions]() -> ExplorationStrategy* {
+    auto* symExec = [&solver, &programInfo, &testgenOptions]() -> ExplorationStrategy* {
         auto explorationStrategy = testgenOptions.explorationStrategy;
         if (explorationStrategy == "RANDOM_ACCESS_STACK") {
             // If the user mistakenly specifies an invalid popLevel, we set it to 3.
@@ -95,24 +92,22 @@ int Testgen::mainImpl(const IR::P4Program* program) {
                 ::warning("--pop-level must be greater than 1; using default value of 3.\n");
                 popLevel = 3;
             }
-            return new RandomAccessStack(solver, *programInfo, seed, popLevel);
+            return new RandomAccessStack(solver, *programInfo, popLevel);
         }
         if (explorationStrategy == "LINEAR_ENUMERATION") {
-            return new LinearEnumeration(solver, *programInfo, seed,
-                                         testgenOptions.linearEnumeration);
+            return new LinearEnumeration(solver, *programInfo, testgenOptions.linearEnumeration);
         }
         if (explorationStrategy == "MAX_COVERAGE") {
-            return new IncrementalMaxCoverageStack(solver, *programInfo, seed);
+            return new IncrementalMaxCoverageStack(solver, *programInfo);
         }
         if (explorationStrategy == "RANDOM_ACCESS_MAX_COVERAGE") {
-            return new RandomAccessMaxCoverage(solver, *programInfo, seed,
-                                               testgenOptions.saddlePoint);
+            return new RandomAccessMaxCoverage(solver, *programInfo, testgenOptions.saddlePoint);
         }
         if (!testgenOptions.selectedBranches.empty()) {
             std::string selectedBranchesStr = testgenOptions.selectedBranches;
-            return new SelectedBranches(solver, *programInfo, seed, selectedBranchesStr);
+            return new SelectedBranches(solver, *programInfo, selectedBranchesStr);
         }
-        return new IncrementalStack(solver, *programInfo, seed);
+        return new IncrementalStack(solver, *programInfo);
     }();
 
     // Define how to handle the final state for each test. This is target defined.