unive-ssv / tarsis

⚒ Implementation of the Tarsis abstract domain

TARSIS Abstract domain for static string analysis

Implementation of Twinning automata and regular expressions for string static analysis, by Luca Negrini, Vincenzo Arceri, Pietro Ferrara and Agostino Cortesi.

This repo is obsolete and it is not currently maintained. However, the Tarsis abstract domain is implemented and mantained in LiSA (https://github.com/lisa-analyzer/lisa).

Links:

• Preprint
• Published version

How to use the abstract domain

Class AutomatonString is the entry point for working with the domain. Use its parameterless constructor to build automaton representing a generic unknown string, and use the one accepting a string parameter to build an automaton recognizing the given string.

How to build the project

Tarsis comes as a gradle 6.0 project. For development with Eclipse, please install the Gradle IDE Pack plugin from the Eclipse marketplace, and make sure to import the project into the workspace as a Gradle project.

tarsis's Issues

Bug in `emptyStringReplace`

Let's add a test to ReplaceTest.java

@Test
public void replaceTestWithBranch001() {

	Automaton a = new Or(new Atom("a"), new Comp(new Atom("a"), new Or(new Atom("b"), new Atom("c")))).toAutomaton();
	Automaton search = Automata.mkAutomaton("");
	Automaton replacer = Automata.mkAutomaton("x");

	// (a | a(b|c)).replace("", "x") = {xax, xaxbx, xaxcx}
	checkEquality(Automata.replace(a, search, replacer).getLanguage(), "xax", "xaxbx", "xaxcx");
}

This test fails, because Automata.replace generates an automaton that accepts also "xa", which is not expected in this case.

Bug in `StringSearcher`

If you add a test analogous to replaceTestWithTop005

tarsis/src/test/java/it/unive/tarsis/test/ReplaceTest.java

Lines 346 to 355 in 3a4230e

	public void replaceTestWithTop005() {
	Automaton a = new Comp(new Or(new Atom("a"), new Atom("b")), TopAtom.INSTANCE).toAutomaton();
	Automaton search = Automata.mkAutomaton("a");
	Automaton replacer = Automata.mkAutomaton("");
	// (a | b)T.replace("abc", "") = {T, bT}
	checkEquality(Automata.replace(a, search, replacer).getLanguage(), TopAtom.INSTANCE.toString(),
	"b" + TopAtom.INSTANCE.toString());
	}

@Test
public void replaceTestWithTop005() {

	Automaton a = new Comp(new Or(new Atom("a"), new Atom("b")), TopAtom.INSTANCE).toAutomaton();
	Automaton search = Automata.mkAutomaton("b");  // <-- HERE I changed "a" to "b"
	Automaton replacer = Automata.mkAutomaton("");

	// (a | b)T.replace("b", "") = {aT, T}
	checkEquality(Automata.replace(a, search, replacer).getLanguage(), TopAtom.INSTANCE.toString(),
			"a" + TopAtom.INSTANCE.toString());
}

it raises an exception in StringSearcher.