Skip to content
Snippets Groups Projects
Commit 0b8c66d1 authored by Andre Maroneze's avatar Andre Maroneze
Browse files

Merge branch 'fix/analysis-scripts/summary' into 'master' 

[Analysis Scripts] fix summary

See merge request frama-c/frama-c!3743
parents f760bfd1 1307a91e
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
share/analysis-scripts/benchmark.sh deleted 100755 → 0
+ 0
− 199
View file @ f760bfd1
#!/bin/bash -eu
# --------------------------------------------------------------------------
# --- Command Line Parsing ---
# --------------------------------------------------------------------------
targets=""
git_hash="master"
clone_dir="frama-c-clones"
comment=""
show_usage=""
repository_path=""
makefile_path="."
output_file="benchmark-results.csv"
while [[ $# > 0 ]]
do
case $1 in
-b|--hash|--branch)
git_hash="$2"
shift
;;
-d|--clone-dir)
clone_dir="$2"
shift
;;
-c|--comment)
comment="$2"
shift
;;
-p|--repository-path)
repository_path="$2"
shift
;;
-m|--makefile-path)
makefile_path="$2"
shift
;;
-o|--output)
output_file="$2"
shift
;;
-h|--help)
show_usage="yes"
;;
*)
targets="$targets $1"
;;
esac
shift
done
if [ -z "$targets" -o -n "$show_usage" ]
then
echo "Usage: $0 TARGET ..."
echo "Run benchmark for the specified targets."
echo ""
echo "The following arguments can be given:"
echo " -b, --hash HASH, selects HASH or BRANCH in the frama-c repository"
echo " --branch BRANCH"
echo " -d, --clone-dir path to the directory where frama-c versions are"
echo " cloned"
echo " -c, --comment COMMENT a comment associated to results for better"
echo " readability of the results; if omitted,"
echo " defaults to the Frama-C branch name"
echo " -p, --repository-path PATH do not clone frama-c, use this repository instead"
echo " -m, --makefile-path FILE path to the makefile which can build the target"
echo " -o, --output FILE path to the output CSV file to be filled"
echo " -h, --help prints this help and quits"
exit 1
fi
if [ -z "$comment" ]
then
# Note: if the user gave us a commit hash instead of a branch name,
# we do not retrieve the branch name (which may not exist anyway)
comment="$git_hash"
fi
# --------------------------------------------------------------------------
# --- Frama-C repository ---
# --------------------------------------------------------------------------
if [ -z "$repository_path" ]
then
# git_hash and comment cannot be parsed yet:
# we need the git clone to dereference it, in case it's a tag/branch name
##### Preparation of git clones/checkouts #####
bare="$clone_dir/frama-c.git"
# Check if bench clone exists
if [ ! -d "$bare" ]
then
echo "Cloning Frama-C..."
git clone --bare --quiet git@git.frama-c.com:frama-c/frama-c "$bare"
sed --in-place '/bare = true/d' $bare/config
fi
# Fetch all refs
(
cd $bare
git fetch origin '+refs/heads/*:refs/heads/*' --prune
)
# Now we can parse the other arguments
# Resolve branch name if given
git_hash=`git --git-dir="$bare" rev-parse "$git_hash"`
# repository_path must be an absolute path
repository_path="$(readlink -f "$clone_dir/$git_hash")"
# Checkout and build the branch if necessary
if [ ! -e "$clone_dir/$git_hash" ]
then
echo "Building Frama-C for git commit: $git_hash"
# 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 "$repository_path" "$git_hash"
else
bash "$workdir_cmd" "$bare" "$repository_path" "$git_hash"
fi
# Build Frama-C
(
cd "$repository_path";
autoconf;
./configure --disable-wp;
make -j;
)
fi
fi
# In case building has failed for some reason, we check if the actual binary
# exists and report an error otherwise, indicating which directory should be
# deleted.
FRAMAC="$repository_path/bin/frama-c"
if [ ! -e "$FRAMAC" ]
then
echo "Error: could not find Frama-C binary: $FRAMAC"
echo "You may try erasing the directory to force a recompilation."
exit 2
fi
# --------------------------------------------------------------------------
# --- Benchmark execution and output ---
# --------------------------------------------------------------------------
header="target\ttimestamp\tFrama-C hash\tcomment\tcpu_time\tmaxmem\talarms\t\
warnings\tsem reach fun\tsyn reach fun\ttotal fun\tsem reach stmt\t\
syn reach stmt\tcommand args\tcase study git hash"
if [ ! -e "$output_file" ]
then
echo "output file does not exist, creating: $output_file"
printf "$header\n" > "$output_file"
fi
for target in $targets
do
pushd $makefile_path > /dev/null
make --no-print-directory $target BENCHMARK=y FRAMAC="$FRAMAC"
case_git_hash=`git rev-parse HEAD`
. $target/stats.txt
popd > /dev/null
printf "%s\t%s\t%s\t%s\t%s\t%s\t%s\t%s\t%s\t%s\t%s\t%s\t%s\t%s\t%s\n" \
"$target" "$timestamp" $git_hash "$comment" \
$user_time $memory $alarms $warnings \
$sem_reach_fun $syn_reach_fun $total_fun $sem_reach_stmt $syn_reach_stmt \
"$cmd_args" $case_git_hash \
>> "$output_file"
if command -v sqlite3 2>&1 >/dev/null
then
export comment
export git_hash
export case_git_hash
export target
"${BASH_SOURCE%/*}/bench-sqlite.sh" "$makefile_path/$target/stats.txt"
else
echo "command 'sqlite3' not found, cannot update the database"
fi
done
share/analysis-scripts/clone.sh
+ 2
− 9
View file @ 0b8c66d1
...@@ -64,15 +64,8 @@ target_path="$(readlink -f "$clone_dir/$git_hash")" ...@@ -64,15 +64,8 @@ target_path="$(readlink -f "$clone_dir/$git_hash")"
# Checkout # Checkout
if [ ! -e "$target_path" ] if [ ! -e "$target_path" ]
then then
# The workdir cmd can extract a working tree of the desired hash git clone "$bare" "$target_path" --quiet
# without cloning once more (cd "$target_path" && git checkout "$git_hash" --quiet)
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 fi
# Build Frama-C # Build Frama-C
......
share/analysis-scripts/results_display.py
+ 19
− 4
View file @ 0b8c66d1
...@@ -133,6 +133,14 @@ class PlainDisplay: ...@@ -133,6 +133,14 @@ class PlainDisplay:
elif s == "@-": elif s == "@-":
attributes = self.NEGATIVE attributes = self.NEGATIVE
else: else:
available = size - n
if len(s) > available:
if available > 16:
s = s[0:9] + '...' + s[13-available:]
elif available > 6:
s = s[0:available - 3] + '...'
else:
s = ''
n += len(s) n += len(s)
self.write(s, attributes if override is None else override) self.write(s, attributes if override is None else override)
if n < size: if n < size:
...@@ -184,7 +192,7 @@ class CursesDisplay(PlainDisplay): ...@@ -184,7 +192,7 @@ class CursesDisplay(PlainDisplay):
stdscr.nodelay(True) stdscr.nodelay(True)
stdscr.refresh() # Needs to be done once or nothing will be output stdscr.refresh() # Needs to be done once or nothing will be output
self.window = curses.newpad(400, 160) self.window = curses.newpad(2000, 160)
curses.init_color(curses.COLOR_YELLOW, 300, 300, 300) curses.init_color(curses.COLOR_YELLOW, 300, 300, 300)
curses.init_pair(1, curses.COLOR_RED, 0) curses.init_pair(1, curses.COLOR_RED, 0)
curses.init_pair(2, curses.COLOR_GREEN, 0) curses.init_pair(2, curses.COLOR_GREEN, 0)
...@@ -198,15 +206,22 @@ class CursesDisplay(PlainDisplay): ...@@ -198,15 +206,22 @@ class CursesDisplay(PlainDisplay):
self.scroll_y = 0 self.scroll_y = 0
def write(self, text, attributes=0): def write(self, text, attributes=0):
self.window.addstr(text, attributes) try:
self.window.addstr(text, attributes)
except curses.error: # don't exactly know why it happens, but it happens
pass
def print_table(self, results): def print_table(self, results):
self.window.clear() self.window.clear()
PlainDisplay.print_table(self, results) PlainDisplay.print_table(self, results)
height, width = self.stdscr.getmaxyx() height, width = self.stdscr.getmaxyx()
self.scroll_y = max(0, min(self.scroll_y, len(results)-height+2)) # relocate scroll if too far
try: try:
self.window.refresh(0, 0, 0, 0, 1, width - 1) if len(results) + 2 > height:
self.window.refresh(self.scroll_y + 2, 0, 2, 0, height - 1, width - 1) self.window.refresh(0, 0, 0, 0, 1, width - 1)
self.window.refresh(self.scroll_y + 2, 0, 2, 0, height - 1, width - 1)
else:
self.window.refresh(0, 0, 0, 0, height - 1, width - 1)
except Exception: except Exception:
# getmaxyx may be out of date, especially when resizing down the # getmaxyx may be out of date, especially when resizing down the
# window ; just ignore errors # window ; just ignore errors
......
share/analysis-scripts/summary.py
+ 36
− 10
View file @ 0b8c66d1
...@@ -30,6 +30,8 @@ import os ...@@ -30,6 +30,8 @@ import os
import signal import signal
import argparse import argparse
import uuid import uuid
import csv
from pathlib import Path
import frama_c_results import frama_c_results
import results_display import results_display
...@@ -76,15 +78,18 @@ def list_targets(dir): ...@@ -76,15 +78,18 @@ def list_targets(dir):
def clone_frama_c(clonedir, hash): def clone_frama_c(clonedir, hash):
print("Cloning Frama-C", hash, "...") print("Cloning Frama-C", hash, "...")
res = subprocess.run( try:
["./scripts/clone.sh", "--clone-dir", clonedir, hash], clone_cmd = Path(__file__).parent / "clone.sh"
stdout=subprocess.PIPE, res = subprocess.run(
encoding="ascii", [clone_cmd, "--clone-dir", clonedir, hash],
) stdout=subprocess.PIPE,
if res.returncode != 0: encoding="ascii",
raise OperationException("Cannot clone repository. Try to manually" check=True)
"remove the broken clone in " + clonedir) return res.stdout.strip() + "/build"
return res.stdout.strip() + "/build" except subprocess.CalledProcessError as e:
raise OperationException(
f"Cannot clone repository. Try to manually remove the broken clone"
f"in {clonedir}\n{e.output}") from e
def run_make(framac, benchmark_tag=None): def run_make(framac, benchmark_tag=None):
args = ["make", "--keep-going", "all"] args = ["make", "--keep-going", "all"]
...@@ -141,6 +146,22 @@ def poll_results(targets, benchmark_tag): ...@@ -141,6 +146,22 @@ def poll_results(targets, benchmark_tag):
return results return results
def dump_results_csv(results, path):
with open(path, 'w', newline='') as file:
fieldnames = [
"target_name", "timestamp",
"sem_reach_fun", "syn_reach_fun", "total_fun",
"sem_reach_stmt", "syn_reach_stmt",
"alarms", "warnings", "coverage",
"user_time", "memory"]
writer = csv.DictWriter(
file,
fieldnames=fieldnames,
extrasaction='ignore')
writer.writeheader()
writer.writerows(results)
def run_analyses(display, database, framac, benchmark_tag): def run_analyses(display, database, framac, benchmark_tag):
results = [] results = []
targets = list_targets(".") targets = list_targets(".")
...@@ -197,7 +218,9 @@ parser.add_argument("-c", "--comment", ...@@ -197,7 +218,9 @@ parser.add_argument("-c", "--comment",
parser.add_argument("-p", "--repository-path", parser.add_argument("-p", "--repository-path",
action="store", metavar="PATH", action="store", metavar="PATH",
help="don't clone Frama-C, use this git repository instead") help="don't clone Frama-C, use this git repository instead")
parser.add_argument("-o", "--output-csv",
action="store", metavar="PATH", type=Path,
help="output the results to the given CSV file")
errors = b"" errors = b""
...@@ -237,6 +260,9 @@ try: ...@@ -237,6 +260,9 @@ try:
print("Results:\n") print("Results:\n")
results_display.PlainDisplay().print_table(results) results_display.PlainDisplay().print_table(results)
if args.output_csv is not None:
dump_results_csv(results, args.output_csv)
except OperationException as e: except OperationException as e:
errors += bytearray(str(e), "ascii") errors += bytearray(str(e), "ascii")
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment