Compiling Program Using NetKAT Syntax Extension Throws DynLoader.Error

[craig-riecke]

Compiling the sample program on the NetKAT Wiki page:

open Core.Std
open Async.Std
open Frenetic_NetKAT

let initial_policy : policy = <:netkat<port := pipe("controller")>>

yields:

ocamlfind ocamldep -syntax camlp4o -package frenetic.syntax -package frenetic.async -package frenetic -package async -package core -modules template_netkat_camlp4.ml > template_netkat_camlp4.ml.depends
+ ocamlfind ocamldep -syntax camlp4o -package frenetic.syntax -package frenetic.async -package frenetic -package async -package core -modules template_netkat_camlp4.ml > template_netkat_camlp4.ml.depends
Camlp4: Uncaught exception: DynLoader.Error ("/home/vagrant/.opam/system/lib/core/core.cma", "error while linking /home/vagrant/.opam/system/lib/core/core.cma.\nReference to undefined global `Condition'")

File "template_netkat_camlp4.ml", line 1:
Error: Error while running external preprocessor
Command line: camlp4 '-I' '/usr/lib/ocaml/camlp4' '-I' '/home/vagrant/.opam/system/lib/ulex' '-I' '/home/vagrant/.opam/system/lib/bytes' '-I' '/usr/li
...

Previously we fixed this by writing a script that runs camlp4 with the threads.cma library explicitly listed before Core. This no longer works, probably since Core tossed out camlp4 compatibility in 113.24, and was hacky anyway.

[smolkaj]

Maybe it's time to throw out camlp4 and replace it with ppx...

[basus]

Personally, I would love to have a way to make small extensions to the NetKAT syntax without writing a new parser every time. For example, I would like to have a "path" operator (==>) so that users can specify multihop paths in their policies and let a fabric compiler fill in the blanks. Off the top of my head, I'm not sure what's a good way to go about this. I'm not even sure if this is related to the syntax extension.

[smolkaj]

@basus: That's not really related. You could do that with the current architecture by modifying the lexer and parser appropriately.

[smolkaj]

Ok, I figured out how to get rid of camlp4, replace it with ppx, and make the whole lexing/parsing pipeline simpler and easier to extend. It's probably best to do this after #512 has been merged in.

[jnfoster]

@smolkaj does the fix you mentioned here still work? What's involved?

I'd like to fix issue #526. The main culprit is that
https://github.com/frenetic-lang/tutorials/blob/master/scripts/netkat-build
doesn't work any more (and also was hacky as it baked in specific incantations to camlp4).

Ideally we'd port the tutorial examples to PPX and then fix the build script.

-N

[jnfoster]

ps. I'm happy to do the legwork if you explain what you meant in the comment above.

[smolkaj]

Yes, we should do this! Here is what I had in mind:

Syntax

let%nk p = {| port := 1 |} in 
let%nk q = {| filter switch = 1; $p |} in
...

We may also want to support expressions:

{nk| port := 1 |nk}

ppx-extension

Should be easy following this blog post (just a "context-free extension expander"). However, we will need a parser of type string -> OCaml AST that can also handle anti-quotations ($p). Then, we simple look for let%nk p = s in e nodes, run x = parse s (at preprocessing time), and replace the node with let p = x in e.

Parser

We need to replace the Camlp4 parser. I suggest Menhir. Note that we actually need two parsers:

(* produces NetKAT AST *)
(* used to parse policy.kat files at runtime of the NetKAT compiler / Frenetic system *)
parser : string -> NetKAT.policy

(* produces OCaml AST *of* NetKAT AST: parser' s = parser s |> to_ocaml_ast *)
(* however, the equation above does not hold if s contains an antiquation, because `parser` cannot support them *)
(* used to parse embedded NetKAT at OCaml compile-time *)
parser' : string -> OCaml AST.

Since the parsers are identical up to semantic actions, it would be a shame to have two separate implementations, as we did in the past. I propose to have two semantic actions for each parse rule, and use CPPO to to produce two parsers from this one specification. I have a prototype of this at home, and it is quite clean. Let me post it here tonight.

How to build OCaml ASTs conveniently:
https://github.com/alainfrisch/ppx_tools/blob/master/ppx_metaquot.ml
https://github.com/alainfrisch/ppx_tools/blob/master/ast_convenience.mli

Lexer

I think we need to replace the lexer as well? Not sure what's the best option here. Here is an example of how to make menhir work with ulex. Looks pretty straight-forward: https://github.com/Drup/llvm/blob/3c43000f4e86af5b9b368f50721604957d403750/test/Bindings/OCaml/kaleidoscope/src/syntax.ml

Plan of Attack

I would implement things top-down in the order of my description: first the ppx-extension (with a dummy parser), than the parser, than the lexer.

[smolkaj]

@jnfoster: I will create a new branch tonight and push what I have.

[jnfoster]

Wonderful! I like the PPX design.

-N

On Thu, Nov 3, 2016 at 11:57 AM, Steffen Smolka notifications@github.com
wrote:

@jnfoster https://github.com/jnfoster: I will create a new branch
tonight and push what I have.

—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
#507 (comment),
or mute the thread
https://github.com/notifications/unsubscribe-auth/ABwi0jXzjXyZPfU2ljDLtDmmjYFTbb0Fks5q6i6GgaJpZM4I5ySf
.

[smolkaj]

Cool, let's push on this. Shouldn't be too much work. I just pushed a draft of the parser: https://github.com/frenetic-lang/frenetic/tree/ppx

I'll try to hack up a skeleton of the ppx extension. We also need a lexer.

[smolkaj]

Ok, the ppx extension works! This was surprisingly difficult, because things are very poorly documented. For future reference, this is where the OCaml AST definitions can be found: https://caml.inria.fr/pub/docs/manual-ocaml/libref/Parsetree.html#TYPEexpression

I only implemented let%nk p = {| ... |} in ... yet, but declarations and expression will be easy to add as well now that i have figured things out.

[smolkaj]

(We still need to finish the parser and implement the lexer.)

[smolkaj]

This problem has been solved with #527.

@basus: We also have a new parser and a new lexer. Extending them for experimentation should be really easy. The relevant files to look at are https://github.com/frenetic-lang/frenetic/blob/master/lib/Parser.cppo.mly and https://github.com/frenetic-lang/frenetic/blob/master/lib/Frenetic_NetKAT_Lexer.ml.