SV-COMP: Missing overrides mega-issue

[RyanGlScott]

crux-llvm-svcomp fails to verify certain SV-COMP programs due to missing overrides. This issue exists to categorize which functions were responsible for missing overrides most of the time. Here are the results for unreach-call:

• 78 memcmp
• 29 snprintf
• 13 fopen
• 6 fesetround (Missing floating point operations #187)
• 6 __isnan (Missing floating point operations #187)
• 5 __isinf (Missing floating point operations #187)
• 4 strcmp
• 4 __signbit (Missing floating point operations #187)
• 4 __fpclassifyf (Missing floating point operations #187)
• 3 strncpy
• 3 ldv_xmalloc
• 2 strchr
• 2 __isinff (Missing floating point operations #187)
• 2 __fpclassify (Missing floating point operations #187)
• 1 strncmp
• 1 strcpy
• 1 sprintf
• 1 smp_send_req
• 1 remainder (Missing floating point operations #187)
• 1 nan (Missing floating point operations #187)
• 1 modff (Missing floating point operations #187)
• 1 llvm.va_start (crucible-llvm: Support varargs #857)
• 1 fdim (Missing floating point operations #187)
• 1 __isnanf (Missing floating point operations #187)
• 1 __VERIFIER_nondet_ulonglong (SV-COMP: Add overrides for more __VERIFIER_nondet_* functions #842)
• 1 __VERIFIER_nondet_charp (SV-COMP: Add overrides for more __VERIFIER_nondet_* functions #842)

And for no-overflow:

• 60 memcmp
• 16 llvm.va_start (crucible-llvm: Support varargs #857)
• 2 time
• 2 strrchr
• 2 strcmp
• 2 strchr
• 1 fflush

Some of these functions have their own, more specific issues dedicated to them. For each function, I've made an effort to include a link to the relevant issue in its list entry.

Some of these may be "wontfix". For example, __VERIFIER_nondet_charp's inclusion is dubious—see #842 (comment). I'm also skeptical of the inclusion of functions like ldv_xmalloc and smp_send_req.

[travitch]

Do you have a sense for what behavior is expected for the IO operations here? Do they just "succeed" and return arbitrary bytes?

[RyanGlScott]

A good question. I took a brief look at some of the call sites for fflush and fopen in these benchmarks:

• busybox-1.22.0/hostid.c calls fflush on NULL, which flushes all open output streams. This is expected to pass on the no-overflow category, which seems reasonable I guess.
• loop-industry-pattern/aiob_1.c, loop-industry-pattern/ofuf_1.c, and friends use fopen to open a file named in.eds (which, AFAICT, doesn't exist) with r mode. If the fopen fails, there is no way to ever reach_error(). If the fopen succeeds, the rest of the program runs. As far as I can tell, nothing in the remainder of the program ever uses the FILE* that fopen returns.

Bottom line: the behavior of fopen and fflush doesn't seem to matter that much for these benchmarks. I suppose we can make them behave in whatever way is most convenient.

[robdockins]

Well, purely by the numbers, it's clear that memcmp is the biggest bang-for-buck, followed by snprintf probably.