allow binary arithmetic of a vector type and a scalar type

regression/cbmc/gcc_vector1/main.c

@@ -18,6 +18,7 @@ int main()
 
   vector_u x, y, z;
 
+  // vector operator vector
   z.v=x.v+y.v;
 
   assert(z.members[0]==x.members[0]+y.members[0]);
@@ -46,6 +47,22 @@ int main()
   assert(z.members[2]==~x.members[2]);
   assert(z.members[3]==~x.members[3]);
 
+  // vector operator scalar
+  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);
+
+  // unary operators on vectors
+  z=x;
+  z.v=-z.v;
+  assert(z.members[0]==-x.members[0]);
+  assert(z.members[1]==-x.members[1]);
+  assert(z.members[2]==-x.members[2]);
+  assert(z.members[3]==-x.members[3]);
+
   // build vector with typecast
   z.v=(v4si){ 0, 1, 2, 3 };
   assert(z.members[0]==0 && z.members[1]==1 && z.members[2]==2 && z.members[3]==3);

src/ansi-c/c_typecheck_expr.cpp

@@ -2983,6 +2983,24 @@ void c_typecheck_baset::typecheck_expr_binary_arithmetic(exprt &expr)
       return;
     }
   }
+  else if(
+    o_type0.id() == ID_vector && o_type1.id() != ID_vector &&
+    is_number(o_type1))
+  {
+    // convert op1 to the vector type
+    op1.make_typecast(o_type0);
+    expr.type() = o_type0;
+    return;
+  }
+  else if(
+    o_type0.id() != ID_vector && o_type1.id() == ID_vector &&
+    is_number(o_type0))
+  {
+    // convert op0 to the vector type
+    op0.make_typecast(o_type1);
+    expr.type() = o_type1;
+    return;
+  }
 
   // promote!
 

src/goto-programs/remove_vector.cpp

@@ -135,6 +135,23 @@ static void remove_vector(exprt &expr)
     {
       expr.id(ID_array);
     }
+    else if(expr.id() == ID_typecast)
+    {
+      const auto &op = to_typecast_expr(expr).op();
+
+      if(op.type().id() != ID_array)
+      {
+        // (vector-type) x ==> { x, x, ..., x }
+        remove_vector(expr.type());
+        array_typet array_type = to_array_type(expr.type());
+        const auto dimension = numeric_cast_v<std::size_t>(array_type.size());
+        exprt casted_op =
+          typecast_exprt::conditional_cast(op, array_type.subtype());
+        array_exprt array_expr(array_type);
+        array_expr.operands().resize(dimension, op);
+        expr = array_expr;
+      }
+    }
   }
 
   remove_vector(expr.type());