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 <m.now...@imperial.ac.uk> wrote: > > Hi Morgan, > > On 17. Jan 2022, at 10:23, Morgan <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 <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 > > > 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 <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
