diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2022-01-05 15:32:46 +0100 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2022-01-05 15:32:46 +0100 |
commit | 1749be90299633474d2acad39ec8c70df6ccab32 (patch) | |
tree | 0e1e6a0ca8dccfabb9688eb3ea5b94193223b1b2 /ccomp_profiling/prof_ci_tests.sh | |
parent | 7b5ea95586f59c14f64b76e02fb3443c5c1ef6b8 (diff) | |
download | compcert-kvx-1749be90299633474d2acad39ec8c70df6ccab32.tar.gz compcert-kvx-1749be90299633474d2acad39ec8c70df6ccab32.zip |
update from BTL dev branch
Diffstat (limited to 'ccomp_profiling/prof_ci_tests.sh')
-rwxr-xr-x | ccomp_profiling/prof_ci_tests.sh | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/ccomp_profiling/prof_ci_tests.sh b/ccomp_profiling/prof_ci_tests.sh new file mode 100755 index 00000000..9af2428a --- /dev/null +++ b/ccomp_profiling/prof_ci_tests.sh @@ -0,0 +1,31 @@ +#!/bin/bash +# @author gourdinl +# Script to compute profiling results as csv from CI tests + +if [ $# -ne 2 ]; then + echo "Usage: ./prof_ci_tests.sh <root_dir> <fct1;fct2;...>" + echo $# + exit 1 +fi + +RDIR=$1 +RESULT=prof.csv +JQ=jq +CCOMP=$RDIR/ccomp +TMP=$RDIR/json_tmp +PROF_FCT=/home/yuki/Work/VERIMAG/Compcert_two/ccomp_profiling/prof_function.sh +LANDMARKSFLAGS="on,format=json,output=temporary:$TMP,time" +FCTS=$2 + +cd $RDIR +rm -rf $TMP +mkdir $TMP +make -C test clean +export OCAML_LANDMARKS=$LANDMARKSFLAGS +make -j4 -C test all_s +echo "test_name,ratio_cycles,ratio_time" > $RESULT +for file in $TMP/*; do + echo "Computing profiling results for $file" + RATIOS=$($PROF_FCT $JQ $file $FCTS | tail -n 1) + echo $RATIOS >> $RESULT +done |