Svadev mailing list

["Adve, Vikram Sadanand" <vadve AT illinois.edu>]

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