Svadev mailing list

[Daniel Huang <dan.e.huang AT gmail.com>]

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