From 16b8ca566e35f32237307a1f6863d790da6985d0 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Sun, 4 Oct 2026 14:40:33 +0200 Subject: [PATCH] Bind the Python package to NajaEDA through its shipped headers The naja fork now ships only the headers matching its wheel's libraries (najaeda/sdk/include) instead of the shared-runtime SDK. Replace the SDK path and the separate published-wheel adapter with one provider path: naja_provider.py resolves the installed package's libraries and headers (or the 0.7.24 source archive with KEPLER_USE_PUBLISHED_NAJAEDA), KeplerSharedNaja.cmake creates the imported targets, and KeplerNajaRuntime.cpp checks the provider's version, git hash, file hashes, exported Python types and live universe before borrowing a design through its wrapper. The DNL singleton is swapped through naja's exported dnlFull_ in both modes. Re-sign the installed extension on macOS: CMake's install RPATH rewrite invalidated the fixup's ad-hoc signature, so a plain pip install was killed at import on Apple Silicon. Update the submodule to fork main (ad34893b, NajaEDA 0.7.27) and the development provider pins to 0.7.27. --- .github/workflows/regress-python.yml | 2 +- ci/prepare_python_release.py | 2 +- ci/shared_naja_wheels.py | 6 +- docs/python-api.md | 26 +- docs/python-regression.md | 3 +- docs/python-release.md | 11 +- pyproject.toml | 4 +- regress/run_python_regress.py | 15 +- src/python/CMakeLists.txt | 20 +- src/python/KeplerNajaRuntime.cpp | 124 ++++++-- src/python/KeplerNajaState.cpp | 10 +- src/python/KeplerPublishedNaja.cmake | 78 ----- src/python/KeplerPublishedNajaRuntime.cpp | 186 ------------ src/python/KeplerSharedNaja.cmake | 106 +++++-- src/python/PyKeplerFormal.cpp | 2 +- ...ublished_runtime.py => _provider_check.py} | 28 +- ...{published_najaeda.py => naja_provider.py} | 151 +++++++--- test/python/test_naja_provider.py | 284 ++++++++++++++++++ test/python/test_najaeda.py | 29 -- ...y.py => test_provider_interoperability.py} | 15 +- test/python/test_published_najaeda.py | 187 ------------ test/python/test_python_release.py | 10 +- ...ction.py => test_shared_naja_selection.py} | 177 ++++++----- thirdparty/naja | 2 +- 24 files changed, 744 insertions(+), 734 deletions(-) delete mode 100644 src/python/KeplerPublishedNaja.cmake delete mode 100644 src/python/KeplerPublishedNajaRuntime.cpp rename src/python/kepler_formal/{_published_runtime.py => _provider_check.py} (67%) rename src/python/{published_najaeda.py => naja_provider.py} (65%) create mode 100644 test/python/test_naja_provider.py rename test/python/{test_published_interoperability.py => test_provider_interoperability.py} (91%) delete mode 100644 test/python/test_published_najaeda.py rename test/python/{test_shared_naja_sdk_selection.py => test_shared_naja_selection.py} (54%) diff --git a/.github/workflows/regress-python.yml b/.github/workflows/regress-python.yml index 9733c9de..ee7a5fa0 100644 --- a/.github/workflows/regress-python.yml +++ b/.github/workflows/regress-python.yml @@ -36,7 +36,7 @@ jobs: with: python-version: '3.12' - # The SDK-selection tests require CMake 3.30 or newer. + # The provider-selection tests require CMake 3.30 or newer. - uses: jwlawson/actions-setup-cmake@v2 with: cmake-version: '3.31.x' diff --git a/ci/prepare_python_release.py b/ci/prepare_python_release.py index 1e4ccf39..64be71e5 100644 --- a/ci/prepare_python_release.py +++ b/ci/prepare_python_release.py @@ -16,7 +16,7 @@ import re -DEVELOPMENT_REQUIREMENT = "najaeda==0.7.26" +DEVELOPMENT_REQUIREMENT = "najaeda==0.7.27" PUBLISHED_REQUIREMENT = "najaeda==0.7.24" CMAKE_OPTION = "KEPLER_USE_PUBLISHED_NAJAEDA" VERSION_PATTERN = r'KEPLER_VERSION\s*\{\s*"(?P[0-9]+\.[0-9]+\.[0-9]+)"' diff --git a/ci/shared_naja_wheels.py b/ci/shared_naja_wheels.py index 7bdbb209..5236056c 100644 --- a/ci/shared_naja_wheels.py +++ b/ci/shared_naja_wheels.py @@ -2,7 +2,7 @@ # Copyright 2026 keplertech.io # SPDX-License-Identifier: GPL-3.0-only -"""Build a local SDK provider for CI, and repair consumers without copying it. +"""Build a local NajaEDA provider for CI, and repair consumers without copying it. The provider is a separate wheel. This helper never publishes either package. After the matching NajaEDA release exists, ordinary isolated pip builds can @@ -24,7 +24,7 @@ # version number as the NajaEDA release it is based on, so the version alone # cannot tell the two providers apart. USE_PUBLISHED_PROVIDER = os.environ.get("KEPLER_USE_PUBLISHED_NAJAEDA") == "1" -PROVIDER_REQUIREMENT = "najaeda==0.7.24" if USE_PUBLISHED_PROVIDER else "najaeda==0.7.26" +PROVIDER_REQUIREMENT = "najaeda==0.7.24" if USE_PUBLISHED_PROVIDER else "najaeda==0.7.27" def run(*arguments: str, env: dict[str, str] | None = None) -> None: @@ -135,7 +135,7 @@ def repair_external(wheel: Path, destination: Path, dependencies: dict[str, Path if dependencies: command += ["--exclude", os.pathsep.join(dependencies)] else: - # Keep the provider's SDK import-library DLL names stable. + # Keep the DLL names matching the provider's shipped import libraries. command += ["--no-mangle", "naja_*.dll;libnaja_*.dll"] run(*command, str(wheel)) else: diff --git a/docs/python-api.md b/docs/python-api.md index 3e5cdc80..bdfddb44 100644 --- a/docs/python-api.md +++ b/docs/python-api.md @@ -17,8 +17,9 @@ For local regression without wheels or publishing, use the [source regression runner](python-regression.md). It compiles both Python packages from this checkout and tests their shared runtime. -The default development build uses the matching NajaEDA shared-runtime SDK, -version `0.7.26` in `thirdparty/naja`. Build both packages from this +The default development build links the NajaEDA wheel built from +`thirdparty/naja` (version `0.7.27`), which ships the headers matching its +libraries under `najaeda/sdk/include`. Build both packages from this recursive checkout in one virtual environment, with the native build dependencies installed: @@ -31,14 +32,13 @@ python -m pip install --no-build-isolation . Default wheel CI runs on relevant pull requests, pushes to `main`, `v*` tags, and manual runs. It builds and installs a separate local provider wheel for every Python/platform combination. Only a manual `publish` request adds a second, -parallel set of jobs against published NajaEDA `0.7.24` wheels through KF's -version-specific compatibility adapter. Only published-provider jobs must +parallel set of jobs against published NajaEDA `0.7.24` wheels, which ship no +headers; `KEPLER_USE_PUBLISHED_NAJAEDA` takes them from that release's verified +source archive instead. Only published-provider jobs must pass for publication; development-provider jobs remain independent regression checks. Only wheels tested against the published provider are uploaded. -The adapter obtains matching release headers, links the installed native -libraries, and checks their identity before sharing designs. Those wheels -require `najaeda==0.7.24`, which pip installs normally. There is no separate -provider checkbox; see [release instructions](python-release.md). +Those wheels require `najaeda==0.7.24`, which pip installs normally. There is +no separate provider checkbox; see [release instructions](python-release.md). `BUILD_KEPLER_PYTHON=ON` is a Python-only CMake build. Build the standalone executable separately with `BUILD_KEPLER_PYTHON=OFF`; it continues to use the @@ -66,10 +66,12 @@ Maintainers can publish tested wheels using the manual ## Shared NajaEDA runtime `najaeda` is a runtime dependency of `kepler_formal` and is imported before -Kepler's native extension. Development builds use its versioned native API to -check build and runtime identity. The published-provider adapter instead checks -the pinned release's native-file fingerprints, exported Python types, and live -universe identity. Both paths reject mismatches before accepting live designs. +Kepler's native extension. The extension links the installed package's own +`libnaja_*` libraries and records their version, git hash and file +fingerprints at build time. At import it checks those, the exported Python +types, and the live universe identity, and rejects any mismatch before +accepting live designs. The same checks apply to development and published +providers. For compatibility, `kepler_formal.najaeda` and all of its submodules are aliases to the original package: diff --git a/docs/python-regression.md b/docs/python-regression.md index 17338543..6898bad3 100644 --- a/docs/python-regression.md +++ b/docs/python-regression.md @@ -1,7 +1,8 @@ # Python regression from source The regression builds NajaEDA from the pinned `thirdparty/naja` submodule, -then builds Kepler's Python extension against that NajaEDA SDK. Both packages +then builds Kepler's Python extension against that NajaEDA's installed +libraries and headers. Both packages are installed with CMake into a private directory. No wheels, package index, or publishing are involved. diff --git a/docs/python-release.md b/docs/python-release.md index 51b2af33..39936d9c 100644 --- a/docs/python-release.md +++ b/docs/python-release.md @@ -56,8 +56,8 @@ and [GitHub environment protection documentation](https://docs.github.com/en/act After the workflow is present on the repository's default branch, open **Actions → Python wheels → Run workflow**. Leave `publish` unchecked and -`version` empty. These jobs use locally built NajaEDA `0.7.26` from the -pinned submodule and its shared-runtime SDK. The workflow builds, repairs, +`version` empty. These jobs use locally built NajaEDA `0.7.27` from the +pinned submodule, whose wheel ships its headers. The workflow builds, repairs, and tests wheels, then stores them as Actions artifacts. Use this to check a branch before merging. @@ -86,9 +86,10 @@ repository defaults and development jobs stay on the development provider with the option off. Build and runtime pins must match, so installations of a published-provider Kepler wheel select the same NajaEDA release. -Published NajaEDA does not supply the development shared-runtime SDK. This -compatibility path is deliberately pinned to `0.7.24` and uses released native -symbols, including the private DNL cache integration. It is not a general ABI +Published NajaEDA `0.7.24` ships no headers, so this path takes them from the +release's verified source archive and is deliberately pinned to that version. +Both providers are linked the same way, through released native symbols +including the private DNL cache integration. This is not a general ABI guarantee for arbitrary NajaEDA versions; any provider upgrade requires a new compatibility review and the complete wheel tests. It does not change NajaEDA or bundle a second Naja runtime. diff --git a/pyproject.toml b/pyproject.toml index 135f0a79..51294f88 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -2,7 +2,7 @@ # SPDX-License-Identifier: Apache-2.0 [build-system] -requires = ["scikit-build-core>=0.11.3,<0.12", "najaeda==0.7.26"] +requires = ["scikit-build-core>=0.11.3,<0.12", "najaeda==0.7.27"] build-backend = "scikit_build_core.build" [project] @@ -11,7 +11,7 @@ description = "Native Python interface for Kepler Formal equivalence checking" authors = [{name = "keplertech.io", email = "contact@keplertech.io"}] readme = "src/python/README.rst" requires-python = ">=3.10" -dependencies = ["najaeda==0.7.26"] +dependencies = ["najaeda==0.7.27"] license = {file = "LICENSE.rst"} dynamic = ["version"] classifiers = [ diff --git a/regress/run_python_regress.py b/regress/run_python_regress.py index 935c1fa1..9803287b 100644 --- a/regress/run_python_regress.py +++ b/regress/run_python_regress.py @@ -43,7 +43,7 @@ def main(): stage = build / "packages" environment = build / "venv" # Keep system and user Python packages out of the test environment. Both - # projects use this exact interpreter, compiler configuration, and SDK. + # projects use this exact interpreter, compiler configuration, and headers. venv.EnvBuilder(with_pip=False).create(environment) python = environment / ("Scripts/python.exe" if os.name == "nt" else "bin/python") env = dict(os.environ, PYTHONPATH=str(stage), PYTHONNOUSERSITE="1", @@ -74,7 +74,7 @@ def run(*command): f"-DCMAKE_INSTALL_PREFIX={stage}", ] try: - # Fail early rather than reaching the SDK-selection regression + # Fail early rather than reaching the provider-selection regression # after compiling with an older CMake. version_check = build / "check_cmake.cmake" version_check.write_text("cmake_minimum_required(VERSION 3.30)\n") @@ -91,10 +91,10 @@ def run(*command): import sys from pathlib import Path import najaeda -from najaeda import sdk stage = Path(sys.argv[1]).resolve() -assert Path(najaeda.__file__).resolve().is_relative_to(stage), najaeda.__file__ -assert Path(sdk.get_cmake_dir()).resolve().is_relative_to(stage), sdk.get_cmake_dir() +root = Path(najaeda.__file__).resolve().parent +assert root.is_relative_to(stage), najaeda.__file__ +assert (root / 'sdk/include/naja/core/NajaVersion.h').is_file(), 'NajaEDA ships no headers' print('Source-built NajaEDA:', najaeda.__file__) """, stage) @@ -104,11 +104,6 @@ def run(*command): run("cmake", "--build", consumer, "--target", "kepler_formal_native", "kepler-borrowed-native-tests", "--parallel", args.jobs) run("cmake", "--install", consumer, "--component", "python") - if sys.platform == "darwin": - # The SDK signs the build artifact. CMake then adjusts its - # install RPATH, invalidating that signature on Apple Silicon. - for extension in (stage / "kepler_formal").glob("_native*.so"): - run("codesign", "--force", "--sign", "-", extension) run(python, "-c", """ import sys from pathlib import Path diff --git a/src/python/CMakeLists.txt b/src/python/CMakeLists.txt index de189dc5..65a9abaf 100644 --- a/src/python/CMakeLists.txt +++ b/src/python/CMakeLists.txt @@ -16,13 +16,7 @@ add_library(kepler_borrowed_designs STATIC KeplerBorrowedDesigns.cpp KeplerNajaS target_include_directories(kepler_borrowed_designs PUBLIC ${CMAKE_CURRENT_SOURCE_DIR}) target_link_libraries(kepler_borrowed_designs PUBLIC kepler_verification_support) -if(KEPLER_USE_PUBLISHED_NAJAEDA) - set(kepler_runtime_source KeplerPublishedNajaRuntime.cpp) - target_compile_definitions(kepler_borrowed_designs PUBLIC KEPLER_USE_PUBLISHED_NAJAEDA=1) -else() - set(kepler_runtime_source KeplerNajaRuntime.cpp) -endif() -Python3_add_library(kepler_formal_native MODULE WITH_SOABI PyKeplerFormal.cpp ${kepler_runtime_source}) +Python3_add_library(kepler_formal_native MODULE WITH_SOABI PyKeplerFormal.cpp KeplerNajaRuntime.cpp) set_target_properties(kepler_formal_native PROPERTIES OUTPUT_NAME _native CXX_VISIBILITY_PRESET hidden @@ -32,6 +26,9 @@ target_compile_definitions(kepler_formal_native PRIVATE KEPLER_FORMAL_VERSION="${PROJECT_VERSION}" KEPLER_FORMAL_GIT_HASH="${KEPLER_FORMAL_GIT_HASH}" ) +if(KEPLER_USE_PUBLISHED_NAJAEDA) + target_compile_definitions(kepler_formal_native PRIVATE KEPLER_USE_PUBLISHED_NAJAEDA=1) +endif() target_include_directories(kepler_formal_native PRIVATE ${PROJECT_SOURCE_DIR}/src/bin) target_link_libraries(kepler_formal_native PRIVATE kepler_borrowed_designs @@ -55,6 +52,15 @@ install(TARGETS PUBLIC_HEADER DESTINATION kepler_formal/include COMPONENT python-headers ) +if(APPLE) + # The provider fixup ad-hoc signs the module after linking. Installing + # rewrites its RPATH, which invalidates that signature, and Apple Silicon + # then kills the importing process. Sign the installed copy again. + install(CODE "execute_process(COMMAND codesign --force --sign - + \"\${CMAKE_INSTALL_PREFIX}/kepler_formal/$\" + COMMAND_ERROR_IS_FATAL ANY)" + COMPONENT python) +endif() install( DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/kepler_formal diff --git a/src/python/KeplerNajaRuntime.cpp b/src/python/KeplerNajaRuntime.cpp index 0a2c082f..ea18bb98 100644 --- a/src/python/KeplerNajaRuntime.cpp +++ b/src/python/KeplerNajaRuntime.cpp @@ -3,56 +3,120 @@ #include "KeplerNajaRuntime.h" -#include +#include -#include "NajaPythonRuntimeAPI.h" -#include "NajaRuntimeBuild.h" +#include "KeplerNajaProviderBuild.h" #include "NLUniverse.h" +#include "PyNLUniverse.h" +#include "PySNLDesign.h" namespace KEPLER_FORMAL { namespace { -const NajaPythonRuntimeAPI* getRuntimeAPI(PyObject* errorType) { - const auto* api = NajaPythonRuntime_Import(); - if (api == nullptr) { - return nullptr; +struct PyObjectDeleter { + void operator()(PyObject* object) const { Py_XDECREF(object); } +}; +using OwnedPyObject = std::unique_ptr; + +bool validateProviderBuild() { + // The GIL serializes this check. Each process checks the provider's bytes + // once; subsequent calls still validate the live types and universe below. + static bool validated = false; + if (validated) { + return true; } - if (api->build_id == nullptr || api->runtime_identity == nullptr || - api->get_universe == nullptr || api->unwrap_design == nullptr) { - PyErr_SetString(errorType, "Incomplete NajaEDA native runtime API"); - return nullptr; + OwnedPyObject helper(PyImport_ImportModule("kepler_formal._provider_check")); + if (helper == nullptr) { + return false; + } + OwnedPyObject result(PyObject_CallMethod( + helper.get(), "validate_provider", "sss", KEPLER_NAJA_PROVIDER_MANIFEST, + KEPLER_NAJA_PROVIDER_VERSION, KEPLER_NAJA_PROVIDER_GIT_HASH)); + if (result == nullptr) { + return false; } - if (std::strcmp(api->build_id, NAJA_RUNTIME_BUILD_ID) != 0) { + validated = true; + return true; +} + +bool requireIdentityString(PyObject* module, const char* method, + const char* expected, PyObject* errorType) { + OwnedPyObject value(PyObject_CallMethod(module, method, nullptr)); + if (value == nullptr) { + return false; + } + if (!PyUnicode_Check(value.get()) || + PyUnicode_CompareWithASCIIString(value.get(), expected) != 0) { PyErr_Format(errorType, - "NajaEDA native build mismatch: provider %.80s, Kepler %.80s", - api->build_id, NAJA_RUNTIME_BUILD_ID); - return nullptr; + "Kepler Formal was built against NajaEDA with %s() = %s", + method, expected); + return false; + } + return true; +} + +} // namespace + +bool validateNajaRuntime(PyObject* errorType) { + OwnedPyObject module(PyImport_ImportModule("najaeda.naja")); + if (module == nullptr || + !requireIdentityString(module.get(), "getVersion", + KEPLER_NAJA_PROVIDER_VERSION, errorType) || + !requireIdentityString(module.get(), "getGitHash", + KEPLER_NAJA_PROVIDER_GIT_HASH, errorType) || + !validateProviderBuild()) { + return false; + } + + OwnedPyObject designType(PyObject_GetAttrString(module.get(), "SNLDesign")); + OwnedPyObject universeType(PyObject_GetAttrString(module.get(), "NLUniverse")); + if (designType == nullptr || universeType == nullptr) { + return false; } - if (api->runtime_identity != naja::NL::NLUniverse::getRuntimeIdentity()) { + // Compare live exported objects: the type objects Python sees must be the + // ones this extension linked, or two Naja copies are loaded. + if (designType.get() != reinterpret_cast(&PYNAJA::PyTypeSNLDesign) || + universeType.get() != reinterpret_cast(&PYNAJA::PyTypeNLUniverse)) { PyErr_SetString( errorType, "NajaEDA and Kepler Formal did not load the same native runtime"); - return nullptr; + return false; + } + OwnedPyObject pythonUniverse( + PyObject_CallMethod(universeType.get(), "get", nullptr)); + if (pythonUniverse == nullptr) { + return false; } - if (api->get_universe() != naja::NL::NLUniverse::get()) { + OwnedPyObject linkedUniverse( + PYNAJA::PyNLUniverse_Link(naja::NL::NLUniverse::get())); + if (linkedUniverse == nullptr) { + return false; + } + if (pythonUniverse.get() != linkedUniverse.get()) { PyErr_SetString(errorType, "NajaEDA and Kepler Formal disagree on the active universe"); - return nullptr; + return false; } - return api; -} - -} // namespace - -bool validateNajaRuntime(PyObject* errorType) { - return getRuntimeAPI(errorType) != nullptr; + return true; } naja::NL::SNLDesign* unwrapNajaDesign(PyObject* object) { - const auto* api = getRuntimeAPI(PyExc_RuntimeError); - return api == nullptr - ? nullptr - : static_cast(api->unwrap_design(object)); + if (!validateNajaRuntime(PyExc_RuntimeError)) { + return nullptr; + } + if (object == nullptr || !PyObject_TypeCheck(object, &PYNAJA::PyTypeSNLDesign)) { + PyErr_SetString(PyExc_TypeError, + "Expected an SNLDesign from this NajaEDA runtime"); + return nullptr; + } + // Naja clears the wrapper's native pointer when the design, its library, + // database or universe is destroyed. + auto* design = reinterpret_cast(object)->object_; + if (design == nullptr) { + PyErr_SetString(PyExc_ReferenceError, "The NajaEDA design was destroyed"); + return nullptr; + } + return design; } } // namespace KEPLER_FORMAL diff --git a/src/python/KeplerNajaState.cpp b/src/python/KeplerNajaState.cpp index a9836bc4..ce7c0e1c 100644 --- a/src/python/KeplerNajaState.cpp +++ b/src/python/KeplerNajaState.cpp @@ -3,28 +3,22 @@ #include "KeplerNajaState.h" -#ifdef KEPLER_USE_PUBLISHED_NAJAEDA namespace naja::DNL { -// NajaEDA 0.7.24 exports this storage but has no public exchange function. -// This version-specific bridge is enabled only with the published adapter. +// NajaEDA exports this storage but has no public exchange function. The +// provider identity checks guarantee the linked build owns this symbol. #ifdef _WIN32 __declspec(dllimport) extern DNLFull* dnlFull_; #else extern DNLFull* dnlFull_; #endif } // namespace naja::DNL -#endif namespace KEPLER_FORMAL { naja::DNL::DNLFull* exchangeNajaDNL(naja::DNL::DNLFull* replacement) noexcept { -#ifdef KEPLER_USE_PUBLISHED_NAJAEDA auto* previous = naja::DNL::dnlFull_; naja::DNL::dnlFull_ = replacement; return previous; -#else - return naja::DNL::exchange(replacement); -#endif } } // namespace KEPLER_FORMAL diff --git a/src/python/KeplerPublishedNaja.cmake b/src/python/KeplerPublishedNaja.cmake deleted file mode 100644 index 61346e77..00000000 --- a/src/python/KeplerPublishedNaja.cmake +++ /dev/null @@ -1,78 +0,0 @@ -# Copyright 2026 keplertech.io -# SPDX-License-Identifier: GPL-3.0-only - -# Opt-in compatibility for the unmodified, published NajaEDA 0.7.24 wheels. -# Only headers are obtained from its verified source archive; all runtime -# targets below point to the libraries owned by the installed Python package. -set(KEPLER_NAJAEDA_SOURCE_ARCHIVE "" CACHE FILEPATH "Optional cached NajaEDA 0.7.24 source archive") -set(published_naja_args --cmake --output-dir "${CMAKE_BINARY_DIR}/published-najaeda") -if(KEPLER_NAJAEDA_SOURCE_ARCHIVE) - list(APPEND published_naja_args --source-archive "${KEPLER_NAJAEDA_SOURCE_ARCHIVE}") -endif() -execute_process( - COMMAND "${Python3_EXECUTABLE}" "${CMAKE_CURRENT_LIST_DIR}/published_najaeda.py" ${published_naja_args} - RESULT_VARIABLE provider_status - OUTPUT_VARIABLE provider_config - ERROR_VARIABLE provider_error -) -if(NOT provider_status EQUAL 0) - message(FATAL_ERROR "Cannot use published NajaEDA: ${provider_error}") -endif() -set(provider_config_file "${CMAKE_BINARY_DIR}/published-najaeda/provider.cmake") -file(WRITE "${provider_config_file}" "${provider_config}") -include("${provider_config_file}") -find_package(TBB REQUIRED) -find_path(NajaEDA_BOOST_INCLUDE_DIR boost/intrusive/set.hpp REQUIRED) - -foreach(dependency IN ITEMS tbb tbbmalloc) - if(DEFINED NajaEDA_${dependency}_LIBRARY) - get_filename_component(provider_name "${NajaEDA_${dependency}_LIBRARY}" NAME) - foreach(suffix IN ITEMS "" _RELEASE _DEBUG _RELWITHDEBINFO _MINSIZEREL) - set_property(TARGET TBB::${dependency} PROPERTY IMPORTED_LOCATION${suffix} "${NajaEDA_${dependency}_LIBRARY}") - set_property(TARGET TBB::${dependency} PROPERTY IMPORTED_SONAME${suffix} "${provider_name}") - if(WIN32) - set_property(TARGET TBB::${dependency} PROPERTY IMPORTED_IMPLIB${suffix} "${NajaEDA_${dependency}_IMPLIB}") - endif() - endforeach() - endif() -endforeach() - -foreach(runtime IN ITEMS naja_nl naja_dnl naja_bne naja_opt naja_metrics naja_python) - if(TARGET ${runtime}) - message(FATAL_ERROR "Published NajaEDA cannot share an existing ${runtime} target") - endif() - add_library(${runtime} SHARED IMPORTED GLOBAL) - set_target_properties(${runtime} PROPERTIES - IMPORTED_LOCATION "${NajaEDA_${runtime}_LIBRARY}" - SYSTEM FALSE - IMPORTED_NO_SYSTEM TRUE - INTERFACE_INCLUDE_DIRECTORIES "${NajaEDA_INCLUDE_DIRS};${NajaEDA_BOOST_INCLUDE_DIR}" - INTERFACE_SYSTEM_INCLUDE_DIRECTORIES "${NajaEDA_BOOST_INCLUDE_DIR}" - INTERFACE_COMPILE_FEATURES cxx_std_20) - if(WIN32) - set_property(TARGET ${runtime} PROPERTY IMPORTED_IMPLIB "${NajaEDA_${runtime}_IMPLIB}") - endif() -endforeach() -target_link_libraries(naja_dnl INTERFACE naja_nl TBB::tbb TBB::tbbmalloc) -target_link_libraries(naja_bne INTERFACE naja_nl naja_dnl) -target_link_libraries(naja_opt INTERFACE naja_nl naja_dnl naja_bne) -target_link_libraries(naja_metrics INTERFACE naja_nl naja_dnl) -target_link_libraries(naja_python INTERFACE naja_nl naja_dnl naja_bne naja_opt naja_metrics Python3::Module) -foreach(component IN ITEMS naja_core naja_nl_dump naja_snl_liberty naja_snl_systemverilog naja_snl_verilog naja_snl_visual) - add_library(${component} INTERFACE IMPORTED GLOBAL) - if(component STREQUAL "naja_core") - target_link_libraries(${component} INTERFACE naja_nl) - else() - target_link_libraries(${component} INTERFACE naja_python) - endif() -endforeach() - -function(najaeda_fixup_consumer target) - if(APPLE) - set(helper "${CMAKE_CURRENT_FUNCTION_LIST_DIR}/published_najaeda.py") - set_property(TARGET "${target}" APPEND PROPERTY LINK_DEPENDS "${helper}") - add_custom_command(TARGET "${target}" POST_BUILD - COMMAND "${Python3_EXECUTABLE}" "${helper}" --fixup-consumer "$" - VERBATIM) - endif() -endfunction() diff --git a/src/python/KeplerPublishedNajaRuntime.cpp b/src/python/KeplerPublishedNajaRuntime.cpp deleted file mode 100644 index d1b0b0f3..00000000 --- a/src/python/KeplerPublishedNajaRuntime.cpp +++ /dev/null @@ -1,186 +0,0 @@ -// Copyright 2026 keplertech.io -// SPDX-License-Identifier: Apache-2.0 - -#include "KeplerNajaRuntime.h" - -#include -#include - -#include "KeplerPublishedNajaBuild.h" -#include "NLID.h" -#include "NLUniverse.h" -#include "PyNLUniverse.h" -#include "PySNLDesign.h" - -namespace KEPLER_FORMAL { -namespace { - -struct PyObjectDeleter { - void operator()(PyObject* object) const { Py_XDECREF(object); } -}; -using OwnedPyObject = std::unique_ptr; - -bool validateProviderBuild() { - // The GIL serializes this check. Each process checks the provider's bytes - // once; subsequent calls still validate the live types and universe below. - static bool validated = false; - if (validated) { - return true; - } - OwnedPyObject helper(PyImport_ImportModule("kepler_formal._published_runtime")); - if (helper == nullptr) { - return false; - } - OwnedPyObject result(PyObject_CallMethod( - helper.get(), "validate_provider", "s", KEPLER_NAJA_PROVIDER_MANIFEST)); - if (result == nullptr) { - return false; - } - validated = true; - return true; -} - -bool requireIdentityString(PyObject* module, const char* method, - const char* expected, PyObject* errorType) { - OwnedPyObject value(PyObject_CallMethod(module, method, nullptr)); - if (value == nullptr) { - return false; - } - if (!PyUnicode_Check(value.get()) || - PyUnicode_CompareWithASCIIString(value.get(), expected) != 0) { - PyErr_Format(errorType, - "Kepler Formal's published NajaEDA adapter requires %s() = %s", - method, expected); - return false; - } - return true; -} - -template -bool readID(PyObject* identifier, const char* method, ID& result) { - OwnedPyObject value(PyObject_CallMethod(identifier, method, nullptr)); - if (value == nullptr) { - return false; - } - if (!PyLong_Check(value.get()) || PyBool_Check(value.get())) { - PyErr_SetString(PyExc_TypeError, "NajaEDA design IDs must be integers"); - return false; - } - const auto number = PyLong_AsUnsignedLongLong(value.get()); - if (PyErr_Occurred()) { - return false; - } - if (number > std::numeric_limits::max()) { - PyErr_SetString(PyExc_OverflowError, "NajaEDA design ID is out of range"); - return false; - } - result = static_cast(number); - return true; -} - -} // namespace - -bool validateNajaRuntime(PyObject* errorType) { - OwnedPyObject module(PyImport_ImportModule("najaeda.naja")); - if (module == nullptr || - !requireIdentityString(module.get(), "getVersion", "0.7.24", errorType) || - !requireIdentityString(module.get(), "getGitHash", "2263958", errorType) || - !validateProviderBuild()) { - return false; - } - - // This adapter targets the published pre-SDK runtime exclusively. A capsule - // belongs to another contract and must not silently override these checks. - OwnedPyObject capsule(PyObject_GetAttrString(module.get(), "_C_API")); - if (capsule != nullptr) { - PyErr_SetString(errorType, - "Incompatible NajaEDA native runtime API for the published adapter"); - return false; - } - if (!PyErr_ExceptionMatches(PyExc_AttributeError)) { - return false; - } - PyErr_Clear(); - - OwnedPyObject designType(PyObject_GetAttrString(module.get(), "SNLDesign")); - OwnedPyObject universeType(PyObject_GetAttrString(module.get(), "NLUniverse")); - if (designType == nullptr || universeType == nullptr) { - return false; - } - // Compare live exported objects, not type names or Python wrapper layouts. - if (designType.get() != reinterpret_cast(&PYNAJA::PyTypeSNLDesign) || - universeType.get() != reinterpret_cast(&PYNAJA::PyTypeNLUniverse)) { - PyErr_SetString( - errorType, - "NajaEDA and Kepler Formal did not load the same native runtime"); - return false; - } - OwnedPyObject pythonUniverse( - PyObject_CallMethod(universeType.get(), "get", nullptr)); - if (pythonUniverse == nullptr) { - return false; - } - OwnedPyObject linkedUniverse( - PYNAJA::PyNLUniverse_Link(naja::NL::NLUniverse::get())); - if (linkedUniverse == nullptr) { - return false; - } - if (pythonUniverse.get() != linkedUniverse.get()) { - PyErr_SetString(errorType, - "NajaEDA and Kepler Formal disagree on the active universe"); - return false; - } - return true; -} - -naja::NL::SNLDesign* unwrapNajaDesign(PyObject* object) { - if (!validateNajaRuntime(PyExc_RuntimeError)) { - return nullptr; - } - if (object == nullptr || !PyObject_TypeCheck(object, &PYNAJA::PyTypeSNLDesign)) { - PyErr_SetString(PyExc_TypeError, - "Expected an SNLDesign from this NajaEDA runtime"); - return nullptr; - } - - // Ask the retained owner on every call. Its getter rejects destruction even - // when a replacement design has already reused the same numerical IDs. - OwnedPyObject identifier(PyObject_CallMethod(object, "getNLID", nullptr)); - if (identifier == nullptr) { - if (PyErr_ExceptionMatches(PyExc_RuntimeError)) { - PyErr_Clear(); - PyErr_SetString(PyExc_ReferenceError, "The NajaEDA design was destroyed"); - } - return nullptr; - } - naja::NL::NLID::DBID dbID; - naja::NL::NLID::LibraryID libraryID; - naja::NL::NLID::DesignID designID; - if (!readID(identifier.get(), "getDBID", dbID) || - !readID(identifier.get(), "getLibraryID", libraryID) || - !readID(identifier.get(), "getDesignID", designID)) { - return nullptr; - } - const auto* universe = naja::NL::NLUniverse::get(); - auto* design = universe == nullptr - ? nullptr - : universe->getSNLDesign( - naja::NL::NLID::DesignReference(dbID, libraryID, designID)); - if (design == nullptr) { - PyErr_SetString(PyExc_ReferenceError, - "The NajaEDA design is not in the active universe"); - return nullptr; - } - OwnedPyObject linkedDesign(PYNAJA::PySNLDesign_Link(design)); - if (linkedDesign == nullptr) { - return nullptr; - } - if (linkedDesign.get() != object) { - PyErr_SetString(PyExc_ReferenceError, - "The NajaEDA design no longer matches its native object"); - return nullptr; - } - return design; -} - -} // namespace KEPLER_FORMAL diff --git a/src/python/KeplerSharedNaja.cmake b/src/python/KeplerSharedNaja.cmake index d7677609..a8630f02 100644 --- a/src/python/KeplerSharedNaja.cmake +++ b/src/python/KeplerSharedNaja.cmake @@ -1,37 +1,38 @@ # Copyright 2026 keplertech.io # SPDX-License-Identifier: GPL-3.0-only +# A Python build links the NajaEDA runtime installed in the build interpreter +# instead of compiling the vendored Naja. The default provider is a wheel built +# from thirdparty/naja, which ships its headers. KEPLER_USE_PUBLISHED_NAJAEDA +# selects the unmodified 0.7.24 release; its headers come from the verified +# source archive. Every runtime target below points to the installed package's +# own libraries; this build never modifies the provider. +set(KEPLER_NAJAEDA_SOURCE_ARCHIVE "" CACHE FILEPATH "Optional cached NajaEDA 0.7.24 source archive") +set(naja_provider_args --cmake --output-dir "${CMAKE_BINARY_DIR}/naja-provider") if(KEPLER_USE_PUBLISHED_NAJAEDA) - include("${CMAKE_CURRENT_LIST_DIR}/KeplerPublishedNaja.cmake") -else() -# Use the SDK belonging to this interpreter's installed provider. A CMake -# override alone must not select a different runtime than Python will import. + list(APPEND naja_provider_args --published) + if(KEPLER_NAJAEDA_SOURCE_ARCHIVE) + list(APPEND naja_provider_args --source-archive "${KEPLER_NAJAEDA_SOURCE_ARCHIVE}") + endif() +endif() +# Ask the interpreter itself: a CMake override alone must not select a +# different runtime than Python will import. execute_process( - COMMAND "${Python3_EXECUTABLE}" -c - "from najaeda import sdk; print(sdk.get_cmake_dir())" + COMMAND "${Python3_EXECUTABLE}" "${CMAKE_CURRENT_LIST_DIR}/naja_provider.py" ${naja_provider_args} RESULT_VARIABLE provider_status - OUTPUT_VARIABLE provider_cmake_dir + OUTPUT_VARIABLE provider_config ERROR_VARIABLE provider_error - OUTPUT_STRIP_TRAILING_WHITESPACE ) -# Package-manager wrappers can expand find_package arguments a second time. -# Normalize native Windows separators before a path such as C:\Users reaches -# vcpkg's macro, where the backslash would otherwise introduce an escape. -file(TO_CMAKE_PATH "${provider_cmake_dir}" provider_cmake_dir) -if(NOT provider_status EQUAL 0 OR NOT IS_DIRECTORY "${provider_cmake_dir}") +if(NOT provider_status EQUAL 0) message(FATAL_ERROR - "Python builds require the NajaEDA shared-runtime SDK in ${Python3_EXECUTABLE}. " - "Install the matching NajaEDA development wheel first (see docs/python-api.md).\n" - "${provider_error}") -endif() -# NO_DEFAULT_PATH does not ignore a preexisting _DIR cache entry. -# Shadow it locally so both fresh and reused builds select Python's provider. -set(NajaEDA_DIR "${provider_cmake_dir}") -find_package(NajaEDA CONFIG REQUIRED PATHS "${provider_cmake_dir}" NO_DEFAULT_PATH) + "Python builds require an installed NajaEDA provider in ${Python3_EXECUTABLE} " + "(see docs/python-api.md).\n${provider_error}") endif() +set(provider_config_file "${CMAKE_BINARY_DIR}/naja-provider/provider.cmake") +file(WRITE "${provider_config_file}" "${provider_config}") +include("${provider_config_file}") # These build-policy targets normally come from the vendored Naja project. -# Do not modify the installed provider's compilation or import another runtime. foreach(policy_target IN ITEMS coverage_config sanitizers_config) if(NOT TARGET "${policy_target}") add_library("${policy_target}" INTERFACE) @@ -49,3 +50,64 @@ if(WIN32) __TBB_NO_IMPLICIT_LINKAGE=1) endforeach() endif() + +# Keep the development package's TBB headers, but link the allocator and +# runtime bundled with the provider rather than introducing a second copy. +foreach(dependency IN ITEMS tbb tbbmalloc) + if(DEFINED NajaEDA_${dependency}_LIBRARY) + get_filename_component(provider_name "${NajaEDA_${dependency}_LIBRARY}" NAME) + foreach(suffix IN ITEMS "" _RELEASE _DEBUG _RELWITHDEBINFO _MINSIZEREL) + set_property(TARGET TBB::${dependency} PROPERTY IMPORTED_LOCATION${suffix} "${NajaEDA_${dependency}_LIBRARY}") + set_property(TARGET TBB::${dependency} PROPERTY IMPORTED_SONAME${suffix} "${provider_name}") + if(WIN32) + set_property(TARGET TBB::${dependency} PROPERTY IMPORTED_IMPLIB${suffix} "${NajaEDA_${dependency}_IMPLIB}") + endif() + endforeach() + endif() +endforeach() + +foreach(runtime IN ITEMS naja_nl naja_dnl naja_bne naja_opt naja_metrics naja_python) + if(TARGET ${runtime}) + message(FATAL_ERROR "The NajaEDA provider cannot share an existing ${runtime} target") + endif() + add_library(${runtime} SHARED IMPORTED GLOBAL) + set_target_properties(${runtime} PROPERTIES + IMPORTED_LOCATION "${NajaEDA_${runtime}_LIBRARY}" + # The provider's headers must precede any older Naja headers on CPATH, so + # they keep ordinary -I precedence instead of -isystem. + SYSTEM FALSE + IMPORTED_NO_SYSTEM TRUE + INTERFACE_INCLUDE_DIRECTORIES "${NajaEDA_INCLUDE_DIRS};${Boost_INCLUDE_DIR}" + INTERFACE_SYSTEM_INCLUDE_DIRECTORIES "${Boost_INCLUDE_DIR}" + INTERFACE_COMPILE_FEATURES cxx_std_20) + if(WIN32) + set_property(TARGET ${runtime} PROPERTY IMPORTED_IMPLIB "${NajaEDA_${runtime}_IMPLIB}") + endif() +endforeach() +target_link_libraries(naja_dnl INTERFACE naja_nl TBB::tbb TBB::tbbmalloc) +target_link_libraries(naja_bne INTERFACE naja_nl naja_dnl) +target_link_libraries(naja_opt INTERFACE naja_nl naja_dnl naja_bne) +target_link_libraries(naja_metrics INTERFACE naja_nl naja_dnl) +target_link_libraries(naja_python INTERFACE naja_nl naja_dnl naja_bne naja_opt naja_metrics Python3::Module) +# The vendored build's static components live inside the provider's shared +# libraries: naja_core in naja_nl, the format and dump components in naja_python. +foreach(component IN ITEMS naja_core naja_nl_dump naja_snl_liberty naja_snl_systemverilog naja_snl_verilog naja_snl_visual) + add_library(${component} INTERFACE IMPORTED GLOBAL) + if(component STREQUAL "naja_core") + target_link_libraries(${component} INTERFACE naja_nl) + else() + target_link_libraries(${component} INTERFACE naja_python) + endif() +endforeach() + +# Repair-renamed Mach-O install IDs need an explicit post-link relocation in +# build trees. Call this from the directory that owns the consumer target. +function(najaeda_fixup_consumer target) + if(APPLE) + set(helper "${CMAKE_CURRENT_FUNCTION_LIST_DIR}/naja_provider.py") + set_property(TARGET "${target}" APPEND PROPERTY LINK_DEPENDS "${helper}") + add_custom_command(TARGET "${target}" POST_BUILD + COMMAND "${Python3_EXECUTABLE}" "${helper}" --fixup-consumer "$" + VERBATIM) + endif() +endfunction() diff --git a/src/python/PyKeplerFormal.cpp b/src/python/PyKeplerFormal.cpp index 18d6a9e2..13ee3e91 100644 --- a/src/python/PyKeplerFormal.cpp +++ b/src/python/PyKeplerFormal.cpp @@ -594,7 +594,7 @@ PyMODINIT_FUNC PyInit__native() { #ifdef KEPLER_USE_PUBLISHED_NAJAEDA constexpr const char* providerMode = "published"; #else - constexpr const char* providerMode = "sdk"; + constexpr const char* providerMode = "development"; #endif if (PyModule_AddStringConstant(result.get(), "_provider_mode", providerMode) < 0) { nativeDesignType = nullptr; diff --git a/src/python/kepler_formal/_published_runtime.py b/src/python/kepler_formal/_provider_check.py similarity index 67% rename from src/python/kepler_formal/_published_runtime.py rename to src/python/kepler_formal/_provider_check.py index 9b692851..ae768c1f 100644 --- a/src/python/kepler_formal/_published_runtime.py +++ b/src/python/kepler_formal/_provider_check.py @@ -1,6 +1,6 @@ # Copyright 2026 keplertech.io # SPDX-License-Identifier: Apache-2.0 -"""Fail closed when an opt-in published-provider build loads another runtime.""" +"""Fail closed when Kepler's native extension loads another NajaEDA runtime.""" from __future__ import annotations from functools import lru_cache @@ -12,10 +12,10 @@ @lru_cache(maxsize=4) -def validate_provider(manifest_json: str) -> None: +def validate_provider(manifest_json: str, version: str, git_hash: str) -> None: """Validate the exact provider binaries used to compile this extension. - Python package versions alone do not identify a C++ ABI. The adapter is + Python package versions alone do not identify a C++ ABI. The extension is compiled for a particular wheel's native files; their hashes travel with Kepler's extension. Successful validation is cached for this process. """ @@ -23,12 +23,19 @@ def validate_provider(manifest_json: str) -> None: from najaeda import naja try: - version = importlib.metadata.version("najaeda") - if version != "0.7.24" or naja.getGitHash() != "2263958": - raise ImportError("Kepler's published-provider adapter requires NajaEDA 0.7.24 (2263958)") + try: + distribution = importlib.metadata.distribution("najaeda") + except importlib.metadata.PackageNotFoundError: + # A plain CMake install, as in the source regression, has no metadata. + distribution = None + installed_version = naja.getVersion() if distribution is None else distribution.version + if installed_version != version or naja.getGitHash() != git_hash: + raise ImportError( + f"Kepler Formal was built against NajaEDA {version} ({git_hash}); " + f"found {installed_version} ({naja.getGitHash()})") root = Path(najaeda.__file__).resolve().parent - distribution = importlib.metadata.distribution("najaeda") - if distribution.locate_file("najaeda/__init__.py").resolve() != root / "__init__.py": + if (distribution is not None + and distribution.locate_file("najaeda/__init__.py").resolve() != root / "__init__.py"): raise ImportError("Imported NajaEDA does not match its installed distribution") extension = Path(naja.__file__).resolve() if extension.parent != root: @@ -52,6 +59,5 @@ def validate_provider(manifest_json: str) -> None: raise ImportError( f"NajaEDA runtime differs from the wheel Kepler was built against: {relative}. " "Install matching Kepler Formal and NajaEDA wheels.") - except (AttributeError, OSError, TypeError, ValueError, - importlib.metadata.PackageNotFoundError) as error: - raise ImportError(f"Cannot validate Kepler's published NajaEDA provider: {error}") from error + except (AttributeError, OSError, TypeError, ValueError) as error: + raise ImportError(f"Cannot validate Kepler's NajaEDA provider: {error}") from error diff --git a/src/python/published_najaeda.py b/src/python/naja_provider.py similarity index 65% rename from src/python/published_najaeda.py rename to src/python/naja_provider.py index 32309ff8..a6fc6130 100644 --- a/src/python/published_najaeda.py +++ b/src/python/naja_provider.py @@ -1,10 +1,14 @@ # Copyright 2026 keplertech.io # SPDX-License-Identifier: Apache-2.0 -"""Build the opt-in Kepler adapter for the published NajaEDA 0.7.24 wheel. +"""Describe the installed NajaEDA provider to Kepler's CMake build. -Only release headers are extracted; this helper never builds or edits Naja. -PE export/import-library handling and Mach-O fixup are adapted from Naja's -Apache-2.0 licensed najaeda/sdk.py (The Naja authors). +Kepler's Python extension links the native libraries of the NajaEDA package +installed in the build interpreter. The default provider is a wheel built from +``thirdparty/naja``, which ships its headers under ``najaeda/sdk/include``. +``--published`` selects the unmodified NajaEDA 0.7.24 release instead and takes +its headers from the verified source archive. This helper never builds or +edits Naja. PE export/import-library handling and Mach-O fixup are adapted from +the former Apache-2.0 licensed najaeda/sdk.py (The Naja authors). """ from __future__ import annotations @@ -21,32 +25,64 @@ import sys import tarfile import tempfile +from typing import NamedTuple import urllib.request -VERSION = "0.7.24" -GIT_COMMIT = "2263958" -SOURCE_SHA256 = "00145fd267e50031e92637160df3b164e9da5df2f75591ce5bd3f2f786a7abc0" -SOURCE_URL = "https://files.pythonhosted.org/packages/source/n/najaeda/najaeda-0.7.24.tar.gz" +PUBLISHED_VERSION = "0.7.24" +PUBLISHED_GIT_COMMIT = "2263958" +PUBLISHED_SOURCE_SHA256 = "00145fd267e50031e92637160df3b164e9da5df2f75591ce5bd3f2f786a7abc0" +PUBLISHED_SOURCE_URL = "https://files.pythonhosted.org/packages/source/n/najaeda/najaeda-0.7.24.tar.gz" RUNTIMES = ("naja_nl", "naja_dnl", "naja_bne", "naja_opt", "naja_metrics", "naja_python") -def _provider() -> tuple[Path, Path]: +class Provider(NamedTuple): + root: Path + extension: Path + version: str + git_commit: str + + +def _provider_root() -> tuple[Path, Path, str | None]: + """Return the imported package root, its extension and distribution version.""" import najaeda from najaeda import naja - version = importlib.metadata.version("najaeda") - if version != VERSION or naja.getGitHash() != GIT_COMMIT: - raise RuntimeError( - f"Published NajaEDA adapter requires {VERSION} ({GIT_COMMIT}); " - f"found {version} ({naja.getGitHash()})") root = Path(najaeda.__file__).resolve().parent extension = Path(naja.__file__).resolve() - distribution = importlib.metadata.distribution("najaeda") - if distribution.locate_file("najaeda/__init__.py").resolve() != root / "__init__.py": + try: + distribution = importlib.metadata.distribution("najaeda") + except importlib.metadata.PackageNotFoundError: + # A plain CMake install, as in the source regression, has no metadata. + distribution = None + if (distribution is not None + and distribution.locate_file("najaeda/__init__.py").resolve() != root / "__init__.py"): raise RuntimeError("Imported NajaEDA does not match the installed distribution") if extension.parent != root: raise RuntimeError("NajaEDA imported a native extension outside its package") - return root, extension + return root, extension, None if distribution is None else distribution.version + + +def _provider(published: bool = False) -> Provider: + from najaeda import naja + + root, extension, version = _provider_root() + if version is None: + version = naja.getVersion() + git_commit = naja.getGitHash() + if published: + if version != PUBLISHED_VERSION or git_commit != PUBLISHED_GIT_COMMIT: + raise RuntimeError( + f"Published NajaEDA adapter requires {PUBLISHED_VERSION} ({PUBLISHED_GIT_COMMIT}); " + f"found {version} ({git_commit})") + elif not (root / "sdk/include/naja/core/NajaVersion.h").is_file(): + raise RuntimeError( + f"NajaEDA {version} ({git_commit}) in {root} ships no headers. Install the " + "development wheel built from thirdparty/naja, or configure with " + f"KEPLER_USE_PUBLISHED_NAJAEDA=ON for the published {PUBLISHED_VERSION} release") + if naja.getVersion() != version: + raise RuntimeError( + f"NajaEDA distribution {version} reports native version {naja.getVersion()}") + return Provider(root, extension, version, git_commit) def _provider_files(root: Path) -> tuple[Path, ...]: @@ -71,16 +107,27 @@ def _libraries(root: Path) -> dict[str, Path]: return libraries -def _headers(output_dir: Path, source_archive: Path | None) -> list[Path]: +def _wheel_headers(root: Path) -> list[Path]: + """Use the headers the development wheel installed next to its libraries.""" + include_root = root / "sdk/include" + include_dirs = {include_root} + include_dirs.update(path.parent for path in (include_root / "naja").rglob("*.h")) + if not (include_root / "naja/core/NajaVersion.h").is_file(): + raise RuntimeError("NajaEDA wheel headers contain no version header") + return sorted(include_dirs) + + +def _published_headers(output_dir: Path, source_archive: Path | None) -> list[Path]: + """Extract the published release's headers from its verified source archive.""" if source_archive is None: - source_archive = output_dir / f"najaeda-{VERSION}.tar.gz" + source_archive = output_dir / f"najaeda-{PUBLISHED_VERSION}.tar.gz" if not source_archive.is_file(): - with urllib.request.urlopen(SOURCE_URL, timeout=60) as response: + with urllib.request.urlopen(PUBLISHED_SOURCE_URL, timeout=60) as response: content = response.read() - if hashlib.sha256(content).hexdigest() != SOURCE_SHA256: + if hashlib.sha256(content).hexdigest() != PUBLISHED_SOURCE_SHA256: raise RuntimeError("Published NajaEDA source archive checksum mismatch") source_archive.write_bytes(content) - if hashlib.sha256(source_archive.read_bytes()).hexdigest() != SOURCE_SHA256: + if hashlib.sha256(source_archive.read_bytes()).hexdigest() != PUBLISHED_SOURCE_SHA256: raise RuntimeError("Published NajaEDA source archive checksum mismatch") destination = output_dir / "release-headers" include_dirs = {output_dir / "include"} @@ -89,7 +136,7 @@ def _headers(output_dir: Path, source_archive: Path | None) -> list[Path]: path = PurePosixPath(member.name) if path.is_absolute() or ".." in path.parts or "\\" in member.name: raise RuntimeError(f"Unsafe path in NajaEDA source archive: {member.name}") - if not path.parts or path.parts[0] != f"najaeda-{VERSION}": + if not path.parts or path.parts[0] != f"najaeda-{PUBLISHED_VERSION}": raise RuntimeError("Unexpected NajaEDA source archive root") relative = PurePosixPath(*path.parts[1:]) if not relative.parts: @@ -106,7 +153,7 @@ def _headers(output_dir: Path, source_archive: Path | None) -> list[Path]: target = destination.joinpath(*relative.parts) if relative.name == "NajaVersion.h.in": target = output_dir / "include" / "NajaVersion.h" - content = content.replace(b"@NAJA_GIT_HASH@", GIT_COMMIT.encode("ascii")) + content = content.replace(b"@NAJA_GIT_HASH@", PUBLISHED_GIT_COMMIT.encode("ascii")) target.parent.mkdir(parents=True, exist_ok=True) target.write_bytes(content) if is_source: @@ -122,7 +169,7 @@ def fixup_consumer(consumer: Path) -> None: """Resolve repaired Mach-O install IDs without modifying provider files.""" if sys.platform != "darwin": return - root, _ = _provider() + root, _, _ = _provider_root() consumer = consumer.resolve(strict=True) files = _provider_files(root) if consumer in files: @@ -164,7 +211,7 @@ def unpack(fmt: str, offset: int) -> tuple[int, ...]: machine, count, _, _, _, optional_size, _ = unpack(" tuple[int, int]: return exports -def _import_library(name: str, library: Path, output_dir: Path) -> Path: +def _import_library(name: str, library: Path, output_dir: Path, root: Path | None = None) -> Path: + # The development wheel ships the original import libraries. They only + # match DLLs whose names wheel repair left unchanged. + if root is not None and library.name.lower() == f"{name}.dll": + original = root / "sdk/lib" / f"{name}.lib" + if original.is_file(): + return original digest = hashlib.sha256(library.read_bytes()).hexdigest()[:20] output_dir.mkdir(parents=True, exist_ok=True) destination = output_dir / f"{name}-{digest}.lib" @@ -245,33 +298,43 @@ def _cmake_value(value: object) -> str: return f"[==[{value}]==]" -def cmake_config(output_dir: Path, source_archive: Path | None = None) -> str: - root, extension = _provider() - libraries = _libraries(root) +def cmake_config(output_dir: Path, *, published: bool = False, + source_archive: Path | None = None) -> str: + provider = _provider(published) + libraries = _libraries(provider.root) output_dir = output_dir.resolve() - output_dir.mkdir(parents=True, exist_ok=True) - include_dirs = _headers(output_dir, source_archive) + (output_dir / "include").mkdir(parents=True, exist_ok=True) + if published: + include_dirs = _published_headers(output_dir, source_archive) + else: + include_dirs = [output_dir / "include", *_wheel_headers(provider.root)] manifest = {} - for path in (*libraries.values(), extension): + for path in (*libraries.values(), provider.extension): try: - relative = path.relative_to(root.parent).as_posix() + relative = path.relative_to(provider.root.parent).as_posix() except ValueError as error: raise RuntimeError(f"Provider library is outside its installation: {path}") from error manifest[relative] = hashlib.sha256(path.read_bytes()).hexdigest() manifest_json = json.dumps(manifest, sort_keys=True, separators=(",", ":")) - (output_dir / "include" / "KeplerPublishedNajaBuild.h").write_text( - "// Generated from the installed published NajaEDA provider.\n#pragma once\n" + # The extension validates these at import: the same release and the same + # native files it was compiled against. Package versions alone do not + # identify a C++ ABI. + (output_dir / "include" / "KeplerNajaProviderBuild.h").write_text( + "// Generated from the installed NajaEDA provider.\n#pragma once\n" + f"#define KEPLER_NAJA_PROVIDER_VERSION {json.dumps(provider.version)}\n" + f"#define KEPLER_NAJA_PROVIDER_GIT_HASH {json.dumps(provider.git_commit)}\n" f"#define KEPLER_NAJA_PROVIDER_MANIFEST {json.dumps(manifest_json)}\n", encoding="utf-8") - values = {"NajaEDA_VERSION": VERSION, "NajaEDA_GIT_COMMIT": GIT_COMMIT, - "NajaEDA_BUILD_ID": "published-" + hashlib.sha256(manifest_json.encode()).hexdigest()} + values = {"NajaEDA_VERSION": provider.version, "NajaEDA_GIT_COMMIT": provider.git_commit, + "NajaEDA_BUILD_ID": hashlib.sha256(manifest_json.encode()).hexdigest()} lines = [f"set({name} {_cmake_value(value)})" for name, value in values.items()] lines.append("set(NajaEDA_INCLUDE_DIRS " + " ".join(map(_cmake_value, include_dirs)) + ")") lines.append("set(NajaEDA_RUNTIME_LIBRARIES " + " ".join(map(_cmake_value, libraries.values())) + ")") for name, library in libraries.items(): lines.append(f"set(NajaEDA_{name}_LIBRARY {_cmake_value(library)})") if sys.platform == "win32": - implib = _import_library(name, library, output_dir / "import-libs") + implib = _import_library(name, library, output_dir / "import-libs", + None if published else provider.root) lines.append(f"set(NajaEDA_{name}_IMPLIB {_cmake_value(implib)})") return "\n".join(lines) + "\n" @@ -282,12 +345,18 @@ def main() -> None: action.add_argument("--cmake", action="store_true") action.add_argument("--fixup-consumer", type=Path) parser.add_argument("--output-dir", type=Path) - parser.add_argument("--source-archive", type=Path) + parser.add_argument("--published", action="store_true", + help=f"use the published NajaEDA {PUBLISHED_VERSION} release") + parser.add_argument("--source-archive", type=Path, + help="cached source archive of the published release") args = parser.parse_args() if args.cmake and args.output_dir is None: parser.error("--cmake requires --output-dir") + if args.source_archive is not None and not args.published: + parser.error("--source-archive requires --published") if args.cmake: - print(cmake_config(args.output_dir, args.source_archive), end="") + print(cmake_config(args.output_dir, published=args.published, + source_archive=args.source_archive), end="") else: fixup_consumer(args.fixup_consumer) diff --git a/test/python/test_naja_provider.py b/test/python/test_naja_provider.py new file mode 100644 index 00000000..c3045586 --- /dev/null +++ b/test/python/test_naja_provider.py @@ -0,0 +1,284 @@ +# Copyright 2026 keplertech.io +# SPDX-License-Identifier: Apache-2.0 + +from __future__ import annotations + +import hashlib +import importlib.util +import json +from pathlib import Path +import struct +import sys +import tempfile +from types import ModuleType, SimpleNamespace +import unittest +from unittest.mock import patch + + +_SOURCE = Path(__file__).resolve().parents[2] / "src/python" +_VERSION = "0.7.27" +_GIT_HASH = "abc1234" + + +def _load(name, path): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +builder = _load("naja_provider_builder", _SOURCE / "naja_provider.py") +guard = _load("naja_provider_guard", _SOURCE / "kepler_formal/_provider_check.py") + + +class _FakeProviderCase(unittest.TestCase): + """An importable fake NajaEDA package with native files and metadata.""" + + def setUp(self): + temporary = tempfile.TemporaryDirectory(prefix="kepler naja provider ") + self.addCleanup(temporary.cleanup) + self.root = Path(temporary.name).resolve() + self.package = self.root / "najaeda" + self.package.mkdir() + (self.package / "__init__.py").touch() + self.extension = self.package / "naja.so" + self.extension.write_bytes(b"provider native module") + windows = sys.platform == "win32" + self.libraries = {} + for name in builder.RUNTIMES: + library = self.package / (f"{name}.dll" if windows else f"lib{name}.so") + library.write_bytes(b"provider runtime " + name.encode()) + self.libraries[name] = library + if windows: + (self.package / "sdk/lib").mkdir(parents=True, exist_ok=True) + (self.package / "sdk/lib" / f"{name}.lib").touch() + self.manifest = { + path.relative_to(self.root).as_posix(): hashlib.sha256(path.read_bytes()).hexdigest() + for path in (self.extension, *self.libraries.values()) + } + self.naja = ModuleType("najaeda.naja") + self.naja.__file__ = str(self.extension) + self.naja.getGitHash = lambda: _GIT_HASH + self.naja.getVersion = lambda: _VERSION + najaeda = ModuleType("najaeda") + najaeda.__file__ = str(self.package / "__init__.py") + najaeda.naja = self.naja + self._patch(patch.dict(sys.modules, {"najaeda": najaeda, "najaeda.naja": self.naja})) + self.distribution = self._patch(patch.object( + guard.importlib.metadata, "distribution", return_value=self.installed(_VERSION))) + guard.validate_provider.cache_clear() + self.addCleanup(guard.validate_provider.cache_clear) + + def _patch(self, patcher): + result = patcher.start() + self.addCleanup(patcher.stop) + return result + + def installed(self, version, prefix=None): + """Distribution metadata for a pip-installed package under ``prefix``.""" + prefix = self.root if prefix is None else prefix + return SimpleNamespace(version=version, locate_file=lambda path: prefix / path) + + def without_metadata(self): + """A plain CMake install, as in the source regression, has no metadata.""" + self.distribution.side_effect = guard.importlib.metadata.PackageNotFoundError("najaeda") + + def add_wheel_headers(self): + include = self.package / "sdk/include" + for relative in ("naja/core/NajaVersion.h", "naja/core/NLUniverse.h", + "naja/dnl/DNL.h", "spdlog/spdlog.h"): + (include / relative).parent.mkdir(parents=True, exist_ok=True) + (include / relative).touch() + return include + + +class ProviderGuardTest(_FakeProviderCase): + def validate(self, manifest=None, version=_VERSION, git_hash=_GIT_HASH): + guard.validate_provider( + json.dumps(self.manifest if manifest is None else manifest), version, git_hash) + + def test_accepts_matching_native_files(self): + self.validate() + + def test_accepts_a_cmake_install_without_distribution_metadata(self): + self.without_metadata() + self.validate() + self.naja.getVersion = lambda: "0.7.25" + guard.validate_provider.cache_clear() + with self.assertRaisesRegex(ImportError, "found 0.7.25"): + self.validate() + + def test_rejects_replaced_native_library(self): + self.libraries["naja_nl"].write_bytes(b"different binary with same release number") + with self.assertRaisesRegex(ImportError, "runtime differs"): + self.validate() + + def test_rejects_version_and_revision_mismatch(self): + for version, revision in (("0.7.25", _GIT_HASH), (_VERSION, "unknown")): + with self.subTest(version=version, revision=revision): + with self.assertRaisesRegex(ImportError, "built against NajaEDA"): + self.validate(version=version, git_hash=revision) + + def test_rejects_wrong_distribution_and_foreign_extension(self): + self.distribution.return_value = self.installed(_VERSION, self.root / "foreign") + with self.assertRaisesRegex(ImportError, "installed distribution"): + self.validate() + self.distribution.return_value = self.installed(_VERSION) + self.naja.__file__ = str(self.root / "foreign/naja.so") + with self.assertRaisesRegex(ImportError, "outside its package"): + self.validate() + + def test_rejects_missing_file_and_manifest_without_extension(self): + self.libraries["naja_nl"].unlink() + with self.assertRaisesRegex(ImportError, "Cannot validate"): + self.validate() + with self.assertRaisesRegex(ImportError, "does not identify"): + self.validate({"najaeda/libnaja_nl.so": "0" * 64}) + + def test_rejects_empty_manifest_and_path_escapes(self): + with self.assertRaisesRegex(ImportError, "invalid NajaEDA provider manifest"): + self.validate({}) + for path in ("../outside", "/outside", "najaeda/../outside", "najaeda\\outside", "other/package"): + with self.subTest(path=path): + manifest = {**self.manifest, path: "0" * 64} + with self.assertRaisesRegex(ImportError, "invalid NajaEDA provider manifest entry"): + self.validate(manifest) + + +class ProviderDescriptionTest(_FakeProviderCase): + def test_development_provider_requires_wheel_headers(self): + with self.assertRaisesRegex(RuntimeError, "ships no headers"): + builder._provider() + self.add_wheel_headers() + expected = builder.Provider(self.package, self.extension, _VERSION, _GIT_HASH) + self.assertEqual(expected, builder._provider()) + self.without_metadata() + self.assertEqual(expected, builder._provider()) + + def test_published_provider_requires_the_pinned_release(self): + with self.assertRaisesRegex(RuntimeError, f"requires {builder.PUBLISHED_VERSION}"): + builder._provider(published=True) + self.distribution.return_value = self.installed(builder.PUBLISHED_VERSION) + self.naja.getGitHash = lambda: builder.PUBLISHED_GIT_COMMIT + self.naja.getVersion = lambda: builder.PUBLISHED_VERSION + # The published release ships no headers; they come from its archive. + self.assertEqual(builder.PUBLISHED_VERSION, builder._provider(published=True).version) + + def test_native_version_must_match_the_distribution(self): + self.add_wheel_headers() + self.naja.getVersion = lambda: "0.0.0" + with self.assertRaisesRegex(RuntimeError, "reports native version"): + builder._provider() + + def test_wheel_headers_list_every_naja_header_directory(self): + include = self.add_wheel_headers() + self.assertEqual([include, include / "naja/core", include / "naja/dnl"], + builder._wheel_headers(self.package)) + (include / "naja/core/NajaVersion.h").unlink() + with self.assertRaisesRegex(RuntimeError, "no version header"): + builder._wheel_headers(self.package) + + def test_cmake_config_describes_the_development_provider(self): + self.add_wheel_headers() + output = self.root / "consumer build" + text = builder.cmake_config(output) + self.assertIn(f"set(NajaEDA_VERSION [==[{_VERSION}]==])", text) + self.assertIn(f"set(NajaEDA_GIT_COMMIT [==[{_GIT_HASH}]==])", text) + self.assertIn(f"set(NajaEDA_naja_nl_LIBRARY [==[{self.libraries['naja_nl'].as_posix()}]==])", text) + self.assertIn((self.package / "sdk/include/naja/core").as_posix(), text) + header = (output / "include/KeplerNajaProviderBuild.h").read_text(encoding="utf-8") + self.assertIn(f'#define KEPLER_NAJA_PROVIDER_VERSION "{_VERSION}"', header) + self.assertIn(f'#define KEPLER_NAJA_PROVIDER_GIT_HASH "{_GIT_HASH}"', header) + manifest_line = next(line for line in header.splitlines() if "PROVIDER_MANIFEST" in line) + manifest = json.loads(json.loads(manifest_line.split(" ", 2)[2])) + self.assertEqual(self.manifest, manifest) + + +class ProviderBuildTest(unittest.TestCase): + def test_library_discovery_uses_wheel_repaired_names_and_bundled_tbb(self): + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary).resolve() / "najaeda" + root.mkdir() + siblings = root.parent / "najaeda.libs" + siblings.mkdir() + expected = {} + for name in (*builder.RUNTIMES, "tbb", "tbbmalloc"): + path = siblings / f"lib{name}-123abc.so.1" + path.touch() + expected[name] = path + self.assertEqual(expected, builder._libraries(root)) + duplicate = root / "libnaja_nl.so" + duplicate.touch() + with self.assertRaisesRegex(RuntimeError, "Expected one naja_nl"): + builder._libraries(root) + duplicate.unlink() + expected["naja_nl"].unlink() + with self.assertRaisesRegex(RuntimeError, "Expected one naja_nl"): + builder._libraries(root) + + def test_rejects_source_archive_with_wrong_checksum(self): + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary) + archive = root / "wrong.tar.gz" + archive.write_bytes(b"not the pinned release archive") + with self.assertRaisesRegex(RuntimeError, "checksum mismatch"): + builder._published_headers(root, archive) + self.assertFalse((root / "release-headers").exists()) + + def test_import_library_prefers_the_wheel_import_library(self): + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary) + (root / "sdk/lib").mkdir(parents=True) + original = root / "sdk/lib/naja_nl.lib" + original.touch() + library = root / "naja_nl.dll" + library.write_bytes(b"MZ") + self.assertEqual(original, builder._import_library("naja_nl", library, root / "out", root)) + # A repair-renamed DLL needs a regenerated import library instead. + renamed = root / "naja_nl-1a2b3c.dll" + renamed.write_bytes(b"MZ") + with self.assertRaises(RuntimeError): + builder._import_library("naja_nl", renamed, root / "out", root) + + def test_cmake_values_preserve_spaces_and_reject_control_delimiters(self): + self.assertEqual("[==[C:/Program Files/provider]==]", builder._cmake_value(r"C:\Program Files\provider")) + for value in ("path;other", "path\nother", "path\rother", "path]==]other"): + with self.subTest(value=value), self.assertRaises(RuntimeError): + builder._cmake_value(value) + + def test_pe_export_reader_distinguishes_function_and_uninitialized_data(self): + # The cache singleton is an exported data symbol. Misclassifying it as + # a function creates a bad Windows import library even when linking succeeds. + data = bytearray(0x510) + pe, optional, optional_size = 0x80, 0x98, 0xF0 + data[:2] = b"MZ" + struct.pack_into("=0.11.3,<0.12", "najaeda==0.7.26"] +requires = ["scikit-build-core>=0.11.3,<0.12", "najaeda==0.7.27"] [project] name = "kepler-formal" -dependencies = ["najaeda==0.7.26"] +dependencies = ["najaeda==0.7.27"] dynamic = ["version"] [tool.scikit-build.cmake.define] @@ -78,7 +78,7 @@ def test_default_preparation_does_not_modify_checkout(self): def test_published_preparation_changes_only_pins_and_cmake_option(self): release.prepare_project(self.project, published_najaeda=True) - expected = METADATA.replace("najaeda==0.7.26", "najaeda==0.7.24").replace( + expected = METADATA.replace("najaeda==0.7.27", "najaeda==0.7.24").replace( 'KEPLER_USE_PUBLISHED_NAJAEDA = "OFF"', 'KEPLER_USE_PUBLISHED_NAJAEDA = "ON"') self.assertEqual(expected, self.metadata.read_text(encoding="utf-8")) @@ -92,8 +92,8 @@ def test_published_preparation_adds_missing_cmake_option(self): self.assertEqual("0.5.0", self._validate()) def test_mismatched_or_unsupported_provider_pins_do_not_modify_checkout(self): - for text in (METADATA.replace("najaeda==0.7.26", "najaeda==0.7.24", 1), - METADATA.replace("najaeda==0.7.26", "najaeda>=0.7.24")): + for text in (METADATA.replace("najaeda==0.7.27", "najaeda==0.7.24", 1), + METADATA.replace("najaeda==0.7.27", "najaeda>=0.7.24")): with self.subTest(text=text): self.metadata.write_text(text, encoding="utf-8") with self.assertRaisesRegex(ValueError, "supported provider"): diff --git a/test/python/test_shared_naja_sdk_selection.py b/test/python/test_shared_naja_selection.py similarity index 54% rename from test/python/test_shared_naja_sdk_selection.py rename to test/python/test_shared_naja_selection.py index 0d0b556b..db5d5923 100644 --- a/test/python/test_shared_naja_sdk_selection.py +++ b/test/python/test_shared_naja_selection.py @@ -13,6 +13,7 @@ _MODULE = Path(__file__).resolve().parents[2] / "src/python/KeplerSharedNaja.cmake" +_RUNTIMES = ("naja_nl", "naja_dnl", "naja_bne", "naja_opt", "naja_metrics", "naja_python") _TBB_FINDER = """ set(TBB_FOUND TRUE) foreach(dependency IN ITEMS tbb tbbmalloc) @@ -29,13 +30,93 @@ """ +def _make_provider(site: Path, version: str = "0.7.27", git_hash: str = "abc1234") -> Path: + """Create an importable fake NajaEDA development wheel installed in ``site``.""" + package = site / "najaeda" + (package / "sdk/include/naja/core").mkdir(parents=True) + (package / "__init__.py").touch() + (package / "naja.py").write_text( + f"def getVersion():\n return {version!r}\n" + f"def getGitHash():\n return {git_hash!r}\n", encoding="utf-8") + for name in ("NajaVersion.h", "NLUniverse.h"): + (package / "sdk/include/naja/core" / name).touch() + windows = sys.platform == "win32" + for name in _RUNTIMES: + (package / (f"{name}.dll" if windows else f"lib{name}.so")).write_bytes(b"provider " + name.encode()) + if windows: + (package / "sdk/lib").mkdir(exist_ok=True) + (package / "sdk/lib" / f"{name}.lib").touch() + info = site / f"najaeda-{version}.dist-info" + info.mkdir() + (info / "METADATA").write_text( + f"Metadata-Version: 2.1\nName: najaeda\nVersion: {version}\n", encoding="utf-8") + return package + + +def _write_fixture(source: Path, body: str, *, languages: str = "NONE") -> None: + (source / "FindTBB.cmake").write_text(_TBB_FINDER, encoding="utf-8") + (source / "boost").mkdir(exist_ok=True) + (source / "boost/version.hpp").touch() + (source / "CMakeLists.txt").write_text( + "cmake_minimum_required(VERSION 3.30)\n" + f"project(SharedProviderSelection LANGUAGES {languages})\n" + 'set(CMAKE_MODULE_PATH "${CMAKE_CURRENT_SOURCE_DIR}")\n' + "add_library(Python3::Module INTERFACE IMPORTED)\n" + f"include([==[{_MODULE.as_posix()}]==])\n" + body, encoding="utf-8") + + @unittest.skipUnless(shutil.which("cmake"), "CMake is required") -class SharedNajaSDKSelectionTests(unittest.TestCase): - def test_python_provider_overrides_cached_or_user_sdk_directory(self): - self._check_provider_selection(windows_separators=False) +class SharedNajaSelectionTests(unittest.TestCase): + def test_build_links_the_provider_installed_in_the_build_interpreter(self): + with tempfile.TemporaryDirectory(prefix="kepler provider selection ") as temporary: + root = Path(temporary).resolve() + source = root / "source" + source.mkdir() + _write_fixture(source, """ +string(FIND "${NajaEDA_naja_nl_LIBRARY}" "${EXPECTED_PROVIDER}/" position) +if(NOT position EQUAL 0) + message(FATAL_ERROR "Linked ${NajaEDA_naja_nl_LIBRARY} instead of ${EXPECTED_PROVIDER}") +endif() +get_target_property(includes naja_nl INTERFACE_INCLUDE_DIRECTORIES) +if(NOT "${EXPECTED_PROVIDER}/sdk/include/naja/core" IN_LIST includes) + message(FATAL_ERROR "Provider headers are not used: ${includes}") +endif() +""") + # Reconfigure the same build directory with another provider: the + # interpreter's current package wins, not a cached selection. + for site_name in ("provider one", "provider two"): + with self.subTest(provider=site_name): + site = root / "Users" / site_name + package = _make_provider(site) + environment = os.environ.copy() + environment.update(PYTHONPATH=str(site), PYTHONDONTWRITEBYTECODE="1") + result = subprocess.run([ + shutil.which("cmake"), "-S", str(source), "-B", str(root / "build"), + f"-DPython3_EXECUTABLE={sys.executable}", + f"-DBoost_INCLUDE_DIR={source}", + f"-DEXPECTED_PROVIDER={package.as_posix()}", + ], env=environment, capture_output=True, text=True) + self.assertEqual(0, result.returncode, result.stdout + result.stderr) - def test_windows_sdk_path_through_package_wrapper(self): - self._check_provider_selection(windows_separators=True) + def test_published_release_is_rejected_without_the_option(self): + with tempfile.TemporaryDirectory(prefix="kepler provider selection ") as temporary: + root = Path(temporary).resolve() + source = root / "source" + source.mkdir() + _write_fixture(source, "") + site = root / "site" + package = _make_provider(site, version="0.7.24", git_hash="2263958") + shutil.rmtree(package / "sdk") + environment = os.environ.copy() + environment.update(PYTHONPATH=str(site), PYTHONDONTWRITEBYTECODE="1") + result = subprocess.run([ + shutil.which("cmake"), "-S", str(source), "-B", str(root / "build"), + f"-DPython3_EXECUTABLE={sys.executable}", + f"-DBoost_INCLUDE_DIR={source}", + ], env=environment, capture_output=True, text=True) + self.assertNotEqual(0, result.returncode) + self.assertIn("ships no headers", result.stderr) + self.assertIn("KEPLER_USE_PUBLISHED_NAJAEDA", result.stderr) @unittest.skipUnless( any(shutil.which(compiler) for compiler in @@ -43,22 +124,11 @@ def test_windows_sdk_path_through_package_wrapper(self): if compiler), "A C++ compiler is required") def test_tbb_auto_link_policy_propagates_only_to_windows_consumers(self): with tempfile.TemporaryDirectory(prefix="kepler tbb policy ") as temporary: - root = Path(temporary) - package = root / "provider/najaeda" - config = package / "sdk/cmake" - config.mkdir(parents=True) - (package / "__init__.py").touch() - (package / "sdk.py").write_text( - "from pathlib import Path\n" - "def get_cmake_dir():\n" - " return str(Path(__file__).resolve().parent / 'sdk/cmake')\n", - encoding="utf-8") - (config / "NajaEDAConfig.cmake").write_text( - "set(NajaEDA_FOUND TRUE)\n", encoding="utf-8") + root = Path(temporary).resolve() + site = root / "provider" + _make_provider(site) source = root / "source" - (source / "boost").mkdir(parents=True) - (source / "boost/version.hpp").touch() - (source / "FindTBB.cmake").write_text(_TBB_FINDER, encoding="utf-8") + source.mkdir() (source / "probe.cpp").write_text(""" #if EXPECT_TBB_NO_IMPLICIT_LINKAGE #if !defined(__TBB_NO_IMPLICIT_LINKAGE) || __TBB_NO_IMPLICIT_LINKAGE != 1 @@ -69,10 +139,14 @@ def test_tbb_auto_link_policy_propagates_only_to_windows_consumers(self): #endif int tbb_linkage_probe() { return 0; } """, encoding="utf-8") + (source / "FindTBB.cmake").write_text(_TBB_FINDER, encoding="utf-8") + (source / "boost").mkdir() + (source / "boost/version.hpp").touch() (source / "CMakeLists.txt").write_text( "cmake_minimum_required(VERSION 3.30)\n" "project(TBBAutoLinkPolicy LANGUAGES CXX)\n" 'set(CMAKE_MODULE_PATH "${CMAKE_CURRENT_SOURCE_DIR}")\n' + "add_library(Python3::Module INTERFACE IMPORTED)\n" # Emulate only the policy branch, retaining the host compiler # and platform for the actual object/static-library builds. 'set(host_is_windows "${WIN32}")\n' @@ -100,7 +174,7 @@ def test_tbb_auto_link_policy_propagates_only_to_windows_consumers(self): target_compile_definitions(unrelated PRIVATE EXPECT_TBB_NO_IMPLICIT_LINKAGE=0) """, encoding="utf-8") environment = os.environ.copy() - environment.update(PYTHONPATH=str(package.parent), PYTHONDONTWRITEBYTECODE="1") + environment.update(PYTHONPATH=str(site), PYTHONDONTWRITEBYTECODE="1") for windows_policy in (False, True): with self.subTest(windows_policy=windows_policy): build = root / ("windows" if windows_policy else "non-windows") @@ -116,67 +190,6 @@ def test_tbb_auto_link_policy_propagates_only_to_windows_consumers(self): capture_output=True, text=True, timeout=120) self.assertEqual(0, result.returncode, result.stdout + result.stderr) - def _check_provider_selection(self, *, windows_separators): - with tempfile.TemporaryDirectory(prefix="kepler sdk selection ") as temporary: - root = Path(temporary) - source = root / "source" - source.mkdir() - wrong = root / "wrong sdk" - wrong.mkdir() - (wrong / "NajaEDAConfig.cmake").write_text( - 'message(FATAL_ERROR "Loaded a foreign cached SDK")\n', encoding="utf-8") - (source / "FindTBB.cmake").write_text(_TBB_FINDER, encoding="utf-8") - (source / "boost").mkdir() - (source / "boost/version.hpp").touch() - # vcpkg wraps find_package in a macro and expands ARGN again in - # set(). Native Windows paths can then turn '\\U' into an invalid - # CMake escape, even when the original call quoted its argument. - package_wrapper = ( - "if(POLICY CMP0219)\n" - " cmake_policy(SET CMP0219 OLD)\n" - "endif()\n" - "macro(find_package)\n" - ' set(wrapper_arguments "${ARGN}")\n' - " _find_package(${wrapper_arguments})\n" - "endmacro()\n" - ) if windows_separators else "" - (source / "CMakeLists.txt").write_text( - "cmake_minimum_required(VERSION 3.30)\n" - "project(SharedSDKSelection NONE)\n" - 'set(CMAKE_MODULE_PATH "${CMAKE_CURRENT_SOURCE_DIR}")\n' - + package_wrapper + - f"include([==[{_MODULE.as_posix()}]==])\n" - 'if(NOT NajaEDA_CONFIG STREQUAL "${provider_cmake_dir}/NajaEDAConfig.cmake")\n' - ' message(FATAL_ERROR "Selected SDK does not belong to Python provider")\n' - "endif()\n", encoding="utf-8") - for provider_name in ("provider one", "provider two"): - with self.subTest(provider=provider_name): - provider = root / "Users" / provider_name - package = provider / "najaeda" - config = package / "sdk/cmake" - config.mkdir(parents=True) - (package / "__init__.py").touch() - (package / "sdk.py").write_text( - "from pathlib import Path\n" - "def get_cmake_dir():\n" - " path = str(Path(__file__).resolve().parent / 'sdk/cmake')\n" - + (" return path.replace('/', chr(92))\n" - if windows_separators else " return path\n"), - encoding="utf-8") - (config / "NajaEDAConfig.cmake").write_text( - "set(NajaEDA_FOUND TRUE)\n", encoding="utf-8") - environment = os.environ.copy() - environment.update(PYTHONPATH=str(provider), PYTHONDONTWRITEBYTECODE="1") - result = subprocess.run([ - shutil.which("cmake"), "-S", str(source), "-B", str(root / "build"), - f"-DPython3_EXECUTABLE={sys.executable}", - f"-DBoost_INCLUDE_DIR={source}", - # Keep a real stale/user-selected cache entry while - # changing the Python provider between configurations. - f"-DNajaEDA_DIR={wrong}", - ], env=environment, capture_output=True, text=True) - self.assertEqual(0, result.returncode, result.stdout + result.stderr) - if __name__ == "__main__": unittest.main() diff --git a/thirdparty/naja b/thirdparty/naja index 6331960c..ad34893b 160000 --- a/thirdparty/naja +++ b/thirdparty/naja @@ -1 +1 @@ -Subproject commit 6331960cb372ef6d332d07a42fb449d0bea01bbe +Subproject commit ad34893beb810ce4e30af9b5f82a7612c8be6992