i386: fix the major problems at least #513

MichaelRawson · 2023-12-12T10:20:20Z

We are alerted in #512 that Vampire is broken on 32-bit platforms, which we knew, but weren't aware that anyone cared. We currently reject 32-bit systems at compile-time in Lib/Portability.hpp.

However, it doesn't actually seem that hard to get Vampire running on 32-bit systems. The biggest problem is that sizeof(size_t) is now 32, and we assume sizeof(TermList) == sizeof(size_t) to be at least 64 to get the bits we want into it - but this can be fixed by saying that TermList should be exactly 64 bits instead of sizeof(size_t).

This patch produces a 32-bit Vampire that runs plausibly on my system. Since we have users who want 32-bit support, I propose that we relax our 64-bit-only policy until we end up in a situation where we really can't support 32-bit systems any more.

@barracuda156 - you might want to test on this branch. I don't guarantee this fixes PowerPC, or even that we don't have serious bugs even on i386, but it should be much less crashy.

Indexing/LiteralSubstitutionTree.cpp

MichaelRawson · 2023-12-12T10:22:56Z

SAT/SATClause.hpp

@@ -51,6 +51,7 @@ class SATClause
  void setInference(SATInference* val);

  void* operator new(size_t,unsigned length);
+  void operator delete(void *);


This is weird; 32-bit Clang and GCC complains that this function doesn't exist for generating exception-cleanup code, but never actually calls it and I don't see why it would be needed. If we ever actually need an implementation, it should just call DEALLOC_KNOWN(this, length).

Complains in a sense of warnings or errors? I did not have any compile-time errors besides failing static asserts. (But produced binary was broken.)

Errors, surprisingly: https://godbolt.org/z/9sb819xT8 - try with/without -m32.

MichaelRawson · 2023-12-12T10:24:48Z

Generally, TermList is hazardous and could use an overhaul. But that will be a big job.

barracuda156 · 2023-12-12T12:22:36Z

@MichaelRawson Building from 3c2909c fails for me with:

:info:build FAILED: CMakeFiles/obj.dir/Kernel/MLMatcher.cpp.o 
:info:build /opt/local/bin/g++-mp-13 -DCHECK_LEAKS=0 -DVDEBUG=1 -DVTIME_PROFILING=0 -DVZ3=1 -I/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3c2909cbbe6df7edc610110355cf99db45fca79d -isystem /opt/local/include -pipe -mcpu=native -mtune=native -I/opt/local/include -D_GLIBCXX_USE_CXX11_ABI=0 -g -arch ppc -mmacosx-version-min=10.6 -Wall -fno-threadsafe-statics -fno-rtti -fsized-deallocation -std=c++14 -MD -MT CMakeFiles/obj.dir/Kernel/MLMatcher.cpp.o -MF CMakeFiles/obj.dir/Kernel/MLMatcher.cpp.o.d -o CMakeFiles/obj.dir/Kernel/MLMatcher.cpp.o -c /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3c2909cbbe6df7edc610110355cf99db45fca79d/Kernel/MLMatcher.cpp
:info:build /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3c2909cbbe6df7edc610110355cf99db45fca79d/Kernel/MLMatcher.cpp: In function 'bool {anonymous}::createLiteralBindings(Kernel::Literal*, const Kernel::LiteralList*, Kernel::Clause*, Kernel::Literal*, unsigned int*&, Kernel::TermList**&, Kernel::TermList*&)':
:info:build /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3c2909cbbe6df7edc610110355cf99db45fca79d/Kernel/MLMatcher.cpp:111:54: error: call of overloaded 'TermList(size_t)' is ambiguous
:info:build   111 |           ::new (altBindingData++) TermList((size_t)0);
:info:build       |                                                      ^
:info:build In file included from /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3c2909cbbe6df7edc610110355cf99db45fca79d/Debug/TimeProfiling.hpp:19,
:info:build                  from /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3c2909cbbe6df7edc610110355cf99db45fca79d/Lib/Metaiterators.hpp:29,
:info:build                  from /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3c2909cbbe6df7edc610110355cf99db45fca79d/Lib/BinaryHeap.hpp:26,
:info:build                  from /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3c2909cbbe6df7edc610110355cf99db45fca79d/Kernel/MLMatcher.cpp:17:
:info:build /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3c2909cbbe6df7edc610110355cf99db45fca79d/Kernel/Term.hpp:100:12: note: candidate: 'Kernel::TermList::TermList(Kernel::Term*)'
:info:build   100 |   explicit TermList(Term* t) : _content(0) {
:info:build       |            ^~~~~~~~
:info:build /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3c2909cbbe6df7edc610110355cf99db45fca79d/Kernel/Term.hpp:98:12: note: candidate: 'Kernel::TermList::TermList(uint64_t)'
:info:build    98 |   explicit TermList(uint64_t data) : _content(data) {}
:info:build       |            ^~~~~~~~
:info:build /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3c2909cbbe6df7edc610110355cf99db45fca79d/Kernel/Term.hpp:91:7: note: candidate: 'constexpr Kernel::TermList::TermList(const Kernel::TermList&)'
:info:build    91 | class TermList {
:info:build       |       ^~~~~~~~
:info:build /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3c2909cbbe6df7edc610110355cf99db45fca79d/Kernel/Term.hpp:91:7: note: candidate: 'constexpr Kernel::TermList::TermList(Kernel::TermList&&)'
:info:build /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3c2909cbbe6df7edc610110355cf99db45fca79d/Kernel/MLMatcher.cpp:124:54: error: call of overloaded 'TermList(size_t)' is ambiguous
:info:build   124 |           ::new (altBindingData++) TermList((size_t)0);
:info:build       |                                                      ^
:info:build /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3c2909cbbe6df7edc610110355cf99db45fca79d/Kernel/Term.hpp:100:12: note: candidate: 'Kernel::TermList::TermList(Kernel::Term*)'
:info:build   100 |   explicit TermList(Term* t) : _content(0) {
:info:build       |            ^~~~~~~~
:info:build /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3c2909cbbe6df7edc610110355cf99db45fca79d/Kernel/Term.hpp:98:12: note: candidate: 'Kernel::TermList::TermList(uint64_t)'
:info:build    98 |   explicit TermList(uint64_t data) : _content(data) {}
:info:build       |            ^~~~~~~~
:info:build /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3c2909cbbe6df7edc610110355cf99db45fca79d/Kernel/Term.hpp:91:7: note: candidate: 'constexpr Kernel::TermList::TermList(const Kernel::TermList&)'
:info:build    91 | class TermList {
:info:build       |       ^~~~~~~~
:info:build /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3c2909cbbe6df7edc610110355cf99db45fca79d/Kernel/Term.hpp:91:7: note: candidate: 'constexpr Kernel::TermList::TermList(Kernel::TermList&&)'
:info:build /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3c2909cbbe6df7edc610110355cf99db45fca79d/Kernel/MLMatcher.cpp:141:52: error: call of overloaded 'TermList(size_t)' is ambiguous
:info:build   141 |         ::new (altBindingData++) TermList((size_t)0);
:info:build       |                                                    ^
:info:build /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3c2909cbbe6df7edc610110355cf99db45fca79d/Kernel/Term.hpp:100:12: note: candidate: 'Kernel::TermList::TermList(Kernel::Term*)'
:info:build   100 |   explicit TermList(Term* t) : _content(0) {
:info:build       |            ^~~~~~~~
:info:build /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3c2909cbbe6df7edc610110355cf99db45fca79d/Kernel/Term.hpp:98:12: note: candidate: 'Kernel::TermList::TermList(uint64_t)'
:info:build    98 |   explicit TermList(uint64_t data) : _content(data) {}
:info:build       |            ^~~~~~~~
:info:build /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3c2909cbbe6df7edc610110355cf99db45fca79d/Kernel/Term.hpp:91:7: note: candidate: 'constexpr Kernel::TermList::TermList(const Kernel::TermList&)'
:info:build    91 | class TermList {
:info:build       |       ^~~~~~~~

MichaelRawson · 2023-12-12T12:51:35Z

@barracuda156 - a question I should already have asked - is your PowerPC machine 32- or 64- bit?

I don't get these compilation errors, but it looks like changing casts of this form from (size_t)0 to (uint64_t)0 would work. Could you try it and let me know? As it happens both overloads do the same thing in this case.

barracuda156 · 2023-12-12T12:59:24Z

@MichaelRawson Machine in a sense of a hardware (G5 / ppc970) supports both, but 10.6 only supports ppc.
(In principle I could test for ppc64 too, but not at the moment, since I have no functional set-up on 10.5.8.)

barracuda156 · 2023-12-12T15:56:58Z

P. S. Please allow me until tomorrow, I am away from the fast PowerMac now. Will update with results once back to it.

MichaelRawson · 2023-12-12T15:58:10Z

P. S. Please allow me until tomorrow, I am away from the fast PowerMac now. Will update with results once back to it.

You must be new here. ;-) No hurry!

barracuda156 · 2023-12-13T15:09:53Z

@MichaelRawson Rebuilt from your branch, replacing (size_t) with (uint64_t) in MLMatcher.cpp, but the binary remains broken on launch:

(gdb) run
Starting program: /opt/local/bin/vampire 
Reading symbols for shared libraries +++++.... done

Program received signal EXC_BAD_ACCESS, Could not access memory.
Reason: KERN_PROTECTION_FAILURE at address: 0x00000008
0x0002dc14 in Kernel::Term::functor ()
(gdb) where
#0  0x0002dc14 in Kernel::Term::functor ()
#1  0x00038ebc in Kernel::Term::isSpecial ()
#2  0x00059a00 in Kernel::Term::toString ()
#3  0x0005993c in Kernel::TermList::toString ()
#4  0x00053e3c in Kernel::OperatorType::toString ()
#5  0x000498e4 in Kernel::Signature::addInterpretedPredicate ()
#6  0x0004959c in Kernel::Signature::addEquality ()
#7  0x00007014 in Lib::Environment::Environment ()
#8  0x000073cc in __static_initialization_and_destruction_0 ()
#9  0x0000741c in _GLOBAL__sub_I_Environment.cpp ()
#10 0x8fe15d60 in __dyld__ZN16ImageLoaderMachO16doInitializationERKN11ImageLoader11LinkContextE ()
#11 0x8fe0f70c in __dyld__ZN11ImageLoader23recursiveInitializationERKNS_11LinkContextEj ()
#12 0x8fe0f804 in __dyld__ZN11ImageLoader15runInitializersERKNS_11LinkContextE ()
#13 0x8fe02708 in __dyld__ZN4dyld24initializeMainExecutableEv ()
#14 0x8fe08690 in __dyld__ZN4dyld5_mainEPK11mach_headermiPPKcS5_S5_ ()
#15 0x8fe017cc in __dyld__ZN13dyldbootstrap5startEPK11mach_headeriPPKcl ()
#16 0x8fe01064 in __dyld__dyld_start ()

barracuda156 · 2023-12-13T15:11:20Z

Two issues to have in mind for ppc: it is Big endian and it has 4-byte bool (and spinlock). If anything of these matters and is not accounted for in the code.

MichaelRawson · 2023-12-14T07:53:33Z

Moved conversation about PowerPC back to the original issue. This PR should nonetheless fix 32-bit Intel.

barracuda156 · 2023-12-14T08:26:55Z

I will try to test it on i386 in a few days.

Could we also fix those type mismatches, as per your suggestion? As long as that works across other archs, it is desirable: while it is not enough for ppc, it is needed at least to fix the compilation.

MichaelRawson · 2023-12-14T09:03:58Z

I will try to test it on i386 in a few days.

Thanks - I can actually test this locally on a 64-bit machine, but if you have actually 32-bit silicon that'd be great.

Could we also fix those type mismatches, as per your suggestion? As long as that works across other archs, it is desirable: while it is not enough for ppc, it is needed at least to fix the compilation.

Good point. I'll update this.

Lib/Portability.hpp

quickbeam123 · 2023-12-15T10:47:52Z

Approved. Modulo the question about the removed static assert...

barracuda156 · 2023-12-15T17:35:12Z

Thank you! And I will try with ppc build tonight and update in the issue.

i386: fix the major problems at least

3c2909c

MichaelRawson requested a review from quickbeam123 December 12, 2023 10:20

MichaelRawson commented Dec 12, 2023

View reviewed changes

Indexing/LiteralSubstitutionTree.cpp Show resolved Hide resolved

MichaelRawson commented Dec 12, 2023

View reviewed changes

MichaelRawson added 2 commits December 14, 2023 09:09

fix MLMatcher casts

cf95b4c

better solution for MLMatcher casts

b3b638a

quickbeam123 reviewed Dec 15, 2023

View reviewed changes

Lib/Portability.hpp Show resolved Hide resolved

quickbeam123 approved these changes Dec 15, 2023

View reviewed changes

MichaelRawson merged commit 459694c into master Dec 15, 2023
1 check passed

MichaelRawson deleted the michael-fix-32-bit branch December 15, 2023 17:34

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

i386: fix the major problems at least #513

i386: fix the major problems at least #513

MichaelRawson commented Dec 12, 2023

MichaelRawson Dec 12, 2023

barracuda156 Dec 12, 2023

MichaelRawson Dec 12, 2023

MichaelRawson commented Dec 12, 2023

barracuda156 commented Dec 12, 2023

MichaelRawson commented Dec 12, 2023

barracuda156 commented Dec 12, 2023 •

edited

Loading

barracuda156 commented Dec 12, 2023

MichaelRawson commented Dec 12, 2023

barracuda156 commented Dec 13, 2023

barracuda156 commented Dec 13, 2023

MichaelRawson commented Dec 14, 2023

barracuda156 commented Dec 14, 2023

MichaelRawson commented Dec 14, 2023

quickbeam123 commented Dec 15, 2023

barracuda156 commented Dec 15, 2023

i386: fix the major problems at least #513

i386: fix the major problems at least #513

Conversation

MichaelRawson commented Dec 12, 2023

MichaelRawson Dec 12, 2023

Choose a reason for hiding this comment

barracuda156 Dec 12, 2023

Choose a reason for hiding this comment

MichaelRawson Dec 12, 2023

Choose a reason for hiding this comment

MichaelRawson commented Dec 12, 2023

barracuda156 commented Dec 12, 2023

MichaelRawson commented Dec 12, 2023

barracuda156 commented Dec 12, 2023 • edited Loading

barracuda156 commented Dec 12, 2023

MichaelRawson commented Dec 12, 2023

barracuda156 commented Dec 13, 2023

barracuda156 commented Dec 13, 2023

MichaelRawson commented Dec 14, 2023

barracuda156 commented Dec 14, 2023

MichaelRawson commented Dec 14, 2023

quickbeam123 commented Dec 15, 2023

barracuda156 commented Dec 15, 2023

barracuda156 commented Dec 12, 2023 •

edited

Loading