Svadev mailing list

[Daniel Huang <dehuang AT fas.harvard.edu>]

Great, this was what I was looking for. Thanks for the speedy responses!

Regards,

Dan

On Mon, Apr 23, 2012 at 1:29 PM, John Criswell <criswell AT illinois.edu> wrote:

On 4/23/12 11:51 AM, Daniel Huang wrote:

Thanks, the writeup would be very helpful. I'll also take a look at those other resources.

The first draft of the write-up is done.  Please svn up safecode/docs.  Comments and questions are welcome.

I've been scaling out the PLDI 06 formalism to a larger subset of LLVM in the Coq Proof Assistant (so in addition its machine-checked).

I see.  If you're just interested in the sounds points-to analysis/call-graph/type-inference guarantees, you can probably ignore the boundscheck() checks.

I should also warn you that the current SAFECode implementation has automatic pool allocation and the type-safety optimization disabled (they need more work before going prime-time), so what you currently get out of SAFECode won't provide sound points-to analysis (unless your points-to analysis says that every pointer aliases every other pointer).

-- John T.

Thanks for the help!

Dan

On Mon, Apr 23, 2012 at 12:16 PM, John Criswell <criswell AT illinois.edu> wrote:

On 4/23/12 10:58 AM, Daniel Huang wrote:

1) I'm wondering if there is a list of all run-time checks that SAFECode could emit and what they do. For example, when I examine SAFECode's output, I see functions like:

declare void @pool_register(i8*, i8*, i32)

declare void @fastlscheck(i8*, i8*, i32)
etc ...

Okay.  I'm currently trying to write them up in the Software Architecture Guide.

I would like to know what each of these functions do, what parameters they take, and when they are emitted.

One thing you can do is to look at the SAFECode run-time library in safecode/runtime/DebugRuntime.  The functions should be relatively well commented (and if they're not, you can file a bug to say that they should be).

2) The typechecker should ideally have this property:

if typecheck(code) = true, then execution(code) has the safety properties guaranteed by SVA.

Which properties are you wanting guaranteed?  SAFECode's safety guarantees depend on which SAFECode paper you're reading; SVA's safety guarantees are a combination of those found in two of the SAFECode publications (namely, the ICSE 2006 and PLDI 2006 papers).

Also, the safety properties in the PLDI 2006 paper were formally proven.  Are you redoing that proof with a more complete version of the LLVM instruction set?

Also, where is this SAFECode Software Architect manual located? I'm having trouble accessing the Safecode website.

It's in the SAFECode SVN repository which is still on-line on llvm.org.  Just look in safecode/docs directory.

-- John T.

Thanks,

Dan

On Sun, Apr 22, 2012 at 6:24 PM, John Criswell <criswell AT illinois.edu> wrote:

On 4/21/12 3:39 PM, Daniel Huang wrote:

Hi,

Is there a place that documents all the instructions a SAFECode instrumentation pass can emit?

Are you asking for a list of all the run-time checks that SAFECode could emit and the situations under which it would do so, or are you asking which subset of the LLVM instruction set SAFECode instruments correctly?

 I'm thinking about building a verified type-checker for a subset of SVA and knowing what I need to model/how they work would be of great help. Right now, I've been writing test programs and trying to reverse engineer what the individual functions are doing w.r.t to the PLDI paper ...

Is your type-checker just checking that SVA enforces the points-to analysis and type-inference analysis correctly, or is it doing something more?

I can try to write up a description of the SAFECode run-time checks in the SAFECode Software Architecture manual.  Would that help?

-- John T.

Regards,

Dan

_______________________________________________
svadev mailing list
svadev AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/svadev