merge

documentation/sphinx_doc/boolean_function_decorator.rst

@@ -0,0 +1,5 @@
+Boolean Function Decorator
+==============================
+
+.. autoclass:: hal_py.BooleanFunctionDecorator
+   :members:

documentation/sphinx_doc/hal_py.rst

@@ -6,6 +6,7 @@ HAL Core Documentation
 
    base_plugin_interface
    boolean_function
+   boolean_function_decorator
    boolean_function_net_decorator
    core_utils
    data_container

include/hal_core/netlist/boolean_function.h

@@ -91,15 +91,15 @@ namespace hal
          * 
          * @param[in] value - The value as a bit-vector.
          * @param[in] base - The base that the values should be converted to. Valid values are 2 (default), 8, 10, and 16.
-         * @returns A string representing the values in the given base or an error.
+         * @returns A string representing the values in the given base on success, an error otherwise.
          */
         static Result<std::string> to_string(const std::vector<BooleanFunction::Value>& value, u8 base = 2);
 
         /**
-         * Convert the given bit-vector to its unsigned 64 bit integer representation.
+         * Convert the given bit-vector to its unsigned 64-bit integer representation.
          * 
          * @param[in] value - The value as a bit-vector.
-         * @returns An u64 representing the values in the given base or an error.
+         * @returns A 64-bit integer representing the values on success, an error otherwise.
          */
         static Result<u64> to_u64(const std::vector<BooleanFunction::Value>& value);
 

include/hal_core/netlist/boolean_function/types.h

@@ -260,15 +260,15 @@ namespace hal
 			 *
 			 * @param[in] model_str - The SMT-Lib model string.
 			 * @param[in] solver - The solver that computed the model.
-			 * @returns Ok() and the model on success, Err() otherwise.
+			 * @returns The model on success, an error otherwise.
 			 */
             static Result<Model> parse(const std::string& model_str, const SolverType& solver);
 
             /**
-			 * Evaluates the given boolean function by replacing all variables contained in the model with their corresponding value and simplifying.
+			 * Evaluates the given Boolean function by replacing all variables contained in the model with their corresponding value and simplifying the result.
 			 *
-			 * @param[in] bf - Boolean function to evaluate.
-			 * @returns Ok() and the evaluated function on success, Err() otherwise.
+			 * @param[in] bf - The Boolean function to evaluate.
+			 * @returns The evaluated function on success, an error otherwise.
 			 */
             Result<BooleanFunction> evaluate(const BooleanFunction& bf) const;
         };

include/hal_core/netlist/decorators/boolean_function_decorator.h

@@ -0,0 +1,77 @@
+// 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.
+
+#pragma once
+
+#include "hal_core/defines.h"
+#include "hal_core/netlist/boolean_function.h"
+#include "hal_core/netlist/net.h"
+
+namespace hal
+{
+    class NETLIST_API BooleanFunctionDecorator
+    {
+    public:
+        /**
+         * Construct new BooleanFunction object.
+         * 
+         * @param[in] bf - The Boolean function to operate on. 
+         */
+        BooleanFunctionDecorator(const BooleanFunction& bf);
+
+        /**
+         * Substitute all Boolean function variables fed by power or ground gates by constant '1' and '0'. 
+         * 
+         * @param[in] nl - The netlist to operate on.
+         * @return The resulting Boolean function on success, an error otherwise.
+         */
+        Result<BooleanFunction> substitute_power_ground_nets(const Netlist* nl) const;
+
+        /**
+         * Get the Boolean function that is the concatenation of variable names corresponding to nets of a netlist.
+         * The Boolean function can optionally be extended to any desired size greater the size of the given net vector.
+         * 
+         * @param[in] nets - The nets to concatenate. 
+         * @param[in] extend_to_size - The size to which to extend the Boolean function. Set to 0 to prevent extension. Defaults to 0.
+         * @param[in] sign_extend - Set `true` to sign extend, `false` to zero extend. Defaults to `false`.
+         * @return The resulting Boolean function on success, an error otherwise.
+         */
+        static Result<BooleanFunction> get_boolean_function_from(const std::vector<Net*>& nets, u32 extend_to_size = 0, bool sign_extend = false);
+
+        /**
+         * Get the Boolean function that is the concatenation of Boolean functions.
+         * The Boolean function can optionally be extended to any desired size greater the size of the given Boolean function vector.
+         * 
+         * @param[in] functions - The Boolean functions to concatenate. 
+         * @param[in] extend_to_size - The size to which to extend the Boolean function. Set to 0 to prevent extension. Defaults to 0.
+         * @param[in] sign_extend - Set `true` to sign extend, `false` to zero extend. Defaults to `false`.
+         * @return The resulting Boolean function on success, an error otherwise.
+         */
+        static Result<BooleanFunction> get_boolean_function_from(const std::vector<BooleanFunction>& functions, u32 extend_to_size = 0, bool sign_extend = false);
+
+    private:
+        const BooleanFunction& m_bf;
+    };
+}    // namespace hal

include/hal_core/python_bindings/python_bindings.h

@@ -31,6 +31,7 @@
 #include "hal_core/netlist/boolean_function/symbolic_execution.h"
 #include "hal_core/netlist/boolean_function/symbolic_state.h"
 #include "hal_core/netlist/boolean_function/types.h"
+#include "hal_core/netlist/decorators/boolean_function_decorator.h"
 #include "hal_core/netlist/decorators/boolean_function_net_decorator.h"
 #include "hal_core/netlist/decorators/subgraph_netlist_decorator.h"
 #include "hal_core/netlist/gate.h"
@@ -303,6 +304,13 @@ namespace hal
      */
     void subgraph_netlist_decorator_init(py::module& m);
 
+    /**
+     * Initializes Python bindings for the HAL Boolean function decorator in a python module.
+     *
+     * @param[in] m - the python module
+     */
+    void boolean_function_decorator_init(py::module& m);
+
     /**
      * @}
      */

include/hal_core/utilities/result.h

@@ -196,7 +196,7 @@ namespace hal
          * @param[in] f - The mapping function.
          * @returns The result mapped to the target data type.
          */
-        template<typename U = T, typename std::enable_if_t<!std::is_same_v<U, void>, int> = 0>
+        template<typename U, typename std::enable_if_t<!std::is_same_v<U, void>, int> = 0>
         Result<U> map(const std::function<Result<U>(const T&)>& f) const
         {
             if (this->is_ok())
@@ -209,6 +209,26 @@ namespace hal
             }
         }
 
+        /**
+          * Map the result to a different user-defined data type using the provided mapping function.
+          * 
+          * @tparam U - The target data type.
+          * @param[in] f - The mapping function.
+          * @returns The result mapped to the target data type.
+          */
+        template<typename U, typename std::enable_if_t<!std::is_same_v<U, void>, int> = 0>
+        Result<U> map(const std::function<Result<U>(T&&)>& f)
+        {
+            if (this->is_ok())
+            {
+                return f(this->get());
+            }
+            else
+            {
+                return ERR(this->get_error());
+            }
+        }
+
     private:
         std::variant<T, Error> m_result;
     };

plugins/verilog_writer/test/verilog_writer.cpp

@@ -90,10 +90,6 @@ namespace hal
                 VerilogWriter verilog_writer;
                 ASSERT_TRUE(verilog_writer.write(nl.get(), path_netlist).is_ok());
 
-                std::ifstream fdump(path_netlist);
-                if (fdump.good())
-                    std::cout << "----\n" << fdump.rdbuf() << "----" << std::endl;
-
                 VerilogParser verilog_parser;
                 auto parsed_nl_res = verilog_parser.parse_and_instantiate(path_netlist, m_gl);
                 ASSERT_TRUE(parsed_nl_res.is_ok());

src/netlist/boolean_function/simplification_abc.cpp

@@ -553,10 +553,11 @@ namespace hal
         Result<BooleanFunction> slice_at(const BooleanFunction& function, const u16 index)
         {
             // (1) setup the sliced Boolean function
-            if (auto res = BooleanFunction::Slice(function.clone(), BooleanFunction::Index(index, function.size()), BooleanFunction::Index(index, function.size()), 1).map<BooleanFunction>([](auto f) {
-                    // (2) perform a local simplification in order to remove unnecessary slices
-                    return Simplification::local_simplification(f);
-                });
+            if (auto res =
+                    BooleanFunction::Slice(function.clone(), BooleanFunction::Index(index, function.size()), BooleanFunction::Index(index, function.size()), 1).map<BooleanFunction>([](const auto& f) {
+                        // (2) perform a local simplification in order to remove unnecessary slices
+                        return Simplification::local_simplification(f);
+                    });
                 res.is_error())
             {
                 return ERR(res.get_error());
@@ -991,15 +992,15 @@ namespace hal
         static std::mutex mutex;
         mutex.lock();
 
-        auto status = translate_to_abc(function).map<std::monostate>([](auto network) { return simplify(network); });
+        auto status = translate_to_abc(function).map<std::monostate>([](const auto& network) { return simplify(network); });
 
         if (status.is_error())
         {
             return ERR_APPEND(status.get_error(), "could not simplyfy Boolean function using ABC: unable to translate & simplify Boolean function '" + function.to_string() + "'");
         }
 
         // (3) translate the ABC graph back into a Boolean function
-        auto translated_function = translate_from_abc().map<BooleanFunction>([&function](auto verilog) { return translate_from_verilog(verilog, function); });
+        auto translated_function = translate_from_abc().map<BooleanFunction>([&function](const auto& verilog) { return translate_from_verilog(verilog, function); });
 
         mutex.unlock();
 

src/netlist/boolean_function/solver.cpp

@@ -335,7 +335,7 @@ namespace hal
             {
                 if (config.generate_model)
                 {
-                    if (auto res = Model::parse(model_str, config.solver).map<SolverResult>([](auto model) -> Result<SolverResult> { return OK(SolverResult::Sat(model)); }); res.is_error())
+                    if (auto res = Model::parse(model_str, config.solver).map<SolverResult>([](const auto& model) -> Result<SolverResult> { return OK(SolverResult::Sat(model)); }); res.is_error())
                     {
                         return ERR_APPEND(res.get_error(), "could not parse SMT result from string: unable to generate model");
                     }

src/netlist/boolean_function/types.cpp

@@ -209,40 +209,6 @@ namespace hal
             return out;
         }
 
-        Result<BooleanFunction> Model::evaluate(const BooleanFunction& bf) const
-        {
-            std::vector<BooleanFunction::Node> new_nodes;
-
-            for (const auto& node : bf.get_nodes())
-            {
-                if (node.is_variable())
-                {
-                    const auto var_name = node.variable;
-                    if (auto it = model.find(var_name); it != model.end())
-                    {
-                        const auto constant = BooleanFunction::Const(std::get<0>(it->second), std::get<1>(it->second));
-                        new_nodes.insert(new_nodes.end(), constant.get_nodes().begin(), constant.get_nodes().end());
-                    }
-                    else
-                    {
-                        new_nodes.push_back(node);
-                    }
-                }
-                else
-                {
-                    new_nodes.push_back(node);
-                }
-            }
-
-            auto build_res = BooleanFunction::build(std::move(new_nodes));
-            if (build_res.is_error())
-            {
-                return ERR_APPEND(build_res.get_error(), "failed to evaluate Boolean function for the model: failed to build function after replacing nodes.");
-            }
-
-            return OK(build_res.get().simplify());
-        }
-
         Result<Model> Model::parse(const std::string& s, const SolverType& type)
         {
             // TODO:
@@ -281,6 +247,40 @@ namespace hal
             return ERR("could not parse SMT-Lib model");
         }
 
+        Result<BooleanFunction> Model::evaluate(const BooleanFunction& bf) const
+        {
+            std::vector<BooleanFunction::Node> new_nodes;
+
+            for (const auto& node : bf.get_nodes())
+            {
+                if (node.is_variable())
+                {
+                    const auto var_name = node.variable;
+                    if (auto it = model.find(var_name); it != model.end())
+                    {
+                        const auto constant = BooleanFunction::Const(std::get<0>(it->second), std::get<1>(it->second));
+                        new_nodes.insert(new_nodes.end(), constant.get_nodes().begin(), constant.get_nodes().end());
+                    }
+                    else
+                    {
+                        new_nodes.push_back(node);
+                    }
+                }
+                else
+                {
+                    new_nodes.push_back(node);
+                }
+            }
+
+            auto build_res = BooleanFunction::build(std::move(new_nodes));
+            if (build_res.is_error())
+            {
+                return ERR_APPEND(build_res.get_error(), "failed to evaluate Boolean function for the model: failed to build function after replacing nodes.");
+            }
+
+            return OK(build_res.get().simplify());
+        }
+
         SolverResult::SolverResult(SolverResultType _type, std::optional<Model> _model) : type(_type), model(_model)
         {
         }