C++: add overflow detection to new range analysis by rdmarsh2 · Pull Request #12599 · github/codeql

rdmarsh2 · 2023-03-20T18:36:46Z

No description provided.

MathiasVP

I've done a first pass over the PR, but I think I'd like another round before I claim to fully understand what's going on. In the meantime, we should:

Fix the merge conflicts. 700a566 makes me think some of the changes have already been merged into main.
Check the performance on this. I suggest you follow the approach I had here: #11928 (comment)

MathiasVP · 2023-03-21T10:41:07Z

+  predicate typeBounds(SemType t, float lb, float ub) {
+    exists(SemIntegerType integralType, float limit |
+      integralType = t and limit = 2.pow(8 * integralType.getByteSize())
+    |
+      if integralType instanceof SemBooleanType
+      then lb = 0 and ub = 1
+      else
+        if integralType.isSigned()
+        then (
+          lb = -(limit / 2) and ub = (limit / 2) - 1
+        ) else (
+          lb = 0 and ub = limit - 1
+        )
+    )
+    or
+    // This covers all floating point types. The range is (-Inf, +Inf).
+    t instanceof SemFloatingPointType and lb = -(1.0 / 0.0) and ub = 1.0 / 0.0
+  }


This looked super scary until I realized it was copy/pasted from SimpleRangeAnalysis.

MathiasVP · 2023-03-21T10:43:17Z

 import cpp
 import experimental.semmle.code.cpp.semantic.analysis.ModulusAnalysis
-import experimental.semmle.code.cpp.semantic.Semantic
+//import experimental.semmle.code.cpp.semantic.Semantic


Why is this commented out? Should we just delete it?

MathiasVP · 2023-03-21T10:44:45Z

+signature module OverflowSig<DeltaSig D> {
+  predicate semExprDoesntOverflow(boolean positively, SemExpr expr);
+}


I think this module signature (and its one predicate) could use some QLDoc.

Nitpicking: could we also write the predicate as semExprDoesNotOverflow. It took me a while to parse Doesnt 😅

MathiasVP · 2023-03-21T11:09:07Z

+      typeBounds(expr.getSemType(), lb, ub) and 
+      ConstantStage::initialBounded(expr, any(ConstantBounds::SemZeroBound b), delta, positively.booleanNot(), _, _, _)
+    |
+      positively = true and delta < ub
+      or
+      positively = false and delta > lb
+    )


Just checking my understanding here: We're finding the minimum and maximum values from the the of expr, and then we're comparing those values with the bounds we can obtain from the constant stage.

I'm not sure I understand the logic, though. If we're trying to deduce that expr doesn't overflow positively, we're checking whether delta (which is the lower bound of expr) is less than the maximum value of the type? Shouldn't this be the other way around? Or have I confused myself?

MathiasVP · 2023-03-21T11:09:36Z

+/*
+  predicate semExprOverflow(float delta, boolean upper, SemExpr expr) {
+    exists(float lb, float ub | typeBounds(expr.getSemType(), lb, ub) |
+      upper = false and delta < lb
+      or
+      upper = true and delta > ub
+    )
+  }
+  */


Should this be deleted?

MathiasVP · 2023-03-21T11:19:47Z

 * due to a conversion.
 */
-predicate exprMightOverflowPositively(Expr expr) { none() }
+predicate exprMightOverflowPositively(Expr expr) { upperBound(expr) > exprMaxVal(expr) }


I was confused about this for a second: we only generate bounds for expressions that won't overflow (due to the disjunction in the bounded predicate), but here it looks like we're looking for expressions that actually do have an overflowing upper bound. However, this works because upperBound is defined to only use the constant stage of range-analysis which doesn't (and can't) have that disjunction that rules out overflowing expressions. Is this correct?

Could we write this explicitly in a comment here, or add QLDoc to upperBound and lowerBound to make this clear?

MathiasVP · 2023-03-21T11:28:35Z

  int total = 0;
  for (i = 0; i < 2; i = i+1) {
-    range(i); // $ range=<=1 range=>=0
+    range(i); // $ range=<=1 MISSING: range=>=0


Are we losing these results because we're now claiming that i+1 on line 41 overflows?

In general: Should we add an InlineExpectationsTest that highlights all the places where we're claiming an overflow might occur. This would give me a lot more confidence in what's actually going on here.

jketema · 2023-03-22T10:19:37Z

+    positively = false and
+    (
+      expr.getOpcode() instanceof Opcode::Negate or
+      expr.getOpcode() instanceof Opcode::SubOne
+    )
+    or
+    positively = false and
+    expr.(SemDivExpr).getSemType() instanceof SemFloatingPointType


Suggested change

positively = false and

(

expr.getOpcode() instanceof Opcode::Negate or

expr.getOpcode() instanceof Opcode::SubOne

)

or

positively = false and

expr.(SemDivExpr).getSemType() instanceof SemFloatingPointType

positively = false and

(

expr.getOpcode() instanceof Opcode::Negate or

expr.getOpcode() instanceof Opcode::SubOne or

expr.(SemDivExpr).getSemType() instanceof SemFloatingPointType

)

MathiasVP

Thanks for pushing through with this, Robert! I have a few comments, but it's mostly just to help my understanding.

Co-authored-by: Mathias Vorreiter Pedersen <mathiasvp@github.com>

MathiasVP · 2023-04-13T21:36:13Z

DCA is showing a really bad join in potentiallyOverflowingExpr (for example, when running on ImageMagick-ImageMagick) 😂.

Before: ``` Tuple counts for RangeAnalysisStage#38d7ce80::RangeStage#FloatDelta#0eab55d1::FloatDelta#RangeAnalysisImpl#edd69a76::ConstantBounds#FloatDelta#0eab55d1::FloatOverflow#RangeAnalysisConstantSpecific#878f81e8::CppLangImplConstant#RangeUtils#6da26777::RangeUtil#FloatDelta#0eab55d1::FloatDelta#RangeAnalysisConstantSpecific#878f81e8::CppLangImplConstant##::potentiallyOverflowingExpr#2#ff/2@36ed7auu after 42.1s: 365 ~0% {2} r1 = JOIN num#SemanticOpcode#e6f455a5::TNegate#f WITH SemanticExpr#91573b9a::SemExpr::getOpcode#0#dispred#fb_10#join_rhs ON FIRST 1 OUTPUT false, Rhs.1 'expr' 0 ~0% {2} r2 = JOIN num#SemanticOpcode#e6f455a5::TSubOne#f WITH SemanticExpr#91573b9a::SemExpr::getOpcode#0#dispred#fb_10#join_rhs ON FIRST 1 OUTPUT false, Rhs.1 'expr' 365 ~0% {2} r3 = r1 UNION r2 0 ~0% {2} r4 = JOIN num#SemanticOpcode#e6f455a5::TAddOne#f WITH project#SemanticExpr#91573b9a::SemKnownExpr#class#fff_10#join_rhs ON FIRST 1 OUTPUT true, Rhs.1 'expr' 2 ~0% {2} r5 = JOIN m#RangeAnalysisStage#38d7ce80::RangeStage#FloatDelta#0eab55d1::FloatDelta#RangeAnalysisImpl#edd69a76::ConstantBounds#FloatDelta#0eab55d1::FloatOverflow#RangeAnalysisConstantSpecific#878f81e8::CppLangImplConstant#RangeUtils#6da26777::RangeUtil#FloatDelta#0eab55d1::FloatDelta#RangeAnalysisConstantSpecific#878f81e8::CppLangImplConstant##::boundedPhiInp1#6#ffbfff WITH num#SemanticOpcode#e6f455a5::TMul#f CARTESIAN PRODUCT OUTPUT Rhs.0, Lhs.0 'positively' 22026 ~0% {2} r6 = JOIN r5 WITH SemanticExpr#91573b9a::SemExpr::getOpcode#0#dispred#fb_10#join_rhs ON FIRST 1 OUTPUT Lhs.1 'positively', Rhs.1 'expr' 2 ~0% {2} r7 = JOIN m#RangeAnalysisStage#38d7ce80::RangeStage#FloatDelta#0eab55d1::FloatDelta#RangeAnalysisImpl#edd69a76::ConstantBounds#FloatDelta#0eab55d1::FloatOverflow#RangeAnalysisConstantSpecific#878f81e8::CppLangImplConstant#RangeUtils#6da26777::RangeUtil#FloatDelta#0eab55d1::FloatDelta#RangeAnalysisConstantSpecific#878f81e8::CppLangImplConstant##::boundedPhiInp1#6#ffbfff WITH num#SemanticOpcode#e6f455a5::TShiftLeft#f CARTESIAN PRODUCT OUTPUT Rhs.0, Lhs.0 'positively' 1978 ~0% {2} r8 = JOIN r7 WITH SemanticExpr#91573b9a::SemExpr::getOpcode#0#dispred#fb_10#join_rhs ON FIRST 1 OUTPUT Lhs.1 'positively', Rhs.1 'expr' 24004 ~0% {2} r9 = r6 UNION r8 24004 ~0% {2} r10 = r4 UNION r9 24369 ~0% {2} r11 = r3 UNION r10 2726 ~1% {2} r12 = JOIN project#SemanticExpr#91573b9a::SemDivExpr#fffff WITH project#SemanticExpr#91573b9a::SemKnownExpr#class#fff#2 ON FIRST 1 OUTPUT Rhs.1, Lhs.0 'expr' 1900 ~2% {2} r13 = JOIN r12 WITH SemanticType#3725723c::SemFloatingPointType#ff ON FIRST 1 OUTPUT false, Lhs.1 'expr' 4500 ~0% {1} r14 = JOIN SemanticExpr#91573b9a::SemExpr::getOpcode#0#dispred#fb_10#join_rhs WITH num#SemanticOpcode#e6f455a5::TAdd#f ON FIRST 1 OUTPUT Lhs.1 'expr' 0 ~0% {1} r15 = JOIN SemanticExpr#91573b9a::SemExpr::getOpcode#0#dispred#fb_10#join_rhs WITH num#SemanticOpcode#e6f455a5::TPointerAdd#f ON FIRST 1 OUTPUT Lhs.1 'expr' 4500 ~0% {1} r16 = r14 UNION r15 4000 ~0% {2} r17 = JOIN r16 WITH project#SemanticExpr#91573b9a::SemBinaryExpr#fffff#2 ON FIRST 1 OUTPUT Rhs.1, Lhs.0 'expr' 7000 ~0% {2} r18 = JOIN r17 WITH SignAnalysisCommon#4b1623af::SignAnalysis#FloatDelta#0eab55d1::FloatDelta#RangeUtils#6da26777::RangeUtil#FloatDelta#0eab55d1::FloatDelta#RangeAnalysisConstantSpecific#878f81e8::CppLangImplConstant##::semExprSign#1#ff ON FIRST 1 OUTPUT Rhs.1, Lhs.1 'expr' 1264 ~0% {2} r19 = JOIN r18 WITH num#Sign#2ecc774b::TNeg#f ON FIRST 1 OUTPUT Lhs.0, Lhs.1 'expr' 188324151 ~0% {2} r20 = JOIN r19 WITH SignAnalysisCommon#4b1623af::SignAnalysis#FloatDelta#0eab55d1::FloatDelta#RangeUtils#6da26777::RangeUtil#FloatDelta#0eab55d1::FloatDelta#RangeAnalysisConstantSpecific#878f81e8::CppLangImplConstant##::semExprSign#1#ff_10#join_rhs ON FIRST 1 OUTPUT Lhs.1 'expr', Rhs.1 1000 ~0% {2} r21 = JOIN r20 WITH project#SemanticExpr#91573b9a::SemBinaryExpr#fffff ON FIRST 2 OUTPUT false, Lhs.0 'expr' 2900 ~0% {2} r22 = r13 UNION r21 3259 ~2% {2} r23 = JOIN r18 WITH num#Sign#2ecc774b::TPos#f ON FIRST 1 OUTPUT Lhs.0, Lhs.1 'expr' 1521124720 ~0% {2} r24 = JOIN r23 WITH SignAnalysisCommon#4b1623af::SignAnalysis#FloatDelta#0eab55d1::FloatDelta#RangeUtils#6da26777::RangeUtil#FloatDelta#0eab55d1::FloatDelta#RangeAnalysisConstantSpecific#878f81e8::CppLangImplConstant##::semExprSign#1#ff_10#join_rhs ON FIRST 1 OUTPUT Lhs.1 'expr', Rhs.1 3000 ~2% {2} r25 = JOIN r24 WITH project#SemanticExpr#91573b9a::SemBinaryExpr#fffff ON FIRST 2 OUTPUT true, Lhs.0 'expr' ``` (I stopped evaluation midway.) After: ```ql Evaluated relational algebra for predicate RangeAnalysisStage#38d7ce80::RangeStage#FloatDelta#0eab55d1::FloatDelta#RangeAnalysisImpl#edd69a76::ConstantBounds#FloatDelta#0eab55d1::FloatOverflow#RangeAnalysisConstantSpecific#878f81e8::CppLangImplConstant#RangeUtils#6da26777::RangeUtil#FloatDelta#0eab55d1::FloatDelta#RangeAnalysisConstantSpecific#878f81e8::CppLangImplConstant##::potentiallyOverflowingExpr#2#ff@dc3a0712 with tuple counts: 26269 ~2% {2} r1 = _SemanticExpr#91573b9a::SemExpr::getOpcode#0#dispred#fb_10#join_rhs_m#RangeAnalysisStage#38d7ce80::R__#shared UNION _SemanticExpr#91573b9a::SemExpr::getOpcode#0#dispred#fb_10#join_rhs_SemanticType#3725723c::SemFloati__#shared 26269 ~2% {2} r2 = _num#SemanticOpcode#e6f455a5::TAddOne#f_project#SemanticExpr#91573b9a::SemKnownExpr#class#fff_10#joi__#shared UNION r1 41333 ~1% {2} r3 = JOIN _SemanticExpr#91573b9a::SemExpr::getOpcode#0#dispred#fb_10#join_rhs_num#SemanticOpcode#e6f455a5::TAd__#shared WITH SignAnalysisCommon#4b1623af::SignAnalysis#FloatDelta#0eab55d1::FloatDelta#RangeUtils#6da26777::RangeUtil#FloatDelta#0eab55d1::FloatDelta#RangeAnalysisConstantSpecific#878f81e8::CppLangImplConstant##::semExprSign#1#ff ON FIRST 1 OUTPUT Rhs.1, Lhs.1 5806 ~2% {2} r4 = JOIN r3 WITH num#Sign#2ecc774b::TNeg#f ON FIRST 1 OUTPUT Lhs.1, Lhs.0 5806 ~1% {3} r5 = JOIN r4 WITH project#SemanticExpr#91573b9a::SemBinaryExpr#fffff#2 ON FIRST 1 OUTPUT Rhs.1, Lhs.1, Lhs.0 3612 ~0% {2} r6 = JOIN r5 WITH SignAnalysisCommon#4b1623af::SignAnalysis#FloatDelta#0eab55d1::FloatDelta#RangeUtils#6da26777::RangeUtil#FloatDelta#0eab55d1::FloatDelta#RangeAnalysisConstantSpecific#878f81e8::CppLangImplConstant##::semExprSign#1#ff ON FIRST 2 OUTPUT false, Lhs.2 18476 ~1% {2} r7 = JOIN r3 WITH num#Sign#2ecc774b::TPos#f ON FIRST 1 OUTPUT Lhs.1, Lhs.0 18476 ~1% {3} r8 = JOIN r7 WITH project#SemanticExpr#91573b9a::SemBinaryExpr#fffff#2 ON FIRST 1 OUTPUT Rhs.1, Lhs.1, Lhs.0 18444 ~2% {2} r9 = JOIN r8 WITH SignAnalysisCommon#4b1623af::SignAnalysis#FloatDelta#0eab55d1::FloatDelta#RangeUtils#6da26777::RangeUtil#FloatDelta#0eab55d1::FloatDelta#RangeAnalysisConstantSpecific#878f81e8::CppLangImplConstant##::semExprSign#1#ff ON FIRST 2 OUTPUT true, Lhs.2 22056 ~0% {2} r10 = r6 UNION r9 24137 ~2% {2} r11 = JOIN _SemanticExpr#91573b9a::SemExpr::getOpcode#0#dispred#fb_10#join_rhs_num#SemanticOpcode#e6f455a5::TPo__#shared WITH SignAnalysisCommon#4b1623af::SignAnalysis#FloatDelta#0eab55d1::FloatDelta#RangeUtils#6da26777::RangeUtil#FloatDelta#0eab55d1::FloatDelta#RangeAnalysisConstantSpecific#878f81e8::CppLangImplConstant##::semExprSign#1#ff ON FIRST 1 OUTPUT Rhs.1, Lhs.1 16966 ~2% {1} r12 = JOIN r11 WITH num#Sign#2ecc774b::TPos#f ON FIRST 1 OUTPUT Lhs.1 16966 ~4% {2} r13 = JOIN r12 WITH project#SemanticExpr#91573b9a::SemBinaryExpr#fffff ON FIRST 1 OUTPUT Rhs.1, Lhs.0 24917 ~1% {2} r14 = JOIN r13 WITH SignAnalysisCommon#4b1623af::SignAnalysis#FloatDelta#0eab55d1::FloatDelta#RangeUtils#6da26777::RangeUtil#FloatDelta#0eab55d1::FloatDelta#RangeAnalysisConstantSpecific#878f81e8::CppLangImplConstant##::semExprSign#1#ff ON FIRST 1 OUTPUT Rhs.1, Lhs.1 2781 ~0% {2} r15 = JOIN r14 WITH num#Sign#2ecc774b::TNeg#f ON FIRST 1 OUTPUT false, Lhs.1 2817 ~0% {1} r16 = JOIN r11 WITH num#Sign#2ecc774b::TNeg#f ON FIRST 1 OUTPUT Lhs.1 2817 ~0% {2} r17 = JOIN r16 WITH project#SemanticExpr#91573b9a::SemBinaryExpr#fffff ON FIRST 1 OUTPUT Rhs.1, Lhs.0 6922 ~0% {2} r18 = JOIN r17 WITH SignAnalysisCommon#4b1623af::SignAnalysis#FloatDelta#0eab55d1::FloatDelta#RangeUtils#6da26777::RangeUtil#FloatDelta#0eab55d1::FloatDelta#RangeAnalysisConstantSpecific#878f81e8::CppLangImplConstant##::semExprSign#1#ff ON FIRST 1 OUTPUT Rhs.1, Lhs.1 2765 ~1% {2} r19 = JOIN r18 WITH num#Sign#2ecc774b::TPos#f ON FIRST 1 OUTPUT true, Lhs.1 5546 ~0% {2} r20 = r15 UNION r19 27602 ~0% {2} r21 = r10 UNION r20 53871 ~0% {2} r22 = r2 UNION r21 return r22 ```

MathiasVP · 2023-04-17T08:29:48Z

@rdmarsh2 I've pushed a join-order fix, and I'll restart DCA.

MathiasVP

LGTM!

rdmarsh2 requested a review from a team as a code owner March 20, 2023 18:36

github-actions Bot added the C++ label Mar 20, 2023

MathiasVP added the no-change-note-required This PR does not need a change note label Mar 21, 2023

MathiasVP reviewed Mar 21, 2023

View reviewed changes

Robert Marsh added 2 commits March 21, 2023 11:01

C++: Add overflow detection to new range analysis

0f4157c

C++: Move overflow detection to SimpleRangeAnalysis.qll

204dbee

rdmarsh2 force-pushed the rdmarsh2/range-analysis-overflow branch from 3c49432 to 204dbee Compare March 21, 2023 15:02

jketema reviewed Mar 22, 2023

View reviewed changes

Robert Marsh added 6 commits March 23, 2023 11:59

C++: SimpleRangeAnalysis wrapper uses constant stage

7ea74df

Merge branch 'main' into rdmarsh2/range-analysis-overflow

4b4fc97

C++: fix SimpleRangeAnalysis for equivclass SemExpr

868b238

C++: sign analysis in potentiallyOverflowingExpr

2606abf

C++: More fixes to overflow detection

e4ae957

Merge branch 'main' into rdmarsh2/range-analysis-overflow

915c969

MathiasVP reviewed Apr 6, 2023

View reviewed changes

rdmarsh2 and others added 3 commits April 11, 2023 10:41

C++: remove commented-out code

18c3feb

Co-authored-by: Mathias Vorreiter Pedersen <mathiasvp@github.com>

C++: respond to overflow PR comments

316cb95

C++: autoformat

fddbffe

MathiasVP and others added 2 commits April 17, 2023 09:34

C++: Autoformat.

2a14479

C++: fix test after module rename

ea7996f

MathiasVP previously approved these changes Apr 17, 2023

View reviewed changes

C++: autoformat

2b41aef

rdmarsh2 dismissed MathiasVP’s stale review via 2b41aef April 17, 2023 15:36

MathiasVP previously approved these changes Apr 17, 2023

View reviewed changes

C++: another 'fix test after module rename'.

d833850

MathiasVP dismissed their stale review via d833850 April 17, 2023 16:49

MathiasVP approved these changes Apr 17, 2023

View reviewed changes

MathiasVP merged commit bb8c3de into github:main Apr 17, 2023

Conversation

rdmarsh2 commented Mar 20, 2023

Uh oh!

MathiasVP left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

MathiasVP left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

MathiasVP commented Apr 13, 2023

Uh oh!

MathiasVP commented Apr 17, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

MathiasVP left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

MathiasVP commented Apr 17, 2023 •

edited

Loading