From 185c77f517ceb3f714c351f334e3fb6a0a5dcb4c Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 5 Dec 2022 17:53:11 +0000
Subject: [PATCH] Introduce bitst and bytest to avoid bit/byte mix-up

Use mp_integers with a unit to clarify when an mp_integer holds a number
of bits or a number of bytes. This makes sure that type-inconsistent
comparisons as fixed in #7411 result in compile-time errors.
---
 src/ansi-c/padding.cpp                        |   4 +-
 src/cprover/bv_pointers_wide.cpp              |  16 ++-
 src/cprover/endianness_map_wide.cpp           |   2 +-
 src/goto-instrument/count_eloc.cpp            |   4 +-
 src/goto-programs/interpreter_class.h         |   2 +-
 src/goto-programs/interpreter_evaluate.cpp    |  10 +-
 src/goto-programs/vcd_goto_trace.cpp          |   2 +-
 src/goto-symex/symex_builtin_functions.cpp    |   4 +-
 src/memory-analyzer/analyze_symbol.cpp        |   7 +-
 src/pointer-analysis/value_set.cpp            |  26 ++--
 src/pointer-analysis/value_set.h              |   8 +-
 .../value_set_dereference.cpp                 |  13 +-
 src/solvers/flattening/bv_pointers.cpp        |  14 +-
 src/solvers/flattening/pointer_logic.cpp      |   8 +-
 src/solvers/flattening/pointer_logic.h        |   5 +-
 src/solvers/smt2/smt2_conv.cpp                |  62 ++++-----
 src/util/arith_tools.h                        |  42 ++++++
 src/util/c_types.cpp                          |   4 +-
 src/util/c_types.h                            |   2 +-
 src/util/expr_util.cpp                        |  14 +-
 src/util/lower_byte_operators.cpp             | 125 +++++++++---------
 src/util/mp_arith.h                           | 108 +++++++++++++++
 src/util/pointer_offset_size.cpp              |  87 ++++++------
 src/util/pointer_offset_size.h                |  14 +-
 src/util/simplify_expr.cpp                    |  79 ++++++-----
 src/util/simplify_expr_int.cpp                |   2 +-
 src/util/simplify_expr_struct.cpp             |   2 +-
 src/util/simplify_utils.cpp                   |  12 +-
 unit/util/pointer_offset_size.cpp             |  14 +-
 29 files changed, 427 insertions(+), 265 deletions(-)

diff --git a/src/ansi-c/padding.cpp b/src/ansi-c/padding.cpp
index 9829ebdc7674..412d237154f8 100644
--- a/src/ansi-c/padding.cpp
+++ b/src/ansi-c/padding.cpp
@@ -251,7 +251,7 @@ static void add_padding_msvc(struct_typet &type, const namespacet &ns)
       {
         // keep track of offset
         const auto size = pointer_offset_size(it->type(), ns);
-        if(size.has_value() && *size >= 1)
+        if(size.has_value() && *size >= bytest{1})
           offset += *size;
       }
     }
@@ -468,7 +468,7 @@ void add_padding(union_typet &type, const namespacet &ns)
 {
   mp_integer max_alignment_bits =
     alignment(type, ns) * config.ansi_c.char_width;
-  mp_integer size_bits=0;
+  bitst size_bits{0};
 
   // check per component, and ignore those without fixed size
   for(const auto &c : type.components())
diff --git a/src/cprover/bv_pointers_wide.cpp b/src/cprover/bv_pointers_wide.cpp
index bef36abb1010..0702acea5e82 100644
--- a/src/cprover/bv_pointers_wide.cpp
+++ b/src/cprover/bv_pointers_wide.cpp
@@ -209,7 +209,7 @@ optionalt<bvt> bv_pointers_widet::convert_address_of_rec(const exprt &expr)
 
     // get size
     auto size = pointer_offset_size(array_type.element_type(), ns);
-    CHECK_RETURN(size.has_value() && *size >= 0);
+    CHECK_RETURN(size.has_value() && *size >= bytest{0});
 
     bv = offset_arithmetic(type, bv, *size, index);
     CHECK_RETURN(bv.size() == bits);
@@ -424,7 +424,7 @@ bvt bv_pointers_widet::convert_pointer_type(const exprt &expr)
         else
         {
           auto size_opt = pointer_offset_size(pointer_base_type, ns);
-          CHECK_RETURN(size_opt.has_value() && *size_opt >= 0);
+          CHECK_RETURN(size_opt.has_value() && *size_opt >= bytest{0});
           size = *size_opt;
         }
       }
@@ -495,7 +495,8 @@ bvt bv_pointers_widet::convert_pointer_type(const exprt &expr)
     else
     {
       auto element_size_opt = pointer_offset_size(pointer_base_type, ns);
-      CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
+      CHECK_RETURN(
+        element_size_opt.has_value() && *element_size_opt > bytest{0});
       element_size = *element_size_opt;
     }
 
@@ -550,7 +551,7 @@ bvt bv_pointers_widet::convert_pointer_type(const exprt &expr)
 
     // get element size
     auto size = pointer_offset_size(element_address_expr.element_type(), ns);
-    CHECK_RETURN(size.has_value() && *size >= 0);
+    CHECK_RETURN(size.has_value() && *size >= bytest{0});
 
     // add offset
     bv = offset_arithmetic(
@@ -637,9 +638,10 @@ bvt bv_pointers_widet::convert_bitvector(const exprt &expr)
       if(lhs_pt.base_type().id() != ID_empty)
       {
         auto element_size_opt = pointer_offset_size(lhs_pt.base_type(), ns);
-        CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
+        CHECK_RETURN(
+          element_size_opt.has_value() && *element_size_opt > bytest{0});
 
-        if(*element_size_opt != 1)
+        if(*element_size_opt != bytest{1})
         {
           bvt element_size_bv =
             bv_utils.build_constant(*element_size_opt, width);
@@ -790,7 +792,7 @@ exprt bv_pointers_widet::bv_get_rec(
 
   pointer_logict::pointert pointer{
     numeric_cast_v<std::size_t>(binary2integer(value_addr, false)),
-    binary2integer(value_offset, true)};
+    bytest{binary2integer(value_offset, true)}};
 
   return annotated_pointer_constant_exprt{
     bvrep, pointer_logic.pointer_expr(pointer, pt)};
diff --git a/src/cprover/endianness_map_wide.cpp b/src/cprover/endianness_map_wide.cpp
index f3d2d03229d7..77c312942812 100644
--- a/src/cprover/endianness_map_wide.cpp
+++ b/src/cprover/endianness_map_wide.cpp
@@ -18,7 +18,7 @@ void endianness_map_widet::build_little_endian(const typet &src)
   {
     auto s = pointer_offset_bits(src, ns);
     CHECK_RETURN(s.has_value());
-    s.value() = s.value() * 2;
+    s.value() = bitst{s.value() * 2};
 
     const std::size_t new_size = map.size() + numeric_cast_v<std::size_t>(*s);
     map.reserve(new_size);
diff --git a/src/goto-instrument/count_eloc.cpp b/src/goto-instrument/count_eloc.cpp
index 51bf3e825d4c..66ac213e245d 100644
--- a/src/goto-instrument/count_eloc.cpp
+++ b/src/goto-instrument/count_eloc.cpp
@@ -185,7 +185,7 @@ void print_global_state_size(const goto_modelt &goto_model)
     }
   }
 
-  mp_integer total_size = 0;
+  bitst total_size{0};
 
   for(const auto &symbol_entry : goto_model.symbol_table.symbols)
   {
@@ -200,7 +200,7 @@ void print_global_state_size(const goto_modelt &goto_model)
     }
 
     const auto bits = pointer_offset_bits(symbol.type, ns);
-    if(bits.has_value() && bits.value() > 0)
+    if(bits.has_value() && bits.value() > bitst{0})
       total_size += bits.value();
   }
 
diff --git a/src/goto-programs/interpreter_class.h b/src/goto-programs/interpreter_class.h
index 425934e87faf..dd574ed3973b 100644
--- a/src/goto-programs/interpreter_class.h
+++ b/src/goto-programs/interpreter_class.h
@@ -287,7 +287,7 @@ class interpretert
 
   bool byte_offset_to_memory_offset(
     const typet &source_type,
-    const mp_integer &byte_offset,
+    const bytest &byte_offset,
     mp_integer &result);
 
   bool memory_offset_to_byte_offset(
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
index 209737e06d66..addab5562db4 100644
--- a/src/goto-programs/interpreter_evaluate.cpp
+++ b/src/goto-programs/interpreter_evaluate.cpp
@@ -159,7 +159,7 @@ bool interpretert::count_type_leaves(const typet &ty, mp_integer &result)
 /// \return Offset into a vector of interpreter values; returns true on error
 bool interpretert::byte_offset_to_memory_offset(
   const typet &source_type,
-  const mp_integer &offset,
+  const bytest &offset,
   mp_integer &result)
 {
   if(source_type.id()==ID_struct)
@@ -206,7 +206,7 @@ bool interpretert::byte_offset_to_memory_offset(
 
     mp_integer array_size=array_size_vec[0];
     auto elem_size_bytes = pointer_offset_size(at.element_type(), ns);
-    if(!elem_size_bytes.has_value() || *elem_size_bytes == 0)
+    if(!elem_size_bytes.has_value() || *elem_size_bytes == bytest{0})
       return true;
 
     mp_integer elem_size_leaves;
@@ -228,7 +228,7 @@ bool interpretert::byte_offset_to_memory_offset(
   {
     result=0;
     // Can't currently subdivide a primitive.
-    return offset!=0;
+    return offset != bytest{0};
   }
 }
 
@@ -1071,7 +1071,9 @@ mp_integer interpretert::evaluate_address(
     {
       mp_integer memory_offset;
       if(!byte_offset_to_memory_offset(
-           byte_extract_expr.op0().type(), extract_offset[0], memory_offset))
+           byte_extract_expr.op0().type(),
+           bytest{extract_offset[0]},
+           memory_offset))
         return evaluate_address(byte_extract_expr.op0(), fail_quietly) +
                memory_offset;
     }
diff --git a/src/goto-programs/vcd_goto_trace.cpp b/src/goto-programs/vcd_goto_trace.cpp
index e012fc4e1779..6a5e89fd8d5c 100644
--- a/src/goto-programs/vcd_goto_trace.cpp
+++ b/src/goto-programs/vcd_goto_trace.cpp
@@ -100,7 +100,7 @@ void output_vcd(
 
         const auto width = pointer_offset_bits(type, ns);
 
-        if(width.has_value() && (*width) >= 1)
+        if(width.has_value() && (*width) >= bitst{1})
           out << "$var reg " << (*width) << " V" << number << " " << identifier
               << " $end"
               << "\n";
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index 1c7783a92492..f284ecca4393 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -83,9 +83,9 @@ void goto_symext::symex_allocate(
       {
         // Did the size get multiplied?
         auto elem_size = pointer_offset_size(*tmp_type, ns);
-        const auto alloc_size = numeric_cast<mp_integer>(tmp_size);
+        const auto alloc_size = numeric_cast<bytest>(tmp_size);
 
-        if(!elem_size.has_value() || *elem_size==0)
+        if(!elem_size.has_value() || *elem_size == bytest{0})
         {
         }
         else if(
diff --git a/src/memory-analyzer/analyze_symbol.cpp b/src/memory-analyzer/analyze_symbol.cpp
index 2bcad763224e..7b1b3a68e97d 100644
--- a/src/memory-analyzer/analyze_symbol.cpp
+++ b/src/memory-analyzer/analyze_symbol.cpp
@@ -325,7 +325,7 @@ exprt gdb_value_extractort::get_pointer_to_member_value(
 
   const auto maybe_member_expr = get_subexpression_at_offset(
     struct_symbol_expr,
-    member_offset,
+    bytest{member_offset},
     to_pointer_type(expr.type()).base_type(),
     ns);
   DATA_INVARIANT(
@@ -554,7 +554,10 @@ exprt gdb_value_extractort::get_pointer_value(
     if(target_expr.type().id() == ID_array)
     {
       const auto result_indexed_expr = get_subexpression_at_offset(
-        target_expr, 0, to_pointer_type(zero_expr.type()).base_type(), ns);
+        target_expr,
+        bytest{0},
+        to_pointer_type(zero_expr.type()).base_type(),
+        ns);
       CHECK_RETURN(result_indexed_expr.has_value());
       if(result_indexed_expr->type() == zero_expr.type())
         return *result_indexed_expr;
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 16385e2993a3..fdb553f94f23 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -314,7 +314,7 @@ bool value_sett::eval_pointer_offset(
       get_value_set(to_pointer_offset_expr(expr).pointer(), ns, true);
 
     exprt new_expr;
-    mp_integer previous_offset=0;
+    bytest previous_offset{0};
 
     const object_map_dt &object_map=reference_set.read();
     for(object_map_dt::const_iterator
@@ -568,7 +568,7 @@ void value_sett::get_value_set_rec(
       insert(
         dest,
         exprt(ID_null_object, to_pointer_type(expr_type).base_type()),
-        mp_integer{0});
+        bytest{0});
     }
     else if(expr_type.id()==ID_unsignedbv ||
             expr_type.id()==ID_signedbv)
@@ -599,7 +599,7 @@ void value_sett::get_value_set_rec(
 
       if(op.is_zero())
       {
-        insert(dest, exprt(ID_null_object, empty_typet{}), mp_integer{0});
+        insert(dest, exprt(ID_null_object, empty_typet{}), bytest{0});
       }
       else
       {
@@ -686,7 +686,7 @@ void value_sett::get_value_set_rec(
 
         auto size = pointer_offset_size(pointer_base_type, ns);
 
-        if(!size.has_value() || (*size) == 0)
+        if(!size.has_value() || (*size) == bytest{0})
         {
           i.reset();
         }
@@ -728,7 +728,7 @@ void value_sett::get_value_set_rec(
 
       // adjust by offset
       if(offset && i.has_value())
-        *offset += *i;
+        *offset += bytest{*i};
       else
         offset.reset();
 
@@ -802,7 +802,7 @@ void value_sett::get_value_set_rec(
       dynamic_object.set_instance(location_number);
       dynamic_object.valid()=true_exprt();
 
-      insert(dest, dynamic_object, mp_integer{0});
+      insert(dest, dynamic_object, bytest{0});
     }
     else if(statement==ID_cpp_new ||
             statement==ID_cpp_new_array)
@@ -815,7 +815,7 @@ void value_sett::get_value_set_rec(
       dynamic_object.set_instance(location_number);
       dynamic_object.valid()=true_exprt();
 
-      insert(dest, dynamic_object, mp_integer{0});
+      insert(dest, dynamic_object, bytest{0});
     }
     else
       insert(dest, exprt(ID_unknown, original_type));
@@ -1146,7 +1146,7 @@ void value_sett::get_reference_set_rec(
       to_array_type(expr.type()).element_type().id() == ID_array)
       insert(dest, expr);
     else
-      insert(dest, expr, mp_integer{0});
+      insert(dest, expr, bytest{0});
 
     return;
   }
@@ -1173,7 +1173,7 @@ void value_sett::get_reference_set_rec(
 
     const index_exprt &index_expr=to_index_expr(expr);
     const exprt &array=index_expr.array();
-    const exprt &offset=index_expr.index();
+    const exprt &index = index_expr.index();
 
     DATA_INVARIANT(
       array.type().id() == ID_array, "index takes array-typed operand");
@@ -1201,19 +1201,19 @@ void value_sett::get_reference_set_rec(
           from_integer(0, c_index_type()));
 
         offsett o = a_it->second;
-        const auto i = numeric_cast<mp_integer>(offset);
+        const auto i = numeric_cast<mp_integer>(index);
 
-        if(offset.is_zero())
+        if(index.is_zero())
         {
         }
         else if(i.has_value() && o)
         {
           auto size = pointer_offset_size(array_type.element_type(), ns);
 
-          if(!size.has_value() || *size == 0)
+          if(!size.has_value() || *size == bytest{0})
             o.reset();
           else
-            *o = *i * (*size);
+            *o = bytest{*i * (*size)};
         }
         else
           o.reset();
diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h
index ac493488d39f..0504a98bb37a 100644
--- a/src/pointer-analysis/value_set.h
+++ b/src/pointer-analysis/value_set.h
@@ -77,7 +77,7 @@ class value_sett
 
   /// Represents the offset into an object: either a unique integer offset,
   /// or an unknown value, represented by `!offset`.
-  typedef optionalt<mp_integer> offsett;
+  typedef optionalt<bytest> offsett;
 
   /// Represents a set of expressions (`exprt` instances) with corresponding
   /// offsets (`offsett` instances). This is the RHS set of a single row of
@@ -145,10 +145,8 @@ class value_sett
   /// \param dest: object map to update
   /// \param src: expression to add
   /// \param offset_value: offset into `src`
-  bool insert(
-    object_mapt &dest,
-    const exprt &src,
-    const mp_integer &offset_value) const
+  bool
+  insert(object_mapt &dest, const exprt &src, const bytest &offset_value) const
   {
     return insert(dest, object_numbering.number(src), offsett(offset_value));
   }
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index 6b082e63b4e7..beda0148a811 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -613,12 +613,11 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
       auto element_size =
         pointer_offset_size(to_array_type(root_object_type).element_type(), ns);
       CHECK_RETURN(element_size.has_value());
-      CHECK_RETURN(*element_size > 0);
+      CHECK_RETURN(*element_size > bytest{0});
 
-      const auto offset_int =
-        numeric_cast_v<mp_integer>(to_constant_expr(offset));
+      const auto offset_int = numeric_cast_v<bytest>(to_constant_expr(offset));
 
-      if(offset_int % *element_size == 0)
+      if(offset_int % *element_size == bytest{0})
       {
         index_exprt index_expr{
           root_object,
@@ -755,14 +754,14 @@ bool value_set_dereferencet::memory_model_bytes(
   auto from_type_element_type_size =
     from_type.id() == ID_array
       ? pointer_offset_size(to_array_type(from_type).element_type(), ns)
-      : optionalt<mp_integer>{};
+      : optionalt<bytest>{};
 
   auto to_type_size = pointer_offset_size(to_type, ns);
 
   if(
     from_type.id() == ID_array && from_type_element_type_size.has_value() &&
-    *from_type_element_type_size == 1 && to_type_size.has_value() &&
-    *to_type_size == 1 &&
+    *from_type_element_type_size == bytest{1} && to_type_size.has_value() &&
+    *to_type_size == bytest{1} &&
     is_a_bv_type(to_array_type(from_type).element_type()) &&
     is_a_bv_type(to_type))
   {
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index ce2d5a2943ed..a787047973f2 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -457,7 +457,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
         else
         {
           auto size_opt = pointer_offset_size(pointer_base_type, ns);
-          CHECK_RETURN(size_opt.has_value() && *size_opt >= 0);
+          CHECK_RETURN(size_opt.has_value() && *size_opt >= bytest{0});
           size = *size_opt;
         }
       }
@@ -530,7 +530,8 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
     else
     {
       auto element_size_opt = pointer_offset_size(pointer_base_type, ns);
-      CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
+      CHECK_RETURN(
+        element_size_opt.has_value() && *element_size_opt > bytest{0});
       element_size = *element_size_opt;
     }
 
@@ -584,7 +585,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
 
     // get element size
     auto size = pointer_offset_size(element_address_expr.element_type(), ns);
-    CHECK_RETURN(size.has_value() && *size >= 0);
+    CHECK_RETURN(size.has_value() && *size >= bytest{0});
 
     // add offset
     bv = offset_arithmetic(
@@ -668,9 +669,10 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
       if(lhs_pt.base_type().id() != ID_empty)
       {
         auto element_size_opt = pointer_offset_size(lhs_pt.base_type(), ns);
-        CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
+        CHECK_RETURN(
+          element_size_opt.has_value() && *element_size_opt > bytest{0});
 
-        if(*element_size_opt != 1)
+        if(*element_size_opt != bytest{1})
         {
           bvt element_size_bv =
             bv_utils.build_constant(*element_size_opt, width);
@@ -797,7 +799,7 @@ exprt bv_pointerst::bv_get_rec(
 
   pointer_logict::pointert pointer{
     numeric_cast_v<std::size_t>(binary2integer(value_addr, false)),
-    binary2integer(value_offset, true)};
+    bytest{binary2integer(value_offset, true)}};
 
   return annotated_pointer_constant_exprt{
     bvrep, pointer_logic.pointer_expr(pointer, pt)};
diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp
index 348525ef0fd4..6d6f96692dd0 100644
--- a/src/solvers/flattening/pointer_logic.cpp
+++ b/src/solvers/flattening/pointer_logic.cpp
@@ -61,7 +61,7 @@ exprt pointer_logict::pointer_expr(
   const mp_integer &object,
   const pointer_typet &type) const
 {
-  return pointer_expr({object, 0}, type);
+  return pointer_expr({object, bytest{0}}, type);
 }
 
 exprt pointer_logict::pointer_expr(
@@ -70,7 +70,7 @@ exprt pointer_logict::pointer_expr(
 {
   if(pointer.object==null_object) // NULL?
   {
-    if(pointer.offset==0)
+    if(pointer.offset == bytest{0})
     {
       return null_pointer_exprt(type);
     }
@@ -132,13 +132,13 @@ exprt pointer_logict::pointer_expr(
     return typecast_exprt::conditional_cast(base, type);
 
   const auto object_size = pointer_offset_size(be.op().type(), ns);
-  if(object_size.has_value() && *object_size <= 1)
+  if(object_size.has_value() && *object_size <= bytest{1})
   {
     return typecast_exprt::conditional_cast(
       plus_exprt(base, from_integer(pointer.offset, pointer_diff_type())),
       type);
   }
-  else if(object_size.has_value() && pointer.offset % *object_size == 0)
+  else if(object_size.has_value() && pointer.offset % *object_size == bytest{0})
   {
     return typecast_exprt::conditional_cast(
       plus_exprt(
diff --git a/src/solvers/flattening/pointer_logic.h b/src/solvers/flattening/pointer_logic.h
index bcfd97b7a1f7..ec8a340713b0 100644
--- a/src/solvers/flattening/pointer_logic.h
+++ b/src/solvers/flattening/pointer_logic.h
@@ -27,9 +27,10 @@ class pointer_logict
 
   struct pointert
   {
-    mp_integer object, offset;
+    mp_integer object;
+    bytest offset;
 
-    pointert(mp_integer _obj, mp_integer _off)
+    pointert(mp_integer _obj, bytest _off)
       : object(std::move(_obj)), offset(std::move(_off))
     {
     }
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index ce53dc704ece..9b15b7b0c7c9 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -247,7 +247,7 @@ void smt2_convt::define_object_size(
     const typet &type = o.type();
     auto size_expr = size_of_expr(type, ns);
     const auto object_size =
-      numeric_cast<mp_integer>(size_expr.value_or(nil_exprt()));
+      numeric_cast<bytest>(size_expr.value_or(nil_exprt()));
 
     if(
       (o.id() != ID_symbol && o.id() != ID_string_constant) ||
@@ -659,7 +659,8 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &type)
 
     // split into object and offset
     mp_integer pow=power(2, width-config.bv_encoding.object_bits);
-    pointer_logict::pointert ptr{numeric_cast_v<std::size_t>(v / pow), v % pow};
+    pointer_logict::pointert ptr{
+      numeric_cast_v<std::size_t>(v / pow), bytest{v % pow}};
     return annotated_pointer_constant_exprt(
       bv_expr.get_value(),
       pointer_logic.pointer_expr(ptr, to_pointer_type(type)));
@@ -758,7 +759,7 @@ void smt2_convt::convert_address_of_rec(
     const irep_idt &component_name = member_expr.get_component_name();
 
     const auto offset = member_offset(struct_type, component_name, ns);
-    CHECK_RETURN(offset.has_value() && *offset >= 0);
+    CHECK_RETURN(offset.has_value() && *offset >= bytest{0});
 
     unsignedbv_typet index_type(boolbv_width(result_type));
 
@@ -1581,8 +1582,8 @@ void smt2_convt::convert_expr(const exprt &expr)
 
       if(shift_expr.distance().type().id() == ID_integer)
       {
-        const mp_integer i =
-          numeric_cast_v<mp_integer>(to_constant_expr(shift_expr.distance()));
+        const auto i =
+          numeric_cast_v<bitst>(to_constant_expr(shift_expr.distance()));
 
         // shift distance must be bit vector
         std::size_t width_op0 = boolbv_width(shift_expr.op().type());
@@ -1645,7 +1646,7 @@ void smt2_convt::convert_expr(const exprt &expr)
 
       out << ' ';
 
-      auto distance_int_op = numeric_cast<mp_integer>(shift_expr.distance());
+      auto distance_int_op = numeric_cast<bitst>(shift_expr.distance());
 
       if(distance_int_op.has_value())
       {
@@ -1797,8 +1798,8 @@ void smt2_convt::convert_expr(const exprt &expr)
 
     if(extractbit_expr.index().is_constant())
     {
-      const mp_integer i =
-        numeric_cast_v<mp_integer>(to_constant_expr(extractbit_expr.index()));
+      const auto i =
+        numeric_cast_v<bitst>(to_constant_expr(extractbit_expr.index()));
 
       out << "(= ((_ extract " << i << " " << i << ") ";
       flatten2bv(extractbit_expr.src());
@@ -1823,10 +1824,10 @@ void smt2_convt::convert_expr(const exprt &expr)
       extractbits_expr.upper().is_constant() &&
       extractbits_expr.lower().is_constant())
     {
-      mp_integer op1_i =
-        numeric_cast_v<mp_integer>(to_constant_expr(extractbits_expr.upper()));
-      mp_integer op2_i =
-        numeric_cast_v<mp_integer>(to_constant_expr(extractbits_expr.lower()));
+      auto op1_i =
+        numeric_cast_v<bitst>(to_constant_expr(extractbits_expr.upper()));
+      auto op2_i =
+        numeric_cast_v<bitst>(to_constant_expr(extractbits_expr.lower()));
 
       if(op2_i>op1_i)
         std::swap(op1_i, op2_i);
@@ -3702,17 +3703,14 @@ void smt2_convt::convert_plus(const plus_exprt &expr)
 
       const auto &base_type = to_pointer_type(expr.type()).base_type();
 
-      mp_integer element_size;
-      if(base_type.id() == ID_empty)
-      {
-        // This is a gcc extension.
-        // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
-        element_size = 1;
-      }
-      else
+      // void pointers are a gcc extension.
+      // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
+      bytest element_size{1};
+      if(base_type.id() != ID_empty)
       {
         auto element_size_opt = pointer_offset_size(base_type, ns);
-        CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 0);
+        CHECK_RETURN(
+          element_size_opt.has_value() && *element_size_opt >= bytest{0});
         element_size = *element_size_opt;
       }
 
@@ -3731,7 +3729,7 @@ void smt2_convt::convert_plus(const plus_exprt &expr)
           << ") ?pointerop) ";
       out << "(bvadd ((_ extract " << offset_bits - 1 << " 0) ?pointerop) ";
 
-      if(element_size >= 2)
+      if(element_size >= bytest{2})
       {
         out << "(bvmul ((_ extract " << offset_bits - 1 << " 0) ";
         convert_expr(i);
@@ -3911,22 +3909,18 @@ void smt2_convt::convert_minus(const minus_exprt &expr)
     {
       // Pointer difference
       const auto &base_type = to_pointer_type(expr.op0().type()).base_type();
-      mp_integer element_size;
-
-      if(base_type.id() == ID_empty)
-      {
-        // Pointer arithmetic on void is a gcc extension.
-        // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
-        element_size = 1;
-      }
-      else
+      // void pointers are a gcc extension.
+      // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
+      bytest element_size{1};
+      if(base_type.id() != ID_empty)
       {
         auto element_size_opt = pointer_offset_size(base_type, ns);
-        CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 1);
+        CHECK_RETURN(
+          element_size_opt.has_value() && *element_size_opt >= bytest{1});
         element_size = *element_size_opt;
       }
 
-      if(element_size >= 2)
+      if(element_size >= bytest{2})
         out << "(bvsdiv ";
 
       INVARIANT(
@@ -3940,7 +3934,7 @@ void smt2_convt::convert_minus(const minus_exprt &expr)
       convert_expr(expr.op1());
       out << ")";
 
-      if(element_size >= 2)
+      if(element_size >= bytest{2})
         out << " (_ bv" << element_size << " " << boolbv_width(expr.type())
             << "))";
     }
diff --git a/src/util/arith_tools.h b/src/util/arith_tools.h
index 4f67c810b925..9044e1531b43 100644
--- a/src/util/arith_tools.h
+++ b/src/util/arith_tools.h
@@ -55,6 +55,48 @@ struct numeric_castt<mp_integer> final
   }
 };
 
+template <>
+struct numeric_castt<bitst> final
+{
+  optionalt<bitst> operator()(const exprt &expr) const
+  {
+    if(expr.id() != ID_constant)
+      return {};
+    else
+      return operator()(to_constant_expr(expr));
+  }
+
+  optionalt<bitst> operator()(const constant_exprt &expr) const
+  {
+    mp_integer out;
+    if(to_integer(expr, out))
+      return {};
+    else
+      return bitst{out};
+  }
+};
+
+template <>
+struct numeric_castt<bytest> final
+{
+  optionalt<bytest> operator()(const exprt &expr) const
+  {
+    if(expr.id() != ID_constant)
+      return {};
+    else
+      return operator()(to_constant_expr(expr));
+  }
+
+  optionalt<bytest> operator()(const constant_exprt &expr) const
+  {
+    mp_integer out;
+    if(to_integer(expr, out))
+      return {};
+    else
+      return bytest{out};
+  }
+};
+
 /// Convert mp_integer or expr to any integral type
 template <typename T>
 struct numeric_castt<T,
diff --git a/src/util/c_types.cpp b/src/util/c_types.cpp
index c89435686114..c1392180dd55 100644
--- a/src/util/c_types.cpp
+++ b/src/util/c_types.cpp
@@ -301,12 +301,12 @@ std::string c_type_as_string(const irep_idt &c_type)
     return "";
 }
 
-optionalt<std::pair<struct_union_typet::componentt, mp_integer>>
+optionalt<std::pair<struct_union_typet::componentt, bitst>>
 union_typet::find_widest_union_component(const namespacet &ns) const
 {
   const union_typet::componentst &comps = components();
 
-  optionalt<mp_integer> max_width;
+  optionalt<bitst> max_width;
   typet max_comp_type;
   irep_idt max_comp_name;
 
diff --git a/src/util/c_types.h b/src/util/c_types.h
index 00460e56f27c..4c8d9b1a45fe 100644
--- a/src/util/c_types.h
+++ b/src/util/c_types.h
@@ -138,7 +138,7 @@ class union_typet : public struct_union_typet
   /// \param ns: Namespace to resolve tag types.
   /// \return Pair of a componentt pointing to the maximum fixed bit-width
   ///   member of the union type and the bit width of that member.
-  optionalt<std::pair<struct_union_typet::componentt, mp_integer>>
+  optionalt<std::pair<struct_union_typet::componentt, bitst>>
   find_widest_union_component(const namespacet &ns) const;
 };
 
diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp
index ead31db6ee91..253584449811 100644
--- a/src/util/expr_util.cpp
+++ b/src/util/expr_util.cpp
@@ -261,9 +261,9 @@ bool is_constantt::is_constant(const exprt &expr) const
     if(!extract_bits.has_value())
       return false;
 
-    const mp_integer offset_bits =
+    const bitst offset_bits{
       numeric_cast_v<mp_integer>(to_constant_expr(be->offset())) *
-      be->get_bits_per_byte();
+      be->get_bits_per_byte()};
 
     return offset_bits + *extract_bits <= *op_bits;
   }
@@ -280,12 +280,12 @@ bool is_constantt::is_constant(const exprt &expr) const
     if(!src_bits.has_value())
       return false;
 
-    const mp_integer lower_bound =
-      numeric_cast_v<mp_integer>(to_constant_expr(eb->lower()));
-    const mp_integer upper_bound =
-      numeric_cast_v<mp_integer>(to_constant_expr(eb->upper()));
+    const bitst lower_bound =
+      numeric_cast_v<bitst>(to_constant_expr(eb->lower()));
+    const bitst upper_bound =
+      numeric_cast_v<bitst>(to_constant_expr(eb->upper()));
 
-    return lower_bound >= 0 && lower_bound <= upper_bound &&
+    return lower_bound >= bitst{0} && lower_bound <= upper_bound &&
            upper_bound < src_bits;
   }
 
diff --git a/src/util/lower_byte_operators.cpp b/src/util/lower_byte_operators.cpp
index 807089d20b50..7a597bd97e64 100644
--- a/src/util/lower_byte_operators.cpp
+++ b/src/util/lower_byte_operators.cpp
@@ -185,7 +185,7 @@ static array_exprt bv_to_array_expr(
     to_bitvector_type(bitvector_expr.type()).get_width();
   if(!num_elements.has_value())
   {
-    if(!subtype_bits.has_value() || *subtype_bits == 0)
+    if(!subtype_bits.has_value() || *subtype_bits == bitst{0})
       num_elements = total_bits;
     else
       num_elements = total_bits / numeric_cast_v<std::size_t>(*subtype_bits);
@@ -404,8 +404,8 @@ static exprt bv_to_expr(
 static exprt unpack_rec(
   const exprt &src,
   bool little_endian,
-  const optionalt<mp_integer> &offset_bytes,
-  const optionalt<mp_integer> &max_bytes,
+  const optionalt<bytest> &offset_bytes,
+  const optionalt<bytest> &max_bytes,
   const std::size_t bits_per_byte,
   const namespacet &ns,
   bool unpack_byte_array = false);
@@ -526,10 +526,10 @@ static exprt unpack_array_vector_no_known_bounds(
 static exprt unpack_array_vector(
   const exprt &src,
   const optionalt<mp_integer> &src_size,
-  const mp_integer &element_bits,
+  const bitst &element_bits,
   bool little_endian,
-  const optionalt<mp_integer> &offset_bytes,
-  const optionalt<mp_integer> &max_bytes,
+  const optionalt<bytest> &offset_bytes,
+  const optionalt<bytest> &max_bytes,
   const std::size_t bits_per_byte,
   const namespacet &ns)
 {
@@ -550,8 +550,10 @@ static exprt unpack_array_vector(
 
   // refine the number of elements to extract in case the element width is known
   // and a multiple of bytes; otherwise we will expand the entire array/vector
-  optionalt<mp_integer> num_elements = src_size;
-  if(element_bits > 0 && element_bits % bits_per_byte == 0)
+  optionalt<mp_integer> num_elements;
+  if(src_size.has_value())
+    num_elements = *src_size;
+  if(element_bits > bitst{0} && element_bits % bits_per_byte == 0)
   {
     if(!num_elements.has_value())
     {
@@ -597,10 +599,10 @@ static exprt unpack_array_vector(
     // recursively unpack each element so that we eventually just have an array
     // of bytes left
 
-    const optionalt<mp_integer> element_max_bytes =
+    const optionalt<bytest> element_max_bytes =
       max_bytes
-        ? std::min(mp_integer{el_bytes}, *max_bytes - byte_operands.size())
-        : optionalt<mp_integer>{};
+        ? std::min(bytest{el_bytes}, *max_bytes - bytest{byte_operands.size()})
+        : optionalt<bytest>{};
     const std::size_t element_max_bytes_int =
       element_max_bytes ? numeric_cast_v<std::size_t>(*element_max_bytes)
                         : el_bytes;
@@ -638,8 +640,8 @@ static void process_bit_fields(
   std::size_t total_bits,
   exprt::operandst &dest,
   bool little_endian,
-  const optionalt<mp_integer> &offset_bytes,
-  const optionalt<mp_integer> &max_bytes,
+  const optionalt<bytest> &offset_bytes,
+  const optionalt<bytest> &max_bytes,
   const std::size_t bits_per_byte,
   const namespacet &ns)
 {
@@ -674,19 +676,19 @@ static void process_bit_fields(
 static array_exprt unpack_struct(
   const exprt &src,
   bool little_endian,
-  const optionalt<mp_integer> &offset_bytes,
-  const optionalt<mp_integer> &max_bytes,
+  const optionalt<bytest> &offset_bytes,
+  const optionalt<bytest> &max_bytes,
   const std::size_t bits_per_byte,
   const namespacet &ns)
 {
   const struct_typet &struct_type = to_struct_type(ns.follow(src.type()));
   const struct_typet::componentst &components = struct_type.components();
 
-  optionalt<mp_integer> offset_in_member;
-  optionalt<mp_integer> max_bytes_left;
+  optionalt<bytest> offset_in_member;
+  optionalt<bytest> max_bytes_left;
   optionalt<std::pair<exprt::operandst, std::size_t>> bit_fields;
 
-  mp_integer member_offset_bits = 0;
+  bitst member_offset_bits{0};
   exprt::operandst byte_operands;
   for(auto it = components.begin(); it != components.end(); ++it)
   {
@@ -726,17 +728,19 @@ static array_exprt unpack_struct(
 
       if(offset_bytes.has_value())
       {
-        offset_in_member = *offset_bytes - member_offset_bits / bits_per_byte;
+        offset_in_member =
+          *offset_bytes - bytest{member_offset_bits / bits_per_byte};
         // if the offset is negative, offset_in_member remains unset, which has
         // the same effect as setting it to zero
-        if(*offset_in_member < 0)
+        if(*offset_in_member < bytest{0})
           offset_in_member.reset();
       }
 
       if(max_bytes.has_value())
       {
-        max_bytes_left = *max_bytes - member_offset_bits / bits_per_byte;
-        if(*max_bytes_left < 0)
+        max_bytes_left =
+          *max_bytes - bytest{member_offset_bits / bits_per_byte};
+        if(*max_bytes_left < bytest{0})
           break;
       }
     }
@@ -822,8 +826,8 @@ static array_exprt unpack_complex(
   exprt sub_real = unpack_rec(
     complex_real_exprt{src},
     little_endian,
-    mp_integer{0},
-    *subtype_bits / bits_per_byte,
+    bytest{0},
+    bytest{*subtype_bits / bits_per_byte},
     bits_per_byte,
     ns,
     true);
@@ -832,8 +836,8 @@ static array_exprt unpack_complex(
   exprt sub_imag = unpack_rec(
     complex_imag_exprt{src},
     little_endian,
-    mp_integer{0},
-    *subtype_bits / bits_per_byte,
+    bytest{0},
+    bytest{*subtype_bits / bits_per_byte},
     bits_per_byte,
     ns,
     true);
@@ -863,8 +867,8 @@ static array_exprt unpack_complex(
 static exprt unpack_rec(
   const exprt &src,
   bool little_endian,
-  const optionalt<mp_integer> &offset_bytes,
-  const optionalt<mp_integer> &max_bytes,
+  const optionalt<bytest> &offset_bytes,
+  const optionalt<bytest> &max_bytes,
   const std::size_t bits_per_byte,
   const namespacet &ns,
   bool unpack_byte_array)
@@ -877,7 +881,7 @@ static exprt unpack_rec(
     auto element_bits = pointer_offset_bits(subtype, ns);
     CHECK_RETURN(element_bits.has_value());
 
-    if(!unpack_byte_array && *element_bits == bits_per_byte)
+    if(!unpack_byte_array && *element_bits == bitst{bits_per_byte})
       return src;
 
     const auto constant_size_opt = numeric_cast<mp_integer>(array_type.size());
@@ -899,7 +903,7 @@ static exprt unpack_rec(
     auto element_bits = pointer_offset_bits(subtype, ns);
     CHECK_RETURN(element_bits.has_value());
 
-    if(!unpack_byte_array && *element_bits == bits_per_byte)
+    if(!unpack_byte_array && *element_bits == bitst{bits_per_byte})
       return src;
 
     return unpack_array_vector(
@@ -935,7 +939,7 @@ static exprt unpack_rec(
         member,
         little_endian,
         offset_bytes,
-        (widest_member->second + bits_per_byte - 1) / bits_per_byte,
+        bytest{(widest_member->second + bits_per_byte - 1) / bits_per_byte},
         bits_per_byte,
         ns,
         true);
@@ -993,20 +997,20 @@ static exprt unpack_rec(
     auto bits_opt = pointer_offset_bits(src.type(), ns);
     DATA_INVARIANT(bits_opt.has_value(), "basic type should have a fixed size");
 
-    const mp_integer total_bits = *bits_opt;
-    mp_integer last_bit = total_bits;
-    mp_integer bit_offset = 0;
+    const bitst total_bits = *bits_opt;
+    bitst last_bit = total_bits;
+    bitst bit_offset{0};
 
     if(max_bytes.has_value())
     {
-      const auto max_bits = *max_bytes * bits_per_byte;
+      const auto max_bits = bitst{*max_bytes * bits_per_byte};
       if(little_endian)
       {
         last_bit = std::min(last_bit, max_bits);
       }
       else
       {
-        bit_offset = std::max(mp_integer{0}, last_bit - max_bits);
+        bit_offset = std::max(bitst{0}, last_bit - max_bits);
       }
     }
 
@@ -1014,7 +1018,7 @@ static exprt unpack_rec(
       src, bv_typet{numeric_cast_v<std::size_t>(total_bits)});
     auto const byte_type = bv_typet{bits_per_byte};
     exprt::operandst byte_operands;
-    for(; bit_offset < last_bit; bit_offset += bits_per_byte)
+    for(; bit_offset < last_bit; bit_offset += bitst{bits_per_byte})
     {
       PRECONDITION(
         pointer_offset_bits(src_as_bitvector.type(), ns).has_value());
@@ -1057,7 +1061,7 @@ static exprt lower_byte_extract_array_vector(
   const byte_extract_exprt &src,
   const byte_extract_exprt &unpacked,
   const typet &subtype,
-  const mp_integer &element_bits,
+  const bitst &element_bits,
   const namespacet &ns)
 {
   optionalt<std::size_t> num_elements;
@@ -1232,9 +1236,9 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
   else if(src.type().id() == ID_empty)
     upper_bound_opt = from_integer(0, size_type());
 
-  const auto lower_bound_int_opt = numeric_cast<mp_integer>(src.offset());
+  const auto lower_bound_int_opt = numeric_cast<bytest>(src.offset());
   const auto upper_bound_int_opt =
-    numeric_cast<mp_integer>(upper_bound_opt.value_or(nil_exprt()));
+    numeric_cast<bytest>(upper_bound_opt.value_or(nil_exprt()));
 
   byte_extract_exprt unpacked(src);
   unpacked.op() = unpack_rec(
@@ -1257,7 +1261,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
     // stitching together consecutive elements down below
     auto element_bits = pointer_offset_bits(subtype, ns);
     if(
-      element_bits.has_value() && *element_bits >= 1 &&
+      element_bits.has_value() && *element_bits >= bitst{1} &&
       *element_bits % src.get_bits_per_byte() == 0)
     {
       return lower_byte_extract_array_vector(
@@ -1347,7 +1351,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
   auto subtype_bits = pointer_offset_bits(*subtype, ns);
 
   DATA_INVARIANT(
-    subtype_bits.has_value() && *subtype_bits == src.get_bits_per_byte(),
+    subtype_bits.has_value() && *subtype_bits == bitst{src.get_bits_per_byte()},
     "offset bits are byte aligned");
 
   auto size_bits = pointer_offset_bits(unpacked.type(), ns);
@@ -1361,9 +1365,9 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
     size_bits = op0_bits;
   }
 
-  mp_integer num_bytes =
-    (*size_bits) / src.get_bits_per_byte() +
-    (((*size_bits) % src.get_bits_per_byte() == 0) ? 0 : 1);
+  bytest num_bytes =
+    bytest{(*size_bits) / src.get_bits_per_byte()} +
+    bytest{(((*size_bits) % src.get_bits_per_byte() == 0) ? 0 : 1)};
 
   // get 'width'-many bytes, and concatenate
   const std::size_t width_bytes = numeric_cast_v<std::size_t>(num_bytes);
@@ -1852,7 +1856,7 @@ static exprt lower_byte_update_array_vector(
   // fall back to bytewise updates in all non-constant or dubious cases
   if(
     !size.is_constant() || !src.offset().is_constant() ||
-    !subtype_bits.has_value() || *subtype_bits == 0 ||
+    !subtype_bits.has_value() || *subtype_bits == bitst{0} ||
     *subtype_bits % src.get_bits_per_byte() != 0 ||
     non_const_update_bound.has_value() || value_as_byte_array.id() != ID_array)
   {
@@ -1862,8 +1866,7 @@ static exprt lower_byte_update_array_vector(
 
   std::size_t num_elements =
     numeric_cast_v<std::size_t>(to_constant_expr(size));
-  mp_integer offset_bytes =
-    numeric_cast_v<mp_integer>(to_constant_expr(src.offset()));
+  bytest offset_bytes = numeric_cast_v<bytest>(to_constant_expr(src.offset()));
 
   exprt::operandst elements;
   elements.reserve(num_elements);
@@ -1884,13 +1887,13 @@ static exprt lower_byte_update_array_vector(
             src.get_bits_per_byte();
       ++i)
   {
-    mp_integer update_offset =
-      offset_bytes - i * (*subtype_bits / src.get_bits_per_byte());
+    bytest update_offset =
+      offset_bytes - bytest{i * (*subtype_bits / src.get_bits_per_byte())};
     mp_integer update_elements = *subtype_bits / src.get_bits_per_byte();
     exprt::operandst::const_iterator first =
       value_as_byte_array.operands().begin();
     exprt::operandst::const_iterator end = value_as_byte_array.operands().end();
-    if(update_offset < 0)
+    if(update_offset < bytest{0})
     {
       INVARIANT(
         value_as_byte_array.operands().size() > -update_offset,
@@ -1913,7 +1916,7 @@ static exprt lower_byte_update_array_vector(
     const byte_update_exprt bu{
       src.id(),
       index_exprt{src.op(), from_integer(i, c_index_type())},
-      from_integer(update_offset < 0 ? 0 : update_offset, src.offset().type()),
+      from_integer(std::max(bytest{0}, update_offset), src.offset().type()),
       array_exprt{
         std::move(update_values),
         array_typet{
@@ -1958,7 +1961,7 @@ static exprt lower_byte_update_struct(
   exprt::operandst elements;
   elements.reserve(struct_type.components().size());
 
-  mp_integer member_offset_bits = 0;
+  bitst member_offset_bits{0};
   for(const auto &comp : struct_type.components())
   {
     auto element_width = pointer_offset_bits(comp.type(), ns);
@@ -1973,7 +1976,7 @@ static exprt lower_byte_update_struct(
         from_integer(
           member_offset_bits / src.get_bits_per_byte(), src.offset().type())},
       ns);
-    auto offset_bytes = numeric_cast<mp_integer>(offset);
+    auto offset_bytes = numeric_cast<bytest>(offset);
     // we don't need to update anything when
     // 1) the update offset is greater than the end of this member (thus the
     // relative offset is greater than this element) or
@@ -1982,7 +1985,7 @@ static exprt lower_byte_update_struct(
     if(
       offset_bytes.has_value() &&
       (*offset_bytes * src.get_bits_per_byte() >= *element_width ||
-       (value_as_byte_array.id() == ID_array && *offset_bytes < 0 &&
+       (value_as_byte_array.id() == ID_array && *offset_bytes < bytest{0} &&
         -*offset_bytes >= value_as_byte_array.operands().size())))
     {
       elements.push_back(std::move(member));
@@ -2027,7 +2030,7 @@ static exprt lower_byte_update_struct(
     mp_integer update_elements =
       (*element_width + src.get_bits_per_byte() - 1) / src.get_bits_per_byte();
     std::size_t first = 0;
-    if(*offset_bytes < 0)
+    if(*offset_bytes < bytest{0})
     {
       offset = from_integer(0, src.offset().type());
       INVARIANT(
@@ -2195,10 +2198,10 @@ static exprt lower_byte_update(
 
     auto element_width = pointer_offset_bits(*subtype, ns);
     CHECK_RETURN(element_width.has_value());
-    CHECK_RETURN(*element_width > 0);
+    CHECK_RETURN(*element_width > bitst{0});
     CHECK_RETURN(*element_width % src.get_bits_per_byte() == 0);
 
-    if(*element_width == src.get_bits_per_byte())
+    if(*element_width == bitst{src.get_bits_per_byte()})
     {
       if(value_as_byte_array.id() != ID_array)
       {
@@ -2249,7 +2252,7 @@ static exprt lower_byte_update(
     // mask out the bits to be updated, shift the value according to the
     // offset and bit-or
     const auto type_width = pointer_offset_bits(src.type(), ns);
-    CHECK_RETURN(type_width.has_value() && *type_width > 0);
+    CHECK_RETURN(type_width.has_value() && *type_width > bitst{0});
     const std::size_t type_bits = numeric_cast_v<std::size_t>(*type_width);
 
     exprt::operandst update_bytes;
@@ -2291,8 +2294,8 @@ static exprt lower_byte_update(
       const exprt src_as_bytes = unpack_rec(
         val_before,
         src.id() == ID_byte_update_little_endian,
-        mp_integer{0},
-        mp_integer{update_bytes.size()},
+        bytest{0},
+        bytest{update_bytes.size()},
         src.get_bits_per_byte(),
         ns);
       CHECK_RETURN(src_as_bytes.id() == ID_array);
diff --git a/src/util/mp_arith.h b/src/util/mp_arith.h
index 99a6175c2b78..a54a490b3e4b 100644
--- a/src/util/mp_arith.h
+++ b/src/util/mp_arith.h
@@ -48,4 +48,112 @@ const mp_integer string2integer(const std::string &, unsigned base=10);
 const std::string integer2binary(const mp_integer &, std::size_t width);
 const mp_integer binary2integer(const std::string &, bool is_signed);
 
+#define BITS_COMPARISON(op)                                                    \
+  bool operator op(const bitst &other) const                                   \
+  {                                                                            \
+    return static_cast<const mp_integer &>(*this)                              \
+      op static_cast<const mp_integer &>(other);                               \
+  }                                                                            \
+  bool operator op(const mp_integer &other) const = delete
+
+class bitst : public mp_integer
+{
+public:
+  explicit bitst(const mp_integer &generic) : mp_integer(generic)
+  {
+  }
+
+  bitst &operator+=(const bitst &other)
+  {
+    static_cast<mp_integer &>(*this) += other;
+    return *this;
+  }
+
+  bitst &operator-=(const bitst &other)
+  {
+    static_cast<mp_integer &>(*this) -= other;
+    return *this;
+  }
+
+  bitst &operator%=(const bitst &other)
+  {
+    static_cast<mp_integer &>(*this) %= other;
+    return *this;
+  }
+
+  BITS_COMPARISON(<);
+  BITS_COMPARISON(>);
+  BITS_COMPARISON(<=);
+  BITS_COMPARISON(>=);
+  BITS_COMPARISON(==);
+  BITS_COMPARISON(!=);
+};
+
+inline bitst operator+(const bitst &lhs, const bitst &rhs)
+{
+  return bitst{lhs} += rhs;
+}
+inline bitst operator-(const bitst &lhs, const bitst &rhs)
+{
+  return bitst{lhs} -= rhs;
+}
+inline bitst operator%(const bitst &lhs, const bitst &rhs)
+{
+  return bitst{lhs} %= rhs;
+}
+
+#define BYTES_COMPARISON(op)                                                   \
+  bool operator op(const bytest &other) const                                  \
+  {                                                                            \
+    return static_cast<const mp_integer &>(*this)                              \
+      op static_cast<const mp_integer &>(other);                               \
+  }                                                                            \
+  bool operator op(const mp_integer &other) const = delete
+
+class bytest : public mp_integer
+{
+public:
+  explicit bytest(const mp_integer &generic) : mp_integer(generic)
+  {
+  }
+
+  bytest &operator+=(const bytest &other)
+  {
+    static_cast<mp_integer &>(*this) += other;
+    return *this;
+  }
+
+  bytest &operator-=(const bytest &other)
+  {
+    static_cast<mp_integer &>(*this) -= other;
+    return *this;
+  }
+
+  bytest &operator%=(const bytest &other)
+  {
+    static_cast<mp_integer &>(*this) %= other;
+    return *this;
+  }
+
+  BYTES_COMPARISON(<);
+  BYTES_COMPARISON(>);
+  BYTES_COMPARISON(<=);
+  BYTES_COMPARISON(>=);
+  BYTES_COMPARISON(==);
+  BYTES_COMPARISON(!=);
+};
+
+inline bytest operator+(const bytest &lhs, const bytest &rhs)
+{
+  return bytest{lhs} += rhs;
+}
+inline bytest operator-(const bytest &lhs, const bytest &rhs)
+{
+  return bytest{lhs} -= rhs;
+}
+inline bytest operator%(const bytest &lhs, const bytest &rhs)
+{
+  return bytest{lhs} %= rhs;
+}
+
 #endif // CPROVER_UTIL_MP_ARITH_H
diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp
index 82249a58d8eb..23bb8ed4a7ba 100644
--- a/src/util/pointer_offset_size.cpp
+++ b/src/util/pointer_offset_size.cpp
@@ -22,12 +22,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "ssa_expr.h"
 #include "std_expr.h"
 
-optionalt<mp_integer> member_offset(
+optionalt<bytest> member_offset(
   const struct_typet &type,
   const irep_idt &member,
   const namespacet &ns)
 {
-  mp_integer result = 0;
+  bytest result{0};
   std::size_t bit_field_bits = 0;
 
   for(const auto &comp : type.components())
@@ -39,13 +39,13 @@ optionalt<mp_integer> member_offset(
     {
       const std::size_t w = to_c_bit_field_type(comp.type()).get_width();
       bit_field_bits += w;
-      result += bit_field_bits / config.ansi_c.char_width;
+      result += bytest{bit_field_bits / config.ansi_c.char_width};
       bit_field_bits %= config.ansi_c.char_width;
     }
     else if(comp.type().id() == ID_bool)
     {
       ++bit_field_bits;
-      result += bit_field_bits / config.ansi_c.char_width;
+      result += bytest{bit_field_bits / config.ansi_c.char_width};
       bit_field_bits %= config.ansi_c.char_width;
     }
     else
@@ -63,12 +63,12 @@ optionalt<mp_integer> member_offset(
   return result;
 }
 
-optionalt<mp_integer> member_offset_bits(
+optionalt<bitst> member_offset_bits(
   const struct_typet &type,
   const irep_idt &member,
   const namespacet &ns)
 {
-  mp_integer offset=0;
+  bitst offset{0};
   const struct_typet::componentst &components=type.components();
 
   for(const auto &comp : components)
@@ -87,19 +87,20 @@ optionalt<mp_integer> member_offset_bits(
 }
 
 /// Compute the size of a type in bytes, rounding up to full bytes
-optionalt<mp_integer>
-pointer_offset_size(const typet &type, const namespacet &ns)
+optionalt<bytest> pointer_offset_size(const typet &type, const namespacet &ns)
 {
   auto bits = pointer_offset_bits(type, ns);
 
   if(bits.has_value())
-    return (*bits + config.ansi_c.char_width - 1) / config.ansi_c.char_width;
+  {
+    return bytest{
+      (*bits + config.ansi_c.char_width - 1) / config.ansi_c.char_width};
+  }
   else
     return {};
 }
 
-optionalt<mp_integer>
-pointer_offset_bits(const typet &type, const namespacet &ns)
+optionalt<bitst> pointer_offset_bits(const typet &type, const namespacet &ns)
 {
   if(type.id()==ID_array)
   {
@@ -112,7 +113,7 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
     if(!size.has_value())
       return {};
 
-    return (*sub) * (*size);
+    return bitst{(*sub) * (*size)};
   }
   else if(type.id()==ID_vector)
   {
@@ -124,21 +125,21 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
     const mp_integer size =
       numeric_cast_v<mp_integer>(to_vector_type(type).size());
 
-    return (*sub) * size;
+    return bitst{(*sub) * size};
   }
   else if(type.id()==ID_complex)
   {
     auto sub = pointer_offset_bits(to_complex_type(type).subtype(), ns);
 
     if(sub.has_value())
-      return (*sub) * 2;
+      return bitst{(*sub) * 2};
     else
       return {};
   }
   else if(type.id()==ID_struct)
   {
     const struct_typet &struct_type=to_struct_type(type);
-    mp_integer result=0;
+    bitst result{0};
 
     for(const auto &c : struct_type.components())
     {
@@ -158,7 +159,7 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
     const union_typet &union_type=to_union_type(type);
 
     if(union_type.components().empty())
-      return mp_integer{0};
+      return bitst{0};
 
     const auto widest_member = union_type.find_widest_union_component(ns);
 
@@ -175,12 +176,12 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
           type.id()==ID_c_bool ||
           type.id()==ID_c_bit_field)
   {
-    return mp_integer(to_bitvector_type(type).get_width());
+    return bitst{to_bitvector_type(type).get_width()};
   }
   else if(type.id()==ID_c_enum)
   {
-    return mp_integer(
-      to_bitvector_type(to_c_enum_type(type).underlying_type()).get_width());
+    return bitst{
+      to_bitvector_type(to_c_enum_type(type).underlying_type()).get_width()};
   }
   else if(type.id()==ID_c_enum_tag)
   {
@@ -188,15 +189,15 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
   }
   else if(type.id()==ID_bool)
   {
-    return mp_integer(1);
+    return bitst{1};
   }
   else if(type.id()==ID_pointer)
   {
     // the following is an MS extension
     if(type.get_bool(ID_C_ptr32))
-      return mp_integer(32);
+      return bitst{32};
 
-    return mp_integer(to_bitvector_type(type).get_width());
+    return bitst{to_bitvector_type(type).get_width()};
   }
   else if(type.id() == ID_union_tag)
   {
@@ -208,11 +209,11 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
   }
   else if(type.id()==ID_code)
   {
-    return mp_integer(0);
+    return bitst{0};
   }
   else if(type.id()==ID_string)
   {
-    return mp_integer(32);
+    return bitst{32};
   }
   else
     return {};
@@ -504,7 +505,7 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
     return {};
 }
 
-optionalt<mp_integer>
+optionalt<bytest>
 compute_pointer_offset(const exprt &expr, const namespacet &ns)
 {
   if(expr.id()==ID_symbol)
@@ -513,7 +514,7 @@ compute_pointer_offset(const exprt &expr, const namespacet &ns)
       return compute_pointer_offset(
         to_ssa_expr(expr).get_original_expr(), ns);
     else
-      return mp_integer(0);
+      return bytest{0};
   }
   else if(expr.id()==ID_index)
   {
@@ -530,11 +531,11 @@ compute_pointer_offset(const exprt &expr, const namespacet &ns)
       const auto &array_type = to_array_type(index_expr.array().type());
       auto sub_size = pointer_offset_size(array_type.element_type(), ns);
 
-      if(sub_size.has_value() && *sub_size > 0)
+      if(sub_size.has_value() && *sub_size > bytest{0})
       {
         const auto i = numeric_cast<mp_integer>(index_expr.index());
         if(i.has_value())
-          return (*o) + (*i) * (*sub_size);
+          return (*o) + bytest{(*i) * (*sub_size)};
       }
     }
 
@@ -561,18 +562,18 @@ compute_pointer_offset(const exprt &expr, const namespacet &ns)
     }
   }
   else if(expr.id()==ID_string_constant)
-    return mp_integer(0);
+    return bytest{0};
 
   return {}; // don't know
 }
 
 optionalt<exprt> get_subexpression_at_offset(
   const exprt &expr,
-  const mp_integer &offset_bytes,
+  const bytest &offset_bytes,
   const typet &target_type_raw,
   const namespacet &ns)
 {
-  if(offset_bytes == 0 && expr.type() == target_type_raw)
+  if(offset_bytes == bytest{0} && expr.type() == target_type_raw)
   {
     exprt result = expr;
 
@@ -583,7 +584,7 @@ optionalt<exprt> get_subexpression_at_offset(
   }
 
   if(
-    offset_bytes == 0 && expr.type().id() == ID_pointer &&
+    offset_bytes == bytest{0} && expr.type().id() == ID_pointer &&
     target_type_raw.id() == ID_pointer)
   {
     return typecast_exprt(expr, target_type_raw);
@@ -598,7 +599,7 @@ optionalt<exprt> get_subexpression_at_offset(
   {
     const struct_typet &struct_type = to_struct_type(source_type);
 
-    mp_integer m_offset_bits = 0;
+    bitst m_offset_bits{0};
     for(const auto &component : struct_type.components())
     {
       const auto m_size_bits = pointer_offset_bits(component.type(), ns);
@@ -608,15 +609,15 @@ optionalt<exprt> get_subexpression_at_offset(
       // if this member completely contains the target, and this member is
       // byte-aligned, recurse into it
       if(
-        offset_bytes * config.ansi_c.char_width >= m_offset_bits &&
+        bitst{offset_bytes * config.ansi_c.char_width} >= m_offset_bits &&
         m_offset_bits % config.ansi_c.char_width == 0 &&
-        offset_bytes * config.ansi_c.char_width + *target_size_bits <=
+        bitst{offset_bytes * config.ansi_c.char_width} + *target_size_bits <=
           m_offset_bits + *m_size_bits)
       {
         const member_exprt member(expr, component.get_name(), component.type());
         return get_subexpression_at_offset(
           member,
-          offset_bytes - m_offset_bits / config.ansi_c.char_width,
+          offset_bytes - bytest{m_offset_bits / config.ansi_c.char_width},
           target_type_raw,
           ns);
       }
@@ -634,17 +635,17 @@ optionalt<exprt> get_subexpression_at_offset(
     // no arrays of non-byte-aligned, zero-, or unknown-sized objects
     if(
       array_type.size().is_constant() && elem_size_bits.has_value() &&
-      *elem_size_bits > 0 && *elem_size_bits % config.ansi_c.char_width == 0 &&
+      *elem_size_bits > bitst{0} &&
+      *elem_size_bits % config.ansi_c.char_width == 0 &&
       *target_size_bits <= *elem_size_bits)
     {
       const mp_integer array_size =
         numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
-      const mp_integer elem_size_bytes =
-        *elem_size_bits / config.ansi_c.char_width;
+      const bytest elem_size_bytes{*elem_size_bits / config.ansi_c.char_width};
       const mp_integer index = offset_bytes / elem_size_bytes;
-      const auto offset_inside_elem = offset_bytes % elem_size_bytes;
-      const auto target_size_bytes =
-        *target_size_bits / config.ansi_c.char_width;
+      const bytest offset_inside_elem{offset_bytes % elem_size_bytes};
+      const bytest target_size_bytes{
+        *target_size_bits / config.ansi_c.char_width};
       // only recurse if the cell completely contains the target
       if(
         index < array_size &&
@@ -695,7 +696,7 @@ optionalt<exprt> get_subexpression_at_offset(
   const typet &target_type,
   const namespacet &ns)
 {
-  const auto offset_bytes = numeric_cast<mp_integer>(offset);
+  const auto offset_bytes = numeric_cast<bytest>(offset);
 
   if(!offset_bytes.has_value())
     return {};
diff --git a/src/util/pointer_offset_size.h b/src/util/pointer_offset_size.h
index b4ce99dbf73d..f1473debd4ec 100644
--- a/src/util/pointer_offset_size.h
+++ b/src/util/pointer_offset_size.h
@@ -22,23 +22,21 @@ class struct_typet;
 class typet;
 class member_exprt;
 
-optionalt<mp_integer> member_offset(
+optionalt<bytest> member_offset(
   const struct_typet &type,
   const irep_idt &member,
   const namespacet &ns);
 
-optionalt<mp_integer> member_offset_bits(
+optionalt<bitst> member_offset_bits(
   const struct_typet &type,
   const irep_idt &member,
   const namespacet &ns);
 
-optionalt<mp_integer>
-pointer_offset_size(const typet &type, const namespacet &ns);
+optionalt<bytest> pointer_offset_size(const typet &type, const namespacet &ns);
 
-optionalt<mp_integer>
-pointer_offset_bits(const typet &type, const namespacet &ns);
+optionalt<bitst> pointer_offset_bits(const typet &type, const namespacet &ns);
 
-optionalt<mp_integer>
+optionalt<bytest>
 compute_pointer_offset(const exprt &expr, const namespacet &ns);
 
 optionalt<exprt> member_offset_expr(const member_exprt &, const namespacet &ns);
@@ -52,7 +50,7 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns);
 
 optionalt<exprt> get_subexpression_at_offset(
   const exprt &expr,
-  const mp_integer &offset,
+  const bytest &offset,
   const typet &target_type,
   const namespacet &ns);
 
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 8e16f80fa079..84c41f392432 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -914,7 +914,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
           simplify_typecast(typecast_exprt(op_plus_expr.op1(), size_type()));
 
         // void*
-        if(*sub_size == 0 || *sub_size == 1)
+        if(*sub_size == bytest{0} || *sub_size == bytest{1})
           new_expr.op() = offset_expr;
         else
         {
@@ -984,7 +984,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
     const auto step =
       pointer_offset_size(to_pointer_type(op_type).base_type(), ns);
 
-    if(step.has_value() && *step != 0)
+    if(step.has_value() && *step != bytest{0})
     {
       const typet size_t_type(size_type());
       auto new_expr = expr;
@@ -994,7 +994,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
       for(auto &op : new_expr.op().operands())
       {
         exprt new_op = simplify_typecast(typecast_exprt(op, size_t_type));
-        if(op.type().id() != ID_pointer && *step > 1)
+        if(op.type().id() != ID_pointer && *step > bytest{1})
         {
           new_op =
             simplify_mult(mult_exprt(from_integer(*step, size_t_type), new_op));
@@ -1651,7 +1651,7 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
   }
 
   const auto el_size = pointer_offset_bits(expr.type(), ns);
-  if(el_size.has_value() && *el_size < 0)
+  if(el_size.has_value() && *el_size < bitst{0})
     return unchanged(expr);
 
   // byte_extract(byte_extract(root, offset1), offset2) =>
@@ -1699,8 +1699,8 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
   }
 
   // the following require a constant offset
-  auto offset = numeric_cast<mp_integer>(expr.offset());
-  if(!offset.has_value() || *offset < 0)
+  auto offset = numeric_cast<bytest>(expr.offset());
+  if(!offset.has_value() || *offset < bytest{0})
     return unchanged(expr);
 
   // byte_extract(byte_update(root, offset_u, value), offset_e) so that the
@@ -1741,12 +1741,13 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
   // don't do any of the following if endianness doesn't match, as
   // bytes need to be swapped
   if(
-    *offset == 0 && ((expr.id() == ID_byte_extract_little_endian &&
-                      config.ansi_c.endianness ==
-                        configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN) ||
-                     (expr.id() == ID_byte_extract_big_endian &&
-                      config.ansi_c.endianness ==
-                        configt::ansi_ct::endiannesst::IS_BIG_ENDIAN)))
+    *offset == bytest{0} &&
+    ((expr.id() == ID_byte_extract_little_endian &&
+      config.ansi_c.endianness ==
+        configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN) ||
+     (expr.id() == ID_byte_extract_big_endian &&
+      config.ansi_c.endianness ==
+        configt::ansi_ct::endiannesst::IS_BIG_ENDIAN)))
   {
     // byte extract of full object is object
     if(expr.type() == expr.op().type())
@@ -1775,7 +1776,7 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
 
   // no proper simplification for expr.type()==void
   // or types of unknown size
-  if(!el_size.has_value() || *el_size == 0)
+  if(!el_size.has_value() || *el_size == bitst{0})
     return unchanged(expr);
 
   if(expr.op().id()==ID_array_of &&
@@ -1886,7 +1887,7 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
 
         // the next member would be misaligned, abort
         if(
-          !component_bits.has_value() || *component_bits == 0 ||
+          !component_bits.has_value() || *component_bits == bitst{0} ||
           *component_bits % expr.get_bits_per_byte() != 0)
         {
           failed = true;
@@ -1936,10 +1937,10 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
     const array_typet &array_type = to_array_type(expr.op().type());
     const auto &element_bit_width =
       pointer_offset_bits(array_type.element_type(), ns);
-    if(element_bit_width.has_value() && *element_bit_width > 0)
+    if(element_bit_width.has_value() && *element_bit_width > bitst{0})
     {
       if(
-        *offset > 0 &&
+        *offset > bytest{0} &&
         *offset * expr.get_bits_per_byte() % *element_bit_width == 0)
       {
         const auto elements_to_erase = numeric_cast_v<std::size_t>(
@@ -1956,7 +1957,7 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
         be.offset() = from_integer(0, expr.offset().type());
         return changed(simplify_byte_extract(be));
       }
-      else if(*offset == 0 && *el_size % *element_bit_width == 0)
+      else if(*offset == bytest{0} && *el_size % *element_bit_width == bitst{0})
       {
         const auto elements_to_keep =
           numeric_cast_v<std::size_t>(*el_size / *element_bit_width);
@@ -2009,8 +2010,8 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
 
   // byte update of full object is byte_extract(new value)
   if(
-    offset.is_zero() && val_size.has_value() && *val_size > 0 &&
-    root_size.has_value() && *root_size > 0 && *val_size >= *root_size)
+    offset.is_zero() && val_size.has_value() && *val_size > bitst{0} &&
+    root_size.has_value() && *root_size > bitst{0} && *val_size >= *root_size)
   {
     byte_extract_exprt be(
       expr.id() == ID_byte_update_little_endian ? ID_byte_extract_little_endian
@@ -2024,11 +2025,12 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
   }
 
   // update bits in a constant
-  const auto offset_int = numeric_cast<mp_integer>(offset);
+  const auto offset_int = numeric_cast<bytest>(offset);
   if(
-    root_size.has_value() && *root_size >= 0 && val_size.has_value() &&
-    *val_size >= 0 && offset_int.has_value() && *offset_int >= 0 &&
-    *offset_int * expr.get_bits_per_byte() + *val_size <= *root_size)
+    root_size.has_value() && *root_size >= bitst{0} && val_size.has_value() &&
+    *val_size >= bitst{0} && offset_int.has_value() &&
+    *offset_int >= bytest{0} &&
+    bitst{*offset_int * expr.get_bits_per_byte()} + *val_size <= *root_size)
   {
     auto root_bits =
       expr2bits(root, expr.id() == ID_byte_update_little_endian, ns);
@@ -2140,13 +2142,13 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
   }
 
   // the following require a constant offset
-  if(!offset_int.has_value() || *offset_int < 0)
+  if(!offset_int.has_value() || *offset_int < bytest{0})
     return unchanged(expr);
 
   const typet &op_type=ns.follow(root.type());
 
   // size must be known
-  if(!val_size.has_value() || *val_size == 0)
+  if(!val_size.has_value() || *val_size == bitst{0})
     return unchanged(expr);
 
   // Are we updating (parts of) a struct? Do individual member updates
@@ -2178,7 +2180,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
 
       // is it a byte-sized member?
       if(
-        !m_size_bits.has_value() || *m_size_bits == 0 ||
+        !m_size_bits.has_value() || *m_size_bits == bitst{0} ||
         (*m_size_bits) % expr.get_bits_per_byte() != 0)
       {
         result_expr.make_nil();
@@ -2192,7 +2194,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
         continue;
       // are we done updating?
       else if(
-        update_size.has_value() && *update_size > 0 &&
+        update_size.has_value() && *update_size > bytest{0} &&
         *m_offset >= *offset_int + *update_size)
       {
         break;
@@ -2209,7 +2211,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
       if(
         *m_offset < *offset_int ||
         (*m_offset == *offset_int && update_size.has_value() &&
-         *update_size > 0 && m_size_bytes > *update_size))
+         *update_size > bytest{0} && m_size_bytes > *update_size))
       {
         byte_update_exprt v(
           ID_byte_update_little_endian,
@@ -2221,7 +2223,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
         to_with_expr(result_expr).new_value().swap(v);
       }
       else if(
-        update_size.has_value() && *update_size > 0 &&
+        update_size.has_value() && *update_size > bytest{0} &&
         *m_offset + m_size_bytes > *offset_int + *update_size)
       {
         // we don't handle this for the moment
@@ -2253,7 +2255,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
       pointer_offset_bits(to_type_with_subtype(op_type).subtype(), ns);
 
     if(
-      !el_size.has_value() || *el_size == 0 ||
+      !el_size.has_value() || *el_size == bitst{0} ||
       (*el_size) % expr.get_bits_per_byte() != 0 ||
       (*val_size) % expr.get_bits_per_byte() != 0)
     {
@@ -2262,7 +2264,8 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
 
     exprt result=root;
 
-    mp_integer m_offset_bits=0, val_offset=0;
+    bitst m_offset_bits{0};
+    bytest val_offset{0};
     Forall_operands(it, result)
     {
       if(*offset_int * expr.get_bits_per_byte() + (*val_size) <= m_offset_bits)
@@ -2270,11 +2273,17 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
 
       if(*offset_int * expr.get_bits_per_byte() < m_offset_bits + *el_size)
       {
-        mp_integer bytes_req =
-          (m_offset_bits + *el_size) / expr.get_bits_per_byte() - *offset_int;
+        bytest bytes_req =
+          bytest{(m_offset_bits + *el_size) / expr.get_bits_per_byte()} -
+          *offset_int;
         bytes_req-=val_offset;
-        if(val_offset + bytes_req > (*val_size) / expr.get_bits_per_byte())
-          bytes_req = (*val_size) / expr.get_bits_per_byte() - val_offset;
+        if(
+          val_offset + bytes_req >
+          bytest{(*val_size) / expr.get_bits_per_byte()})
+        {
+          bytes_req =
+            bytest{(*val_size) / expr.get_bits_per_byte()} - val_offset;
+        }
 
         byte_extract_exprt new_val(
           ID_byte_extract_little_endian,
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index fe36ca6e6fbd..810ec3edc33f 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -1158,7 +1158,7 @@ simplify_exprt::simplify_extractbits(const extractbits_exprt &expr)
     {
       auto op_width = pointer_offset_bits(op.type(), ns);
 
-      if(!op_width.has_value() || *op_width <= 0)
+      if(!op_width.has_value() || *op_width <= bitst{0})
         return unchanged(expr);
 
       if(*start < offset && offset <= *end + *op_width)
diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp
index beb8e8138a6e..21b7d947058e 100644
--- a/src/util/simplify_expr_struct.cpp
+++ b/src/util/simplify_expr_struct.cpp
@@ -220,7 +220,7 @@ simplify_exprt::simplify_member(const member_exprt &expr)
     // type and offset with respect to x.
     if(op_type.id() == ID_struct)
     {
-      optionalt<mp_integer> requested_offset =
+      const auto requested_offset =
         member_offset(to_struct_type(op_type), component_name, ns);
       if(requested_offset.has_value())
       {
diff --git a/src/util/simplify_utils.cpp b/src/util/simplify_utils.cpp
index 67a2b97dc13f..15a41b4dd0d8 100644
--- a/src/util/simplify_utils.cpp
+++ b/src/util/simplify_utils.cpp
@@ -205,9 +205,9 @@ optionalt<exprt> bits2expr(
   if(
     !type_bits.has_value() ||
     (type.id() != ID_union && type.id() != ID_union_tag &&
-     *type_bits != bits.size()) ||
+     *type_bits != bitst{bits.size()}) ||
     ((type.id() == ID_union || type.id() == ID_union_tag) &&
-     *type_bits < bits.size()))
+     *type_bits < bitst{bits.size()}))
   {
     return {};
   }
@@ -302,7 +302,7 @@ optionalt<exprt> bits2expr(
     for(const auto &component : components)
     {
       const auto m_size = pointer_offset_bits(component.type(), ns);
-      CHECK_RETURN(m_size.has_value() && *m_size >= 0);
+      CHECK_RETURN(m_size.has_value() && *m_size >= bitst{0});
 
       std::string comp_bits = std::string(
         bits,
@@ -342,7 +342,7 @@ optionalt<exprt> bits2expr(
       numeric_cast_v<std::size_t>(to_constant_expr(size_expr));
 
     const auto el_size_opt = pointer_offset_bits(array_type.element_type(), ns);
-    CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0);
+    CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > bitst{0});
 
     const std::size_t el_size = numeric_cast_v<std::size_t>(*el_size_opt);
 
@@ -369,7 +369,7 @@ optionalt<exprt> bits2expr(
 
     const auto el_size_opt =
       pointer_offset_bits(vector_type.element_type(), ns);
-    CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0);
+    CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > bitst{0});
 
     const std::size_t el_size = numeric_cast_v<std::size_t>(*el_size_opt);
 
@@ -393,7 +393,7 @@ optionalt<exprt> bits2expr(
     const complex_typet &complex_type = to_complex_type(type);
 
     const auto sub_size_opt = pointer_offset_bits(complex_type.subtype(), ns);
-    CHECK_RETURN(sub_size_opt.has_value() && *sub_size_opt > 0);
+    CHECK_RETURN(sub_size_opt.has_value() && *sub_size_opt > bitst{0});
 
     const std::size_t sub_size = numeric_cast_v<std::size_t>(*sub_size_opt);
 
diff --git a/unit/util/pointer_offset_size.cpp b/unit/util/pointer_offset_size.cpp
index a091f1c7f421..64d9358af825 100644
--- a/unit/util/pointer_offset_size.cpp
+++ b/unit/util/pointer_offset_size.cpp
@@ -34,12 +34,12 @@ TEST_CASE("Build subexpression to access element at offset into array")
   symbol_exprt a("array", array_type);
 
   {
-    const auto result = get_subexpression_at_offset(a, 0, t, ns);
+    const auto result = get_subexpression_at_offset(a, bytest{0}, t, ns);
     REQUIRE(result.value() == index_exprt(a, from_integer(0, c_index_type())));
   }
 
   {
-    const auto result = get_subexpression_at_offset(a, 32 / 8, t, ns);
+    const auto result = get_subexpression_at_offset(a, bytest{32 / 8}, t, ns);
     REQUIRE(result.value() == index_exprt(a, from_integer(1, c_index_type())));
   }
 
@@ -57,7 +57,7 @@ TEST_CASE("Build subexpression to access element at offset into array")
 
   {
     const signedbv_typet small_t(8);
-    const auto result = get_subexpression_at_offset(a, 1, small_t, ns);
+    const auto result = get_subexpression_at_offset(a, bytest{1}, small_t, ns);
     REQUIRE(
       result.value() == make_byte_extract(
                           index_exprt(a, from_integer(0, c_index_type())),
@@ -67,7 +67,7 @@ TEST_CASE("Build subexpression to access element at offset into array")
 
   {
     const signedbv_typet int16_t(16);
-    const auto result = get_subexpression_at_offset(a, 3, int16_t, ns);
+    const auto result = get_subexpression_at_offset(a, bytest{3}, int16_t, ns);
     // At offset 3 there are only 8 bits remaining in an element of type t so
     // not enough to fill a 16 bit int, so this cannot be transformed in an
     // index_exprt.
@@ -94,12 +94,12 @@ TEST_CASE("Build subexpression to access element at offset into struct")
   symbol_exprt s("struct", st);
 
   {
-    const auto result = get_subexpression_at_offset(s, 0, t, ns);
+    const auto result = get_subexpression_at_offset(s, bytest{0}, t, ns);
     REQUIRE(result.value() == member_exprt(s, "foo", t));
   }
 
   {
-    const auto result = get_subexpression_at_offset(s, 32 / 8, t, ns);
+    const auto result = get_subexpression_at_offset(s, bytest{32 / 8}, t, ns);
     REQUIRE(result.value() == member_exprt(s, "bar", t));
   }
 
@@ -117,7 +117,7 @@ TEST_CASE("Build subexpression to access element at offset into struct")
 
   {
     const signedbv_typet small_t(8);
-    const auto result = get_subexpression_at_offset(s, 1, small_t, ns);
+    const auto result = get_subexpression_at_offset(s, bytest{1}, small_t, ns);
     REQUIRE(
       result.value() ==
       make_byte_extract(