@@ -43,20 +43,28 @@ predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, int state) {
4343 )
4444}
4545
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
4857) {
49- exists (
50- int bufIndex , int sizeIndex , Instruction sizeInstr , Instruction bufInstr , ArrayFunction func
51- |
58+ exists ( int bufIndex , int sizeIndex , Instruction bufInstr , ArrayFunction func |
5259 bufInstr = bufSink .asInstruction ( ) and
5360 c .getArgument ( bufIndex ) = bufInstr and
54- sizeInstr = sizeSink .asInstruction ( ) and
61+ sizeBound = sizeSink .asInstruction ( ) and
62+ c .getArgument ( sizeIndex ) = sizeInstr and
5563 c .getStaticCallTarget ( ) = func and
5664 pragma [ only_bind_into ] ( func )
5765 .hasArrayWithVariableSize ( pragma [ only_bind_into ] ( bufIndex ) ,
5866 pragma [ only_bind_into ] ( sizeIndex ) ) and
59- bounded ( c . getArgument ( sizeIndex ) , sizeInstr , delta ) and
67+ bounded ( sizeInstr , sizeBound , delta ) and
6068 eBuf = bufInstr .getUnconvertedResultExpression ( )
6169 )
6270}
@@ -86,7 +94,7 @@ module ValidState {
8694 private module ValidStateConfig implements DataFlow:: ConfigSig {
8795 predicate isSource ( DataFlow:: Node source ) { hasSize ( _, source , _) }
8896
89- predicate isSink ( DataFlow:: Node sink ) { isSinkPairImpl ( _, _, sink , _, _) }
97+ predicate isSink ( DataFlow:: Node sink ) { isSinkPairImpl0 ( _, _, sink , _ , _ , _, _) }
9098
9199 predicate isBarrierOut ( DataFlow:: Node node ) { DataFlow:: flowsToBackEdge ( node ) }
92100 }
@@ -131,14 +139,14 @@ module StringSizeConfig implements ProductFlow::StateConfigSig {
131139 // to the size of the allocation. This state is then checked in `isSinkPair`.
132140 exists ( state1 ) and
133141 hasSize ( bufSource .asExpr ( ) , sizeSource , state2 ) and
134- validState ( sizeSource , state2 )
142+ validState ( sizeSource , _ , state2 )
135143 }
136144
137145 predicate isSinkPair (
138146 DataFlow:: Node bufSink , FlowState1 state1 , DataFlow:: Node sizeSink , FlowState2 state2
139147 ) {
140148 exists ( state1 ) and
141- validState ( sizeSink , state2 ) and
149+ validState ( _ , sizeSink , state2 ) and
142150 exists ( int delta |
143151 isSinkPairImpl ( _, bufSink , sizeSink , delta , _) and
144152 delta > state2
0 commit comments