verified-network-toolchain / petr4

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

Refactor command-line interface #365

Closed hackedy closed 1 year ago

hackedy commented 1 year ago

This PR makes the petr4.exe command-line interface more uniform and hopefully more understandable. I've created -output-LANG flags for each IR which accept a filename as argument and choose what kind of pretty printer to use based on the extension of the filename. So if you write -output-p4light file.v you get a Gallina version of the AST, but -output-p4light file.p4 will print concrete P4 syntax.

% dune exec -- petr4 -help
Petr4: A reference implementation of the P4_16 language

  petr4 FILE.P4

=== flags ===

  [-I dir] ...               . Paths to search for files sourced with #include
                               directives.
  [-gen-loc]                 . Infer locators in P4light AST after typechecking.
  [-normalize]               . Simplify expressions.
  [-output-c file]           . Output C to the specified file.
  [-output-gcl file]         . Output GCL to the specified file.
  [-output-p4cub file]       . Output P4Cub to the specified file.
  [-output-p4flat file]      . Output P4flat to the specified file.
  [-output-p4light file]     . Output P4light to the specified file.
  [-output-p4surface file]   . Output P4surface AST to the specified file.
  [-unroll-parsers depth]    . Unroll parsers to given depth.
  [-v]                       . Be more verbose.
  [-build-info]              . print info about this build and exit
  [-version]                 . print the version of this build and exit
  [-help], -?                . print this help text and exit
hackedy commented 1 year ago

Right now it's just compiler passes, not evaluation, and I haven't tried to iron any bugs out yet.

The "p4flat" IR does not exist yet but I know what I want it to look like (sort of like Inline.v from the GCL compiler but with declarations).

TODOs

hackedy commented 1 year ago

I think this is fully baked now.