Merge pull request #8325 from diffblue/bool-is-mathematical

`__CPROVER_bool` should not have a memory layout

Author: kroening

regression/ansi-c/cprover_bool1/main.c

@@ -24,7 +24,7 @@ __CPROVER_size_t __VERIFIER_nondet_size(void);
 typedef struct
 {
   /// \brief  True iff __CPROVER_w_ok(lb, size) holds at creation
-  __CPROVER_bool is_writable;
+  unsigned char is_writable;
   /// \brief Size of the range in bytes
   __CPROVER_size_t size;
   /// \brief Lower bound address of the range
@@ -56,9 +56,9 @@ typedef struct
   /// \brief Number of elements currently in the elems array
   __CPROVER_size_t nof_elems;
   /// \brief True iff nof_elems is 0
-  __CPROVER_bool is_empty;
+  unsigned char is_empty;
   /// \brief True iff elems is indexed by the object id of the pointers
-  __CPROVER_bool indexed_by_object_id;
+  unsigned char indexed_by_object_id;
   /// \brief Array of void *pointers, indexed by their object ID
   /// or some other order
   void **elems;
@@ -90,17 +90,17 @@ typedef struct
   /// \brief Object set recording the deallocations (used by was_freed)
   __CPROVER_contracts_obj_set_ptr_t linked_deallocated;
   /// \brief True iff the write set checks requires clauses in an assumption ctx
-  __CPROVER_bool assume_requires_ctx;
+  unsigned char assume_requires_ctx;
   /// \brief True iff the write set checks requires clauses in an assertion ctx
-  __CPROVER_bool assert_requires_ctx;
+  unsigned char assert_requires_ctx;
   /// \brief True iff the write set checks ensures clauses in an assumption ctx
-  __CPROVER_bool assume_ensures_ctx;
+  unsigned char assume_ensures_ctx;
   /// \brief True iff this write set checks ensures clauses in an assertion ctx
-  __CPROVER_bool assert_ensures_ctx;
+  unsigned char assert_ensures_ctx;
   /// \brief True iff dynamic allocation is allowed (default: true)
-  __CPROVER_bool allow_allocate;
+  unsigned char allow_allocate;
   /// \brief True iff dynamic deallocation is allowed (default: true)
-  __CPROVER_bool allow_deallocate;
+  unsigned char allow_deallocate;
 } __CPROVER_contracts_write_set_t;
 
 /// \brief Type of pointers to \ref __CPROVER_contracts_write_set_t.

regression/ansi-c/cprover_bool1/test.desc

@@ -39,13 +39,19 @@ static void build_object_descriptor_rec(
     build_object_descriptor_rec(ns, index.array(), dest);
 
     auto sub_size = size_of_expr(expr.type(), ns);
-    CHECK_RETURN(sub_size.has_value());
 
-    dest.offset() = plus_exprt(
-      dest.offset(),
-      mult_exprt(
-        typecast_exprt::conditional_cast(index.index(), c_index_type()),
-        typecast_exprt::conditional_cast(sub_size.value(), c_index_type())));
+    if(sub_size.has_value())
+    {
+      dest.offset() = plus_exprt(
+        dest.offset(),
+        mult_exprt(
+          typecast_exprt::conditional_cast(index.index(), c_index_type()),
+          typecast_exprt::conditional_cast(sub_size.value(), c_index_type())));
+    }
+    else
+    {
+      dest.offset() = exprt(ID_unknown);
+    }
   }
   else if(expr.id() == ID_member)
   {

regression/cpp/cprover_bool1/main.cpp

@@ -290,17 +290,6 @@ std::optional<exprt> size_of_expr(const typet &type, const namespacet &ns)
   {
     const auto &array_type = to_array_type(type);
 
-    // special-case arrays of bits
-    if(array_type.element_type().id() == ID_bool)
-    {
-      auto bits = pointer_offset_bits(array_type, ns);
-
-      if(bits.has_value())
-        return from_integer(
-          (*bits + config.ansi_c.char_width - 1) / config.ansi_c.char_width,
-          size_type());
-    }
-
     auto sub = size_of_expr(array_type.element_type(), ns);
     if(!sub.has_value())
       return {};
@@ -371,14 +360,6 @@ std::optional<exprt> size_of_expr(const typet &type, const namespacet &ns)
         if(bytes > 0)
           result = plus_exprt(result, from_integer(bytes, result.type()));
       }
-      else if(c.is_boolean())
-      {
-        ++bit_field_bits;
-        const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
-        bit_field_bits %= config.ansi_c.char_width;
-        if(bytes > 0)
-          result = plus_exprt(result, from_integer(bytes, result.type()));
-      }
       else if(c.type().get_bool(ID_C_flexible_array_member))
       {
         // flexible array members do not change the sizeof result
@@ -476,7 +457,8 @@ std::optional<exprt> size_of_expr(const typet &type, const namespacet &ns)
   }
   else if(type.id()==ID_bool)
   {
-    return from_integer(1, size_type());
+    // bool is a mathematical type, and has no memory layout
+    return {};
   }
   else if(type.id()==ID_pointer)
   {

regression/cpp/cprover_bool1/test.desc

@@ -220,8 +220,8 @@ TEST_CASE("Tracking dynamic object status.", "[core][smt2_incremental]")
     std::pair<decltype(base_object), decltype(expected_dynamic_status)>;
   std::tie(base_object, expected_dynamic_status) = GENERATE_REF(
     rowt{from_integer(0, unsignedbv_typet{(8)}), false},
-    rowt{symbol_exprt{"foo", bool_typet{}}, false},
-    rowt{symbol_exprt{SYMEX_DYNAMIC_PREFIX "bar", bool_typet{}}, true},
+    rowt{symbol_exprt{"foo", unsignedbv_typet{8}}, false},
+    rowt{symbol_exprt{SYMEX_DYNAMIC_PREFIX "bar", unsignedbv_typet{8}}, true},
     rowt{from_integer(42, make_type_dynamic(signedbv_typet{16})), true});
   INFO("base_object is - " + base_object.pretty(1, 0));
   track_expression_objects(address_of_exprt{base_object}, ns, object_map);