@@ -43,20 +43,28 @@ predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, int state) {
43
43
)
44
44
}
45
45
46
- predicate isSinkPairImpl (
47
- CallInstruction c , DataFlow:: Node bufSink , DataFlow:: Node sizeSink , int delta , Expr eBuf
46
+ /**
47
+ * Holds if `c` a call to an `ArrayFunction` with buffer argument `bufSink`,
48
+ * and a size argument `sizeInstr` which satisfies `sizeInstr <= sizeBound + delta`.
49
+ *
50
+ * Furthermore, the `sizeSink` node is the dataflow node corresponding to
51
+ * `sizeBound`, and the expression `eBuf` is the expression corresponding
52
+ * to `bufInstr`.
53
+ */
54
+ predicate isSinkPairImpl0 (
55
+ CallInstruction c , DataFlow:: Node bufSink , DataFlow:: Node sizeSink , int delta , Expr eBuf ,
56
+ Instruction sizeBound , Instruction sizeInstr
48
57
) {
49
- exists (
50
- int bufIndex , int sizeIndex , Instruction sizeInstr , Instruction bufInstr , ArrayFunction func
51
- |
58
+ exists ( int bufIndex , int sizeIndex , Instruction bufInstr , ArrayFunction func |
52
59
bufInstr = bufSink .asInstruction ( ) and
53
60
c .getArgument ( bufIndex ) = bufInstr and
54
- sizeInstr = sizeSink .asInstruction ( ) and
61
+ sizeBound = sizeSink .asInstruction ( ) and
62
+ c .getArgument ( sizeIndex ) = sizeInstr and
55
63
c .getStaticCallTarget ( ) = func and
56
64
pragma [ only_bind_into ] ( func )
57
65
.hasArrayWithVariableSize ( pragma [ only_bind_into ] ( bufIndex ) ,
58
66
pragma [ only_bind_into ] ( sizeIndex ) ) and
59
- bounded ( c . getArgument ( sizeIndex ) , sizeInstr , delta ) and
67
+ bounded ( sizeInstr , sizeBound , delta ) and
60
68
eBuf = bufInstr .getUnconvertedResultExpression ( )
61
69
)
62
70
}
@@ -86,7 +94,7 @@ module ValidState {
86
94
private module ValidStateConfig implements DataFlow:: ConfigSig {
87
95
predicate isSource ( DataFlow:: Node source ) { hasSize ( _, source , _) }
88
96
89
- predicate isSink ( DataFlow:: Node sink ) { isSinkPairImpl ( _, _, sink , _, _) }
97
+ predicate isSink ( DataFlow:: Node sink ) { isSinkPairImpl0 ( _, _, sink , _ , _ , _, _) }
90
98
91
99
predicate isBarrierOut ( DataFlow:: Node node ) { DataFlow:: flowsToBackEdge ( node ) }
92
100
}
@@ -131,14 +139,14 @@ module StringSizeConfig implements ProductFlow::StateConfigSig {
131
139
// to the size of the allocation. This state is then checked in `isSinkPair`.
132
140
exists ( state1 ) and
133
141
hasSize ( bufSource .asExpr ( ) , sizeSource , state2 ) and
134
- validState ( sizeSource , state2 )
142
+ validState ( sizeSource , _ , state2 )
135
143
}
136
144
137
145
predicate isSinkPair (
138
146
DataFlow:: Node bufSink , FlowState1 state1 , DataFlow:: Node sizeSink , FlowState2 state2
139
147
) {
140
148
exists ( state1 ) and
141
- validState ( sizeSink , state2 ) and
149
+ validState ( _ , sizeSink , state2 ) and
142
150
exists ( int delta |
143
151
isSinkPairImpl ( _, bufSink , sizeSink , delta , _) and
144
152
delta > state2
0 commit comments