Commit 44629438 authored by Raphaël Rieu-Helft's avatar Raphaël Rieu-Helft

Merge branch 'extract-headers' into 'master'

Extract headers

See merge request !10
parents 80f84138 eda39680
......@@ -10,6 +10,9 @@
/bench/encoding/ export-ignore
/examples/in_progress/ export-ignore
/examples/multiprecision/random/ export-ignore
/examples/multiprecision/bench-include/ export-ignore
/examples/multiprecision/mini-gmp/ export-ignore
/misc/ export-ignore
/opam/ export-ignore
/tests/ export-ignore
......
......@@ -182,7 +182,7 @@ extract_and_run () {
}
extract_and_test_wmp () {
dir="examples/in_progress/multiprecision"
dir=$1
shift
printf " $dir... "
printf "clean... "
......@@ -346,7 +346,8 @@ extract_and_run examples/sudoku sudoku.ml 2,0,9,0,0,0,0,1,0,0,0,0,0,6,0,0,0,0,0,
echo ""
echo "=== Checking extraction to C ==="
extract_and_test_wmp
extract_and_test_wmp examples/in_progress/multiprecision
extract_and_test_wmp examples/multiprecision
echo ""
echo "=== Checking --list-* ==="
......
......@@ -3,6 +3,7 @@ printer "c"
prelude "#include <stdlib.h>"
prelude "#include <stdint.h>"
prelude "#include <stdio.h>"
prelude "#include <assert.h>"
module ref.Ref
......@@ -141,6 +142,44 @@ struct __lsld32_result lsld32(uint32_t x, uint32_t cnt)
result.__field_1 = (uint32_t)(r >> 32);
return result;
}
"
interface
"
struct __add32_with_carry_result
{ uint32_t __field_0;
uint32_t __field_1;
};
struct __add32_with_carry_result add32_with_carry(uint32_t x, uint32_t y, uint32_t c);
struct __sub32_with_borrow_result
{ uint32_t __field_0;
uint32_t __field_1;
};
struct __sub32_with_borrow_result sub32_with_borrow(uint32_t x, uint32_t y, uint32_t b);
struct __mul32_double_result
{ uint32_t __field_0;
uint32_t __field_1;
};
struct __mul32_double_result mul32_double(uint32_t x, uint32_t y);
struct __add32_3_result
{ uint32_t __field_0;
uint32_t __field_1;
};
struct __add32_3_result add32_3(uint32_t x, uint32_t y, uint32_t z);
struct __lsld32_result
{ uint32_t __field_0;
uint32_t __field_1;
};
struct __lsld32_result lsld32(uint32_t x, uint32_t cnt);
"
syntax converter of_int "%1U"
......@@ -213,7 +252,6 @@ module mach.int.UInt64GMP
prelude
"
#include \"config.h\"
#include \"gmp.h\"
#include \"gmp-impl.h\"
#include \"longlong.h\"
......@@ -225,7 +263,7 @@ struct __add64_with_carry_result
uint64_t __field_1;
};
struct __add64_with_carry_result
struct __add64_with_carry_result
add64_with_carry(uint64_t x, uint64_t y, uint64_t c)
{
struct __add64_with_carry_result result;
......@@ -241,7 +279,7 @@ struct __add64_double_result
uint64_t __field_1;
};
struct __add64_double_result
struct __add64_double_result
add64_double(uint64_t a1, uint64_t a0, uint64_t b1, uint64_t b0)
{
struct __add64_double_result result;
......@@ -254,7 +292,7 @@ struct __sub64_with_borrow_result
uint64_t __field_1;
};
struct __sub64_with_borrow_result
struct __sub64_with_borrow_result
sub64_with_borrow(uint64_t x, uint64_t y, uint64_t b)
{
struct __sub64_with_borrow_result result;
......@@ -271,7 +309,7 @@ struct __sub64_double_result
uint64_t __field_1;
};
struct __sub64_double_result
struct __sub64_double_result
sub64_double(uint64_t a1, uint64_t a0, uint64_t b1, uint64_t b0)
{
struct __sub64_double_result result;
......@@ -331,6 +369,69 @@ struct __lsld64_result lsld64(uint64_t x, uint64_t cnt)
}
"
interface
"
#include \"gmp.h\"
#include \"gmp-impl.h\"
#include \"longlong.h\"
#undef invert_limb
struct __add64_with_carry_result
{ uint64_t __field_0;
uint64_t __field_1;
};
struct __add64_with_carry_result
add64_with_carry(uint64_t x, uint64_t y, uint64_t c);
struct __add64_double_result
{ uint64_t __field_0;
uint64_t __field_1;
};
struct __add64_double_result
add64_double(uint64_t a1, uint64_t a0, uint64_t b1, uint64_t b0);
struct __sub64_with_borrow_result
{ uint64_t __field_0;
uint64_t __field_1;
};
struct __sub64_with_borrow_result
sub64_with_borrow(uint64_t x, uint64_t y, uint64_t b);
struct __sub64_double_result
{ uint64_t __field_0;
uint64_t __field_1;
};
struct __sub64_double_result
sub64_double(uint64_t a1, uint64_t a0, uint64_t b1, uint64_t b0);
struct __mul64_double_result
{ uint64_t __field_0;
uint64_t __field_1;
};
struct __mul64_double_result mul64_double(uint64_t x, uint64_t y);
uint64_t div64_2by1(uint64_t ul, uint64_t uh, uint64_t d);
struct __add64_3_result
{ uint64_t __field_0;
uint64_t __field_1;
};
struct __add64_3_result add64_3(uint64_t x, uint64_t y, uint64_t z);
struct __lsld64_result
{ uint64_t __field_0;
uint64_t __field_1;
};
struct __lsld64_result lsld64(uint64_t x, uint64_t cnt);
"
syntax converter of_int "%1ULL"
syntax val (+) "%1 + %2"
......
bench/
build/
\ No newline at end of file
BENCH ?= no
ifeq ($(BENCH),yes)
WHY3=../../bin/why3.opt
else
ifeq ($(BINDIR),)
WHY3=why3
else
WHY3=$(BINDIR)/why3
endif
endif
all: why3 extract
clean:
rm -rf build
why3:
make -C ../..
dir:
mkdir -p build
cfiles: why3 dir
$(WHY3) extract -D c -L . --recursive --modular --interface -o build/ wmpn.mlw
extract: why3 dir cfiles
CFILES = build/uint64gmp.c build/div.c build/logical.c build/mul.c build/sub.c build/add.c build/compare.c build/util.c build/int32.c
tests: extract check-gmp
gcc -O2 -Wall -Wno-unused-function -g -std=gnu99 tests.c $(CFILES) -I$(GMP_DIR) -Irandom -L$(GMP_LIB) -fomit-frame-pointer -mtune=haswell -march=haswell -fno-tree-vectorize -lgmp -o build/tests
gcc -O2 -Wall -Wno-unused-function -g -std=gnu99 -DCOMPARE_MINI tests.c $(CFILES) -I$(GMP_DIR) -Irandom -Imini-gmp -fomit-frame-pointer -mtune=haswell -march=haswell -fno-tree-vectorize -o build/minitests
./build/tests
./build/minitests
bench-tests: extract
gcc -O2 -Wall -g -std=gnu99 tests.c $(CFILES) -Ibench-include -Irandom -fomit-frame-pointer -fno-tree-vectorize -lgmp -o build/bench-tests
build/why3%bench: extract check-gmp
gcc -O3 -Wall -g -std=gnu99 -DTEST_WHY3 -DTEST_`echo $* | tr [:lower:] [:upper:]` tests.c $(CFILES) -I$(GMP_DIR) -L$(GMP_LIB) -fomit-frame-pointer -mtune=haswell -march=haswell -fno-tree-vectorize -lgmp -o $@
build/gmp%bench: extract check-gmp
gcc -O3 -Wall -g -std=gnu99 -DTEST_GMP -DTEST_`echo $* | tr [:lower:] [:upper:]` tests.c $(CFILES) -I$(GMP_DIR) -L$(GMP_LIB) -fomit-frame-pointer -mtune=haswell -march=haswell -fno-tree-vectorize -lgmp -o $@
build/minigmp%bench: extract
gcc -O3 -Wall -g -std=gnu99 -DTEST_MINIGMP -DTEST_`echo $* | tr [:lower:] [:upper:]` tests.c $(CFILES) -I$(GMP_DIR) -fomit-frame-pointer -mtune=haswell -march=haswell -fno-tree-vectorize -o $@
alltests: tests build/why3addbench build/why3mulbench build/why3divbench build/gmpaddbench build/gmpmulbench build/gmpdivbench build/minigmpaddbench build/minigmpmulbench build/minigmpdivbench
data: alltests
mkdir -p bench
./build/why3addbench > bench/why3add
./build/why3mulbench > bench/why3mul
./build/why3divbench > bench/why3div
./build/gmpaddbench > bench/gmpadd
./build/gmpmulbench > bench/gmpmul
./build/gmpdivbench > bench/gmpdiv
./build/minigmpaddbench > bench/minigmpadd
./build/minigmpmulbench > bench/minigmpmul
./build/minigmpdivbench > bench/minigmpdiv
plots: data
make all -C plots
check-gmp:
ifndef GMP_DIR
$(error GMP_DIR is undefined)
endif
ifndef GMP_LIB
$(error GMP_LIB is undefined)
endif
This diff is collapsed.
/* This file is automatically generated by gen-fac.c */
#if GMP_NUMB_BITS != 64
Error , error this data is for 64 GMP_NUMB_BITS only
#endif
/* This table is 0!,1!,2!,3!,...,n! where n! has <= GMP_NUMB_BITS bits */
#define ONE_LIMB_FACTORIAL_TABLE CNST_LIMB(0x1),CNST_LIMB(0x1),CNST_LIMB(0x2),CNST_LIMB(0x6),CNST_LIMB(0x18),CNST_LIMB(0x78),CNST_LIMB(0x2d0),CNST_LIMB(0x13b0),CNST_LIMB(0x9d80),CNST_LIMB(0x58980),CNST_LIMB(0x375f00),CNST_LIMB(0x2611500),CNST_LIMB(0x1c8cfc00),CNST_LIMB(0x17328cc00),CNST_LIMB(0x144c3b2800),CNST_LIMB(0x13077775800),CNST_LIMB(0x130777758000),CNST_LIMB(0x1437eeecd8000),CNST_LIMB(0x16beecca730000),CNST_LIMB(0x1b02b9306890000),CNST_LIMB(0x21c3677c82b40000)
/* This table is 0!,1!,2!/2,3!/2,...,n!/2^sn where n!/2^sn is an */
/* odd integer for each n, and n!/2^sn has <= GMP_NUMB_BITS bits */
#define ONE_LIMB_ODD_FACTORIAL_TABLE CNST_LIMB(0x1),CNST_LIMB(0x1),CNST_LIMB(0x1),CNST_LIMB(0x3),CNST_LIMB(0x3),CNST_LIMB(0xf),CNST_LIMB(0x2d),CNST_LIMB(0x13b),CNST_LIMB(0x13b),CNST_LIMB(0xb13),CNST_LIMB(0x375f),CNST_LIMB(0x26115),CNST_LIMB(0x7233f),CNST_LIMB(0x5cca33),CNST_LIMB(0x2898765),CNST_LIMB(0x260eeeeb),CNST_LIMB(0x260eeeeb),CNST_LIMB(0x286fddd9b),CNST_LIMB(0x16beecca73),CNST_LIMB(0x1b02b930689),CNST_LIMB(0x870d9df20ad),CNST_LIMB(0xb141df4dae31),CNST_LIMB(0x79dd498567c1b),CNST_LIMB(0xaf2e19afc5266d),CNST_LIMB(0x20d8a4d0f4f7347),CNST_LIMB(0x335281867ec241ef)
#define ODD_FACTORIAL_TABLE_MAX CNST_LIMB(0x335281867ec241ef)
#define ODD_FACTORIAL_TABLE_LIMIT (25)
/* Previous table, continued, values modulo 2^GMP_NUMB_BITS */
#define ONE_LIMB_ODD_FACTORIAL_EXTTABLE CNST_LIMB(0x9b3093d46fdd5923),CNST_LIMB(0x5e1f9767cc5866b1),CNST_LIMB(0x92dd23d6966aced7),CNST_LIMB(0xa30d0f4f0a196e5b),CNST_LIMB(0x8dc3e5a1977d7755),CNST_LIMB(0x2ab8ce915831734b),CNST_LIMB(0x2ab8ce915831734b),CNST_LIMB(0x81d2a0bc5e5fdcab),CNST_LIMB(0x9efcac82445da75b),CNST_LIMB(0xbc8b95cf58cde171),CNST_LIMB(0xa0e8444a1f3cecf9),CNST_LIMB(0x4191deb683ce3ffd),CNST_LIMB(0xddd3878bc84ebfc7),CNST_LIMB(0xcb39a64b83ff3751),CNST_LIMB(0xf8203f7993fc1495),CNST_LIMB(0xbd2a2a78b35f4bdd),CNST_LIMB(0x84757be6b6d13921),CNST_LIMB(0x3fbbcfc0b524988b),CNST_LIMB(0xbd11ed47c8928df9),CNST_LIMB(0x3c26b59e41c2f4c5),CNST_LIMB(0x677a5137e883fdb3),CNST_LIMB(0xff74e943b03b93dd),CNST_LIMB(0xfe5ebbcb10b2bb97),CNST_LIMB(0xb021f1de3235e7e7),CNST_LIMB(0x33509eb2e743a58f),CNST_LIMB(0x390f9da41279fb7d),CNST_LIMB(0xe5cb0154f031c559),CNST_LIMB(0x93074695ba4ddb6d),CNST_LIMB(0x81c471caa636247f),CNST_LIMB(0xe1347289b5a1d749),CNST_LIMB(0x286f21c3f76ce2ff),CNST_LIMB(0xbe84a2173e8ac7),CNST_LIMB(0x1595065ca215b88b),CNST_LIMB(0xf95877595b018809),CNST_LIMB(0x9c2efe3c5516f887),CNST_LIMB(0x373294604679382b),CNST_LIMB(0xaf1ff7a888adcd35),CNST_LIMB(0x18ddf279a2c5800b),CNST_LIMB(0x18ddf279a2c5800b),CNST_LIMB(0x505a90e2542582cb),CNST_LIMB(0x5bacad2cd8d5dc2b),CNST_LIMB(0xfe3152bcbff89f41)
#define ODD_FACTORIAL_EXTTABLE_LIMIT (67)
/* This table is 1!!,3!!,...,(2n+1)!! where (2n+1)!! has <= GMP_NUMB_BITS bits */
#define ONE_LIMB_ODD_DOUBLEFACTORIAL_TABLE CNST_LIMB(0x1),CNST_LIMB(0x3),CNST_LIMB(0xf),CNST_LIMB(0x69),CNST_LIMB(0x3b1),CNST_LIMB(0x289b),CNST_LIMB(0x20fdf),CNST_LIMB(0x1eee11),CNST_LIMB(0x20dcf21),CNST_LIMB(0x27065f73),CNST_LIMB(0x33385d46f),CNST_LIMB(0x49a10615f9),CNST_LIMB(0x730b9982551),CNST_LIMB(0xc223930bef8b),CNST_LIMB(0x15fe07a85a22bf),CNST_LIMB(0x2a9c2ed62ea3521),CNST_LIMB(0x57e22099c030d941)
#define ODD_DOUBLEFACTORIAL_TABLE_MAX CNST_LIMB(0x57e22099c030d941)
#define ODD_DOUBLEFACTORIAL_TABLE_LIMIT (33)
/* This table x_1, x_2,... contains values s.t. x_n^n has <= GMP_NUMB_BITS bits */
#define NTH_ROOT_NUMB_MASK_TABLE (GMP_NUMB_MASK),CNST_LIMB(0xffffffff),CNST_LIMB(0x285145),CNST_LIMB(0xffff),CNST_LIMB(0x1bdb),CNST_LIMB(0x659),CNST_LIMB(0x235),CNST_LIMB(0xff)
/* This table contains inverses of odd factorials, modulo 2^GMP_NUMB_BITS */
/* It begins with (2!/2)^-1=1 */
#define ONE_LIMB_ODD_FACTORIAL_INVERSES_TABLE CNST_LIMB(0x1),CNST_LIMB(0xaaaaaaaaaaaaaaab),CNST_LIMB(0xaaaaaaaaaaaaaaab),CNST_LIMB(0xeeeeeeeeeeeeeeef),CNST_LIMB(0x4fa4fa4fa4fa4fa5),CNST_LIMB(0x2ff2ff2ff2ff2ff3),CNST_LIMB(0x2ff2ff2ff2ff2ff3),CNST_LIMB(0x938cc70553e3771b),CNST_LIMB(0xb71c27cddd93e49f),CNST_LIMB(0xb38e3229fcdee63d),CNST_LIMB(0xe684bb63544a4cbf),CNST_LIMB(0xc2f684917ca340fb),CNST_LIMB(0xf747c9cba417526d),CNST_LIMB(0xbb26eb51d7bd49c3),CNST_LIMB(0xbb26eb51d7bd49c3),CNST_LIMB(0xb0a7efb985294093),CNST_LIMB(0xbe4b8c69f259eabb),CNST_LIMB(0x6854d17ed6dc4fb9),CNST_LIMB(0xe1aa904c915f4325),CNST_LIMB(0x3b8206df131cead1),CNST_LIMB(0x79c6009fea76fe13),CNST_LIMB(0xd8c5d381633cd365),CNST_LIMB(0x4841f12b21144677),CNST_LIMB(0x4a91ff68200b0d0f),CNST_LIMB(0x8f9513a58c4f9e8b),CNST_LIMB(0x2b3e690621a42251),CNST_LIMB(0x4f520f00e03c04e7),CNST_LIMB(0x2edf84ee600211d3),CNST_LIMB(0xadcaa2764aaacdfd),CNST_LIMB(0x161f4f9033f4fe63),CNST_LIMB(0x161f4f9033f4fe63),CNST_LIMB(0xbada2932ea4d3e03),CNST_LIMB(0xcec189f3efaa30d3),CNST_LIMB(0xf7475bb68330bf91),CNST_LIMB(0x37eb7bf7d5b01549),CNST_LIMB(0x46b35660a4e91555),CNST_LIMB(0xa567c12d81f151f7),CNST_LIMB(0x4c724007bb2071b1),CNST_LIMB(0xf4a0cce58a016bd),CNST_LIMB(0xfa21068e66106475),CNST_LIMB(0x244ab72b5a318ae1),CNST_LIMB(0x366ce67e080d0f23),CNST_LIMB(0xd666fdae5dd2a449),CNST_LIMB(0xd740ddd0acc06a0d),CNST_LIMB(0xb050bbbb28e6f97b),CNST_LIMB(0x70b003fe890a5c75),CNST_LIMB(0xd03aabff83037427),CNST_LIMB(0x13ec4ca72c783bd7),CNST_LIMB(0x90282c06afdbd96f),CNST_LIMB(0x4414ddb9db4a95d5),CNST_LIMB(0xa2c68735ae6832e9),CNST_LIMB(0xbf72d71455676665),CNST_LIMB(0xa8469fab6b759b7f),CNST_LIMB(0xc1e55b56e606caf9),CNST_LIMB(0x40455630fc4a1cff),CNST_LIMB(0x120a7b0046d16f7),CNST_LIMB(0xa7c3553b08faef23),CNST_LIMB(0x9f0bfd1b08d48639),CNST_LIMB(0xa433ffce9a304d37),CNST_LIMB(0xa22ad1d53915c683),CNST_LIMB(0xcb6cbc723ba5dd1d),CNST_LIMB(0x547fb1b8ab9d0ba3),CNST_LIMB(0x547fb1b8ab9d0ba3),CNST_LIMB(0x8f15a826498852e3)
/* This table contains 2n-popc(2n) for small n */
/* It begins with 2-1=1 (n=1) */
#define TABLE_2N_MINUS_POPC_2N 1,3,4,7,8,10,11,15,16,18,19,22,23,25,26,31,32,34,35,38,39,41,42,46,47,49,50,53,54,56,57,63,64,66,67,70,71,73,74,78
#define TABLE_LIMIT_2N_MINUS_POPC_2N 81
#define ODD_CENTRAL_BINOMIAL_OFFSET (13)
/* This table contains binomial(2k,k)/2^t */
/* It begins with ODD_CENTRAL_BINOMIAL_TABLE_MIN */
#define ONE_LIMB_ODD_CENTRAL_BINOMIAL_TABLE CNST_LIMB(0x13d66b),CNST_LIMB(0x4c842f),CNST_LIMB(0x93ee7d),CNST_LIMB(0x11e9e123),CNST_LIMB(0x22c60053),CNST_LIMB(0x873ae4d1),CNST_LIMB(0x10757bd97),CNST_LIMB(0x80612c6cd),CNST_LIMB(0xfaa556bc1),CNST_LIMB(0x3d3cc24821),CNST_LIMB(0x77cfeb6bbb),CNST_LIMB(0x7550ebd97c7),CNST_LIMB(0xe5f08695caf),CNST_LIMB(0x386120ffce11),CNST_LIMB(0x6eabb28dd6df),CNST_LIMB(0x3658e31c82a8f),CNST_LIMB(0x6ad2050312783),CNST_LIMB(0x1a42902a5af0bf),CNST_LIMB(0x33ac44f881661d),CNST_LIMB(0xcb764f927d82123),CNST_LIMB(0x190c23fa46b93983),CNST_LIMB(0x62b7609e25caf1b9),CNST_LIMB(0xc29cb72925ef2cff)
#define ODD_CENTRAL_BINOMIAL_TABLE_LIMIT (35)
/* This table contains the inverses of elements in the previous table. */
#define ONE_LIMB_ODD_CENTRAL_BINOMIAL_INVERSE_TABLE CNST_LIMB(0x61e5bd199bb12643),CNST_LIMB(0x78321494dc8342cf),CNST_LIMB(0x4fd348704ebf7ad5),CNST_LIMB(0x7e722ba086ab568b),CNST_LIMB(0xa5fcc124265843db),CNST_LIMB(0x89c4a6b18633f431),CNST_LIMB(0x4daa2c15f8ce9227),CNST_LIMB(0x801c618ca9be9605),CNST_LIMB(0x32dc192f948a441),CNST_LIMB(0xd02b90c2bf3be1),CNST_LIMB(0xd897e8c1749aa173),CNST_LIMB(0x54a234fc01fef9f7),CNST_LIMB(0x83ff2ab4d1ff7a4f),CNST_LIMB(0xa427f1c9b304e2f1),CNST_LIMB(0x9c14595d1793651f),CNST_LIMB(0x883a71c607a7b46f),CNST_LIMB(0xd089863c54bc9f2b),CNST_LIMB(0x9022f6bce5d07f3f),CNST_LIMB(0xbec207e218768c35),CNST_LIMB(0x9d70cb4cbb4f168b),CNST_LIMB(0x3c3d3403828a9d2b),CNST_LIMB(0x7672df58c56bc489),CNST_LIMB(0x1e66ca55d727d2ff)
/* This table contains the values t in the formula binomial(2k,k)/2^t */
#define CENTRAL_BINOMIAL_2FAC_TABLE 3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,1,2,2,3
/* This file generated by gen-fib.c - DO NOT EDIT. */
#if GMP_NUMB_BITS != 64
Error, error, this data is for 64 bits
#endif
#define FIB_TABLE_LIMIT 93
#define FIB_TABLE_LUCNUM_LIMIT 92
This diff is collapsed.
/* Generic C gmp-mparam.h -- Compiler/machine parameter header file.
Copyright 1991, 1993, 1994, 2000 Free Software Foundation, Inc.
This file is part of the GNU MP Library.
The GNU MP Library is free software; you can redistribute it and/or modify
it under the terms of either:
* the GNU Lesser General Public License as published by the Free
Software Foundation; either version 3 of the License, or (at your
option) any later version.
or
* the GNU General Public License as published by the Free Software
Foundation; either version 2 of the License, or (at your option) any
later version.
or both in parallel, as here.
The GNU MP Library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
for more details.
You should have received copies of the GNU General Public License and the
GNU Lesser General Public License along with the GNU MP Library. If not,
see https://www.gnu.org/licenses/. */
/* Values for GMP_LIMB_BITS etc will be determined by ./configure and put
in config.h. */
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
/* This file generated by gen-bases.c - DO NOT EDIT. */
#if GMP_NUMB_BITS != 64
Error, error, this data is for 64 bits
#endif
/* mp_bases[10] data, as literal values */
#define MP_BASES_CHARS_PER_LIMB_10 19
#define MP_BASES_BIG_BASE_10 CNST_LIMB(0x8ac7230489e80000)
#define MP_BASES_BIG_BASE_INVERTED_10 CNST_LIMB(0xd83c94fb6d2ac34a)
#define MP_BASES_NORMALIZATION_STEPS_10 0
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
This diff is collapsed.
/*
A C-program for MT19937-64 (2004/9/29 version).
Coded by Takuji Nishimura and Makoto Matsumoto.
This is a 64-bit version of Mersenne Twister pseudorandom number
generator.
Before using, initialize the state by using init_genrand64(seed)
or init_by_array64(init_key, key_length).
Copyright (C) 2004, Makoto Matsumoto and Takuji Nishimura,
All rights reserved.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions
are met:
1. Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
3. The names of its contributors may not be used to endorse or promote
products derived from this software without specific prior written
permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR
CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
References:
T. Nishimura, ``Tables of 64-bit Mersenne Twisters''
ACM Transactions on Modeling and
Computer Simulation 10. (2000) 348--357.
M. Matsumoto and T. Nishimura,
``Mersenne Twister: a 623-dimensionally equidistributed
uniform pseudorandom number generator''
ACM Transactions on Modeling and
Computer Simulation 8. (Jan. 1998) 3--30.
Any feedback is very welcome.
http://www.math.hiroshima-u.ac.jp/~m-mat/MT/emt.html
email: m-mat @ math.sci.hiroshima-u.ac.jp (remove spaces)
*/
#include <stdio.h>
#define NN 312
#define MM 156
#define MATRIX_A 0xB5026F5AA96619E9ULL
#define UM 0xFFFFFFFF80000000ULL /* Most significant 33 bits */
#define LM 0x7FFFFFFFULL /* Least significant 31 bits */
/* The array for the state vector */
static unsigned long long mt[NN];
/* mti==NN+1 means mt[NN] is not initialized */
static int mti=NN+1;
/* initializes mt[NN] with a seed */
void init_genrand64(unsigned long long seed)
{
mt[0] = seed;
for (mti=1; mti<NN; mti++)
mt[mti] = (6364136223846793005ULL * (mt[mti-1] ^ (mt[mti-1] >> 62)) + mti);
}
/* initialize by an array with array-length */
/* init_key is the array for initializing keys */
/* key_length is its length */
void init_by_array64(unsigned long long init_key[],
unsigned long long key_length)
{
unsigned long long i, j, k;
init_genrand64(19650218ULL);
i=1; j=0;
k = (NN>key_length ? NN : key_length);
for (; k; k--) {
mt[i] = (mt[i] ^ ((mt[i-1] ^ (mt[i-1] >> 62)) * 3935559000370003845ULL))
+ init_key[j] + j; /* non linear */
i++; j++;
if (i>=NN) { mt[0] = mt[NN-1]; i=1; }
if (j>=key_length) j=0;
}
for (k=NN-1; k; k--) {
mt[i] = (mt[i] ^ ((mt[i-1] ^ (mt[i-1] >> 62)) * 2862933555777941757ULL))
- i; /* non linear */
i++;
if (i>=NN) { mt[0] = mt[NN-1]; i=1; }
}
mt[0] = 1ULL << 63; /* MSB is 1; assuring non-zero initial array */
}
/* generates a random number on [0, 2^64-1]-interval */
unsigned long long genrand64_int64(void)
{
int i;
unsigned long long x;
static unsigned long long mag01[2]={0ULL, MATRIX_A};
if (mti >= NN) { /* generate NN words at one time */
/* if init_genrand64() has not been called, */
/* a default initial seed is used */
if (mti == NN+1)
init_genrand64(5489ULL);
for (i=0;i<NN-MM;i++) {
x = (mt[i]&UM)|(mt[i+1]&LM);
mt[i] = mt[i+MM] ^ (x>>1) ^ mag01[(int)(x&1ULL)];
}
for (;i<NN-1;i++) {
x = (mt[i]&UM)|(mt[i+1]&LM);
mt[i] = mt[i+(MM-NN)] ^ (x>>1) ^ mag01[(int)(x&1ULL)];
}
x = (mt[NN-1]&UM)|(mt[0]&LM);
mt[NN-1] = mt[MM-1] ^ (x>>1) ^ mag01[(int)(x&1ULL)];
mti = 0;
}
x = mt[mti++];
x ^= (x >> 29) & 0x5555555555555555ULL;
x ^= (x << 17) & 0x71D67FFFEDA60000ULL;
x ^= (x << 37) & 0xFFF7EEE000000000ULL;
x ^= (x >> 43);
return x;
}
/* generates a random number on [0, 2^63-1]-interval */
long long genrand64_int63(void)
{
return (long long)(genrand64_int64() >> 1);
}
/* generates a random number on [0,1]-real-interval */
double genrand64_real1(void)
{
return (genrand64_int64() >> 11) * (1.0/9007199254740991.0);
}
/* generates a random number on [0,1)-real-interval */
double genrand64_real2(void)
{
return (genrand64_int64() >> 11) * (1.0/9007199254740992.0);
}
/* generates a random number on (0,1)-real-interval */
double genrand64_real3(void)
{
return ((genrand64_int64() >> 12) + 0.5) * (1.0/4503599627370496.0);
}
#if defined(TEST_GMP) || defined(TEST_WHY3) || defined(TEST_MINIGMP)
#define BENCH
#else
#define COMPARE
#ifdef COMPARE_MINI
#define TEST_MINIGMP
#else
#define TEST_GMP
#endif
#define TEST_WHY3
#define TEST_ADD
#define TEST_MUL
#define TEST_DIV
#endif
#ifdef TEST_MINIGMP
#include "mini-gmp.c"
#else
#include <gmp.h>
#endif
#include "mt19937-64.c"
#include <stdint.h>
#include <stdio.h>
#include <stdlib.h>
#include <sys/time.h>
#include <time.h>
uint64_t add(uint64_t * r3, uint64_t * x4, uint64_t * y3, int32_t sx, int32_t
sy);
void mul(uint64_t * r10, uint64_t * x11, uint64_t * y10, int32_t sx2, int32_t
sy2);
void tdiv_qr(uint64_t * q, uint64_t * r, uint64_t * x, uint64_t * y,
int32_t sx, int32_t sy);
#define TMP_ALLOC_LIMBS(n) malloc((n) * 8)
void mpn_dump(mp_ptr ap, mp_size_t an) {
for (mp_size_t i = 0; i != an; ++i)
printf("%016lx ", ap[i]);
printf("\n");
}
void init_valid (mp_ptr ap, mp_ptr bp, mp_size_t an, mp_size_t bn) {
for (int i = 0; i <= an; i++)
ap[i] = genrand64_int64();
for (int i = 0; i <= bn; i++)
bp[i] = genrand64_int64();
while (bp[bn-1]==0)
bp[bn-1] = genrand64_int64();
return;
}
int main () {
mp_ptr ap, bp, rp, refp, rq, rr, refq, refr;
mp_size_t max_n, an, bn, rn;
#ifdef BENCH
struct timeval begin, end;
double elapsed;
#endif
uint64_t c, refc;
//gmp_randstate_t rands;
//TMP_DECL;
//TMP_MARK;
//tests_start ();
//TESTS_REPS (reps, argv, argc);
//gmp_randinit_default(rands);
//gmp_randseed_ui(rands, 42);
/* Re-interpret reps argument as a size argument. */
init_genrand64((unsigned long long)time(NULL));
max_n = 20;
ap = TMP_ALLOC_LIMBS (max_n + 1);
bp = TMP_ALLOC_LIMBS (max_n + 1);
/* nap = TMP_ALLOC_LIMBS (max_n + 1); */
/* nbp = TMP_ALLOC_LIMBS (max_n + 1); */
rp = TMP_ALLOC_LIMBS (2 * max_n);
refp = TMP_ALLOC_LIMBS (2 * max_n);
rq = TMP_ALLOC_LIMBS (max_n + 1);
rr = TMP_ALLOC_LIMBS (max_n + 1);
refq = TMP_ALLOC_LIMBS (max_n + 1);
refr = TMP_ALLOC_LIMBS (max_n + 1);
#ifdef TEST_ADD
#ifdef BENCH
printf ("#an bn t(s)\n");
#endif
for (an = 2; an <= max_n; an += 1)
{
for (bn = 1; bn <= an; bn += 1)
{
init_valid (ap, bp, an, bn);
#ifdef BENCH
elapsed = 0;
for (int iter = 0; iter != 10000; ++iter) {
init_valid (ap, bp, an, bn);
gettimeofday(&begin, NULL);
for (int i = 0; i != 1000; ++i)
{
#endif
#if defined(TEST_GMP) || defined(TEST_MINIGMP)
c = mpn_add (refp, ap, an, bp, bn);
#endif
#ifdef TEST_WHY3
refc = add (rp, ap, bp, an, bn);
#endif
#ifdef BENCH
}
gettimeofday(&end, NULL);
elapsed +=
(end.tv_sec - begin.tv_sec)
+ ((end.tv_usec - begin.tv_usec)/1000000.0);
}
printf ("%d %d %f\n", an, bn, elapsed);
if (an==bn)
printf ("\n"); //for gnuplot
#endif
#ifdef COMPARE
rn = an;
if (mpn_cmp (refp, rp, rn))
{
printf ("ERROR, an = %d, bn = %d, rn = %d\n",
(int) an, (int) bn, (int) rn);
printf ("a: "); mpn_dump (ap, an);
printf ("b: "); mpn_dump (bp, bn);
printf ("r: "); mpn_dump (rp, rn);
printf ("ref: "); mpn_dump (refp, rn);
abort();
}
if (c != refc)
{
printf ("ERROR, an = %d, bn = %d, rn = %d\n",
(int) an, (int) bn, (int) rn);
printf ("a: "); mpn_dump (ap, an);
printf ("b: "); mpn_dump (bp, bn);
printf ("c: %016lx\n", c);
printf ("refc: %016lx\n", refc);
abort();
}
#endif
}
}
#ifdef COMPARE
printf ("addition ok\n");
#endif
#endif
#ifdef TEST_MUL
#ifdef BENCH
printf ("#an bn t(s)\n");
#endif
for (an = 2; an <= max_n; an += 1)
{
for (bn = 1; bn <= an; bn += 1)
{
init_valid (ap, bp, an, bn);
#ifdef BENCH
elapsed = 0;
for (int iter = 0; iter != 5000; ++iter) {
init_valid (ap, bp, an, bn);
gettimeofday(&begin, NULL);
for (int i = 0; i != 1000; ++i)
{
#endif
#if defined(TEST_GMP) || defined(TEST_MINIGMP)