@@ -38,47 +38,56 @@ predicate isGuarded(SubExpr sub, Expr left, Expr right) {
38
38
* `sub.getLeftOperand()`.
39
39
*/
40
40
predicate exprIsSubLeftOrLess ( SubExpr sub , DataFlow:: Node n ) {
41
- n .asExpr ( ) = sub .getLeftOperand ( )
42
- or
43
- exists ( DataFlow:: Node other |
44
- // dataflow
45
- exprIsSubLeftOrLess ( sub , other ) and
46
- (
47
- DataFlow:: localFlowStep ( n , other ) or
48
- 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
49
74
)
50
- )
51
- or
52
- exists ( DataFlow:: Node other |
53
- // guard constraining `sub`
54
- exprIsSubLeftOrLess ( sub , other ) and
55
- isGuarded ( sub , other .asExpr ( ) , n .asExpr ( ) ) // other >= n
56
- )
57
- or
58
- exists ( DataFlow:: Node other , float p , float q |
59
- // linear access of `other`
60
- exprIsSubLeftOrLess ( sub , other ) and
61
- linearAccess ( n .asExpr ( ) , other .asExpr ( ) , p , q ) and // n = p * other + q
62
- p <= 1 and
63
- q <= 0
64
- )
65
- or
66
- exists ( DataFlow:: Node other , float p , float q |
67
- // linear access of `n`
68
- exprIsSubLeftOrLess ( sub , other ) and
69
- linearAccess ( other .asExpr ( ) , n .asExpr ( ) , p , q ) and // other = p * n + q
70
- p >= 1 and
71
- q >= 0
72
75
)
73
76
}
74
77
75
- from RelationalOperation ro , SubExpr sub
76
- where
77
- not isFromMacroDefinition ( ro ) and
78
+ predicate interestingSubExpr ( SubExpr sub , RelationalOperation ro ) {
78
79
not isFromMacroDefinition ( sub ) and
79
80
ro .getLesserOperand ( ) .getValue ( ) .toInt ( ) = 0 and
80
81
ro .getGreaterOperand ( ) = sub and
81
82
sub .getFullyConverted ( ) .getUnspecifiedType ( ) .( IntegralType ) .isUnsigned ( ) and
82
- exprMightOverflowNegatively ( sub .getFullyConverted ( ) ) and // generally catches false positives involving constants
83
- 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 ( ) ) )
84
93
select ro , "Unsigned subtraction can never be negative."
0 commit comments