From a9f53c1a8bb05a3ea4ef568090596ed2c2fb77b1 Mon Sep 17 00:00:00 2001 From: fruffy Date: Wed, 9 Aug 2023 11:09:06 +0200 Subject: [PATCH] Encode more P4Runtime constraints for the behavioral model. --- .../testgen/targets/bmv2/table_stepper.cpp | 44 ++++++++++++------- 1 file changed, 28 insertions(+), 16 deletions(-) diff --git a/backends/p4tools/modules/testgen/targets/bmv2/table_stepper.cpp b/backends/p4tools/modules/testgen/targets/bmv2/table_stepper.cpp index af7438fe39d..3625ae51982 100644 --- a/backends/p4tools/modules/testgen/targets/bmv2/table_stepper.cpp +++ b/backends/p4tools/modules/testgen/targets/bmv2/table_stepper.cpp @@ -8,6 +8,7 @@ #include +#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" @@ -40,14 +41,14 @@ 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) { @@ -55,17 +56,26 @@ const IR::Expression *Bmv2V1ModelTableStepper::computeTargetMatchType( 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) { @@ -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. @@ -393,10 +403,12 @@ void Bmv2V1ModelTableStepper::checkTargetProperties( void Bmv2V1ModelTableStepper::evalTargetTable( const std::vector &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; @@ -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. @@ -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.