[macOS] Build uses unsupported flags which break it: cc1plus: error: '-fno-fat-lto-objects' are supported only with linker plugin
#512
Comments
|
Hi @barracuda156 - thanks for the report. Could you say how you configured the build? LTO/IPO should not be enabled by default. Also - I think this is for PowerPC, right? Let us know how you get on, we'd be interested to know if Vampire works. |
|
Apparently the issue is that Test for LTO in fact fails, but why does the build proceeds with LTO enabled? It should just disable it instead. This is apparently a configure test error: |
|
@MichaelRawson Thank you for responding! I guess it is Macports portfile forces this option: https://github.com/macports/macports-ports/blob/c7df747729c62f2801614020663ef140a33663e1/math/vampire/Portfile#L33 I wanted to update the port, which is at some archaic version at the moment, left this configure arg as it was there.
Yes. Once the build itself works, I will run tests and let you know. |
|
@MichaelRawson Disabling IPO worked, but then the build fails here: |
|
And then: |
|
I have disabled static_asserts, build succeeds, tests are blocked by sandboxing, it seems: I may know a fix, will rerun the build. |
|
@MichaelRawson So no, it is broken, as of now. Sandboxing error is trivially fixable, but the binary is broken anyway: |
|
|
@MichaelRawson This seems to be nothing specific to either macOS or powerpc, but rather broken 32-bit support. Could this be addressed? If it is just a 32-bit issue, it should be reproducible on Linux on i386, for example. |
|
OK, thanks for investigating - in principle there's no reason we couldn't support 32-bit platforms, but none of us currently use a 32-bit machine (I think). We do some gross stuff with memory (mostly term layout) that is probably the source of that particular crash. I'm cross-compiling now for i386 and working out some of the bugs. |
|
(moving conversation back here, no longer "just" a 32-bit arch problem) Thanks for testing! 4-byte bool should be OK, spinlock...no idea, we don't use them explicitly.
Uh-oh. Showing my PowerPC ignorance here, I didn't know this. I expect this is (another) source of bugs with the term representation, then. However, the existence of the port suggests this worked (miraculously) at some point. Would you be able to bisect this and work out which commit broke PowerPC? |
|
@MichaelRawson Well, existence of port only means it has built at the time (but it also builds now). Whether it ever actually worked is an open question. We could get some extra info from GDB, like registers state, but we needs someone understanding low-level ABI to make sense of that, perhaps. Given that the build works with no hackery, I suspect the issue is either bitness or endianness or a consequence of assuming 1-byte bools (the latter is sometimes not obvious). If you have any suspicion what parts of the code may be relevant, please point to them. I can test this on i386 macOS in a while (to see if 32-bitness specifically on MacOS matters) and possibly ppc64 (which has 1-byte bools, so only endianness is an issue). |
True!
Sure; I was going off the metadata at https://github.com/macports/macports-ports/blob/c7df747729c62f2801614020663ef140a33663e1/math/vampire/Portfile#L11 which suggests commit In the event that this commit works, it's only a couple of years old, so
I'm almost certain it's Line 224 in 31939a4 The comment block above is quite funny in this context! Anyhow, if you move that field to the end of the bitfield, after As far as I'm aware this is the least-portable part of Vampire. There might be others, but I'd look here first. We are generally trying to improve the portability situation, so thank you for bringing this to our attention. |
|
So I tried modifying the struct there like this: Build failed then: |
|
Just in case, I removed the assert and completed the build. The binary now crashes differently: |
Looks like compiler padding broke us, and if Would you be willing to test this approach? Sorry about the extra cycle, I should have tried myself first. If it works (or at least crashes less) I can think about how to fix it properly. |
|
@MichaelRawson This worked! Only few tests fail: Here is the output: |
|
@MichaelRawson If we could incorporate a fix for Big-endian platforms into the code, that would be awesome. Re tests, can these two failures be fixed? |
|
I'm glad it "worked" - looks like we crash a bit less now. :-) A proper fix is now top of my Vampire list, probably end of the week or so. The failures are still a bit concerning. TwoVampires is an old test of probably limited value that launches two separate instances - apparently one with an option we don't have any more. It's interesting that it fails on your machine, though - I think it passes for others, which is why it hasn't been fixed yet. Would you be able to step through control-flow on your machine in a debugger and figure out how it fails? The |
|
Spoke to @joe-hauns earlier. The tests are failing because the Z3 SMT solver returns
If it's (1), then we should investigate. If it's (2) we should file a bug with Z3. To work it out, could you change this line to |
|
@MichaelRawson Sorry for a ridiculous delay, I am back to the issue now. Just in case, is Big-endian support incorporated into the master or should I resort to local patching for now? |
|
Hey, no problem, I'm just getting back to it too. :-)
Unfortunately not - I have a fix planned for the |
|
@MichaelRawson I rebuilt and ran tests from master (with a patch to Temp). Overall results did not change: Is this helpful for Z3 issue? |
|
OK, on my (x86_64 )machine for e.g. So there's something going wrong on the Vampire side. I'll fix the term representation first and we can investigate this later. |
|
@MichaelRawson Great, just ping me when to test it again. |
|
@MichaelRawson Hi, any update on this? Should we return to testing? |
|
Hi! #524 ought to be a "proper fix" for at least the After (if) that's merged we can investigate further. Thanks for persisting. |
|
@MichaelRawson Sure, will test in a couple of days, likely tomorrow. |
|
@MichaelRawson Building from 4455f14 (we also updated Is |
|
Thanks for testing! That patch has now been merged so things ought to improve at least. I don't think there's anything else as bad in Vampire; there is similar pointer-tagging horror here, but it's much less frequently used. Will also fix in time. The failing test case is not a good sign, but it relies on Z3 - do you know if Z3 works on PowerPC? If not, let's disable Z3 first so that we only get failing test cases "from Vampire". Could you re-build without Z3? (you can pass |
|
Z3 does use some pointer tagging magic (see https://github.com/Z3Prover/z3/blob/master/src/util/tptr.h; maybe not the only place, but the only one I know of). But I think what Z3 does only depends on alignment and not on endianness. |
|
@JakobR With 4-byte bools and spinlocks there are chances alignment gets wrong. |
Also realised I failed to respond to this bit - it's not consequential, it's just how we do tracebacks in a pinch. See Not sure why you'd get "permission denied" from trying to run it, but I'm not a Mac expert. |
|
#543 also fixed the more-obscure bitfields in Vampire in a similar way. We might now be OK without Z3, if you can find something that doesn't work with a non-Z3 build let us know! |
|
@MichaelRawson Thank you! Sorry for a delay, I will build and run tests now from the master and disabling Z3. |
|
From c7564c1 and without Z3: |
|
Nice! The unit tests aren't particularly exhaustive, but that's a good sign. Let's consider this closed: feel free to open new issues with new PowerPC bugs. |
|
@MichaelRawson By the way, what is the status on aarch64? I ran tests on Sonoma, and 3 tests failed: (I can open a new issue if this is not something known already.) |
I know nothing about it! Please do open the issue. |
Done: #545 |
12 tasks
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
The text was updated successfully, but these errors were encountered: