Svadev mailing list

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

Hi John,

Thanks for the quick response. I've attached the source code, the emitted code, and the results of the pool pass. I interpret the notation as:

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

PoolForMain : i32*PoolForMain9

PoolForMain8 : i32*PoolForMain | i32*PoolForMain9*PoolForMain

1) PoolForMain9 is a pool that holds objects of unknown type (although I don't know why it is not marked as unknown).

2) PoolForMain is a pool that holds i32* pointers. In particular, the pointers point into region PoolForMain9, or fully annotated as i32*PoolForMain9.

3) PoolForMain8 is a pool that holds i32* or i32** pointers. In particular, the pointers point into region PoolForMain. Thus, if I currently have an i32* pointer, then it is fully annotated as a i32*PoolForMain pointer. If I currently have an i32** pointer, then i have a (i32*PoolForMain9)*PoolForMain fully annotated pointer, because one dereference lands me in PoolForMain, and the next dereference lands me in PoolForMain9. 

I was under the impression that pools were type-homogenous and in the case that they were not, would be put in unknown pools. Hence, the pool-allocation of PoolForMain8 seems to violate type-homogeneity. If the SAFECode compiler produces typed-pools that can have multiple types, it also makes me wonder what invariant SAFECode actually maintains. For example, if I read out of PoolForMain (via a pointer read out of PoolForMain8), I must always check what I got to be able to use it as a pointer into PoolForMain9 since it may be an i32. In a type-homogenous setting, that check can be optimized away. Also in this example, it seems that if the DSgraph were consistent with itself, the resulting pool-allocation would be:

PoolForMain9 : i32

PoolForMain : i32*PoolForMain9

PoolForMain8 : i32*PoolForMain9*PoolForMain

Apologies for the bombardment of questions, but because the implementation has continued to improve/change since the original paper, there is a huge gap in my knowledge of how SAFECode actually works. 

Regards,

Dan

On Mon, Mar 4, 2013 at 5:18 PM, John Criswell <criswell AT illinois.edu> wrote:

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

#include <assert.h>
#include <stdlib.h>

typedef struct foo {
  int **ppX;
  struct foo* ppF;
} foo_t ;

void bar(int **pX) {
  assert(*pX); 
  *pX = malloc(sizeof(int));
}

int main() {
  foo_t *pF = malloc(sizeof(foo_t));
  int *pI = malloc(sizeof(int));
  pF->ppX = &pI + 43024;
  // pF->ppF = pF;
  bar((int**)pF);
  free(pF);
}

Attachment: bstruct7.pool
Description: Binary data

Attachment: bstruct7.ll
Description: Binary data