global meta fields

_oasis

@@ -40,7 +40,9 @@ Library frenetic
     tcpip,
     ulex,
     yojson,
-    threads
+    threads,
+# http://gallium.inria.fr/~fpottier/fix/
+    fix
   Modules:
     Frenetic_Hashcons,
     Frenetic_Bits,

_tags

@@ -1,5 +1,5 @@
 # OASIS_START
-# DO NOT EDIT (digest: 2f510444f9f8afdf56c9ef3cae00c123)
+# DO NOT EDIT (digest: c6512c1020d86e25d9fca42583cfc498)
 # Ignore VCS directories, you can use the same kind of rule outside
 # OASIS_START/STOP if you want to exclude directories that contains
 # useless stuff for the build process
@@ -22,6 +22,7 @@ true: annot, bin_annot
 <lib/*.ml{,i,y}>: package(camlp4.lib)
 <lib/*.ml{,i,y}>: package(core)
 <lib/*.ml{,i,y}>: package(cstruct)
+<lib/*.ml{,i,y}>: package(fix)
 <lib/*.ml{,i,y}>: package(ocamlgraph)
 <lib/*.ml{,i,y}>: package(ppx_deriving.enum)
 <lib/*.ml{,i,y}>: package(ppx_deriving.eq)
@@ -43,6 +44,7 @@ true: annot, bin_annot
 <async/*.ml{,i,y}>: package(core)
 <async/*.ml{,i,y}>: package(cstruct)
 <async/*.ml{,i,y}>: package(cstruct.async)
+<async/*.ml{,i,y}>: package(fix)
 <async/*.ml{,i,y}>: package(mparser)
 <async/*.ml{,i,y}>: package(mparser.re)
 <async/*.ml{,i,y}>: package(ocamlgraph)
@@ -68,6 +70,7 @@ true: annot, bin_annot
 "frenetic/frenetic.native": package(core)
 "frenetic/frenetic.native": package(cstruct)
 "frenetic/frenetic.native": package(cstruct.async)
+"frenetic/frenetic.native": package(fix)
 "frenetic/frenetic.native": package(mparser)
 "frenetic/frenetic.native": package(mparser.re)
 "frenetic/frenetic.native": package(ocamlgraph)
@@ -94,6 +97,7 @@ true: annot, bin_annot
 "frenetic/openflow.native": package(core)
 "frenetic/openflow.native": package(cstruct)
 "frenetic/openflow.native": package(cstruct.async)
+"frenetic/openflow.native": package(fix)
 "frenetic/openflow.native": package(mparser)
 "frenetic/openflow.native": package(mparser.re)
 "frenetic/openflow.native": package(ocamlgraph)
@@ -119,6 +123,7 @@ true: annot, bin_annot
 <frenetic/*.ml{,i,y}>: package(core)
 <frenetic/*.ml{,i,y}>: package(cstruct)
 <frenetic/*.ml{,i,y}>: package(cstruct.async)
+<frenetic/*.ml{,i,y}>: package(fix)
 <frenetic/*.ml{,i,y}>: package(mparser)
 <frenetic/*.ml{,i,y}>: package(mparser.re)
 <frenetic/*.ml{,i,y}>: package(ocamlgraph)
@@ -142,6 +147,7 @@ true: annot, bin_annot
 <syntax/*.ml{,i,y}>: package(camlp4.quotations.o)
 <syntax/*.ml{,i,y}>: package(core)
 <syntax/*.ml{,i,y}>: package(cstruct)
+<syntax/*.ml{,i,y}>: package(fix)
 <syntax/*.ml{,i,y}>: package(ipaddr)
 <syntax/*.ml{,i,y}>: package(ocamlgraph)
 <syntax/*.ml{,i,y}>: package(ppx_deriving.enum)
@@ -161,6 +167,7 @@ true: annot, bin_annot
 <lib_test/lib/*.ml{,i,y}>: package(camlp4.lib)
 <lib_test/lib/*.ml{,i,y}>: package(core)
 <lib_test/lib/*.ml{,i,y}>: package(cstruct)
+<lib_test/lib/*.ml{,i,y}>: package(fix)
 <lib_test/lib/*.ml{,i,y}>: package(ocamlgraph)
 <lib_test/lib/*.ml{,i,y}>: package(ppx_deriving.enum)
 <lib_test/lib/*.ml{,i,y}>: package(ppx_deriving.eq)
@@ -183,6 +190,7 @@ true: annot, bin_annot
 "lib_test/Test.byte": package(core)
 "lib_test/Test.byte": package(cstruct)
 "lib_test/Test.byte": package(cstruct.async)
+"lib_test/Test.byte": package(fix)
 "lib_test/Test.byte": package(mparser)
 "lib_test/Test.byte": package(mparser.re)
 "lib_test/Test.byte": package(ocamlgraph)
@@ -210,6 +218,7 @@ true: annot, bin_annot
 <lib_test/*.ml{,i,y}>: package(core)
 <lib_test/*.ml{,i,y}>: package(cstruct)
 <lib_test/*.ml{,i,y}>: package(cstruct.async)
+<lib_test/*.ml{,i,y}>: package(fix)
 <lib_test/*.ml{,i,y}>: package(mparser)
 <lib_test/*.ml{,i,y}>: package(mparser.re)
 <lib_test/*.ml{,i,y}>: package(ocamlgraph)
@@ -234,6 +243,7 @@ true: annot, bin_annot
 <bench/src/Main.{native,byte}>: package(camlp4.lib)
 <bench/src/Main.{native,byte}>: package(core)
 <bench/src/Main.{native,byte}>: package(cstruct)
+<bench/src/Main.{native,byte}>: package(fix)
 <bench/src/Main.{native,byte}>: package(ocamlgraph)
 <bench/src/Main.{native,byte}>: package(ppx_deriving.enum)
 <bench/src/Main.{native,byte}>: package(ppx_deriving.eq)
@@ -250,6 +260,7 @@ true: annot, bin_annot
 <bench/src/*.ml{,i,y}>: package(camlp4.lib)
 <bench/src/*.ml{,i,y}>: package(core)
 <bench/src/*.ml{,i,y}>: package(cstruct)
+<bench/src/*.ml{,i,y}>: package(fix)
 <bench/src/*.ml{,i,y}>: package(ocamlgraph)
 <bench/src/*.ml{,i,y}>: package(ppx_deriving.enum)
 <bench/src/*.ml{,i,y}>: package(ppx_deriving.eq)

examples/meta-fields/global/meta-global1.kat

@@ -0,0 +1,2 @@
+let meta := 1 in
+if meta = 1 then 1@1=>2@2 else 1@1=>3@3

lib/Frenetic_Fdd.ml

@@ -7,29 +7,33 @@ module Field = struct
 
   (** The order of the constructors defines the default variable ordering and has a massive
       performance impact. Do not change unless you know what you are doing. *)
-  type t
-    = Switch
-    | Location
-    | VSwitch
-    | VPort
-    | Vlan
-    | VlanPcp
-    (* SJS: for simplicity, support only up to 5 meta fields for now *)
-    | Meta0
-    | Meta1
-    | Meta2
-    | Meta3
-    | Meta4
-    | EthType
-    | IPProto
-    | EthSrc
-    | EthDst
-    | IP4Src
-    | IP4Dst
-    | TCPSrcPort
-    | TCPDstPort
-    | VFabric
-    [@@deriving sexp, enumerate, enum]
+  module T = struct
+    type t
+      = Switch
+      | Location
+      | VSwitch
+      | VPort
+      | Vlan
+      | VlanPcp
+      (* SJS: for simplicity, support only up to 5 meta fields for now *)
+      | Meta0
+      | Meta1
+      | Meta2
+      | Meta3
+      | Meta4
+      | EthType
+      | IPProto
+      | EthSrc
+      | EthDst
+      | IP4Src
+      | IP4Dst
+      | TCPSrcPort
+      | TCPDstPort
+      | VFabric
+      [@@deriving sexp, enumerate, enum, compare]
+  end
+  include Comparable.Make(T)
+  include T
   type field = t
 
   let num_fields = max + 1
@@ -43,7 +47,7 @@ module Field = struct
     sexp_of_t t |> Sexp.to_string
 
   let is_valid_order (lst : t list) : bool =
-    Set.Poly.(equal (of_list lst) (of_list all))
+    Set.(equal (of_list lst) (of_list all))
 
   let order = Array.init num_fields ~f:ident
 
@@ -76,8 +80,8 @@ module Field = struct
 
   module Env : ENV = struct
 
-    type t = { 
-      alist : (string * (field * (Frenetic_NetKAT.meta_init * bool))) list; 
+    type t = {
+      alist : (string * (field * (Frenetic_NetKAT.meta_init * bool))) list;
       depth : int
     }
 
@@ -159,12 +163,12 @@ module Field = struct
       | Mod _ -> k (1, lst)
       | Filter a -> k (1, (env, a) :: lst)
       | Seq (p, q) ->
-        f_seq' p lst env (fun (m, lst) -> 
+        f_seq' p lst env (fun (m, lst) ->
           f_seq' q lst env (fun (n, lst) ->
             k (m * n, lst)))
       | Union _ -> k (f_union pol env, lst)
-      | Let (id, init, mut, p) -> 
-        let env = Env.add env id init mut in 
+      | Let (id, init, mut, p) ->
+        let env = Env.add env id init mut in
         f_seq' p lst env k
       | Star p -> k (f_union p env, lst)
       | Link (sw,pt,_,_) -> k (1, (env, Test (Switch sw)) :: (env, Test (Location (Physical pt))) :: lst)
@@ -177,12 +181,12 @@ module Field = struct
       | Mod _ -> (1, lst)
       | Filter a -> (1, (env, a) :: lst)
       | Union (p, q) ->
-        f_union' p lst env (fun (m, lst) -> 
+        f_union' p lst env (fun (m, lst) ->
           f_union' q lst env (fun (n, lst) ->
             k (m + n, lst)))
       | Seq _ -> k (f_seq pol env, lst)
-      | Let (id, init, mut, p) -> 
-        let env = Env.add env id init mut in 
+      | Let (id, init, mut, p) ->
+        let env = Env.add env id init mut in
         k (f_seq p env, lst)
       | Star p -> f_union' p lst env k
       | Link (sw,pt,_,_) -> k (1, (env, Test (Switch sw)) :: (env, Test (Location (Physical pt))) :: lst)

lib/Frenetic_Fdd.mli

@@ -57,6 +57,9 @@ module Field : sig
   type field = t
   include Frenetic_Vlr.HashCmp with type t := t
 
+  module Set : Set.S with type Elt.t = t
+  module Map : Map.S with type Key.t = t
+
   module Env : sig
     type t
     val empty : t

lib/Frenetic_NetKAT_Compiler.ml

@@ -535,6 +535,9 @@ module Pol = struct
             |> mk_filter
       in
       mk_big_seq [filter_loc s1 p1; Dup; post_link ]
+    | Let (metaid, Const v, _, p) ->
+      Seq (Mod (Meta (metaid, v)), of_pol ing p)
+    | Let _ -> failwith "not implemented"
     | VLink _ -> assert false (* SJS / JNF *)
 end
 
@@ -801,6 +804,106 @@ module NetKAT_Automaton = struct
       let fdd = FDD.seq guard (FDD.union e d) in
       FDD.union acc fdd)
 
+  (* META fields *)
+  module Property (* : Fix.PROPERTY *) = struct
+    type property = Field.Set.t (* set of meta fields that a state depends on *)
+    let bottom = Field.(all |> List.filter ~f:is_meta |> Set.of_list)
+    let equal = Field.Set.equal
+    let is_maximal = Field.Set.is_empty
+  end
+
+  module Map (* : Fix.IMPERATIVE_MAPS *) = struct
+    include Int.Table
+    let create () = create ()
+    let add key data tbl = set ~key ~data tbl
+    let find key tbl = find_exn tbl key
+    let iter f tbl = iteri tbl ~f:(fun ~key ~data -> f key data)
+  end
+
+  module Analysis = Fix.Make(Map)(Property)
+
+  let gen fdd =
+    FDD.fold
+      (fun _ -> Field.Set.empty)
+      (fun (f,_) x y -> 
+        let s = Set.union x y in
+        if Field.is_meta f then Set.add s f else s)
+      fdd
+
+  let eq (automaton : t) : Analysis.equations = fun (state : int) ->
+    let (e,d) = Tbl.find_exn automaton.states state in
+    let gen = Set.union (gen e) (gen d) in
+    let conts =
+      let open Action in
+      FDD.fold
+        (fun par -> Par.fold par ~init:Int.Map.empty ~f:(fun acc seq ->
+          let key = Value.to_int_exn (Seq.find_exn seq K) in
+          let data = List.filter_map (Seq.keys seq) ~f:(function 
+              | K -> None 
+              | F f -> if Field.is_meta f then Some f else None)
+            |> Field.Set.of_list
+          in
+          Int.Map.add ~key ~data acc))
+        (fun _ -> Int.Map.merge ~f:(fun ~key v -> Some (match v with
+          | `Left v | `Right v -> v
+          | `Both (v1,v2) -> Set.inter v1 v2)))
+        d
+      |> Int.Map.to_alist
+    in
+    fun deps ->
+      (* kill-gen analysis: gen ∪ (⋃ᵢ inᵢ - killᵢ) *)
+      List.map conts ~f:(fun (k,kill) -> Field.Set.diff (deps k) kill)
+      |> List.cons gen
+      |> Field.Set.union_list
+
+  module Cache = Hashable.Make(struct
+    type env = Value.t Field.Map.t [@@deriving sexp, compare]
+    type t = int * env [@@deriving sexp, compare]
+    let hash (state, env) = 
+      (state, Field.Map.to_alist env) |> Hashtbl.hash
+  end)
+
+  let erase_meta_fields (automaton : t) : t =
+    let meta_deps = Analysis.lfp (eq automaton) in
+    let cache = Cache.Table.create () in
+    let new_auto = create_t () in
+
+    let rec go (state : int) (meta_env : Value.t Field.Map.t) =
+      let deps = meta_deps state in
+      let meta_env = Field.Map.filter meta_env ~f:(fun ~key ~data -> Set.mem deps key) in
+      match Cache.Table.find cache (state, meta_env) with
+      | Some s -> s
+      | None ->
+        let s = mk_state_t new_auto in
+        Cache.Table.add_exn cache ~key:(state, meta_env) ~data:s;
+        add_to_t_with_id new_auto (go' (Tbl.find_exn automaton.states state) meta_env) s;
+        s
+    and go' (e,d) (meta_env : Value.t Field.Map.t) =
+      let e = FDD.restrict (Field.Map.to_alist meta_env) e in
+      let d =
+        Field.Map.to_alist meta_env
+        |> List.map ~f:(fun (f,v) -> (Action.F f, v))
+        |> Seq.of_alist_exn
+        |> Par.singleton
+        |> (fun a -> FDD.seq (FDD.const a) d)
+        |> FDD.map_r (fun par -> Par.fold par ~init:Par.empty ~f:(fun par seq ->
+          let env =
+            Seq.to_hvs seq
+            |> List.filter ~f:(fun (f,v) -> Field.is_meta f)
+            |> Field.Map.of_alist_exn
+          in
+          let seq = Seq.update seq Action.K ~f:(function
+            | None -> assert false
+            | Some k -> Value.of_int (go (Value.to_int_exn k) env))
+          in
+          Par.add par seq))
+      in
+      (e,d)
+    in
+    new_auto.source <- go automaton.source Field.Map.empty;
+    new_auto
+
+
   (* SJS: horrible hack *)
   let to_dot (automaton : t) =
     let states = Tbl.map automaton.states ~f:(fun (e,d) -> FDD.union e d) in
@@ -865,6 +968,7 @@ end
 let compile_global ?(options=default_compiler_options) (pol : Frenetic_NetKAT.policy) : FDD.t =
   prepare_compilation ~options pol;
   NetKAT_Automaton.of_policy pol
+  |> NetKAT_Automaton.erase_meta_fields
   |> NetKAT_Automaton.to_local ~pc:Field.Vlan
 
 

lib/META

@@ -1,9 +1,9 @@
 # OASIS_START
-# DO NOT EDIT (digest: 2aed45dcfbabaef0cfd87efd10e22d19)
+# DO NOT EDIT (digest: a56da596bf8054bafaefe81351a3001b)
 version = "4.0.0"
 description = "The Frenetic Compiler and Runtime System"
 requires =
-"base64 camlp4.lib camlp4.extend camlp4 core cstruct ocamlgraph ppx_jane ppx_deriving.eq ppx_deriving.enum str tcpip ulex yojson threads"
+"base64 camlp4.lib camlp4.extend camlp4 core cstruct ocamlgraph ppx_jane ppx_deriving.eq ppx_deriving.enum str tcpip ulex yojson threads fix"
 archive(byte) = "frenetic.cma"
 archive(byte, plugin) = "frenetic.cma"
 archive(native) = "frenetic.cmxa"