memcpy Merges Regions Unnecessarily

[shaobo-he]

Consider the following program,

typedef struct {
  int* x;
  int y;
} ST;

int main(void) {
  ST a, b;
  b.x = (int*)malloc(sizeof(int));
  *b.x = 1;
  memcpy(&a, &b, sizeof(ST));
  //a.x = b.x;
  //a.y = b.y;
  return *a.x;
}

a and b point to the same node. Converting them into assignments avoids this effect. This is because sea-dsa unifies the nodes pointed by memcpy'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.

[shaobo-he]

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.