Vector handling in GEP instructions

[mortkever]

Hello,

Under the same circumstances as my previous issue (self ported llvm 15), I'm running into an issue in the computeGepOffset function in DsaLocal.cc. Perlbench from the SPEC 2006 benchmarking suite contains some vectors (e.g. <2 x %struct.xrv*>) which are passed to the computeGepOffset function. Here an assert triggers as the operand is a vector and not a pointer.

I see there is support for handling pointers to vectors as the operand of a gep instruction. However executing a gep on a vector has a different effect, the gep is executed on each individual element of the vector.

I assume that to correctly handle these the vector should effectively be split into their separate elements and then handled individually.
Perhaps a branch can be inserted in the visitGetElementInstruction(...) function that handles vectors separately from the regular geps?
However, supporting this would necessitate the support of both extractelement and insertelement.

Are there plans to support vectors in the future? Or do you know of a workaround?
Is there perhaps a way to simply drop these pointers and claim they may point to anything? (just to get rolling again)

Thanks!

[agurfinkel]

We have only very basic support for vector instructions. In our applications, we disable vectorization because it causes issues to other parts of our pipeline (we mostly use SeaDsa with SeaHorn, so the support is motivated by that).

We are happy to accept PRs that improve vector support, but we are not working on this at the time.

We are also happy to accept PRs that, under a flag, make SeaDsa more conservative. For example, treating certain pointers as pointing to anywhere. Again, this is not useful for our application and therefore has been a low priority for us. But we are happy to support such use if there is an interest.

[mortkever]

After some extra effort clang did finally listen and returned only IR without vectors.

Concerning adding support for "blackholes" (nodes that contain effectively all allocation sites) and considering I run into the same issue as #103, the first might be a intermediary solution for the latter. Blackholes could be a fall back for (all?) failing sanity checks and so would not immediately necessitate a flag imo. Wherever checks like these fail the sets can be replaced by a blackhole. This loses large amounts of precision but has the benefit that the analysis can continue, both in cases of obscure bugs as well as unsupported language features.

I am currently looking into implementing this by adding a new node type "blackhole". Logically this implies the the node contains all or no allocations sites. One of the sanity checks done however, is verifying the sets are not empty. So a better approach would perhaps be to add a blackhole allocation site as a placeholder (with no llvm value (or a nullptr)).
I see also that m_alloc_sites directly use values? Are their any side effects from just populating this set with a nullptr? Or should perhaps the set be replaced with a set of DsaAllocSite directly?

In the case where a sanity check fails, the blackhole is added and for the node the bit is set.
Lastly then, before the set is queried, the blackhole bit should be checked, and if necessary all non-blackhole alloc sites should be removed. Further handling is then needed in all the spots where the sets are fetched from.
I don't immediately see issues within seaDSA (in the places egtAllocSites is called) but perhaps this could break things in seahorn?

Do you see any problems with this approach?
I welcome all feedback and remarks