diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-10 22:33:26 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-10 22:33:26 +0200 |
| commit | 1348bc74b48ea8cb366a8bfab379699137276292 (patch) | |
| tree | fc92af59427abf6bd072cdeff22c1c48942c1115 /test/monniaux/minisat | |
| parent | 50d59f7ab7ae06de2ae6439752f0b56695d539df (diff) | |
| download | compcert-kvx-1348bc74b48ea8cb366a8bfab379699137276292.tar.gz compcert-kvx-1348bc74b48ea8cb366a8bfab379699137276292.zip | |
fixing Makefile
Diffstat (limited to 'test/monniaux/minisat')
| -rw-r--r-- | test/monniaux/minisat/Makefile.profiled | 14 | ||||
| -rw-r--r-- | test/monniaux/minisat/k1c.inline_50.log | 14 |
2 files changed, 23 insertions, 5 deletions
diff --git a/test/monniaux/minisat/Makefile.profiled b/test/monniaux/minisat/Makefile.profiled index 64e7cb80..b3b3c2fc 100644 --- a/test/monniaux/minisat/Makefile.profiled +++ b/test/monniaux/minisat/Makefile.profiled @@ -3,11 +3,15 @@ CFILES=main.c solver.c clock.c GCDAFILES=$(CFILES:.c=.gcda) CCOMP=../../../ccomp -GCC=aarch64-linux-gnu-gcc # k1-cos-gcc + +GCC=aarch64-linux-gnu-gcc +GCC=k1-cos-gcc +EXECUTE=qemu-aarch64 +EXECUTE=k1-cluster -- +EXECUTE_CYCLES=k1-cluster --cycle-based -- + LIBS=-lm PROFILING_DAT=compcert_profiling.dat -EXECUTE=qemu-aarch64 # k1-cluster -- -EXECUTE_CYCLES=k1-cluster --cycle-based -- EXAMPLE=sudoku.sat CCOMPFLAGS=-finline-auto-threshold 50 -static -finline-asm GCCFLAGS=-static @@ -37,11 +41,11 @@ minisat.gcc-O3.profiled.exe: $(CFILES) $(GCDAFILES) $(GCC) $(GCCFLAGS) -O3 -fprofile-use $(CFILES) -o $@ $(LIBS) minisat.ccomp.trace-linearize.exe: $(CFILES) - $(CCOMP) $(CCOMPFLAGS) -ftracelinearize $(CFILES) -o $@ $(LIBS) + $(CCOMP) $(CCOMPFLAGS) -fduplicate 0 -ftracelinearize $(CFILES) -o $@ $(LIBS) $(PROFILING_DAT): minisat.ccomp.profile-arcs.exe -rm -f $(PROFILING_DAT) - $(EXECUTE) $< $(EXAMPLE) || true + $(EXECUTE) $< $(EXAMPLE) minisat.ccomp.profiled.exe: $(CFILES) $(PROFILING_DAT) $(CCOMP) $(CCOMPFLAGS) -fprofile-use= $(PROFILING_DAT) -ftracelinearize $(CFILES) -o $@ $(LIBS) diff --git a/test/monniaux/minisat/k1c.inline_50.log b/test/monniaux/minisat/k1c.inline_50.log new file mode 100644 index 00000000..438a06b4 --- /dev/null +++ b/test/monniaux/minisat/k1c.inline_50.log @@ -0,0 +1,14 @@ +==> minisat.ccomp.log <== +time cycles: 3252345 + +==> minisat.ccomp.profiled.log <== +time cycles: 3150170 + +==> minisat.ccomp.trace-linearize.log <== +time cycles: 3192299 + +==> minisat.gcc-O3.log <== +time cycles: 2780324 + +==> minisat.gcc-O3.profiled.log <== +time cycles: 2487533 |