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
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
