CBMC
irep_hash.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: irep hash functions
4 
5 Author: Michael Tautschnig, mt@eecs.qmul.ac.uk
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_UTIL_IREP_HASH_H
13 #define CPROVER_UTIL_IREP_HASH_H
14 
15 // you need to pick one of the following options
16 
17 #define IREP_HASH_BASIC
18 // #define IREP_HASH_MURMURHASH2A
19 // #define IREP_HASH_MURMURHASH3
20 
21 // Comparison for OS X, 64 bit, LLVM version 5.1:
22 //
23 // On the regression test suite (cbmc), BASIC 55 times leads to fewer
24 // calls to irept::operator==, and 210 times MURMURHASH3 results in
25 // fewer calls; BASIC has a total of 1479007 calls, whereas
26 // MURMURHASH3 has 1455539 calls; worst case of BASIC improving over
27 // MURMURHASH3 is strtol1 with 4696 fewer calls (3.0%); best case of
28 // MURMURHASH3 improving over BASIC with 1893 fewer calls (3.5%) is
29 // Double-to-float-with-simp1
30 //
31 // Comparing BASIC and MURMURHASH2A, we have 72 cases with fewer calls
32 // in BASIC, and 195 cases with MURMURHASH2A having fewer calls at a
33 // total of 1454334 calls; BASIC improves the most over MURMURHASH2A
34 // on Double-to-float-with-simp1 with 3367 fewer calls (6.3%), while
35 // MURMURHASH2A compares most favourably on String6 with 3076 fewer
36 // calls (2.9%)
37 
38 #include <climits>
39 #include <cstddef> // std::size_t
40 
41 #ifdef _MSC_VER
42 
43 # define FORCE_INLINE __forceinline
44 
45 # include <cstdint>
46 # include <cstdlib>
47 
48 # define ROTL32(x, y) _rotl(x, y)
49 # define ROTL64(x, y) _rotl64(x, y)
50 
51 # define BIG_CONSTANT(x) (x)
52 
53 #else // !_MSC_VER
54 
55 # define FORCE_INLINE inline __attribute__((always_inline))
56 
57 # include <stdint.h>
58 
59 static FORCE_INLINE uint32_t ROTL32(uint32_t x, int8_t r)
60 {
61  return (x << r) | (x >> (32-r));
62 }
63 
64 static FORCE_INLINE uint64_t ROTL64(uint64_t x, int8_t r)
65 {
66  return (x << r) | (x >> (64-r));
67 }
68 
69 # define BIG_CONSTANT(x) (x##LLU)
70 
71 #endif
72 
73 
74 #ifdef IREP_HASH_BASIC
75 
76 template<int>
77 std::size_t basic_hash_combine(
78  std::size_t h1,
79  std::size_t h2);
80 
81 template<>
82 inline std::size_t basic_hash_combine<32>(
83  std::size_t h1,
84  std::size_t h2)
85 {
86  return ROTL32(h1, 7)^h2;
87 }
88 
89 template<>
90 inline std::size_t basic_hash_combine<64>(
91  std::size_t h1,
92  std::size_t h2)
93 {
94  #ifdef _MSC_VER
95  // The below intentionally limits the hash key to 32 bits.
96  // This is because Visual Studio's STL masks away anything
97  // but the least significant n bits, where 2^n is the size of
98  // the hash table. On systems with 64-bit size_t, we then see
99  // performance degradation as too much of the hash key is
100  // contained in bits that will be masked away. There is no such
101  // issue when using the GNU C++ STL.
102 
103  unsigned int int_value=(unsigned)h1; // lose data here
104  return ROTL32(int_value, 7)^h2;
105  #else
106  return ROTL64(h1, 7)^h2;
107  #endif
108 }
109 
110 inline std::size_t basic_hash_finalize(
111  std::size_t h1,
112  std::size_t len)
113 {
114  (void)len;
115 
116  return h1;
117 }
118 
119 // Boost uses the symbol hash_combine, if you're getting problems here then
120 // you've probably included a Boost header after this one
121 # define hash_combine(h1, h2) \
122  basic_hash_combine<sizeof(std::size_t) * CHAR_BIT>(h1, h2)
123 # define hash_finalize(h1, len) basic_hash_finalize(h1, len)
124 
125 #endif
126 
127 
128 #ifdef IREP_HASH_MURMURHASH2A
129 
130 // Based on Austin Appleby's MurmurHash2A:
131 // https://code.google.com/p/pyfasthash/source/browse/trunk/src/MurmurHash/MurmurHash2A.cpp?r=19
132 // 64 bit constants taken from
133 // https://code.google.com/p/pyfasthash/source/browse/trunk/src/MurmurHash/MurmurHash2_64.cpp?r=19
134 
135 template<int>
136 std::size_t murmurhash2a_hash_combine(
137  std::size_t h1,
138  std::size_t h2);
139 
140 template<int>
141 std::size_t murmurhash2a_hash_finalize(
142  std::size_t h1,
143  std::size_t len);
144 
145 static FORCE_INLINE uint32_t mmix32(uint32_t h1, uint32_t h2)
146 {
147  const int r=24;
148  const uint32_t m=0x5bd1e995;
149 
150  h2*=m;
151  h2^=h2>>r; // NOLINT(whitespace/operators)
152  h2*=m;
153  h1*=m;
154  h1^=h2;
155 
156  return h1;
157 }
158 
159 template<>
160 inline std::size_t murmurhash2a_hash_combine<32>(
161  std::size_t h1,
162  std::size_t h2)
163 {
164  return mmix32(h1, h2);
165 }
166 
168 template<>
169 inline std::size_t murmurhash2a_hash_finalize<32>(
170  std::size_t h1,
171  std::size_t len)
172 {
173  const uint32_t m=0x5bd1e995;
174 
175  h1=mmix32(h1, len);
176 
177  h1^=h1>>13;
178  h1*=m;
179  h1^=h1>>15;
180 
181  return h1;
182 }
183 
184 static FORCE_INLINE uint64_t mmix64(uint64_t h1, uint64_t h2)
185 {
186  const int r=47;
187  const uint64_t m=0xc6a4a7935bd1e995;
188 
189  h2*=m;
190  h2^=h2>>r; // NOLINT(whitespace/operators)
191  h2*=m;
192  // the original 64bit (non-incremental) algorithm swaps the
193  // following two operations
194  h1*=m;
195  h1^=h2;
196 
197  return h1;
198 }
199 
200 template<>
201 inline std::size_t murmurhash2a_hash_combine<64>(
202  std::size_t h1,
203  std::size_t h2)
204 {
205  return mmix64(h1, h2);
206 }
207 
209 template<>
210 inline std::size_t murmurhash2a_hash_finalize<64>(
211  std::size_t h1,
212  std::size_t len)
213 {
214  const int r=47;
215  const uint64_t m=0xc6a4a7935bd1e995;
216 
217  // not in the original code
218  h1=mmix64(h1, len);
219 
220  h1^=h1>>r; // NOLINT(whitespace/operators)
221  h1*=m;
222  h1^=h1>>r; // NOLINT(whitespace/operators)
223 
224  return h1;
225 }
226 
227 # define hash_combine(h1, h2) \
228  murmurhash2a_hash_combine<sizeof(std::size_t) * CHAR_BIT>(h1, h2)
229 # define hash_finalize(h1, len) \
230  murmurhash2a_hash_finalize<sizeof(std::size_t) * CHAR_BIT>(h1, len)
231 
232 #endif
233 
234 
235 #ifdef IREP_HASH_MURMURHASH3
236 
237 // Based on MurmurHash3, originally implemented by Austin Appleby who
238 // placed the code in the public domain, disclaiming any copyright.
239 // See the original source for details and further comments:
240 // https://code.google.com/p/smhasher/source/browse/trunk/MurmurHash3.cpp
241 
242 template<int>
243 std::size_t murmurhash3_hash_combine(
244  std::size_t h1,
245  std::size_t h2);
246 
247 template<int>
248 std::size_t murmurhash3_hash_finalize(
249  std::size_t h1,
250  std::size_t len);
251 
252 template<>
253 inline std::size_t murmurhash3_hash_combine<32>(
254  std::size_t h1,
255  std::size_t h2)
256 {
257  const uint32_t c1=0xcc9e2d51;
258  const uint32_t c2=0x1b873593;
259 
260  h2*=c1;
261  h2=ROTL32(h2, 15);
262  h2*=c2;
263 
264  h1^=h2;
265  h1=ROTL32(h1, 13);
266  h1=h1*5+0xe6546b64;
267 
268  return h1;
269 }
270 
272 static FORCE_INLINE uint32_t fmix32(uint32_t h)
273 {
274  h^=h>>16;
275  h*=0x85ebca6b;
276  h^=h>>13;
277  h*=0xc2b2ae35;
278  h^=h>>16;
279 
280  return h;
281 }
282 
283 template<>
284 inline std::size_t murmurhash3_hash_finalize<32>(
285  std::size_t h1,
286  std::size_t len)
287 {
288  h1^=len;
289 
290  return fmix32(h1);
291 }
292 
293 template<>
294 inline std::size_t murmurhash3_hash_combine<64>(
295  std::size_t h1,
296  std::size_t h2)
297 {
298  const std::size_t h1_tmp=h1;
299 
300  const uint64_t c1=BIG_CONSTANT(0x87c37b91114253d5);
301  const uint64_t c2=BIG_CONSTANT(0x4cf5ad432745937f);
302 
303  h2*=c1;
304  h2=ROTL64(h2, 31);
305  h2*=c2;
306 
307  h1^=h2;
308  h1=ROTL64(h1, 27);
309  // it may be better to omit the following re-combination according
310  // to the LLBMC benchmark set, as it reduces the hash collisions in
311  // boolbv_width::get_entry, but slightly increases them elsewhere
312  h1+=h1_tmp;
313  h1=h1*5+0x52dce729;
314 
315  return h1;
316 }
317 
319 static FORCE_INLINE uint64_t fmix64(uint64_t h)
320 {
321  // a brief experiment with supposedly better constants from
322  // http://zimbry.blogspot.co.uk/2011/09/better-bit-mixing-improving-on.html
323  // rather resulted in a slightly worse result
324  h^=h>>33;
325  h*=BIG_CONSTANT(0xff51afd7ed558ccd);
326  h^=h>>33;
327  h*=BIG_CONSTANT(0xc4ceb9fe1a85ec53);
328  h^=h>>33;
329 
330  return h;
331 }
332 
333 template<>
334 inline std::size_t murmurhash3_hash_finalize<64>(
335  std::size_t h1,
336  std::size_t len)
337 {
338  h1^=len;
339 
340  return fmix64(h1);
341 }
342 
343 # define hash_combine(h1, h2) \
344  murmurhash3_hash_combine<sizeof(std::size_t) * CHAR_BIT>(h1, h2)
345 # define hash_finalize(h1, len) \
346  murmurhash3_hash_finalize<sizeof(std::size_t) * CHAR_BIT>(h1, len)
347 
348 #endif
349 
350 #endif // CPROVER_UTIL_IREP_HASH_H
std::size_t basic_hash_finalize(std::size_t h1, std::size_t len)
Definition: irep_hash.h:110
static int8_t r
Definition: irep_hash.h:60
std::size_t basic_hash_combine(std::size_t h1, std::size_t h2)
#define BIG_CONSTANT(x)
Definition: irep_hash.h:69
std::size_t basic_hash_combine< 64 >(std::size_t h1, std::size_t h2)
Definition: irep_hash.h:90
#define FORCE_INLINE
Definition: irep_hash.h:55
std::size_t basic_hash_combine< 32 >(std::size_t h1, std::size_t h2)
Definition: irep_hash.h:82