[P4_Symbolic] Clean up typos, unused code, and Buildifier warnings. W…

…rite P4-Symbolic IR golden test output to files instead of standard output. Change EvaluateSaiPipeline to depend on the generic parser instead of SAI hardcoded parser

p4_symbolic/ir/BUILD.bazel

@@ -136,6 +136,7 @@ cc_binary(
         "test.cc",
     ],
     deps = [
+        "//gutil:io",
         "//gutil:proto",
         "//p4_symbolic:parser",
         "@com_google_absl//absl/flags:flag",

p4_symbolic/ir/ir.proto

@@ -169,7 +169,7 @@ message ParserTransitionKeyField {
     // Specifies a header field as part of the transition key.
     FieldValue field = 1;
     // Specifies the lookahead value as part of the transition key.
-    // It evalutes to a set of bits from the input packet without advancing the
+    // It evaluates to a set of bits from the input packet without advancing the
     // current read position.
     LookaheadValue lookahead = 2;
   }

p4_symbolic/ir/test.bzl

@@ -74,7 +74,8 @@ def ir_parsing_test(name, p4_program, golden_file, table_entries = None, p4_deps
             ("--bmv2=$(location %s)" % bmv2_file),
             ("--p4info=$(location %s)" % p4info_file),
             ("--entries=$(location %s)" % table_entries if table_entries else ""),
-            "&> $(OUTS) || true",
+            ("--output=$(location %s)" % test_output_file),
+            "|| true",
             # The following line makes sure hexstrings are lowercase in the protobuf file.
             # This is needed because the hexstring representation of boost::multiprecision::cpp_int
             # seems to behave differently accross different versions of boost (although the root

p4_symbolic/ir/test.cc

@@ -14,14 +14,15 @@
 
 // Test file for producing IR representations of P4 Programs.
 
-#include <iostream>
+#include <sstream>
 #include <string>
 
 #include "absl/flags/flag.h"
 #include "absl/flags/parse.h"
 #include "absl/flags/usage.h"
 #include "absl/status/status.h"
 #include "absl/strings/str_format.h"
+#include "gutil/io.h"
 #include "gutil/proto.h"
 #include "p4_symbolic/parser.h"
 
@@ -32,6 +33,7 @@ ABSL_FLAG(std::string, entries, "",
           "The path to the table entries txt file (optional), leave this empty "
           "if the input p4 program contains no (explicit) tables for which "
           "entries are needed.");
+ABSL_FLAG(std::string, output, "", "The output file for parsed IR.");
 
 namespace {
 
@@ -41,24 +43,28 @@ absl::Status Test() {
   const std::string &p4info_path = absl::GetFlag(FLAGS_p4info);
   const std::string &bmv2_path = absl::GetFlag(FLAGS_bmv2);
   const std::string &entries_path = absl::GetFlag(FLAGS_entries);
+  const std::string &output_path = absl::GetFlag(FLAGS_output);
 
   RET_CHECK(!p4info_path.empty());
   RET_CHECK(!bmv2_path.empty());
+  RET_CHECK(!output_path.empty());
 
   // Transform to IR and print.
   ASSIGN_OR_RETURN(
       p4_symbolic::ir::Dataplane dataplane,
       p4_symbolic::ParseToIr(bmv2_path, p4info_path, entries_path));
 
-  // Dump string representation to stdout.
-  std::cout << PrintTextProto(dataplane.program) << std::endl;
+  // Dump string representation to the output file.
+  std::ostringstream output;
+  output << PrintTextProto(dataplane.program) << std::endl;
   for (const auto &[name, entries] : dataplane.entries) {
-    std::cout << "=====" << name << " Entries=====" << std::endl;
-    std::cout << std::endl;
+    output << "=====" << name << " Entries=====" << std::endl;
+    output << std::endl;
     for (const pdpi::IrTableEntry &entry : entries) {
-      std::cout << PrintTextProto(entry) << std::endl;
+      output << PrintTextProto(entry) << std::endl;
     }
   }
+  RETURN_IF_ERROR(gutil::WriteFile(output.str(), output_path));
 
   return absl::OkStatus();
 }
@@ -70,10 +76,10 @@ int main(int argc, char *argv[]) {
   // GOOGLE_PROTOBUF_VERIFY_VERSION;
 
   // Command line arguments and help message.
-  absl::SetProgramUsageMessage(
-      absl::StrFormat("usage: %s %s", argv[0],
-                      "--bmv2=path/to/bmv2.json --p4info=path/to/p4info.pb.txt "
-                      "[--entries=path/to/table_entries.txt]"));
+  absl::SetProgramUsageMessage(absl::StrFormat(
+      "usage: %s %s", argv[0],
+      "--bmv2=path/to/bmv2.json --p4info=path/to/p4info.pb.txt "
+      "--output=path/to/output.txt [--entries=path/to/table_entries.txt]"));
   absl::ParseCommandLine(argc, argv);
 
   // Run test.

p4_symbolic/sai/deparser.cc

@@ -17,16 +17,11 @@
 
 #include <bitset>
 #include <string>
-#include <type_traits>
 
 #include "absl/status/status.h"
 #include "absl/status/statusor.h"
-#include "absl/strings/str_cat.h"
-#include "absl/strings/string_view.h"
-#include "absl/strings/strip.h"
 #include "gutil/status.h"
 #include "p4_pdpi/string_encodings/bit_string.h"
-#include "p4_pdpi/string_encodings/hex_string.h"
 #include "p4_symbolic/sai/fields.h"
 #include "p4_symbolic/symbolic/symbolic.h"
 #include "p4_symbolic/z3_util.h"

p4_symbolic/sai/deparser_test.cc

@@ -115,7 +115,7 @@ TEST_P(SaiDeparserTest, Ipv6TcpPacketParserIntegrationTest) {
                          GetSaiFields(state_->context.ingress_headers));
     state_->solver->add(!fields.headers.ipv4.valid);
     state_->solver->add(fields.headers.tcp.valid);
-    // The only way to have an TCP packet that is not an IPv4 packet is to have
+    // The only way to have a TCP packet that is not an IPv4 packet is to have
     // an IPv6 packet.
   }
 
@@ -213,7 +213,7 @@ TEST_P(SaiDeparserTest, PacketInHeaderIsNeverParsedIntegrationTest) {
     state_->solver->add(fields.headers.packet_in->valid);
   }
 
-  // Should be unsatisifiable, because we never parse a packet-in header.
+  // Should be unsatisfiable, because we never parse a packet-in header.
   ASSERT_EQ(state_->solver->check(), z3::check_result::unsat);
 }
 

p4_symbolic/sai/sai.cc

@@ -92,11 +92,6 @@ absl::StatusOr<std::unique_ptr<symbolic::SolverState>> EvaluateSaiPipeline(
   ASSIGN_OR_RETURN(std::unique_ptr<symbolic::SolverState> state,
                    symbolic::EvaluateP4Program(dataplane, physical_ports,
                                                translation_per_type));
-  ASSIGN_OR_RETURN(std::vector<z3::expr> parser_constraints,
-                   EvaluateSaiParser(state->context.ingress_headers));
-  for (auto& constraint : parser_constraints) {
-    state->solver->add(constraint);
-  }
   return state;
 }
 

p4_symbolic/symbolic/symbolic.h

@@ -78,7 +78,7 @@ using ConcretePerPacketState = absl::btree_map<std::string, std::string>;
 // Then, we will have:
 //    SymbolicMetadata["standard_metadata.ingress_port"] =
 //         <symbolic bit vector of size 9>
-// An instace of this type is passed around and mutated by the functions
+// An instance of this type is passed around and mutated by the functions
 // responsible for symbolically evaluating the program.
 using SymbolicPerPacketState = SymbolicGuardedMap;
 

p4_symbolic/symbolic/table.cc

@@ -67,7 +67,7 @@ int FindMatchWithName(const pdpi::IrTableEntry &entry,
 // Sort the given table entries by priority.
 // Priority depends on the match types.
 // If the matches contain one or more ternary matches, priority is the explicit
-// numeric priority assigned to the the entry.
+// numeric priority assigned to the entry.
 // If no ternary matches exist, and there is *exactly* one lpm match, priority
 // is determined by the length of the prefix to match, such that longer
 // prefixes have higher priority.

p4_symbolic/symbolic/test.bzl

@@ -33,7 +33,9 @@ def end_to_end_test(
         table_entries = None,
         port_count = 2,
         p4_deps = []):
-    """Macro that defines our end to end tests.
+    """
+    Macro that defines our end to end tests.
+
     Given a p4 program, this macro runs our main binary
     on the p4 program and its table entries (if they exist).
     The binary outputs a debugging dump of the underlying smt program,
@@ -49,9 +51,17 @@ def end_to_end_test(
        as given to the macro.
     Use the p4_deps list to specify dependent files that p4_program input
     file depends on (e.g. by including them).
+
+    Args:
+      name: Test name.
+      p4_program: Input P4 program.
+      output_golden_file: File containing the expected output.
+      smt_golden_file: File containing the expected SMT formulae.
+      table_entries: File containing the table entries as input in protobuf text.
+      port_count: Number of ports.
+      p4_deps: List of targets that the P4 program depends on (e.g., included files).
     """
     p4c_name = "%s_p4c" % name
-    run_name = "%s_main" % name
     p4info_file = "%s_bazel-p4c-tmp-output/p4info.pb.txt" % p4c_name
     output_test_name = "%s_output" % name
     smt_test_name = "%s_smt" % name
@@ -60,12 +70,6 @@ def end_to_end_test(
     p4info_file = "tmp/%s.p4info.pb.txt" % name
     test_output_file = "tmp/%s_output" % name
 
-    optional_table_entries = []
-    optional_table_entry_arg = ""
-    if table_entries:
-        optional_table_entries = [table_entries]
-        optional_table_entry_arg = "--entries=$(location %s)" % table_entries
-
     # Run p4c to get bmv2 JSON and p4info.pb.txt files.
     tmp_bmv2_file = "%s.tmp" % bmv2_file
     p4_library(

p4_symbolic/symbolic/util.cc

@@ -35,15 +35,6 @@ namespace util {
 
 namespace {
 
-bool Z3BooltoBool(Z3_lbool z3_bool) {
-  switch (z3_bool) {
-    case Z3_L_TRUE:
-      return true;
-    default:
-      return false;
-  }
-}
-
 // Extract the header field definition of a `field_ref` from the given P4
 // `program`.
 absl::StatusOr<ir::HeaderField> GetFieldDefinition(