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 https://github.com/p4lang/p4-constraints/issues/140#issuecomment-2073842701, 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 < https://github.com/p4lang/p4-constraints/issues/140#issuecomment-2073842701>,

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 https://github.com/p4lang/p4-constraints/issues/140#issuecomment-2076104719, 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. :+1: