Problems with using the checker-framework in my Gradle project.

[Laurens Brinker]

Hello,

My name is Laurens Brinker, a student from Radboud University Nijmegen (The Netherlands), currently writing my bachelor's thesis.
For my thesis I want to use SPARTA to analyse an application made by my university. This android application is called IRMA Cardproxy (https://github.com/credentials/irma_android_cardproxy). I've followed all your instructions on the checker-framework page and tried the tutorial cases. Now, I've tried both via command-line and via the Eclipse plugin, but I just can't get my project of the IRMA application to build. Normally, the project builds with Gradle and uses the build.gradle file to get the dependencies. With an unaltered build.gradle the projects builds fine, but when I follow the the instructions from the manual,http://types.cs.washington.edu/checker-framework/current/checker-framework-manual.html#gradle , and alter my build.gradle to contain the given code, I get some weird errors (see below for link to error information).

IMPORTANT: For Gradle, I tried to run the GradleJava8Example (https://github.com/typetools/checker-framework/tree/master/checker/examples/GradleExamples) and it builds perfectly and gives the expected output. 

However, I can't get my own project to build.
I am not an expert on the java compiler, nor on the specifics of gradle, so I might have overlooked / forgotten something. But I think there is still something wrong with my build.gradle, or due to project specific properties, I need to change some things in my build.gradle to make it work. 

My project: https://github.com/LaurensBrinker/irmaproxychecker
My build.gradle file: https://github.com/LaurensBrinker/irmaproxychecker/blob/master/build.gradle

I would like some advise on how to fix this error so I can start annotating and analyzing the application.

==================
Information:

My project (altered application source): https://github.com/LaurensBrinker/irmaproxychecker
Original application Source Code: https://github.com/credentials/irma_android_cardproxy
Original build.gradle file: https://github.com/credentials/irma_android_cardproxy/blob/master/build.gradle
My altered build.gradle file: https://github.com/LaurensBrinker/irmaproxychecker/blob/master/build.gradle

ERRORS: https://github.com/LaurensBrinker/irmaproxychecker/blob/master/error.txt 


=================
Summary of error:

warning: unknown enum constant ElementType.TYPE_USE
warning: unknown enum constant ElementType.TYPE_PARAMETER
error: InvocationTargetException when invoking constructor for class org.checkerframework.checker.nullness.KeyForVisitor; Underlying cause: InvocationTargetException when invoking constructor for class org.checkerframework.checker.nullness.KeyForAnnotatedTypeFactory; Underlying cause: com.sun.tools.javac.code.Symbol$CompletionFailure: class file for java.lang.Class$AnnotationData not found; invoke the compiler with -AprintErrorStack to see the stack trace.
warning: -source 1.6 does not support type annotations
warning: -source 1.6 does not support type annotations

=================

Kind regards,

Laurens Brinker
Student Computer Science
Radboud University Nijmegen
laurens...@student.ru.nl

ps. My apologies if this is not the place to post this.

[Suzanne Millstein]

Hi Laurens,

Integrating with the Android Gradle plugin is slightly different than integrating with a plain Gradle build script.  We have had success using the instructions in this issue: 

https://github.com/typetools/checker-framework/issues/564#issuecomment-200927221

(Note that those instructions have been used with Android Plugin for Gradle version 1.5.0 and your app seems to be using 1.1.1.)  

Please give those instructions a try and let us know whether they work for you or not.

Thanks,

Suzanne

[laurens...@gmail.com]

Thanks for the quick reply!

I was missing the gradle.projectsEvaluated (which was not listed in the manual). 

Now I have a follow-up question:

I want to use SPARTA to analyse information-flow properties of my application.

I installed the Checker-Framework that was inside the SPARTA repository, but do I have to complete some additional steps to use SPARTA specific annotations (Like @Source and @Sink)?

I read the manual and the two steps that are different from the Checker-Framework installation is that I have to set the SPARTA_CODE variable and that I have to add build targets to the build.xml file.

Since I use gradle I do not have a build.xml file, so is there some documentation on doing this in gradle (since I couldn't find it in the manual).

If there is a problem in my understanding of SPARTA I apologize.

Thanks again for helping me getting the Framework to work Suzanne!

- Laurens Brinker

[Suzanne Millstein]

Hi Laurens,

We are working on adding instructions to the SPARTA manual on how to use it with the Android plugin for Gradle. Below are instructions on how to do so.  Please let us know whether they work for you or not.  Thanks! 

To run the Flow Checker, set the environment variable SPARTA_CODE to a directory with https://github.com/typetools/sparta/releases/download/sparta-1.0.2/sparta-1.0.2.jar in it.  Then add the following to your build.gradle:    

configurations {

    checkerFrameworkJavac {

        description = 'a customization of the Open JDK javac compiler with additional support for type annotations'

    }

    checkerFrameworkAnnotatedJDK {

       description = 'a copy of JDK classes with Checker Framework type qualifers inserted'

    }

    checkerFramework {

       description = 'The Checker Framework: custom pluggable types for Java'

    }

    sparta

}

def typecheck = project.properties['typecheck'] ?: false

allprojects {

if (typecheck) {

    gradle.projectsEvaluated {

        tasks.withType(JavaCompile).all { JavaCompile compile ->

        compile.options.compilerArgs = [

                '-processor', 'sparta.checkers.FlowChecker',

                '-processorpath', "${configurations.sparta.asPath}:${configurations.checkerFramework.asPath}",

                // uncomment to turn Checker Framework errors into warnings

                //'-Awarns',

                "-AprintErrorStack"

        ]

            compile.options.compilerArgs += ['-source', '7', '-target', '7']

            options.bootClasspath = "${configurations.checkerFrameworkJavac.asPath}:" + System.getProperty("sun.boot.class.path") + ":" + options.bootClasspath

            options.fork = true

            options.forkOptions.jvmArgs += ["-Xbootclasspath/p:${configurations.checkerFrameworkJavac.asPath}"]

        }

    }

}

}

dependencies {

    ext.checkerFrameworkVersion = '1.9.11'

    ext.jdkVersion = JavaVersion.current().isJava7() ? 'jdk7' : 'jdk8'

    checkerFrameworkAnnotatedJDK "org.checkerframework:${jdkVersion}:${checkerFrameworkVersion}"

    checkerFrameworkJavac "org.checkerframework:compiler:${checkerFrameworkVersion}"

    checkerFramework "org.checkerframework:checker:${checkerFrameworkVersion}"

    compile "org.checkerframework:checker-qual:${checkerFrameworkVersion}"

    sparta fileTree(dir: "$System.env.SPARTA_CODE", include: ['*.jar'])

    if (typecheck) {

        compile fileTree(dir: "$System.env.SPARTA_CODE", include: ['*.jar'])

    }

....Other dependencies....

}

Then you can run the Flow Checker like so:

gradle compileReleaseJavaWithJavac -Ptypecheck=true

Any Flow Checker option you wish to use can be added to compile.options.compilerArgs:  For example, you can use the flowPolicy option like so:

compile.options.compilerArgs = [

                '-processor', 'sparta.checkers.FlowChecker',

                '-processorpath', "${configurations.sparta.asPath}:${configurations.checkerFramework.asPath}",

                `-AflowPolicy=pathToFlowPolicy"

        ]

Thanks,

Suzanne

--

---
You received this message because you are subscribed to the Google Groups "Checker Framework discussion" group.
To unsubscribe from this group and stop receiving emails from it, send an email to checker-framework-...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[laurens...@gmail.com]

Thanks for your reply, it worked!

The output is now:

*************************

(...)

  flow forbidden by flow-policy  

  found: @Sink("ANY") @Source("ANY") byte @Sink("ANY") @Source("ANY") [] 

  forbidden flows:

    ANY -> ANY 

100 errors

Which is as expected I suppose since I didn't specify any annotations.

However, when I tried to get a bit of practice with Flow Policies (via your manual). I was directed to http://types.cs.washington.edu/sparta/tutorial/ContactManager for an example.

This website returned a 403 - Forbidden for me. Is there a way to access this example?

Thanks again for the great help,

Laurens Brinker

[Suzanne Millstein]

Hi Laurens,

I fixed the permissions on this link:

http://types.cs.washington.edu/sparta/tutorial/ContactManager.tgz

Thanks for reporting the problem!

-Suzanne

--

[laurens...@gmail.com]

Thanks!

I've tried to annotate my project but I got some issues:

For instance when I wanted to annotate the first flow:

/home/laptop/Documents/Bachelor-Scriptie/Irma-Application/irmaproxychecker/src/org/irmacard/androidcardproxy/ProtocolResponseSerializer.java:21: error: [forbidden.flow] 

JsonObject obj =  new JsonObject();

                 ^

  flow forbidden by flow-policy  

  found: @Sink("ANY") @Source("ANY") JsonObject 

  forbidden flows:

    ANY -> ANY 

I added the following annotation to see if something changed:

/*@Sink(ANY)*/JsonObject obj =  new JsonObject(); (In comments because I needed the 1.7 jdk for android).

However, when I run the checker I get the following error:

/home/laptop/Documents/Bachelor-Scriptie/Irma-Application/irmaproxychecker/src/org/irmacard/androidcardproxy/ProtocolResponseSerializer.java:24: error: cannot find symbol

/*@Sink(ANY)*/JsonObject obj =  new JsonObject();

  ^

  symbol:   class Sink

  location: class ProtocolResponseSerializer

My guess was that SPARTA is not working correctly (although it appeared to give a reasonable output).

So I tried ant all-tests in the sparta directory and I also got some errors there aswell:

.....

     [java] /home/laptop/Documents/Bachelor-Scriptie/sparta-sparta-1.0.2/tests/src/tests/AndroidTests.java:36: error: cannot find symbol

     [java]         Result run = jc.run(AndroidFenumCheckerTests.class);

     [java]         ^

     [java]   symbol:   class Result

     [java]   location: class AndroidTests

     [java] /home/laptop/Documents/Bachelor-Scriptie/sparta-sparta-1.0.2/tests/src/tests/AndroidTests.java:44: error: cannot find symbol

     [java]             for (Failure f : run.getFailures()) {

     [java]                  ^

     [java]   symbol:   class Failure

     [java]   location: class AndroidTests

     [java] 18 errors

Do you perhaps have a suggestion on what I should do next?

Thanks in advance,

Laurens Brinker

[Suzanne Millstein]

Hi Laurens,

/*@Sink(ANY)*/JsonObject obj =  new JsonObject(); (In comments because I needed the 1.7 jdk for android).

However, when I run the checker I get the following error:

/home/laptop/Documents/Bachelor-Scriptie/Irma-Application/irmaproxychecker/src/org/irmacard/androidcardproxy/ProtocolResponseSerializer.java:24: error: cannot find symbol

/*@Sink(ANY)*/JsonObject obj =  new JsonObject();

  ^

  symbol:   class Sink

  location: class ProtocolResponseSerializer

It looks like you did not import sparta.checkers.qual.Sink.  You'll probably want to write the import statement in comments, too. http://types.cs.washington.edu/checker-framework/current/checker-framework-manual.html#receivers-and-imports-in-comments

-Suzanne

[laurens...@gmail.com]

You're absolutely right, I needed to import Sink and Source (duh).

But after I've done this I have been experimenting with the tool.

Now I'm wondering what you recommend. Because first of all I cannot use ant infer so I have to annotate everything manually. Secondly, because the project I'm trying to analyse uses a lot of external APIs they are defaulted to @Sink(ANY) @Source(ANY), I based this on the manual: "Any method, constructor, or field not written in the stub files or found in source code is not defaulted normally. Instead, all locations except final fields are default to @Source(ANY) @Sink(ANY).", correct me if I'm wrong. And placing ANY->ANY as an allowed policy fixes a lot of warnings, but then again I'm pretty sure this is not the right way to do it. 

So again, what would you recommend doing when starting to analyse a gradle project from scratch (with a lot of APIs) ?

I greatly appreciate your excellent help so far, and I apologize if I misunderstood trivial things.

- Laurens Brinker