agodio/taco repository overview

RunTACO

Run with docker run -ti --rm agodio/taco. This will take you to /home/TACO, where TACO lives.

Let's verify a program:

java -cp lib/junit-4.8.2.jar:lib/*:bin org.junit.runner.JUnitCore edu.utep.ds2.BinarySearchBook

After some minutes, the output should contain this line:

* Outcome : SAT: A failure has been detected.

TACO found a counterexample! Run vim output/edu/utep/ds2/BinarySearch.java and navigate to the end of the file with G. The main method builds the parameters of binary required to expose the bug. Exit the vim editor with :q and open the code being analyzed with vim tests/edu/utep/ds2/BinarySearch.java

Can you spot the bug on the method binary?

You can fix the bug, recompile with ant compile and repeat the aforementioned java command to see whether TACO still finds a counterexample.

Finally, to configure the analysis run vim unittest/edu/utep/ds2/BinarySearchBookch.java. In this file you can set, for example, the loop unroll and integer bitwith.

Updating TACO

TACO is under development. To update TACO and its dependencies copy and paste the following code to the container:

cd /home/TACO
git -C /home/dynalloy4/ pull
git -C /home/jDynAlloy/ pull
git pull
ant -f ../dynalloy4/build.xml clean build jar
cp -v ../dynalloy4/dist/dynalloy4.jar ../jDynAlloy/lib/
cp -v ../dynalloy4/dist/dynalloy4.jar lib/
ant -f ../jDynAlloy/build.xml clean build jar
cp -v ../jDynAlloy/dist/jdynalloy.jar lib
ant clean compile