Interpreter: switch to sparse vector memory map

This will allow large address reservations for unbounded-sized
objects, with actual cells allocated on demand.

Original patch:
From: Chris Smowton <[email protected]>
Date: Tue, 21 Mar 2017 15:24:03 +0000
Subject: [PATCH 1/3] Interpreter: switch to sparse vector memory map

Author: romainbrenguier

src/goto-programs/interpreter.cpp

@@ -712,22 +712,24 @@ exprt interpretert::get_value(
     if(rhs[offset]<memory.size())
     {
       // We want the symbol pointed to
-      memory_cellt &cell=memory[integer2unsigned(rhs[offset])];
-      const typet type=get_type(cell.identifier);
+      std::size_t address=integer2size_t(rhs[offset]);
+      irep_idt identifier=address_to_identifier(address);
+      size_t offset=address_to_offset(address);
+      const typet type=get_type(identifier);
       exprt symbol_expr(ID_symbol, type);
-      symbol_expr.set(ID_identifier, cell.identifier);
+      symbol_expr.set(ID_identifier, identifier);
 
-      if(cell.offset==0)
+      if(offset==0)
         return address_of_exprt(symbol_expr);
       if(ns.follow(type).id()==ID_struct)
       {
-        irep_idt member_id=get_component_id(cell.identifier, cell.offset);
+        irep_idt member_id=get_component_id(identifier, offset);
         member_exprt member_expr(symbol_expr, member_id);
         return address_of_exprt(member_expr);
       }
       index_exprt index_expr(
         symbol_expr,
-        from_integer(cell.offset, integer_typet()));
+        from_integer(offset, integer_typet()));
       return index_expr;
     }
 
@@ -828,12 +830,13 @@ void interpretert::assign(
   {
     if((address+i)<memory.size())
     {
-      memory_cellt &cell=memory[integer2unsigned(address+i)];
+      std::size_t address_val=integer2size_t(address+i);
+      memory_cellt &cell=memory[address_val];
       if(show)
       {
         status() << total_steps << " ** assigning "
-                 << cell.identifier << "["
-                 << cell.offset << "]:=" << rhs[i]
+                 << address_to_identifier(address_val) << "["
+                 << address_to_offset(address_val) << "]:=" << rhs[i]
                  << "\n" << eom;
       }
       cell.value=rhs[i];
@@ -913,8 +916,9 @@ void interpretert::execute_function_call()
   // Retrieve the empty last trace step struct we pushed for this step
   // of the interpreter run to fill it with the corresponding data
   goto_trace_stept &trace_step=steps.get_last_step();
-  const memory_cellt &cell=memory[integer2size_t(a)];
-  const irep_idt &identifier=cell.identifier;
+  std::size_t address=integer2size_t(a);
+  const memory_cellt &cell=memory[address];
+  const irep_idt &identifier=address_to_identifier(address);
   trace_step.identifier=identifier;
 
   const goto_functionst::function_mapt::const_iterator f_it=
@@ -1020,9 +1024,7 @@ void interpretert::build_memory_map()
 {
   // put in a dummy for NULL
   memory.resize(1);
-  memory[0].offset=0;
-  memory[0].identifier="NULL-OBJECT";
-  memory[0].initialized=0;
+  inverse_memory_map[0]="NULL-OBJECT";
 
   num_dynamic_objects=0;
   dynamic_types.clear();
@@ -1062,18 +1064,10 @@ void interpretert::build_memory_map(const symbolt &symbol)
 
   if(size!=0)
   {
-    unsigned address=memory.size();
+    std::size_t address=memory.size();
     memory.resize(address+size);
     memory_map[symbol.name]=address;
-
-    for(size_t i=0; i<size; i++)
-    {
-      memory_cellt &cell=memory[address+i];
-      cell.identifier=symbol.name;
-      cell.offset=i;
-      cell.value=0;
-      cell.initialized=0;
-    }
+    inverse_memory_map[address]=symbol.name;
   }
 }
 
@@ -1136,12 +1130,10 @@ mp_integer interpretert::build_memory_map(
 
   if(it!=dynamic_types.end())
   {
-    unsigned offset=1;
-    unsigned address=memory_map[id];
-    while(memory[address+offset].offset>0) offset++;
-
+    std::size_t address=memory_map[id];
+    std::size_t current_size=base_address_to_alloc_size(address);
     // current size <= size already recorded
-    if(size<=offset)
+    if(size<=current_size)
       return memory_map[id];
   }
 
@@ -1151,19 +1143,12 @@ mp_integer interpretert::build_memory_map(
   if(size==0)
     size=1; // This is a hack to create existence
 
-  unsigned address=memory.size();
+  std::size_t address=memory.size();
   memory.resize(address+size);
   memory_map[id]=address;
+  inverse_memory_map[address]=id;
   dynamic_types.insert(std::pair<const irep_idt, typet>(id, alloc_type));
 
-  for(size_t i=0; i<size; i++)
-  {
-    memory_cellt &cell=memory[address+i];
-    cell.identifier=id;
-    cell.offset=i;
-    cell.value=0;
-    cell.initialized=0;
-  }
   return address;
 }
 

src/goto-programs/interpreter_class.h

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include <stack>
 
 #include <util/arith_tools.h>
+#include <util/sparse_vector.h>
 
 #include "goto_functions.h"
 #include "goto_trace.h"
@@ -68,6 +69,9 @@ class interpretert:public messaget
   // List of dynamically allocated symbols that are not in the symbol table
   typedef std::map<irep_idt, typet> dynamic_typest;
 
+  typedef std::map<irep_idt, function_assignmentst> output_valuest;
+  output_valuest output_values;
+
   // An assignment list annotated with the calling context.
   struct function_assignments_contextt
   {
@@ -103,27 +107,78 @@ class interpretert:public messaget
 
   const goto_functionst &goto_functions;
 
-  typedef std::unordered_map<irep_idt, unsigned, irep_id_hash> memory_mapt;
+  typedef std::unordered_map<irep_idt, std::size_t, irep_id_hash> memory_mapt;
+  typedef std::map<std::size_t, irep_idt> inverse_memory_mapt;
   memory_mapt memory_map;
+  inverse_memory_mapt inverse_memory_map;
+
+  const inverse_memory_mapt::value_type &address_to_object_record(
+    std::size_t address) const
+  {
+    auto lower_bound=inverse_memory_map.lower_bound(address);
+    if(lower_bound->first!=address)
+    {
+      assert(lower_bound!=inverse_memory_map.begin());
+      --lower_bound;
+    }
+    return *lower_bound;
+  }
+
+  irep_idt address_to_identifier(std::size_t address) const
+  {
+    return address_to_object_record(address).second;
+  }
+
+  std::size_t address_to_offset(std::size_t address) const
+  {
+    return address-(address_to_object_record(address).first);
+  }
+
+  std::size_t base_address_to_alloc_size(std::size_t address) const
+  {
+    assert(address_to_offset(address)==0);
+    auto upper_bound=inverse_memory_map.upper_bound(address);
+    std::size_t next_alloc_address=
+      upper_bound==inverse_memory_map.end() ?
+      memory.size() :
+      upper_bound->first;
+    return next_alloc_address-address;
+  }
+
+  std::size_t base_address_to_actual_size(std::size_t address) const
+  {
+    auto memory_iter=memory.find(address);
+    if(memory_iter==memory.end())
+      return 0;
+    std::size_t ret=0;
+    std::size_t alloc_size=base_address_to_alloc_size(address);
+    while(memory_iter!=memory.end() && ret<alloc_size)
+    {
+      ++ret;
+      ++memory_iter;
+    }
+    return ret;
+  }
 
   class memory_cellt
   {
   public:
-    irep_idt identifier;
-    unsigned offset;
+    memory_cellt() :
+    value(0),
+    initialized(0)
+    {}
     mp_integer value;
     // Initialized is annotated even during reads
     // Set to 1 when written-before-read, -1 when read-before-written
     mutable char initialized;
   };
 
-  typedef std::vector<memory_cellt> memoryt;
+  typedef sparse_vectort<memory_cellt> memoryt;
   typedef std::map<std::string, const irep_idt &> parameter_sett;
   // mapping <structure, field> -> value
   typedef std::pair<const irep_idt, const irep_idt> struct_member_idt;
   typedef std::map<struct_member_idt, const exprt> struct_valuest;
 
-
   //  The memory is being annotated/reshaped even during reads
   //  (ie to find a read-before-write location) thus memory
   //  properties need to be mutable to avoid making all calls nonconst
@@ -135,6 +190,7 @@ class interpretert:public messaget
   void build_memory_map(const symbolt &symbol);
   mp_integer build_memory_map(const irep_idt &id, const typet &type);
   typet concretize_type(const typet &type);
+  bool unbounded_size(const typet &);
   size_t get_size(const typet &type);
 
   irep_idt get_component_id(const irep_idt &object, unsigned offset);
@@ -169,6 +225,10 @@ class interpretert:public messaget
     mp_integer address,
     mp_vectort &dest) const;
 
+  void read_unbounded(
+    mp_integer address,
+    mp_vectort &dest) const;
+
   virtual void command();
 
   class stack_framet