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