diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-09 14:19:33 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-09 14:19:33 +0200 |
| commit | 07247055911bc1a436e469a3114649d3bb317d73 (patch) | |
| tree | 35d85c64134cb444ded5eb5e1dfd88b99c01dc3b /test/monniaux/minisat | |
| parent | 112beeee204d4a06b8c39e9554255261365f3fed (diff) | |
| download | compcert-kvx-07247055911bc1a436e469a3114649d3bb317d73.tar.gz compcert-kvx-07247055911bc1a436e469a3114649d3bb317d73.zip | |
for profiling
Diffstat (limited to 'test/monniaux/minisat')
| -rw-r--r-- | test/monniaux/minisat/Makefile.profiled | 33 | ||||
| l--------- | test/monniaux/minisat/clock.c | 1 |
2 files changed, 28 insertions, 6 deletions
diff --git a/test/monniaux/minisat/Makefile.profiled b/test/monniaux/minisat/Makefile.profiled index febac0d5..08283c8a 100644 --- a/test/monniaux/minisat/Makefile.profiled +++ b/test/monniaux/minisat/Makefile.profiled @@ -1,21 +1,42 @@ -CFILES=main.c solver.c ../clock.c +CFILES=main.c solver.c clock.c +GCDAFILES=$(CFILES:.c=.gcda) CCOMP=../../../ccomp -CCOMPFLAGS= +GCC=k1-cos-gcc +LIBS=-lm PROFILING_DAT=compcert_profiling.dat EXECUTE=k1-cluster -- EXAMPLE=sudoku.sat -all: minisat.ccomp minisat.branch_linearize minisat.profiled +ALL=minisat.ccomp minisat.branch_linearize minisat.profiled minisat.gcc-O3 minisat.gcc-O3.profiled + +all: $(ALL) minisat.ccomp: $(CFILES) - $(CCOMP) $(CCOMPFLAGS) $(CFILES) -o $@ + $(CCOMP) $(CCOMPFLAGS) $(CFILES) -o $@ $(LIBS) + +minisat.gcc-O3: $(CFILES) + $(GCC) $(GCCFLAGS) -O3 $(CFILES) -o $@ $(LIBS) + +minisat.gcc-O3.profile-arcs: $(CFILES) + $(GCC) $(GCCFLAGS) -fprofile-arcs -O3 $(CFILES) -o $@ $(LIBS) + +$(GCDAFILES): minisat.gcc-O3.profile-arcs + $(EXECUTE) $< $(EXAMPLE) + +minisat.gcc-O3.profiled: $(CFILES) $(GCDAFILES) + $(GCC) $(GCCFLAGS) -O3 -fprofile-use $(CFILES) -o $@ $(LIBS) minisat.branch_linearize: $(CFILES) - $(CCOMP) $(CCOMPFLAGS) -fbranchlinearize $(CFILES) -o $@ + $(CCOMP) $(CCOMPFLAGS) -fbranchlinearize $(CFILES) -o $@ $(LIBS) $(PROFILING_DAT): minisat.profile_arcs -rm -f $(PROFILING_DAT) $(EXECUTE) $< $(EXAMPLE) minisat.profiled: $(CFILES) $(PROFILING_DAT) - $(CCOMP) $(CCOMPFLAGS) -fprofile-use= $(PROFILING_DAT) -fbranchlinearize $(CFILES) -o $@ + $(CCOMP) $(CCOMPFLAGS) -fprofile-use= $(PROFILING_DAT) -fbranchlinearize $(CFILES) -o $@ $(LIBS) + +clean: + -rm -f $(ALL) $(PROFILING_DAT) $(GCDAFILES) + +.PHONY: clean diff --git a/test/monniaux/minisat/clock.c b/test/monniaux/minisat/clock.c new file mode 120000 index 00000000..d6bade99 --- /dev/null +++ b/test/monniaux/minisat/clock.c @@ -0,0 +1 @@ +../clock.c
\ No newline at end of file |