Question: Why doesn't Clam use SeaDSA's butd-cs analysis? about clam

[caballa]

It wouldn't be sound.

The key is Figure 8 (https://jorgenavas.github.io/papers/sea-dsa-SAS17.pdf) that shows two aliasing patterns between callers and callee that cannot happen, otherwise inter-procedural Clam would be unsound:

1. if two formal parameters in the callee alias then the corresponding two parameters cannot point to two disjoint regions.
2. if two formal parameters in the callee do not alias then we cannot have a callsite where the two corresponding call parameters do alias.

The bottom-up pass avoids (1) and the top-down avoids (2). However, after we apply top-down we are modifying the aliasing patterns of a function. Therefore, we need to revisit all callees of that function. In the end, we need to revisit all callsites in the program until (1) and (2) cannot happen. Termination is ensured because at each bottom-up or top-down pass we merge at least two parameters and since the number is finite we end up in the worst case merging all parameters of all callsites and functions which would be similar to a context-insensitive analysis.

[adrianherrera]

Great, makes sense! Thanks Jorge