verified-network-toolchain / petr4

Petr4: Formal Semantics for P4
Apache License 2.0
75 stars 21 forks source link

Fix even more STF tests #395

Closed hackedy closed 1 year ago

hackedy commented 1 year ago

This pull request fixes the following issues.

  1. A bug in the STF testing framework that was comparing expected and actual packets incorrectly.
  2. A bug in the v1model semantics that threw out unparsed packet body instead of forwarding it along to be joined with the deparser output.
  3. An accidentally deleted lookup_func in the definition of exec_call.
  4. Silent failure in get_arg_directions
  5. Construction of ill-typed ActionRefs by unwrap_action_ref, which caused problems in get_arg_directions.

Qinshi, can you let me know if any of this breaks VerifiableP4? Thanks.

hackedy commented 1 year ago

Fixes #394