trim abstract semantics defined on regexes

lisa-analyzer · Jul 20, 2023 · cbd3a37 · cbd3a37
1 parent 3fac166
commit cbd3a37
Show file tree

Hide file tree

Showing 8 changed files with 64 additions and 49 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
@@ -471,7 +471,15 @@ public RegexAutomaton repeat(long n) {
 		return toRegex().simplify().repeat(n).toAutomaton(this).minimize();
 	}
 
+	public RegexAutomaton trimLeft() {
+		return this.toRegex().trimLeft().simplify().toAutomaton(this);
+	}
+
+	public RegexAutomaton trimRight() {
+		return this.toRegex().trimRight().simplify().toAutomaton(this);
+	}
+
 	public RegexAutomaton trim() {
-		return toRegex().simplify().trim().toAutomaton(this);
+		return this.toRegex().trimRight().simplify().trimLeft().simplify().toAutomaton(this);
 	}
 }
diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/tarsis/TrimTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/tarsis/TrimTest.java
@@ -42,13 +42,8 @@ public void trimSingleString() throws MathNumberConversionException {
 		Tarsis f = new Tarsis(comp2);
 		assertTrue(f.trim().getAutomaton().isEqualTo(RegexAutomaton.string("a b")));
 
-		// " a b c "*.trim() = "a b c " + (" a b c ")* + " a b c"
-		Tarsis g = new Tarsis(abc_with_ws.star());
-		assertTrue(g.trim().getAutomaton().isEqualTo(RegexAutomaton.string("a b c   ").concat(abc_with_ws.star())
-				.concat(RegexAutomaton.string("   a b c")).star()));
-
 		// " abc " + " ".trim() = "abc"
-		Tarsis h = new Tarsis(comp3);
-		assertTrue(h.trim().getAutomaton().isEqualTo(RegexAutomaton.string("abc")));
+		Tarsis g = new Tarsis(comp3);
+		assertTrue(g.trim().getAutomaton().isEqualTo(RegexAutomaton.string("abc")));
 	}
 }
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
@@ -196,17 +196,23 @@ public RegularExpression repeat(long n) {
 	}
 
 	@Override
-	public RegularExpression trim() {
-		return new Atom(this.string.trim());
+	public RegularExpression trimLeft() {
+		String trimLeft = StringUtils.stripStart(this.string, null);
+		if (trimLeft.isEmpty())
+			return Atom.EPSILON;
+		return new Atom(trimLeft);
 	}
 
 	@Override
-	public RegularExpression trimLeft() {
-		return new Atom(StringUtils.stripStart(this.string, null));
+	public RegularExpression trimRight() {
+		String trimRight = StringUtils.stripEnd(this.string, null);
+		if (trimRight.isEmpty())
+			return Atom.EPSILON;
+		return new Atom(trimRight);
 	}
 
 	@Override
-	public RegularExpression trimRight() {
-		return new Atom(StringUtils.stripEnd(this.string, null));
+	protected boolean readsWhiteSpaceString() {
+		return string.trim().isEmpty();
 	}
 }
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
@@ -300,34 +300,38 @@ public RegularExpression repeat(long n) {
 		return r.simplify();
 	}
 
-	@Override
-	public RegularExpression trim() {
-		RegularExpression trimLeftFirst = first.trimLeft().simplify();
-		if (trimLeftFirst.isEmpty())
-			return second.trim();
-
-		RegularExpression trimRightSecond = second.trimRight().simplify();
-		if (trimRightSecond.isEmpty())
-			return first.trim();
-
-		return new Comp(trimLeftFirst, trimRightSecond).simplify();
-	}
-
 	@Override
 	public RegularExpression trimLeft() {
-		RegularExpression trimLeftFirst = this.first.trimLeft().simplify();
+		RegularExpression trimLeftFirst = first.trimLeft().simplify();
+		// it means that first reads just whitespaces strings (L(first)
+		// \subseteq { }*)
 		if (trimLeftFirst.isEmpty())
 			return this.second.trimLeft();
+		// first reads at least a whitespace string
+		else if (first.readsWhiteSpaceString())
+			return new Or(new Comp(trimLeftFirst, second), second.trimLeft());
+//			return new Comp(trimLeftFirst, new Or(second, second.trimLeft()));
 		else
 			return new Comp(trimLeftFirst, second);
 	}
 
 	@Override
 	public RegularExpression trimRight() {
-		RegularExpression trimRightSecond = this.second.trimRight().simplify();
+		RegularExpression trimRightSecond = second.trimRight().simplify();
+		// it means that second reads just whitespaces strings (L(second)
+		// \subseteq { }*)
 		if (trimRightSecond.isEmpty())
 			return this.first.trimRight();
+		// second reads at least a whitespace string
+		else if (second.readsWhiteSpaceString())
+			return new Or(new Comp(first, trimRightSecond), first.trimRight());
+//			return new Comp(new Or(first, first.trimRight()), trimRightSecond);
 		else
 			return new Comp(this.first, trimRightSecond);
 	}
+
+	@Override
+	protected boolean readsWhiteSpaceString() {
+		return first.readsWhiteSpaceString() && second.readsWhiteSpaceString();
+	}
 }
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
@@ -138,17 +138,17 @@ public RegularExpression repeat(long n) {
 	}
 
 	@Override
-	public RegularExpression trim() {
+	public RegularExpression trimLeft() {
 		return this;
 	}
 
 	@Override
-	public RegularExpression trimLeft() {
+	public RegularExpression trimRight() {
 		return this;
 	}
 
 	@Override
-	public RegularExpression trimRight() {
-		return this;
+	protected boolean readsWhiteSpaceString() {
+		return false;
 	}
 }
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
@@ -283,11 +283,6 @@ public RegularExpression repeat(long n) {
 		return new Or(first.repeat(n), second.repeat(n)).simplify();
 	}
 
-	@Override
-	public RegularExpression trim() {
-		return new Or(first.trim(), second.trim());
-	}
-
 	@Override
 	public RegularExpression trimLeft() {
 		return new Or(first.trimLeft(), second.trimLeft());
@@ -298,4 +293,9 @@ public RegularExpression trimLeft() {
 	public RegularExpression trimRight() {
 		return new Or(first.trimRight(), second.trimRight());
 	}
+
+	@Override
+	protected boolean readsWhiteSpaceString() {
+		return first.readsWhiteSpaceString() || second.readsWhiteSpaceString();
+	}
 }
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
@@ -312,8 +312,6 @@ public String toString() {
 
 	public abstract RegularExpression repeat(long n);
 
-	public abstract RegularExpression trim();
-
 	public abstract RegularExpression trimLeft();
 
 	public abstract RegularExpression trimRight();
@@ -431,6 +429,8 @@ public String toString() {
 	 */
 	public abstract RegularExpression[] explode();
 
+	protected abstract boolean readsWhiteSpaceString();
+
 	/**
 	 * Builds the Kleene closure of this regular expression ({@link Star}),
 	 * recognizing {@code this} zero or more times.

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
@@ -241,21 +241,23 @@ public RegularExpression repeat(long n) {
 	}
 
 	@Override
-	public RegularExpression trim() {
-		RegularExpression left = this.op.trimLeft().simplify();
-		if (left.isEmpty())
+	public RegularExpression trimLeft() {
+		RegularExpression trimLeft = op.trimLeft().simplify();
+		if (trimLeft.isEmpty())
 			return Atom.EPSILON;
-		RegularExpression right = this.op.trimRight().simplify();
-		return new Star(new Comp(new Comp(left, this), right)).simplify();
+		return new Or(Atom.EPSILON, new Comp(trimLeft, this));
 	}
 
 	@Override
-	public RegularExpression trimLeft() {
-		return new Star(new Comp(this.op.trimLeft(), op));
+	public RegularExpression trimRight() {
+		RegularExpression trimRight = op.trimRight();
+		if (trimRight.isEmpty())
+			return Atom.EPSILON;
+		return new Or(Atom.EPSILON, new Comp(this, trimRight));
 	}
 
 	@Override
-	public RegularExpression trimRight() {
-		return new Comp(this, op.trimRight());
+	protected boolean readsWhiteSpaceString() {
+		return op.readsWhiteSpaceString();
 	}
 }