summary.py 7.82 KB
Newer Older
1
2
3
4
5
6
#!/usr/bin/env python3
#-*- coding: utf-8 -*-
##########################################################################
#                                                                        #
#  This file is part of Frama-C.                                         #
#                                                                        #
Andre Maroneze's avatar
Andre Maroneze committed
7
#  Copyright (C) 2007-2020                                               #
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
#    CEA (Commissariat à l'énergie atomique et aux énergies              #
#         alternatives)                                                  #
#                                                                        #
#  you can redistribute it and/or modify it under the terms of the GNU   #
#  Lesser General Public License as published by the Free Software       #
#  Foundation, version 2.1.                                              #
#                                                                        #
#  It is distributed in the hope that it will be useful,                 #
#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         #
#  GNU Lesser General Public License for more details.                   #
#                                                                        #
#  See the GNU Lesser General Public License version 2.1                 #
#  for more details (enclosed in the file licenses/LGPLv2.1).            #
#                                                                        #
##########################################################################

import re
import sys
import subprocess
import time
import os
import signal
import argparse
import uuid

import frama_c_results
import results_display
import benchmark_database

class OperationException(Exception):
    pass

def build_env(framac):
    if framac is None:
        return { **os.environ }
    else:
        bindir = framac + '/build/bin'
        return { **os.environ,  'PATH' : bindir + ':' + os.environ['PATH'] }

48
def list_targets(dir):
49
50
    env = build_env(framac)
    res = subprocess.run(
51
        ["make", "--directory", dir, "--quiet", "display-targets"],
52
53
54
        env=env,
        stdout=subprocess.PIPE,
        encoding='ascii')
55
56
57
    targets = res.stdout.split()
    res = []
    for target in targets:
58
59
60
        target_path = f"{dir}/{target}"
        if os.path.isdir(target_path):
            res.append(target_path)
61
        else:
62
            raise OperationException(f"target is not a directory: {target_path}")
63
    return res
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82

def clone_frama_c(clonedir, hash):
    print("Cloning Frama-C", hash, "...")
    res = subprocess.run(
        ["./scripts/clone.sh", "--clone-dir", clonedir, hash],
        stdout=subprocess.PIPE,
        encoding='ascii')
    if res.returncode != 0:
        raise OperationException("Cannot clone repository. Try to manually"
            "remove the broken clone in " + clonedir)
    return res.stdout.strip()

def run_make(framac, benchmark_tag=None):
    args = ['make', '--keep-going', 'all']
    env = build_env(framac)
    if not framac is None:
        bindir = framac + '/build/bin'
        args += [
            'FRAMAC_DIR=' + bindir,
83
            'FRAMAC=' + bindir + '/frama-c']
84
    if benchmark_tag is None:
85
        args += ['-j', str(os.cpu_count ())]
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
    else:
        args += ['BENCHMARK=' + benchmark_tag]
    return subprocess.Popen(args, env=env,
        stdout=subprocess.DEVNULL,
        stderr=subprocess.PIPE,
        preexec_fn=os.setsid)

def terminate_process(process):
    if process is None:
        return b""
    else:
        try:
            os.killpg(os.getpgid(process.pid), signal.SIGTERM)
            pass
        except ProcessLookupError:
            pass
        output,errors = process.communicate()
        return errors

def smart_rename(target):
106
    target = re.sub('^\./', '', target)
107
108
    target = re.sub('main\.eva$', '', target)
    target = re.sub('\.eva$', '', target)
109
    target = re.sub('\.frama-c/', '', target)
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
    target = re.sub('qds/frama-c', 'qds', target)
    return target

def is_running(target):
    return os.path.isfile(target + '/running')

def poll_results(targets, benchmark_tag):
    results = []
    for target in targets:
        filename = target + '/stats.txt'
        result = frama_c_results.read(filename)
        result["target"] = target
        result["target_name"] = smart_rename(target)
        result["is_running"] = is_running(target)
        result["up_to_date"] = benchmark_tag is None or benchmark_tag == result['benchmark_tag']
        results.append(result);
    return results


def run_analyses(display, database, framac, benchmark_tag):
    results = []
131
    targets = list_targets(".")
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
    process = run_make(framac, benchmark_tag)
    errors = b""
    next_poll = time.time()

    def update():
        nonlocal  display, database, targets, benchmark_tag, results
        results = poll_results(targets, benchmark_tag)
        if not database is None:
            database.update(results)
        display.needs_update = True

    try:
        while process.poll() is None:
            if time.time() >= next_poll:
                update()
                next_poll = time.time() + 2.0
            display.process_inputs()
            if display.needs_update:
                display.print_table(results)
            time.sleep(0.05)
        update()
    except (KeyboardInterrupt, results_display.UserExitRequest):
        print("Analyzes interrupted by user.")
    except Exception as e:
        # terminate_process below is somehow blocking the exception printing
        errors += bytearray(str(e), 'ascii')
        raise e
    finally:
        errors += terminate_process(process)
    return results,errors


parser = argparse.ArgumentParser(
    description="Run analyses and summarize the results. Must be run in a "
                "directory with a Makefile having two rules: 'all', a target "
                "that runs the analysis, and 'display-targets', the target that "
                "lists the built results.")
parser.add_argument('rev', nargs='?', metavar="REVISION",
    help="a Frama-C revision to use for analyses (default: use the "
        "default configuration for Frama-C)")
parser.add_argument('-b', '--benchmark',
    action="store_true",
    help="sets benchmark mode: do not run analyses in parallel and rerun all "
        "analyses")
parser.add_argument('-v', '--vs',
    action="store", metavar="REVISION", default="master",
    help="a revision to compare the results to")
parser.add_argument('-c', '--comment',
    action="store", metavar="COMMENT",
    help="when benchmarking, add this comment inside the database")
parser.add_argument('-p', '--repository-path',
    action="store", metavar="PATH",
    help="don't clone Frama-C, use this git repository instead")


errors = b''

try:
    args = parser.parse_args()

    if args.repository_path is None:
        if args.rev is None:
            gitdir = None
            framac = None
        else:
            clonedir = "./frama-c-clones"
            gitdir = clonedir + "/frama-c.git"
            framac = clone_frama_c(clonedir, args.rev)
    else:
        framac = args.repository_path
        gitdir = framac

    if args.benchmark:
        benchmark_tag=str(uuid.uuid1())
        print("Running benchmarks with benchmark tag", benchmark_tag, "...")
    else:
        benchmark_tag=None
        print("Running analyses ...")

    benchmark_comment = args.comment

    if gitdir is None:
        database = None
    else:
        database = benchmark_database.Database(benchmark_tag, benchmark_comment,
            gitdir, args.rev, args.vs)

    results,errors = results_display.wrapper(run_analyses, database, framac,
        benchmark_tag, curses=True)

    print("Results:\n")
    results_display.PlainDisplay().print_table(results)

except OperationException as e:
    errors += bytearray(str(e), 'ascii')

sys.stderr.buffer.write(errors + b'\n')