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

[P4Testgen] Encode more P4Runtime constraints for the behavioral model #4103

Merged
merged 1 commit into from
Oct 3, 2023
Merged

[P4Testgen] Encode more P4Runtime constraints for the behavioral model #4103

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
44 changes: 28 additions & 16 deletions backends/p4tools/modules/testgen/targets/bmv2/table_stepper.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@

#include <boost/multiprecision/cpp_int.hpp>

#include "backends/p4tools/common/lib/constants.h"
#include "backends/p4tools/common/lib/trace_event_types.h"
#include "backends/p4tools/common/lib/variables.h"
#include "ir/declaration.h"
Expand Down Expand Up @@ -40,32 +41,41 @@ const IR::Expression *Bmv2V1ModelTableStepper::computeTargetMatchType(
const TableUtils::KeyProperties &keyProperties, TableMatchMap *matches,
const IR::Expression *hitCondition) {
const IR::Expression *keyExpr = keyProperties.key->expression;
const auto &testgenOptions = TestgenOptions::get();

// TODO: We consider optional match types to be a no-op, but we could make them exact matches.
if (keyProperties.matchType == BMv2Constants::MATCH_KIND_OPT) {
if (keyProperties.matchType == BMv2Constants::MATCH_KIND_OPT ||
keyProperties.matchType == P4Constants::MATCH_KIND_TERNARY) {
cstring keyName = properties.tableName + "_key_" + keyProperties.name;
const auto *ctrlPlaneKey = ToolsVariables::getSymbolicVariable(keyExpr->type, keyName);
// We can recover from taint by simply not adding the optional match.
// Create a new symbolic variable that corresponds to the key expression.
const IR::Expression *ternaryMask = nullptr;
// We can recover from taint by inserting a ternary match that is 0.
const auto *wildCard = IR::getConstant(keyExpr->type, 0);
if (keyProperties.isTainted) {
matches->emplace(keyProperties.name,
new Ternary(keyProperties.key, ctrlPlaneKey, wildCard));
return hitCondition;
}
cstring maskName = properties.tableName + "_mask_" + keyProperties.name;
const auto *fullMatch = IR::getMaxValueConstant(keyExpr->type);
ternaryMask = ToolsVariables::getSymbolicVariable(keyExpr->type, maskName);
auto *maskCond =
new IR::LOr(new IR::Equ(ternaryMask, wildCard), new IR::Equ(ternaryMask, fullMatch));
matches->emplace(keyProperties.name,
new Ternary(keyProperties.key, ctrlPlaneKey, wildCard));
return new IR::LAnd(
hitCondition,
new IR::LAnd(maskCond, new IR::Equ(new IR::BAnd(keyExpr, ternaryMask),
new IR::BAnd(ctrlPlaneKey, ternaryMask))));
// Calculate the conditions for the ternary or optional match.
const auto *ternaryMask = ToolsVariables::getSymbolicVariable(
keyExpr->type, properties.tableName + "_mask_" + keyProperties.name);
// Encode P4Runtime constraints for PTF and Protobuf tests.
// (https://p4.org/p4-spec/docs/p4runtime-spec-working-draft-html-version.html#sec-match-format)
if (testgenOptions.testBackend == "PTF" || testgenOptions.testBackend == "PROTOBUF") {
hitCondition = new IR::LAnd(
hitCondition, new IR::Equ(new IR::BAnd(ctrlPlaneKey, ternaryMask), ctrlPlaneKey));
}
// Optional matches are either a ternary exact match or are fully wildcarded.
if (keyProperties.matchType == BMv2Constants::MATCH_KIND_OPT) {
const auto *fullMatch = IR::getMaxValueConstant(keyExpr->type);
hitCondition =
new IR::LAnd(hitCondition, new IR::LOr(new IR::Equ(ternaryMask, wildCard),
new IR::Equ(ternaryMask, fullMatch)));
}
return new IR::LAnd(hitCondition, new IR::Equ(new IR::BAnd(keyExpr, ternaryMask),
new IR::BAnd(ctrlPlaneKey, ternaryMask)));
}
// Action selector entries are not part of the match.
if (keyProperties.matchType == BMv2Constants::MATCH_KIND_SELECTOR) {
Expand All @@ -74,7 +84,7 @@ const IR::Expression *Bmv2V1ModelTableStepper::computeTargetMatchType(
}
// Ranges are not yet implemented for BMv2 STF tests.
if (keyProperties.matchType == BMv2Constants::MATCH_KIND_RANGE &&
TestgenOptions::get().testBackend != "STF") {
testgenOptions.testBackend != "STF") {
cstring minName = properties.tableName + "_range_min_" + keyProperties.name;
cstring maxName = properties.tableName + "_range_max_" + keyProperties.name;
// We can recover from taint by matching on the entire possible range.
Expand Down Expand Up @@ -393,10 +403,12 @@ void Bmv2V1ModelTableStepper::checkTargetProperties(
void Bmv2V1ModelTableStepper::evalTargetTable(
const std::vector<const IR::ActionListElement *> &tableActionList) {
const auto *keys = table->getKey();
const auto &testgenOptions = TestgenOptions::get();

// If we have no keys, there is nothing to match.
if (keys == nullptr) {
// Either override the default action or fall back to executing it.
auto testBackend = TestgenOptions::get().testBackend;
auto testBackend = testgenOptions.testBackend;
if (testBackend == "STF" && !properties.defaultIsImmutable) {
setTableDefaultEntries(tableActionList);
return;
Expand Down Expand Up @@ -424,7 +436,7 @@ void Bmv2V1ModelTableStepper::evalTargetTable(
case TableImplementation::selector: {
// If an action selector is attached to the table, do not assume normal control plane
// behavior.
if (TestgenOptions::get().testBackend != "STF") {
if (testgenOptions.testBackend != "STF") {
evalTableActionSelector(tableActionList);
} else {
// We can only generate profile entries for PTF and Protobuf tests.
Expand All @@ -437,7 +449,7 @@ void Bmv2V1ModelTableStepper::evalTargetTable(
case TableImplementation::profile: {
// If an action profile is attached to the table, do not assume normal control plane
// behavior.
if (TestgenOptions::get().testBackend != "STF") {
if (testgenOptions.testBackend != "STF") {
evalTableActionProfile(tableActionList);
} else {
// We can only generate profile entries for PTF and Protobuf tests.
Expand Down