@@ -137,57 +137,95 @@ predicate directParamPlusConstAlloc(Function f, int paramIndex, int constPart) {
137137}
138138
139139/**
140- * Computes the constant allocation size for a call to a function that
141- * transitively calls `memory_heap_alloc` without its own ensure_free.
142- *
143- * Case 1: The callee has a direct `memory_heap_alloc` with a fully constant size.
144- * Case 2: The callee has `memory_heap_alloc(heap, constant + param)` and the
145- * caller passes a constant for that parameter.
146- * Case 3: Wrapper function -- the callee doesn't directly call `memory_heap_alloc`
147- * but calls another function that does, and we can compute its size
148- * via a function-level summary (avoids recursing over calls).
140+ * Holds if `leafCall` is a call reachable from function `f` (through wrapper
141+ * functions that don't call ensure_free) to a function that directly calls
142+ * `memory_heap_alloc`. This is a monotonic reachability predicate that avoids
143+ * non-monotonic recursion through aggregation.
144+ */
145+ pragma [ nomagic]
146+ predicate reachableLeafAllocCall ( Function f , FunctionCall leafCall ) {
147+ // Base: f directly contains a call to a wrapper that directly allocates
148+ leafCall .getEnclosingFunction ( ) = f and
149+ not isEnsureFreeCall ( leafCall ) and
150+ not leafCall .getTarget ( ) .hasName ( "memory_heap_alloc" ) and
151+ directlyCallsHeapAlloc ( leafCall .getTarget ( ) ) and
152+ not callsEnsureFree ( leafCall .getTarget ( ) )
153+ or
154+ // Recursive: f calls wrapper g which has reachable leaf alloc calls
155+ exists ( FunctionCall callToG , Function g |
156+ callToG .getEnclosingFunction ( ) = f and
157+ g = callToG .getTarget ( ) and
158+ not callsEnsureFree ( g ) and
159+ not isEnsureFreeCall ( callToG ) and
160+ not g .hasName ( "memory_heap_alloc" ) and
161+ reachableLeafAllocCall ( g , leafCall )
162+ )
163+ }
164+
165+ /**
166+ * Gets the constant allocation size for a call to a function that directly
167+ * calls `memory_heap_alloc` (a leaf wrapper). Non-recursive: only considers
168+ * the direct `memory_heap_alloc` calls within the callee.
149169 */
150170pragma [ noinline]
151- int getConstAllocSize ( FunctionCall call ) {
171+ int leafAllocSize ( FunctionCall call ) {
152172 exists ( Function callee | callee = call .getTarget ( ) |
153- // Case 1: Direct memory_heap_alloc with fully constant size
154173 directlyCallsHeapAlloc ( callee ) and
155174 not callsEnsureFree ( callee ) and
156- result = directFullyConstAllocSize ( callee ) and
157- // Ensure there's no parameter-dependent alloc (avoid double-counting)
158- not directParamPlusConstAlloc ( callee , _, _)
159- or
160- // Case 2: Direct memory_heap_alloc with constant + param, caller passes constant
161- exists ( int paramIndex , int constPart , int paramVal |
162- directlyCallsHeapAlloc ( callee ) and
163- not callsEnsureFree ( callee ) and
164- directParamPlusConstAlloc ( callee , paramIndex , constPart ) and
165- paramVal = constExprValue ( call .getArgument ( paramIndex ) ) and
166- result = constPart + paramVal
167- )
168- or
169- // Case 3: Wrapper function -- use function-level summary
170- not directlyCallsHeapAlloc ( callee ) and
171- not callsEnsureFree ( callee ) and
172- transitivelyCallsHeapAllocWithoutEnsureFree ( callee ) and
173- result = funcConstAllocSize ( callee )
175+ result =
176+ sum ( int s | s = directFullyConstAllocSize ( callee ) | s )
177+ +
178+ sum ( int paramIndex , int constPart |
179+ directParamPlusConstAlloc ( callee , paramIndex , constPart ) and
180+ exists ( constExprValue ( call .getArgument ( paramIndex ) ) )
181+ | constPart + constExprValue ( call .getArgument ( paramIndex ) ) )
174182 )
175183}
176184
177185/**
178- * Gets the constant allocation size reachable within function `f`
179- * (through inner calls that allocate without their own ensure_free).
180- * This is a function-level summary that avoids per-call recursion.
181- * May return multiple values; callers use maxConstAllocSize to take the max.
186+ * Computes the total constant allocation size for a call to a function that
187+ * transitively calls `memory_heap_alloc` without its own ensure_free.
188+ *
189+ * Aggregates all applicable constant contributions from the callee:
190+ * - All fully-constant direct `memory_heap_alloc` sizes
191+ * - All `memory_heap_alloc(heap, constant + param)` where the caller passes
192+ * a constant for that parameter
193+ * - All transitive wrapper function contributions (via reachableLeafAllocCall)
182194 */
183- pragma [ nomagic]
184- int funcConstAllocSize ( Function f ) {
185- exists ( FunctionCall innerCall |
186- innerCall .getEnclosingFunction ( ) = f and
187- transitivelyCallsHeapAllocWithoutEnsureFree ( innerCall .getTarget ( ) ) and
188- not isEnsureFreeCall ( innerCall ) and
189- not innerCall .getTarget ( ) .hasName ( "memory_heap_alloc" ) and
190- result = getConstAllocSize ( innerCall )
195+ pragma [ noinline]
196+ int getConstAllocSize ( FunctionCall call ) {
197+ exists ( Function callee | callee = call .getTarget ( ) |
198+ not callsEnsureFree ( callee ) and
199+ transitivelyCallsHeapAllocWithoutEnsureFree ( callee ) and
200+ // At least one constant contribution must exist
201+ (
202+ exists ( directFullyConstAllocSize ( callee ) )
203+ or
204+ exists ( int pi , int cp |
205+ directParamPlusConstAlloc ( callee , pi , cp ) and
206+ exists ( constExprValue ( call .getArgument ( pi ) ) )
207+ )
208+ or
209+ exists ( FunctionCall leafCall |
210+ reachableLeafAllocCall ( callee , leafCall ) and
211+ exists ( leafAllocSize ( leafCall ) )
212+ )
213+ ) and
214+ result =
215+ // Sum all fully-constant direct allocations
216+ sum ( int s | s = directFullyConstAllocSize ( callee ) | s )
217+ +
218+ // Sum all param+const allocations where caller passes a constant
219+ sum ( int paramIndex , int constPart |
220+ directParamPlusConstAlloc ( callee , paramIndex , constPart ) and
221+ exists ( constExprValue ( call .getArgument ( paramIndex ) ) )
222+ | constPart + constExprValue ( call .getArgument ( paramIndex ) ) )
223+ +
224+ // Sum transitive wrapper contributions via reachable leaf calls
225+ sum ( FunctionCall leafCall , int leafSize |
226+ reachableLeafAllocCall ( callee , leafCall ) and
227+ leafSize = leafAllocSize ( leafCall )
228+ | leafSize )
191229 )
192230}
193231
0 commit comments