Svadev mailing list

[John Criswell <criswell AT uiuc.edu>]

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
>