z3/.github/workflows/README-macos-headerpad.md

macOS Dylib Header Padding Validation

Background

Release 4.15.5 broke install_name_tool on macOS with "larger updated load commands do not fit" errors. The Mach-O dylib headers lacked sufficient padding for install name modifications.

See:

• Issue: https://github.com/Z3Prover/z3/issues/8532
• Fix: https://github.com/Z3Prover/z3/pull/8535

The Problem

macOS dynamic libraries (dylibs) have a Mach-O header that includes "load commands" specifying various metadata, including the library's install name. Tools like install_name_tool can modify these load commands to change paths.

However, if the header doesn't have sufficient padding, modifying the install name to a longer path will fail with:

error: changing install names or rpaths can't be redone for: libz3.dylib (for architecture arm64) 
because larger updated load commands do not fit (the program must be relinked, 
and you may need to use -headerpad or -headerpad_max_install_names)

This breaks tools like setup-z3 which need to modify the install name to absolute paths in CI environments.

The Solution

Build-Time Fix

The Z3 build system now unconditionally adds -Wl,-headerpad_max_install_names when building shared libraries on macOS:

• Python build system: Modified scripts/mk_util.py to apply the flag unconditionally (not just when ML bindings are enabled)
• CMake build system: Added target_link_options to all macOS shared libraries (libz3, z3java, z3jl, OCaml bindings)

Validation Jobs

To prevent this issue from recurring, we've added validation jobs to the CI/CD pipeline that test whether install_name_tool can successfully modify the dylib install names.

Workflows with Validation

1. nightly.yml - Nightly builds

   • validate-macos-headerpad-x64: Validates x64 macOS builds
   • validate-macos-headerpad-arm64: Validates ARM64 macOS builds
   • These jobs run after the build stage and before deployment

2. release.yml - Release builds

   • validate-macos-headerpad-x64: Validates x64 macOS builds
   • validate-macos-headerpad-arm64: Validates ARM64 macOS builds
   • These jobs run after the build stage and before publication

3. nightly-validation.yml - Post-deployment validation

   • validate-macos-headerpad-x64: Validates published x64 builds
   • validate-macos-headerpad-arm64: Validates published ARM64 builds
   • These jobs run after releases are published to verify the artifacts

How Validation Works

Each validation job:

1. Downloads the macOS build artifact
2. Extracts the zip file and locates libz3.dylib
3. Uses otool -D to read the current install name
4. Attempts to change the install name to a long path similar to what setup-z3 uses:

   /Users/runner/hostedtoolcache/z3/latest/x64/z3-4.15.5-x64-osx-15.7.3/bin/libz3.dylib
   

5. Verifies the change succeeded
6. Fails the build if headerpad is insufficient

Test Path Selection

The validation uses paths that match the length and structure of real-world usage by setup-z3. The actual test paths used are:

• x64: /Users/runner/hostedtoolcache/z3/latest/x64/z3-test-dir/bin/libz3.dylib
• ARM64: /Users/runner/hostedtoolcache/z3/latest/arm64/z3-test-dir/bin/libz3.dylib

These paths are representative of the GitHub Actions hosted tool cache paths. For example, setup-z3 might use paths like:

• /Users/runner/hostedtoolcache/z3/latest/x64/z3-4.15.5-x64-osx-15.7.3/bin/libz3.dylib

The test paths use z3-test-dir instead of actual version numbers to remain version-agnostic while maintaining the same path length characteristics.

Impact

With these validations in place:

• Releases with insufficient header padding will fail CI before publication
• Users won't encounter install_name_tool errors when using Z3 in CI
• The issue can be detected and fixed immediately during development

References

• Original issue: https://github.com/Z3Prover/z3/issues/8532
• Fix PR: https://github.com/Z3Prover/z3/pull/8535
• Previous similar issue: https://github.com/Z3Prover/z3/pull/7623
• setup-z3 action: https://github.com/cda-tum/setup-z3