forwarded submission: Inference of static types

[John Plond JORGENSEN <jjorge1@cs.mcgill.ca>]

As list maintainer, I am just forwarding a submission to the
soot-list which was bounced because the sender is not (yet?) a
member.  Etienne -- who was CC'ed a personal copy of the message
-- has already copied his reply to the list.


From: "Lipsky, Nikita" <nlipsky@excelsior-usa.com>
To: "'soot-list@sable.mcgill.ca'" <soot-list@sable.mcgill.ca>
Cc: "'gagnon@sable.mcgill.ca'" <gagnon@sable.mcgill.ca>
Subject: Inference of static types
Date: Wed, 30 May 2001 19:42:57 +0700

> Hi there!
> 
> I have read carefully the paper "Efficient Inference of Static Types for
> Java Bytecode".
> 
> Would you be so kind to answer some related questions?
> 
> 1. What constraints will be added to the system for the cast or instanceof
> usage of a variable?
> 2. The same for the boolean equality operator?
> 3. If  there any constraints for "a = null" will be added?
> 
> Additionally, I probably found a defect in the algorithm:
> 
> Let us consider the next sample:
> 
> public class test {
> 
>   static boolean flag = true;
> 
>   public static void use(Integer i){};
> 
>   public static void main(String[] args) {
>     Object b;
>     if (flag){
>       b = null;
>       use(b);
>     }
>     else
>       b = new Boolean(true);
> 
>     System.out.println(b);
>   }
> }
> 
> It is not correct Java program, however the bytecode represented by this
> code is verifiable, according to Sun's specs. For instance, it may be
> trivially produced by a mean bytecode obfuscator.
> 
> In my mind, your algorithm infers Boolean type for variable b that is not
> correct static type in the case, indeed.
> 
> In fact, the constraint system for the method main has one soft node T(b)
> that has a child constraint to the Boolean hard node and two parent
> contraints to the Integer and Object hard nodes. Constraints system has no
> connected components and transitive constraints, so we fall into the
> single constraints phase. As can be seen, T(b) merges with the Boolean
> hard node by the merge of single child constraints rule and no additiobnal
> merges will occur since there is no single soft parent constraint in the
> system.
> 
> Thus, Stage 1 succeeds with type Boolean for variable b since the only
> soft node merges with the hard node Boolean.
> 
> Please, send me your comments on the counterexample, if possible.
> 
> May be I missed something,
> 
> With best regards,
> 
> Nikita Lipsky
> 
> Excelsior RND
> 
>