[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