Linear checker doesn't work for nested data structures

[hun10]

Linear checker passes the following code.

static void proc(@Linear String[] oo) {
    @Linear String[] a1 = oo;
    @Linear String[] a2 = oo;
}

But it should raise an error according to the manual.

I suspect this has something to do with https://github.com/typetools/checker-framework/commit/88723e6a2b68d0ecfca2c11f94ca20c099b056db stating that linear checker should be rewritten to the "new flow framework"

[renatoathaydes]

Hi! I was hoping to use @Linear annotations in my code but it seems that most of the errors are not being caught correctly, so it's not helping at all.

I would be happy to contribute implementing this better. Can you give some pointers? What is this "new flow framework" that is mentioned by the OP?

[wmdietl]

Updating the Linear Checker would be a very welcome contribution!

I would first read through https://checkerframework.org/manual/#creating-a-checker (Please also give feedback on this! It's always good to hear from somebody who goes through these instructions for the first time.)

Then, think through what the type rules should actually be and review the existing code. Once you're clear on the right semantics, see what changes you need. I'm not sure whether better dataflow is needed for nested data structures or whether something else is wrong with the current implementation.

The "new flow framework" is at https://github.com/typetools/checker-framework/tree/master/dataflow which is a general dataflow framework for Java source code. It is adapted for our type system usage in https://github.com/typetools/checker-framework/tree/master/framework/src/org/checkerframework/framework/flow and then used by the different type systems. A type system might need to customize the transfer functions, e.g. see https://github.com/typetools/checker-framework/blob/master/checker/src/org/checkerframework/checker/regex/RegexTransfer.java Some type system might also require custom Store abstractions, e.g. see https://github.com/typetools/checker-framework/blob/master/checker/src/org/checkerframework/checker/nullness/NullnessStore.java

Please let us know how things go and if you want to discuss anything.

[renatoathaydes]

@wmdietl just finished following the instructions to build checker from source. This is a beast of a build! Looks like you need to do some cleanup, perhaps use Gradle instead of Maven+Ant+shell scripts :)

I will spend some time to get familiar with the code base, but from what I can see there's no tests for @Linear?! I found test for many checkers, but not from this one...

I think the tests should be at jsr308/checker-framework/checker/tests, right?

Should I create an implementation of CheckerFrameworkPerDirectoryTest and create a linear directory under jsr308/checker-framework/checker/tests?

[mernst]

@renatoathaydes We agree that it would be good to switch the build to gradle. This is a big task. Help is always welcome. :-)

You are right that there are no tests for the linear type-checker. Creating tests for it would be very useful and we would happily accept them.

(Background: We were asked to build it by a Google engineer with a PhD in programming languages, and then after building and demoing it the Google engineer said, "Oh, yeah, that's what linear means. That isn't actually what I want, though." So we moved on to other work and haven't done a lot of development on the linear type system since then.)

[renatoathaydes]

haha. typical. I will try to focus on the linear type checker for now... if it works out well, i might get more involved with the build and the tests... I wonder if using an in-memory Java compiler like this one that I wrote would make these tests faster and more straightforward to write?! I might try that and see if it's helpful.

[mernst]

Working on the Linear Checker sounds great. Thanks!

Your in-memory Java compiler sounds extremely useful. It can't help but make the tests faster, which would be great. A project that is even more compile-time-bound is Randoop, and that is another place that your in-memory compiler could make a big impact.

[wmdietl]

I found issue #13 which was marked as closed... looks like for the Linear Checker no tests were actually added.

You would start by copying one of the existing test drivers, e.g. https://github.com/typetools/checker-framework/blob/master/checker/tests/src/tests/InterningTest.java and then adding test files in checker/tests/linear.

Having the in-memory compiler could speed up test execution further. The switch to CheckerFrameworkPerDirectoryTest already improved performance by compiling all files in a directory at once, instead of invoking the compiler separately for each file. I don't think it would have an effect on how we write tests though.

Thanks for looking into the Linear Checker!

[renatoathaydes]

Cool.

I will start by writing tests in my own separate project, then try to integrate with the existing code.

It's much more convenient for me to do it like that.

Here's a test to demonstrate the in-memory compiler:

public class LinearTypeCheckerTest {

    @Test
    public void canCompileGoodClass() throws IllegalAccessException, InstantiationException {
        OsgiaasJavaCompiler compiler = new OsgiaasJavaCompiler( DefaultClassLoaderContext.INSTANCE );

        Optional<Class<Object>> runner = compiler.compile( "Runner", "public class Runner implements Runnable {" +
                "  public void run() {" +
                "    System.out.println(\"hello world\");" +
                "  }" +
                "}", System.out );

        runner.orElseThrow( () -> new RuntimeException( "Error compiling" ) )
                .asSubclass( Runnable.class )
                .newInstance()
                .run();
    }

    @Test
    public void cannotCompileBadClass() {
        OsgiaasJavaCompiler compiler = new OsgiaasJavaCompiler( DefaultClassLoaderContext.INSTANCE );

        ByteArrayOutputStream writer = new ByteArrayOutputStream();

        Optional<Class<Object>> compiledClass = compiler.compile( "Runner", "public class Runner implements Runnable {" +
                "  public void run() {" +
                "    System.out" +
                "  }" +
                "}", new PrintStream( writer, true ) );

        assertFalse( compiledClass.isPresent() );
        assertThat( writer.toString(), CoreMatchers.containsString( "error: ';' expected" ) );
    }
}

This runs in 0.275 seconds on my machine. Most of the time is actually on the JVM getting warm, so I think a large amount of tests should still run in under one second (not sure about that after adding the type checker, of course, will see).