CBMC's pointer check results maybe conflicting?

Question

CBMC's pointer check results maybe conflicting?

Opened this issue 10 months ago · 2 comments

This is demo code for checking:

1	#include <stdio.h>
2	#include <stdlib.h>
3	#include <assert.h>
4	
5	struct insideStu{
6	    int a;
7	    int* b;
8	};
9	
10	struct testStu{
11	    char (*p)();
12	    int *b;
13	    int c;
14	    struct insideStu *inside;
15	};
16	
17	void derefPtr(char* p)
18	{
19	    scanf("%c",p);
20	}
21	
22	extern struct testStu* external_func();
23	
24	void func()
25	{
26	    struct testStu *stu = external_func();
27	    stu->c = 0x200;
28	    if(stu->inside)
29	        stu->inside->a = 0x100;
30	    stu->p();
31	    stu->c = 0x100;
32	    stu->inside->a = 0x200;
33	    derefPtr((char*)stu->b);
34	}
35	
36	int main()
37	{
38	    func();
39	    return 0;
40	}

CBMC command: cbmc test.c --pointer-check

part of output results:

test.c function func
[func.pointer_dereference.1] line 27 dereference failure: pointer NULL in stu->c: FAILURE
[func.pointer_dereference.2] line 27 dereference failure: pointer invalid in stu->c: FAILURE
[func.pointer_dereference.3] line 27 dereference failure: deallocated dynamic object in stu->c: FAILURE
[func.pointer_dereference.4] line 27 dereference failure: dead object in stu->c: FAILURE
[func.pointer_dereference.5] line 27 dereference failure: pointer outside object bounds in stu->c: FAILURE
[func.pointer_dereference.6] line 27 dereference failure: invalid integer address in stu->c: FAILURE
[func.pointer_dereference.7] line 28 dereference failure: pointer NULL in stu->inside: FAILURE
[func.pointer_dereference.8] line 28 dereference failure: pointer invalid in stu->inside: FAILURE
[func.pointer_dereference.9] line 28 dereference failure: deallocated dynamic object in stu->inside: FAILURE
[func.pointer_dereference.10] line 28 dereference failure: dead object in stu->inside: FAILURE
[func.pointer_dereference.11] line 28 dereference failure: pointer outside object bounds in stu->inside: FAILURE
[func.pointer_dereference.12] line 28 dereference failure: invalid integer address in stu->inside: FAILURE
[func.pointer_dereference.13] line 29 dereference failure: pointer NULL in stu->inside->a: FAILURE
[func.pointer_dereference.14] line 29 dereference failure: pointer invalid in stu->inside->a: FAILURE
[func.pointer_dereference.15] line 29 dereference failure: deallocated dynamic object in stu->inside->a: FAILURE
[func.pointer_dereference.16] line 29 dereference failure: dead object in stu->inside->a: FAILURE
[func.pointer_dereference.17] line 29 dereference failure: pointer outside object bounds in stu->inside->a: FAILURE
[func.pointer_dereference.18] line 29 dereference failure: invalid integer address in stu->inside->a: FAILURE
[func.pointer_dereference.19] line 30 dereference failure: pointer NULL in stu->p: FAILURE
[func.pointer_dereference.20] line 30 dereference failure: pointer invalid in stu->p: FAILURE
[func.pointer_dereference.21] line 30 dereference failure: deallocated dynamic object in stu->p: FAILURE
[func.pointer_dereference.22] line 30 dereference failure: dead object in stu->p: FAILURE
[func.pointer_dereference.23] line 30 dereference failure: pointer outside object bounds in stu->p: FAILURE
[func.pointer_dereference.24] line 30 dereference failure: invalid integer address in stu->p: FAILURE
[func.pointer_dereference.25] line 30 dereference failure: pointer NULL in stu->p: FAILURE
[func.pointer_dereference.26] line 30 dereference failure: pointer invalid in stu->p: FAILURE
[func.pointer_dereference.27] line 30 dereference failure: deallocated dynamic object in stu->p: FAILURE
[func.pointer_dereference.28] line 30 dereference failure: dead object in stu->p: FAILURE
[func.pointer_dereference.29] line 30 dereference failure: pointer outside object bounds in stu->p: FAILURE
[func.pointer_dereference.30] line 30 dereference failure: invalid integer address in stu->p: FAILURE
[func.pointer_dereference.31] line 30 no candidates for dereferenced function pointer: FAILURE
[func.pointer_dereference.32] line 31 dereference failure: pointer NULL in stu->c: SUCCESS
[func.pointer_dereference.33] line 31 dereference failure: pointer invalid in stu->c: SUCCESS
[func.pointer_dereference.34] line 31 dereference failure: deallocated dynamic object in stu->c: SUCCESS
[func.pointer_dereference.35] line 31 dereference failure: dead object in stu->c: SUCCESS
[func.pointer_dereference.36] line 31 dereference failure: pointer outside object bounds in stu->c: SUCCESS
[func.pointer_dereference.37] line 31 dereference failure: invalid integer address in stu->c: SUCCESS
[func.pointer_dereference.38] line 32 dereference failure: pointer NULL in stu->inside: SUCCESS
[func.pointer_dereference.39] line 32 dereference failure: pointer invalid in stu->inside: SUCCESS
[func.pointer_dereference.40] line 32 dereference failure: deallocated dynamic object in stu->inside: SUCCESS
[func.pointer_dereference.41] line 32 dereference failure: dead object in stu->inside: SUCCESS
[func.pointer_dereference.42] line 32 dereference failure: pointer outside object bounds in stu->inside: SUCCESS
[func.pointer_dereference.43] line 32 dereference failure: invalid integer address in stu->inside: SUCCESS
[func.pointer_dereference.44] line 32 dereference failure: pointer NULL in stu->inside->a: SUCCESS
[func.pointer_dereference.45] line 32 dereference failure: pointer invalid in stu->inside->a: SUCCESS
[func.pointer_dereference.46] line 32 dereference failure: deallocated dynamic object in stu->inside->a: SUCCESS
[func.pointer_dereference.47] line 32 dereference failure: dead object in stu->inside->a: SUCCESS
[func.pointer_dereference.48] line 32 dereference failure: pointer outside object bounds in stu->inside->a: SUCCESS
[func.pointer_dereference.49] line 32 dereference failure: invalid integer address in stu->inside->a: SUCCESS
[func.pointer_dereference.50] line 33 dereference failure: pointer NULL in stu->b: SUCCESS
[func.pointer_dereference.51] line 33 dereference failure: pointer invalid in stu->b: SUCCESS
[func.pointer_dereference.52] line 33 dereference failure: deallocated dynamic object in stu->b: SUCCESS
[func.pointer_dereference.53] line 33 dereference failure: dead object in stu->b: SUCCESS
[func.pointer_dereference.54] line 33 dereference failure: pointer outside object bounds in stu->b: SUCCESS
[func.pointer_dereference.55] line 33 dereference failure: invalid integer address in stu->b: SUCCESS

First, the result of line 27,28,29 confused me, take line 27 at first: it says that "line 27 dereference failure: pointer NULL in stu->c: FAILURE", according to structure's definition, c is not a pointer, so the result should indicate that null dereference happens when access c field from stu? If so, the result: "line 29 dereference failure: pointer NULL in stu->inside->a: FAILURE" is conflict with the check of line 28. As I cannot find any manual to parse output of checking results, could you please tell me how to understand of CBMC pointer check's result?

Second, "line 31 dereference failure: pointer NULL in stu->c: SUCCESS" is also conflict with "line 27 dereference failure: pointer NULL in stu->c: FAILURE". Does CBMC think a variable maybe secure after using of it? (like call a member function on line 30)

Finally, on line 33, stu->b as a pointer is passed to derefPtr, but CBMC think this is safe. Does CBMC take the assumption tha a pointer passed to a function call doesn't mean dereference of it? Or the source code need explicit dereference like *(stu->b) instead of stu->b?

I'd really appreciate it if someone could answer these questions.

CBMC version: 5.95.1
Operating system: Linux ae 5.15.0-91-generic #101-Ubuntu SMP Tue Nov 14 13:30:08 UTC 2023 x86_64 x86_64 x86_64 GNU/Linux
Exact command line resulting in the issue: cbmc test.c --pointer-check
What behaviour did you expect: line 30 should not pass, cbmc should not generate duplicated results
What happened instead: line 30 passed, and got duplicated results on line 29

Answer 1 · 2023-12-15T11:45:50.000Z

When we say "pointer NULL in stu->c" we refer to the attempt to dereference stu. We could perhaps present this as "pointer NULL in *stu", but then *stu does not appear in the source code, so could equally be considered confusing.

Lines 31 and beyond are considered to be unreachable, because the function pointer call in line 30 has no viable candidates.

Answer 2 · 2023-12-16T05:18:39.000Z

Thanks for the answer. Am I correct in understanding the null pointer as a subset of the invalid pointer? And on line 29 , even the var I want to use has been checked, but its source comes from uninformative and unreliable external function, thus lead to check FALSE?