From 5dbc273036dc161d02d21fd9a9b9d0a7cf55705d Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Thu, 9 Jan 2025 14:54:46 +0100
Subject: [PATCH] C++: Only propagate smallest/largest range bound in
 conditional expressions

---
 .../cpp/rangeanalysis/SimpleRangeAnalysis.qll | 64 +++++++++++--------
 1 file changed, 38 insertions(+), 26 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll
index 990def8b2f1c1..8d89a46bdb5aa 100644
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll
@@ -773,22 +773,28 @@ private float getLowerBoundsImpl(Expr expr) {
       )
     )
     or
-    // ConditionalExpr (true branch)
-    exists(ConditionalExpr condExpr |
+    exists(ConditionalExpr condExpr, Expr conv, float ub, float lb |
       expr = condExpr and
+      conv = condExpr.getCondition().getFullyConverted() and
       // Use `boolConversionUpperBound` to determine whether the condition
       // might evaluate to `true`.
-      boolConversionUpperBound(condExpr.getCondition().getFullyConverted()) = 1 and
-      result = getFullyConvertedLowerBounds(condExpr.getThen())
-    )
-    or
-    // ConditionalExpr (false branch)
-    exists(ConditionalExpr condExpr |
-      expr = condExpr and
-      // Use `boolConversionLowerBound` to determine whether the condition
-      // might evaluate to `false`.
-      boolConversionLowerBound(condExpr.getCondition().getFullyConverted()) = 0 and
-      result = getFullyConvertedLowerBounds(condExpr.getElse())
+      lb = boolConversionLowerBound(conv) and
+      ub = boolConversionUpperBound(conv)
+    |
+      // Both branches can be taken
+      ub = 1 and
+      lb = 0 and
+      exists(float thenLb, float elseLb |
+        thenLb = getFullyConvertedLowerBounds(condExpr.getThen()) and
+        elseLb = getFullyConvertedLowerBounds(condExpr.getElse()) and
+        result = thenLb.minimum(elseLb)
+      )
+      or
+      // Only the `true` branch can be taken
+      ub = 1 and lb != 0 and result = getFullyConvertedLowerBounds(condExpr.getThen())
+      or
+      // Only the `false` branch can be taken
+      ub != 1 and lb = 0 and result = getFullyConvertedLowerBounds(condExpr.getElse())
     )
     or
     exists(AddExpr addExpr, float xLow, float yLow |
@@ -977,22 +983,28 @@ private float getUpperBoundsImpl(Expr expr) {
       )
     )
     or
-    // ConditionalExpr (true branch)
-    exists(ConditionalExpr condExpr |
+    exists(ConditionalExpr condExpr, Expr conv, float ub, float lb |
       expr = condExpr and
+      conv = condExpr.getCondition().getFullyConverted() and
       // Use `boolConversionUpperBound` to determine whether the condition
       // might evaluate to `true`.
-      boolConversionUpperBound(condExpr.getCondition().getFullyConverted()) = 1 and
-      result = getFullyConvertedUpperBounds(condExpr.getThen())
-    )
-    or
-    // ConditionalExpr (false branch)
-    exists(ConditionalExpr condExpr |
-      expr = condExpr and
-      // Use `boolConversionLowerBound` to determine whether the condition
-      // might evaluate to `false`.
-      boolConversionLowerBound(condExpr.getCondition().getFullyConverted()) = 0 and
-      result = getFullyConvertedUpperBounds(condExpr.getElse())
+      lb = boolConversionLowerBound(conv) and
+      ub = boolConversionUpperBound(conv)
+    |
+      // Both branches can be taken
+      ub = 1 and
+      lb = 0 and
+      exists(float thenLb, float elseLb |
+        thenLb = getFullyConvertedUpperBounds(condExpr.getThen()) and
+        elseLb = getFullyConvertedUpperBounds(condExpr.getElse()) and
+        result = thenLb.maximum(elseLb)
+      )
+      or
+      // Only the `true` branch can be taken
+      ub = 1 and lb != 0 and result = getFullyConvertedUpperBounds(condExpr.getThen())
+      or
+      // Only the `false` branch can be taken
+      ub != 1 and lb = 0 and result = getFullyConvertedUpperBounds(condExpr.getElse())
     )
     or
     exists(AddExpr addExpr, float xHigh, float yHigh |