Svadev mailing list

[John Criswell <criswell AT illinois.edu>]

On 3/3/13 1:45 PM, Daniel Huang wrote:

Hi svadev,

In the case that DSA infers multiple types at the same offset and the node is not marked as unknown, what is the invariant that SAFECode enforces when it generates code? For example, I've observed code that produces the following pool allocation.

PoolForMain9: (no inferred types, not marked as unknown, not marked as completely folded)

PoolForMain: i32* (and points into PoolForMain9)

PoolForMain8: i32* | i32** (not marked as unknown, not marked as completely folded, and points into PoolForMain)

It would help if you gave me the C source code, LLVM IR, and the DSGraphs for your sample programs when you have a question.  Your notation is not what I'm used to reading, and I'm not sure if I'm interpreting your notation correctly.

I think what you're saying above is that you have a memory object (PoolForMain9) which holds i32's, another memory object that contains an i32* (PoolForMain), and a final memory object (PoolForMain8) into which the program stores both an i32* to the objects in PoolForMain9 and an i32** to objects in PoolForMain.  Is this correct?

Annotating fully with types,

PoolForMain9 : (no inferred types, not marked as unknown, not marked as completely folded)

PoolForMain : i32*PoolForMain9

PoolForMain8 : i32*PoolForMain | i32*PoolForMain9*PoolForMain

If I have a pointer into region PoolForMain8, what does a poolcheck on that pointer guarantee? Does it guarantee a pointer into PoolForMain at the first type, the second type, or an unknown type?

Assuming my understanding of the previous notation is correct, then something looks amiss.  DSA should be merging pointers at the same offset in a DSNode into a single DSNode (i.e., PoolForMain and PoolForMain9 should be the same pool represented by a single folded DSNode).

As an aside, I find it weird that PoolForMain9 has no inferred types since I would have expected PoolForMain to constrain what type it holds. Furthermore, I would have expected PoolForMain to constrain what types could be in PoolForMain8.

I think I really need to see the LLVM IR and/or C source code to understand what is going on.  Either you've hit a DSA bug, or I am not understanding your notation.

Without seeing the LLVM IR and/or C source code, it is difficult to know what I would expect you to see in the analysis results.

-- John T.

Thanks in advance,

Dan

_______________________________________________
svadev mailing list
svadev AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/svadev