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

@@ -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())

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)};

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);

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();
   }
 

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(

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;
     }

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";

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(

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;

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();

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));
   }

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))
   {

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);