Merge pull request diffblue#5812 from tautschnig/fix-vector

Fix type checking of vector expressions

Author: kroening

regression/cbmc/gcc_vector1/main.c

@@ -47,6 +47,13 @@ int main()
   assert(z.members[2]==~x.members[2]);
   assert(z.members[3]==~x.members[3]);
 
+  z = x;
+  z.v <<= (v4si){1, 2, 3, 4};
+  assert(z.members[0] == (x.members[0] << 1));
+  assert(z.members[1] == (x.members[1] << 2));
+  assert(z.members[2] == (x.members[2] << 3));
+  assert(z.members[3] == (x.members[3] << 4));
+
   // vector operator scalar
   z=x;
   z.v=z.v+1;
@@ -55,6 +62,41 @@ int main()
   assert(z.members[2]==x.members[2]+1);
   assert(z.members[3]==x.members[3]+1);
 
+  z = x;
+  z.v += 1;
+  assert(z.members[0] == x.members[0] + 1);
+  assert(z.members[1] == x.members[1] + 1);
+  assert(z.members[2] == x.members[2] + 1);
+  assert(z.members[3] == x.members[3] + 1);
+
+  z = x;
+  z.v = z.v & 1;
+  assert(z.members[0] == (x.members[0] & 1));
+  assert(z.members[1] == (x.members[1] & 1));
+  assert(z.members[2] == (x.members[2] & 1));
+  assert(z.members[3] == (x.members[3] & 1));
+
+  z = x;
+  z.v &= 1;
+  assert(z.members[0] == (x.members[0] & 1));
+  assert(z.members[1] == (x.members[1] & 1));
+  assert(z.members[2] == (x.members[2] & 1));
+  assert(z.members[3] == (x.members[3] & 1));
+
+  z = x;
+  z.v = z.v << 2;
+  assert(z.members[0] == (x.members[0] << 2));
+  assert(z.members[1] == (x.members[1] << 2));
+  assert(z.members[2] == (x.members[2] << 2));
+  assert(z.members[3] == (x.members[3] << 2));
+
+  z = x;
+  z.v <<= 2;
+  assert(z.members[0] == (x.members[0] << 2));
+  assert(z.members[1] == (x.members[1] << 2));
+  assert(z.members[2] == (x.members[2] << 2));
+  assert(z.members[3] == (x.members[3] << 2));
+
   // unary operators on vectors
   z=x;
   z.v=-z.v;

src/ansi-c/c_typecheck_expr.cpp

@@ -3360,6 +3360,7 @@ void c_typecheck_baset::typecheck_expr_shifts(shift_exprt &expr)
     is_number(o_type1))
   {
     // {a0, a1, ..., an} >> b == {a0 >> b, a1 >> b, ..., an >> b}
+    op1 = typecast_exprt(op1, o_type0);
     expr.type()=op0.type();
     return;
   }
@@ -3586,6 +3587,21 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
   else if(statement==ID_assign_shl ||
           statement==ID_assign_shr)
   {
+    if(o_type0.id() == ID_vector)
+    {
+      if(
+        o_type1.id() == ID_vector && o_type0.subtype() == o_type1.subtype() &&
+        is_number(o_type0.subtype()))
+      {
+        return;
+      }
+      else if(is_number(o_type0.subtype()) && is_number(o_type1))
+      {
+        op1 = typecast_exprt(op1, o_type0);
+        return;
+      }
+    }
+
     implicit_typecast_arithmetic(op0);
     implicit_typecast_arithmetic(op1);
 
@@ -3650,6 +3666,16 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
         return;
       }
     }
+    else if(
+      o_type0.id() == ID_vector &&
+      (o_type1.id() == ID_bool || o_type1.id() == ID_c_bool ||
+       o_type1.id() == ID_c_enum_tag || o_type1.id() == ID_unsignedbv ||
+       o_type1.id() == ID_signedbv))
+    {
+      implicit_typecast_arithmetic(op1);
+      op1 = typecast_exprt(op1, o_type0);
+      return;
+    }
   }
   else
   {
@@ -3670,6 +3696,18 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
         return;
       }
     }
+    else if(o_type0.id() == ID_vector)
+    {
+      implicit_typecast_arithmetic(op1);
+
+      if(
+        is_number(op1.type()) || op1.type().id() == ID_bool ||
+        op1.type().id() == ID_c_bool || op1.type().id() == ID_c_enum_tag)
+      {
+        op1 = typecast_exprt(op1, o_type0);
+        return;
+      }
+    }
     else if(o_type0.id()==ID_bool ||
             o_type0.id()==ID_c_bool)
     {

src/goto-programs/remove_vector.cpp

@@ -25,11 +25,14 @@ static bool have_to_remove_vector(const exprt &expr)
 {
   if(expr.type().id()==ID_vector)
   {
-    if(expr.id()==ID_plus || expr.id()==ID_minus ||
-       expr.id()==ID_mult || expr.id()==ID_div ||
-       expr.id()==ID_mod  || expr.id()==ID_bitxor ||
-       expr.id()==ID_bitand || expr.id()==ID_bitor)
+    if(
+      expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
+      expr.id() == ID_div || expr.id() == ID_mod || expr.id() == ID_bitxor ||
+      expr.id() == ID_bitand || expr.id() == ID_bitor || expr.id() == ID_shl ||
+      expr.id() == ID_lshr || expr.id() == ID_ashr)
+    {
       return true;
+    }
     else if(expr.id()==ID_unary_minus || expr.id()==ID_bitnot)
       return true;
     else if(expr.id()==ID_vector)
@@ -77,10 +80,11 @@ static void remove_vector(exprt &expr)
 
   if(expr.type().id()==ID_vector)
   {
-    if(expr.id()==ID_plus || expr.id()==ID_minus ||
-       expr.id()==ID_mult || expr.id()==ID_div ||
-       expr.id()==ID_mod  || expr.id()==ID_bitxor ||
-       expr.id()==ID_bitand || expr.id()==ID_bitor)
+    if(
+      expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
+      expr.id() == ID_div || expr.id() == ID_mod || expr.id() == ID_bitxor ||
+      expr.id() == ID_bitand || expr.id() == ID_bitor || expr.id() == ID_shl ||
+      expr.id() == ID_lshr || expr.id() == ID_ashr)
     {
       // FIXME plus, mult, bitxor, bitand and bitor are defined as n-ary
       //      operations rather than binary. This code assumes that they