diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index 7a3f10d403f..a072a41560a 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/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", diff --git a/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp index 34bcecc285f..08e8512ea47 100644 --- a/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp +++ b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp @@ -40,13 +40,13 @@ 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 { @@ -54,7 +54,7 @@ class tt } array_typet witness_type() const { - return array_typet(length_type(), infinity_exprt(length_type())); + return array_typet(length_type(), length_type().largest_expr()); } }; diff --git a/jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp b/jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp index 44464c46b2d..9be7e93d268 100644 --- a/jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp +++ b/jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp @@ -21,7 +21,7 @@ Author: Diffblue Ltd. #include #endif -typet length_type() +signedbv_typet length_type() { return signedbv_typet(32); } @@ -29,7 +29,7 @@ typet length_type() /// 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)}}); diff --git a/regression/cbmc-concurrency/thread_chain_cbmc1/main.c b/regression/cbmc-concurrency/thread_chain_cbmc1/main.c index ed0471a5b18..ea6ac3475a0 100644 --- a/regression/cbmc-concurrency/thread_chain_cbmc1/main.c +++ b/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. diff --git a/regression/cbmc-concurrency/thread_chain_cbmc2/main.c b/regression/cbmc-concurrency/thread_chain_cbmc2/main.c index ed0471a5b18..ea6ac3475a0 100644 --- a/regression/cbmc-concurrency/thread_chain_cbmc2/main.c +++ b/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. diff --git a/regression/cbmc-cpp/Vector1/lib/list b/regression/cbmc-cpp/Vector1/lib/list index 0a94dd9740b..d3b06603972 100644 --- a/regression/cbmc-cpp/Vector1/lib/list +++ b/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)]; }; } diff --git a/regression/cbmc-cpp/Vector1/lib/vector b/regression/cbmc-cpp/Vector1/lib/vector index c43a00f0d24..fa7acda6fec 100644 --- a/regression/cbmc-cpp/Vector1/lib/vector +++ b/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)]; }; } diff --git a/regression/cbmc-cpp/initialization5/main.cpp b/regression/cbmc-cpp/initialization5/main.cpp index 3c5bf63f7cd..88970679da5 100644 --- a/regression/cbmc-cpp/initialization5/main.cpp +++ b/regression/cbmc-cpp/initialization5/main.cpp @@ -1,9 +1,9 @@ #include -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; diff --git a/regression/cbmc/Unbounded_Array5/main.c b/regression/cbmc/Unbounded_Array5/main.c index 783bf7cd9ba..edca61d1b98 100644 --- a/regression/cbmc/Unbounded_Array5/main.c +++ b/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() { diff --git a/regression/cbmc/array_of_bool_as_bitvec/main.c b/regression/cbmc/array_of_bool_as_bitvec/main.c index e509f41d7c1..1ad1e309f6d 100644 --- a/regression/cbmc/array_of_bool_as_bitvec/main.c +++ b/regression/cbmc/array_of_bool_as_bitvec/main.c @@ -3,7 +3,7 @@ #include __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() { diff --git a/regression/contracts/is_unique_01_replace/main.c b/regression/contracts/is_unique_01_replace/main.c index b81f917e90c..7cae7206e21 100644 --- a/regression/contracts/is_unique_01_replace/main.c +++ b/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); diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 915aa6b58d6..0de6fa16e06 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/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 " + diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 35bc45cb257..c48e222d726 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/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; diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp index e17d59966c7..f7dc63df22d 100644 --- a/src/ansi-c/c_typecheck_initializer.cpp +++ b/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; diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 02e50709308..f3eac0a8521 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/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)) { diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 07003ead306..253d1fa6bc4 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -4110,7 +4110,6 @@ std::optional 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"}, diff --git a/src/ansi-c/goto-conversion/goto_check_c.cpp b/src/ansi-c/goto-conversion/goto_check_c.cpp index f829ebeda7e..c6c870c1356 100644 --- a/src/ansi-c/goto-conversion/goto_check_c.cpp +++ b/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))) diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h index 7e3b5693d25..3fee04b3253 100644 --- a/src/ansi-c/library/cprover.h +++ b/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; diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c index 87a60a463a4..fd5fa366db4 100644 --- a/src/ansi-c/library/pthread_lib.c +++ b/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,7 +547,8 @@ 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 @@ -552,9 +556,9 @@ __CPROVER_thread_local unsigned long __CPROVER_thread_id = 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) { diff --git a/src/ansi-c/library/unistd.c b/src/ansi-c/library/unistd.c index f9f26267b8b..f09b665eafc 100644 --- a/src/ansi-c/library/unistd.c +++ b/src/ansi-c/library/unistd.c @@ -80,7 +80,9 @@ int unlink(const char *s) #define __CPROVER_ERRNO_H_INCLUDED #endif -extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint]; +extern struct __CPROVER_pipet __CPROVER_pipes + [(__CPROVER_size_t)1 + << (sizeof(__CPROVER_size_t) * 8 - 1 - sizeof(struct __CPROVER_pipet))]; // offset to make sure we don't collide with other fds extern const int __CPROVER_pipe_offset; unsigned __CPROVER_pipe_count = 0; @@ -132,7 +134,9 @@ __CPROVER_HIDE:; /* FUNCTION: close */ -extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint]; +extern struct __CPROVER_pipet __CPROVER_pipes + [(__CPROVER_size_t)1 + << (sizeof(__CPROVER_size_t) * 8 - 1 - sizeof(struct __CPROVER_pipet))]; // offset to make sure we don't collide with other fds extern const int __CPROVER_pipe_offset; @@ -186,7 +190,9 @@ int _close(int fildes) #define size_type size_t #endif -extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint]; +extern struct __CPROVER_pipet __CPROVER_pipes + [(__CPROVER_size_t)1 + << (sizeof(__CPROVER_size_t) * 8 - 1 - sizeof(struct __CPROVER_pipet))]; // offset to make sure we don't collide with other fds extern const int __CPROVER_pipe_offset; @@ -264,7 +270,9 @@ ret_type _write(int fildes, const void *buf, size_type nbyte) #define size_type size_t #endif -extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint]; +extern struct __CPROVER_pipet __CPROVER_pipes + [(__CPROVER_size_t)1 + << (sizeof(__CPROVER_size_t) * 8 - 1 - sizeof(struct __CPROVER_pipet))]; // offset to make sure we don't collide with other fds extern const int __CPROVER_pipe_offset; diff --git a/src/cpp/cpp_constructor.cpp b/src/cpp/cpp_constructor.cpp index b10f5cdfe55..c4c24553ffa 100644 --- a/src/cpp/cpp_constructor.cpp +++ b/src/cpp/cpp_constructor.cpp @@ -57,9 +57,6 @@ std::optional cpp_typecheckt::cpp_constructor( const exprt &size_expr = to_array_type(object_tc.type()).size(); - if(size_expr.id() == ID_infinity) - return {}; // don't initialize - exprt tmp_size=size_expr; make_constant_index(tmp_size); diff --git a/src/cpp/cpp_destructor.cpp b/src/cpp/cpp_destructor.cpp index a03364ccb0e..df5fed9a4f9 100644 --- a/src/cpp/cpp_destructor.cpp +++ b/src/cpp/cpp_destructor.cpp @@ -32,9 +32,6 @@ std::optional cpp_typecheckt::cpp_destructor( { const exprt &size_expr = to_array_type(object.type()).size(); - if(size_expr.id() == ID_infinity) - return {}; // don't initialize - exprt tmp_size=size_expr; make_constant_index(tmp_size); diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp index 4c7992282e6..effe2b68581 100644 --- a/src/cpp/cpp_internal_additions.cpp +++ b/src/cpp/cpp_internal_additions.cpp @@ -64,7 +64,6 @@ void cpp_internal_additions(std::ostream &out) out << "extern \"C\" {" << '\n'; // CPROVER extensions - out << "const unsigned __CPROVER::constant_infinity_uint;" << '\n'; out << "typedef void " CPROVER_PREFIX "integer;" << '\n'; out << "typedef void " CPROVER_PREFIX "rational;" << '\n'; diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp index 79709e447a2..eeddc47aefb 100644 --- a/src/cpp/cpp_typecheck_constructor.cpp +++ b/src/cpp/cpp_typecheck_constructor.cpp @@ -383,14 +383,6 @@ void cpp_typecheckt::default_assignop_value( { const exprt &size_expr = to_array_type(c.type()).size(); - if(size_expr.id()==ID_infinity) - { - // error().source_location=object); - // err << "cannot copy array of infinite size\n"; - // throw 0; - continue; - } - const auto size = numeric_cast(size_expr); CHECK_RETURN(!size.has_value()); CHECK_RETURN(*size >= 0); diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp index 3eb9d8ac8c6..305bc56b9a1 100644 --- a/src/cpp/cpp_typecheck_initializer.cpp +++ b/src/cpp/cpp_typecheck_initializer.cpp @@ -233,9 +233,6 @@ void cpp_typecheckt::zero_initializer( const array_typet &array_type=to_array_type(type); const exprt &size_expr=array_type.size(); - if(size_expr.id()==ID_infinity) - return; // don't initialize - const mp_integer size = numeric_cast_v(to_constant_expr(size_expr)); CHECK_RETURN(size>=0); diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index e555353ed55..b75f074629f 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -821,11 +821,6 @@ exprt cpp_typecheck_resolvet::do_builtin( dest=type_exprt(typet(base_name)); } - else if(base_name.starts_with("constant_infinity")) - { - // ok, but type missing - dest=exprt(ID_infinity, size_type()); - } else if(base_name=="dump_scopes") { dest=exprt(ID_constant, typet(ID_empty)); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp index 242b330b4d3..22f3623c871 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp @@ -520,8 +520,7 @@ const symbolt &dfcc_libraryt::get_instrumented_functions_map_symbol() if(goto_model.symbol_table.has_symbol(map_name)) return goto_model.symbol_table.lookup_ref(map_name); - auto map_type = - array_typet(unsigned_char_type(), infinity_exprt(size_type())); + auto map_type = array_typet(unsigned_char_type(), size_type().largest_expr()); return dfcc_utilst::create_static_symbol( goto_model.symbol_table, diff --git a/src/goto-instrument/contracts/memory_predicates.cpp b/src/goto-instrument/contracts/memory_predicates.cpp index c0d2dbe5ce6..ab1968b819d 100644 --- a/src/goto-instrument/contracts/memory_predicates.cpp +++ b/src/goto-instrument/contracts/memory_predicates.cpp @@ -138,7 +138,7 @@ void is_fresh_baset::update_ensures(goto_programt &ensures) array_typet is_fresh_baset::get_memmap_type() { - return array_typet(unsigned_char_type(), infinity_exprt(size_type())); + return array_typet(unsigned_char_type(), size_type().largest_expr()); } void is_fresh_baset::add_memory_map_decl(goto_programt &program) diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index 3104f1d9de8..d40ab373bd5 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -554,15 +554,7 @@ exprt interpretert::get_value( // Get size of array mp_integer subtype_size = get_size(to_array_type(type).element_type()); - mp_integer count; - if(unbounded_size(type)) - { - count=base_address_to_actual_size(offset)/subtype_size; - } - else - { - count = numeric_cast_v(to_constant_expr(size_expr)); - } + mp_integer count = numeric_cast_v(to_constant_expr(size_expr)); // Retrieve the value for each member in the array result.reserve_operands(numeric_cast_v(count)); @@ -937,34 +929,12 @@ mp_integer interpretert::build_memory_map(const symbol_exprt &symbol_expr) return address; } -bool interpretert::unbounded_size(const typet &type) -{ - if(type.id()==ID_array) - { - const exprt &size=to_array_type(type).size(); - if(size.id()==ID_infinity) - return true; - return unbounded_size(to_array_type(type).element_type()); - } - else if(type.id()==ID_struct) - { - const auto &st=to_struct_type(type); - if(st.components().empty()) - return false; - return unbounded_size(st.components().back().type()); - } - return false; -} - /// Retrieves the actual size of the provided structured type. Unbounded objects /// get allocated 2^(platform bit-width / 2 + 1) address space each. /// \param type: a structured type /// \return Size of the given type mp_integer interpretert::get_size(const typet &type) { - if(unbounded_size(type)) - return mp_integer(2) << (sizeof(std::size_t) * CHAR_BIT / 2); - if(type.id()==ID_struct) { const struct_typet::componentst &components= diff --git a/src/goto-programs/interpreter_class.h b/src/goto-programs/interpreter_class.h index e873546db7a..a0984313e76 100644 --- a/src/goto-programs/interpreter_class.h +++ b/src/goto-programs/interpreter_class.h @@ -195,7 +195,6 @@ class interpretert void build_memory_map(const symbolt &symbol); mp_integer build_memory_map(const symbol_exprt &symbol_expr); typet concretize_type(const typet &type); - bool unbounded_size(const typet &); mp_integer get_size(const typet &type); struct_typet::componentt diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index cdb413e351e..30e89dc5d84 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -401,9 +401,7 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr) else if(expr.id()==ID_struct) { mp_vectort dest; - - if(!unbounded_size(expr.type())) - dest.reserve(numeric_cast_v(get_size(expr.type()))); + dest.reserve(numeric_cast_v(get_size(expr.type()))); bool error=false; @@ -418,7 +416,7 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr) mp_vectort tmp = evaluate(op); - if(unbounded_size(op.type()) || tmp.size() == sub_size) + if(tmp.size() == sub_size) { for(std::size_t i=0; i(get_size(expr.type()))); read(address, dest); return dest; } - else - { - mp_vectort dest; - read_unbounded(address, dest); - return dest; - } } } else if(expr.id()==ID_typecast) @@ -928,11 +920,7 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr) { const auto &ty=to_array_type(expr.type()); - mp_vectort size; - if(ty.size().id()==ID_infinity) - size.push_back(0); - else - size = evaluate(ty.size()); + mp_vectort size = evaluate(ty.size()); if(size.size()==1) { @@ -954,7 +942,7 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr) const auto &subtype = to_array_type(expr.type()).element_type(); - if(!new_value.empty() && where.size()==1 && !unbounded_size(subtype)) + if(!new_value.empty() && where.size() == 1) { // Ignore indices < 0, which the string solver sometimes produces if(where[0]<0) @@ -978,14 +966,6 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr) { return {0}; } - else if(expr.id()==ID_infinity) - { - if(expr.type().id()==ID_signedbv) - { - output.warning() << "Infinite size arrays not supported" << messaget::eom; - return {}; - } - } output.error() << "!! failed to evaluate expression: " << from_expr(ns, function->first, expr) << "\n" << expr.id() << "[" << expr.type().id() << "]" diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index 5a00c5a7efb..04847ea4deb 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -436,10 +436,8 @@ symbol_exprt string_abstractiont::add_dummy_symbol_and_value( new_symbol.value = struct_exprt( {build_unknown(whatt::IS_ZERO, false), build_unknown(whatt::LENGTH, false), - to_array_type(source_type).size().id() == ID_infinity - ? build_unknown(whatt::SIZE, false) - : typecast_exprt::conditional_cast( - to_array_type(source_type).size(), build_type(whatt::SIZE))}, + typecast_exprt::conditional_cast( + to_array_type(source_type).size(), build_type(whatt::SIZE))}, string_struct); } else diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp index 336c848d7dd..37848644ff0 100644 --- a/src/linking/static_lifetime_init.cpp +++ b/src/linking/static_lifetime_init.cpp @@ -37,7 +37,6 @@ static std::optional static_lifetime_init( // special values if( - identifier == CPROVER_PREFIX "constant_infinity_uint" || identifier == CPROVER_PREFIX "memory" || identifier == "__func__" || identifier == "__FUNCTION__" || identifier == "__PRETTY_FUNCTION__" || identifier == "argc'" || identifier == "argv'" || identifier == "envp'" || diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index 451436e04a0..18c00aac9ef 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -1534,7 +1534,7 @@ void smt2_parsert::setup_sorts() // we can turn arrays that map an unsigned bitvector type // to something else into our 'array_typet' if(domain.id() == ID_unsignedbv) - return array_typet(range, infinity_exprt(domain)); + return array_typet(range, to_unsignedbv_type(domain).largest_expr()); else throw error("unsupported array sort"); }; diff --git a/src/solvers/strings/array_pool.cpp b/src/solvers/strings/array_pool.cpp index 4b88e8fad56..6c6b60e16b0 100644 --- a/src/solvers/strings/array_pool.cpp +++ b/src/solvers/strings/array_pool.cpp @@ -56,7 +56,8 @@ array_poolt::get_length_if_exists(const array_string_exprt &s) const array_string_exprt array_poolt::fresh_string(const typet &index_type, const typet &char_type) { - array_typet array_type{char_type, infinity_exprt(index_type)}; + array_typet array_type{ + char_type, to_integer_bitvector_type(index_type).largest_expr()}; symbol_exprt content = fresh_symbol("string_content", array_type); array_string_exprt str = to_array_string_expr(content); arrays_of_pointers.emplace( @@ -144,10 +145,7 @@ static void attempt_assign_length_from_type( // If we find a case where this is violated, try calling // attempt_assign_length_from_type on the true and false cases. const exprt &size_from_type = to_array_type(array_expr.type()).size(); - const exprt &size_to_assign = - size_from_type != infinity_exprt(size_from_type.type()) - ? size_from_type - : symbol_generator("string_length", array_expr.length_type()); + const exprt &size_to_assign = size_from_type; const auto emplace_result = length_of_array.emplace(array_expr, size_to_assign); diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp index e1980bed5f4..dd93e28447f 100644 --- a/src/solvers/strings/string_refinement.cpp +++ b/src/solvers/strings/string_refinement.cpp @@ -768,7 +768,8 @@ string_refinementt::dec_solve(const exprt &assumption) const auto &witness_type = [&] { const auto &rtype = to_array_type(nc_axiom.s0.type()); const typet &index_type = rtype.size().type(); - return array_typet(index_type, infinity_exprt(index_type)); + return array_typet( + index_type, to_integer_bitvector_type(index_type).largest_expr()); }(); not_contain_witnesses.emplace( nc_axiom, generator.fresh_symbol("not_contains_witness", witness_type)); @@ -1800,7 +1801,8 @@ exprt substitute_array_lists(exprt expr, size_t string_max_length) string_refinement_invariantt("array-lists must have at least two " "operands")); const typet &char_type = expr.operands()[1].type(); - array_typet arr_type(char_type, infinity_exprt(char_type)); + array_typet arr_type( + char_type, to_integer_bitvector_type(char_type).largest_expr()); exprt ret_expr = array_of_exprt(from_integer(0, char_type), arr_type); for(size_t i = 0; i < expr.operands().size(); i += 2) diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp index 3525b2804e1..ed7230839c2 100644 --- a/src/util/expr_initializer.cpp +++ b/src/util/expr_initializer.cpp @@ -148,9 +148,7 @@ std::optional expr_initializert::expr_initializer_rec( return {}; const auto array_size = numeric_cast(array_type.size()); - if( - array_type.size().id() == ID_infinity || !array_size.has_value() || - *array_size > MAX_FLATTENED_ARRAY_SIZE) + if(!array_size.has_value() || *array_size > MAX_FLATTENED_ARRAY_SIZE) { if(init_expr.id() == ID_nondet) return side_effect_expr_nondett(type, source_location); diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index f1728411191..87664e702b9 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -251,7 +251,6 @@ IREP_ID_ONE(rol) IREP_ID_ONE(ror) IREP_ID_ONE(comma) IREP_ID_ONE(concatenation) -IREP_ID_ONE(infinity) IREP_ID_ONE(return_type) IREP_ID_ONE(typedef) IREP_ID_ONE(typedef_type) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index af6f3c55186..9904efa8596 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -759,15 +759,6 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr) const typet &expr_type = expr.type(); const typet &op_type = expr.op().type(); - // eliminate casts of infinity - if(expr.op().id() == ID_infinity) - { - typet new_type=expr.type(); - exprt tmp = expr.op(); - tmp.type()=new_type; - return std::move(tmp); - } - // casts from NULL to any integer if( op_type.id() == ID_pointer && expr.op().is_constant() && diff --git a/src/util/std_expr.h b/src/util/std_expr.h index d9ca4f64bab..c6436a51e27 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -3092,16 +3092,6 @@ inline bool can_cast_expr(const exprt &base) return base.id() == ID_nil; } -/// \brief An expression denoting infinity -class infinity_exprt : public nullary_exprt -{ -public: - explicit infinity_exprt(typet _type) - : nullary_exprt(ID_infinity, std::move(_type)) - { - } -}; - /// \brief A base class for variable bindings (quantifiers, let, lambda) class binding_exprt : public binary_exprt { diff --git a/unit/solvers/strings/string_refinement/concretize_array.cpp b/unit/solvers/strings/string_refinement/concretize_array.cpp index 516edffdd3c..ba959b077b6 100644 --- a/unit/solvers/strings/string_refinement/concretize_array.cpp +++ b/unit/solvers/strings/string_refinement/concretize_array.cpp @@ -20,7 +20,7 @@ SCENARIO( { // Arrange const typet char_type = unsignedbv_typet(16); - const typet int_type = signedbv_typet(32); + const auto int_type = signedbv_typet(32); const exprt index1 = from_integer(1, int_type); const exprt charx = from_integer('x', char_type); const exprt index4 = from_integer(4, int_type); @@ -29,7 +29,7 @@ SCENARIO( const exprt char0 = from_integer('0', char_type); const exprt index2 = from_integer(2, int_type); const exprt charz = from_integer('z', char_type); - array_typet array_type(char_type, infinity_exprt(int_type)); + array_typet array_type(char_type, int_type.largest_expr()); // input_expr is // ARRAY_OF(0) WITH [1:=x] WITH [4:=y] WITH [100:=z]` diff --git a/unit/solvers/strings/string_refinement/sparse_array.cpp b/unit/solvers/strings/string_refinement/sparse_array.cpp index 8a265aba4a1..a3942f84428 100644 --- a/unit/solvers/strings/string_refinement/sparse_array.cpp +++ b/unit/solvers/strings/string_refinement/sparse_array.cpp @@ -19,7 +19,7 @@ SCENARIO("sparse_array", "[core][solvers][strings][string_refinement]") GIVEN("`ARRAY_OF(0) WITH [4:=x] WITH [1:=y] WITH [100:=z]`") { const typet char_type = unsignedbv_typet(16); - const typet int_type = signedbv_typet(32); + const auto int_type = signedbv_typet(32); const exprt index1 = from_integer(1, int_type); const exprt charx = from_integer('x', char_type); const exprt index4 = from_integer(4, int_type); @@ -28,7 +28,7 @@ SCENARIO("sparse_array", "[core][solvers][strings][string_refinement]") const exprt char0 = from_integer('0', char_type); const exprt index2 = from_integer(2, int_type); const exprt charz = from_integer('z', char_type); - const array_typet array_type(char_type, infinity_exprt(int_type)); + const array_typet array_type(char_type, int_type.largest_expr()); const with_exprt input_expr( with_exprt( diff --git a/unit/solvers/strings/string_refinement/string_refinement.cpp b/unit/solvers/strings/string_refinement/string_refinement.cpp index d86abcec0e5..b062057da2c 100644 --- a/unit/solvers/strings/string_refinement/string_refinement.cpp +++ b/unit/solvers/strings/string_refinement/string_refinement.cpp @@ -40,7 +40,7 @@ SCENARIO("string refinement", "[core][solvers][strings][string_refinement]") { const signedbv_typet int_type{64}; const unsignedbv_typet char_type{16}; - const array_typet char_array_type{char_type, infinity_exprt{int_type}}; + const array_typet char_array_type{char_type, int_type.largest_expr()}; const refined_string_typet string_type{int_type, pointer_type(char_type)}; const symbol_exprt array1{"array1", char_array_type}; const symbol_exprt pointer1{"pointer1", pointer_type(char_type)}; diff --git a/unit/solvers/strings/string_refinement/substitute_array_list.cpp b/unit/solvers/strings/string_refinement/substitute_array_list.cpp index b66e17a54fc..15bbc838ad5 100644 --- a/unit/solvers/strings/string_refinement/substitute_array_list.cpp +++ b/unit/solvers/strings/string_refinement/substitute_array_list.cpp @@ -16,8 +16,8 @@ Author: Diffblue Ltd. SCENARIO("substitute_array_list", "[core][solvers][strings][string_refinement]") { const typet char_type = unsignedbv_typet(16); - const typet int_type = signedbv_typet(32); - const array_typet array_type(char_type, infinity_exprt(int_type)); + const auto int_type = signedbv_typet(32); + const array_typet array_type(char_type, int_type.largest_expr()); const exprt index0 = from_integer(0, int_type); const exprt charx = from_integer('x', char_type); const exprt index1 = from_integer(1, int_type); diff --git a/unit/util/lower_byte_operators.cpp b/unit/util/lower_byte_operators.cpp index 4f3ac9ba9be..bbc7e70c761 100644 --- a/unit/util/lower_byte_operators.cpp +++ b/unit/util/lower_byte_operators.cpp @@ -99,7 +99,7 @@ SCENARIO("byte_extract_lowering", "[core][util][lowering][byte_extract]") cmdlinet cmdline; config.set(cmdline); - const symbol_tablet symbol_table; + symbol_tablet symbol_table; const namespacet ns(symbol_table); GIVEN("A byte_extract over a POD") @@ -135,6 +135,8 @@ SCENARIO("byte_extract_lowering", "[core][util][lowering][byte_extract]") GIVEN("A an unbounded byte_extract over a bounded operand") { const exprt deadbeef = from_integer(0xdeadbeef, unsignedbv_typet(32)); + symbolt array_size{"some_size", size_type(), ID_C}; + symbol_table.insert(array_size); const byte_extract_exprt be1( ID_byte_extract_little_endian, deadbeef, @@ -142,8 +144,7 @@ SCENARIO("byte_extract_lowering", "[core][util][lowering][byte_extract]") config.ansi_c.char_width, struct_typet( {{"unbounded_array", - array_typet( - unsignedbv_typet(16), exprt(ID_infinity, size_type()))}})); + array_typet(unsignedbv_typet(16), array_size.symbol_expr())}})); THEN("byte_extract lowering does not raise an exception") { @@ -164,6 +165,8 @@ SCENARIO("byte_extract_lowering", "[core][util][lowering][byte_extract]") GIVEN("A an unbounded union byte_extract over a bounded operand") { const exprt deadbeef = from_integer(0xdeadbeef, unsignedbv_typet(32)); + symbolt array_size{"some_size2", size_type(), ID_C}; + symbol_table.insert(array_size); const byte_extract_exprt be1( ID_byte_extract_little_endian, deadbeef, @@ -171,8 +174,7 @@ SCENARIO("byte_extract_lowering", "[core][util][lowering][byte_extract]") config.ansi_c.char_width, union_typet( {{"unbounded_array", - array_typet( - unsignedbv_typet(16), exprt(ID_infinity, size_type()))}})); + array_typet(unsignedbv_typet(16), array_size.symbol_expr())}})); THEN("byte_extract lowering does not raise an exception") {