Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work

4 files changed, 36 insertions, 19 deletions

diff --git a/test/monniaux/.gitignore b/test/monniaux/.gitignore
index 12b3c9db..6da0fa8d 100644
--- a/test/monniaux/.gitignore
+++ b/test/monniaux/.gitignore
@@ -1,5 +1,16 @@
 **.host
 **.k1c
+**measures.csv
+
+commands.txt
+oracle_times.txt
+verifier_times.txt
+compile_times.pdf
+measure_times.host.pdf
+measure_times.k1c.pdf
+
+/.mypy_cache/
+
 binary_search/Makefile
 bitsliced-aes/Makefile
 bitsliced-tea/Makefile
diff --git a/test/monniaux/Makefile b/test/monniaux/Makefile
index 0831a93c..b436c034 100644
--- a/test/monniaux/Makefile
+++ b/test/monniaux/Makefile
@@ -2,7 +2,7 @@
 
 CCOMP?=ccomp
 
-all: compile_times.pdf
+all: compile_times.pdf measure_times.k1c.pdf
 
 verifier_times.txt: Asmblockdeps.patch
 	patch ../../extraction/Asmblockdeps.ml < $<
@@ -16,9 +16,17 @@ oracle_times.txt: PostpassSchedulingOracle.patch
 	bash clean_benches.sh
 	bash build_benches.sh $@
 
+measures.csv:
+	(cd ../../ && make -j20 && make install)
+	bash build_benches.sh
+	bash run_benches.sh $@
+
 compile_times.pdf: gencompile.py verifier_times.txt oracle_times.txt
 	python3.6 $^ $@
 
+measure_times.k1c.pdf: gengraphs.py measures.csv
+	python3.6 $^ $(basename $(basename $@))
+
 .PHONY:
 clean:
-	rm -f verifier_times.txt oracle_times.txt compile_times.pdf
+	rm -f verifier_times.txt oracle_times.txt compile_times.pdf measure_times.k1c.pdf measures.csv
diff --git a/test/monniaux/gengraphs.py b/test/monniaux/gengraphs.py
index 3ffe6f3d..97cb08dc 100755
--- a/test/monniaux/gengraphs.py
+++ b/test/monniaux/gengraphs.py
@@ -10,9 +10,9 @@ from typing import *
 # Reading data
 ##
 
-if len(sys.argv) != 2:
-  raise Exception("Only 1 argument should be given to this script: the make.proto file")
-csv_file = sys.argv[1]
+if len(sys.argv) != 3:
+  raise Exception("Arguments for this script: the csv file, the base name of the output PDF file")
+_, csv_file, output_basename = sys.argv
 
 with open(csv_file, "r") as f:
   df = pd.read_csv(csv_file)
@@ -47,18 +47,18 @@ def subdivide_interv(inf: Any, sup: float, n: int) -> List[float]:
 # df associates the environment string (e.g. "gcc host") to the cycles
 # envs is the list of environments to compare
 # The returned value will be a dictionnary associating the compiler (e.g. "gcc") to his relative comparison on the best result
-def make_relative_heights(data: Any, envs: List[str]) -> Dict[str, List[float]]:
-  n_benches: int = len((data.values)) # type: ignore
-  cols: Dict[str, List[int]] = {extract_compiler(env):data[env] for env in envs}
+def make_relative_heights(data: Dict[str, List[float]], envs: List[str]) -> Dict[str, List[float]]:
+  n_benches: int = len(data["benches"])
+  cols: Dict[str, List[float]] = {extract_compiler(env):data[env] for env in envs}
 
   ret: Dict[str, List[float]] = {}
   for compiler in cols:
     ret[compiler] = []
 
   for i in range(n_benches):
-    max_time: int = max([cols[compiler][i] for compiler in cols])
+    maximum: float = max([cols[compiler][i] for compiler in cols])
     for compiler in cols:
-      ret[compiler].append(cols[compiler][i] / float(max_time))
+      ret[compiler].append(cols[compiler][i] / float(maximum))
 
   return ret
 
@@ -70,7 +70,8 @@ def generate_file(f: str, cols: List[str]) -> None:
 
   compilers = extract_compilers(cols)
   start_inds = subdivide_interv(ind, ind+2*width, len(compilers))
-  heights: Dict[str, List[float]] = make_relative_heights(df, cols)
+  inverse_cycles = {key:[1./x if isinstance(x, int) else x for x in list(df[key])] for key in df.columns}
+  heights: Dict[str, List[float]] = make_relative_heights(inverse_cycles, cols)
 
   fig, ax = plt.subplots()
   rects = []
@@ -78,7 +79,7 @@ def generate_file(f: str, cols: List[str]) -> None:
     rects.append(ax.bar(start_inds[i], heights[compiler], width, color=colors[i], label=compiler))
 
   # Add some text for labels, title and custom x-axis tick labels, etc.
-  ax.set_ylabel('Cycles (%)')
+  ax.set_ylabel('1/cycles (%)')
   ax.set_yticklabels(['{:,.0%}'.format(x) for x in ax.get_yticks()])
   ax.set_title('TITLE')
   ax.set_xticks(ind)
@@ -90,5 +91,5 @@ def generate_file(f: str, cols: List[str]) -> None:
 
   plt.savefig(f)
 
-generate_file("measures-host.pdf", host_measures_cols)
-generate_file("measures-k1c.pdf", k1c_measures_cols)
+generate_file(output_basename + ".host.pdf", host_measures_cols)
+generate_file(output_basename + ".k1c.pdf", k1c_measures_cols)
diff --git a/test/monniaux/run_benches.sh b/test/monniaux/run_benches.sh
index 479d09eb..5f9f22cb 100755
--- a/test/monniaux/run_benches.sh
+++ b/test/monniaux/run_benches.sh
@@ -19,8 +19,5 @@ for bench in $benches; do
   fi
 done
 
-nawk 'FNR==1 && NR!=1{next;}{print}' $benches_csv > measures.csv
-echo "measures.csv done"
-
-./gengraphs.py measures.csv
-echo "Graphs done"
+nawk 'FNR==1 && NR!=1{next;}{print}' $benches_csv > $1
+echo "$1 done"