Merge pull request #4330 from JohnDumbell/jd/enhancement/gdb_pretty_printers

Add GDB pretty-printers

Author: JohnDumbell

scripts/README.md

@@ -0,0 +1,27 @@
+A collection of utility scripts and script applications.
+
+pretty-printers 
+------
+
+GDB:
+
+Pretty-printers for CBMC that enable easier debugging in IDEs and mitigate
+certain crashes due to the way some objects' memory is shared.
+
+Currently it deals with:
+* irep_idt
+* dstring
+* instructiont
+
+To install:
+
+1. Navigate to /pretty-printers/gdb.
+2. Run install.py with python 3+.
+3. If an exception occurs, create an empty '.gdbinit' file in your home
+    folder, and copy/paste the blob of code at the top of the install.py file.
+    
+The .gdbinit file is used by GDB during start-up to run any initial commands or 
+scripts, and the code injects the pretty-printers during that.
+
+Nothing else is required to get the pretty-printers to work, beside using 
+GDB to debug the code.

scripts/pretty-printers/gdb/__init__.py

@@ -0,0 +1,24 @@
+import gdb
+import pretty_printers
+
+
+def build_pretty_printer_collection():
+    
+    printers = gdb.printing.RegexpCollectionPrettyPrinter("CBMC")
+    
+    # First argument is the name of the pretty-printer, second is a regex match for which type
+    # it should be applied too, third is the class that should be called to pretty-print that type.
+    printers.add_printer(
+        'irep_idt', '^irep_idt', pretty_printers.DStringPrettyPrinter)
+    printers.add_printer(
+        'dstringt', '^dstringt', pretty_printers.DStringPrettyPrinter)
+    printers.add_printer(
+        'instructiont', '^goto_programt::instructiont', pretty_printers.InstructionPrettyPrinter)
+    return printers
+
+
+# If you change the name of this make sure to change install.py too.
+def load_pretty_printers():
+
+    # We aren't associating with a particular object file, so pass in None instead of gdb.current_objfile()
+    gdb.printing.register_pretty_printer(None, build_pretty_printer_collection(), replace=True)

scripts/pretty-printers/gdb/auto_load.py

@@ -0,0 +1,63 @@
+#!/usr/bin/env python
+
+import os
+
+# This is the code that should be copied if you're applying the changes by hand.
+# Replace {0} with the path to this folder.
+file_contents = """
+python
+import sys
+import os
+
+pretty_printer_folder = '{0}'
+if os.path.exists(pretty_printer_folder):
+    sys.path.insert(1, pretty_printer_folder)
+    import auto_load
+    auto_load.load_pretty_printers()
+end
+"""
+
+
+def create_gdbinit_file():
+    """
+    Add or append to a .gdbinit file the python code to set-up cbmc pretty-printers.
+    """
+
+    print("Attempting to enable cbmc-specific pretty-printers.")
+
+    home_folder = os.path.expanduser("~")
+    if not home_folder:
+        print(home_folder + " is an invalid home folder, please manually create a .gdbinit file and apply the code.")
+        return
+
+    gdbinit_file = os.path.join(home_folder, ".gdbinit")
+    file_write_mode = 'w'
+    if os.path.exists(gdbinit_file):
+        print(".gdbinit file exists at " + gdbinit_file + "."
+              " Please type 'y' if you want to append the pretty-printer commands to it. Press any other key to exit.")
+        while True:
+            choice = input().lower()
+            if choice == 'y':
+                file_write_mode = 'a'
+                break
+            else:
+                print("Not appending to file. Exiting.")
+                return
+
+    if file_write_mode == 'w':
+        print("Creating .gdbinit file.")
+
+    print("Adding pretty-print commands to {0}.".format(gdbinit_file))
+    parent_directory = os.path.dirname(os.path.abspath(__file__))
+    try:
+        file = open(gdbinit_file, file_write_mode)
+        file.write(file_contents.format(parent_directory))
+        file.close()
+        print("Commands added.")
+    except:
+        print("Exception occured writing to file. Please apply changes manually.")
+
+
+if __name__ == "__main__":
+    create_gdbinit_file()
+

scripts/pretty-printers/gdb/install.py

@@ -0,0 +1,48 @@
+import gdb
+
+
+class DStringPrettyPrinter:
+    def __init__(self, val):
+        self.val = val
+
+    def to_string(self):
+        try:
+            raw_address = str(self.val.address)
+
+            # If it's ::empty, we know it's empty without going further.
+            if "::empty" in raw_address:
+                return ""
+
+            # Split the address on the first space, return that value
+            # Addresses are usually {address} {optional type_name}
+            typed_pointer = '({}*){}'.format(self.val.type, raw_address.split(None, 1)[0])
+
+            # Check that the pointer is not null.
+            if gdb.parse_and_eval(typed_pointer + ' == 0'):
+                return ""
+
+            # If it isn't attempt to find the string.
+            value = '(*{})'.format(typed_pointer)
+            return gdb.parse_and_eval(value + '.c_str()')
+        except:
+            return ""
+
+    def display_hint(self):
+        return 'string'
+
+
+class InstructionPrettyPrinter:
+    def __init__(self, val):
+        self.val = val
+
+    def to_string(self):
+        try:
+            raw_address = str(self.val.address)
+            variable_accessor = '(*({}*){})'.format(self.val.type, raw_address.split(None, 1)[0])
+            expr = '{0}.to_string()'.format(variable_accessor)
+            return gdb.parse_and_eval(expr)
+        except:
+            return ""
+
+    def display_hint(self):
+        return 'string'