From 8a46390987f98c052bdeedbdff7a5a496e6a3d79 Mon Sep 17 00:00:00 2001
From: Mark Mitchell <mark.mitchell@sri.com>
Date: Wed, 29 Nov 2023 17:00:39 -0600
Subject: [PATCH] Centralize check for maximum number of elements.

---
 src/terms/bit_expr.c      | 18 ++----------------
 src/terms/pprod_table.c   |  8 ++------
 src/terms/terms.c         | 16 ++--------------
 src/terms/types.c         | 20 ++------------------
 src/utils/indexed_table.c |  5 +++--
 src/utils/indexed_table.h |  3 +++
 6 files changed, 14 insertions(+), 56 deletions(-)

diff --git a/src/terms/bit_expr.c b/src/terms/bit_expr.c
index 6594d4064..fd32816ca 100644
--- a/src/terms/bit_expr.c
+++ b/src/terms/bit_expr.c
@@ -44,17 +44,6 @@
 #include "utils/memalloc.h"
 
 
-/*
- * Extend table.
- */
-static void extend_node_table(indexed_table_t *table) {
-  // abort if the new size is too large
-  if (table->size > MAX_NODE_TABLE_SIZE) {
-    out_of_memory();
-  }
-}
-
-
 /*
  * Initialize a node table (empty)
  * - n = initial size
@@ -64,13 +53,10 @@ static void alloc_node_table(node_table_t *table, uint32_t n) {
     n = DEF_NODE_TABLE_SIZE;
   }
 
-  if (n > MAX_NODE_TABLE_SIZE) {
-    out_of_memory();
-  }
-
   static const indexed_table_vtbl_t vtbl = {
     .elem_size = sizeof(node_desc_t),
-    .extend = extend_node_table
+    .max_elems = MAX_NODE_TABLE_SIZE,
+    .extend = NULL
   };
 
   indexed_table_init(&table->nodes, n, &vtbl);
diff --git a/src/terms/pprod_table.c b/src/terms/pprod_table.c
index 1decb5c89..b203487a3 100644
--- a/src/terms/pprod_table.c
+++ b/src/terms/pprod_table.c
@@ -31,10 +31,8 @@
  * Extend the table.
  */
 static void extend_pprod_table(indexed_table_t *t) {
-  uint32_t n = t->size;
   pprod_table_t *pprods = (pprod_table_t *) t;
-  
-  pprods->mark = extend_bitvector(pprods->mark, n);
+  pprods->mark = extend_bitvector(pprods->mark, t->size);
 }
 
 
@@ -46,12 +44,10 @@ void init_pprod_table(pprod_table_t *table, uint32_t n) {
   if (n == 0) {
     n = PPROD_TABLE_DEF_SIZE;
   }
-  if (n >= PPROD_TABLE_MAX_SIZE) {
-    out_of_memory();
-  }
 
   static const indexed_table_vtbl_t vtbl = {
     .elem_size = sizeof(pprod_table_elem_t),
+    .max_elems = PPROD_TABLE_MAX_SIZE,
     .extend = extend_pprod_table
   };
   
diff --git a/src/terms/terms.c b/src/terms/terms.c
index b62a66f13..6f6bfae8f 100644
--- a/src/terms/terms.c
+++ b/src/terms/terms.c
@@ -119,16 +119,8 @@ static void default_special_finalizer(special_term_t *s, term_kind_t tag) {
  * Callback for indexed_table::extend.
  */
 static void term_table_extend(indexed_table_t *t) {
-  uint32_t n = t->size;
-
-  // force abort if n is too large
-  if (n > YICES_MAX_TERMS) {
-    out_of_memory();
-  }
-
   term_table_t *terms = (term_table_t *)t;
-
-  terms->mark = extend_bitvector(terms->mark, n);
+  terms->mark = extend_bitvector(terms->mark, t->size);
 }
 
 
@@ -138,16 +130,12 @@ static void term_table_extend(indexed_table_t *t) {
  * - ptbl = attached power-product table.
  */
 static void term_table_init(term_table_t *table, uint32_t n, type_table_t *ttbl, pprod_table_t *ptbl) {
-  // abort if n is too large
-  if (n > YICES_MAX_TERMS) {
-    out_of_memory();
-  }
-
   /* The indexed_table_elem_t must be first. */
   assert(offsetof(term_desc_t, elem) == 0);
   
   static const indexed_table_vtbl_t vtbl = {
     .elem_size = sizeof(term_desc_t),
+    .max_elems = YICES_MAX_TERMS,
     .extend = term_table_extend
   };
   
diff --git a/src/terms/types.c b/src/terms/types.c
index e2dd2e643..7b1ce9ef7 100644
--- a/src/terms/types.c
+++ b/src/terms/types.c
@@ -91,12 +91,6 @@ static inline void delete_descriptor(type_macro_t *d) {
 }
 
 
-static void type_mtbl_extend(indexed_table_t *table) {
-  if (table->nelems > TYPE_MACRO_MAX_SIZE)
-    out_of_memory();
-}
-
-
 /*
  * Initialize the macro table
  * - n = initial size
@@ -106,13 +100,9 @@ static void type_mtbl_extend(indexed_table_t *table) {
  *   on the first addition.
  */
 static void init_type_mtbl(type_mtbl_t *table, uint32_t n) {
-  if (n > TYPE_MACRO_MAX_SIZE) {
-    out_of_memory();
-  }
-  
   static const indexed_table_vtbl_t vtbl = {
     .elem_size = sizeof(type_mtbl_elem_t),
-    .extend = type_mtbl_extend
+    .max_elems = TYPE_MACRO_MAX_SIZE,
   };
 
   indexed_table_init(&table->macros, n, &vtbl);
@@ -207,12 +197,6 @@ static void typename_finalizer(stbl_rec_t *r) {
   string_decref(r->string);
 }
 
-static void type_table_exend(indexed_table_t *t) {
-  if (t->nelems > YICES_MAX_TYPES) {
-    out_of_memory();
-  }
-}
-
 /*
  * Initialize table, with initial size = n.
  */
@@ -227,7 +211,7 @@ static void type_table_init(type_table_t *table, uint32_t n) {
 
   static const indexed_table_vtbl_t vtbl = {
     .elem_size = sizeof(type_desc_t),
-    .extend = type_table_exend
+    .max_elems = YICES_MAX_TYPES,
   };
   
   indexed_table_init(&table->types, n, &vtbl);
diff --git a/src/utils/indexed_table.c b/src/utils/indexed_table.c
index 24669eeb0..24dc3300d 100644
--- a/src/utils/indexed_table.c
+++ b/src/utils/indexed_table.c
@@ -10,7 +10,7 @@ static inline size_t elem_size(const indexed_table_t *t) {
 }
 
 static inline void check_nelems(const indexed_table_t *t) {
-  if (t->size > UINT32_MAX / elem_size(t))
+  if (t->size > t->vtbl->max_elems)
     out_of_memory();
 }
 
@@ -28,7 +28,8 @@ static void extend(indexed_table_t *t) {
 
   t->elems = safe_realloc(t->elems, n * elem_size(t));
 
-  t->vtbl->extend(t);
+  if (t->vtbl->extend)
+    t->vtbl->extend(t);
 }
 
 void indexed_table_init(indexed_table_t *t, uindex_t n,
diff --git a/src/utils/indexed_table.h b/src/utils/indexed_table.h
index 62860fa17..994949a6a 100644
--- a/src/utils/indexed_table.h
+++ b/src/utils/indexed_table.h
@@ -34,6 +34,9 @@ typedef struct indexed_table_vtbl_s {
   /* The size of an individual element. */
   size_t elem_size;
 
+  /* The maximum number of elements permitted in the table. */
+  uindex_t max_elems;
+
   /* Called after extending the table. */
   void (*extend)(indexed_table_t *t);
 } indexed_table_vtbl_t;