boolean_function.h

Go to the documentation of this file.

// 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/utilities/enums.h"
#include "hal_core/utilities/result.h"
#include "z3++.h"
 
#include <algorithm>
#include <cassert>
#include <map>
#include <ostream>
#include <set>
#include <unordered_map>
#include <vector>
 
namespace hal
{
    class NETLIST_API BooleanFunction final
    {
    public:
        // Forward Declarations
 
        /*
         * We forward declare the abstract syntax tree nodes and types of the 
         * Boolean function in order to re-use BooleanFunction both as a class 
         * and a namespace for its underlying node data structures.
         */
 
        struct Node;        
        struct NodeType;    
 
        enum Value
        {
            ZERO = 0,  
            ONE  = 1,  
            X    = -1, 
            Z    = -2  
        };
 
        static std::string to_string(Value value);
 
        static Result<std::string> to_string(const std::vector<BooleanFunction::Value>& value, u8 base = 2);
 
        static Result<u64> to_u64(const std::vector<BooleanFunction::Value>& value);
 
        friend std::ostream& operator<<(std::ostream& os, Value v);
 
        // Constructors / Factories, Destructors, Operators
 
        explicit BooleanFunction();
 
        static Result<BooleanFunction> build(std::vector<Node>&& nodes);
 
        static BooleanFunction Var(const std::string& name, u16 size = 1);
 
        static BooleanFunction Const(const BooleanFunction::Value& value);
 
        static BooleanFunction Const(const std::vector<BooleanFunction::Value>& value);
 
        static BooleanFunction Const(u64 value, u16 size);
 
        static BooleanFunction Index(u16 index, u16 size);
 
        static Result<BooleanFunction> And(BooleanFunction&& p0, BooleanFunction&& p1, u16 size);
 
        static Result<BooleanFunction> Or(BooleanFunction&& p0, BooleanFunction&& p1, u16 size);
 
        static Result<BooleanFunction> Not(BooleanFunction&& p0, u16 size);
 
        static Result<BooleanFunction> Xor(BooleanFunction&& p0, BooleanFunction&& p1, u16 size);
 
        static Result<BooleanFunction> Add(BooleanFunction&& p0, BooleanFunction&& p1, u16 size);
 
        static Result<BooleanFunction> Sub(BooleanFunction&& p0, BooleanFunction&& p1, u16 size);
 
        static Result<BooleanFunction> Mul(BooleanFunction&& p0, BooleanFunction&& p1, u16 size);
 
        static Result<BooleanFunction> Sdiv(BooleanFunction&& p0, BooleanFunction&& p1, u16 size);
 
        static Result<BooleanFunction> Udiv(BooleanFunction&& p0, BooleanFunction&& p1, u16 size);
 
        static Result<BooleanFunction> Srem(BooleanFunction&& p0, BooleanFunction&& p1, u16 size);
 
        static Result<BooleanFunction> Urem(BooleanFunction&& p0, BooleanFunction&& p1, u16 size);
 
        static Result<BooleanFunction> Slice(BooleanFunction&& p0, BooleanFunction&& p1, BooleanFunction&& p2, u16 size);
 
        static Result<BooleanFunction> Concat(BooleanFunction&& p0, BooleanFunction&& p1, u16 size);
 
        static Result<BooleanFunction> Zext(BooleanFunction&& p0, BooleanFunction&& p1, u16 size);
 
        static Result<BooleanFunction> Sext(BooleanFunction&& p0, BooleanFunction&& p1, u16 size);
 
        static Result<BooleanFunction> Shl(BooleanFunction&& p0, BooleanFunction&& p1, u16 size);
 
        static Result<BooleanFunction> Lshr(BooleanFunction&& p0, BooleanFunction&& p1, u16 size);
 
        static Result<BooleanFunction> Ashr(BooleanFunction&& p0, BooleanFunction&& p1, u16 size);
 
        static Result<BooleanFunction> Rol(BooleanFunction&& p0, BooleanFunction&& p1, u16 size);
 
        static Result<BooleanFunction> Ror(BooleanFunction&& p0, BooleanFunction&& p1, u16 size);
 
        static Result<BooleanFunction> Eq(BooleanFunction&& p0, BooleanFunction&& p1, u16 size);
 
        static Result<BooleanFunction> Sle(BooleanFunction&& p0, BooleanFunction&& p1, u16 size);
 
        static Result<BooleanFunction> Slt(BooleanFunction&& p0, BooleanFunction&& p1, u16 size);
 
        static Result<BooleanFunction> Ule(BooleanFunction&& p0, BooleanFunction&& p1, u16 size);
 
        static Result<BooleanFunction> Ult(BooleanFunction&& p0, BooleanFunction&& p1, u16 size);
 
        static Result<BooleanFunction> Ite(BooleanFunction&& p0, BooleanFunction&& p1, BooleanFunction&& p2, u16 size);
 
        friend std::ostream& operator<<(std::ostream& os, const BooleanFunction& f);
 
        BooleanFunction operator&(const BooleanFunction& other) const;
 
        BooleanFunction& operator&=(const BooleanFunction& other);
 
        BooleanFunction operator~() const;
 
        BooleanFunction operator|(const BooleanFunction& other) const;
 
        BooleanFunction& operator|=(const BooleanFunction& other);
 
        BooleanFunction operator^(const BooleanFunction& other) const;
 
        BooleanFunction& operator^=(const BooleanFunction& other);
 
        BooleanFunction operator+(const BooleanFunction& other) const;
 
        BooleanFunction& operator+=(const BooleanFunction& other);
 
        BooleanFunction operator-(const BooleanFunction& other) const;
 
        BooleanFunction& operator-=(const BooleanFunction& other);
 
        BooleanFunction operator*(const BooleanFunction& other) const;
 
        BooleanFunction& operator*=(const BooleanFunction& other);
 
        bool operator==(const BooleanFunction& other) const;
 
        bool operator!=(const BooleanFunction& other) const;
 
        bool operator<(const BooleanFunction& other) const;
 
        bool is_empty() const;
 
        // Interface: Nodes, Sizes, and Checks
 
        BooleanFunction clone() const;
 
        u16 size() const;
 
        bool is(u16 type) const;
 
        bool is_variable() const;
 
        bool has_variable_name(const std::string& variable_name) const;
 
        Result<std::string> get_variable_name() const;
 
        bool is_constant() const;
 
        bool has_constant_value(const std::vector<Value>& value) const;
 
        bool has_constant_value(u64 value) const;
 
        Result<std::vector<Value>> get_constant_value() const;
 
        Result<u64> get_constant_value_u64() const;
 
        bool is_index() const;
 
        bool has_index_value(u16 index) const;
 
        Result<u16> get_index_value() const;
 
        const BooleanFunction::Node& get_top_level_node() const;
 
        u32 length() const;
 
        const std::vector<BooleanFunction::Node>& get_nodes() const;
 
        std::vector<BooleanFunction> get_parameters() const;
 
        std::set<std::string> get_variable_names() const;
 
        // Interface: String Translation
 
        std::string to_string(std::function<Result<std::string>(const BooleanFunction::Node& node, std::vector<std::string>&& operands)>&& printer = default_printer) const;
 
        static Result<BooleanFunction> from_string(const std::string& expression);
 
        // Interface: Simplification / Substitution / Evaluation
 
        BooleanFunction simplify() const;
 
        BooleanFunction simplify_local() const;
 
        BooleanFunction substitute(const std::string& old_variable_name, const std::string& new_variable_name) const;
 
        Result<BooleanFunction> substitute(const std::string& variable_name, const BooleanFunction& function) const;
 
        BooleanFunction substitute(const std::map<std::string, std::string>& substitutions) const;
 
        Result<BooleanFunction> substitute(const std::map<std::string, BooleanFunction>& substitutions) const;
 
        Result<Value> evaluate(const std::unordered_map<std::string, Value>& inputs) const;
 
        Result<std::vector<Value>> evaluate(const std::unordered_map<std::string, std::vector<Value>>& inputs) const;
 
        Result<std::vector<std::vector<Value>>> compute_truth_table(const std::vector<std::string>& ordered_variables = {}, bool remove_unknown_variables = false) const;
 
        Result<std::string> get_truth_table_as_string(const std::vector<std::string>& ordered_variables = {}, std::string function_name = "", bool remove_unknown_variables = false) const;
 
        [[deprecated("Will be removed in a future version. Use z3_utils::from_bf() in the z3_utils plugin instead.")]] z3::expr to_z3(z3::context& context,
                                                                                                                                      const std::map<std::string, z3::expr>& var2expr = {}) const;
 
    private:
        // Constructors, Destructors, Operators
 
        explicit BooleanFunction(std::vector<BooleanFunction::Node>&& nodes);
 
        template<typename... T, typename = std::enable_if_t<std::conjunction_v<std::is_same<T, BooleanFunction>...>>>
        explicit BooleanFunction(BooleanFunction::Node&& node, T&&... p)
        {
            auto size = 1;
            ((size += p.size()), ...);
            this->m_nodes.reserve(size);
 
            (this->m_nodes.insert(this->m_nodes.end(), p.m_nodes.begin(), p.m_nodes.end()), ...);
            this->m_nodes.emplace_back(std::move(node));
        }
 
        explicit BooleanFunction(BooleanFunction::Node&& node, std::vector<BooleanFunction>&& p);
 
        // Internal Interface
 
        std::string to_string_in_reverse_polish_notation() const;
 
        static Result<std::string> default_printer(const BooleanFunction::Node& node, std::vector<std::string>&& operands);
 
        static Result<std::string> algebraic_printer(const BooleanFunction::Node& node, std::vector<std::string>&& operands);
 
        static Result<BooleanFunction> validate(BooleanFunction&& function);
 
        std::vector<u32> compute_node_coverage() const;
 
        // Member
 
        std::vector<BooleanFunction::Node> m_nodes{};
    };
 
    template<>
    std::map<BooleanFunction::Value, std::string> EnumStrings<BooleanFunction::Value>::data;
 
    struct BooleanFunction::Node final
    {
        // Member
 
        u16 type;
        u16 size;
        std::vector<BooleanFunction::Value> constant{};
        u16 index{};
        std::string variable{};
 
        // Constructors, Destructors, Operators
 
        static Node Operation(u16 type, u16 size);
 
        static Node Constant(const std::vector<BooleanFunction::Value> value);
 
        static Node Index(u16 index, u16 size);
 
        static Node Variable(const std::string variable, u16 size);
 
        bool operator==(const Node& other) const;
 
        bool operator!=(const Node& other) const;
 
        bool operator<(const Node& other) const;
 
        // Interface
 
        Node clone() const;
 
        std::string to_string() const;
 
        u16 get_arity() const;
 
        static u16 get_arity_of_type(u16 type);
 
        bool is(u16 type) const;
 
        bool is_constant() const;
 
        bool has_constant_value(const std::vector<Value>& value) const;
 
        bool has_constant_value(u64 value) const;
 
        Result<std::vector<Value>> get_constant_value() const;
 
        Result<u64> get_constant_value_u64() const;
 
        bool is_index() const;
 
        bool has_index_value(u16 value) const;
 
        Result<u16> get_index_value() const;
 
        bool is_variable() const;
 
        bool has_variable_name(const std::string& variable_name) const;
 
        Result<std::string> get_variable_name() const;
 
        bool is_operation() const;
 
        bool is_operand() const;
 
        bool is_commutative() const;
 
    private:
        // Constructors, Destructors, Operators
 
        Node(u16 _type, u16 _size, std::vector<BooleanFunction::Value> _constant, u16 _index, std::string variable);
    };
 
    struct BooleanFunction::NodeType final
    {
        static constexpr u16 And = 0x0000;
        static constexpr u16 Or  = 0x0001;
        static constexpr u16 Not = 0x0002;
        static constexpr u16 Xor = 0x0003;
 
        static constexpr u16 Add  = 0x0010;
        static constexpr u16 Sub  = 0x0011;
        static constexpr u16 Mul  = 0x0012;
        static constexpr u16 Sdiv = 0x0013;
        static constexpr u16 Udiv = 0x0014;
        static constexpr u16 Srem = 0x0015;
        static constexpr u16 Urem = 0x0016;
 
        static constexpr u16 Concat = 0x0100;
        static constexpr u16 Slice  = 0x0101;
        static constexpr u16 Zext   = 0x0102;
        static constexpr u16 Sext   = 0x0103;
 
        static constexpr u16 Shl  = 0x0200;
        static constexpr u16 Lshr = 0x0201;
        static constexpr u16 Ashr = 0x0202;
        static constexpr u16 Rol  = 0x0203;
        static constexpr u16 Ror  = 0x0204;
 
        static constexpr u16 Eq  = 0x0400;
        static constexpr u16 Sle = 0x0401;
        static constexpr u16 Slt = 0x0402;
        static constexpr u16 Ule = 0x0403;
        static constexpr u16 Ult = 0x0404;
        static constexpr u16 Ite = 0x0405;
 
        static constexpr u16 Constant = 0x1000;
        static constexpr u16 Index    = 0x1001;
        static constexpr u16 Variable = 0x1002;
    };
}    // namespace hal