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

Implement header union invalidation in the BMv2 back end. #4982

Draft
wants to merge 3 commits into
base: main
Choose a base branch
from
Draft

Implement header union invalidation in the BMv2 back end. #4982

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
4ea69b5
Set other headers also invalid when calling setInvalid on a union hea…
fruffy Aug 5, 2024
17df75b
Add an option to copy structures to skip expanding header unions.
fruffy Aug 7, 2024
afcadec
Implement header union invaidation in the BMv2 back end.
fruffy Aug 5, 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
Next Next commit
Set other headers also invalid when calling setInvalid on a union hea… 
…der.

Signed-off-by: fruffy <fruffy@nyu.edu>
  • Loading branch information
@fruffy
fruffy committed Oct 25, 2024
commit 4ea69b575edd8a6639044b263c184022663d4953
52 changes: 31 additions & 21 deletions backends/p4tools/modules/testgen/core/small_step/abstract_stepper.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -210,38 +210,48 @@ bool AbstractStepper::stepGetHeaderValidity(const IR::StateVariable &headerRef)
return false;
}

void AbstractStepper::setHeaderValidity(const IR::StateVariable &headerRef, bool validity,
ExecutionState &nextState) {
namespace {

void setHeaderValidityHelper(const IR::StateVariable &headerRef, bool validity,
const ProgramInfo &programInfo, ExecutionState &nextState) {
const auto &headerRefValidity = ToolsVariables::getHeaderValidity(headerRef);
nextState.set(headerRefValidity, IR::BoolLiteral::get(validity));

// In some cases, the header may be `part of a union.
if (validity) {
const auto *headerBaseMember = headerRef.ref->to<IR::Member>();
if (headerBaseMember == nullptr) {
return;
// The header is going to be invalid. Set all fields to taint constants.
// TODO: Should we make this target specific? Some targets set the header fields to 0...
if (!validity) {
std::vector<IR::StateVariable> validityVector;
auto fieldsVector = nextState.getFlatFields(headerRef, &validityVector);
for (const auto &field : validityVector) {
nextState.set(field, IR::BoolLiteral::get(false));
}
for (const auto &field : fieldsVector) {
nextState.set(field, programInfo.createTargetUninitialized(field->type, true));
}
const auto *headerBase = headerBaseMember->expr;
}
}

} // namespace

void AbstractStepper::setHeaderValidity(const IR::StateVariable &headerRef, bool validity,
ExecutionState &nextState) {
setHeaderValidityHelper(headerRef, validity, programInfo, nextState);

// In some cases, the header may be nested.
if (const auto *headerBase = headerRef.ref->to<IR::Member>()) {
// In the case of header unions, we need to set all other union members invalid.
if (const auto *hdrUnion = headerBase->type->to<IR::Type_HeaderUnion>()) {
CHECK_NULL(headerBase->expr->type);
if (const auto *hdrUnion = headerBase->expr->type->to<IR::Type_HeaderUnion>()) {
for (const auto *field : hdrUnion->fields) {
auto *member = new IR::Member(field->type, headerBase, field->name);
// Ignore the member we are setting to valid.
if (headerRef->equiv(*member)) {
// Ignore the member we are setting.
if (headerBase->member == field->name) {
continue;
}
// Set all other members to invalid.
setHeaderValidity(member, false, nextState);
setHeaderValidityHelper(new IR::Member(field->type, headerBase->expr, field->name),
false, programInfo, nextState);
}
}
return;
}
std::vector<IR::StateVariable> validityVector;
auto fieldsVector = nextState.getFlatFields(headerRef, &validityVector);
// The header is going to be invalid. Set all fields to taint constants.
// TODO: Should we make this target specific? Some targets set the header fields to 0.
for (const auto &field : fieldsVector) {
nextState.set(field, programInfo.createTargetUninitialized(field->type, true));
}
}

Expand Down
9 changes: 9 additions & 0 deletions backends/p4tools/modules/testgen/targets/bmv2/test/BMV2PTFXfail.cmake
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,15 @@ p4tools_add_xfail_reason(
v1model-digest-custom-type.p4
)

p4tools_add_xfail_reason(
"testgen-p4c-bmv2-ptf"
"Expected packet was not received on device"
# BMv2 has the incorrect HU invalidation implementation.
bmv2_invalid_hu_1.p4
bmv2_invalid_hu_2.p4
union4-bmv2.p4
)

####################################################################################################
# 2. P4Testgen Issues
# These are failures in P4Testgen that need to be fixed.
Expand Down
9 changes: 9 additions & 0 deletions backends/p4tools/modules/testgen/targets/bmv2/test/BMV2STFXfail.cmake
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,6 +62,15 @@ p4tools_add_xfail_reason(
extract_for_header_union.p4
)

p4tools_add_xfail_reason(
"testgen-p4c-bmv2-stf"
"differs|Expected ([0-9]+) packets on port ([0-9]+) got ([0-9]+)"
# BMv2 has the incorrect HU invalidation implementation.
bmv2_invalid_hu_1.p4
bmv2_invalid_hu_2.p4
union4-bmv2.p4
)

####################################################################################################
# 2. P4Testgen Issues
# These are failures in P4Testgen that need to be fixed.
Expand Down
76 changes: 76 additions & 0 deletions backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/bmv2_invalid_hu_1.p4
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,76 @@
#include <v1model.p4>

header opt_t {
bit<8> opt;
}

header ethernet_t {
bit<48> dst_addr;
bit<48> src_addr;
bit<16> eth_type;
}

header H {
bit<8> a;
bit<8> a1;
bit<8> b;
}

header_union U {
ethernet_t e;
H h;
}

struct Headers {
opt_t opt;
U u;
}

struct Meta {}

parser p(packet_in pkt, out Headers h, inout Meta meta, inout standard_metadata_t stdmeta) {
state start {
pkt.extract(h.opt);
transition select(h.opt.opt) {
0x0: parse_e;
0x1: parse_h;
default: accept;
}
}

state parse_e {
pkt.extract(h.u.e);
transition accept;
}

state parse_h {
pkt.extract(h.u.h);
transition accept;
}
}

control vrfy(inout Headers h, inout Meta meta) {
apply { }
}

control ingress(inout Headers h, inout Meta m, inout standard_metadata_t s) {
apply {
h.u.e.setInvalid();
}
}

control egress(inout Headers h, inout Meta m, inout standard_metadata_t s) {
apply { }
}

control update(inout Headers h, inout Meta m) {
apply { }
}

control deparser(packet_out pkt, in Headers h) {
apply {
pkt.emit(h);
}
}

V1Switch(p(), vrfy(), ingress(), egress(), update(), deparser()) main;
80 changes: 80 additions & 0 deletions backends/p4tools/modules/testgen/targets/bmv2/test/p4-programs/bmv2_invalid_hu_2.p4
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,80 @@
#include <v1model.p4>

header opt_t {
bit<8> opt;
}

header ethernet_t {
bit<48> dst_addr;
bit<48> src_addr;
bit<16> eth_type;
}

header H {
bit<8> a;
bit<8> a1;
bit<8> b;
}

header_union U {
ethernet_t e;
H h;
}

struct Headers {
opt_t opt;
U u;
}

struct Meta {}

parser p(packet_in pkt, out Headers h, inout Meta meta, inout standard_metadata_t stdmeta) {
state start {
pkt.extract(h.opt);
transition select(h.opt.opt) {
0x0: parse_e;
0x1: parse_h;
default: accept;
}
}

state parse_e {
pkt.extract(h.u.e);
transition invalidate;
}

state parse_h {
pkt.extract(h.u.h);
transition invalidate;
}

state invalidate {
h.u.e.setInvalid();
transition accept;
}
}

control vrfy(inout Headers h, inout Meta meta) {
apply { }
}

control ingress(inout Headers h, inout Meta m, inout standard_metadata_t s) {
apply {
}
}

control egress(inout Headers h, inout Meta m, inout standard_metadata_t s) {
apply { }
}

control update(inout Headers h, inout Meta m) {
apply { }
}

control deparser(packet_out pkt, in Headers h) {
apply {
pkt.emit(h);
}
}

V1Switch(p(), vrfy(), ingress(), egress(), update(), deparser()) main;