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