[PATCH] D103317: [Analyzer][Core] Make SValBuilder to better simplify svals with 3 symbols in the tree

[Gabor Marton via Phabricator via cfe-commits]

martong added inline comments.


================
Comment at: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:1144
+                                              : (SVal)SVB.makeIntVal(*Const);
+      return SVal();
+    }
----------------
steakhal wrote:
> Let's be explicit about it.
Good point.


================
Comment at: clang/lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:1148-1151
+      SVal Ret = getConst(Sym);
+      if (Ret.isUndef())
+        Ret = Visit(Sym);
+      return Ret;
----------------
steakhal wrote:
> 
Makes sense.


================
Comment at: clang/test/Analysis/svalbuilder-simplify-compound-svals.cpp:23
+  x = y = z = 1;
+  return 0;
+}
----------------
steakhal wrote:
> It feels odd that in some of your examples you return some value, but in the rest, you don't.
yep, I agree, updated.


================
Comment at: clang/test/Analysis/svalbuilder-simplify-compound-svals.cpp:32
+  clang_analyzer_eval(x + y * z == 0); // expected-warning{{TRUE}}
+  clang_analyzer_eval(y * z == 0);     // expected-warning{{TRUE}}
+  clang_analyzer_eval(x == 0);         // expected-warning{{TRUE}}
----------------
steakhal wrote:
> You could additionally assert that `y == 0` and `z == 0`.
`y * z == 0` does not imply that both `y` and `z` are `0`. However, we could expect that one of them is `0`, but currently we don't have such a deduction (this might be done in `ConstraintAssignor` in an independent patch).


================
Comment at: clang/test/Analysis/svalbuilder-simplify-compound-svals.cpp:50
+void test_SymInt_constrained(int x, int y, int z) {
+  if (x * y * z != 4)
+    return;
----------------
steakhal wrote:
> What if `z` were in the middle? Would it still pass?
No, that would not pass. This is because we do not handle commutativity, for that we should have a canonical form of the symbol trees (check out point 3 here https://reviews.llvm.org/D102696#2784624).


================
Comment at: clang/test/Analysis/svalbuilder-simplify-compound-svals.cpp:65
+  x = 77 / (y + z);
+  if (y + z != 1)
+    return;
----------------
steakhal wrote:
> Would the test pass if you were using `z + y != 1` here?
No, because we do not handle commutativity.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D103317