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 <limits.h>
> ^~~~~~~~~~
> 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 <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 <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 <m...@numin.it> 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 <m...@numin.it> 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 <c.ca...@imperial.ac.uk> 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
> <julian.buen...@rwth-aachen.de> 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 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
> klee-dev@imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev@imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev@imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev@imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev@imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
