@@ -58,6 +58,7 @@ $PrebuiltZ3ServerFeatures = "--features openshell-server/prebuilt-z3,openshell-p
5858$PrebuiltZ3Version = " 5.1.0"
5959$Z3WorkspaceFeatures = $PrebuiltZ3WorkspaceFeatures
6060$Z3ServerFeatures = $PrebuiltZ3ServerFeatures
61+ $Z3GatewayFeatures = " --features prebuilt-z3"
6162
6263function Get-VsInstallRoots {
6364 $programFiles = @ (
@@ -514,6 +515,39 @@ function Invoke-Build([string] $RustTarget) {
514515 - RustTarget $RustTarget `
515516 - CargoArgs " cargo build --release --target $RustTarget --bin openshell-gateway --bin openshell --bin openshell-supervisor --bin openshell-windows-sandbox $Z3WorkspaceFeatures " `
516517 - LogName " build-$RustTarget -release.log"
518+ Stage- Z3Runtime $RustTarget
519+ }
520+
521+ function Stage-Z3Runtime ([string ] $RustTarget ) {
522+ $release = Join-Path $TargetDir " $RustTarget /release"
523+ if ($env: Z3_LIBRARY_PATH_OVERRIDE ) {
524+ $candidates = @ (Get-Item - LiteralPath (Join-Path $env: Z3_LIBRARY_PATH_OVERRIDE ' libz3.dll' ) - ErrorAction SilentlyContinue)
525+ } else {
526+ # Only use the pinned release from this target's build cache. Never pick
527+ # the newest arbitrary DLL, or trust a stale adjacent runtime.
528+ $candidates = @ (Get-ChildItem - Path (Join-Path $release " build/z3-sys-*/out/z3-$PrebuiltZ3Version /bin/libz3.dll" ) - File - ErrorAction SilentlyContinue)
529+ }
530+ if ($candidates.Count -eq 0 ) { throw " Matching libz3.dll not found for $RustTarget ." }
531+ $hashes = @ ($candidates | ForEach-Object { (Get-FileHash - LiteralPath $_.FullName - Algorithm SHA256).Hash } | Select-Object - Unique)
532+ if ($hashes.Count -ne 1 ) { throw " Ambiguous Z3 runtimes for $RustTarget ; use a clean target cache or Z3_LIBRARY_PATH_OVERRIDE." }
533+ $source = $candidates [0 ].FullName
534+ $reader = [IO.BinaryReader ]::new([IO.File ]::OpenRead($source ))
535+ try {
536+ if ($reader.ReadUInt16 () -ne 0x5A4D ) { throw " Invalid Z3 DLL: $source " }
537+ $reader.BaseStream.Position = 0x3C
538+ $offset = $reader.ReadInt32 ()
539+ if ($offset -lt 64 -or $offset -gt $reader.BaseStream.Length - 6 ) { throw ' Invalid Z3 PE offset.' }
540+ $reader.BaseStream.Position = $offset
541+ if ($reader.ReadUInt32 () -ne 0x00004550 ) { throw ' Invalid Z3 PE signature.' }
542+ $expected = if ($RustTarget -eq ' aarch64-pc-windows-msvc' ) { 0xAA64 } else { 0x8664 }
543+ if ($reader.ReadUInt16 () -ne $expected ) { throw " Z3 DLL architecture does not match $RustTarget ." }
544+ } finally { $reader.Dispose () }
545+ $destination = Join-Path $release ' libz3.dll'
546+ if ([IO.Path ]::GetFullPath($source ) -ne [IO.Path ]::GetFullPath($destination )) {
547+ Copy-Item - LiteralPath $source - Destination $destination - Force
548+ }
549+ if ((Get-FileHash - LiteralPath $destination - Algorithm SHA256).Hash -ne $hashes [0 ]) { throw ' Staged Z3 DLL hash mismatch.' }
550+ Write-Host " ==> Staged $destination (SHA256=$ ( $hashes [0 ]) )"
517551}
518552
519553function Invoke-Test ([string ] $RustTarget ) {
@@ -542,7 +576,7 @@ function Invoke-UnsupportedContractTests([string] $RustTarget) {
542576 foreach ($test in $tests ) {
543577 Invoke-VsCargo `
544578 - RustTarget $RustTarget `
545- - CargoArgs " cargo test -p openshell-gateway --target $RustTarget $test $Z3WorkspaceFeatures " `
579+ - CargoArgs " cargo test -p openshell-gateway --target $RustTarget $test $Z3GatewayFeatures " `
546580 - LogName " test-$RustTarget -unsupported-$test .log"
547581 }
548582
@@ -551,7 +585,7 @@ function Invoke-UnsupportedContractTests([string] $RustTarget) {
551585 $variant = if ($features ) { $features.Replace (" ," , " -" ) } else { " protocol-only" }
552586 Invoke-VsCargo `
553587 - RustTarget $RustTarget `
554- - CargoArgs " cargo test -p openshell-gateway --lib --target $RustTarget --no-default-features $featureArgs $Z3ServerFeatures " `
588+ - CargoArgs " cargo test -p openshell-gateway --lib --target $RustTarget --no-default-features $featureArgs $Z3GatewayFeatures " `
555589 - LogName " test-$RustTarget -selective-$variant .log"
556590 }
557591}
@@ -618,6 +652,7 @@ if ($Action -in @("check", "lint", "build", "build-mxc-fixtures", "test", "test-
618652 $z3Features = Configure- Z3
619653 $Z3WorkspaceFeatures = $z3Features.WorkspaceFeatures
620654 $Z3ServerFeatures = $z3Features.ServerFeatures
655+ $Z3GatewayFeatures = if ($z3Features.WorkspaceFeatures ) { " --features prebuilt-z3" } else { " " }
621656 $env: LIBCLANG_PATH = Resolve-LibclangPath
622657 Add-PathEntry $env: LIBCLANG_PATH
623658 Write-Host " ==> LIBCLANG_PATH=$env: LIBCLANG_PATH "
0 commit comments