mirror of
https://github.com/Z3Prover/z3
synced 2026-06-19 07:06:28 +00:00
Add validate-dotnet-anycpu job to nightly-validation workflow (issue #9863)
This commit is contained in:
parent
cc0cc84177
commit
0648a8be97
1 changed files with 94 additions and 0 deletions
94
.github/workflows/nightly-validation.yml
vendored
94
.github/workflows/nightly-validation.yml
vendored
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue