Add support for unbounded-size objects

They get allocated 2^32 address space each (of a 2^64 sized space)
using the sparse-vector memory representation to keep the actual
storage requirements sensible.

Original patch:
From: Chris Smowton <[email protected]>
Date: Tue, 21 Mar 2017 17:13:43 +0000
Subject: [PATCH 2/3] Add support for unbounded-size objects

Corrected linting issues

Using empty, and comments on get_size

Author: romainbrenguier

src/goto-programs/interpreter.cpp

@@ -597,16 +597,25 @@ exprt interpretert::get_value(
     exprt result=array_exprt(to_array_type(real_type));
     const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
     size_t subtype_size=get_size(type.subtype());
-    mp_integer mp_count;
-    to_integer(size_expr, mp_count);
-    unsigned count=integer2unsigned(mp_count);
+    std::size_t count;
+    if(size_expr.id()!=ID_constant)
+    {
+      count=base_address_to_actual_size(offset)/subtype_size;
+    }
+    else
+    {
+      mp_integer mp_count;
+      to_integer(size_expr, mp_count);
+      count=integer2size_t(mp_count);
+    }
 
     // Retrieve the value for each member in the array
     result.reserve_operands(count);
     for(unsigned i=0; i<count; i++)
     {
-      const exprt operand=get_value(type.subtype(),
-          offset+i*subtype_size);
+      const exprt operand=get_value(
+        type.subtype(),
+        offset+i*subtype_size);
       result.copy_to_operands(operand);
     }
     return result;
@@ -663,9 +672,17 @@ exprt interpretert::get_value(
 
     // Get size of array
     size_t subtype_size=get_size(type.subtype());
-    mp_integer mp_count;
-    to_integer(size_expr, mp_count);
-    unsigned count=integer2unsigned(mp_count);
+    unsigned count;
+    if(unbounded_size(type))
+    {
+      count=base_address_to_actual_size(offset)/subtype_size;
+    }
+    else
+    {
+      mp_integer mp_count;
+      to_integer(size_expr, mp_count);
+      count=integer2unsigned(mp_count);
+    }
 
     // Retrieve the value for each member in the array
     result.reserve_operands(count);
@@ -917,7 +934,9 @@ void interpretert::execute_function_call()
   // of the interpreter run to fill it with the corresponding data
   goto_trace_stept &trace_step=steps.get_last_step();
   std::size_t address=integer2size_t(a);
+#if 0
   const memory_cellt &cell=memory[address];
+#endif
   const irep_idt &identifier=address_to_identifier(address);
   trace_step.identifier=identifier;
 
@@ -1113,7 +1132,7 @@ Function: interpretert::build_memory_map
 
   Inputs:
 
- Outputs: Updtaes the memory map to include variable id if it does
+ Outputs: Updates the memory map to include variable id if it does
           not exist
 
  Purpose: Populates dynamic entries of the memory map
@@ -1152,20 +1171,45 @@ mp_integer interpretert::build_memory_map(
   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(type.subtype());
+  }
+  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;
+}
+
 /*******************************************************************\
 
 Function: interpretert::get_size
 
   Inputs:
+    type - a structured type
 
- Outputs:
+ Outputs: Size of the given type
 
- Purpose: Retrieves the actual size of the provided structured type
+ Purpose: Retrieves the actual size of the provided structured type.
+          Unbounded objects get allocated 2^32 address space each
+          (of a 2^64 sized space).
 
 \*******************************************************************/
 
 size_t interpretert::get_size(const typet &type)
 {
+  if(unbounded_size(type))
+    return 2ULL << 32ULL;
+
   if(type.id()==ID_struct)
   {
     const struct_typet::componentst &components=
@@ -1253,7 +1297,7 @@ exprt interpretert::get_value(const irep_idt &id)
   symbol_exprt symbol_expr(id, get_type);
   mp_integer whole_lhs_object_address=evaluate_address(symbol_expr);
 
-  return get_value(get_type, integer2unsigned(whole_lhs_object_address));
+  return get_value(get_type, integer2size_t(whole_lhs_object_address));
 }
 
 /*******************************************************************\
@@ -1295,10 +1339,13 @@ Function: interpretert::print_memory
 
 void interpretert::print_memory(bool input_flags)
 {
-  for(size_t i=0; i<memory.size(); i++)
+  for(const auto &cell_address : memory)
   {
-    memory_cellt &cell=memory[i];
-    debug() << cell.identifier << "[" << cell.offset << "]"
+    std::size_t i=cell_address.first;
+    const memory_cellt &cell=cell_address.second;
+    const auto identifier=address_to_identifier(i);
+    const auto offset=address_to_offset(i);
+    debug() << identifier << "[" << offset << "]"
             << "=" << cell.value << eom;
     if(input_flags)
       debug() << "(" << static_cast<int>(cell.initialized) << ")"