From 0079017d806bbcb4079b05e639f97e896d760cde Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Fri, 27 Sep 2024 13:13:56 -0400
Subject: [PATCH] bitvector_typet: set width from mp_integer

This adds C-style getter/setter methods to bitvector_typet for the width of
the vector.

The setter takes an mp_integer, which checks that the width fits within
std::size_t.  This removes the burden of performing this check from the
caller, and allows callers to avoid potential arithmetic overflows by using
mp_integer.
---
 src/ansi-c/c_typecheck_type.cpp |  2 +-
 src/util/std_types.cpp          | 11 +++++++++++
 src/util/std_types.h            |  9 +++++++++
 3 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
index 02e50709308..3e3121b0f40 100644
--- a/src/ansi-c/c_typecheck_type.cpp
+++ b/src/ansi-c/c_typecheck_type.cpp
@@ -1496,7 +1496,7 @@ void c_typecheck_baset::typecheck_c_bit_field_type(c_bit_field_typet &type)
         << "bit field width is negative";
     }
 
-    type.set_width(numeric_cast_v<std::size_t>(i));
+    type.width(i);
     type.remove(ID_size);
   }
 
diff --git a/src/util/std_types.cpp b/src/util/std_types.cpp
index 3f203ebe913..61c4e0932f8 100644
--- a/src/util/std_types.cpp
+++ b/src/util/std_types.cpp
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "std_types.h"
 
+#include "arith_tools.h"
 #include "c_types.h"
 #include "namespace.h"
 #include "std_expr.h"
@@ -154,6 +155,16 @@ bool is_rvalue_reference(const typet &type)
          type.get_bool(ID_C_rvalue_reference);
 }
 
+std::size_t bitvector_typet::width() const
+{
+  return get_size_t(ID_width);
+}
+
+void bitvector_typet::width(const mp_integer &width)
+{
+  set_width(numeric_cast_v<std::size_t>(width));
+}
+
 void range_typet::set_from(const mp_integer &from)
 {
   set(ID_from, integer2string(from));
diff --git a/src/util/std_types.h b/src/util/std_types.h
index ad314267454..4755d684993 100644
--- a/src/util/std_types.h
+++ b/src/util/std_types.h
@@ -917,16 +917,25 @@ class bitvector_typet : public typet
     set_width(width);
   }
 
+  bitvector_typet(const irep_idt &_id, mp_integer _width) : typet(_id)
+  {
+    width(_width);
+  }
+
   std::size_t get_width() const
   {
     return get_size_t(ID_width);
   }
 
+  std::size_t width() const;
+
   void set_width(std::size_t width)
   {
     set_size_t(ID_width, width);
   }
 
+  void width(const mp_integer &);
+
   static void check(
     const typet &type,
     const validation_modet vm = validation_modet::INVARIANT)