Skip to content

Commit

Permalink
Merge pull request #10 from frenetic-lang/current-frenetic
Browse files Browse the repository at this point in the history
Compile against current Frenetic master
  • Loading branch information
jnfoster committed Nov 15, 2016
2 parents f682c7c + 243e138 commit 97a50f6
Show file tree
Hide file tree
Showing 27 changed files with 8,487 additions and 129 deletions.
3 changes: 1 addition & 2 deletions ocaml/DiamondTopo.ml
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
open Async_NetKAT

open Pathetic.Regex
module G = Net.Topology

let s1 = Switch 1L
Expand Down
24 changes: 11 additions & 13 deletions ocaml/FaultTolerance.ml
Original file line number Diff line number Diff line change
@@ -1,24 +1,22 @@
open NetKAT_Types
open Frenetic_NetKAT
open Pathetic.Regex
open Pathetic.RegexUtils
open Async_NetKAT
(* open NetCoreFT *)

module G = Net.Topology

let fake_choice (a,b) = NetKAT_Types.Union (a,b)
let fake_choice (a,b) = Union (a,b)

(* open NetCoreEval0x04 *)

(** Constructing k-resilient trees (k-trees) from regular expression paths **)

let trivial_pol = Filter False

let rec action_choice_to_choice lst = match lst with
| [a] -> a
| a :: lst -> fake_choice (a, action_choice_to_choice lst)
(* let rec action_choice_to_choice lst = match lst with *)
(* | [a] -> a *)
(* | a :: lst -> fake_choice (a, action_choice_to_choice lst) *)

let lpar (a,b) = Seq (Filter a, action_choice_to_choice b)
let lpar (a,b) = Seq (Filter a, Frenetic_NetKAT_Optimize.mk_big_union b)

(* Tree w/ ordered children. Leafs are hosts, internal nodes are switches *)
type k_tree =
Expand Down Expand Up @@ -195,8 +193,8 @@ let rec policy_from_k_tree' inport tree topo path_tag tag =
let next_hops = List.map (next_hop_from_k_tree sw' topo) children in
let children_pols = List.fold_left
(fun a (sw'', inport,tree) ->
NetKAT_Types.Union(a, policy_from_k_tree' inport (snd tree) topo path_tag (fst tree))) trivial_pol next_hops in
NetKAT_Types.Union(backup, children_pols)
Frenetic_NetKAT.Union(a, policy_from_k_tree' inport (snd tree) topo path_tag (fst tree))) trivial_pol next_hops in
Frenetic_NetKAT.Union(backup, children_pols)

let next_port_from_k_tree_root sw topo pathTag tree =
match tree with
Expand All @@ -219,8 +217,8 @@ let policy_from_k_tree pr tree topo path_tag tag =
let next_hops = List.map (next_hop_from_k_tree (Switch sw) topo) children in
let children_pols = List.fold_left
(fun a (sw'', inport,treeTag) ->
NetKAT_Types.Union(a, policy_from_k_tree' inport (snd treeTag) topo path_tag (fst treeTag))) trivial_pol next_hops in
NetKAT_Types.Union(backup, children_pols)
Frenetic_NetKAT.Union(a, policy_from_k_tree' inport (snd treeTag) topo path_tag (fst treeTag))) trivial_pol next_hops in
Frenetic_NetKAT.Union(backup, children_pols)


(* let rec pred_to_netkat_pred pr = match pr with *)
Expand All @@ -244,5 +242,5 @@ let rec compile_ft_to_kat regpol topo =
let genSym = GenSym.create() in
let pols = normalize regpol in
List.fold_left (fun acc pol -> let vid = (GenSym.next_val genSym) in
NetKAT_Types.Union(compile_ft_regex pol vid topo, acc))
Frenetic_NetKAT.Union(compile_ft_regex pol vid topo, acc))
trivial_pol pols
11 changes: 5 additions & 6 deletions ocaml/Graph.ml
Original file line number Diff line number Diff line change
@@ -1,15 +1,14 @@
open Frenetic_NetKAT
module H = Hashtbl
module Q = Queue
module M = OpenFlow0x04_Core
module P = OpenFlow0x04_Core

module type GRAPH =
sig
type node =
Host of int
| Switch of M.switchId
| Switch of switchId
type a = node
type b = P.portId
type b = portId
type graph
val create : unit -> graph
val add_node : graph -> a -> unit
Expand Down Expand Up @@ -43,9 +42,9 @@ module Graph : GRAPH =
struct
type node =
Host of int
| Switch of M.switchId
| Switch of switchId
type a = node
type b = P.portId
type b = portId
type h = int
(* sw -> port -> (sw*port) *)
type portTbl_t = ((a,(b, (a*b)) H.t) H.t)
Expand Down
4 changes: 2 additions & 2 deletions ocaml/Graph.mli
Original file line number Diff line number Diff line change
Expand Up @@ -2,10 +2,10 @@ module type GRAPH =
sig
type node =
Host of int
| Switch of OpenFlow0x04_Core.switchId
| Switch of Frenetic_NetKAT.switchId

type a = node
type b = OpenFlow0x04_Core.portId
type b = Frenetic_NetKAT.portId
type graph
val create : unit -> graph
val add_node : graph -> a -> unit
Expand Down
5 changes: 1 addition & 4 deletions ocaml/IDSTopo.ml
Original file line number Diff line number Diff line change
@@ -1,7 +1,4 @@
open Platform0x04
open NetCoreFT

module G = Graph.Graph
module G = NetCore_Graph.Graph

let s1 = G.Switch (Int64.of_int 1)
let s2 = G.Switch (Int64.of_int 2)
Expand Down
13 changes: 13 additions & 0 deletions ocaml/META
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
# OASIS_START
# DO NOT EDIT (digest: 647c7e2a7e19e2573b545647c74ae335)
version = "0.2"
description = "Fault Tolerating Regular Expressions"
requires =
"async base64 camlp4.lib camlp4.extend camlp4 core cstruct frenetic pathetic ppx_jane ppx_deriving.eq ppx_deriving.enum str tcpip threads oUnit"
archive(byte) = "fattire.cma"
archive(byte, plugin) = "fattire.cma"
archive(native) = "fattire.cmxa"
archive(native, plugin) = "fattire.cmxs"
exists_if = "fattire.cma"
# OASIS_STOP

54 changes: 23 additions & 31 deletions ocaml/Makefile
Original file line number Diff line number Diff line change
@@ -1,43 +1,35 @@
# LIBRARIES = OpenFlowLib
all: build

SUFFIXES = .a .cmxa .cma .d.cma
J=4

.PHONY: all doc clean $(LIBRARIES)
setup.ml: _oasis
oasis setup

OCAMLBUILD = ocamlbuild -use-ocamlfind $(addprefix -I ,$(LIBRARIES))
setup.data: setup.ml
./configure

OCAMLFIND = ocamlfind
build: setup.data setup.ml
ocaml setup.ml -build -j $(J)

%.d.byte:
$(OCAMLBUILD) -cflag -ppopt -cflag -lwt-debug $@
install: setup.data setup.ml
ocaml setup.ml -install

%.native %.byte:
$(OCAMLBUILD) $@
reinstall: setup.ml
ocaml setup.ml -reinstall

%.d.cma:
$(OCAMLBUILD) -no-links -cflag -ppopt -cflag -lwt-debug $@
uninstall: setup.ml
ocaml setup.ml -uninstall

%.a %.cmxa %.cma:
$(OCAMLBUILD) -no-links $@
test: setup.ml build
ocaml setup.ml -test $(TESTFLAGS)

# $(LIBRARIES):
# $(foreach SUFFIX, $(SUFFIXES), \
# $(OCAMLBUILD) $(addsuffix $(SUFFIX),$@/$@);)

all: $(LIBRARIES)
$(OCAMLBUILD) main.otarget

debug:
$(OCAMLBUILD) debug.otarget
clean:
ocamlbuild -clean
rm -f setup.data setup.log

native:
$(OCAMLBUILD) native.otarget
distclean:
ocaml setup.ml -distclean
rm -f setup.data setup.log

doc:
$(OCAMLBUILD) doc.docdir/index.html

test:
$(OCAMLBUILD) test.otarget

clean:
rm -rf _build
ocaml setup.ml -doc
8 changes: 4 additions & 4 deletions ocaml/NetCore_Graph.ml
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
module H = Hashtbl
module Q = Queue
module M = NetKAT_Types
module M = Frenetic_NetKAT

module type GRAPH =
sig
Expand All @@ -20,11 +20,11 @@ sig
val shortest_path : graph -> a -> a -> a list
val get_ports : graph -> a -> a -> (b*b)
val ports_of_switch : graph -> a -> b list
val edge_ports_of_switch : graph -> NetCore_Types.switchId -> b list
val get_switches : graph -> NetCore_Types.switchId list
val edge_ports_of_switch : graph -> M.switchId -> b list
val get_switches : graph -> M.switchId list
val get_hosts : graph -> a list
val get_nodes : graph -> a list
val get_switches_and_ports : graph -> (NetCore_Types.switchId * b list) list
val get_switches_and_ports : graph -> (M.switchId * b list) list
(* val get_ports : graph -> a -> b list *)
(* val get_other_port : graph -> a -> b -> (a*b) option *)
val next_hop : graph -> a -> b -> a
Expand Down
3 changes: 0 additions & 3 deletions ocaml/Pathetic.mlpack

This file was deleted.

12 changes: 12 additions & 0 deletions ocaml/Pathetic/META
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
# OASIS_START
# DO NOT EDIT (digest: dd6dc931d7b8279975c466b43b62d2a0)
version = "0.2"
description = "Fault Tolerating Regular Expressions"
requires = "core frenetic ppx_jane threads"
archive(byte) = "pathetic.cma"
archive(byte, plugin) = "pathetic.cma"
archive(native) = "pathetic.cmxa"
archive(native, plugin) = "pathetic.cmxs"
exists_if = "pathetic.cma"
# OASIS_STOP

63 changes: 53 additions & 10 deletions ocaml/Pathetic/Regex.ml
Original file line number Diff line number Diff line change
@@ -1,13 +1,54 @@
(* open OpenFlow0x01Types *)
open NetKAT_Types
module G = Async_NetKAT
open NetKAT_Pretty
open Core.Std
open Frenetic_NetKAT
open Frenetic_Packet
open Frenetic_Network
open Frenetic_NetKAT_Pretty

(* type graph = (switchId * switchId * int) list *)
type node =
| Switch of switchId
| Host of dlAddr * nwAddr [@@deriving sexp]

module Node = struct
type t = node [@@deriving sexp]

let compare = Pervasives.compare

let to_string t = match t with
| Switch(sw_id) -> Printf.sprintf "switch %Lu" sw_id
| Host(dlAddr, nwAddr) -> Printf.sprintf "host %s/%s"
(string_of_nwAddr nwAddr)
(string_of_dlAddr dlAddr)

let parse_dot _ _ = failwith "NYI: Node.parse_dot"
let parse_gml _ = failwith "NYI: Node.parse_dot"

let to_dot t = match t with
| Switch(sw_id) -> Printf.sprintf "%s [label=SW%Lu]" (to_string t) sw_id
| Host(dlAddr, nwAddr) -> Printf.sprintf "%s [label=%s]" (to_string t) (string_of_nwAddr nwAddr)

let to_mininet _ = failwith "NYI: Node.to_mininet"
end

module Link = struct
type t = unit [@@deriving sexp]

let compare = Pervasives.compare

let to_string () = "()"
let default = ()

let parse_dot _ = failwith "NYI: Link.parse_dot"
let parse_gml _ = failwith "NYI: Link.parse_dot"

let to_dot = to_string
let to_mininet _ = failwith "NYI: Link.to_mininet"
end

module Net = Frenetic_Network.Make(Node)(Link)

type regex =
| Const of G.Node.t
| Const of Node.t
| Star
| Sequence of regex * regex
| Union of regex * regex
Expand All @@ -29,7 +70,7 @@ let (||) a b = Union(a,b)
let (<.>) a b = Sequence(a,b)

let rec regex_to_string reg = match reg with
| Const(h) -> Printf.sprintf "%s" (G.Node.to_string h)
| Const(n) -> Node.to_string n
| Star -> "*"
| Empty -> "Empty"
| EmptySet -> "{}"
Expand Down Expand Up @@ -99,12 +140,14 @@ let rec nu re =
(* Printf.printf "returned %s\n" (regex_to_string foo); *)
foo

let rec is_empty re = match re with
let rec is_empty re : bool =
let open Pervasives in
match re with
| Empty -> false
| EmptySet -> true
| Const _ -> false
| Sequence(a,b) -> is_empty(a) or is_empty(b)
| Union(a,b) -> is_empty(a) & is_empty(b)
| Sequence(a,b) -> ( is_empty a ) || (is_empty b)
| Union(a,b) -> is_empty(a) && is_empty(b)
| Intersection(a,b) -> is_empty (Comp (Union (Comp a, Comp b)))
| Star -> false
| Comp a -> not (is_empty a)
Expand All @@ -124,7 +167,7 @@ let rec deriv sym re =
(* Printf.printf "returned %s\n" (regex_to_string return); *)
return

let rec deriv_path path re = List.fold_left (fun x y -> deriv y x) re (List.rev path)
let rec deriv_path path re = List.fold_left ~f:(fun x y -> deriv y x) ~init:re (List.rev path)

let rec match_path re path =
let return = match path with
Expand Down
23 changes: 21 additions & 2 deletions ocaml/Pathetic/Regex.mli
Original file line number Diff line number Diff line change
@@ -1,7 +1,26 @@
(* type graph = (switchId * switchId * int) list *)
open Frenetic_NetKAT
open Frenetic_Packet

(** [node] is an entity in the network, currently either a switch with a
datapath id, or a host with a MAC and IPv4 address. *)
type node =
| Switch of switchId
| Host of dlAddr * nwAddr

module Node : Frenetic_Network.VERTEX
with type t = node
module Link : Frenetic_Network.EDGE
with type t = unit

(** A representation of the network, with [node] as a label for vertices, and
[unit] as labels for edges. *)
module Net : Frenetic_Network.NETWORK
with module Topology.Vertex = Node
and module Topology.Edge = Link

type regex =
Const of Async_NetKAT.Node.t
| Const of Node.t
| Star
| Sequence of regex * regex
| Union of regex * regex
Expand All @@ -11,7 +30,7 @@ type regex =
| EmptySet

type regex_policy =
RegPol of NetKAT_Types.pred * regex * int
RegPol of pred * regex * int
| RegUnion of regex_policy * regex_policy
| RegInter of regex_policy * regex_policy

Expand Down
Loading

0 comments on commit 97a50f6

Please sign in to comment.