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

[Devin Coughlin via Phabricator via cfe-commits]

dcoughlin added a comment.

Thanks for the patch, and apologies for the delay reviewing!

Here are some initial comments -- there are more coming.



================
Comment at: include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h:159
+    llvm::APFloat To(S, llvm::APFloat::uninitialized);
+    assert(Convert(To, From) && "Failed to convert integer to floating-point!");
+    return getValue(To);
----------------
The called overload of Convert() initializes 'To', right? Should it be in an assert()? I'm worried about losing the side effect in non-assert builds.


================
Comment at: include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h:173
+#endif
+    assert(!(Status & (llvm::APFloat::opOverflow | llvm::APFloat::opInvalidOp)));
+    return getValue(To);
----------------
There are multiple checks for overflow or invalid in this file. Can the checks be factored out into a static member function?


================
Comment at: include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:137
   /// value for a symbol, even if it is perfectly constrained.
   virtual const llvm::APSInt* getSymVal(ProgramStateRef state,
                                         SymbolRef sym) const {
----------------
What do you think about renaming this to "getSymIntVal" now that we have getSymFloatVal()?


================
Comment at: include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:175
+  ///  query whether it is supported, use this to ask directly.
+  virtual bool canReasonAboutFloat() const = 0;
+
----------------
The name seems slightly weird. How about "canReasonAboutFloats" or "canReasonAboutFloatingPoint"?


================
Comment at: include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h:118
+  /// that value is returned. Otherwise, returns NULL.
+  virtual const llvm::APFloat *getKnownFloatValue(ProgramStateRef state, SVal val) = 0;
+
----------------
Note the 80-column violation here.


================
Comment at: include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h:575
+
+  const SymFloatExpr *getSymFloatExpr(const SymExpr &lhs,
+                                      BinaryOperator::Opcode op,
----------------
I don't think we need the 'const SymExpr &lhs' entry point. It seems superfluous and as far as I can tell the analog for getSymIntExpr() is never called and should probably be removed.


================
Comment at: lib/StaticAnalyzer/Checkers/BuiltinFunctionChecker.cpp:80
+    DefinedOrUnknownSVal isPInf = SVB.evalEQ(state, V, SPInf);
+    if (isPInf.isConstant(1)) {
+      C.addTransition(state->BindExpr(CE, LCtx, isPInf));
----------------
Is there a reason you're not using assumeDual() here?


================
Comment at: lib/StaticAnalyzer/Checkers/BuiltinFunctionChecker.cpp:95
+    // TODO: FIXME
+    // This should be BO_LOr for (V == -\inf) || (V == \inf), but logical
+    // operations are handled much earlier during ExplodedGraph generation.
----------------
Logical || has control flow implications, which is why it is handled at a higher level. We don't have a good way of representing generalized lazy disjunctive constraints. We can eagerly case split at the top level for disjunction, but this is bad for performance and is usually not needed.

Your trick of using bitwise OR as an ad hoc lazy disjunct seems reasonable here.


================
Comment at: lib/StaticAnalyzer/Core/BasicValueFactory.cpp:118
+const llvm::APFloat &BasicValueFactory::getValue(const llvm::APFloat& X) {
+  llvm::FoldingSetNodeID ID;
+  void *InsertPos;
----------------
This logic is nearly identical to that in getValue(const llvm::APSInt& X). Can the logic be factored out in some sort of zero-costish abstraction? (Perhaps templatized over the value type?)


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1242
+        BinaryOperator::isComparisonOp(BSE->getOpcode())) {
+      const llvm::APFloat *LHS, *RHS;
+      if (const FloatSymExpr *FSE = dyn_cast<FloatSymExpr>(BSE)) {
----------------
My compiler is complaining about these being uninitialized at line 1251 when both the if and else if guard conditions are false.


https://reviews.llvm.org/D28954