[Checkers] IGJ And Type Inference
mahmood at MIT.EDU
Wed Mar 19 15:26:41 EDT 2008
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
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
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:
Thanks. These is very helpful. I will look at it this weekend.
More information about the checkers