Re: [klee-dev] KLEE: ERROR: Loading file /usr/local/lib/klee/runtime/klee-uclibc.bca failed: Invalid record

2022-08-09 Thread Frank Busse
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

2022-08-08 Thread Biqian Cheng
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

2022-08-08 Thread Frank Busse
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

2022-08-08 Thread Biqian Cheng
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

2022-08-08 Thread Frank Busse
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