verified-network-toolchain / petr4

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

Fix some STF tests #387

Closed hackedy closed 1 year ago

hackedy commented 1 year ago

~Not yet ready for merge~ Ready, I think.

hackedy commented 1 year ago

Update on the interpreter test suite (the STF tests, make test-stf). I have it down to 90 failures on this branch, compared with 143 failures on poulet4 (as you might guess there are 143 tests total). Most of the fixes were directed at tests that were failing by going wrong somewhere in the interpreter, rather than successfully executing and just producing the wrong output packets. I have fixed all of these "going wrong" errors except for (1) Unimplemented externs, architectures, etc etc. and (2) Some kind of overloading or arity related problem that causes a failure in interp_args.

I made an invasive fix to (2) that ultimately didn't work so I am going to go back to the drawing board next week and see if I can resolve it with less impact to e.g. the type system and program logic. And I think I can implement the missing externs etc pretty quickly by cribbing from the OCaml implementation.

The other invasive fix is that we need a way to add new rules to tables at run time in order to support the stf Add command.

And then there's a ton of failures that are genuine failures in what shows up in the packet at the end of the test; I haven't investigated these at all yet.

hackedy commented 1 year ago

If I can revert my invasive fix for the interp_arg problem, the merge conflicts with Typing/ should go away and I'd like to merge. Hopefully I can take a look at that later today.

hackedy commented 1 year ago

After reverting the invasive changes around interp_arg it's back up to 91 failures.

hackedy commented 1 year ago

Oops, I left some stuff in InterpreterSafe commented out. Will fix that today.

hackedy commented 1 year ago

@QinshiWang can you take a look at this? I want to merge today or tomorrow.