[P4_Symbolic] Extend BMv2 proto with deparser related messages. Fix memory leaks about Z3 assertions.

p4_symbolic/bmv2/bmv2.proto

@@ -243,6 +243,10 @@ message Deparser {
   int32 id = 2;
   // Information on the source code location of the deparser definition.
   SourceLocation source_info = 3;
+  // Ordered list of header instance names from the outer-most header to the
+  // inner-most header. When the target switch invokes a deparser, the headers
+  // will be serialized in this order, and invalid headers will be skipped.
+  repeated string order = 4;
 }
 
 // A pipeline is a sequence of actions and table applications

p4_symbolic/bmv2/expected/basic.pb.txt

@@ -458,6 +458,8 @@ deparsers {
     column: 8
     source_fragment: "MyDeparser"
   }
+  order: "ethernet"
+  order: "ipv4"
 }
 actions {
   name: "NoAction"

p4_symbolic/bmv2/expected/table_hit_1.pb.txt

@@ -278,6 +278,7 @@ deparsers {
     column: 8
     source_fragment: "MyDeparser"
   }
+  order: "ethernet"
 }
 actions {
   name: "MyIngress.drop"

p4_symbolic/bmv2/expected/table_hit_2.pb.txt

@@ -289,6 +289,7 @@ deparsers {
     column: 8
     source_fragment: "MyDeparser"
   }
+  order: "h1"
 }
 actions {
   name: "MyIngress.forward"

p4_symbolic/symbolic/symbolic.cc

@@ -181,13 +181,9 @@ absl::StatusOr<std::unique_ptr<SolverState>> EvaluateP4Pipeline(
       .egress_headers = std::move(egress_headers),
       .trace = std::move(trace),
   };
-  return std::make_unique<SolverState>(SolverState{
-      .program = data_plane.program,
-      .entries = data_plane.entries,
-      .context = std::move(context),
-      .solver = std::move(z3_solver),
-      .translator = std::move(translator),
-  });
+  return std::make_unique<SolverState>(
+      SolverState(data_plane.program, data_plane.entries, std::move(context),
+                  std::move(z3_solver), std::move(translator)));
 }
 
 absl::StatusOr<std::optional<ConcreteContext>> Solve(

p4_symbolic/symbolic/symbolic.h

@@ -204,7 +204,27 @@ struct Dataplane {
 // Only one instance of this struct will be constructed per P4 program
 // evaluation, which can be then used to solve for particular assertions
 // many times.
-struct SolverState {
+class SolverState {
+ public:
+  SolverState(ir::P4Program program, ir::TableEntries entries,
+              SymbolicContext context, std::unique_ptr<z3::solver> solver,
+              values::P4RuntimeTranslator translator)
+      : program(std::move(program)),
+        entries(std::move(entries)),
+        context(std::move(context)),
+        solver(std::move(solver)),
+        translator(std::move(translator)) {}
+  SolverState(const SolverState &) = delete;
+  SolverState(SolverState &&) = default;
+  ~SolverState() {
+    // During the destruction of a z3::solver object, previously added
+    // assertions (through z3::solver::add) sometimes lead to memory leaks. The
+    // exact details of the root cause is not yet clear. Here we explicitly
+    // clear the assertions upon releasing a solver.
+    // See b/285990074 for more details.
+    if (solver) solver->reset();
+  }
+
   // The IR represnetation of the p4 program being analyzed.
   ir::P4Program program;
   // Maps the name of a table to a list of its entries.