zhihan/janala2-gradle

CATG updated

janala2-gradle

Migrate CATG (janala2) library to use Gradle and upgrade some dependencies. Branched from https://github.com/ksen007/janala2

Here is more information on the background of the project. https://www.youtube.com/watch?v=9lEvPwR7g-Q

Major changes

• Support Java 8
• Upgrade ASM library to 5.0.4
• Remove dependency on GNU trove
• Unit tests.

This is a working repository. The changes will be merged back to the main repository. I will keep this repository updated to experiment some ideas with.

Requirements

• Gradle 2
• Python 2
• CVC4 (http://cvc4.cs.nyu.edu/web/)
• Java 1.8

How to compile

In the root of the repository, do

gradle build

In addition, the project has a number of unit tests written in Groovy. To see the current test coverage. Do the following

gradle jacocoTestReport

And then look at the test coverage report in build/reports.

Integration tests

The integration tests from the original CATG repo are now included in this repo. To run these tests, first download a copy of asm-all-5.0.4.jar, automaton-1.11-8.jar and put them in the /lib directory.

At the root directory, invoke gradle to compile the test classes.

gradle integrationClasses

Go to /scripts directory and do the following.

./setup.sh

Run the integration tests by invoking the following command from /scripts directory.

python testall.py

Now a number of integration tests are failing. I am still investigating why.

More integration tests

More integration tests are being added. These tests require a working version of CVC4 in your path. To run these tests, do the following.

gradle integrationTest

janala2-gradle's Issues

Use String theory solver in CVC4

CVC4 now supports String theory, it might be worth to look into how to use the String theory solver to improve efficiency.

Support test runner

It would be nice to have a test runner. Like @RunWith in JUnit style.

LinkageError when referencing own <init> in try-catch block

I came across a subtle bug when trying to instrument a Java class that referenced its own constructor in a try-catch block. Here's a minimal test case Hello.java to reproduce the bug:

public class Hello {
    public static void main(String[] args) {
      try {
        Object o = new Hello();
      } catch (Exception e) {}
    }
}

If we try to instrument this class and log instructions as follows:

$JANALA_DIR/scripts/instrument.sh Hello

We get the following LinkageError with Java 1.8.0_102:

Exception in thread "main" java.lang.LinkageError: loader (instance of  sun/misc/Launcher$AppClassLoader): attempted  duplicate class definition for name: "Hello"
	at java.lang.ClassLoader.defineClass1(Native Method)
	at java.lang.ClassLoader.defineClass(ClassLoader.java:763)
	at java.security.SecureClassLoader.defineClass(SecureClassLoader.java:142)
	at java.net.URLClassLoader.defineClass(URLClassLoader.java:467)
	at java.net.URLClassLoader.access$100(URLClassLoader.java:73)
	at java.net.URLClassLoader$1.run(URLClassLoader.java:368)
	at java.net.URLClassLoader$1.run(URLClassLoader.java:362)
	at java.security.AccessController.doPrivileged(Native Method)
	at java.net.URLClassLoader.findClass(URLClassLoader.java:361)
	at java.lang.ClassLoader.loadClass(ClassLoader.java:424)
	at sun.misc.Launcher$AppClassLoader.loadClass(Launcher.java:331)
	at java.lang.ClassLoader.loadClass(ClassLoader.java:357)
	at sun.launcher.LauncherHelper.checkAndLoadMain(LauncherHelper.java:495)

The funny thing is that if we replace new Hello() with new Object() or any new Foo() the instrumentation works just fine. Similarly, the error disappears if we remove the surrounding try-catch block.

However, this is not a bug inherent to Janala. The problem is actually rooted in ASM, because the same error occurs even if you strip off all instrumentation and simply read/write the exact same bytecode in janala.instrument.SnoopInstructionTransformer (by replacing the ClassVisitor with a visitor that does nothing). In such a case, disabling COMPUTE_FRAMES in the constructor of ASM's ClassWriter gets rid of the LinkageError, indicating that the bug lies within the computation of stack map frames in the bytecode.

Consider using SMT-Lib interface

Using SMT-lib standard interface allows one to swap CVC4 with other SMT solvers, like Z3.

Add more tests to get a higher test coverage

Sort fields of base class before the fields of sub-class.

It seems that every concrete class has fields and the code does not guarantee that the fields of base classes always sorted before subclass. Consider the following case

Sup
-f

Sub
-g

The fields created should be
[f]
and
[f, g]
so that when setting the f field on the either super or sub class, it is setting the same field. In the current implementation it is
[f]
and
[g, f]
and the ObjectValue is confused which field is set.

Cannot use annotation reflections with instrumentation

With the current setup, I got a NoClassDefFoundError when I use reflections at run time. This is not limited to the new Test annotation but applies to all annotations.

http://stackoverflow.com/questions/32870098/how-to-make-java-agent-and-reflection-work-together

ArrayIndexOutOfBounds when creating a simple object.

Hello,

Running the following code in janala (Ubuntu 15.04 64-bit, Java 8) results in an exception being thrown.

package tests.bugreports.putfieldbug;

public class SienaBuggyExample {

  private int irrelevant0;
  private int irrelevant1;
  private Object tmp;


  public SienaBuggyExample() {
    tmp = new Object();
  }

  public static void main(String[] args) {
    SienaBuggyExample tok = new SienaBuggyExample();
    System.out.println("ok");
  }
}

Here is the stacktrace:

java.lang.ArrayIndexOutOfBoundsException: 2
    at janala.interpreters.ObjectValue.setField(ObjectValue.java:104)
    at janala.interpreters.ConcolicInterpreter.visitPUTFIELD(ConcolicInterpreter.java:1384)
    at janala.logger.inst.PUTFIELD.visit(PUTFIELD.java:16)
    at janala.logger.DirectConcolicExecution.log(DirectConcolicExecution.java:58)
    at janala.logger.AbstractLogger.SPECIAL(AbstractLogger.java:706)
    at janala.logger.DJVM.SPECIAL(DJVM.java:708)
    at tests.bugreports.putfieldbug.SienaBuggyExample.<init>(SienaBuggyExample.java:11)
    at tests.bugreports.putfieldbug.SienaBuggyExample.main(SienaBuggyExample.java:15)

After some initial debugging, I believe this issue happens because there is a reference to ObjectValue.NULL instead of the new Object() during the call to SienaBuggyExample' constructor. However, I have no clue why this is happening :(

Investigate whether the 'init' methods in the ClassNames and ObjectInfo classes are still needed.

As far as I can tell, these functions are never called.

Some integration tests are failing.

Consider upgrading ChocoSolver to Choco3 and address the differences with CVC4.

Optimize the two-pass solving strategy

In the solver it solves two SMT problems, the first is an abstract one where strings are handled by examining lengths. And the second pass scalarize the strings as vectors of chars. If the program does not have string variables, there is no need for the second pass.