BDDReachabilityAnalysisFactory: fix denied out (#5573)

And add comments to code, plus simplify with branch.
batfish · Feb 20, 2020 · f3348fb · f3348fb
1 parent fbddfe3
commit f3348fb
Show file tree

Hide file tree

Showing 3 changed files with 84 additions and 13 deletions.
diff --git a/...cts/batfish/src/main/java/org/batfish/bddreachability/BDDReachabilityAnalysisFactory.java b/...cts/batfish/src/main/java/org/batfish/bddreachability/BDDReachabilityAnalysisFactory.java
@@ -4,15 +4,16 @@
 import static com.google.common.base.Predicates.alwaysTrue;
 import static org.batfish.bddreachability.BidirectionalReachabilityReturnPassInstrumentation.instrumentReturnPassEdges;
 import static org.batfish.bddreachability.SessionInstrumentation.sessionInstrumentation;
+import static org.batfish.bddreachability.transition.Transitions.IDENTITY;
 import static org.batfish.bddreachability.transition.Transitions.ZERO;
 import static org.batfish.bddreachability.transition.Transitions.addLastHopConstraint;
 import static org.batfish.bddreachability.transition.Transitions.addNoLastHopConstraint;
 import static org.batfish.bddreachability.transition.Transitions.addOriginatingFromDeviceConstraint;
 import static org.batfish.bddreachability.transition.Transitions.addSourceInterfaceConstraint;
+import static org.batfish.bddreachability.transition.Transitions.branch;
 import static org.batfish.bddreachability.transition.Transitions.compose;
 import static org.batfish.bddreachability.transition.Transitions.constraint;
 import static org.batfish.bddreachability.transition.Transitions.eraseAndSet;
-import static org.batfish.bddreachability.transition.Transitions.or;
 import static org.batfish.bddreachability.transition.Transitions.removeLastHopConstraint;
 import static org.batfish.bddreachability.transition.Transitions.removeSourceConstraint;
 import static org.batfish.common.util.CollectionUtil.toImmutableMap;
@@ -136,7 +137,7 @@
  * that node). For forward edges this is established by constraining to a single source. For
  * backward edges it's established using {@link BDDSourceManager#isValidValue}. When we exit the
  * node (e.g. forward into another node or a disposition state, or backward into another node or an
- * origination state), we erase the contraint on source by existential quantification.
+ * origination state), we erase the constraint on source by existential quantification.
  */
 @ParametersAreNonnullByDefault
 public final class BDDReachabilityAnalysisFactory {
@@ -1051,7 +1052,8 @@ private Stream<Edge> generateRules_PreOutEdgePostNat_PreInInterface() {
             });
   }
 
-  private Stream<Edge> generateRules_PreOutInterfaceDisposition_NodeDropAclOut() {
+  @VisibleForTesting
+  Stream<Edge> generateRules_PreOutInterfaceDisposition_NodeDropAclOut() {
     if (_ignoreFilters) {
       return Stream.of();
     }
@@ -1066,29 +1068,39 @@ private Stream<Edge> generateRules_PreOutInterfaceDisposition_NodeDropAclOut() {
                         StateExpr postState = new NodeDropAclOut(node);
                         return nodeEntry.getValue().getActiveInterfaces(vrfEntry.getKey()).values()
                             .stream()
-                            .filter(iface -> iface.getOutgoingFilterName() != null)
+                            .filter(
+                                iface ->
+                                    iface.getPreTransformationOutgoingFilterName() != null
+                                        || iface.getOutgoingFilterName() != null)
                             .flatMap(
                                 iface -> {
                                   String ifaceName = iface.getName();
                                   BDD denyPreAclBDD =
                                       ignorableAclDenyBDD(
                                           node, iface.getPreTransformationOutgoingFilterName());
-                                  BDD permitPreAclBDD =
-                                      ignorableAclPermitBDD(
-                                          node, iface.getPreTransformationOutgoingFilterName());
                                   BDD denyPostAclBDD =
                                       ignorableAclDenyBDD(node, iface.getOutgoingFilterName());
                                   Transition transformation =
                                       _bddOutgoingTransformations.get(node).get(ifaceName);
 
+                                  // DENIED_OUT: either denied by the pre-Transformation ACL or
+                                  // transformed and denied by the post-Transformation ACL.
+                                  Transition deniedFlows =
+                                      branch(
+                                          // branch on whether denied by pre-trans ACL
+                                          denyPreAclBDD,
+                                          // deny all flows denied by pre-trans ACL
+                                          IDENTITY,
+                                          // for flows permitted by pre-trans ACL, transform and
+                                          // then apply the post-trans ACL. deny any that are denied
+                                          // by the post-trans ACL.
+                                          compose(transformation, constraint(denyPostAclBDD)));
+
+                                  // We must clear any node-specific constraints before exiting the
+                                  // node.
                                   Transition transition =
                                       compose(
-                                          or(
-                                              constraint(denyPreAclBDD),
-                                              compose(
-                                                  constraint(permitPreAclBDD),
-                                                  transformation,
-                                                  constraint(denyPostAclBDD))),
+                                          deniedFlows,
                                           removeSourceConstraint(_bddSourceManagers.get(node)),
                                           removeLastHopConstraint(_lastHopMgr, node));
 

diff --git a/...batfish/src/test/java/org/batfish/bddreachability/BDDReachabilityAnalysisFactoryTest.java b/...batfish/src/test/java/org/batfish/bddreachability/BDDReachabilityAnalysisFactoryTest.java
@@ -1,5 +1,7 @@
 package org.batfish.bddreachability;
 
+import static org.batfish.bddreachability.EdgeMatchers.edge;
+import static org.batfish.bddreachability.TransitionMatchers.mapsForward;
 import static org.batfish.bddreachability.transition.Transitions.addOriginatingFromDeviceConstraint;
 import static org.batfish.bddreachability.transition.Transitions.compose;
 import static org.batfish.bddreachability.transition.Transitions.constraint;
@@ -1951,4 +1953,52 @@ public void testGenerateRootEdges_OriginateInterface_PostInVrf() throws IOExcept
                         factory.getBDDSourceManagers().get(c.getHostname())),
                     constraint(rootBdd)))));
   }
+
+  @Test
+  public void testDroppedByPreTransformationOutgoingFilter() throws IOException {
+    NetworkFactory nf = new NetworkFactory();
+    Configuration c =
+        nf.configurationBuilder().setConfigurationFormat(ConfigurationFormat.CISCO_IOS).build();
+    Vrf vrf = nf.vrfBuilder().setOwner(c).build();
+    Interface.Builder ib = nf.interfaceBuilder().setOwner(c).setVrf(vrf).setActive(true);
+    Interface iface1 =
+        ib.setAddress(ConcreteInterfaceAddress.parse("1.1.1.1/24"))
+            .setPreTransformationOutgoingFilter(
+                nf.aclBuilder().setOwner(c).setLines(ExprAclLine.REJECT_ALL).build())
+            .setOutgoingFilter(null)
+            .build();
+
+    String hostname = c.getHostname();
+    SortedMap<String, Configuration> configs = ImmutableSortedMap.of(hostname, c);
+    Batfish batfish = BatfishTestUtils.getBatfish(configs, temp);
+    batfish.computeDataPlane(batfish.getSnapshot());
+    DataPlane dataPlane = batfish.loadDataPlane(batfish.getSnapshot());
+    BDDReachabilityAnalysisFactory factory =
+        new BDDReachabilityAnalysisFactory(
+            PKT,
+            configs,
+            dataPlane.getForwardingAnalysis(),
+            new IpsRoutedOutInterfacesFactory(dataPlane.getFibs()),
+            false,
+            false);
+    List<Edge> edges =
+        factory
+            .generateRules_PreOutInterfaceDisposition_NodeDropAclOut()
+            .collect(ImmutableList.toImmutableList());
+
+    String ifaceName = iface1.getName();
+    StateExpr deliveredToSubnet = new PreOutInterfaceDeliveredToSubnet(hostname, ifaceName);
+    StateExpr exitsNetwork = new PreOutInterfaceExitsNetwork(hostname, ifaceName);
+    StateExpr neighborUnreachable = new PreOutInterfaceNeighborUnreachable(hostname, ifaceName);
+    StateExpr insufficientInfo = new PreOutInterfaceInsufficientInfo(hostname, ifaceName);
+    StateExpr nodeDropAclOut = new NodeDropAclOut(hostname);
+
+    assertThat(
+        edges,
+        containsInAnyOrder(
+            edge(deliveredToSubnet, nodeDropAclOut, mapsForward(ONE, ONE)),
+            edge(exitsNetwork, nodeDropAclOut, mapsForward(ONE, ONE)),
+            edge(neighborUnreachable, nodeDropAclOut, mapsForward(ONE, ONE)),
+            edge(insufficientInfo, nodeDropAclOut, mapsForward(ONE, ONE))));
+  }
 }
diff --git a/projects/batfish/src/test/java/org/batfish/bddreachability/EdgeMatchers.java b/projects/batfish/src/test/java/org/batfish/bddreachability/EdgeMatchers.java
@@ -1,5 +1,6 @@
 package org.batfish.bddreachability;
 
+import static org.hamcrest.Matchers.allOf;
 import static org.hamcrest.Matchers.equalTo;
 
 import org.batfish.bddreachability.EdgeMatchersImpl.HasPostState;
@@ -25,4 +26,12 @@ public static Matcher<Edge> hasPreState(StateExpr expr) {
   public static Matcher<Edge> hasTransition(Matcher<Transition> matcher) {
     return new HasTransition(matcher);
   }
+
+  /**
+   * Matches {@link Edge#getPostState}, {@link Edge#getPreState}, and {@link Edge#getTransition}.
+   */
+  public static Matcher<Edge> edge(
+      StateExpr preState, StateExpr postState, Matcher<Transition> transitionMatcher) {
+    return allOf(hasPreState(preState), hasPostState(postState), hasTransition(transitionMatcher));
+  }
 }