Support shuffle_vector_exprt in goto programs

de4557f added support for _builtin_shuffle/__builtin_shufflevector via
a shuffle_vector_exprt. This expression, however, was lowered right away
in the C front end, making it unavailable to other language front-ends.
By moving the lowering to `remove_vector` there no longer is such a
limitation. Kani will be able to use it directly for Rust programs.

Regression test cbmc/gcc_vector3 continues to pass, demonstrating that
processing via the C front-end works as before.

Fixes: #6297

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);