diff --git a/CHANGELOG.md b/CHANGELOG.md index f6c3a5072daa..c7234a714fdf 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -29,6 +29,8 @@ All notable changes to this project will be documented in this file. * fixed `Eq` reporting a definite inequality when an undefined bit could have made the two values equal, it now reports an undefined result like the other comparisons do * added constant folding for the `Sdiv`, `Udiv`, `Srem` and `Urem` operations, which were not implemented and made evaluation of any function containing them fail, following the SMT-LIB definitions these operations are translated to * sped up evaluation with constant inputs by about 3x by folding the values directly instead of building a Boolean function per operation, which dominates the runtime of `compute_truth_table()` and thereby of the HAWKEYE S-box identification + * fixed `SMT::Solver::has_local_solver_for` testing `SolverCall::Binary` in both of its branches, so the branch for `SolverCall::Library` was unreachable and library availability always reported `false` + * fixed `SMT::SymbolicState::set` using `emplace`, which leaves an existing binding untouched, so setting a variable a second time did nothing and a loop stepping a symbolic state forward silently kept the value it started with * added simplification rules for the word level operations, which the single-bit simplification through ABC cannot reach: extensions to the width the value already has, nested extensions and slices, slices that fall into one half of a concatenation or into either part of an extension, unsigned comparisons against zero and the maximum, equality of a value with its own negation, and single bit equalities and selections * Python bindings * fixed the Python bindings handing out gates, nets, modules, endpoints and pins without tying them to the netlist that owns them, so that dropping the netlist left them pointing into freed memory. Reading 500 gates and 500 nets of a dropped netlist returned the wrong name and ID for 184 and 230 of them respectively, silently rather than by crashing @@ -44,6 +46,10 @@ All notable changes to this project will be documented in this file. * added a test that calls every no-argument binding reachable from a small netlist and imports every plugin module, so that a binding which compiles and only fails when called is caught * changed every binding that hands out a borrowed object to keep its **owner** alive rather than the object it was read from, through the new `hal::borrowed()` call policy that replaces `py::return_value_policy::reference_internal` at 241 places. The policy was only applied while a wrapper was being created, so whether an object was protected depended on which binding happened to hand it over first, and a module read from a gate was tied to that gate although the netlist is what owns it * fixed `DataContainer`, `ProjectDirectory`, `hawkeye.DetectionConfiguration`, `hawkeye.SBoxDatabase` and `dataflow.Configuration` leaking every instance created from Python, as each was bound with a holder that never frees. `SBoxDatabase.from_file` leaked 25 KB per call, and `ProjectManager.get_project_directory` leaked a copy on every call, as pybind11 copies a returned reference by default + * fixed `SMT.SymbolicExecution.evaluate` raising a `TypeError` on every call: both overloads were bound directly, so they returned an unregistered `Result`, where every other binding in that file unwraps it + * fixed the `hal::borrowed()` call policy having no effect on any of the 55 properties it was given to, so those still handed out a borrowed object without keeping its owner alive. `def_property_readonly` builds the getter itself before it forwards the attributes that follow, so a call policy given to a property never reaches the function that performs the call + * fixed a Python interpreter that loaded the HAL plugins segfaulting on the way out unless it unloaded them again by hand, as the plugin libraries were closed while the parser and writer registries still held a factory function out of each of them + * added Python bindings for `SMT.SolverCall` and `SMT.Solver.to_smt2`, and the missing `Bitwuzla` value of `SMT.SolverType`. Without `SolverCall`, neither `QueryConfig.with_call` nor `Solver.has_local_solver_for` could be called at all although both were bound * fixed three enum values that were bound to a different value of their own enum, which made them indistinguishable from Python: `GateTypeProperty.fifo` was bound to `ram`, `module_identification.CandidateType.addition_offset` to `addition`, and `gui_extension_demo.ParameterType.Module` to `Gate` * Plugins * HAWKEYE @@ -68,6 +74,8 @@ All notable changes to this project will be documented in this file. * netlist preprocessing * fixed `remove_redundant_gates` treating two flip-flops as duplicates although they start out at different values, as the fingerprint it groups them by covers the gate type and the fan-in but not the initial value, and flip-flops are merged on that fingerprint alone without the equivalence check that combinational gates get. This affects 11 of the 13 flip-flop types of the Xilinx UNISIM library, all of which carry an `INIT` value * bit-order propagation + * changed the interface to speak in a `BitOrder`, which is the order of one module pin group, and a `BitOrderResult`, which is what a propagation reports, in place of a map from pairs of module and pin group to a map from net to index. A bit order is now an object rather than a container, so Python can be given one without losing track of the netlist it belongs to, and a result iterates by module and pin group ID rather than by the addresses they happen to sit at + * added tests for the plugin, which had none * fixed bug in the bitorder propagation algorithm that would assign a wrong propagation order if pingroups with direction none were given as parameters * simulation * added feature, selecting a waveform in viewer selects net in graph view as well diff --git a/include/hal_core/netlist/boolean_function/symbolic_state.h b/include/hal_core/netlist/boolean_function/symbolic_state.h index 3c6674672df5..5bb639d8812c 100644 --- a/include/hal_core/netlist/boolean_function/symbolic_state.h +++ b/include/hal_core/netlist/boolean_function/symbolic_state.h @@ -65,7 +65,10 @@ namespace hal const BooleanFunction& get(const BooleanFunction& key) const; /** - * Sets a Boolean function equivalent in the symbolic state. + * Sets a Boolean function equivalent in the symbolic state, replacing an equivalent that + * was set for the same key before. + * + * Does nothing if the key is not a variable. * * @param[in] key - The Boolean function. * @param[in] value - The equivalent Boolean function. diff --git a/plugins/bitorder_propagation/CMakeLists.txt b/plugins/bitorder_propagation/CMakeLists.txt index 63e22c7d3139..3124aee4c1bd 100644 --- a/plugins/bitorder_propagation/CMakeLists.txt +++ b/plugins/bitorder_propagation/CMakeLists.txt @@ -12,4 +12,6 @@ if(PL_BITORDER_PROPAGATION OR BUILD_ALL_PLUGINS) PYDOC SPHINX_DOC_INDEX_FILE ${CMAKE_CURRENT_SOURCE_DIR}/documentation/bitorder_propagation.rst LINK_LIBRARIES nlohmann_json::nlohmann_json ) + + add_subdirectory(test) endif() diff --git a/plugins/bitorder_propagation/include/bitorder_propagation/bit_order.h b/plugins/bitorder_propagation/include/bitorder_propagation/bit_order.h new file mode 100644 index 000000000000..5d465616fd76 --- /dev/null +++ b/plugins/bitorder_propagation/include/bitorder_propagation/bit_order.h @@ -0,0 +1,208 @@ +// MIT License +// +// Copyright (c) 2019 Ruhr University Bochum, Chair for Embedded Security. All Rights reserved. +// Copyright (c) 2019 Marc Fyrbiak, Sebastian Wallat, Max Hoffmann ("ORIGINAL AUTHORS"). All rights reserved. +// Copyright (c) 2021 Max Planck Institute for Security and Privacy. All Rights reserved. +// Copyright (c) 2021 Jörn Langheinrich, Julian Speith, Nils Albartus, René Walendy, Simon Klix ("ORIGINAL AUTHORS"). All Rights reserved. +// +// Permission is hereby granted, free of charge, to any person obtaining a copy +// of this software and associated documentation files (the "Software"), to deal +// in the Software without restriction, including without limitation the rights +// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +// copies of the Software, and to permit persons to whom the Software is +// furnished to do so, subject to the following conditions: +// +// The above copyright notice and this permission notice shall be included in all +// copies or substantial portions of the Software. +// +// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +// SOFTWARE. + +/** + * @file bit_order.h + * @brief This file contains the bit order of a module pin group and the collection of bit orders that a propagation produces. + */ + +#pragma once + +#include "hal_core/defines.h" +#include "hal_core/netlist/pins/pin_group.h" + +#include +#include + +namespace hal +{ + class Net; + class Module; + class ModulePin; + + namespace bitorder_propagation + { + /** + * The index of a module pin group among the words that `export_bitorder_propagation_information` writes. + * + * It identifies a word within the exported file and has nothing to do with the index of a bit. + */ + using WordIndex = u32; + + /** + * The bit order of a single module pin group, i.e., which net of the pin group carries which bit. + * + * The index of a net is stored with it rather than implied by its position, so that an order with gaps in + * it can be expressed. Propagation produces a continuous order today, but it is not guaranteed to keep + * doing so, and the pin group a bit order belongs to need not start at index 0 either. + */ + class BitOrder + { + public: + /** + * Construct a bit order for a module pin group. + * + * The order is sorted by index, so that iterating over it walks the bits from the lowest index to the + * highest no matter in which order they were discovered. + * + * @param[in] module - The module the pin group belongs to. + * @param[in] pin_group - The pin group. + * @param[in] order - The index of each net of the pin group. + */ + BitOrder(Module* module, PinGroup* pin_group, std::vector> order); + + /** + * Get the module that the pin group belongs to. + * + * @returns The module. + */ + Module* get_module() const; + + /** + * Get the pin group whose bit order this is. + * + * @returns The pin group. + */ + PinGroup* get_pin_group() const; + + /** + * Get the index of every net, ordered by index. + * + * @returns The nets and their indices. + */ + const std::vector>& get_order() const; + + /** + * Get the index of the given net. + * + * @param[in] net - The net. + * @returns The index of the net, or `std::nullopt` if the net is not part of this bit order. + */ + std::optional get_index(const Net* net) const; + + /** + * Get the net at the given index. + * + * @param[in] index - The index. + * @returns The net at the index, or a `nullptr` if no net carries that index. + */ + Net* get_net_at(u32 index) const; + + /** + * Get the number of nets that the bit order covers. + * + * @returns The number of nets. + */ + u32 get_size() const; + + /** + * Check whether the indices run from 0 without leaving a gap. + * + * @returns `true` if the order is continuous, `false` otherwise. + */ + bool is_continuous() const; + + bool operator==(const BitOrder& other) const; + bool operator!=(const BitOrder& other) const; + + private: + Module* m_module; + PinGroup* m_pin_group; + std::vector> m_order; + }; + + /** + * The bit orders that are known, which is what a propagation reports: the ones it was given as well as + * the ones it worked out. + * + * The bit orders are held in a stable order, by module ID and then by pin group ID, so that iterating over + * a result does not depend on where the modules and pin groups happen to be allocated. + */ + class BitOrderResult + { + public: + BitOrderResult() = default; + + /** + * Construct a result from the given bit orders. + * + * @param[in] bit_orders - The bit orders. + */ + explicit BitOrderResult(std::vector bit_orders); + + /** + * Add a bit order, replacing one that is already known for the same pin group. + * + * @param[in] bit_order - The bit order. + */ + void add(BitOrder bit_order); + + /** + * Get every bit order, ordered by module ID and pin group ID. + * + * @returns The bit orders. + */ + const std::vector& get_bit_orders() const; + + /** + * Get the bit order of the given pin group. + * + * @param[in] module - The module the pin group belongs to. + * @param[in] pin_group - The pin group. + * @returns The bit order, or a `nullptr` if the pin group has no known bit order. + */ + const BitOrder* get(const Module* module, const PinGroup* pin_group) const; + + /** + * Check whether the bit order of the given pin group is known. + * + * @param[in] module - The module the pin group belongs to. + * @param[in] pin_group - The pin group. + * @returns `true` if the bit order is known, `false` otherwise. + */ + bool contains(const Module* module, const PinGroup* pin_group) const; + + /** + * Get the number of pin groups whose bit order is known. + * + * @returns The number of bit orders. + */ + u32 get_size() const; + + /** + * Check whether no bit order at all is known. + * + * @returns `true` if there is no bit order, `false` otherwise. + */ + bool is_empty() const; + + std::vector::const_iterator begin() const; + std::vector::const_iterator end() const; + + private: + std::vector m_bit_orders; + }; + } // namespace bitorder_propagation +} // namespace hal diff --git a/plugins/bitorder_propagation/include/bitorder_propagation/bitorder_propagation.h b/plugins/bitorder_propagation/include/bitorder_propagation/bitorder_propagation.h index 89080ab0ca9f..714f27eb2695 100644 --- a/plugins/bitorder_propagation/include/bitorder_propagation/bitorder_propagation.h +++ b/plugins/bitorder_propagation/include/bitorder_propagation/bitorder_propagation.h @@ -30,6 +30,7 @@ #pragma once +#include "bitorder_propagation/bit_order.h" #include "hal_core/defines.h" #include "hal_core/netlist/pins/pin_group.h" #include "hal_core/utilities/result.h" @@ -59,8 +60,8 @@ namespace hal * @param[in] enforce_continuous_bitorders - Set `true` to only allow for continuous bit orders, `false` to also allow bit orders that are not continuous. Defaults to `true`. * @returns OK and a map containing all known bit orders (including new and already known ones) on success, an error otherwise. */ - Result*>, std::map>> - propagate_module_pingroup_bitorder(const std::map*>, std::map>& src, + Result + propagate_module_pingroup_bitorder(const BitOrderResult& src, const std::set*>>& dst, const bool enforce_continuous_bitorders = true); @@ -70,7 +71,7 @@ namespace hal * @param[in] ordered_module_pin_groups - A mapping from pairs of modules and their pin groups to known bit-order information given as a mapping from nets to their index. * @returns OK on success, an error otherwise. */ - Result reorder_module_pin_groups(const std::map*>, std::map>& ordered_module_pin_groups); + Result reorder_module_pin_groups(const BitOrderResult& ordered_module_pin_groups); /** * @brief Propagate known bit-order information from one module pin group to another module pin group of unknown bit order. @@ -84,7 +85,7 @@ namespace hal * @param[in] dst - The pair of module ID and pin group name with unknown bit order. * @returns OK and a map containing all known bit orders (including new and already known ones) on success, an error otherwise. */ - Result*>, std::map>> propagate_bitorder(Netlist* nl, const std::pair& src, const std::pair& dst); + Result propagate_bitorder(Netlist* nl, const std::pair& src, const std::pair& dst); /** * @brief Propagate known bit-order information from one module pin group to another module pin group of unknown bit order. @@ -97,7 +98,7 @@ namespace hal * @param[in] dst - The pair of module and pin group with unknown bit order. * @returns OK and a map containing all known bit orders (including new and already known ones) on success, an error otherwise. */ - Result*>, std::map>> propagate_bitorder(const std::pair*>& src, + Result propagate_bitorder(const std::pair*>& src, const std::pair*>& dst); /** @@ -112,7 +113,7 @@ namespace hal * @param[in] dst - The pairs of module ID and pin group name with unknown bit order. * @returns OK and a map containing all known bit orders (including new and already known ones) on success, an error otherwise. */ - Result*>, std::map>> + Result propagate_bitorder(Netlist* nl, const std::vector>& src, const std::vector>& dst); /** @@ -126,7 +127,7 @@ namespace hal * @param[in] dst - The pairs of module and pin group with unknown bit order. * @returns OK and a map containing all known bit orders (including new and already known ones) on success, an error otherwise. */ - Result*>, std::map>> propagate_bitorder(const std::vector*>>& src, + Result propagate_bitorder(const std::vector*>>& src, const std::vector*>>& dst); /** @@ -137,7 +138,7 @@ namespace hal * @param[in] export_filepath - The filepath where the `.json` file should be written to. * @returns OK and a map containing all known bit orders (including new and already known ones) on success, an error otherwise. */ - Result*>, u32>> export_bitorder_propagation_information(const std::vector*>>& src, + Result*>, WordIndex>> export_bitorder_propagation_information(const std::vector*>>& src, const std::vector*>>& dst, const std::string& export_filepath); /** @@ -148,7 +149,7 @@ namespace hal * @param[in] export_filepath - The filepath where the `.json` file should be written to. * @returns OK and the mapping from each mdoule/pingroup pair to its index on success, an error otherwise. */ - Result*>, u32>> export_bitorder_propagation_information(const std::map*>, std::map>& src, + Result*>, WordIndex>> export_bitorder_propagation_information(const BitOrderResult& src, const std::set*>>& dst, const std::string& export_filepath); diff --git a/plugins/bitorder_propagation/python/python_bindings.cpp b/plugins/bitorder_propagation/python/python_bindings.cpp index f768e3f1afb5..3db0e400b2c5 100644 --- a/plugins/bitorder_propagation/python/python_bindings.cpp +++ b/plugins/bitorder_propagation/python/python_bindings.cpp @@ -67,11 +67,126 @@ namespace hal :rtype: str )"); + py::class_ py_bit_order(m, "BitOrder", R"( + The bit order of a single module pin group, i.e., which net of the pin group carries which bit. + )"); + + py_bit_order.def(py::init*, std::vector>>(), py::arg("module"), py::arg("pin_group"), py::arg("order"), R"( + Construct a bit order for a module pin group. + + :param hal_py.Module module: The module the pin group belongs to. + :param hal_py.ModulePinGroup pin_group: The pin group. + :param list[tuple(hal_py.Net,int)] order: The index of each net of the pin group. + )"); + + // The getter is built as a cpp_function here rather than handed over directly, because + // def_property_readonly builds it itself without passing on any of the attributes that follow, + // so a call policy given to the property never reaches the function that does the call. + py_bit_order.def_property_readonly("module", py::cpp_function(&bitorder_propagation::BitOrder::get_module, py::is_method(py_bit_order), borrowed()), R"( + The module that the pin group belongs to. + + :type: hal_py.Module + )"); + + py_bit_order.def_property_readonly("pin_group", py::cpp_function(&bitorder_propagation::BitOrder::get_pin_group, py::is_method(py_bit_order), borrowed()), R"( + The pin group whose bit order this is. + + :type: hal_py.ModulePinGroup + )"); + + py_bit_order.def_property_readonly("order", py::cpp_function(&bitorder_propagation::BitOrder::get_order, py::is_method(py_bit_order), borrowed()), R"( + The index of every net, ordered by index. + + :type: list[tuple(hal_py.Net,int)] + )"); + + py_bit_order.def("get_index", &bitorder_propagation::BitOrder::get_index, py::arg("net"), R"( + Get the index of the given net. + + :param hal_py.Net net: The net. + :returns: The index of the net, ``None`` if the net is not part of this bit order. + :rtype: int or None + )"); + + py_bit_order.def("get_net_at", &bitorder_propagation::BitOrder::get_net_at, py::arg("index"), borrowed(), R"( + Get the net at the given index. + + :param int index: The index. + :returns: The net at the index, ``None`` if no net carries that index. + :rtype: hal_py.Net or None + )"); + + py_bit_order.def_property_readonly("size", &bitorder_propagation::BitOrder::get_size, R"( + The number of nets that the bit order covers. + + :type: int + )"); + + py_bit_order.def("is_continuous", &bitorder_propagation::BitOrder::is_continuous, R"( + Check whether the indices run from 0 without leaving a gap. + + :returns: ``True`` if the order is continuous, ``False`` otherwise. + :rtype: bool + )"); + + py_bit_order.def(py::self == py::self); + py_bit_order.def(py::self != py::self); + + py::class_ py_bit_order_result(m, "BitOrderResult", R"( + The bit orders that are known, which is what a propagation reports: the ones it was given as well as the ones it worked out. + + Iterating over a result walks the bit orders by module ID and then by pin group ID, so it does not depend on where the modules and pin groups happen to be allocated. + )"); + + py_bit_order_result.def(py::init<>(), R"(Construct a result that holds no bit order.)"); + + py_bit_order_result.def(py::init>(), py::arg("bit_orders"), R"( + Construct a result from the given bit orders. + + :param list[bitorder_propagation.BitOrder] bit_orders: The bit orders. + )"); + + py_bit_order_result.def("add", &bitorder_propagation::BitOrderResult::add, py::arg("bit_order"), R"( + Add a bit order, replacing one that is already known for the same pin group. + + :param bitorder_propagation.BitOrder bit_order: The bit order. + )"); + + py_bit_order_result.def_property_readonly( + "bit_orders", py::cpp_function(&bitorder_propagation::BitOrderResult::get_bit_orders, py::is_method(py_bit_order_result), borrowed()), R"( + Every bit order, ordered by module ID and pin group ID. + + :type: list[bitorder_propagation.BitOrder] + )"); + + py_bit_order_result.def("get", &bitorder_propagation::BitOrderResult::get, py::arg("module"), py::arg("pin_group"), borrowed(), R"( + Get the bit order of the given pin group. + + :param hal_py.Module module: The module the pin group belongs to. + :param hal_py.ModulePinGroup pin_group: The pin group. + :returns: The bit order, ``None`` if the pin group has no known bit order. + :rtype: bitorder_propagation.BitOrder or None + )"); + + py_bit_order_result.def("contains", &bitorder_propagation::BitOrderResult::contains, py::arg("module"), py::arg("pin_group"), R"( + Check whether the bit order of the given pin group is known. + + :param hal_py.Module module: The module the pin group belongs to. + :param hal_py.ModulePinGroup pin_group: The pin group. + :returns: ``True`` if the bit order is known, ``False`` otherwise. + :rtype: bool + )"); + + py_bit_order_result.def("__len__", &bitorder_propagation::BitOrderResult::get_size); + + py_bit_order_result.def( + "__iter__", [](const bitorder_propagation::BitOrderResult& self) { return py::make_iterator(self.begin(), self.end()); }, py::keep_alive<0, 1>()); + m.def( "propagate_module_pingroup_bitorder", - [](const std::map*>, std::map>& src, + [](const bitorder_propagation::BitOrderResult& src, const std::set*>>& dst, - const bool enforce_continuous_bitorders = true) -> std::optional*>, std::map>> { + const bool enforce_continuous_bitorders = true) -> std::optional { const auto res = bitorder_propagation::propagate_module_pingroup_bitorder(src, dst, enforce_continuous_bitorders); if (res.is_ok()) { @@ -91,16 +206,16 @@ namespace hal The known bit-order information is taken from the map from net to index given for each pair of module and pin group in ``src``. After propagation, the algorithm tries to reconstruct valid bit orders from the propagated information. - :param dict[tuple(hal_py.Module,hal_py.ModulePinGroup),dict[hal_py.Net,int]] src: The known indices for the nets belonging to the given module pin groups. + :param bitorder_propagation.BitOrderResult src: The bit orders that are already known. :param set[tuple(hal_py.Module,hal_py.ModulePinGroup)] dst: The pairs of module ID and pin group name with unknown bit order. :param bool enforce_continuous_bitorders: Set ``True`` to only allow for continuous bit orders, ``^`` to also allow bit orders that are not continuous. Defaults to ``True``. - :returns: A dict containing all known bit orders (including new and already known ones) on success, ``None`` otherwise. - :rtype: dict[tuple(hal_py.Module,hal_py.ModulePinGroup),dict[hal_py.Net,int]] or None + :returns: All known bit orders, the new ones as well as the ones already known, on success, ``None`` otherwise. + :rtype: bitorder_propagation.BitOrderResult or None )"); m.def( "reorder_module_pin_groups", - [](const std::map*>, std::map>& ordered_module_pin_groups) -> bool { + [](const bitorder_propagation::BitOrderResult& ordered_module_pin_groups) -> bool { const auto res = bitorder_propagation::reorder_module_pin_groups(ordered_module_pin_groups); if (res.is_ok()) { @@ -116,14 +231,14 @@ namespace hal R"( Reorder and rename the pins of the pin groups according to the provided bit-order information. - :param dict[tuple(hal_py.Module,hal_py.ModulePinGroup),dict[hal_py.Net,int]] ordered_module_pin_groups: A mapping from pairs of modules and their pin groups to known bit-order information given as a mapping from nets to their index. + :param bitorder_propagation.BitOrderResult ordered_module_pin_groups: The bit orders to apply. :returns: ``True`` on success, ``False`` otherwise. :rtype: bool )"); m.def( "propagate_bitorder", - [](Netlist* nl, const std::pair& src, const std::pair& dst) -> std::optional*>, std::map>> { + [](Netlist* nl, const std::pair& src, const std::pair& dst) -> std::optional { const auto res = bitorder_propagation::propagate_bitorder(nl, src, dst); if (res.is_ok()) { @@ -154,7 +269,7 @@ namespace hal m.def( "propagate_bitorder", [](const std::pair*>& src, - const std::pair*>& dst) -> std::optional*>, std::map>> { + const std::pair*>& dst) -> std::optional { const auto res = bitorder_propagation::propagate_bitorder(src, dst); if (res.is_ok()) { @@ -184,7 +299,7 @@ namespace hal "propagate_bitorder", [](Netlist* nl, const std::vector>& src, - const std::vector>& dst) -> std::optional*>, std::map>> { + const std::vector>& dst) -> std::optional { const auto res = bitorder_propagation::propagate_bitorder(nl, src, dst); if (res.is_ok()) { @@ -215,7 +330,7 @@ namespace hal m.def( "propagate_bitorder", [](const std::vector*>>& src, - const std::vector*>>& dst) -> std::optional*>, std::map>> { + const std::vector*>>& dst) -> std::optional { const auto res = bitorder_propagation::propagate_bitorder(src, dst); if (res.is_ok()) { @@ -243,7 +358,7 @@ namespace hal m.def( "export_bitorder_propagation_information", - [](const std::map*>, std::map>& src, + [](const bitorder_propagation::BitOrderResult& src, const std::set*>>& dst, const std::string& export_filepath) -> std::optional*>, u32>> { const auto res = bitorder_propagation::export_bitorder_propagation_information(src, dst, export_filepath); @@ -263,7 +378,7 @@ namespace hal R"( Export collected bitorder information like word composition, known bitorder and connectivity in ``.json`` format to solve with external tools. - :param dict[tuple(hal_py.Module,hal_py.ModulePinGroup),dict[hal_py.Net,int]] src: The known indices for the nets belonging to the given module pin groups. + :param bitorder_propagation.BitOrderResult src: The bit orders that are already known. :param set[tuple(hal_py.Module,hal_py.ModulePinGroup)] dst: The pairs of module ID and pin group name with unknown bit order. :param str export_filepath: The filepath where the ``.json`` file should be written to. :returns: The mapping from each mdoule/pingroup pair to its index on success, ``None`` otherwise. diff --git a/plugins/bitorder_propagation/src/bit_order.cpp b/plugins/bitorder_propagation/src/bit_order.cpp new file mode 100644 index 000000000000..cfe358b3a494 --- /dev/null +++ b/plugins/bitorder_propagation/src/bit_order.cpp @@ -0,0 +1,154 @@ +#include "bitorder_propagation/bit_order.h" + +#include "hal_core/netlist/module.h" +#include "hal_core/netlist/net.h" + +#include + +namespace hal +{ + namespace bitorder_propagation + { + BitOrder::BitOrder(Module* module, PinGroup* pin_group, std::vector> order) + : m_module(module), m_pin_group(pin_group), m_order(std::move(order)) + { + std::sort(m_order.begin(), m_order.end(), [](const auto& lhs, const auto& rhs) { return lhs.second < rhs.second; }); + } + + Module* BitOrder::get_module() const + { + return m_module; + } + + PinGroup* BitOrder::get_pin_group() const + { + return m_pin_group; + } + + const std::vector>& BitOrder::get_order() const + { + return m_order; + } + + std::optional BitOrder::get_index(const Net* net) const + { + const auto it = std::find_if(m_order.begin(), m_order.end(), [net](const auto& entry) { return entry.first == net; }); + return (it == m_order.end()) ? std::nullopt : std::optional(it->second); + } + + Net* BitOrder::get_net_at(u32 index) const + { + const auto it = std::find_if(m_order.begin(), m_order.end(), [index](const auto& entry) { return entry.second == index; }); + return (it == m_order.end()) ? nullptr : it->first; + } + + u32 BitOrder::get_size() const + { + return m_order.size(); + } + + bool BitOrder::is_continuous() const + { + // m_order is sorted by index, so it suffices that the indices are 0, 1, ... without repetition. + for (u32 i = 0; i < m_order.size(); i++) + { + if (m_order.at(i).second != i) + { + return false; + } + } + return true; + } + + bool BitOrder::operator==(const BitOrder& other) const + { + return (m_module == other.m_module) && (m_pin_group == other.m_pin_group) && (m_order == other.m_order); + } + + bool BitOrder::operator!=(const BitOrder& other) const + { + return !(*this == other); + } + + namespace + { + /// Order by module and pin group ID, so that a result reads the same from one run to the next. + bool precedes(const BitOrder& lhs, const Module* module, const PinGroup* pin_group) + { + const u32 lhs_module = lhs.get_module()->get_id(); + const u32 rhs_module = module->get_id(); + if (lhs_module != rhs_module) + { + return lhs_module < rhs_module; + } + return lhs.get_pin_group()->get_id() < pin_group->get_id(); + } + } // namespace + + BitOrderResult::BitOrderResult(std::vector bit_orders) + { + for (auto& bit_order : bit_orders) + { + add(std::move(bit_order)); + } + } + + void BitOrderResult::add(BitOrder bit_order) + { + const auto it = std::lower_bound(m_bit_orders.begin(), m_bit_orders.end(), bit_order, [](const BitOrder& lhs, const BitOrder& rhs) { + return precedes(lhs, rhs.get_module(), rhs.get_pin_group()); + }); + + if ((it != m_bit_orders.end()) && (it->get_module() == bit_order.get_module()) && (it->get_pin_group() == bit_order.get_pin_group())) + { + *it = std::move(bit_order); + return; + } + + m_bit_orders.insert(it, std::move(bit_order)); + } + + const std::vector& BitOrderResult::get_bit_orders() const + { + return m_bit_orders; + } + + const BitOrder* BitOrderResult::get(const Module* module, const PinGroup* pin_group) const + { + const auto it = std::lower_bound(m_bit_orders.begin(), m_bit_orders.end(), 0, [module, pin_group](const BitOrder& lhs, int) { + return precedes(lhs, module, pin_group); + }); + + if ((it != m_bit_orders.end()) && (it->get_module() == module) && (it->get_pin_group() == pin_group)) + { + return &(*it); + } + return nullptr; + } + + bool BitOrderResult::contains(const Module* module, const PinGroup* pin_group) const + { + return get(module, pin_group) != nullptr; + } + + u32 BitOrderResult::get_size() const + { + return m_bit_orders.size(); + } + + bool BitOrderResult::is_empty() const + { + return m_bit_orders.empty(); + } + + std::vector::const_iterator BitOrderResult::begin() const + { + return m_bit_orders.begin(); + } + + std::vector::const_iterator BitOrderResult::end() const + { + return m_bit_orders.end(); + } + } // namespace bitorder_propagation +} // namespace hal diff --git a/plugins/bitorder_propagation/src/bitorder_propagation.cpp b/plugins/bitorder_propagation/src/bitorder_propagation.cpp index d733afc23557..c51a61a2bafc 100644 --- a/plugins/bitorder_propagation/src/bitorder_propagation.cpp +++ b/plugins/bitorder_propagation/src/bitorder_propagation.cpp @@ -1,4 +1,6 @@ #include "bitorder_propagation/bitorder_propagation.h" + +#include "bitorder_propagation/bit_order.h" #include "hal_core/netlist/decorators/boolean_function_net_decorator.h" #include "hal_core/netlist/gate.h" #include "hal_core/netlist/module.h" @@ -852,9 +854,41 @@ namespace hal } // namespace - Result>> - propagate_module_pingroup_bitorder(const std::map>& known_bitorders, const std::set& unknown_bitorders, const bool enforce_continuous_bitorders) + namespace + { + /// The algorithm below works on a map of pin groups to net indices. Translate at the boundary rather + /// than rewrite 1600 lines of it, so that the interface can change without the behaviour doing so. + std::map> to_internal(const BitOrderResult& bit_orders) + { + std::map> res; + for (const auto& bit_order : bit_orders) + { + std::map indices; + for (const auto& [net, index] : bit_order.get_order()) + { + indices.insert({net, index}); + } + res.insert({{bit_order.get_module(), bit_order.get_pin_group()}, std::move(indices)}); + } + return res; + } + + BitOrderResult from_internal(const std::map>& bit_orders) + { + BitOrderResult res; + for (const auto& [mpg, indices] : bit_orders) + { + res.add(BitOrder(mpg.first, mpg.second, {indices.begin(), indices.end()})); + } + return res; + } + } // namespace + + Result + propagate_module_pingroup_bitorder(const BitOrderResult& src, const std::set& unknown_bitorders, const bool enforce_continuous_bitorders) { + const std::map> known_bitorders = to_internal(src); + // std::unordered_map, std::vector>>, boost::hash>>> connectivity_inwards; // std::unordered_map, std::vector>>, boost::hash>>> connectivity_outwards; @@ -1230,11 +1264,13 @@ namespace hal log_info("bitorder_propagation", "Found a valid bitorder for {} pingroups.", wellformed_module_pin_groups.size()); - return OK(wellformed_module_pin_groups); + return OK(from_internal(wellformed_module_pin_groups)); } - Result reorder_module_pin_groups(const std::map>& ordered_module_pin_groups) + Result reorder_module_pin_groups(const BitOrderResult& bit_orders) { + const std::map> ordered_module_pin_groups = to_internal(bit_orders); + // reorder pin groups to match found bit orders for (const auto& [mpg, bitorder] : ordered_module_pin_groups) { @@ -1284,14 +1320,14 @@ namespace hal return OK({}); } - Result*>, std::map>> propagate_bitorder(Netlist* nl, const std::pair& src, const std::pair& dst) + Result propagate_bitorder(Netlist* nl, const std::pair& src, const std::pair& dst) { const std::vector> src_vec = {src}; const std::vector> dst_vec = {dst}; return propagate_bitorder(nl, src_vec, dst_vec); } - Result*>, std::map>> propagate_bitorder(const std::pair*>& src, + Result propagate_bitorder(const std::pair*>& src, const std::pair*>& dst) { if (!src.second) @@ -1307,7 +1343,7 @@ namespace hal return propagate_bitorder(src_vec, dst_vec); } - Result*>, std::map>> + Result propagate_bitorder(Netlist* nl, const std::vector>& src, const std::vector>& dst) { std::vector*>> internal_src; @@ -1381,7 +1417,7 @@ namespace hal return propagate_bitorder(internal_src, internal_dst); } - Result*>, std::map>> propagate_bitorder(const std::vector*>>& src, + Result propagate_bitorder(const std::vector*>>& src, const std::vector*>>& dst) { std::map> known_bitorders; @@ -1409,7 +1445,7 @@ namespace hal } // actually propagate the bit order - const auto res = propagate_module_pingroup_bitorder(known_bitorders, unknown_bitorders); + const auto res = propagate_module_pingroup_bitorder(from_internal(known_bitorders), unknown_bitorders); if (res.is_error()) { return ERR_APPEND(res.get_error(), "cannot propagate bit order: failed propagation"); @@ -1437,7 +1473,7 @@ namespace hal #endif // print stats - const u32 all_wellformed_bitorders_count = all_wellformed_module_pin_groups.size(); + const u32 all_wellformed_bitorders_count = all_wellformed_module_pin_groups.get_size(); const u32 new_bit_order_count = all_wellformed_bitorders_count - src.size(); log_info("bitorder_propagation", "reconstructed {} unknown bit orders from {} known bit orders", new_bit_order_count, src.size()); @@ -1451,7 +1487,7 @@ namespace hal return OK(all_wellformed_module_pin_groups); } - Result> export_bitorder_propagation_information(const std::vector*>>& src, + Result> export_bitorder_propagation_information(const std::vector*>>& src, const std::vector*>>& dst, const std::string& export_filepath) { @@ -1479,13 +1515,15 @@ namespace hal known_bitorders.insert({{m, pg}, src_bitorder}); } - return export_bitorder_propagation_information(known_bitorders, unknown_bitorders, export_filepath); + return export_bitorder_propagation_information(from_internal(known_bitorders), unknown_bitorders, export_filepath); } - Result> export_bitorder_propagation_information(const std::map*>, std::map>& known_bitorders, - const std::set*>>& unknown_bitorders, - const std::string& export_filepath) + Result> export_bitorder_propagation_information(const BitOrderResult& src, + const std::set*>>& unknown_bitorders, + const std::string& export_filepath) { + const std::map> known_bitorders = to_internal(src); + std::map, std::vector>>> connectivity_inwards; std::map, std::vector>>> connectivity_outwards; diff --git a/plugins/bitorder_propagation/test/CMakeLists.txt b/plugins/bitorder_propagation/test/CMakeLists.txt new file mode 100644 index 000000000000..91b9dc55f5e4 --- /dev/null +++ b/plugins/bitorder_propagation/test/CMakeLists.txt @@ -0,0 +1,13 @@ +if(BUILD_TESTS) + include_directories(${gtest_SOURCE_DIR}/include ${gtest_SOURCE_DIR} ${CMAKE_SOURCE_DIR}/include ${CMAKE_SOURCE_DIR}/tests ${CMAKE_SOURCE_DIR}/plugins/bitorder_propagation/include) + + add_executable(runTest-bitorder_propagation bitorder_propagation.cpp) + + target_link_libraries(runTest-bitorder_propagation bitorder_propagation pthread gtest hal::core hal::netlist test_utils) + + add_test(runTest-bitorder_propagation ${CMAKE_BINARY_DIR}/bin/hal_plugins/runTest-bitorder_propagation --gtest_output=xml:${CMAKE_BINARY_DIR}/gtestresults-runBasicTests.xml) + + if(${CMAKE_BUILD_TYPE} STREQUAL "Debug") + add_sanitizers(runTest-bitorder_propagation) + endif() +endif() diff --git a/plugins/bitorder_propagation/test/bitorder_propagation.cpp b/plugins/bitorder_propagation/test/bitorder_propagation.cpp new file mode 100644 index 000000000000..65b8f2399b1c --- /dev/null +++ b/plugins/bitorder_propagation/test/bitorder_propagation.cpp @@ -0,0 +1,298 @@ +#include "bitorder_propagation/bitorder_propagation.h" + +#include "gate_library_test_utils.h" +#include "hal_core/netlist/module.h" +#include "hal_core/netlist/net.h" +#include "hal_core/netlist/netlist.h" +#include "netlist_test_utils.h" + +#include + +namespace hal +{ + /** + * Tests of the bit-order propagation. + * + * These describe what the plugin does today rather than what it ought to do, so that the types its + * interface is written in can be replaced without the behaviour changing unnoticed. The plugin had + * no tests at all before. + */ + class BitorderPropagationTest : public ::testing::Test + { + protected: + virtual void SetUp() + { + NO_COUT_BLOCK; + test_utils::init_log_channels(); + test_utils::create_sandbox_directory(); + } + + virtual void TearDown() + { + test_utils::remove_sandbox_directory(); + } + + /** + * A netlist of two modules joined by a bus of `width` nets: `width` buffers inside the source + * module each drive one net, and `width` buffers inside the destination module each read one. + * + * The nets are handed over in the order they were created, so a test can state a bit order for + * one side and check what the other side ends up with. + */ + struct Fixture + { + std::unique_ptr netlist; + Module* src_module = nullptr; + Module* dst_module = nullptr; + PinGroup* src_pin_group = nullptr; + PinGroup* dst_pin_group = nullptr; + std::vector bus; + }; + + Fixture build_bus(u32 width) + { + Fixture f; + f.netlist = test_utils::create_empty_netlist(); + const GateLibrary* gl = f.netlist->get_gate_library(); + + std::vector src_gates, dst_gates; + for (u32 i = 0; i < width; i++) + { + Gate* driver = f.netlist->create_gate(gl->get_gate_type_by_name("BUF"), "driver_" + std::to_string(i)); + Gate* reader = f.netlist->create_gate(gl->get_gate_type_by_name("BUF"), "reader_" + std::to_string(i)); + src_gates.push_back(driver); + dst_gates.push_back(reader); + + Net* n = test_utils::connect(f.netlist.get(), driver, "O", reader, "I", "bus_" + std::to_string(i)); + f.bus.push_back(n); + + // Give each buffer something to read, so that the source module has an input as well. + Net* stimulus = f.netlist->create_net("stimulus_" + std::to_string(i)); + stimulus->add_destination(driver, "I"); + stimulus->mark_global_input_net(); + } + + f.src_module = f.netlist->create_module("src", f.netlist->get_top_module(), src_gates); + f.dst_module = f.netlist->create_module("dst", f.netlist->get_top_module(), dst_gates); + + // A net crossing a module boundary gets a pin of its own, and each pin a group of its own. + // Collect them into one group per side, which is what a bus looks like and what the + // propagation works on. + std::vector src_pins, dst_pins; + for (auto* n : f.bus) + { + src_pins.push_back(f.src_module->get_pin_by_net(n)); + dst_pins.push_back(f.dst_module->get_pin_by_net(n)); + } + + // Ascending from 0, so that the group is indexed 0..width-1 like a bus. The default is + // descending from 0, which indexes the group 0, -1, -2, ... and leaves it unable to accept + // any positive index later on. + auto src_group = f.src_module->create_pin_group("OUT", src_pins, PinDirection::output, PinType::none, true, 0); + auto dst_group = f.dst_module->create_pin_group("IN", dst_pins, PinDirection::input, PinType::none, true, 0); + f.src_pin_group = src_group.is_ok() ? src_group.get() : nullptr; + f.dst_pin_group = dst_group.is_ok() ? dst_group.get() : nullptr; + return f; + } + }; + + /** + * A pin group whose bit order is known hands that order to the pin group it drives. + * + * Functions: propagate_module_pingroup_bitorder + */ + TEST_F(BitorderPropagationTest, check_propagate_to_connected_pin_group) + { + TEST_START + { + Fixture f = build_bus(4); + ASSERT_NE(f.netlist, nullptr); + + ASSERT_NE(f.src_pin_group, nullptr); + ASSERT_NE(f.dst_pin_group, nullptr); + ASSERT_EQ(f.src_pin_group->get_pins().size(), 4); + ASSERT_EQ(f.dst_pin_group->get_pins().size(), 4); + + std::vector> order; + for (u32 i = 0; i < f.bus.size(); i++) + { + order.push_back({f.bus.at(i), i}); + } + + bitorder_propagation::BitOrderResult known({bitorder_propagation::BitOrder(f.src_module, f.src_pin_group, order)}); + + auto res = bitorder_propagation::propagate_module_pingroup_bitorder(known, {{f.dst_module, f.dst_pin_group}}); + ASSERT_TRUE(res.is_ok()); + + const auto* propagated = res.get().get(f.dst_module, f.dst_pin_group); + ASSERT_NE(propagated, nullptr); + EXPECT_EQ(propagated->get_order(), order); + } + TEST_END + } + + /** + * A bit order with gaps in it is rejected unless non-continuous orders are allowed. + * + * Functions: propagate_module_pingroup_bitorder + */ + TEST_F(BitorderPropagationTest, check_continuous_bitorder_is_enforced_on_request) + { + TEST_START + { + // Indices 0, 1, 2 and 4: a bus of four nets whose order leaves a hole at 3. + const std::vector indices = {0, 1, 2, 4}; + + for (const bool enforce_continuous : {true, false}) + { + Fixture f = build_bus(4); + ASSERT_NE(f.netlist, nullptr); + ASSERT_NE(f.src_pin_group, nullptr); + + std::vector> order; + for (u32 i = 0; i < f.bus.size(); i++) + { + order.push_back({f.bus.at(i), indices.at(i)}); + } + + bitorder_propagation::BitOrderResult known({bitorder_propagation::BitOrder(f.src_module, f.src_pin_group, order)}); + EXPECT_FALSE(known.get_bit_orders().front().is_continuous()); + + auto res = bitorder_propagation::propagate_module_pingroup_bitorder(known, {{f.dst_module, f.dst_pin_group}}, enforce_continuous); + ASSERT_TRUE(res.is_ok()); + + const auto* propagated = res.get().get(f.dst_module, f.dst_pin_group); + + if (enforce_continuous) + { + // The hole makes the order invalid, so nothing is reconstructed for the destination. + EXPECT_EQ(propagated, nullptr); + } + else + { + // The destination is reconstructed, and its indices come out continuous even so: + // what the flag permits is accepting an order with a hole in it as input, not + // carrying that hole over to what is reconstructed from it. + ASSERT_NE(propagated, nullptr); + EXPECT_TRUE(propagated->is_continuous()); + EXPECT_EQ(propagated->get_size(), 4); + } + } + } + TEST_END + } + + /** + * Propagating to a pin group that is already known leaves it alone and reports it back unchanged. + * + * Functions: propagate_module_pingroup_bitorder + */ + TEST_F(BitorderPropagationTest, check_known_bitorder_is_reported_back) + { + TEST_START + { + Fixture f = build_bus(4); + ASSERT_NE(f.netlist, nullptr); + ASSERT_NE(f.src_pin_group, nullptr); + + std::vector> order; + for (u32 i = 0; i < f.bus.size(); i++) + { + order.push_back({f.bus.at(i), i}); + } + + bitorder_propagation::BitOrderResult known({bitorder_propagation::BitOrder(f.src_module, f.src_pin_group, order)}); + + auto res = bitorder_propagation::propagate_module_pingroup_bitorder(known, {{f.dst_module, f.dst_pin_group}}); + ASSERT_TRUE(res.is_ok()); + + // The result carries the orders that were already known as well as the ones just found. + const auto& all = res.get(); + EXPECT_EQ(all.get_size(), 2); + const auto* reported = all.get(f.src_module, f.src_pin_group); + ASSERT_NE(reported, nullptr); + EXPECT_EQ(reported->get_order(), order); + } + TEST_END + } + + /** + * Reordering renames the pins of a group so that their names carry the propagated indices. + * + * Functions: reorder_module_pin_groups + */ + TEST_F(BitorderPropagationTest, check_reorder_renames_pins) + { + TEST_START + { + Fixture f = build_bus(4); + ASSERT_NE(f.netlist, nullptr); + ASSERT_NE(f.dst_pin_group, nullptr); + + std::vector> order; + for (u32 i = 0; i < f.bus.size(); i++) + { + order.push_back({f.bus.at(i), i}); + } + + bitorder_propagation::BitOrderResult to_apply({bitorder_propagation::BitOrder(f.dst_module, f.dst_pin_group, order)}); + + auto res = bitorder_propagation::reorder_module_pin_groups(to_apply); + ASSERT_TRUE(res.is_ok()); + + // Every net of the bus now sits at the index it was given, and the group counts as ordered. + auto* group = f.dst_module->get_pin_by_net(f.bus.front())->get_group().first; + ASSERT_NE(group, nullptr); + EXPECT_EQ(group->get_pins().size(), 4); + for (u32 i = 0; i < f.bus.size(); i++) + { + auto* pin = f.dst_module->get_pin_by_net(f.bus.at(i)); + ASSERT_NE(pin, nullptr); + EXPECT_EQ(pin->get_group().first, group); + EXPECT_EQ(pin->get_group().second, i); + } + } + TEST_END + } + + /** + * The export writes the problem out as json and reports which word each pin group became. + * + * Functions: export_bitorder_propagation_information + */ + TEST_F(BitorderPropagationTest, check_export_writes_the_problem) + { + TEST_START + { + Fixture f = build_bus(4); + ASSERT_NE(f.netlist, nullptr); + ASSERT_NE(f.src_pin_group, nullptr); + + std::vector> order; + for (u32 i = 0; i < f.bus.size(); i++) + { + order.push_back({f.bus.at(i), i}); + } + + bitorder_propagation::BitOrderResult known({bitorder_propagation::BitOrder(f.src_module, f.src_pin_group, order)}); + + const std::string path = test_utils::create_sandbox_path("bitorder_export.json").string(); + auto res = bitorder_propagation::export_bitorder_propagation_information(known, {{f.dst_module, f.dst_pin_group}}, path); + ASSERT_TRUE(res.is_ok()); + + // Every pin group involved is reported with the index of the word it became in the file. + const auto& word_of = res.get(); + EXPECT_EQ(word_of.size(), 2); + EXPECT_NE(word_of.find({f.src_module, f.src_pin_group}), word_of.end()); + EXPECT_NE(word_of.find({f.dst_module, f.dst_pin_group}), word_of.end()); + + std::ifstream file(path); + ASSERT_TRUE(file.is_open()); + const std::string content((std::istreambuf_iterator(file)), std::istreambuf_iterator()); + EXPECT_NE(content.find("word_definitions"), std::string::npos); + EXPECT_NE(content.find("known_bit_order"), std::string::npos); + EXPECT_NE(content.find("connected_words"), std::string::npos); + } + TEST_END + } +} // namespace hal diff --git a/src/netlist/boolean_function/solver.cpp b/src/netlist/boolean_function/solver.cpp index c0ba0afa2ddb..0ae33dc15867 100644 --- a/src/netlist/boolean_function/solver.cpp +++ b/src/netlist/boolean_function/solver.cpp @@ -376,23 +376,13 @@ namespace hal { if (call == SolverCall::Binary) { - switch (auto it = type2query_binary.find(type); it != type2query_binary.end()) - { - case true: - return it->second().is_ok(); - default: - return false; - } + const auto it = type2query_binary.find(type); + return (it != type2query_binary.end()) && it->second().is_ok(); } - else if (call == SolverCall::Binary) + else if (call == SolverCall::Library) { - switch (auto it = type2link_status.find(type); it != type2link_status.end()) - { - case true: - return it->second; - default: - return false; - } + const auto it = type2link_status.find(type); + return (it != type2link_status.end()) && it->second; } return false; diff --git a/src/netlist/boolean_function/symbolic_state.cpp b/src/netlist/boolean_function/symbolic_state.cpp index 27bd0d25a1ff..5f2f749db62c 100644 --- a/src/netlist/boolean_function/symbolic_state.cpp +++ b/src/netlist/boolean_function/symbolic_state.cpp @@ -39,7 +39,10 @@ namespace hal { if (key.is_variable()) { - this->variable.emplace(std::move(key), std::move(value)); + // insert_or_assign, not emplace: emplace leaves an existing binding untouched, so + // setting a variable a second time did nothing and a loop that steps a state forward + // silently kept the value it started with. + this->variable.insert_or_assign(key.clone(), value.clone()); } } } // namespace SMT diff --git a/src/plugin_system/plugin_manager.cpp b/src/plugin_system/plugin_manager.cpp index 7c7d642544fe..f006b9a64fc0 100644 --- a/src/plugin_system/plugin_manager.cpp +++ b/src/plugin_system/plugin_manager.cpp @@ -27,8 +27,43 @@ namespace hal { namespace { + /** + * A loaded plugin and the library it was loaded from. + * + * Exists so that the library can be kept open when the map is torn down at exit, which a + * std::tuple of the two gives no way to express. See the destructor. + */ + struct LoadedPlugin + { + std::unique_ptr instance; + std::unique_ptr library; + + /** + * Lets go of the library rather than unloading it. + * + * This only does anything while the process is exiting: unload() moves both pointers out + * before it erases an entry, so on that path there is nothing left here to destroy. + * + * Unloading at exit is not merely pointless but wrong. The netlist parser and writer + * registries hold a std::function per plugin that provides one, those registries live in + * libhal_netlist and are destroyed after this map is, and closing the libraries here left + * every one of those functions pointing into memory that had just been unmapped, which + * segfaulted on the way out. + */ + ~LoadedPlugin() + { + (void)library.release(); + } + + LoadedPlugin() = default; + LoadedPlugin(LoadedPlugin&&) = default; + LoadedPlugin& operator=(LoadedPlugin&&) = default; + LoadedPlugin(const LoadedPlugin&) = delete; + LoadedPlugin& operator=(const LoadedPlugin&) = delete; + }; + // stores library and factory identified by plugin name) - std::unordered_map, std::unique_ptr>> m_loaded_plugins; + std::unordered_map m_loaded_plugins; // stores special features offered by plugin std::unordered_map> m_plugin_features; @@ -315,7 +350,7 @@ namespace hal } m_current_loading.clear(); - m_loaded_plugins[plugin_name] = std::make_tuple(std::move(instance), std::move(lib)); + m_loaded_plugins[plugin_name] = LoadedPlugin{std::move(instance), std::move(lib)}; /* notify callback that a plugin was loaded*/ m_hook(true, plugin_name, file_path.string()); @@ -355,8 +390,8 @@ namespace hal log_info("core", "unloading plugin '{}'...", plugin_name); - auto rt_library = std::move(std::get<1>(loaded_it->second)); - auto plugin_inst = std::move(std::get<0>(loaded_it->second)); + auto rt_library = std::move(loaded_it->second.library); + auto plugin_inst = std::move(loaded_it->second.instance); { auto iplugType = dynamic_cast(plugin_inst.get()) ? 1 : 0; @@ -428,7 +463,7 @@ namespace hal return nullptr; } - auto instance = std::get<0>(it->second).get(); + auto instance = it->second.instance.get(); if (instance != nullptr && initialize) { instance->initialize(); @@ -440,7 +475,7 @@ namespace hal { for (const auto& [_, plugin] : m_loaded_plugins) { - if (auto* ui_plugin = dynamic_cast(std::get<0>(plugin).get()); ui_plugin != nullptr) + if (auto* ui_plugin = dynamic_cast(plugin.instance.get()); ui_plugin != nullptr) { return ui_plugin; } diff --git a/src/python_bindings/bindings/base_pin.cpp b/src/python_bindings/bindings/base_pin.cpp index 86ecd6c7f4c0..ad24a4c260ad 100644 --- a/src/python_bindings/bindings/base_pin.cpp +++ b/src/python_bindings/bindings/base_pin.cpp @@ -81,7 +81,7 @@ namespace hal :rtype: hal_py.PinType )"); - py_gate_base_pin.def_property_readonly("group", &BasePin::get_group, borrowed(), R"( + py_gate_base_pin.def_property_readonly("group", py::cpp_function(&BasePin::get_group, py::is_method(py_gate_base_pin), borrowed()), R"( A tuple comprising the group of the pin as well as the index of the pin within the group. :type: tuple(hal_py.GatePinGroup,int) @@ -171,7 +171,7 @@ namespace hal :rtype: hal_py.PinType )"); - py_module_base_pin.def_property_readonly("group", &BasePin::get_group, borrowed(), R"( + py_module_base_pin.def_property_readonly("group", py::cpp_function(&BasePin::get_group, py::is_method(py_module_base_pin), borrowed()), R"( A tuple comprising the group of the pin as well as the index of the pin within the group. :type: tuple(hal_py.ModulePinGroup,int) diff --git a/src/python_bindings/bindings/endpoint.cpp b/src/python_bindings/bindings/endpoint.cpp index 972b47260be3..7833a476800f 100644 --- a/src/python_bindings/bindings/endpoint.cpp +++ b/src/python_bindings/bindings/endpoint.cpp @@ -8,7 +8,7 @@ namespace hal An endpoint comprises the pin of a gate, the respective gate, and the connected net. )"); - py_endpoint.def_property_readonly("gate", &Endpoint::get_gate, borrowed(), R"( + py_endpoint.def_property_readonly("gate", py::cpp_function(&Endpoint::get_gate, py::is_method(py_endpoint), borrowed()), R"( The gate associated with the endpoint. :type: hal_py.Gate @@ -35,7 +35,7 @@ namespace hal :rtype: hal_py.Gate )"); - py_endpoint.def_property_readonly("pin", &Endpoint::get_pin, borrowed(), R"( + py_endpoint.def_property_readonly("pin", py::cpp_function(&Endpoint::get_pin, py::is_method(py_endpoint), borrowed()), R"( The pin associated with the endpoint. :type: hal_py.GatePin @@ -48,7 +48,7 @@ namespace hal :rtype: hal_py.GatePin )"); - py_endpoint.def_property_readonly("net", &Endpoint::get_net, borrowed(), R"( + py_endpoint.def_property_readonly("net", py::cpp_function(&Endpoint::get_net, py::is_method(py_endpoint), borrowed()), R"( The net associated with the endpoint. :type: hal_py.Net diff --git a/src/python_bindings/bindings/gate.cpp b/src/python_bindings/bindings/gate.cpp index e78bd61aaf0a..adc1317d1071 100644 --- a/src/python_bindings/bindings/gate.cpp +++ b/src/python_bindings/bindings/gate.cpp @@ -159,7 +159,7 @@ namespace hal :param tuple(int,int) location: A tuple . )"); - py_gate.def_property_readonly("module", &Gate::get_module, borrowed(), R"( + py_gate.def_property_readonly("module", py::cpp_function(&Gate::get_module, py::is_method(py_gate), borrowed()), R"( The module in which contains this gate. :type: hal_py.Module @@ -172,7 +172,7 @@ namespace hal :rtype: hal_py.Module )"); - py_gate.def_property_readonly("modules", [](Gate* g) { return g->get_modules(); }, borrowed(), R"( + py_gate.def_property_readonly("modules", py::cpp_function([](Gate* g) { return g->get_modules(); }, py::is_method(py_gate), borrowed()), R"( A list of all modules that contain this gate, either directly or as parent of another module. :type: list[hal_py.Module] @@ -306,7 +306,7 @@ namespace hal :rtype: bool )"); - py_gate.def_property_readonly("fan_in_nets", py::overload_cast<>(&Gate::get_fan_in_nets, py::const_), borrowed(), R"( + py_gate.def_property_readonly("fan_in_nets", py::cpp_function(py::overload_cast<>(&Gate::get_fan_in_nets, py::const_), py::is_method(py_gate), borrowed()), R"( A list of all fan-in nets of the gate, i.e., all nets that are connected to one of the input pins. :type: list[hal_py.Net] @@ -352,7 +352,7 @@ namespace hal :rtype: bool )"); - py_gate.def_property_readonly("fan_in_endpoints", py::overload_cast<>(&Gate::get_fan_in_endpoints, py::const_), borrowed(), R"( + py_gate.def_property_readonly("fan_in_endpoints", py::cpp_function(py::overload_cast<>(&Gate::get_fan_in_endpoints, py::const_), py::is_method(py_gate), borrowed()), R"( A list of all fan-in endpoints of the gate, i.e., all endpoints associated with an input pin of the gate. :type: list[hal_py.Endpoint] @@ -398,7 +398,7 @@ namespace hal :rtype: hal_py.Endpoint or None )"); - py_gate.def_property_readonly("fan_out_nets", py::overload_cast<>(&Gate::get_fan_out_nets, py::const_), borrowed(), R"( + py_gate.def_property_readonly("fan_out_nets", py::cpp_function(py::overload_cast<>(&Gate::get_fan_out_nets, py::const_), py::is_method(py_gate), borrowed()), R"( A list of all fan-out nets of the gate, i.e., all nets that are connected to one of the output pins. :type: list[hal_py.Net] @@ -444,7 +444,7 @@ namespace hal :rtype: bool )"); - py_gate.def_property_readonly("fan_out_endpoints", py::overload_cast<>(&Gate::get_fan_out_endpoints, py::const_), borrowed(), R"( + py_gate.def_property_readonly("fan_out_endpoints", py::cpp_function(py::overload_cast<>(&Gate::get_fan_out_endpoints, py::const_), py::is_method(py_gate), borrowed()), R"( A list of all fan-out endpoints of the gate, i.e., all endpoints associated with an output pin of the gate. :type: list[hal_py.Endpoint] @@ -490,7 +490,7 @@ namespace hal :rtype: hal_py.Endpoint or None )"); - py_gate.def_property_readonly("unique_predecessors", [](Gate* g) { return g->get_unique_predecessors(); }, borrowed(), R"( + py_gate.def_property_readonly("unique_predecessors", py::cpp_function([](Gate* g) { return g->get_unique_predecessors(); }, py::is_method(py_gate), borrowed()), R"( A list of all unique predecessor gates of the gate. :type: list[hal_py.Gate] @@ -505,7 +505,7 @@ namespace hal :rtype: list[hal_py.Gate] )"); - py_gate.def_property_readonly("predecessors", [](Gate* g) { return g->get_predecessors(); }, borrowed(), R"( + py_gate.def_property_readonly("predecessors", py::cpp_function([](Gate* g) { return g->get_predecessors(); }, py::is_method(py_gate), borrowed()), R"( A list of all direct predecessor endpoints of the gate, i.e., all predecessor endpoints that are connected to an input pin of the gate. :type: list[hal_py.Endpoint] @@ -538,7 +538,7 @@ namespace hal :rtype: hal_py.Endpoint or None )"); - py_gate.def_property_readonly("unique_successors", [](Gate* g) { return g->get_unique_successors(); }, borrowed(), R"( + py_gate.def_property_readonly("unique_successors", py::cpp_function([](Gate* g) { return g->get_unique_successors(); }, py::is_method(py_gate), borrowed()), R"( A list of all unique successor gates of the gate. :type: list[hal_py.Gate] @@ -553,7 +553,7 @@ namespace hal :rtype: list[hal_py.Gate] )"); - py_gate.def_property_readonly("successors", [](Gate* g) { return g->get_successors(); }, borrowed(), R"( + py_gate.def_property_readonly("successors", py::cpp_function([](Gate* g) { return g->get_successors(); }, py::is_method(py_gate), borrowed()), R"( A list of all direct successor endpoints of the gate, i.e., all successor endpoints that are connected to an output pin of the gate. :type: list[hal_py.Endpoint] diff --git a/src/python_bindings/bindings/gate_library.cpp b/src/python_bindings/bindings/gate_library.cpp index b20a9cbe4f34..b43902f5b0e1 100644 --- a/src/python_bindings/bindings/gate_library.cpp +++ b/src/python_bindings/bindings/gate_library.cpp @@ -101,7 +101,7 @@ namespace hal :rtype: hal_py.GateType or None )"); - py_gate_library.def_property_readonly("gate_types", [](const GateLibrary& self) { return self.get_gate_types(); }, borrowed(), R"( + py_gate_library.def_property_readonly("gate_types", py::cpp_function([](const GateLibrary& self) { return self.get_gate_types(); }, py::is_method(py_gate_library), borrowed()), R"( All gate types of the gate library as as dict from gate type names to gate types. :type: dict[str,hal_py.GateType] @@ -124,7 +124,7 @@ namespace hal :rtype: bool )"); - py_gate_library.def_property_readonly("vcc_gate_types", &GateLibrary::get_vcc_gate_types, borrowed(), R"( + py_gate_library.def_property_readonly("vcc_gate_types", py::cpp_function(&GateLibrary::get_vcc_gate_types, py::is_method(py_gate_library), borrowed()), R"( All VCC gate types of the gate library as as dict from gate type names to gate types. :type: dict[str,hal_py.GateType] @@ -145,7 +145,7 @@ namespace hal :rtype: bool )"); - py_gate_library.def_property_readonly("gnd_gate_types", &GateLibrary::get_vcc_gate_types, borrowed(), R"( + py_gate_library.def_property_readonly("gnd_gate_types", py::cpp_function(&GateLibrary::get_vcc_gate_types, py::is_method(py_gate_library), borrowed()), R"( All GND gate types of the gate library as as dict from gate type names to gate types. :type: dict[str,hal_py.GateType] diff --git a/src/python_bindings/bindings/gate_pin_group.cpp b/src/python_bindings/bindings/gate_pin_group.cpp index a604a1555ee9..25a5b0649411 100644 --- a/src/python_bindings/bindings/gate_pin_group.cpp +++ b/src/python_bindings/bindings/gate_pin_group.cpp @@ -81,7 +81,7 @@ namespace hal :rtype: hal_py.PinType )"); - py_gate_pin_group.def_property_readonly("pins", [](const PinGroup& self) -> std::vector { return self.get_pins(nullptr); }, borrowed(), R"( + py_gate_pin_group.def_property_readonly("pins", py::cpp_function([](const PinGroup& self) -> std::vector { return self.get_pins(nullptr); }, py::is_method(py_gate_pin_group), borrowed()), R"( The (ordered) pins of the pin groups. :type: list[hal_py.GatePin] diff --git a/src/python_bindings/bindings/gate_type.cpp b/src/python_bindings/bindings/gate_type.cpp index 4404512e2a74..7740389f1fbc 100644 --- a/src/python_bindings/bindings/gate_type.cpp +++ b/src/python_bindings/bindings/gate_type.cpp @@ -96,7 +96,7 @@ namespace hal )"); py_gate_type.def_property_readonly( - "components", [](const GateType& self) { return self.get_components(); }, borrowed(), R"( + "components", py::cpp_function([](const GateType& self) { return self.get_components(); }, py::is_method(py_gate_type), borrowed()), R"( All components of the gate type as a list. :type: list[hal_py.GateTypeComponent] @@ -186,7 +186,7 @@ namespace hal :rtype: bool )"); - py_gate_type.def_property_readonly("gate_library", &GateType::get_gate_library, borrowed(), R"( + py_gate_type.def_property_readonly("gate_library", py::cpp_function(&GateType::get_gate_library, py::is_method(py_gate_type), borrowed()), R"( The gate library this gate type is associated with. :type: hal_py.GateLibrary @@ -281,9 +281,7 @@ namespace hal )"); py_gate_type.def_property_readonly( - "pins", - [](const GateType& self) -> std::vector { return self.get_pins(); }, - borrowed(), R"( + "pins", py::cpp_function([](const GateType& self) -> std::vector { return self.get_pins(); }, py::is_method(py_gate_type), borrowed()), R"( An ordered list of all pins of the gate type. :type: list[hal_py.GatePin] @@ -317,7 +315,7 @@ namespace hal :rtype: list[str] )"); - py_gate_type.def_property_readonly("input_pins", &GateType::get_input_pins, borrowed(), R"( + py_gate_type.def_property_readonly("input_pins", py::cpp_function(&GateType::get_input_pins, py::is_method(py_gate_type), borrowed()), R"( An ordered list of all input pins of the gate type (including inout pins). :type: list[hal_py.GatePin] @@ -343,7 +341,7 @@ namespace hal :rtype: list[str] )"); - py_gate_type.def_property_readonly("output_pins", &GateType::get_output_pins, borrowed(), R"( + py_gate_type.def_property_readonly("output_pins", py::cpp_function(&GateType::get_output_pins, py::is_method(py_gate_type), borrowed()), R"( An ordered list of all output pins of the gate type (including inout pins). :type: list[hal_py.GatePin] diff --git a/src/python_bindings/bindings/gate_type_components.cpp b/src/python_bindings/bindings/gate_type_components.cpp index b3d9e65c7777..6b5b91b0dce1 100644 --- a/src/python_bindings/bindings/gate_type_components.cpp +++ b/src/python_bindings/bindings/gate_type_components.cpp @@ -30,7 +30,7 @@ namespace hal .value("ram_port", GateTypeComponent::ComponentType::ram_port, R"(RAM port component type.)") .export_values(); - py_gate_type_component.def_property_readonly("type", &GateTypeComponent::get_type, borrowed(), R"( + py_gate_type_component.def_property_readonly("type", py::cpp_function(&GateTypeComponent::get_type, py::is_method(py_gate_type_component), borrowed()), R"( The type of the gate type component. :type: hal_py.GateTypeComponent.ComponentType @@ -43,7 +43,7 @@ namespace hal :rtype: hal_py.GateTypeComponent.ComponentType )"); - py_gate_type_component.def_property_readonly("components", &GateTypeComponent::get_components, borrowed(), R"( + py_gate_type_component.def_property_readonly("components", py::cpp_function(&GateTypeComponent::get_components, py::is_method(py_gate_type_component), borrowed()), R"( All components of the gate type component as a list. :type: list[hal_py.GateTypeComponent] diff --git a/src/python_bindings/bindings/grouping.cpp b/src/python_bindings/bindings/grouping.cpp index 8104057a8d35..03d36b2821d1 100644 --- a/src/python_bindings/bindings/grouping.cpp +++ b/src/python_bindings/bindings/grouping.cpp @@ -80,7 +80,7 @@ namespace hal :rtype: bool )"); - py_grouping.def_property_readonly("gates", py::overload_cast<>(&Grouping::get_gates, py::const_), borrowed(), R"( + py_grouping.def_property_readonly("gates", py::cpp_function(py::overload_cast<>(&Grouping::get_gates, py::const_), py::is_method(py_grouping), borrowed()), R"( All gates contained within the grouping. :type: list[hal_py.Gate] @@ -174,7 +174,7 @@ namespace hal :rtype: bool )"); - py_grouping.def_property_readonly("nets", py::overload_cast<>(&Grouping::get_nets, py::const_), borrowed(), R"( + py_grouping.def_property_readonly("nets", py::cpp_function(py::overload_cast<>(&Grouping::get_nets, py::const_), py::is_method(py_grouping), borrowed()), R"( All nets contained within the grouping. :type: list[hal_py.Net] @@ -268,7 +268,7 @@ namespace hal :rtype: bool )"); - py_grouping.def_property_readonly("modules", py::overload_cast<>(&Grouping::get_modules, py::const_), borrowed(), R"( + py_grouping.def_property_readonly("modules", py::cpp_function(py::overload_cast<>(&Grouping::get_modules, py::const_), py::is_method(py_grouping), borrowed()), R"( All modules contained within the grouping. :type: list[hal_py.Module] diff --git a/src/python_bindings/bindings/module.cpp b/src/python_bindings/bindings/module.cpp index 535cb7fdc54c..6cce93c0f9f3 100644 --- a/src/python_bindings/bindings/module.cpp +++ b/src/python_bindings/bindings/module.cpp @@ -118,7 +118,7 @@ namespace hal :rtype: hal_py.Module or None )"); - py_module.def_property_readonly("parent_modules", [](Module* mod) { return mod->get_parent_modules(); }, borrowed(), R"( + py_module.def_property_readonly("parent_modules", py::cpp_function([](Module* mod) { return mod->get_parent_modules(); }, py::is_method(py_module), borrowed()), R"( The parent modules of this module. :type: list[hal_py.Module] @@ -153,7 +153,7 @@ namespace hal :rtype: bool )"); - py_module.def_property_readonly("submodules", [](Module* mod) { return mod->get_submodules(); }, borrowed(), R"( + py_module.def_property_readonly("submodules", py::cpp_function([](Module* mod) { return mod->get_submodules(); }, py::is_method(py_module), borrowed()), R"( A list of all direct submodules of this module. :type: list[hal_py.Module] @@ -232,7 +232,7 @@ namespace hal :rtype: bool )"); - py_module.def_property_readonly("nets", py::overload_cast<>(&Module::get_nets, py::const_), borrowed(), R"( + py_module.def_property_readonly("nets", py::cpp_function(py::overload_cast<>(&Module::get_nets, py::const_), py::is_method(py_module), borrowed()), R"( An unordered set of all nets that have at least one source or one destination within the module. :type: set[hal_py.Net] @@ -256,7 +256,7 @@ namespace hal :rtype: set[hal_py.Net] )"); - py_module.def_property_readonly("input_nets", &Module::get_input_nets, borrowed(), R"( + py_module.def_property_readonly("input_nets", py::cpp_function(&Module::get_input_nets, py::is_method(py_module), borrowed()), R"( A set of all nets that are either a global input to the netlist or have at least one source outside of the module. :type: set[hal_py.Net] @@ -269,7 +269,7 @@ namespace hal :rtype: set[hal_py.Net] )"); - py_module.def_property_readonly("output_nets", &Module::get_output_nets, borrowed(), R"( + py_module.def_property_readonly("output_nets", py::cpp_function(&Module::get_output_nets, py::is_method(py_module), borrowed()), R"( A set of all nets that are either a global output to the netlist or have at least one destination outside of the module. :type: set[hal_py.Net] @@ -282,7 +282,7 @@ namespace hal :rtype: set[hal_py.Net] )"); - py_module.def_property_readonly("internal_nets", &Module::get_internal_nets, borrowed(), R"( + py_module.def_property_readonly("internal_nets", py::cpp_function(&Module::get_internal_nets, py::is_method(py_module), borrowed()), R"( A set of all nets that have at least one source and one destination within the module, including its submodules. The result may contain nets that are also regarded as input or output nets. :type: set[hal_py.Net] @@ -375,7 +375,7 @@ namespace hal :rtype: hal_py.Gate or None )"); - py_module.def_property_readonly("gates", py::overload_cast<>(&Module::get_gates, py::const_), borrowed(), R"( + py_module.def_property_readonly("gates", py::cpp_function(py::overload_cast<>(&Module::get_gates, py::const_), py::is_method(py_module), borrowed()), R"( The list of all gates contained within the module. :type: list[hal_py.Gate] @@ -491,7 +491,7 @@ namespace hal )"); py_module.def_property_readonly( - "pins", [](const Module& self) { return self.get_pins(); }, borrowed(), R"( + "pins", py::cpp_function([](const Module& self) { return self.get_pins(); }, py::is_method(py_module), borrowed()), R"( The (ordered) pins of the module. :type: list[hal_py.ModulePin] @@ -525,7 +525,7 @@ namespace hal :rtype: list[str] )"); - py_module.def_property_readonly("input_pins", &Module::get_input_pins, borrowed(), R"( + py_module.def_property_readonly("input_pins", py::cpp_function(&Module::get_input_pins, py::is_method(py_module), borrowed()), R"( An ordered list of all input pins of the module (including inout pins). :type: list[hal_py.ModulePin] @@ -551,7 +551,7 @@ namespace hal :rtype: list[str] )"); - py_module.def_property_readonly("output_pins", &Module::get_output_pins, borrowed(), R"( + py_module.def_property_readonly("output_pins", py::cpp_function(&Module::get_output_pins, py::is_method(py_module), borrowed()), R"( An ordered list of all output pins of the module (including inout pins). :type: list[hal_py.ModulePin] @@ -578,7 +578,7 @@ namespace hal )"); py_module.def_property_readonly( - "pin_groups", [](const Module& self) { return self.get_pin_groups(); }, borrowed(), R"( + "pin_groups", py::cpp_function([](const Module& self) { return self.get_pin_groups(); }, py::is_method(py_module), borrowed()), R"( All pin_groups of the module. :type: list[hal_py.ModulePinGroup] diff --git a/src/python_bindings/bindings/module_pin.cpp b/src/python_bindings/bindings/module_pin.cpp index befc6d0ece22..2ff8ad1e077b 100644 --- a/src/python_bindings/bindings/module_pin.cpp +++ b/src/python_bindings/bindings/module_pin.cpp @@ -22,7 +22,7 @@ namespace hal :rtype: bool )"); - py_module_pin.def_property_readonly("net", &ModulePin::get_net, borrowed(), R"( + py_module_pin.def_property_readonly("net", py::cpp_function(&ModulePin::get_net, py::is_method(py_module_pin), borrowed()), R"( The net passing through the pin. :type: hal_py.Net diff --git a/src/python_bindings/bindings/module_pin_group.cpp b/src/python_bindings/bindings/module_pin_group.cpp index 0f1804315fca..31752feae18a 100644 --- a/src/python_bindings/bindings/module_pin_group.cpp +++ b/src/python_bindings/bindings/module_pin_group.cpp @@ -81,7 +81,7 @@ namespace hal :rtype: hal_py.PinType )"); - py_module_pin_group.def_property_readonly("pins", [](const PinGroup& self) -> std::vector { return self.get_pins(nullptr); }, borrowed(), R"( + py_module_pin_group.def_property_readonly("pins", py::cpp_function([](const PinGroup& self) -> std::vector { return self.get_pins(nullptr); }, py::is_method(py_module_pin_group), borrowed()), R"( The (ordered) pins of the pin groups. :type: list[hal_py.ModulePin] diff --git a/src/python_bindings/bindings/net.cpp b/src/python_bindings/bindings/net.cpp index 2b8274c7d613..b0dd4ffdf30b 100644 --- a/src/python_bindings/bindings/net.cpp +++ b/src/python_bindings/bindings/net.cpp @@ -179,7 +179,7 @@ namespace hal :rtype: int )"); - py_net.def_property_readonly("sources", [](Net* n) { return n->get_sources(); }, borrowed(), R"( + py_net.def_property_readonly("sources", py::cpp_function([](Net* n) { return n->get_sources(); }, py::is_method(py_net), borrowed()), R"( A list of sources of the net. :type: list[hal_py.Endpoint] @@ -293,7 +293,7 @@ namespace hal :rtype: int )"); - py_net.def_property_readonly("destinations", [](Net* n) { return n->get_destinations(); }, borrowed(), R"( + py_net.def_property_readonly("destinations", py::cpp_function([](Net* n) { return n->get_destinations(); }, py::is_method(py_net), borrowed()), R"( A list of destinations of the net. :type: list[hal_py.Endpoint] diff --git a/src/python_bindings/bindings/netlist.cpp b/src/python_bindings/bindings/netlist.cpp index 7010824c908a..bac3e7234d62 100644 --- a/src/python_bindings/bindings/netlist.cpp +++ b/src/python_bindings/bindings/netlist.cpp @@ -218,7 +218,7 @@ namespace hal :rtype: hal_py.Gate or None )"); - py_netlist.def_property_readonly("gates", py::overload_cast<>(&Netlist::get_gates, py::const_), borrowed(), R"( + py_netlist.def_property_readonly("gates", py::cpp_function(py::overload_cast<>(&Netlist::get_gates, py::const_), py::is_method(py_netlist), borrowed()), R"( All gates contained within the netlist. :type: list[hal_py.Gate] @@ -288,7 +288,7 @@ namespace hal :rtype: bool )"); - py_netlist.def_property_readonly("vcc_gates", &Netlist::get_vcc_gates, borrowed(), R"( + py_netlist.def_property_readonly("vcc_gates", py::cpp_function(&Netlist::get_vcc_gates, py::is_method(py_netlist), borrowed()), R"( All global VCC gates. :type: list[hal_py.Gate] @@ -301,7 +301,7 @@ namespace hal :rtype: list[hal_py.Gate] )"); - py_netlist.def_property_readonly("gnd_gates", &Netlist::get_gnd_gates, borrowed(), R"( + py_netlist.def_property_readonly("gnd_gates", py::cpp_function(&Netlist::get_gnd_gates, py::is_method(py_netlist), borrowed()), R"( All global GND gates. :type: list[hal_py.Gate] @@ -314,7 +314,7 @@ namespace hal :rtype: list[hal_py.Gate] )"); - py_netlist.def_property_readonly("vcc_nets", &Netlist::get_vcc_nets, borrowed(), R"( + py_netlist.def_property_readonly("vcc_nets", py::cpp_function(&Netlist::get_vcc_nets, py::is_method(py_netlist), borrowed()), R"( All global VCC nets. :type: list[hal_py.Net] @@ -327,7 +327,7 @@ namespace hal :rtype: list[hal_py.Net] )"); - py_netlist.def_property_readonly("gnd_nets", &Netlist::get_gnd_nets, borrowed(), R"( + py_netlist.def_property_readonly("gnd_nets", py::cpp_function(&Netlist::get_gnd_nets, py::is_method(py_netlist), borrowed()), R"( All global GND nets. :type: list[hal_py.Net] @@ -390,7 +390,7 @@ namespace hal :rtype: hal_py.Net or None )"); - py_netlist.def_property_readonly("nets", py::overload_cast<>(&Netlist::get_nets, py::const_), borrowed(), R"( + py_netlist.def_property_readonly("nets", py::cpp_function(py::overload_cast<>(&Netlist::get_nets, py::const_), py::is_method(py_netlist), borrowed()), R"( All nets contained within the netlist. :type: list[hal_py.Net] @@ -460,7 +460,7 @@ namespace hal :rtype: bool )"); - py_netlist.def_property_readonly("global_input_nets", &Netlist::get_global_input_nets, borrowed(), R"( + py_netlist.def_property_readonly("global_input_nets", py::cpp_function(&Netlist::get_global_input_nets, py::is_method(py_netlist), borrowed()), R"( All global input nets. :type: list[hal_py.Net] @@ -473,7 +473,7 @@ namespace hal :rtype: list[hal_py.Net] )"); - py_netlist.def_property_readonly("global_output_nets", &Netlist::get_global_output_nets, borrowed(), R"( + py_netlist.def_property_readonly("global_output_nets", py::cpp_function(&Netlist::get_global_output_nets, py::is_method(py_netlist), borrowed()), R"( All global output nets. :type: list[hal_py.Net] @@ -560,7 +560,7 @@ namespace hal :rtype: hal_py.Module )"); - py_netlist.def_property_readonly("modules", py::overload_cast<>(&Netlist::get_modules, py::const_), borrowed(), R"( + py_netlist.def_property_readonly("modules", py::cpp_function(py::overload_cast<>(&Netlist::get_modules, py::const_), py::is_method(py_netlist), borrowed()), R"( All modules contained within the netlist, including the top module. :type: list[hal_py.Module] @@ -582,7 +582,7 @@ namespace hal :rtype: list[hal_py.Module] )"); - py_netlist.def_property_readonly("top_module", &Netlist::get_top_module, borrowed(), R"( + py_netlist.def_property_readonly("top_module", py::cpp_function(&Netlist::get_top_module, py::is_method(py_netlist), borrowed()), R"( The top module of the netlist. :type: hal_py.Module @@ -652,7 +652,7 @@ namespace hal :rtype: hal_py.Grouping )"); - py_netlist.def_property_readonly("groupings", py::overload_cast<>(&Netlist::get_groupings, py::const_), borrowed(), R"( + py_netlist.def_property_readonly("groupings", py::cpp_function(py::overload_cast<>(&Netlist::get_groupings, py::const_), py::is_method(py_netlist), borrowed()), R"( All groupings contained within the netlist. :type: list[hal_py.Grouping] diff --git a/src/python_bindings/bindings/smt.cpp b/src/python_bindings/bindings/smt.cpp index ec1d3ca83af2..439438bcbf40 100644 --- a/src/python_bindings/bindings/smt.cpp +++ b/src/python_bindings/bindings/smt.cpp @@ -14,9 +14,18 @@ namespace hal py_smt_solver_type.value("Z3", SMT::SolverType::Z3, R"(Z3 SMT solver.)") .value("Boolector", SMT::SolverType::Boolector, R"(Boolector SMT solver.)") + .value("Bitwuzla", SMT::SolverType::Bitwuzla, R"(Bitwuzla SMT solver.)") .value("Unknown", SMT::SolverType::Unknown, R"(Unknown (unsupported) SMT solver.)") .export_values(); + py::enum_ py_smt_solver_call(py_smt, "SolverCall", R"( + Identifier for how the SMT solver is invoked. + )"); + + py_smt_solver_call.value("Binary", SMT::SolverCall::Binary, R"(Call the solver binary in a subprocess.)") + .value("Library", SMT::SolverCall::Library, R"(Call the solver through the library linked into HAL.)") + .export_values(); + py::class_ py_smt_query_config(py_smt, "QueryConfig", R"( Represents the data structure to configure an SMT query. )"); @@ -422,6 +431,26 @@ namespace hal :rtype: hal_py.SMT.Result or str )"); + py_smt_solver.def( + "to_smt2", + [](const SMT::Solver& self, const SMT::QueryConfig& config) -> std::optional { + auto res = self.to_smt2(config); + if (res.is_ok()) + { + return res.get(); + } + log_error("python_context", "{}", res.get_error().get()); + return std::nullopt; + }, + py::arg("config"), + R"( + Translate the constraints of the solver into an smt2 representation of the query. + + :param hal_py.SMT.QueryConfig config: The SMT solver query configuration. + :returns: The smt2 representation on success, ``None`` otherwise. + :rtype: str or None + )"); + py_smt_solver.def_static( "query_local_with_smt2", [](const SMT::QueryConfig& config, const std::string& smt2) -> std::optional { @@ -498,20 +527,44 @@ namespace hal :param list[hal_py.BooleanFunction] variables: The (optional) list of variables. )"); - py_smt_symbolic_execution.def("evaluate", py::overload_cast(&SMT::SymbolicExecution::evaluate, py::const_), py::arg("function"), R"( + py_smt_symbolic_execution.def( + "evaluate", + [](const SMT::SymbolicExecution& self, const BooleanFunction& function) -> std::optional { + auto res = self.evaluate(function); + if (res.is_ok()) + { + return res.get(); + } + log_error("python_context", "{}", res.get_error().get()); + return std::nullopt; + }, + py::arg("function"), + R"( Evaluates a Boolean function within the symbolic state of the symbolic execution. :param hal_py.BooleanFunction function: The Boolean function to evaluate. - :returns: The evaluated Boolean function on success, a string error message otherwise. - :rtype: hal_py.BooleanFunction or str + :returns: The evaluated Boolean function on success, ``None`` otherwise. + :rtype: hal_py.BooleanFunction or None )"); - py_smt_symbolic_execution.def("evaluate", py::overload_cast(&SMT::SymbolicExecution::evaluate), py::arg("constraint"), R"( + py_smt_symbolic_execution.def( + "evaluate", + [](SMT::SymbolicExecution& self, const SMT::Constraint& constraint) -> bool { + auto res = self.evaluate(constraint); + if (res.is_ok()) + { + return true; + } + log_error("python_context", "{}", res.get_error().get()); + return false; + }, + py::arg("constraint"), + R"( Evaluates an equality constraint and applies it to the symbolic state of the symbolic execution. :param hal_py.SMT.Constraint constraint: The equality constraint to evaluate. - :returns: ``None`` on success, a string error message otherwise. - :rtype: None or str + :returns: ``True`` on success, ``False`` otherwise. + :rtype: bool )"); } } // namespace hal diff --git a/tests/python_bindings/CMakeLists.txt b/tests/python_bindings/CMakeLists.txt index 9104556082c4..2b9b5a06e5c3 100644 --- a/tests/python_bindings/CMakeLists.txt +++ b/tests/python_bindings/CMakeLists.txt @@ -12,3 +12,12 @@ add_test(NAME runTest-python_binding_smoke WORKING_DIRECTORY ${CMAKE_SOURCE_DIR}) set_tests_properties(runTest-python_binding_smoke PROPERTIES ENVIRONMENT "PYTHONPATH=${CMAKE_BINARY_DIR}/lib;HAL_BASE_PATH=${CMAKE_BINARY_DIR}") + +# Loading the plugins and letting the interpreter exit without unloading them used to segfault, so +# this checks that a process which does exactly that comes back with a zero exit code. It runs its +# cases in subprocesses, as what is under test is how a process ends. +add_test(NAME runTest-python_teardown + COMMAND ${Python3_EXECUTABLE} ${CMAKE_CURRENT_SOURCE_DIR}/teardown_test.py + WORKING_DIRECTORY ${CMAKE_SOURCE_DIR}) +set_tests_properties(runTest-python_teardown PROPERTIES + ENVIRONMENT "PYTHONPATH=${CMAKE_BINARY_DIR}/lib;HAL_BASE_PATH=${CMAKE_BINARY_DIR}") diff --git a/tests/python_bindings/smoke_test_bindings.py b/tests/python_bindings/smoke_test_bindings.py index 46f0a205a453..56f949a13f3a 100644 --- a/tests/python_bindings/smoke_test_bindings.py +++ b/tests/python_bindings/smoke_test_bindings.py @@ -172,15 +172,12 @@ def main(): import hal_py # The gate library is read by a plugin, so the plugins have to be loaded before anything else. - # They also have to be unloaded again before the interpreter exits: leaving them loaded segfaults - # at teardown, independently of anything this test does. That is a real defect, but it predates - # this test -- it reproduces on a build from well before the binding work -- so it is not this - # test's job to fail on it. + # They are left loaded, which used to segfault at teardown. This test cannot be relied on to + # notice if that comes back, though, because it imports the plugin modules as well and an + # imported module holds a reference of its own to the library, which keeps it mapped. See + # teardown_test.py, which reproduces it without importing anything. hal_py.plugin_manager.load_all_plugins() - try: - return run_checks(hal_py) - finally: - hal_py.plugin_manager.unload_all_plugins() + return run_checks(hal_py) def run_checks(hal_py): diff --git a/tests/python_bindings/teardown_test.py b/tests/python_bindings/teardown_test.py new file mode 100644 index 000000000000..f75058794ebc --- /dev/null +++ b/tests/python_bindings/teardown_test.py @@ -0,0 +1,52 @@ +#!/usr/bin/env python3 +"""Check that an interpreter which loaded the plugins can exit. + +Loading the plugins and letting the interpreter exit without unloading them used to segfault. The +parser and writer registries live in libhal_netlist and hold a std::function per plugin that provides +one; the plugin libraries were closed when the map holding them was destroyed, which happens before +those registries are, so every one of those functions was left pointing into memory that had been +unmapped. + +The check runs in a subprocess, because what is being tested is the exit of a process rather than +anything observable from within it. It also has to avoid importing any plugin module: an imported +module holds a reference of its own to the library, which keeps it mapped and hides the fault. That +is why the binding smoke test does not notice this one. +""" + +import os +import subprocess +import sys + +CASES = { + "load the plugins and exit": "import hal_py; hal_py.plugin_manager.load_all_plugins()", + "load, unload, and exit": "import hal_py; hal_py.plugin_manager.load_all_plugins(); hal_py.plugin_manager.unload_all_plugins()", + "load, unload, load again, and exit": ( + "import hal_py; " + "hal_py.plugin_manager.load_all_plugins(); " + "hal_py.plugin_manager.unload_all_plugins(); " + "hal_py.plugin_manager.load_all_plugins()" + ), +} + + +def main(): + failures = [] + for description, code in CASES.items(): + result = subprocess.run([sys.executable, "-c", code], capture_output=True, env=os.environ.copy()) + if result.returncode != 0: + reason = f"signal {-result.returncode}" if result.returncode < 0 else f"exit code {result.returncode}" + failures.append((description, reason, result.stderr.decode(errors="replace")[-400:])) + print(f" {description}: {'ok' if result.returncode == 0 else 'FAILED'}") + + if failures: + print(f"\n{len(failures)} interpreter(s) did not exit cleanly:\n", file=sys.stderr) + for description, reason, stderr in failures: + print(f"--- {description}: {reason} ---", file=sys.stderr) + print(stderr, file=sys.stderr) + return 1 + + return 0 + + +if __name__ == "__main__": + sys.exit(main())