CBMC aborts path exploration when it cannot resolve a function pointer

[celinval]

CBMC version: 5.60
Operating system: Ubuntu 18.04
Exact command line resulting in the issue: cbmc main.c
What behaviour did you expect: I expected that at least one of the assertions in this code would fail.
What happened instead: CBMC verification is successful.

This is the test case I created.

#include<assert.h>

struct PtrWrapper {
    char* value_c;
};


void fn(struct PtrWrapper wrapper) {
    assert(wrapper.value_c == 'B');
}

void indirect(int (*fn_ptr) (char*), char* data) {
    fn_ptr(data);
    assert(0);
}

int main() {
    struct PtrWrapper wrapper;
    wrapper.value_c = 'A';

    int (*alias) (char*) = (int (*) (char*)) fn;
    indirect(alias, &wrapper.value_c);
}

When I run cbmc main.c, I get the following:

** Results:
missing_fn.c function fn
[fn.assertion.1] line 9 assertion wrapper.value_c == 'B': SUCCESS

missing_fn.c function indirect
[indirect.assertion.1] line 14 assertion 0: SUCCESS

** 0 of 2 failed (1 iterations)
VERIFICATION SUCCESSFUL

If I add --pointer-check there is one failure:

no candidates for dereferenced function pointer: FAILURE

When I execute this code after compiling it with either gcc or clang, I get the following assertion failure:

missing_fn: missing_fn.c:9: fn: Assertion `wrapper.value_c == 'B'' failed.

Questions?

1. Is this function pointer conversion invalid?
2. Even if this function pointer conversion is incorrect, I would expect the assert(0) statement to be reachable. Why isn't this the case?

[tautschnig]

Is this function pointer conversion invalid?

The argument type and parameter type are not compatible, so this isn't defined behaviour in the C standard. (I will therefore also remove the "soundness" label from this issue.) CBMC does not currently think that fn is a reasonable candidate here, but we could fix this by extending function-pointer discovery rules to also accept cases where one type is T and the other is struct { T }.

Even if this function pointer conversion is incorrect, I would expect the assert(0) statement to be reachable. Why isn't this the case?

If you don't use --pointer-check when expanding function pointers, the "else" case is generated as ASSUME(false).

[celinval]

Why is it adding an assume(false)? Shouldn't the behavior at least mirror the behavior chosen by the user for missing functions?

[tautschnig]

Why is it adding an assume(false)? Shouldn't the behavior at least mirror the behavior chosen by the user for missing functions?

Fair point, though it's harder for us to produce a warning here.

[celinval]

In Kani we use assert-false-assume-false for missing functions. Would that be possible here?

[jimgrundy]

Questions:

• Do we need to introduce the weaker pointer conversion rule Michael suggested above, perhaps as an option for use with the Rust front end.
• CBMC seems to have a "closed world" approach for resolving function pointers, namely that the set of options it knows about is the full set of options. This is perhaps not good when verifying library code that will be placed in richer contexts later. Perhaps we should make that assumption flag selectable, which would change that assume(false) to an assert(false)? (or am I talking nonsense here).
• Could Kani be running with "--pointer-check"? Actually I've always felt that should be the default and people can turn it off rather than the other way around. This is hard for us to do in CBMC without fear of breaking legacy use, but Kani could do it that way and I suspect they should.

[tautschnig]

1. If rustc generates function pointer calls that involve type conversion as in the provided example then it might be more suitable for Kani to use goto-instrument --value-set-fi-fp-removal (once De-duplicate and fix code of value-set backed function pointer removal #6985 has landed). Or just wait for goto-symex now handles function pointers #6463, which delays function pointer resolution until symbolic execution. Both approaches use value sets (points-to sets) rather than a type-based choice.
2. I am working on adding a "something else" option as the "else" case for function pointer removal that would, to some extent, also address the closed-world issue. But I'm not sure this really makes a big difference over assert-false. It will, however, permit choosing assert-false-assume-false.

[celinval]

Questions:

* Do we need to introduce the weaker pointer conversion rule Michael suggested above, perhaps as an option for use with the Rust front end.

I actually don't think we need to. The use case I had in mind was to simplify our code generation, but we can (and should) just respect the C spec. My main problem is with the fact that CBMC just assume(0) at the else branch. This can lead to soundness issues if we encode anything incorrectly.

* CBMC seems to have a "closed world" approach for resolving function pointers, namely that the set of options it knows about is the full set of options. This is perhaps not good when verifying library code that will be placed in richer contexts later. Perhaps we should make that assumption flag selectable, which would change that assume(false) to an assert(false)? (or am I talking nonsense here).

That's exactly what we need. I think it would make a lot of sense to just pick whatever encoding the user chooses for missing functions definitions but we're OK with a different flag.

* Could Kani be running with "--pointer-check"? Actually I've always felt that should be the default and people can turn it off rather than the other way around. This is hard for us to do in CBMC without fear of breaking legacy use, but Kani could do it that way and I suspect they should.

We do enable --pointer-check. But for some reason I could not reproduce that yet in C.

[celinval]

I think there is a soundness issue, but it might be related to --drop-unused-functions. Using the same test in the example above. The following commands succeed even with --pointer-check.

goto-cc missing_fn.c -o missing_fn.c.1.out
goto-cc missing_fn.c.1.out --function main -o missing_fn.c.2.out
goto-instrument --drop-unused-functions missing_fn.c.2.out missing_fn.c.3.out
cbmc --pointer-check missing_fn.c.3.out

[tautschnig]

Oh, yes, in that case you'd have to use --pointer-check with goto-instrument --drop-unused-functions, because that stage will do the function pointer removal already.

[tautschnig]

#6987 now implements the proposed approach of introducing a dummy function (the behaviour of which you can configure when using --generate-function-body after having done --remove-function-pointers).

[tautschnig]

Oh, yes, in that case you'd have to use --pointer-check with goto-instrument --drop-unused-functions, because that stage will do the function pointer removal already.

#7011 at least addresses this part of the problem.

[jimgrundy]

Assigning Michael T so he can drive merging the PRs that would address this.

[celinval]

Thanks @tautschnig! #7011 addresses my main concern which was interrupting the analysis without producing any error.