update from BTL dev branch

1 files changed, 72 insertions, 0 deletions

diff --git a/ccomp_profiling/old_script_with_perf/perf_append.sh b/ccomp_profiling/old_script_with_perf/perf_append.sh
new file mode 100755
index 00000000..4b86a99e
--- /dev/null
+++ b/ccomp_profiling/old_script_with_perf/perf_append.sh
@@ -0,0 +1,72 @@
+#!/bin/bash
+
+CSV=perfs.csv
+TDIR=test/monniaux/yarpgen
+CCOMP_ROOT_BTL_NEW=/home/yuki/Work/VERIMAG/Compcert_two
+CCOMP_ROOT_BTL_OLD=/home/yuki/Work/VERIMAG/Compcert_three
+CCOMP_ROOT_RTL=/home/yuki/Work/VERIMAG/Compcert_one
+FILTER_BTL_NEW=simu_check_single_1421
+FILTER_BTL_OLD_LIVE=liveness_checker_720
+FILTER_BTL_OLD_SB=simu_check_1445
+FILTER_RTL_LIVE=list_path_checker_706
+FILTER_RTL_SB=function_equiv_checker_235
+
+clean_n_build () {
+  cd $CCOMP_ROOT_BTL_NEW/$TDIR
+  rm perf.*.data
+  make clean && make tests_c tests_s
+  cd $CCOMP_ROOT_BTL_OLD/$TDIR
+  rm perf.*.data
+  make clean && make tests_c tests_s
+  cd $CCOMP_ROOT_RTL/$TDIR
+  rm perf.*.data
+  make clean && make tests_c tests_s
+  echo "file,btl_new ($FILTER_BTL_NEW),btl_old ($FILTER_BTL_OLD_LIVE + $FILTER_BTL_OLD_SB),rtl ($FILTER_RTL_LIVE + $FILTER_RTL_SB)" > $CSV
+}
+
+check_result () {
+  if [[ $1 ]]; then
+    echo "$1"
+  else
+    echo "0"
+  fi
+}
+
+awk_filter () {
+  res=$(echo "$1" | awk -F "," '/%*ccomp/ { print substr($1,2,length($1)-4) }')
+  check_result $res
+}
+
+perf_btl_new () {
+  cd $CCOMP_ROOT_BTL_NEW/$TDIR
+  perc_btl_new=$(awk_filter "$(perf report -t , --stdio --symbol-filter=$FILTER_BTL_NEW -i $1)")
+}
+
+perf_btl_old () {
+  cd $CCOMP_ROOT_BTL_OLD/$TDIR
+  btl_live=$(awk_filter "$(perf report -t , --stdio --symbol-filter=$FILTER_BTL_OLD_LIVE -i $1)")
+  btl_sb=$(awk_filter "$(perf report -t , --stdio --symbol-filter=$FILTER_BTL_OLD_SB -i $1)")
+  echo "btl_old: $btl_live + $btl_sb"
+  perc_btl_old=$(bc <<< "$btl_live + $btl_sb")
+}
+
+perf_rtl () {
+  cd $CCOMP_ROOT_RTL/$TDIR
+  rtl_live=$(awk_filter "$(perf report -t , --stdio --symbol-filter=$FILTER_RTL_LIVE -i $1)")
+  rtl_sb=$(awk_filter "$(perf report -t , --stdio --symbol-filter=$FILTER_RTL_SB -i $1)")
+  echo "rtl_old: $rtl_live + $rtl_sb"
+  perc_rtl=$(bc <<< "$rtl_live + $rtl_sb")
+}
+
+rdir=$(pwd)
+clean_n_build
+for file in $CCOMP_ROOT_RTL/$TDIR/perf.*; do
+  bfile=$(basename $file)
+  perf_btl_new "$bfile"
+  perf_btl_old "$bfile"
+  perf_rtl "$bfile"
+  cd $rdir
+  echo "$file, $perc_btl_new, $perc_btl_old, $perc_rtl"
+  echo "$file, $perc_btl_new, $perc_btl_old, $perc_rtl" >> $CSV
+done
+