https://gcc.gnu.org/bugzilla/show_bug.cgi?id=65752
--- Comment #34 from rguenther at suse dot de <rguenther at suse dot de> --- On Sat, 23 May 2015, gil.hur at sf dot snu.ac.kr wrote: > https://gcc.gnu.org/bugzilla/show_bug.cgi?id=65752 > > --- Comment #33 from Chung-Kil Hur <gil.hur at sf dot snu.ac.kr> --- > Dear Richard, > > Thanks for the detailed response. > > I have a suggestion for a solution of the problem, which is based on my paper > to appear at PLDI 2015. > > * A Formal C Memory Model Supporting Integer-Pointer Casts. > Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve > Zdancewic, Viktor Vafeiadis. > http://sf.snu.ac.kr/gil.hur/publications/intptrcast.pdf > > The suggestion is simple. > You do not need to turn off the phiopt optimizations. > We propose to slightly change the following assumption. > > > PTA considers that all pointers coming from integer constants > > point to global memory only. > > Here, if you change this as follows, you can solve the problem. > > * All pointers coming from integer constants can point to only global memory > and > local variables whose addresses have been cast to integers. Ok, so you basically add a 2nd class of "escaping". So in GCC PTA terms you'd add a new ESCAPE-like 'INTEGER' variable with INTEGER = NONLOCAL and add INTEGER = x constraints for each .. = (integer-type) &x conversion and for the reverse ptr = (pointer-type) i add ptr = INTEGER > Also, we expect that this would not decrease the optimization performance of > GCC very much because those variables whose addresses have been cast to > integers tend to be escaped (e.g. passed to a hash function, or stored in the > memory). Well - the above basically makes _all_ pointers converted from integers point to non-local memory, it also basically globs all pointers converted from integers into a single equivalence class. So I think you underestimate the effect on optimization (but I may overestimate the effect on optimization of not simply making all pointers converted from integers point to all globals and all address-taken locals, aka ANYTHING in GCC PTA terms)