search

SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
363 stars 45 forks source link

Poor test results on PowerPC: how to improve/fix? #424

Open barracuda156 opened 1 year ago

barracuda156 commented 1 year ago

I am bringing yices into Macports, and we maintain support for older macOS there. With minimal fixes to build system, I have built yices for ppc32 on 10.6.8. However, while the build is successful, test results are dismal:

Pass: 128
Fail: 869

P. S. I made no modifications to the code itself – then only thing I had to fix was adding support for powerpc-apple-darwin to ARCH.

tests_10.6.8_Rosetta_ppc32.txt

BrunoDutertre commented 1 year ago

Try to compile statically and in debug mode. For example:

make static-check MODE=debug

will run all the tests with assertions enabled.

barracuda156 commented 1 year ago

Try to compile statically and in debug mode. For example:

make static-check MODE=debug

will run all the tests with assertions enabled.

@BrunoDutertre Thank you, will try that.

By the way, on MacOS x86_64 static targets do not build at all: https://github.com/macports/macports-ports/pull/17078#issuecomment-1366074386 On PPC they did, though I had to add -read_only_relocs suppress ldflag.

BrunoDutertre commented 1 year ago

Static builds work fine for me on x86_64 (and have for a long time). No special flag required. The main issue is building GMP in PIC mode.

barracuda156 commented 1 year ago

Static builds work fine for me on x86_64 (and have for a long time). No special flag required. The main issue is building GMP in PIC mode.

I looked into the docs, it appears that it needs three versions of gmp, which is highly problematic. Not that it is impossible to implement in Macports, but it is hardly justified, and I am not sure such intrusive change will be welcomed.

BrunoDutertre commented 1 year ago

The three versions is only for windows. On other platforms, you can build GMP once in PIC mode. You'll have libgmp.a for linking statically and libgmp.dylib for linking dynamically.

barracuda156 commented 1 year ago

The three versions is only for windows. On other platforms, you can build GMP once in PIC mode. You'll have libgmp.a for linking statically and libgmp.dylib for linking dynamically.

Well, then maybe we can make a variant of libgmp port to install in a separate location and then use it --with-pic-gmp=. Not something convenient, but doable :)