From 1749be90299633474d2acad39ec8c70df6ccab32 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Wed, 5 Jan 2022 15:32:46 +0100
Subject: update from BTL dev branch

---
 ccomp_profiling/prof_ci_tests.sh | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100755 ccomp_profiling/prof_ci_tests.sh

(limited to 'ccomp_profiling/prof_ci_tests.sh')

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
-- 
cgit