Adding files in p4_symbolic (sonic-net#519)

p4_symbolic/symbolic/test.bzl

@@ -0,0 +1,124 @@
+# Copyright 2024 Google LLC
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#      http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+"""Rules for testing p4-symbolic.
+
+This file contains rule definitions for running
+the test binary to produce output json and protobuf files,
+subset diff the input and output json files, and golden file
+testing the output protobuf files against the expected files.
+It also defines a Macro that simplifies defining a protobuf test
+over a sample P4 program.
+"""
+
+load("@com_github_p4lang_p4c//:bazel/p4_library.bzl", "p4_library")
+load("//p4_pdpi/testing:diff_test.bzl", "diff_test")
+
+def end_to_end_test(
+        name,
+        p4_program,
+        output_golden_file,
+        smt_golden_file,
+        table_entries = None,
+        p4_deps = []):
+    """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,
+    as well as the output test packets.
+    The macro compares both of these outputs against the provided
+    expected golden files.
+    The macro defines these rules in order:
+    1. A rule for producing bmv2 json and p4info files from a .p4 file using p4c.
+    2. A rule for running the main binary on the inputs using p4_symbolic/main.cc,
+       and dumping both output files.
+    3. Two rules for golden file testing of the two output files.
+    4. A test suite combining the two rules above with the same name
+       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).
+    """
+    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
+
+    bmv2_file = "tmp/%s.bmv2.json" % name
+    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(
+        name = p4c_name,
+        src = p4_program,
+        deps = p4_deps,
+        target = "bmv2",
+        target_out = tmp_bmv2_file,
+        p4info_out = p4info_file,
+    )
+    native.genrule(
+        name = "%s_strip_files_paths_for_portability" % name,
+        visibility = ["//visibility:private"],
+        srcs = [tmp_bmv2_file],
+        outs = [bmv2_file],
+        cmd = """sed -e 's|"[^"]*\\.p4"|""|g' $(SRCS) > $(OUTS)""",
+    )
+
+    # Use p4_symbolic/main.cc to run our tool on the p4 program
+    # and produce a debugging smt file and an output file with
+    # interesting testing packets.
+    test_output_file = "generated/%s.txt" % name
+    smt_output_file = "generated/%s.smt2" % name
+    native.genrule(
+        name = "%s_test_runner" % name,
+        srcs = [
+            bmv2_file,
+            p4info_file,
+        ] + ([table_entries] if table_entries else []),
+        outs = [test_output_file, smt_output_file],
+        tools = ["//p4_symbolic:main"],
+        cmd = " ".join([
+            "$(location //p4_symbolic:main)",
+            "--hardcoded_parser=false",
+            ("--bmv2=$(location %s)" % bmv2_file),
+            ("--p4info=$(location %s)" % p4info_file),
+            ("--entries=$(location %s)" % table_entries if table_entries else ""),
+            ("--debug=$(location %s)" % smt_output_file),
+            ("&> $(location %s)" % test_output_file),
+        ]),
+    )
+
+    # Exact diff test for the packet output file.
+    diff_test(
+        name = output_test_name,
+        actual = test_output_file,
+        expected = output_golden_file,
+    )
+
+    # Group tests into a test_suite with the given name.
+    # This is just to make the provided name alias to something.
+    native.test_suite(
+        name = name,
+        tests = [
+            (":%s" % output_test_name),
+        ],
+    )

p4_symbolic/symbolic/util.cc

@@ -0,0 +1,177 @@
+// Copyright 2024 Google LLC
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//      http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// Helpful utilities for managing symbolic and concrete headers and values.
+
+#include "p4_symbolic/symbolic/util.h"
+
+#include <string>
+
+#include "absl/strings/str_format.h"
+#include "p4_pdpi/utils/ir.h"
+#include "p4_symbolic/symbolic/operators.h"
+#include "p4_symbolic/symbolic/packet.h"
+
+namespace p4_symbolic {
+namespace symbolic {
+namespace util {
+
+namespace {
+
+bool Z3BooltoBool(Z3_lbool z3_bool) {
+  switch (z3_bool) {
+    case Z3_L_TRUE:
+      return true;
+    default:
+      return false;
+  }
+}
+
+}  // namespace
+
+absl::StatusOr<std::unordered_map<std::string, z3::expr>> FreeSymbolicHeaders(
+    const google::protobuf::Map<std::string, ir::HeaderType> &headers) {
+  // Loop over every header instance in the p4 program.
+  // Find its type, and loop over every field in it, creating a symbolic free
+  // variable for every field in every header instance.
+  std::unordered_map<std::string, z3::expr> symbolic_headers;
+  for (const auto &[header_name, header_type] : headers) {
+    // Special validity field.
+    std::string valid_field_name = absl::StrFormat("%s.$valid$", header_name);
+    z3::expr valid_expression =
+        Z3Context().bool_const(valid_field_name.c_str());
+    symbolic_headers.insert({valid_field_name, valid_expression});
+
+    // Regular fields defined in the p4 program or v1model.
+    for (const auto &[field_name, field] : header_type.fields()) {
+      if (field.signed_()) {
+        return absl::UnimplementedError(
+            "Negative header fields are not supported");
+      }
+
+      std::string field_full_name =
+          absl::StrFormat("%s.%s", header_name, field_name);
+      z3::expr field_expression =
+          Z3Context().bv_const(field_full_name.c_str(), field.bitwidth());
+      symbolic_headers.insert({field_full_name, field_expression});
+    }
+  }
+
+  // Finally, we have a special field marking if the packet represented by
+  // these headers was dropped.
+  symbolic_headers.insert({"$dropped$", Z3Context().bool_val(false)});
+  return symbolic_headers;
+}
+
+SymbolicTableMatch DefaultTableMatch() {
+  return {
+      Z3Context().bool_val(false),  // No match yet!
+      Z3Context().int_val(-1)       // No match index.
+  };
+}
+
+absl::StatusOr<ConcreteContext> ExtractFromModel(
+    SymbolicContext context, z3::model model,
+    const values::P4RuntimeTranslator &translator) {
+  // Extract ports.
+  std::string ingress_port = model.eval(context.ingress_port, true).to_string();
+  std::string egress_port = model.eval(context.egress_port, true).to_string();
+
+  // Extract an input packet and its predicted output.
+  ConcretePacket ingress_packet =
+      packet::ExtractConcretePacket(context.ingress_packet, model);
+  ConcretePacket egress_packet =
+      packet::ExtractConcretePacket(context.egress_packet, model);
+
+  // Extract the ingress and egress headers.
+  ConcretePerPacketState ingress_headers;
+  for (const auto &[name, expr] : context.ingress_headers) {
+    ASSIGN_OR_RETURN(ingress_headers[name],
+                     values::TranslateValueToP4RT(
+                         name, model.eval(expr, true).to_string(), translator));
+  }
+  ConcretePerPacketState egress_headers;
+  for (const auto &[name, expr] : context.egress_headers) {
+    ASSIGN_OR_RETURN(egress_headers[name],
+                     values::TranslateValueToP4RT(
+                         name, model.eval(expr, true).to_string(), translator));
+  }
+
+  // Extract the trace (matches on every table).
+  bool dropped =
+      Z3BooltoBool(model.eval(context.trace.dropped, true).bool_value());
+  std::unordered_map<std::string, ConcreteTableMatch> matches;
+  for (const auto &[table, match] : context.trace.matched_entries) {
+    matches[table] = {
+        Z3BooltoBool(model.eval(match.matched, true).bool_value()),
+        model.eval(match.entry_index, true).get_numeral_int()};
+  }
+  ConcreteTrace trace = {matches, dropped};
+
+  return ConcreteContext{ingress_port,  egress_port,     ingress_packet,
+                         egress_packet, ingress_headers, egress_headers,
+                         trace};
+}
+
+absl::StatusOr<SymbolicTrace> MergeTracesOnCondition(
+    const z3::expr &condition, const SymbolicTrace &true_trace,
+    const SymbolicTrace &false_trace) {
+  ASSIGN_OR_RETURN(
+      z3::expr merged_dropped,
+      operators::Ite(condition, true_trace.dropped, false_trace.dropped));
+
+  // The merged trace is initially empty.
+  SymbolicTrace merged = {{}, merged_dropped};
+
+  // Merge all tables matches in true_trace (including ones in both traces).
+  for (const auto &[name, true_match] : true_trace.matched_entries) {
+    // Find match in other trace (or use default).
+    SymbolicTableMatch false_match = DefaultTableMatch();
+    if (false_trace.matched_entries.count(name) > 0) {
+      false_match = false_trace.matched_entries.at(name);
+    }
+
+    // Merge this match.
+    ASSIGN_OR_RETURN(
+        z3::expr matched,
+        operators::Ite(condition, true_match.matched, false_match.matched));
+    ASSIGN_OR_RETURN(z3::expr index,
+                     operators::Ite(condition, true_match.entry_index,
+                                    false_match.entry_index));
+    merged.matched_entries.insert({name, {matched, index}});
+  }
+
+  // Merge all tables matches in false_trace only.
+  for (const auto &[name, false_match] : false_trace.matched_entries) {
+    SymbolicTableMatch true_match = DefaultTableMatch();
+    if (true_trace.matched_entries.count(name) > 0) {
+      continue;  // Already covered.
+    }
+
+    // Merge this match.
+    ASSIGN_OR_RETURN(
+        z3::expr matched,
+        operators::Ite(condition, true_match.matched, false_match.matched));
+    ASSIGN_OR_RETURN(z3::expr index,
+                     operators::Ite(condition, true_match.entry_index,
+                                    false_match.entry_index));
+    merged.matched_entries.insert({name, {matched, index}});
+  }
+
+  return merged;
+}
+
+}  // namespace util
+}  // namespace symbolic
+}  // namespace p4_symbolic

p4_symbolic/symbolic/util.h

@@ -0,0 +1,63 @@
+// Copyright 2024 Google LLC
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//      http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// Helpful utilities for managing symbolic and concrete headers and values.
+
+#ifndef P4_SYMBOLIC_SYMBOLIC_UTIL_H_
+#define P4_SYMBOLIC_SYMBOLIC_UTIL_H_
+
+#include <string>
+#include <unordered_map>
+
+#include "google/protobuf/map.h"
+#include "gutil/status.h"
+#include "p4_pdpi/ir.pb.h"
+#include "p4_symbolic/ir/ir.pb.h"
+#include "p4_symbolic/symbolic/symbolic.h"
+#include "p4_symbolic/symbolic/values.h"
+#include "z3++.h"
+
+namespace p4_symbolic {
+namespace symbolic {
+namespace util {
+
+// Free (unconstrained) symbolic headers consisting of free symbolic variables
+// for every field in every header instance defined in the P4 program.
+absl::StatusOr<std::unordered_map<std::string, z3::expr>> FreeSymbolicHeaders(
+    const google::protobuf::Map<std::string, ir::HeaderType> &headers);
+
+// Returns an symbolic table match containing default values.
+// The table match expression is false, the index is -1, and the value is
+// undefined.
+SymbolicTableMatch DefaultTableMatch();
+
+// Extract a concrete context by evaluating every component's corresponding
+// expression in the model.
+absl::StatusOr<ConcreteContext> ExtractFromModel(
+    SymbolicContext context, z3::model model,
+    const values::P4RuntimeTranslator &translator);
+
+// Merges two symbolic traces into a single trace. A field in the new trace
+// has the value of the changed trace if the condition is true, and the value
+// of the original one otherwise.
+// Assertion: both traces must contain matches for the same set of table names.
+absl::StatusOr<SymbolicTrace> MergeTracesOnCondition(
+    const z3::expr &condition, const SymbolicTrace &true_trace,
+    const SymbolicTrace &false_trace);
+
+}  // namespace util
+}  // namespace symbolic
+}  // namespace p4_symbolic
+
+#endif  // P4_SYMBOLIC_SYMBOLIC_UTIL_H_