Make P4-Constraints Typechecker Idempotent

Dockerfile

@@ -14,7 +14,7 @@
 #
 # SPDX-License-Identifier: Apache-2.0
 
-FROM ubuntu:16.04
+FROM ubuntu:24.04
 
 ARG DEBIAN_FRONTEND=noninteractive
 

README.md

@@ -181,14 +181,14 @@ bazel test //...                                    # Run tests in container.
 
 The easiest way to experiment with p4-constraints is to write a
 [golden test](https://ro-che.info/articles/2017-12-04-golden-tests).
-We provide [Bazel rules](e2e_test/p4check.bzl) `run_p4check` and `diff_test` to
+We provide [Bazel rules](e2e_tests/p4check.bzl) `run_p4check` and `diff_test` to
 make this convenient.
-See the [e2e_test/](e2e_test/) folder -- in particular
-[e2e_test/BUILD.bazel](e2e_test/BUILD.bazel) -- for examples of how to use them.
+See the [e2e_tests/](e2e_tests/) folder -- in particular
+[e2e_tests/BUILD.bazel](e2e_tests/BUILD.bazel) -- for examples of how to use them.
 
 To run all golden tests, execute
 ```sh
-bazel test //e2e_test/...
+bazel test //e2e_tests/...
 ```
 [Recall](#building) that this will build p4c and requires
 [Bison](https://en.wikipedia.org/wiki/GNU_Bison) and
@@ -204,7 +204,7 @@ bazel run //e2e_test:invalid_constraints_test
 
 The `p4check` CLI allows invoking the p4-constraints library from the command
 line. The most convenient way to run `p4check` is using the
-[`run_p4check`-rule](e2e_test/p4check.bzl), as is done for
+[`run_p4check`-rule](e2e_tests/p4check.bzl), as is done for
 [golden testing](#golden-tests).
 
 To learn how to invoke [p4check](p4_constraints/cli/p4check.cc) manually,
@@ -217,7 +217,7 @@ bazel run p4_constraints/cli:p4check -- --help
 
 See [docs/language-specification.md](docs/language-specification.md) for a
 documentation of the constraint languages, or look at some example constraints
-in the .p4-files in the [e2e_test folder](e2e_test/).
+in the .p4-files in the [e2e_tests folder](e2e_tests/).
 
 ## Contributing
 

format.sh

@@ -25,4 +25,5 @@ find . -not -path "./third_party/**" \
   | egrep "\.(${CLANG_FORMAT_EXTENSIONS})\$" \
   | xargs clang-format --verbose -style=google -i
 
-bazel run -- @buildifier_prebuilt//:buildifier --lint=fix -r .
+bazel run -- \
+  @buildifier_prebuilt//:buildifier --lint=fix -r $(bazel info workspace)

p4_constraints/backend/type_checker.cc

@@ -109,7 +109,33 @@ bool StrictlyAboveInCastabilityOrder(const Type& left, const Type& right) {
       return false;
   }
 }
+// Returns true if 'left' is exactly one level above 'right' in the castability
+// order. This ensures that casts only move one level up the Hasse diagram.
+bool OneLevelAboveInCastabilityOrder(const Type& left, const Type& right) {
+  // Check if left is strictly above right in the castability order
+  if (!StrictlyAboveInCastabilityOrder(left, right)) {
+    return false;
+  }
+
+  // Now check that there isn't an intermediate type between them
+  // For the specific Hasse diagram used in P4-Constraints:
+
+  // Case 1: right is arbitrary_int, left must be fixed_unsigned
+  if (right.type_case() == Type::kArbitraryInt) {
+    return left.type_case() == Type::kFixedUnsigned;
+  }
 
+  // Case 2: right is fixed_unsigned, left must be one of the match types
+  if (right.type_case() == Type::kFixedUnsigned) {
+    return left.type_case() == Type::kExact ||
+           left.type_case() == Type::kTernary ||
+           left.type_case() == Type::kLpm || left.type_case() == Type::kRange ||
+           left.type_case() == Type::kOptionalMatch;
+  }
+
+  // No other valid one-level jumps in the hierarchy
+  return false;
+}
 // Returns the least upper bound of the given types in the castability ordering.
 //
 // The least upper bound (join, supremum) is the lowest common ancestor of the
@@ -325,11 +351,25 @@ absl::Status InferAndCheckTypes(Expression* expr, const ActionInfo* action_info,
       return absl::OkStatus();
     }
 
-    case ast::Expression::kTypeCast:
-      return StaticTypeError(constraint_source, expr->start_location(),
-                             expr->end_location())
-             << "type casts should only be inserted by the type checker";
+    case ast::Expression::kTypeCast: {
+      // Type check the inner expression first
+      Expression* inner_expr = expr->mutable_type_cast();
+      RETURN_IF_ERROR(InferAndCheckTypes(inner_expr, action_info, table_info));
 
+      const Type& target_type = expr->type();
+      const Type& inner_type = inner_expr->type();
+
+      // Validate the cast is exactly one level in the castability order
+      if (!OneLevelAboveInCastabilityOrder(target_type, inner_type)) {
+        return StaticTypeError(constraint_source, expr->start_location(),
+                               expr->end_location())
+               << "invalid type cast from " << TypeName(inner_type) << " to "
+               << TypeName(target_type)
+               << " - must be a single-step cast in the type hierarchy";
+      }
+
+      return absl::OkStatus();
+    }
     case Expression::kBinaryExpression: {
       BinaryExpression* bin_expr = expr->mutable_binary_expression();
       Expression* left = bin_expr->mutable_left();

p4_constraints/backend/type_checker_test.cc

@@ -388,7 +388,28 @@ TEST_F(InferAndCheckTypesTest, IllegalTypeCastEqualityComparisonFails) {
     }
   }
 }
+TEST_F(InferAndCheckTypesTest, IdempotentTypeCastHandling) {
+  const std::pair<std::string, std::string> castable_pairs[] = {
+      {"int", "bit16"}, {"int", "exact32"}, {"bit32", "exact32"}};
+  for (ast::BinaryOperator op : {ast::EQ, ast::NE}) {
+    for (std::pair<std::string, std::string> left_right : castable_pairs) {
+      Expression expr = ParseTextProtoOrDie<Expression>(
+          absl::Substitute(R"pb(
+                             binary_expression {
+                               binop: $0
+                               left { key: "$1" }
+                               right { key: "$2" }
+                             })pb",
+                           op, left_right.first, left_right.second));
 
+      ASSERT_THAT(InferAndCheckTypes(&expr, kTableInfo), IsOk())
+          << "First type check failed: " << expr.DebugString();
+      // Idempotent type cast test.
+      ASSERT_THAT(InferAndCheckTypes(&expr, kTableInfo), IsOk())
+          << "Idempotence test failed: " << expr.DebugString();
+    }
+  }
+}
 TEST_F(InferAndCheckTypesTest, BinaryBooleanOperators) {
   for (ast::BinaryOperator op : {ast::AND, ast::OR, ast::IMPLIES}) {
     // Positive tests.
@@ -561,5 +582,4 @@ TEST_F(InferAndCheckTypesTest, AttributeAccessTypeChecks) {
   ASSERT_OK(InferAndCheckTypes(&expr, kTableInfo)) << expr.DebugString();
   EXPECT_EQ(expr.type(), kArbitraryInt) << expr.DebugString();
 }
-
-}  // namespace p4_constraints
+}  // namespace p4_constraints