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

[Dominic Chen via Phabricator via cfe-commits]

ddcc added a comment.

As an aside, I think it'd be good to land https://reviews.llvm.org/D28954 and https://reviews.llvm.org/D28955 first, since they affect accuracy and precision of various analyzer parts that this depends on.

> 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:

Yeah, those should definitely be fixed. In general, I tried to avoid performing simplifications on anything not of floating-point type, particularly in SimpleSValBuilder, but there are probably cases that I've missed.

In your example `clang_analyzer_eval(a < 4.0 || a >= 4.0)` (and likewise for the rest), the following is happening:

1. At ExprEngineC.cpp:VisitLogicalExpr(), we hit this logical expression for the first time, the introspection fails, and we generate the SVal `(((double) (reg_$0<float a>)) >= 4.0E+0) != 0` that is bound to `a < 4.0 || a >= 4.0`.
2. The next time around, the introspection succeeds, and we generate the SVal `1 S32b` that is bound to `a < 4.0 || a >= 4.0`.
3. Now, when we hit ExprInspectionChecker.cpp:getArgumentValueString(), we retrieve the SVal `1 S32b`, and attempt to assert it.
4. Then, we hit SimpleConstraintManager.cpp:assumeAux(), and fall into the `nonloc::ConcreteIntKind` case. When `Assumption` is `true`, we are fine and return the original `State`, but then when `Assumption` is `false`, we return `nullptr`.
5. Back in ExprInspectionChecker.cpp:getArgumentValueString(), we see `StTrue != nullptr` and `StFalse == nullptr`, and we print `TRUE` instead of `UNKNOWN`.

I'm not familiar with `VisitLogicalExpr()` and why integer constants are being bound to the logical expressions. Wouldn't we simply want to assume that the logical expression, when expressed as a symbolic constraint, is either true/false in each respective child state?



================
Comment at: include/clang/StaticAnalyzer/Checkers/Checkers.td:150
 
+def FloatingPointMathChecker : Checker<"FPMath">,
+  HelpText<"Check for domain errors in floating-point math functions">,
----------------
dcoughlin wrote:
> 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?
This checker is a bit of a toy, in that (last I checked) Clang doesn't support the floating-point environment, which is typically used to install global floating-point exception handlers (for e.g. NaN, etc). As a result, there are probably going to lots of false-positives on real codebases.

Additionally, it requires the z3 solver, which probably isn't being built by default in most Linux distributions (and I doubt we're at the point of asking package maintainers to add a dependency for clang on libz3, even for those that do build that package).

So I think it should definitely be optional.


================
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));
----------------
dcoughlin wrote:
> Is there a reason you're not using assumeDual() here?
I'm not sure how `assumeDual` helps here?  The explicit checks `isPInf` and `isNInf` implement the short-circuit effect of logical or, whereas omitting them and binding directly to `isInf` miss the short-circuit effect.


================
Comment at: lib/StaticAnalyzer/Core/BasicValueFactory.cpp:118
+const llvm::APFloat &BasicValueFactory::getValue(const llvm::APFloat& X) {
+  llvm::FoldingSetNodeID ID;
+  void *InsertPos;
----------------
dcoughlin wrote:
> 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?)
The tricky part is that there are associate class member variables for each function (`APSIntSet` and `APFloatSet`). I can factor out `getValue` to a template, but then I'd need to introduce a templated helper function with two specializations to retrieve the class member variable for the input template type. I'm not sure if that'd be zero-cost?


================
Comment at: lib/StaticAnalyzer/Core/BasicValueFactory.cpp:331
+    case BO_Div:
+      // Divide by zero
+      if (V1.isFinite() && V2.isInfinity())
----------------
dcoughlin wrote:
> Is this comment correct? Is this really a divide by zero?
> 
> I'm also a bit surprised APFloat::divide() doesn't handle this case.
I don't recall why I wrote this...


================
Comment at: lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp:1092
 
+  assert(!V.isFloat());
+
----------------
dcoughlin wrote:
> 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? 
The trapping should be for debugging purposes only, since it is easy to accidentally call the wrong `getKnown*Value` function without disambiguating on the input type, and this wasn't previously necessary.


================
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1334
+      const llvm::APSInt *Int = getSymVal(State, CastSym);
+      assert(CastTy->isRealFloatingType());
+      llvm::APFloat Float(Ctx.getFloatTypeSemantics(CastTy));
----------------
dcoughlin wrote:
> 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?
Would you prefer returning nullptr instead?

I guess the question is if calling `getSymFloatVal` on a non floating-point type implies that the result should be converted to a floating-point type, and if so, whether that should trigger an assertion failure or return a null pointer on failure?


https://reviews.llvm.org/D28954