mirror of
https://github.com/Z3Prover/z3
synced 2026-06-17 14:16:22 +00:00
66795ea322
`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>
940 lines
32 KiB
YAML
940 lines
32 KiB
YAML
name: Nightly Build Validation
|
|
|
|
on:
|
|
workflow_run:
|
|
workflows: ["Nightly Build"]
|
|
types:
|
|
- completed
|
|
workflow_dispatch:
|
|
inputs:
|
|
release_tag:
|
|
description: 'Release tag to validate (default: Nightly)'
|
|
required: false
|
|
default: 'Nightly'
|
|
|
|
permissions:
|
|
contents: read
|
|
|
|
jobs:
|
|
# ============================================================================
|
|
# VALIDATION JOBS FOR NUGET PACKAGES
|
|
# ============================================================================
|
|
|
|
validate-nuget-windows-x64:
|
|
name: "Validate NuGet on Windows x64"
|
|
runs-on: windows-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v6.0.3
|
|
|
|
- name: Setup .NET
|
|
uses: actions/setup-dotnet@v5
|
|
with:
|
|
dotnet-version: '8.x'
|
|
|
|
- name: Download NuGet package from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
shell: pwsh
|
|
run: |
|
|
$tag = "${{ github.event.inputs.release_tag }}"
|
|
if ([string]::IsNullOrEmpty($tag)) {
|
|
$tag = "Nightly"
|
|
}
|
|
gh release download $tag --pattern "*.nupkg" --dir nuget-packages
|
|
|
|
- name: Create test project
|
|
shell: pwsh
|
|
run: |
|
|
mkdir test-nuget
|
|
cd test-nuget
|
|
dotnet new console
|
|
$nupkgFile = Get-ChildItem ../nuget-packages/*.nupkg -Exclude *.symbols.nupkg | Select-Object -First 1
|
|
dotnet add package Microsoft.Z3 --source ../nuget-packages --prerelease
|
|
|
|
- name: Create test code
|
|
shell: pwsh
|
|
run: |
|
|
@"
|
|
using Microsoft.Z3;
|
|
class Program {
|
|
static void Main() {
|
|
using (Context ctx = new Context()) {
|
|
IntExpr x = ctx.MkIntConst("x");
|
|
Solver solver = ctx.MkSolver();
|
|
solver.Assert(ctx.MkGt(x, ctx.MkInt(0)));
|
|
if (solver.Check() == Status.SATISFIABLE) {
|
|
System.Console.WriteLine("sat");
|
|
System.Console.WriteLine(solver.Model);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
"@ | Out-File -FilePath test-nuget/Program.cs -Encoding utf8
|
|
|
|
- name: Run test
|
|
shell: pwsh
|
|
run: |
|
|
cd test-nuget
|
|
dotnet run
|
|
|
|
validate-nuget-ubuntu-x64:
|
|
name: "Validate NuGet on Ubuntu x64"
|
|
runs-on: ubuntu-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v6.0.3
|
|
|
|
- name: Setup .NET
|
|
uses: actions/setup-dotnet@v5
|
|
with:
|
|
dotnet-version: '8.x'
|
|
|
|
- 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: Create test project
|
|
run: |
|
|
mkdir test-nuget
|
|
cd test-nuget
|
|
dotnet new console
|
|
dotnet add package Microsoft.Z3 --source ../nuget-packages --prerelease
|
|
|
|
- name: Create test code
|
|
run: |
|
|
cat > test-nuget/Program.cs << 'EOF'
|
|
using Microsoft.Z3;
|
|
class Program {
|
|
static void Main() {
|
|
using (Context ctx = new Context()) {
|
|
IntExpr x = ctx.MkIntConst("x");
|
|
Solver solver = ctx.MkSolver();
|
|
solver.Assert(ctx.MkGt(x, ctx.MkInt(0)));
|
|
if (solver.Check() == Status.SATISFIABLE) {
|
|
System.Console.WriteLine("sat");
|
|
System.Console.WriteLine(solver.Model);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
EOF
|
|
|
|
- name: Run test
|
|
run: |
|
|
cd test-nuget
|
|
dotnet run
|
|
|
|
validate-nuget-macos-x64:
|
|
name: "Validate NuGet on macOS x64"
|
|
runs-on: macos-15-intel
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v6.0.3
|
|
|
|
- name: Setup .NET
|
|
uses: actions/setup-dotnet@v5
|
|
with:
|
|
dotnet-version: '8.x'
|
|
|
|
- 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: Create test project
|
|
run: |
|
|
mkdir test-nuget
|
|
cd test-nuget
|
|
dotnet new console
|
|
dotnet add package Microsoft.Z3 --source ../nuget-packages --prerelease
|
|
|
|
- name: Create test code
|
|
run: |
|
|
cat > test-nuget/Program.cs << 'EOF'
|
|
using Microsoft.Z3;
|
|
class Program {
|
|
static void Main() {
|
|
using (Context ctx = new Context()) {
|
|
IntExpr x = ctx.MkIntConst("x");
|
|
Solver solver = ctx.MkSolver();
|
|
solver.Assert(ctx.MkGt(x, ctx.MkInt(0)));
|
|
if (solver.Check() == Status.SATISFIABLE) {
|
|
System.Console.WriteLine("sat");
|
|
System.Console.WriteLine(solver.Model);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
EOF
|
|
|
|
- name: Run test
|
|
run: |
|
|
cd test-nuget
|
|
dotnet run
|
|
|
|
validate-nuget-macos-arm64:
|
|
name: "Validate NuGet on macOS ARM64"
|
|
runs-on: macos-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v6.0.3
|
|
|
|
- name: Setup .NET
|
|
uses: actions/setup-dotnet@v5
|
|
with:
|
|
dotnet-version: '8.x'
|
|
|
|
- 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: Create test project
|
|
run: |
|
|
mkdir test-nuget
|
|
cd test-nuget
|
|
dotnet new console
|
|
dotnet add package Microsoft.Z3 --source ../nuget-packages --prerelease
|
|
|
|
- name: Create test code
|
|
run: |
|
|
cat > test-nuget/Program.cs << 'EOF'
|
|
using Microsoft.Z3;
|
|
class Program {
|
|
static void Main() {
|
|
using (Context ctx = new Context()) {
|
|
IntExpr x = ctx.MkIntConst("x");
|
|
Solver solver = ctx.MkSolver();
|
|
solver.Assert(ctx.MkGt(x, ctx.MkInt(0)));
|
|
if (solver.Check() == Status.SATISFIABLE) {
|
|
System.Console.WriteLine("sat");
|
|
System.Console.WriteLine(solver.Model);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
EOF
|
|
|
|
- name: Run test
|
|
run: |
|
|
cd test-nuget
|
|
dotnet run
|
|
|
|
# ============================================================================
|
|
# VALIDATION JOBS FOR EXECUTABLES
|
|
# ============================================================================
|
|
|
|
validate-exe-windows-x64:
|
|
name: "Validate executable on Windows x64"
|
|
runs-on: windows-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v6.0.3
|
|
|
|
- name: Download Windows x64 build from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
shell: pwsh
|
|
run: |
|
|
$tag = "${{ github.event.inputs.release_tag }}"
|
|
if ([string]::IsNullOrEmpty($tag)) {
|
|
$tag = "Nightly"
|
|
}
|
|
gh release download $tag --pattern "*x64-win*.zip" --dir downloads
|
|
|
|
- name: Extract and test
|
|
shell: pwsh
|
|
run: |
|
|
$zipFile = Get-ChildItem downloads/*x64-win*.zip | Select-Object -First 1
|
|
Expand-Archive -Path $zipFile -DestinationPath z3-test
|
|
$z3Dir = Get-ChildItem z3-test -Directory | Select-Object -First 1
|
|
& "$z3Dir/bin/z3.exe" --version
|
|
|
|
# Test basic SMT solving
|
|
@"
|
|
(declare-const x Int)
|
|
(assert (> x 0))
|
|
(check-sat)
|
|
(get-model)
|
|
"@ | & "$z3Dir/bin/z3.exe" -in
|
|
|
|
validate-exe-windows-x86:
|
|
name: "Validate executable on Windows x86"
|
|
runs-on: windows-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v6.0.3
|
|
|
|
- name: Download Windows x86 build from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
shell: pwsh
|
|
run: |
|
|
$tag = "${{ github.event.inputs.release_tag }}"
|
|
if ([string]::IsNullOrEmpty($tag)) {
|
|
$tag = "Nightly"
|
|
}
|
|
gh release download $tag --pattern "*x86-win*.zip" --dir downloads
|
|
|
|
- name: Extract and test
|
|
shell: pwsh
|
|
run: |
|
|
$zipFile = Get-ChildItem downloads/*x86-win*.zip | Select-Object -First 1
|
|
Expand-Archive -Path $zipFile -DestinationPath z3-test
|
|
$z3Dir = Get-ChildItem z3-test -Directory | Select-Object -First 1
|
|
& "$z3Dir/bin/z3.exe" --version
|
|
|
|
# Test basic SMT solving
|
|
@"
|
|
(declare-const x Int)
|
|
(assert (> x 0))
|
|
(check-sat)
|
|
(get-model)
|
|
"@ | & "$z3Dir/bin/z3.exe" -in
|
|
|
|
validate-exe-ubuntu-x64:
|
|
name: "Validate executable on Ubuntu x64"
|
|
runs-on: ubuntu-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v6.0.3
|
|
|
|
- name: Download Ubuntu x64 build 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 "*x64-glibc*.zip" --dir downloads
|
|
|
|
- name: Extract and test
|
|
run: |
|
|
cd downloads
|
|
unzip *x64-glibc*.zip
|
|
Z3_DIR=$(find . -maxdepth 1 -type d -name "z3-*" | head -n 1)
|
|
cd "$Z3_DIR"
|
|
./bin/z3 --version
|
|
|
|
# Test basic SMT solving
|
|
echo "(declare-const x Int)
|
|
(assert (> x 0))
|
|
(check-sat)
|
|
(get-model)" | ./bin/z3 -in
|
|
|
|
validate-exe-macos-x64:
|
|
name: "Validate executable on macOS x64"
|
|
runs-on: macos-15-intel
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v6.0.3
|
|
|
|
- name: Download macOS x64 build 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 "*x64-osx*.zip" --dir downloads
|
|
|
|
- name: Extract and test
|
|
run: |
|
|
cd downloads
|
|
unzip *x64-osx*.zip
|
|
Z3_DIR=$(find . -maxdepth 1 -type d -name "z3-*" | head -n 1)
|
|
cd "$Z3_DIR"
|
|
./bin/z3 --version
|
|
|
|
# Test basic SMT solving
|
|
echo "(declare-const x Int)
|
|
(assert (> x 0))
|
|
(check-sat)
|
|
(get-model)" | ./bin/z3 -in
|
|
|
|
validate-exe-macos-arm64:
|
|
name: "Validate executable on macOS ARM64"
|
|
runs-on: macos-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v6.0.3
|
|
|
|
- name: Download macOS ARM64 build 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 "*arm64-osx*.zip" --dir downloads
|
|
|
|
- name: Extract and test
|
|
run: |
|
|
cd downloads
|
|
unzip *arm64-osx*.zip
|
|
Z3_DIR=$(find . -maxdepth 1 -type d -name "z3-*" | head -n 1)
|
|
cd "$Z3_DIR"
|
|
./bin/z3 --version
|
|
|
|
# Test basic SMT solving
|
|
echo "(declare-const x Int)
|
|
(assert (> x 0))
|
|
(check-sat)
|
|
(get-model)" | ./bin/z3 -in
|
|
|
|
# ============================================================================
|
|
# REGRESSION TEST VALIDATION
|
|
# ============================================================================
|
|
|
|
validate-regressions-ubuntu:
|
|
name: "Validate regression tests on Ubuntu"
|
|
runs-on: ubuntu-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 60
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v6.0.3
|
|
|
|
- name: Setup Python
|
|
uses: actions/setup-python@v6
|
|
with:
|
|
python-version: '3.x'
|
|
|
|
- name: Download Ubuntu x64 build 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 "*x64-glibc*.zip" --dir downloads
|
|
|
|
- name: Extract build
|
|
run: |
|
|
cd downloads
|
|
unzip *x64-glibc*.zip
|
|
cd ..
|
|
|
|
- name: Clone z3test repository
|
|
run: git clone https://github.com/z3prover/z3test z3test
|
|
|
|
- name: Run regression tests
|
|
run: |
|
|
Z3_PATH=$(find downloads -name z3 -type f | head -n 1)
|
|
chmod +x $Z3_PATH
|
|
python z3test/scripts/test_benchmarks.py $Z3_PATH z3test/regressions/smt2
|
|
|
|
validate-regressions-windows:
|
|
name: "Validate regression tests on Windows"
|
|
runs-on: windows-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 60
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v6.0.3
|
|
|
|
- name: Setup Python
|
|
uses: actions/setup-python@v6
|
|
with:
|
|
python-version: '3.x'
|
|
|
|
- name: Download Windows x64 build from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
shell: pwsh
|
|
run: |
|
|
$tag = "${{ github.event.inputs.release_tag }}"
|
|
if ([string]::IsNullOrEmpty($tag)) {
|
|
$tag = "Nightly"
|
|
}
|
|
gh release download $tag --pattern "*x64-win*.zip" --dir downloads
|
|
|
|
- name: Extract build
|
|
shell: pwsh
|
|
run: |
|
|
$zipFile = Get-ChildItem downloads/*x64-win*.zip | Select-Object -First 1
|
|
Expand-Archive -Path $zipFile -DestinationPath downloads
|
|
|
|
- name: Clone z3test repository
|
|
run: git clone https://github.com/z3prover/z3test z3test
|
|
|
|
- name: Run regression tests
|
|
shell: pwsh
|
|
run: |
|
|
$z3Path = Get-ChildItem downloads -Filter z3.exe -Recurse | Select-Object -First 1
|
|
python z3test/scripts/test_benchmarks.py $z3Path.FullName z3test/regressions/smt2
|
|
|
|
validate-regressions-macos:
|
|
name: "Validate regression tests on macOS"
|
|
runs-on: macos-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 60
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v6.0.3
|
|
|
|
- name: Setup Python
|
|
uses: actions/setup-python@v6
|
|
with:
|
|
python-version: '3.x'
|
|
|
|
- name: Download macOS ARM64 build 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 "*arm64-osx*.zip" --dir downloads
|
|
|
|
- name: Extract build
|
|
run: |
|
|
cd downloads
|
|
unzip *arm64-osx*.zip
|
|
cd ..
|
|
|
|
- name: Clone z3test repository
|
|
run: git clone https://github.com/z3prover/z3test z3test
|
|
|
|
- name: Run regression tests
|
|
run: |
|
|
Z3_PATH=$(find downloads -name z3 -type f | head -n 1)
|
|
chmod +x $Z3_PATH
|
|
python z3test/scripts/test_benchmarks.py $Z3_PATH z3test/regressions/smt2
|
|
|
|
# ============================================================================
|
|
# PYTHON WHEEL VALIDATION
|
|
# ============================================================================
|
|
|
|
validate-python-wheel-ubuntu-x64:
|
|
name: "Validate Python wheel on Ubuntu x64"
|
|
runs-on: ubuntu-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v6.0.3
|
|
|
|
- name: Setup Python
|
|
uses: actions/setup-python@v6
|
|
with:
|
|
python-version: '3.x'
|
|
|
|
- name: Download Python wheel 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 "*manylinux*x86_64.whl" --dir wheels
|
|
|
|
- name: Install and test wheel
|
|
run: |
|
|
pip install wheels/*.whl
|
|
python -c "import z3; x = z3.Int('x'); s = z3.Solver(); s.add(x > 0); print('Result:', s.check()); print('Model:', s.model())"
|
|
|
|
validate-python-wheel-macos-arm64:
|
|
name: "Validate Python wheel on macOS ARM64"
|
|
runs-on: macos-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v6.0.3
|
|
|
|
- name: Setup Python
|
|
uses: actions/setup-python@v6
|
|
with:
|
|
python-version: '3.x'
|
|
|
|
- name: Download Python wheel 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 "*macosx*arm64.whl" --dir wheels
|
|
|
|
- name: Install and test wheel
|
|
run: |
|
|
pip install wheels/*.whl
|
|
python -c "import z3; x = z3.Int('x'); s = z3.Solver(); s.add(x > 0); print('Result:', s.check()); print('Model:', s.model())"
|
|
|
|
validate-python-wheel-macos-x64:
|
|
name: "Validate Python wheel on macOS x64"
|
|
runs-on: macos-15-intel
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v6.0.3
|
|
|
|
- name: Setup Python
|
|
uses: actions/setup-python@v6
|
|
with:
|
|
python-version: '3.x'
|
|
|
|
- name: Download Python wheel 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 "*macosx*x86_64.whl" --dir wheels
|
|
|
|
- name: Install and test wheel
|
|
run: |
|
|
pip install wheels/*.whl
|
|
python -c "import z3; x = z3.Int('x'); s = z3.Solver(); s.add(x > 0); print('Result:', s.check()); print('Model:', s.model())"
|
|
|
|
validate-python-wheel-windows-x64:
|
|
name: "Validate Python wheel on Windows x64"
|
|
runs-on: windows-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v6.0.3
|
|
|
|
- name: Setup Python
|
|
uses: actions/setup-python@v6
|
|
with:
|
|
python-version: '3.x'
|
|
|
|
- name: Download Python wheel from release
|
|
env:
|
|
GH_TOKEN: ${{ github.token }}
|
|
shell: pwsh
|
|
run: |
|
|
$tag = "${{ github.event.inputs.release_tag }}"
|
|
if ([string]::IsNullOrEmpty($tag)) {
|
|
$tag = "Nightly"
|
|
}
|
|
gh release download $tag --pattern "*win_amd64.whl" --dir wheels
|
|
|
|
- name: Install and test wheel
|
|
shell: pwsh
|
|
run: |
|
|
$wheel = Get-ChildItem wheels/*.whl | Select-Object -First 1
|
|
pip install $wheel.FullName
|
|
python -c "import z3; x = z3.Int('x'); s = z3.Solver(); s.add(x > 0); print('Result:', s.check()); print('Model:', s.model())"
|
|
|
|
validate-python-wheel-riscv64:
|
|
name: "Validate Python wheel for RISC-V 64"
|
|
runs-on: ubuntu-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v6.0.3
|
|
|
|
- name: Setup Python
|
|
uses: actions/setup-python@v6
|
|
with:
|
|
python-version: '3.x'
|
|
|
|
- name: Download RISC-V 64 Python wheel 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 "*riscv64.whl" --dir wheels
|
|
|
|
- name: Verify wheel platform tag and contents
|
|
run: |
|
|
pip install wheel
|
|
WHEEL_FILE=$(ls wheels/*.whl | head -n 1)
|
|
echo "Wheel file: $WHEEL_FILE"
|
|
|
|
# Check that the wheel has a riscv64 platform tag
|
|
WHEEL_NAME=$(basename $WHEEL_FILE)
|
|
echo "Wheel name: $WHEEL_NAME"
|
|
if echo "$WHEEL_NAME" | grep -q "riscv64"; then
|
|
echo "riscv64 platform tag found"
|
|
else
|
|
echo "ERROR: riscv64 platform tag not found in wheel name"
|
|
exit 1
|
|
fi
|
|
|
|
# Inspect wheel contents
|
|
python -m zipfile -l $WHEEL_FILE
|
|
|
|
# Verify wheel contains z3 library
|
|
if python -m zipfile -l $WHEEL_FILE | grep -q "libz3"; then
|
|
echo "libz3 found in wheel"
|
|
else
|
|
echo "ERROR: libz3 not found in wheel"
|
|
exit 1
|
|
fi
|
|
|
|
# ============================================================================
|
|
# MACOS DYLIB HEADERPAD VALIDATION
|
|
# ============================================================================
|
|
|
|
validate-macos-headerpad-x64:
|
|
name: "Validate macOS x64 dylib headerpad"
|
|
runs-on: macos-15-intel
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v6.0.3
|
|
|
|
- name: Download macOS x64 build 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 "*x64-osx*.zip" --dir downloads
|
|
|
|
- name: Extract build
|
|
run: |
|
|
cd downloads
|
|
unzip *x64-osx*.zip
|
|
Z3_DIR=$(find . -maxdepth 1 -type d -name "z3-*" | head -n 1)
|
|
echo "Z3_DIR=$Z3_DIR" >> $GITHUB_ENV
|
|
|
|
- name: Test install_name_tool with headerpad
|
|
run: |
|
|
cd downloads/$Z3_DIR/bin
|
|
|
|
# Get the original install name
|
|
ORIGINAL_NAME=$(otool -D libz3.dylib | tail -n 1)
|
|
echo "Original install name: $ORIGINAL_NAME"
|
|
|
|
# Create a test path with same length as typical setup-z3 usage
|
|
# This simulates what setup-z3 does: changing to absolute path
|
|
TEST_PATH="/Users/runner/hostedtoolcache/z3/latest/x64/z3-test-dir/bin/libz3.dylib"
|
|
|
|
# Try to change the install name - this will fail if headerpad is insufficient
|
|
install_name_tool -id "$TEST_PATH" -change "$ORIGINAL_NAME" "$TEST_PATH" libz3.dylib
|
|
|
|
# Verify the change was successful
|
|
NEW_NAME=$(otool -D libz3.dylib | tail -n 1)
|
|
echo "New install name: $NEW_NAME"
|
|
|
|
if [ "$NEW_NAME" = "$TEST_PATH" ]; then
|
|
echo "✓ install_name_tool succeeded - headerpad is sufficient"
|
|
else
|
|
echo "✗ install_name_tool failed to update install name"
|
|
exit 1
|
|
fi
|
|
|
|
validate-macos-headerpad-arm64:
|
|
name: "Validate macOS ARM64 dylib headerpad"
|
|
runs-on: macos-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 30
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v6.0.3
|
|
|
|
- name: Download macOS ARM64 build 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 "*arm64-osx*.zip" --dir downloads
|
|
|
|
- name: Extract build
|
|
run: |
|
|
cd downloads
|
|
unzip *arm64-osx*.zip
|
|
Z3_DIR=$(find . -maxdepth 1 -type d -name "z3-*" | head -n 1)
|
|
echo "Z3_DIR=$Z3_DIR" >> $GITHUB_ENV
|
|
|
|
- name: Test install_name_tool with headerpad
|
|
run: |
|
|
cd downloads/$Z3_DIR/bin
|
|
|
|
# Get the original install name
|
|
ORIGINAL_NAME=$(otool -D libz3.dylib | tail -n 1)
|
|
echo "Original install name: $ORIGINAL_NAME"
|
|
|
|
# Create a test path with same length as typical setup-z3 usage
|
|
# This simulates what setup-z3 does: changing to absolute path
|
|
TEST_PATH="/Users/runner/hostedtoolcache/z3/latest/arm64/z3-test-dir/bin/libz3.dylib"
|
|
|
|
# Try to change the install name - this will fail if headerpad is insufficient
|
|
install_name_tool -id "$TEST_PATH" -change "$ORIGINAL_NAME" "$TEST_PATH" libz3.dylib
|
|
|
|
# Verify the change was successful
|
|
NEW_NAME=$(otool -D libz3.dylib | tail -n 1)
|
|
echo "New install name: $NEW_NAME"
|
|
|
|
if [ "$NEW_NAME" = "$TEST_PATH" ]; then
|
|
echo "✓ install_name_tool succeeded - headerpad is sufficient"
|
|
else
|
|
echo "✗ install_name_tool failed to update install name"
|
|
exit 1
|
|
fi
|
|
|
|
# ============================================================================
|
|
# BUILD SCRIPT UNIT TESTS
|
|
# ============================================================================
|
|
|
|
validate-build-script-tests:
|
|
name: "Validate build script unit tests"
|
|
runs-on: ubuntu-latest
|
|
if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
|
|
timeout-minutes: 10
|
|
steps:
|
|
- name: Checkout code
|
|
uses: actions/checkout@v6.0.3
|
|
|
|
- name: Setup Python
|
|
uses: actions/setup-python@v6
|
|
with:
|
|
python-version: '3.x'
|
|
|
|
- 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
|