Svadev mailing list

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

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 ...

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

2) The typechecker should ideally have this property:

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

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

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