Reduce overtainting by short-circuiting some expressions and extern i…

…nvocations. (#4030)
p4lang · Jun 15, 2023 · df6c77d · df6c77d
1 parent c73abda
commit df6c77d
Show file tree

Hide file tree

Showing 2 changed files with 41 additions and 2 deletions.
diff --git a/backends/p4tools/common/lib/taint.cpp b/backends/p4tools/common/lib/taint.cpp
@@ -112,6 +112,22 @@ bool Taint::hasTaint(const IR::Expression *expr) {
         return false;
     }
     if (const auto *binaryExpr = expr->to<IR::Operation_Binary>()) {
+        // We can short-circuit '&&'...
+        if (const auto *lAndExpr = binaryExpr->to<IR::LAnd>()) {
+            if (const auto *boolVal = lAndExpr->left->to<IR::BoolLiteral>()) {
+                if (!boolVal->value) {
+                    return false;
+                }
+            }
+        }
+        // ...and '||' in some cases.
+        if (const auto *lOrExpr = binaryExpr->to<IR::LOr>()) {
+            if (const auto *boolVal = lOrExpr->left->to<IR::BoolLiteral>()) {
+                if (boolVal->value) {
+                    return false;
+                }
+            }
+        }
         return hasTaint(binaryExpr->left) || hasTaint(binaryExpr->right);
     }
     if (const auto *unaryExpr = expr->to<IR::Operation_Unary>()) {

diff --git a/backends/p4tools/modules/testgen/targets/bmv2/expr_stepper.cpp b/backends/p4tools/modules/testgen/targets/bmv2/expr_stepper.cpp
@@ -1489,6 +1489,17 @@ void Bmv2V1ModelExprStepper::evalExternMethodCall(const IR::MethodCallExpression
              const auto *algo = args->at(3)->expression;
              const auto *oneBitType = IR::getBitType(1);
 
+             // In some cases the condition is false already. No need to do complex processing then.
+             if (const auto *boolVal = verifyCond->to<IR::BoolLiteral>()) {
+                 if (!boolVal->value) {
+                     auto &taintedState = state.clone();
+                     taintedState.popBody();
+                     result->emplace_back(taintedState);
+                     return;
+                 }
+             }
+
+             // Handle the case where the condition might be true.
              // If the condition is tainted or the input data is tainted, the checksum error
              // will not be reliable.
              if (argsAreTainted) {
@@ -1502,8 +1513,6 @@ void Bmv2V1ModelExprStepper::evalExternMethodCall(const IR::MethodCallExpression
                  return;
              }
 
-             // Handle the case where the condition is true.
-
              // Generate the checksum arguments.
              auto *checksumArgs = new IR::Vector<IR::Argument>();
              checksumArgs->push_back(new IR::Argument(checksumValue));
@@ -1603,6 +1612,20 @@ void Bmv2V1ModelExprStepper::evalExternMethodCall(const IR::MethodCallExpression
              const auto *checksumVarType = checksumVar->type;
              const auto *data = args->at(1)->expression;
              const auto *algo = args->at(3)->expression;
+
+             // In some cases the condition is false already. No need to do complex processing then.
+             if (const auto *boolVal = updateCond->to<IR::BoolLiteral>()) {
+                 if (!boolVal->value) {
+                     auto &taintedState = state.clone();
+                     taintedState.popBody();
+                     result->emplace_back(taintedState);
+                     return;
+                 }
+             }
+
+             // Handle the case where the condition might be true.
+             // If the condition is tainted or the input data is tainted, the checksum error
+             // will not be reliable.
              // If the condition is tainted or the input data is tainted.
              // The checksum will also be tainted.
              if (argsAreTainted) {