[P4_Symbolic] Adding p4_symbolic/symbolic/util_test.cc [Evaluate parsers symbolically.]

p4_symbolic/symbolic/util_test.cc

@@ -0,0 +1,62 @@
+// 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/util.h"
+
+#include "absl/status/status.h"
+#include "gmock/gmock.h"
+#include "gtest/gtest.h"
+#include "gutil/status_matchers.h"
+#include "gutil/testing.h"
+#include "p4_symbolic/ir/ir.pb.h"
+
+namespace p4_symbolic::symbolic::util {
+namespace {
+
+TEST(GetFieldBitwidthTest, FailsForSyntacticallyIncorrectInput) {
+  ir::P4Program program;
+  ASSERT_THAT(GetFieldBitwidth("a.b.c.d", program),
+              gutil::StatusIs(absl::StatusCode::kInvalidArgument));
+}
+
+TEST(GetFieldBitwidthTest, FailsForNonExistingHeader) {
+  ir::P4Program program;
+  ASSERT_THAT(GetFieldBitwidth("dummy_header.dummy_field", program),
+              gutil::StatusIs(absl::StatusCode::kInvalidArgument));
+}
+
+TEST(GetFieldBitwidthTest, FailsForNonExistingField) {
+  ir::P4Program program;
+  (*program.mutable_headers())["dummy_header"] = ir::HeaderType();
+  ASSERT_THAT(GetFieldBitwidth("dummy_header.dummy_field", program),
+              gutil::StatusIs(absl::StatusCode::kInvalidArgument));
+}
+
+TEST(GetFieldBitwidthTest, YieldCorrectFieldBitwidth) {
+  auto program = gutil::ParseProtoOrDie<ir::P4Program>(R"pb(
+    headers {
+      key: "dummy_header"
+      value {
+        fields {
+          key: "dummy_field"
+          value { bitwidth: 10 }
+        }
+      }
+    })pb");
+  ASSERT_THAT(GetFieldBitwidth("dummy_header.dummy_field", program),
+              gutil::IsOkAndHolds(testing::Eq(10)));
+}
+
+}  // namespace
+}  // namespace p4_symbolic::symbolic::util

p4_symbolic/symbolic/v1model.h

@@ -0,0 +1,44 @@
+// 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 P4_SYMBOLIC_SYMBOLIC_V1MODEL_H_
+#define P4_SYMBOLIC_SYMBOLIC_V1MODEL_H_
+
+#include <vector>
+
+#include "absl/status/statusor.h"
+#include "p4_symbolic/ir/ir.h"
+#include "p4_symbolic/symbolic/symbolic.h"
+#include "p4_symbolic/symbolic/values.h"
+
+namespace p4_symbolic {
+namespace symbolic {
+namespace v1model {
+
+// Initializes the ingress headers to appropriate values.
+absl::Status InitializeIngressHeaders(const ir::P4Program &program,
+                                      SymbolicPerPacketState &ingress_headers);
+
+// Symbolically evaluates the parser, ingress, and egress pipelines of the given
+// P4 program with the given entries, assuming the program is written against V1
+// model.
+absl::StatusOr<SymbolicContext> EvaluateV1model(
+    const ir::Dataplane &data_plane, const std::vector<int> &physical_ports,
+    values::P4RuntimeTranslator &translator);
+
+}  // namespace v1model
+}  // namespace symbolic
+}  // namespace p4_symbolic
+
+#endif  // P4_SYMBOLIC_SYMBOLIC_V1MODEL_H_