[Soot-list] Paddle

[Ondrej Lhotak]

Thank you for the very detailed bug report.

The problem was caused by a silly bug in the code that presents the
BDD-based results using the old Soot interface. I've fixed it in
the Paddle Subversion repository, and the fix should show up in the
nightly build tomorrow morning.

With the fix, your analysis produces the following output, which is
still not what you were expecting:
[4,4]    Container.item intersect? true
[4,8]    Container.item intersect? true
[4,12]   Container.item intersect? true
[8,8]    Container.item intersect? true
[8,12]   Container.item intersect? true
[12,12]  Container.item intersect? true

The reason for this is the line
        private Item item = new Item();
in Container. This line assigns the same (abstract) Item to all
the containers. One way to fix this is to replace the line with
        private Item item;
Then the analysis returns false for [4,8] and [4,12] as you expect.
Another way to fix this is to run Paddle using a context-sensitive
heap abstraction (option context-heap:true). This allows Paddle to
distinguish the different Items assigned to the different Containers.

Ondrej


On Tue, Apr 25, 2006 at 03:46:36PM +0200, Janus Dam Nielsen wrote:
>    Hi,
> 
>    I am looking into Paddle and managed to get an example based on Figure
>    4.4 in http://plg.uwaterloo.ca/~olhotak/pubs/thesis-olhotak-phd.ps up
>    and running using BDD and it gives the expected points-to sets for the
>    local variables but for the fields of the Container class I don't get
>    the expected results when running Paddle in context-sensitive mode -
>    and I can't find the bug, hope some of you can help me.
> 
>    Background:
> 
>    I have the two classes Container and Item, and I have the go
>    method. I want to analyze the go method using Paddle.
> 
>    public class Container {
>        private Item item = new Item();
>        void setItem(Item item) {
>            this.item = item;
>        }
>        Item getItem() {
>            return this.item;
>        }
>    }
> 
>    public class Item {
>        Object data;
>    }
> 
>    public void go() {
>    (4)Container c1 = new Container();
>        Item i1 = new Item();
>        c1.setItem(i1);
>           
>    (8)Container c2 = new Container();
>        Item i2 = new Item();
>        c2.setItem(i2);   
>           
>    (12)Container c3 = c2;
>    }
> 
>    I would expect Paddle to discover the following:
>    - The points-to set of c1 and c1 are intersecting.
>    - The points-to set of c1 and c2 are non-intersecting.
>    - The points-to set of c1 and c3 are non-intersecting.
>    - The points-to set of c2 and c2 are intersecting.
>    - The points-to set of c2 and c3 are intersecting.
>    - The points-to set of c3 and c3 are intersecting.
> 
>    - The points-to set of c1.item and c1.item are intersecting.
>    - The points-to set of c1.item and c2.item are non-intersecting.
>    - The points-to set of c1.item and c3.item are non-intersecting.
>    - The points-to set of c2.item and c2.item are intersecting.
>    - The points-to set of c2.item and c3.item are intersecting.
>    - The points-to set of c3.item and c3.item are intersecting.
> 
>    Running Paddle with the following options:
>    HashMap opt = new HashMap();
>    opt.put("enabled","true");
>    opt.put("verbose","true");
>    opt.put("bdd","true");
>    opt.put("backend","buddy");
>    opt.put("context","1cfa");
>    opt.put("k","1");
>    opt.put("propagator","auto");
>    opt.put("conf","ofcg");
>    opt.put("order","32");
>    opt.put("q","auto");
>    opt.put("set-impl","double");
>    opt.put("double-set-old","hybrid");
>    opt.put("double-set-new","hybrid");
>    opt.put("pre-jimplify","false");
> 
>    PaddleTransformer pt = new PaddleTransformer();
>    PaddleOptions paddle_opt = new PaddleOptions(opt);
>    pt.setup(paddle_opt);
>    pt.solve(paddle_opt);
>    soot.jimple.paddle.Results.v().makeStandardSootResults();   
> 
>    Reveals the following information:
> 
>    [4,4]     Container intersect? true
>    [4,8]     Container intersect? false
>    [4,12]     Container intersect? false
>    [8,8]     Container intersect? true
>    [8,12]     Container intersect? true
>    [12,12]     Container intersect? true
>    As expected.
> 
>    But the flowing output puzzles me:
>    [4,4]     Container.item intersect? false
>    [4,8]     Container.item intersect? false
>    [4,12]     Container.item intersect? false
>    [8,8]     Container.item intersect? false
>    [8,12]     Container.item intersect? false
>    [12,12]     Container.item intersect? false
> 
>    Nothing seems like it should be. The fields does not intersect with
>    them selves. The fields of the containers declared at line 8 and 12
>    does not intersect as expected! Where is the bug?
> 
>    I am running a nightly build of Paddle about a month old along with
>    Soot-2.2.2, Jasmin-2.2.2, Polyglot-1.3.2, and Jedd version 0.3(October
>    2005).
> 
>    If you want to have a look at the source code you can download a tar-ball
>    with the source of the example including a Makefile for compiling and
>    running the example can be found at:
>    http://www.daimi.au.dk/~fagidiot/soot/paddleproblem.tar.gz
> 
>    Kind regards
>    Janus Dam Nielsen

> _______________________________________________
> Soot-list mailing list
> Soot-list at sable.mcgill.ca
> http://mailman.cs.mcgill.ca/mailman/listinfo/soot-list