Skip to Content.
Sympa Menu

svadev - Re: [svadev] Documentation

svadev AT lists.siebelschool.illinois.edu

Subject: Svadev mailing list

List archive

Re: [svadev] Documentation


Chronological Thread 
  • From: "Adve, Vikram Sadanand" <vadve AT illinois.edu>
  • To: John Criswell <criswell AT uiuc.edu>
  • Cc: "svadev AT cs.uiuc.edu" <svadev AT cs.uiuc.edu>
  • Subject: Re: [svadev] Documentation
  • Date: Tue, 9 Mar 2010 18:09:50 -0600
  • Accept-language: en-US
  • Acceptlanguage: en-US
  • List-archive: <http://lists.cs.uiuc.edu/pipermail/svadev>
  • List-id: <svadev.cs.uiuc.edu>

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





Archive powered by MHonArc 2.6.16.

Top of Page