Make P4-Constraints Typechecker Idempotent

[sumit7754]

Current Behavior:

• The function performs type checking on an expression.
• If the expression has already been type checked, it explicitly fails (likely throws an error or returns a non-success status).

Desired Behavior (Idempotence):

• The function should perform type checking on an expression.
• If the expression has already been type checked and the types are valid, the function shouldn't modify the existing type information or cause any errors.
• If the expression has already been type checked but has type errors, the function should still report the errors (existing error handling logic should remain intact).

[smolkaj]

Thanks for the suggestion. I agree that on the surface, this seems like much nicer behavior.

Would you be able/willing to share some additional context on how/where you're running into this, and what issues it is causing?

In terms of implementation, I think the main gap is that the type checker inserts type casts into the AST during type checking, but errors out if the AST already contains type casts. This was mostly done for simplicity, since no one has had a need to support it thus far. I don't expect this would be hard to support.

[sumit7754]

This task was assigned to me by @jonathan-dilorenzo. I proposed a solution in which I checked the isTypeChecked boolean. If it was true, I returned the result; otherwise, I continued with the same flow. However, Jonathan pointed out that this approach could lead to redundancy issues. Now, I am considering two solutions:

1. Caching: This approach involves storing the inferred type of a subexpression for future use.
2. Recursive function: This approach involves creating a recursive function that traverses the expression tree to identify any type cast nodes.
   Can you please guide me further to fix it?

[smolkaj]

I'd like to encourage you to pursue the second approach, since introducing additional state/caching opens a new can of worms: what is the behavior if the state/cache gets into an in inconsistent state? How to unit test our code well, now that it depends on additional state? Etc.

For the second approach, take a look at InferAndCheckTypes, which is the recursive function traversing the expression tree that is currently implementing type checking. What's missing is support for type casts: https://github.com/p4lang/p4-constraints/blob/master/p4_constraints/backend/type_checker.cc#L327-L330

    case ast::Expression::kTypeCast:
      return StaticTypeError(constraint_source, expr->start_location(),
                             expr->end_location())
             << "type casts should only be inserted by the type checker";

[sumit7754]

Thank you for the feedback and suggestions.

I'll focus on implementing the second approach, as it aligns better with our current implementation and minimizes the risk of introducing complexities.

I'll review the code and work on adding support for type casts within the expression tree traversal and keep you updated on the progress.

[smolkaj]

The casts we want to allow are documented here:

// Castability of types is given by the following Hasse diagram, where lower
// types can be cast to higher types (but not vice versa):
//
//   exact<W>  ternary<W>  lpm<W>  range<W>  optional<W>
//           \_________ \ /  _____/_________/
//                     bit<W>
//                       |
//                  arbitrary_int
//
// Types missing from the diagram cannot be cast to any other types. Formally,
// castability is a partial order on types.

A cast to type T is allowed if you can get from the type of the wrapped expression, T', to T via a single upward edge in the diagram.

[sumit7754]

Here is my approach please look into this :

1. Identify type cast expressions (kTypeCast) within the AST by traversing the expression tree.
2. Check the partial order defined by the Hasse diagram to ensure a single upward edge exists from the type of the wrapped expression to the target type, validating the type cast.
3. If the type cast is valid, mutate the expression's type to the target type. Mutation occurs only if the input type is lower than the target type in the partial order.
4. Return a descriptive message if the type cast is invalid based on the partial order, providing clear error information.

Looking forward to your thoughts on this.

[sumit7754]

@smolkaj Could you please review my approach so that I can proceed further? It would be very helpful.

[smolkaj]

I’m currently at a conference, so please expect some delay on this. I will get to it next week.

…

On Tue, Apr 23, 2024 at 21:50 sumit7754 ***@***.***> wrote: @smolkaj <https://github.com/smolkaj> Could you please review my approach so that I can proceed further? It would be very helpful. — Reply to this email directly, view it on GitHub <#140 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABSVS4X4GG6LMCS5G2DBYGLY64FXPAVCNFSM6AAAAABGGGT732VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDANZTHA2DENZQGE> . You are receiving this because you were mentioned.Message ID: ***@***.***>

[sumit7754]

Thank you, Steffen, for taking the time to update me. I'll await further information. On Thu, 25 Apr 2024 at 06:08, Steffen Smolka ***@***.***> wrote:

…

I’m currently at a conference, so please expect some delay on this. I will get to it next week. On Tue, Apr 23, 2024 at 21:50 sumit7754 ***@***.***> wrote: > @smolkaj <https://github.com/smolkaj> Could you please review my approach > so that I can proceed further? It would be very helpful. > > — > Reply to this email directly, view it on GitHub > < #140 (comment)>, > or unsubscribe > < https://github.com/notifications/unsubscribe-auth/ABSVS4X4GG6LMCS5G2DBYGLY64FXPAVCNFSM6AAAAABGGGT732VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDANZTHA2DENZQGE> > . > You are receiving this because you were mentioned.Message ID: > ***@***.***> > — Reply to this email directly, view it on GitHub <#140 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/A7557SWXHYMQKS3DEG5CUZ3Y7BF6RAVCNFSM6AAAAABGGGT732VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDANZWGEYDINZRHE> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[smolkaj]

Here is my approach please look into this :

1. Identify type cast expressions (kTypeCast) within the AST by traversing the expression tree.
2. Check the partial order defined by the Hasse diagram to ensure a single upward edge exists from the type of the wrapped expression to the target type, validating the type cast.
3. If the type cast is valid, mutate the expression's type to the target type. Mutation occurs only if the input type is lower than the target type in the partial order.
4. Return a descriptive message if the type cast is invalid based on the partial order, providing clear error information.

Looking forward to your thoughts on this.

Sorry for the delay. This looks great, please proceed. 👍

[jameshu15869]

In terms of implementation, I think the main gap is that the type checker inserts type casts into the AST during type checking, but errors out if the AST already contains type casts. This was mostly done for simplicity, since no one has had a need to support it thus far. I don't expect this would be hard to support.

I reproduced this error by adding a second call to InferAndCheckTypes() in LegalTypeCastEqualityComparisonTypeChecks after the check ensuring that the operand types match.

Since type casts aren't exposed in the surface language to the user, can we expect that any (valid) type casts encountered were inserted by the type checker and thus already a properly type checked expression?

In that case, can we just check if an encountered type cast expression is valid in the castability order and return Ok/Error accordingly?

Please let me know if I'm misunderstanding something!

[Kaiwen-Guo]

It seems like if we can assume that any type cast node was inserted by a previous run of the typechecker like what James proposed, kTypeCast can be modified to:

1. Get the inner expression and its type
2. Calls StrictlyAboveInCastabilityOrder by passing in target type and inner type, and return any static type errors found.
3. If no errors found, return OkStatus

thus by modifying the kTypeCast like below, it can passed an additional IdempotentTypeCastHandling test:

    case ast::Expression::kTypeCast: {
      // Get the inner expression and its type
      Expression* inner_expr = expr->mutable_type_cast();
      const Type& target_type = expr->type();
      const Type& inner_type = inner_expr->type();
      
      // Validate the cast according to the castability partial order
      if (!StrictlyAboveInCastabilityOrder(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);
      }
      
      return absl::OkStatus();
    }

Let me know if this is what we are thinking of! If so, I will create a MR with the modification to kTypeCast and the additional test in type_checker_test.cc

[smolkaj]

Since type casts aren't exposed in the surface language to the user, can we expect that any (valid) type casts encountered were inserted by the type checker and thus already a properly type checked expression?

Ideally we wouldn't make that assumption to simplify the contract and avoid future surprises. How hard would it be to implement things without that assumption?

[smolkaj]

Perhaps we could define a function OneLevelAboveInCastabilityOrder similar to StrictlyAboveInCastabilityOrder, and check that all casts increase the type level by 1 using that function?

[jameshu15869]

How hard would it be to implement things without that assumption?

Would the goal then be to simplify nested casts? I think I'm confused on why you need to verify that all casts increase the type by exactly 1.

Do you by any chance have an example of desired behavior from a second idempotent call to InferAndCheckTypes()? i.e. should the second call do anything other than continue type checking inside the expression that was casted from?