@@ -14,7 +14,7 @@ import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysi
14
14
import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExprSpecific
15
15
import semmle.code.cpp.ir.IR
16
16
import semmle.code.cpp.ir.dataflow.DataFlow
17
- import StitchedPathGraph
17
+ import FieldAddressToDerefFlow :: PathGraph
18
18
19
19
pragma [ nomagic]
20
20
Instruction getABoundIn ( SemBound b , IRFunction func ) {
@@ -42,21 +42,6 @@ bindingset[b]
42
42
pragma [ inline_late]
43
43
predicate bounded2 ( Instruction i , Instruction b , int delta ) { boundedImpl ( i , b , delta ) }
44
44
45
- module FieldAddressToPointerArithmeticConfig implements DataFlow:: ConfigSig {
46
- predicate isSource ( DataFlow:: Node source ) { isFieldAddressSource ( _, source ) }
47
-
48
- predicate isSink ( DataFlow:: Node sink ) {
49
- exists ( PointerAddInstruction pai | pai .getLeft ( ) = sink .asInstruction ( ) )
50
- }
51
- }
52
-
53
- module FieldAddressToPointerArithmeticFlow =
54
- DataFlow:: Global< FieldAddressToPointerArithmeticConfig > ;
55
-
56
- predicate isFieldAddressSource ( Field f , DataFlow:: Node source ) {
57
- source .asInstruction ( ) .( FieldAddressInstruction ) .getField ( ) = f
58
- }
59
-
60
45
bindingset [ delta]
61
46
predicate isInvalidPointerDerefSinkImpl (
62
47
int delta , Instruction i , AddressOperand addr , string operation
@@ -93,56 +78,61 @@ predicate isInvalidPointerDerefSink2(DataFlow::Node sink, Instruction i, string
93
78
)
94
79
}
95
80
96
- predicate isConstantSizeOverflowSource ( Field f , FieldAddressToPointerArithmeticFlow:: PathNode fieldSource , PointerAddInstruction pai , int delta ) {
97
- exists ( int size , int bound , FieldAddressToPointerArithmeticFlow:: PathNode sink |
98
- FieldAddressToPointerArithmeticFlow:: flowPath ( fieldSource , sink ) and
99
- isFieldAddressSource ( f , fieldSource .getNode ( ) ) and
100
- pai .getLeft ( ) = sink .getNode ( ) .( DataFlow:: InstructionNode ) .asInstruction ( ) and
101
- pai .getElementSize ( ) = f .getUnspecifiedType ( ) .( ArrayType ) .getBaseType ( ) .getSize ( ) and
102
- f .getUnspecifiedType ( ) .( ArrayType ) .getArraySize ( ) = size and
103
- semBounded ( getSemanticExpr ( pai .getRight ( ) ) , any ( SemZeroBound b ) , bound , true , _) and
104
- delta = bound - size and
105
- delta >= 0 and
106
- size != 0 and
107
- size != 1
108
- )
81
+ predicate pointerArithOverflow (
82
+ PointerArithmeticInstruction pai , Field f , int size , int bound , int delta
83
+ ) {
84
+ pai .getElementSize ( ) = f .getUnspecifiedType ( ) .( ArrayType ) .getBaseType ( ) .getSize ( ) and
85
+ f .getUnspecifiedType ( ) .( ArrayType ) .getArraySize ( ) = size and
86
+ semBounded ( getSemanticExpr ( pai .getRight ( ) ) , any ( SemZeroBound b ) , bound , true , _) and
87
+ delta = bound - size
109
88
}
110
89
111
- module PointerArithmeticToDerefConfig implements DataFlow:: ConfigSig {
112
- predicate isSource ( DataFlow :: Node source ) {
113
- isConstantSizeOverflowSource ( _ , _ , source . asInstruction ( ) , _ )
114
- }
90
+ module FieldAddressToDerefConfig implements DataFlow:: StateConfigSig {
91
+ newtype FlowState =
92
+ additional TArray ( Field f ) or
93
+ additional TOverflowArithmetic ( PointerArithmeticInstruction pai )
115
94
116
- pragma [ inline]
117
- predicate isSink ( DataFlow:: Node sink ) { isInvalidPointerDerefSink1 ( sink , _, _) }
118
- }
119
-
120
- module MergedPathGraph = DataFlow:: MergePathGraph< PointerArithmeticToDerefFlow:: PathNode , FieldAddressToPointerArithmeticFlow:: PathNode , PointerArithmeticToDerefFlow:: PathGraph , FieldAddressToPointerArithmeticFlow:: PathGraph > ;
121
- class PathNode = MergedPathGraph:: PathNode ;
122
- module StitchedPathGraph implements DataFlow:: PathGraphSig< PathNode > {
123
- query predicate edges ( PathNode a , PathNode b ) {
124
- MergedPathGraph:: PathGraph:: edges ( a , b )
125
- or
126
- a .asPathNode2 ( ) .getNode ( ) .( DataFlow:: InstructionNode ) .asInstruction ( ) = b .asPathNode1 ( ) .getNode ( ) .( DataFlow:: InstructionNode ) .asInstruction ( ) .( PointerAddInstruction ) .getLeft ( )
95
+ predicate isSource ( DataFlow:: Node source , FlowState state ) {
96
+ exists ( Field f |
97
+ source .asInstruction ( ) .( FieldAddressInstruction ) .getField ( ) = f and
98
+ state = TArray ( f )
99
+ )
127
100
}
128
101
129
- query predicate nodes ( PathNode n , string key , string val ) {
130
- MergedPathGraph:: PathGraph:: nodes ( n , key , val )
102
+ predicate isSink ( DataFlow:: Node sink , FlowState state ) {
103
+ isInvalidPointerDerefSink1 ( sink , _, _) and
104
+ state instanceof TOverflowArithmetic
131
105
}
132
106
133
- query predicate subpaths ( PathNode arg , PathNode par , PathNode ret , PathNode out ) {
134
- MergedPathGraph:: PathGraph:: subpaths ( arg , par , ret , out )
107
+ predicate isBarrier ( DataFlow:: Node node , FlowState state ) { none ( ) }
108
+
109
+ predicate isAdditionalFlowStep (
110
+ DataFlow:: Node node1 , FlowState state1 , DataFlow:: Node node2 , FlowState state2
111
+ ) {
112
+ exists ( PointerArithmeticInstruction pai , Field f , int size , int delta |
113
+ state1 = TArray ( f ) and
114
+ state2 = TOverflowArithmetic ( pai ) and
115
+ pai .getLeft ( ) = node1 .asInstruction ( ) and
116
+ node2 .asInstruction ( ) = pai and
117
+ pointerArithOverflow ( pai , f , size , _, delta ) and
118
+ delta >= 0 and
119
+ size != 0 and
120
+ size != 1
121
+ )
135
122
}
136
123
}
137
- module PointerArithmeticToDerefFlow = DataFlow:: Global< PointerArithmeticToDerefConfig > ;
124
+
125
+ module FieldAddressToDerefFlow = DataFlow:: GlobalWithState< FieldAddressToDerefConfig > ;
138
126
139
127
from
140
- Field f , PathNode fieldSource , PathNode paiNode ,
141
- PathNode sink , Instruction deref , string operation , int delta
128
+ Field f , FieldAddressToDerefFlow :: PathNode source , PointerArithmeticInstruction pai ,
129
+ FieldAddressToDerefFlow :: PathNode sink , Instruction deref , string operation , int delta
142
130
where
143
- PointerArithmeticToDerefFlow :: flowPath ( paiNode . asPathNode1 ( ) , sink . asPathNode1 ( ) ) and
131
+ FieldAddressToDerefFlow :: flowPath ( source , sink ) and
144
132
isInvalidPointerDerefSink2 ( sink .getNode ( ) , deref , operation ) and
145
- isConstantSizeOverflowSource ( f , fieldSource .asPathNode2 ( ) , paiNode .getNode ( ) .asInstruction ( ) , delta )
146
- select paiNode , fieldSource , sink ,
133
+ source .getState ( ) = FieldAddressToDerefConfig:: TArray ( f ) and
134
+ sink .getState ( ) = FieldAddressToDerefConfig:: TOverflowArithmetic ( pai ) and
135
+ pointerArithOverflow ( pai , f , _, _, delta )
136
+ select pai , source , sink ,
147
137
"This pointer arithmetic may have an off-by-" + ( delta + 1 ) +
148
138
" error allowing it to overrun $@ at this $@." , f , f .getName ( ) , deref , operation
0 commit comments