Skip to content

Commit

Permalink
TransferBDD: Convert some community set regexes to community regexes (b…
Browse files Browse the repository at this point in the history
…atfish#8724)

This PR conservatively identifies community set regexes that can be treated as regexes on individual communities, and hence can be represented as such in the Batfish vendor-independent model. Doing so simplifies the analysis of such regexes and enables symbolic reasoning about route policies (e.g., SearchRoutePolicies and CompareRoutePolicies), which currently does not support reasoning about community set regexes due to their complex semantics.
  • Loading branch information
millstein authored May 26, 2023
1 parent 50c9a17 commit 0962bac
Show file tree
Hide file tree
Showing 27 changed files with 179 additions and 200 deletions.
1 change: 1 addition & 0 deletions projects/batfish-common-protocol/BUILD.bazel
Original file line number Diff line number Diff line change
Expand Up @@ -173,6 +173,7 @@ java_library(
"@maven//:com_ibm_icu_icu4j",
"@maven//:commons_cli_commons_cli",
"@maven//:commons_io_commons_io",
"@maven//:dk_brics_automaton",
"@maven//:jakarta_ws_rs_jakarta_ws_rs_api",
"@maven//:org_antlr_antlr4_runtime",
"@maven//:org_apache_commons_commons_configuration2",
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,13 @@
/** Utility functions for generating {@link RoutingPolicy routing policies}. */
public final class Common {

/**
* A Java regex translation for the underscore character that can appear in regexes in routing
* policies. This is a default translation that works for many vendors, but some vendors may treat
* underscore differently and so may need their own translation.
*/
public static final String DEFAULT_UNDERSCORE_REPLACEMENT = "(,|\\\\{|\\\\}|^|\\$| )";

/**
* Creates a generation policy for the aggregate network with the given {@link Prefix}. The
* generation policy matches any route with a destination more specific than {@code prefix}.
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,10 @@
package org.batfish.datamodel.routing_policy.communities;

import dk.brics.automaton.Automaton;
import dk.brics.automaton.RegExp;
import javax.annotation.Nonnull;
import org.apache.commons.text.StringEscapeUtils;
import org.batfish.datamodel.routing_policy.Common;

/** Utility class for constructing {@link CommunitySetExpr}s. */
public final class CommunitySetExprs {
Expand All @@ -12,4 +16,34 @@ public final class CommunitySetExprs {
private static final CommunitySetExpr EMPTY = new LiteralCommunitySet(CommunitySet.empty());

private CommunitySetExprs() {}

/**
* Creates an expression that matches on the given community-set regex. If the regex can be
* identified as one that only requires the existence of a single community, then the result makes
* that explicit by using {@link CommunityMatchRegex} instead of {@link CommunitySetMatchRegex}.
*
* @param regex the regex
* @return an expression that represents a community-set match on the regex
*/
public static @Nonnull CommunitySetMatchExpr toMatchExpr(String regex) {
String trimmedRegex = regex;
// a conservative check to determine if the regex only matches on the existence of a single
// community in the set: the regex optionally starts with _, optionally ends with _, and in
// between only accepts strings containing digits and colons
String underscore = StringEscapeUtils.unescapeJava(Common.DEFAULT_UNDERSCORE_REPLACEMENT);
if (trimmedRegex.startsWith(underscore)) {
trimmedRegex = trimmedRegex.substring(underscore.length());
}
if (trimmedRegex.endsWith(underscore)) {
trimmedRegex = trimmedRegex.substring(0, trimmedRegex.length() - underscore.length());
}
Automaton trimmedRegexAuto = new RegExp(trimmedRegex).toAutomaton();
Automaton digitsAndColons = new RegExp("[0-9:]+").toAutomaton();
if (trimmedRegexAuto.intersection(digitsAndColons).equals(trimmedRegexAuto)) {
return new HasCommunity(new CommunityMatchRegex(ColonSeparatedRendering.instance(), regex));
} else {
return new CommunitySetMatchRegex(
new TypesFirstAscendingSpaceSeparated(ColonSeparatedRendering.instance()), regex);
}
}
}
1 change: 1 addition & 0 deletions projects/batfish-common-protocol/src/test/BUILD.bazel
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,7 @@ junit_tests(
"@maven//:junit_junit",
"@maven//:org_antlr_antlr4_runtime",
"@maven//:org_apache_commons_commons_lang3",
"@maven//:org_apache_commons_commons_text",
"@maven//:org_hamcrest_hamcrest",
"@maven//:org_parboiled_parboiled_core",
],
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,55 @@
package org.batfish.datamodel.routing_policy.communities;

import static org.batfish.datamodel.routing_policy.communities.CommunitySetExprs.toMatchExpr;
import static org.junit.Assert.assertEquals;

import org.apache.commons.text.StringEscapeUtils;
import org.batfish.datamodel.routing_policy.Common;
import org.junit.Test;

public final class CommunitySetExprsTest {

@Test
public void testCommunitySetMatchRegexUnoptimized() {
assertEquals(
toMatchExpr("^65000:123 65011:12[3]$"),
new CommunitySetMatchRegex(
new TypesFirstAscendingSpaceSeparated(ColonSeparatedRendering.instance()),
"^65000:123 65011:12[3]$"));
assertEquals(
toMatchExpr("^$"),
new CommunitySetMatchRegex(
new TypesFirstAscendingSpaceSeparated(ColonSeparatedRendering.instance()), "^$"));
}

@Test
public void testVisitCommunitySetMatchRegexOptimized() {

String underscore = StringEscapeUtils.unescapeJava(Common.DEFAULT_UNDERSCORE_REPLACEMENT);

assertEquals(
toMatchExpr("53"),
new HasCommunity(new CommunityMatchRegex(ColonSeparatedRendering.instance(), "53")));
assertEquals(
toMatchExpr("53:"),
new HasCommunity(new CommunityMatchRegex(ColonSeparatedRendering.instance(), "53:")));
assertEquals(
toMatchExpr(underscore + "53:"),
new HasCommunity(
new CommunityMatchRegex(ColonSeparatedRendering.instance(), underscore + "53:")));
assertEquals(
toMatchExpr(":53"),
new HasCommunity(new CommunityMatchRegex(ColonSeparatedRendering.instance(), ":53")));
assertEquals(
toMatchExpr(":53" + underscore),
new HasCommunity(
new CommunityMatchRegex(ColonSeparatedRendering.instance(), ":53" + underscore)));
assertEquals(
toMatchExpr("[0-9]+:"),
new HasCommunity(new CommunityMatchRegex(ColonSeparatedRendering.instance(), "[0-9]+:")));
assertEquals(
toMatchExpr("[0-9]+:[123]*"),
new HasCommunity(
new CommunityMatchRegex(ColonSeparatedRendering.instance(), "[0-9]+:[123]*")));
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@
import static org.batfish.datamodel.Names.generatedOspfExportPolicyName;
import static org.batfish.datamodel.bgp.LocalOriginationTypeTieBreaker.NO_PREFERENCE;
import static org.batfish.datamodel.bgp.NextHopIpTieBreaker.HIGHEST_NEXT_HOP_IP;
import static org.batfish.datamodel.routing_policy.Common.DEFAULT_UNDERSCORE_REPLACEMENT;
import static org.batfish.datamodel.routing_policy.Common.initDenyAllBgpRedistributionPolicy;
import static org.batfish.datamodel.routing_policy.Common.suppressSummarizedPrefixes;
import static org.batfish.representation.arista.AristaConversions.getSourceInterfaceIp;
Expand Down Expand Up @@ -346,8 +347,7 @@ static String toJavaRegex(String ciscoRegex) {
} else {
withoutQuotes = ciscoRegex;
}
String underscoreReplacement = "(,|\\\\{|\\\\}|^|\\$| )";
String output = withoutQuotes.replaceAll("_", underscoreReplacement);
String output = withoutQuotes.replaceAll("_", DEFAULT_UNDERSCORE_REPLACEMENT);
return output;
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,9 @@
import static org.batfish.datamodel.Names.generatedBgpPeerExportPolicyName;
import static org.batfish.datamodel.Names.generatedBgpPeerImportPolicyName;
import static org.batfish.datamodel.bgp.AllowRemoteAsOutMode.ALWAYS;
import static org.batfish.datamodel.routing_policy.Common.DEFAULT_UNDERSCORE_REPLACEMENT;
import static org.batfish.datamodel.routing_policy.Common.generateSuppressionPolicy;
import static org.batfish.datamodel.routing_policy.communities.CommunitySetExprs.toMatchExpr;
import static org.batfish.datamodel.routing_policy.statement.Statements.RemovePrivateAs;
import static org.batfish.representation.arista.AristaConfiguration.DEFAULT_VRF_NAME;
import static org.batfish.representation.arista.AristaConfiguration.MAX_ADMINISTRATIVE_COST;
Expand All @@ -29,7 +31,6 @@
import java.util.Optional;
import java.util.Set;
import java.util.SortedMap;
import java.util.regex.Pattern;
import java.util.stream.Collectors;
import javax.annotation.Nonnull;
import javax.annotation.Nullable;
Expand Down Expand Up @@ -70,10 +71,8 @@
import org.batfish.datamodel.routing_policy.communities.CommunitySetAclLine;
import org.batfish.datamodel.routing_policy.communities.CommunitySetMatchAll;
import org.batfish.datamodel.routing_policy.communities.CommunitySetMatchExpr;
import org.batfish.datamodel.routing_policy.communities.CommunitySetMatchRegex;
import org.batfish.datamodel.routing_policy.communities.HasCommunity;
import org.batfish.datamodel.routing_policy.communities.LiteralCommunitySet;
import org.batfish.datamodel.routing_policy.communities.TypesFirstAscendingSpaceSeparated;
import org.batfish.datamodel.routing_policy.expr.BooleanExpr;
import org.batfish.datamodel.routing_policy.expr.CallExpr;
import org.batfish.datamodel.routing_policy.expr.Conjunction;
Expand Down Expand Up @@ -874,39 +873,7 @@ static CommunityMatchRegex toCommunityMatchRegex(String regex) {

@Nonnull
static CommunitySetAclLine toCommunitySetAclLine(ExpandedCommunityListLine line) {

String regex = line.getRegex();

// If the line's regex only requires some community in the set to have a particular format,
// create a regex on an individual community rather than on the whole set.
// Regexes on individual communities have a simpler semantics, and some questions
// (e.g. SearchRoutePolicies) do not handle arbitrary community-set regexes.
String containsAColon = "(_?\\d+)?:?(\\d+_?)?";
String noColon = "_?\\d+|\\d+_?";
String singleCommRegex = containsAColon + "|" + noColon;
Pattern p = Pattern.compile(singleCommRegex);
if (p.matcher(regex).matches()) {
return toCommunitySetAclLineOptimized(line);
} else {
return toCommunitySetAclLineUnoptimized(line);
}
}

// This method should only be used if the line's regex has a special form; see
// toCommunitySetAclLine(ExpandedCommunityListLine) above.
@Nonnull
static CommunitySetAclLine toCommunitySetAclLineOptimized(ExpandedCommunityListLine line) {
return new CommunitySetAclLine(
line.getAction(), new HasCommunity(toCommunityMatchRegex(line.getRegex())));
}

@Nonnull
static CommunitySetAclLine toCommunitySetAclLineUnoptimized(ExpandedCommunityListLine line) {
return new CommunitySetAclLine(
line.getAction(),
new CommunitySetMatchRegex(
new TypesFirstAscendingSpaceSeparated(ColonSeparatedRendering.instance()),
toJavaRegex(line.getRegex())));
return new CommunitySetAclLine(line.getAction(), toMatchExpr(toJavaRegex(line.getRegex())));
}

@Nonnull
Expand All @@ -917,8 +884,7 @@ static String toJavaRegex(String ciscoRegex) {
} else {
withoutQuotes = ciscoRegex;
}
String underscoreReplacement = "(,|\\\\{|\\\\}|^|\\$| )";
String output = withoutQuotes.replaceAll("_", underscoreReplacement);
String output = withoutQuotes.replaceAll("_", DEFAULT_UNDERSCORE_REPLACEMENT);
return output;
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,9 @@
import static org.batfish.datamodel.Names.generatedBgpPeerExportPolicyName;
import static org.batfish.datamodel.ospf.OspfNetworkType.BROADCAST;
import static org.batfish.datamodel.ospf.OspfNetworkType.POINT_TO_POINT;
import static org.batfish.datamodel.routing_policy.Common.DEFAULT_UNDERSCORE_REPLACEMENT;
import static org.batfish.datamodel.routing_policy.Common.generateSuppressionPolicy;
import static org.batfish.datamodel.routing_policy.communities.CommunitySetExprs.toMatchExpr;
import static org.batfish.datamodel.tracking.TrackMethods.alwaysFalse;
import static org.batfish.datamodel.tracking.TrackMethods.alwaysTrue;
import static org.batfish.datamodel.tracking.TrackMethods.interfaceActive;
Expand Down Expand Up @@ -45,7 +47,6 @@
import java.util.Set;
import java.util.SortedMap;
import java.util.function.Predicate;
import java.util.regex.Pattern;
import java.util.stream.Collectors;
import java.util.stream.Stream;
import javax.annotation.Nonnull;
Expand Down Expand Up @@ -106,14 +107,12 @@
import org.batfish.datamodel.routing_policy.communities.CommunitySet;
import org.batfish.datamodel.routing_policy.communities.CommunitySetAclLine;
import org.batfish.datamodel.routing_policy.communities.CommunitySetMatchAny;
import org.batfish.datamodel.routing_policy.communities.CommunitySetMatchRegex;
import org.batfish.datamodel.routing_policy.communities.CommunitySetUnion;
import org.batfish.datamodel.routing_policy.communities.HasCommunity;
import org.batfish.datamodel.routing_policy.communities.InputCommunities;
import org.batfish.datamodel.routing_policy.communities.LiteralCommunitySet;
import org.batfish.datamodel.routing_policy.communities.MatchCommunities;
import org.batfish.datamodel.routing_policy.communities.SetCommunities;
import org.batfish.datamodel.routing_policy.communities.TypesFirstAscendingSpaceSeparated;
import org.batfish.datamodel.routing_policy.expr.BooleanExpr;
import org.batfish.datamodel.routing_policy.expr.BooleanExprs;
import org.batfish.datamodel.routing_policy.expr.CallExpr;
Expand Down Expand Up @@ -566,39 +565,7 @@ static AsPathAccessList toAsPathAccessList(IpAsPathAccessList pathList) {
}

static @Nonnull CommunitySetAclLine toCommunitySetAclLine(ExpandedCommunityListLine line) {

String regex = line.getRegex();

// If the line's regex only requires some community in the set to have a particular format,
// create a regex on an individual community rather than on the whole set.
// Regexes on individual communities have a simpler semantics, and some questions
// (e.g. SearchRoutePolicies) do not handle arbitrary community-set regexes.
String containsAColon = "(_?\\d+)?:?(\\d+_?)?";
String noColon = "_?\\d+|\\d+_?";
String singleCommRegex = containsAColon + "|" + noColon;
Pattern p = Pattern.compile(singleCommRegex);
if (p.matcher(regex).matches()) {
return toCommunitySetAclLineOptimized(line);
} else {
return toCommunitySetAclLineUnoptimized(line);
}
}

// This method should only be used if the line's regex has a special form; see
// toCommunitySetAclLine(ExpandedCommunityListLine) above.
static @Nonnull CommunitySetAclLine toCommunitySetAclLineOptimized(
ExpandedCommunityListLine line) {
return new CommunitySetAclLine(
line.getAction(), new HasCommunity(toCommunityMatchRegex(line.getRegex())));
}

static @Nonnull CommunitySetAclLine toCommunitySetAclLineUnoptimized(
ExpandedCommunityListLine line) {
return new CommunitySetAclLine(
line.getAction(),
new CommunitySetMatchRegex(
new TypesFirstAscendingSpaceSeparated(ColonSeparatedRendering.instance()),
toJavaRegex(line.getRegex())));
return new CommunitySetAclLine(line.getAction(), toMatchExpr(toJavaRegex(line.getRegex())));
}

static String toJavaRegex(String ciscoRegex) {
Expand All @@ -608,8 +575,7 @@ static String toJavaRegex(String ciscoRegex) {
} else {
withoutQuotes = ciscoRegex;
}
String underscoreReplacement = "(,|\\\\{|\\\\}|^|\\$| )";
String output = withoutQuotes.replaceAll("_", underscoreReplacement);
String output = withoutQuotes.replaceAll("_", DEFAULT_UNDERSCORE_REPLACEMENT);
return output;
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@
import static org.batfish.datamodel.bgp.AllowRemoteAsOutMode.ALWAYS;
import static org.batfish.datamodel.bgp.LocalOriginationTypeTieBreaker.NO_PREFERENCE;
import static org.batfish.datamodel.bgp.NextHopIpTieBreaker.HIGHEST_NEXT_HOP_IP;
import static org.batfish.datamodel.routing_policy.Common.DEFAULT_UNDERSCORE_REPLACEMENT;
import static org.batfish.datamodel.routing_policy.Common.suppressSummarizedPrefixes;
import static org.batfish.datamodel.tracking.TrackMethods.negatedReference;
import static org.batfish.representation.cisco_asa.AsaConversions.computeDistributeListPolicies;
Expand Down Expand Up @@ -414,8 +415,7 @@ static String toJavaRegex(String ciscoRegex) {
} else {
withoutQuotes = ciscoRegex;
}
String underscoreReplacement = "(,|\\\\{|\\\\}|^|\\$| )";
String output = withoutQuotes.replaceAll("_", underscoreReplacement);
String output = withoutQuotes.replaceAll("_", DEFAULT_UNDERSCORE_REPLACEMENT);
return output;
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,9 @@
import static org.batfish.datamodel.Names.generatedBgpPeerExportPolicyName;
import static org.batfish.datamodel.ospf.OspfNetworkType.BROADCAST;
import static org.batfish.datamodel.ospf.OspfNetworkType.POINT_TO_POINT;
import static org.batfish.datamodel.routing_policy.Common.DEFAULT_UNDERSCORE_REPLACEMENT;
import static org.batfish.datamodel.routing_policy.Common.generateSuppressionPolicy;
import static org.batfish.datamodel.routing_policy.communities.CommunitySetExprs.toMatchExpr;
import static org.batfish.representation.cisco_asa.AsaConfiguration.computeBgpDefaultRouteExportPolicyName;
import static org.batfish.representation.cisco_asa.AsaConfiguration.computeBgpPeerImportPolicyName;
import static org.batfish.representation.cisco_asa.AsaConfiguration.computeIcmpObjectGroupAclName;
Expand Down Expand Up @@ -99,14 +101,12 @@
import org.batfish.datamodel.routing_policy.communities.CommunitySetMatchAll;
import org.batfish.datamodel.routing_policy.communities.CommunitySetMatchAny;
import org.batfish.datamodel.routing_policy.communities.CommunitySetMatchExpr;
import org.batfish.datamodel.routing_policy.communities.CommunitySetMatchRegex;
import org.batfish.datamodel.routing_policy.communities.CommunitySetUnion;
import org.batfish.datamodel.routing_policy.communities.HasCommunity;
import org.batfish.datamodel.routing_policy.communities.InputCommunities;
import org.batfish.datamodel.routing_policy.communities.LiteralCommunitySet;
import org.batfish.datamodel.routing_policy.communities.MatchCommunities;
import org.batfish.datamodel.routing_policy.communities.SetCommunities;
import org.batfish.datamodel.routing_policy.communities.TypesFirstAscendingSpaceSeparated;
import org.batfish.datamodel.routing_policy.expr.BooleanExpr;
import org.batfish.datamodel.routing_policy.expr.BooleanExprs;
import org.batfish.datamodel.routing_policy.expr.CallExpr;
Expand Down Expand Up @@ -1627,11 +1627,7 @@ private static CommunityMatchRegex toCommunityMatchRegex(String regex) {
@Nonnull
private static CommunitySetAclLine toCommunitySetAclLineUnoptimized(
ExpandedCommunityListLine line) {
return new CommunitySetAclLine(
line.getAction(),
new CommunitySetMatchRegex(
new TypesFirstAscendingSpaceSeparated(ColonSeparatedRendering.instance()),
toJavaRegex(line.getRegex())));
return new CommunitySetAclLine(line.getAction(), toMatchExpr(toJavaRegex(line.getRegex())));
}

@Nonnull
Expand All @@ -1642,8 +1638,7 @@ private static String toJavaRegex(String ciscoRegex) {
} else {
withoutQuotes = ciscoRegex;
}
String underscoreReplacement = "(,|\\\\{|\\\\}|^|\\$| )";
String output = withoutQuotes.replaceAll("_", underscoreReplacement);
String output = withoutQuotes.replaceAll("_", DEFAULT_UNDERSCORE_REPLACEMENT);
return output;
}

Expand Down
Loading

0 comments on commit 0962bac

Please sign in to comment.