From d9528b9d5684efe0d47c68dff8a364655d68e59f Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 31 May 2022 14:50:36 +0200
Subject: [PATCH] [Analysis Scripts] remove obsolete benchmark.sh
---
share/analysis-scripts/benchmark.sh | 199 ----------------------------
1 file changed, 199 deletions(-)
delete mode 100755 share/analysis-scripts/benchmark.sh
diff --git a/share/analysis-scripts/benchmark.sh b/share/analysis-scripts/benchmark.sh
deleted file mode 100755
index 3b94892cd32..00000000000
--- 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
--
GitLab