verified-network-toolchain / petr4

Petr4: Formal Semantics for P4
Apache License 2.0
73 stars 20 forks source link

Poulet4 p4light match #399

Closed rudynicolop closed 1 year ago

rudynicolop commented 1 year ago

In progress pull request for p4light Match, MatchPreT, and ValueSet.

These changes are to make Match and MatchPreT use ValueSet instead of Expression.

Match and MatchPreT are parameterized by the data type for p4 types and value sets/patterns. In p4light syntax and semantics this is always instantiated with P4Type and ValueSet. This is to enable a broader interface for Target.v that does not rely upon p4light data types.

I'm currently stuck refactoring exec_match in Semantics.v. Match uses ValueSet for mask and range operands but ValueSet usesValueBase for mask and range operands. Match used to use Expression and evaluate the expressions to values for this but in changing it to ValueSet it's not as straightforward to "evaluate" a ValueSet to a value. Should ValueSet use ValueSet for mask and range?

QinshiWang commented 1 year ago

I'm very confused about your changes. Maybe we should have a discussion. First, what is BigValue.v? I believe it's something we have deliberately removed in P4light.

rudynicolop commented 1 year ago

I'm very confused about your changes. Maybe we should have a discussion. First, what is BigValue.v? I believe it's something we have deliberately removed in P4light.

I want Match to use ValueSet instead of Expression.

I had to split Value.v into 2 files, now Value.v and BigValue.v. There was a potential circular dependency when attempting to make Match and MatchPreT use upon ValueSet.

If ValueSet.v were to remain in Value.v, then Syntax.v could not use ValueSet in Match b/c ValueLvalue and ValueTable are in Value.v and they use Syntax.v. If ValueSet moves to Syntax.v then now Syntax.v depends upon Value.v which already depends upon Syntax.v becayse of ValueLvalue and ValueTable.

To resolve this I moved ValueSet to Syntax.v, and moved the remaining definitions such as ValueLvalue and ValueTable to a new file BigValue.v (I didn't know what to call it there's probably a better name). So now Value.v <- Syntax.v <- BigValue.v.

hackedy commented 1 year ago

I am all for making Match use ValueSet instead of Expression. But parametrizing match over values and having to inject little helper functions to deal with its type parameters everywhere smells like over-engineering to me. Targets only use P4light values right now and we should stay consistent with that convention.

QinshiWang commented 1 year ago

Why ValueSet has a constructor of unevaluated match expressions? | ValSetValueSet (size: N) (members: list (list (@Syntax.Match tags_t))) (sets: list ValueSet).

hackedy commented 1 year ago

Wait, yeah. Matches should have expressions in them and should not appear in run-time state. Matches should evaluate to ValueSets and appear in run-time state. We've got it mixed up.

rudynicolop commented 1 year ago

Should Target.v use ValueSet instead of Match then?

rudynicolop commented 1 year ago

Why ValueSet has a constructor of unevaluated match expressions? | ValSetValueSet (size: N) (members: list (list (@Syntax.Match tags_t))) (sets: list ValueSet).

I have no idea 😅. What should members be?

hackedy commented 1 year ago

It might clarify matters to call these things PatternExpr and PatternValue instead of Match and ValueSet.

rudynicolop commented 1 year ago

I think this branch's changes got out of hand. I propose instead:

I'll delete this branch and start a new one.

hackedy commented 1 year ago

I think this branch's changes got out of hand. I propose instead:

  • Match and MatchPreT are left unchanged from before this branch (still using expressions).
  • Match is removed from ValueSet.
  • ValueSet is used in place of Match in Target.v.

I'll delete this branch and start a new one.

I'm on board with this 👍

QinshiWang commented 1 year ago

I think this branch's changes got out of hand. I propose instead:

  • Match and MatchPreT are left unchanged from before this branch (still using expressions).
  • Match is removed from ValueSet.
  • ValueSet is used in place of Match in Target.v.

I'll delete this branch and start a new one.

Yes. This is also what I think.