[llvm] [MemCpyOpt] Require writable object during call slot optimization (PR #71542)

Nuno Lopes via llvm-commits llvm-commits at lists.llvm.org
Wed Nov 8 01:25:25 PST 2023


nunoplopes wrote:

> > does alive model these sorts of issues?
> 
> I'm not really sure. I believe it doesn't reason about data races and doesn't support `noalias`, but maybe it has read-only memory? I think this would be a variant of a test case that doesn't rely on noalias: https://alive2.llvm.org/ce/z/ZDcarT And it doesn't verify ... but I'm not sure whether it fails to verify for the right reasons. I never know how to interpret these "Function triggered UB" results. cc @nunoplopes

Alive2 doesn't support `writable` yet; I've put that on the todo list.
Besides that, it doesn't model data races. It happily accepts introduction of stores if the memory is dereferenceable. noalias.

That test case should verify AFACIT, it's just that the refinement of function arguments is too strict. I'll open a bug report.

https://github.com/llvm/llvm-project/pull/71542


More information about the llvm-commits mailing list