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 (#187)
• [ ] 6 __isnan (#187)
• [ ] 5 __isinf (#187)
• [ ] 4 strcmp
• [ ] 4 __signbit (#187)
• [ ] 4 __fpclassifyf (#187)
• [ ] 3 strncpy
• [ ] 3 ldv_xmalloc
• [ ] 2 strchr
• [ ] 2 __isinff (#187)
• [ ] 2 __fpclassify (#187)
• [ ] 1 strncmp
• [ ] 1 strcpy
• [ ] 1 sprintf
• [ ] 1 smp_send_req
• [ ] 1 remainder (#187)
• [ ] 1 nan (#187)
• [ ] 1 modff (#187)
• [ ] 1 llvm.va_start (#857)
• [ ] 1 fdim (#187)
• [ ] 1 __isnanf (#187)
• [ ] 1 __VERIFIER_nondet_ulonglong (#842)
• [ ] 1 __VERIFIER_nondet_charp (#842)

And for no-overflow:

• [ ] 60 memcmp
• [ ] 16 llvm.va_start (#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 https://github.com/GaloisInc/crucible/issues/842#issuecomment-922972806. 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.