TEMP: Make sure type-based reasons propagate through bounds for add e…

…xpressions.
github · Aug 1, 2023 · 44a88b8 · 44a88b8
1 parent c25b7a9
commit 44a88b8
Show file tree

Hide file tree

Showing 3 changed files with 27 additions and 3 deletions.
diff --git a/...e/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisConstantSpecific.qll b/...e/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisConstantSpecific.qll
@@ -20,6 +20,8 @@ module CppLangImplConstant implements LangSig<FloatDelta> {
   abstract class SemReason extends TSemReason {
     /** Gets a textual representation of this reason. */
     abstract string toString();
+
+    abstract SemReason combineWith(SemReason reason);
   }
 
   abstract class SemValueReason extends SemReason { }
@@ -30,6 +32,8 @@ module CppLangImplConstant implements LangSig<FloatDelta> {
    */
   class SemNoReason extends SemValueReason, TSemNoReason {
     override string toString() { result = "NoReason" }
+
+    override SemReason combineWith(SemReason reason) { result = reason }
   }
 
   /** A reason for an inferred bound pointing to a condition. */
@@ -38,10 +42,16 @@ module CppLangImplConstant implements LangSig<FloatDelta> {
     SemGuard getCond() { this = TSemCondReason(result) }
 
     override string toString() { result = this.getCond().toString() }
+
+    override SemReason combineWith(SemReason reason) {
+      if reason instanceof SemTypeReason then result instanceof SemTypeReason else result = this
+    }
   }
 
   private class SemTypeReason extends SemReason, TSemTypeReason {
     override string toString() { result = "TypeReason" }
+
+    override SemReason combineWith(SemReason reason) { result = this and exists(reason) }
   }
 
   /**

diff --git a/...e/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisRelativeSpecific.qll b/...e/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisRelativeSpecific.qll
@@ -22,6 +22,8 @@ module CppLangImplRelative implements LangSig<FloatDelta> {
   abstract class SemReason extends TSemReason {
     /** Gets a textual representation of this reason. */
     abstract string toString();
+
+    abstract SemReason combineWith(SemReason reason);
   }
 
   class SemValueReason = SemReason;
@@ -32,6 +34,8 @@ module CppLangImplRelative implements LangSig<FloatDelta> {
    */
   class SemNoReason extends SemValueReason, TSemNoReason {
     override string toString() { result = "NoReason" }
+
+    override SemReason combineWith(SemReason reason) { result = reason }
   }
 
   /** A reason for an inferred bound pointing to a condition. */
@@ -40,6 +44,8 @@ module CppLangImplRelative implements LangSig<FloatDelta> {
     SemGuard getCond() { this = TSemCondReason(result) }
 
     override string toString() { result = this.getCond().toString() }
+
+    override SemReason combineWith(SemReason reason) { result = reason }
   }
 
   /**

diff --git a/...l/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll b/...l/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll
@@ -113,7 +113,9 @@ signature module DeltaSig {
 }
 
 signature module LangSig<DeltaSig D> {
-  class SemReason;
+  class SemReason {
+    SemReason combineWith(SemReason reason);
+  }
 
   class SemValueReason extends SemReason;
 
@@ -1120,9 +1122,15 @@ module RangeStage<
         delta = D::fromFloat(D::toFloat(dLeft) + D::toFloat(dRight)) and
         fromBackEdge = fbeLeft.booleanOr(fbeRight)
       |
-        b = bLeft and origdelta = odLeft and reason = rLeft and bRight instanceof SemZeroBound
+        b = bLeft and
+        origdelta = odLeft and
+        reason = rLeft.combineWith(rRight) and
+        bRight instanceof SemZeroBound
         or
-        b = bRight and origdelta = odRight and reason = rRight and bLeft instanceof SemZeroBound
+        b = bRight and
+        origdelta = odRight and
+        reason = rRight.combineWith(rLeft) and
+        bLeft instanceof SemZeroBound
       )
       or
       exists(