bloomFilter/bloom2.c0 at master · shback0708/bloomFilter · GitHub

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
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
#use <string>


/*** Interface to bloom filters ***/

typedef struct bloom_filter* bloom_t;

bloom_t bloom_new(int m)
  /*@requires m > 0; @*/
  /*@ensures \result != NULL; @*/ ;

bool bloom_contains(bloom_t B, string x)
  /*@requires B != NULL; @*/ ;

void bloom_add(bloom_t B, string x)
  /*@requires B != NULL; @*/
  /*@ensures bloom_contains(B, x); @*/ ;

bool get_bit(int[] A, int i)
  /*@requires 0 <= i && i/32 < \length(A); @*/ ;

void set_bit(int[] A, int i)
  /*@requires 0 <= i && i/32 < \length(A); @*/
  /*@ensures get_bit(A,i); @*/ ;

/*** Implementation of bloom filters ***/

int hash1(string s){
    char[] char_arr = string_to_chararray(s);
    int len = string_length(s);
    int count = 0;
    int hash_result = 0;
    while (count < len) {
    hash_result = hash_result * 31 + char_ord(char_arr[count]);
    count++;
    }
    if (hash_result < 0){
        return -1 * (hash_result + 1);
    }
    return hash_result;
}

int hash2(string s){
    char[] char_arr = string_to_chararray(s);
    int len = string_length(s);
    int count = 0;
    int hash_result = 0;
    while (count < len) {
    hash_result = hash_result * 179 + char_ord(char_arr[count]);
    count++;
    }
    if (hash_result < 0){
        return -1 * (hash_result + 1);
    }
    return hash_result;
}

int hash3(string s){
    char[] char_arr = string_to_chararray(s);
    int len = string_length(s);
    int count = 0;
    int hash_result = 0;
    while (count < len) {
    hash_result = hash_result * 419 + char_ord(char_arr[count]);
    count++;
    }
    if (hash_result < 0){
        return -1 * (hash_result + 1);
    }
    return hash_result;
}

typedef struct bloom_filter bloom;
struct bloom_filter {
  int[] data;
  int limit; // limit == \length(data);
};

bool is_bloom(bloom_t B)

{
  if (B == NULL) return false;
  //@assert B -> limit == \length(B -> data);
  return true;
}

bloom* bloom_new(int m)
//@requires m > 0;
//@ensures is_bloom(\result);
{
  bloom_t B = alloc(bloom);
  B->data = alloc_array(int,(m-1)/32+1);
  B -> limit = (m-1)/32+1;
  for (int i = 0; i < B->limit; i++){
    B -> data[i] = B -> limit;
  }
  return B;
}

bool bloom_contains(bloom* B, string x)
//@requires is_bloom(B);
{
  int i1 = hash1(x)%B->limit*32;
  int i2 = hash2(x)%B->limit*32;
  int i3 = hash3(x)%B->limit*32;
  return get_bit(B->data,i1) && get_bit(B->data,i2) && get_bit(B->data,i3);
}

void bloom_add(bloom* B, string x)
//@requires is_bloom(B);
//@ensures is_bloom(B);
//@ensures bloom_contains(B, x);
{
  int i1 = hash1(x)%B->limit*32;
  int i2 = hash2(x)%B->limit*32;
  int i3 = hash3(x)%B->limit*32;
  set_bit(B->data,i1);
  set_bit(B->data,i2);
  set_bit(B->data,i3);
}

bool get_bit(int[] A, int i)
{
  int bucket = A[i/32];
  if ((bucket >> (i % 32)) % 2 == 1){
    return true;
  }
  return false;
}

void set_bit(int[] A, int i)
{
  A[i/32] = A[i/32] | 1 << (i % 32);
}