fixed import issue

README.md

@@ -13,7 +13,7 @@ The plugin adds the following commands:
 
 More APIs can be executed through the python shell. For example, we can use the solver to _prove_ a condition for the current state:
 ``` python
->>> import seninja
+>>> import borzacchiello_seninja as seninja
 >>> s = seninja.get_current_state()
 >>> s.solver.satisfiable(extra_constraints=[s.regs.eax == 3])
 ```

apis.py

@@ -1,4 +1,4 @@
-import seninja.seninja_globals as globs
+from .seninja_globals import globs
 from binaryninja import (
     log_alert,
     log_info,

apis_ui.py

@@ -1,4 +1,4 @@
-import seninja.seninja_globals as globs
+from .seninja_globals import globs
 from .ui import (
     ui_sync_view,
     ui_reset_view,

plugin.json

@@ -9,7 +9,7 @@
       "python3"
    ],
    "description": "Symbolic execution plugin for BinaryNinja",
-   "longdescription": "# SENinja - Symbolic Execution Plugin for Binary Ninja\n![](https://github.com/borzacchiello/seninja/raw/master/pictures/screenshot.png)\nThis is a binary ninja plugin that implements a symbolic execution engine based only on z3, highly inspired by the _angr framework_ (https://angr.io/). \nThe plugin is implemented as an emulator of LLIL instructions that builds and manipulates z3 formulas. \n\nSENinja simulates a debugger: the execution is _path driven_, only one state is _active_ and executes instructions. The other states, generated at branches, are saved in a _deferred queue_. At any time, the active state can be changed with a deferred one.\n\n### Commands\nThe plugin adds the following commands:\n![](pictures/commands.png)\n\n---\n\nMore APIs can be executed through the python shell. For example, we can use the solver to _prove_ a condition for the current state:\n\n``` python\n>>> import seninja\n>>> s = seninja.get_current_state()\n>>> s.solver.satisfiable(extra_constraints=[s.regs.eax == 3])\n```\n\nthe code will check the satisfiablity of `eax == 3` given the path constraint of the active state.\n\nConsult the [wiki](https://github.com/borzacchiello/seninja/wiki) to have more info about the commands.\n\n### Settings\n\nSENinja gives to the user the possibility to configure many parts of the symbolic engine (e.g. dimension of pages, symbolic memory access strategy, etc.). \nAll the available settings can be accessed and modified by clicking on `Edit/Preferences/Settings` and selecting `SENinja` in the left widget.\n\n### UI Widgets\n\nSENinja comes with two widgets that can be used to visualize the registers and a portion of memory of the active state. The widgets can be activated by clicking on `View/Show SENinja *`. \n\n#### Buffers View\n![](https://github.com/borzacchiello/seninja/raw/master/pictures/buffers_view.png)\nThis widget allows the creation of buffers containing symbolic data.\n\n#### Register View\n![](https://github.com/borzacchiello/seninja/raw/master/pictures/register_view.png)\n\nThe Register View can be used to visualize the value of the registers of the active state. The value of a register can be modifyied by double-clicking on it. The right-click menu allows to:\n- Copy the content of the register\n- Concretize the value of the register\n- Evaluate the value of the register using the solver\n- Inject symbols\n- Show the register expression\n- Set the register to the address of a buffer created with the buffer view\n\n#### Memory View\n![](https://github.com/borzacchiello/seninja/raw/master/pictures/memory_view.png)\n\nThe Memory View can be used to visualize the value of a portion of memory of the active state. By clicking on \"monitor memory\", the user can specify a memory address to monitor. The widget will show 512 bytes starting from that address. \nThe memory view is splitted in two sections: an hexview and an ascii view. The hexview shows the hex value of each byte only if the byte is mapped and concrete. If the byte is unmapped, the characted `_` is shown; if the byte is symbolic, the widget shows the character `.`. \n\nDouble-clicking on a byte allows the user to modify its value in the active state.\nThe right-click menu allows to:\n- Copy the selection (in various format, e.g. little-endian, binary, etc.)\n- Concretize the value of the selection\n- Evaluate the value of the selection using the solver\n- Inject symbols\n\n#### Version and Dependencies\nTested with \n- binary ninja `2.1` with personal license\n- python `3.6.9` \n- z3 `4.8.7`\n\nTo make it work, you need to install z3 with pip:\n`$ pip3 install z3-solver`\n",
+   "longdescription": "# SENinja - Symbolic Execution Plugin for Binary Ninja\n![](https://github.com/borzacchiello/seninja/raw/master/pictures/screenshot.png)\nThis is a binary ninja plugin that implements a symbolic execution engine based only on z3, highly inspired by the _angr framework_ (https://angr.io/). \nThe plugin is implemented as an emulator of LLIL instructions that builds and manipulates z3 formulas. \n\nSENinja simulates a debugger: the execution is _path driven_, only one state is _active_ and executes instructions. The other states, generated at branches, are saved in a _deferred queue_. At any time, the active state can be changed with a deferred one.\n\n### Commands\nThe plugin adds the following commands:\n![](pictures/commands.png)\n\n---\n\nMore APIs can be executed through the python shell. For example, we can use the solver to _prove_ a condition for the current state:\n\n``` python\n>>> import borzacchiello_seninja as seninja\n>>> s = seninja.get_current_state()\n>>> s.solver.satisfiable(extra_constraints=[s.regs.eax == 3])\n```\n\nthe code will check the satisfiablity of `eax == 3` given the path constraint of the active state.\n\nConsult the [wiki](https://github.com/borzacchiello/seninja/wiki) to have more info about the commands.\n\n### Settings\n\nSENinja gives to the user the possibility to configure many parts of the symbolic engine (e.g. dimension of pages, symbolic memory access strategy, etc.). \nAll the available settings can be accessed and modified by clicking on `Edit/Preferences/Settings` and selecting `SENinja` in the left widget.\n\n### UI Widgets\n\nSENinja comes with two widgets that can be used to visualize the registers and a portion of memory of the active state. The widgets can be activated by clicking on `View/Show SENinja *`. \n\n#### Buffers View\n![](https://github.com/borzacchiello/seninja/raw/master/pictures/buffers_view.png)\nThis widget allows the creation of buffers containing symbolic data.\n\n#### Register View\n![](https://github.com/borzacchiello/seninja/raw/master/pictures/register_view.png)\n\nThe Register View can be used to visualize the value of the registers of the active state. The value of a register can be modifyied by double-clicking on it. The right-click menu allows to:\n- Copy the content of the register\n- Concretize the value of the register\n- Evaluate the value of the register using the solver\n- Inject symbols\n- Show the register expression\n- Set the register to the address of a buffer created with the buffer view\n\n#### Memory View\n![](https://github.com/borzacchiello/seninja/raw/master/pictures/memory_view.png)\n\nThe Memory View can be used to visualize the value of a portion of memory of the active state. By clicking on \"monitor memory\", the user can specify a memory address to monitor. The widget will show 512 bytes starting from that address. \nThe memory view is splitted in two sections: an hexview and an ascii view. The hexview shows the hex value of each byte only if the byte is mapped and concrete. If the byte is unmapped, the characted `_` is shown; if the byte is symbolic, the widget shows the character `.`. \n\nDouble-clicking on a byte allows the user to modify its value in the active state.\nThe right-click menu allows to:\n- Copy the selection (in various format, e.g. little-endian, binary, etc.)\n- Concretize the value of the selection\n- Evaluate the value of the selection using the solver\n- Inject symbols\n\n#### Version and Dependencies\nTested with \n- binary ninja `2.1` with personal license\n- python `3.6.9` \n- z3 `4.8.7`\n\nTo make it work, you need to install z3 with pip:\n`$ pip3 install z3-solver`\n",
    "license": {
       "name": "2-Clause BSD",
       "text": "Copyright 2019 Luca Borzacchiello\n\nRedistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:\n\n1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.\n\n2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.\n\nTHIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS \"AS IS\" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE."
@@ -24,6 +24,6 @@
       "Windows": "Install `z3-solver` using pip: `pip install z3-solver`",
       "Linux": "Install `z3-solver` using pip: `pip install z3-solver`"
    },
-   "version": "0.2",
+   "version": "0.2.2",
    "minimumbinaryninjaversion": 2100
 }

seninja_globals.py

@@ -1,13 +1,9 @@
-executor = None
-dfs_searcher = None
-bfs_searcher = None
-searcher_tags = {}
-_stop = False
-_running = False
-TARGET_TAG_TYPE = None
-AVOID_TAG_TYPE = None
-
-
-class SENinjaGlobManager(object):
-    # TODO write this
-    pass
+class globs(object):
+    executor = None
+    dfs_searcher = None
+    bfs_searcher = None
+    searcher_tags = {}
+    _stop = False
+    _running = False
+    TARGET_TAG_TYPE = None
+    AVOID_TAG_TYPE = None

ui/__init__.py

@@ -1,4 +1,4 @@
-import seninja.seninja_globals as globs
+from ..seninja_globals import globs
 from PySide2.QtWidgets import QApplication
 from binaryninjaui import DockHandler, UIAction, UIActionHandler, Menu
 from PySide2.QtCore import Qt
@@ -7,30 +7,28 @@
 from .buffer_view import BufferView
 from .argv_form import GetArgvDialog
 
-RW = None
-MW = None
-BW = None
+class BNWidgets(object):
+    RW = None
+    MW = None
+    BW = None
 
 
 def _get_registerview_widget(name, parent, data):
-    global RW
-    RW = RegisterView(parent, name, data)
-    RW.setEnabled(False)
-    return RW
+    BNWidgets.RW = RegisterView(parent, name, data)
+    BNWidgets.RW.setEnabled(False)
+    return BNWidgets.RW
 
 
 def _get_memoryview_widget(name, parent, data):
-    global MW
-    MW = MemoryView(parent, name, data)
-    MW.setEnabled(False)
-    return MW
+    BNWidgets.MW = MemoryView(parent, name, data, BNWidgets)
+    BNWidgets.MW.setEnabled(False)
+    return BNWidgets.MW
 
 
 def _get_buffer_view_widget(name, parent, data):
-    global BW
-    BW = BufferView(parent, name, data)
-    BW.setEnabled(False)
-    return BW
+    BNWidgets.BW = BufferView(parent, name, data)
+    BNWidgets.BW.setEnabled(False)
+    return BNWidgets.BW
 
 
 def _launchArgvDialog(context):
@@ -74,59 +72,59 @@ def _registerUIActions():
 
 
 def enable_widgets():
-    assert RW is not None
-    assert MW is not None
-    assert BW is not None
+    assert BNWidgets.RW is not None
+    assert BNWidgets.MW is not None
+    assert BNWidgets.BW is not None
 
-    RW.setEnabled(True)
-    MW.setEnabled(True)
-    BW.setEnabled(True)
+    BNWidgets.RW.setEnabled(True)
+    BNWidgets.MW.setEnabled(True)
+    BNWidgets.BW.setEnabled(True)
 
 
 def disable_widgets():
-    assert RW is not None
-    assert MW is not None
-    assert BW is not None
+    assert BNWidgets.RW is not None
+    assert BNWidgets.MW is not None
+    assert BNWidgets.BW is not None
 
-    RW.setEnabled(False)
-    MW.setEnabled(False)
-    BW.setEnabled(False)
+    BNWidgets.RW.setEnabled(False)
+    BNWidgets.MW.setEnabled(False)
+    BNWidgets.BW.setEnabled(False)
 
 
 def ui_set_arch(arch, state):
-    assert RW is not None
-    assert MW is not None
-    assert BW is not None
+    assert BNWidgets.RW is not None
+    assert BNWidgets.MW is not None
+    assert BNWidgets.BW is not None
 
-    RW.init(arch, state)
-    MW.init(arch, state)
-    BW.init(state)
+    BNWidgets.RW.init(arch, state)
+    BNWidgets.MW.init(arch, state)
+    BNWidgets.BW.init(state)
 
 
 def ui_sync_view(state, delta=True):
-    assert RW is not None
-    assert MW is not None
-    assert BW is not None
+    assert BNWidgets.RW is not None
+    assert BNWidgets.MW is not None
+    assert BNWidgets.BW is not None
 
-    if RW.isVisible():
-        RW.set_reg_values(state)
-    if MW.isVisible():
+    if BNWidgets.RW.isVisible():
+        BNWidgets.RW.set_reg_values(state)
+    if BNWidgets.MW.isVisible():
         if delta:
-            MW.update_mem_delta(state)
+            BNWidgets.MW.update_mem_delta(state)
         else:
-            MW.update_mem(state)
-    if BW.isVisible():
-        BW.update_state(state)
+            BNWidgets.MW.update_mem(state)
+    if BNWidgets.BW.isVisible():
+        BNWidgets.BW.update_state(state)
 
 
 def ui_reset_view():
-    assert RW is not None
-    assert MW is not None
-    assert BW is not None
+    assert BNWidgets.RW is not None
+    assert BNWidgets.MW is not None
+    assert BNWidgets.BW is not None
 
-    RW.reset()
-    MW.reset()
-    BW.reset()
+    BNWidgets.RW.reset()
+    BNWidgets.MW.reset()
+    BNWidgets.BW.reset()
 
 
 _registerDynamicWidgets()

ui/memory_view.py

@@ -1,4 +1,3 @@
-import seninja.ui as sui
 from binaryninja import BackgroundTaskThread
 from binaryninja.interaction import (
     show_message_box,
@@ -32,7 +31,6 @@
 from ..expr.bitvector import BVS, BVV
 from .hexview import HexViewWidget
 
-
 def _normalize_tab_name(tab_name):
     return tab_name[:tab_name.find("(")-1]
 
@@ -52,14 +50,15 @@ def run(self):
 
 class MemoryView(QWidget, DockContextHandler):
 
-    def __init__(self, parent, name, data):
+    def __init__(self, parent, name, data, bnwidgets):
         QWidget.__init__(self, parent)
         DockContextHandler.__init__(self, self, name)
 
         self.actionHandler = UIActionHandler()
         self.actionHandler.setupActionHandler(self)
         self.data = data
         self.parent = parent
+        self.bnwidgets = bnwidgets
 
         self.current_state = None
         self.arch = None
@@ -293,7 +292,7 @@ def _make_symbolic(self, address, size):
         )
         self.symb_idx += 1
         self.update_mem_delta(self.current_state)
-        sui.BW.onNewBufferSignal.emit(self.current_state)
+        self.bnwidgets.BW.onNewBufferSignal.emit(self.current_state)
 
     def _copy_big_endian(self, expr):
         mime = QMimeData()