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