1#!/usr/bin/env python3 2 3import argparse 4 5 6# Read arguments 7 8parser = argparse.ArgumentParser(description='Decompile an ELF file.') 9parser.add_argument('filename', metavar='filename', type=str, 10 help='base of filename, e.g. loop for loop.elf.txt') 11parser.add_argument('--fast', dest='fast', action='store_const', 12 const=True, default=False, 13 help='fast mode skips some proofs') 14parser.add_argument('--ignore', metavar='names', type=str, nargs='?', 15 default='', 16 help='comma separated list of function names that are to be ignored (decompiler output will contain stubs for these)') 17 18args = parser.parse_args() 19 20if args.fast: 21 fast_str = 'true' 22else: 23 fast_str = 'false' 24 25 26# Run HOL 27 28import subprocess 29import io 30import sys 31import os 32 33def printn(str): 34 sys.stdout.write(str) 35 36def call_input_output(args,input_str,output_file): 37 with open('.input.txt',"w") as input: 38 input.write(input_str) 39 input.close() 40 with open('.input.txt',"r") as input, open(output_file,"wb") as out: 41 try: 42 ret = subprocess.call(args, stdin=input, stdout=out, stderr=out, universal_newlines=True, shell=True) 43 except KeyboardInterrupt: 44 print('\nInterrupted') 45 exit(1) 46 return ret 47 48elf = os.path.abspath(args.filename) 49output_file = os.path.abspath(args.filename + '_output.txt') 50 51ml_input = """ 52load "decompileLib"; 53val _ = decompileLib.decomp "{0}" {1} "{2}"; 54""" 55 56ml_input = ml_input.format(elf, fast_str, args.ignore) 57 58decompiler_dir = os.path.dirname(sys.argv[0]) 59if decompiler_dir: 60 os.chdir(decompiler_dir) 61 62printn("Building dependencies ...") 63sys.stdout.flush() 64ret = call_input_output('Holmake','','hol_output.txt') 65if ret != 0: 66 print("failed!") 67 print("Holmake failed, abandoning.") 68 print("Short failure summary:") 69 outp = os.path.abspath('hol_output.txt') 70 last_lines = list (open (outp))[-20:] 71 for l in ['\n'] + last_lines + ['\n']: 72 printn(l) 73 print("(more error information in %s )." % outp) 74 exit(1) 75print("done.") 76sys.stdout.flush() 77 78printn("Decompiling {0} ... (output in {1})".format(elf,output_file)) 79sys.stdout.flush() 80call_input_output('hol',ml_input,output_file) 81last_lines = list (open (output_file))[-20:] 82summaries = [i for (i, l) in enumerate (last_lines) if l.strip() == 'Summary'] 83if not summaries: 84 print("failed!") 85 print() 86 print("Short failure summary:") 87 for l in ['\n'] + last_lines + ['\n']: 88 printn(l) 89 print("(more information in %s )" % output_file) 90 exit(1) 91print("done.") 92for l in [''] + last_lines[summaries[-1]:]: 93 printn(l) 94sys.stdout.flush() 95