Z3 and loadable optimization

I created a loadable optimization following the tutorial at http://llvm.org/docs/WritingAnLLVMPass.html. I want to use the Z3 library, installed in my system, in my optimization. When I include z3++.h (the name of the library) in the code and use its classes, it compiles well, but when I try to run it it says:

opt: symbol lookup error: /home/giacomo/llvm/Debug+Asserts/lib/Acsl.so: undefined symbol: Z3_mk_config

What’s the issue?

If the Z3 library is a dynamically linked library, then it’s probably not being loaded into opt. You might be able to force loading of it with the -load option or by setting your LD_LIBRARY_PATH environment variable to include the location of the Z3 library. If the Z3 library is a statically linked library (a .a file on Linux), then it might be the case that not all of the symbols in libz3.a are being linked into your pass’s .so file (because the linker doesn’t think those symbols are used). LLVM has similar problems with its .a files and uses LinkAllPasses.h to trick the compiler into including all the functions that it needs for .a files. A similar hack should fix the problem that you’re seeing. – John T.

I think I am in the first case, but I don’t understand something, the -load option during which command? opt? and which file should I load? libz3.so?

Yes and Yes. Try using the -load option of the opt command to load libz3.so into opt’s address space. It might work even though libz3.so isn’t a plugin to opt. – John T.