Difficulty using "assert(false)" for unimplemented functions

[danielsn]

I am trying to use assert(false) instead of return __nondet() for missing functions to increase soundness. You can see the code, and the failure, on this PR for RMC https://github.com/model-checking/rmc/pull/535/files

If I use the arguments '--generate-function-body-options', 'assert-false', '--generate-function-body', '.*', I see the expected failure for missing functions, but also references to missing standard library functions, which was unexpected. Is there a better way to do this?

<builtin-library-memset> function memset
[memset.assertion.1] assertion false: FAILURE

[SaswatPadhi]

We tried this with malloc and having #include <stdlib.h> doesn't help either.

#include <stdlib.h>

int main() {
    void *x = malloc(1);
    assert(x != 0);
}

commandline:

goto-cc test.c -o test.o
goto-instrument --generate-function-body-options assert-false --generate-function-body '.*' test.o test.2.o
cbmc test.2.o

[SaswatPadhi]

If we use --add-library first with goto-instrument, this works as expected.

int main() {
    void *x = malloc(1);  // should not be replaced by `assert(false);`
    assert(x != 0);
    void *y = mallocx(1); // should be replaced by `assert(false);`
    assert(y != 0);
}

commandline:

goto-cc test.c -o test.o
goto-instrument --add-library test.o test.1.o
goto-instrument --generate-function-body-options assert-false --generate-function-body '.*' test.1.o test.2.o
cbmc test.2.o

[jimgrundy]

Also, rather than just throwing an assert false violation it would save a lot of debug effort if we got an error of the form "undefined function reached".

[thomasspriggs]

Also, rather than just throwing an assert false violation it would save a lot of debug effort if we got an error of the form "undefined function reached".

That sounds like a worthwhile improvement, but it is slightly off track from the original problem described in this issue. I have raised a task in my team's internal tracking system, to keep track of your suggestion.

[thomasspriggs]

It seems like Saswat has managed to find a way to make the functionality you wanted work for the moment. I think that ideally we should generate an appropriate warning/suggestion if an attempt is made to generate function bodies, before the standard libraries have been linked.

[jimgrundy]

One could argue that this is a symptom of a more general issue, which is how to we ensure that folks run the steps of a transformation in the right order. We might want to look at annotating code with information about what has/has-not been done to it so we can check if further transformations are safe. There is an RFC started over on #6495 to discuss that.

Can we close this issue and pick up the discussion over there?

[tautschnig]

Just confirming that using --add-library in the same goto-instrument call together with --generate-function-body works just fine and does exactly the right thing. I will nevertheless issue two follow-up PRs:

1. Cleanup of goto-instrument to make sure that --add-library works correctly with all code transformations.
2. Adjusting the comment for the assertion generated.