Re: [klee-dev] KLEE: ERROR: Loading file /usr/local/lib/klee/runtime/klee-uclibc.bca failed: Invalid record
Hi, On Mon, 8 Aug 2022 18:24:27 -0700 Biqian Cheng wrote: > Did you rebuild it (make) in case it was wrong beforehand? > > Yes, I tried to use "cmake -DENABLE_POSIX_RUNTIME=ON > -DENABLE_KLEE_UCLIBC=ON -DKLEE_UCLIBC_PATH=/home/klee-uclibc .." then > "make -j2" to rebuild it. I meant uclibc. There is a "make -j2" line in step 5: https://klee.github.io/build-llvm11/ Here you are configuring KLEE. Do a "make clean" in KLEE's build directory and call cmake with your options again but add the path to your llvm-config-11: -DLLVM_CONFIG_BINARY=/bin/llvm-config-11 > Then check the LLVM version klee is linked against (e.g. ldd >> /bin/klee) > > > I used "ldd /usr/local/bin/klee", it gives me: > > ... > libLLVM-10.so.1 => /usr/lib/llvm-10/lib/libLLVM-10.so.1 > (0x7f183c049000) libstdc++.so.6 => > ... > Is this indicating I'm using LLVM-10, while I'm supposed to use > LLVM-11? Yes. > and finally the build output of your program.bc (enable verbose mode > for > > make/...). > > > Does this mean make -j2? Depending on the Makefile for that program you can run "make VERBOSE=1" or use a hack like "make SHELL='sh -x'" to see what commands are executed. If it's just a single C file and you are using clang directly, you don't need that step. Kind regards, Frank ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] KLEE: ERROR: Loading file /usr/local/lib/klee/runtime/klee-uclibc.bca failed: Invalid record
Hi Frank, Did you rebuild it (make) in case it was wrong beforehand? Yes, I tried to use "cmake -DENABLE_POSIX_RUNTIME=ON -DENABLE_KLEE_UCLIBC=ON -DKLEE_UCLIBC_PATH=/home/klee-uclibc .." then "make -j2" to rebuild it. Then check the LLVM version klee is linked against (e.g. ldd > /bin/klee) I used "ldd /usr/local/bin/klee", it gives me: linux-vdso.so.1 (0x7fff2cba9000) libsqlite3.so.0 => /lib/x86_64-linux-gnu/libsqlite3.so.0 (0x7f1841e9) libz3.so.4 => /lib/x86_64-linux-gnu/libz3.so.4 (0x7f18408f) libz.so.1 => /lib/x86_64-linux-gnu/libz.so.1 (0x7f18408d4000) libtcmalloc.so.4 => /lib/x86_64-linux-gnu/libtcmalloc.so.4 (0x7f18406dd000) libLLVM-10.so.1 => /usr/lib/llvm-10/lib/libLLVM-10.so.1 (0x7f183c049000) libstdc++.so.6 => /lib/x86_64-linux-gnu/libstdc++.so.6 (0x7f183be67000) libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x7f183bd16000) libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x7f183bb24000) libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x7f183bb01000) libdl.so.2 => /lib/x86_64-linux-gnu/libdl.so.2 (0x7f183bafb000) libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x7f183bae) /lib64/ld-linux-x86-64.so.2 (0x7f1842332000) libunwind.so.8 => /lib/x86_64-linux-gnu/libunwind.so.8 (0x7f183bac3000) libffi.so.7 => /lib/x86_64-linux-gnu/libffi.so.7 (0x7f183bab5000) libedit.so.2 => /lib/x86_64-linux-gnu/libedit.so.2 (0x7f183ba7d000) librt.so.1 => /lib/x86_64-linux-gnu/librt.so.1 (0x7f183ba73000) libtinfo.so.6 => /lib/x86_64-linux-gnu/libtinfo.so.6 (0x7f183ba43000) liblzma.so.5 => /lib/x86_64-linux-gnu/liblzma.so.5 (0x7f183ba1a000) libbsd.so.0 => /lib/x86_64-linux-gnu/libbsd.so.0 (0x7f183b9fe000) Is this indicating I'm using LLVM-10, while I'm supposed to use LLVM-11? and finally the build output of your program.bc (enable verbose mode for > make/...). Does this mean make -j2? > Does klee complain without "--libc=uclibc"? No, when I deleted "--libc=uclibc". The issue disappears. Thank you for your help! --Biqian On Mon, Aug 8, 2022 at 1:30 PM Frank Busse wrote: > Hi, > > > On Mon, 8 Aug 2022 13:18:54 -0700 > Biqian Cheng wrote: > > > Thanks for your reply. I typed this command as you suggested > > previously: ./configure --make-llvm-lib --with-cc clang-11 > > --with-llvm-config llvm-config-11 > > > > Here are what I got after typing that command: > > Looks good. Did you rebuild it (make) in case it was wrong beforehand? > Then check the LLVM version klee is linked against (e.g. ldd > /bin/klee) and finally the build output of your program.bc > (enable verbose mode for make/...). Does klee complain > without "--libc=uclibc"? > > > libllvm10/focal,now 1:10.0.0-4ubuntu1 amd64 [installed,automatic] > > Given that LLVM10 is on your machine as well I think we're on the right > path. ;) > > > Kind regards, > > Frank > ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] KLEE: ERROR: Loading file /usr/local/lib/klee/runtime/klee-uclibc.bca failed: Invalid record
Hi, On Mon, 8 Aug 2022 13:18:54 -0700 Biqian Cheng wrote: > Thanks for your reply. I typed this command as you suggested > previously: ./configure --make-llvm-lib --with-cc clang-11 > --with-llvm-config llvm-config-11 > > Here are what I got after typing that command: Looks good. Did you rebuild it (make) in case it was wrong beforehand? Then check the LLVM version klee is linked against (e.g. ldd /bin/klee) and finally the build output of your program.bc (enable verbose mode for make/...). Does klee complain without "--libc=uclibc"? > libllvm10/focal,now 1:10.0.0-4ubuntu1 amd64 [installed,automatic] Given that LLVM10 is on your machine as well I think we're on the right path. ;) Kind regards, Frank ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] KLEE: ERROR: Loading file /usr/local/lib/klee/runtime/klee-uclibc.bca failed: Invalid record
Hi Frank, Thanks for your reply. I typed this command as you suggested previously: ./configure --make-llvm-lib --with-cc clang-11 --with-llvm-config llvm-config-11 Here are what I got after typing that command: INFO:Forcing C compiler to be...clang-11 INFO:Absolute path to compiler.../usr/bin/clang-11 INFO:Disabling assertions INFO:Configuring for Debug build INFO:Configuring for LLVM bitcode archive INFO:Using llvm-config at.../usr/bin/llvm-config-11 INFO:Using llvm tool dir.../usr/lib/llvm-11/bin INFO:Found "/usr/lib/llvm-11/bin/llvm-nm". INFO:Found "/usr/lib/llvm-11/bin/llvm-ar". INFO:Found "/usr/lib/llvm-11/bin/llvm-link". INFO:Found "/usr/lib/llvm-11/bin/llvm-objdump". INFO:Using LLVM Bitcode Compiler specified by CC .../usr/bin/clang-11 INFO:Testing LLVM Bitcode compiler.../usr/bin/clang-11 INFO:Compiler /usr/bin/clang-11 works INFO:Checking for ncurses... INFO:Removing template destination "/home/biqiancheng/klee-uclibc/Makefile.klee" INFO:Writing templated file to "/home/biqiancheng/klee-uclibc/Makefile.klee" WARNING:Removing existing config file.../home/biqiancheng/klee-uclibc/.config INFO:Setting up pre-made configure for...x86_64 INFO:Installing .config file INFO:Looking for kernel include path... INFO:Found "/usr/include/x86_64-linux-gnu" This should mean I have configured it correctly, right? After doing that, I still get the same error message: KLEE: ERROR: Loading file /usr/local/lib/klee/runtime/klee-uclibc.bca failed: Invalid record I checked LLVM versions that are installed by running this command: apt list --installed | grep -i llvm WARNING: apt does not have a stable CLI interface. Use with caution in scripts. libllvm10/focal,now 1:10.0.0-4ubuntu1 amd64 [installed,automatic] libllvm11/unknown,now 1:11.1.0~++20211011094159+1fdec59bffc1-1~exp1~20211011214622.5 amd64 [installed,automatic] llvm-10-dev/focal,now 1:10.0.0-4ubuntu1 amd64 [installed,automatic] llvm-10-runtime/focal,now 1:10.0.0-4ubuntu1 amd64 [installed,automatic] llvm-10-tools/focal,now 1:10.0.0-4ubuntu1 amd64 [installed,automatic] llvm-10/focal,now 1:10.0.0-4ubuntu1 amd64 [installed,automatic] llvm-11-dev/unknown,now 1:11.1.0~++20211011094159+1fdec59bffc1-1~exp1~20211011214622.5 amd64 [installed] llvm-11-doc/unknown,unknown,now 1:11.1.0~++20211011094159+1fdec59bffc1-1~exp1~20211011214622.5 all [installed,automatic] llvm-11-linker-tools/unknown,now 1:11.1.0~++20211011094159+1fdec59bffc1-1~exp1~20211011214622.5 amd64 [installed,automatic] llvm-11-runtime/unknown,now 1:11.1.0~++20211011094159+1fdec59bffc1-1~exp1~20211011214622.5 amd64 [installed,automatic] llvm-11-tools/unknown,now 1:11.1.0~++20211011094159+1fdec59bffc1-1~exp1~20211011214622.5 amd64 [installed] llvm-11/unknown,now 1:11.1.0~++20211011094159+1fdec59bffc1-1~exp1~20211011214622.5 amd64 [installed] llvm-dev/focal,now 1:10.0-50~exp1 amd64 [installed] llvm-runtime/focal,now 1:10.0-50~exp1 amd64 [installed,automatic] llvm/focal,now 1:10.0-50~exp1 amd64 [installed] I used clang-11 to get .bc files, and build KLEE with LLVM 11. Based on this, do I mix different LLVM versions? Thank you! Biqian Cheng On Mon, Aug 8, 2022 at 12:56 PM Frank Busse wrote: > Hi, > > > On Mon, 8 Aug 2022 12:30:24 -0700 > Biqian Cheng wrote: > > > The error message is: > > > > KLEE: ERROR: Loading file /usr/local/lib/klee/runtime/klee-uclibc.bca > > failed: Invalid record > > This happens typically when you mix different LLVM versions. See step 5: > https://klee.github.io/build-llvm11/ > > and make sure you're using the right llvm-config (and don't put '#' in > the command). > > > Kind regards, > > Frank > ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] KLEE: ERROR: Loading file /usr/local/lib/klee/runtime/klee-uclibc.bca failed: Invalid record
Hi, On Mon, 8 Aug 2022 12:30:24 -0700 Biqian Cheng wrote: > The error message is: > > KLEE: ERROR: Loading file /usr/local/lib/klee/runtime/klee-uclibc.bca > failed: Invalid record This happens typically when you mix different LLVM versions. See step 5: https://klee.github.io/build-llvm11/ and make sure you're using the right llvm-config (and don't put '#' in the command). Kind regards, Frank ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev