BoiseState-AdaptLab / IEGenLib

Inspector/Executor Generation Library for manipulating sets and relations with uninterpreted function symbols.
BSD 2-Clause "Simplified" License
2 stars 4 forks source link

Multiple array writes #129

Open Aaron3154518 opened 3 years ago

Aaron3154518 commented 3 years ago

In some cases, code will write to multiple indexes of an array before reading from them. Our SSA implementation does not differentiate between different indices and thus renames the array at each write. This means all array writes except the last one will have no reads. This is a unique case because multiple writes to different array indices do not make previous writes useless, as happens with non-array variables.

Example: In Update_Sources(), sources_dw is an array. sources_dw[0] gets written to and then sources_dw[1] gets written to. The second write renames sources_dw in the first write, creating two separate dataspace nodes. The first node, however has no reads despite the fact that soures_dw[0] is read from. This is a bug.