irep_idt pretty printer improvements

scripts/pretty-printers/gdb/install.py

@@ -1,63 +1,70 @@
-#!/usr/bin/env python
+#!/usr/bin/env python3
 
 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
-"""
+from shutil import copyfile
 
 
 def create_gdbinit_file():
     """
-    Add or append to a .gdbinit file the python code to set-up cbmc pretty-printers.
+    Create and insert into 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.")
+        print(home_folder + " is an invalid home folder, can't auto-configure .gdbinit.")
         return
 
+    # This is the code that should be copied if you're applying the changes by hand.
+    gdb_directory = os.path.dirname(os.path.abspath(__file__))
+    code_block_start = "cbmc_printers_folder = "
+    code_block = \
+        [
+            "{0}'{1}'".format(code_block_start, gdb_directory),
+            "if os.path.exists(cbmc_printers_folder):",
+            "    sys.path.insert(1, cbmc_printers_folder)",
+            "    from pretty_printers import load_cbmc_printers",
+            "    load_cbmc_printers()",
+        ]
+
     gdbinit_file = os.path.join(home_folder, ".gdbinit")
-    file_write_mode = 'w'
+    lines = []
     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.")
+        with open(gdbinit_file, 'r') as file:
+            lines = [ line.rstrip() for line in file ]
+    line_no = 0
+    imports = { "os", "sys" }
+    while line_no < len(lines):
+        if lines[line_no].startswith('import '):
+            imports.add(lines[line_no][len("import "):].strip())
+            lines.pop(line_no)
+        else:
+            if lines[line_no].startswith(code_block_start):
+                print(".gdbinit already contains our pretty printers, not changing it")
                 return
+            line_no += 1
+    while len(lines) != 0 and (lines[0] == "" or lines[0] == "python"):
+        lines.pop(0)
 
-    if file_write_mode == 'w':
-        print("Creating .gdbinit file.")
+    lines = [ "python" ] + list(map("import {}".format, sorted(imports))) + [ "", "" ] + code_block + [ "", "" ] + lines + [ "" ]
 
+    backup_file = os.path.join(home_folder, "backup.gdbinit")
+    if os.path.exists(backup_file):
+        print("backup.gdbinit file already exists. Type 'y' if you would like to overwrite it or any other key to exit.")
+        choice = input().lower()
+        if choice != 'y':
+            return
+    print("Backing up {0}".format(gdbinit_file))
+    copyfile(gdbinit_file, backup_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()
+        with open(gdbinit_file, 'w+') as file:
+            file.write('\n'.join(lines))
         print("Commands added.")
     except:
         print("Exception occured writing to file. Please apply changes manually.")
 
 
 if __name__ == "__main__":
     create_gdbinit_file()
-

scripts/pretty-printers/gdb/pretty_printers.py

@@ -1,11 +1,17 @@
 import gdb
 
 
+# Class for pretty-printing dstringt
 class DStringPrettyPrinter:
+    "Print a dstringt"
+
     def __init__(self, val):
         self.val = val
 
     def to_string(self):
+        # ideally, we want to access the memory where the string
+        # is stored directly instead of calling a function. However,
+        # this is simpler.
         try:
             raw_address = str(self.val.address)
 
@@ -15,20 +21,32 @@ def to_string(self):
 
             # 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])
+            typed_pointer = "((const {} *){})".format(self.val.type, raw_address.split(None, 1)[0])
+
+            string_no = self.val["no"]
 
             # Check that the pointer is not null.
-            if gdb.parse_and_eval(typed_pointer + ' == 0'):
+            null_ptr = gdb.parse_and_eval("{} == 0".format(typed_pointer))
+            if null_ptr.is_optimized_out:
+                return "{}: <Ptr optimized out>".format(string_no)
+            if null_ptr:
                 return ""
 
-            # If it isn't attempt to find the string.
-            value = '(*{})'.format(typed_pointer)
-            return gdb.parse_and_eval(value + '.c_str()')
+            table_len = gdb.parse_and_eval("get_string_container().string_vector.size()")
+            if table_len.is_optimized_out:
+                return "{}: <Table len optimized out>".format(string_no)
+            if string_no >= table_len:
+                return "{} index ({}) out of range".format(self.val.type, string_no)
+
+            value = gdb.parse_and_eval("{}->c_str()".format(typed_pointer))
+            if value.is_optimized_out:
+                return "{}: <Optimized out>".format(string_no)
+            return "{}: \"{}\"".format(string_no, value.string().replace("\0", "").replace("\"", "\\\""))
         except:
             return ""
 
     def display_hint(self):
-        return 'string'
+        return None
 
 
 class InstructionPrettyPrinter:
@@ -38,11 +56,23 @@ def __init__(self, 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)
+            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'
+        return "string"
+
+
+# If you change the name of this make sure to change install.py too.
+def load_cbmc_printers():
+    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("dstringt", "^(?:dstringt|irep_idt)", DStringPrettyPrinter)
+    printers.add_printer("instructiont", "^goto_programt::instructiont", InstructionPrettyPrinter)
+    # We aren't associating with a particular object file, so pass in None instead of gdb.current_objfile()
+    gdb.printing.register_pretty_printer(None, printers, replace=True)