Abstract semantics for repeat in Tarsis

lisa-analyzer · Jul 6, 2023 · dbb0c48 · dbb0c48
1 parent 581382b
commit dbb0c48
Show file tree

Hide file tree

Showing 8 changed files with 74 additions and 15 deletions.
diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/tarsis/RegexAutomaton.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/string/tarsis/RegexAutomaton.java
@@ -455,4 +455,15 @@ private RegexAutomaton union(RegexAutomaton... automata) {
 
 		return result;
 	}
+
+	/**
+	 * Yields an automaton that corresponds to the {@code n}-time concatenation of {@code this}.
+	 * @param n the number of repetitions
+	 * @return an automaton that corresponds to the {@code n}-time concatenation of {@code this}
+	 */
+	public RegexAutomaton repeat(int n) {
+		if (n == 0)
+			return emptyString();		
+		return toRegex().repeat(n).toAutomaton(this);
+	}
 }
diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/datastructures/regex/Atom.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/datastructures/regex/Atom.java
@@ -1,11 +1,12 @@
 package it.unive.lisa.util.datastructures.regex;
 
+import java.util.HashSet;
+import java.util.Set;
+
 import it.unive.lisa.util.datastructures.automaton.AutomataFactory;
 import it.unive.lisa.util.datastructures.automaton.Automaton;
 import it.unive.lisa.util.datastructures.automaton.TransitionSymbol;
 import it.unive.lisa.util.datastructures.regex.symbolic.SymbolicString;
-import java.util.HashSet;
-import java.util.Set;
 
 /**
  * A {@link RegularExpression} representing a single string.
@@ -78,7 +79,7 @@ public RegularExpression simplify() {
 
 	@Override
 	public <A extends Automaton<A, T>,
-			T extends TransitionSymbol<T>> A toAutomaton(AutomataFactory<A, T> factory) {
+	T extends TransitionSymbol<T>> A toAutomaton(AutomataFactory<A, T> factory) {
 		return isEmpty() ? factory.emptyString() : factory.singleString(string);
 	}
 
@@ -181,4 +182,16 @@ public RegularExpression[] explode() {
 	protected int compareToAux(RegularExpression other) {
 		return string.compareTo(other.asAtom().string);
 	}
+
+	@Override
+	public RegularExpression repeat(int n) {
+		if (n == 0)
+			return Atom.EPSILON;
+
+		RegularExpression r = Atom.EPSILON;
+		for (int i = 0; i < n; i++)
+			r = new Comp(r, this);
+		r.simplify();
+		return r;
+	}
 }
diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/datastructures/regex/Comp.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/datastructures/regex/Comp.java
@@ -1,11 +1,12 @@
 package it.unive.lisa.util.datastructures.regex;
 
+import java.util.HashSet;
+import java.util.Set;
+
 import it.unive.lisa.util.datastructures.automaton.AutomataFactory;
 import it.unive.lisa.util.datastructures.automaton.Automaton;
 import it.unive.lisa.util.datastructures.automaton.TransitionSymbol;
 import it.unive.lisa.util.datastructures.regex.symbolic.SymbolicString;
-import java.util.HashSet;
-import java.util.Set;
 
 /**
  * A {@link RegularExpression} representing the sequential composition of two
@@ -288,4 +289,16 @@ protected int compareToAux(RegularExpression other) {
 			return cmp;
 		return second.compareTo(other.asComp().second);
 	}
+
+	@Override
+	public RegularExpression repeat(int n) {
+		if (n == 0)
+			return Atom.EPSILON;
+
+		RegularExpression r = Atom.EPSILON;
+		for (int i = 0; i < n; i++)
+			r = new Comp(r, this);
+		r.simplify();
+		return r;
+	}
 }
diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/datastructures/regex/EmptySet.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/datastructures/regex/EmptySet.java
@@ -1,10 +1,11 @@
 package it.unive.lisa.util.datastructures.regex;
 
+import java.util.Collections;
+import java.util.Set;
+
 import it.unive.lisa.util.datastructures.automaton.AutomataFactory;
 import it.unive.lisa.util.datastructures.automaton.Automaton;
 import it.unive.lisa.util.datastructures.automaton.TransitionSymbol;
-import java.util.Collections;
-import java.util.Set;
 
 /**
  * A {@link RegularExpression} representing the empty set of strings.
@@ -131,4 +132,9 @@ public RegularExpression[] explode() {
 	protected int compareToAux(RegularExpression other) {
 		return 0;
 	}
+
+	@Override
+	public RegularExpression repeat(int n) {
+		return this;
+	}
 }
diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/datastructures/regex/Or.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/datastructures/regex/Or.java
@@ -1,10 +1,11 @@
 package it.unive.lisa.util.datastructures.regex;
 
+import java.util.HashSet;
+import java.util.Set;
+
 import it.unive.lisa.util.datastructures.automaton.AutomataFactory;
 import it.unive.lisa.util.datastructures.automaton.Automaton;
 import it.unive.lisa.util.datastructures.automaton.TransitionSymbol;
-import java.util.HashSet;
-import java.util.Set;
 
 /**
  * A {@link RegularExpression} representing an or between two other regular
@@ -277,4 +278,9 @@ protected int compareToAux(RegularExpression other) {
 			return cmp;
 		return second.compareTo(other.asOr().second);
 	}
+
+	@Override
+	public RegularExpression repeat(int n) {
+		return new Or(first.repeat(n), second.repeat(n));
+	}
 }
diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/datastructures/regex/RegularExpression.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/datastructures/regex/RegularExpression.java
@@ -1,11 +1,12 @@
 package it.unive.lisa.util.datastructures.regex;
 
+import java.util.Set;
+import java.util.stream.Collectors;
+
 import it.unive.lisa.util.datastructures.automaton.AutomataFactory;
 import it.unive.lisa.util.datastructures.automaton.Automaton;
 import it.unive.lisa.util.datastructures.automaton.TransitionSymbol;
 import it.unive.lisa.util.datastructures.regex.symbolic.SymbolicString;
-import java.util.Set;
-import java.util.stream.Collectors;
 
 /**
  * A regular expression that can be recognized by an {@link Automaton}, or that
@@ -310,6 +311,8 @@ public String toString() {
 	 */
 	protected abstract Set<PartialSubstring> substringAux(int charsToSkip, int missingChars);
 
+	public abstract RegularExpression repeat(int n);
+
 	/**
 	 * Yields {@code true} if and only if this regular expression corresponds to
 	 * the empty string or to no strings at all.

diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/datastructures/regex/Star.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/datastructures/regex/Star.java
@@ -1,11 +1,12 @@
 package it.unive.lisa.util.datastructures.regex;
 
+import java.util.HashSet;
+import java.util.Set;
+
 import it.unive.lisa.util.datastructures.automaton.AutomataFactory;
 import it.unive.lisa.util.datastructures.automaton.Automaton;
 import it.unive.lisa.util.datastructures.automaton.TransitionSymbol;
 import it.unive.lisa.util.datastructures.regex.symbolic.SymbolicString;
-import java.util.HashSet;
-import java.util.Set;
 
 /**
  * A {@link RegularExpression} representing a loop, repeated an arbitrary number
@@ -234,4 +235,9 @@ public RegularExpression[] explode() {
 	protected int compareToAux(RegularExpression other) {
 		return op.compareTo(other.asStar().op);
 	}
+
+	@Override
+	public RegularExpression repeat(int n) {
+		return this;
+	}
 }
diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/datastructures/regex/TopAtom.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/util/datastructures/regex/TopAtom.java
@@ -1,11 +1,12 @@
 package it.unive.lisa.util.datastructures.regex;
 
+import java.util.HashSet;
+import java.util.Set;
+
 import it.unive.lisa.util.datastructures.automaton.AutomataFactory;
 import it.unive.lisa.util.datastructures.automaton.Automaton;
 import it.unive.lisa.util.datastructures.automaton.TransitionSymbol;
 import it.unive.lisa.util.datastructures.regex.symbolic.SymbolicString;
-import java.util.HashSet;
-import java.util.Set;
 
 /**
  * A {@link RegularExpression} representing a sequence of unknown characters of