search

vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
302 stars 52 forks source link

Aligned allocation is broken: `error: 'aligned_alloc' is not a member of 'std'; did you mean 'aligned_union'?` #592

Closed barracuda156 closed 2 months ago

barracuda156 commented 2 months ago

@MichaelRawson We got a new problem here, could you please take a look?

/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-4.9/Lib/Allocator.cpp:46:25: error: 'aligned_alloc' is not a member of 'std'; did you mean 'aligned_union'?
   46 |     if(void *ptr = std::aligned_alloc(align, size))
      |                         ^~~~~~~~~~~~~
      |                         aligned_union

aligned_alloc is not provided by the compiler, it is provided or not by the OS. Since MacOS does not have it on most versions, this fails. It should use posix_memalign as a fallback or malloc.

Also broken in the master:

FAILED: CMakeFiles/obj.dir/Lib/Allocator.cpp.o 
/opt/local/bin/ccache /opt/local/bin/g++-mp-14 -DCHECK_LEAKS=0 -DVDEBUG=0 -DVTIME_PROFILING=0 -DVZ3=0 -I/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-2f897a03725680d11eefb03b1a2e7022158e7f7a -pipe -DNDEBUG -I/opt/local/include -D_GLIBCXX_USE_CXX11_ABI=0 -O3 -DNDEBUG -std=c++17 -arch ppc -mmacosx-version-min=10.6 -Wall -fno-threadsafe-statics -fno-rtti -fsized-deallocation -MD -MT CMakeFiles/obj.dir/Lib/Allocator.cpp.o -MF CMakeFiles/obj.dir/Lib/Allocator.cpp.o.d -o CMakeFiles/obj.dir/Lib/Allocator.cpp.o -c /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-2f897a03725680d11eefb03b1a2e7022158e7f7a/Lib/Allocator.cpp
/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-2f897a03725680d11eefb03b1a2e7022158e7f7a/Lib/Allocator.cpp: In function 'void* operator new(size_t, std::align_val_t)':
/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-2f897a03725680d11eefb03b1a2e7022158e7f7a/Lib/Allocator.cpp:50:25: error: 'aligned_alloc' is not a member of 'std'
   50 |     if(void *ptr = std::aligned_alloc(align, size))
      |                         ^~~~~~~~~~~~~
barracuda156 commented 2 months ago

Specifically, aligned_alloc was added in macOS 10.13. So everything prior to that should use a fallback. posix_memalign is supported in 10.6+, malloc perhaps everywhere.

MichaelRawson commented 2 months ago

Thanks for bringing this up! I try to care about portability but clearly failed in this case: the std:: prefix gave me a false sense of security.

barracuda156 commented 2 months ago

@MichaelRawson Yeah, it was a poor choice, but GNU folks don’t see a problem here: https://gcc.gnu.org/bugzilla/show_bug.cgi?id=83662#c14