Invalid tasks in HeapMemSafety

[martinhruska]

Hi all,

@tautschnig and @dbeyer have currently added the following tasks

termination-crafted/LexIndexValue-Pointer_false-valid-deref.c
termination-crafted/SyntaxSupportPointer01_false-valid-deref.c
termination-crafted/Nyala-2lex_false-valid-deref.c

to the HeapMemSafety category. However, I don't see any invalid pointer dereference in these tasks. E.g. there is even no pointer manipulation in the task "termination-crafted/Nyala-2lex_false-valid-deref.c" at all. It looks that the tasks have been added to the repository by @leostrakosch.

I suppose that these tasks have been derived from the same tasks with _true-termination suffix on fixing the undefined behavior in the original tasks. The programs were left in the benchmark as false cases but maybe with incorrect property (i.e., invalid dereference). Am I right or is there any invalid pointer dereference that I have not noticed? If the tasks are in the HeapMemSafety by mistake I would like to propose to remove them.

[lembergerth]

I suppose that these tasks have been derived from the same tasks with _true-termination suffix on fixing the undefined behavior in the original tasks. The programs were left in the benchmark as false cases but maybe with incorrect property (i.e., invalid dereference).

Yes, that's the case.
At the time of #183 and related PRs I kept almost all original files, adding property false-valid-deref because no better fitting label existed at that time.
They were not added to any category though and just kept in case we want to use them later, but it was my fault for not using some placeholder-label instead.

So all false-valid-deref files added in PRs #183 #182 #181 #177 and #171 should not be considered as real false-valid-derefs (but then again, that doesn't mean that there are not a few).

[martinhruska]

@leostrakosch thank you for your response. So should I prepare a pull request removing the tasks
termination-crafted/LexIndexValue-Pointer_false-valid-deref.c termination-crafted/SyntaxSupportPointer01_false-valid-deref.c termination-crafted/Nyala-2lex_false-valid-deref.c array-examples/relax_false-valid-deref.i
from the HeapMemSafety category to fix the issue?

[mikhailramalho]

This is a duplicate of #262 and #274.

I actually changed LexIndexValue-Pointer_false-valid-deref.c, SyntaxSupportPointer01_false-valid-deref.c and array-examples/relax_false-valid-deref.i on pull request #296. Instead of remove those, can I suggest we revert my changes and relabel them to false-valid-free? There are also underflows on the postdecrement operations, so we might want to add that as well.

About LexIndexValue-Pointer_false-valid-deref.c, I think it might be correct labelled. Consider the following, 'q' is incremented 1048 times (nondet_int() returns true 1048 times), the loop condition dereferences 'q' (*q >= 0), which is an out-of-bounds access.

[lembergerth]

So should I prepare a pull request removing the tasks
termination-crafted/LexIndexValue-Pointer_false-valid-deref.c termination-crafted/SyntaxSupportPointer01_false-valid-deref.c termination-crafted/Nyala-2lex_false-valid-deref.c array-examples/relax_false-valid-deref.i
from the HeapMemSafety category to fix the issue?

These tasks were added only lately in b21675b , I presume with the intent that we don't have any unclassified/unused files lying around.
But until #261 is resolved, this is not possible on master without losing the information that these tasks have undefined behavior.

So my suggestion would be to keep all these incorrectly introduced false-valid-deref files (there are some from other directories, too) with some new file name-tag in a branch and delete them on master, for now.
@dbeyer @PhilippWendler @tautschnig How do you think about the above?

And @mikhailramalho

Consider the following, 'q' is incremented 1048 times (nondet_int() returns true 1048 times), the loop condition dereferences 'q' (*q >= 0), which is an out-of-bounds access.

Does the second condition q < p + 1048 * sizeof(int) not take care of that?

[ For quick access: LexIndexValue-Pointer_false-valid-deref.c ]

[mikhailramalho]

Hi @leostrakosch,

Does the second condition q < p + 1048 * sizeof(int) not take care of that?

Only if it is evaluated before (*q >= 0).

I checked it with clang's address sanitizer and it finds a buffer overflow. I used a slightly modified version of the program, to better localize the bug (program). As you can see, it complains about line 22, the (*q >= 0).

$ clang termination-crafted/LexIndexValue-Pointer_false-valid-deref.c -g -fsanitize=address
$ ./a.out 
=================================================================
==29733==ERROR: AddressSanitizer: heap-buffer-overflow on address 0x62100001dd60 at pc 0x0000004e4cc5 bp 0x7ffe41e24cb0 sp 0x7ffe41e24ca8
READ of size 4 at 0x62100001dd60 thread T0
    #0 0x4e4cc4 in main /home/mramalho/sv-benchmarks/c/termination-crafted/LexIndexValue-Pointer_false-valid-deref.c:22:12
    #1 0x7fc0f32bb57f in __libc_start_main (/lib64/libc.so.6+0x2057f)
    #2 0x419028 in _start (/home/mramalho/sv-benchmarks/c/a.out+0x419028)

0x62100001dd60 is located 0 bytes to the right of 4192-byte region [0x62100001cd00,0x62100001dd60)
allocated by thread T0 here:
    #0 0x4b783c in __interceptor_malloc /home/nikola/final/llvm.src/projects/compiler-rt/lib/asan/asan_malloc_linux.cc:64:3
    #1 0x4e4b5a in main /home/mramalho/sv-benchmarks/c/termination-crafted/LexIndexValue-Pointer_false-valid-deref.c:14:11
    #2 0x7fc0f32bb57f in __libc_start_main (/lib64/libc.so.6+0x2057f)

[lembergerth]

Hey,

even better then, thank you for the clarification!

So now only the question about renaming/removing the other files remains.

[mchalupa]

Just to fill in the list of related pull-requests and issues, there's the #280 PR. I also added there a list of files that are suffering (or suffered) from this mislabeling: #280 (comment)

[tautschnig]

So just to add my notes on this issue: I've rather blindly added them to categories according to their labels, only deciding between Heap vs. Array based on contents. I'm happy with any proposal that is different from "let's name them somehow and fix it later" as that has failed us before, as those files prove.

[martinhruska]

@tautschnig as you pointed in #274 there is even no undefined behavior in termination-crafted/SyntaxSupportPointer01_false-valid-deref.c so removing the test case from the benchmark may be OK. @mikhailramalho explained that termination-crafted/LexIndexValue-Pointer_false-valid-deref.c is labeled correctly since an invalid dereference is really possible. Finally, because termination-crafted/Nyala-2l ex_false-valid-deref.c contains an undefined behavior, a proper solution depends on #261. Although only renaming file is not a nice solution it would be better than leaving the task in a wrong category.

[dbeyer]

Solved by PR #314 "Fix wrong valid-deref labels".