Merge pull request #5940 from tautschnig/fix-5930

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

Author: kroening

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/ansi-c/c_typecheck_base.h

@@ -182,7 +182,7 @@ class c_typecheck_baset:
   virtual void typecheck_expr_member(exprt &expr);
   virtual void typecheck_expr_ptrmember(exprt &expr);
   virtual void typecheck_expr_rel(binary_relation_exprt &expr);
-  virtual void typecheck_expr_rel_vector(binary_relation_exprt &expr);
+  virtual void typecheck_expr_rel_vector(binary_exprt &expr);
   virtual void adjust_float_rel(binary_relation_exprt &);
   static void add_rounding_mode(exprt &);
   virtual void typecheck_expr_index(exprt &expr);

src/ansi-c/c_typecheck_expr.cpp

@@ -1417,18 +1417,12 @@ void c_typecheck_baset::typecheck_expr_rel(
   throw 0;
 }
 
-void c_typecheck_baset::typecheck_expr_rel_vector(
-  binary_relation_exprt &expr)
+void c_typecheck_baset::typecheck_expr_rel_vector(binary_exprt &expr)
 {
-  exprt &op0=expr.op0();
-  exprt &op1=expr.op1();
+  const typet &o_type0 = as_const(expr).op0().type();
+  const typet &o_type1 = as_const(expr).op1().type();
 
-  const typet o_type0 = op0.type();
-  const typet o_type1 = op1.type();
-
-  if(
-    o_type0.id() != ID_vector || o_type1.id() != ID_vector ||
-    o_type0.subtype() != o_type1.subtype())
+  if(o_type0.id() != ID_vector || o_type0 != o_type1)
   {
     error().source_location = expr.source_location();
     error() << "vector operator '" << expr.id() << "' not defined for types '"
@@ -1437,9 +1431,18 @@ void c_typecheck_baset::typecheck_expr_rel_vector(
     throw 0;
   }
 
-  // Comparisons between vectors produce a vector
-  // of integers with the same dimension.
-  expr.type()=vector_typet(signed_int_type(), to_vector_type(o_type0).size());
+  // Comparisons between vectors produce a vector of integers of the same width
+  // with the same dimension.
+  auto subtype_width = to_bitvector_type(o_type0.subtype()).get_width();
+  expr.type() =
+    vector_typet{signedbv_typet{subtype_width}, to_vector_type(o_type0).size()};
+
+  // Replace the id as the semantics of these are point-wise application (and
+  // the result is not of bool type).
+  if(expr.id() == ID_notequal)
+    expr.id(ID_vector_notequal);
+  else
+    expr.id("vector-" + id2string(expr.id()));
 }
 
 void c_typecheck_baset::typecheck_expr_ptrmember(exprt &expr)

src/goto-programs/remove_vector.cpp

@@ -35,6 +35,13 @@ 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_vector_equal || expr.id() == ID_vector_notequal ||
+      expr.id() == ID_vector_lt || expr.id() == ID_vector_le ||
+      expr.id() == ID_vector_gt || expr.id() == ID_vector_ge)
+    {
+      return true;
+    }
     else if(expr.id()==ID_vector)
       return true;
   }
@@ -103,6 +110,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 +138,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 +150,66 @@ static void remove_vector(exprt &expr)
 
       expr=array_expr;
     }
+    else if(
+      expr.id() == ID_vector_equal || expr.id() == ID_vector_notequal ||
+      expr.id() == ID_vector_lt || expr.id() == ID_vector_le ||
+      expr.id() == ID_vector_gt || expr.id() == ID_vector_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();
+      PRECONDITION(subtype.id() == ID_signedbv);
+      exprt minus_one = from_integer(-1, subtype);
+      exprt zero = from_integer(0, subtype);
+
+      exprt::operandst operands;
+      operands.reserve(dimension);
+
+      const bool is_float =
+        binary_expr.lhs().type().subtype().id() == ID_floatbv;
+      irep_idt new_id;
+      if(binary_expr.id() == ID_vector_notequal)
+      {
+        if(is_float)
+          new_id = ID_ieee_float_notequal;
+        else
+          new_id = ID_notequal;
+      }
+      else if(binary_expr.id() == ID_vector_equal)
+      {
+        if(is_float)
+          new_id = ID_ieee_float_equal;
+        else
+          new_id = ID_equal;
+      }
+      else
+      {
+        // just strip the "vector-" prefix
+        new_id = id2string(binary_expr.id()).substr(7);
+      }
+
+      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},
+                                         new_id,
+                                         index_exprt{binary_expr.rhs(), index}},
+                   minus_one,
+                   zero});
+      }
+
+      source_locationt 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 +227,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_locationt 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/irep_ids.def

@@ -843,6 +843,12 @@ IREP_ID_ONE(min)
 IREP_ID_ONE(constant_interval)
 IREP_ID_TWO(C_bounds_check, #bounds_check)
 IREP_ID_ONE(count_leading_zeros)
+IREP_ID_TWO(vector_equal, vector-=)
+IREP_ID_TWO(vector_notequal, vector-!=)
+IREP_ID_TWO(vector_ge, vector->=)
+IREP_ID_TWO(vector_le, vector-<=)
+IREP_ID_TWO(vector_gt, vector->)
+IREP_ID_TWO(vector_lt, vector-<)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.def in their source tree