Local meta fields (#517, #521)

Local compiler now supports meta fields (or "logical fields"). They can be mutable or immutable, and they can be initialized with the value of another field (such as the ingress port) or with a constant. See #517 for details.

bench/src/Main.ml

@@ -76,10 +76,12 @@ let compile compiler per_switch varorder tbl_opt debug filename =
     | "varorder-heuristic" -> `Heuristic
     | "varorder-fattree" ->
       `Static [ EthType; Switch; Location; EthSrc; EthDst; Vlan;
-                VlanPcp; IPProto;IP4Src; IP4Dst; TCPSrcPort; TCPDstPort; VSwitch; VPort; VFabric; ]
+                VlanPcp; IPProto;IP4Src; IP4Dst; TCPSrcPort; TCPDstPort; VSwitch; VPort; VFabric;
+                Meta0; Meta1; Meta2; Meta3; Meta4; ]
     | "varorder-zoo" ->
       `Static [ EthType; Switch; IP4Dst; Location; EthSrc; EthDst; Vlan;
-                VlanPcp; IPProto;IP4Src; TCPSrcPort; TCPDstPort; VSwitch; VPort; VFabric; ]
+                VlanPcp; IPProto;IP4Src; TCPSrcPort; TCPDstPort; VSwitch; VPort; VFabric;
+                Meta0; Meta1; Meta2; Meta3; Meta4; ]
     | _ -> assert false in
   let to_table sw fdd = match tbl_opt with
     | "tablegen-steffen" ->
@@ -133,7 +135,7 @@ let sdx filename =
   let order =
     let open Frenetic_NetKAT_Compiler.Field in
     `Static [ Location; EthDst; TCPSrcPort; TCPDstPort; IP4Src; EthType; Switch; IP4Dst;
-              EthSrc;  Vlan; VlanPcp; IPProto; VSwitch; VPort; VFabric ] in
+              EthSrc;  Vlan; VlanPcp; IPProto; VSwitch; VPort; VFabric; Meta0; Meta1; Meta2; Meta3; Meta4 ] in
   (* eprintf "Number of elements in disjoint union: %d\n%!" (List.length pols); *)
   let f pol =
     let opts = { Frenetic_NetKAT_Compiler.default_compiler_options with

examples/meta-fields/README.md

@@ -0,0 +1,8 @@
+# Meta Fields
+
+## Documentation
+see https://github.com/frenetic-lang/frenetic/pull/517
+
+## Runing the examples
+The examples in this directory can be run by executing `frenetic dump local <file>`.
+Some examples require adding the flag `--switch 1`.

examples/meta-fields/craig.kat

@@ -0,0 +1,3 @@
+var suspect:=0 in
+filter switch=1 and ip4Src=8.0.0.0/8; suspect:=1; port:=5 |
+filter switch=2 and suspect=1; drop

examples/meta-fields/default-port.kat

@@ -0,0 +1,12 @@
+(* create immutable meta field that carries original port value *)
+let ingress := port in
+
+(* by default, forward packets to controller *)
+port := pipe("controller");
+
+(* overwrite default behavior ... *)
+begin
+  if ingress=1 then port:=2 else
+  if ethDst=1 then port:=1 else
+  id
+end

examples/meta-fields/meta-error1.kat

@@ -0,0 +1,3 @@
+(* let declares immutable variables - hence this should not compile *)
+let meta:=0 in
+meta:=1

examples/meta-fields/meta-error2.kat

@@ -0,0 +1,3 @@
+(* let declares immutable variables - hence this should not compile *)
+let meta:=switch in
+meta:=1

examples/meta-fields/meta1.kat

@@ -0,0 +1,4 @@
+let x:=1 in
+filter x=0; port:=0 |
+filter x=1; port:=1 |
+filter x=2; port:=2

examples/meta-fields/multiple-error.kat

@@ -0,0 +1,8 @@
+(* this will fail since we currently only support up to 5 meta fields in scope at once *)
+let m1 := vlanId in
+let m2 := port in
+let m3 := 423 in
+let m4 := port in
+let m5 := 1 in
+let m6 := 2 in
+id

examples/meta-fields/multiple.kat

@@ -0,0 +1,7 @@
+let m1 := vlanId in
+let m2 := port in
+let m3 := 423 in
+let m4 := port in
+filter m1=1 and m2=1 and m3=423; port:=pipe("success!") |
+filter m1=2 and m2=2 and m3=1;   port:=pipe("fail :(") |
+filter m1=2 and m2=2 and m4=3;   port:=pipe("fail :(")

frenetic/Dump.ml

@@ -37,8 +37,14 @@ let time f =
   let t2 = Unix.gettimeofday () in
   (t2 -. t1, r)
 
-let print_time time =
-  printf "Compilation time: %.4f\n" time
+let print_time ?(prefix="") time =
+  printf "%scompilation time: %.4f\n" prefix time
+
+let print_order () =
+  Frenetic_NetKAT_Compiler.Field.(get_order ()
+    |> List.map ~f:to_string
+    |> String.concat ~sep:" > "
+    |> printf "FDD field ordering: %s\n")
 
 
 (*===========================================================================*)
@@ -85,6 +91,10 @@ module Flag = struct
     flag "--json" no_arg
       ~doc: " Parse input file as JSON."
 
+  let print_order =
+    flag "--print-order" no_arg
+      ~doc: " Print FDD field order used by the compiler."
+
   let vpol =
     flag "--vpol" (optional_with_default "vpol.dot" file)
       ~doc: "file Virtual policy. Must not contain links. \
@@ -137,9 +147,10 @@ module Local = struct
     +> Flag.dump_fdd
     +> Flag.no_tables
     +> Flag.json
+    +> Flag.print_order
   )
 
-  let run file nr_switches printfdd dumpfdd no_tables json () =
+  let run file nr_switches printfdd dumpfdd no_tables json printorder () =
     let pol = parse_pol ~json file in
     let (t, fdd) = time (fun () -> Frenetic_NetKAT_Compiler.compile_local pol) in
     let switches = match nr_switches with
@@ -150,6 +161,7 @@ module Local = struct
       printf "Number of switches not automatically recognized!\n\
               Use the --switch flag to specify it manually.\n"
     else
+      if printorder then print_order ();
       if printfdd then print_fdd fdd;
       if dumpfdd then dump_fdd fdd ~file:(file ^ ".dot");
       print_all_tables ~no_tables fdd switches;
@@ -168,12 +180,14 @@ module Global = struct
     +> Flag.dump_auto
     +> Flag.no_tables
     +> Flag.json
+    +> Flag.print_order
   )
 
-  let run file printfdd dumpfdd printauto dumpauto no_tables json () =
+  let run file printfdd dumpfdd printauto dumpauto no_tables json printorder () =
     let pol = parse_pol ~json file in
     let (t, fdd) = time (fun () -> Frenetic_NetKAT_Compiler.compile_global pol) in
     let switches = Frenetic_NetKAT_Semantics.switches_of_policy pol in
+    if printorder then print_order ();
     if printfdd then print_fdd fdd;
     if dumpfdd then dump_fdd fdd ~file:(file ^ ".dot");
     print_all_tables ~no_tables fdd switches;
@@ -198,9 +212,12 @@ module Virtual = struct
     +> Flag.print_fdd
     +> Flag.dump_fdd
     +> Flag.print_global_pol
+    +> Flag.no_tables
+    +> Flag.print_order
   )
 
-  let run vpol_file vrel vtopo ving_pol ving veg ptopo ping peg printfdd dumpfdd printglobal () =
+  let run vpol_file vrel vtopo ving_pol ving veg ptopo ping peg printfdd dumpfdd printglobal
+    no_tables printorder () =
     (* parse files *)
     let vpol = parse_pol vpol_file in
     let vrel = parse_pred vrel in
@@ -214,21 +231,22 @@ module Virtual = struct
 
     (* compile *)
     let module Virtual = Frenetic_NetKAT_Virtual_Compiler in
-    let global_pol =
-      Virtual.compile vpol ~log:true ~vrel ~vtopo ~ving_pol ~ving ~veg ~ptopo ~ping ~peg
-    in
-    let fdd = Frenetic_NetKAT_Compiler.compile_global global_pol in
+    let (t1, global_pol) = time (fun () ->
+      Virtual.compile vpol ~log:true ~vrel ~vtopo ~ving_pol ~ving ~veg ~ptopo ~ping ~peg) in
+    let (t2, fdd) = time (fun () -> Frenetic_NetKAT_Compiler.compile_global global_pol) in
 
     (* print & dump *)
     let switches = Frenetic_NetKAT_Semantics.switches_of_policy global_pol in
     if printglobal then begin
       Format.fprintf fmt "Global Policy:@\n@[%a@]@\n@\n"
         Frenetic_NetKAT_Pretty.format_policy global_pol
     end;
+    if printorder then print_order ();
     if printfdd then print_fdd fdd;
     if dumpfdd then dump_fdd fdd ~file:(vpol_file ^ ".dot");
-    print_all_tables fdd switches
-
+    print_all_tables ~no_tables fdd switches;
+    print_time ~prefix:"virtual " t1;
+    print_time ~prefix:"global " t2;
 end