[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)) >= 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 ::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 

[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(
+*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(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? 

[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 ,
+  BinaryOperator::Opcode op,

I don't think we need the 'const SymExpr ' 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 ::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(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



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

[Dominic Chen via Phabricator via cfe-commits]

ddcc updated this revision to Diff 99522.
ddcc added a comment.
Herald added a subscriber: eraman.

Rebase, avoid generating floating-point constraints if unsupported by 
constraint manager


https://reviews.llvm.org/D28954

Files:
  include/clang/StaticAnalyzer/Checkers/Checkers.td
  include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h
  include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
  include/clang/StaticAnalyzer/Core/PathSensitive/SVals.def
  include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h
  include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
  include/clang/StaticAnalyzer/Core/PathSensitive/Symbols.def
  lib/StaticAnalyzer/Checkers/BuiltinFunctionChecker.cpp
  lib/StaticAnalyzer/Checkers/CMakeLists.txt
  lib/StaticAnalyzer/Checkers/FloatingPointMath.cpp
  lib/StaticAnalyzer/Core/BasicValueFactory.cpp
  lib/StaticAnalyzer/Core/Environment.cpp
  lib/StaticAnalyzer/Core/ProgramState.cpp
  lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
  lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
  lib/StaticAnalyzer/Core/RegionStore.cpp
  lib/StaticAnalyzer/Core/SValBuilder.cpp
  lib/StaticAnalyzer/Core/SVals.cpp
  lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
  lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
  lib/StaticAnalyzer/Core/SymbolManager.cpp
  lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  test/Analysis/diagnostics/macros.cpp
  test/Analysis/float-rules.c
  test/Analysis/float.c
  test/Analysis/inline.cpp
  test/Analysis/operator-calls.cpp

Index: test/Analysis/operator-calls.cpp
===
--- test/Analysis/operator-calls.cpp
+++ test/Analysis/operator-calls.cpp
@@ -81,8 +81,8 @@
   void test(int coin) {
 // Force a cache-out when we try to conjure a temporary region for the operator call.
 // ...then, don't crash.
-clang_analyzer_eval(+(coin ? getSmallOpaque() : getSmallOpaque())); // expected-warning{{UNKNOWN}}
-clang_analyzer_eval(+(coin ? getLargeOpaque() : getLargeOpaque())); // expected-warning{{UNKNOWN}}
+clang_analyzer_eval(+(coin ? getSmallOpaque() : getSmallOpaque())); // expected-warning{{TRUE}}
+clang_analyzer_eval(+(coin ? getLargeOpaque() : getLargeOpaque())); // expected-warning{{TRUE}}
   }
 }
 
Index: test/Analysis/inline.cpp
===
--- test/Analysis/inline.cpp
+++ test/Analysis/inline.cpp
@@ -285,11 +285,11 @@
   }
 
   void testFloatReference() {
-clang_analyzer_eval(defaultFloatReference(1) == -1); // expected-warning{{UNKNOWN}}
-clang_analyzer_eval(defaultFloatReference() == -42); // expected-warning{{UNKNOWN}}
+clang_analyzer_eval(defaultFloatReference(1) == -1); // expected-warning{{TRUE}}
+clang_analyzer_eval(defaultFloatReference() == -42); // expected-warning{{TRUE}}
 
-clang_analyzer_eval(defaultFloatReferenceZero(1) == -1); // expected-warning{{UNKNOWN}}
-clang_analyzer_eval(defaultFloatReferenceZero() == 0); // expected-warning{{UNKNOWN}}
+clang_analyzer_eval(defaultFloatReferenceZero(1) == -1); // expected-warning{{TRUE}}
+clang_analyzer_eval(defaultFloatReferenceZero() == 0); // expected-warning{{TRUE}}
   }
 
   char defaultString(const char *s = "abc") {
Index: test/Analysis/float.c
===
--- /dev/null
+++ test/Analysis/float.c
@@ -0,0 +1,83 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core.builtin,debug.ExprInspection -verify %s
+// REQUIRES: z3
+
+void clang_analyzer_eval(int);
+
+void float1() {
+  float z1 = 0.0, z2 = -0.0;
+  clang_analyzer_eval(z1 == z2); // expected-warning{{TRUE}}
+}
+
+void float2(float a, float b) {
+  clang_analyzer_eval(a == b); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(a != b); // expected-warning{{UNKNOWN}}
+}
+
+void float3(float a, float b) {
+  if (__builtin_isnan(a) || __builtin_isnan(b) || a < b) {
+clang_analyzer_eval(a > b); // expected-warning{{FALSE}}
+clang_analyzer_eval(a == b); // expected-warning{{FALSE}}
+return;
+  }
+  clang_analyzer_eval(a >= b); // expected-warning{{TRUE}}
+  clang_analyzer_eval(a == b); // expected-warning{{UNKNOWN}}
+}
+
+void float4(float a) {
+  if (__builtin_isnan(a) || a < 0.0f)
+return;
+  clang_analyzer_eval(a >= 0.0Q); // expected-warning{{TRUE}}
+  clang_analyzer_eval(a >= 0.0F); // expected-warning{{TRUE}}
+  clang_analyzer_eval(a >= 0.0); // expected-warning{{TRUE}}
+  clang_analyzer_eval(a >= 0); // expected-warning{{TRUE}}
+}
+
+void float5() {
+  double value = 1.0;
+  double pinf = __builtin_inf();
+  double ninf = -__builtin_inf();
+  double nan = __builtin_nan("");
+
+  /* NaN */
+  clang_analyzer_eval(__builtin_isnan(value)); // expected-warning{{FALSE}}
+  clang_analyzer_eval(__builtin_isnan(nan)); // expected-warning{{TRUE}}
+
+  clang_analyzer_eval(__builtin_isnan(0.0 / 0.0)); // 

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

[Dominic Chen via Phabricator via cfe-commits]

ddcc added a comment.

In https://reviews.llvm.org/D28954#754478, @lirhea wrote:

> In https://reviews.llvm.org/D28954#714936, @ddcc wrote:
>
> > Rebase, update tests, fix bugs
>
>
> Excuse me,I want to download full codes of this version,but I have no idea 
> how to do it,can you tell me?
>  And my system is windows, I haven't install anything about Phabricator.
>  Thank you!


You're probably better off waiting for these patches 
(https://reviews.llvm.org/D28952, https://reviews.llvm.org/D28953, and 
https://reviews.llvm.org/D28954) to land rather than grabbing the commits, 
since some of these diffs are old and I haven't had a chance to rebase and 
retest them yet. But if you want to try them now, you'll need to compile 
Clang/LLVM from source, since they haven't landed in any release. I'm also not 
sure how well the CMake bindings for Z3 work on Windows, it's not a platform 
I've tested. Either grab the raw diffs of these three commits using "download 
raw diff" from the web interface, or using Arcanist's `arc patch` commit. 
Alternatively, I have an older tree with all three commits at 
https://github.com/ddcc/clang/tree/debug , just revert the debugging commit.


https://reviews.llvm.org/D28954



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

[chen, zheyu via Phabricator via cfe-commits]

lirhea added a comment.

In https://reviews.llvm.org/D28954#714936, @ddcc wrote:

> Rebase, update tests, fix bugs


Excuse me,I want to download full codes of this version,but I have no idea how 
to do it,can you tell me?
And my system is windows.


https://reviews.llvm.org/D28954



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

[Dominic Chen via Phabricator via cfe-commits]

ddcc updated this revision to Diff 93590.
ddcc added a comment.

Rebase, update tests, fix bugs


https://reviews.llvm.org/D28954

Files:
  include/clang/StaticAnalyzer/Checkers/Checkers.td
  include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h
  include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
  include/clang/StaticAnalyzer/Core/PathSensitive/SVals.def
  include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h
  include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
  include/clang/StaticAnalyzer/Core/PathSensitive/Symbols.def
  lib/StaticAnalyzer/Checkers/BuiltinFunctionChecker.cpp
  lib/StaticAnalyzer/Checkers/CMakeLists.txt
  lib/StaticAnalyzer/Checkers/FloatingPointMath.cpp
  lib/StaticAnalyzer/Core/BasicValueFactory.cpp
  lib/StaticAnalyzer/Core/Environment.cpp
  lib/StaticAnalyzer/Core/ProgramState.cpp
  lib/StaticAnalyzer/Core/RegionStore.cpp
  lib/StaticAnalyzer/Core/SValBuilder.cpp
  lib/StaticAnalyzer/Core/SVals.cpp
  lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
  lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
  lib/StaticAnalyzer/Core/SymbolManager.cpp
  lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  test/Analysis/diagnostics/macros.cpp
  test/Analysis/float-rules.c
  test/Analysis/float.c
  test/Analysis/inline.cpp
  test/Analysis/lit.local.cfg
  test/Analysis/operator-calls.cpp

Index: test/Analysis/operator-calls.cpp
===
--- test/Analysis/operator-calls.cpp
+++ test/Analysis/operator-calls.cpp
@@ -81,8 +81,8 @@
   void test(int coin) {
 // Force a cache-out when we try to conjure a temporary region for the operator call.
 // ...then, don't crash.
-clang_analyzer_eval(+(coin ? getSmallOpaque() : getSmallOpaque())); // expected-warning{{UNKNOWN}}
-clang_analyzer_eval(+(coin ? getLargeOpaque() : getLargeOpaque())); // expected-warning{{UNKNOWN}}
+clang_analyzer_eval(+(coin ? getSmallOpaque() : getSmallOpaque())); // expected-warning{{TRUE}}
+clang_analyzer_eval(+(coin ? getLargeOpaque() : getLargeOpaque())); // expected-warning{{TRUE}}
   }
 }
 
Index: test/Analysis/lit.local.cfg
===
--- test/Analysis/lit.local.cfg
+++ test/Analysis/lit.local.cfg
@@ -1,20 +1,35 @@
+import lit.Test
 import lit.TestRunner
 import sys
 
 # Custom format class for static analyzer tests
 class AnalyzerTest(lit.formats.ShTest, object):
 
 def execute(self, test, litConfig):
-result = self.executeWithAnalyzeSubstitution(test, litConfig, '-analyzer-constraints=range')
+results = []
 
-if result.code == lit.Test.FAIL:
-return result
+# Parse any test requirements ('REQUIRES: ')
+saved_test = test
+lit.TestRunner.parseIntegratedTestScript(test)
+
+if 'z3' not in test.requires:
+results.append(self.executeWithAnalyzeSubstitution(saved_test, litConfig, '-analyzer-constraints=range'))
+
+if results[-1].code == lit.Test.FAIL:
+return results[-1]
 
 # If z3 backend available, add an additional run line for it
 if test.config.clang_staticanalyzer_z3 == '1':
-result = self.executeWithAnalyzeSubstitution(test, litConfig, '-analyzer-constraints=z3 -DANALYZER_CM_Z3')
+results.append(self.executeWithAnalyzeSubstitution(saved_test, litConfig, '-analyzer-constraints=z3 -DANALYZER_CM_Z3'))
 
-return result
+# Combine all result outputs into the last element
+for x in results:
+if x != results[-1]:
+results[-1].output = x.output + results[-1].output
+
+if results:
+return results[-1]
+return lit.Test.Result(lit.Test.UNSUPPORTED, "Test requires the following unavailable features: z3")
 
 def executeWithAnalyzeSubstitution(self, test, litConfig, substitution):
 saved_substitutions = list(test.config.substitutions)
Index: test/Analysis/inline.cpp
===
--- test/Analysis/inline.cpp
+++ test/Analysis/inline.cpp
@@ -285,11 +285,11 @@
   }
 
   void testFloatReference() {
-clang_analyzer_eval(defaultFloatReference(1) == -1); // expected-warning{{UNKNOWN}}
-clang_analyzer_eval(defaultFloatReference() == -42); // expected-warning{{UNKNOWN}}
+clang_analyzer_eval(defaultFloatReference(1) == -1); // expected-warning{{TRUE}}
+clang_analyzer_eval(defaultFloatReference() == -42); // expected-warning{{TRUE}}
 
-clang_analyzer_eval(defaultFloatReferenceZero(1) == -1); // expected-warning{{UNKNOWN}}
-clang_analyzer_eval(defaultFloatReferenceZero() == 0); // expected-warning{{UNKNOWN}}
+clang_analyzer_eval(defaultFloatReferenceZero(1) == -1); // expected-warning{{TRUE}}
+clang_analyzer_eval(defaultFloatReferenceZero() == 0); // expected-warning{{TRUE}}
   }
 
 

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

[Dominic Chen via Phabricator via cfe-commits]

ddcc updated this revision to Diff 85315.
ddcc added a comment.

Rebase


https://reviews.llvm.org/D28954

Files:
  include/clang/StaticAnalyzer/Checkers/Checkers.td
  include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h
  include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
  include/clang/StaticAnalyzer/Core/PathSensitive/SVals.def
  include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h
  include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
  include/clang/StaticAnalyzer/Core/PathSensitive/Symbols.def
  lib/StaticAnalyzer/Checkers/BuiltinFunctionChecker.cpp
  lib/StaticAnalyzer/Checkers/CMakeLists.txt
  lib/StaticAnalyzer/Checkers/FloatingPointMath.cpp
  lib/StaticAnalyzer/Core/BasicValueFactory.cpp
  lib/StaticAnalyzer/Core/Environment.cpp
  lib/StaticAnalyzer/Core/ProgramState.cpp
  lib/StaticAnalyzer/Core/RegionStore.cpp
  lib/StaticAnalyzer/Core/SValBuilder.cpp
  lib/StaticAnalyzer/Core/SVals.cpp
  lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
  lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
  lib/StaticAnalyzer/Core/SymbolManager.cpp
  lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
  test/Analysis/diagnostics/macros.cpp
  test/Analysis/float-rules.c
  test/Analysis/float.c
  test/Analysis/inline.cpp
  test/Analysis/operator-calls.cpp

Index: test/Analysis/operator-calls.cpp
===
--- test/Analysis/operator-calls.cpp
+++ test/Analysis/operator-calls.cpp
@@ -81,8 +81,8 @@
   void test(int coin) {
 // Force a cache-out when we try to conjure a temporary region for the operator call.
 // ...then, don't crash.
-clang_analyzer_eval(+(coin ? getSmallOpaque() : getSmallOpaque())); // expected-warning{{UNKNOWN}}
-clang_analyzer_eval(+(coin ? getLargeOpaque() : getLargeOpaque())); // expected-warning{{UNKNOWN}}
+clang_analyzer_eval(+(coin ? getSmallOpaque() : getSmallOpaque())); // expected-warning{{TRUE}}
+clang_analyzer_eval(+(coin ? getLargeOpaque() : getLargeOpaque())); // expected-warning{{TRUE}}
   }
 }
 
Index: test/Analysis/inline.cpp
===
--- test/Analysis/inline.cpp
+++ test/Analysis/inline.cpp
@@ -285,11 +285,11 @@
   }
 
   void testFloatReference() {
-clang_analyzer_eval(defaultFloatReference(1) == -1); // expected-warning{{UNKNOWN}}
-clang_analyzer_eval(defaultFloatReference() == -42); // expected-warning{{UNKNOWN}}
+clang_analyzer_eval(defaultFloatReference(1) == -1); // expected-warning{{TRUE}}
+clang_analyzer_eval(defaultFloatReference() == -42); // expected-warning{{TRUE}}
 
-clang_analyzer_eval(defaultFloatReferenceZero(1) == -1); // expected-warning{{UNKNOWN}}
-clang_analyzer_eval(defaultFloatReferenceZero() == 0); // expected-warning{{UNKNOWN}}
+clang_analyzer_eval(defaultFloatReferenceZero(1) == -1); // expected-warning{{TRUE}}
+clang_analyzer_eval(defaultFloatReferenceZero() == 0); // expected-warning{{TRUE}}
   }
 
   char defaultString(const char *s = "abc") {
Index: test/Analysis/float.c
===
--- /dev/null
+++ test/Analysis/float.c
@@ -0,0 +1,83 @@
+// RUN: %clang_cc1 -analyze -analyzer-checker=core.builtin,debug.ExprInspection -verify %s
+// REQUIRES: z3
+
+void clang_analyzer_eval(int);
+
+void float1() {
+  float z1 = 0.0, z2 = -0.0;
+  clang_analyzer_eval(z1 == z2); // expected-warning{{TRUE}}
+}
+
+void float2(float a, float b) {
+  clang_analyzer_eval(a == b); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(a != b); // expected-warning{{UNKNOWN}}
+}
+
+void float3(float a, float b) {
+  if (__builtin_isnan(a) || __builtin_isnan(b) || a < b) {
+clang_analyzer_eval(a > b); // expected-warning{{FALSE}}
+clang_analyzer_eval(a == b); // expected-warning{{FALSE}}
+return;
+  }
+  clang_analyzer_eval(a >= b); // expected-warning{{TRUE}}
+  clang_analyzer_eval(a == b); // expected-warning{{UNKNOWN}}
+}
+
+void float4(float a) {
+  if (__builtin_isnan(a) || a < 0.0f)
+return;
+  clang_analyzer_eval(a >= 0.0Q); // expected-warning{{TRUE}}
+  clang_analyzer_eval(a >= 0.0F); // expected-warning{{TRUE}}
+  clang_analyzer_eval(a >= 0.0); // expected-warning{{TRUE}}
+  clang_analyzer_eval(a >= 0); // expected-warning{{TRUE}}
+}
+
+void float5() {
+  double value = 1.0;
+  double pinf = __builtin_inf();
+  double ninf = -__builtin_inf();
+  double nan = __builtin_nan("");
+
+  /* NaN */
+  clang_analyzer_eval(__builtin_isnan(value)); // expected-warning{{FALSE}}
+  clang_analyzer_eval(__builtin_isnan(nan)); // expected-warning{{TRUE}}
+
+  clang_analyzer_eval(__builtin_isnan(0.0 / 0.0)); // expected-warning{{TRUE}}
+  clang_analyzer_eval(__builtin_isnan(pinf / ninf)); // expected-warning{{TRUE}}
+  clang_analyzer_eval(__builtin_isnan(pinf / pinf)); // expected-warning{{TRUE}}
+  clang_analyzer_eval(__builtin_isnan(ninf / 

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

[Dominic Chen via Phabricator via cfe-commits]

ddcc added a comment.

- This patch introduces a virtual overloaded `llvm::APFloat getSymVal()` for 
returning the value of known floating-point constants. In the long term, both 
`getSymVal()` functions should probably be refactored to return something like 
a `llvm::Con
- There are also long-term issues with the flexibility of the `SymExpr` class. 
Currently, this patch adds two `SymFloatExpr` and `FloatSymExpr` subclasses, 
but this isn't expressive enough for certain types of symbolic queries. For 
example, the current implementation checks whether a floating-point value is 
`NaN` by comparing whether `V == V`, which should only be false for `NaN`. It 
would be better to add support for special queries for whether a value is NaN, 
positive infinity, negative infinity, etc.


https://reviews.llvm.org/D28954



___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

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

[Dominic Chen via Phabricator via cfe-commits]

ddcc created this revision.
Herald added a subscriber: mgorny.

With the Z3 constraint manager, symbolic floating-point constraints can also be 
reasoned about. This commit includes a basic floating-point checker for domain 
errors with math functions.


https://reviews.llvm.org/D28954

Files:
  include/clang/StaticAnalyzer/Checkers/Checkers.td
  include/clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h
  include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
  include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h
  include/clang/StaticAnalyzer/Core/PathSensitive/SVals.def
  include/clang/StaticAnalyzer/Core/PathSensitive/SVals.h
  include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
  include/clang/StaticAnalyzer/Core/PathSensitive/Symbols.def
  lib/StaticAnalyzer/Checkers/BuiltinFunctionChecker.cpp
  lib/StaticAnalyzer/Checkers/CMakeLists.txt
  lib/StaticAnalyzer/Checkers/FloatingPointMath.cpp
  lib/StaticAnalyzer/Core/BasicValueFactory.cpp
  lib/StaticAnalyzer/Core/Environment.cpp
  lib/StaticAnalyzer/Core/ProgramState.cpp
  lib/StaticAnalyzer/Core/RegionStore.cpp
  lib/StaticAnalyzer/Core/SValBuilder.cpp
  lib/StaticAnalyzer/Core/SVals.cpp
  lib/StaticAnalyzer/Core/SimpleConstraintManager.cpp
  lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
  lib/StaticAnalyzer/Core/SymbolManager.cpp
  test/Analysis/diagnostics/macros.cpp
  test/Analysis/float-rules.c
  test/Analysis/float.c
  test/Analysis/inline.cpp
  test/Analysis/operator-calls.cpp
  tools/z3-constraint-manager/Z3ConstraintManager.cpp

Index: tools/z3-constraint-manager/Z3ConstraintManager.cpp
===
--- tools/z3-constraint-manager/Z3ConstraintManager.cpp
+++ tools/z3-constraint-manager/Z3ConstraintManager.cpp
@@ -77,6 +77,12 @@
 
 Z3_ast Assign = Z3_model_get_const_interp(Z3Expr::ZC, Model, Func);
 Z3_sort Sort = Z3_get_sort(Z3Expr::ZC, Assign);
+if (Z3_get_sort_kind(Z3Expr::ZC, Sort) == Z3_FLOATING_POINT_SORT) {
+  llvm::APFloat Float(llvm::APFloat::Bogus());
+  if (!Z3Expr::toAPFloat(Sort, Assign, Float, false))
+return false;
+  return BasicValueFactory::Convert(Int, Float);
+}
 return Z3Expr::toAPSInt(Sort, Assign, Int, true);
   }
 
@@ -88,6 +94,12 @@
 
 Z3_ast Assign = Z3_model_get_const_interp(Z3Expr::ZC, Model, Func);
 Z3_sort Sort = Z3_get_sort(Z3Expr::ZC, Assign);
+if (Z3_get_sort_kind(Z3Expr::ZC, Sort) != Z3_FLOATING_POINT_SORT) {
+  llvm::APSInt Int;
+  if (!Z3Expr::toAPSInt(Sort, Assign, Int, false))
+return false;
+  return BasicValueFactory::Convert(Float, Int);
+}
 return Z3Expr::toAPFloat(Sort, Assign, Float, true);
   }
 
@@ -617,8 +629,8 @@
 }; // end class Z3Expr
 
 void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
-  llvm::report_fatal_error("Z3 error: " +
-   llvm::Twine(Z3_get_error_msg_ex(Context, Error)));
+  llvm::report_fatal_error(
+  "Z3 error: " + llvm::Twine(Z3_get_error_msg_ex(Context, Error)));
 }
 
 Z3_context Z3Expr::ZC;
@@ -660,6 +672,9 @@
   const llvm::APSInt *getSymVal(ProgramStateRef State,
 SymbolRef Sym) const override;
 
+  const llvm::APFloat *getSymFloatVal(ProgramStateRef State,
+  SymbolRef Sym) const override;
+
   ProgramStateRef removeDeadBindings(ProgramStateRef St,
  SymbolReaper ) override;
 
@@ -740,6 +755,10 @@
   // Helper functions.
   //===--===//
 
+  // Recover the QualType of an APFloat.
+  // TODO: Refactor to put elsewhere
+  QualType getAPFloatType(const llvm::APFloat ) const;
+
   // Recover the QualType of an APSInt.
   // TODO: Refactor to put elsewhere
   QualType getAPSIntType(const llvm::APSInt ) const;
@@ -765,6 +784,11 @@
   void doFloatTypeConversion(T , QualType , T ,
  QualType ) const;
 
+  // Callback function for doCast parameter on APFloat type.
+  static llvm::APFloat castAPFloat(const llvm::APFloat , QualType ToTy,
+   uint64_t ToWidth, QualType FromTy,
+   uint64_t FromWidth);
+
   // Callback function for doCast parameter on APSInt type.
   static llvm::APSInt castAPSInt(const llvm::APSInt , QualType ToTy,
  uint64_t ToWidth, QualType FromTy,
@@ -853,6 +877,10 @@
 Sym = SIE->getLHS();
   } else if (const IntSymExpr *ISE = dyn_cast(BSE)) {
 Sym = ISE->getRHS();
+  } else if (const SymFloatExpr *SFE = dyn_cast(BSE)) {
+Sym = SFE->getLHS();
+  } else if (const FloatSymExpr *FSE = dyn_cast(BSE)) {
+Sym = FSE->getRHS();
   } else if (const SymSymExpr *SSM = dyn_cast(BSE)) {
 return canReasonAbout(nonloc::SymbolVal(SSM->getLHS())) &&
canReasonAbout(nonloc::SymbolVal(SSM->getRHS()));
@@ -889,6