Skip to content

Commit

Permalink
Batfish: delete NoD reachability and everything that only it depended…
Browse files Browse the repository at this point in the history 
… on (#3711)
  • Loading branch information
@dhalperi
dhalperi committed Apr 26, 2019
1 parent d0c09b9 commit 6dd3105
Show file tree
Hide file tree
Showing 159 changed files with 92 additions and 17,999 deletions.
3 changes: 0 additions & 3 deletions ...batfish-common-protocol/src/main/java/org/batfish/datamodel/answers/NodAnswerElement.java
View file

This file was deleted.

16 changes: 7 additions & 9 deletions projects/batfish/src/main/java/org/batfish/bddreachability/BDDReachabilityAnalysis.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,18 +28,16 @@
import org.batfish.z3.state.OriginateInterfaceLink;
import org.batfish.z3.state.OriginateVrf;
import org.batfish.z3.state.Query;
import org.batfish.z3.state.visitors.DefaultTransitionGenerator;

/**
* A new reachability analysis engine using BDDs. The analysis maintains a graph that describes how
* packets flow through the network and through logical phases of a router. The graph is similar to
* the one generated by {@link DefaultTransitionGenerator} for reachability analysis using NOD. In
* particular, the graph nodes are {@link StateExpr StateExprs} and the edges are mostly the same as
* the NOD program rules/transitions. {@link BDD BDDs} label the nodes and edges of the graph. A
* node label represent the set of packets that can reach that node, and an edge label represents
* the set of packets that can traverse the edge. There is a single designated {@link Query}
* StateExpr that we compute reachability sets (i.e. sets of packets that reach the query state).
* The query state never has any out-edges, and has in-edges from the dispositions of interest.
* packets flow through the network and through logical phases of a router. In particular, the graph
* nodes are {@link StateExpr StateExprs} and the edges are mostly the same as the NOD program
* rules/transitions. {@link BDD BDDs} label the nodes and edges of the graph. A node label
* represent the set of packets that can reach that node, and an edge label represents the set of
* packets that can traverse the edge. There is a single designated {@link Query} StateExpr that we
* compute reachability sets (i.e. sets of packets that reach the query state). The query state
* never has any out-edges, and has in-edges from the dispositions of interest.
*
* <p>The two main departures from the NOD program are: 1) ACLs are encoded as a single BDD that
* labels an edge (rather than a series of states/transitions in NOD programs). 2) Source NAT is
Expand Down
8 changes: 3 additions & 5 deletions ...cts/batfish/src/main/java/org/batfish/bddreachability/BDDReachabilityAnalysisFactory.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -111,11 +111,9 @@
import org.batfish.z3.state.Query;

/**
* Constructs a the reachability graph for {@link BDDReachabilityAnalysis}. The graph is very
* similar to the NOD programs generated by {@link
* org.batfish.z3.state.visitors.DefaultTransitionGenerator}. The public API is very simple: it
* provides two methods for constructing {@link BDDReachabilityAnalysis}, depending on whether or
* not you have a destination Ip constraint.
* Constructs a the reachability graph for {@link BDDReachabilityAnalysis}. The public API is very
* simple: it provides two methods for constructing {@link BDDReachabilityAnalysis}, depending on
* whether or not you have a destination Ip constraint.
*
* <p>The core of the implementation is the {@code generateEdges()} method and its many helpers,
* which generate the {@link StateExpr nodes} and {@link Edge edges} of the reachability graph. Each
Expand Down
142 changes: 10 additions & 132 deletions ...batfish/src/main/java/org/batfish/bddreachability/OriginationStateToTerminationState.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,29 +4,7 @@
import java.util.List;
import javax.annotation.Nullable;
import org.batfish.z3.expr.StateExpr;
import org.batfish.z3.expr.TransformationExpr;
import org.batfish.z3.expr.TransformationStepExpr;
import org.batfish.z3.state.Accept;
import org.batfish.z3.state.AclDeny;
import org.batfish.z3.state.AclLineIndependentMatch;
import org.batfish.z3.state.AclLineMatch;
import org.batfish.z3.state.AclLineNoMatch;
import org.batfish.z3.state.AclPermit;
import org.batfish.z3.state.Debug;
import org.batfish.z3.state.DeliveredToSubnet;
import org.batfish.z3.state.Drop;
import org.batfish.z3.state.DropAcl;
import org.batfish.z3.state.DropAclIn;
import org.batfish.z3.state.DropAclOut;
import org.batfish.z3.state.DropNoRoute;
import org.batfish.z3.state.DropNullRoute;
import org.batfish.z3.state.ExitsNetwork;
import org.batfish.z3.state.InsufficientInfo;
import org.batfish.z3.state.NeighborUnreachable;
import org.batfish.z3.state.NeighborUnreachableOrExitsNetwork;
import org.batfish.z3.state.NodeAccept;
import org.batfish.z3.state.NodeDrop;
import org.batfish.z3.state.NodeDropAcl;
import org.batfish.z3.state.NodeDropAclIn;
import org.batfish.z3.state.NodeDropAclOut;
import org.batfish.z3.state.NodeDropNoRoute;
Expand All @@ -35,15 +13,11 @@
import org.batfish.z3.state.NodeInterfaceExitsNetwork;
import org.batfish.z3.state.NodeInterfaceInsufficientInfo;
import org.batfish.z3.state.NodeInterfaceNeighborUnreachable;
import org.batfish.z3.state.NodeInterfaceNeighborUnreachableOrExitsNetwork;
import org.batfish.z3.state.NodeNeighborUnreachableOrExitsNetwork;
import org.batfish.z3.state.NumberedQuery;
import org.batfish.z3.state.OriginateInterfaceLink;
import org.batfish.z3.state.OriginateVrf;
import org.batfish.z3.state.PostInInterface;
import org.batfish.z3.state.PostInInterfacePostNat;
import org.batfish.z3.state.PostInVrf;
import org.batfish.z3.state.PostOutEdge;
import org.batfish.z3.state.PreInInterface;
import org.batfish.z3.state.PreOutEdge;
import org.batfish.z3.state.PreOutEdgePostNat;
Expand All @@ -52,7 +26,6 @@
import org.batfish.z3.state.PreOutInterfaceInsufficientInfo;
import org.batfish.z3.state.PreOutInterfaceNeighborUnreachable;
import org.batfish.z3.state.PreOutVrf;
import org.batfish.z3.state.Query;
import org.batfish.z3.state.visitors.GenericStateExprVisitor;

/**
Expand All @@ -70,101 +43,48 @@ private OriginationStateToTerminationState() {}
return expr.accept(INSTANCE);
}

@SuppressWarnings("unchecked")
@Override
public List<StateExpr> castToGenericStateExprVisitorReturnType(Object o) {
return (List<StateExpr>) o;
}

@Override
public List<StateExpr> visitAccept(Accept accept) {
return null;
}

@Override
public List<StateExpr> visitAclDeny(AclDeny aclDeny) {
return null;
}

@Override
public List<StateExpr> visitAclLineIndependentMatch(
AclLineIndependentMatch aclLineIndependentMatch) {
return null;
}

@Override
public List<StateExpr> visitAclLineMatch(AclLineMatch aclLineMatch) {
return null;
}

@Override
public List<StateExpr> visitAclLineNoMatch(AclLineNoMatch aclLineNoMatch) {
return null;
}

@Override
public List<StateExpr> visitAclPermit(AclPermit aclPermit) {
return null;
}

@Override
public List<StateExpr> visitDebug(Debug debug) {
public List<StateExpr> visitAccept() {
return null;
}

@Override
public List<StateExpr> visitDrop(Drop drop) {
public List<StateExpr> visitDropAclIn() {
return null;
}

@Override
public List<StateExpr> visitDropAcl(DropAcl dropAcl) {
public List<StateExpr> visitDropAclOut() {
return null;
}

@Override
public List<StateExpr> visitDropAclIn(DropAclIn dropAclIn) {
public List<StateExpr> visitDropNoRoute() {
return null;
}

@Override
public List<StateExpr> visitDropAclOut(DropAclOut dropAclOut) {
public List<StateExpr> visitDropNullRoute() {
return null;
}

@Override
public List<StateExpr> visitDropNoRoute(DropNoRoute dropNoRoute) {
public List<StateExpr> visitExitsNetwork() {
return null;
}

@Override
public List<StateExpr> visitDropNullRoute(DropNullRoute dropNullRoute) {
public List<StateExpr> visitDeliveredToSubnet() {
return null;
}

@Override
public List<StateExpr> visitExitsNetwork(ExitsNetwork exitsNetwork) {
public List<StateExpr> visitInsufficientInfo() {
return null;
}

@Override
public List<StateExpr> visitDeliveredToSubnet(DeliveredToSubnet deliveredToSubnet) {
return null;
}

@Override
public List<StateExpr> visitInsufficientInfo(InsufficientInfo insufficientInfo) {
return null;
}

@Override
public List<StateExpr> visitNeighborUnreachable(NeighborUnreachable neighborUnreachable) {
return null;
}

@Override
public List<StateExpr> visitNeighborUnreachableOrExitsNetwork(
NeighborUnreachableOrExitsNetwork neighborUnreachableOrExitsNetwork) {
public List<StateExpr> visitNeighborUnreachable() {
return null;
}

Expand All @@ -173,16 +93,6 @@ public List<StateExpr> visitNodeAccept(NodeAccept nodeAccept) {
return null;
}

@Override
public List<StateExpr> visitNodeDrop(NodeDrop nodeDrop) {
return null;
}

@Override
public List<StateExpr> visitNodeDropAcl(NodeDropAcl nodeDropAcl) {
return null;
}

@Override
public List<StateExpr> visitNodeDropAclIn(NodeDropAclIn nodeDropAclIn) {
return null;
Expand Down Expand Up @@ -227,23 +137,6 @@ public List<StateExpr> visitNodeInterfaceNeighborUnreachable(
return null;
}

@Override
public List<StateExpr> visitNodeInterfaceNeighborUnreachableOrExitsNetwork(
NodeInterfaceNeighborUnreachableOrExitsNetwork nodeNeighborUnreachable) {
return null;
}

@Override
public List<StateExpr> visitNodeNeighborUnreachableOrExitsNetwork(
NodeNeighborUnreachableOrExitsNetwork nodeNeighborUnreachableOrExitsNetwork) {
return null;
}

@Override
public List<StateExpr> visitNumberedQuery(NumberedQuery numberedQuery) {
return null;
}

@Override
public List<StateExpr> visitOriginateInterfaceLink(OriginateInterfaceLink state) {
String hostname = state.getHostname();
Expand Down Expand Up @@ -277,11 +170,6 @@ public List<StateExpr> visitPostInVrf(PostInVrf postInVrf) {
return null;
}

@Override
public List<StateExpr> visitPostOutEdge(PostOutEdge preOutInterface) {
return null;
}

@Override
public List<StateExpr> visitPreInInterface(PreInInterface preInInterface) {
return null;
Expand Down Expand Up @@ -327,17 +215,7 @@ public List<StateExpr> visitPreOutInterfaceNeighborUnreachable(
}

@Override
public List<StateExpr> visitTransformation(TransformationExpr transformationExpr) {
return null;
}

@Override
public List<StateExpr> visitTransformationStep(TransformationStepExpr transformationStepExpr) {
return null;
}

@Override
public List<StateExpr> visitQuery(Query query) {
public List<StateExpr> visitQuery() {
return null;
}
}

0 comments on commit 6dd3105

Please sign in to comment.