3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-16 21:56:22 +00:00

ci: validate Microsoft.Z3.dll PE Machine field is AnyCPU in nightly build validation (#9873)

`Microsoft.Z3.dll` ships with PE `Machine=0x8664` (AMD64), causing the
CLR loader to reject it on arm64 .NET hosts (macOS/Linux/Windows ARM)
even though the assembly is pure IL (`CorFlags.ILONLY=True`) and arm64
native libraries are already bundled in the package.

## Changes

- **`.github/workflows/nightly-validation.yml`** — adds
`validate-dotnet-anycpu` job to the Nightly Build Validation workflow:
  - Downloads the nightly NuGet package from the GitHub release
- Extracts `lib/netstandard2.0/Microsoft.Z3.dll` (NuGet packages are ZIP
archives)
- Reads the COFF `Machine` field from the PE header using Python
`struct`
- Fails with an actionable error if `Machine` is `0x8664` (AMD64) or
`0xAA64` (ARM64); passes for `0x014C` (i386/AnyCPU) or `0x0000`

The check catches any regression where the managed wrapper is compiled
architecture-specific, blocking non-x64 .NET hosts from loading it.

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This commit is contained in:
Copilot 2026-06-16 11:16:19 -06:00 committed by GitHub
parent b6c7ef2f68
commit 66795ea322
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -844,3 +844,97 @@ jobs:
- name: Run build script unit tests
run: python -m unittest discover -s scripts/tests -p "test_*.py" -v
# ============================================================================
# DOTNET MANAGED WRAPPER ARCHITECTURE VALIDATION
# ============================================================================
validate-dotnet-anycpu:
name: "Validate Microsoft.Z3.dll is AnyCPU (issue #9863)"
runs-on: ubuntu-latest
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
timeout-minutes: 15
steps:
- name: Checkout code
uses: actions/checkout@v6.0.3
- name: Download NuGet package from release
env:
GH_TOKEN: ${{ github.token }}
run: |
TAG="${{ github.event.inputs.release_tag }}"
if [ -z "$TAG" ]; then
TAG="Nightly"
fi
gh release download $TAG --pattern "*.nupkg" --dir nuget-packages
- name: Extract managed DLL from NuGet package
run: |
# NuGet packages are ZIP archives; exclude the symbols package
NUPKG=$(ls nuget-packages/*.nupkg | grep -v '\.symbols\.' | grep -v '\.snupkg' | head -n 1)
echo "Checking package: $NUPKG"
unzip -q "$NUPKG" "lib/netstandard2.0/Microsoft.Z3.dll" -d nupkg-extracted
- name: Check PE Machine field is AnyCPU (not architecture-specific)
run: |
python3 - <<'EOF'
import struct
import sys
dll_path = "nupkg-extracted/lib/netstandard2.0/Microsoft.Z3.dll"
with open(dll_path, 'rb') as f:
# Verify MZ magic
if f.read(2) != b'MZ':
print("ERROR: Not a valid PE file (missing MZ header)")
sys.exit(1)
# Read PE header offset stored at 0x3C in the DOS stub
f.seek(0x3C)
pe_offset = struct.unpack('<I', f.read(4))[0]
# Verify PE signature
f.seek(pe_offset)
if f.read(4) != b'PE\x00\x00':
print("ERROR: Missing PE\\0\\0 signature")
sys.exit(1)
# COFF Machine field is the 2 bytes immediately after the PE signature
machine = struct.unpack('<H', f.read(2))[0]
machine_names = {
0x0000: "Unknown/AnyCPU",
0x014C: "i386 (AnyCPU for managed assemblies)",
0x8664: "AMD64/x64",
0xAA64: "ARM64",
0x01C0: "ARM",
0x01C4: "ARM Thumb-2",
}
machine_name = machine_names.get(machine, f"0x{machine:04X}")
print(f"Machine field: 0x{machine:04X} = {machine_name}")
if machine == 0x8664:
print()
print("FAIL: Machine is AMD64 (0x8664).")
print("This prevents loading on arm64 .NET hosts even though the assembly")
print("contains only pure IL (CorFlags.ILONLY=True).")
print("The DLL must be built as AnyCPU (Machine=0x014C) so the CLR loader")
print("accepts it on every host architecture.")
print("See issue #9863 for details.")
sys.exit(1)
elif machine == 0xAA64:
print()
print("FAIL: Machine is ARM64 (0xAA64).")
print("This prevents loading on x64 .NET hosts.")
print("The DLL must be built as AnyCPU (Machine=0x014C).")
sys.exit(1)
elif machine in (0x014C, 0x0000):
print()
print("PASS: Machine field indicates AnyCPU.")
print("Microsoft.Z3.dll will load on any .NET host architecture.")
else:
print()
print(f"FAIL: Unexpected Machine field 0x{machine:04X}.")
print("Expected 0x014C (i386/AnyCPU) for a managed-only assembly.")
sys.exit(1)
EOF