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 <m...@numin.it> 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 <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
