Simmo fixed some soundness issues (#106) that arise when the region analysis is executed with symbolic equality and field-sensitive refinement for all benchmarks. Previously, these flags were only turned on for specific benchmarks. The pull request fixed all surface issues that emerged, but it did not raise our confidence in the code.

• Figure out if we really need general exp rather than lval to be stored for accesses.
• The field offset handling is fairly suspect and should be documented. I am not 100% convinced adding field-sensitivity to the region analysis in this way is sound, even for non-overlapping fields.
• Eliminate the todos for the offset handling. Why are some offsets dropped and some are handled.
• Build the partition domain on top of the Powerset domain.
• Unsoundness when a pointer to fresh region escapes to another thread, see Add zstd thread pool example to regression tests #641 (comment).
• Fixpoint error when interprocedural, see 16077e3.
  Reveals multiple issues:
  • Narrowing should be no-op instead of meet?
  • Bullet to bullet assign special case not implemented.
  • enter doesn't remove outer scope locals.
  • Interprocedural diamond from region paper not implemented.
  • Bullet concretization semantics are unclear.
  • Postsolver verify checks post-solution which isn't necessary with non-monotonicity and narrowing.

The region analysis is very simple on paper, but we have not worked out these interactions with field-sensitivity. We may need a deeper understanding of these things. We take a pointer p into an equivalence class and upon p -> f just appending f to all members of that class. This is sound under certain specific assumptions, but it's not clear that these assumptions are maintained by all operations of the region analysis.