[Checkers] Thoughts on Type Inference: Part 2

[Michael Ernst]

Mahmood-

Is this the email with the inference algorithm design, or was there another
one?  Did you ever write this up in more detail as mentioned at the end of
the email?

I not sure, for example, how you plan to determine aliasing relationships
(any remaining references that could point to this one).  You actually
don't want a too accurate analysis, since that would result in application
invariants that would not be checkable by the type system.  The
determination needs to use similar rules to what the checker will later use
when verifying the inferred types.

                    -Mike


> From: Mahmood Ali <mahmood at MIT.EDU>
> Sender: checkers-bounces at lists.csail.mit.edu
> To: checkers at lists.csail.mit.edu
> Subject: [Checkers] Thoughts on Type Inference: Part 2
> Date: Thu, 11 Sep 2008 01:02:04 -0400
> 
> Greetings again,
> 
> This email would touch on the type inference algorithm itself for IGJ  
> and how we can refractor it to make a more generic type inference.
> 
> __ IGJ specific core algorithm __
> We do it in three stages:
> 1. Analysis to infer mutability, which is identical to Javari.  Find  
> references that need to be mutable, and propagate their mutability to  
> any Object/reference that the reference could refer to.
> 2. If a reference is known to be a mutable reference, then all  
> remaining references that could point to this reference must be read- 
> onlys (i.e. cannot be immutable).
> 3. All remaining references are immutable!
> 
> Unfortunately, this is very IGJ specific algorithm and not very  
> extensible.
> 
> __ More generic algorithm __
> For any type system, we can generate constraints for a reference based  
> on the values it refers to and potential method invocation.   
> Basically, we simply reverse the rules used for type checking:
> 1. For any assignment (or pseudo-assignment) 'a = b', 'a' type needs  
> to be a supertype of 'b'.
> 2. For any method invocation (another form of pseudo-assignment),  
> 'a.m()', 'a' type needs to be a subtype of 'm()' receiver.
> 3. needs to inverse some other rules (e.g. field re-assignment in IGJ,  
> de-referncing for nullness).
> 
> The qualifier on a reference 'a' type is the supertype of all  
> qualifiers of the types of values it 'a' could potentially refer to  
> and a subtype of qualifiers on receivers of the methods that could  
> potentially be invoked on 'a'.  This should be sufficient for finding  
> all mutable references and read only references.  Any remaining  
> references can be marked as Immutable, in IGJ.  (I may need to  
> elaborate on this point).
> 
> __ Error in code __
> Javari algorithm and most type inference algorithms assumes that the  
> code is valid code.  Unfortunately, this is an unreasonable  
> assumptions for some type systems.
> 
> It is known, for example, that Java code are full of null pointer  
> errors.  We cannot infer nullness property properly if the code is  
> invalid.  Other type systems (maybe IGJ and Javari) may not have this  
> problem.
> 
> The second more generic approach could easily find such errors, as  
> they would result in a contradiction in the bounds of the reference.
> 
> OK... Need to sleep now.  I will write a document later about this.
> 
> Regards,
> Mahmood
> 
> 
> _______________________________________________
> checkers mailing list
> checkers at lists.csail.mit.edu
> https://lists.csail.mit.edu/mailman/listinfo/checkers