Add gdb pretty-printers for irep_idt and instructiont

The instructiont here is important because of the way the tree sharing
works it causes an infinite loop in the default pretty-printers.
This commit is contained in:
johndumbell 2019-02-25 15:27:13 +00:00
parent 00f125f36f
commit 655e93689e
5 changed files with 162 additions and 0 deletions

27
scripts/README.md Normal file
View File

@ -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.

View File

View File

@ -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)

View File

@ -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()

View File

@ -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'