Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[P4-Symbolic] Migrate to p4c from 2022-11-23. #691

Merged
merged 4 commits into from
Nov 7, 2024
Merged

[P4-Symbolic] Migrate to p4c from 2022-11-23. #691

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
a2109ad
[p4-symbolic] Migrate to p4c from 2022-11-23.
smolkaj Dec 1, 2022
ca1adab
Merge branch 'main' of https://github.com/VSuryaprasad-HCL/sonic-pins…
VSuryaprasad-HCL Nov 4, 2024
6e17672
Merge branch 'main' of https://github.com/VSuryaprasad-HCL/sonic-pins…
VSuryaprasad-HCL Nov 6, 2024
5289a82
Merge branch 'main' into symbolic_import_branch_77
kishanps Nov 7, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 9 additions & 10 deletions p4_symbolic/main.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,7 +117,6 @@ absl::Status ParseAndEvaluate() {
// Whether packet was dropped or not!
std::cout << "\tDropped = " << packet_option.value().trace.dropped
<< std::endl;

// Ports
std::cout << "\tstandard_metadata.ingress_port = "
<< packet_option.value().ingress_port << std::endl;
Expand All @@ -143,25 +142,25 @@ absl::Status ParseAndEvaluate() {
}
// VRF
if (packet_option.value().egress_headers.count(
"scalars.userMetadata.vrf")) {
std::cout << "\tscalars.userMetadata.vrf = "
"scalars.local_metadata_t.vrf")) {
std::cout << "\tscalars.local_metadata_t.vrf = "
<< packet_option.value().egress_headers.at(
"scalars.userMetadata.vrf")
"scalars.local_metadata_t.vrf")
<< std::endl;
}
if (packet_option.value().egress_headers.count(
"scalars.userMetadata.vrf_is_valid")) {
std::cout << "\tscalars.userMetadata.vrf_is_valid = "
"scalars.local_metadata_t.vrf_is_valid")) {
std::cout << "\tscalars.local_metadata_t.vrf_is_valid = "
<< packet_option.value().egress_headers.at(
"scalars.userMetadata.vrf_is_valid")
"scalars.local_metadata_t.vrf_is_valid")
<< std::endl;
}
// Custom metadata field defined in testdata/string-optional/program.p4
if (packet_option.value().egress_headers.contains(
"scalars.userMetadata.string_field")) {
std::cout << "\tscalars.userMetadata.string_field = "
"scalars.metadata.string_field")) {
std::cout << "\tscalars.metadata.string_field = "
<< packet_option.value().egress_headers.at(
"scalars.userMetadata.string_field")
"scalars.metadata.string_field")
<< std::endl;
}
} else {
Expand Down
29 changes: 22 additions & 7 deletions p4_symbolic/sai/fields.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@
#include "absl/strings/ascii.h"
#include "absl/strings/match.h"
#include "absl/strings/str_join.h"
#include "absl/strings/string_view.h"
#include "gutil/status.h"
#include "p4_symbolic/symbolic/symbolic.h"
#include "p4_symbolic/z3_util.h"
Expand All @@ -40,14 +41,28 @@ absl::StatusOr<z3::expr> GetUserMetadata(const std::string& field,
const SymbolicPerPacketState& state) {
// Compute set of mangled field names that match the given field name.
std::vector<std::string> mangled_candidates;
// p4c seems to use the following template to name metadata fields:
// "scalars.userMetadata._<field name><a number>". We look for names that
// match the template.
const std::string prefix = absl::StrCat("scalars.userMetadata._", field);

// p4c seems to use the following template to name user metadata fields:
//
// - Until ~ 2022-11-01:
// "scalars.userMetadata._<field name><a number>"
//
// - After ~ 2022-11-01:
// "scalars.<user metadata typename>._<field name><a number>", where
// <user metadata typename> is "local_metadata_t" in SAI P4.
//
// We look for names that match these templates.
// TODO: Remove `old_prefix` eventually when we no longer
// need backward compatability.
const std::string old_prefix = absl::StrCat("scalars.userMetadata._", field);
const std::string new_prefix =
absl::StrCat("scalars.local_metadata_t._", field);
for (const auto& [key, _] : state) {
if (absl::StartsWith(key, prefix) && key.length() > prefix.length() &&
absl::ascii_isdigit(key.at(prefix.length()))) {
mangled_candidates.push_back(key);
for (absl::string_view prefix : {old_prefix, new_prefix}) {
if (absl::StartsWith(key, prefix) && key.length() > prefix.length() &&
absl::ascii_isdigit(key.at(prefix.length()))) {
mangled_candidates.push_back(key);
}
}
}

Expand Down
48 changes: 24 additions & 24 deletions p4_symbolic/symbolic/expected/string_optional.smt2
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
(set-info :status unknown)
(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun scalars.userMetadata.string_field () (_ BitVec 9))
(declare-fun scalars.metadata.string_field () (_ BitVec 9))
(assert
(let (($x38 (= standard_metadata.ingress_port (_ bv2 9))))
(let (($x35 (= standard_metadata.ingress_port (_ bv1 9))))
Expand All @@ -17,7 +17,7 @@
(let (($x33 (and true $x32)))
(let (($x41 (not $x33)))
(let (($x46 (and true (and $x41 (not (and true (= standard_metadata.ingress_port (_ bv1 9))))))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.metadata.string_field))))
(let (($x35 (= standard_metadata.ingress_port (_ bv1 9))))
(let (($x36 (and true $x35)))
(let (($x40 (and true $x33)))
Expand All @@ -37,7 +37,7 @@
(let (($x33 (and true $x32)))
(let (($x41 (not $x33)))
(let (($x46 (and true (and $x41 (not (and true (= standard_metadata.ingress_port (_ bv1 9))))))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.metadata.string_field))))
(let (($x35 (= standard_metadata.ingress_port (_ bv1 9))))
(let (($x36 (and true $x35)))
(let (($x40 (and true $x33)))
Expand All @@ -55,7 +55,7 @@
(set-info :status unknown)
(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun scalars.userMetadata.string_field () (_ BitVec 9))
(declare-fun scalars.metadata.string_field () (_ BitVec 9))
(assert
(let (($x38 (= standard_metadata.ingress_port (_ bv2 9))))
(let (($x35 (= standard_metadata.ingress_port (_ bv1 9))))
Expand All @@ -70,7 +70,7 @@
(let (($x33 (and true $x32)))
(let (($x41 (not $x33)))
(let (($x46 (and true (and $x41 (not (and true (= standard_metadata.ingress_port (_ bv1 9))))))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.metadata.string_field))))
(let (($x35 (= standard_metadata.ingress_port (_ bv1 9))))
(let (($x36 (and true $x35)))
(let (($x40 (and true $x33)))
Expand All @@ -90,7 +90,7 @@
(let (($x33 (and true $x32)))
(let (($x41 (not $x33)))
(let (($x46 (and true (and $x41 (not (and true (= standard_metadata.ingress_port (_ bv1 9))))))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.metadata.string_field))))
(let (($x35 (= standard_metadata.ingress_port (_ bv1 9))))
(let (($x36 (and true $x35)))
(let (($x40 (and true $x33)))
Expand All @@ -109,7 +109,7 @@
(set-info :status unknown)
(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun scalars.userMetadata.string_field () (_ BitVec 9))
(declare-fun scalars.metadata.string_field () (_ BitVec 9))
(assert
(let (($x38 (= standard_metadata.ingress_port (_ bv2 9))))
(let (($x35 (= standard_metadata.ingress_port (_ bv1 9))))
Expand All @@ -124,7 +124,7 @@
(let (($x33 (and true $x32)))
(let (($x41 (not $x33)))
(let (($x46 (and true (and $x41 (not (and true (= standard_metadata.ingress_port (_ bv1 9))))))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.metadata.string_field))))
(let (($x35 (= standard_metadata.ingress_port (_ bv1 9))))
(let (($x36 (and true $x35)))
(let (($x40 (and true $x33)))
Expand All @@ -144,7 +144,7 @@
(let (($x33 (and true $x32)))
(let (($x41 (not $x33)))
(let (($x46 (and true (and $x41 (not (and true (= standard_metadata.ingress_port (_ bv1 9))))))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.metadata.string_field))))
(let (($x35 (= standard_metadata.ingress_port (_ bv1 9))))
(let (($x36 (and true $x35)))
(let (($x40 (and true $x33)))
Expand All @@ -162,7 +162,7 @@
(set-info :status unknown)
(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun scalars.userMetadata.string_field () (_ BitVec 9))
(declare-fun scalars.metadata.string_field () (_ BitVec 9))
(assert
(let (($x38 (= standard_metadata.ingress_port (_ bv2 9))))
(let (($x35 (= standard_metadata.ingress_port (_ bv1 9))))
Expand All @@ -177,7 +177,7 @@
(let (($x33 (and true $x32)))
(let (($x41 (not $x33)))
(let (($x46 (and true (and $x41 (not (and true (= standard_metadata.ingress_port (_ bv1 9))))))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.metadata.string_field))))
(let (($x35 (= standard_metadata.ingress_port (_ bv1 9))))
(let (($x36 (and true $x35)))
(let (($x40 (and true $x33)))
Expand All @@ -201,7 +201,7 @@
(let (($x39 (and true $x38)))
(let (($x41 (not $x33)))
(let (($x46 (and true (and $x41 (not (and true (= standard_metadata.ingress_port (_ bv1 9))))))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.metadata.string_field))))
(let (($x35 (= standard_metadata.ingress_port (_ bv1 9))))
(let (($x36 (and true $x35)))
(let ((?x66 (ite $x40 ?x65 (ite (and (and true $x41) $x36) (concat (_ bv0 8) (_ bv1 1)) ?x54))))
Expand All @@ -217,7 +217,7 @@
(set-info :status unknown)
(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun scalars.userMetadata.string_field () (_ BitVec 9))
(declare-fun scalars.metadata.string_field () (_ BitVec 9))
(assert
(let (($x38 (= standard_metadata.ingress_port (_ bv2 9))))
(let (($x35 (= standard_metadata.ingress_port (_ bv1 9))))
Expand All @@ -232,7 +232,7 @@
(let (($x33 (and true $x32)))
(let (($x41 (not $x33)))
(let (($x46 (and true (and $x41 (not (and true (= standard_metadata.ingress_port (_ bv1 9))))))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.metadata.string_field))))
(let (($x35 (= standard_metadata.ingress_port (_ bv1 9))))
(let (($x36 (and true $x35)))
(let (($x40 (and true $x33)))
Expand All @@ -256,7 +256,7 @@
(let (($x39 (and true $x38)))
(let (($x41 (not $x33)))
(let (($x46 (and true (and $x41 (not (and true (= standard_metadata.ingress_port (_ bv1 9))))))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.metadata.string_field))))
(let (($x35 (= standard_metadata.ingress_port (_ bv1 9))))
(let (($x36 (and true $x35)))
(let ((?x66 (ite $x40 ?x65 (ite (and (and true $x41) $x36) (concat (_ bv0 8) (_ bv1 1)) ?x54))))
Expand All @@ -273,7 +273,7 @@
(set-info :status unknown)
(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun scalars.userMetadata.string_field () (_ BitVec 9))
(declare-fun scalars.metadata.string_field () (_ BitVec 9))
(assert
(let (($x38 (= standard_metadata.ingress_port (_ bv2 9))))
(let (($x35 (= standard_metadata.ingress_port (_ bv1 9))))
Expand All @@ -288,7 +288,7 @@
(let (($x33 (and true $x32)))
(let (($x41 (not $x33)))
(let (($x46 (and true (and $x41 (not (and true (= standard_metadata.ingress_port (_ bv1 9))))))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.metadata.string_field))))
(let (($x35 (= standard_metadata.ingress_port (_ bv1 9))))
(let (($x36 (and true $x35)))
(let (($x40 (and true $x33)))
Expand All @@ -312,7 +312,7 @@
(let (($x39 (and true $x38)))
(let (($x41 (not $x33)))
(let (($x46 (and true (and $x41 (not (and true (= standard_metadata.ingress_port (_ bv1 9))))))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.metadata.string_field))))
(let (($x35 (= standard_metadata.ingress_port (_ bv1 9))))
(let (($x36 (and true $x35)))
(let ((?x66 (ite $x40 ?x65 (ite (and (and true $x41) $x36) (concat (_ bv0 8) (_ bv1 1)) ?x54))))
Expand All @@ -328,7 +328,7 @@
(set-info :status unknown)
(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun scalars.userMetadata.string_field () (_ BitVec 9))
(declare-fun scalars.metadata.string_field () (_ BitVec 9))
(assert
(let (($x38 (= standard_metadata.ingress_port (_ bv2 9))))
(let (($x35 (= standard_metadata.ingress_port (_ bv1 9))))
Expand All @@ -343,7 +343,7 @@
(let (($x33 (and true $x32)))
(let (($x41 (not $x33)))
(let (($x46 (and true (and $x41 (not (and true (= standard_metadata.ingress_port (_ bv1 9))))))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.metadata.string_field))))
(let (($x35 (= standard_metadata.ingress_port (_ bv1 9))))
(let (($x36 (and true $x35)))
(let (($x40 (and true $x33)))
Expand All @@ -367,7 +367,7 @@
(let (($x39 (and true $x38)))
(let (($x41 (not $x33)))
(let (($x46 (and true (and $x41 (not (and true (= standard_metadata.ingress_port (_ bv1 9))))))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.metadata.string_field))))
(let (($x35 (= standard_metadata.ingress_port (_ bv1 9))))
(let (($x36 (and true $x35)))
(let ((?x66 (ite $x40 ?x65 (ite (and (and true $x41) $x36) (concat (_ bv0 8) (_ bv1 1)) ?x54))))
Expand All @@ -383,7 +383,7 @@
(set-info :status unknown)
(declare-fun standard_metadata.ingress_port () (_ BitVec 9))
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun scalars.userMetadata.string_field () (_ BitVec 9))
(declare-fun scalars.metadata.string_field () (_ BitVec 9))
(assert
(let (($x38 (= standard_metadata.ingress_port (_ bv2 9))))
(let (($x35 (= standard_metadata.ingress_port (_ bv1 9))))
Expand All @@ -398,7 +398,7 @@
(let (($x33 (and true $x32)))
(let (($x41 (not $x33)))
(let (($x46 (and true (and $x41 (not (and true (= standard_metadata.ingress_port (_ bv1 9))))))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.metadata.string_field))))
(let (($x35 (= standard_metadata.ingress_port (_ bv1 9))))
(let (($x36 (and true $x35)))
(let (($x40 (and true $x33)))
Expand All @@ -418,7 +418,7 @@
(let (($x33 (and true $x32)))
(let (($x41 (not $x33)))
(let (($x46 (and true (and $x41 (not (and true (= standard_metadata.ingress_port (_ bv1 9))))))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.userMetadata.string_field))))
(let ((?x54 (ite (and $x46 $x39) ?x29 (ite true ?x29 scalars.metadata.string_field))))
(let (($x35 (= standard_metadata.ingress_port (_ bv1 9))))
(let (($x36 (and true $x35)))
(let (($x40 (and true $x33)))
Expand Down
6 changes: 6 additions & 0 deletions p4_symbolic/symbolic/expected/string_optional.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,11 +5,13 @@ Finding packet for table MyIngress.optional_match and row 0
Dropped = 0
standard_metadata.ingress_port = #b000000000
standard_metadata.egress_spec = #b000000000
scalars.metadata.string_field = VALUE-0

Finding packet for table MyIngress.optional_match and row 1
Dropped = 0
standard_metadata.ingress_port = #b000000010
standard_metadata.egress_spec = #b000000001
scalars.metadata.string_field = VALUE-2

Finding packet for table MyIngress.set_field_table and row -1
Cannot find solution!
Expand All @@ -18,19 +20,23 @@ Finding packet for table MyIngress.set_field_table and row 0
Dropped = 0
standard_metadata.ingress_port = #b000000000
standard_metadata.egress_spec = #b000000000
scalars.metadata.string_field = VALUE-0

Finding packet for table MyIngress.set_field_table and row 1
Dropped = 0
standard_metadata.ingress_port = #b000000001
standard_metadata.egress_spec = #b000000001
scalars.metadata.string_field = VALUE-1

Finding packet for table MyIngress.set_field_table and row 2
Dropped = 0
standard_metadata.ingress_port = #b000000010
standard_metadata.egress_spec = #b000000001
scalars.metadata.string_field = VALUE-2

Finding packet for table tbl_program92 and row -1
Dropped = 0
standard_metadata.ingress_port = #b000000010
standard_metadata.egress_spec = #b000000001
scalars.metadata.string_field = VALUE-2

Loading
Loading