Generalize the SymbolIDs used for SymbolData to all SymExprs and use
these IDs for comparison SymbolRef keys in various containers, such as
ConstraintMap. These IDs are superior to raw pointer values because they
are more controllable and are not randomized across executions (unlike
[pointers](https://en.wikipedia.org/wiki/Address_space_layout_randomization)).
These IDs order is stable across runs because SymExprs are allocated in
the same order.
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
and C++ projects with the total number of ~78 000 symbolic-execution
issues passing Z3 refutation.
This patch reduced the run-to-run churn (flakiness) 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).
Note, most of the issue churn (flakiness) is caused by the mentioned Z3
refutation. With Z3 refutation disabled, issue churn goes down to ~10
issues out of 83K and this patch has no effect on appearing/disappearing
issues between runs. It however, seems to reduce the volatility of the
execution flow: before we had 40-80 issues with changed execution flow,
after - 10-30.
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 significant effect on
memory footprint or analysis time.
This PR reapplies https://github.com/llvm/llvm-project/pull/121551 with
a fix to a g++ compiler error reported on some build bots
CPP-5919
Generalize the `SymbolID`s used for `SymbolData` to all `SymExpr`s and
use these IDs for comparison `SymbolRef` keys in various containers,
such as `ConstraintMap`. These IDs are superior to raw pointer values
because they are more controllable and are not randomized across
executions (unlike
[pointers](https://en.wikipedia.org/wiki/Address_space_layout_randomization)).
These IDs order is stable across runs because SymExprs are allocated in
the same order.
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
and C++ projects with the total number of ~78 000 symbolic-execution
issues passing Z3 refutation.
This patch reduced the run-to-run churn (flakiness) 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).
Note, most of the issue churn (flakiness) is caused by the mentioned Z3
refutation. With Z3 refutation disabled, issue churn goes down to ~10
issues out of 83K and this patch has no effect on appearing/disappearing
issues between runs. It however, seems to reduce the volatility of the
execution flow: before we had 40-80 issues with changed execution flow,
after - 10-30.
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 significant effect on
memory footprint or analysis time.
CPP-5919
This patch adds a new descendant to the SymExpr hierarchy. This way, now
we can assign constraints to symbolic unary expressions. Only the unary
minus and bitwise negation are handled.
Differential Revision: https://reviews.llvm.org/D125318
