Missing library functions for sv-comp

[michael-schwarz]

Definitions for the following library functions are missing:

Floats

• __builtin_uaddl_overflow / __builtin_uadd_overflow / __builtin_umull_overflow Not floats, but still (Equip float domain to handle definite NaN, +Inf, -Inf, and some missing float stubs #869)
• __isnan, __signbit, __signbitf, _isinff, __isinf, __isnanf, __finite (Equip float domain to handle definite NaN, +Inf, -Inf, and some missing float stubs #869)
• fegetround / fesetround (Equip float domain to handle definite NaN, +Inf, -Inf, and some missing float stubs #869)
• __fpclassify / __fpclassifyl / __fpclassifyf (Equip float domain to handle definite NaN, +Inf, -Inf, and some missing float stubs #869)
• __builtin_huge_val / __builtin_huge_valf (Equip float domain to handle definite NaN, +Inf, -Inf, and some missing float stubs #869)
• __builtin_isgreater / __builtin_isgreaterequal / __builtin_isless / __builtin_islessequal / __builtin_islessgreater / __builtin_isunordered (Equip float domain to handle definite NaN, +Inf, -Inf, and some missing float stubs #869)

Easy to add

• pthread_attr_destroy Add some further library functions #878
• puts Add some further library functions #878
• strspn / strcspn Add some further library functions #878
• strtoll / strtoull / strtod Add some further library functions #878
• mktime Add some further library functions #878
• clearerr Add some further library functions #878
• ctime Add some further library functions #878
• setbuf Add some further library functions #878
• ntohs Add some further library functions #878
• __builtin_popcountl Add some further library functions #878
• swprintf Add some further library functions #878

Driver / Kernel internals

• b1pcmcia_addcard_m2 / b1pcmcia_addcard_m1 / b1pcmcia_addcard_b1 (Reported upstream https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1355)
• __bad_percpu_size / __bad_size_call_parameter / __xchg_wrong_size / __cmpxchg_wrong_size / __xadd_wrong_size / __put_user_bad Add some further library functions #878
• fw_card_release (Reported upstream https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1355)
• usbnet_read_cmd_nopm / usbnet_write_cmd_nopm / usbnet_write_cmd / usbnet_read_cmd (Reported upstream https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1355)
• em28xx_free_device (Reported upstream https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1355)
• smp_send_req (Reported upstream https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1355)
• rcu_barrier_sched, rcu_barrier_bh, rcu_barrier, synchronize_rcu_expedited, synchronize_rcu_bh (Reported upstream https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1355)

LDV Stubs

• ldv_xmalloc / ldv_calloc (Should be fixed in the benchmarks: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1349)
• __VERIFIER_nondet_size_t, __VERIFIER_nondet_u16, __VERIFIER_nondet_u8, __VERIFIER_nondet_u32, __VERIFIER_nondet_loff_t, __VERIFIER_nondet_uint128, __VERIFIER_nondet_longlong, __VERIFIER_nondet_ulonglong, __VERIFIER_nondet_unsigned_char, __VERIFIER_nondet_const_char_pointer, __VERIFIER_nondet_charp Add missing __VERIFIER_nondet_X()s #886

Require deeply integrated support

• setjmp / longjmp (tracked in Soundly handle setjmp and longjmp #887)
• __atomic_store_n / __atomic_load_n (stop-gap Add library functions for __atomic_{store,load}_n #884)
• pthread_getspecific / pthread_setspecific (stop-gap First approximation of pthread_setspecific by escaping things reachable from the argument and invalidating all globals #877, tracked as Support for thread-local variables / pthread_getspecific & pthread_setspecific #876)

[sim642]

Some of the Linux ones sound like they should be fixed by defining them in the sv-benchmarks themselves.

A couple of the nondet ones are indeed also missing here:

analyzer/lib/sv-comp/stub/src/sv-comp.c

Line 25 in 0e49d1f

// __VERIFIER_nondet(loff_t)

I think the issue was that the typedef for loff_t only comes in the benchmark itself and might depend on the architecture defined for the benchmark. Although maybe all the Linux tasks have the same architecture, so we can hardcode the specific primitive type.

[michael-schwarz]

There is a separate issue for longjmp and setjmp, so I am closing this issue.