From e57813643321647bb587be636ca60c298b72adee Mon Sep 17 00:00:00 2001
From: reuk <reuk@users.noreply.github.com>
Date: Sat, 2 Sep 2017 10:48:37 +0100
Subject: [PATCH 1/3] Avoid integer truncation

---
 src/goto-programs/interpreter.cpp     | 5 +++--
 src/goto-programs/interpreter_class.h | 2 +-
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
index 25d2be08cb8..e25247ba8c1 100644
--- a/src/goto-programs/interpreter.cpp
+++ b/src/goto-programs/interpreter.cpp
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "interpreter.h"
 
 #include <cctype>
+#include <cstdint>
 #include <cstdio>
 #include <iostream>
 #include <fstream>
@@ -965,7 +966,7 @@ bool interpretert::unbounded_size(const typet &type)
 /// get allocated 2^32 address space each (of a 2^64 sized space).
 /// \param type: a structured type
 /// \return Size of the given type
-size_t interpretert::get_size(const typet &type)
+uint64_t interpretert::get_size(const typet &type)
 {
   if(unbounded_size(type))
     return 2ULL << 32ULL;
@@ -992,7 +993,7 @@ size_t interpretert::get_size(const typet &type)
     const union_typet::componentst &components=
       to_union_type(type).components();
 
-    size_t max_size=0;
+    uint64_t max_size=0;
 
     for(const auto &comp : components)
     {
diff --git a/src/goto-programs/interpreter_class.h b/src/goto-programs/interpreter_class.h
index 1b9ab433083..9fb2b046058 100644
--- a/src/goto-programs/interpreter_class.h
+++ b/src/goto-programs/interpreter_class.h
@@ -193,7 +193,7 @@ class interpretert:public messaget
   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);
+  uint64_t get_size(const typet &type);
 
   irep_idt get_component_id(const irep_idt &object, unsigned offset);
   typet get_type(const irep_idt &id) const;

From b860c265f4103d0bbcd777c41633f41c7c7c4045 Mon Sep 17 00:00:00 2001
From: reuk <reuk@users.noreply.github.com>
Date: Tue, 5 Sep 2017 16:38:12 +0100
Subject: [PATCH 2/3] Use mp_integer more extensively in interpreter

---
 src/goto-programs/interpreter.cpp          | 40 +++++++++++-----------
 src/goto-programs/interpreter_class.h      | 28 +++++++--------
 src/goto-programs/interpreter_evaluate.cpp |  4 +--
 src/util/sparse_vector.h                   | 18 +++++-----
 4 files changed, 46 insertions(+), 44 deletions(-)

diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
index e25247ba8c1..26c0a446c25 100644
--- a/src/goto-programs/interpreter.cpp
+++ b/src/goto-programs/interpreter.cpp
@@ -393,7 +393,7 @@ void interpretert::execute_other()
     mp_vectort tmp, rhs;
     evaluate(pc->code.op1(), tmp);
     mp_integer address=evaluate_address(pc->code.op0());
-    size_t size=get_size(pc->code.op0().type());
+    auto size=get_size(pc->code.op0().type());
     while(rhs.size()<size) rhs.insert(rhs.end(), tmp.begin(), tmp.end());
     if(size!=rhs.size())
       error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
@@ -420,7 +420,7 @@ void interpretert::execute_decl()
 /// \par parameters: an object and a memory offset
 irep_idt interpretert::get_component_id(
   const irep_idt &object,
-  unsigned offset)
+  mp_integer offset)
 {
   const symbolt &symbol=ns.lookup(object);
   const typet real_type=ns.follow(symbol.type);
@@ -434,7 +434,7 @@ irep_idt interpretert::get_component_id(
   {
     if(offset<=0)
       return it->id();
-    size_t size=get_size(it->type());
+    auto size=get_size(it->type());
     offset-=size;
   }
   return object;
@@ -453,7 +453,7 @@ typet interpretert::get_type(const irep_idt &id) const
 /// type
 exprt interpretert::get_value(
   const typet &type,
-  std::size_t offset,
+  uint64_t offset,
   bool use_non_det)
 {
   const typet real_type=ns.follow(type);
@@ -468,7 +468,7 @@ exprt interpretert::get_value(
     for(struct_typet::componentst::const_iterator it=components.begin();
         it!=components.end(); it++)
     {
-      size_t size=get_size(it->type());
+      auto size=get_size(it->type());
       const exprt operand=get_value(it->type(), offset);
       offset+=size;
       result.copy_to_operands(operand);
@@ -480,7 +480,7 @@ exprt interpretert::get_value(
     // Get size of array
     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());
+    auto subtype_size=get_size(type.subtype());
     std::size_t count;
     if(size_expr.id()!=ID_constant)
     {
@@ -518,7 +518,7 @@ exprt interpretert::get_value(
 exprt interpretert::get_value(
   const typet &type,
   mp_vectort &rhs,
-  std::size_t offset)
+  uint64_t offset)
 {
   const typet real_type=ns.follow(type);
   PRECONDITION(!rhs.empty());
@@ -533,7 +533,7 @@ exprt interpretert::get_value(
     result.reserve_operands(components.size());
     for(const struct_union_typet::componentt &expr : components)
     {
-      size_t size=get_size(expr.type());
+      auto size=get_size(expr.type());
       const exprt operand=get_value(expr.type(), rhs, offset);
       offset+=size;
       result.copy_to_operands(operand);
@@ -546,7 +546,7 @@ exprt interpretert::get_value(
     const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
 
     // Get size of array
-    size_t subtype_size=get_size(type.subtype());
+    auto subtype_size=get_size(type.subtype());
     unsigned count;
     if(unbounded_size(type))
     {
@@ -606,7 +606,7 @@ exprt interpretert::get_value(
       // We want the symbol pointed to
       std::size_t address=integer2size_t(rhs[offset]);
       irep_idt identifier=address_to_identifier(address);
-      size_t offset=address_to_offset(address);
+      auto offset=address_to_offset(address);
       const typet type=get_type(identifier);
       exprt symbol_expr(ID_symbol, type);
       symbol_expr.set(ID_identifier, identifier);
@@ -652,7 +652,7 @@ void interpretert::execute_assign()
   if(!rhs.empty())
   {
     mp_integer address=evaluate_address(code_assign.lhs());
-    size_t size=get_size(code_assign.lhs().type());
+    auto size=get_size(code_assign.lhs().type());
 
     if(size!=rhs.size())
       error() << "!! failed to obtain rhs ("
@@ -681,7 +681,7 @@ void interpretert::execute_assign()
     if(side_effect.get_statement()==ID_nondet)
     {
       unsigned address=integer2unsigned(evaluate_address(code_assign.lhs()));
-      size_t size=get_size(code_assign.lhs().type());
+      auto size=get_size(code_assign.lhs().type());
       for(size_t i=0; i<size; i++)
       {
         memory[address+i].initialized=
@@ -863,7 +863,7 @@ void interpretert::build_memory_map()
 
 void interpretert::build_memory_map(const symbolt &symbol)
 {
-  size_t size=0;
+  uint64_t size=0;
 
   if(symbol.type.id()==ID_code)
   {
@@ -876,7 +876,7 @@ void interpretert::build_memory_map(const symbolt &symbol)
 
   if(size!=0)
   {
-    std::size_t address=memory.size();
+    auto address=memory.size();
     memory.resize(address+size);
     memory_map[symbol.name]=address;
     inverse_memory_map[address]=symbol.name;
@@ -916,13 +916,13 @@ mp_integer interpretert::build_memory_map(
   const typet &type)
 {
   typet alloc_type=concretize_type(type);
-  size_t size=get_size(alloc_type);
+  auto size=get_size(alloc_type);
   auto it=dynamic_types.find(id);
 
   if(it!=dynamic_types.end())
   {
-    std::size_t address=memory_map[id];
-    std::size_t current_size=base_address_to_alloc_size(address);
+    const auto address=memory_map[id];
+    const auto current_size=base_address_to_alloc_size(address);
     // current size <= size already recorded
     if(size<=current_size)
       return memory_map[id];
@@ -934,7 +934,7 @@ mp_integer interpretert::build_memory_map(
   if(size==0)
     size=1; // This is a hack to create existence
 
-  std::size_t address=memory.size();
+  const auto address=memory.size();
   memory.resize(address+size);
   memory_map[id]=address;
   inverse_memory_map[address]=id;
@@ -976,7 +976,7 @@ uint64_t interpretert::get_size(const typet &type)
     const struct_typet::componentst &components=
       to_struct_type(type).components();
 
-    unsigned sum=0;
+    uint64_t sum=0;
 
     for(const auto &comp : components)
     {
@@ -1068,7 +1068,7 @@ void interpretert::print_memory(bool input_flags)
 {
   for(const auto &cell_address : memory)
   {
-    std::size_t i=cell_address.first;
+    const auto 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);
diff --git a/src/goto-programs/interpreter_class.h b/src/goto-programs/interpreter_class.h
index 9fb2b046058..409ea609c47 100644
--- a/src/goto-programs/interpreter_class.h
+++ b/src/goto-programs/interpreter_class.h
@@ -103,13 +103,13 @@ class interpretert:public messaget
 
   const goto_functionst &goto_functions;
 
-  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;
+  typedef std::unordered_map<irep_idt, mp_integer, irep_id_hash> memory_mapt;
+  typedef std::map<mp_integer, 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
+    const mp_integer &address) const
   {
     auto lower_bound=inverse_memory_map.lower_bound(address);
     if(lower_bound->first!=address)
@@ -120,34 +120,34 @@ class interpretert:public messaget
     return *lower_bound;
   }
 
-  irep_idt address_to_identifier(std::size_t address) const
+  irep_idt address_to_identifier(const mp_integer &address) const
   {
     return address_to_object_record(address).second;
   }
 
-  std::size_t address_to_offset(std::size_t address) const
+  mp_integer address_to_offset(const mp_integer &address) const
   {
     return address-(address_to_object_record(address).first);
   }
 
-  std::size_t base_address_to_alloc_size(std::size_t address) const
+  mp_integer base_address_to_alloc_size(const mp_integer &address) const
   {
     PRECONDITION(address_to_offset(address)==0);
     auto upper_bound=inverse_memory_map.upper_bound(address);
-    std::size_t next_alloc_address=
+    mp_integer 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
+  uint64_t base_address_to_actual_size(const mp_integer &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);
+    mp_integer alloc_size=base_address_to_alloc_size(address);
     while(memory_iter!=memory.end() && memory_iter->first<(address+alloc_size))
     {
       ++ret;
@@ -186,7 +186,7 @@ class interpretert:public messaget
   //  properties need to be mutable to avoid making all calls nonconst
   mutable memoryt memory;
 
-  std::size_t stack_pointer;
+  mp_integer stack_pointer;
 
   void build_memory_map();
   void build_memory_map(const symbolt &symbol);
@@ -195,13 +195,13 @@ class interpretert:public messaget
   bool unbounded_size(const typet &);
   uint64_t get_size(const typet &type);
 
-  irep_idt get_component_id(const irep_idt &object, unsigned offset);
+  irep_idt get_component_id(const irep_idt &object, mp_integer offset);
   typet get_type(const irep_idt &id) const;
   exprt get_value(
     const typet &type,
-    std::size_t offset=0,
+    uint64_t offset=0,
     bool use_non_det=false);
-  exprt get_value(const typet &type, mp_vectort &rhs, std::size_t offset=0);
+  exprt get_value(const typet &type, mp_vectort &rhs, uint64_t offset=0);
   exprt get_value(const irep_idt &id);
 
   void step();
@@ -240,7 +240,7 @@ class interpretert:public messaget
     goto_functionst::function_mapt::const_iterator return_function;
     mp_integer return_value_address;
     memory_mapt local_map;
-    unsigned old_stack_pointer;
+    mp_integer old_stack_pointer;
   };
 
   typedef std::stack<stack_framet> call_stackt;
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
index 81d3fd33527..5ab036406f9 100644
--- a/src/goto-programs/interpreter_evaluate.cpp
+++ b/src/goto-programs/interpreter_evaluate.cpp
@@ -52,10 +52,10 @@ void interpretert::read_unbounded(
 {
   // copy memory region
   std::size_t address_val=integer2size_t(address);
-  const std::size_t offset=address_to_offset(address_val);
+  const auto offset=address_to_offset(address_val);
   const std::size_t alloc_size=
     base_address_to_actual_size(address_val-offset);
-  const std::size_t to_read=alloc_size-offset;
+  const auto to_read=alloc_size-offset;
   for(size_t i=0; i<to_read; i++)
   {
     mp_integer value;
diff --git a/src/util/sparse_vector.h b/src/util/sparse_vector.h
index 0b8332400a7..42ccac0cb5a 100644
--- a/src/util/sparse_vector.h
+++ b/src/util/sparse_vector.h
@@ -13,6 +13,7 @@ Author: Romain Brenguier
 #define CPROVER_UTIL_SPARSE_VECTOR_H
 
 #include "invariant.h"
+#include "mp_arith.h"
 
 #include <cstdint>
 #include <map>
@@ -20,35 +21,36 @@ Author: Romain Brenguier
 template<class T> class sparse_vectort
 {
 protected:
-  typedef std::map<uint64_t, T> underlyingt;
+  typedef std::map<mp_integer, T> underlyingt;
+  typedef typename underlyingt::key_type key_type;
   underlyingt underlying;
-  uint64_t _size;
+  mp_integer _size;
 
 public:
   sparse_vectort() :
     _size(0) {}
 
-  const T &operator[](uint64_t idx) const
+  const T &operator[](const key_type &idx) const
   {
     INVARIANT(idx<_size, "index out of range");
     return underlying[idx];
   }
 
-  T &operator[](uint64_t idx)
+  T &operator[](const key_type &idx)
   {
     INVARIANT(idx<_size, "index out of range");
     return underlying[idx];
   }
 
-  uint64_t size() const
+  mp_integer size() const
   {
     return _size;
   }
 
-  void resize(uint64_t new_size)
+  void resize(mp_integer new_size)
   {
     INVARIANT(new_size>=_size, "sparse vector can't be shrunk (yet)");
-    _size=new_size;
+    _size=std::move(new_size);
   }
 
   typedef typename underlyingt::iterator iteratort;
@@ -60,7 +62,7 @@ template<class T> class sparse_vectort
   iteratort end() { return underlying.end(); }
   const_iteratort end() const { return underlying.end(); }
 
-  const_iteratort find(uint64_t idx) { return underlying.find(idx); }
+  const_iteratort find(const mp_integer &idx) { return underlying.find(idx); }
 };
 
 #endif // CPROVER_UTIL_SPARSE_VECTOR_H

From 661e09592e232bafcddd7823e100ca5edfafe7a2 Mon Sep 17 00:00:00 2001
From: reuk <reuk@users.noreply.github.com>
Date: Tue, 5 Sep 2017 18:15:45 +0100
Subject: [PATCH 3/3] Stop using unsigned and uint64_t in interpreter

---
 src/goto-programs/interpreter.cpp          | 89 +++++++++++-----------
 src/goto-programs/interpreter_class.h      | 13 ++--
 src/goto-programs/interpreter_evaluate.cpp | 44 +++++------
 3 files changed, 74 insertions(+), 72 deletions(-)

diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
index 26c0a446c25..46567548e2b 100644
--- a/src/goto-programs/interpreter.cpp
+++ b/src/goto-programs/interpreter.cpp
@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <fstream>
 #include <algorithm>
 #include <string.h>
+#include <type_traits>
 
 #include <util/invariant.h>
 #include <util/std_types.h>
@@ -393,7 +394,7 @@ void interpretert::execute_other()
     mp_vectort tmp, rhs;
     evaluate(pc->code.op1(), tmp);
     mp_integer address=evaluate_address(pc->code.op0());
-    auto size=get_size(pc->code.op0().type());
+    const auto size=get_size(pc->code.op0().type());
     while(rhs.size()<size) rhs.insert(rhs.end(), tmp.begin(), tmp.end());
     if(size!=rhs.size())
       error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
@@ -434,7 +435,7 @@ irep_idt interpretert::get_component_id(
   {
     if(offset<=0)
       return it->id();
-    auto size=get_size(it->type());
+    const auto size=get_size(it->type());
     offset-=size;
   }
   return object;
@@ -453,7 +454,7 @@ typet interpretert::get_type(const irep_idt &id) const
 /// type
 exprt interpretert::get_value(
   const typet &type,
-  uint64_t offset,
+  mp_integer offset,
   bool use_non_det)
 {
   const typet real_type=ns.follow(type);
@@ -468,7 +469,7 @@ exprt interpretert::get_value(
     for(struct_typet::componentst::const_iterator it=components.begin();
         it!=components.end(); it++)
     {
-      auto size=get_size(it->type());
+      const auto size=get_size(it->type());
       const exprt operand=get_value(it->type(), offset);
       offset+=size;
       result.copy_to_operands(operand);
@@ -480,8 +481,8 @@ exprt interpretert::get_value(
     // Get size of array
     exprt result=array_exprt(to_array_type(real_type));
     const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
-    auto subtype_size=get_size(type.subtype());
-    std::size_t count;
+    const auto subtype_size=get_size(type.subtype());
+    mp_integer count=0;
     if(size_expr.id()!=ID_constant)
     {
       count=base_address_to_actual_size(offset)/subtype_size;
@@ -490,12 +491,12 @@ exprt interpretert::get_value(
     {
       mp_integer mp_count;
       to_integer(size_expr, mp_count);
-      count=integer2size_t(mp_count);
+      count=mp_count;
     }
 
     // Retrieve the value for each member in the array
-    result.reserve_operands(count);
-    for(unsigned i=0; i<count; i++)
+    result.reserve_operands(integer2size_t(count));
+    for(decltype(count) i=0; i<count; ++i)
     {
       const exprt operand=get_value(
         type.subtype(),
@@ -518,7 +519,7 @@ exprt interpretert::get_value(
 exprt interpretert::get_value(
   const typet &type,
   mp_vectort &rhs,
-  uint64_t offset)
+  mp_integer offset)
 {
   const typet real_type=ns.follow(type);
   PRECONDITION(!rhs.empty());
@@ -533,7 +534,7 @@ exprt interpretert::get_value(
     result.reserve_operands(components.size());
     for(const struct_union_typet::componentt &expr : components)
     {
-      auto size=get_size(expr.type());
+      const auto size=get_size(expr.type());
       const exprt operand=get_value(expr.type(), rhs, offset);
       offset+=size;
       result.copy_to_operands(operand);
@@ -546,8 +547,8 @@ exprt interpretert::get_value(
     const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
 
     // Get size of array
-    auto subtype_size=get_size(type.subtype());
-    unsigned count;
+    const auto subtype_size=get_size(type.subtype());
+    mp_integer count;
     if(unbounded_size(type))
     {
       count=base_address_to_actual_size(offset)/subtype_size;
@@ -556,12 +557,12 @@ exprt interpretert::get_value(
     {
       mp_integer mp_count;
       to_integer(size_expr, mp_count);
-      count=integer2unsigned(mp_count);
+      count=mp_count;
     }
 
     // Retrieve the value for each member in the array
-    result.reserve_operands(count);
-    for(unsigned i=0; i<count; i++)
+    result.reserve_operands(integer2size_t(count));
+    for(std::remove_const<decltype(count)>::type i=0; i<count; ++i)
     {
       const exprt operand=get_value(type.subtype(), rhs,
           offset+i*subtype_size);
@@ -572,41 +573,41 @@ exprt interpretert::get_value(
   else if(real_type.id()==ID_floatbv)
   {
     ieee_floatt f(to_floatbv_type(type));
-    f.unpack(rhs[offset]);
+    f.unpack(rhs[integer2size_t(offset)]);
     return f.to_expr();
   }
   else if(real_type.id()==ID_fixedbv)
   {
     fixedbvt f;
-    f.from_integer(rhs[offset]);
+    f.from_integer(rhs[integer2size_t(offset)]);
     return f.to_expr();
   }
   else if(real_type.id()==ID_bool)
   {
-    if(rhs[offset]!=0)
+    if(rhs[integer2size_t(offset)]!=0)
       return true_exprt();
     else
       false_exprt();
   }
   else if(real_type.id()==ID_c_bool)
   {
-    return from_integer(rhs[offset]!=0?1:0, type);
+    return from_integer(rhs[integer2size_t(offset)]!=0?1:0, type);
   }
   else if((real_type.id()==ID_pointer) || (real_type.id()==ID_address_of))
   {
-    if(rhs[offset]==0)
+    if(rhs[integer2size_t(offset)]==0)
     {
       // NULL pointer
       constant_exprt result(type);
       result.set_value(ID_NULL);
       return result;
     }
-    if(rhs[offset]<memory.size())
+    if(rhs[integer2size_t(offset)]<memory.size())
     {
       // We want the symbol pointed to
-      std::size_t address=integer2size_t(rhs[offset]);
+      const auto address=rhs[integer2size_t(offset)];
       irep_idt identifier=address_to_identifier(address);
-      auto offset=address_to_offset(address);
+      const auto offset=address_to_offset(address);
       const typet type=get_type(identifier);
       exprt symbol_expr(ID_symbol, type);
       symbol_expr.set(ID_identifier, identifier);
@@ -625,7 +626,7 @@ exprt interpretert::get_value(
       return index_expr;
     }
 
-    error() << "interpreter: invalid pointer " << rhs[offset]
+    error() << "interpreter: invalid pointer " << rhs[integer2size_t(offset)]
             << " > object count " << memory.size() << eom;
     throw "interpreter: reading from invalid pointer";
   }
@@ -633,11 +634,11 @@ exprt interpretert::get_value(
   {
     // Strings are currently encoded by their irep_idt ID.
     return constant_exprt(
-      irep_idt::make_from_table_index(rhs[offset].to_long()),
+      irep_idt::make_from_table_index(rhs[integer2size_t(offset)].to_long()),
       type);
   }
   // Retrieve value of basic data type
-  return from_integer(rhs[offset], type);
+  return from_integer(rhs[integer2size_t(offset)], type);
 }
 
 /// executes the assign statement at the current pc value
@@ -652,7 +653,7 @@ void interpretert::execute_assign()
   if(!rhs.empty())
   {
     mp_integer address=evaluate_address(code_assign.lhs());
-    auto size=get_size(code_assign.lhs().type());
+    const auto size=get_size(code_assign.lhs().type());
 
     if(size!=rhs.size())
       error() << "!! failed to obtain rhs ("
@@ -680,9 +681,9 @@ void interpretert::execute_assign()
     side_effect_exprt side_effect=to_side_effect_expr(code_assign.rhs());
     if(side_effect.get_statement()==ID_nondet)
     {
-      unsigned address=integer2unsigned(evaluate_address(code_assign.lhs()));
-      auto size=get_size(code_assign.lhs().type());
-      for(size_t i=0; i<size; i++)
+      const auto address=evaluate_address(code_assign.lhs());
+      const auto size=get_size(code_assign.lhs().type());
+      for(std::remove_const<decltype(size)>::type i=0; i<size; ++i)
       {
         memory[address+i].initialized=
           memory_cellt::initializedt::READ_BEFORE_WRITTEN;
@@ -700,7 +701,7 @@ void interpretert::assign(
   {
     if((address+i)<memory.size())
     {
-      std::size_t address_val=integer2size_t(address+i);
+      const auto address_val=address+i;
       memory_cellt &cell=memory[address_val];
       if(show)
       {
@@ -750,7 +751,7 @@ 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();
-  std::size_t address=integer2size_t(a);
+  const auto address=a;
 #if 0
   const memory_cellt &cell=memory[address];
 #endif
@@ -799,7 +800,7 @@ void interpretert::execute_function_call()
     for(const auto &id : locals)
     {
       const symbolt &symbol=ns.lookup(id);
-      frame.local_map[id]=integer2unsigned(build_memory_map(id, symbol.type));
+      frame.local_map[id]=build_memory_map(id, symbol.type);
     }
 
     // assign the arguments
@@ -863,7 +864,7 @@ void interpretert::build_memory_map()
 
 void interpretert::build_memory_map(const symbolt &symbol)
 {
-  uint64_t size=0;
+  mp_integer size=0;
 
   if(symbol.type.id()==ID_code)
   {
@@ -876,7 +877,7 @@ void interpretert::build_memory_map(const symbolt &symbol)
 
   if(size!=0)
   {
-    auto address=memory.size();
+    const auto address=memory.size();
     memory.resize(address+size);
     memory_map[symbol.name]=address;
     inverse_memory_map[address]=symbol.name;
@@ -917,7 +918,7 @@ mp_integer interpretert::build_memory_map(
 {
   typet alloc_type=concretize_type(type);
   auto size=get_size(alloc_type);
-  auto it=dynamic_types.find(id);
+  const auto it=dynamic_types.find(id);
 
   if(it!=dynamic_types.end())
   {
@@ -966,7 +967,7 @@ bool interpretert::unbounded_size(const typet &type)
 /// get allocated 2^32 address space each (of a 2^64 sized space).
 /// \param type: a structured type
 /// \return Size of the given type
-uint64_t interpretert::get_size(const typet &type)
+mp_integer interpretert::get_size(const typet &type)
 {
   if(unbounded_size(type))
     return 2ULL << 32ULL;
@@ -976,7 +977,7 @@ uint64_t interpretert::get_size(const typet &type)
     const struct_typet::componentst &components=
       to_struct_type(type).components();
 
-    uint64_t sum=0;
+    mp_integer sum=0;
 
     for(const auto &comp : components)
     {
@@ -993,7 +994,7 @@ uint64_t interpretert::get_size(const typet &type)
     const union_typet::componentst &components=
       to_union_type(type).components();
 
-    uint64_t max_size=0;
+    mp_integer max_size=0;
 
     for(const auto &comp : components)
     {
@@ -1009,7 +1010,7 @@ uint64_t interpretert::get_size(const typet &type)
   {
     const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
 
-    size_t subtype_size=get_size(type.subtype());
+    const auto subtype_size=get_size(type.subtype());
 
     mp_vectort i;
     evaluate(size_expr, i);
@@ -1021,7 +1022,7 @@ uint64_t interpretert::get_size(const typet &type)
       mp_integer size_mp;
       bool ret=to_integer(size_const, size_mp);
       CHECK_RETURN(!ret);
-      return subtype_size*integer2unsigned(size_mp);
+      return subtype_size*size_mp;
     }
     return subtype_size;
   }
@@ -1037,7 +1038,7 @@ exprt interpretert::get_value(const irep_idt &id)
   // The dynamic type and the static symbol type may differ for VLAs,
   // where the symbol carries a size expression and the dynamic type
   // registry contains its actual length.
-  auto findit=dynamic_types.find(id);
+  const auto findit=dynamic_types.find(id);
   typet get_type;
   if(findit!=dynamic_types.end())
     get_type=findit->second;
@@ -1047,7 +1048,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, integer2size_t(whole_lhs_object_address));
+  return get_value(get_type, whole_lhs_object_address);
 }
 
 void interpreter(
diff --git a/src/goto-programs/interpreter_class.h b/src/goto-programs/interpreter_class.h
index 409ea609c47..3d6b870f121 100644
--- a/src/goto-programs/interpreter_class.h
+++ b/src/goto-programs/interpreter_class.h
@@ -141,12 +141,12 @@ class interpretert:public messaget
     return next_alloc_address-address;
   }
 
-  uint64_t base_address_to_actual_size(const mp_integer &address) const
+  mp_integer base_address_to_actual_size(const mp_integer &address) const
   {
     auto memory_iter=memory.find(address);
     if(memory_iter==memory.end())
       return 0;
-    std::size_t ret=0;
+    mp_integer ret=0;
     mp_integer alloc_size=base_address_to_alloc_size(address);
     while(memory_iter!=memory.end() && memory_iter->first<(address+alloc_size))
     {
@@ -193,15 +193,16 @@ class interpretert:public messaget
   mp_integer build_memory_map(const irep_idt &id, const typet &type);
   typet concretize_type(const typet &type);
   bool unbounded_size(const typet &);
-  uint64_t get_size(const typet &type);
+  mp_integer get_size(const typet &type);
 
   irep_idt get_component_id(const irep_idt &object, mp_integer offset);
   typet get_type(const irep_idt &id) const;
   exprt get_value(
     const typet &type,
-    uint64_t offset=0,
+    mp_integer offset=0,
     bool use_non_det=false);
-  exprt get_value(const typet &type, mp_vectort &rhs, uint64_t offset=0);
+  exprt get_value(
+    const typet &type, mp_vectort &rhs, mp_integer offset=0);
   exprt get_value(const irep_idt &id);
 
   void step();
@@ -217,7 +218,7 @@ class interpretert:public messaget
 
   void allocate(
     const mp_integer &address,
-    size_t size);
+    mp_integer size);
 
   void assign(
     const mp_integer &address,
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
index 5ab036406f9..6c9b6b76368 100644
--- a/src/goto-programs/interpreter_evaluate.cpp
+++ b/src/goto-programs/interpreter_evaluate.cpp
@@ -51,12 +51,12 @@ void interpretert::read_unbounded(
   mp_vectort &dest) const
 {
   // copy memory region
-  std::size_t address_val=integer2size_t(address);
+  const auto address_val=address;
   const auto offset=address_to_offset(address_val);
-  const std::size_t alloc_size=
+  const auto alloc_size=
     base_address_to_actual_size(address_val-offset);
   const auto to_read=alloc_size-offset;
-  for(size_t i=0; i<to_read; i++)
+  for(std::remove_const<decltype(to_read)>::type i=0; i<to_read; ++i)
   {
     mp_integer value;
 
@@ -77,10 +77,10 @@ void interpretert::read_unbounded(
 /// reserves memory block of size at address
 void interpretert::allocate(
   const mp_integer &address,
-  size_t size)
+  mp_integer size)
 {
   // clear memory region
-  for(size_t i=0; i<size; i++)
+  for(decltype(size) i=0; i<size; ++i)
   {
     if((address+i)<memory.size())
     {
@@ -307,7 +307,7 @@ void interpretert::evaluate(
   {
     if(expr.type().id()==ID_struct)
     {
-      dest.reserve(get_size(expr.type()));
+      dest.reserve(integer2size_t(get_size(expr.type())));
       bool error=false;
 
       forall_operands(it, expr)
@@ -315,7 +315,7 @@ void interpretert::evaluate(
         if(it->type().id()==ID_code)
           continue;
 
-        size_t sub_size=get_size(it->type());
+        const auto sub_size=get_size(it->type());
         if(sub_size==0)
           continue;
 
@@ -324,8 +324,8 @@ void interpretert::evaluate(
 
         if(tmp.size()==sub_size)
         {
-          for(size_t i=0; i<sub_size; i++)
-            dest.push_back(tmp[i]);
+          for(std::remove_const<decltype(sub_size)>::type i=0; i<sub_size; ++i)
+            dest.push_back(tmp[integer2size_t(i)]);
         }
         else
           error=true;
@@ -380,7 +380,7 @@ void interpretert::evaluate(
     {
       irep_idt value=to_constant_expr(expr).get_value();
       const char *str=value.c_str();
-      size_t length=strlen(str)+1;
+      const auto length=strlen(str)+1;
       if(show)
         warning() << "string decoding not fully implemented "
                   << length << eom;
@@ -401,7 +401,7 @@ void interpretert::evaluate(
   else if(expr.id()==ID_struct)
   {
     if(!unbounded_size(expr.type()))
-      dest.reserve(get_size(expr.type()));
+      dest.reserve(integer2size_t(get_size(expr.type())));
     bool error=false;
 
     forall_operands(it, expr)
@@ -409,7 +409,7 @@ void interpretert::evaluate(
       if(it->type().id()==ID_code)
         continue;
 
-      size_t sub_size=get_size(it->type());
+      const auto sub_size=get_size(it->type());
       if(sub_size==0)
         continue;
 
@@ -852,7 +852,7 @@ void interpretert::evaluate(
       mp_integer address=result[0];
       if(address>0 && address<memory.size())
       {
-        std::size_t address_val=integer2size_t(address);
+        const auto address_val=address;
         auto obj_type=get_type(address_to_identifier(address_val));
 
         mp_integer offset=address_to_offset(address_val);
@@ -954,7 +954,7 @@ void interpretert::evaluate(
     {
       if(!unbounded_size(expr.type()))
       {
-        dest.resize(get_size(expr.type()));
+        dest.resize(integer2size_t(get_size(expr.type())));
         read(address, dest);
       }
       else
@@ -1020,8 +1020,8 @@ void interpretert::evaluate(
       evaluate(ty.size(), size);
     if(size.size()==1)
     {
-      std::size_t size_int=integer2size_t(size[0]);
-      for(std::size_t i=0; i<size_int; ++i)
+      const auto size_int=size[0];
+      for(std::remove_const<decltype(size_int)>::type i=0; i<size_int; ++i)
         evaluate(expr.op0(), dest);
       return;
     }
@@ -1040,13 +1040,13 @@ void interpretert::evaluate(
       // Ignore indices < 0, which the string solver sometimes produces
       if(where[0]<0)
         return;
-      std::size_t where_idx=integer2size_t(where[0]);
-      std::size_t subtype_size=get_size(subtype);
-      std::size_t need_size=(where_idx+1)*subtype_size;
+      const auto where_idx=where[0];
+      const auto subtype_size=get_size(subtype);
+      const auto need_size=(where_idx+1)*subtype_size;
       if(dest.size()<need_size)
-        dest.resize(need_size, 0);
+        dest.resize(integer2size_t(need_size), 0);
       for(std::size_t i=0; i<new_value.size(); ++i)
-        dest[(where_idx*subtype_size)+i]=new_value[i];
+        dest[integer2size_t((where_idx*subtype_size)+i)]=new_value[i];
       return;
     }
   }
@@ -1135,7 +1135,7 @@ mp_integer interpretert::evaluate_address(
     const irep_idt &component_name=
       to_member_expr(expr).get_component_name();
 
-    unsigned offset=0;
+    mp_integer offset=0;
 
     for(const auto &comp : struct_type.components())
     {