Broken CI

[lzaoral]

Hi, merging the following PR's to your fork of KLEE should fix many warnings in its compilation and the failing CI in this repository:

• staticafi/klee#2
• staticafi/klee#3

[lzaoral]

A friendly bump.

[lzaoral]

Thanks for merging the PRs, @mchalupa. However, the CI will fail once again due to a bug in the latest release of Benchexec: https://github.com/sosy-lab/benchexec/issues/598

[mchalupa]

Hmm, not only that. There is also this issue when compiling dg:

dg/include/dg/llvm/PointerAnalysis/LLVMPointsToSet.h:131:16: error: 

      chosen constructor is explicit in copy-initialization

        return {o, l};

               ^~~~~~

[lzaoral]

That issue was fixed in https://github.com/mchalupa/dg/commit/e3a2019c1a27135e9b0f87e480b1704d7208fd66, so updating the module should be enough.

[lzaoral]

The benchexec crash has been fixed in Benchexec 3.3.

[mchalupa]

Just an update: dg and benchexec seem to work, now there's the issue with instrumentation.

/usr/bin/../lib/gcc/x86_64-linux-gnu/5.5.0/../../../../include/c++/5.5.0/bits/hashtable_policy.h:85:11: error: implicit instantiation of undefined template 'std::hash<PredatorPlugin::ErrorType>'

        noexcept(declval<const _Hash&>()(declval<const _Key&>()))>

                 ^
[....]

/usr/bin/../lib/gcc/x86_64-linux-gnu/5.5.0/../../../../include/c++/5.5.0/bits/unordered_set.h:494:7: error: multiple overloads of 'erase' instantiate to the same signature 'std::unordered_set<PredatorPlugin::ErrorType, std::hash<PredatorPlugin::ErrorType>, std::equal_to<PredatorPlugin::ErrorType>, std::allocator<PredatorPlugin::ErrorType> >::iterator (std::unordered_set<PredatorPlugin::ErrorType, std::hash<PredatorPlugin::ErrorType>, std::equal_to<PredatorPlugin::ErrorType>, std::allocator<PredatorPlugin::ErrorType> >::iterator)' (aka 'int (int)')

      erase(iterator __position)

 [....]

/usr/bin/../lib/gcc/x86_64-linux-gnu/5.5.0/../../../../include/c++/5.5.0/bits/unordered_map.h:109:36: error: no type named 'mapped_type' in 'std::_Hashtable<std::pair<unsigned int, unsigned int>, std::pair<const std::pair<unsigned int, unsigned int>, std::unordered_set<PredatorPlugin::ErrorType, std::hash<PredatorPlugin::ErrorType>, std::equal_to<PredatorPlugin::ErrorType>, std::allocator<PredatorPlugin::ErrorType> > >, std::allocator<std::pair<const std::pair<unsigned int, unsigned int>, std::unordered_set<PredatorPlugin::ErrorType, std::hash<PredatorPlugin::ErrorType>, std::equal_to<PredatorPlugin::ErrorType>, std::allocator<PredatorPlugin::ErrorType> > > >, std::__detail::_Select1st, std::equal_to<std::pair<unsigned int, unsigned int> >, PredatorPlugin::PairHash, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<true, false, true> >'

      typedef typename _Hashtable::mapped_type  mapped_type;

              ~~~~~~~~~~~~~~~~~~~~~^~~~~~~~~~~

[....]

[ 47%] Linking CXX shared module libCheckNSWPlugin.so

/home/travis/build/staticafi/symbiotic/sbt-instrumentation/analyses/predator_plugin.cpp:23:12: error: cannot initialize return object of type 'InstrPlugin *' with an rvalue of type 'PredatorPlugin *'

    return new PredatorPlugin(module);

           ^~~~~~~~~~~~~~~~~~~~~~~~~~

[lzaoral]

@mchalupa, that should be fixed by https://github.com/staticafi/sbt-instrumentation/pull/54

[lzaoral]

The CI now fails because jsoncpp recently disabled in source builds.

[lzaoral]

The only remaining problem seems to be #183.

[mchalupa]

Should be fixed now.

[lzaoral]

Thanks! A scratch of GitHub Actions is here https://github.com/lzaoral/symbiotic/commit/9877cd85916c40ab3b601090eb540df16c9039a3, when it's ready I'll make a PR. By the way, benchexec reports a fairly high amount of wrong results. Were they present when the previous CI was functional as well or are they regressions? Either way, we should probably fix them before merging.

[lzaoral]

Sorry, I forgot that benchexec actually tells the result of the verification process and not that the result is correct. It's weird though that the final statistics are empty.

[mchalupa]

It's weird though that the final statistics are empty.

My guess is that the newer versions of benchexec do not support the specification of the result in the name of the benchmark. Benchexec moved to using dedicated .yml files that hold metadata for each benchmark, so we'll probably need to do that too. An example of program and its .yml spec:

https://github.com/sosy-lab/sv-benchmarks/blob/master/c/array-cav19/array_init_var_plus_ind.c https://github.com/sosy-lab/sv-benchmarks/blob/master/c/array-cav19/array_init_var_plus_ind.yml

Or, alternatively, we can drop benchexec and move to lit. However, with lit, we would need to do the magic with -check-prefix or so as we want to test one program with several configurations - it is quite comfy handling this with benchexec. Any preferences?

[lzaoral]

Well, that depends whether we want the tests to be CI-only or whether we want them to be run by anyone on their machines (and maybe run the tests in build scripts by default).

In the latter case, I strongly prefer lit as benchexec is Linux-only and even with Linux it's a bit painful to set-up. For instance, due to cgroup-v2 being default in Fedora 31+ you cannot launch benchexec without additional changes to the kernel command-line to use cgroup-v1 (cgroup-v2 is in kernel for almost 5 years now) and even after that you have to do some manual changes¹ with permissions.

The only Linux distros where using benchexec is quite comfortable are Debian and Ubuntu as the "systemd cgroup magic" is handled by their official package.

¹ I know that Fedora uses systemd but this was the only approach that worked for me.

[lzaoral]

@mchalupa What is your opinion on this topic? Regardless of the choice of the test runner, I'll make the needed changes to fix the CI.

It looks like now you can use benchexec on any Linux distro if it has kernel 5.11+ which looks quite promising: https://github.com/sosy-lab/benchexec/commit/f8508986c85fc8dace9ea54a64e81edd02cc3b57

Edit: Well, it looks like the problems with cgroups are still present.

[mchalupa]

@lzaoral I don't have much time to rewrite the tests to lit, but if you are willing to do that, then lit is probably the better and (eventually) simpler option.

[lzaoral]

@mchalupa lit turned out to be not very suitable for our use so I wrote a very simple test runner in Python (https://github.com/lzaoral/symbiotic/blob/update-ci/tests/test_runner.py) that should be sufficient. You can see it in action here: https://github.com/lzaoral/symbiotic/runs/2992865699?check_suite_focus=true If you have any comments or suggestions, please tell me!

[mchalupa]

@lzaoral what was the problem with lit?

[lzaoral]

Writing a custom test runner was more straight-forward as I could reuse the property regexes in .set files and extract the expected outputs contained in test's file names. The script basically behaves as a very simple "drop-in" replacement of benchexec (no changes to the tests needed) that does not measure or control system resources and that can be run practically anywhere.

It is definitely possible to use lit but the conversion of the tests would require more time and I was not able to force timeouts in lit.cfg (both documentation and actual sources of lit do not mention this possibility).

[mchalupa]

I checked the code and I do not see that you handle multiple properties: some tests have multiple properties. Or am I missing something?

It is definitely possible to use lit but the conversion of the tests would require more time and I was not able to force timeouts in lit.cfg (both documentation and actual sources of lit do not mention this possibility).

btw. for timeouts, you can always use the timeout utility or --timeout switch of Symbiotic

[lzaoral]

I checked the code and I do not see that you handle multiple properties: some tests have multiple properties. Or am I missing something?

These are handled by the .set files which mimics the behaviour of benchexec so if you run ./test_runner.py reach.set memsafety.set, then terminator_true-unreach-call_true-valid-memsafety.i would be run twice for each property. In CI, this is handled by https://github.com/lzaoral/symbiotic/blob/update-ci/tests/run_tests.sh.