@Test public void testSourceNatExitsNetwork() throws IOException { NetworkFactory nf = new NetworkFactory(); Configuration config = nf.configurationBuilder().setConfigurationFormat(ConfigurationFormat.CISCO_IOS).build(); Vrf vrf = nf.vrfBuilder().setOwner(config).build(); Ip poolIp = Ip.parse("5.5.5.5"); HeaderSpace postNatOutAclHeaderSpace = HeaderSpace.builder().setDstPorts(ImmutableList.of(SubRange.singleton(80))).build(); HeaderSpace natMatchHeaderSpace = HeaderSpace.builder().setSrcPorts(ImmutableList.of(SubRange.singleton(100))).build(); HeaderSpace preNatOutAclHeaderSpace = HeaderSpace.builder().setSrcPorts(ImmutableList.of(new SubRange(50, 150))).build(); Interface iface = nf.interfaceBuilder() .setOwner(config) .setVrf(vrf) .setActive(true) .setAddress(ConcreteInterfaceAddress.parse("1.0.0.0/31")) .setPreTransformationOutgoingFilter( nf.aclBuilder() .setOwner(config) .setLines(ImmutableList.of(acceptingHeaderSpace(preNatOutAclHeaderSpace))) .build()) .setOutgoingFilter( nf.aclBuilder() .setOwner(config) .setLines(ImmutableList.of(acceptingHeaderSpace(postNatOutAclHeaderSpace))) .build()) .setOutgoingTransformation( when(match(natMatchHeaderSpace)).apply(assignSourceIp(poolIp, poolIp)).build()) .build(); String ifaceName = iface.getName(); Prefix staticRoutePrefix = Prefix.parse("3.3.3.3/32"); vrf.setStaticRoutes( ImmutableSortedSet.of( StaticRoute.builder() .setNextHopInterface(ifaceName) .setAdministrativeCost(1) .setNetwork(staticRoutePrefix) .build())); String hostname = config.getHostname(); SortedMap<String, Configuration> configs = ImmutableSortedMap.of(hostname, config); BDDReachabilityAnalysisFactory factory = makeBddReachabilityAnalysisFactory(configs); BDDReachabilityAnalysis analysis = factory.bddReachabilityAnalysis( IpSpaceAssignment.builder() .assign(new InterfaceLocation(hostname, ifaceName), UniverseIpSpace.INSTANCE) .build()); HeaderSpaceToBDD toBDD = new HeaderSpaceToBDD(PKT, ImmutableMap.of()); IpSpaceToBDD srcToBdd = toBDD.getSrcIpSpaceToBdd(); BDD preNatOutAclBdd = toBDD.toBDD(preNatOutAclHeaderSpace); BDD postNatOutAclBdd = toBDD.toBDD(postNatOutAclHeaderSpace); BDD natMatchBdd = toBDD.toBDD(natMatchHeaderSpace); BDD poolIpBdd = srcToBdd.toBDD(poolIp); BDD origSrcIpBdd = srcToBdd.toBDD(Ip.parse("6.6.6.6")); BDD deniedAfterNat = natMatchBdd.ite(poolIpBdd, origSrcIpBdd).and(postNatOutAclBdd.not()); BDD deniedBeforeNat = origSrcIpBdd.and(preNatOutAclBdd.not()); BDD dropAclOut = deniedBeforeNat.or(deniedAfterNat); BDD dispositionBdd = preNatOutAclBdd.and(natMatchBdd.ite(poolIpBdd, origSrcIpBdd).and(postNatOutAclBdd)); Map<StateExpr, Map<StateExpr, Transition>> forwardEdges = analysis.getForwardEdgeMap(); Transition transition = forwardEdges .get(new PreOutInterfaceDeliveredToSubnet(hostname, ifaceName)) .get(new NodeInterfaceDeliveredToSubnet(hostname, ifaceName)); assertThat(transition.transitForward(origSrcIpBdd), equalTo(dispositionBdd)); transition = forwardEdges .get(new PreOutInterfaceExitsNetwork(hostname, ifaceName)) .get(new NodeInterfaceExitsNetwork(hostname, ifaceName)); assertThat(transition.transitForward(origSrcIpBdd), equalTo(dispositionBdd)); transition = forwardEdges .get(new PreOutInterfaceInsufficientInfo(hostname, ifaceName)) .get(new NodeInterfaceInsufficientInfo(hostname, ifaceName)); assertThat(transition.transitForward(origSrcIpBdd), equalTo(dispositionBdd)); transition = forwardEdges .get(new PreOutInterfaceNeighborUnreachable(hostname, ifaceName)) .get(new NodeInterfaceNeighborUnreachable(hostname, ifaceName)); assertThat(transition.transitForward(origSrcIpBdd), equalTo(dispositionBdd)); transition = forwardEdges .get(new PreOutInterfaceDeliveredToSubnet(hostname, ifaceName)) .get(new NodeDropAclOut(hostname)); assertEquals(transition.transitForward(origSrcIpBdd), dropAclOut); transition = forwardEdges .get(new PreOutInterfaceExitsNetwork(hostname, ifaceName)) .get(new NodeDropAclOut(hostname)); assertEquals(transition.transitForward(origSrcIpBdd), dropAclOut); transition = forwardEdges .get(new PreOutInterfaceInsufficientInfo(hostname, ifaceName)) .get(new NodeDropAclOut(hostname)); assertEquals(transition.transitForward(origSrcIpBdd), dropAclOut); transition = forwardEdges .get(new PreOutInterfaceNeighborUnreachable(hostname, ifaceName)) .get(new NodeDropAclOut(hostname)); assertEquals(transition.transitForward(origSrcIpBdd), dropAclOut); }
public BDDReachabilityAnalysis bddReachabilityAnalysis(IpSpaceAssignment srcIpSpaceAssignment) { return bddReachabilityAnalysis(srcIpSpaceAssignment, false); }
BDDReachabilityAnalysisFactory { public BDDReachabilityAnalysis bddReachabilityAnalysis(IpSpaceAssignment srcIpSpaceAssignment) { return bddReachabilityAnalysis(srcIpSpaceAssignment, false); } }
BDDReachabilityAnalysisFactory { public BDDReachabilityAnalysis bddReachabilityAnalysis(IpSpaceAssignment srcIpSpaceAssignment) { return bddReachabilityAnalysis(srcIpSpaceAssignment, false); } BDDReachabilityAnalysisFactory(
      BDDPacket packet,
      Map<String, Configuration> configs,
      ForwardingAnalysis forwardingAnalysis,
      IpsRoutedOutInterfacesFactory ipsRoutedOutInterfacesFactory,
      boolean ignoreFilters,
      boolean initializeSessions); }
BDDReachabilityAnalysisFactory { public BDDReachabilityAnalysis bddReachabilityAnalysis(IpSpaceAssignment srcIpSpaceAssignment) { return bddReachabilityAnalysis(srcIpSpaceAssignment, false); } BDDReachabilityAnalysisFactory(
      BDDPacket packet,
      Map<String, Configuration> configs,
      ForwardingAnalysis forwardingAnalysis,
      IpsRoutedOutInterfacesFactory ipsRoutedOutInterfacesFactory,
      boolean ignoreFilters,
      boolean initializeSessions); BDDReachabilityAnalysis bddReachabilityAnalysis(IpSpaceAssignment srcIpSpaceAssignment); BDDReachabilityAnalysis bddReachabilityAnalysis(
      IpSpaceAssignment srcIpSpaceAssignment, boolean useInterfaceRoots); BDDLoopDetectionAnalysis bddLoopDetectionAnalysis(IpSpaceAssignment srcIpSpaceAssignment); Map<IngressLocation, BDD> getAllBDDs(
      IpSpaceAssignment srcIpSpaceAssignment,
      AclLineMatchExpr initialHeaderSpace,
      Set<String> forbiddenTransitNodes,
      Set<String> requiredTransitNodes,
      Set<String> finalNodes,
      Set<FlowDisposition> actions); @VisibleForTesting BDDReachabilityAnalysis bddReachabilityAnalysis(
      IpSpaceAssignment srcIpSpaceAssignment,
      AclLineMatchExpr initialHeaderSpace,
      Set<String> forbiddenTransitNodes,
      Set<String> requiredTransitNodes,
      Set<String> finalNodes,
      Set<FlowDisposition> actions); @VisibleForTesting BDDReachabilityAnalysis bddReachabilityAnalysis(
      IpSpaceAssignment srcIpSpaceAssignment,
      AclLineMatchExpr initialHeaderSpace,
      Set<String> forbiddenTransitNodes,
      Set<String> requiredTransitNodes,
      Set<String> finalNodes,
      Set<FlowDisposition> actions,
      boolean useInterfaceRoots); Map<String, BDDOutgoingOriginalFlowFilterManager> getBddOutgoingOriginalFlowFilterManagers(); Map<String, BDDSourceManager> getBDDSourceManagers(); @Nullable LastHopOutgoingInterfaceManager getLastHopManager(); }
BDDReachabilityAnalysisFactory { public BDDReachabilityAnalysis bddReachabilityAnalysis(IpSpaceAssignment srcIpSpaceAssignment) { return bddReachabilityAnalysis(srcIpSpaceAssignment, false); } BDDReachabilityAnalysisFactory(
      BDDPacket packet,
      Map<String, Configuration> configs,
      ForwardingAnalysis forwardingAnalysis,
      IpsRoutedOutInterfacesFactory ipsRoutedOutInterfacesFactory,
      boolean ignoreFilters,
      boolean initializeSessions); BDDReachabilityAnalysis bddReachabilityAnalysis(IpSpaceAssignment srcIpSpaceAssignment); BDDReachabilityAnalysis bddReachabilityAnalysis(
      IpSpaceAssignment srcIpSpaceAssignment, boolean useInterfaceRoots); BDDLoopDetectionAnalysis bddLoopDetectionAnalysis(IpSpaceAssignment srcIpSpaceAssignment); Map<IngressLocation, BDD> getAllBDDs(
      IpSpaceAssignment srcIpSpaceAssignment,
      AclLineMatchExpr initialHeaderSpace,
      Set<String> forbiddenTransitNodes,
      Set<String> requiredTransitNodes,
      Set<String> finalNodes,
      Set<FlowDisposition> actions); @VisibleForTesting BDDReachabilityAnalysis bddReachabilityAnalysis(
      IpSpaceAssignment srcIpSpaceAssignment,
      AclLineMatchExpr initialHeaderSpace,
      Set<String> forbiddenTransitNodes,
      Set<String> requiredTransitNodes,
      Set<String> finalNodes,
      Set<FlowDisposition> actions); @VisibleForTesting BDDReachabilityAnalysis bddReachabilityAnalysis(
      IpSpaceAssignment srcIpSpaceAssignment,
      AclLineMatchExpr initialHeaderSpace,
      Set<String> forbiddenTransitNodes,
      Set<String> requiredTransitNodes,
      Set<String> finalNodes,
      Set<FlowDisposition> actions,
      boolean useInterfaceRoots); Map<String, BDDOutgoingOriginalFlowFilterManager> getBddOutgoingOriginalFlowFilterManagers(); Map<String, BDDSourceManager> getBDDSourceManagers(); @Nullable LastHopOutgoingInterfaceManager getLastHopManager();  }