(WIP) Linear type checker

[renatoathaydes]

This is work in progress.

Please let me know if I am going in the correct direction. I found it very difficult to understand how the flow framework and the checker visitor work. This is my attempt so far.

I've been writing/testing this code in a separate repo because the build in this repo is impossible to use for development...

To run just the tests for my checker takes almost 30 seconds! It seems to recompile the whole thing even when I just change one class (or don't change anything at all).

Also, the tests are failing, even though in my own repo the (simialr) tests pass when I enable my checker. I can't see why that would be the case!

Finally, there's a git hook stopping me from committing due to code formatting issues.... I've used the default Java format that seems to be used in all other files in this repo... can you explain how I can re-format my code to pass the git hook? Running ant reformat doesn't work.

Thanks.

[renatoathaydes]

The test I am running in my project can be seen here and it passes.

[smillst]

If you merge typetools/master into your branch, the merge problem in the Travis test will go away. (Also, if you give us permission to push to your branch, we can fix trivial problems like this for you. See https://help.github.com/articles/allowing-changes-to-a-pull-request-branch-created-from-a-fork/#enabling-repository-maintainer-permissions-on-existing-pull-requests)

[mernst]

Can you be more specific than "Running ant reformat doesn't work."? We'd like to help you with that issue, but we don't have enough information to do so.

[renatoathaydes]

@mernst doesn't work as in doesn't exist in the checker-frameworks/checker ant build file. Can you give precise instructions on how to make it work to format a single file (that's what I was actually asking)?

@smillst I opted to not give access because the PR is not ready and I want to know exactly what the steps required for things to work are... so I don't depend on someone else to fix simple things.

[mernst]

Run ant reformat from the top level -- the checker-framework directory.

[mernst]

Or pull from master -- commit fbfe23f924686477ae5ce3ee315d2941482683d6 makes ant reformat work from the checker directory too.

[renatoathaydes]

@mernst thanks. Any comments on what my implementation is doing or on why the tests may be failing in the Checker test suite, but not in my separate project?

[renatoathaydes]

After rebasing my branch on master and running ant reformat, I see this:

➜  checker-framework git:(linear-type-checker) ✗ ant reformat
Buildfile: /home/renato/programming/projects/jsr308/checker-framework/build.xml

-run-google-java-format.check:

-get-run-google-java-format:

update-run-google-java-format:
     [exec] error: Your local changes to the following files would be overwritten by merge:
     [exec]     fixup-google-java-format.py
     [exec] Please, commit your changes or stash them before you can merge.
     [exec] Aborting
     [exec] Result: 1

reformat:

BUILD SUCCESSFUL
Total time: 19 seconds

The Python file is not modified in my repository... not sure if this worked or not :) it says SUCCESS but at the same time logs an error and says "aborting".

[mernst]

Thanks for the details. That makes it clear what is going on. What aborted is the update-run-google-java-format rule, but the remainder of the rules can run even if it fails. There is some local change in your repository. I suggest you delete that entire subrepository and the next time you run ant reformat, it will be re-cloned and all should be well. If the changes in your clone persist, you'll need to figure out what process on your compute is making the changes.

[renatoathaydes]

EDIT: sorry, I am writing as I try things!! So I will just start this message again to avoid wasting your time...

I was not expecting these errors:

Runner.java:5: error: [type.invalid.annotations.on.use] invalid type: annotations [@Unusable] conflict with declaration of type java.lang.String
    String t = s.toUpperCase(); // used up
           ^
Runner.java:7: error: [type.invalid.annotations.on.use] invalid type: annotations [@Unusable] conflict with declaration of type java.lang.String
    System.out.println(t);
                       ^
Runner.java:7: error: [use.unsafe] (use.unsafe)
    System.out.println(t);
                       ^

Full code used in this test:

import com.athaydes.checker.linear.qual.Linear;
public class Runner implements Runnable {
  public void run() {
    @Linear String s = \"hello @Linear\";
    String t = s.toUpperCase(); // used up
    System.out.println(s.toLowerCase()); // should fail here
    System.out.println(t);
  }
}

What's this annotation conflict about?

[renatoathaydes]

I have currently managed to allow literals and new Objects to be assigned to variables annotated with @Linear... but I am now stuck because of this error:

Runner.java:5: error: [type.invalid.annotations.on.use] invalid type: annotations [@Unusable] conflict with declaration of type java.lang.String
    String t = s.toUpperCase(); // used up
           ^

The code in question:

import com.athaydes.checker.linear.qual.Linear;
public class Runner implements Runnable {
  public void run() {
    @Linear String s = \"hello @Linear\";
    String t = s.toUpperCase(); // used up
    System.out.println(t);
  }
}

I removed my transfer function, so currently all my code is doing is replacing the annotation of anything being assigned to a @Linear variable with the @Linear annotation, so it allows compilation of such cases (which it doesn't if I don't replace the annotation)...

Could you help me understand why the framework thinks there's a conflict and where the @Unsable annotation is coming from, given I never mentioned it in any code (and I have not modified any of the annotations definitions)?

[renatoathaydes]

By debugging, I found out that the defaults seem wrong for my annotations.

This is the value of QualifierDefaults#toString() on the LinearAnnotatedTypeFactory.defaults variable:

Checked code defaults: 
( LOCAL_VARIABLE => @com.athaydes.checker.linear.qual.Unusable )
( RESOURCE_VARIABLE => @com.athaydes.checker.linear.qual.Unusable )
( EXCEPTION_PARAMETER => @com.athaydes.checker.linear.qual.Unusable )
( LOWER_BOUND => @com.athaydes.checker.linear.qual.Linear )
( IMPLICIT_LOWER_BOUND => @com.athaydes.checker.linear.qual.Linear )
( IMPLICIT_UPPER_BOUND => @com.athaydes.checker.linear.qual.Unusable )
( OTHERWISE => @com.athaydes.checker.linear.qual.Normal )
Unchecked code defaults: 
( FIELD => @com.athaydes.checker.linear.qual.Unusable )
( PARAMETER => @com.athaydes.checker.linear.qual.Linear )
( RETURN => @com.athaydes.checker.linear.qual.Unusable )
( LOWER_BOUND => @com.athaydes.checker.linear.qual.Linear )
( UPPER_BOUND => @com.athaydes.checker.linear.qual.Unusable )
useUncheckedCodeDefaultsSource: false
useUncheckedCodeDefaultsBytecode: false

So, I added @DefaultFor({TypeUseLocation.LOCAL_VARIABLE}) on @Normal, then the code worked!

The question now is: why was it using @Unusable as a default? In @Normal there was already the @DefaultQualifierInHierarchy annotation! What's the appropriate thing to do? Add several @DefaultFor on @Normal for all use-locations I think it's appropriate (probably all of them)?

[smillst]

@DefaultQualifierInHierarachy applies everywhere except CLIMB locations. The CLIMB rules can be overriden using @DefaultFor.

[smillst]

I'm closing this pull request since we decided that the current Linear Checker hierarchy makes it impossible to use the dataflow framework.