1#include <stdlib.h>
2#include <stdbool.h>
3#include <stdio.h>
4#include <string.h>
5#include <barrelfish/barrelfish.h>
6#include <barrelfish/types.h>
7#include <barrelfish/cap_predicates.h>
8#include <mdb/mdb.h>
9#include <mdb/mdb_tree.h>
10
11bool debug_all_the_things = false;
12
13#define DEBUG_ALL_THE_THINGS(...) \
14    do { \
15        if (debug_all_the_things) \
16            printf(__VA_ARGS__); \
17    } while(0)
18
19
20#define RUNS 20
21#define MIN_RANGES 30
22#define MAX_RANGES 100
23#define MAX_ADDR_BITS 20
24#define MAX_ADDR (1<<MAX_ADDR_BITS)
25#define QUERY_COUNT 20
26
27struct node {
28    genvaddr_t address;
29    size_t size;
30    int tiebreak;
31};
32
33static inline size_t randrange(size_t begin, size_t end)
34{
35    return begin + rand() / (RAND_MAX / (end - begin + 1) + 1);
36}
37
38static void
39get_ranges(size_t count, uint8_t max_addr_bits, struct cte *out)
40{
41    size_t gencount = 0;
42    size_t sizebits;
43    size_t size;
44    genvaddr_t max_addr = 1ULL<<max_addr_bits;
45    while (gencount < count) {
46        sizebits = randrange(1,max_addr_bits-2);
47        size = 1ULL<<sizebits;
48        genvaddr_t begin = randrange(max_addr/10, max_addr-max_addr/4);
49        genvaddr_t end = begin + size;
50        if (end > max_addr) {
51            continue;
52        }
53        bool valid = true;
54        for (int j = 0; j < gencount; j++) {
55            genvaddr_t r_addr = get_address(&(out[j].cap));
56            size_t r_size = get_size(&(out[j].cap));
57            genvaddr_t r_end = r_addr + r_size;
58            if (begin < r_addr && end > r_addr && end < r_end) {
59                valid = false;
60                break;
61            }
62            if (begin > r_addr && begin < r_end && end > r_end) {
63                valid = false;
64                break;
65            }
66        }
67        if (valid) {
68            memset(&out[gencount], 0, sizeof(struct cte));
69            out[gencount].cap.type = ObjType_RAM;
70            out[gencount].cap.rights = CAPRIGHTS_ALLRIGHTS;
71            out[gencount].cap.u.ram = (struct RAM) { .base = begin, .bytes = (1UL << sizebits) };
72            gencount++;
73        }
74    }
75}
76
77static inline size_t min_count(size_t *counts, size_t countcount)
78{
79    size_t min = (size_t)-1;
80    for (int i = 0; i < countcount; i++) {
81        if (counts[i] < min)
82            min = counts[i];
83    }
84    return min;
85}
86
87__attribute__((unused))
88static void dump_ranges(struct cte *ranges, size_t count)
89{
90    for (int i = 0; i < count; i++) {
91        printf("address = %"PRIxGENVADDR"\nsize=%zu\n",
92                ranges[i].cap.u.ram.base, ranges[i].cap.u.ram.bytes);
93    }
94}
95
96extern struct cte *mdb_root;
97int main(int argc, char *argv[])
98{
99    int r = 0;
100    for (int run = 0; run < RUNS; run++) {
101        putchar('-'); fflush(stdout);
102        size_t count = randrange(MIN_RANGES, MAX_RANGES);
103        struct cte ranges[count];
104        get_ranges(count, MAX_ADDR_BITS, ranges);
105        //dump_ranges(ranges, count);
106        set_init_mapping(ranges, count);
107        r = mdb_check_invariants();
108        assert(!r); // invariants should hold at this point
109        for (int i = 0; i < QUERY_COUNT; i++) {
110            // check what happens if we remove the root node
111            remove_mapping(mdb_root);
112            r = mdb_check_invariants();
113            if(r) {
114                printf("===================\nINVARIANT %d FAILED\n===================\n", r);
115                mdb_dump_all_the_things();
116            }
117        }
118        // empty tree
119        memset(ranges, 0, count * sizeof(struct cte));
120        mdb_root = NULL;
121    }
122    printf("Everything ok\n");
123    return 0;
124}
125