diff --git a/Dockerfile b/Dockerfile index 8619b03..094b973 100644 --- a/Dockerfile +++ b/Dockerfile @@ -14,7 +14,7 @@ # # SPDX-License-Identifier: Apache-2.0 -FROM ubuntu:16.04 +FROM ubuntu:24.04 ARG DEBIAN_FRONTEND=noninteractive diff --git a/README.md b/README.md index 4bfce45..c85086e 100644 --- a/README.md +++ b/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 diff --git a/format.sh b/format.sh index 9752b31..f2795a8 100755 --- a/format.sh +++ b/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) diff --git a/p4_constraints/backend/type_checker.cc b/p4_constraints/backend/type_checker.cc index ebca57b..b0fe3ac 100644 --- a/p4_constraints/backend/type_checker.cc +++ b/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(); diff --git a/p4_constraints/backend/type_checker_test.cc b/p4_constraints/backend/type_checker_test.cc index 087c4b5..20200fe 100644 --- a/p4_constraints/backend/type_checker_test.cc +++ b/p4_constraints/backend/type_checker_test.cc @@ -388,7 +388,28 @@ TEST_F(InferAndCheckTypesTest, IllegalTypeCastEqualityComparisonFails) { } } } +TEST_F(InferAndCheckTypesTest, IdempotentTypeCastHandling) { + const std::pair castable_pairs[] = { + {"int", "bit16"}, {"int", "exact32"}, {"bit32", "exact32"}}; + for (ast::BinaryOperator op : {ast::EQ, ast::NE}) { + for (std::pair left_right : castable_pairs) { + Expression expr = ParseTextProtoOrDie( + 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 \ No newline at end of file