Re: Inference of static types

["Etienne M. Gagnon" <egagnon@j-meg.com>]

"Lipsky, Nikita" wrote:
> > 1. What constraints will be added to the system for the cast or instanceof
> > usage of a variable?

a = (Type) b;

This implies the 2 constraints:

T(b) >= Type 
T(a) <= Type

> > 2. The same for the boolean equality operator?

Equality operator is a little tricky, specially when you want to handle
primitive types.

For the details, please look at Soot's source code. [file:
soot-1.2.2/soot/src/soot/jimple/toolkits/typing/ConstraintCollector.java]

The basic idea when you compare variables of reference type, is that
they should be comparable, or in other words, have a common ancestor
type.

if (a == b)...

implies

[new type variable X]
T(a) <= X
T(b) <= X

> > 3. If  there any constraints for "a = null" will be added?

Yes.  There is a special type (called "NullType" within Soot) that
represents the type of "null".  This type is a subtype of all reference
types. In other words: T(null) <= any reference type

So:

a = null;

implies:

a <= T(null)


> > Additionally, I probably found a defect in the algorithm:

There's no defect.  Let's look.

> >   public static void main(String[] args) {
> >     Object b;
> >     if (flag){
> >       b = null;

T(b) <= T(null)

> >       use(b);

T(b) >= Integer

> >     }
> >     else
> >       b = new Boolean(true);

T(b) <= Boolean

> >
> >     System.out.println(b);
> >   }
> > }


Now, if you combine all these constraints you get:

Integer <= T(b) <= Boolean

Which is not possible because:

Integer not<= Boolean

So, the typing algorithm resorts to step 2, which does nothing in this
case. (Read the paper for details)

Finally, step 3 is applies.  In a few words, step 3 ignores "use"
constraints.  So, above, it ignores the "T(b) >= Integer" constraint. 
The system becomes:

T(b) <= Boolean
T(b) <= T(null)

Which simplifies to:
T(b) <= Boolean

So, T(b) is assigned Boolean.  Then "use" contraints are checked, and
type casts are added if necessary.  Which would lead to:

use((Integer) b)

But, as Soot has simple statement, we need to add a new variable to do
the cast:

temp = (Integer) b;
use (temp);

Which explains Soot's output.

Etienne
-- 
----------------------------------------------------------------------
Etienne M. Gagnon, M.Sc.                     e-mail: egagnon@j-meg.com
Author of SableCC:                             http://www.sablecc.org/
and SableVM:                                   http://www.sablevm.org/