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
