[analyzer] Demonstrate superfluous unsigned >= 0 assumption

[NagyDonat]

This commit adds a testcase which highlights the current incorrect behavior of the CSA diagnostic generation: it produces a note which says "Assuming 'arg' is >= 0" in a situation where this is not a fresh assumption because 'arg' is an unsigned integer.

I also created ticket #78440 to track this bug.

[llvmbot]

@llvm/pr-subscribers-clang-static-analyzer-1

@llvm/pr-subscribers-clang

Author: None (NagyDonat)

Changes

This commit adds a testcase which highlights the current incorrect behavior of the CSA diagnostic generation: it produces a note which says "Assuming 'arg' is >= 0" in a situation where this is not a fresh assumption because 'arg' is an unsigned integer.

I also created ticket #78440 to track this bug.

---

Full diff: https://github.com/llvm/llvm-project/pull/78442.diff

1 Files Affected:

• (added) clang/test/Analysis/assuming-unsigned-ge-0.c (+19)

diff --git a/clang/test/Analysis/assuming-unsigned-ge-0.c b/clang/test/Analysis/assuming-unsigned-ge-0.c
new file mode 100644
index 00000000000000..553e68cb96c6bd
--- /dev/null
+++ b/clang/test/Analysis/assuming-unsigned-ge-0.c
@@ -0,0 +1,19 @@
+// RUN: %clang_analyze_cc1 -analyzer-output=text        \
+// RUN:     -analyzer-checker=core -verify %s
+
+int assuming_unsigned_ge_0(unsigned arg) {
+  // TODO This testcase demonstrates the current incorrect behavior of Clang
+  // Static Analyzer: here 'arg' is unsigned, so "arg >= 0" is not a fresh
+  // assumption, but it still appears in the diagnostics as if it's fresh:
+  // expected-note@+2 {{Assuming 'arg' is >= 0}}
+  // expected-note@+1 {{Taking false branch}}
+  if (arg < 0)
+    return 0;
+  // expected-note@+2 {{Assuming 'arg' is <= 0}}
+  // expected-note@+1 {{Taking false branch}}
+  if (arg > 0)
+    return 0;
+  // expected-note@+2 {{Division by zero}}
+  // expected-warning@+1 {{Division by zero}}
+  return 100 / arg;
+}

[NagyDonat]

I don't know what's the usual policy for testcases like this that demonstrate a bug: we could merge it to have an in-repository reminder (which automatically alerts us when a change fixes this issue), or we could leave it as an open pull request to avoid cluttering the repository.

[steakhal]

I'd advise against introducing a separate file for this, but I'm okay with landing tests.
Given this issue, I'd be interested to look at how difficult it is to actually fix it and commit the case along with the fix.
Have you looked at potential solutions?

[NagyDonat]

I didn't check for potential solutions yet, I wanted to document and report this ASAP and then switch to other tasks. I think I'll leave this commit here without merging it for some time, and if I don't end up resolving this within a month, then I'll find a place for this TC in some existing file.

[NagyDonat]

Thanks for the approval; I forgot about this issue a few weeks ago.

Now that you reminded me, I tried to research its cause and dropped a FIXME onto the statement that is not sound logically. Unfortunately I don't see an easy solution for this issue (apart from a ham-fisted hack that explicitly handles comparisons between unsigned values and zero as a special case).

I considered a completely different logic for the IsAssuming check: instead of checking for a change in constraints or an unknown opaque value, we could look for a branching point in the exploded graph. However, I fear that the exploded graph is complicated and a bit "magical" so implementing this completely correctly could waste lots of time.

As the only effect of this bug is a slightly inaccurate message, I feel that it's low priority and it's not worth to work on it. I think I would like to merge this testcase and FIXME (mainly to mark that this issue is already known), and then switch to different tasks.

I tried to look for an existing test file where I could place this testcase but I didn't find anything that's clearly connected to this issue, so I think it's better to keep this in a separate file. (But if you can suggest a file where I could place this, then I'm happy to do so.)

[steakhal]

Still looks good.