search

typetools / checker-framework

Pluggable type-checking for Java
http://checkerframework.org/
Other
990 stars 347 forks source link

Flow refinement is ignored when initializing the store for inner classes #266

Closed GoogleCodeExporter closed 5 years ago

GoogleCodeExporter commented 8 years ago

List of test cases: checker/tests/nullness/FinalVar2.java checker/tests/nullness/Issue411.java checker/tests/nullness/Issue811java checker/tests/nullness/Issue266.java checker/tests/nullness/Issue266a.java

# What steps will reproduce the problem?

Run the nullness checker on the attached file.

# What is the expected output? What do you see instead?

I expected the nullness checker to recognize that the deference of 'tmp' in the 
inner class will always succeed. Instead, I got the error:

FinalNullable.java:16: error: dereference of possibly-null reference tmp
        return tmp.toString();
               ^

#What version of the product are you using? On what operating system?

javac 1.8.0-jsr308-1.6.7 (7102:18502dce6db5)

Original issue reported on code.google.com by cus...@google.com on 16 Oct 2013 at 4:45

Attachments:

GoogleCodeExporter commented 8 years ago 
The Checker Framework currently does type refinement on a final variable based 
on the initializer expression, but not based on subsequent conditional 
expressions.

I have committed a test case as 
checker-framework/checkers/tests/nullness/FinalVar2.java

Original comment by michael.ernst@gmail.com on 16 Oct 2013 at 9:59

GoogleCodeExporter commented 8 years ago 
I find comment #1 misleading.
The following example:

  static Object method1(@Nullable Object arg) {
    final Object tmp = arg;
    if (tmp == null) {
      return "hello";
    }
    tmp.hashCode();
    return "bye";
  }

passes the Nullness Checker without an error.

I think we correctly type refine the final variable in the outer class, but 
when we initialize the store for the anonymous inner class, we only use the 
declared types of the final variables. We should take the refined values of the 
final variables at the point where the anonymous class is instantiated.

Stefan recently worked on anonymous inner classes, maybe he can have a quick 
look.

Original comment by wdi...@gmail.com on 17 Oct 2013 at 3:23

GoogleCodeExporter commented 8 years ago 
We do remember the refined value of final variables and use it to initialize 
the store in the anonymous inner class.  However, the refinement is only based 
on the initializer of the final variable;  future refinements based on 
comparing the final variable with other values are not used.  This has the 
advantage, that only a single value per final variable needs to be remembered, 
rather than (potentially) a value for every program point.

I'm sure it would be possible to remember more information, but it also does 
not seem like a high-priority issue.  It can easily be worked around by doing 
the check what value the final variable holds earlier.  For the example given, 
one could change it as follows:

    if (arg == null) {
      return null;
    }
    final Object tmp = arg;
    return new Inner() {
      String getThing() {
        return tmp.toString();
      }
    };

I changed the priority to low for now.

Original comment by stefanheule@gmail.com on 17 Oct 2013 at 5:16

GoogleCodeExporter commented 8 years ago

Original comment by michael.ernst@gmail.com on 25 May 2014 at 4:25

GoogleCodeExporter commented 8 years ago

Original comment by michael.ernst@gmail.com on 29 May 2014 at 4:04

GoogleCodeExporter commented 8 years ago 
Issue 411 has been merged into this issue.

Original comment by wdi...@gmail.com on 16 Mar 2015 at 8:54

GoogleCodeExporter commented 8 years ago 
Issue 411 has been merged into this issue.

Original comment by wdi...@gmail.com on 16 Mar 2015 at 8:54

scottkennedy commented 8 years ago

While the workaround seems reasonable, it would be nice to not require to change valid code to meet the requirements of a static analysis tool.

smillst commented 7 years ago

This issue was reported by another user in #811.

smillst commented 7 years ago

I added a test case checker/tests/nullness/Issue811java.

wmdietl commented 7 years ago

org.checkerframework.dataflow.cfg.CFGBuilder.CFGTranslationPhaseOne.visitNewClass(NewClassTree, Void) contains the comment "We ignore any class body because its methods should be visited separately.". This is likely the location where the current store should be propagated to that anonymous class.

Handling of inner/anonymous classes probably needs a solution similar to how lambda expressions are handled. Note how rewriting an anonymous class to an equivalent lambda expression gives the correct refinement behavior. See

mh-dm commented 7 years ago

Is there a cleaner annotation based workaround rather the local variable copy? (I'm thinking something like @MonotonicNonNull - although this one specifically doesn't work).

wmdietl commented 7 years ago

I don't think an approach with an annotation on the field is possible. Annotating the field would not help you with determining whether the type was refined or not. Flow-sensitivity needs to be implemented correctly, which is a considerable engineering effort. I wrote up a few comments last week, but won't get to work on this for a while.

mh-dm commented 7 years ago

Issue #903 was closed as a dupe of this. Given that, can you add the following as a test when fixing this issue? Thanks!

class Foo {
  private final Object mBar;

  public Foo() {
    mBar = "test";
    Runnable runnable = new Runnable() {
        @Override
        public void run() {
          // unexpected [dereference.of.nullable] error here
          mBar.toString();
        }
      };
    runnable.run();
  }
}
mernst commented 7 years ago

Thanks for the test case. In commit ce3465d, I have added two test cases as files checker/tests/nullness/Issue266.java and checker/tests/nullness/Issue266a.java.

wmdietl commented 5 years ago

Fixed by https://github.com/typetools/checker-framework/commit/c74edd7884c7682f37ad49db401de84458023c66