Local meta fields

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