-
Notifications
You must be signed in to change notification settings - Fork 26
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[P4_Symbolic] Adding p4_symbolic/testdata/parser/fall_through_transit…
…ion.p4 [Evaluate parsers symbolically.]
- Loading branch information
1 parent
f48f3c9
commit aa4d303
Showing
3 changed files
with
75 additions
and
7 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -394,11 +394,4 @@ errors { | |
value: 3 | ||
} | ||
} | ||
deparsers { | ||
key: "deparser" | ||
value { | ||
name: "deparser" | ||
header_order: "ethernet" | ||
} | ||
} | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,68 @@ | ||
#include <v1model.p4> | ||
#include "../common/headers.p4" | ||
|
||
struct local_metadata_t { | ||
/* empty */ | ||
} | ||
|
||
struct headers_t { | ||
ethernet_t ethernet; | ||
ipv4_t ipv4; | ||
} | ||
|
||
parser packet_parser(packet_in packet, out headers_t headers, | ||
inout local_metadata_t local_metadata, | ||
inout standard_metadata_t standard_metadata) { | ||
state start { | ||
transition parse_ethernet; | ||
} | ||
|
||
state parse_ethernet { | ||
packet.extract(headers.ethernet); | ||
transition select(headers.ethernet.ether_type) { | ||
ETHERTYPE_IPV4: parse_ipv4; | ||
} | ||
} | ||
|
||
state parse_ipv4 { | ||
packet.extract(headers.ipv4); | ||
transition accept; | ||
} | ||
} | ||
|
||
control empty_verify_checksum(inout headers_t headers, | ||
inout local_metadata_t local_metadata) { | ||
apply {} | ||
} // control empty_verify_checksum | ||
|
||
control ingress(inout headers_t headers, | ||
inout local_metadata_t local_metadata, | ||
inout standard_metadata_t standard_metadata) { | ||
apply {} | ||
} // control ingress | ||
|
||
control egress(inout headers_t headers, | ||
inout local_metadata_t local_metadata, | ||
inout standard_metadata_t standard_metadata) { | ||
apply {} | ||
} // control egress | ||
|
||
control empty_compute_checksum(inout headers_t headers, | ||
inout local_metadata_t local_metadata) { | ||
apply {} | ||
} // control empty_compute_checksum | ||
|
||
control packet_deparser(packet_out packet, in headers_t headers) { | ||
apply { | ||
packet.emit(headers.ethernet); | ||
} | ||
} // control packet_deparser | ||
|
||
V1Switch( | ||
packet_parser(), | ||
empty_verify_checksum(), | ||
ingress(), | ||
egress(), | ||
empty_compute_checksum(), | ||
packet_deparser() | ||
) main; |