@@ -22,11 +22,13 @@ import semmle.code.cpp.dataflow.DataFlow
2222 * Holds if `sub` is guarded by a condition which ensures that
2323 * `left >= right`.
2424 */
25- pragma [ noinline ]
25+ pragma [ nomagic ]
2626predicate isGuarded ( SubExpr sub , Expr left , Expr right ) {
27- exists ( GuardCondition guard , int k |
28- guard .controls ( sub .getBasicBlock ( ) , _) and
29- guard .ensuresLt ( left , right , k , sub .getBasicBlock ( ) , false ) and
27+ exprIsSubLeftOrLess ( pragma [ only_bind_into ] ( sub ) , _) and // Manual magic
28+ exists ( GuardCondition guard , int k , BasicBlock bb |
29+ pragma [ only_bind_into ] ( bb ) = sub .getBasicBlock ( ) and
30+ guard .controls ( pragma [ only_bind_into ] ( bb ) , _) and
31+ guard .ensuresLt ( left , right , k , bb , false ) and
3032 k >= 0
3133 )
3234}
@@ -36,47 +38,56 @@ predicate isGuarded(SubExpr sub, Expr left, Expr right) {
3638 * `sub.getLeftOperand()`.
3739 */
3840predicate exprIsSubLeftOrLess ( SubExpr sub , DataFlow:: Node n ) {
39- n .asExpr ( ) = sub .getLeftOperand ( )
40- or
41- exists ( DataFlow:: Node other |
42- // dataflow
43- exprIsSubLeftOrLess ( sub , other ) and
44- (
45- DataFlow:: localFlowStep ( n , other ) or
46- DataFlow:: localFlowStep ( other , n )
41+ interestingSubExpr ( sub , _) and // Manual magic
42+ (
43+ n .asExpr ( ) = sub .getLeftOperand ( )
44+ or
45+ exists ( DataFlow:: Node other |
46+ // dataflow
47+ exprIsSubLeftOrLess ( sub , other ) and
48+ (
49+ DataFlow:: localFlowStep ( n , other ) or
50+ DataFlow:: localFlowStep ( other , n )
51+ )
52+ )
53+ or
54+ exists ( DataFlow:: Node other |
55+ // guard constraining `sub`
56+ exprIsSubLeftOrLess ( sub , other ) and
57+ isGuarded ( sub , other .asExpr ( ) , n .asExpr ( ) ) // other >= n
58+ )
59+ or
60+ exists ( DataFlow:: Node other , float p , float q |
61+ // linear access of `other`
62+ exprIsSubLeftOrLess ( sub , other ) and
63+ linearAccess ( n .asExpr ( ) , other .asExpr ( ) , p , q ) and // n = p * other + q
64+ p <= 1 and
65+ q <= 0
66+ )
67+ or
68+ exists ( DataFlow:: Node other , float p , float q |
69+ // linear access of `n`
70+ exprIsSubLeftOrLess ( sub , other ) and
71+ linearAccess ( other .asExpr ( ) , n .asExpr ( ) , p , q ) and // other = p * n + q
72+ p >= 1 and
73+ q >= 0
4774 )
48- )
49- or
50- exists ( DataFlow:: Node other |
51- // guard constraining `sub`
52- exprIsSubLeftOrLess ( sub , other ) and
53- isGuarded ( sub , other .asExpr ( ) , n .asExpr ( ) ) // other >= n
54- )
55- or
56- exists ( DataFlow:: Node other , float p , float q |
57- // linear access of `other`
58- exprIsSubLeftOrLess ( sub , other ) and
59- linearAccess ( n .asExpr ( ) , other .asExpr ( ) , p , q ) and // n = p * other + q
60- p <= 1 and
61- q <= 0
62- )
63- or
64- exists ( DataFlow:: Node other , float p , float q |
65- // linear access of `n`
66- exprIsSubLeftOrLess ( sub , other ) and
67- linearAccess ( other .asExpr ( ) , n .asExpr ( ) , p , q ) and // other = p * n + q
68- p >= 1 and
69- q >= 0
7075 )
7176}
7277
73- from RelationalOperation ro , SubExpr sub
74- where
75- not isFromMacroDefinition ( ro ) and
78+ predicate interestingSubExpr ( SubExpr sub , RelationalOperation ro ) {
7679 not isFromMacroDefinition ( sub ) and
7780 ro .getLesserOperand ( ) .getValue ( ) .toInt ( ) = 0 and
7881 ro .getGreaterOperand ( ) = sub and
7982 sub .getFullyConverted ( ) .getUnspecifiedType ( ) .( IntegralType ) .isUnsigned ( ) and
80- exprMightOverflowNegatively ( sub .getFullyConverted ( ) ) and // generally catches false positives involving constants
81- not exprIsSubLeftOrLess ( sub , DataFlow:: exprNode ( sub .getRightOperand ( ) ) ) // generally catches false positives where there's a relation between the left and right operands
83+ // generally catches false positives involving constants
84+ exprMightOverflowNegatively ( sub .getFullyConverted ( ) )
85+ }
86+
87+ from RelationalOperation ro , SubExpr sub
88+ where
89+ interestingSubExpr ( sub , ro ) and
90+ not isFromMacroDefinition ( ro ) and
91+ // generally catches false positives where there's a relation between the left and right operands
92+ not exprIsSubLeftOrLess ( sub , DataFlow:: exprNode ( sub .getRightOperand ( ) ) )
8293select ro , "Unsigned subtraction can never be negative."
0 commit comments