Merge pull request #1120 from jcreedcmu/jcreed/nan

C++: Teach range analysis to pay attention to NaNs.

Author: jbj

change-notes/1.21/analysis-cpp.md

@@ -15,5 +15,6 @@
 | Memory may not be freed (`cpp/memory-may-not-be-freed`) | More correct results | Support added for more Microsoft-specific allocation functions, including `LocalAlloc`, `GlobalAlloc`, `HeapAlloc` and `CoTaskMemAlloc`. |
 | Memory is never freed (`cpp/memory-never-freed`) | More correct results | Support added for more Microsoft-specific allocation functions, including `LocalAlloc`, `GlobalAlloc`, `HeapAlloc` and `CoTaskMemAlloc`. |
 | Resource not released in destructor (`cpp/resource-not-released-in-destructor`) | Fewer false positive results | Resource allocation and deallocation functions are now determined more accurately. |
+| Comparison result is always the same | Fewer false positive results | The range analysis library is now more conservative about floating point values being possibly `NaN` |
 
 ## Changes to QL libraries

cpp/ql/src/semmle/code/cpp/rangeanalysis/NanAnalysis.qll

@@ -0,0 +1,41 @@
+import cpp
+private import semmle.code.cpp.rangeanalysis.RangeSSA
+
+/**
+ * Holds if `guard` won't return the value `polarity` when either
+ * operand is NaN.
+ */
+predicate nanExcludingComparison(ComparisonOperation guard, boolean polarity) {
+  polarity = true and
+  (
+    guard instanceof LTExpr or
+    guard instanceof LEExpr or
+    guard instanceof GTExpr or
+    guard instanceof GEExpr or
+    guard instanceof EQExpr
+  )
+  or
+  polarity = false and
+  guard instanceof NEExpr
+}
+
+/**
+ * Holds if `v` is a use of an SSA definition in `def` which cannot be NaN,
+ * by virtue of the guard in `def`.
+ */
+private predicate excludesNan(RangeSsaDefinition def, VariableAccess v) {
+  exists(VariableAccess inCond, ComparisonOperation guard, boolean branch, LocalScopeVariable lsv |
+    def.isGuardPhi(inCond, guard, branch) and
+    inCond.getTarget() = lsv and
+    v = def.getAUse(lsv) and
+    guard.getAnOperand() = inCond and
+    nanExcludingComparison(guard, branch)
+  )
+}
+
+/**
+ * A variable access which cannot be NaN.
+ */
+class NonNanVariableAccess extends VariableAccess {
+  NonNanVariableAccess() { excludesNan(_, this) }
+}

cpp/ql/src/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll

@@ -45,6 +45,7 @@ import cpp
 private import RangeAnalysisUtils
 import RangeSSA
 import SimpleRangeAnalysisCached
+private import NanAnalysis
 
 /**
  * This fixed set of lower bounds is used when the lower bounds of an
@@ -993,6 +994,25 @@ predicate unanalyzableDefBounds(
   ub = varMaxVal(v)
 }
 
+/**
+ * Holds if in the `branch` branch of a guard `guard` involving `v`,
+ * we know that `v` is not NaN, and therefore it is safe to make range
+ * inferences about `v`.
+ */
+bindingset[guard, v, branch]
+predicate nonNanGuardedVariable(ComparisonOperation guard, VariableAccess v, boolean branch) {
+  v.getType().getUnspecifiedType() instanceof IntegralType
+  or
+  v.getType().getUnspecifiedType() instanceof FloatingPointType and v instanceof NonNanVariableAccess
+  or
+  // The reason the following case is here is to ensure that when we say
+  // `if (x > 5) { ...then... } else { ...else... }`
+  // it is ok to conclude that `x > 5` in the `then`, (though not safe
+  // to conclude that x <= 5 in `else`) even if we had no prior
+  // knowledge of `x` not being `NaN`.
+  nanExcludingComparison(guard, branch)
+}
+
 /**
  * If the guard is a comparison of the form `p*v + q <CMP> r`, then this
  * predicate uses the bounds information for `r` to compute a lower bound
@@ -1004,10 +1024,12 @@ predicate lowerBoundFromGuard(
 ) {
   exists (float childLB, RelationStrictness strictness
   | boundFromGuard(guard, v, childLB, true, strictness, branch)
-  | if (strictness = Nonstrict() or
-        not (v.getType().getUnspecifiedType() instanceof IntegralType))
-      then lb = childLB
-      else lb = childLB+1)
+  | if nonNanGuardedVariable(guard, v, branch)
+    then (if (strictness = Nonstrict() or
+            not (v.getType().getUnspecifiedType() instanceof IntegralType))
+          then lb = childLB
+          else lb = childLB+1)
+    else lb = varMinVal(v.getTarget()))
 }
 
 /**
@@ -1021,10 +1043,12 @@ predicate upperBoundFromGuard(
 ) {
   exists (float childUB, RelationStrictness strictness
   | boundFromGuard(guard, v, childUB, false, strictness, branch)
-  | if (strictness = Nonstrict() or
-        not (v.getType().getUnspecifiedType() instanceof IntegralType))
-      then ub = childUB
-      else ub = childUB-1)
+  | if nonNanGuardedVariable(guard, v, branch)
+    then (if (strictness = Nonstrict() or
+            not (v.getType().getUnspecifiedType() instanceof IntegralType))
+          then ub = childUB
+          else ub = childUB-1)
+    else ub = varMaxVal(v.getTarget()))
 }
 
 /**

cpp/ql/test/query-tests/Likely Bugs/Arithmetic/PointlessComparison/PointlessComparison.c

@@ -265,3 +265,30 @@ int negative_zero(double dbl) {
   }
   return 0;
 }
+
+int nan(double x) {
+  if (x < 0.0) {
+    return 100;
+  }
+  else if (x >= 0.0) { // GOOD [x could be NaN]
+    return 200;
+  }
+  else {
+    return 300;
+  }
+}
+
+int nan2(double x) {
+  if (x == x) {
+    // If x compares with anything at all, it's not NaN
+    if (x < 0.0) {
+      return 100;
+    }
+    else if (x >= 0.0) { // BAD [Always true]
+      return 200;
+    }
+    else {
+      return 300;
+    }
+  }
+}

cpp/ql/test/query-tests/Likely Bugs/Arithmetic/PointlessComparison/PointlessComparison.expected

@@ -32,5 +32,6 @@
 | PointlessComparison.c:129:12:129:16 | ... > ... | Comparison is always false because a <= 3. |
 | PointlessComparison.c:197:7:197:11 | ... < ... | Comparison is always false because x >= 0. |
 | PointlessComparison.c:264:12:264:22 | ... >= ... | Comparison is always true because dbl >= 0 and -0 >= - .... |
+| PointlessComparison.c:287:14:287:21 | ... >= ... | Comparison is always true because x >= 0. |
 | RegressionTests.cpp:57:7:57:22 | ... <= ... | Comparison is always true because * ... <= 4294967295. |
 | Templates.cpp:9:10:9:24 | ... <= ... | Comparison is always true because local <= 32767. |