Function pointer removal doesn't handle NULL pointers correctly

[martin-cs]

I've got the poison, but I think @thk123 may have the remedy. It seems there are a number of problems here:

1. function pointer removal doesn't account for the possibility of NULL. Maybe we should create a __CPROVER_invalid_function_pointer() function which contains a single dereference of a NULL pointer so that the options for pointer instrumentation just work. This could then be added as an else condition on the function pointer dereference to handle all manner of pointer corruption.

2. I'm not sure why the assignment is not being handled correctly.

$ cat null-function-pointers.c
#include <assert.h>
#include <stdlib.h>

typedef void(*fp)(void);

void f00 (void) {
assert(0);
return;
}

int main (int argc, char **argv) {
fp ptr = &f00;
ptr = NULL;

ptr();

return 1;

}

$ cbmc null-function-pointers.c
CBMC version 5.6 64-bit x86_64 linux
Parsing null-function-pointers.c
Converting
Type-checking null-function-pointers
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 47 steps
simple slicing removed 7 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
404 variables, 604 clauses
SAT checker: instance is SATISFIABLE
Runtime decision procedure: 0.005s

** Results:
[f00.assertion.1] assertion 0: FAILURE

** 1 of 1 failed (1 iteration)
VERIFICATION FAILED

$ goto-instrument --remove-function-pointers --show-goto-functions null-function-pointers.goto
Reading GOTO program from `null-function-pointers.goto'
Function Pointer Removal
Virtual function removal
Java instanceof removal
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

main /* main */
// 0 file null-function-pointers.c line 12 function main
void (ptr)(void);
// 1 file null-function-pointers.c line 12 function main
ptr = f00;
// 2 file null-function-pointers.c line 13 function main
ptr = (void ()(void))(void *)0;
// 3 file null-function-pointers.c line 15 function main
ptr;
// 4 file null-function-pointers.c line 15 function main
IF ptr == f00 THEN GOTO 1
// 5 file null-function-pointers.c line 15 function main
1: f00();
// 6 file null-function-pointers.c line 17 function main
return 1;
// 7 file null-function-pointers.c line 17 function main
dead ptr;
// 8 file null-function-pointers.c line 18 function main
END_FUNCTION

[thk123]

Sorry I don't understand, this output is exactly what I would expect.

We cannot optimise away calls to ptr since it isn't const so therefore its value can (and indeed does in this example) change. Further, calling a function on a null pointer is undefined behaviour so the goto program doesn't generate cases to handle this.

[martin-cs]

On Fri, 2017-02-10 at 08:36 -0800, thk123 wrote: Sorry I don't understand, this output is exactly what I would expect. We cannot optimise away calls to ptr since it isn't const so therefore its value can (and indeed does in this example) change.

Yes. There is a similar issue in the case that your patch can be used.

Further, calling a function on a null pointer is undefined behaviour so the goto program doesn't generate cases to handle this.

The assumption of no undefined behaviour is mainly for goto-analyze. Transforms in goto-instrument should not make this assumption. Many instrumentation options for CBMC are for locating undefined behaviour. We then handle these in as graceful as way as possible. Specific issues with this code: 1. There is no "else" case in function pointer removal so that there is no way for CBMC et al. to catch that this is undefined behaviour. 2. The value of ptr is not being tracked correctly so that f00 is called (resulting in an assertion failure) despite ptr clearly *not* pointing to it.

[thk123]

OK I misunderstood the pointer about UB then... I thought if the code contained UB then we basically didn't have to worry about what output was produced.

I think therefore the two issues are the same and indeed this issue existed before any changes. I'm not sure I understand exactly what you mean about a function containing a null pointer dereference, but yeah a function __CPROVER_invalid_function_pointer() whose symbol the remove_function_pointers knows about.

• If when resolving a FP we find a null pointer (e.g. in an array) we can add that symbol into the list of possible functions.
• If we fail to resolve the FP (as we would do in this case) then in addition to all the functions that match signature we should also "match" this __CPROVER_invalid_function_pointer()
• When generating the code for the IF statements, when we find the null symbol, rather than checking it equals that (which will never happen) we check if the pointer == null.
• Also the remove_const_function_pointers should check for null not just in arrays but in any time we get down to the nitty gritty and if found add the step.

Is that essentially what you meant? I guess we could make the body of __CPROVER_invalid_function_pointer() be void_fp null_fp = 0; null_fp(); so that it amounts to the same code, but then won't we try and remove that FP?

[martin-cs]

On Fri, 2017-02-10 at 09:00 -0800, thk123 wrote: OK I misunderstood the pointer about UB then... I thought if the code contained UB then we basically didn't have to worry about what output was produced.

In general we have to worry. goto-analyze / abstract interpretation is a bit of a special case as there are some case of undefined behaviour that we need to ignore to get results that aren't just \top. For example, writing into arrays when we cannot show that the index is in range. In the strictest sense this could be undefined behaviour so we should set the domain to \top but ... if we do that we'll get junk results all of the time. So... we have to make some pragmatic calls about what undefined behaviour does. I'm trying to sort out a definitive line on this but it doesn't seem to be a well studied problem.

I think therefore the two issues are the same and indeed this issue existed before any changes.

Agreed. I simply pinged you because you were ... in the area and had a head full of the code at the moment.

I'm not sure I understand exactly what you mean about a function containing a null pointer dereference,

void __CPROVER_invalid_function_pointer (...) { int *ptr = NULL; *ptr = *ptr; return; }

--pointer-checks should find this and add an (effectively) assert(0);

but yeah a function `__CPROVER_invalid_function_pointer()` whose symbol the `remove_function_pointers` knows about.

Yes.

- If when resolving a FP we find a null pointer (e.g. in an array) we can add that symbol into the list of possible functions.

Yes.

- If we fail to resolve the FP (as we would do in this case) then in addition to all the functions that match signature we should also "match" this `__CPROVER_invalid_function_pointer()`

It should be the else case of the if ladder of possible functions.

- When generating the code for the IF statements, when we find the null symbol, rather than checking it equals that (which will never happen) we check if the pointer == null.

Have it as the else case because that handles cases where the pointer is otherwise corrupted.

- Also the `remove_const_function_pointers` should check for null not just in arrays but in any time we get down to the nitty gritty and if found add the step.

Yep.

Is that essentially what you meant?

Yes.

I guess we could make the body of `__CPROVER_invalid_function_pointer()` be `void_fp null_fp = 0; null_fp();` so that it amounts to the same code, but then won't we try and remove that FP?

Could do... there are a number of options here. As long as --pointer-check finds it and catches the case of it being corrupted / generates a counter-example trace we're good.

[thk123]

Just spotted a add_safety_assertion which asserts false if none of the IF statements match. This covers all the cases I can think of since is essentially an else and currently null pointers are ignored. This can be enabled with the flag --pointer-check is this sufficient?

For your code it would generate:

main /* main */
        // 0 file martin_code.c line 12 function main
        void (*ptr)(void);
        // 1 file martin_code.c line 12 function main
        ptr = f00;
        // 2 file martin_code.c line 13 function main
        ptr = (void (*)(void))(void *)0;
        // 3 file martin_code.c line 15 function main
        ASSERT !(POINTER_OBJECT(ptr) == POINTER_OBJECT(((void (*)(void))NULL))) // dereference failure: pointer NULL in ptr
        // 4 file martin_code.c line 15 function main
        ASSERT !INVALID-POINTER(ptr) // dereference failure: pointer invalid in ptr
        // 5 file martin_code.c line 15 function main
        ASSERT !(POINTER_OBJECT(ptr) == POINTER_OBJECT(__CPROVER_deallocated)) // dereference failure: deallocated dynamic object in ptr
        // 6 file martin_code.c line 15 function main
        ASSERT !(POINTER_OBJECT(ptr) == POINTER_OBJECT(__CPROVER_dead_object)) // dereference failure: dead object in ptr
        // 7 file martin_code.c line 15 function main
        ASSERT POINTER_OFFSET(ptr) >= 0 && __CPROVER_malloc_size >= (unsigned long int)POINTER_OFFSET(ptr) || !(POINTER_OBJECT(ptr) == POINTER_OBJECT(__CPROVER_malloc_object)) // dereference failure: pointer outside dynamic object bounds in ptr
        // 8 file martin_code.c line 15 function main
        ASSERT OBJECT_SIZE(ptr) >= POINTER_OFFSET(ptr) && POINTER_OFFSET(ptr) >= 0 || DYNAMIC_OBJECT(ptr) // dereference failure: pointer outside object bounds in ptr
        // 9 file martin_code.c line 15 function main
        ptr;
        // 10 file martin_code.c line 15 function main
        IF ptr == f00 THEN GOTO 1
        // 11 file martin_code.c line 15 function main
        ASSERT FALSE // invalid function pointer
        // 12 file martin_code.c line 15 function main
     1: f00();
        // 13 file martin_code.c line 17 function main
        main#return_value = 1;
        // 14 file martin_code.c line 17 function main
        dead ptr;
        // 15 file martin_code.c line 18 function main
        END_FUNCTION

[martin-cs]

On Fri, 2017-02-10 at 09:22 -0800, thk123 wrote: Just spotted a `add_safety_assertion` which asserts false if none of the IF statements match. This covers all the cases I can think of since is essentially an else and currently null pointers are ignored. This can be enabled with the flag `--pointer-check` is this sufficient?

Yes if you make sure that your removal code is compatible with it :-)

[thomasspriggs]

This looks to have been resolved by PR519, which is merged. Therefore I am going to close out this issue. Feel free to reopen if you think there is still work which needs to be done around this.