Skip to content

Commit

Permalink
Encode more P4Runtime constraints for the behavioral model.
Browse files Browse the repository at this point in the history
  • Loading branch information
@fruffy
fruffy committed Aug 26, 2023
1 parent 5824a6b commit afd3598
Showing 1 changed file with 28 additions and 16 deletions.
44 changes: 28 additions & 16 deletions backends/p4tools/modules/testgen/targets/bmv2/table_stepper.cpp
View file
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

0 comments on commit afd3598

Please sign in to comment.