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.

Author: tautschnig

Diff for: src/analyses/goto_rw.cpp

@@ -150,7 +150,7 @@ void rw_range_sett::get_objects_byte_extract(
   auto object_size_bits_opt = pointer_offset_bits(be.op().type(), ns);
   const exprt simp_offset=simplify_expr(be.offset(), ns);
 
-  auto index = numeric_cast<mp_integer>(simp_offset);
+  auto index = numeric_cast<bytest>(simp_offset);
   if(
     range_start.is_unknown() || !index.has_value() ||
     !object_size_bits_opt.has_value())
@@ -159,25 +159,25 @@ void rw_range_sett::get_objects_byte_extract(
   }
   else
   {
-    *index *= be.get_bits_per_byte();
-    if(*index >= *object_size_bits_opt)
+    bitst index_bits = bytes_to_bits(*index, be.get_bits_per_byte());
+    if(index_bits >= *object_size_bits_opt)
       return;
 
     endianness_mapt map(
       be.op().type(),
       be.id()==ID_byte_extract_little_endian,
       ns);
     range_spect offset = range_start;
-    if(*index > 0)
+    if(index_bits > bitst{0})
     {
       offset += range_spect::to_range_spect(
-        map.map_bit(numeric_cast_v<std::size_t>(*index)));
+        bitst{map.map_bit(numeric_cast_v<std::size_t>(index_bits))});
     }
     else
     {
       // outside the bounds of immediate byte-extract operand, might still be in
       // bounds of a parent object
-      offset += range_spect::to_range_spect(*index);
+      offset += range_spect::to_range_spect(index_bits);
     }
     get_objects_rec(mode, be.op(), offset, size);
   }
@@ -197,7 +197,7 @@ void rw_range_sett::get_objects_shift(
                            ? range_spect::to_range_spect(*op_bits)
                            : range_spect::unknown();
 
-  const auto dist = numeric_cast<mp_integer>(simp_distance);
+  const auto dist = numeric_cast<bitst>(simp_distance);
   if(
     range_start.is_unknown() || size.is_unknown() || src_size.is_unknown() ||
     !dist.has_value())
@@ -312,7 +312,7 @@ void rw_range_sett::get_objects_index(
     get_objects_rec(
       mode,
       expr.array(),
-      range_start + range_spect::to_range_spect(*index) * sub_size,
+      range_start + range_spect::to_range_spect(bitst{*index}) * sub_size,
       size);
   }
 }
@@ -342,7 +342,7 @@ void rw_range_sett::get_objects_array(
     range_start.is_unknown() ? range_spect{0} : range_start;
   range_spect full_r_e =
     size.is_unknown()
-      ? sub_size * range_spect::to_range_spect(expr.operands().size())
+      ? sub_size * range_spect::to_range_spect(bitst{expr.operands().size()})
       : full_r_s + size;
 
   for(const auto &op : expr.operands())

Diff for: src/analyses/goto_rw.h

@@ -76,15 +76,15 @@ class range_spect
     return *this == unknown();
   }
 
-  static range_spect to_range_spect(const mp_integer &size)
+  static range_spect to_range_spect(const bitst &size)
   {
     // The size need not fit into the analysis platform's width of a signed long
     // (as an example, it could be an unsigned size_t max, or perhaps the source
     // platform has much wider types than the analysis platform.
-    if(!size.is_long())
+    if(!size.get().is_long())
       return range_spect::unknown();
 
-    mp_integer::llong_t ll = size.to_long();
+    mp_integer::llong_t ll = size.get().to_long();
     if(
       ll > std::numeric_limits<range_spect::value_type>::max() ||
       ll < std::numeric_limits<range_spect::value_type>::min())
@@ -128,7 +128,7 @@ class range_spect
   {
     if(is_unknown() || other.is_unknown())
       return range_spect::unknown();
-    return range_spect::to_range_spect(mp_integer{v} + mp_integer{other.v});
+    return range_spect::to_range_spect(bitst{v} + bitst{other.v});
   }
 
   range_spect &operator+=(const range_spect &other)
@@ -142,7 +142,7 @@ class range_spect
   {
     if(is_unknown() || other.is_unknown())
       return range_spect::unknown();
-    return range_spect::to_range_spect(mp_integer{v} - mp_integer{other.v});
+    return range_spect::to_range_spect(bitst{v} - bitst{other.v});
   }
 
   range_spect &operator-=(const range_spect &other)
@@ -156,7 +156,8 @@ class range_spect
   {
     if(is_unknown() || other.is_unknown())
       return range_spect::unknown();
-    return range_spect::to_range_spect(mp_integer{v} * mp_integer{other.v});
+    return range_spect::to_range_spect(
+      bitst{mp_integer{v} * mp_integer{other.v}});
   }
 
 private:

Diff for: src/ansi-c/ansi_c_internal_additions.cpp

@@ -125,9 +125,10 @@ static std::string architecture_string(const std::string &value, const char *s)
 template <typename T>
 static std::string architecture_string(T value, const char *s)
 {
-  return std::string("const " CPROVER_PREFIX "integer " CPROVER_PREFIX
-                     "architecture_") +
-         std::string(s) + "=" + std::to_string(value) + ";\n";
+  std::ostringstream os;
+  os << "const " << CPROVER_PREFIX "integer " << CPROVER_PREFIX "architecture_"
+     << s << '=' << value << ";\n";
+  return os.str();
 }
 
 /// The maximum allocation size is determined by the number of bits that

Diff for: src/ansi-c/c_typecheck_expr.cpp

@@ -1085,7 +1085,7 @@ void c_typecheck_baset::typecheck_expr_alignof(exprt &expr)
   }
 
   // we only care about the type
-  mp_integer a=alignment(argument_type, *this);
+  bytest a = alignment(argument_type, *this);
 
   exprt tmp=from_integer(a, size_type());
   tmp.add_source_location()=expr.source_location();

Diff for: src/ansi-c/expr2c.cpp

@@ -3726,8 +3726,9 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()==ID_bswap)
     return convert_function(
       src,
-      "__builtin_bswap" + integer2string(*pointer_offset_bits(
-                            to_unary_expr(src).op().type(), ns)));
+      "__builtin_bswap" +
+        integer2string(
+          pointer_offset_bits(to_unary_expr(src).op().type(), ns)->get()));
 
   else if(has_prefix(src.id_string(), "byte_extract"))
     return convert_byte_extract(to_byte_extract_expr(src), precedence = 16);