[P4Testgen] BMv2 test generation improvements

backends/bmv2/run-bmv2-ptf-test.py

@@ -177,6 +177,7 @@ def run_ptf(self, grpc_port: int, json_name: Path, info_name: Path) -> int:
             return returncode
         test_params = (
             f"grpcaddr='{PTF_ADDR}:{grpc_port}';p4info='{info_name}';config='{json_name}';"
+            f"packet_wait_time='0.1';"
         )
         # TODO: There is currently a bug where we can not support more than 344 ports at once.
         # The nanomsg test back end simply hangs, the reason is unclear.
@@ -240,6 +241,7 @@ def run_ptf(self, grpc_port: int, json_name: Path, info_name: Path) -> int:
         ifaces = self.get_iface_str(num_ifaces=self.options.num_ifaces, prefix="br_")
         test_params = (
             f"grpcaddr='{PTF_ADDR}:{grpc_port}';p4info='{info_name}';config='{json_name}';"
+            f"packet_wait_time='0.1';"
         )
         run_ptf_cmd = (
             f"ptf --pypath {pypath} {ifaces} --log-file {self.options.testdir.joinpath('ptf.log')} "

backends/p4tools/common/core/z3_solver.cpp

@@ -149,11 +149,11 @@ z3::sort Z3Solver::toSort(const IR::Type *type) {
     BUG_CHECK(type, "Z3Solver::toSort with empty pointer");
 
     if (type->is<IR::Type_Boolean>()) {
-        return z3context.bool_sort();
+        return ctx().bool_sort();
     }
 
     if (const auto *bits = type->to<IR::Type_Bits>()) {
-        return z3context.bv_sort(bits->width_bits());
+        return ctx().bv_sort(bits->width_bits());
     }
 
     BUG("Z3Solver: unimplemented type %1%: %2% ", type->node_type_name(), type);
@@ -167,7 +167,7 @@ std::string Z3Solver::generateName(const IR::SymbolicVariable &var) {
 
 z3::expr Z3Solver::declareVar(const IR::SymbolicVariable &var) {
     auto sort = toSort(var.type);
-    auto expr = z3context.constant(generateName(var).c_str(), sort);
+    auto expr = ctx().constant(generateName(var).c_str(), sort);
     BUG_CHECK(
         !declaredVarsById.empty(),
         "DeclaredVarsById should have at least one entry! Check if push() was used correctly.");
@@ -184,12 +184,24 @@ void Z3Solver::reset() {
     z3Assertions.resize(0);
 }
 
+void Z3Solver::clearMemory() {
+    auto p4AssertionsBuf = p4Assertions;
+    reset();
+    Z3_finalize_memory();
+    z3solver = z3::solver(*new z3::context());
+    p4Assertions.clear();
+    for (const auto &assert : p4AssertionsBuf) {
+        push();
+        asrt(assert);
+    }
+}
+
 void Z3Solver::push() {
     if (isIncremental) {
         z3solver.push();
     }
     checkpoints.push_back(p4Assertions.size());
-    declaredVarsById.push_back({});
+    declaredVarsById.emplace_back();
 }
 
 void Z3Solver::pop() {
@@ -230,6 +242,7 @@ void Z3Solver::comment(cstring commentStr) {
 
 void Z3Solver::seed(unsigned seed) {
     Z3_LOG("set a new seed:'%d'", seed);
+    auto &z3context = z3solver.ctx();
     z3::params param(z3context);
     param.set("phase_selection", 5U);
     param.set("random_seed", seed);
@@ -239,13 +252,15 @@ void Z3Solver::seed(unsigned seed) {
 
 void Z3Solver::timeout(unsigned tm) {
     Z3_LOG("set a timeout:'%d'", tm);
+    auto &z3context = z3solver.ctx();
     z3::params param(z3context);
     param.set(":timeout", tm);
     z3solver.set(param);
     timeout_ = tm;
 }
 
 std::optional<bool> Z3Solver::checkSat(const std::vector<const Constraint *> &asserts) {
+    Util::ScopedTimer ctZ3("z3");
     if (isIncremental) {
         // Find common prefix with the previous invocation's list of assertions
         auto from = asserts.begin();
@@ -267,7 +282,6 @@ std::optional<bool> Z3Solver::checkSat(const std::vector<const Constraint *> &as
     }
     Z3_LOG("checking satisfiability for %d assertions",
            isIncremental ? z3solver.assertions().size() : z3Assertions.size());
-    Util::ScopedTimer ctZ3("z3");
     Util::ScopedTimer ctCheckSat("checkSat");
     z3::check_result result = isIncremental ? z3solver.check() : z3solver.check(z3Assertions);
     switch (result) {
@@ -306,6 +320,7 @@ void Z3Solver::asrt(const Constraint *assertion) {
 }
 
 const SymbolicMapping &Z3Solver::getSymbolicMapping() const {
+    Util::ScopedTimer ctZ3("z3");
     auto *result = new SymbolicMapping();
     // First, collect a map of all the declared variables we have encountered in the stack.
     std::map<unsigned int, const IR::SymbolicVariable *> declaredVars;
@@ -317,7 +332,6 @@ const SymbolicMapping &Z3Solver::getSymbolicMapping() const {
     }
     // Then, get the model and match each declaration in the model to its IR::SymbolicVariable.
     try {
-        Util::ScopedTimer ctZ3("z3");
         Util::ScopedTimer ctCheckSat("getModel");
         auto z3Model = z3solver.get_model();
         Z3_LOG("z3 model:%s", toString(z3Model));
@@ -400,12 +414,14 @@ void Z3Solver::addZ3Pushes(size_t &chkIndex, size_t asrtIndex) {
 
 const z3::solver &Z3Solver::getZ3Solver() const { return z3solver; }
 
-const z3::context &Z3Solver::getZ3Ctx() const { return z3context; }
+const z3::context &Z3Solver::getZ3Ctx() const { return z3solver.ctx(); }
+
+z3::context &Z3Solver::ctx() const { return z3solver.ctx(); }
 
 bool Z3Solver::isInIncrementalMode() const { return isIncremental; }
 
 Z3Solver::Z3Solver(bool isIncremental, std::optional<std::istream *> inOpt)
-    : z3solver(z3context), isIncremental(isIncremental), z3Assertions(z3context) {
+    : z3solver(*new z3::context), isIncremental(isIncremental), z3Assertions(ctx()) {
     // Add a top-level set to declaration vars that we can insert variables.
     // TODO: Think about whether this is necessary or it is not better to remove it.
     declaredVarsById.emplace_back();
@@ -434,7 +450,7 @@ Z3Solver::Z3Solver(bool isIncremental, std::optional<std::istream *> inOpt)
     addZ3Pushes(chkIndex, assertions.size());
 }
 
-Z3Translator::Z3Translator(Z3Solver &solver) : result(solver.z3context), solver(solver) {}
+Z3Translator::Z3Translator(Z3Solver &solver) : result(solver.ctx()), solver(solver) {}
 
 bool Z3Translator::preorder(const IR::Node *node) {
     BUG("%1%: Unhandled node type: %2%", node, node->node_type_name());
@@ -452,8 +468,8 @@ bool Z3Translator::preorder(const IR::Cast *cast) {
             exprSize = exprType->width_bits();
         } else if (castExtrType->is<IR::Type_Boolean>()) {
             exprSize = 1;
-            auto trueVal = solver.z3context.bv_val(1, exprSize);
-            auto falseVal = solver.z3context.bv_val(0, exprSize);
+            auto trueVal = solver.ctx().bv_val(1, exprSize);
+            auto falseVal = solver.ctx().bv_val(0, exprSize);
             castExpr = z3::ite(castExpr, trueVal, falseVal);
         } else if (const auto *exprType = castExtrType->to<IR::Extracted_Varbits>()) {
             exprSize = exprType->width_bits();
@@ -477,7 +493,7 @@ bool Z3Translator::preorder(const IR::Cast *cast) {
     if (cast->destType->is<IR::Type_Boolean>()) {
         if (const auto *exprType = castExtrType->to<IR::Type_Bits>()) {
             if (exprType->width_bits() == 1) {
-                castExpr = z3::operator==(castExpr, solver.z3context.bv_val(1, 1));
+                castExpr = z3::operator==(castExpr, solver.ctx().bv_val(1, 1));
             } else {
                 BUG("Cast expression type %1% is not bit<1> : %2%", exprType, castExpr);
             }
@@ -495,31 +511,31 @@ bool Z3Translator::preorder(const IR::Cast *cast) {
 bool Z3Translator::preorder(const IR::Constant *constant) {
     // Handle infinite-integer constants.
     if (constant->type->is<IR::Type_InfInt>()) {
-        result = solver.z3context.int_val(constant->value.str().c_str());
+        result = solver.ctx().int_val(constant->value.str().c_str());
         return false;
     }
 
     // Handle bit<n> constants.
     if (const auto *bits = constant->type->to<IR::Type_Bits>()) {
-        result = solver.z3context.bv_val(constant->value.str().c_str(), bits->size);
+        result = solver.ctx().bv_val(constant->value.str().c_str(), bits->size);
         return false;
     }
 
     if (const auto *bits = constant->type->to<IR::Extracted_Varbits>()) {
-        result = solver.z3context.bv_val(constant->value.str().c_str(), bits->width_bits());
+        result = solver.ctx().bv_val(constant->value.str().c_str(), bits->width_bits());
         return false;
     }
 
     BUG("Z3Translator: unsupported type for constant %1%", constant);
 }
 
 bool Z3Translator::preorder(const IR::BoolLiteral *boolLiteral) {
-    result = solver.z3context.bool_val(boolLiteral->value);
+    result = solver.ctx().bool_val(boolLiteral->value);
     return false;
 }
 
 bool Z3Translator::preorder(const IR::StringLiteral *stringLiteral) {
-    result = solver.z3context.string_const(stringLiteral->value);
+    result = solver.ctx().string_const(stringLiteral->value);
     return false;
 }
 

backends/p4tools/common/core/z3_solver.h

@@ -58,7 +58,6 @@ class Z3Solver : public AbstractSolver {
     /// @returns the list of active assertions on this solver.
     [[nodiscard]] safe_vector<const Constraint *> getAssertions() const;
 
- private:
     /// Resets the internal state: pops all assertions from previous solver
     /// invocation, removes variable declarations.
     void reset();
@@ -69,12 +68,20 @@ class Z3Solver : public AbstractSolver {
     /// Removes the last solver context.
     void pop();
 
+    /// Reset the internal Z3 solver state (memory and active assertions).
+    /// In incremental state, all active assertions are reapplied after resetting.
+    void clearMemory();
+
+ private:
     /// Inserts an assertion into the topmost solver context.
     void asrt(const Constraint *assertion);
 
     /// Converts a P4 type to a Z3 sort.
     z3::sort toSort(const IR::Type *type);
 
+    /// Get the actual Z3 context that this class uses. This context can be manipulated.
+    [[nodiscard]] z3::context &ctx() const;
+
     /// Declares the given symbolic variable to Z3.
     ///
     /// @returns the resulting Z3 variable.
@@ -94,9 +101,6 @@ class Z3Solver : public AbstractSolver {
     /// Helps to restore a state of incremental solver in a constructor.
     void addZ3Pushes(size_t &chkIndex, size_t asrtIndex);
 
-    /// Main Z3 context.
-    z3::context z3context;
-
     /// The underlying Z3 instance.
     z3::solver z3solver;
 

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

@@ -23,8 +23,12 @@
 namespace P4Tools::P4Testgen {
 
 SymbolicExecutor::StepResult SymbolicExecutor::step(ExecutionState &state) {
-    Util::ScopedTimer st("step");
-    StepResult successors = evaluator.step(state);
+    StepResult successors = nullptr;
+    // Use a scope here to measure the time it takes for a step.
+    {
+        Util::ScopedTimer st("step");
+        successors = evaluator.step(state);
+    }
     // Remove any successors that are unsatisfiable.
     successors->erase(
         std::remove_if(successors->begin(), successors->end(),

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

@@ -1,5 +1,7 @@
 #include "backends/p4tools/modules/testgen/lib/test_backend.h"
 
+#include <backends/p4tools/common/core/z3_solver.h>
+
 #include <iostream>
 #include <optional>
 
@@ -55,6 +57,14 @@ bool TestBackEnd::run(const FinalState &state) {
                          "AssertionMode: Found an input that triggers an assertion.");
         }
 
+        // For long-running tests periodically reset the solver state to free up memory.
+        if (testCount != 0 && testCount % RESET_THRESHOLD == 0) {
+            auto &solver = state.getSolver();
+            auto *z3Solver = solver.to<Z3Solver>();
+            CHECK_NULL(z3Solver);
+            z3Solver->clearMemory();
+        }
+
         bool abort = false;
 
         // Execute concolic functions that may occur in the output packet, the output port,

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

@@ -25,6 +25,9 @@ class TestBackEnd {
     /// The current test count. If it exceeds @var maxTests, the symbolic executor will stop.
     int64_t testCount = 0;
 
+    /// 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;

backends/p4tools/modules/testgen/targets/bmv2/backend/ptf/ptf.cpp

@@ -248,6 +248,12 @@ class AbstractTest(bt.P4RuntimeTest):
         bt.P4RuntimeTest.setUp(self)
         success = bt.P4RuntimeTest.updateConfig(self)
         assert success
+        packet_wait_time = ptfutils.test_param_get("packet_wait_time")
+        if not packet_wait_time:
+            self.packet_wait_time = 0.1
+        else:
+            self.packet_wait_time = float(packet_wait_time)
+
 
     def tearDown(self):
         bt.P4RuntimeTest.tearDown(self)
@@ -404,10 +410,10 @@ class Test{{test_id}}(AbstractTest):
 ## else 
         ptfutils.verify_packet(self, exp_pkt, eg_port)
         bt.testutils.log.info("Verifying no other packets ...")
-        ptfutils.verify_no_other_packets(self, self.device_id, timeout=2)
+        ptfutils.verify_no_other_packets(self, self.device_id, timeout=self.packet_wait_time)
 ## endif
 ## else
-        ptfutils.verify_no_other_packets(self, self.device_id, timeout=2)
+        ptfutils.verify_no_other_packets(self, self.device_id, timeout=self.packet_wait_time)
 ## endif
 
     def runTest(self):

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

@@ -512,17 +512,23 @@ const IR::Node *AssertsParser::postorder(IR::P4Table *node) {
         return node;
     }
 
+    Z3Solver solver;
     for (const auto *restrStr : annotation->body) {
         auto restrictions =
             genIRStructs(node->controlPlaneName(), restrStr->text, key->keyElements);
-        /// Using Z3Solver, we check the feasibility of restrictions, if they are not
-        /// feasible, we delete keys and entries from the table to execute
-        /// default_action
-        Z3Solver solver;
+        // Using Z3Solver, we check the feasibility of restrictions, if they are not
+        // feasible, we delete keys and entries from the table to execute
+        // default_action
+        solver.push();
         if (solver.checkSat(restrictions) == true) {
             restrictionsVec.push_back(restrictions);
             continue;
         }
+        ::warning(
+            "Restriction %1% is not feasible. Not generating entries for table %2% and instead "
+            "using default action.",
+            restrStr, node);
+        solver.pop();
         auto *cloneTable = node->clone();
         auto *cloneProperties = node->properties->clone();
         IR::IndexedVector<IR::Property> properties;

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

@@ -1,7 +1,6 @@
 #include "backends/p4tools/modules/testgen/targets/bmv2/p4_refers_to_parser.h"
 
-#include <stddef.h>
-
+#include <cstddef>
 #include <cstdint>
 #include <iostream>
 #include <string>
@@ -13,7 +12,6 @@
 #include "ir/ir.h"
 #include "ir/vector.h"
 #include "lib/exceptions.h"
-#include "lib/log.h"
 #include "lib/null.h"
 
 namespace P4Tools::RefersToParser {
@@ -34,7 +32,7 @@ void RefersToParser::createConstraint(bool table, cstring currentName, cstring c
     } else {
         tmp = currentName + currentKeyName;
     }
-    auto left = ToolsVariables::getSymbolicVariable(type, tmp);
+    const auto *left = ToolsVariables::getSymbolicVariable(type, tmp);
     std::string str = currentName.c_str();
     std::vector<std::string> elems;
     std::stringstream ss(str);
@@ -47,7 +45,7 @@ void RefersToParser::createConstraint(bool table, cstring currentName, cstring c
         str += elems[i] + ".";
     }
     tmp = str + destTableName + "_key_" + destKeyName;
-    auto right = ToolsVariables::getSymbolicVariable(type, tmp);
+    const auto *right = ToolsVariables::getSymbolicVariable(type, tmp);
     auto *expr = new IR::Equ(left, right);
     std::vector<const IR::Expression *> constraint;
     constraint.push_back(expr);
@@ -64,9 +62,6 @@ cstring buildName(IR::Vector<IR::AnnotationToken> input) {
     return result;
 }
 
-/// An intermediate function that determines the type for future variables and partially
-/// collects their names for them, after which it calls the createConstraint function,
-/// which completes the construction of the constraint
 void RefersToParser::createRefersToConstraint(const IR::Annotation *annotation,
                                               const IR::Type *inputType, cstring controlPlaneName,
                                               bool isParameter, cstring inputName) {