Global compiler: merge states using graph coloring & use reach of sta…

…te instead of vlans wherever possible (#586)

* split compiler module into local compiler and global compiler

.gitignore

@@ -23,9 +23,7 @@ setup.log
 *.mllib
 .merlin
 *.install
-
-# auto generated files
-lib/Frenetic_NetKAT_Tokens*
+*.pdf
 
 # ppx/test
 ppx/test/_tags

bench/src/benchmark.ml

@@ -1,8 +1,9 @@
 open Core
 open Frenetic.Netkat.Syntax
 open Benchmarking_Util
+module Netkat = Frenetic.Netkat
 
-let to_table = Frenetic.Netkat.Compiler.to_table
+let to_table = Netkat.Local_compiler.to_table
 
 let print_flowtables tbls =
   List.iter tbls ~f:(fun tbl ->
@@ -17,37 +18,37 @@ let dst_based_routing ~(in_file : string) ~(out_file : string) ~kind : unit =
     | `Local -> PolicyGen.shortest_paths topo
     | `Global -> PolicyGen.shortest_paths_global_policy topo in
   printf "Dumping policy to JSON...\n%!";
-  let str = Frenetic.Netkat.Json.policy_to_json_string pol in
+  let str = Netkat.Json.policy_to_json_string pol in
   Out_channel.with_file out_file ~f:(fun chan ->
     Out_channel.output_string chan str)
 
 let fattree_json ~(k : int) ~(out_file : string) : unit =
   Out_channel.with_file out_file ~f:(fun chan ->
     FatTree.fattree_routing ~k
-    |> Frenetic.Netkat.Json.policy_to_json_string
+    |> Netkat.Json.policy_to_json_string
     |> Out_channel.output_string chan)
 
 let pretty_json filename =
   let pol = In_channel.with_file filename
-    ~f:Frenetic.Netkat.Json.pol_of_json_channel
-    |> Frenetic.Netkat.Pretty.pretty_assoc
+    ~f:Netkat.Json.pol_of_json_channel
+    |> Netkat.Pretty.pretty_assoc
   in
-  print_endline (Frenetic.Netkat.Pretty.string_of_policy pol)
+  print_endline (Netkat.Pretty.string_of_policy pol)
 
 let classbench ~(in_file : string) ~(out_file : string) : unit =
   let pred = ClassBench.parse_classbench in_file in
-  let str = Frenetic.Netkat.Json.policy_to_json_string (Filter pred) in
+  let str = Netkat.Json.policy_to_json_string (Filter pred) in
   Out_channel.with_file out_file ~f:(fun chan ->
     Out_channel.output_string chan str)
 
-let switches pol = match Frenetic.Netkat.Semantics.switches_of_policy pol with
+let switches pol = match Netkat.Semantics.switches_of_policy pol with
     | [] -> [1L]
     | n -> n
 
 let per_switch_compilation to_table compiler pol : int =
   let switches = switches pol in
   let switches_and_pols = List.map switches
-    ~f:(fun sw -> Frenetic.Netkat.Optimize.specialize_policy sw pol) in
+    ~f:(fun sw -> Netkat.Optimize.specialize_policy sw pol) in
   let tbl_lens = List.map switches_and_pols
     ~f:(fun pol -> List.length (to_table 0L (compiler pol))) in
   int_sum tbl_lens
@@ -71,7 +72,7 @@ let compile compiler per_switch varorder tbl_opt debug filename =
     | "false" -> false
     | _ -> assert false in
   let order =
-    let open Frenetic.Netkat.Compiler.Field in
+    let open Netkat.Local_compiler.Field in
     match varorder with
     | "varorder-heuristic" -> `Heuristic
     | "varorder-fattree" ->
@@ -85,40 +86,40 @@ let compile compiler per_switch varorder tbl_opt debug filename =
     | _ -> assert false in
   let to_table sw fdd = match tbl_opt with
     | "tablegen-steffen" ->
-       Frenetic.Netkat.Compiler.(to_table ~options:{default_compiler_options with optimize=true; dedup_flows=true } sw fdd)
+       Netkat.Local_compiler.(to_table ~options:{default_compiler_options with optimize=true; dedup_flows=true } sw fdd)
     | "tablegen-naive" ->
-       Frenetic.Netkat.Compiler.(to_table ~options:{default_compiler_options with optimize=false; dedup_flows=true } sw fdd)
+       Netkat.Local_compiler.(to_table ~options:{default_compiler_options with optimize=false; dedup_flows=true } sw fdd)
     | _ -> assert false in
   let to_table sw fdd = match is_debug with
     | false -> to_table sw fdd
     | true -> print_table to_table sw fdd in
   let compiler_fun = match compiler with
     | "global" ->
        (fun pol ->
-	let fdd = Frenetic.Netkat.Compiler.compile_global pol in
+	let fdd = Netkat.Global_compiler.compile pol in
         (if not is_debug then
-           Frenetic.Netkat.Compiler.to_dotfile fdd "fdk.dot");
+           Netkat.Local_compiler.to_dotfile fdd "fdk.dot");
 	fdd)
     | "local" ->
        let opts =
-	 {Frenetic.Netkat.Compiler.default_compiler_options with
+	 {Netkat.Local_compiler.default_compiler_options with
 	   field_order=order;
 	   cache_prepare=`Empty} in
-       Frenetic.Netkat.Compiler.compile_local ~options:opts
+       Netkat.Local_compiler.compile ~options:opts
     | _ -> assert false in
   let f = match per_switch with
     | "big-fdd" -> big_fdd_compilation to_table compiler_fun
     | "per-switch" -> per_switch_compilation to_table compiler_fun
     | _ -> assert false in
   let pol = In_channel.with_file filename
-    ~f:Frenetic.Netkat.Json.pol_of_json_channel in
+    ~f:Netkat.Json.pol_of_json_channel in
   let (compile_time, tbl_size) = profile (fun () -> f pol) in
   printf "%s,%s,%s,%s,%s,%d,%f\n" filename compiler per_switch varorder tbl_opt tbl_size compile_time
 
 let policy_size filename =
   let pol = In_channel.with_file filename
-    ~f:Frenetic.Netkat.Json.pol_of_json_channel in
-  let size = Frenetic.Netkat.Semantics.size pol in
+    ~f:Netkat.Json.pol_of_json_channel in
+  let size = Netkat.Semantics.size pol in
   printf "%s,%d\n" filename size
 
 
@@ -128,21 +129,21 @@ let sdx filename =
     let open Yojson.Basic.Util in
     assert (json |> member "type" |> to_string = "disjoint");
     json |> member "pols" |> to_list
-      |> List.map ~f:Frenetic.Netkat.Json.pol_of_json in
-  let open Frenetic.Netkat.Pretty in
+      |> List.map ~f:Netkat.Json.pol_of_json in
+  let open Netkat.Pretty in
   (* let _ = List.iteri pols ~f:(fun i pol -> *)
     (* string_of_policy pol |> printf "Policy %d:\n%s\n\n%!" i) in *)
   let order =
-    let open Frenetic.Netkat.Compiler.Field in
+    let open Netkat.Local_compiler.Field in
     `Static [ Location; EthDst; TCPSrcPort; TCPDstPort; IP4Src; EthType; Switch; IP4Dst;
               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
+    let opts = { Netkat.Local_compiler.default_compiler_options with
 		 field_order = order;
 		 optimize = true } in
-    let tbl = Frenetic.Netkat.Compiler.to_table ~options:opts 0L
-		(Frenetic.Netkat.Compiler.compile_local ~options:opts pol) in
+    let tbl = Netkat.Local_compiler.to_table ~options:opts 0L
+		(Netkat.Local_compiler.compile ~options:opts pol) in
      (* eprintf "Table:\n%s\n%!" (Frenetic.OpenFlow.string_of_flowTable tbl); *)
     List.length tbl in
   let (compile_time, tbl_size) = profile (fun () ->
@@ -152,12 +153,12 @@ let sdx filename =
 let dot_to_virtual ~in_file =
   let topo = PolicyGen.parse_topo_file ~log:false in_file in
   let (vpol, vrel, vtopo, vingpol, vinout, ptopo, pinout) = PolicyGen.big_switch ~topo in
-  let open Frenetic.Netkat.Pretty in
+  let open Netkat.Pretty in
   let open Out_channel in
   let () = () in
-  List.iter [("vpol", vpol); ("vtopo", vtopo); ("vingpol", vingpol); ("ptopo", ptopo)]
+  List.iter [("vpol", vpol); ("vtopo", vtopo); ("ving_pol", vingpol); ("ptopo", ptopo)]
     ~f:(fun (file, pol) -> write_all (file ^ ".kat") ~data:(string_of_policy pol));
-  List.iter [("vrel", vrel); ("vinout", vinout); ("pinout", pinout)]
+  List.iter [("vrel", vrel); ("ving", vinout); ("veg", vinout); ("ping", pinout); ("peg", pinout)]
     ~f:(fun (file, pred) -> write_all (file ^ ".kat") ~data:(string_of_pred pred))
 
 

examples/global/coloring.kat

@@ -0,0 +1,8 @@
+(* Ideally, this policy should not require the use of any tags.
+   Switch 2 should match on the ip4Dst to forward packets appropriately.
+*)
+
+filter switch=1;(
+  filter ip4Dst=10.0.0.2; port:=2; 1@2=>2@1; port:=2 +
+  filter ip4Dst=10.0.0.3; port:=2; 1@2=>2@1; port:=3
+)

frenetic/Dump.ml

@@ -1,35 +1,36 @@
 open Core
+module Netkat = Frenetic.Netkat
 
 (*===========================================================================*)
 (* UTILITY FUNCTIONS                                                         *)
 (*===========================================================================*)
 
 let parse_pol ?(json=false) file =
   match json with
-  | false -> Frenetic.Netkat.Parser.pol_of_file file
+  | false -> Netkat.Parser.pol_of_file file
   | true ->
     In_channel.create file
-    |> Frenetic.Netkat.Json.pol_of_json_channel
+    |> Netkat.Json.pol_of_json_channel
 
-let parse_pred file = Frenetic.Netkat.Parser.pred_of_file file
+let parse_pred file = Netkat.Parser.pred_of_file file
 
 let fmt = Format.formatter_of_out_channel stdout
 let _ = Format.pp_set_margin fmt 120
 
 let print_fdd fdd =
-  printf "%s\n" (Frenetic.Netkat.Compiler.to_string fdd)
+  printf "%s\n" (Netkat.Local_compiler.to_string fdd)
 
 let dump data ~file =
   Out_channel.write_all file ~data
 
 let dump_fdd fdd ~file =
-  dump ~file (Frenetic.Netkat.Compiler.to_dot fdd)
+  dump ~file (Netkat.Local_compiler.to_dot fdd)
 
 let dump_auto auto ~file =
-  dump ~file (Frenetic.Netkat.Compiler.Automaton.to_dot auto)
+  dump ~file (Netkat.Global_compiler.Automaton.to_dot auto)
 
 let print_table fdd sw =
-  Frenetic.Netkat.Compiler.to_table sw fdd
+  Netkat.Local_compiler.to_table sw fdd
   |> Frenetic.OpenFlow.string_of_flowTable ~label:(sprintf "Switch %Ld" sw)
   |> printf "%s\n"
 
@@ -46,7 +47,7 @@ let print_time ?(prefix="") time =
   printf "%scompilation time: %.4f\n" prefix time
 
 let print_order () =
-  Frenetic.Netkat.Compiler.Field.(get_order ()
+  Netkat.Local_compiler.Field.(get_order ()
     |> List.map ~f:to_string
     |> String.concat ~sep:" > "
     |> printf "FDD field ordering: %s\n")
@@ -165,9 +166,9 @@ module Local = struct
 
   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 (t, fdd) = time (fun () -> Netkat.Local_compiler.compile pol) in
     let switches = match nr_switches with
-      | None -> Frenetic.Netkat.Semantics.switches_of_policy pol
+      | None -> Netkat.Semantics.switches_of_policy pol
       | Some n -> List.range 0 n |> List.map ~f:Int64.of_int
     in
     if Option.is_none nr_switches && List.is_empty switches then
@@ -198,8 +199,8 @@ module Global = struct
 
   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
+    let (t, fdd) = time (fun () -> Netkat.Global_compiler.compile pol) in
+    let switches = 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");
@@ -243,17 +244,17 @@ module Virtual = struct
     let peg = parse_pred peg in
 
     (* compile *)
-    let module FG = Frenetic.Netkat.FabricGen.FabricGen in
-    let module Virtual = Frenetic.Netkat.Virtual_Compiler.Make(FG) in
+    let module FG = Netkat.FabricGen.FabricGen in
+    let module Virtual = Netkat.Virtual_Compiler.Make(FG) 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
+    let (t2, fdd) = time (fun () -> Netkat.Global_compiler.compile global_pol) in
 
     (* print & dump *)
-    let switches = Frenetic.Netkat.Semantics.switches_of_policy global_pol in
+    let switches = 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
+        Netkat.Pretty.format_policy global_pol
     end;
     if printorder then print_order ();
     if printfdd then print_fdd fdd;
@@ -277,7 +278,7 @@ module Auto = struct
   let run file json printorder dedup cheap_minimize () =
     let pol = parse_pol ~json file in
     let (t, auto) = time (fun () ->
-      Frenetic.Netkat.Compiler.Automaton.of_policy pol ~dedup ~cheap_minimize) in
+      Netkat.Global_compiler.Automaton.of_policy pol ~dedup ~cheap_minimize) in
     if printorder then print_order ();
     dump_auto auto ~file:(file ^ ".auto.dot");
     print_time t;

frenetic/main.ml

@@ -1,4 +1,5 @@
 open Core
+module Netkat = Frenetic.Netkat
 
 (*===========================================================================*)
 (* AUXILLIARY FUNCTIONS                                                      *)
@@ -24,8 +25,8 @@ let log_outputs : (string * Async.Log.Output.t Lazy.t) Command.Spec.Arg_type.t =
       | "stdout" -> ("stdout", lazy (Async_extended.Extended_log.Console.output (Lazy.force Async.Writer.stdout)))
       | filename -> (filename, lazy (Async.Log.Output.file `Text filename)) )
 
-let table_fields : Frenetic.Netkat.Compiler.flow_layout Command.Spec.Arg_type.t =
-  let open Frenetic.Netkat.Fdd.Field in
+let table_fields : Netkat.Local_compiler.flow_layout Command.Spec.Arg_type.t =
+  let open Netkat.Fdd.Field in
   Command.Spec.Arg_type.create
     (fun table_field_string ->
       let opts = [ ("switch", Switch); ("vlan", Vlan); ("pcp", VlanPcp);
@@ -87,7 +88,7 @@ module Flag = struct
       ~doc:"int Port to listen on for OpenFlow switches. Defaults to 6633."
 
   let table_fields =
-    flag "--table" (optional_with_default [Frenetic.Netkat.Fdd.Field.get_order ()] table_fields)
+    flag "--table" (optional_with_default [Netkat.Fdd.Field.get_order ()] table_fields)
       ~doc:"Partition of fields into Openflow 1.3 tables, e.g. ethsrc,ethdst;ipsrc,ipdst"
 
   let policy_file =
@@ -180,7 +181,7 @@ let portless_controller : Command.t =
                   ++ default_spec)
     (fun openflow_port topology_name topology_file policy_file ->
        run (
-         let pol = Frenetic.Netkat.Parser.Portless.pol_of_file policy_file in
+         let pol = Netkat.Parser.Portless.pol_of_file policy_file in
 
          (* If the topology_name is specified, use that. If not, use the topology_file. *)
          let topo = match topology_name with
@@ -189,7 +190,7 @@ let portless_controller : Command.t =
 
          let module Controller = Frenetic.Async.NetKAT_Controller.Make (Frenetic.Async.OpenFlow0x01_Plugin) in
          Controller.start openflow_port;
-         Frenetic.Netkat.Portless_Compiler.compile pol topo
+         Netkat.Portless_Compiler.compile pol topo
          |> Controller.update
          |> Async.Deferred.don't_wait_for;
          never_returns (Async.Scheduler.go ());

lib/async/Common.ml

@@ -57,4 +57,4 @@ let parse_update_json body =
 
 let parse_config_json body =
   Body.to_string body >>= fun str ->
-  return (Frenetic_netkat.Compiler.options_from_json_string str)
+  return (Frenetic_netkat.Local_compiler.options_from_json_string str)

lib/async/Compile_Server.ml

@@ -4,7 +4,7 @@ open Cohttp_async
 open Frenetic_netkat.Syntax
 module Server = Cohttp_async.Server
 open Common
-module Comp = Frenetic_netkat.Compiler
+module Comp = Frenetic_netkat.Local_compiler
 
 let policy = ref Frenetic_netkat.Syntax.drop
 
@@ -13,7 +13,7 @@ let current_compiler_options = ref { Comp.default_compiler_options with optimize
 let compile_respond pol =
   (* Compile pol to tables and time everything. *)
   let (time, tbls) = profile (fun () ->
-  let fdd = Comp.compile_local ~options:!current_compiler_options pol in
+  let fdd = Comp.compile ~options:!current_compiler_options pol in
   let sws =
     let sws = Frenetic_netkat.Semantics.switches_of_policy pol in
     if List.length sws = 0 then [0L] else sws in
@@ -51,7 +51,7 @@ let handle_request
            Cohttp_async.Server.respond `OK)
     | `GET, [switchId; "flow_table"] ->
        let sw = Int64.of_string switchId in
-       Comp.compile_local ~options:!current_compiler_options !policy |>
+       Comp.compile ~options:!current_compiler_options !policy |>
          Comp.to_table ~options:!current_compiler_options sw |>
          Frenetic_netkat.Json.flowTable_to_json |>
          Yojson.Basic.to_string ~std:true |>

lib/async/Http_Controller.ml

@@ -4,7 +4,7 @@ open Cohttp_async
 open Frenetic_netkat.Syntax
 open Common
 module Server = Cohttp_async.Server
-module Comp = Frenetic_netkat.Compiler
+module Comp = Frenetic_netkat.Local_compiler
 
 type client = {
   (* Write new policies to this node *)