From 423b8c8a9483351d53ee17d5fa8e7c2225cd2cda Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Mon, 18 Mar 2019 18:21:42 +0100
Subject: [PATCH] [fcscript] Add a script to monitor and summarize multiple
analyses
---
Makefile | 18 +-
bin/frama-c-script | 9 +
headers/header_spec.txt | 9 +-
share/analysis-scripts/benchmark_database.py | 177 +++++++++++++
share/analysis-scripts/clone.sh | 91 +++++++
share/analysis-scripts/find_fun.py | 2 +-
share/analysis-scripts/frama_c_results.py | 73 ++++++
share/analysis-scripts/git_utils.py | 59 +++++
share/analysis-scripts/list_files.py | 2 +-
share/analysis-scripts/results_display.py | 255 +++++++++++++++++++
share/analysis-scripts/summary.py | 219 ++++++++++++++++
11 files changed, 906 insertions(+), 8 deletions(-)
create mode 100644 share/analysis-scripts/benchmark_database.py
create mode 100755 share/analysis-scripts/clone.sh
create mode 100644 share/analysis-scripts/frama_c_results.py
create mode 100644 share/analysis-scripts/git_utils.py
create mode 100644 share/analysis-scripts/results_display.py
create mode 100755 share/analysis-scripts/summary.py
diff --git a/Makefile b/Makefile
index d007948e544..c451aa21fec 100644
--- a/Makefile
+++ b/Makefile
@@ -251,16 +251,21 @@ DISTRIB_FILES:=\
Changelog config.h.in \
VERSION VERSION_CODENAME $(wildcard licenses/*) \
$(LIBC_FILES) \
+ share/analysis-scripts/benchmark_database.py \
share/analysis-scripts/cmd-dep.sh \
share/analysis-scripts/concat-csv.sh \
+ share/analysis-scripts/clone.sh \
$(wildcard share/analysis-scripts/examples/*) \
share/analysis-scripts/find_fun.py \
share/analysis-scripts/flamegraph.pl \
share/analysis-scripts/frama-c.mk \
+ share/analysis-scripts/frama_c_results.py \
+ share/analysis-scripts/git_utils.py \
share/analysis-scripts/list_files.py \
share/analysis-scripts/parse-coverage.sh \
- share/analysis-scripts/summary.sh \
share/analysis-scripts/README.md \
+ share/analysis-scripts/results_display.py \
+ share/analysis-scripts/summary.py \
share/analysis-scripts/template.mk \
$(wildcard share/emacs/*.el) share/autocomplete_frama-c \
share/_frama-c \
@@ -1898,15 +1903,20 @@ install:: install-lib
share/configure.ac share/autocomplete_frama-c share/_frama-c \
$(FRAMAC_DATADIR)
$(MKDIR) $(FRAMAC_DATADIR)/analysis-scripts
- $(CP) share/analysis-scripts/cmd-dep.sh \
+ $(CP) share/analysis-scripts/benchmark_database.py \
+ share/analysis-scripts/cmd-dep.sh \
share/analysis-scripts/concat-csv.sh \
+ share/analysis-scripts/clone.sh \
share/analysis-scripts/find_fun.py \
share/analysis-scripts/flamegraph.pl \
share/analysis-scripts/frama-c.mk \
+ share/analysis-scripts/frama_c_results.py \
+ share/analysis-scripts/git_utils.py \
+ share/analysis-scripts/list_files.py \
share/analysis-scripts/parse-coverage.sh \
share/analysis-scripts/README.md \
- share/analysis-scripts/list_files.py \
- share/analysis-scripts/summary.sh \
+ share/analysis-scripts/results_display.py \
+ share/analysis-scripts/summary.py \
share/analysis-scripts/template.mk \
$(FRAMAC_DATADIR)/analysis-scripts
$(MKDIR) $(FRAMAC_DATADIR)/analysis-scripts/examples
diff --git a/bin/frama-c-script b/bin/frama-c-script
index b46c6944edc..b797957eeb5 100755
--- a/bin/frama-c-script
+++ b/bin/frama-c-script
@@ -54,6 +54,11 @@ if [ $# -lt 1 ]; then
echo " Lists files in [dirs] declaring or defining <function-name>"
echo " (defaults to PWD + /usr/include)."
echo " Heuristics-based: neither correct nor complete."
+ echo ""
+ echo " - summary [options]"
+ echo " Monitors and summarizes multiple analyses dispatched by a Makefile"
+ echo " in the current PWD."
+ echo " Use $0 summary --help for more informations."
exit
fi
@@ -201,6 +206,10 @@ case "$command" in
shift;
flamegraph "$@";
;;
+ "summary")
+ shift;
+ ${FRAMAC_SHARE}/analysis-scripts/summary.py "$@";
+ ;;
*)
echo "error: unrecognized command: $command"
esac
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 5666f1680d5..5960673ee93 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -113,8 +113,10 @@ ptests/.gitignore: .ignore
ptests/.merlin: .ignore
ptests/ptests.ml: CEA_LGPL
share/_frama-c: CEA_LGPL
+share/analysis-scripts/benchmark_database.py: .ignore
+share/analysis-scripts/clone.sh: .ignore
share/analysis-scripts/frama-c.mk: CEA_LGPL
-share/analysis-scripts/README.md: .ignore
+share/analysis-scripts/frama_c_results.py: .ignore
share/analysis-scripts/cmd-dep.sh: .ignore
share/analysis-scripts/concat-csv.sh: .ignore
share/analysis-scripts/examples/example.c: .ignore
@@ -124,9 +126,12 @@ share/analysis-scripts/examples/example-slevel.mk: .ignore
share/analysis-scripts/examples/Makefile: .ignore
share/analysis-scripts/find_fun.py: .ignore
share/analysis-scripts/flamegraph.pl: CDDL
+share/analysis-scripts/git_utils.py: .ignore
share/analysis-scripts/list_files.py: .ignore
share/analysis-scripts/parse-coverage.sh: .ignore
-share/analysis-scripts/summary.sh: .ignore
+share/analysis-scripts/README.md: .ignore
+share/analysis-scripts/results_display.py: .ignore
+share/analysis-scripts/summary.py: .ignore
share/analysis-scripts/template.mk: .ignore
share/autocomplete_frama-c: CEA_LGPL
share/Makefile.clean: CEA_LGPL
diff --git a/share/analysis-scripts/benchmark_database.py b/share/analysis-scripts/benchmark_database.py
new file mode 100644
index 00000000000..0f74d2c8084
--- /dev/null
+++ b/share/analysis-scripts/benchmark_database.py
@@ -0,0 +1,177 @@
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2019 #
+# 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 time
+import os
+import csv
+import sqlite3
+
+import git_utils
+
+def dict_factory(cursor, row):
+ d = {}
+ for idx, col in enumerate(cursor.description):
+ d[col[0]] = row[idx]
+ return d
+
+
+class Database:
+ inserted_targets = {}
+
+ def __init__(self, benchmark_tag, benchmark_comment, gitdir, analyzer_rev, reference_rev):
+ self.benchmark_tag = benchmark_tag
+ self.benchmark_comment = benchmark_comment
+ if analyzer_rev is None:
+ self.analyzer_hash = None
+ self.analyzer = None
+ else:
+ self.analyzer_hash = git_utils.rev_parse(gitdir, analyzer_rev)
+ self.analyzer = git_utils.name_rev(gitdir, analyzer_rev)
+ self.reference_hash = git_utils.rev_parse(gitdir, reference_rev)
+ self.connection = sqlite3.connect('benchmark-results.db')
+ self.connection.row_factory = dict_factory
+ self.setup_rdb()
+ self.reference_results = self.query_rdb(self.reference_hash)
+
+ def update(self, results):
+ if not self.benchmark_tag is None:
+ for result in results:
+ inserted = result["target"] in self.inserted_targets
+ if result["up_to_date"] and not inserted:
+ self.insert(result)
+ self.inserted_targets[result["target"]] = True
+
+ for result in results:
+ if result['target'] in self.reference_results:
+ ref = self.reference_results[result['target']]
+ def compute_diff(column, ratio):
+ nonlocal result, ref
+ try:
+ if ratio:
+ diff = result[column] / ref[column] - 1.0
+ else:
+ diff = result[column] - ref[column]
+ except TypeError:
+ diff =None
+ result['diff_' + column] = diff
+
+ compute_diff('alarms', False)
+ compute_diff('warnings', False)
+ compute_diff('user_time', True)
+ compute_diff('memory', True)
+ compute_diff('coverage', False)
+ else:
+ result['diff_alarms'] = None
+ result['diff_warnings'] = None
+ result['diff_user_time'] = None
+ result['diff_memory'] = None
+ result['diff_coverage'] = None
+
+ def insert_csv(self, result):
+ filename="benchmark-results.csv"
+ file_already_exists=os.path.isfile(filename)
+ fieldnames = [
+ 'benchmark_tag', 'timestamp',
+ 'analyzer', 'analyzer_hash',
+ 'target', 'target_hash',
+ 'user_time', 'memory', 'alarms', 'warnings',
+ 'sem_reach_fun', 'syn_reach_fun', 'total_fun',
+ 'sem_reach_stmt', 'syn_reach_stmt',
+ 'cmd_args', 'benchmark_comment']
+ with open(filename, 'a', newline='') as file:
+ writer = csv.DictWriter(file,
+ fieldnames=fieldnames, extrasaction='ignore',
+ delimiter="\t", quotechar='"')
+ if not file_already_exists:
+ writer.writeheader()
+ writer.writerow(result)
+
+ def insert(self, result):
+ completed_result = { **result,
+ 'benchmark_tag' : self.benchmark_tag,
+ 'benchmark_comment' : self.benchmark_comment,
+ 'target_hash' : git_utils.current_rev(result["target"]),
+ 'analyzer' : self.analyzer,
+ 'analyzer_hash' : self.analyzer_hash }
+ self.insert_csv(completed_result)
+ self.insert_rdb(completed_result)
+
+ def setup_rdb(self):
+ cursor = self.connection.cursor()
+ cursor.execute(
+ "CREATE TABLE IF NOT EXISTS benchmark_results ("
+ "benchmark_tag TEXT NOT NULL,"
+ "timestamp TEXT NOT NULL,"
+ "analyzer TEXT NOT NULL,"
+ "analyzer_hash TEXT NOT NULL,"
+ "target TEXT NOT NULL,"
+ "target_hash TEXT NOT NULL,"
+ "user_time REAL NOT NULL,"
+ "memory INTEGER NOT NULL,"
+ "alarms INTEGER NOT NULL,"
+ "warnings INTEGER NOT NULL,"
+ "sem_reach_fun INTEGER NOT NULL,"
+ "syn_reach_fun INTEGER NOT NULL,"
+ "total_fun INTEGER NOT NULL,"
+ "sem_reach_stmt INTEGER NOT NULL,"
+ "syn_reach_stmt INTEGER NOT NULL,"
+ "cmd_args TEXT NOT NULL,"
+ "benchmark_comment TEXT);")
+ self.connection.commit()
+
+ def insert_rdb(self, result):
+ cursor = self.connection.cursor()
+ cursor.execute(
+ "INSERT INTO benchmark_results("
+ "benchmark_tag, timestamp, "
+ "analyzer, analyzer_hash, target, target_hash, "
+ "user_time, memory, alarms, warnings, "
+ "sem_reach_fun, syn_reach_fun, total_fun, "
+ "sem_reach_stmt, syn_reach_stmt, "
+ "cmd_args, benchmark_comment) "
+ "VALUES("
+ "DATETIME('now','localtime'), "
+ ":benchmark_tag, :analyzer, "
+ ":analyzer_hash, :target, :target_hash, "
+ ":user_time, :memory, :alarms, :warnings, "
+ ":sem_reach_fun, :syn_reach_fun, :total_fun, "
+ ":sem_reach_stmt, :syn_reach_stmt, "
+ ":cmd_args, :benchmark_comment)", result)
+ self.connection.commit()
+
+ def query_rdb(self, analyzer_hash):
+ cursor = self.connection.cursor()
+ cursor.execute(
+ "SELECT "
+ "target, "
+ "avg(user_time) as user_time, avg(memory) as memory, "
+ "min(alarms) as alarms, min(warnings) as warnings, "
+ "max(sem_reach_stmt) as sem_reach_stmt, "
+ "max(syn_reach_stmt) as syn_reach_stmt "
+ "FROM benchmark_results "
+ "WHERE analyzer_hash=? "
+ "GROUP BY target", (analyzer_hash,))
+ results = {}
+ for r in cursor.fetchall():
+ r['coverage'] = r['sem_reach_stmt'] / r['syn_reach_stmt']
+ results[r['target']] = r
+ return results
diff --git a/share/analysis-scripts/clone.sh b/share/analysis-scripts/clone.sh
new file mode 100755
index 00000000000..19fe1a82afc
--- /dev/null
+++ b/share/analysis-scripts/clone.sh
@@ -0,0 +1,91 @@
+#!/bin/bash -eu
+
+git_hash="master"
+clone_dir="frama-c-clones"
+repository_path="git@git.frama-c.com:frama-c/frama-c"
+show_usage=""
+
+while [[ $# > 0 ]]
+do
+ case $1 in
+ -d|--clone-dir)
+ clone_dir="$2"
+ shift
+ ;;
+
+ -p|--repository-path)
+ repository_path="$2"
+ shift
+ ;;
+
+ -h|--help)
+ show_usage="yes"
+ ;;
+
+ *)
+ git_hash="$1"
+ ;;
+ esac
+ shift
+done
+
+if [ -n "$show_usage" ]
+then
+ echo "Usage: $0 HASH"
+ echo "Provides a working tree of Frama-C."
+ echo ""
+ echo "The following arguments can be given:"
+ echo " -d, --clone-dir path to the directory where frama-c versions are"
+ echo " cloned"
+ echo " -p, --repository-path PATH do not clone from frama-c gitlab, use this path instead"
+ echo " -h, --help prints this help and quits"
+ exit 1
+fi
+
+
+bare="$clone_dir/frama-c.git"
+
+# Check if bench clone exists
+if [ ! -d "$bare" ]
+then
+ git clone --bare --quiet $repository_path "$bare"
+ sed --in-place '/bare = true/d' $bare/config
+fi
+
+# Fetch all refs
+git -C $bare fetch origin '+refs/heads/*:refs/heads/*' --prune
+
+# Resolve branch name if given
+git_hash=`git --git-dir="$bare" rev-parse "$git_hash"`
+
+# target_path must be an absolute path
+target_path="$(readlink -f "$clone_dir/$git_hash")"
+
+# Checkout
+if [ ! -e "$target_path" ]
+then
+ # The workdir cmd can extract a working tree of the desired hash
+ # without cloning once more
+ workdir_cmd=`locate git-new-workdir --limit 1`
+ if [ -z "$workdir_cmd" ]
+ then
+ git --git-dir="$bare" worktree add "$target_path" "$git_hash"
+ else
+ bash "$workdir_cmd" "$bare" "$target_path" "$git_hash"
+ fi
+fi
+
+# Build Frama-C
+if [ ! -e "$target_path/build/bin/frama-c" ]
+then
+ (
+ cd "$target_path";
+ autoconf -f --warnings=none;
+ ./configure --quiet --prefix=$(pwd)/build > /dev/null;
+ make -j > /dev/null;
+ make install > /dev/null;
+ )
+fi
+
+# Output repository path
+echo "$target_path"
diff --git a/share/analysis-scripts/find_fun.py b/share/analysis-scripts/find_fun.py
index 8451cdf1302..b8a3565da0b 100755
--- a/share/analysis-scripts/find_fun.py
+++ b/share/analysis-scripts/find_fun.py
@@ -4,7 +4,7 @@
# #
# This file is part of Frama-C. #
# #
-# Copyright (C) 2007-2018 #
+# Copyright (C) 2007-2019 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
diff --git a/share/analysis-scripts/frama_c_results.py b/share/analysis-scripts/frama_c_results.py
new file mode 100644
index 00000000000..63cdfc18288
--- /dev/null
+++ b/share/analysis-scripts/frama_c_results.py
@@ -0,0 +1,73 @@
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2019 #
+# 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
+
+stat_file_re = re.compile("^([^=]*)=(.*)$", re.MULTILINE)
+
+def load(filename):
+ data = {}
+ try:
+ with open(filename, 'r') as file:
+ content = file.read()
+ for (key,value) in stat_file_re.findall(content):
+ data[key] = value
+ except OSError:
+ pass
+ return data
+
+re_escape_space = re.compile(r'\\ ')
+
+def convert(data, key, to_type, default=None):
+ try:
+ value = data[key].strip()
+ if to_type is str:
+ value = re.sub(r'\\ ', ' ', value)
+ value = re.sub(r'\\,', ',', value)
+ return value
+ else:
+ return to_type(value)
+ except (ValueError, TypeError, KeyError):
+ return default
+
+def parse(data):
+ result = {}
+ result["timestamp"] = convert(data, "timestamp", str)
+ result["sem_reach_fun"] = convert(data, "sem_reach_fun", int)
+ result["syn_reach_fun"] = convert(data, "syn_reach_fun", int)
+ result["total_fun"] = convert(data, "total_fun", int)
+ result["sem_reach_stmt"] = convert(data, "sem_reach_stmt", int)
+ result["syn_reach_stmt"] = convert(data, "syn_reach_stmt", int)
+ result["alarms"] = convert(data, "alarms", int)
+ result["warnings"] = convert(data, "warnings", int)
+ result["user_time"] = convert(data, "user_time", float)
+ result["memory"] = convert(data, "memory", int)
+ result["cmd_args"] = convert(data, "cmd_args", str)
+ result["benchmark_tag"] = convert(data, "benchmark_tag", str)
+ if result["sem_reach_stmt"] != None and result["syn_reach_stmt"] != None:
+ result["coverage"] = result["sem_reach_stmt"] / result["syn_reach_stmt"]
+ else:
+ result["coverage"] = None
+ return result
+
+def read(filename):
+ return parse(load(filename))
diff --git a/share/analysis-scripts/git_utils.py b/share/analysis-scripts/git_utils.py
new file mode 100644
index 00000000000..7e174ebda83
--- /dev/null
+++ b/share/analysis-scripts/git_utils.py
@@ -0,0 +1,59 @@
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2019 #
+# 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 subprocess
+
+def rev_parse(gitdir, rev):
+ res = subprocess.run(
+ ['git', 'rev-parse', rev],
+ stdout=subprocess.PIPE,
+ stderr=subprocess.DEVNULL,
+ encoding='ascii',
+ cwd=gitdir)
+ name = res.stdout.strip()
+ return name if name else None
+
+def name_rev(gitdir, rev):
+ res = subprocess.run(
+ ['git', 'name-rev', '--name-only', rev],
+ stdout=subprocess.PIPE,
+ stderr=subprocess.DEVNULL,
+ encoding='ascii',
+ cwd=gitdir)
+ name = res.stdout.strip()
+ return name if name else None
+
+def current_rev(gitdir):
+ return name_rev(gitdir, "HEAD")
+
+def is_clean(gitdir):
+ # git diff and diff-index are not working on some of our case studies to
+ # decide whether the workingin dir is clean or not ; git status is more
+ # reliable
+ res = subprocess.run(
+ ['git', 'status', '--untracked-files=no', '--porcelain'],
+ stdout=subprocess.PIPE,
+ stderr=subprocess.DEVNULL,
+ encoding='ascii',
+ cwd=gitdir)
+ return res.returncode == 0 and not res.stdout
+
diff --git a/share/analysis-scripts/list_files.py b/share/analysis-scripts/list_files.py
index 859979b2286..7a1a8972dc6 100755
--- a/share/analysis-scripts/list_files.py
+++ b/share/analysis-scripts/list_files.py
@@ -4,7 +4,7 @@
# #
# This file is part of Frama-C. #
# #
-# Copyright (C) 2007-2018 #
+# Copyright (C) 2007-2019 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
diff --git a/share/analysis-scripts/results_display.py b/share/analysis-scripts/results_display.py
new file mode 100644
index 00000000000..2f368a3ce0c
--- /dev/null
+++ b/share/analysis-scripts/results_display.py
@@ -0,0 +1,255 @@
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2019 #
+# 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 string
+import curses
+
+
+sensitivity = 0.02
+
+class ResultsFormatter(string.Formatter):
+ @staticmethod
+ def format_memory(kilobytes):
+ if kilobytes < 4096:
+ return str(kilobytes) + " kiB"
+ megabytes = round(kilobytes / 1024)
+ if megabytes < 4096:
+ return str(megabytes) + " MiB"
+ gigabytes = round(megabytes / 1024)
+ return str(gygabytes) + " GiB"
+
+ @staticmethod
+ def format_time(seconds):
+ if seconds < 10:
+ return str(round(seconds,2)) + "s"
+ if seconds < 100:
+ return str(round(seconds,1)) + "s"
+ if seconds < 600:
+ return str(round(seconds)) + "s"
+ minutes = round(seconds / 60)
+ if minutes < 600:
+ return str(minutes) + "m"
+ hours = round(minutes / 60)
+ return str(hours) + "h"
+
+ @staticmethod
+ def attribute(value, inverted):
+ if value > sensitivity:
+ return "@-" if inverted else "@+"
+ elif value < -sensitivity:
+ return "@+" if inverted else "@-"
+ else:
+ return "@="
+
+ def get_field(self, field_name, args, kwargs):
+ try:
+ return super().get_field(field_name, args, kwargs)
+ except (KeyError, AttributeError):
+ return None,field_name
+
+ def format_field(self, value, format_spec):
+ if value == None:
+ return ""
+ elif format_spec.startswith('+cmp:'):
+ remainder = format_spec.split("+cmp:",1)[1]
+ return (self.attribute(value, False) +
+ self.format_field(value, remainder) + "@=")
+ elif format_spec.startswith('-cmp:'):
+ remainder = format_spec.split("-cmp:",1)[1]
+ return (self.attribute(value, True) +
+ self.format_field(value, remainder) + "@=")
+ elif format_spec == 'time':
+ return self.format_time(value)
+ elif format_spec == 'memory':
+ return self.format_memory(value)
+ else:
+ return super().format_field(value, format_spec)
+
+class UserExitRequest (Exception):
+ pass
+
+class PlainDisplay:
+ NEGATIVE = 1
+ POSITIVE = 2
+ RUNNING = 3
+ HEADER = 4
+
+ columns = [
+ {"size":64, "caption":"Case", "format":"{target_name:s}"},
+ {"size":14, "caption":"Coverage",
+ "format":"{coverage:>8.0%} {diff_coverage:+cmp:+.0%}"},
+ {"size":14, "caption":"Alarms",
+ "format":"{alarms:>8d} {diff_alarms:-cmp:+d}"},
+ {"size":14 , "caption":"Warnings",
+ "format":"{warnings:>8d} {diff_warnings:-cmp:+d}"},
+ {"size":14, "caption":"Time",
+ "format":"{user_time:time} {diff_user_time:-cmp:+.0%}"},
+ {"size":14, "caption":"Memory",
+ "format":"{memory:memory} {diff_memory:-cmp:+.0%}"}]
+
+ def __init__(self):
+ self.NEGATIVE = 0
+ self.POSITIVE = 0
+ self.RUNNING = 0
+ self.HEADER = 0
+ self.OBSOLETE = 0
+ self.needs_update = False
+
+ def write(self, text, attributes=0):
+ sys.stdout.write(text)
+
+ def rich_write(self, text, override=None, size=0):
+ attributes = 0
+ n = 0
+ for s in re.split(r'(@.)', text):
+ if s == "@=":
+ attributes = 0
+ elif s == "@+":
+ attributes = self.POSITIVE
+ elif s == "@-":
+ attributes = self.NEGATIVE
+ else:
+ n += len(s)
+ self.write(s, attributes if override is None else override)
+ if n < size:
+ self.write(' ' * (size - n), attributes if override is None else override)
+
+ fmt = ResultsFormatter()
+
+ def format(self, *args, **kwargs):
+ return self.fmt.format(*args, **kwargs)
+
+ def print_table(self, results):
+ self.write(" ", self.HEADER)
+ for column in self.columns:
+ self.write(self.format('{caption:^{size}}', **column), self.HEADER)
+ self.write(" ", self.HEADER)
+
+ self.write("\n-")
+ for column in self.columns:
+ self.write(self.format('{:-^{size}}', "", **column))
+ self.write("-")
+
+ self.write("\n")
+ for result in results:
+ self.write(" ")
+ for column in self.columns:
+ s = self.fmt.format(column["format"], **result)
+ if result["is_running"]:
+ attribute = self.RUNNING
+ elif not result["up_to_date"]:
+ attribute = self.OBSOLETE
+ else:
+ attribute = None
+ self.rich_write(s, attribute, size=column['size'])
+
+ self.write(" ")
+ self.write("\n")
+
+ self.write("\n")
+ self.needs_update = False
+
+ def process_inputs(self):
+ pass
+
+
+class CursesDisplay(PlainDisplay):
+ def __init__(self, stdscr):
+ self.stdscr = stdscr
+ #curses.mousemask(curses.ALL_MOUSE_EVENTS)
+ stdscr.nodelay(True)
+ stdscr.refresh() # Needs to be done once or nothing will be output
+
+ self.window = curses.newpad(400, 160)
+ curses.init_color(curses.COLOR_YELLOW, 300, 300, 300)
+ curses.init_pair(1, curses.COLOR_RED, 0)
+ curses.init_pair(2, curses.COLOR_GREEN, 0)
+ curses.init_pair(3, curses.COLOR_WHITE, curses.COLOR_YELLOW)
+ curses.init_pair(4, curses.COLOR_YELLOW, 0)
+ self.NEGATIVE = curses.color_pair(1)
+ self.POSITIVE = curses.color_pair(2)
+ self.RUNNING = curses.A_BLINK | curses.color_pair(3)
+ self.HEADER = curses.A_BOLD
+ self.OBSOLETE = curses.color_pair(4)
+ self.scroll_y = 0
+
+ def write(self, text, attributes=0):
+ self.window.addstr(text, attributes)
+
+ def print_table(self, results):
+ self.window.clear()
+ PlainDisplay.print_table(self, results)
+ height, width = self.stdscr.getmaxyx()
+ try:
+ self.window.refresh(0, 0, 0, 0, 1, width-1)
+ self.window.refresh(self.scroll_y+2, 0, 2, 0, height-1, width-1)
+ except Exception:
+ # getmaxyx may be out of date, especially when resizing down the
+ # window ; just ignore errors
+ pass
+
+
+ def process_inputs(self):
+ previous_y = self.scroll_y
+ c = self.stdscr.getch()
+ while c != -1:
+ if c == ord('q'):
+ raise UserExitRequest
+ elif c == curses.KEY_UP:
+ self.scroll_y -= 1
+ elif c == curses.KEY_DOWN:
+ self.scroll_y += 1
+ elif c == curses.KEY_NPAGE:
+ self.scroll_y += 10
+ elif c == curses.KEY_PPAGE:
+ self.scroll_y -= 10
+ elif c == curses.KEY_MOUSE:
+ id,x,y,z,bstate = curses.getmouse()
+ if z > 0:
+ self.scroll_y += 1
+ elif z < 0:
+ self.scroll_y -= 1
+ self.scroll_y = max(0, self.scroll_y)
+ c = self.stdscr.getch()
+ if self.scroll_y != previous_y:
+ self.needs_update = True
+
+
+def wrapper(f, *args, **kwargs):
+ if 'curses' in kwargs:
+ use_curses = kwargs['curses']
+ del kwargs['curses']
+ else:
+ use_curses = False
+
+ if use_curses:
+ def g(stdscr):
+ nonlocal f, args, kwargs
+ display = CursesDisplay(stdscr)
+ return f(display, *args, **kwargs)
+ return curses.wrapper(g)
+ else:
+ display = PlainDisplay()
+ return f(display, *args, **kwargs)
+
diff --git a/share/analysis-scripts/summary.py b/share/analysis-scripts/summary.py
new file mode 100755
index 00000000000..9c0c586ef51
--- /dev/null
+++ b/share/analysis-scripts/summary.py
@@ -0,0 +1,219 @@
+#!/usr/bin/env python3
+#-*- coding: utf-8 -*-
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2019 #
+# 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'] }
+
+def list_targets():
+ env = build_env(framac)
+ res = subprocess.run(
+ ["make", "--quiet", "display-targets"],
+ env=env,
+ stdout=subprocess.PIPE,
+ encoding='ascii')
+ return res.stdout.split()
+
+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,
+ 'FRAMAC=' + bindir + '/frama-c',
+ 'FRAMAC_CONFIG=' + bindir + '/frama-c-config']
+ if benchmark_tag is None:
+ args += ['-j', '8']
+ 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):
+ target = re.sub('main\.eva$', '', target)
+ target = re.sub('\.eva$', '', target)
+ 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 = []
+ targets = list_targets()
+ 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')
--
GitLab