diff --git a/share/analysis-scripts/benchmark.sh b/share/analysis-scripts/benchmark.sh
deleted file mode 100755
index 3b94892cd32f197cd0c5597e277ebafcd0395b58..0000000000000000000000000000000000000000
--- a/share/analysis-scripts/benchmark.sh
+++ /dev/null
@@ -1,199 +0,0 @@
-#!/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
diff --git a/share/analysis-scripts/clone.sh b/share/analysis-scripts/clone.sh
index 19fe1a82afc70a5f1b8880713e67d0648e57af6d..0ed6b8553c2144fb94fb9cd8f3260f39b65212d9 100755
--- a/share/analysis-scripts/clone.sh
+++ b/share/analysis-scripts/clone.sh
@@ -64,15 +64,8 @@ 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
+ git clone "$bare" "$target_path" --quiet
+ (cd "$target_path" && git checkout "$git_hash" --quiet)
fi
# Build Frama-C
diff --git a/share/analysis-scripts/results_display.py b/share/analysis-scripts/results_display.py
index 732784ea6ddfd9ca73f3436aedb753418fd8de30..afec20997215b4f077ac97000b3848155009421c 100644
--- a/share/analysis-scripts/results_display.py
+++ b/share/analysis-scripts/results_display.py
@@ -133,6 +133,14 @@ class PlainDisplay:
elif s == "@-":
attributes = self.NEGATIVE
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)
self.write(s, attributes if override is None else override)
if n < size:
@@ -184,7 +192,7 @@ class CursesDisplay(PlainDisplay):
stdscr.nodelay(True)
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_pair(1, curses.COLOR_RED, 0)
curses.init_pair(2, curses.COLOR_GREEN, 0)
@@ -198,15 +206,22 @@ class CursesDisplay(PlainDisplay):
self.scroll_y = 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):
self.window.clear()
PlainDisplay.print_table(self, results)
height, width = self.stdscr.getmaxyx()
+ self.scroll_y = max(0, min(self.scroll_y, len(results)-height+2)) # relocate scroll if too far
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)
+ if len(results) + 2 > height:
+ 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:
# getmaxyx may be out of date, especially when resizing down the
# window ; just ignore errors
diff --git a/share/analysis-scripts/summary.py b/share/analysis-scripts/summary.py
index 8c9949fa10ab2cc036ab80477dc0e848506c0ce7..b2ee5d102f1b4319ecc279c67e73e45d60fe4c38 100755
--- a/share/analysis-scripts/summary.py
+++ b/share/analysis-scripts/summary.py
@@ -30,6 +30,8 @@ import os
import signal
import argparse
import uuid
+import csv
+from pathlib import Path
import frama_c_results
import results_display
@@ -76,15 +78,18 @@ def list_targets(dir):
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() + "/build"
+ try:
+ clone_cmd = Path(__file__).parent / "clone.sh"
+ res = subprocess.run(
+ [clone_cmd, "--clone-dir", clonedir, hash],
+ stdout=subprocess.PIPE,
+ encoding="ascii",
+ check=True)
+ 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):
args = ["make", "--keep-going", "all"]
@@ -141,6 +146,22 @@ def poll_results(targets, benchmark_tag):
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):
results = []
targets = list_targets(".")
@@ -197,7 +218,9 @@ parser.add_argument("-c", "--comment",
parser.add_argument("-p", "--repository-path",
action="store", metavar="PATH",
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""
@@ -237,6 +260,9 @@ try:
print("Results:\n")
results_display.PlainDisplay().print_table(results)
+ if args.output_csv is not None:
+ dump_results_csv(results, args.output_csv)
+
except OperationException as e:
errors += bytearray(str(e), "ascii")