aboutsummaryrefslogtreecommitdiffstats
path: root/test/monniaux/Makefile
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-03 08:17:40 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-03 08:17:40 +0100
commit1ab7b51c30e1b10ac45b0bd64cefdc01da0f7f68 (patch)
tree210ffc156c83f04fb0c61a40b4f9037d7ba8a7e1 /test/monniaux/Makefile
parent222c9047d61961db9c6b19fed5ca49829223fd33 (diff)
parent12be46d59a2483a10d77fa8ee67f7e0ca1bd702f (diff)
downloadcompcert-kvx-1ab7b51c30e1b10ac45b0bd64cefdc01da0f7f68.tar.gz
compcert-kvx-1ab7b51c30e1b10ac45b0bd64cefdc01da0f7f68.zip
Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
Diffstat (limited to 'test/monniaux/Makefile')
-rw-r--r--test/monniaux/Makefile39
1 files changed, 39 insertions, 0 deletions
diff --git a/test/monniaux/Makefile b/test/monniaux/Makefile
new file mode 100644
index 00000000..d7437eea
--- /dev/null
+++ b/test/monniaux/Makefile
@@ -0,0 +1,39 @@
+# NOTE: do NOT run this makefile with the -j option
+
+CCOMP?=ccomp
+
+#all: verifier_times.txt oracle_times.txt measures.csv
+all: measures.csv
+
+verifier_times.txt: Asmblockdeps.patch
+ (cd ../../ && make -j20 && make install)
+ patch $(realpath ../../extraction/Asmblockdeps.ml) < $<
+ (cd ../../ && make -j20 && make install); patch -R $(realpath ../../extraction/Asmblockdeps.ml) < $<
+ bash clean_benches.sh
+ bash build_benches.sh $@
+
+oracle_times.txt: PostpassSchedulingOracle.patch
+ (cd ../../ && make -j20 && make install)
+ patch $(realpath ../../mppa_k1c/PostpassSchedulingOracle.ml) < $<
+ (cd ../../ && make -j20 && make install); patch -R $(realpath ../../mppa_k1c/PostpassSchedulingOracle.ml) < $<
+ bash clean_benches.sh
+ bash build_benches.sh $@
+
+measures.csv:
+ @echo "Building compcert.."
+ @(cd ../../ && make -s -j20 && make -s install)
+ @echo "Building benches..."
+ @bash build_benches.sh
+ @echo "Benches built. Running benches..."
+ @bash run_benches.sh $@
+
+#compile_times.pdf: gencompile.py verifier_times.txt oracle_times.txt
+# python3.5 $^ $@
+#
+#measure_times.k1c.pdf: gengraphs.py measures.csv
+# python3.5 $^ $(basename $(basename $@))
+
+.PHONY:
+clean:
+ @bash clean_benches.sh
+ rm -f verifier_times.txt oracle_times.txt compile_times.pdf measure_times.k1c.pdf measures.csv