Svadev mailing list

[John Criswell <criswell AT illinois.edu>]

On 11/27/12 11:21 AM, Daniel Huang wrote:

Hi svadev,

I'm starting to hook the verified type-checker to the SAFEcode compiler. As a rehash, I need LLVM bitcode decorated with regions (its ok if all of the regions are global) and to convert this LLVM bitcode into my AST. I'm open to suggestions, but my current plan is to write an LLVM pass (using the Caml interface) to translate the internal LLVM bitcode into my AST in memory. I would appreciate pointers on how to get started on this, such as which files/passes/APIs (e.g. how to query which region a variable is in) to look at and where is the relevant documentation. Hope everyone had a good Thanksgiving!

Hi Daniel.

Regarding the OCaml interface to the LLVM API, I would ask about that on the llvmdev list.  I haven't used it myself, so I'm not sure how to use it or what state it's in.  You could also ask on the LLVM IRC channel.

As for querying for the regions, I'm not sure if there's a really good way to do this currently.  The automatic pool allocation pass does have methods for querying the pool handle to which an LLVM SSA register belongs, but that interface is deprecated since it makes the automatic pool allocation pass a combined transform/analysis pass (which the LLVM pass manager doesn't really support).  It might work, but I would not expect it to work.

Instead, what you could do is use the DSNodeEquivs pass (include/assistDS/DSNodeEquivs.h).  This pass takes all the different DSGraphs for each function and matches up those DSNodes which refer to the same abstract memory location.  What you need to do is to have your pass require the DSNodeEquivs pass and then have it use the DSNodeEquivs::getMemberForValue() method to find a DSNode for each value.  That DSNode uniquely represents a global region.

Using DSNodeEquivs will work if you just want to test your type checker on global regions.  If you want to test functions that are region polymorphic, then more work will need to be done.  One possibility would be to separate out of poolalloc the code that assigns regions to SSA values.  Part of that code lives in the Heuristic analysis group, but some of it is still hard-coded into poolalloc itself.

Does this help?

-- John T.

Regards,

Dan

On Wed, Nov 21, 2012 at 7:36 PM, Adve, Vikram Sadanand <vadve AT illinois.edu> wrote:

On Nov 21, 2012, at 1:02 PM, Daniel Huang <dan.e.huang AT gmail.com>

 wrote:

1) Any version of SVA that annotates LLVM bitcode with regions will work. What do you mean when you say "region attributes on pointer values will be available through API calls"? Is the API call referring to an API call available when I'm writing a LLVM pass, or do you mean a pointer value's region manifests itself in the LLVM bitcode as an API call?

An API call available within an LLVM pass.  The PoolAlloc transform allows you to query the pool handle (region) for any given pointer-type variable in scope in a function, including local (SSA) variables, parameters and globals.

2) It would probably be easiest for me to write a LLVM pass (using the Caml interface) to translate the internal LLVM bitcode into my AST (in memory), and then have the type-checker interface directly with this (so no parsing is necessary). 

That makes sense.

I'll pick this up after the holidays, so there is no rush. Have a great Thanksgiving!

Enjoy the holiday!!

--Vikram

Regards,

Dan

On Tue, Nov 20, 2012 at 11:35 PM, Adve, Vikram Sadanand <vadve AT illinois.edu> wrote:

Dan,

Glad to hear you've reached this point.  Getting the type checker proved sound and generating it from Coq are major milestones!

I think there are 2 main parts to what you will need:

1. Getting LLVM bitcode decorated with region annotations and poolalloc / poolfree calls.

2. Converting the LLVM bitcode into your AST.  

For the first one, we have a fairly robust version of pool allocation that simply uses a single global pool for all objects.  This means that all the pointers will point to the same region, but the syntax and the type rules should still be valid.  It will just model a very weak analysis.  If that will work for you, then you will have all the information you need to perform step 2.  The poolalloc/poolfree calls will be explicit function calls in the LLVM bitcode.  The region attributes on pointer values will be available through API calls.

For the second one, I didn't realize you are using your own AST -- that could be a small amount of additional work, but shouldn't be too bad.  There are two ways I can imagine accomplishing what you need.  One is to interface to the LLVM bitcode directly from the type checker, since the LLVM IR has an OCaml interface.  The other is to write an LLVM pass that translates LLVM instructions into your instruction syntax (either in memory via the OCaml interface) or offline by emitting your AST in, say, assembly form.  You would know best which of these is easier for you.

Let me know if you'd like to start with the single-global-pool transform and we'll get you information on how to do it.  And of course, if you have any questions.  (This week may be a little slow of answers since both John Criswell and I, and I presume others, will be off the next few days.)

--Vikram

Professor, Computer Science

University of Illinois at Urbana-Champaign

http://llvm.org/~vadve

On Nov 20, 2012, at 2:12 PM, Daniel Huang <dan.e.huang AT gmail.com>

 wrote:

Hi svadev,

I've been working on a verified type-checker for SVA and am at the point where I would like to type-check code produced by the SVA compiler. Currently, the type-checker operates on a LLVM-like syntax defined like the datatype below:

op ::= %x | constant

type ::= Int | Ptr (type, region)

instr ::= load type op | store type op type op | ...

block ::= list instr ; terminator

...

It is my understanding that the compiler will run Automatic Pool Allocation to infer program regions, decorate the program with those regions, and then codegens to LLVM bitcode, where the codegen erases some type information so the LLVM type-checker passes. For example, 

(Internal representation?)

int*r1 x = poolalloc(r1, 4);

store int 5, int*r1 x;

 -->

(Output LLVM bitcode)

%1 = (i8*) poolalloc(r1, 4);

%2 = bitcast i8* %1 to i32*;

store int 5, int* %2;

 

What is the easiest way to convert the LLVM bitcode into a datatype that my type-checker understands (i.e. fully decorated with regions)? For example, would I write a LLVM pass that outputs the internal LLVM AST as my AST decorated with the regions directly? If so, are there suggestions on how to do this (e.g. which files to look at, how hard this is to do)? 

Thanks,

Dan

_______________________________________________
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