Avoid breaking all sharing on remove_vector/complex when the program doesn't use those features.

Author: smowton

src/goto-programs/remove_complex.cpp

@@ -60,8 +60,20 @@ Purpose: removes complex data type
 
 \*******************************************************************/
 
+static bool contains_complex(const exprt& e)
+{
+  if(e.type().id()==ID_complex)
+    return true;
+  forall_operands(it,e)
+    if(contains_complex(*it))
+      return true;
+  return false;
+}
+
 void remove_complex(exprt &expr)
 {
+  if(!contains_complex(expr))
+    return;
   if(expr.id()==ID_typecast)
   {
     assert(expr.operands().size()==1);
@@ -200,8 +212,38 @@ Purpose: removes complex data type
 
 \*******************************************************************/
 
+static bool contains_complex(const typet& type)
+{
+  if(type.id()==ID_struct || type.id()==ID_union)
+  {
+    const struct_union_typet &struct_union_type=
+      to_struct_union_type(type);
+    for(struct_union_typet::componentst::const_iterator
+	it=struct_union_type.components().begin();
+        it!=struct_union_type.components().end();
+        it++)
+    {
+      if(contains_complex(it->type()))
+	return true;
+    }
+  }
+  else if(type.id()==ID_pointer ||
+          type.id()==ID_vector ||
+          type.id()==ID_array)
+  {
+    if(contains_complex(type.subtype()))
+      return true;
+  }
+  else if(type.id()==ID_complex)
+    return true;
+
+  return false;
+}
+
 void remove_complex(typet &type)
 {
+  if(!contains_complex(type))
+    return;
   if(type.id()==ID_struct || type.id()==ID_union)
   {
     struct_union_typet &struct_union_type=

src/goto-programs/remove_vector.cpp

@@ -15,6 +15,46 @@ Date:   September 2014
 void remove_vector(typet &);
 void remove_vector(exprt &);
 
+static bool contains_vector(const typet& type)
+{
+  // Determine whether remove_vector is necessary, without breaking sharing.
+  if(type.id()==ID_struct || type.id()==ID_union)
+  {
+    const struct_union_typet &struct_union_type=
+      to_struct_union_type(type);
+
+    for(struct_union_typet::componentst::const_iterator
+	it=struct_union_type.components().begin();
+        it!=struct_union_type.components().end();
+        it++)
+    {
+      if(contains_vector(it->type()))
+	return true;	
+    }
+  }
+  else if(type.id()==ID_pointer ||
+          type.id()==ID_complex ||
+          type.id()==ID_array)
+  {
+    if(contains_vector(type.subtype()))
+      return true;
+       
+  }
+  else if(type.id()==ID_vector)
+    return true;
+  return false;
+}
+
+static bool contains_vector(const exprt& e)
+{
+  if(e.type().id()==ID_vector)
+    return true;
+  forall_operands(it,e)
+    if(contains_vector(*it))
+      return true;
+  return false;
+}
+
 /*******************************************************************\
 
 Function: remove_vector
@@ -29,6 +69,9 @@ Purpose: removes vector data type
 
 void remove_vector(exprt &expr)
 {
+  if(!contains_vector(expr))
+    return;
+  
   Forall_operands(it, expr)
     remove_vector(*it);
 
@@ -111,6 +154,8 @@ Purpose: removes vector data type
 
 void remove_vector(typet &type)
 {
+  if(!contains_vector(type))
+    return;
   if(type.id()==ID_struct || type.id()==ID_union)
   {
     struct_union_typet &struct_union_type=