package frenetic
Install
dune-project
Dependency
Authors
Maintainers
Sources
md5=baf754df13a759c32f2c86a1b6f328da
sha512=80140900e7009ccab14b25e244fe7edab87d858676f8a4b3799b4fea16825013cf68363fe5faec71dd54ba825bb4ea2f812c2c666390948ab217ffa75d9cbd29
doc/frenetic.netkat/Frenetic_netkat/Local_compiler/index.html
Module Frenetic_netkat.Local_compilerSource
Compilation
The exception that's thrown when the local compiler is given a policy with a Link term in it. To compile policies with Link terms, invoke global compiler.
compile p returns the intermediate representation of the local policy p. You can generate a flowtable from t by passing it to the to_table function below.
restrict hv t returns the fragment of t that applies when the assignment hv is true. The result will no longer make any reference to the header named in hv. This is equivalent to traversing the original NetKAT syntax tree and replacing all occurrences of Test(hv) with True.
This function is called by to_table to restrict t to the portion that should run on a single switch.
val to_table :
?options:compiler_options ->
?group_tbl:Frenetic_kernel.GroupTable0x04.t ->
Frenetic_kernel.OpenFlow.switchId ->
t ->
Frenetic_kernel.OpenFlow.flow listto_table sw t returns a flowtable that implements t for switch sw.
val to_table' :
?options:compiler_options ->
?group_tbl:Frenetic_kernel.GroupTable0x04.t ->
Frenetic_kernel.OpenFlow.switchId ->
t ->
(Frenetic_kernel.OpenFlow.flow * string list) listComposition
seq p q returns the sequential composotion of the two intermediate representations p and q. The result is semantically equivalent to the seqential composition of the two policies from which p and q were derived.
union p q returns the parallel composition of the two intermediate representations p and q. The result is semantically equivalent to the parallel composition of the two policies from which p and q were derived.
star p returns the star of the intermediate representation p. The result is semantically equivalent to the star of the policy from which p was derived.
Utilities
queries t returns the list of queries that occur in t along with the predicates associated with the query. Frenetic_kernel.Packet and byte counts of flows that match the predicate should count towards its associated query.
equal a b returns whether or not the two intermediate representations are structurally equal.
If the two representations are structurally equal, then the policies they derived from are semantically equivalent. However, if the two representations are not equal, the policies they were derived from may still be semantically equivalent.
to_local_pol t returns a NetKAT policy that is semantically equivalent to t. If was generated from compiling a policy p, it is not guarateed that to_local_pol t will be identical to p.
to_string t returns a string representation of t. This will be a representation of the Vlr diagram from the tdk package.
Interpreter
eval pkt t returns a PacketSet.t that is the result of the packet pkt being run through the policy represented by t.
val eval_pipes :
Semantics.packet ->
t ->
(string * Semantics.packet) list
* (string * Semantics.packet) list
* Semantics.packet listeval_pipes pkt t returns the result of running the packet pkt through the policy represented by t, with packets grouped according to the type of location to which the policy assigns them. The result is a triple whose first component is a list of packets and corresponding pipe location, whose second is a list of packets and corresponding query location, and whose third is a list of packets that are at physical locations.
options_from_json_string s returns a compiler_options type suitable. Mostly for HTTP servers
type multitable_flow = {pattern : Frenetic_kernel.OpenFlow.Pattern.t;idle_timeout : Frenetic_kernel.OpenFlow.timeout;hard_timeout : Frenetic_kernel.OpenFlow.timeout;instruction : instruction;flowId : flowId;
}val to_multitable :
?options:compiler_options ->
Frenetic_kernel.OpenFlow.switchId ->
flow_layout ->
t ->
multitable_flow list * Frenetic_kernel.GroupTable0x04.t