[PATCH] D124658: [analyzer] Canonicalize SymIntExpr so the RHS is positive when possible

[Balázs Benics via Phabricator via cfe-commits]

steakhal added a comment.

It looks good at first glance.

For the review, it would be nice to see which `clang_analyzer_dumps` and `reachables` change with the patch.
Could you mark the ones which have different results depending on whether you apply your fix or not?
E.g put a `no-warning` where we previously had a report, but now we don't.

In D124658#3481929 <https://reviews.llvm.org/D124658#3481929>, @tomasz-kaminski-sonarsource wrote:

> Without the changes, out of the following unsatisfiable conditions:
> A) `(l - 1000) > 0`
> B) `l > 1000`
> C) `l > 1000L`
> D) `(l + 0L) > 1000`
> CSA was considering A and B to satisable. The `l` is `(long)(x + 1 - 10U)` and `x` is in range `[10, 100]` so no overflow happens.

Ah, I see. It would be still nice to see a comment in the test :D

PS: we tend to use regular expression matching for masking out the number in the symbol dump: `expected-warning-re {{(reg_${{[0-9]+}}<int x>) - 1}}`



================
Comment at: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:204
+    // subtraction/addition of the negated value.
+    if (!RHS.isNegative()) {
+      ConvertedRHS = &BasicVals.Convert(resultTy, RHS);
----------------
I would rather swap these branches though, to leave the default case (aka. this) to the end.


================
Comment at: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:212-219
+      llvm::APSInt ConvertedRHSValue = resultIntTy.convert(RHS);
+      // Check if the negation of the RHS is representable,
+      // i.e., the resultTy is signed, and it is not the lowest
+      // representable negative value.
+      if (ConvertedRHSValue > resultIntTy.getMinValue()) {
+        ConvertedRHS = &BasicVals.getValue(-ConvertedRHSValue);
+        op = (op == BO_Add) ? BO_Sub : BO_Add;
----------------
Somehow I miss a check for signedness here.
Why do you think it would be only triggered for signed types?

I have a guess, that since we already handled `x +-0`, SymIntExprs like `x - (-0)` cannot exist here, thus cannot trigger this condition spuriously. I cannot think of any ther example that could cause this misbehaving. So in that sense `ConvertedRHSValue > resultIntTy.getMinValue()` implies *at this place* that `ConvertedRHSValue.isSigned()`.
I would rather see this redundant check here to make the correctness reasoning local though.


================
Comment at: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:661-667
+              // If the op and lop agrees, then we just need to
+              // sum the constants. Otherwise, we change to operation
+              // type if substraction would produce negative value
+              // (and cause overflow for unsigned integers),
+              // as consequence x+1U-10 produces x-9U, instead
+              // of x+4294967287U, that would be produced without this
+              // additional check.
----------------
It feels like this is a completely different problem compared to the //simplification of X - (-N) to X + N//.
If this is the case, I would rather split that part into a separate patch instead.


================
Comment at: clang/test/Analysis/additive-op-on-sym-int-expr.c:1
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -analyzer-config eagerly-assume=false -verify %s
+
----------------
You assume that `int` has 8 bytes and that 1 byte is 8 bits. Pin the target triple.


================
Comment at: clang/test/Analysis/additive-op-on-sym-int-expr.c:11
+  }
+
+  int i = x + 1;
----------------



================
Comment at: clang/test/Analysis/additive-op-on-sym-int-expr.c:35-36
+
+  l = -1l;
+  i = l;
+  clang_analyzer_dump(x + i); // expected-warning {{(reg_$0<int x>) - 1}}
----------------
You could simply assign the right value directly to `i` AFAIK.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D124658/new/

https://reviews.llvm.org/D124658