chiark - git - mdw - xyla/blob - rb-check.c

   1 /* -*-c-*-
   2  *
   3  * Checking red-black trees
   4  *
   5  * (c) 2024 Straylight/Edgeware
   6  */
   7
   8 /*----- Licensing notice --------------------------------------------------*
   9  *
  10  * This file is part of Xyla, a library of binary trees.
  11  *
  12  * Xyla is free software: you can redistribute it and/or modify it under
  13  * the terms of the GNU Lesser General Public License as published by the
  14  * Free Software Foundation; either version 3 of the License, or (at your
  15  * option) any later version.
  16  *
  17  * Xyla is distributed in the hope that it will be useful, but WITHOUT
  18  * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
  19  * FITNESS FOR A PARTICULAR PURPOSE.  See the GNU Lesser General Public
  20  * License for more details.
  21  *
  22  * You should have received a copy of the GNU Lesser General Public
  23  * License along with Xyla.  If not, see <https://www.gnu.org/licenses/>.
  24  */
  25
  26 /*----- Header files ------------------------------------------------------*/
  27
  28 #include "lib.h"
  29 #include "rb.h"
  30
  31 /*----- Data structures ---------------------------------------------------*/
  32
  33 struct nodeinfo {
  34   int ht;
  35 };
  36
  37 struct chkstate {
  38   int blkht;
  39 };
  40
  41 /*----- Main code ---------------------------------------------------------*/
  42
  43 static int chkrb(unsigned op, const struct xyla_bt_check *chk)
  44 {
  45   /* Check the red-black balance properties for a node. */
  46
  47   struct xyla_bt_nodecls *cls = chk->cls;
  48   struct chkstate *st = chk->state;
  49   const struct xyla_rb_node *node, *parent;
  50   struct nodeinfo *node_info, *left_info, *right_info;
  51   int ht, lht, rht;
  52   int rc = XYLA_RC_OK;
  53
  54   switch (op) {
  55     case XYLA_CHKOP_BEFORE:
  56       node = CONST_RB_NODE(chk->node); parent = CONST_RB_NODE(chk->parent);
  57       if (node->rb.f&XYLA_RBF_RED) {
  58         if (chk->pos == XYLA_BTPOS_ROOT) {
  59           if (chk->fp) {
  60             xyla_bt_bughdr("XYLA-RB", chk->root, chk->fp);
  61             fputs("root ", chk->fp);
  62             xyla_bt_printnode(cls, &node->bt, chk->fp);
  63             fputs(" is red\n", chk->fp);
  64           }
  65           rc = XYLA_RC_BAD;
  66         } else if (parent->rb.f&XYLA_RBF_RED) {
  67           if (chk->fp) {
  68             xyla_bt_bughdr("XYLA-RB", chk->root, chk->fp);
  69             fputs("red ", chk->fp);
  70             xyla_bt_printnode(cls, &node->bt, chk->fp);
  71             fputs(" has red parent ", chk->fp);
  72             xyla_bt_printnode(cls, &parent->bt, chk->fp);
  73             putc('\n', chk->fp);
  74           }
  75           rc = XYLA_RC_BAD;
  76         }
  77       }
  78       break;
  79
  80     case XYLA_CHKOP_AFTER:
  81       node_info = chk->node_info;
  82       left_info = chk->left_info; right_info = chk->right_info;
  83       node = CONST_RB_NODE(chk->node);
  84       lht = left_info ? left_info->ht : 0;
  85       rht = right_info ? right_info->ht : 0;
  86       if (lht == -1 || rht == -1) { ht = -1; goto skip_htchk; }
  87       if (lht != rht) {
  88         if (chk->fp) {
  89           xyla_bt_bughdr("XYLA-RB", chk->root, chk->fp);
  90           xyla_bt_printnode(cls, &node->bt, chk->fp);
  91           fprintf(chk->fp,
  92                   " left black-height %d /= %d right black-height\n",
  93                   lht, rht);
  94         }
  95         ht = -1; rc = XYLA_RC_BAD; goto skip_htchk;
  96       }
  97       ht = lht + (node->rb.f&XYLA_RBF_RED ? 0 : 1);
  98       if (chk->pos == XYLA_BTPOS_ROOT &&
  99           st->blkht != -1 && ht != st->blkht) {
 100         if (chk->fp) {
 101           xyla_bt_bughdr("XYLA-RB", chk->root, chk->fp);
 102           fputs("root ", chk->fp);
 103           xyla_bt_printnode(cls, &node->bt, chk->fp);
 104           fprintf(chk->fp, " black-height %d /= %d expected\n",
 105                   ht, st->blkht);
 106         }
 107         ht = -1; rc = XYLA_RC_BAD; goto skip_htchk;
 108       }
 109     skip_htchk:
 110       node_info->ht = ht;
 111       break;
 112   }
 113   return (rc);
 114 }
 115
 116 int xyla_rb_check(struct xyla_bt_nodecls *cls,
 117                   struct xyla_bt_node *const *root, FILE *fp, unsigned f,
 118                   int blkht, void *arg)
 119 {
 120   /* Examine a red-black tree, checking that it satisfies all of the
 121    * necessary invariants.  If BLKHT is not equal to -1, then check that the
 122    * tree's black-height is equal to BLKHT.
 123    *
 124    * This function uses the `xyla_bt_check' framework; see the description of
 125    * that function for details.  Returns `XYLA_RC_OK' on success,
 126    * `XYLA_RC_BAD' if problems are found, or some other code if verification
 127    * had to finish prematurely.
 128    */
 129
 130   struct chkstate st;
 131
 132   st.blkht = blkht;
 133   return (xyla_bt_check(cls, root, fp, f,
 134                         chkrb, sizeof(struct nodeinfo), &st, arg));
 135 }
 136
 137 /*----- That's all, folks -------------------------------------------------*/