Merge pull request #3699 from tautschnig/width-use-api

kroening · web-flow · commit 651f60d549a1 · 2019-01-07T16:06:21.000Z
Use proper APIs to get or set bitvector type width
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -974,7 +974,7 @@ static std::size_t get_bytecode_type_width(const typet &ty)
 {
   if(ty.id()==ID_pointer)
     return 32;
-  return ty.get_size_t(ID_width);
+  return to_bitvector_type(ty).get_width();
 }
 
 code_blockt java_bytecode_convert_methodt::convert_instructions(
@@ -2646,7 +2646,7 @@ exprt::operandst &java_bytecode_convert_methodt::convert_ushr(
 {
   const typet type = java_type_from_char(statement[0]);
 
-  const std::size_t width = type.get_size_t(ID_width);
+  const std::size_t width = get_bytecode_type_width(type);
   typet target = unsignedbv_typet(width);
 
   exprt lhs = op[0];
diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp
@@ -33,7 +33,7 @@ unsigned java_local_variable_slots(const typet &t)
   if(t.id()==ID_pointer)
     return 1;
 
-  const std::size_t bitwidth = t.get_size_t(ID_width);
+  const std::size_t bitwidth = to_bitvector_type(t).get_width();
   INVARIANT(
     bitwidth==8 ||
     bitwidth==16 ||
diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp
@@ -279,10 +279,10 @@ typet c_typecastt::follow_with_qualifiers(const typet &src_type)
 c_typecastt::c_typet c_typecastt::get_c_type(
   const typet &type) const
 {
-  const std::size_t width = type.get_size_t(ID_width);
-
   if(type.id()==ID_signedbv)
   {
+    const std::size_t width = to_bitvector_type(type).get_width();
+
     if(width<=config.ansi_c.char_width)
       return CHAR;
     else if(width<=config.ansi_c.short_int_width)
@@ -298,6 +298,8 @@ c_typecastt::c_typet c_typecastt::get_c_type(
   }
   else if(type.id()==ID_unsignedbv)
   {
+    const std::size_t width = to_bitvector_type(type).get_width();
+
     if(width<=config.ansi_c.char_width)
       return UCHAR;
     else if(width<=config.ansi_c.short_int_width)
@@ -317,6 +319,8 @@ c_typecastt::c_typet c_typecastt::get_c_type(
     return BOOL;
   else if(type.id()==ID_floatbv)
   {
+    const std::size_t width = to_bitvector_type(type).get_width();
+
     if(width<=config.ansi_c.single_width)
       return SINGLE;
     else if(width<=config.ansi_c.double_width)
@@ -591,8 +595,8 @@ void c_typecastt::implicit_typecast_arithmetic(
   if(max_type==LARGE_SIGNED_INT || max_type==LARGE_UNSIGNED_INT)
   {
     // get the biggest width of both
-    std::size_t width1=type1.get_size_t(ID_width);
-    std::size_t width2=type2.get_size_t(ID_width);
+    std::size_t width1 = to_bitvector_type(type1).get_width();
+    std::size_t width2 = to_bitvector_type(type2).get_width();
 
     // produce type
     typet result_type;
diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp
@@ -69,12 +69,13 @@ exprt c_typecheck_baset::do_initializer_rec(
   if(value.id()==ID_initializer_list)
     return do_initializer_list(value, type, force_constant);
 
-  if(value.id()==ID_array &&
-     value.get_bool(ID_C_string_constant) &&
-     full_type.id()==ID_array &&
-     (full_type.subtype().id()==ID_signedbv ||
-      full_type.subtype().id()==ID_unsignedbv) &&
-      full_type.subtype().get(ID_width)==value.type().subtype().get(ID_width))
+  if(
+    value.id() == ID_array && value.get_bool(ID_C_string_constant) &&
+    full_type.id() == ID_array &&
+    (full_type.subtype().id() == ID_signedbv ||
+     full_type.subtype().id() == ID_unsignedbv) &&
+    to_bitvector_type(full_type.subtype()).get_width() ==
+      to_bitvector_type(value.type().subtype()).get_width())
   {
     exprt tmp=value;
 
@@ -130,11 +131,12 @@ exprt c_typecheck_baset::do_initializer_rec(
     return tmp;
   }
 
-  if(value.id()==ID_string_constant &&
-     full_type.id()==ID_array &&
-     (full_type.subtype().id()==ID_signedbv ||
-      full_type.subtype().id()==ID_unsignedbv) &&
-      full_type.subtype().get(ID_width)==char_type().get(ID_width))
+  if(
+    value.id() == ID_string_constant && full_type.id() == ID_array &&
+    (full_type.subtype().id() == ID_signedbv ||
+     full_type.subtype().id() == ID_unsignedbv) &&
+    to_bitvector_type(full_type.subtype()).get_width() ==
+      char_type().get_width())
   {
     // will go away, to be replaced by the above block
 
@@ -876,11 +878,12 @@ exprt c_typecheck_baset::do_initializer_list(
 
     // 6.7.9, 14: An array of character type may be initialized by a character
     // string literal or UTF-8 string literal, optionally enclosed in braces.
-    if(value.operands().size()>=1 &&
-       value.op0().id()==ID_string_constant &&
-       (full_type.subtype().id()==ID_signedbv ||
-        full_type.subtype().id()==ID_unsignedbv) &&
-       full_type.subtype().get(ID_width)==char_type().get(ID_width))
+    if(
+      value.operands().size() >= 1 && value.op0().id() == ID_string_constant &&
+      (full_type.subtype().id() == ID_signedbv ||
+       full_type.subtype().id() == ID_unsignedbv) &&
+      to_bitvector_type(full_type.subtype()).get_width() ==
+        char_type().get_width())
     {
       if(value.operands().size()>1)
       {
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
@@ -76,7 +76,8 @@ void c_typecheck_baset::typecheck_type(typet &type)
   else if(type.id()==ID_pointer)
   {
     typecheck_type(type.subtype());
-    INVARIANT(!type.get(ID_width).empty(), "pointers must have width");
+    INVARIANT(
+      to_bitvector_type(type).get_width() > 0, "pointers must have width");
   }
   else if(type.id()==ID_struct ||
           type.id()==ID_union)
@@ -1433,7 +1434,7 @@ void c_typecheck_baset::typecheck_c_bit_field_type(c_bit_field_typet &type)
       throw 0;
     }
 
-    sub_width = c_enum_type.subtype().get_size_t(ID_width);
+    sub_width = to_bitvector_type(c_enum_type.subtype()).get_width();
   }
   else
   {
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
@@ -244,7 +244,7 @@ std::string expr2ct::convert_rec(
       return q+"long double"+d;
     else
     {
-      std::string swidth=src.get_string(ID_width);
+      std::string swidth = std::to_string(width);
       std::string fwidth=src.get_string(ID_f);
       return q + CPROVER_PREFIX + "floatbv[" + swidth + "][" + fwidth + "]";
     }
@@ -282,7 +282,7 @@ std::string expr2ct::convert_rec(
 
     // There is also wchar_t among the above, but this isn't a C type.
 
-    mp_integer width=string2integer(src.get_string(ID_width));
+    const std::size_t width = to_bitvector_type(src).get_width();
 
     bool is_signed=src.id()==ID_signedbv;
     std::string sign_str=is_signed?"signed ":"unsigned ";
diff --git a/src/ansi-c/literals/convert_integer_literal.cpp b/src/ansi-c/literals/convert_integer_literal.cpp
@@ -90,8 +90,8 @@ exprt convert_integer_literal(const std::string &src)
     else
       c_type=is_unsigned?ID_unsigned_long_long_int:ID_signed_long_long_int;
 
-    typet type=typet(is_unsigned?ID_unsignedbv:ID_signedbv);
-    type.set(ID_width, width_suffix);
+    bitvector_typet type(
+      is_unsigned ? ID_unsignedbv : ID_signedbv, width_suffix);
     type.set(ID_C_c_type, c_type);
 
     exprt result=from_integer(value, type);
@@ -166,9 +166,7 @@ exprt convert_integer_literal(const std::string &src)
       c_type=ID_signed_long_long_int;
   }
 
-  typet type=typet(is_signed?ID_signedbv:ID_unsignedbv);
-
-  type.set(ID_width, width);
+  bitvector_typet type(is_signed ? ID_signedbv : ID_unsignedbv, width);
   type.set(ID_C_c_type, c_type);
 
   exprt result;
diff --git a/src/ansi-c/padding.cpp b/src/ansi-c/padding.cpp
@@ -123,7 +123,7 @@ underlying_width(const c_bit_field_typet &type, const namespacet &ns)
     const typet &c_enum_type = ns.follow_tag(to_c_enum_tag_type(subtype));
 
     if(c_enum_type.id() == ID_c_enum)
-      return c_enum_type.subtype().get_size_t(ID_width);
+      return to_bitvector_type(c_enum_type.subtype()).get_width();
     else
       return {};
   }
diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp
@@ -784,8 +784,8 @@ void cpp_typecheckt::typecheck_expr_new(exprt &expr)
     typecheck_expr(size);
 
     bool size_is_unsigned=(size.type().id()==ID_unsignedbv);
-    typet integer_type(size_is_unsigned?ID_unsignedbv:ID_signedbv);
-    integer_type.set(ID_width, config.ansi_c.int_width);
+    bitvector_typet integer_type(
+      size_is_unsigned ? ID_unsignedbv : ID_signedbv, config.ansi_c.int_width);
     implicit_typecast(size, integer_type);
 
     expr.set(ID_statement, ID_cpp_new_array);
diff --git a/src/cpp/expr2cpp.cpp b/src/cpp/expr2cpp.cpp
@@ -295,7 +295,8 @@ std::string expr2cppt::convert_rec(
   }
   else if(src.id()==ID_verilog_signedbv ||
           src.id()==ID_verilog_unsignedbv)
-    return "sc_lv["+id2string(src.get(ID_width))+"]"+d;
+    return "sc_lv[" + std::to_string(to_bitvector_type(src).get_width()) + "]" +
+           d;
   else if(src.id()==ID_unassigned)
     return "?";
   else if(src.id()==ID_code)
diff --git a/src/goto-instrument/accelerate/overflow_instrumenter.cpp b/src/goto-instrument/accelerate/overflow_instrumenter.cpp
@@ -110,8 +110,8 @@ void overflow_instrumentert::overflow_expr(
     }
 
     const typet &old_type=ns.follow(expr.op0().type());
-    const std::size_t new_width = expr.type().get_size_t(ID_width);
-    const std::size_t old_width = old_type.get_size_t(ID_width);
+    const std::size_t new_width = to_bitvector_type(expr.type()).get_width();
+    const std::size_t old_width = to_bitvector_type(old_type).get_width();
 
     if(type.id()==ID_signedbv)
     {
diff --git a/src/solvers/flattening/boolbv_not.cpp b/src/solvers/flattening/boolbv_not.cpp
@@ -19,9 +19,10 @@ bvt boolbvt::convert_not(const not_exprt &expr)
   if(op_type.id()!=ID_verilog_signedbv ||
      op_type.id()!=ID_verilog_unsignedbv)
   {
-    if((expr.type().id()==ID_verilog_signedbv ||
-        expr.type().id()==ID_verilog_unsignedbv) &&
-        expr.type().get_size_t(ID_width) == 1)
+    if(
+      (expr.type().id() == ID_verilog_signedbv ||
+       expr.type().id() == ID_verilog_unsignedbv) &&
+      to_bitvector_type(expr.type()).get_width() == 1)
     {
       literalt has_x_or_z=bv_utils.verilog_bv_has_x_or_z(op_bv);
       literalt normal_bits_zero=
diff --git a/src/solvers/flattening/boolbv_reduction.cpp b/src/solvers/flattening/boolbv_reduction.cpp
@@ -76,9 +76,10 @@ bvt boolbvt::convert_bv_reduction(const unary_exprt &expr)
   if(op_type.id()!=ID_verilog_signedbv ||
      op_type.id()!=ID_verilog_unsignedbv)
   {
-    if((expr.type().id()==ID_verilog_signedbv ||
-        expr.type().id()==ID_verilog_unsignedbv) &&
-        expr.type().get_size_t(ID_width) == 1)
+    if(
+      (expr.type().id() == ID_verilog_signedbv ||
+       expr.type().id() == ID_verilog_unsignedbv) &&
+      to_bitvector_type(expr.type()).get_width() == 1)
     {
       bvt bv;
       bv.resize(2);
diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp
@@ -105,7 +105,7 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
           type_id==ID_verilog_unsignedbv)
   {
     // we encode with two bits
-    std::size_t size = type.get_size_t(ID_width);
+    std::size_t size = to_bitvector_type(type).get_width();
     DATA_INVARIANT(
       size > 0, "verilog bitvector width shall be greater than zero");
     entry.total_width = size * 2;
@@ -175,7 +175,7 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
   else if(type_id==ID_c_enum)
   {
     // these have a subtype
-    entry.total_width = type.subtype().get_size_t(ID_width);
+    entry.total_width = to_bitvector_type(type.subtype()).get_width();
     CHECK_RETURN(entry.total_width > 0);
   }
   else if(type_id==ID_incomplete_c_enum)
diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp
@@ -153,7 +153,7 @@ constant_exprt from_integer(
   else if(type_id==ID_c_enum)
   {
     const std::size_t width =
-      to_c_enum_type(type).subtype().get_size_t(ID_width);
+      to_bitvector_type(to_c_enum_type(type).subtype()).get_width();
     return constant_exprt(integer2bvrep(int_value, width), type);
   }
   else if(type_id==ID_c_bool)
diff --git a/src/util/bv_arithmetic.cpp b/src/util/bv_arithmetic.cpp
@@ -43,7 +43,7 @@ void bv_spect::from_type(const typet &type)
   else
     UNREACHABLE;
 
-  width=unsafe_string2unsigned(type.get_string(ID_width));
+  width = to_bitvector_type(type).get_width();
 }
 
 void bv_arithmetict::print(std::ostream &out) const
diff --git a/src/util/json_expr.cpp b/src/util/json_expr.cpp
@@ -283,8 +283,8 @@ json_objectt json(
     {
       result["name"]=json_stringt("integer");
       result["binary"] = json_stringt(binary(constant_expr));
-      result["width"] =
-        json_numbert(to_c_enum_type(type).subtype().get_string(ID_width));
+      result["width"] = json_numbert(std::to_string(
+        to_bitvector_type(to_c_enum_type(type).subtype()).get_width()));
       result["type"]=json_stringt("enum");
       result["data"]=json_stringt(value_string);
     }
@@ -303,15 +303,17 @@ json_objectt json(
     else if(type.id()==ID_fixedbv)
     {
       result["name"]=json_stringt("fixed");
-      result["width"]=json_numbert(type.get_string(ID_width));
+      result["width"] =
+        json_numbert(std::to_string(to_bitvector_type(type).get_width()));
       result["binary"] = json_stringt(binary(constant_expr));
       result["data"]=
         json_stringt(fixedbvt(to_constant_expr(expr)).to_ansi_c_string());
     }
     else if(type.id()==ID_floatbv)
     {
       result["name"]=json_stringt("float");
-      result["width"]=json_numbert(type.get_string(ID_width));
+      result["width"] =
+        json_numbert(std::to_string(to_bitvector_type(type).get_width()));
       result["binary"] = json_stringt(binary(constant_expr));
       result["data"]=
         json_stringt(ieee_floatt(to_constant_expr(expr)).to_ansi_c_string());
@@ -349,7 +351,8 @@ json_objectt json(
     else if(type.id()==ID_c_bool)
     {
       result["name"]=json_stringt("integer");
-      result["width"]=json_numbert(type.get_string(ID_width));
+      result["width"] =
+        json_numbert(std::to_string(to_bitvector_type(type).get_width()));
       result["type"]=json_stringt(type_string);
       result["binary"]=json_stringt(expr.get_string(ID_value));
       result["data"]=json_stringt(value_string);
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
@@ -913,7 +913,7 @@ bool simplify_exprt::simplify_concatenation(exprt &expr)
           });
 
         to_constant_expr(opi).set_value(new_value);
-        opi.type().set(ID_width, new_width);
+        to_bitvector_type(opi.type()).set_width(new_width);
         // erase opn
         expr.operands().erase(expr.operands().begin()+i+1);
         result = false;
@@ -943,7 +943,7 @@ bool simplify_exprt::simplify_concatenation(exprt &expr)
         const std::string new_value=
           opi.get_string(ID_value)+opn.get_string(ID_value);
         opi.set(ID_value, new_value);
-        opi.type().set(ID_width, new_value.size());
+        to_bitvector_type(opi.type()).set_width(new_value.size());
         opi.type().id(ID_verilog_unsignedbv);
         // erase opn
         expr.operands().erase(expr.operands().begin()+i+1);
@@ -995,8 +995,7 @@ bool simplify_exprt::simplify_shifts(exprt &expr)
   if(expr.op0().type().id()==ID_unsignedbv ||
      expr.op0().type().id()==ID_signedbv)
   {
-    mp_integer width=
-      string2integer(id2string(expr.op0().type().get(ID_width)));
+    const std::size_t width = to_bitvector_type(expr.op0().type()).get_width();
 
     if(expr.id()==ID_lshr)
     {
diff --git a/src/util/xml_expr.cpp b/src/util/xml_expr.cpp
@@ -196,7 +196,7 @@ xmlt xml(
       result.name="integer";
       result.set_attribute("binary", expr.get_string(ID_value));
       result.set_attribute(
-        "width", to_c_enum_type(type).subtype().get_string(ID_width));
+        "width", to_bitvector_type(to_c_enum_type(type).subtype()).get_width());
       result.set_attribute("c_type", "enum");
 
       mp_integer i;
@@ -218,14 +218,14 @@ xmlt xml(
     else if(type.id()==ID_fixedbv)
     {
       result.name="fixed";
-      result.set_attribute("width", type.get_string(ID_width));
+      result.set_attribute("width", to_bitvector_type(type).get_width());
       result.set_attribute("binary", expr.get_string(ID_value));
       result.data=fixedbvt(to_constant_expr(expr)).to_ansi_c_string();
     }
     else if(type.id()==ID_floatbv)
     {
       result.name="float";
-      result.set_attribute("width", type.get_string(ID_width));
+      result.set_attribute("width", to_bitvector_type(type).get_width());
       result.set_attribute("binary", expr.get_string(ID_value));
       result.data=ieee_floatt(to_constant_expr(expr)).to_ansi_c_string();
     }

Original file line number	Diff line number	Diff line change
`@@ -974,7 +974,7 @@ static std::size_t get_bytecode_type_width(const typet &ty)`
`974`	`974`	`{`
`975`	`975`	`if(ty.id()==ID_pointer)`
`976`	`976`	`return 32;`
`977`		`- return ty.get_size_t(ID_width);`
	`977`	`+ return to_bitvector_type(ty).get_width();`
`978`	`978`	`}`
`979`	`979`
`980`	`980`	`code_blockt java_bytecode_convert_methodt::convert_instructions(`
`@@ -2646,7 +2646,7 @@ exprt::operandst &java_bytecode_convert_methodt::convert_ushr(`
`2646`	`2646`	`{`
`2647`	`2647`	`const typet type = java_type_from_char(statement[0]);`
`2648`	`2648`
`2649`		`- const std::size_t width = type.get_size_t(ID_width);`
	`2649`	`+ const std::size_t width = get_bytecode_type_width(type);`
`2650`	`2650`	`typet target = unsignedbv_typet(width);`
`2651`	`2651`
`2652`	`2652`	`exprt lhs = op[0];`
Original file line number	Diff line number	Diff line change
`@@ -76,7 +76,8 @@ void c_typecheck_baset::typecheck_type(typet &type)`
`76`	`76`	`else if(type.id()==ID_pointer)`
`77`	`77`	`{`
`78`	`78`	`typecheck_type(type.subtype());`
`79`		`- INVARIANT(!type.get(ID_width).empty(), "pointers must have width");`
	`79`	`+ INVARIANT(`
	`80`	`+ to_bitvector_type(type).get_width() > 0, "pointers must have width");`
`80`	`81`	`}`
`81`	`82`	`else if(type.id()==ID_struct \|\|`
`82`	`83`	`type.id()==ID_union)`
`@@ -1433,7 +1434,7 @@ void c_typecheck_baset::typecheck_c_bit_field_type(c_bit_field_typet &type)`
`1433`	`1434`	`throw 0;`
`1434`	`1435`	`}`
`1435`	`1436`
`1436`		`- sub_width = c_enum_type.subtype().get_size_t(ID_width);`
	`1437`	`+ sub_width = to_bitvector_type(c_enum_type.subtype()).get_width();`
`1437`	`1438`	`}`
`1438`	`1439`	`else`
`1439`	`1440`	`{`
Original file line number	Diff line number	Diff line change
`@@ -244,7 +244,7 @@ std::string expr2ct::convert_rec(`
`244`	`244`	`return q+"long double"+d;`
`245`	`245`	`else`
`246`	`246`	`{`
`247`		`- std::string swidth=src.get_string(ID_width);`
	`247`	`+ std::string swidth = std::to_string(width);`
`248`	`248`	`std::string fwidth=src.get_string(ID_f);`
`249`	`249`	`return q + CPROVER_PREFIX + "floatbv[" + swidth + "][" + fwidth + "]";`
`250`	`250`	`}`
`@@ -282,7 +282,7 @@ std::string expr2ct::convert_rec(`
`282`	`282`
`283`	`283`	`// There is also wchar_t among the above, but this isn't a C type.`
`284`	`284`
`285`		`- mp_integer width=string2integer(src.get_string(ID_width));`
	`285`	`+ const std::size_t width = to_bitvector_type(src).get_width();`
`286`	`286`
`287`	`287`	`bool is_signed=src.id()==ID_signedbv;`
`288`	`288`	`std::string sign_str=is_signed?"signed ":"unsigned ";`
Original file line number	Diff line number	Diff line change
`@@ -123,7 +123,7 @@ underlying_width(const c_bit_field_typet &type, const namespacet &ns)`
`123`	`123`	`const typet &c_enum_type = ns.follow_tag(to_c_enum_tag_type(subtype));`
`124`	`124`
`125`	`125`	`if(c_enum_type.id() == ID_c_enum)`
`126`		`- return c_enum_type.subtype().get_size_t(ID_width);`
	`126`	`+ return to_bitvector_type(c_enum_type.subtype()).get_width();`
`127`	`127`	`else`
`128`	`128`	`return {};`
`129`	`129`	`}`