Build and infrastructure fixes for FreeBSD #7924
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
tautschnig
requested review from
a team,
peterschrammel,
kroening,
NlightNFotis,
thomasspriggs,
remi-delmas-3000,
jimgrundy and
TGWDB
as code owners
kroening
reviewed
Sep 27, 2023
Codecov ReportAttention:
Additional details and impacted files@@ Coverage Diff @@
## develop #7924 +/- ##
===========================================
- Coverage 79.08% 79.07% -0.01%
===========================================
Files 1696 1696
Lines 196429 196456 +27
===========================================
+ Hits 155343 155352 +9
- Misses 41086 41104 +18 ☔ View full report in Codecov by Sentry. |
tautschnig
force-pushed
the
bugfixes/freebsd-build
branch
4 times, most recently
from
a1ae212 to
547ae0e
Compare
#7956 fixes that one. |
tautschnig
force-pushed
the
bugfixes/freebsd-build
branch
4 times, most recently
from
81b105b to
b791e29
Compare
tautschnig
force-pushed
the
bugfixes/freebsd-build
branch
from
0de2cb1 to
08f211c
Compare
|
@kroening @TGWDB I am hoping that this one is now uncontroversial. It would be great to get this merged in time for a version 6 release so that we can safely claim that version 6 also builds on FreeBSD. (And I would then try to sort out #7651 on top of this so that we can even claim OpenBSD/NetBSD support.) |
kroening
approved these changes
Nov 17, 2023
TGWDB
approved these changes
Nov 17, 2023
tautschnig
force-pushed
the
bugfixes/freebsd-build
branch
8 times, most recently
from
2109148 to
ecfafd9
Compare
We rely on thin archives via `ar rcT` for libcprover-cpp nests archives, which FreeBSD's `ar` does not support. Use `llvm-ar` instead, which does have this capability. This enables a successful build.
This improves portability as not all systems have bash, perl, or python in /usr/bin (FreeBSD is one such example).
FreeBSD has inline implementations of fe{set,get}round.
FreeBSD redefines various inet_* function names to __inet_*.
This is the same problem as previously seen on macOS.
It works for both FreeBSD kernel-only as well as full FreeBSD userland.
The object files are already part of libcprover-cpp, no need to add them again. Doing so results in duplicate-definition errors on FreeBSD.
Implemented as over-approximations of the implementations found at https://cgit.freebsd.org/src/tree/lib/libc/stdio/.
With Makefile-based builds, we rely on CaDiCaL's configure to produce an appropriate build script.
We can always fall back to `getrusage` for minimal memory usage information.
BSD systems won't alias gcc to clang.
Tags may contain an exclamation mark, which the shell will treat as a request for history expansion.
Library functions may introduce inline assembler. For example, FreeBSD's fesetround is an inline function with inline assembler. Library functions might introduce calls to fesetround, and thereby introduce inline assembler. Thus, run a fixed point over remove_asm and library linking.
This has the same usage as __assert_func in newlib. See https://github.com/openbsd/src/blob/master/include/assert.h.
Uses https://github.com/cross-platform-actions/action, and can be extended to OpenBSD and NetBSD. QEMU on Linux runners appears to be faster than nested virtualisation on macOS runnners (even when the latter ought to use more hardware acceleration).
Uses the same virtualisation set-up as FreeBSD checks.
This appears to have much better performance (FreeBSD job completes in 26 minutes instead of 4 hours). We can now also enable the same number of steps in OpenBSD and NetBSD.
This needs to be debugged eventually.
tautschnig
force-pushed
the
bugfixes/freebsd-build
branch
from
ecfafd9 to
18a35b8
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
We rely on thin archives via
ar rcTfor libcprover-cpp nests archives, which FreeBSD'sardoes not support. Usellvm-arinstead, which does have this capability. This enables a successful build.All further changes are to enable successful test runs, with one caveat: goto-analyzer/loop-termination-eq/test-value-sets.desc yields a segmentation fault that I was unable to root cause thus far.