Open shaobo-he opened 3 years ago
After reading the sea-dsa paper, I think I have a better understanding of this. The consequence of memcpy on this example is not that bad because unifying the nodes does not collapse them. However, copying a structure into a byte array could cause node collapse, which further spreads all over the program.
Consider the following program,
a
andb
point to the same node. Converting them into assignments avoids this effect. This is because sea-dsa unifies the nodes pointed bymemcpy
's source and destination arguments if the element types contain pointers.SeaHorn has a
memcpy
rewritten pass (https://github.com/seahorn/seahorn/blob/dev10/lib/Transforms/Scalar/PromoteMemcpy.cc), which we can borrow to avoid this issue.