SearchRoutePolicies: handle the Java regex format for Juniper AS-path…

… regexes (batfish#7984)

* handle the Java regex format for Juniper AS-path regexes

projects/minesweeper/src/main/java/org/batfish/minesweeper/SymbolicAsPathRegex.java

@@ -14,18 +14,26 @@ public class SymbolicAsPathRegex extends SymbolicRegex implements Comparable<Sym
 
   @Nonnull private static final String AS_NUM_REGEX = "(0|[1-9][0-9]*)";
 
-  // a regex that represents the language of AS paths: a space-separated list of
-  // AS numbers, starting and ending with the ^ (start-of-string) and $ (end-of-string)
-  // tokens respectively.
-  // Note: in general an AS path is a list of *sets* of AS numbers.  but the format of
-  // regexes over sets is apparently vendor-dependent.  for now we do not support them.
+  /**
+   * A regex that represents the language of AS paths: a space-separated list of AS numbers,
+   * starting and ending with the ^ (start-of-string) and $ (end-of-string) tokens respectively. For
+   * non-empty AS-path regexes we require two ^ characters at the front. This is because of the way
+   * that Juniper AS-path regexes are translated to Java. For example, "^80$" is translated to "^(^|
+   * )80$". Because the automaton library treats ^ as a regular character we have to deal with the
+   * fact that there can be two of them at the front. We will therefore arrange that there are
+   * _always_ two of them at the front, regardless of what the original Java regex looks like (see
+   * toAutomaton below), so we can properly compare regexes to one another.
+   *
+   * <p>Note: in general an AS path is a list of *sets* of AS numbers. but the format of regexes
+   * over sets is apparently vendor-dependent. for now we do not support them.
+   */
   @Nonnull
   private static final String AS_PATH_REGEX =
       // the empty AS-path
-      "^$"
+      "^^$"
           + "|"
           // non-empty AS-paths
-          + "^"
+          + "^^"
           + "("
           + AS_NUM_REGEX
           + " "
@@ -35,11 +43,12 @@ public class SymbolicAsPathRegex extends SymbolicRegex implements Comparable<Sym
 
   /**
    * When converting an AS path regex to an automaton (see toAutomaton()), we intersect with this
-   * automaton, which represents the language of AS paths. Doing so serves two purposes. First, it
-   * is necessary for correctness of the symbolic analysis. For example, a regex like ".*" does not
-   * actually match any possible string since AS paths cannot be arbitrary strings. Second, it
-   * ensures that when we solve for AS paths that match regexes, we will get examples that are
-   * sensible and also able to be parsed by Batfish.
+   * automaton, which represents the language of AS paths. Doing so serves several purposes. First,
+   * it is necessary for correctness of the symbolic analysis. For example, a regex like ".*" does
+   * not actually match any possible string since AS paths cannot be arbitrary strings. Second, it
+   * addresses the issue of different formats for Java regexes mentioned above. Third, it ensures
+   * that when we solve for AS paths that match regexes, we will get examples that are sensible and
+   * also able to be parsed by Batfish.
    */
   @Nonnull static final Automaton AS_PATH_FSM = new RegExp(AS_PATH_REGEX).toAutomaton();
 

projects/minesweeper/src/main/java/org/batfish/minesweeper/SymbolicRegex.java

@@ -10,7 +10,7 @@ public abstract class SymbolicRegex {
   @Nonnull protected final String _regex;
 
   public SymbolicRegex(String regex) {
-    _regex = regex;
+    _regex = toAutomatonRegex(regex);
   }
 
   @Nonnull
@@ -25,4 +25,12 @@ public String getRegex() {
    * @return the automaton
    */
   public abstract Automaton toAutomaton();
+
+  // modify the given regex to conform to the grammar of the Automaton library that we use to
+  // analyze regexes
+  @Nonnull
+  private String toAutomatonRegex(String regex) {
+    // the Automaton library does not support the character class \d
+    return regex.replace("\\d", "[0-9]");
+  }
 }

projects/minesweeper/src/main/java/org/batfish/minesweeper/question/searchroutepolicies/SearchRoutePoliciesAnswerer.java

@@ -207,11 +207,11 @@ static AsPath satAssignmentToAsPath(BDD fullModel, BDDRoute r, ConfigAtomicPredi
     // As-path regex automata should only accept strings with this property;
     // see SymbolicAsPathRegex::toAutomaton
     checkState(
-        asPathStr.startsWith("^") && asPathStr.endsWith("$"),
+        asPathStr.startsWith("^^") && asPathStr.endsWith("$"),
         "AS-path example %s has an unexpected format",
         asPathStr);
-    // strip off the leading ^ and trailing $
-    asPathStr = asPathStr.substring(1, asPathStr.length() - 1);
+    // strip off the leading ^^ and trailing $
+    asPathStr = asPathStr.substring(2, asPathStr.length() - 1);
     // the string is a space-separated list of numbers; convert them to a list of numbers
     List<Long> asns;
     if (asPathStr.isEmpty()) {

projects/minesweeper/src/test/java/org/batfish/minesweeper/RegexAtomicPredicatesTest.java

@@ -76,13 +76,13 @@ public void testInitAtomicPredicatesAsPath() {
 
     assertEquals(asPathAPs.getNumAtomicPredicates(), 5);
 
-    Automaton a1 = new RegExp("^$").toAutomaton();
+    Automaton a1 = new RegExp("^^$").toAutomaton();
     // starts with 5 and ends with 4
-    Automaton a2 = new RegExp("^5 ((0|[1-9][0-9]*) )*4$").toAutomaton();
+    Automaton a2 = new RegExp("^^5 ((0|[1-9][0-9]*) )*4$").toAutomaton();
     // ends with 4 but does not start with 5
-    Automaton a3 = new RegExp("^([0-4]|[6-9]|[1-9][0-9]+) ((0|[1-9][0-9]*) )*4$").toAutomaton();
+    Automaton a3 = new RegExp("^^([0-4]|[6-9]|[1-9][0-9]+) ((0|[1-9][0-9]*) )*4$").toAutomaton();
     // starts with 5 but does not end with 4
-    Automaton a4 = new RegExp("^5( (0|[1-9][0-9]*))* ([0-3]|[5-9]|[1-9][0-9]+)$").toAutomaton();
+    Automaton a4 = new RegExp("^^5( (0|[1-9][0-9]*))* ([0-3]|[5-9]|[1-9][0-9]+)$").toAutomaton();
 
     assertEquals(asPathAPs.getAtomicPredicateAutomata().size(), 5);
     assertThat(asPathAPs.getAtomicPredicateAutomata().values(), hasItem(a1));

projects/minesweeper/src/test/java/org/batfish/minesweeper/SymbolicAsPathRegexTest.java

@@ -14,7 +14,7 @@ public class SymbolicAsPathRegexTest {
   private static final String UNDERSCORE = "(,|{|}|^|$| )";
 
   @Test
-  public void testToAutomaton() {
+  public void testToAutomatonRegex() {
 
     SymbolicAsPathRegex r1 = new SymbolicAsPathRegex("^40$");
     SymbolicAsPathRegex r2 = new SymbolicAsPathRegex("^$");
@@ -26,12 +26,28 @@ public void testToAutomaton() {
     SymbolicAsPathRegex r5 =
         new SymbolicAsPathRegex(UNDERSCORE + "40" + UNDERSCORE + "50" + UNDERSCORE);
 
-    assertThat(r1.toAutomaton(), equalTo(new RegExp("^40$").toAutomaton()));
-    assertThat(r2.toAutomaton(), equalTo(new RegExp("^$").toAutomaton()));
-    assertThat(r3.toAutomaton(), equalTo(new RegExp("^((0|[1-9][0-9]*) )*40$").toAutomaton()));
-    assertThat(r4.toAutomaton(), equalTo(new RegExp("^40( (0|[1-9][0-9]*))*$").toAutomaton()));
+    assertThat(r1.toAutomaton(), equalTo(new RegExp("^^40$").toAutomaton()));
+    assertThat(r2.toAutomaton(), equalTo(new RegExp("^^$").toAutomaton()));
+    assertThat(r3.toAutomaton(), equalTo(new RegExp("^^((0|[1-9][0-9]*) )*40$").toAutomaton()));
+    assertThat(r4.toAutomaton(), equalTo(new RegExp("^^40( (0|[1-9][0-9]*))*$").toAutomaton()));
     assertThat(
         r5.toAutomaton(),
-        equalTo(new RegExp("^((0|[1-9][0-9]*) )*40 50( (0|[1-9][0-9]*))*$").toAutomaton()));
+        equalTo(new RegExp("^^((0|[1-9][0-9]*) )*40 50( (0|[1-9][0-9]*))*$").toAutomaton()));
+  }
+
+  @Test
+  public void testToAutomatonJuniper() {
+
+    SymbolicAsPathRegex r1 = new SymbolicAsPathRegex("^(^| )40$");
+    SymbolicAsPathRegex r2 = new SymbolicAsPathRegex("^$");
+    // .*40$
+    SymbolicAsPathRegex r3 = new SymbolicAsPathRegex("^((^| )\\d+)*(^| )40$");
+    // ^40.*
+    SymbolicAsPathRegex r4 = new SymbolicAsPathRegex("^(^| )40((^| )\\d+)*$");
+
+    assertThat(r1.toAutomaton(), equalTo(new RegExp("^^40$").toAutomaton()));
+    assertThat(r2.toAutomaton(), equalTo(new RegExp("^^$").toAutomaton()));
+    assertThat(r3.toAutomaton(), equalTo(new RegExp("^^((0|[1-9][0-9]*) )*40$").toAutomaton()));
+    assertThat(r4.toAutomaton(), equalTo(new RegExp("^^40( (0|[1-9][0-9]*))*$").toAutomaton()));
   }
 }