Re: Inference of static types

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

"Lipsky, Nikita" wrote:
> > a = (Type) b;
> >
> > This implies the 2 constraints:
> >
> > T(b) >= Type
> > T(a) <= Type
> >
> Thank you very much for your answers. It was not clear from the paper.

Many details are not explained in the paper.  There was no space to
explain them all.  That's why we provide an open implementation;-)

> You missed T(b)>=Object hear. So we have:
> 
>         Integer <= T(b) <= Boolean
>      Object  <=       <=T(null)
> 
> So stage 1 will infer Boolean type as I mentioned in the previous letter.

NO, it will NOT!!!  Stage 1 will ***FAIL***.  Please use a debugger, or
any tool you like, and simply trace Soot's typing algorithm, and you'll
see.  Or if you insist, simply take a pencil, and draw little nodes and
directed edges and apply the algorithm.  You'll see that stage 1 fails. 
Here's a simplified view:

[1] T(b) <= Boolean
[2] T(b) <= T(null)
[3] Integer <= T(b)
[4] Object  <= T(b)

The removal of transitive constraints eliminates [2] and [4].  So we are
left with [1] and [3].

Now, when merging T(b) with Boolean, the algorithm checks the newly
combined constraints (i.e. directed edges) of the node [T(b)/Boolean]
(which is a hard node) and detects that constraint [3] is violated. 
This causes immediate abortion of stage1 (failure).

> > So, T(b) is assigned Boolean.
> This is exactly what I thought. No matter in what stage we get this result,
> :).

Yes, it does matter (at least to me).

> >
> > use((Integer) b)
> >
> Cast of Boolean to Integer is illegal in Java. So Boolean type for b
> variable is NOT correct. The only correct type is Object. Am I wrong?

Ah!  But this one is simple to solve, and should be done at the
"decompiler" level.  This problem is similar with primitive types, as
the type inference algorithm can do things like:

int i;
boolean b;

i = (int) b;
/* and */
b = (boolean) i;

So, the solution is...
...
...
;-)


i = b ? 1 : 0;
b = (i != 0);
use((Integer) (Object) b)

So, in other words, the algorithm works well.  You just have to
carefully handle Jimple type casts if you want to go back to Java source
code.

I admit that I had not really thought of the specific case of "illegal"
Java casting for reference types. (I was aware of the primitive type
one).

Have fun!

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/