Re: [klee-dev] Packaging klee on Nix - gtest broken?
Figured it out and submitted a new KLEE PR to fix a test failure in the Nix sandbox. https://github.com/klee/klee/pull/1385 https://github.com/klee/klee/pull/1471 https://github.com/NixOS/nixpkgs/pull/156413 Thanks for the help. I'll do a subsequent PR to update documentation on https://klee.github.io/. Morgan On Sun, Jan 23, 2022 at 6:55 PM Morgan wrote: > > Martin, > > Thanks, that got me closer. Here's the pull request with some > improvements to the KLEE Nix package: > > https://github.com/NixOS/nixpkgs/pull/156413 > > I'm currently dealing with an error in the test suite using > klee-uclibc. Have any of you seen this? > > TEST 'KLEE :: > Runtime/POSIX/MixedConcreteSymbolic.c' FAILED > Script: > -- > : 'RUN: at line 1'; > /nix/store/js3xavmfccyzr8nzp7cg8gf3rlyqd7q5-clang-wrapper-9.0.1/bin/clang > -I/build/source/include > /build/source/test/Runtime/POSIX/MixedConcreteSymbolic.c -emit > -llvm -O0 -Xclang -disable-O0-optnone -c -o > /build/source/build/test/Runtime/POSIX/Output/MixedConcreteSymbolic.c.tmp.bc > : 'RUN: at line 2'; rm -rf > /build/source/build/test/Runtime/POSIX/Output/MixedConcreteSymbolic.c.tmp.klee-out > : 'RUN: at line 3'; /build/source/build/bin/klee > --output-dir=/build/source/build/test/Runtime/POSIX/Output/MixedConcreteSymbolic.c.tmp.klee-out > --external-calls=all --exit-on-erro > r --libc=uclibc --posix-runtime > /build/source/build/test/Runtime/POSIX/Output/MixedConcreteSymbolic.c.tmp.bc > --sym-stdin 10 > 2>/build/source/build/test/Runtime/POSIX/Output/MixedConc > reteSymbolic.c.tmp.log | FileCheck > /build/source/test/Runtime/POSIX/MixedConcreteSymbolic.c > -- > Exit Code: 2 > > Command Output (stdout): > -- > $ ":" "RUN: at line 1" > $ "/nix/store/js3xavmfccyzr8nzp7cg8gf3rlyqd7q5-clang-wrapper-9.0.1/bin/clang" > "-I/build/source/include" > "/build/source/test/Runtime/POSIX/MixedConcreteSymbolic.c" > "-emit-llvm" "-O0" > "-Xclang" "-disable-O0-optnone" "-c" "-o" > "/build/source/build/test/Runtime/POSIX/Output/MixedConcreteSymbolic.c.tmp.bc" > $ ":" "RUN: at line 2" > $ "rm" "-rf" > "/build/source/build/test/Runtime/POSIX/Output/MixedConcreteSymbolic.c.tmp.klee-out" > $ ":" "RUN: at line 3" > $ "/build/source/build/bin/klee" > "--output-dir=/build/source/build/test/Runtime/POSIX/Output/MixedConcreteSymbolic.c.tmp.klee-out" > "--external-calls=all" "--exit-on-error" "--libc=uc > libc" "--posix-runtime" > "/build/source/build/test/Runtime/POSIX/Output/MixedConcreteSymbolic.c.tmp.bc" > "--sym-stdin" "10" > # redirected output from > '/build/source/build/test/Runtime/POSIX/Output/MixedConcreteSymbolic.c.tmp.log': > KLEE: NOTE: Using POSIX model: > /build/source/build/runtime/lib/libkleeRuntimePOSIX64_Debug.bca > KLEE: NOTE: Using klee-uclibc : > /build/source/build/runtime/lib/klee-uclibc.bca > KLEE: output directory is > "/build/source/build/test/Runtime/POSIX/Output/MixedConcreteSymbolic.c.tmp.klee-out" > KLEE: Using STP solver backend > error: Linking globals named '__xstat': symbol multiply defined! > > note: command had no output on stdout or stderr > error: command failed with exit status: 1 > $ "FileCheck" "/build/source/test/Runtime/POSIX/MixedConcreteSymbolic.c" > # redirected output from > '/build/source/build/test/Runtime/POSIX/Output/MixedConcreteSymbolic.c.tmp.log': > KLEE: NOTE: Using POSIX model: > /build/source/build/runtime/lib/libkleeRuntimePOSIX64_Debug.bca > KLEE: NOTE: Using klee-uclibc : > /build/source/build/runtime/lib/klee-uclibc.bca > KLEE: output directory is > "/build/source/build/test/Runtime/POSIX/Output/MixedConcreteSymbolic.c.tmp.klee-out" > KLEE: Using STP solver backend > error: Linking globals named '__xstat': symbol multiply defined! > > # command stderr: > FileCheck error: '-' is empty. > FileCheck command line: FileCheck > /build/source/test/Runtime/POSIX/MixedConcreteSymbolic.c > > error: command failed with exit status: 2 > > -- > > Thanks, > Morgan > > On Mon, Jan 17, 2022 at 3:15 AM Nowack, Martin > wrote: > > > > Hi Morgan, > > > > On 17. Jan 2022, at 10:23, Morgan wrote: > > > > In the meantime, I'm having trouble building klee-uclibc. I got past > > the locale download (had to set > > UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=n and copy it over after > > configure since it builds in the Nix sandbox) but this seems to be > > happening now. > > > > > > That sounds like a good approach. > > If I remember correctly, with `UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=y`, > > it would only download the data if it is not available locally yet. > > So, you could download/add it first before you start the configure part. > > > > > > > > # include_next > > ^~ > > 1 error generated. > > make: *** [Makerules:175: libcrypt/des.os] Error 1 > > > > For full logs, run 'nix log > > /nix/store/r52lifnjkgn0n7fc5gxa877hnsyzpjsf-klee-uclibc-1.2.drv'. > > error: 1 dependencies of derivation > > '/nix/store/55dr6nb1cfq1hx8sr3ci4kvkzr2x8s2m-klee-2.2.drv' failed to > >
Re: [klee-dev] Packaging klee on Nix - gtest broken?
Martin, Thanks, that got me closer. Here's the pull request with some improvements to the KLEE Nix package: https://github.com/NixOS/nixpkgs/pull/156413 I'm currently dealing with an error in the test suite using klee-uclibc. Have any of you seen this? TEST 'KLEE :: Runtime/POSIX/MixedConcreteSymbolic.c' FAILED Script: -- : 'RUN: at line 1'; /nix/store/js3xavmfccyzr8nzp7cg8gf3rlyqd7q5-clang-wrapper-9.0.1/bin/clang -I/build/source/include /build/source/test/Runtime/POSIX/MixedConcreteSymbolic.c -emit -llvm -O0 -Xclang -disable-O0-optnone -c -o /build/source/build/test/Runtime/POSIX/Output/MixedConcreteSymbolic.c.tmp.bc : 'RUN: at line 2'; rm -rf /build/source/build/test/Runtime/POSIX/Output/MixedConcreteSymbolic.c.tmp.klee-out : 'RUN: at line 3'; /build/source/build/bin/klee --output-dir=/build/source/build/test/Runtime/POSIX/Output/MixedConcreteSymbolic.c.tmp.klee-out --external-calls=all --exit-on-erro r --libc=uclibc --posix-runtime /build/source/build/test/Runtime/POSIX/Output/MixedConcreteSymbolic.c.tmp.bc --sym-stdin 10 2>/build/source/build/test/Runtime/POSIX/Output/MixedConc reteSymbolic.c.tmp.log | FileCheck /build/source/test/Runtime/POSIX/MixedConcreteSymbolic.c -- Exit Code: 2 Command Output (stdout): -- $ ":" "RUN: at line 1" $ "/nix/store/js3xavmfccyzr8nzp7cg8gf3rlyqd7q5-clang-wrapper-9.0.1/bin/clang" "-I/build/source/include" "/build/source/test/Runtime/POSIX/MixedConcreteSymbolic.c" "-emit-llvm" "-O0" "-Xclang" "-disable-O0-optnone" "-c" "-o" "/build/source/build/test/Runtime/POSIX/Output/MixedConcreteSymbolic.c.tmp.bc" $ ":" "RUN: at line 2" $ "rm" "-rf" "/build/source/build/test/Runtime/POSIX/Output/MixedConcreteSymbolic.c.tmp.klee-out" $ ":" "RUN: at line 3" $ "/build/source/build/bin/klee" "--output-dir=/build/source/build/test/Runtime/POSIX/Output/MixedConcreteSymbolic.c.tmp.klee-out" "--external-calls=all" "--exit-on-error" "--libc=uc libc" "--posix-runtime" "/build/source/build/test/Runtime/POSIX/Output/MixedConcreteSymbolic.c.tmp.bc" "--sym-stdin" "10" # redirected output from '/build/source/build/test/Runtime/POSIX/Output/MixedConcreteSymbolic.c.tmp.log': KLEE: NOTE: Using POSIX model: /build/source/build/runtime/lib/libkleeRuntimePOSIX64_Debug.bca KLEE: NOTE: Using klee-uclibc : /build/source/build/runtime/lib/klee-uclibc.bca KLEE: output directory is "/build/source/build/test/Runtime/POSIX/Output/MixedConcreteSymbolic.c.tmp.klee-out" KLEE: Using STP solver backend error: Linking globals named '__xstat': symbol multiply defined! note: command had no output on stdout or stderr error: command failed with exit status: 1 $ "FileCheck" "/build/source/test/Runtime/POSIX/MixedConcreteSymbolic.c" # redirected output from '/build/source/build/test/Runtime/POSIX/Output/MixedConcreteSymbolic.c.tmp.log': KLEE: NOTE: Using POSIX model: /build/source/build/runtime/lib/libkleeRuntimePOSIX64_Debug.bca KLEE: NOTE: Using klee-uclibc : /build/source/build/runtime/lib/klee-uclibc.bca KLEE: output directory is "/build/source/build/test/Runtime/POSIX/Output/MixedConcreteSymbolic.c.tmp.klee-out" KLEE: Using STP solver backend error: Linking globals named '__xstat': symbol multiply defined! # command stderr: FileCheck error: '-' is empty. FileCheck command line: FileCheck /build/source/test/Runtime/POSIX/MixedConcreteSymbolic.c error: command failed with exit status: 2 -- Thanks, Morgan On Mon, Jan 17, 2022 at 3:15 AM Nowack, Martin wrote: > > Hi Morgan, > > On 17. Jan 2022, at 10:23, Morgan wrote: > > In the meantime, I'm having trouble building klee-uclibc. I got past > the locale download (had to set > UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=n and copy it over after > configure since it builds in the Nix sandbox) but this seems to be > happening now. > > > That sounds like a good approach. > If I remember correctly, with `UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=y`, > it would only download the data if it is not available locally yet. > So, you could download/add it first before you start the configure part. > > > > # include_next > ^~ > 1 error generated. > make: *** [Makerules:175: libcrypt/des.os] Error 1 > > For full logs, run 'nix log > /nix/store/r52lifnjkgn0n7fc5gxa877hnsyzpjsf-klee-uclibc-1.2.drv'. > error: 1 dependencies of derivation > '/nix/store/55dr6nb1cfq1hx8sr3ci4kvkzr2x8s2m-klee-2.2.drv' failed to > build > > > > My CC is LLVM/clang 9. Seems similar to this issue, but I can't figure > out what's going on. > > https://github.com/klee/klee-uclibc/issues/7 > > > The problem with this one is that systems headers are not found. > Can you add them to your sandbox? > You have to workaround this issues: > > https://github.com/NixOS/nixpkgs/blob/3ddd960a3b575bf3230d0e59f42614b71f9e0db9/pkgs/build-support/cc-wrapper/default.nix#L338 > > Best, > Martin > > > > Morgan > > On Tue, Jan 11, 2022 at 2:30 AM Nowack, Martin > wrote: > > > Hi Morgan, > > Just looked at the build instructions: > >
Re: [klee-dev] Packaging klee on Nix - gtest broken?
Hi Morgan,
On 17. Jan 2022, at 10:23, Morgan mailto:m...@numin.it>> wrote:
In the meantime, I'm having trouble building klee-uclibc. I got past
the locale download (had to set
UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=n and copy it over after
configure since it builds in the Nix sandbox) but this seems to be
happening now.
That sounds like a good approach.
If I remember correctly, with `UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=y`,
it would only download the data if it is not available locally yet.
So, you could download/add it first before you start the configure part.
# include_next
^~
1 error generated.
make: *** [Makerules:175: libcrypt/des.os] Error 1
For full logs, run 'nix log
/nix/store/r52lifnjkgn0n7fc5gxa877hnsyzpjsf-klee-uclibc-1.2.drv'.
error: 1 dependencies of derivation
'/nix/store/55dr6nb1cfq1hx8sr3ci4kvkzr2x8s2m-klee-2.2.drv' failed to
build
My CC is LLVM/clang 9. Seems similar to this issue, but I can't figure
out what's going on.
https://github.com/klee/klee-uclibc/issues/7
The problem with this one is that systems headers are not found.
Can you add them to your sandbox?
You have to workaround this issues:
https://github.com/NixOS/nixpkgs/blob/3ddd960a3b575bf3230d0e59f42614b71f9e0db9/pkgs/build-support/cc-wrapper/default.nix#L338
Best,
Martin
Morgan
On Tue, Jan 11, 2022 at 2:30 AM Nowack, Martin
mailto:m.now...@imperial.ac.uk>> wrote:
Hi Morgan,
Just looked at the build instructions:
https://github.com/NixOS/nixpkgs/blob/master/pkgs/applications/science/logic/klee/default.nix#L53
"-DKLEE_RUNTIME_BUILD_TYPE=${buildType}"
I would recommend to handle the build type for the `KLEE_RUNTIME_BUILD_TYPE`
separate from the `CMAKE_BUILD_TYPE`. They are independent.
The runtime is linked to your software under test and often should contain
debug information for better stack traces reported as part of the generated
test cases, even with release builds of KLEE.
Great effort!
Best,
Martin
On 8. Jan 2022, at 23:08, Morgan wrote:
Also, do these build flags look halfway reasonable? Is there anything
that users should be able to customize? In Nix, all packages are
functions, and we can call the functions with various extra arguments
(like debug ? false) in the package.
https://github.com/NixOS/nixpkgs/blob/5f8f72c10c43514a4e9093efb9029cf3f8a9ec00/pkgs/applications/science/logic/klee/default.nix#L48
Currently we're not building klee-uclibc as I ran into some weird
issues with it, but that's next on my todo list.
I'm hoping that this package dramatically reduces the barrier to entry
to using KLEE. If users have Nix or are running NixOS, they should
just be able to use `nix-shell -p klee` or `nix-shell -p
'klee.override {debug = true;}'` or whatever they want to drop into a
shell with KLEE available.
Morgan
On Sat, Jan 8, 2022 at 2:49 PM Morgan wrote:
Somewhat related, I'm having trouble building KLEE on aarch64. Here's
the failing part:
-- Build files have been written to: /build/source/build
cmake: enabled parallel building
building
build flags: -j4 -l4
SHELL=/nix/store/fbf5n09drbi3bxv9rb9fgf58dm4da4a8-bash-5.1-p12/bin/bash
[ 1%] Building CXX object lib/Basic/CMakeFiles/kleeBasic.dir/KTest.cpp.o
[ 1%] Building CXX object
lib/Support/CMakeFiles/kleeSupport.dir/CompressionStream.cpp.o
[ 1%] Building CXX object lib/Expr/CMakeFiles/kleaverExpr.dir/ArrayCache.cpp.o
[ 1%] Building C object
runtime/Runtest/CMakeFiles/kleeRuntest.dir/intrinsics.c.o
[ 1%] Building CXX object
runtime/Runtest/CMakeFiles/kleeRuntest.dir/__/__/lib/Basic/KTest.cpp.o
[ 1%] Building CXX object lib/Basic/CMakeFiles/kleeBasic.dir/Statistics.cpp.o
[ 1%] Linking CXX shared library ../../lib/libkleeRuntest.so
[ 1%] Built target kleeRuntest
[ 1%] Building CXX object
lib/Support/CMakeFiles/kleeSupport.dir/ErrorHandling.cpp.o
[ 1%] Linking CXX static library ../libkleeBasic.a
[ 1%] Built target kleeBasic
[ 1%] Building CXX object
lib/Expr/CMakeFiles/kleaverExpr.dir/ArrayExprOptimizer.cpp.o
[ 2%] Generating memset64_Release.bc
[ 2%] Generating stubs64_Release.bc
[ 2%] Building CXX object
lib/Support/CMakeFiles/kleeSupport.dir/FileHandling.cpp.o
[ 2%] Generating fortify-fs64_Release.bc
[ 2%] Generating memcmp64_Release.bc
[ 2%] Generating fd64_Release.bc
[ 3%] Generating memcpy64_Release.bc
/build/source/runtime/POSIX/fd.c:98:18: error: use of undeclared
identifier '__NR_access'
return syscall(__NR_access, __concretize_string(pathname), mode);
^
/build/source/runtime/POSIX/fd.c:194:25: error: use of undeclared
identifier '__NR_open'; did you mean '__fd_open'?
int os_fd = syscall(__NR_open, __concretize_string(pathname), flags, mode);
^
__fd_open
/build/source/runtime/POSIX/fd.c:141:5: note: '__fd_open' declared here
int __fd_open(const char *pathname, int flags, mode_t mode) {
^
/build/source/runtime/POSIX/fd.c:286:18: error: use of undeclared
identifier '__NR_utimes'
return
Re: [klee-dev] Packaging klee on Nix - gtest broken?
Thanks Martin. I'll make this change.
In the meantime, I'm having trouble building klee-uclibc. I got past
the locale download (had to set
UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=n and copy it over after
configure since it builds in the Nix sandbox) but this seems to be
happening now.
error: builder for
'/nix/store/r52lifnjkgn0n7fc5gxa877hnsyzpjsf-klee-uclibc-1.2.drv'
failed with exit code 2;
last 10 log lines:
> cat ../../extra/locale/uClibc_locale_data.h | awk
'BEGIN{i=1}{ if ( /WANT_/ ) i = /endif/ ; else if (i) print }' >
../../include/bits/uClibc_locale_data.h
> CC libcrypt/crypt.os
> CC libcrypt/des.os
> In file included from libcrypt/des.c:62:
> In file included from ./include/sys/param.h:22:
> ./include/limits.h:124:16: fatal error: 'limits.h' file not found
> # include_next
>^~
> 1 error generated.
> make: *** [Makerules:175: libcrypt/des.os] Error 1
For full logs, run 'nix log
/nix/store/r52lifnjkgn0n7fc5gxa877hnsyzpjsf-klee-uclibc-1.2.drv'.
error: 1 dependencies of derivation
'/nix/store/55dr6nb1cfq1hx8sr3ci4kvkzr2x8s2m-klee-2.2.drv' failed to
build
My CC is LLVM/clang 9. Seems similar to this issue, but I can't figure
out what's going on.
https://github.com/klee/klee-uclibc/issues/7
Morgan
On Tue, Jan 11, 2022 at 2:30 AM Nowack, Martin wrote:
>
> Hi Morgan,
>
> Just looked at the build instructions:
>
> https://github.com/NixOS/nixpkgs/blob/master/pkgs/applications/science/logic/klee/default.nix#L53
>
> "-DKLEE_RUNTIME_BUILD_TYPE=${buildType}"
>
> I would recommend to handle the build type for the `KLEE_RUNTIME_BUILD_TYPE`
> separate from the `CMAKE_BUILD_TYPE`. They are independent.
> The runtime is linked to your software under test and often should contain
> debug information for better stack traces reported as part of the generated
> test cases, even with release builds of KLEE.
>
> Great effort!
>
> Best,
> Martin
>
> On 8. Jan 2022, at 23:08, Morgan wrote:
>
> Also, do these build flags look halfway reasonable? Is there anything
> that users should be able to customize? In Nix, all packages are
> functions, and we can call the functions with various extra arguments
> (like debug ? false) in the package.
>
> https://github.com/NixOS/nixpkgs/blob/5f8f72c10c43514a4e9093efb9029cf3f8a9ec00/pkgs/applications/science/logic/klee/default.nix#L48
>
> Currently we're not building klee-uclibc as I ran into some weird
> issues with it, but that's next on my todo list.
>
> I'm hoping that this package dramatically reduces the barrier to entry
> to using KLEE. If users have Nix or are running NixOS, they should
> just be able to use `nix-shell -p klee` or `nix-shell -p
> 'klee.override {debug = true;}'` or whatever they want to drop into a
> shell with KLEE available.
>
> Morgan
>
> On Sat, Jan 8, 2022 at 2:49 PM Morgan wrote:
>
>
> Somewhat related, I'm having trouble building KLEE on aarch64. Here's
> the failing part:
>
> -- Build files have been written to: /build/source/build
> cmake: enabled parallel building
> building
> build flags: -j4 -l4
> SHELL=/nix/store/fbf5n09drbi3bxv9rb9fgf58dm4da4a8-bash-5.1-p12/bin/bash
> [ 1%] Building CXX object lib/Basic/CMakeFiles/kleeBasic.dir/KTest.cpp.o
> [ 1%] Building CXX object
> lib/Support/CMakeFiles/kleeSupport.dir/CompressionStream.cpp.o
> [ 1%] Building CXX object
> lib/Expr/CMakeFiles/kleaverExpr.dir/ArrayCache.cpp.o
> [ 1%] Building C object
> runtime/Runtest/CMakeFiles/kleeRuntest.dir/intrinsics.c.o
> [ 1%] Building CXX object
> runtime/Runtest/CMakeFiles/kleeRuntest.dir/__/__/lib/Basic/KTest.cpp.o
> [ 1%] Building CXX object lib/Basic/CMakeFiles/kleeBasic.dir/Statistics.cpp.o
> [ 1%] Linking CXX shared library ../../lib/libkleeRuntest.so
> [ 1%] Built target kleeRuntest
> [ 1%] Building CXX object
> lib/Support/CMakeFiles/kleeSupport.dir/ErrorHandling.cpp.o
> [ 1%] Linking CXX static library ../libkleeBasic.a
> [ 1%] Built target kleeBasic
> [ 1%] Building CXX object
> lib/Expr/CMakeFiles/kleaverExpr.dir/ArrayExprOptimizer.cpp.o
> [ 2%] Generating memset64_Release.bc
> [ 2%] Generating stubs64_Release.bc
> [ 2%] Building CXX object
> lib/Support/CMakeFiles/kleeSupport.dir/FileHandling.cpp.o
> [ 2%] Generating fortify-fs64_Release.bc
> [ 2%] Generating memcmp64_Release.bc
> [ 2%] Generating fd64_Release.bc
> [ 3%] Generating memcpy64_Release.bc
> /build/source/runtime/POSIX/fd.c:98:18: error: use of undeclared
> identifier '__NR_access'
> return syscall(__NR_access, __concretize_string(pathname), mode);
> ^
> /build/source/runtime/POSIX/fd.c:194:25: error: use of undeclared
> identifier '__NR_open'; did you mean '__fd_open'?
>int os_fd = syscall(__NR_open, __concretize_string(pathname), flags, mode);
>^
>__fd_open
> /build/source/runtime/POSIX/fd.c:141:5: note: '__fd_open' declared here
> int __fd_open(const char
Re: [klee-dev] Packaging klee on Nix - gtest broken?
Hi Morgan,
Just looked at the build instructions:
https://github.com/NixOS/nixpkgs/blob/master/pkgs/applications/science/logic/klee/default.nix#L53
"-DKLEE_RUNTIME_BUILD_TYPE=${buildType}"
I would recommend to handle the build type for the `KLEE_RUNTIME_BUILD_TYPE`
separate from the `CMAKE_BUILD_TYPE`. They are independent.
The runtime is linked to your software under test and often should contain
debug information for better stack traces reported as part of the generated
test cases, even with release builds of KLEE.
Great effort!
Best,
Martin
On 8. Jan 2022, at 23:08, Morgan mailto:m...@numin.it>> wrote:
Also, do these build flags look halfway reasonable? Is there anything
that users should be able to customize? In Nix, all packages are
functions, and we can call the functions with various extra arguments
(like debug ? false) in the package.
https://github.com/NixOS/nixpkgs/blob/5f8f72c10c43514a4e9093efb9029cf3f8a9ec00/pkgs/applications/science/logic/klee/default.nix#L48
Currently we're not building klee-uclibc as I ran into some weird
issues with it, but that's next on my todo list.
I'm hoping that this package dramatically reduces the barrier to entry
to using KLEE. If users have Nix or are running NixOS, they should
just be able to use `nix-shell -p klee` or `nix-shell -p
'klee.override {debug = true;}'` or whatever they want to drop into a
shell with KLEE available.
Morgan
On Sat, Jan 8, 2022 at 2:49 PM Morgan wrote:
Somewhat related, I'm having trouble building KLEE on aarch64. Here's
the failing part:
-- Build files have been written to: /build/source/build
cmake: enabled parallel building
building
build flags: -j4 -l4
SHELL=/nix/store/fbf5n09drbi3bxv9rb9fgf58dm4da4a8-bash-5.1-p12/bin/bash
[ 1%] Building CXX object lib/Basic/CMakeFiles/kleeBasic.dir/KTest.cpp.o
[ 1%] Building CXX object
lib/Support/CMakeFiles/kleeSupport.dir/CompressionStream.cpp.o
[ 1%] Building CXX object lib/Expr/CMakeFiles/kleaverExpr.dir/ArrayCache.cpp.o
[ 1%] Building C object
runtime/Runtest/CMakeFiles/kleeRuntest.dir/intrinsics.c.o
[ 1%] Building CXX object
runtime/Runtest/CMakeFiles/kleeRuntest.dir/__/__/lib/Basic/KTest.cpp.o
[ 1%] Building CXX object lib/Basic/CMakeFiles/kleeBasic.dir/Statistics.cpp.o
[ 1%] Linking CXX shared library ../../lib/libkleeRuntest.so
[ 1%] Built target kleeRuntest
[ 1%] Building CXX object
lib/Support/CMakeFiles/kleeSupport.dir/ErrorHandling.cpp.o
[ 1%] Linking CXX static library ../libkleeBasic.a
[ 1%] Built target kleeBasic
[ 1%] Building CXX object
lib/Expr/CMakeFiles/kleaverExpr.dir/ArrayExprOptimizer.cpp.o
[ 2%] Generating memset64_Release.bc
[ 2%] Generating stubs64_Release.bc
[ 2%] Building CXX object
lib/Support/CMakeFiles/kleeSupport.dir/FileHandling.cpp.o
[ 2%] Generating fortify-fs64_Release.bc
[ 2%] Generating memcmp64_Release.bc
[ 2%] Generating fd64_Release.bc
[ 3%] Generating memcpy64_Release.bc
/build/source/runtime/POSIX/fd.c:98:18: error: use of undeclared
identifier '__NR_access'
return syscall(__NR_access, __concretize_string(pathname), mode);
^
/build/source/runtime/POSIX/fd.c:194:25: error: use of undeclared
identifier '__NR_open'; did you mean '__fd_open'?
int os_fd = syscall(__NR_open, __concretize_string(pathname), flags, mode);
^
__fd_open
/build/source/runtime/POSIX/fd.c:141:5: note: '__fd_open' declared here
int __fd_open(const char *pathname, int flags, mode_t mode) {
^
/build/source/runtime/POSIX/fd.c:286:18: error: use of undeclared
identifier '__NR_utimes'
return syscall(__NR_utimes, __concretize_string(path), times);
^
/build/source/runtime/POSIX/fd.c:308:18: error: use of undeclared
identifier '__NR_futimesat'
return syscall(__NR_futimesat, (long)fd,
<...>
Is there some syscall-relevant include I'm missing?
Morgan
On Sat, Jan 8, 2022 at 2:19 PM Morgan wrote:
Is this also the issue you ran into? If yes, maybe you want try the
patches from the PR I linked above. If not and are you having a
different problem, maybe you could try to provide some more details?
Then I will try and see if can help resolve them.
This is the problem. No tests discovered. That patch fixed it, thanks a ton!
Hydra will be running the full KLEE system and unit test suite from now on.
Morgan
On Wed, Jan 5, 2022 at 2:48 AM Cristian Cadar wrote:
Hi all,
Indeed, it would be great to update
https://klee.github.io/getting-started/ (via a PR at
https://github.com/klee/klee.github.io) to mention the Fedora and Nix
packages. And thanks to everyone who is maintaining KLEE packages!
Best,
Cristian
On 05/01/2022 10:01, Julian Büning wrote:
Hi Lukas,
nice and thanks for letting me know!
I was briefly considering to go the same route, but didn't encounter
your fix. But as it turns out, not using gtest_main (which I understand
is more or less offered for convenience) has certain other advantages
for KLEE (e.g. stack traces; reducing the number of
Re: [klee-dev] Packaging klee on Nix - gtest broken?
Also, do these build flags look halfway reasonable? Is there anything
that users should be able to customize? In Nix, all packages are
functions, and we can call the functions with various extra arguments
(like debug ? false) in the package.
https://github.com/NixOS/nixpkgs/blob/5f8f72c10c43514a4e9093efb9029cf3f8a9ec00/pkgs/applications/science/logic/klee/default.nix#L48
Currently we're not building klee-uclibc as I ran into some weird
issues with it, but that's next on my todo list.
I'm hoping that this package dramatically reduces the barrier to entry
to using KLEE. If users have Nix or are running NixOS, they should
just be able to use `nix-shell -p klee` or `nix-shell -p
'klee.override {debug = true;}'` or whatever they want to drop into a
shell with KLEE available.
Morgan
On Sat, Jan 8, 2022 at 2:49 PM Morgan wrote:
>
> Somewhat related, I'm having trouble building KLEE on aarch64. Here's
> the failing part:
>
> -- Build files have been written to: /build/source/build
> cmake: enabled parallel building
> building
> build flags: -j4 -l4
> SHELL=/nix/store/fbf5n09drbi3bxv9rb9fgf58dm4da4a8-bash-5.1-p12/bin/bash
> [ 1%] Building CXX object lib/Basic/CMakeFiles/kleeBasic.dir/KTest.cpp.o
> [ 1%] Building CXX object
> lib/Support/CMakeFiles/kleeSupport.dir/CompressionStream.cpp.o
> [ 1%] Building CXX object
> lib/Expr/CMakeFiles/kleaverExpr.dir/ArrayCache.cpp.o
> [ 1%] Building C object
> runtime/Runtest/CMakeFiles/kleeRuntest.dir/intrinsics.c.o
> [ 1%] Building CXX object
> runtime/Runtest/CMakeFiles/kleeRuntest.dir/__/__/lib/Basic/KTest.cpp.o
> [ 1%] Building CXX object lib/Basic/CMakeFiles/kleeBasic.dir/Statistics.cpp.o
> [ 1%] Linking CXX shared library ../../lib/libkleeRuntest.so
> [ 1%] Built target kleeRuntest
> [ 1%] Building CXX object
> lib/Support/CMakeFiles/kleeSupport.dir/ErrorHandling.cpp.o
> [ 1%] Linking CXX static library ../libkleeBasic.a
> [ 1%] Built target kleeBasic
> [ 1%] Building CXX object
> lib/Expr/CMakeFiles/kleaverExpr.dir/ArrayExprOptimizer.cpp.o
> [ 2%] Generating memset64_Release.bc
> [ 2%] Generating stubs64_Release.bc
> [ 2%] Building CXX object
> lib/Support/CMakeFiles/kleeSupport.dir/FileHandling.cpp.o
> [ 2%] Generating fortify-fs64_Release.bc
> [ 2%] Generating memcmp64_Release.bc
> [ 2%] Generating fd64_Release.bc
> [ 3%] Generating memcpy64_Release.bc
> /build/source/runtime/POSIX/fd.c:98:18: error: use of undeclared
> identifier '__NR_access'
> return syscall(__NR_access, __concretize_string(pathname), mode);
> ^
> /build/source/runtime/POSIX/fd.c:194:25: error: use of undeclared
> identifier '__NR_open'; did you mean '__fd_open'?
> int os_fd = syscall(__NR_open, __concretize_string(pathname), flags,
> mode);
> ^
> __fd_open
> /build/source/runtime/POSIX/fd.c:141:5: note: '__fd_open' declared here
> int __fd_open(const char *pathname, int flags, mode_t mode) {
> ^
> /build/source/runtime/POSIX/fd.c:286:18: error: use of undeclared
> identifier '__NR_utimes'
> return syscall(__NR_utimes, __concretize_string(path), times);
> ^
> /build/source/runtime/POSIX/fd.c:308:18: error: use of undeclared
> identifier '__NR_futimesat'
> return syscall(__NR_futimesat, (long)fd,
>
> <...>
>
> Is there some syscall-relevant include I'm missing?
>
> Morgan
>
>
> On Sat, Jan 8, 2022 at 2:19 PM Morgan wrote:
> >
> > >Is this also the issue you ran into? If yes, maybe you want try the
> > >patches from the PR I linked above. If not and are you having a
> > >different problem, maybe you could try to provide some more details?
> > >Then I will try and see if can help resolve them.
> >
> > This is the problem. No tests discovered. That patch fixed it, thanks a ton!
> > Hydra will be running the full KLEE system and unit test suite from now on.
> >
> >
> > Morgan
> >
> > On Wed, Jan 5, 2022 at 2:48 AM Cristian Cadar
> > wrote:
> > >
> > > Hi all,
> > >
> > > Indeed, it would be great to update
> > > https://klee.github.io/getting-started/ (via a PR at
> > > https://github.com/klee/klee.github.io) to mention the Fedora and Nix
> > > packages. And thanks to everyone who is maintaining KLEE packages!
> > >
> > > Best,
> > > Cristian
> > >
> > > On 05/01/2022 10:01, Julian Büning wrote:
> > > > Hi Lukas,
> > > >
> > > > nice and thanks for letting me know!
> > > >
> > > > I was briefly considering to go the same route, but didn't encounter
> > > > your fix. But as it turns out, not using gtest_main (which I understand
> > > > is more or less offered for convenience) has certain other advantages
> > > > for KLEE (e.g. stack traces; reducing the number of combinations between
> > > > vanilla Google Test, LLVM's Google Test, llvm-lit, and their respective
> > > > versions). Still, it's certainly a nice addition for llvm-lit, hopefully
> > > > somebody with commit access will pick it up soon!
> > > >
> > > > Thanks to your email I also found out that there is
Re: [klee-dev] Packaging klee on Nix - gtest broken?
Somewhat related, I'm having trouble building KLEE on aarch64. Here's
the failing part:
-- Build files have been written to: /build/source/build
cmake: enabled parallel building
building
build flags: -j4 -l4
SHELL=/nix/store/fbf5n09drbi3bxv9rb9fgf58dm4da4a8-bash-5.1-p12/bin/bash
[ 1%] Building CXX object lib/Basic/CMakeFiles/kleeBasic.dir/KTest.cpp.o
[ 1%] Building CXX object
lib/Support/CMakeFiles/kleeSupport.dir/CompressionStream.cpp.o
[ 1%] Building CXX object lib/Expr/CMakeFiles/kleaverExpr.dir/ArrayCache.cpp.o
[ 1%] Building C object
runtime/Runtest/CMakeFiles/kleeRuntest.dir/intrinsics.c.o
[ 1%] Building CXX object
runtime/Runtest/CMakeFiles/kleeRuntest.dir/__/__/lib/Basic/KTest.cpp.o
[ 1%] Building CXX object lib/Basic/CMakeFiles/kleeBasic.dir/Statistics.cpp.o
[ 1%] Linking CXX shared library ../../lib/libkleeRuntest.so
[ 1%] Built target kleeRuntest
[ 1%] Building CXX object
lib/Support/CMakeFiles/kleeSupport.dir/ErrorHandling.cpp.o
[ 1%] Linking CXX static library ../libkleeBasic.a
[ 1%] Built target kleeBasic
[ 1%] Building CXX object
lib/Expr/CMakeFiles/kleaverExpr.dir/ArrayExprOptimizer.cpp.o
[ 2%] Generating memset64_Release.bc
[ 2%] Generating stubs64_Release.bc
[ 2%] Building CXX object
lib/Support/CMakeFiles/kleeSupport.dir/FileHandling.cpp.o
[ 2%] Generating fortify-fs64_Release.bc
[ 2%] Generating memcmp64_Release.bc
[ 2%] Generating fd64_Release.bc
[ 3%] Generating memcpy64_Release.bc
/build/source/runtime/POSIX/fd.c:98:18: error: use of undeclared
identifier '__NR_access'
return syscall(__NR_access, __concretize_string(pathname), mode);
^
/build/source/runtime/POSIX/fd.c:194:25: error: use of undeclared
identifier '__NR_open'; did you mean '__fd_open'?
int os_fd = syscall(__NR_open, __concretize_string(pathname), flags, mode);
^
__fd_open
/build/source/runtime/POSIX/fd.c:141:5: note: '__fd_open' declared here
int __fd_open(const char *pathname, int flags, mode_t mode) {
^
/build/source/runtime/POSIX/fd.c:286:18: error: use of undeclared
identifier '__NR_utimes'
return syscall(__NR_utimes, __concretize_string(path), times);
^
/build/source/runtime/POSIX/fd.c:308:18: error: use of undeclared
identifier '__NR_futimesat'
return syscall(__NR_futimesat, (long)fd,
<...>
Is there some syscall-relevant include I'm missing?
Morgan
On Sat, Jan 8, 2022 at 2:19 PM Morgan wrote:
>
> >Is this also the issue you ran into? If yes, maybe you want try the
> >patches from the PR I linked above. If not and are you having a
> >different problem, maybe you could try to provide some more details?
> >Then I will try and see if can help resolve them.
>
> This is the problem. No tests discovered. That patch fixed it, thanks a ton!
> Hydra will be running the full KLEE system and unit test suite from now on.
>
>
> Morgan
>
> On Wed, Jan 5, 2022 at 2:48 AM Cristian Cadar wrote:
> >
> > Hi all,
> >
> > Indeed, it would be great to update
> > https://klee.github.io/getting-started/ (via a PR at
> > https://github.com/klee/klee.github.io) to mention the Fedora and Nix
> > packages. And thanks to everyone who is maintaining KLEE packages!
> >
> > Best,
> > Cristian
> >
> > On 05/01/2022 10:01, Julian Büning wrote:
> > > Hi Lukas,
> > >
> > > nice and thanks for letting me know!
> > >
> > > I was briefly considering to go the same route, but didn't encounter
> > > your fix. But as it turns out, not using gtest_main (which I understand
> > > is more or less offered for convenience) has certain other advantages
> > > for KLEE (e.g. stack traces; reducing the number of combinations between
> > > vanilla Google Test, LLVM's Google Test, llvm-lit, and their respective
> > > versions). Still, it's certainly a nice addition for llvm-lit, hopefully
> > > somebody with commit access will pick it up soon!
> > >
> > > Thanks to your email I also found out that there is actually a Fedora
> > > package for KLEE in the main repository. Awesome! I'm not sure how I
> > > missed that. You should definitely get it mentioned on klee.github.io!
> > >
> > > Best,
> > > Julian
> > >
> > > On 1/5/22 10:15, Lukas Zaoral wrote:
> > >> Hi Julian,
> > >> I've encountered the same problem with lit and latest gtest when
> > >> I was packaging KLEE for Fedora as I had to use gtest from repos
> > >> due to Fedora's packaging guidelines.
> > >>
> > >> I sent a patch to LLVM to fix this incompatibility at the beginning
> > >> of last April and it was finally accepted last month [1]. It still needs
> > >> to be committed, though.
> > >>
> > >> Sincerely,
> > >> Lukas
> > >>
> > >> [1] https://reviews.llvm.org/D100043
> > >>
> > >> On Wed, Jan 5, 2022 at 9:44 AM Julian Büning
> > >> wrote:
> > >>>
> > >>> Hi Morgan,
> > >>>
> > >>> nice to see your packaging efforts for KLEE!
> > >>>
> > >>> I recently ran into some issues with more recent versions of Google Test
> > >>> when building KLEE (and running unit tests). I just
Re: [klee-dev] Packaging klee on Nix - gtest broken?
>Is this also the issue you ran into? If yes, maybe you want try the >patches from the PR I linked above. If not and are you having a >different problem, maybe you could try to provide some more details? >Then I will try and see if can help resolve them. This is the problem. No tests discovered. That patch fixed it, thanks a ton! Hydra will be running the full KLEE system and unit test suite from now on. Morgan On Wed, Jan 5, 2022 at 2:48 AM Cristian Cadar wrote: > > Hi all, > > Indeed, it would be great to update > https://klee.github.io/getting-started/ (via a PR at > https://github.com/klee/klee.github.io) to mention the Fedora and Nix > packages. And thanks to everyone who is maintaining KLEE packages! > > Best, > Cristian > > On 05/01/2022 10:01, Julian Büning wrote: > > Hi Lukas, > > > > nice and thanks for letting me know! > > > > I was briefly considering to go the same route, but didn't encounter > > your fix. But as it turns out, not using gtest_main (which I understand > > is more or less offered for convenience) has certain other advantages > > for KLEE (e.g. stack traces; reducing the number of combinations between > > vanilla Google Test, LLVM's Google Test, llvm-lit, and their respective > > versions). Still, it's certainly a nice addition for llvm-lit, hopefully > > somebody with commit access will pick it up soon! > > > > Thanks to your email I also found out that there is actually a Fedora > > package for KLEE in the main repository. Awesome! I'm not sure how I > > missed that. You should definitely get it mentioned on klee.github.io! > > > > Best, > > Julian > > > > On 1/5/22 10:15, Lukas Zaoral wrote: > >> Hi Julian, > >> I've encountered the same problem with lit and latest gtest when > >> I was packaging KLEE for Fedora as I had to use gtest from repos > >> due to Fedora's packaging guidelines. > >> > >> I sent a patch to LLVM to fix this incompatibility at the beginning > >> of last April and it was finally accepted last month [1]. It still needs > >> to be committed, though. > >> > >> Sincerely, > >> Lukas > >> > >> [1] https://reviews.llvm.org/D100043 > >> > >> On Wed, Jan 5, 2022 at 9:44 AM Julian Büning > >> wrote: > >>> > >>> Hi Morgan, > >>> > >>> nice to see your packaging efforts for KLEE! > >>> > >>> I recently ran into some issues with more recent versions of Google Test > >>> when building KLEE (and running unit tests). I just opened a PR that > >>> addresses these: https://github.com/klee/klee/pull/1458 > >>> > >>> Among these issues is one that I image you may also have run into (as I > >>> assume your package will not be built against Google Test 1.7.0), but it > >>> differs quite a bit from the issue that you linked. Thus, I will go > >>> ahead and describe what I experienced (hoping you can tell me if that > >>> matches what you saw). > >>> > >>> When building KLEE with Google Test 1.7.0 and running the unit tests, I > >>> get 36 successfully passed tests. When instead using a newer Google Test > >>> version, like 1.11.0, I get the same number of passed tests, but the > >>> following 10 unresolved tests in addition: > >>> > >>> Unresolved Tests (10): > >>> KLEE Unit tests :: ./AssignmentTest/Running main() from > >>> /some/absolute/path/to/gtest_main.cc > >>> KLEE Unit tests :: ./DiscretePDFTest/Running main() from > >>> /some/absolute/path/to/gtest_main.cc > >>> KLEE Unit tests :: ./ExprTest/Running main() from > >>> /some/absolute/path/to/gtest_main.cc > >>> KLEE Unit tests :: ./RNGTest/Running main() from > >>> /some/absolute/path/to/gtest_main.cc > >>> KLEE Unit tests :: ./RefTest/Running main() from > >>> /some/absolute/path/to/gtest_main.cc > >>> KLEE Unit tests :: ./SearcherTest/Running main() from > >>> /some/absolute/path/to/gtest_main.cc > >>> KLEE Unit tests :: ./SolverTest/Running main() from > >>> /some/absolute/path/to/gtest_main.cc > >>> KLEE Unit tests :: ./TimeTest/Running main() from > >>> /some/absolute/path/to/gtest_main.cc > >>> KLEE Unit tests :: ./TreeStreamTest/Running main() from > >>> /some/absolute/path/to/gtest_main.cc > >>> KLEE Unit tests :: ./Z3SolverTest/Running main() from > >>> /some/absolute/path/to/gtest_main.cc > >>> > >>> For each of these "tests" I see some earlier output like this: > >>> > >>> UNRESOLVED: KLEE Unit tests :: ./AssignmentTest/Running main() from > >>> /some/absolute/path/to/gtest_main.cc (1 of 46) > >>> TEST 'KLEE Unit tests :: ./AssignmentTest/Running > >>> main() from /some/absolute/path/to/gtest_main.cc' FAILED > >>> > >>> Unable to find '[ PASSED ] 1 test.' in gtest output: > >>> > >>> Running main() from /some/absolute/path/to/gtest_main.cc > >>> Note: Google Test filter = Running main() from > >>> /some/absolute/path/to/gtest_main.cc > >>> [==] Running 0 tests from 0 test cases. > >>> [==] 0 tests from 0 test cases ran. (0 ms total) > >>> [ PASSED ] 0 tests. > >>> > >>> > >>> >
Re: [klee-dev] Packaging klee on Nix - gtest broken?
Hi all, Indeed, it would be great to update https://klee.github.io/getting-started/ (via a PR at https://github.com/klee/klee.github.io) to mention the Fedora and Nix packages. And thanks to everyone who is maintaining KLEE packages! Best, Cristian On 05/01/2022 10:01, Julian Büning wrote: Hi Lukas, nice and thanks for letting me know! I was briefly considering to go the same route, but didn't encounter your fix. But as it turns out, not using gtest_main (which I understand is more or less offered for convenience) has certain other advantages for KLEE (e.g. stack traces; reducing the number of combinations between vanilla Google Test, LLVM's Google Test, llvm-lit, and their respective versions). Still, it's certainly a nice addition for llvm-lit, hopefully somebody with commit access will pick it up soon! Thanks to your email I also found out that there is actually a Fedora package for KLEE in the main repository. Awesome! I'm not sure how I missed that. You should definitely get it mentioned on klee.github.io! Best, Julian On 1/5/22 10:15, Lukas Zaoral wrote: Hi Julian, I've encountered the same problem with lit and latest gtest when I was packaging KLEE for Fedora as I had to use gtest from repos due to Fedora's packaging guidelines. I sent a patch to LLVM to fix this incompatibility at the beginning of last April and it was finally accepted last month [1]. It still needs to be committed, though. Sincerely, Lukas [1] https://reviews.llvm.org/D100043 On Wed, Jan 5, 2022 at 9:44 AM Julian Büning wrote: Hi Morgan, nice to see your packaging efforts for KLEE! I recently ran into some issues with more recent versions of Google Test when building KLEE (and running unit tests). I just opened a PR that addresses these: https://github.com/klee/klee/pull/1458 Among these issues is one that I image you may also have run into (as I assume your package will not be built against Google Test 1.7.0), but it differs quite a bit from the issue that you linked. Thus, I will go ahead and describe what I experienced (hoping you can tell me if that matches what you saw). When building KLEE with Google Test 1.7.0 and running the unit tests, I get 36 successfully passed tests. When instead using a newer Google Test version, like 1.11.0, I get the same number of passed tests, but the following 10 unresolved tests in addition: Unresolved Tests (10): KLEE Unit tests :: ./AssignmentTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./DiscretePDFTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./ExprTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./RNGTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./RefTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./SearcherTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./SolverTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./TimeTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./TreeStreamTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./Z3SolverTest/Running main() from /some/absolute/path/to/gtest_main.cc For each of these "tests" I see some earlier output like this: UNRESOLVED: KLEE Unit tests :: ./AssignmentTest/Running main() from /some/absolute/path/to/gtest_main.cc (1 of 46) TEST 'KLEE Unit tests :: ./AssignmentTest/Running main() from /some/absolute/path/to/gtest_main.cc' FAILED Unable to find '[ PASSED ] 1 test.' in gtest output: Running main() from /some/absolute/path/to/gtest_main.cc Note: Google Test filter = Running main() from /some/absolute/path/to/gtest_main.cc [==] Running 0 tests from 0 test cases. [==] 0 tests from 0 test cases ran. (0 ms total) [ PASSED ] 0 tests. The last 3 lines look similar to the output in the issue you linked. But this is simply the output of Google Test when there are no `TEST()`s next to `main()` in an executable. The rest stems from a different problem (detailed below). Is this also the issue you ran into? If yes, maybe you want try the patches from the PR I linked above. If not and are you having a different problem, maybe you could try to provide some more details? Then I will try and see if can help resolve them. --- BEGIN: More details --- The issue we see above actually stems from llvm-lit, not from Google Test itself. Starting from 1.8.1, Google Test's gtest_main.cc uses `__FILE__` [1] instead of a fixed string [2] to output a line like this: > Running main() from /some/absolute/path/to/gtest_main.cc To determine which tests exist, llvm-lit will call each executable with the `--gtest_list_tests` argument. However, the (usually) first line will be the above "Running main()" output. To
Re: [klee-dev] Packaging klee on Nix - gtest broken?
Hi Lukas, nice and thanks for letting me know! I was briefly considering to go the same route, but didn't encounter your fix. But as it turns out, not using gtest_main (which I understand is more or less offered for convenience) has certain other advantages for KLEE (e.g. stack traces; reducing the number of combinations between vanilla Google Test, LLVM's Google Test, llvm-lit, and their respective versions). Still, it's certainly a nice addition for llvm-lit, hopefully somebody with commit access will pick it up soon! Thanks to your email I also found out that there is actually a Fedora package for KLEE in the main repository. Awesome! I'm not sure how I missed that. You should definitely get it mentioned on klee.github.io! Best, Julian On 1/5/22 10:15, Lukas Zaoral wrote: Hi Julian, I've encountered the same problem with lit and latest gtest when I was packaging KLEE for Fedora as I had to use gtest from repos due to Fedora's packaging guidelines. I sent a patch to LLVM to fix this incompatibility at the beginning of last April and it was finally accepted last month [1]. It still needs to be committed, though. Sincerely, Lukas [1] https://reviews.llvm.org/D100043 On Wed, Jan 5, 2022 at 9:44 AM Julian Büning wrote: Hi Morgan, nice to see your packaging efforts for KLEE! I recently ran into some issues with more recent versions of Google Test when building KLEE (and running unit tests). I just opened a PR that addresses these: https://github.com/klee/klee/pull/1458 Among these issues is one that I image you may also have run into (as I assume your package will not be built against Google Test 1.7.0), but it differs quite a bit from the issue that you linked. Thus, I will go ahead and describe what I experienced (hoping you can tell me if that matches what you saw). When building KLEE with Google Test 1.7.0 and running the unit tests, I get 36 successfully passed tests. When instead using a newer Google Test version, like 1.11.0, I get the same number of passed tests, but the following 10 unresolved tests in addition: Unresolved Tests (10): KLEE Unit tests :: ./AssignmentTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./DiscretePDFTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./ExprTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./RNGTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./RefTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./SearcherTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./SolverTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./TimeTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./TreeStreamTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./Z3SolverTest/Running main() from /some/absolute/path/to/gtest_main.cc For each of these "tests" I see some earlier output like this: UNRESOLVED: KLEE Unit tests :: ./AssignmentTest/Running main() from /some/absolute/path/to/gtest_main.cc (1 of 46) TEST 'KLEE Unit tests :: ./AssignmentTest/Running main() from /some/absolute/path/to/gtest_main.cc' FAILED Unable to find '[ PASSED ] 1 test.' in gtest output: Running main() from /some/absolute/path/to/gtest_main.cc Note: Google Test filter = Running main() from /some/absolute/path/to/gtest_main.cc [==] Running 0 tests from 0 test cases. [==] 0 tests from 0 test cases ran. (0 ms total) [ PASSED ] 0 tests. The last 3 lines look similar to the output in the issue you linked. But this is simply the output of Google Test when there are no `TEST()`s next to `main()` in an executable. The rest stems from a different problem (detailed below). Is this also the issue you ran into? If yes, maybe you want try the patches from the PR I linked above. If not and are you having a different problem, maybe you could try to provide some more details? Then I will try and see if can help resolve them. --- BEGIN: More details --- The issue we see above actually stems from llvm-lit, not from Google Test itself. Starting from 1.8.1, Google Test's gtest_main.cc uses `__FILE__` [1] instead of a fixed string [2] to output a line like this: > Running main() from /some/absolute/path/to/gtest_main.cc To determine which tests exist, llvm-lit will call each executable with the `--gtest_list_tests` argument. However, the (usually) first line will be the above "Running main()" output. To skip this, each line is compared to "Running main() from gtest_main.cc" [3], which is a fixed string assuming the behavior of 1.8.0 and before. Hence, the line with path will be recorded as a test, and result in a corresponding call to the test executable with `--gtest_filter` set accordingly. As
Re: [klee-dev] Packaging klee on Nix - gtest broken?
Hi Julian, I've encountered the same problem with lit and latest gtest when I was packaging KLEE for Fedora as I had to use gtest from repos due to Fedora's packaging guidelines. I sent a patch to LLVM to fix this incompatibility at the beginning of last April and it was finally accepted last month [1]. It still needs to be committed, though. Sincerely, Lukas [1] https://reviews.llvm.org/D100043 On Wed, Jan 5, 2022 at 9:44 AM Julian Büning wrote: > > Hi Morgan, > > nice to see your packaging efforts for KLEE! > > I recently ran into some issues with more recent versions of Google Test > when building KLEE (and running unit tests). I just opened a PR that > addresses these: https://github.com/klee/klee/pull/1458 > > Among these issues is one that I image you may also have run into (as I > assume your package will not be built against Google Test 1.7.0), but it > differs quite a bit from the issue that you linked. Thus, I will go > ahead and describe what I experienced (hoping you can tell me if that > matches what you saw). > > When building KLEE with Google Test 1.7.0 and running the unit tests, I > get 36 successfully passed tests. When instead using a newer Google Test > version, like 1.11.0, I get the same number of passed tests, but the > following 10 unresolved tests in addition: > > Unresolved Tests (10): >KLEE Unit tests :: ./AssignmentTest/Running main() from > /some/absolute/path/to/gtest_main.cc >KLEE Unit tests :: ./DiscretePDFTest/Running main() from > /some/absolute/path/to/gtest_main.cc >KLEE Unit tests :: ./ExprTest/Running main() from > /some/absolute/path/to/gtest_main.cc >KLEE Unit tests :: ./RNGTest/Running main() from > /some/absolute/path/to/gtest_main.cc >KLEE Unit tests :: ./RefTest/Running main() from > /some/absolute/path/to/gtest_main.cc >KLEE Unit tests :: ./SearcherTest/Running main() from > /some/absolute/path/to/gtest_main.cc >KLEE Unit tests :: ./SolverTest/Running main() from > /some/absolute/path/to/gtest_main.cc >KLEE Unit tests :: ./TimeTest/Running main() from > /some/absolute/path/to/gtest_main.cc >KLEE Unit tests :: ./TreeStreamTest/Running main() from > /some/absolute/path/to/gtest_main.cc >KLEE Unit tests :: ./Z3SolverTest/Running main() from > /some/absolute/path/to/gtest_main.cc > > For each of these "tests" I see some earlier output like this: > > UNRESOLVED: KLEE Unit tests :: ./AssignmentTest/Running main() from > /some/absolute/path/to/gtest_main.cc (1 of 46) > TEST 'KLEE Unit tests :: ./AssignmentTest/Running > main() from /some/absolute/path/to/gtest_main.cc' FAILED > > Unable to find '[ PASSED ] 1 test.' in gtest output: > > Running main() from /some/absolute/path/to/gtest_main.cc > Note: Google Test filter = Running main() from > /some/absolute/path/to/gtest_main.cc > [==] Running 0 tests from 0 test cases. > [==] 0 tests from 0 test cases ran. (0 ms total) > [ PASSED ] 0 tests. > > > > The last 3 lines look similar to the output in the issue you linked. But > this is simply the output of Google Test when there are no `TEST()`s > next to `main()` in an executable. The rest stems from a different > problem (detailed below). > > Is this also the issue you ran into? If yes, maybe you want try the > patches from the PR I linked above. If not and are you having a > different problem, maybe you could try to provide some more details? > Then I will try and see if can help resolve them. > > --- BEGIN: More details --- > > The issue we see above actually stems from llvm-lit, not from Google > Test itself. Starting from 1.8.1, Google Test's gtest_main.cc uses > `__FILE__` [1] instead of a fixed string [2] to output a line like this: > > Running main() from /some/absolute/path/to/gtest_main.cc > > To determine which tests exist, llvm-lit will call each executable with > the `--gtest_list_tests` argument. However, the (usually) first line > will be the above "Running main()" output. To skip this, each line is > compared to "Running main() from gtest_main.cc" [3], which is a fixed > string assuming the behavior of 1.8.0 and before. > > Hence, the line with path will be recorded as a test, and result in a > corresponding call to the test executable with `--gtest_filter` set > accordingly. As there is no test that matches the given pattern, we see > the output shown above. As it does not include the expected "[ PASSED > ] 1 test." line, it is counted as unresolved. > > [1] > https://github.com/google/googletest/blob/release-1.8.1/googletest/src/gtest_main.cc > > [2] > https://github.com/google/googletest/blob/release-1.8.0/googletest/src/gtest_main.cc > > [3] > https://github.com/llvm/llvm-project/blob/llvmorg-13.0.0/llvm/utils/lit/lit/formats/googletest.py#L60-L64 > > --- END: More details --- > > Looking forward to your answer! > > Best, > Julian > > > > On 1/1/22 01:28, Morgan wrote: > > Hey there, > > > > I like Klee and have been
Re: [klee-dev] Packaging klee on Nix - gtest broken?
Hi Morgan, nice to see your packaging efforts for KLEE! I recently ran into some issues with more recent versions of Google Test when building KLEE (and running unit tests). I just opened a PR that addresses these: https://github.com/klee/klee/pull/1458 Among these issues is one that I image you may also have run into (as I assume your package will not be built against Google Test 1.7.0), but it differs quite a bit from the issue that you linked. Thus, I will go ahead and describe what I experienced (hoping you can tell me if that matches what you saw). When building KLEE with Google Test 1.7.0 and running the unit tests, I get 36 successfully passed tests. When instead using a newer Google Test version, like 1.11.0, I get the same number of passed tests, but the following 10 unresolved tests in addition: Unresolved Tests (10): KLEE Unit tests :: ./AssignmentTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./DiscretePDFTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./ExprTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./RNGTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./RefTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./SearcherTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./SolverTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./TimeTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./TreeStreamTest/Running main() from /some/absolute/path/to/gtest_main.cc KLEE Unit tests :: ./Z3SolverTest/Running main() from /some/absolute/path/to/gtest_main.cc For each of these "tests" I see some earlier output like this: UNRESOLVED: KLEE Unit tests :: ./AssignmentTest/Running main() from /some/absolute/path/to/gtest_main.cc (1 of 46) TEST 'KLEE Unit tests :: ./AssignmentTest/Running main() from /some/absolute/path/to/gtest_main.cc' FAILED Unable to find '[ PASSED ] 1 test.' in gtest output: Running main() from /some/absolute/path/to/gtest_main.cc Note: Google Test filter = Running main() from /some/absolute/path/to/gtest_main.cc [==] Running 0 tests from 0 test cases. [==] 0 tests from 0 test cases ran. (0 ms total) [ PASSED ] 0 tests. The last 3 lines look similar to the output in the issue you linked. But this is simply the output of Google Test when there are no `TEST()`s next to `main()` in an executable. The rest stems from a different problem (detailed below). Is this also the issue you ran into? If yes, maybe you want try the patches from the PR I linked above. If not and are you having a different problem, maybe you could try to provide some more details? Then I will try and see if can help resolve them. --- BEGIN: More details --- The issue we see above actually stems from llvm-lit, not from Google Test itself. Starting from 1.8.1, Google Test's gtest_main.cc uses `__FILE__` [1] instead of a fixed string [2] to output a line like this: > Running main() from /some/absolute/path/to/gtest_main.cc To determine which tests exist, llvm-lit will call each executable with the `--gtest_list_tests` argument. However, the (usually) first line will be the above "Running main()" output. To skip this, each line is compared to "Running main() from gtest_main.cc" [3], which is a fixed string assuming the behavior of 1.8.0 and before. Hence, the line with path will be recorded as a test, and result in a corresponding call to the test executable with `--gtest_filter` set accordingly. As there is no test that matches the given pattern, we see the output shown above. As it does not include the expected "[ PASSED ] 1 test." line, it is counted as unresolved. [1] https://github.com/google/googletest/blob/release-1.8.1/googletest/src/gtest_main.cc [2] https://github.com/google/googletest/blob/release-1.8.0/googletest/src/gtest_main.cc [3] https://github.com/llvm/llvm-project/blob/llvmorg-13.0.0/llvm/utils/lit/lit/formats/googletest.py#L60-L64 --- END: More details --- Looking forward to your answer! Best, Julian On 1/1/22 01:28, Morgan wrote: Hey there, I like Klee and have been trying to package it in nixpkgs so more people can reproducibly use it without resorting to things like setup scripts or Docker. Here are the cmake flags I'm using: https://github.com/NixOS/nixpkgs/pull/153014/files#diff-cb8d40a4e82c0c50ce6ec4031c12e06a4dac4bded86b9f01afcb2b4f22532dbbR46 Everything works including the system tests, which is a very good sign. However, I'm having trouble with the unit tests that resembles this problem: https://github.com/google/googletest/issues/2157 Has anyone else run into this? Thanks! Morgan ___ klee-dev mailing list
