Support ==,!=,<,<=,>,>= over vectors

These need to be rewritten to point-wise applications and return -1
(true) or 0 (false) per element.

Fixes: #5930

Author: tautschnig

regression/cbmc/gcc_vector1/main.c

@@ -105,6 +105,20 @@ int main()
   assert(z.members[2]==-x.members[2]);
   assert(z.members[3]==-x.members[3]);
 
+  // Boolean operators on vectors
+  z = x;
+  y.v = z.v == x.v;
+  assert(y.members[0]);
+  assert(y.members[1]);
+  assert(y.members[2]);
+  assert(y.members[3]);
+
+  y.v = x.v <= z.v;
+  assert(y.members[0]);
+  assert(y.members[1]);
+  assert(y.members[2]);
+  assert(y.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/goto-programs/remove_vector.cpp

@@ -35,6 +35,12 @@ static bool have_to_remove_vector(const exprt &expr)
     }
     else if(expr.id()==ID_unary_minus || expr.id()==ID_bitnot)
       return true;
+    else if(
+      expr.id() == ID_equal || expr.id() == ID_notequal || expr.id() == ID_lt ||
+      expr.id() == ID_le || expr.id() == ID_gt || expr.id() == ID_ge)
+    {
+      return true;
+    }
     else if(expr.id()==ID_vector)
       return true;
   }
@@ -103,6 +109,7 @@ static void remove_vector(exprt &expr)
       // x+y -> vector(x[0]+y[0],x[1]+y[1],...)
       array_exprt array_expr({}, array_type);
       array_expr.operands().resize(numeric_cast_v<std::size_t>(dimension));
+      array_expr.add_source_location() = expr.source_location();
 
       for(std::size_t i=0; i<array_expr.operands().size(); i++)
       {
@@ -130,6 +137,7 @@ static void remove_vector(exprt &expr)
       // -x -> vector(-x[0],-x[1],...)
       array_exprt array_expr({}, array_type);
       array_expr.operands().resize(numeric_cast_v<std::size_t>(dimension));
+      array_expr.add_source_location() = expr.source_location();
 
       for(std::size_t i=0; i<array_expr.operands().size(); i++)
       {
@@ -141,6 +149,41 @@ static void remove_vector(exprt &expr)
 
       expr=array_expr;
     }
+    else if(
+      expr.id() == ID_equal || expr.id() == ID_notequal || expr.id() == ID_lt ||
+      expr.id() == ID_le || expr.id() == ID_gt || expr.id() == ID_ge)
+    {
+      // component-wise and generate 0 (false) or -1 (true)
+      // x ~ y -> vector(x[0] ~ y[0] ? -1 : 0, x[1] ~ y[1] ? -1 : 0, ...)
+
+      auto const &binary_expr = to_binary_expr(expr);
+      const vector_typet &vector_type = to_vector_type(expr.type());
+      const auto dimension = numeric_cast_v<std::size_t>(vector_type.size());
+
+      const typet &subtype = vector_type.subtype();
+      exprt minus_one = from_integer(-1, subtype);
+      exprt zero = from_integer(0, subtype);
+
+      exprt::operandst operands;
+      operands.reserve(dimension);
+
+      for(std::size_t i = 0; i < dimension; ++i)
+      {
+        exprt index = from_integer(i, vector_type.size().type());
+
+        operands.push_back(
+          if_exprt{binary_relation_exprt{index_exprt{binary_expr.lhs(), index},
+                                         binary_expr.id(),
+                                         index_exprt{binary_expr.rhs(), index}},
+                   minus_one,
+                   zero});
+      }
+
+      source_location source_location = expr.source_location();
+      expr = array_exprt{std::move(operands),
+                         array_typet{subtype, vector_type.size()}};
+      expr.add_source_location() = std::move(source_location);
+    }
     else if(expr.id()==ID_vector)
     {
       expr.id(ID_array);
@@ -158,7 +201,9 @@ static void remove_vector(exprt &expr)
           numeric_cast_v<std::size_t>(to_constant_expr(array_type.size()));
         exprt casted_op =
           typecast_exprt::conditional_cast(op, array_type.subtype());
+        source_location source_location = expr.source_location();
         expr = array_exprt(exprt::operandst(dimension, casted_op), array_type);
+        expr.add_source_location() = std::move(source_location);
       }
     }
   }

src/util/std_expr.h

@@ -664,8 +664,8 @@ class binary_predicate_exprt:public binary_exprt
 
     DATA_CHECK(
       vm,
-      expr.type().id() == ID_bool,
-      "result of binary predicate expression should be of type bool");
+      expr.type().id() == ID_bool || expr.id().id() == ID_vector,
+      "result of binary predicate expression should be of type bool or vector");
   }
 };