Commit 2e7b140
committed
[clang][analyzer] Stabilize path-constraint order by using alloc IDs
These IDs are essentially allocator offsets for the SymExpr pool. They
are superior to raw pointer values because they are more controllable
and are not randomized across executions.
They are not stable across runs because some spurious allocations might happen
only in certain runs. For example, an unrelated ImmutableMap rotates its
AVL tree based on the key values that are pointers. The rotation causes
extra allocations in the shared allocator, and the next SymExpr
allocation happens at a different offset.
Yet, these IDs *order* is stable across runs because SymExprs are
allocated in the same order and allocator offset grows monotonously.
Stability of the constraint order is important for the stability of the
analyzer results. I evaluated this change on a set of 200+ open-source
C++ projects with the total number of ~78 000 symbolic-execution issues.
This patch reduced the run-to-run churn (flakyness) in SE issues from
80-90 to 30-40 (out of 78K) in our CSA deployment (in our setting flaky
issues are mostly due to Z3 refutation instability).
Importantly, this change is necessary for the next step in stabilizing
analysis results by caching Z3 query outcomes between analysis
runs (work in progress).
Across our admittedly noisy CI runs, I detected no noticeable effect on
memory footprint or analysis time.
CPP-59191 parent 79af7bd commit 2e7b140
File tree
4 files changed
+74
-39
lines changed- clang
- include/clang/StaticAnalyzer/Core/PathSensitive
- lib/StaticAnalyzer/Core
4 files changed
+74
-39
lines changedLines changed: 16 additions & 1 deletion
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
401 | 401 | | |
402 | 402 | | |
403 | 403 | | |
404 | | - | |
| 404 | + | |
| 405 | + | |
| 406 | + | |
| 407 | + | |
| 408 | + | |
| 409 | + | |
| 410 | + | |
| 411 | + | |
| 412 | + | |
| 413 | + | |
| 414 | + | |
| 415 | + | |
| 416 | + | |
| 417 | + | |
| 418 | + | |
| 419 | + | |
405 | 420 | | |
406 | 421 | | |
407 | 422 | | |
| |||
Lines changed: 7 additions & 2 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
31 | 31 | | |
32 | 32 | | |
33 | 33 | | |
| 34 | + | |
34 | 35 | | |
35 | 36 | | |
36 | 37 | | |
| |||
39 | 40 | | |
40 | 41 | | |
41 | 42 | | |
| 43 | + | |
42 | 44 | | |
43 | 45 | | |
44 | | - | |
| 46 | + | |
45 | 47 | | |
46 | 48 | | |
47 | 49 | | |
| |||
56 | 58 | | |
57 | 59 | | |
58 | 60 | | |
| 61 | + | |
| 62 | + | |
59 | 63 | | |
60 | 64 | | |
61 | 65 | | |
| |||
122 | 126 | | |
123 | 127 | | |
124 | 128 | | |
125 | | - | |
| 129 | + | |
| 130 | + | |
126 | 131 | | |
127 | 132 | | |
128 | 133 | | |
| |||
Lines changed: 33 additions & 26 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
44 | 44 | | |
45 | 45 | | |
46 | 46 | | |
47 | | - | |
48 | | - | |
| 47 | + | |
| 48 | + | |
| 49 | + | |
49 | 50 | | |
50 | 51 | | |
51 | 52 | | |
| |||
86 | 87 | | |
87 | 88 | | |
88 | 89 | | |
89 | | - | |
90 | | - | |
| 90 | + | |
| 91 | + | |
| 92 | + | |
91 | 93 | | |
92 | 94 | | |
93 | 95 | | |
| |||
138 | 140 | | |
139 | 141 | | |
140 | 142 | | |
141 | | - | |
142 | | - | |
| 143 | + | |
| 144 | + | |
| 145 | + | |
| 146 | + | |
143 | 147 | | |
144 | 148 | | |
145 | 149 | | |
| |||
181 | 185 | | |
182 | 186 | | |
183 | 187 | | |
184 | | - | |
185 | | - | |
| 188 | + | |
| 189 | + | |
186 | 190 | | |
187 | 191 | | |
188 | 192 | | |
| |||
223 | 227 | | |
224 | 228 | | |
225 | 229 | | |
226 | | - | |
227 | | - | |
228 | | - | |
229 | | - | |
230 | | - | |
231 | | - | |
232 | | - | |
233 | | - | |
234 | | - | |
235 | | - | |
| 230 | + | |
| 231 | + | |
| 232 | + | |
| 233 | + | |
| 234 | + | |
| 235 | + | |
| 236 | + | |
| 237 | + | |
| 238 | + | |
| 239 | + | |
| 240 | + | |
236 | 241 | | |
237 | 242 | | |
238 | 243 | | |
| |||
287 | 292 | | |
288 | 293 | | |
289 | 294 | | |
290 | | - | |
291 | | - | |
| 295 | + | |
| 296 | + | |
292 | 297 | | |
293 | 298 | | |
294 | 299 | | |
| |||
333 | 338 | | |
334 | 339 | | |
335 | 340 | | |
336 | | - | |
337 | | - | |
| 341 | + | |
| 342 | + | |
| 343 | + | |
338 | 344 | | |
339 | 345 | | |
340 | 346 | | |
| |||
381 | 387 | | |
382 | 388 | | |
383 | 389 | | |
384 | | - | |
385 | | - | |
| 390 | + | |
| 391 | + | |
| 392 | + | |
386 | 393 | | |
387 | 394 | | |
388 | 395 | | |
| |||
427 | 434 | | |
428 | 435 | | |
429 | 436 | | |
430 | | - | |
431 | | - | |
| 437 | + | |
| 438 | + | |
432 | 439 | | |
433 | 440 | | |
434 | 441 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
170 | 170 | | |
171 | 171 | | |
172 | 172 | | |
173 | | - | |
| 173 | + | |
| 174 | + | |
174 | 175 | | |
175 | 176 | | |
176 | 177 | | |
| |||
188 | 189 | | |
189 | 190 | | |
190 | 191 | | |
191 | | - | |
| 192 | + | |
| 193 | + | |
192 | 194 | | |
193 | 195 | | |
194 | 196 | | |
| |||
204 | 206 | | |
205 | 207 | | |
206 | 208 | | |
207 | | - | |
| 209 | + | |
| 210 | + | |
208 | 211 | | |
209 | 212 | | |
210 | 213 | | |
| |||
219 | 222 | | |
220 | 223 | | |
221 | 224 | | |
222 | | - | |
| 225 | + | |
| 226 | + | |
223 | 227 | | |
224 | 228 | | |
225 | 229 | | |
| |||
236 | 240 | | |
237 | 241 | | |
238 | 242 | | |
239 | | - | |
| 243 | + | |
| 244 | + | |
240 | 245 | | |
241 | 246 | | |
242 | 247 | | |
| |||
252 | 257 | | |
253 | 258 | | |
254 | 259 | | |
255 | | - | |
| 260 | + | |
256 | 261 | | |
257 | 262 | | |
258 | 263 | | |
| |||
268 | 273 | | |
269 | 274 | | |
270 | 275 | | |
271 | | - | |
| 276 | + | |
272 | 277 | | |
273 | 278 | | |
274 | 279 | | |
| |||
284 | 289 | | |
285 | 290 | | |
286 | 291 | | |
287 | | - | |
| 292 | + | |
| 293 | + | |
288 | 294 | | |
289 | 295 | | |
290 | 296 | | |
| |||
301 | 307 | | |
302 | 308 | | |
303 | 309 | | |
304 | | - | |
| 310 | + | |
| 311 | + | |
305 | 312 | | |
306 | 313 | | |
307 | 314 | | |
| |||
316 | 323 | | |
317 | 324 | | |
318 | 325 | | |
319 | | - | |
| 326 | + | |
| 327 | + | |
320 | 328 | | |
321 | 329 | | |
322 | 330 | | |
| |||
0 commit comments