source: CIVL/examples/verifyThis/treeBuffer/treebuffer.cvl

#include <stdio.h>
#include <seq.cvh>
#include <assert.h>
#include <stdarg.h>
#include <stdint.h>
#include <stdio.h>
#include <stdlib.h>
#include "treebuffer.h"

#define unused(x) ((void)x)
#define M (t->mems += 1)
#define MM (t->mems += 2)
#define MMM (t->mems += 3)
#define MMMM (t->mems += 4)

struct Node {
  Node * parent;
  int children; // the number of x such that (x->parent == this)
  Node * ll, * rl; // left link, right link; used for several lists
  int depth; // distance to root
  Node * representant; // ancestor with (depth % history == 0)
  int active_count; // number of x that are active and x->representant == this
  char seen; // used for garbage collection
  char active;
  int data;

  // NOTE: All lists using |ll| and |rl| are doubly linked, circular, and
  // using a sentinel.

  // TODO: pointer to tree so that I can assert that added nodes aren't already in a tree
};

typedef struct TBTree {
  int history;
  enum algo algo;
  Node * active; // list of active nodes
  Node * to_delete;
  //  FILE * statistics_file;
  int node_count; // only maintained by tb_amortized
  int last_gc_node_count; // only maintained by tb_amortized
  int mems;
  int ref_count; // references from "Tree"
} TBTree;

struct Tree {
  int history;
  TBTree * tree;
  Node * last_add;
};

Node * tb_make_node(int data) {
  Node * r = malloc(sizeof(Node));
  r->parent = 0;
  r->children = 0;
  r->ll = r->rl = r;
  r->depth = -1;
  r->representant = 0;
  r->active_count = 0;
  r->seen = 0;
  r->active = 1;
  r->data = data;
  return r;
}

int tb_get_data(Node * x) {
  return x->data;
}

TBTree * tb_initialize(int history, enum algo algo, Node * root) {
  assert (root);
  assert (history > 0);
  TBTree * t = malloc(sizeof(TBTree));
  t->history = history;
  t->algo = algo;
  t->active = malloc(sizeof(Node));
  t->active->ll = t->active->rl = root;
  t->active->parent = 0;
  root->ll = root->rl = t->active;
  root->depth = 0;
  root->representant = root;
  root->active_count = 1;
  assert (root->active);
  t->to_delete = malloc(sizeof(Node));
  t->to_delete->ll = t->to_delete->rl = t->to_delete;
  //t->statistics_file = 0;
  t->node_count = 1;
  t->last_gc_node_count = 1;
  t->mems = 0;
  t->ref_count = 0;
  return t;
}

void cut_parent(TBTree * t, Node * y) {
  Node * x = (M, y->parent);
  if (x && (M, --x->children == 0) && !(M, x->active)) {
    assert (x->ll == x); // not in some other list
    assert (x->rl == x);
    x->ll = t->to_delete, MM; x->rl = t->to_delete->rl, MMM;
    x->ll->rl = x->rl->ll = x, MMMM;
  }
  y->parent = 0, M;
}

void delete_one(TBTree * t) {
  assert (t);
  Node * x = (MM, t->to_delete->rl);
  if ((M, x == t->to_delete)) return;
  assert (t->algo == tb_real_time);
  x->ll->rl = x->rl, MMM; x->rl->ll = x->ll, MMM;
  x->ll = x->rl = x, MM;
  cut_parent(t, x);
  free(x), M;
}

void tb_delete(TBTree * t) {
  if (!t) return;
  assert (t->mems == 0);

  // Move |active| into |to_delete|.
  { Node * L = (MM, t->active->ll);
    Node * R = (MM, t->active->rl);
    R->ll = t->to_delete, MM;
    L->rl = t->to_delete->rl, MMM;
    t->active->rl->ll->rl = t->active->rl; t->mems += 6;
    t->active->ll->rl->ll = t->active->ll; t->mems += 6;
    t->active->ll = t->active->rl = t->active; t->mems += 5;
  }

  // Cleanup.
  t->algo = tb_real_time, M;
  while ((MMM, t->to_delete->rl != t->to_delete)) delete_one(t);
  t->mems = 0;
  free(t->active);
  free(t->to_delete);
  free(t);
}

void gc_todo_parent(TBTree * t, Node * y, Node * todo) {
  assert (y);
  Node * x = (M, y->parent);
  if (!x) return;
  if ((M, x->seen)) return;
  x->seen = 1, M;
  x->ll = todo, M; x->rl = todo->rl, MM;
  x->ll->rl = x->rl->ll = x, MMMM;
}

void gc_parent(TBTree *, Node *);

void gc_node(TBTree * t, Node * x) {
  assert (t);
  assert (x);
  assert (!x->seen);
  assert (!x->active);
  assert (x->children == 0);
  gc_parent(t, x);
  free(x);
  if (t->algo == tb_amortized) --t->node_count, M;
}

void gc_parent(TBTree * t, Node * y) {
  assert (t);
  assert (y);
  Node * x = (M, y->parent);
  y->parent = 0, M;
  if (x && (M, --x->children == 0) && (M, !x->seen)) {
    gc_node(t, x);
  }
}

void gc(TBTree * t) {
  assert (t);
  assert (t->algo == tb_gc || t->algo == tb_amortized);

  for (Node * n = (MM, t->active->rl); (M, n != t->active); (M, n = n->rl)) {
    n->seen = 1, M;
  }
  Node sentinel_a, sentinel_b, sentinel_c;
  Node * now; // being processed now
  Node * todo; // to process after now
  Node * middle; // was processed, but doesn't include active nodes
  now = &sentinel_a; todo = &sentinel_b; middle = &sentinel_c;
  middle->ll = middle->rl = middle, MM;
  now->ll = now->rl = now, MM;
  todo->ll = todo->rl = todo, MM;
  for (Node * n = (MM, t->active->rl); (M, n != t->active); (M, n = n->rl)) {
    gc_todo_parent(t, n, todo);
  }
  for (int layer = 2; (MM, layer < t->history && todo != todo->rl); ++layer) {
    { Node * tmp = now; now = todo; todo = tmp; }
    for (Node * n = (M, now->rl); n != now; (M, n = n->rl)) {
      gc_todo_parent(t, n, todo);
    }

    // Move |now| content into |middle|.
    { Node * nl = (M, now->ll);
      Node * nr = (M, now->rl);
      nr->ll = middle, M;
      nl->rl = middle->rl, MM;
      now->rl->ll->rl = now->rl, MMMM;
      now->ll->rl->ll = now->ll, MMMM;
      now->ll = now->rl = now, MM;
    }
  }
  for (Node * n = (M, todo->rl); n != todo; (M, n = n->rl)) {
    gc_parent(t, n);
  }
  { Node * p, * q;
    for (p = (MM, t->to_delete->rl); p != (M, t->to_delete); p = q) {
      q = p->rl, M;
      gc_node(t, p);
    }
    t->to_delete->rl = t->to_delete->ll = t->to_delete, t->mems += 5;
  }
  assert (now->ll == now);
  assert (now->rl == now);
  for (Node * n = (M, todo->rl); n != todo; (M, n = n->rl)) n->seen = 0, M;
  for (Node * n = (M, middle->rl); n != middle; (M, n = n->rl)) n->seen = 0, M;
  for (Node * n = (MM, t->active->rl); (M, n != t->active); (M, n = n->rl))
    n->seen = 0, M;
  { Node * p, * q;
    for (p = (M, todo->rl); p != todo; p = q) {
      q = p->rl, M;
      p->ll = p->rl = p, MM;
    }
    for (p = (M, middle->rl); p != middle; p = q) {
      q = p->rl, M;
      p->ll = p->rl = p, MM;
    }
  }

  if (t->algo == tb_amortized) {
    t->last_gc_node_count = t->node_count, MM;
  }
}

void tb_add_child(TBTree * t, Node * parent, Node * child) {
  assert (t);
  assert (t->mems == 0);
  assert (parent);
  assert (child);
  child->parent = parent, M;
  ++parent->children, M;
  child->ll = t->active, MM; child->rl = t->active->rl, MMM;
  child->ll->rl = child->rl->ll = child, MMMM;
  if (t->algo == tb_amortized) {
    if ((MM, ++t->node_count >= 2 * t->last_gc_node_count)) gc(t);
  } else if (t->algo == tb_real_time) {
    delete_one(t);
    child->depth = parent->depth + 1, MM;
    child->representant =
      (MM, child->depth % t->history == 0)? child : (M, parent->representant); M;
    ++child->representant->active_count, MM;
  }
  t->mems = 0;
}

void tb_deactivate(TBTree * t, Node * n) {
  assert (t);
  assert (t->mems == 0);
  assert (n);
  assert (n->active);
  n->active = 0;
  n->ll->rl = n->rl, MMM; n->rl->ll = n->ll, MMM;
  n->ll = n->rl = n, MM;
  if ((M, n->children == 0)) {
    n->ll = t->to_delete, MM; n->rl = t->to_delete->rl, MMM;
    n->ll->rl = n->rl->ll = n, MMMM;
  }
  if (t->algo == tb_gc) {
    gc(t);
  }
  if (t->algo == tb_real_time) {
    assert (n->representant);
    if ((MM, --n->representant->active_count) == 0) {
      cut_parent(t, n->representant);
    }
  }
  t->mems = 0;
}

void tb_expand(TBTree * t, Node * parent, Node * children[]) {
  for (Node ** n = children; *n; ++n) tb_add_child(t, parent, *n);
  tb_deactivate(t, parent);
}

void tb_history(TBTree * t, Node * node, Node * ancestors[]) {
  assert (t->mems == 0);
  assert (node->active);
  int h = (M, t->history);
  while (node && h--) {
    *ancestors++ = node, M;
    node = node->parent, M;
  }
  *ancestors = 0, M;
  t->mems = 0;
}

Node * tb_active(const TBTree * t) {
  assert (t);
  if (t->active->rl == t->active) return 0;
  return t->active->rl;
}

// PRE: |n| is in |t| (*not* checked by assertions), and active
Node * tb_next_active(const TBTree * t, const Node * n) {
  assert (t);
  assert (n);
  //  assert (n->active);
  if (n->rl == t->active) return 0;
  return n->rl;
}

/* ********* VerifyThis 2017 interface extension ********* */

int get_data(Node * node) {
  return tb_get_data(node);
}

Tree * empty(int history) {
  Tree * tree = (Tree*)malloc(sizeof(Tree));
  
  tree->history = history;
  tree->tree = NULL;
  tree->last_add = NULL;
  return tree;
}

Tree * add(Tree * tree, int data) {
  Node * child = tb_make_node(data);
  Tree * new_tree = (Tree*)malloc(sizeof(Tree));
  
  if (tree->tree == NULL) {
    new_tree->tree = tb_initialize(tree->history, tb_real_time, child);
    new_tree->history = tree->history;
    new_tree->last_add = child;
  } else {
    tb_add_child(tree->tree, tree->last_add, child);
    new_tree->tree = tree->tree;
    new_tree->history = tree->history;
    new_tree->last_add = child;
  }
  new_tree->tree->ref_count++;
  return new_tree;
}

void take(Tree * tree, Node * ancestors[]) {
  if (tree->tree != NULL)
    tb_history(tree->tree, tree->last_add, ancestors);
  else
    ancestors[0] = 0;
}

void delete(Tree *tree) {
  TBTree * tb_tree = tree->tree;
  
  if (tb_tree!=NULL && --tb_tree->ref_count == 0)
    tb_delete(tree->tree);
  free(tree);
}

int hasSeen(Node * node, Node * seens[], int n) {
  for (int i = 0; i < n; i++) {
    if (node == seens[i]) return 1;
  }
  return 0;
}

/* Computing the H_<h, which is descried as the bound of the heap
   size */
int computing_bounds(Tree * tree) {
  $atomic{
    TBTree * t = tree->tree;
    Node *active = t->active;
    Node * level[];
    Node * seen[];
    
    $seq_init(&level, 0, NULL);  
    $seq_init(&seen, 0, NULL);  
    while (active != NULL) {
      $seq_append(&level, &active, 1);
      $seq_append(&seen, &active, 1);
      active = tb_next_active(t, active);
    }
    
    int i = 1;
    
    while (i < tree->history) {
      int level_size = $seq_length(&level);
      int seen_size;
      Node * nxt_level[];

      $seq_init(&nxt_level, 0, NULL);
      for (int j = 0; j < level_size; j++) {
        active = level[j]->parent;
        seen_size = $seq_length(&seen);
        if (active != NULL)
          if (!hasSeen(active, seen, seen_size)) {
            $seq_append(&nxt_level, &active, 1);
            $seq_append(&seen, &active, 1);
          }
      }
      // level := nxt_levl ...
      $seq_remove(&level, 0, NULL, level_size);
      $seq_append(&level, &nxt_level, $seq_length(&nxt_level));
      i++;
    }
    return $seq_length(&seen);
  }
}

void check_heap_inbound(size_t heapsize, int history, Tree * tree, size_t *max) {
  int H = computing_bounds(tree);
  size_t boundsize = sizeof(Tree) + sizeof(TBTree) + sizeof(Node) * H
    // root, active and to_delete ...
    + sizeof(Node) * 3;
  
  if (boundsize < *max)
    boundsize = *max;
  else
    *max = boundsize;
    printf("max=%d\n", *max);
      printf("H<i=%d\n", H);
      printf("heap_size=%d\n", heapsize);
      printf("bound_size=%d\n", boundsize);
  assert(boundsize >= heapsize);
}