hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2025-12-24 04:36:35 +01:00
Code Issues Packages Projects Releases Wiki Activity

C++: respond to overflow PR comments

Browse Source
This commit is contained in:
Robert Marsh
2023-04-13 10:03:55 -04:00
parent 18c3feb9d8
commit 316cb95547
6 changed files with 11 additions and 21 deletions
Download Patch File Download Diff File Expand all files Collapse all files

13
cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/FloatDelta.qll
View File

@@ -21,7 +21,7 @@ module FloatDelta implements DeltaSig {
}
module FloatOverflow implements OverflowSig<FloatDelta> {
predicate semExprDoesntOverflow(boolean positively, SemExpr expr) {
predicate semExprDoesNotOverflow(boolean positively, SemExpr expr) {
exists(float lb, float ub, float delta |
typeBounds(expr.getSemType(), lb, ub) and
ConstantStage::initialBounded(expr, any(ConstantBounds::SemZeroBound b), delta, positively, _, _, _)
@@ -31,17 +31,8 @@ module FloatOverflow implements OverflowSig<FloatDelta> {
positively = false and delta > lb
)
}
/*
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
)
}
*/
predicate typeBounds(SemType t, float lb, float ub) {
additional predicate typeBounds(SemType t, float lb, float ub) {
exists(SemIntegerType integralType, float limit |
integralType = t and limit = 2.pow(8 * integralType.getByteSize())
|

2
cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisSpecific.qll → cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisConstantSpecific.qll
View File

@@ -6,7 +6,7 @@ private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
private import RangeAnalysisStage
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta
module CppLangImpl implements LangSig<FloatDelta> {
module CppLangImplConstant implements LangSig<FloatDelta> {
/**
* Holds if the specified expression should be excluded from the result of `ssaRead()`.
*

7
cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll
View File

@@ -1,5 +1,6 @@
private import RangeAnalysisStage
private import RangeAnalysisSpecific
private import RangeAnalysisConstantSpecific
private import RangeAnalysisRelativeSpecific
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta
private import RangeUtils
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticBound as SemanticBound
@@ -47,10 +48,10 @@ module RelativeBounds implements BoundSig<FloatDelta> {
}
module ConstantStage =
RangeStage<FloatDelta, ConstantBounds, FloatOverflow, CppLangImpl, RangeUtil<FloatDelta, CppLangImpl>>;
RangeStage<FloatDelta, ConstantBounds, FloatOverflow, CppLangImplConstant, RangeUtil<FloatDelta, CppLangImplConstant>>;
module RelativeStage =
RangeStage<FloatDelta, RelativeBounds, FloatOverflow, CppLangImpl, RangeUtil<FloatDelta, CppLangImpl>>;
RangeStage<FloatDelta, RelativeBounds, FloatOverflow, CppLangImplRelative, RangeUtil<FloatDelta, CppLangImplRelative>>;
private newtype TSemReason =
TSemNoReason() or

2
cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisSpecific2.qll → cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisRelativeSpecific.qll
View File

@@ -9,7 +9,7 @@ private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.IntD
private import RangeAnalysisImpl
private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
module CppLangImpl2 implements LangSig<FloatDelta> {
module CppLangImplRelative implements LangSig<FloatDelta> {
/**
* Holds if the specified expression should be excluded from the result of `ssaRead()`.
*

6
cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll
View File

@@ -242,7 +242,7 @@ signature module BoundSig<DeltaSig D> {
}
signature module OverflowSig<DeltaSig D> {
predicate semExprDoesntOverflow(boolean positively, SemExpr expr);
predicate semExprDoesNotOverflow(boolean positively, SemExpr expr);
}
module RangeStage<
@@ -935,12 +935,10 @@ module RangeStage<
) {
initialBounded(e, b, delta, upper, fromBackEdge, origdelta, reason) and
(
semExprDoesntOverflow(upper.booleanNot(), e)
semExprDoesNotOverflow(upper.booleanNot(), e)
or
not potentiallyOverflowingExpr(upper.booleanNot(), e)
or
initialBounded(e, any(SemZeroBound z), _, upper.booleanNot(), _, _, _)
or
exists(D::Delta otherDelta |
initialBounded(e, _, otherDelta, upper.booleanNot(), _, _, _) and
(

2
cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll
View File

@@ -3,7 +3,7 @@
*/
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
private import RangeAnalysisSpecific
private import RangeAnalysisRelativeSpecific
private import RangeAnalysisStage as Range
private import ConstantAnalysis