search

fbrausse / esbmc

The efficient SMT-based bounded model checker
http://esbmc.org/
Other
0 stars 0 forks source link

[cheri] c2goto combinatorial state explosion #1

Closed fbrausse closed 2 years ago

fbrausse commented 2 years ago

For each of the new to-be-supported ABIs --cheri {off,hybrid,purecap}, another version of the goto-libs has to be linked. This is in addition to the 4 versions already included for --{32,64} and --{fixedbv,floatbv}, totalling then in 12. Additionally, there is the question how these libraries play together with the new --target and --sysroot options: using the cheri-clang frontend, we can only support CHERI-C on the targets it supports, i.e., the cheribsd ones {mips{,64},riscv{32,64},morello}-unknown-freebsd{,-purecap}. All are distinct from the ones CI is building for and they are also not relevant for competitions. In my opinion, the best option would be to add a feature that includes all of the c2goto/{headers,library} into the preamble before the translation units in case no c2goto library has been built for this target.

fbrausse commented 2 years ago

Oh, forgot about --cheri-uncompressed, make that ~24~ 20.

fbrausse commented 2 years ago

The hand-crafted version of __esbmc_cheri_length_get() which is based on the new bit-field support inherently depends on the endianness. This would increase the number of libraries required to 36 (twice the amount for each CHERI-C-enabled version of the libs).

fbrausse commented 2 years ago

Fixed by esbmc#581.