better exception handling and misc fixes

Author: borzacchiello

models/libc.py

@@ -2,7 +2,7 @@
 from ..utility.expr_wrap_util import symbolic
 from ..expr import BVV, BVS, BoolV, ITE, Or, And
 from ..utility.models_util import get_arg_k
-from ..utility.exceptions import ExitException
+from ..utility.exceptions import ExitException, ModelError
 from ..utility.string_util import as_bytes, str_to_bv_list
 from ..memory.sym_memory import InitData
 import re
@@ -34,9 +34,8 @@ def strtoul_handler(state: State, view):
     endptr = get_arg_k(state, 2, state.arch.bits() // 8, view)
     base = get_arg_k(state, 3, 4, view)
 
-    assert not symbolic(base)    # concrete model
-    assert not symbolic(endptr)  # concrete model
-    assert not symbolic(str_p)   # concrete model
+    if symbolic(base) or symbolic(endptr) or symbolic(str_p):
+        raise ModelError("strtoul", "symbolic arguments are not supported")
 
     i = 0
     str_data = b""
@@ -334,8 +333,12 @@ def _atox(state: State, view, size: int):
 
     input_p = get_arg_k(state, 1, state.arch.bits() // 8, view)
 
-    # no man. Don't make me cry
-    assert not symbolic(input_p) or not state.solver.symbolic(input_p)
+    if symbolic(input_p) and state.solver.symbolic(input_p):
+        # FIXME: I should:
+        #            1. return a fresh new symbol
+        #            2. allocate a new buffer with a concrete address
+        #            3. store the correct expression in the buffer for consistency
+        raise ModelError("atox", "symbolic input pointer (not supported)")
 
     def build_or_expression(b):
         conditions = []

plugin.json

@@ -12,7 +12,7 @@
    "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."
+      "text": "Copyright 2019-2022 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."
    },
    "platforms": [
       "Darwin",

sym_executor.py

@@ -1,3 +1,5 @@
+import sys
+
 from binaryninja import (
     BinaryReader, BinaryWriter,
     RegisterValueType, enums
@@ -360,7 +362,8 @@ def _execute_one(self):
                 self.put_in_exited(self.state)
                 self.state = None
             except exceptions.SENinjaError as err:
-                print("An error occurred: %s" % err.message)
+                sys.stderr.write("An error occurred: %s\n" % err.message)
+                self.put_in_errored(self.state, str(err))
                 self.state = None
                 self._last_error = err
                 if err.is_fatal():
@@ -389,13 +392,30 @@ def execute_one(self):
         if not self.state:
             return
 
-        single_llil_step = self.bncache.get_setting(
-            "single_llil_step") == 'true'
-        if single_llil_step:
-            res = self._execute_one()
-        else:
-            old_ip = self.ip
-            res = old_ip
-            while res == old_ip:
+        res = None
+        try:
+            single_llil_step = self.bncache.get_setting(
+                "single_llil_step") == 'true'
+            if single_llil_step:
                 res = self._execute_one()
+            else:
+                old_ip = self.ip
+                res = old_ip
+                while res == old_ip:
+                    res = self._execute_one()
+        except exceptions.SENinjaError:
+            res = None
+        except Exception as e:
+            import os
+            _, _, exc_tb = sys.exc_info()
+            fname = os.path.split(exc_tb.tb_frame.f_code.co_filename)[1]
+            sys.stderr.write("Unknown exception in SymbolicExecutor.execute_one():\n")
+            sys.stderr.write(" ".join(map(str, "\t", repr(e), fname, exc_tb.tb_lineno, "\n")))
+
+            res = None
+
+        if res is None:
+            if not self.fringe.is_empty():
+                self.select_from_deferred()
+
         return res

ui/buffer_view.py

@@ -5,19 +5,16 @@
     get_choice_input
 )
 from binaryninjaui import (
-    DockHandler,
     DockContextHandler,
     getMonospaceFont,
     UIActionHandler
 )
 from PySide6 import QtCore
 from PySide6.QtCore import Qt, QMimeData
-from PySide6.QtGui import QBrush, QColor
 from PySide6.QtWidgets import (
     QApplication,
     QVBoxLayout,
     QWidget,
-    QComboBox,
     QTableWidget,
     QTableWidgetItem,
     QMenu,

ui/hexview.py

@@ -12,18 +12,13 @@
     QItemSelection
 )
 from PySide6.QtWidgets import (
-    QApplication,
     QTableView,
     QWidget,
-    QTableWidgetItem,
-    QMainWindow,
-    QFormLayout,
     QVBoxLayout,
     QLabel,
     QSizePolicy,
     QAbstractItemView,
     QMenu,
-    QHeaderView,
     QItemDelegate,
     QSizePolicy
 )
@@ -503,7 +498,7 @@ def _handle_mouse_release(self, key_event):
 
 
 class HexViewWidget(QWidget):
-    full_data_changed = Signal(list, list, int)
+    full_data_changed = Signal(object, dict, int)
     single_data_changed = Signal(object, list)
     data_edited = Signal(object, int)
 
@@ -584,9 +579,6 @@ def _handle_data_edited(self, address, data):
         # print("edited address data", address, data)
 
     def _handle_data_changed(self, new_address, new_data, new_data_size):
-        if new_address == []:
-            return
-
         self._model.buf = new_data
         self._model.buf_size = new_data_size
         self._model.start_address = new_address

ui/memory_view.py

@@ -2,29 +2,18 @@
 from binaryninja.interaction import (
     show_message_box,
     get_int_input,
-    get_choice_input
 )
 from binaryninjaui import (
-    DockHandler,
     DockContextHandler,
-    getMonospaceFont,
     UIActionHandler
 )
-from PySide6 import QtCore
-from PySide6.QtCore import Qt, QMimeData
-from PySide6.QtGui import QBrush, QColor, QStandardItemModel, QStandardItem
+from PySide6.QtCore import QMimeData
 from PySide6.QtWidgets import (
     QApplication,
     QGridLayout,
     QWidget,
-    QComboBox,
-    QTableWidget,
-    QTableWidgetItem,
-    QStackedWidget,
     QMenu,
-    QTableView,
     QPushButton,
-    QHeaderView
 )
 
 from ..utility.expr_wrap_util import symbolic, split_bv_in_list

ui/registers_view.py

@@ -4,19 +4,16 @@
     get_choice_input
 )
 from binaryninjaui import (
-    DockHandler,
     DockContextHandler,
     getMonospaceFont,
     UIActionHandler
 )
-from PySide6 import QtCore
 from PySide6.QtCore import Qt, QMimeData
 from PySide6.QtGui import QBrush, QColor
 from PySide6.QtWidgets import (
     QApplication,
     QVBoxLayout,
     QWidget,
-    QComboBox,
     QTableWidget,
     QTableWidgetItem,
     QMenu