Type validation through validateTypeOf

[GoogleCodeExporter]

The validation checks on declared return types do not appear to be working.  

For example:
    @Tainted @Untainted ExtendsAndAnnotation testMethod(){return null;}

Produces:

error: Found exception during TypeHierarchy.isSubtype of null and @Tainted 
@Untainted ExtendsAndAnnotation; invoke the compiler with -AprintErrorStack to 
see the stack trace.

But it should produce an type.invalid error. 

Or in the Flow Checker:

@Source(READ_SMS) @Sink({})  ExtendsAndAnnotation testMethod(){return null;}

No longer produces a forbidden flow warning. 

The call to validateTypeOf(ret) shown below does not issue a warning, because 
atypeFactory.getAnnotatedType(ret) does not return the explicitly written 
annotations.

// (BaseTypeVisitor, line ~401)
            Tree ret = node.getReturnType();
            if (ret != null &&
                    methodType.getReturnType().getKind() != TypeKind.VOID) {
                validateTypeOf(ret);
            }

Before revision e9436f0fc57e, this check was implemented using the 
typeValidator, which did produce the invalid type and forbidden flow warnings. 

typeValidator.visit(methodType.getReturnType(), node.getReturnType());

Original issue reported on code.google.com by smil...@cs.washington.edu on 18 Dec 2013 at 12:26

[GoogleCodeExporter]

Note that validateTypeOf calls the typeValidator and performs more checks.

The problem is that the node.getReturnType does not contain the type 
annotations in the tree.
I will refactor validateTypeOf, either optionally or always taking the type as 
extra argument.

You could address the note in 
checker-framework/checkers/tests/tainting/ExtendsAndAnnotation.java
and produce an invalid type in every possible syntactic location - including in 
a method return.

Original comment by wdi...@gmail.com on 18 Dec 2013 at 12:39

• Changed state: Accepted

[GoogleCodeExporter]

I've separated out test case checkers/tests/tainting/TypeInvalid.java.
It performs the correct tests for method return types and fields now.
Please do let me know if this solved this issue for you. Feel free to expand 
the TypeInvalid.java test case for any locations not yet covered.

Original comment by wdi...@gmail.com on 18 Dec 2013 at 3:50

• Changed title: Type validation through validateTypeOf
• Changed state: Pushed

[GoogleCodeExporter]

Thanks!  That fixed the problem.  

What is this code validating if ret.getReturnType() does not have annotations?  
(I just want to make sure I understand your changes.)
         Tree ret = node.getReturnType();
            if (ret != null &&
                    methodType.getReturnType().getKind() != TypeKind.VOID) {
                validateTypeOf(ret);
            } 

Original comment by smil...@cs.washington.edu on 18 Dec 2013 at 5:11

[GoogleCodeExporter]

Great catch! It didn't do anything, exactly because the annotations weren't in 
that tree. The reason the test passed was that in the return statement I also 
have to validate the return type.
I now fixed this to work for abstract methods that don't have a return 
statement and check constructor returns.
Please feel free to add more tests to tainting/TypeInvalid.java.

Original comment by wdi...@gmail.com on 18 Dec 2013 at 7:25

[GoogleCodeExporter]

Original comment by Jonathan...@gmail.com on 6 Jan 2014 at 6:53

• Changed state: Fixed