Give a bit order a type, make the SMT interface usable, and let the call policy reach a property

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

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.

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()

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 <optional>
+#include <vector>
+
+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<ModulePin>* pin_group, std::vector<std::pair<Net*, u32>> 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<ModulePin>* get_pin_group() const;
+
+            /**
+             * Get the index of every net, ordered by index.
+             *
+             * @returns The nets and their indices.
+             */
+            const std::vector<std::pair<Net*, u32>>& 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<u32> 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<ModulePin>* m_pin_group;
+            std::vector<std::pair<Net*, u32>> 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<BitOrder> 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<BitOrder>& 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<ModulePin>* 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<ModulePin>* 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<BitOrder>::const_iterator begin() const;
+            std::vector<BitOrder>::const_iterator end() const;
+
+        private:
+            std::vector<BitOrder> m_bit_orders;
+        };
+    }    // namespace bitorder_propagation
+}    // namespace hal