From 5e14b5cca753bfaf0097c19ded18c6b2987c8dde Mon Sep 17 00:00:00 2001 From: Mathias Vorreiter Pedersen Date: Wed, 16 Aug 2023 12:09:42 +0100 Subject: [PATCH 1/2] C++: 'origDelta' should always be 'odLeft' when deriving subtraction ranges. --- .../semantic/analysis/RangeAnalysisStage.qll | 13 +++---------- 1 file changed, 3 insertions(+), 10 deletions(-) diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll index ee87eab1f1c9..5d8b01785233 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll @@ -1106,12 +1106,9 @@ module RangeStage< b = bRight and origdelta = odRight and reason = rRight and bLeft instanceof SemZeroBound ) or - exists( - D::Delta dLeft, D::Delta dRight, boolean fbeLeft, boolean fbeRight, D::Delta odLeft, - D::Delta odRight, SemReason rLeft, SemReason rRight - | - boundedSubOperandLeft(e, upper, b, dLeft, fbeLeft, odLeft, rLeft) and - boundedSubOperandRight(e, upper, dRight, fbeRight, odRight, rRight) and + exists(D::Delta dLeft, D::Delta dRight, boolean fbeLeft, boolean fbeRight | + boundedSubOperandLeft(e, upper, b, dLeft, fbeLeft, origdelta, reason) and + boundedSubOperandRight(e, upper, dRight, fbeRight, _, _) and // when `upper` is `true` we have: // left <= b + dLeft // right >= 0 + dRight @@ -1124,10 +1121,6 @@ module RangeStage< // = b + (dLeft - dRight) delta = D::fromFloat(D::toFloat(dLeft) - D::toFloat(dRight)) and fromBackEdge = fbeLeft.booleanOr(fbeRight) - | - origdelta = odLeft and reason = rLeft - or - origdelta = odRight and reason = rRight ) or exists( From 20df63f26d75e79b76c22c2152384da501a900ae Mon Sep 17 00:00:00 2001 From: Mathias Vorreiter Pedersen Date: Wed, 16 Aug 2023 12:50:41 +0100 Subject: [PATCH 2/2] C++: Respond to review comments. --- .../internal/semantic/analysis/RangeAnalysisStage.qll | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll index 5d8b01785233..0bd665ed10cf 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll @@ -1108,7 +1108,7 @@ module RangeStage< or exists(D::Delta dLeft, D::Delta dRight, boolean fbeLeft, boolean fbeRight | boundedSubOperandLeft(e, upper, b, dLeft, fbeLeft, origdelta, reason) and - boundedSubOperandRight(e, upper, dRight, fbeRight, _, _) and + boundedSubOperandRight(e, upper, dRight, fbeRight) and // when `upper` is `true` we have: // left <= b + dLeft // right >= 0 + dRight @@ -1210,13 +1210,12 @@ module RangeStage< */ pragma[nomagic] private predicate boundedSubOperandRight( - SemSubExpr sub, boolean upper, D::Delta delta, boolean fromBackEdge, D::Delta origdelta, - SemReason reason + SemSubExpr sub, boolean upper, D::Delta delta, boolean fromBackEdge ) { // `semValueFlowStep` already handles the case where one of the operands is a constant. not semValueFlowStep(sub, _, _) and - bounded(sub.getRightOperand(), any(SemZeroBound zb), delta, upper.booleanNot(), fromBackEdge, - origdelta, reason) + bounded(sub.getRightOperand(), any(SemZeroBound zb), delta, upper.booleanNot(), fromBackEdge, _, + _) } pragma[nomagic]