Svadev mailing list

[Daniel Huang <dan.e.huang AT gmail.com>]

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)

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?

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. 

Thanks in advance,

Dan