Svadev mailing list

[Jean-Baptiste Tristan <jean.baptiste.tristan AT gmail.com>]

On Wed, Mar 10, 2010 at 2:48 PM, John Criswell 
<criswell AT uiuc.edu>
 wrote:
> Jean-Baptiste Tristan wrote:
>>
>> I was expecting to be able to apply SAFEcode on the example in figure
>> 2 a of the PLDI 06
>> paper and match the result (in figure 4) with what I obtain.
>>
>
> Note that SAFECode in the PLDI 2006 publication used automatic pool
> allocation.  Using the default options to sc, automatic pool allocation is
> not used, so you will only see one pool.
>
> Automatic pool allocation hasn't been used in awhile, so it is experiencing
> some bitrot issues.  Improving pool allocation's quality of implementation
> is on our TODO list.
>>
>> With the input code
>>
>>  int **x, *y, *z, ***w, u;
>>  x = (int **) malloc(4);
>>  y = (int *) malloc (4);
>>  z = (int *) malloc(4);
>>
>>  *x = y;
>>  *y = 5;
>>  free(z);
>>  *z = 10;
>>
>>  u = *z;
>>  w = (int ***) z;
>>  *w = x;
>>
>>  return 0;
>>
>>
>>
>> SAFEcode gives me :
>>
>>
>>  call void @__sc_dbg_poolargvregister(i32 %argc, i8** %argv)
>>  %sizetmp = mul i32 1, 4                         ; <i32> [#uses=2]
>>  %call29 = call i8* @__sc_dbg_src_poolalloc(%PoolDescriptor*
>> @__poolalloc_GlobalPool, i32 %sizetmp, i32 0, i8* getelementptr
>> inbounds ([5 x i8]* @sourcefile, i32 0, i32 0), i32 1) ; <i8*>
>> [#uses=2]
>>  %call2.casted = bitcast i8* %call29 to i8*      ; <i8*> [#uses=1]
>>  %__poolalloc_GlobalPool.casted8 = bitcast %PoolDescriptor*
>> @__poolalloc_GlobalPool to i8* ; <i8*> [#uses=1]
>>  call void @__sc_dbg_src_poolregister(i8*
>> %__poolalloc_GlobalPool.casted8, i8* %call2.casted, i32 %sizetmp, i32
>> 6, i8* getelementptr inbounds ([5 x i8]* @sourcefile7, i32 0, i32 0),
>> i32 7)
>>  %0 = bitcast i8* %call29 to i8*                 ; <i8*> [#uses=1]
>>  %conv = bitcast i8* %0 to i32**                 ; <i32**> [#uses=2]
>>  %sizetmp3 = mul i32 1, 4                        ; <i32> [#uses=2]
>>  %call1410 = call i8* @__sc_dbg_src_poolalloc(%PoolDescriptor*
>> @__poolalloc_GlobalPool, i32 %sizetmp3, i32 1, i8* getelementptr
>> inbounds ([5 x i8]* @sourcefile2, i32 0, i32 0), i32 2) ; <i8*>
>> [#uses=2]
>>  %call14.casted = bitcast i8* %call1410 to i8*   ; <i8*> [#uses=1]
>>  %__poolalloc_GlobalPool.casted7 = bitcast %PoolDescriptor*
>> @__poolalloc_GlobalPool to i8* ; <i8*> [#uses=1]
>>  call void @__sc_dbg_src_poolregister(i8*
>> %__poolalloc_GlobalPool.casted7, i8* %call14.casted, i32 %sizetmp3,
>> i32 5, i8* getelementptr inbounds ([5 x i8]* @sourcefile6, i32 0, i32
>> 0), i32 6)
>>  %1 = bitcast i8* %call1410 to i8*               ; <i8*> [#uses=1]
>>  %conv2 = bitcast i8* %1 to i32*                 ; <i32*> [#uses=2]
>>  %sizetmp5 = mul i32 1, 4                        ; <i32> [#uses=2]
>>  %call3611 = call i8* @__sc_dbg_src_poolalloc(%PoolDescriptor*
>> @__poolalloc_GlobalPool, i32 %sizetmp5, i32 2, i8* getelementptr
>> inbounds ([5 x i8]* @sourcefile3, i32 0, i32 0), i32 3) ; <i8*>
>> [#uses=3]
>>  %call36.casted = bitcast i8* %call3611 to i8*   ; <i8*> [#uses=1]
>>  %__poolalloc_GlobalPool.casted = bitcast %PoolDescriptor*
>> @__poolalloc_GlobalPool to i8* ; <i8*> [#uses=1]
>>  call void @__sc_dbg_src_poolregister(i8*
>> %__poolalloc_GlobalPool.casted, i8* %call36.casted, i32 %sizetmp5, i32
>> 4, i8* getelementptr inbounds ([5 x i8]* @sourcefile5, i32 0, i32 0),
>> i32 5)
>>  %2 = bitcast i8* %call3611 to i8*               ; <i8*> [#uses=1]
>>  %conv4 = bitcast i8* %2 to i32*                 ; <i32*> [#uses=4]
>>  store i32* %conv2, i32** %conv
>>  store i32 5, i32* %conv2
>>  %conv8 = bitcast i32* %conv4 to i8*             ; <i8*> [#uses=1]
>>  call void @__sc_dbg_poolunregister_debug(i8* bitcast
>> (%PoolDescriptor* @__poolalloc_GlobalPool to i8*), i8* %call3611, i32
>> 7, i8* getelementptr inbounds ([5 x i8]* @sourcefile8, i32 0, i32 0),
>> i32 8)
>>  call void @__sc_dbg_src_poolfree(%PoolDescriptor*
>> @__poolalloc_GlobalPool, i8* %conv8, i32 3, i8* getelementptr inbounds
>> ([5 x i8]* @sourcefile4, i32 0, i32 0), i32 4)
>>  store i32 10, i32* %conv4
>>  %tmp11 = load i32* %conv4                       ; <i32> [#uses=0]
>>  %conv13 = bitcast i32* %conv4 to i32***         ; <i32***> [#uses=1]
>>  store i32** %conv, i32*** %conv13
>>  ret i32 0
>>
>>
>> And I have difficulties to find the pool information that may be used
>> to perform type verification
>> or the poolinit, pooldestroy operations.
>>
>
> The pool is explicitly passed into the poolalloc and poolfree calls (named
> __sc_dbg_src_poolalloc and __sc_dbg_src_poolfree, respectively).  I do not
> see the call to poolinit(); I believe calls to poolinit() for global (i.e.,
> context insensitive) pools are done in a constructor function instead of in
> the main() function (because C++ global variables may have constructors that
> are called before main(), so the pools that they use must be initialized
> before main() too).

Yes, OK.

%PoolDescriptor = type [92 x i8*]
@__poolalloc_GlobalPool = global %PoolDescriptor zeroinitializer ;
<%PoolDescriptor*> [#uses=9]

Having only one pool doesn't change the safety guarantees, it only
results in more runtime checks
and an increased memory consumption that what would be needed with a
better pool allocation. Is that right ?

> If automatic pool allocation would have been used, then each allocation
> would have ended up in a different pool (unless DSA thinks they may alias).
>
> The SAFECode transform does not annotate the LLVM bitcode to link pools to
> the types inferred for that pool by DSA.  Instead, that information is kept
> in memory by the DSA/Pool Allocation passes; the SAFECode transform passes
> query DSA/Pool Allocation whenever they need to know the type and pool
> information of a pointer.
>
> Writing a pass that annotates pools with the DSA-inferred type of the
> objects within the pool would probably be a straightforward pass to write.

That's a good news. I think it would be nice to add this piece of information
so that type checking can be done completely independently of the
SAFEcode tools and
allowing some kind of proof-carying code.


>
> -- John T.
>
>> -John
>>
>>
>> On Tue, Mar 9, 2010 at 7:09 PM, Adve, Vikram Sadanand
>> <vadve AT illinois.edu>
>>  wrote:
>>
>>>
>>> Jean,
>>>
>>> FYI, the type encoding from the PLDI06 paper hasn't been tested much
>>> since the SOSP 07 paper.  DSA and Poolalloc (and LLVM) have evolved
>>> since then so the old code probably doesn't work.
>>>
>>> What exactly do you want with the code?  I think the PLDI paper is
>>> more reliable, anyway, though much less detailed.
>>>
>>> --Vikram
>>> http://llvm.org/~vadve
>>>
>>>
>>> On Mar 9, 2010, at 3:24 PM, "John Criswell" 
>>> <criswell AT uiuc.edu>
>>>  wrote:
>>>
>>>
>>>>
>>>> Jean-Baptiste Tristan wrote:
>>>>
>>>>>
>>>>> Hi,
>>>>>
>>>>> I have transformed a piece of code using sc, and the resulting code
>>>>> has a few extra function declarations such as:
>>>>>
>>>>> declare void @sc.lscheck(i8*, i8*)
>>>>>
>>>>> Is there any documentation that could help me understand what those
>>>>> functions do ?
>>>>>
>>>>>
>>>>
>>>> There isn't documentation per se, but the comments in
>>>> runtime/DebugRuntime might be able to help explain what these
>>>> functions
>>>> do.  You might also want to consult the SOSP 2007 paper on SVA; it
>>>> might
>>>> describe the run-time checks more clearly and is closer to the current
>>>> SAFECode implementation than the PLDI paper.
>>>>
>>>> Briefly, the run-time functions that SAFECode inserts are:
>>>>
>>>> 1) sc.lscheck - Load/store check.  This is the poolcheck() function
>>>> from
>>>> the PLDI 2006 publication.
>>>>
>>>> 2) sc.poolcheckalign - Load/store alignment check.  Ensures that the
>>>> pointer points to a valid object and is of the correct alignment
>>>>
>>>> 3) sc.boundscheck[ui] - Ensure that an indexing operation (a GEP) does
>>>> not create an out of bounds pointer.  This check was introduced, I
>>>> believe, in the ICSE publication.
>>>>
>>>> 4) pool_register/pool_unregister - These functions tell the run-time
>>>> when objects have been allocated or deallocated.  There are now
>>>> separate
>>>> versions for global, stack, and heap objects so that the runtime can
>>>> treat them differently.
>>>>
>>>> 5) pool_shadow/pool_unshadow - These functions implement the MMU
>>>> remapping for danging pointer detection.  This technique is
>>>> described in
>>>> the DSN paper.  As dangling pointer *detection* (as opposed to
>>>> *protection*) is disabled by default, you probably won't see any calls
>>>> to these functions.
>>>>
>>>> Note that there are alternative versions of these functions that
>>>> take a
>>>> tag and source filename/line number information.  These are used for
>>>> the
>>>> SAFECode debugging tool.
>>>>
>>>>
>>>>>
>>>>> Some of those functions have a name that is close to the name of some
>>>>> of the statements
>>>>> or expressions used in the type system described in the paper
>>>>> "SAFEcode: Enforcing Alias Analysis
>>>>> for Weakly Typed Languages". Do you use those functions to "encode"
>>>>> the type system described in
>>>>> this paper into regular LLVM code ?
>>>>>
>>>>>
>>>>
>>>> I don't believe they "encode" the type system; rather, they implement
>>>> the run-time checks required to provide the memory safety guarantees
>>>> described in the PLDI and ICSE papers.  The typing information, I
>>>> believe, is implicit in the pools used in the calls to poolalloc and
>>>> the
>>>> above run-time checks (when automatic pool allocation is enabled;
>>>> currently, SAFECode disables automatic pool allocation and uses a
>>>> simpler transform which puts all heap objects into a single pool; it
>>>> adjusts the points-to analysis results to reflect the fact that
>>>> everything is going into a global pool).
>>>>
>>>> There is code to encode the points-to analysis results in the LLVM
>>>> bitcode.  That is the code in the safecode/lib/ProofWrap directory.
>>>> Dinakar wrote it for the SOSP 2007 paper.  I have never used it, so I
>>>> can't comment on its functionality at present.  I may look into it at
>>>> some point, but that depends on work priorities.
>>>>
>>>> -- John T.
>>>>
>>>>>
>>>>> -John
>>>>> _______________________________________________
>>>>> svadev mailing list
>>>>> svadev AT cs.uiuc.edu
>>>>> http://lists.cs.uiuc.edu/mailman/listinfo/svadev
>>>>>
>>>>>
>>>>
>>>> _______________________________________________
>>>> svadev mailing list
>>>> svadev AT cs.uiuc.edu
>>>> http://lists.cs.uiuc.edu/mailman/listinfo/svadev
>>>>
>
>