refactor: Reservoir sampling to emulate byte-wise reading of a stream…

… (if the stream ends, i.e., the read syscall returns less than 1 byte, a safety violation is triggered, i.e., div-by-zero)

lion/reservoir-sampling.c

@@ -3,7 +3,6 @@
 // @UNROLL = TODO
 
 // 1, 2, 3, 4, 5, 6, 7, 15
-// user input index = 2
 // user input value = 42
 
 #include <stdio.h>
@@ -17,68 +16,90 @@ uint64_t main() {
   uint64_t* reservoir;
   // loop counters
   uint64_t n;
-  uint64_t m;
-  // number of iterations
-  uint64_t sampling_rounds;
+  uint64_t round;
+  uint64_t sum;
+  uint64_t avg;
+  uint64_t read_bytes;
   // position to replace in reservoir
   uint64_t index;
-  // value to consider for new value in reservoir
-  uint64_t new;
-  uint64_t old;
   // offset for division-by-zero safety property
-  uint64_t offset;
+  // uint64_t offset;
 
-  // TODO: Ask user for number of sampling rounds and offset?
-  sampling_rounds = 10;
   // larger numbers require more bits as user input
   // Decimal examples:
   // 42     = 00101010 (1 byte; 6 bits)
   // 4242   = 00010000 10010010 (2 bytes; 13 bits)
   // 424242 = 00000110 01111001 00110010 (3 bytes; 19 bits)
   // 42424242 = 00000010 10000111 01010111 10110010 (4 bytes; 26 bits)
-  offset = 42; 
+  // offset = 256; 
 
   entry_size = SIZEOFUINT64; // one spot has 64 bits = 8 bytes
-  entry_count = SIZEOFUINT64; // 8 spots
+  entry_count = 8; // 8 spots
 
   // allocate (8 x 8) bytes = 64 bytes
   reservoir = malloc(entry_count * entry_size);
 
-  // inital filling of reservoir
-  n = 0;
-  while (n < entry_count) {
-    *(reservoir + n) = VERIFIER_nondet_uint();
-    n = n + 1;
-  }
+  read_bytes = 0;
+
+  // inital filling of reservoir (dec.):
+  //        +--+--+-+--+-+--+--+--+
+  //        |38|39|5|24|2|28|18|50|
+  //        +--+--+-+--+-+--+--+--+
+  // hard-coded, sum = CC (dec: 204)
+  *(reservoir + 0) = 0x00000026; // dec: 38
+  *(reservoir + 1) = 0x00000027; // dec: 39
+  *(reservoir + 2) = 0x00000005; // dec: 5
+  *(reservoir + 3) = 0x00000018; // dec: 24
+  *(reservoir + 4) = 0x00000002; // dec: 2
+  *(reservoir + 5) = 0x0000001C; // dec: 28
+  *(reservoir + 6) = 0x00000012; // dec: 18
+  *(reservoir + 7) = 0x00000032; // dec: 50
 
   // actual reservoir sampling until su
-  n = 0;
-  while (n < sampling_rounds) {
-    // determine index to replace by user input
-    index = VERIFIER_nondet_uint();
+  round = 0;
+  sum = 0;
+  while (round < 10) {
+    // debug
+    n = 0;
+    printf("Reservoir (round %ld): [ ", round);
+    while (n < entry_count) {
+      printf("%ld ", *(reservoir + n));
+      n = n + 1;
+    }
+    printf("]\n");
 
-    // determine new value by user input
-    new = VERIFIER_nondet_uint();
-
-    // new value: old value^2 divided by (offset - user input)
-    // possibly a division-by-zero if (offset - new) is zero
-    if (index >= 0) {
-      if (index < entry_count) {
-        old = *(reservoir + index);
-        new = (old * old) / (offset - new);
-      }
+    // do some work with constant complexity
+    // build sum of current reservoir
+    n = 0;
+    sum = 0;
+    while (n < entry_count) {
+      sum = sum + *(reservoir + n);
+      n = n + 1;
     }
+    // compute avg of current reservoir
+    avg = sum / entry_count;
+    // debug 
+    printf("sum: %ld, avg: %ld\n", sum, avg);
 
-    // replace value in reservoir
-    if (index >= 0)
-      if (index < entry_count)
-        *(reservoir + index) = new;
 
-    n = n + 1;
-  }
+    // replace a "random" element
+    index = round % entry_count;
+    // debug
+    printf("reservoir[%ld] = %ld", index, *(reservoir + index));
 
-  VERIFIER_error();
+    // determine new value by user input
+    read_bytes = read(0, (reservoir + index), SIZEOFUINT8);
+    printf(", new bytes = %lx", *(reservoir + index));
+
+    // check if the expected amount of bytes has been read
+    if (read_bytes < SIZEOFUINT8)
+      *(reservoir + index) = 1 / 0; // (offset - sum);
+
+    // debug
+    printf(" ===>>> %ld (read_bytes: %ld)\n", *(reservoir + index), read_bytes);
+
+    round = round + 1;
+  }
 
-  // gcc / valgrind
-  // free(reservoir);
+  return 0;
 }