search

GaloisInc / crucible

Crucible is a library for symbolic simulation of imperative programs
617 stars 42 forks source link

CI: Run crux-llvm test suite in macOS #1172

Closed RyanGlScott closed 5 months ago

RyanGlScott commented 5 months ago

Previously, we concocted a clang-withIncl script for running Clang on macOS CI runners, but this neglected to pass any arguments to Clang (among other issues). This patch replaces the clang-withIncl machinery with a much simpler, Homebrew-based setup for install Clang/LLVM. With this in place, we can finally run the crux-llvm test suite on macOS.

Fixes https://github.com/GaloisInc/crucible/issues/999.

Running the test suite on macOS reveals several additional issues, among them #885 and #1013. This PR also applies a series of fixes for these issues.

RyanGlScott commented 5 months ago

I assume the generalization of zero v.s. non-zero in isinf and isnan tests is due to different return values from the different OS environments?

Yes. I added this to the commit message:

On Ubuntu, isinf(x) will return 1 if x is positive infinity and -1 if x is negative infinity. The C standard doesn't guarantee this, however, as it only requires that isinf(x) return some non-zero value if x is infinite. More to the point, Apple Clang's version of isinf doesn't return the same values that Ubuntu's Clang does, but the isinf.c test case in the crux-llvm test suite specifically checks for these values, making the test fail on macOS.

This patch makes the checks in isinf.c more general so that they will pass regardless of which non-zero value gets returned from isinf(x).