Task with floats: bmc incorrect false, with somehow correct test harness

[AdamZsofi]

Describe the bug gazer-bmc produces an incorrect false result when run on the following SV-Comp task (besides other, similar tasks) : float-no-simp8.i float-no-simp8.c float-no-simp8.yml

As stated in the YAML task definition, the task is true for the unreach error property, which means, that the function reach_error() should not be reachable. Somehow bmc is able to produce a test harness float-no-simp8.i.ll.txt (should be .ll, but github only supports txt), which, if compiled together with float-no-simp8.i outputs:

float-no-simp8: float-no-simp8.c:3: void reach_error(): Assertion `0' failed.
Aborted (core dumped)

(The body of reach_error contains an assert(0))

It is possible, that the task definition is wrong, but if it is, we should prove it somehow (but this is unlikely). I should note, that clang produces lots of warnings (-Wunknown-attributes), but this is probably not connected to the issue.

To Reproduce Gazer version used: 1.2.0 Running gazer to get the test harness: gazer/scripts/gazer_starter.py float-no-simp8.i Compiling and running: clang float-no-simp8.i.ll float-no-simp8.i -o float-no-simp8 && ./float-no-simp8

Expected behavior The verification should be reported as successful

Version: Gazer v1.2.0

[sallaigy]

The underlying issue here is the unsupported signbitf library function in math.h. The test harness "works" correctly because it mocks this function, giving it a behavior that will make the assertion fail. Not sure how to fix this without describing the behavior of signbitf explicitly during translation. Maybe we could blacklist known library functions in the test harness generator, so they won't be generated?

[AdamZsofi]

How would you choose/sort which functions are to be blacklisted? Would it be then more or less just a "hardcoded" list of functions after that?

[sallaigy]

Yes. I think it would make sense to blacklist everything that is a function name in the C standard library,

[AdamZsofi]

I took a look at it and it seems a bit more complicated than that. The test harnesses are not redefining the standard library functions, that we mostly use in C when writing code, rather more internal ones, which are included by the preprocessor to provide the platform and type specific functionality of the standard library functions - and there is a lot of them.

For example, if you take the task I used above: The test harness is redefining __signbitf, which is defined in the header bits/floatn.h, which is included in math.h:

/* Gather machine dependent type support.  */
#include <bits/floatn.h>

and this isn't the standard library, only a little part of math.h. (If I'm running gazer on the .c file instead of the preprocessed one, the result is the same.) It would probably be complicated to extract all of these internal helper(?) functions into a list and it would probably be really long and hard to handle (and possible portability issues can arise as well, but I'm not sure about that).

Furthermore, if we would only blacklist these from test harness generation, wouldn't that mean, that we would still have an incorrect false, if we don't check the test harness (though we do this check on SV-Comp)?

On another note, I'm still surprised, that we only had this problem with math.h functions - maybe I should try to create a task to generate the issue with other standard library functions.

[radl97]

I think that the macros or functions implemented inline in math.h are the problems. Maybe "overriding" math.h will solve the problem... (I think) We would need to change how clang works, but I know not, how to do this properly... Maybe there is a flag. But I am quite sure that it's harder to solve at LLVM's level.