diff --git a/regression/cbmc/gcc_vector1/main.c b/regression/cbmc/gcc_vector1/main.c index a7609613b97..6c454459d66 100644 --- a/regression/cbmc/gcc_vector1/main.c +++ b/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); diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index 2791da7a694..8a7bda5681b 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/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); diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 975123572cd..25eee7f69e5 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/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) diff --git a/src/goto-programs/remove_vector.cpp b/src/goto-programs/remove_vector.cpp index e824ec945b7..9314fe3a32b 100644 --- a/src/goto-programs/remove_vector.cpp +++ b/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(dimension)); + array_expr.add_source_location() = expr.source_location(); for(std::size_t i=0; i vector(-x[0],-x[1],...) array_exprt array_expr({}, array_type); array_expr.operands().resize(numeric_cast_v(dimension)); + array_expr.add_source_location() = expr.source_location(); for(std::size_t i=0; i 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(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(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); } } } diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 4493e83d4da..e78c3eac98d 100644 --- a/src/util/irep_ids.def +++ b/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