[LLVMdev] vmkit and klee

[Nicolas Geoffray]

Hi Cristian,

Cristian Zamfir wrote:
> Hi,
>
> I am trying to evaluate how complex would be to modify KLEE ( http://klee.llvm.org/ 
>   ) so that it can run LLVM bitcode compiled from Java code obtained  
> with vmjc (from the VMKIT project). Your feedback will be very  
> appreciated.
>   

OK.

> I am familiar with KLEE but I would like to know more about VMKIT, so  
> please point me to the right docs/source code if appropriate.
>
> After a quick look over VMKIT, I think that I would need to add  
> support in KLEE for synchronization, exceptions, class loading,  
> inheritance and maybe some simple garbage collection, since  
> performance is not an issue.
>   

Why would you need support in klee? Can't you run a .so while executing 
with klee? You can compile vmkit's jvm to a .so.

> Another problem seems to be that the bitcode depends on the core class  
> libraries provided by Classpath.
> I guess these would need to be compiled to LLVM and loaded by KLEE too  
> but that would make the resulting LLVM bitcode huge. Do you have any  
> suggestions for that?
>   

So yeah, a .bc file generated by vmjc depends on the standard library 
compiled into a huge .so file (you can generate that .so file by typing 
make in the tools/vmjc/libvmjc directory). What's possible is to include 
in the application .bc file all its dependencies with the standard 
library. That's something vmkit currently does not do, but I don't see a 
real difficulty in supporting it.
> Finally, is there a VMKIT tool that runs the *.bc output of vmjc, or  
> the only option is to run jnjvm with the jar file? I think such a tool  
> would be exactly what I need to take a look at.
>
>   

OK, that can be provided easily. Currently, you can generate a .exe file 
or a .so file. jnjvm first tries to load a .so of the application before 
looking at the .jar. Adding a .bc file that is jit-generated should not 
be difficult. I can try to look into that soon if you'd like.

Nicolas

> Thanks,
> Cristi
>
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
>