package frenetic

  1. Overview
  2. Docs
package frenetic
Legend:
Library
Module
Module type
Parameter
Class
Class type

In a BDD, each node is an implicit predicate, "variable = true". In a FDD, each node is a test of a field against a particular value, as in EthSrc = "FE:89:00:12:34:12". The edges are either true or false just like in a BDD. But we also use values in modifcations - as in "port := 2". Note only Const and Mask are really used by OpenFlow. Both Pipe and Query are translated to the pseudoport Controller.

Each packet field can take on a certain range of values that in general have a lattice structure. This sometimes enables multiple tests on fields to be compressed into a single test. This module implements the Lattice signature from Vlr.

All integer bit widths are represented by an Int64.t and will be cast to the appropriate bit width for use during final translation to flowtables.

A simple bitmask variant is also supported. Mask(n, m) indicates that the first m bits of the value n are fixed, while the rest should be treated as wildcards.

Because this is a big union of possible value types, it's possible for the programmer to construct (Field.t, Value.t) pairs that do not make any sense, e.g., (Field.EthSrc, Value.Pipe "learn"). This will be detected during flowtable generation, though the syntax of the NetKAT language will prevent programs from generating these ill-formed predicates.

type t =
  1. | Const of Core.Int64.t
  2. | Mask of Core.Int64.t * int
  3. | AbstractLocation of string
  4. | Pipe of string
  5. | Query of string
  6. | FastFail of Core.Int32.t list
include Ppx_sexp_conv_lib.Sexpable.S with type t := t
include Frenetic_netkat.Vlr.Lattice with type t := t
include Frenetic_netkat.Vlr.HashCmp with type t := t
val equal : t -> t -> Ppx_deriving_runtime.bool
include Ppx_sexp_conv_lib.Sexpable.S with type t := t
val t_of_sexp : Sexplib0.Sexp.t -> t
val sexp_of_t : t -> Sexplib0.Sexp.t
val compare : t -> t -> int
val hash_fold_t : Base.Hash.state -> t -> Base.Hash.state
val hash : t -> Base.Hash.hash_value
val subset_eq : t -> t -> bool

subset_eq a b returns true if a and b in the partial ordering of the lattice. This relation should be reflexive, transitive, and antisymmetric.

val to_string : t -> string
val of_int : int -> t

of_int i converts an integer to a Const value

val of_int64 : int64 -> t

of_int64 i converts a 64-bit integer to a Const value

val to_int64_exn : t -> int64

to_int64_exn value returns just the integer for Const values, or an exception otherwise