Relax type of bitwise operations to any bitvector

Lowering of the byte extraction and byte update expressions can yield
non-integer bitvector typed operands.
Because we do not require a numeric interpretation of them we can relax
the requirement of integer-typed operands for bitwise operators.

Author: Enrico Steffinlongo

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -367,7 +367,7 @@ static smt_termt convert_expr_to_smt(
   const bitand_exprt &bitwise_and_expr,
   const sub_expression_mapt &converted)
 {
-  if(operands_are_of_type<integer_bitvector_typet>(bitwise_and_expr))
+  if(operands_are_of_type<bitvector_typet>(bitwise_and_expr))
   {
     return convert_multiary_operator_to_terms(
       bitwise_and_expr, converted, smt_bit_vector_theoryt::make_and);
@@ -384,7 +384,7 @@ static smt_termt convert_expr_to_smt(
   const bitor_exprt &bitwise_or_expr,
   const sub_expression_mapt &converted)
 {
-  if(operands_are_of_type<integer_bitvector_typet>(bitwise_or_expr))
+  if(operands_are_of_type<bitvector_typet>(bitwise_or_expr))
   {
     return convert_multiary_operator_to_terms(
       bitwise_or_expr, converted, smt_bit_vector_theoryt::make_or);
@@ -401,7 +401,7 @@ static smt_termt convert_expr_to_smt(
   const bitxor_exprt &bitwise_xor,
   const sub_expression_mapt &converted)
 {
-  if(operands_are_of_type<integer_bitvector_typet>(bitwise_xor))
+  if(operands_are_of_type<bitvector_typet>(bitwise_xor))
   {
     return convert_multiary_operator_to_terms(
       bitwise_xor, converted, smt_bit_vector_theoryt::make_xor);
@@ -418,10 +418,7 @@ static smt_termt convert_expr_to_smt(
   const bitnot_exprt &bitwise_not,
   const sub_expression_mapt &converted)
 {
-  const bool operand_is_bitvector =
-    can_cast_type<integer_bitvector_typet>(bitwise_not.op().type());
-
-  if(operand_is_bitvector)
+  if(can_cast_type<bitvector_typet>(bitwise_not.op().type()))
   {
     return smt_bit_vector_theoryt::make_not(converted.at(bitwise_not.op()));
   }
@@ -436,9 +433,7 @@ static smt_termt convert_expr_to_smt(
   const unary_minus_exprt &unary_minus,
   const sub_expression_mapt &converted)
 {
-  const bool operand_is_bitvector =
-    can_cast_type<integer_bitvector_typet>(unary_minus.op().type());
-  if(operand_is_bitvector)
+  if(can_cast_type<integer_bitvector_typet>(unary_minus.op().type()))
   {
     return smt_bit_vector_theoryt::negate(converted.at(unary_minus.op()));
   }

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -727,20 +727,23 @@ TEST_CASE(
   }
 }
 
-SCENARIO(
+TEMPLATE_TEST_CASE(
   "Bitwise \"AND\" expressions are converted to SMT terms",
-  "[core][smt2_incremental]")
+  "[core][smt2_incrzmental]",
+  signedbv_typet,
+  unsignedbv_typet,
+  bv_typet)
 {
   auto test = expr_to_smt_conversion_test_environmentt::make(test_archt::i386);
-  GIVEN("three integer bitvectors and their smt-term equivalents")
+  GIVEN("three bitvectors and their smt-term equivalents")
   {
     const smt_termt smt_term_one = smt_bit_vector_constant_termt{1, 8};
     const smt_termt smt_term_three = smt_bit_vector_constant_termt{3, 8};
     const smt_termt smt_term_five = smt_bit_vector_constant_termt{5, 8};
 
-    const auto one_bvint = from_integer(1, signedbv_typet{8});
-    const auto three_bvint = from_integer(3, signedbv_typet{8});
-    const auto five_bvint = from_integer(5, signedbv_typet{8});
+    const auto one_bvint = from_integer(1, TestType{8});
+    const auto three_bvint = from_integer(3, TestType{8});
+    const auto five_bvint = from_integer(5, TestType{8});
 
     WHEN("a bitand_exprt with two of them as arguments is converted")
     {
@@ -766,8 +769,7 @@ SCENARIO(
       // support direct construction with multiple operands - so we have to
       // construct its parent class and downcast it.
       const exprt::operandst and_operands{one_bvint, three_bvint, five_bvint};
-      const multi_ary_exprt first_step{
-        ID_bitand, and_operands, signedbv_typet{8}};
+      const multi_ary_exprt first_step{ID_bitand, and_operands, TestType{8}};
       const auto bitand_expr = to_bitand_expr(first_step);
 
       const auto constructed_term = test.convert(bitand_expr);
@@ -800,20 +802,23 @@ SCENARIO(
   }
 }
 
-SCENARIO(
+TEMPLATE_TEST_CASE(
   "Bitwise \"OR\" expressions are converted to SMT terms",
-  "[core][smt2_incremental]")
+  "[core][smt2_incremental]",
+  signedbv_typet,
+  unsignedbv_typet,
+  bv_typet)
 {
   auto test = expr_to_smt_conversion_test_environmentt::make(test_archt::i386);
-  GIVEN("three integer bitvectors and their smt-term equivalents")
+  GIVEN("three bitvectors and their smt-term equivalents")
   {
     const smt_termt smt_term_one = smt_bit_vector_constant_termt{1, 8};
     const smt_termt smt_term_three = smt_bit_vector_constant_termt{3, 8};
     const smt_termt smt_term_five = smt_bit_vector_constant_termt{5, 8};
 
-    const auto one_bvint = from_integer(1, signedbv_typet{8});
-    const auto three_bvint = from_integer(3, signedbv_typet{8});
-    const auto five_bvint = from_integer(5, signedbv_typet{8});
+    const auto one_bvint = from_integer(1, TestType{8});
+    const auto three_bvint = from_integer(3, TestType{8});
+    const auto five_bvint = from_integer(5, TestType{8});
 
     WHEN("a bitor_exprt with two of them as arguments is converted")
     {
@@ -840,8 +845,7 @@ SCENARIO(
     WHEN("a ternary bitor_exprt gets connverted to smt terms")
     {
       const exprt::operandst or_operands{one_bvint, three_bvint, five_bvint};
-      const multi_ary_exprt first_step{
-        ID_bitor, or_operands, signedbv_typet{8}};
+      const multi_ary_exprt first_step{ID_bitor, or_operands, TestType{8}};
       const auto bitor_expr = to_bitor_expr(first_step);
 
       const auto constructed_term = test.convert(bitor_expr);
@@ -877,20 +881,23 @@ SCENARIO(
   }
 }
 
-SCENARIO(
+TEMPLATE_TEST_CASE(
   "Bitwise \"XOR\" expressions are converted to SMT terms",
-  "[core][smt2_incremental]")
+  "[core][smt2_incremental]",
+  signedbv_typet,
+  unsignedbv_typet,
+  bv_typet)
 {
   auto test = expr_to_smt_conversion_test_environmentt::make(test_archt::i386);
-  GIVEN("three integer bitvectors and their smt-term equivalents")
+  GIVEN("three bitvectors and their smt-term equivalents")
   {
     const smt_termt smt_term_one = smt_bit_vector_constant_termt{1, 8};
     const smt_termt smt_term_three = smt_bit_vector_constant_termt{3, 8};
     const smt_termt smt_term_five = smt_bit_vector_constant_termt{5, 8};
 
-    const auto one_bvint = from_integer(1, signedbv_typet{8});
-    const auto three_bvint = from_integer(3, signedbv_typet{8});
-    const auto five_bvint = from_integer(5, signedbv_typet{8});
+    const auto one_bvint = from_integer(1, TestType{8});
+    const auto three_bvint = from_integer(3, TestType{8});
+    const auto five_bvint = from_integer(5, TestType{8});
 
     WHEN("a bitxor_exprt with two of them as arguments is converted")
     {
@@ -913,8 +920,7 @@ SCENARIO(
     WHEN("a ternary bitxor_exprt gets connverted to smt terms")
     {
       const exprt::operandst xor_operands{one_bvint, three_bvint, five_bvint};
-      const multi_ary_exprt first_step{
-        ID_bitxor, xor_operands, signedbv_typet{8}};
+      const multi_ary_exprt first_step{ID_bitxor, xor_operands, TestType{8}};
       const auto bitxor_expr = to_bitxor_expr(first_step);
 
       const auto constructed_term = test.convert(bitxor_expr);
@@ -949,14 +955,17 @@ SCENARIO(
   }
 }
 
-SCENARIO(
+TEMPLATE_TEST_CASE(
   "Bitwise \"NOT\" expressions are converted to SMT terms (1's complement)",
-  "[core][smt2_incremental]")
+  "[core][smt2_incremental]",
+  signedbv_typet,
+  unsignedbv_typet,
+  bv_typet)
 {
   auto test = expr_to_smt_conversion_test_environmentt::make(test_archt::i386);
-  GIVEN("An integer bitvector")
+  GIVEN("An bitvector")
   {
-    const auto one_bvint = from_integer(1, signedbv_typet{8});
+    const auto one_bvint = from_integer(1, TestType{8});
 
     WHEN("A bitnot_exprt is constructed and converted to an SMT term")
     {