Merge pull request #6645 from tautschnig/features/shuffle_vector-middle-end

Support shuffle_vector_exprt in goto programs

Author: tautschnig

src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp

@@ -1459,7 +1459,7 @@ exprt c_typecheck_baset::typecheck_shuffle_vector(
       operands.push_back(std::move(mod_index));
     }
 
-    return shuffle_vector_exprt{arg0, arg1, std::move(operands)}.lower();
+    return shuffle_vector_exprt{arg0, arg1, std::move(operands)};
   }
   else if(identifier == "__builtin_shufflevector")
   {
@@ -1509,8 +1509,8 @@ exprt c_typecheck_baset::typecheck_shuffle_vector(
       }
     }
 
-    return shuffle_vector_exprt{arguments[0], arguments[1], std::move(operands)}
-      .lower();
+    return shuffle_vector_exprt{
+      arguments[0], arguments[1], std::move(operands)};
   }
   else
     UNREACHABLE;

src/goto-programs/remove_vector.cpp

@@ -16,6 +16,8 @@ Date:   September 2014
 #include <util/arith_tools.h>
 #include <util/std_expr.h>
 
+#include <ansi-c/c_expr.h>
+
 #include "goto_model.h"
 
 static bool have_to_remove_vector(const typet &type);
@@ -41,6 +43,8 @@ static bool have_to_remove_vector(const exprt &expr)
     {
       return true;
     }
+    else if(expr.id() == ID_shuffle_vector)
+      return true;
     else if(expr.id()==ID_vector)
       return true;
   }
@@ -93,6 +97,14 @@ static void remove_vector(exprt &expr)
   if(!have_to_remove_vector(expr))
     return;
 
+  if(expr.id() == ID_shuffle_vector)
+  {
+    exprt result = to_shuffle_vector_expr(expr).lower();
+    remove_vector(result);
+    expr.swap(result);
+    return;
+  }
+
   Forall_operands(it, expr)
     remove_vector(*it);