[Checkers] IGJ And Type Inference

[Mahmood Ali]

Hi Jaime,

Thanks to the clarification. This is quite helpful. Let me clarify  
some points and get your input on this.

>> 1. I believe that any type inference tool need to work on both:  
>> source and bytecode.  [...] The source is essential for users to  
>> annotate their own (potentially partially annotated) code, [...]
> So, the fact that some code will be partially annotated does not  
> affect whether or not to make a source- or bytecode-based inference  
> tool [...] As for inserting annotations back into source code,  
> that's one of the selling points of the annotation file format; it  
> is a simple format for storing annotations that can then be inserted  
> into the source or bytecode.  If the tool outputs an annotation  
> file, it leaves this decision up to the user.

Yes, I didn't mean that supporting partially annotated code would  
require either approach. However, I was highlighting the two uses of  
any type inference system and claiming that they require some what  
different user experience:
1. bytecode support:
- binary libraries are usually either fully annotated or not.  It's  
useless for a vendor to distribute a partially annotated binary.
- Users simply want to use the type inference tool for binary files  
just so that their own code compiles properly.  Personally, I will not  
debug the output of the inference tool for such system unless they  
impact my own code annotation in unexpected ways.
- It is OK for to simply output the annotation in a different index  
file.  As long as my code compiles and it's a matter of an extra  
argument for compiling, I wouldn't care about how the annotations are  
represented.

2. Source support:
- It is usually partially annotated.
- I expect the use to interact with the type inference within an IDE.
- Requires support of iterative process.  Command-line commands aren't  
quite good in this.
- Annotations should really go into the source directly and not a  
separate index file.  It's OK to have the index file as an  
intermediate representation and automate the process of insertion to  
source.  As a user of the tool, I wouldn't like to spend time simply  
copying annotations to the source.  I would like to see the  
annotations on code mainly for the next modules, and it's couter- 
productive to consult the seperate index file everytime I develop new  
code.

If the annotation file format allows for insertion into the source  
directly. That's great. Otherwise, I wouldn't use it.


>> 2. I believe that it is highly desirable (yet not quite important)  
>> that the type inference tool does not load the classes.
> What do you mean by 'load' exactly?
I mean that it wouldn't call ClassLoader.loadClass().  This is not a  
memory requirement, but I think that it's desirable, but not necessary  
*required*, to be able to annotate a class that the JVM depends on  
(e.g. java.util.Stack, java.lang.Object), or a class that requires jni  
native linking without getting UnsatisfiedLinkError.

That excludes using the javac compiler and the checker framework.  I  
assume that Soot doesn't do that.

> I think what you're describing is a general framework for qualifier  
> inference.   This generality makes the JQual paper difficult to read  
> if you want to understand the fine details of inferring readonly,  
> along with the fact that you need context-sensitivity and field- 
> sensitivity to get good results.  You may actually want to start by  
> reading the Javarifier ECOOP paper, which describes a constraint- 
> based system that infers Javari readonly qualifiers.  (Also, any  
> feedback you give me would be helpful in finishing the final version  
> of that paper.)   I've put a pdf at:
>
> http://people.csail.mit.edu/jaimeq/javarifier-ecoop.pdf
Thanks.  These is very helpful.  I will look at it this weekend.

Regards,
Mahmood