[P4_Symbolic] Move symbolic/concrete context to context.{cc,h} separated from symbolic.{cc,h}, and make the context-related objects constructed along with the solver state and then passed along the symbolic evaluation.

p4_symbolic/sai/sai.cc

@@ -14,7 +14,6 @@
 
 #include "p4_symbolic/sai/sai.h"
 
-#include <memory>
 #include <string>
 #include <type_traits>
 #include <unordered_set>

p4_symbolic/symbolic/BUILD.bazel

@@ -24,6 +24,7 @@ cc_library(
     srcs = [
         "action.cc",
         "conditional.cc",
+        "context.cc",
         "control.cc",
         "guarded_map.cc",
         "operators.cc",
@@ -37,6 +38,7 @@ cc_library(
     hdrs = [
         "action.h",
         "conditional.h",
+        "context.h",
         "control.h",
         "guarded_map.h",
         "operators.h",

p4_symbolic/symbolic/action.h

@@ -25,7 +25,7 @@
 #include "google/protobuf/repeated_ptr_field.h"
 #include "p4_pdpi/ir.pb.h"
 #include "p4_symbolic/ir/ir.pb.h"
-#include "p4_symbolic/symbolic/symbolic.h"
+#include "p4_symbolic/symbolic/context.h"
 #include "p4_symbolic/symbolic/values.h"
 #include "z3++.h"
 

p4_symbolic/symbolic/conditional.h

@@ -20,7 +20,7 @@
 
 #include "p4_symbolic/ir/ir.h"
 #include "p4_symbolic/ir/ir.pb.h"
-#include "p4_symbolic/symbolic/symbolic.h"
+#include "p4_symbolic/symbolic/context.h"
 #include "p4_symbolic/symbolic/values.h"
 #include "z3++.h"
 

p4_symbolic/symbolic/context.cc

@@ -0,0 +1,69 @@
+// 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.
+
+#include "p4_symbolic/symbolic/context.h"
+
+#include <string>
+
+#include "absl/strings/str_cat.h"
+
+namespace p4_symbolic {
+namespace symbolic {
+
+std::string ConcreteTableMatch::to_string() const {
+  if (!matched) {
+    return "was not matched!";
+  }
+  return absl::StrCat("was matched on entry ", entry_index);
+}
+
+std::string ConcreteTrace::to_string() const {
+  std::string result;
+  absl::StrAppend(&result, "dropped = ", dropped, "\n");
+  absl::StrAppend(&result, "got cloned = ", got_cloned);
+  for (const auto &[table, match] : matched_entries) {
+    absl::StrAppend(&result, "\n", table, " => ", match.to_string());
+  }
+  return result;
+}
+
+std::string ConcreteContext::to_string() const {
+  return to_string(/*verbose=*/false);
+}
+
+std::string ConcreteContext::to_string(bool verbose) const {
+  auto result = absl::StrCat("ingress_port = ", ingress_port, "\n",
+                             "egress_port = ", egress_port, "\n", "trace:\n",
+                             trace.to_string());
+  if (verbose) {
+    auto ingress_string = absl::StrCat("ingress_headers", ":");
+    auto parsed_string = absl::StrCat("parsed_headers", ":");
+    auto egress_string = absl::StrCat("egress_headers", ":");
+    for (const auto &[name, ingress_value] : ingress_headers) {
+      absl::StrAppend(&ingress_string, "\n", name, " = ", ingress_value);
+    }
+    for (const auto &[name, parsed_value] : parsed_headers) {
+      absl::StrAppend(&parsed_string, "\n", name, " = ", parsed_value);
+    }
+    for (const auto &[name, egress_value] : egress_headers) {
+      absl::StrAppend(&egress_string, "\n", name, " = ", egress_value);
+    }
+    absl::StrAppend(&result, "\n\n", ingress_string, "\n\n", parsed_string,
+                    "\n\n", egress_string);
+  }
+  return result;
+}
+
+}  // namespace symbolic
+}  // namespace p4_symbolic

p4_symbolic/symbolic/context.h

@@ -0,0 +1,129 @@
+// 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.
+
+#ifndef PINS_P4_SYMBOLIC_SYMBOLIC_CONTEXT_H_
+#define PINS_P4_SYMBOLIC_SYMBOLIC_CONTEXT_H_
+
+#include <string>
+
+#include "absl/container/btree_map.h"
+#include "p4_symbolic/symbolic/guarded_map.h"
+#include "p4_symbolic/z3_util.h"
+#include "z3++.h"
+
+namespace p4_symbolic {
+namespace symbolic {
+
+// Maps the name of a header field in the p4 program to its concrete value.
+using ConcretePerPacketState = absl::btree_map<std::string, std::string>;
+
+// The symbolic counterpart of ConcretePerPacketState.
+// Maps the name of a header field in the p4 program to its symbolic value.
+// This can be used to constrain p4 program fields inside assertions.
+// This is automatically constructed from the header type definitions
+// the p4 program has.
+// Assume the p4 program has a header instance named "standard_metadata" of type
+// "standard_metadata_t", which has field "ingress_port" of type "bit<9>" in it.
+// Then, we will have:
+//     SymbolicMetadata["standard_metadata.ingress_port"] =
+//         <symbolic bit vector of size 9>
+// An instance of this type is passed around and mutated by the functions
+// responsible for symbolically evaluating the program.
+using SymbolicPerPacketState = SymbolicGuardedMap;
+
+// Expresses a concrete match for a corresponding concrete packet with a
+// table in the program.
+struct ConcreteTableMatch {
+  bool matched;  // false if no entry in this table was matched, true otherwise.
+  // If matched is false, this is set to -1.
+  // If matched is true, this is the index of the matched table entry, or -1 if
+  // the default entry was matched.
+  int entry_index;
+  std::string to_string() const;
+};
+
+// Exposes a symbolic handle for a match between the symbolic packet and
+// a symbolic table.
+// This allows encoding of constraints on which (if any) entries are matched,
+// and the value of the match.
+// e.g. for some table "<table_name>":
+// (<symbolic_table_match>.entry_index == i) iff
+//  <entries>[<table_name>][i] was matched/hit.
+struct SymbolicTableMatch {
+  z3::expr matched;
+  z3::expr entry_index;
+};
+
+// `SymbolicTableMatch`es by table name.
+using SymbolicTableMatches = absl::btree_map<std::string, SymbolicTableMatch>;
+
+// Specifies the expected trace in the program that the corresponding
+// concrete packet is expected to take.
+struct ConcreteTrace {
+  absl::btree_map<std::string, ConcreteTableMatch> matched_entries;
+  // Can be extended more in the future to include useful
+  // flags about dropping the packet, taking specific code (e.g. if)
+  // branches, vrf, other interesting events, etc.
+  bool dropped;     // true if the packet was dropped.
+  bool got_cloned;  // true if the packet got cloned.
+  std::string to_string() const;
+};
+
+// Provides symbolic handles for the trace the symbolic packet is constrained
+// to take in the program.
+struct SymbolicTrace {
+  SymbolicTrace() : dropped(Z3Context()), got_cloned(Z3Context()) {}
+
+  // Full table name to its symbolic match.
+  // TODO: Rename to matches_by_table_name.
+  SymbolicTableMatches matched_entries;
+  z3::expr dropped;
+  z3::expr got_cloned;
+};
+
+// The result of solving with some assertion.
+// This contains an input test packet with its predicted flow in the program,
+// and the predicted output.
+struct ConcreteContext {
+  std::string ingress_port;
+  std::string egress_port;
+  ConcretePerPacketState ingress_headers;
+  ConcretePerPacketState parsed_headers;
+  ConcretePerPacketState egress_headers;
+  ConcreteTrace trace;  // Expected trace in the program.
+
+  std::string to_string() const;
+  std::string to_string(bool verbose) const;
+};
+
+// The symbolic context within our analysis.
+// Exposes symbolic handles for the fields of the input packet,
+// and its trace in the program.
+// Assertions are defined on a symbolic context.
+class SymbolicContext {
+ public:
+  SymbolicContext() : ingress_port(Z3Context()), egress_port(Z3Context()) {}
+
+  z3::expr ingress_port;
+  z3::expr egress_port;
+  SymbolicPerPacketState ingress_headers;
+  SymbolicPerPacketState parsed_headers;
+  SymbolicPerPacketState egress_headers;
+  SymbolicTrace trace;
+};
+
+}  // namespace symbolic
+}  // namespace p4_symbolic
+
+#endif  // PINS_P4_SYMBOLIC_SYMBOLIC_CONTEXT_H_

p4_symbolic/symbolic/control.cc

@@ -28,7 +28,7 @@
 #include "p4_symbolic/ir/ir.h"
 #include "p4_symbolic/ir/ir.pb.h"
 #include "p4_symbolic/symbolic/conditional.h"
-#include "p4_symbolic/symbolic/symbolic.h"
+#include "p4_symbolic/symbolic/context.h"
 #include "p4_symbolic/symbolic/table.h"
 
 namespace p4_symbolic::symbolic::control {

p4_symbolic/symbolic/control.h

@@ -60,7 +60,7 @@
 #include <string>
 
 #include "p4_symbolic/ir/ir.h"
-#include "p4_symbolic/symbolic/symbolic.h"
+#include "p4_symbolic/symbolic/context.h"
 #include "p4_symbolic/symbolic/values.h"
 #include "z3++.h"
 

p4_symbolic/symbolic/guarded_map.h

@@ -22,7 +22,6 @@
 #include "absl/container/btree_map.h"
 #include "absl/status/status.h"
 #include "google/protobuf/map.h"
-#include "gutil/status.h"
 #include "p4_symbolic/ir/ir.pb.h"
 #include "z3++.h"
 
@@ -31,37 +30,40 @@ namespace symbolic {
 
 // This class wraps around an internal absl::btree_map instance,
 // while enforcing the following:
-// 1. This class can only be instantiated with an instance of the IR
-//    header definitions. The resulting instance will be initialized
-//    to have exactly the same keys as the fields defined in those header
-//    definitions. These keys are initially mapped to free symbolic variables,
-//    with the same sort (including bitsize) described in the definitions.
-// 2. This class supports a const reference .Get(<key>), which returns
-//    an absl error if the key is not found in the map.
-// 3. This class allows mutation via .Set(<key>, <value>, <guard>), which
-//    sets the value of the key to z3::ite(<guard>, <value>, <old value>),
-//    after checking that the sort of <value> matches the sort of <old value>
-//    modulo padding.
+// 1. When instantiated with an instance of the IR header definitions. The
+//    resulting instance will be initialized to have exactly the same keys as
+//    the fields defined in those header definitions. These keys are initially
+//    mapped to free symbolic variables, with the same sort (including bitsize)
+//    described in the definitions.
+// 2. This class supports const references .Get(<key>) and .Get(<header_name>,
+//    <field_name>), which returns an absl error if the key is not found in the
+//    map.
+// 3. This class allows mutation via .Set(<key>, <value>, <guard>) and
+//    .Set(<header_name>, <field_name>, <value>, <guard>), which set the value
+//    of the key to z3::ite(<guard>, <value>, <old value>), after checking that
+//    the sort of <value> matches the sort of <old value> modulo padding.
+// 4. Special mutation methods are supported via .UnguardedSet(<key>, <value>)
+//    and .UnguardedSet(<header_name>, <field_name>, <value>), which
+//    unconditionally overwrite the old values in the map and are mainly used
+//    for initializing certain architecture- or target-specific values.
 //
 // As such, this class provides the following safety properties:
 // 1. Once initialized, the class has a fixed set of keys.
 // 2. A value mapped by a key always has the same sort.
 // 3. A value can only be assigned to a key given a guard.
 //
 class SymbolicGuardedMap {
-public:
-  // Constructor requires passing the headers definition and will fill the map
-  // with a free symbolic variable per header field.
+ public:
+  // By passing the headers definition, the constructor will fill the map with a
+  // free symbolic variable per header field.
   static absl::StatusOr<SymbolicGuardedMap> CreateSymbolicGuardedMap(
       const google::protobuf::Map<std::string, ir::HeaderType> &headers);
 
-  // Explicitly copyable and movable!
+  SymbolicGuardedMap() = default;
   SymbolicGuardedMap(const SymbolicGuardedMap &other) = default;
   SymbolicGuardedMap(SymbolicGuardedMap &&other) = default;
-
-  // Not assignable.
-  SymbolicGuardedMap &operator=(const SymbolicGuardedMap &other) = delete;
-  SymbolicGuardedMap &operator=(SymbolicGuardedMap &&other) = delete;
+  SymbolicGuardedMap &operator=(const SymbolicGuardedMap &other) = default;
+  SymbolicGuardedMap &operator=(SymbolicGuardedMap &&other) = default;
 
   // Getters.
   bool ContainsKey(absl::string_view key) const;
@@ -96,7 +98,7 @@ class SymbolicGuardedMap {
 
   // Private constructor used by factory.
   explicit SymbolicGuardedMap(absl::btree_map<std::string, z3::expr> map)
-      : map_(map) {}
+      : map_(std::move(map)) {}
 };
 
 } // namespace symbolic