Remove unnecessary use of ns.follow in flattening

Only structs, unions, enums can be hidden behind tags. And keeping symbol or tag
types in the mapping is just fine, there is no need to store the expanded
version.

Author: tautschnig

src/solvers/flattening/arrays.cpp

@@ -55,7 +55,7 @@ literalt arrayst::record_array_equality(
   }
 
   DATA_INVARIANT(
-    ns.follow(op0.type()).id()==ID_array,
+    op0.type().id() == ID_array,
     "record_array_equality parameter should be array-typed");
 
   array_equalities.push_back(array_equalityt());
@@ -90,7 +90,7 @@ void arrayst::collect_indices(const exprt &expr)
     const index_exprt &e = to_index_expr(expr);
     collect_indices(e.index()); // necessary?
 
-    const typet &array_op_type=ns.follow(e.array().type());
+    const typet &array_op_type = e.array().type();
 
     if(array_op_type.id()==ID_array)
     {
@@ -107,8 +107,7 @@ void arrayst::collect_indices(const exprt &expr)
 
 void arrayst::collect_arrays(const exprt &a)
 {
-  const array_typet &array_type=
-    to_array_type(ns.follow(a.type()));
+  const array_typet &array_type = to_array_type(a.type());
 
   if(a.id()==ID_with)
   {
@@ -337,7 +336,7 @@ void arrayst::add_array_Ackermann_constraints()
 
           if(indices_equal_lit!=const_literal(false))
           {
-            const typet &subtype=ns.follow(arrays[i].type()).subtype();
+            const typet &subtype = arrays[i].type().subtype();
             index_exprt index_expr1(arrays[i], *i1, subtype);
 
             index_exprt index_expr2=index_expr1;
@@ -415,10 +414,10 @@ void arrayst::add_array_constraints_equality(
 
   for(const auto &index : index_set)
   {
-    const typet &subtype1=ns.follow(array_equality.f1.type()).subtype();
+    const typet &subtype1 = array_equality.f1.type().subtype();
     index_exprt index_expr1(array_equality.f1, index, subtype1);
 
-    const typet &subtype2=ns.follow(array_equality.f2.type()).subtype();
+    const typet &subtype2 = array_equality.f2.type().subtype();
     index_exprt index_expr2(array_equality.f2, index, subtype2);
 
     DATA_INVARIANT(
@@ -477,7 +476,7 @@ void arrayst::add_array_constraints(
     // add a[i]=b[i]
     for(const auto &index : index_set)
     {
-      const typet &subtype=ns.follow(expr.type()).subtype();
+      const typet &subtype = expr.type().subtype();
       index_exprt index_expr1(expr, index, subtype);
       index_exprt index_expr2(expr.op0(), index, subtype);
 
@@ -514,7 +513,7 @@ void arrayst::add_array_constraints_with(
   const exprt &value=expr.new_value();
 
   {
-    index_exprt index_expr(expr, index, ns.follow(expr.type()).subtype());
+    index_exprt index_expr(expr, index, expr.type().subtype());
 
     if(index_expr.type()!=value.type())
     {
@@ -545,7 +544,7 @@ void arrayst::add_array_constraints_with(
 
       if(guard_lit!=const_literal(true))
       {
-        const typet &subtype=ns.follow(expr.type()).subtype();
+        const typet &subtype = expr.type().subtype();
         index_exprt index_expr1(expr, other_index, subtype);
         index_exprt index_expr2(expr.op0(), other_index, subtype);
 
@@ -584,7 +583,7 @@ void arrayst::add_array_constraints_update(
   const exprt &value=expr.new_value();
 
   {
-    index_exprt index_expr(expr, index, ns.follow(expr.type()).subtype());
+    index_exprt index_expr(expr, index, expr.type().subtype());
 
     if(index_expr.type()!=value.type())
     {
@@ -613,7 +612,7 @@ void arrayst::add_array_constraints_update(
 
       if(guard_lit!=const_literal(true))
       {
-        const typet &subtype=ns.follow(expr.type()).subtype();
+        const typet &subtype=expr.type().subtype();
         index_exprt index_expr1(expr, other_index, subtype);
         index_exprt index_expr2(expr.op0(), other_index, subtype);
 
@@ -643,7 +642,7 @@ void arrayst::add_array_constraints_array_of(
 
   for(const auto &index : index_set)
   {
-    const typet &subtype=ns.follow(expr.type()).subtype();
+    const typet &subtype = expr.type().subtype();
     index_exprt index_expr(expr, index, subtype);
 
     DATA_INVARIANT(
@@ -672,7 +671,7 @@ void arrayst::add_array_constraints_if(
 
   for(const auto &index : index_set)
   {
-    const typet subtype=ns.follow(expr.type()).subtype();
+    const typet subtype = expr.type().subtype();
     index_exprt index_expr1(expr, index, subtype);
     index_exprt index_expr2(expr.true_case(), index, subtype);
 
@@ -690,7 +689,7 @@ void arrayst::add_array_constraints_if(
   // now the false case
   for(const auto &index : index_set)
   {
-    const typet subtype=ns.follow(expr.type()).subtype();
+    const typet subtype = expr.type().subtype();
     index_exprt index_expr1(expr, index, subtype);
     index_exprt index_expr2(expr.false_case(), index, subtype);
 

src/solvers/flattening/boolbv.cpp

@@ -628,9 +628,6 @@ exprt boolbvt::make_free_bv_expr(const typet &type)
 
 bool boolbvt::is_unbounded_array(const typet &type) const
 {
-  if(type.id() == ID_symbol_type)
-    return is_unbounded_array(ns.follow(type));
-
   if(type.id()!=ID_array)
     return false;
 

src/solvers/flattening/boolbv.h

@@ -32,15 +32,13 @@ class member_exprt;
 class boolbvt:public arrayst
 {
 public:
-  boolbvt(
-    const namespacet &_ns,
-    propt &_prop):
-    arrayst(_ns, _prop),
-    unbounded_array(unbounded_arrayt::U_NONE),
-    boolbv_width(_ns),
-    bv_utils(_prop),
-    functions(*this),
-    map(_prop, _ns, boolbv_width)
+  boolbvt(const namespacet &_ns, propt &_prop)
+    : arrayst(_ns, _prop),
+      unbounded_array(unbounded_arrayt::U_NONE),
+      boolbv_width(_ns),
+      bv_utils(_prop),
+      functions(*this),
+      map(_prop, boolbv_width)
   {
   }
 

src/solvers/flattening/boolbv_add_sub.cpp

@@ -19,7 +19,7 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
     expr.id() == ID_plus || expr.id() == ID_minus ||
     expr.id() == "no-overflow-plus" || expr.id() == "no-overflow-minus");
 
-  const typet &type=ns.follow(expr.type());
+  const typet &type = expr.type();
 
   if(type.id()!=ID_unsignedbv &&
      type.id()!=ID_signedbv &&
@@ -53,9 +53,8 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
   bool no_overflow=(expr.id()=="no-overflow-plus" ||
                     expr.id()=="no-overflow-minus");
 
-  typet arithmetic_type=
-    (type.id()==ID_vector || type.id()==ID_complex)?
-      ns.follow(type.subtype()):type;
+  typet arithmetic_type =
+    (type.id() == ID_vector || type.id() == ID_complex) ? type.subtype() : type;
 
   bv_utilst::representationt rep=
     (arithmetic_type.id()==ID_signedbv ||

src/solvers/flattening/boolbv_floatbv_op.cpp

@@ -23,8 +23,8 @@ bvt boolbvt::convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
   bvt bv0=convert_bv(op0);
   bvt bv1=convert_bv(op1);
 
-  const typet &src_type=ns.follow(expr.op0().type());
-  const typet &dest_type=ns.follow(expr.type());
+  const typet &src_type = expr.op0().type();
+  const typet &dest_type = expr.type();
 
   if(src_type==dest_type) // redundant type cast?
     return bv0;
@@ -94,17 +94,16 @@ bvt boolbvt::convert_floatbv_op(const exprt &expr)
   bvt rhs_as_bv = convert_bv(rhs);
   bvt rounding_mode_as_bv = convert_bv(rounding_mode);
 
-  const typet &resolved_type = ns.follow(expr.type());
   DATA_INVARIANT_WITH_DIAGNOSTICS(
-    lhs.type() == resolved_type && rhs.type() == resolved_type,
-    "both operands of a floating point operator must have the same type",
+    lhs.type() == expr.type() && rhs.type() == expr.type(),
+    "both operands of a floating point operator must match the expression type",
     irep_pretty_diagnosticst{expr});
 
   float_utilst float_utils(prop);
 
   float_utils.set_rounding_mode(rounding_mode_as_bv);
 
-  if(resolved_type.id() == ID_floatbv)
+  if(expr.type().id() == ID_floatbv)
   {
     float_utils.spec=ieee_float_spect(to_floatbv_type(expr.type()));
 
@@ -121,15 +120,15 @@ bvt boolbvt::convert_floatbv_op(const exprt &expr)
     else
       UNREACHABLE;
   }
-  else if(resolved_type.id() == ID_vector || resolved_type.id() == ID_complex)
+  else if(expr.type().id() == ID_vector || expr.type().id() == ID_complex)
   {
-    const typet &subtype = ns.follow(resolved_type.subtype());
+    const typet &subtype = expr.type().subtype();
 
     if(subtype.id()==ID_floatbv)
     {
       float_utils.spec=ieee_float_spect(to_floatbv_type(subtype));
 
-      std::size_t width = boolbv_width(resolved_type);
+      std::size_t width = boolbv_width(expr.type());
       std::size_t sub_width=boolbv_width(subtype);
 
       DATA_INVARIANT(

src/solvers/flattening/boolbv_get.cpp

@@ -71,9 +71,6 @@ exprt boolbvt::bv_get_rec(
   std::size_t offset,
   const typet &type) const
 {
-  if(type.id() == ID_symbol_type)
-    return bv_get_rec(bv, unknown, offset, ns.follow(type));
-
   std::size_t width=boolbv_width(type);
 
   assert(bv.size()==unknown.size());
@@ -143,7 +140,7 @@ exprt boolbvt::bv_get_rec(
 
       for(const auto &c : components)
       {
-        const typet &subtype = ns.follow(c.type());
+        const typet &subtype = c.type();
         op.push_back(nil_exprt());
 
         std::size_t sub_width=boolbv_width(subtype);
@@ -178,7 +175,7 @@ exprt boolbvt::bv_get_rec(
     }
     else if(type.id()==ID_vector)
     {
-      const typet &subtype=ns.follow(type.subtype());
+      const typet &subtype = type.subtype();
       std::size_t sub_width=boolbv_width(subtype);
 
       if(sub_width!=0 && width%sub_width==0)
@@ -196,7 +193,7 @@ exprt boolbvt::bv_get_rec(
     }
     else if(type.id()==ID_complex)
     {
-      const typet &subtype=ns.follow(type.subtype());
+      const typet &subtype = type.subtype();
       std::size_t sub_width=boolbv_width(subtype);
 
       if(sub_width!=0 && width==sub_width*2)

src/solvers/flattening/boolbv_index.cpp

@@ -21,7 +21,7 @@ bvt boolbvt::convert_index(const index_exprt &expr)
   const exprt &array=expr.array();
   const exprt &index=expr.index();
 
-  const typet &array_op_type=ns.follow(array.type());
+  const typet &array_op_type = array.type();
 
   bvt bv;
 
@@ -276,8 +276,7 @@ bvt boolbvt::convert_index(
   const exprt &array,
   const mp_integer &index)
 {
-  const array_typet &array_type=
-    to_array_type(ns.follow(array.type()));
+  const array_typet &array_type = to_array_type(array.type());
 
   std::size_t width=boolbv_width(array_type.subtype());
 

src/solvers/flattening/boolbv_map.cpp

@@ -50,9 +50,6 @@ boolbv_mapt::map_entryt &boolbv_mapt::get_map_entry(
   const irep_idt &identifier,
   const typet &type)
 {
-  if(type.id() == ID_symbol_type)
-    return get_map_entry(identifier, ns.follow(type));
-
   std::pair<mappingt::iterator, bool> result=
     mapping.insert(std::pair<irep_idt, map_entryt>(
       identifier, map_entryt()));

src/solvers/flattening/boolbv_map.h

@@ -23,11 +23,8 @@ Author: Daniel Kroening, [email protected]
 class boolbv_mapt
 {
 public:
-  boolbv_mapt(
-    propt &_prop,
-    const namespacet &_ns,
-    const boolbv_widtht &_boolbv_width):
-    prop(_prop), ns(_ns), boolbv_width(_boolbv_width)
+  boolbv_mapt(propt &_prop, const boolbv_widtht &_boolbv_width)
+    : prop(_prop), boolbv_width(_boolbv_width)
   {
   }
 
@@ -81,7 +78,6 @@ class boolbv_mapt
 
 protected:
   propt ∝
-  const namespacet &ns;
   const boolbv_widtht &boolbv_width;
 };
 

src/solvers/flattening/boolbv_power.cpp

@@ -11,7 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 bvt boolbvt::convert_power(const binary_exprt &expr)
 {
-  const typet &type=ns.follow(expr.type());
+  const typet &type = expr.type();
 
   std::size_t width=boolbv_width(type);
 

src/solvers/flattening/boolbv_typecast.cpp

@@ -19,14 +19,12 @@ Author: Daniel Kroening, [email protected]
 
 bvt boolbvt::convert_bv_typecast(const typecast_exprt &expr)
 {
-  const typet &expr_type=ns.follow(expr.type());
   const exprt &op=expr.op();
-  const typet &op_type=ns.follow(op.type());
   const bvt &op_bv=convert_bv(op);
 
   bvt bv;
 
-  if(type_conversion(op_type, op_bv, expr_type, bv))
+  if(type_conversion(op.type(), op_bv, expr.type(), bv))
     return conversion_failed(expr);
 
   return bv;
@@ -84,15 +82,9 @@ bool boolbvt::type_conversion(
       lower.assign(src.begin(), src.begin()+src.size()/2);
       upper.assign(src.begin()+src.size()/2, src.end());
       type_conversion(
-        ns.follow(src_type.subtype()),
-        lower,
-        ns.follow(dest_type.subtype()),
-        lower_res);
+        src_type.subtype(), lower, dest_type.subtype(), lower_res);
       type_conversion(
-        ns.follow(src_type.subtype()),
-        upper,
-        ns.follow(dest_type.subtype()),
-        upper_res);
+        src_type.subtype(), upper, dest_type.subtype(), upper_res);
       INVARIANT(
         lower_res.size() + upper_res.size() == dest_width,
         "lower result bitvector size plus upper result bitvector size shall "
@@ -526,17 +518,17 @@ bool boolbvt::type_conversion(
         return false;
       }
     }
-    else if(dest_type.id()==ID_struct)
+    else if(ns.follow(dest_type).id() == ID_struct)
     {
-      const struct_typet &dest_struct=to_struct_type(dest_type);
+      const struct_typet &dest_struct = to_struct_type(ns.follow(dest_type));
 
-      if(src_type.id()==ID_struct)
+      if(ns.follow(src_type).id() == ID_struct)
       {
         // we do subsets
 
         dest.resize(dest_width, const_literal(false));
 
-        const struct_typet &op_struct=to_struct_type(src_type);
+        const struct_typet &op_struct = to_struct_type(ns.follow(src_type));
 
         const struct_typet::componentst &dest_comp=
           dest_struct.components();

src/solvers/flattening/boolbv_unary_minus.cpp

@@ -19,7 +19,7 @@ Author: Daniel Kroening, [email protected]
 
 bvt boolbvt::convert_unary_minus(const unary_minus_exprt &expr)
 {
-  const typet &type=ns.follow(expr.type());
+  const typet &type = expr.type();
 
   std::size_t width=boolbv_width(type);
 
@@ -36,7 +36,7 @@ bvt boolbvt::convert_unary_minus(const unary_minus_exprt &expr)
   if(bvtype==bvtypet::IS_UNKNOWN &&
      (type.id()==ID_vector || type.id()==ID_complex))
   {
-    const typet &subtype=ns.follow(type.subtype());
+    const typet &subtype = type.subtype();
 
     std::size_t sub_width=boolbv_width(subtype);