diff --git a/regression/cbmc/gcc_vector1/main.c b/regression/cbmc/gcc_vector1/main.c index f52283d75b1..a7609613b97 100644 --- a/regression/cbmc/gcc_vector1/main.c +++ b/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; diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index a53b6f32343..335c8004890 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/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) { diff --git a/src/goto-programs/remove_vector.cpp b/src/goto-programs/remove_vector.cpp index 3844bcbaac2..e824ec945b7 100644 --- a/src/goto-programs/remove_vector.cpp +++ b/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