Permit re-setting --object-bits and malloc failure mode

Support choosing the number of object bits to be used by CBMC at runtime
even with pre-compiled goto binaries. Equally, permit re-setting the
malloc failure mode via --malloc-may-fail.

Fixes: #5443

Author: tautschnig

doc/man/goto-cc.1

@@ -96,9 +96,6 @@ files.
 .TP
 \fB\-\-print\-rejected\-preprocessed\-source\fR \fIfile\fR
 Copy failing (preprocessed) source to \fIfile\fR.
-.TP
-\fB\-\-object\-bits\fR \fIN\fR
-Configure the number of bits used for object numbering in CBMC's pointer encoding.
 .SH ENVIRONMENT
 All tools honor the TMPDIR environment variable when generating temporary
 files and directories.

regression/CMakeLists.txt

@@ -63,7 +63,6 @@ else()
   add_subdirectory(goto-cl)
 endif()
 add_subdirectory(goto-cc-cbmc)
-add_subdirectory(goto-cc-cbmc-shared-options)
 add_subdirectory(cbmc-cpp)
 add_subdirectory(goto-cc-goto-analyzer)
 add_subdirectory(goto-analyzer-simplify)

regression/Makefile

@@ -36,7 +36,6 @@ DIRS = cbmc-shadow-memory \
        goto-gcc \
        goto-cl \
        goto-cc-cbmc \
-       goto-cc-cbmc-shared-options \
        cbmc-cpp \
        goto-cc-goto-analyzer \
        goto-analyzer-simplify \

regression/cbmc/simplify_singleton_interval_7690/singleton_interval_in_assume_7690.c

@@ -5,7 +5,6 @@
 #include <stdlib.h>
 #include <stdint.h>
 
-extern size_t __CPROVER_max_malloc_size;
 int __builtin_clzll(unsigned long long);
 
 #define __nof_symex_objects                                                    \

regression/goto-cc-cbmc-shared-options/CMakeLists.txt

@@ -1,4 +1,4 @@
-CORE winbug
+CORE
 test.c
 --function main --object-bits 6
 ^EXIT=10$

regression/goto-cc-cbmc-shared-options/Makefile

@@ -1,4 +1,4 @@
-CORE winbug
+CORE
 test.c
 --function main --object-bits 10
 ^EXIT=10$

regression/goto-cc-cbmc-shared-options/README.md

@@ -130,34 +130,6 @@ static std::string architecture_string(T value, const char *s)
          std::string(s) + "=" + std::to_string(value) + ";\n";
 }
 
-/// The maximum allocation size is determined by the number of bits that
-/// are left in the pointer of width \p pointer_width.
-///
-/// The allocation size cannot exceed the number represented by the (signed)
-/// offset, otherwise it would not be possible to store a pointer into a
-/// valid bit of memory. Therefore, the max allocation size is
-/// 2^(offset_bits - 1), where the offset bits is the number of bits left in the
-/// pointer after the object bits.
-///
-/// The offset must be signed, as a pointer can point to the end of the memory
-/// block, and needs to be able to point back to the start.
-/// \param pointer_width: The width of the pointer
-/// \param object_bits : The number of bits used to represent the ID
-/// \return The size in bytes of the maximum allocation supported.
-static mp_integer
-max_malloc_size(std::size_t pointer_width, std::size_t object_bits)
-{
-  PRECONDITION(pointer_width >= 1);
-  PRECONDITION(object_bits < pointer_width);
-  PRECONDITION(object_bits >= 1);
-  const auto offset_bits = pointer_width - object_bits;
-  // We require the offset to be able to express upto allocation_size - 1,
-  // but also down to -allocation_size, therefore the size is allowable
-  // is number of bits, less the signed bit.
-  const auto bits_for_positive_offset = offset_bits - 1;
-  return ((mp_integer)1) << (mp_integer)bits_for_positive_offset;
-}
-
 void ansi_c_internal_additions(std::string &code)
 {
   // clang-format off
@@ -181,9 +153,9 @@ void ansi_c_internal_additions(std::string &code)
       CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n"
     "void " CPROVER_PREFIX "deallocate(void *);\n"
 
-    CPROVER_PREFIX "size_t " CPROVER_PREFIX "max_malloc_size="+
-    integer2string(max_malloc_size(config.ansi_c.pointer_width, config
-    .bv_encoding.object_bits))+";\n"
+    CPROVER_PREFIX "thread_local " CPROVER_PREFIX "size_t "
+      CPROVER_PREFIX "max_malloc_size="+
+      integer2string(config.max_malloc_size())+";\n"
 
     // this is ANSI-C
     "extern " CPROVER_PREFIX "thread_local const char __func__["

regression/goto-cc-cbmc-shared-options/chain.sh

@@ -24,19 +24,14 @@ static std::string get_cprover_library_text(
   std::ostringstream library_text;
 
   library_text << "#line 1 \"<built-in-additions>\"\n"
-                  "#define " CPROVER_PREFIX "malloc_failure_mode "
-               << std::to_string(config.ansi_c.malloc_failure_mode)
-               << "\n"
                   "#define " CPROVER_PREFIX "malloc_failure_mode_return_null "
                << std::to_string(config.ansi_c.malloc_failure_mode_return_null)
                << "\n"
                   "#define " CPROVER_PREFIX
                   "malloc_failure_mode_assert_then_assume "
                << std::to_string(
                     config.ansi_c.malloc_failure_mode_assert_then_assume)
-               << "\n"
-                  "#define " CPROVER_PREFIX "malloc_may_fail "
-               << std::to_string(config.ansi_c.malloc_may_fail) << "\n";
+               << "\n";
 
   library_text <<
     "#line 1 \"<builtin-library>\"\n"

regression/goto-cc-cbmc-shared-options/object-bits/default_bits.desc renamed to regression/goto-cc-cbmc/object-bits/default_bits.desc

@@ -52,4 +52,5 @@ void cprover_c_library_factory_force_load(
   const std::set<irep_idt> &functions,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler);
+
 #endif // CPROVER_ANSI_C_CPROVER_LIBRARY_H

regression/goto-cc-cbmc-shared-options/object-bits/fewer_bits.desc renamed to regression/goto-cc-cbmc/object-bits/fewer_bits.desc

@@ -25,9 +25,7 @@ void __CPROVER_deallocate(void *);
 extern const void *__CPROVER_deallocated;
 extern const void *__CPROVER_memory_leak;
 
-extern int __CPROVER_malloc_failure_mode;
-extern __CPROVER_size_t __CPROVER_max_malloc_size;
-extern __CPROVER_bool __CPROVER_malloc_may_fail;
+extern __CPROVER_thread_local __CPROVER_size_t __CPROVER_max_malloc_size;
 
 // malloc failure modes
 extern int __CPROVER_malloc_failure_mode_return_null;

regression/goto-cc-cbmc-shared-options/object-bits/more_bits.desc renamed to regression/goto-cc-cbmc/object-bits/more_bits.desc

@@ -7,12 +7,12 @@
 #define __CPROVER_contracts_library_defined
 
 // external dependencies
-extern __CPROVER_size_t __CPROVER_max_malloc_size;
 const void *__CPROVER_alloca_object = 0;
 extern const void *__CPROVER_deallocated;
 const void *__CPROVER_new_object = 0;
 extern const void *__CPROVER_memory_leak;
 __CPROVER_bool __CPROVER_malloc_is_new_array = 0;
+extern __CPROVER_thread_local int __CPROVER_malloc_failure_mode;
 int __builtin_clzll(unsigned long long);
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 __CPROVER_size_t __VERIFIER_nondet_size(void);

regression/goto-cc-cbmc-shared-options/object-bits/test.c renamed to regression/goto-cc-cbmc/object-bits/test.c

@@ -142,6 +142,8 @@ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 _Bool __builtin_mul_overflow();
 #endif
 __CPROVER_bool __CPROVER_malloc_is_new_array = 0;
+__CPROVER_thread_local int __CPROVER_malloc_failure_mode = 0;
+__CPROVER_thread_local __CPROVER_bool __CPROVER_malloc_may_fail = 0;
 
 void *calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size)
 {
@@ -205,6 +207,8 @@ __CPROVER_HIDE:;
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 #ifndef LIBRARY_CHECK
 __CPROVER_bool __CPROVER_malloc_is_new_array = 0;
+__CPROVER_thread_local int __CPROVER_malloc_failure_mode = 0;
+__CPROVER_thread_local __CPROVER_bool __CPROVER_malloc_may_fail = 0;
 #endif
 
 // malloc is marked "inline" for the benefit of goto-analyzer. Really,

src/ansi-c/ansi_c_internal_additions.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "cbmc_parse_options.h"
 
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/exit_codes.h>
 #include <util/help_formatter.h>
@@ -744,6 +745,8 @@ int cbmc_parse_optionst::get_goto_program(
 
   goto_model = initialize_goto_model(cmdline.args, ui_message_handler, options);
 
+  update_max_malloc_size(goto_model, ui_message_handler);
+
   if(cmdline.isset("show-symbol-table"))
   {
     show_symbol_table(goto_model, ui_message_handler);
@@ -830,6 +833,13 @@ bool cbmc_parse_optionst::process_goto_program(
   link_to_library(
     goto_model, log.get_message_handler(), cprover_c_library_factory);
 
+  if(
+    config.ansi_c.malloc_failure_mode !=
+    configt::ansi_ct::malloc_failure_mode_none)
+  {
+    update_malloc_configuration(goto_model, log.get_message_handler());
+  }
+
   // Common removal of types and complex constructs
   if(::process_goto_program(goto_model, options, log))
     return true;

src/ansi-c/cprover_library.cpp

@@ -29,7 +29,6 @@ const char *goto_cc_options_with_separated_argument[]=
   "--native-linker",
   "--print-rejected-preprocessed-source",
   "--mangle-suffix",
-  "--object-bits",
   nullptr
 };
 

src/ansi-c/cprover_library.h

@@ -69,7 +69,6 @@ void goto_cc_modet::help()
   " --mangle-suffix suffix      append suffix to exported file-local symbols\n"
   " --print-rejected-preprocessed-source file\n"
   "                             copy failing (preprocessed) source to file\n"
-  " --object-bits               number of bits used for object addresses\n"
   "\n";
   // clang-format on
 }

src/ansi-c/library/cprover.h

@@ -32,6 +32,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/ensure_one_backedge_per_target.h>
 #include <goto-programs/goto_check.h>
 #include <goto-programs/goto_inline.h>
+#include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/interpreter.h>
 #include <goto-programs/label_function_pointer_call_sites.h>
 #include <goto-programs/link_to_library.h>
@@ -1086,6 +1087,13 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     link_to_library(
       goto_model, ui_message_handler, cprover_cpp_library_factory);
     link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);
+
+    if(
+      config.ansi_c.malloc_failure_mode !=
+      configt::ansi_ct::malloc_failure_mode_none)
+    {
+      update_malloc_configuration(goto_model, log.get_message_handler());
+    }
   }
 
   {

src/ansi-c/library/cprover_contracts.c

@@ -11,22 +11,27 @@ Author: Daniel Kroening, [email protected]
 
 #include "initialize_goto_model.h"
 
-#include <fstream>
-
+#include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/config.h>
+#include <util/expr_util.h>
 #include <util/message.h>
 #include <util/options.h>
 
+#include <fstream>
+
 #ifdef _MSC_VER
 #  include <util/unicode.h>
 #endif
 
+#include <util/exception_utils.h>
+
+#include <goto-programs/rebuild_goto_start_function.h>
+
 #include <langapi/language.h>
 #include <langapi/language_file.h>
 #include <langapi/mode.h>
-
-#include <goto-programs/rebuild_goto_start_function.h>
-#include <util/exception_utils.h>
+#include <linking/static_lifetime_init.h>
 
 #include "goto_convert_functions.h"
 #include "read_goto_binary.h"
@@ -245,3 +250,64 @@ goto_modelt initialize_goto_model(
 
   return goto_model;
 }
+
+void update_max_malloc_size(
+  goto_modelt &goto_model,
+  message_handlert &message_handler)
+{
+  if(!goto_model.symbol_table.has_symbol(CPROVER_PREFIX "max_malloc_size"))
+    return;
+
+  const auto previous_max_malloc_size_value = numeric_cast<mp_integer>(
+    goto_model.symbol_table.lookup_ref(CPROVER_PREFIX "max_malloc_size").value);
+  const mp_integer current_max_malloc_size = config.max_malloc_size();
+
+  if(
+    !previous_max_malloc_size_value.has_value() ||
+    *previous_max_malloc_size_value != current_max_malloc_size)
+  {
+    symbolt &max_malloc_size_sym = goto_model.symbol_table.get_writeable_ref(
+      CPROVER_PREFIX "max_malloc_size");
+    max_malloc_size_sym.value =
+      from_integer(current_max_malloc_size, size_type());
+
+    if(goto_model.can_produce_function(INITIALIZE_FUNCTION))
+      recreate_initialize_function(goto_model, message_handler);
+  }
+}
+
+void update_malloc_configuration(
+  goto_modelt &goto_model,
+  message_handlert &message_handler)
+{
+  const symbolt *malloc_may_fail_ptr =
+    goto_model.symbol_table.lookup(CPROVER_PREFIX "malloc_may_fail");
+  if(!malloc_may_fail_ptr)
+    return;
+
+  bool reinit_required = false;
+  if(malloc_may_fail_ptr->value.is_true() != config.ansi_c.malloc_may_fail)
+  {
+    symbolt &malloc_may_fail_sym = goto_model.symbol_table.get_writeable_ref(
+      CPROVER_PREFIX "malloc_may_fail");
+    malloc_may_fail_sym.value =
+      make_boolean_expr(config.ansi_c.malloc_may_fail);
+    reinit_required = true;
+  }
+
+  symbolt &malloc_failure_mode_sym = goto_model.symbol_table.get_writeable_ref(
+    CPROVER_PREFIX "malloc_failure_mode");
+  const auto previous_failure_mode =
+    numeric_cast<mp_integer>(malloc_failure_mode_sym.value);
+  if(
+    !previous_failure_mode.has_value() ||
+    *previous_failure_mode != config.ansi_c.malloc_failure_mode)
+  {
+    malloc_failure_mode_sym.value =
+      from_integer(config.ansi_c.malloc_failure_mode, signed_int_type());
+    reinit_required = true;
+  }
+
+  if(reinit_required && goto_model.can_produce_function(INITIALIZE_FUNCTION))
+    recreate_initialize_function(goto_model, message_handler);
+}