[PATCH] D28954: [analyzer] Add support for symbolic float expressions

[Devin Coughlin via Phabricator via cfe-commits]

dcoughlin added a comment.

This looks like a very solid start!

One area that I'm very worried about is that in various places the analyzer makes assumptions about algebraic simplifications that don't hold for floating point because of NaN and other floating point oddities. I think it really important to write a fairly comprehensive set of tests for these gotchas to make sure we're not applying for floating point. We should test for these both with and without the Z3 solver.

Here are some examples that should all be UNKNOWN (right?) but are not in the current patch, assuming `a` and `b` hold unconstrained symbols of floating-point type:

  clang_analyzer_eval(a != 4.0 || a == 4.0);
  clang_analyzer_eval(a < 4.0 || a >= 4.0);
  clang_analyzer_eval((a != b) == !(a == b));
  clang_analyzer_eval((a != 4.0) == !(a == 4.0));





================
Comment at: include/clang/StaticAnalyzer/Checkers/Checkers.td:150
 
+def FloatingPointMathChecker : Checker<"FPMath">,
+  HelpText<"Check for domain errors in floating-point math functions">,
----------------
It is fine to have this in alpha now. What package to do envision this in after it is ready? Is this something that should always be on, or should be opted into on a per-project basis?


================
Comment at: lib/StaticAnalyzer/Checkers/FloatingPointMath.cpp:47
+    C.emitReport(llvm::make_unique<BugReport>(
+        *BT, "Argument value is out of valid domain for function call", N));
+  }
----------------
I think it would be a better user experience if the diagnostic could (1) mention the function name and (2) tell the programmer what the valid domain is. (1) should be easy. Do you think (2) is feasible for floating point?


================
Comment at: lib/StaticAnalyzer/Checkers/FloatingPointMath.cpp:105
+    // Skip if known to be NaN, otherwise assume to be not NaN
+    SVal notNaN = SVB.evalBinOp(State, BO_EQ, V, V, SVB.getConditionType());
+    if (notNaN.isUnknown() || notNaN.isZeroConstant()) {
----------------
Can the checking for not NaN be factored out? It looks there is similar checking in multiple places.


================
Comment at: lib/StaticAnalyzer/Core/BasicValueFactory.cpp:331
+    case BO_Div:
+      // Divide by zero
+      if (V1.isFinite() && V2.isInfinity())
----------------
Is this comment correct? Is this really a divide by zero?

I'm also a bit surprised APFloat::divide() doesn't handle this case.


================
Comment at: lib/StaticAnalyzer/Core/BasicValueFactory.cpp:359
+
+  // TODO: Fix sign of special results
+  if (Status & llvm::APFloat::opOverflow)
----------------
Could you add a little more context to this TODO? This way if you don't get around to it someone can pick it up.


================
Comment at: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:378
+      return false;
+    } else if (const SymExpr *SE = SymVal->getSymbol()) {
+      if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
----------------
LLVM style generally discourages putting an 'else' after a return. http://llvm.org/docs/CodingStandards.html#don-t-use-else-after-a-return Here you can just use 'if'.


================
Comment at: lib/StaticAnalyzer/Core/SValBuilder.cpp:46
+
+  // FIXME: Handle structs.
   return UnknownVal();
----------------
Aren't structs already handled by the isRecordType() disjunct above that makes a compound value? Can you provide more detail in the FIXME about what needs to be fixed?


================
Comment at: lib/StaticAnalyzer/Core/SValBuilder.cpp:70
+                               const llvm::APFloat& rhs, QualType type) {
+  // The Environment ensures we always get a persistent APSInt in
+  // BasicValueFactory, so we don't need to get the APSInt from
----------------
Should this say 'APFloat' in the comment?


================
Comment at: lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp:133
+#ifndef NDEBUG
+    assert(BVF.Convert(FromF, From) && "Integer failed to convert to float!");
+    assert(BVF.Convert(ToF, To) && "Integer failed to convert to float!");
----------------
I guess this is safe, but it seems quite strange to have operations with side effects inside an assert(). Can you store the return value from convert in a local use and `(void)local;` to suppress the unused variable diagnostic?


================
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:160
+                         !castTy->isSignedIntegerOrEnumerationType());
+      // Cannot be represented in destination type, this is undefined behavior
+      if (!BasicValueFactory::Convert(Value, CF->getValue()))
----------------
Is this the kind of thing it could eventually be a good idea to issue a diagnostic for?


================
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:1092
 
+  assert(!V.isFloat());
+
----------------
I'm wondering whether we should rename this method to "getKnownIntValue()" and then just return nullptr here. What are the merits of trapping vs. returning nullptr here? 


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1334
+      const llvm::APSInt *Int = getSymVal(State, CastSym);
+      assert(CastTy->isRealFloatingType());
+      llvm::APFloat Float(Ctx.getFloatTypeSemantics(CastTy));
----------------
I'm wondering whether this assert is too strong. Should it be the responsibility of callers of this method to guarantee that it doesn't fire? If so, can we document the implied precondition for the method?


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1766
+#endif
+  assert(!(Status & (llvm::APFloat::opOverflow | llvm::APFloat::opInvalidOp)));
+  return To;
----------------
It is probably easier to maintain if you use:
```
(void)Status;
```
here instead of the duplication.


https://reviews.llvm.org/D28954