Set addr_bits via command line and per language

regression/cbmc-java/address_space_size_limit1/Test.java

@@ -0,0 +1,13 @@
+public class Test {
+    int x;
+    Test(int x) { this.x = x; }
+
+    public static void main(String[] args) {
+        int i;
+        Test[] tests = new Test[30];
+        for(i = 0; i < 30; ++i) {
+            tests[i] = new Test(i);
+        }
+        assert i == tests[0].x;
+    }
+}

regression/cbmc-java/address_space_size_limit1/test.desc

@@ -0,0 +1,5 @@
+CORE
+Test.class
+--object-bits 4
+too many addressed objects
+--

regression/cbmc-java/address_space_size_limit2/Test.java

@@ -0,0 +1,13 @@
+public class Test {
+    int x;
+    Test(int x) { this.x = x; }
+
+    public static void main(String[] args) {
+        int i;
+        Test[] tests = new Test[30];
+        for(i = 0; i < 30; ++i) {
+            tests[i] = new Test(i);
+        }
+        assert i == tests[0].x;
+    }
+}

regression/cbmc-java/address_space_size_limit2/test.desc

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--object-bits 8
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\[java::Test.main:\(\[Ljava/lang/String;\)V.assertion.1\] .*: FAILURE$
+--

regression/cbmc/address_space_size_limit1/test.desc

@@ -1,5 +1,5 @@
 CORE
 test.c
---no-simplify --unwind 300
-too many variables
+--no-simplify --unwind 300 --object-bits 8
+too many addressed objects
 --

regression/cbmc/address_space_size_limit2/test.c

@@ -0,0 +1,10 @@
+#include <stdlib.h>
+#include <assert.h>
+
+int main(int argc, char** argv)
+{
+  char* c=(char*)malloc(10);
+  char* d=c;
+  for(char i=0; i<10; i++, d++);
+  assert((size_t)d==(size_t)c+10);
+}

regression/cbmc/address_space_size_limit2/test.desc

@@ -0,0 +1,5 @@
+KNOWNBUG
+test.c
+--32 --object-bits 31 --unwind 11 --no-simplify
+dynamic object too large
+--

regression/cbmc/address_space_size_limit3/main.c

@@ -0,0 +1,136 @@
+// copy of Pointer_Arithmetic12
+
+#include <stdint.h>
+
+#include <assert.h>
+
+uint32_t __stack[32];
+
+uint32_t eax;
+uint32_t ebp;
+uint32_t ebx;
+uint32_t ecx;
+uint32_t edi;
+uint32_t edx;
+uint32_t esi;
+uint32_t esp=(uint32_t)&(__stack[31]);
+uint32_t var0;
+uint32_t var1;
+uint32_t var10;
+uint32_t var11;
+uint32_t var12;
+uint32_t var13;
+uint32_t var14;
+uint32_t var15;
+uint32_t var16;
+uint32_t var2;
+uint32_t var3;
+uint32_t var4;
+uint32_t var5;
+uint32_t var6;
+uint32_t var7;
+uint32_t var8;
+uint32_t var9;
+
+void g__L_0x3b4_0()
+{
+  L_0x3b4_0: esp-=0x4;
+  L_0x3b4_1: *(uint32_t*)(esp)=ebp;
+  L_0x3b5_0: ebp=esp;
+  L_0x3b7_0: var4=ebp;
+  L_0x3b7_1: var4+=0xc;
+  L_0x3b7_2: eax=*(uint32_t*)(var4);
+  L_0x3ba_0: edx=eax;
+  L_0x3bc_0: edx&=0x3;
+  L_0x3bf_0: var5=ebp;
+  L_0x3bf_1: var5+=0x8;
+  L_0x3bf_2: eax=*(uint32_t*)(var5);
+  L_0x3c2_0: *(uint32_t*)(eax)=edx;
+  L_0x3c4_0: ebp=*(uint32_t*)(esp);
+  L_0x3c4_1: esp+=0x4;
+  L_0x3c5_0: return;
+}
+
+void f__L_0x3c6_0()
+{
+  L_0x3c6_0: esp-=0x4;
+  L_0x3c6_1: *(uint32_t*)(esp)=ebp;
+  L_0x3c7_0: ebp=esp;
+  L_0x3c9_0: esp-=0x18;
+  L_0x3cc_0: var6=ebp;
+  L_0x3cc_1: var6-=0x4;
+  L_0x3cc_2: *(uint32_t*)(var6)=0x0;
+  L_0x3d3_0: var7=ebp;
+  L_0x3d3_1: var7-=0x8;
+  L_0x3d3_2: *(uint32_t*)(var7)=0x0;
+  L_0x3da_0: var8=ebp;
+  L_0x3da_1: var8+=0x8;
+  L_0x3da_2: eax=*(uint32_t*)(var8);
+  L_0x3dd_0: var9=ebp;
+  L_0x3dd_1: var9-=0x4;
+  L_0x3dd_2: *(uint32_t*)(var9)=eax;
+  L_0x3e0_0: var10=ebp;
+  L_0x3e0_1: var10-=0x4;
+  L_0x3e0_2: eax=*(uint32_t*)(var10);
+  L_0x3e3_0: var11=esp;
+  L_0x3e3_1: var11+=0x4;
+  L_0x3e3_2: *(uint32_t*)(var11)=eax;
+  L_0x3e7_0: var12=ebp;
+  L_0x3e7_1: var12-=0x8;
+  L_0x3e7_2: eax=(uint32_t)&*(uint32_t*)(var12);
+  L_0x3ea_0: *(uint32_t*)(esp)=eax;
+  L_0x3ed_0: esp-=4; g__L_0x3b4_0(); esp+=4;
+  L_0x3f2_0: var13=ebp;
+  L_0x3f2_1: var13-=0x4;
+  L_0x3f2_2: *(uint32_t*)(var13)=0x5;
+  L_0x3f9_0: var14=ebp;
+  L_0x3f9_1: var14-=0x8;
+  L_0x3f9_2: eax=*(uint32_t*)(var14);
+  L_0x3fc_0: esp=ebp;
+  L_0x3fc_1: ebp=*(uint32_t*)(esp);
+  L_0x3fc_2: esp+=0x4;
+  L_0x3fd_0: return;
+}
+
+int main()
+{
+  L_0x3fe_0: esp-=0x4;
+  L_0x3fe_1: *(uint32_t*)(esp)=ebp;
+  L_0x3ff_0: ebp=esp;
+  L_0x401_0: esp-=0x14;
+  L_0x404_0: var15=ebp;
+  L_0x404_1: var15-=0x4;
+#ifdef NONDET
+  L_0x404_2: *(uint32_t*)(var15)=nondet_uint();
+#else
+  L_0x404_2: *(uint32_t*)(var15)=0xffffffff;
+#endif
+  L_0x40b_0: var16=ebp;
+  L_0x40b_1: var16-=0x4;
+  L_0x40b_2: eax=*(uint32_t*)(var16);
+  L_0x40e_0: *(uint32_t*)(esp)=eax;
+  L_0x411_0: esp-=4; f__L_0x3c6_0(); esp+=4;
+#if 1
+             uint32_t eax1=eax;
+  C_0x3ff_0: ebp=esp;
+  C_0x401_0: esp-=0x14;
+  C_0x404_0: var15=ebp;
+  C_0x404_1: var15-=0x4;
+#ifdef NONDET
+  C_0x404_2: *(uint32_t*)(var15)=nondet_uint();
+#else
+  C_0x404_2: *(uint32_t*)(var15)=0xffffffff;
+#endif
+  C_0x40b_0: var16=ebp;
+  C_0x40b_1: var16-=0x4;
+  C_0x40b_2: eax=*(uint32_t*)(var16);
+  C_0x40e_0: *(uint32_t*)(esp)=eax;
+  C_0x411_0: esp-=4; f__L_0x3c6_0(); esp+=4;
+             uint32_t eax2=eax;
+             assert(eax2==eax1);
+#endif
+  L_0x416_0: esp=ebp;
+  L_0x416_1: ebp=*(uint32_t*)(esp);
+  L_0x416_2: esp+=0x4;
+  L_0x417_0: return 0;
+}

regression/cbmc/address_space_size_limit3/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--32 --little-endian --object-bits 25 --pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^.* dereference failure: pointer outside object bounds in .*: FAILURE$
+--
+^warning: ignoring
+--
+requires at least 8 offset bits

src/cbmc/cbmc_parse_options.cpp

@@ -435,7 +435,23 @@ int cbmc_parse_optionst::doit()
   //
 
   optionst options;
-  get_command_line_options(options);
+  try
+  {
+    get_command_line_options(options);
+  }
+
+  catch(const char *error_msg)
+  {
+    error() << error_msg << eom;
+    return 6; // should contemplate EX_SOFTWARE from sysexits.h
+  }
+
+  catch(const std::string error_msg)
+  {
+    error() << error_msg << eom;
+    return 6; // should contemplate EX_SOFTWARE from sysexits.h
+  }
+
   eval_verbosity();
 
   //
@@ -659,9 +675,6 @@ int cbmc_parse_optionst::get_goto_program(
       }
     }
 
-    if(!binaries.empty())
-      config.set_from_symbol_table(symbol_table);
-
     if(cmdline.isset("show-symbol-table"))
     {
       show_symbol_table();
@@ -689,6 +702,8 @@ int cbmc_parse_optionst::get_goto_program(
       show_goto_functions(ns, get_ui(), goto_functions);
       return 0;
     }
+
+    status() << config.object_bits_info() << eom;
   }
 
   catch(const char *e)
@@ -1060,6 +1075,7 @@ void cbmc_parse_optionst::help()
     " --graphml-witness filename   write the witness in GraphML format to filename\n" // NOLINT(*)
     "\n"
     "Backend options:\n"
+    " --object-bits n              number of bits used for object addresses\n"
     " --dimacs                     generate CNF in DIMACS format\n"
     " --beautify                   beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
     " --localize-faults            localize faults (experimental)\n"

src/cbmc/cbmc_parse_options.h

@@ -31,6 +31,7 @@ class optionst;
   "(debug-level):(no-propagation)(no-simplify-if)" \
   "(document-subgoals)(outfile):(test-preprocessor)" \
   "D:I:(c89)(c99)(c11)(cpp89)(cpp99)(cpp11)" \
+  "(object-bits):" \
   "(classpath):(cp):(main-class):" \
   "(depth):(partial-loops)(no-unwinding-assertions)(unwinding-assertions)" \
   OPT_GOTO_CHECK \

src/clobber/clobber_parse_options.cpp

@@ -209,8 +209,6 @@ bool clobber_parse_optionst::get_goto_program(
            symbol_table, goto_functions, get_message_handler()))
         return true;
 
-      config.set_from_symbol_table(symbol_table);
-
       if(cmdline.isset("show-symbol-table"))
       {
         show_symbol_table();

src/goto-diff/goto_diff_parse_options.cpp

@@ -347,7 +347,6 @@ int goto_diff_parse_optionst::get_goto_program(
       return 6;
 
     config.set(cmdline);
-    config.set_from_symbol_table(goto_model.symbol_table);
 
     // This one is done.
     cmdline.args.erase(cmdline.args.begin());

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -867,7 +867,6 @@ void goto_instrument_parse_optionst::get_goto_program()
     throw 0;
 
   config.set(cmdline);
-  config.set_from_symbol_table(symbol_table);
 }
 
 void goto_instrument_parse_optionst::instrument_goto_program()

src/goto-programs/initialize_goto_model.cpp

@@ -131,9 +131,6 @@ bool initialize_goto_model(
         return true;
     }
 
-    if(!binaries.empty())
-      config.set_from_symbol_table(goto_model.symbol_table);
-
     msg.status() << "Generating GOTO Program" << messaget::eom;
 
     goto_convert(

src/goto-programs/read_goto_binary.cpp

@@ -28,6 +28,7 @@ Module: Read Goto Programs
 #include <util/tempfile.h>
 #include <util/rename_symbol.h>
 #include <util/base_type.h>
+#include <util/config.h>
 
 #include <langapi/language_ui.h>
 
@@ -383,6 +384,9 @@ bool read_object_and_link(
       linking.object_type_updates))
     return true;
 
+  // reading successful, let's update config
+  config.set_from_symbol_table(symbol_table);
+
   return false;
 }
 

src/langapi/language_ui.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <util/namespace.h>
 #include <util/language.h>
 #include <util/cmdline.h>
+#include <util/config.h>
 #include <util/unicode.h>
 
 #include "mode.h"
@@ -121,6 +122,8 @@ bool language_uit::final()
     return true;
   }
 
+  config.set_object_bits_from_symbol_table(symbol_table);
+
   return false;
 }
 

src/musketeer/musketeer_parse_options.cpp

@@ -139,8 +139,6 @@ void goto_fence_inserter_parse_optionst::get_goto_program(
   if(read_goto_binary(cmdline.args[0],
     symbol_table, goto_functions, get_message_handler()))
     throw 0;
-
-  config.set_from_symbol_table(symbol_table);
 }
 
 void goto_fence_inserter_parse_optionst::instrument_goto_program(

src/solvers/flattening/bv_pointers.cpp

@@ -95,7 +95,7 @@ bv_pointerst::bv_pointerst(
   boolbvt(_ns, _prop),
   pointer_logic(_ns)
 {
-  object_bits=BV_ADDR_BITS;
+  object_bits=config.bv_encoding.object_bits;
   offset_bits=config.ansi_c.pointer_width-object_bits;
   bits=config.ansi_c.pointer_width;
 }
@@ -600,7 +600,7 @@ exprt bv_pointerst::bv_get_rec(
   result.set_value(value);
 
   pointer_logict::pointert pointer;
-  pointer.object=integer2unsigned(binary2integer(value_addr, false));
+  pointer.object=integer2size_t(binary2integer(value_addr, false));
   pointer.offset=binary2integer(value_offset, true);
 
   // we add the elaborated expression as operand
@@ -681,8 +681,12 @@ void bv_pointerst::add_addr(const exprt &expr, bvt &bv)
 {
   std::size_t a=pointer_logic.add_object(expr);
 
-  if(a==(std::size_t(1)<<object_bits))
-    throw "too many variables";
+  const std::size_t max_objects=std::size_t(1)<<object_bits;
+  if(a==max_objects)
+    throw
+      "too many addressed objects: maximum number of objects is set to 2^n="+
+      std::to_string(max_objects)+" (with n="+std::to_string(object_bits)+"); "+
+      "use the `--object-bits n` option to increase the maximum number";
 
   encode(a, bv);
 }

src/solvers/flattening/pointer_logic.h

@@ -16,8 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/expr.h>
 #include <util/numbering.h>
 
-#define BV_ADDR_BITS 8
-
 class namespacet;
 
 class pointer_logict