1#!/usr/bin/env python 2# 3# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 4# 5# SPDX-License-Identifier: BSD-2-Clause 6# 7 8import os 9import errno 10import subprocess 11import argparse 12import shutil 13import tempfile 14import datetime 15import glob 16import time 17import re 18import numpy 19 20# Create a temporary directory 21 22 23class TempDir(object): 24 def __enter__(self, cleanup=True): 25 self.filename = tempfile.mkdtemp() 26 self.cleanup = cleanup 27 return self.filename 28 29 def __exit__(self, type, value, traceback): 30 if self.cleanup: 31 shutil.rmtree(self.filename) 32 return False 33 34 35def mkdir_p(path): 36 try: 37 os.makedirs(path) 38 except OSError as exc: 39 if exc.errno == errno.EEXIST: 40 pass 41 else: 42 raise 43 44 45def phase_sort_key(x): 46 d = { 47 "CParser": 1, 48 "L1": 2, 49 "L1except": 3, 50 "L1peep": 4, 51 "L2": 5, 52 "L2simp": 6, 53 "HL": 7, 54 "HLsimp": 8, 55 "TS": 9, 56 "polish": 10, 57 } 58 if x in d: 59 return (d[x], x) 60 return (100, x) 61 62 63def write_theory_file(f, enable_stats): 64 f.write(""" 65 theory Stats 66 imports AutoCorres 67 begin 68 69 (* %(time)s *) 70 71 declare [[record_codegen = false]] 72 declare [[allow_underscore_idents = true]] 73 74 (* Start recording times. *) 75 ML {* 76 val cpuTimer = Timer.startCPUTimer (); 77 val realTimer = Timer.startRealTimer (); 78 *} 79 80 (* Parse the C file. *) 81 install_C_file "input.c" 82 83 (* Fetch C parser times. *) 84 ML {* 85 val {sys = a, usr = b} = Timer.checkCPUTimer cpuTimer; 86 writeln ("C Parser CPU Time : " ^ (PolyML.makestring (Time.toMilliseconds a + Time.toMilliseconds b))); 87 writeln ("C Parser Real Time : " ^ (PolyML.makestring (Timer.checkRealTimer realTimer |> Time.toMilliseconds))); 88 89 val cpuTimer = Timer.startCPUTimer (); 90 val realTimer = Timer.startRealTimer (); 91 *} 92 93 (* Enable statistics. *) 94 ML {* if %(enable_stats)s then Statistics.setup_measure_fn (Statistics.complexity_measure_fn) else () *} 95 96 autocorres "input.c" 97 98 (* Fetch autocorres times. *) 99 ML {* 100 val {sys = a, usr = b} = Timer.checkCPUTimer cpuTimer; 101 writeln ("AutoCorres CPU Time : " ^ (PolyML.makestring (Time.toMilliseconds a + Time.toMilliseconds b))); 102 writeln ("AutoCorres Real Time : " ^ (PolyML.makestring (Timer.checkRealTimer realTimer |> Time.toMilliseconds))); 103 *} 104 105 end 106 """ % { 107 "time": str(datetime.datetime.now()), 108 "enable_stats": "true" if enable_stats else "false", 109 }) 110 111 112# Check usage. 113parser = argparse.ArgumentParser( 114 description='Generate statistics about AutoCorres and the C Parser.') 115parser.add_argument('input', metavar='INPUT', 116 type=str, help='Input C source file.') 117parser.add_argument('-n', '--no-isabelle', 118 default=False, action='store_true', 119 help="Don't run Isabelle, but reuse previous log file.") 120parser.add_argument('-b', '--browse', default=False, action='store_true', 121 help='Open shell in temp directory.') 122parser.add_argument('-r', '--root', action='store', type=str, 123 help='Root to l4.verified directory.', default=None) 124parser.add_argument('-R', '--repeats', action='store', 125 help='Number of runs for timing data.', default=1) 126parser.add_argument('-o', '--output', metavar='OUTPUT', 127 default="/dev/stdout", type=str, help='Output file.') 128args = parser.parse_args() 129 130if args.root == None and not args.no_isabelle: 131 parser.error("Must specify root to l4.verified directory.") 132if args.root != None: 133 args.root = os.path.abspath(args.root) 134 135output = open(args.output, "w") 136output.write("Processing %s\n\n" % args.output) 137 138# Create temp dir. 139with TempDir() as tmp_dir: 140 try: 141 # Copy file. 142 shutil.copyfile(args.input, os.path.join(tmp_dir, "input.c")) 143 144 # Get lines of code. 145 lines_of_code = int(subprocess.check_output( 146 ["c_count", args.input]).strip().split("\n")[-1]) 147 148 # Generate a root file. 149 with open(os.path.join(tmp_dir, "ROOT"), "w") as f: 150 f.write(""" 151 session Stats = AutoCorres + 152 theories 153 "Stats" 154 """) 155 156 # 157 # Pass 1: Generate statisics. 158 # 159 160 # Generate a theory file. 161 with open(os.path.join(tmp_dir, "Stats.thy"), "w") as f: 162 write_theory_file(f, enable_stats=True) 163 164 # Process theory file with Isabelle. 165 if not args.no_isabelle: 166 subprocess.check_call(["isabelle", "build", "-v", "-d", args.root, 167 "-d", ".", "-c", "Stats"], cwd=tmp_dir) 168 169 # Fetch log file. 170 log_data = subprocess.check_output( 171 ["isabelle", "env", "sh", "-c", "zcat ${ISABELLE_OUTPUT}/log/Stats.gz"]) 172 phase_lines_of_spec = {} 173 phase_term_size = {} 174 phase_num_functions = {} 175 num_functions = 0 176 for line in log_data.replace("\r", "").split("\n"): 177 if line.startswith("Defining (L1)"): 178 num_functions += 1 179 if line.startswith("SC"): 180 m = re.match("^SC: ([A-Za-z0-9]+): ([^ ]+) (\d+) LoS: (\d+)$", line) 181 if m: 182 phase = m.group(1) 183 term_size = m.group(3) 184 los = m.group(4) 185 186 for d in [phase_lines_of_spec, phase_term_size, phase_num_functions]: 187 d.setdefault(m.group(1), 0) 188 189 phase_num_functions[phase] += 1 190 phase_term_size[phase] += int(term_size) 191 phase_lines_of_spec[phase] += int(los) 192 193 output.write("\n") 194 output.write("%d input line(s) of code\n" % lines_of_code) 195 output.write("%d function(s)\n" % num_functions) 196 output.write("\n") 197 output.write("%-10s %10s %10s\n" % ("Phase", "LoS", "Term Size")) 198 199 for phase in sorted(phase_term_size.keys(), key=phase_sort_key): 200 output.write("%-10s %10d %10d\n" % (phase, 201 phase_lines_of_spec[phase], phase_term_size[phase] / phase_num_functions[phase])) 202 output.write("\n") 203 204 # 205 # Pass 2: generate timing data. 206 # 207 208 # Generate a theory file. 209 with open(os.path.join(tmp_dir, "Stats.thy"), "w") as f: 210 write_theory_file(f, enable_stats=False) 211 212 # Process theory file with Isabelle. 213 c_parser_cpu_time = [] 214 c_parser_real_time = [] 215 ac_cpu_time = [] 216 ac_real_time = [] 217 for i in xrange(int(args.repeats)): 218 if not args.no_isabelle: 219 subprocess.check_call(["isabelle", "build", "-v", "-o", "threads=1", 220 "-d", args.root, "-d", ".", "-c", "Stats"], cwd=tmp_dir) 221 222 # Fetch log file. 223 log_data = subprocess.check_output( 224 ["isabelle", "env", "sh", "-c", "zcat ${ISABELLE_OUTPUT}/log/Stats.gz"]) 225 for line in log_data.replace("\r", "").split("\n"): 226 if line.startswith("C Parser CPU Time"): 227 c_parser_cpu_time.append(int(line.split(":")[1])) 228 if line.startswith("C Parser Real Time"): 229 c_parser_real_time.append(int(line.split(":")[1])) 230 if line.startswith("AutoCorres CPU Time"): 231 ac_cpu_time.append(int(line.split(":")[1])) 232 if line.startswith("AutoCorres Real Time"): 233 ac_real_time.append(int(line.split(":")[1])) 234 235 # Generate summary data. 236 for (name, values) in [ 237 ("C Parser CPU Time", c_parser_cpu_time), 238 ("C Parser Real Time", c_parser_real_time), 239 ("AutoCorres CPU Time", ac_cpu_time), 240 ("AutoCorres Real Time", ac_real_time), 241 ]: 242 output.write("%s: %.2f (%.2f)\n" % (name, numpy.mean(values), numpy.std(values))) 243 output.write(" samples: " + (", ".join([str(x) for x in values])) + "\n") 244 245 # Open a shell in the directory if requested. 246 if args.browse: 247 print "Opening shell..." 248 subprocess.call("zsh", cwd=tmp_dir) 249 except Exception as e: 250 print "Test failed" 251 print e 252 if args.browse: 253 subprocess.call("zsh", cwd=tmp_dir) 254 raise 255