[PATCH] D41938: [Analyzer] SValBuilder Comparison Rearrangement (with Restrictions and Analyzer Option)

[George Karpenkov via Phabricator via cfe-commits]

george.karpenkov added inline comments.


================
Comment at: include/clang/StaticAnalyzer/Core/AnalyzerOptions.h:597
+  // than or equal to the quarter of the maximum value of that type.
+  bool shouldAggressivelySimplifyRelationalComparison();
+
----------------
High level comment: can you list all [[ https://en.wikipedia.org/wiki/Rewriting | rewriting ]] rules you are applying in a formula explicitly in a comment?
>From the phabricator discussion I see that you are applying
```
A + n >= B + m -> A - B >= n + m // A, B symbolic, n and m are integers
```

but from the code it seems that you are applying more canonicalization rules?


================
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:317
+// with simpler symbols on every recursive call.
+static bool isOverflowClampedBy4(SymbolRef Sym, ProgramStateRef State) {
+  SValBuilder &SVB = State->getStateManager().getSValBuilder();
----------------
Can we have a better function name here? I can't think of one straight away, but "clamped" is not very self-descriptive. `isWithinConstantOverflowBounds`?


================
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:326
+
+  llvm::APSInt Max = AT.getMaxValue() >> 2; // Divide by 4.
+  SVal IsCappedFromAbove =
----------------
Would just division produce the same result? Also probably it's better to make "4" a constant, at least with `#define`


================
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:330
+                      nonloc::ConcreteInt(Max), SVB.getConditionType());
+  if (auto DV = IsCappedFromAbove.getAs<DefinedSVal>()) {
+    if (State->assume(*DV, false))
----------------
6 lines of branching is probably better expressed as

```
if (!isa<DefinedSVal>(IsCappedFromAbove) || State->assume(*dyn_cast<DefinedSVal>(IsCappedFromAbove), false))
   return false
```


================
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:337
+
+  llvm::APSInt Min = -Max;
+  SVal IsCappedFromBelow =
----------------
326-335 duplicates 338-346.
Perhaps we could have

```
static bool isCappedFrom(bool Above, llvm::APSInt bound, ...)
```

?


================
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:352
+// Same for the concrete integers: see if I is within [min/4, max/4].
+static bool isOverflowClampedBy4(llvm::APSInt I) {
+  APSIntType AT(I);
----------------
Again, could we do better with a function name?


================
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:357
+
+  llvm::APSInt Max = AT.getMaxValue() >> 2;
+  if (I > Max)
----------------
I think you want

```
return (I <= Max) && (I >= -Max)
```

instead of 358-365


================
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:376
+  // Fail to decompose: "reduce" the problem to the "$x + 0" case.
+  return std::make_tuple(Sym, BO_Add, BV.getValue(0, Sym->getType()));
+}
----------------
Is it beneficial to do this though? At the point where `decomposeSymbol` is called we are still checking whether the rearrangement could be performed, so maybe just returning a false flag would be better?


================
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:403
+  if (LOp == BO_Sub)
+    LInt = -LInt;
+  else
----------------
I think this is a separate rewrite, which is better performed in a separate function.
If you move it to `decomposeSymbol` or to a separate function, you would get a lot of simplifications:

1. This function would be performing only a single rewrite.
2. You would no longer need to take `Lop` and `Rop` as parameters
3. At that point, two separate cases would be clearly seen: `Op` is a comparison operator, or `Op` is an additive operator.
I would separate those two rewrites in separate functions, distinguishing between them at the callsite.


================
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:429
+  if (BinaryOperator::isComparisonOp(Op)) {
+    // Prefer comparing to a non-negative number.
+    // FIXME: Maybe it'd be better to have consistency in
----------------
It seems that having a concrete positive RHS is a part of your rewrite rule. In that case, that should be documented in a high-level overview of the rewrite rules.


================
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:432
+    // "$x - $y" vs. "$y - $x" because those are solver's keys.
+    if (LInt > RInt) {
+      ResultSym = SymMgr.getSymSymExpr(RSym, BO_Sub, LSym, SymTy);
----------------
I think this could be shortened and made more explicit by constructing the LHS and RHS first, and then reversing both and the comparison operator if RHS is negative.


================
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:472
+  if (BinaryOperator::isComparisonOp(Op) &&
+      Opts.shouldAggressivelySimplifyRelationalComparison()) {
+    if (ResultTy != SVB.getConditionType())
----------------
I am confused why the option `shouldAggressivelySimplifyRelationalComparison` is checked here. Do we rewrite cases where `Op` is additive even if the option is not checked? It's generally better to check the flag outside of the rearranging function, so that the high-level logic can be seen.


================
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:489
+    if (SingleTy != ResultTy)
+      return None;
+  } else {
----------------
This check is weird: you have just set `SingleTy` to `ResultTy` at line 477.
Instead of this whole if-block (from line 487), why not just set `SingleTy` above line 473. where you have already checked that the operator is performing comparison?


================
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:494
+
+  assert(!SingleTy.isNull() && "We should have figured out the type by now!");
+
----------------
I would also move this assert up, below line 481.


================
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:497
+  // Substracting unsigned integers is a nightmare.
+  if (!SingleTy->isSignedIntegerOrEnumerationType())
+    return None;
----------------
this check should be inside the block at line 477, since it does not make sense for relational comparisons.


================
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:508
+  std::tie(LSym, LOp, LInt) = decomposeSymbol(LSym, BV);
+  if (LSym->getType() != SingleTy ||
+      !isOverflowClampedBy4(LSym, State) || !isOverflowClampedBy4(LInt))
----------------
Why `isComparisonOp()` check is done in 512-516, but not here? Additionally, can this check be factored out into a function?


================
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:774
 
+      if (Optional<NonLoc> V = tryRearrange(state, op, lhs, rhs, resultTy))
+        return *V;
----------------
I would expect that checking the analyzer option would be performed here?



================
Comment at: test/Analysis/svalbuilder-rearrange-comparisons.c:19
+  if (x < -(((int)INT_MAX) / 4))
+    exit(1);
+  return x;
----------------
assert would express intent better


================
Comment at: test/Analysis/svalbuilder-rearrange-comparisons.c:28
+  clang_analyzer_dump(x == y);
+  // expected-warning at -1{{((conj_$2{int}) - (conj_$5{int})) == 0}}
+}
----------------
Can we also have integration-like tests where rearrangement would affect observable behavior?

Also, `clang_analyzer_dump` is a debugging function, and I am not sure whether we should rely on its output in tests.


https://reviews.llvm.org/D41938