Remove infinity_exprt

This removes `infinity_exprt` together with all its uses, where were all
about array size. Any such arrays were replaced by arrays of the maximum
viable size.

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -450,7 +450,7 @@ refined_string_exprt java_string_library_preprocesst::replace_char_array(
     get_length(array, symbol_table), char_array, refined_string_type);
 
   const dereference_exprt inf_array(
-    char_array, array_typet(java_char_type(), infinity_exprt(java_int_type())));
+    char_array, array_typet(java_char_type(), java_int_type().largest_expr()));
 
   add_pointer_to_array_association(
     string_expr.content(), inf_array, symbol_table, loc, function_id, code);
@@ -619,7 +619,7 @@ exprt make_nondet_infinite_char_array(
   code_blockt &code)
 {
   const array_typet array_type(
-    java_char_type(), infinity_exprt(java_int_type()));
+    java_char_type(), java_int_type().largest_expr());
   const symbolt data_sym = fresh_java_symbol(
     pointer_type(array_type),
     "nondet_infinite_array_pointer",

jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -40,21 +40,21 @@ class tt
   {
     return java_char_type();
   }
-  typet length_type() const
+  signedbv_typet length_type() const
   {
     return java_int_type();
   }
   array_typet array_type() const
   {
-    return array_typet(char_type(), infinity_exprt(length_type()));
+    return array_typet(char_type(), length_type().largest_expr());
   }
   refined_string_typet string_type() const
   {
     return refined_string_typet(length_type(), pointer_type(char_type()));
   }
   array_typet witness_type() const
   {
-    return array_typet(length_type(), infinity_exprt(length_type()));
+    return array_typet(length_type(), length_type().largest_expr());
   }
 };
 

jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp

@@ -21,15 +21,15 @@ Author: Diffblue Ltd.
 #include <java_bytecode/java_bytecode_language.h>
 #endif
 
-typet length_type()
+signedbv_typet length_type()
 {
   return signedbv_typet(32);
 }
 
 /// Make a struct with a pointer content and an integer length
 struct_exprt make_string_argument(std::string name)
 {
-  const array_typet char_array(char_type(), infinity_exprt(length_type()));
+  const array_typet char_array(char_type(), length_type().largest_expr());
   struct_typet type(
     {{"length", length_type()}, {"content", pointer_type(char_array)}});
 

regression/cbmc-concurrency/thread_chain_cbmc1/main.c

@@ -18,7 +18,8 @@
 typedef unsigned long thread_id_t;
 
 // Internal unbounded array indexed by local thread identifiers
-__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
+__CPROVER_bool __CPROVER_threads_exited
+  [(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
 
 // A thread_chain is like a chain of threads `f, g, ...` where `f`
 // must terminate before `g` can start to run, and so forth.

regression/cbmc-concurrency/thread_chain_cbmc2/main.c

@@ -18,7 +18,8 @@
 typedef unsigned long thread_id_t;
 
 // Internal unbounded array indexed by local thread identifiers
-__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
+__CPROVER_bool __CPROVER_threads_exited
+  [(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
 
 // A thread_chain is like a chain of threads `f, g, ...` where `f`
 // must terminate before `g` can start to run, and so forth.

regression/cbmc-cpp/Vector1/lib/list

@@ -372,10 +372,10 @@ namespace std {
   #ifdef VERS1
   unsigned _version;
   #elif defined VERS2
-  unsigned _version[__CPROVER::constant_infinity_uint];
+  unsigned _version[(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
   #endif
 
-  T _data[__CPROVER::constant_infinity_uint];
+  T _data[(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
   };
 
 }

regression/cbmc-cpp/Vector1/lib/vector

@@ -416,10 +416,10 @@ namespace std {
   #ifdef VERS1
   unsigned _version;
   #elif defined VERS2
-  unsigned _version[__CPROVER::constant_infinity_uint];
+  unsigned _version[(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
   #endif
 
-  T _data[__CPROVER::constant_infinity_uint];
+  T _data[(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
   };
 
 }

regression/cbmc-cpp/initialization5/main.cpp

@@ -1,9 +1,9 @@
 #include <cassert>
-int a[__CPROVER::constant_infinity_uint];
+int a[(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
 
 struct A
 {
-  int i[__CPROVER::constant_infinity_uint];
+  int i[(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
 };
 
 A o;

regression/cbmc/Unbounded_Array5/main.c

@@ -1,4 +1,4 @@
-int mem[__CPROVER_constant_infinity_uint];
+int mem[(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
 
 int main()
 {

regression/cbmc/array_of_bool_as_bitvec/main.c

@@ -3,7 +3,7 @@
 #include <stdlib.h>
 
 __CPROVER_bool w[8];
-__CPROVER_bool v[__CPROVER_constant_infinity_uint];
+__CPROVER_bool v[(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
 
 void main()
 {

regression/contracts/is_unique_01_replace/main.c

@@ -18,7 +18,7 @@ bool ptr_ok(int *x)
 /*
 	Here are the meanings of the predicates: 
 
-static _Bool __foo_memory_map[__CPROVER_constant_infinity_uint]; 
+static _Bool __foo_memory_map[(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)]; 
 
 bool __foo_requires_is_fresh(void **elem, size_t size) {
 	*elem = malloc(size);

src/ansi-c/ansi_c_internal_additions.cpp

@@ -142,11 +142,10 @@ void ansi_c_internal_additions(std::string &code, bool support_float16_type)
     "typedef __typeof__(sizeof(int)) " CPROVER_PREFIX "size_t;\n"
     "typedef "+c_type_as_string(signed_size_type().get(ID_C_c_type))+
       " " CPROVER_PREFIX "ssize_t;\n"
-    "const unsigned " CPROVER_PREFIX "constant_infinity_uint;\n"
     "typedef void " CPROVER_PREFIX "integer;\n"
     "typedef void " CPROVER_PREFIX "rational;\n"
     "extern unsigned char " CPROVER_PREFIX "memory["
-      CPROVER_PREFIX "constant_infinity_uint];\n"
+      "(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];\n"
 
     // malloc
     "const void *" CPROVER_PREFIX "deallocated=0;\n"
@@ -169,13 +168,13 @@ void ansi_c_internal_additions(std::string &code, bool support_float16_type)
   code+=
     // this is ANSI-C
     "extern " CPROVER_PREFIX "thread_local const char __func__["
-      CPROVER_PREFIX "constant_infinity_uint];\n"
+      "(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];\n"
 
     // this is GCC
     "extern " CPROVER_PREFIX "thread_local const char __FUNCTION__["
-      CPROVER_PREFIX "constant_infinity_uint];\n"
+      "(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];\n"
     "extern " CPROVER_PREFIX "thread_local const char __PRETTY_FUNCTION__["
-      CPROVER_PREFIX "constant_infinity_uint];\n"
+      "(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];\n"
 
     // float stuff
     "int " CPROVER_PREFIX "thread_local " +

src/ansi-c/c_typecheck_expr.cpp

@@ -178,10 +178,6 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
     typecheck_expr_side_effect(to_side_effect_expr(expr));
   else if(expr.is_constant())
     typecheck_expr_constant(expr);
-  else if(expr.id()==ID_infinity)
-  {
-    // ignore
-  }
   else if(expr.id()==ID_symbol)
     typecheck_expr_symbol(expr);
   else if(expr.id()==ID_unary_plus ||
@@ -885,13 +881,6 @@ void c_typecheck_baset::typecheck_expr_symbol(exprt &expr)
     // preserve location
     expr.add_source_location()=source_location;
   }
-  else if(identifier.starts_with(CPROVER_PREFIX "constant_infinity"))
-  {
-    expr=infinity_exprt(symbol.type);
-
-    // put it back
-    expr.add_source_location()=source_location;
-  }
   else if(identifier=="__func__" ||
           identifier=="__FUNCTION__" ||
           identifier=="__PRETTY_FUNCTION__")
@@ -4637,9 +4626,6 @@ class is_compile_time_constantt
   /// "constants"
   bool is_constant(const exprt &e) const
   {
-    if(e.id() == ID_infinity)
-      return true;
-
     if(e.is_constant())
       return true;
 

src/ansi-c/c_typecheck_initializer.cpp

@@ -223,10 +223,6 @@ exprt c_typecheck_baset::do_initializer_rec(
 
 void c_typecheck_baset::do_initializer(symbolt &symbol)
 {
-  // this one doesn't need initialization
-  if(symbol.name.starts_with(CPROVER_PREFIX "constant_infinity"))
-    return;
-
   if(symbol.is_type)
     return;
 

src/ansi-c/c_typecheck_type.cpp

@@ -581,10 +581,6 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
 
       size=tmp_size;
     }
-    else if(tmp_size.id()==ID_infinity)
-    {
-      size=tmp_size;
-    }
     else if(tmp_size.id()==ID_symbol &&
             tmp_size.type().get_bool(ID_C_constant))
     {

src/ansi-c/expr2c.cpp

@@ -4110,7 +4110,6 @@ std::optional<std::string> expr2ct::convert_function(const exprt &src)
     {ID_get_must, CPROVER_PREFIX "get_must"},
     {ID_ieee_float_equal, "IEEE_FLOAT_EQUAL"},
     {ID_ieee_float_notequal, "IEEE_FLOAT_NOTEQUAL"},
-    {ID_infinity, "INFINITY"},
     {ID_is_dynamic_object, "IS_DYNAMIC_OBJECT"},
     {ID_is_invalid_pointer, "IS_INVALID_POINTER"},
     {ID_is_invalid_pointer, CPROVER_PREFIX "is_invalid_pointer"},

src/ansi-c/goto-conversion/goto_check_c.cpp

@@ -1680,9 +1680,6 @@ void goto_check_ct::bounds_check_index(
     // Linking didn't complete, we don't have a size.
     // Not clear what to do.
   }
-  else if(size.id() == ID_infinity)
-  {
-  }
   else if(
     expr.array().id() == ID_member &&
     (size.is_zero() || array_type.get_bool(ID_C_flexible_array_member)))

src/ansi-c/library/cprover.h

@@ -18,8 +18,6 @@ typedef __typeof__(sizeof(int)) __CPROVER_size_t;
 // NOLINTNEXTLINE(readability/identifiers)
 typedef signed long long __CPROVER_ssize_t;
 
-#define __CPROVER_constant_infinity_uint 1
-
 void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
 void __CPROVER_deallocate(void *);
 extern const void *__CPROVER_deallocated;

src/ansi-c/library/pthread_lib.c

@@ -291,15 +291,16 @@ int pthread_mutex_destroy(pthread_mutex_t *mutex)
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
+__CPROVER_bool __CPROVER_threads_exited
+  [(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
 __CPROVER_thread_local unsigned long __CPROVER_thread_id = 0;
 #if 0
   // Destructor support is disabled as it is too expensive due to its extensive
   // use of shared variables.
 __CPROVER_thread_local const void
-  *__CPROVER_thread_keys[__CPROVER_constant_infinity_uint];
+  *__CPROVER_thread_keys[(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
 __CPROVER_thread_local void (
-  *__CPROVER_thread_key_dtors[__CPROVER_constant_infinity_uint])(void *);
+  *__CPROVER_thread_key_dtors[(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)])(void *);
 __CPROVER_thread_local unsigned long __CPROVER_next_thread_key = 0;
 #endif
 
@@ -337,7 +338,8 @@ void pthread_exit(void *value_ptr)
 #define __CPROVER_ERRNO_H_INCLUDED
 #endif
 
-__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
+__CPROVER_bool __CPROVER_threads_exited
+  [(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
 #ifndef LIBRARY_CHECK
 __CPROVER_thread_local unsigned long __CPROVER_thread_id = 0;
 #endif
@@ -376,7 +378,8 @@ __CPROVER_HIDE:;
 #endif
 
 #ifdef __APPLE__
-__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
+__CPROVER_bool __CPROVER_threads_exited
+  [(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
 #  ifndef LIBRARY_CHECK
 __CPROVER_thread_local unsigned long __CPROVER_thread_id = 0;
 unsigned long __CPROVER_next_thread_id = 0;
@@ -544,17 +547,18 @@ int pthread_rwlock_wrlock(pthread_rwlock_t *lock)
 
 /* FUNCTION: __spawned_thread */
 
-__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
+__CPROVER_bool __CPROVER_threads_exited
+  [(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
 #ifndef LIBRARY_CHECK
 __CPROVER_thread_local unsigned long __CPROVER_thread_id = 0;
 #endif
 #if 0
   // Destructor support is disabled as it is too expensive due to its extensive
   // use of shared variables.
 __CPROVER_thread_local const void
-  *__CPROVER_thread_keys[__CPROVER_constant_infinity_uint];
+  *__CPROVER_thread_keys[(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
 __CPROVER_thread_local void (
-  *__CPROVER_thread_key_dtors[__CPROVER_constant_infinity_uint])(void *);
+  *__CPROVER_thread_key_dtors[(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)])(void *);
 #endif
 __CPROVER_thread_local unsigned long __CPROVER_next_thread_key = 0;
 
@@ -618,7 +622,7 @@ __CPROVER_HIDE:;
 unsigned long __CPROVER_next_thread_id = 0;
 #  if 0
 __CPROVER_thread_local void (
-  *__CPROVER_thread_key_dtors[__CPROVER_constant_infinity_uint])(void *);
+  *__CPROVER_thread_key_dtors[(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)])(void *);
 #  endif
 __CPROVER_thread_local unsigned long __CPROVER_next_thread_key = 0;
 #endif
@@ -952,12 +956,12 @@ int pthread_barrier_wait(pthread_barrier_t *barrier)
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-__CPROVER_thread_local const void
-  *__CPROVER_thread_keys[__CPROVER_constant_infinity_uint];
+__CPROVER_thread_local const void *__CPROVER_thread_keys
+  [(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 1 - sizeof(void *))];
 #ifndef LIBRARY_CHECK
 #  if 0
 __CPROVER_thread_local void (
-  *__CPROVER_thread_key_dtors[__CPROVER_constant_infinity_uint])(void *);
+  *__CPROVER_thread_key_dtors[(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)])(void *);
 #  endif
 __CPROVER_thread_local unsigned long __CPROVER_next_thread_key = 0;
 #endif
@@ -984,8 +988,8 @@ __CPROVER_HIDE:;
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-__CPROVER_thread_local const void
-  *__CPROVER_thread_keys[__CPROVER_constant_infinity_uint];
+__CPROVER_thread_local const void *__CPROVER_thread_keys
+  [(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 1 - sizeof(void *))];
 
 int pthread_key_delete(pthread_key_t key)
 {
@@ -1001,8 +1005,8 @@ __CPROVER_HIDE:;
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-__CPROVER_thread_local const void
-  *__CPROVER_thread_keys[__CPROVER_constant_infinity_uint];
+__CPROVER_thread_local const void *__CPROVER_thread_keys
+  [(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 1 - sizeof(void *))];
 
 void *pthread_getspecific(pthread_key_t key)
 {
@@ -1017,8 +1021,8 @@ __CPROVER_HIDE:;
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-__CPROVER_thread_local const void
-  *__CPROVER_thread_keys[__CPROVER_constant_infinity_uint];
+__CPROVER_thread_local const void *__CPROVER_thread_keys
+  [(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 1 - sizeof(void *))];
 
 int pthread_setspecific(pthread_key_t key, const void *value)
 {