examples/multiprecision/Makefile

   1 BENCH ?= no
   2 OVERLAY ?= no
   3 LOCAL ?= $(BENCH)
   4
   5 ifeq ($(LOCAL),yes)
   6   WHY3=../../bin/why3.opt
   7 else
   8   ifeq ($(BINDIR),)
   9     WHY3=why3
  10   else
  11     WHY3=$(BINDIR)/why3
  12   endif
  13 endif
  14
  15 ifndef CFLAGS
  16   ifdef GMP_DIR
  17     CFLAGS = $(shell sed -n -e 's/^CFLAGS = \(.*\)/\1/p' $(GMP_DIR)/Makefile)
  18   else
  19     CFLAGS = -march=native -O2 -fomit-frame-pointer
  20   endif
  21 endif
  22
  23 ifdef GMP_LIB
  24   GMPFLAGS = -I$(GMP_LIB)/include -L$(GMP_LIB)/lib
  25 endif
  26
  27 CFLAGS += -Wall -Wno-unused -g -std=c11 -Wno-pedantic
  28
  29 .PHONY: all clean extract plots benchs why3benchs gmpbenchs minigmpbenchs
  30
  31 all: extract
  32
  33 clean:
  34         rm -rf build bench
  35
  36 why3:
  37         make -C ../..
  38
  39 MLWFILES = \
  40   mpz_get_str mpz_set_str mpz_div2exp mpz_mul2exp mpz_div mpz_mul mpz_sub mpz_add mpz_getset mpz_abs mpz_cmp mpz_cmpabs mpz_neg mpz_realloc2 mpz \
  41   set_str get_str base_info powm sqrtrem sqrt toom logical div mul sub add compare util
  42
  43 build/extracted: $(addsuffix .mlw, $(MLWFILES))
  44         mkdir -p build
  45         rm -f $@
  46         $(WHY3) extract -D wmpn.drv -D c -L . --recursive --modular --interface -o build/ \
  47           --debug=c_no_error_msgs wmpn.mlw
  48         touch $@
  49
  50 build/sqrtinit.h: sqrtinit.ml
  51         mkdir -p build
  52         ocaml sqrtinit.ml > build/sqrtinit.h
  53
  54 build/binverttab.h: binverttab.ml
  55         mkdir -p build
  56         ocaml binverttab.ml > build/binverttab.h
  57
  58 EXTRACTED = build/extracted build/sqrtinit.h build/binverttab.h
  59
  60 extract: $(EXTRACTED)
  61
  62 CFILES = \
  63   zutil.c z.c zcmp.c zcmpabs.c zabs.c zneg.c zrealloc2.c \
  64   zadd.c zsub.c zmul.c zdiv.c zmul2exp.c zdiv2exp.c zget_str.c zset_str.c \
  65   set.c get_str.c set_str.c baseinfo.c powm.c sqrt.c sqrt1.c toom.c div.c \
  66   logical.c logicalold.c mul_basecase.c sub.c sub_1.c add.c add_1.c \
  67   compare.c util.c utilold.c
  68
  69 ifneq ($(OVERLAY),gmp)
  70 CFILES += mul.c addold.c subold.c
  71 endif
  72
  73 gmp_INCLUDES = mul.h add.h sub.h
  74 mini_INCLUDES = uint64gmp.h
  75 no_INCLUDES =
  76 INCLUDES = $($(OVERLAY)_INCLUDES)
  77
  78 build/libwmp.a: $(EXTRACTED)
  79         cd build; $(CC) $(CFLAGS) $(INCLUDES:%=-include ../overlays/%) -c $(CFILES)
  80         ar rcs $@ $(addprefix build/,$(CFILES:.c=.o))
  81
  82 build/tests: tests.c build/libwmp.a
  83         $(CC) $(CFLAGS) tests.c -Irandom -Lbuild -lm -lwmp -lgmp -o $@
  84
  85 build/minitests: tests.c build/libwmp.a
  86         $(CC) $(CFLAGS) -DCOMPARE_MINI tests.c -Irandom -Imini-gmp -Lbuild -lm -lwmp -o $@
  87
  88 UPPER = $(shell echo $* | tr [:lower:] [:upper:])
  89
  90 build/why3%bench: tests.c build/libwmp.a
  91         $(CC) $(CFLAGS) -DTEST_WHY3 -DTEST_$(UPPER) tests.c -Iinclude -Irandom -Lbuild -lm -lwmp -lgmp -o $@
  92
  93 build/gmp%bench: tests.c build/libwmp.a
  94         $(CC) $(CFLAGS) $(GMPFLAGS) -DTEST_GMP -DTEST_$(UPPER) tests.c -Iinclude -Irandom -lm -lgmp -o $@
  95
  96 build/minigmp%bench: tests.c build/libwmp.a
  97         $(CC) $(CFLAGS) -DTEST_MINIGMP -DTEST_$(UPPER) tests.c -Iinclude -Imini-gmp -Irandom -lm -o $@
  98
  99 BENCHS = toomb sqrtrem millerrabin toomu add mul div powm toomm zgetset
 100
 101
 102 WHY3BENCHFILES = $(addprefix bench/why3, $(BENCHS))
 103 GMPBENCHFILES = $(addprefix bench/gmp, $(BENCHS))
 104 MINIGMPBENCHFILES = $(addprefix bench/minigmp, $(BENCHS))
 105 BENCHFILES = $(WHY3BENCHFILES) $(GMPBENCHFILES) $(MINIGMPBENCHFILES)
 106
 107 $(BENCHFILES): bench/%: build/%bench
 108         mkdir -p bench
 109         $< > $@
 110
 111 why3benchs: $(WHY3BENCHFILES)
 112 gmpbenchs: $(GMPBENCHFILES)
 113 minigmpbenchs: $(MINIGMPBENCHFILES)
 114 benchs: why3benchs gmpbenchs minigmpbenchs
 115
 116 plots: $(BENCHFILES)
 117         make all -C plots