Skip to content

Commit

Permalink
Merge pull request #372 from emsec/feature/boolean-influence
Browse files Browse the repository at this point in the history
Boolean Influence Plugin
  • Loading branch information
SJulianS committed Jan 22, 2021
2 parents 1e02dd7 + ebc7ca4 commit 2dc3428
Show file tree
Hide file tree
Showing 29 changed files with 1,328 additions and 55 deletions.
6 changes: 4 additions & 2 deletions .github/workflows/ccpp.yml
Original file line number Diff line number Diff line change
Expand Up @@ -138,8 +138,10 @@ jobs:
# See https://cmake.org/cmake/help/latest/manual/ctest.1.html for more detail
run: |
cd build
ninja -v hal_coverage
bash <(curl -s https://codecov.io/bash) -f hal_coverage.info.cleaned || echo "Codecov did not collect coverage reports"
ninja
ctest
# ninja -v hal_coverage
# bash <(curl -s https://codecov.io/bash) -f hal_coverage.info.cleaned || echo "Codecov did not collect coverage reports"
env:
LDFLAGS: "-L/usr/local/opt/qt/lib -L/usr/local/opt/llvm/lib -Wl,-rpath,/usr/local/opt/llvm/lib"
CPPFLAGS: "-I/usr/local/opt/qt/include -I/usr/local/opt/llvm/include"
Expand Down
4 changes: 2 additions & 2 deletions .gitlab-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -161,8 +161,8 @@ test:ubuntu:
- cmake -G Ninja .. -DCMAKE_BUILD_TYPE=Debug -DBUILD_ALL_PLUGINS=ON -DBUILD_TESTS=ON -DBUILD_COVERAGE=ON -DPL_GUI=ON -DBUILD_DOCUMENTATION=ON -DCMAKE_INSTALL_PREFIX=/usr/
- export CCACHE_DIR=$(pwd)/../ccache
- cmake --build . --target all --clean-first -- -j4
- ninja hal_coverage
- bash <(curl -s https://codecov.io/bash) -f hal_coverage.info.cleaned || echo "Codecov did not collect coverage reports"
# - ninja hal_coverage
# - bash <(curl -s https://codecov.io/bash) -f hal_coverage.info.cleaned || echo "Codecov did not collect coverage reports"
# - curl -s https://report.ci/upload.py | python - --include='*.xml' --framework=gtest # Upload not working
artifacts:
paths:
Expand Down
1 change: 1 addition & 0 deletions Brewfile
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ brew "qt"
brew "ccache"
brew "llvm"
brew "libomp"
brew "libopenmpt"
brew "ninja"
brew "cmake"
brew "flex"
Expand Down
4 changes: 4 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,10 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).

## [Unreleased]
* added plugin `boolean_influence` that enables calculation of the boolean influence for each FF depending on the predecessing FFs
* extended the `z3_utils` plugin with a `z3Wrapper` class, which holds exactly one `z3::expr` and the corresponding `z3::context`
* removed the code coverage checks from the macOS pipeline and added test command, so the macOS pipeline will work again properly
* fixed a bug in DANA, where sometimes the net names were output in the DANA results instead of the gate names

## [3.2.3] - 2021-01-18 18:30:00+02:00 (urgency: medium)
* fixed `z3_utils` plugin being disabled by default causing linking errors
Expand Down
2 changes: 1 addition & 1 deletion Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ RUN apt-get update && apt-get install -y apt-transport-https ca-certificates gnu
build-essential lsb-release git cmake pkgconf libspdlog-dev libboost-all-dev qt5-default libpython3.8-dev \
pybind11-dev build-essential libyaml-cpp-dev ccache autoconf autotools-dev flex bison libsodium-dev libqt5svg5-dev libqt5svg5* ninja-build lcov gcovr graphviz \
python3-sphinx doxygen python3-sphinx-rtd-theme python3-jedi flex bison devscripts debhelper dh-make pkgconf gnupg2 pybind11-dev python3-pybind11 \
python3-paramiko rapidjson-dev libspdlog-dev libigraph0-dev python3-dateutil libz3-dev\
python3-paramiko rapidjson-dev libspdlog-dev libigraph0-dev python3-dateutil libz3-dev libomp-dev\
&& apt-get clean \
&& rm -rf /var/lib/apt/lists/*
CMD cmake -G Ninja /home/src -DCMAKE_BUILD_TYPE=MinSizeRel -DBUILD_ALL_PLUGINS=OFF -DPL_GRAPH_ALGORITHM=ON -DPL_GATE_DECORATOR_SYSTEM=ON -DBUILD_TESTS=ON -PL_GUI=ON -DCMAKE_INSTALL_PREFIX=/usr/ -DCPACK_OUTPUT_FILE_PREFIX=/home/build-output/ && \
Expand Down
6 changes: 6 additions & 0 deletions cmake/detect_dependencies.cmake
Original file line number Diff line number Diff line change
Expand Up @@ -84,6 +84,12 @@ else()
endif()
endif()

if(OPENMP_FOUND)
message(STATUS "openMP found")
else()
message(STATUS "openMP not found")
endif()

################################
##### Filesystem
################################
Expand Down
2 changes: 1 addition & 1 deletion install_dependencies.sh
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ elif [[ "$platform" == 'linux' ]]; then
sudo apt-get update && sudo apt-get install -y build-essential lsb-release git cmake pkgconf qt5-default \
libpython3-dev ccache autoconf autotools-dev libsodium-dev libigraph0-dev \
libqt5svg5-dev libqt5svg5* ninja-build lcov gcovr python3-sphinx doxygen python3-sphinx-rtd-theme python3-jedi python3-pip pybind11-dev python3-pybind11 rapidjson-dev libspdlog-dev libz3-dev\
graphviz # For documentation
graphviz libomp-dev # For documentation
sudo pip3 install -r requirements.txt
elif [[ "$distribution" == "Arch" ]]; then
yay -S --needed base-devel lsb-release git cmake pkgconf \
Expand Down
2 changes: 1 addition & 1 deletion packaging/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,7 @@ if(CPACK_GENERATORS)
set(CPACK_DEBIAN_PACKAGE_SECTION libs)
set(CPACK_DEBIAN_PACKAGE_PRIORITY optional)
set(CPACK_DEBIAN_PACKAGE_DEPENDS "libstdc++6 (>= 6.3)" "libgomp1 (>= 6.3)" "libc6 (>= 2.24)" "libqt5widgets5 (>= 5.7)" "libqt5concurrent5 (>= 5.7)" "python3 (>= 3.6)" "python3-pybind11 (>= 2)" "libqt5svg5-dev (>= 5.9.5)" "python3-jedi (>= 0.11)")
set(CPACK_DEBIAN_PACKAGE_BUILD_DEPENDS "pkg-config" "git" "devscripts" "dh-make" "pkgconf (>= 0.9)" "cmake (>= 3.7)" "g++ (>= 6.3)" "qt5-default (>= 5.7)" "libpython3-dev (>= 3.7)" "libqt5svg5-dev (>= 5.9.5)" "python3-sphinx (>= 1.6)" "python3-sphinx-rtd-theme (>= 0.2)" "pybind11-dev (>=2.0)" "python3-pybind11 (>=2.0)" "rapidjson-dev (>=1.1.0)" "libspdlog-dev (>= 0.16.3)" "libigraph0-dev (>= 0.7.1)" "libz3-dev (>= 4.8.7)")
set(CPACK_DEBIAN_PACKAGE_BUILD_DEPENDS "pkg-config" "git" "devscripts" "dh-make" "pkgconf (>= 0.9)" "cmake (>= 3.7)" "g++ (>= 6.3)" "qt5-default (>= 5.7)" "libpython3-dev (>= 3.7)" "libqt5svg5-dev (>= 5.9.5)" "python3-sphinx (>= 1.6)" "python3-sphinx-rtd-theme (>= 0.2)" "pybind11-dev (>=2.0)" "python3-pybind11 (>=2.0)" "rapidjson-dev (>=1.1.0)" "libspdlog-dev (>= 0.16.3)" "libigraph0-dev (>= 0.7.1)" "libz3-dev (>= 4.8.7)" "libomp-dev (>= 1:10.0)")
set(CPACK_DEBIAN_PACKAGE_CONFLICTS "hal-plugins (<= 0.0.22)")
if(NOT PPA_DEBIAN_VERSION)
set(PPA_DEBIAN_VERSION ppa1)
Expand Down
2 changes: 2 additions & 0 deletions plugins/.gitignore
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
*
!boolean_influence*
!boolean_influence/**/*
!dataflow_analysis*
!dataflow_analysis/**/*
!example_gate_library*
Expand Down
14 changes: 14 additions & 0 deletions plugins/boolean_influence/CMakeLists.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
option(PL_BOOLEAN_INFLUENCE "PL_BOOLEAN_INFLUENCE" OFF)
if(PL_BOOLEAN_INFLUENCE OR BUILD_ALL_PLUGINS)
file(GLOB_RECURSE BOOLEAN_INFLUENCE_INC ${CMAKE_CURRENT_SOURCE_DIR}/include/*.h)
file(GLOB_RECURSE BOOLEAN_INFLUENCE_SRC ${CMAKE_CURRENT_SOURCE_DIR}/src/*.cpp)
file(GLOB_RECURSE BOOLEAN_INFLUENCE_PYTHON_SRC ${CMAKE_CURRENT_SOURCE_DIR}/python/*.cpp)

hal_add_plugin(boolean_influence
SHARED
HEADER ${BOOLEAN_INFLUENCE_INC}
SOURCES ${BOOLEAN_INFLUENCE_SRC} ${BOOLEAN_INFLUENCE_PYTHON_SRC}
LINK_LIBRARIES PUBLIC ${Z3_LIBRARIES} z3_utils OpenMP::OpenMP_CXX
PYDOC SPHINX_DOC_INDEX_FILE ${CMAKE_CURRENT_SOURCE_DIR}/documentation/boolean_influence.rst
)
endif()
5 changes: 5 additions & 0 deletions plugins/boolean_influence/documentation/boolean_influence.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
Boolean Influence
==========================

.. autoclass:: boolean_influence.BooleanInfluencePlugin
:members:
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
#pragma once

#include "hal_core/plugin_system/plugin_interface_base.h"

#include "hal_core/netlist/net.h"
#include "hal_core/netlist/gate.h"

namespace hal
{
class PLUGIN_API BooleanInfluencePlugin : public BasePluginInterface
{
public:

std::string get_name() const override;
std::string get_version() const override;

void initialize() override;

/**
* Generates the function of the dataport net of the given flip-flop.
* Afterwards the generated function gets translated from a z3::expr to efficent c code, compiled, executed and evalated.G
*
* @param[in] gate - Pointer to the flip-flop which data input net is used to build the boolean function.
* @returns A mapping of the gates that appear in the function of the data net to their boolean influence in said function.
*/
std::map<Net*, double> get_boolean_influences_of_gate(const Gate* gate);

private:
std::vector<Gate*> extract_function_gates(const Gate* start, const std::string& pin);
void add_inputs(Gate* gate, std::unordered_set<Gate*>& gates);
};
}
46 changes: 46 additions & 0 deletions plugins/boolean_influence/python/python_bindings.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
#include "pybind11/operators.h"
#include "pybind11/pybind11.h"
#include "pybind11/stl.h"
#include "pybind11/stl_bind.h"
#include "hal_core/python_bindings/python_bindings.h"

#include "boolean_influence/plugin_boolean_influence.h"

namespace py = pybind11;

namespace hal
{

// the name in PYBIND11_MODULE/PYBIND11_PLUGIN *MUST* match the filename of the output library (without extension),
// otherwise you will get "ImportError: dynamic module does not define module export function" when importing the module

#ifdef PYBIND11_MODULE
PYBIND11_MODULE(boolean_influence, m)
{
m.doc() = "hal BooleanInfluencePlugin python bindings";
#else
PYBIND11_PLUGIN(boolean_influence)
{
py::module m("boolean_influence", "hal BooleanInfluencePlugin python bindings");
#endif // ifdef PYBIND11_MODULE

py::class_<BooleanInfluencePlugin, RawPtrWrapper<BooleanInfluencePlugin>, BasePluginInterface>(m, "BooleanInfluencePlugin")
.def_property_readonly("name", &BooleanInfluencePlugin::get_name)
.def("get_name", &BooleanInfluencePlugin::get_name)
.def_property_readonly("version", &BooleanInfluencePlugin::get_version)
.def("get_version", &BooleanInfluencePlugin::get_version)
.def("get_boolean_influences_of_gate", &BooleanInfluencePlugin::get_boolean_influences_of_gate, py::arg("gate"), R"(
Generates the function of the dataport net of the given flip-flop.
Afterwards the generated function gets translated from a z3::expr to efficent c code, compiled, executed and evalated.
:param halPy.Gate gate: The flip-flop which data input net is used to build the boolean function..
:returns: A mapping of the gates that appear in the function of the data net to their boolean influence in said function.
:rtype: dict
)");
;

#ifndef PYBIND11_MODULE
return m.ptr();
#endif // PYBIND11_MODULE
}
}
106 changes: 106 additions & 0 deletions plugins/boolean_influence/src/plugin_boolean_influence.cpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,106 @@
#include "boolean_influence/plugin_boolean_influence.h"

#include "z3_utils/include/plugin_z3_utils.h"

namespace hal
{
extern std::unique_ptr<BasePluginInterface> create_plugin_instance()
{
return std::make_unique<BooleanInfluencePlugin>();
}

std::string BooleanInfluencePlugin::get_name() const
{
return std::string("boolean_influence");
}

std::string BooleanInfluencePlugin::get_version() const
{
return std::string("0.1");
}

void BooleanInfluencePlugin::initialize()
{
}

std::map<Net*, double> BooleanInfluencePlugin::get_boolean_influences_of_gate(const Gate* gate)
{
if (gate->get_type()->get_base_type() != hal::GateType::BaseType::ff)
{
log_error("boolean_influence", "Can only handle flip flops but found gate type {}.", gate->get_type()->get_name());
return {};
}

// Check for the data port pin
std::unordered_set<std::string> d_ports = gate->get_type()->get_pins_of_type(GateType::PinType::data);
if (d_ports.size() != 1)
{
log_error("boolean_influence", "Can only handle flip flops with exactly 1 data port, but found {}.", d_ports.size());
return {};
}
std::string data_pin = *d_ports.begin();

// Extract all gates in front of the data port and iterate backwards until another flip flop is found.
std::vector<Gate*> function_gates = extract_function_gates(gate, data_pin);

// Generate function for the data port
z3_utils::SubgraphFunctionGenerator g;

std::unique_ptr ctx = std::make_unique<z3::context>();
std::unique_ptr func = std::make_unique<z3::expr>(*ctx);

std::unordered_set<u32> net_ids;
g.get_subgraph_z3_function(gate->get_fan_in_net(data_pin), function_gates, *ctx, *func, net_ids);

z3_utils::z3Wrapper func_wrapper = z3_utils::z3Wrapper(std::move(ctx), std::move(func));

// Generate boolean influence
std::unordered_map<u32, double> net_ids_to_inf = func_wrapper.get_boolean_influence();

// translate net_ids back to nets
std::map<Net*, double> nets_to_inf;

Netlist* nl = gate->get_netlist();
for (const auto& [net_id, inf] : net_ids_to_inf)
{
Net* net = nl->get_net_by_id(net_id);

if (net->get_sources().size() != 1)
{
log_error("boolean_influence", "Net ({}) has either multiple or 0 sources ({})", net->get_id(), net->get_sources().size());
return {};
}

nets_to_inf.insert({net, inf});
}

return nets_to_inf;
}

std::vector<Gate*> BooleanInfluencePlugin::extract_function_gates(const Gate* start, const std::string& pin)
{
std::unordered_set<Gate*> function_gates;

add_inputs(start->get_predecessor(pin)->get_gate(), function_gates);

return {function_gates.begin(), function_gates.end()};
}

void BooleanInfluencePlugin::add_inputs(Gate* gate, std::unordered_set<Gate*>& gates)
{
if (gate->is_vcc_gate() || gate->is_gnd_gate() || gate->get_type()->get_base_type() == hal::GateType::BaseType::ff || gate->get_type()->get_name().find("RAM") != std::string::npos)
{
return;
}

gates.insert(gate);
for (const auto& pre : gate->get_predecessors())
{
if (pre->get_gate() && gates.find(pre->get_gate()) == gates.end())
{
add_inputs(pre->get_gate(), gates);
}
}
return;
}
} // namespace hal
8 changes: 8 additions & 0 deletions plugins/boolean_influence/test.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
from hal_plugins import boolean_influence

pl = hal_py.plugin_manager.get_plugin_instance("boolean_influence")

g = netlist.get_gate_by_id(1547)
inf = pl.get_boolean_influences_of_gate(g)

print(inf)
Original file line number Diff line number Diff line change
Expand Up @@ -45,16 +45,7 @@ namespace hal

for (const auto& single_ff : gates)
{
auto name = state->netlist_abstr.nl->get_gate_by_id(single_ff)->get_name() + ", ";
if (state->netlist_abstr.yosys)
{
auto net = state->netlist_abstr.nl->get_gate_by_id(single_ff)->get_fan_out_net("Q");
name = state->netlist_abstr.nl->get_gate_by_id(single_ff)->get_name() + ", ";
if (net != nullptr)
{
name = net->get_name();
}
}
auto name = state->netlist_abstr.nl->get_gate_by_id(single_ff)->get_name() + ", ";
auto type = "type: " + state->netlist_abstr.nl->get_gate_by_id(single_ff)->get_type()->get_name() + ", ";
auto id = "id: " + std::to_string(state->netlist_abstr.nl->get_gate_by_id(single_ff)->get_id()) + ", ";
std::string stages = "RS: ";
Expand Down
16 changes: 9 additions & 7 deletions plugins/solve_fsm/include/solve_fsm/plugin_solve_fsm.h
Original file line number Diff line number Diff line change
Expand Up @@ -24,26 +24,28 @@ namespace hal
void initialize() override;

/**
* Generates the state graph of a finite state machine in dot format of a given fsm using z3 as sat solver.
* Generates the state graph of a finite state machine and returns a mapping from each state to a vector of all its possible successor states.
*
* @param[in] nl - Pointer to the netlist.
* @param[in] state_reg - A vector containing all the gates of the fsm representing the state register.
* @param[in] transition_logic - A vector containing all the gates of the fsm representing the transition_logic.
* @param[in] initial_state - A mapping from the state registers to their initial value. If omitted the intial state will be set to 0.
* @param[in] graph_path - Path where the transition state graph in dot format is saved.
* @param[in] timeout - Timeout value for the sat solvers. Defaults to 600000 ms.
* @returns The transition state graph in dot format.
* @returns A mapping from each state to all its successors states.
*/
std::string solve_fsm(Netlist* nl, const std::vector<Gate*> state_reg, const std::vector<Gate*> transition_logic, const std::map<Gate*, bool> initial_state = {}, const u32 timeout = 600000);
std::map<u64, std::vector<u64>> solve_fsm(Netlist* nl, const std::vector<Gate*> state_reg, const std::vector<Gate*> transition_logic, const std::map<Gate*, bool> initial_state = {}, const std::string graph_path = "", const u32 timeout = 600000);

/**
* Generates the state graph of a finite state machine in dot format of a given fsm using a simple brute force approach.
* Generates the state graph of a finite state machine and returns a mapping from each state to a vector of all its possible successor states using a simple brute force approach.
*
* @param[in] nl - Pointer to the netlist.
* @param[in] state_reg - A vector containing all the gates of the fsm representing the state register.
* @param[in] transition_logic - A vector containing all the gates of the fsm representing the transition_logic.
* @returns The transition state graph in dot format.
* @param[in] graph_path - Path where the transition state graph in dot format is saved.
* @returns A mapping from each state to all its successors states.
*/
std::string solve_fsm_brute_force(Netlist* nl, const std::vector<Gate*> state_reg, const std::vector<Gate*> transition_logic);
std::map<u64, std::vector<u64>> solve_fsm_brute_force(Netlist* nl, const std::vector<Gate*> state_reg, const std::vector<Gate*> transition_logic, const std::string graph_path="");

private:
std::map<Net*, Net*> find_output_net_to_input_net(const std::set<Gate*> state_reg);
Expand All @@ -53,7 +55,7 @@ namespace hal
FsmTransition generate_transition_with_inputs(const z3::expr& start_state, const z3::expr& state, const std::vector<u32>& inputs, const u64 input_values);
std::vector<FsmTransition> merge_transitions(const std::vector<FsmTransition>& transitions);

std::string generate_dot_graph(const Netlist* nl, const std::vector<FsmTransition>& transitions);
std::string generate_dot_graph(const Netlist* nl, const std::vector<FsmTransition>& transitions, const std::vector<Gate*>& state_reg);
std::string generate_state_transition_table(const Netlist* nl, const std::vector<FsmTransition>& transitions, const std::map<u32, z3::expr>& external_ids_to_expr);
};
} // namespace hal
2 changes: 1 addition & 1 deletion plugins/solve_fsm/include/utils/fsm_transition.h
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ namespace hal {

FsmTransition merge(const FsmTransition& other) const;
std::string to_string() const;
std::string to_dot_string(const Netlist* nl) const;
std::string to_dot_string(const Netlist* nl, const u32 state_size) const;

z3::expr starting_state_expr;
z3::expr end_state_expr;
Expand Down
Loading

0 comments on commit 2dc3428

Please sign in to comment.