It's currently implemented as
|
let hasAttribute s al = |
|
(filterAttributes s al <> []) |
This is silly because filterAttributes will allocate a new list, just to check containment. This should be done with List.exists or something reasonable that doesn't allocate at all.
This showed up as a notable source of allocations while analyzing rsync. The hasAttribute is used by bitsOffset calculation (to look for packing attributes) which we heavily use in Goblint during semantic_equal of addresses (and their sets).
In addition to the one-liner change, we should evaluate the impact on rsync/sv-benchmarks.
Besides fixing this, it might make sense to also cache the bitsOffset calls on Goblint side.
It's currently implemented as
cil/src/cil.ml
Lines 1429 to 1430 in bf39f60
This is silly because
filterAttributeswill allocate a new list, just to check containment. This should be done withList.existsor something reasonable that doesn't allocate at all.This showed up as a notable source of allocations while analyzing rsync. The
hasAttributeis used bybitsOffsetcalculation (to look for packing attributes) which we heavily use in Goblint duringsemantic_equalof addresses (and their sets).In addition to the one-liner change, we should evaluate the impact on rsync/sv-benchmarks.
Besides fixing this, it might make sense to also cache the
bitsOffsetcalls on Goblint side.