Bug fix - place into the pointer-sizes map types that belong to subexpressions.

Before this change, we would be able to handle an expression like (*a + 2)
but not one like (&a - &b) + (&c - &d), because we wouldn't iterate through
each subexpression of the original one.

Author: thomasspriggs

src/solvers/smt2_incremental/pointer_size_mapping.cpp

@@ -17,44 +17,32 @@ void associate_pointer_sizes(
   const smt_object_mapt &object_map,
   const smt_object_sizet::make_applicationt &object_size)
 {
-  if(std::any_of(
-       expression.operands().cbegin(),
-       expression.operands().cend(),
-       [](exprt operand)
-       { return can_cast_type<pointer_typet>(operand.type()); }))
-  {
-    exprt pointer;
-    for(auto &operand : expression.operands())
+  expression.visit_pre([&](const exprt &sub_expression) {
+    if(
+      const auto &pointer_type =
+        type_try_dynamic_cast<pointer_typet>(sub_expression.type()))
     {
-      if(can_cast_type<pointer_typet>(operand.type()))
+      const auto find_result = pointer_size_map.find(pointer_type->base_type());
+      if(find_result != pointer_size_map.cend())
+        return;
+      exprt pointer_size_expr;
+      // There's a special case for a pointer subtype here: the case where the pointer is `void *`. This means
+      // that we don't know the underlying base type, so we're just assigning a size expression value of 1 (given
+      // that this is going to be used in a multiplication and 1 is the identity value for multiplcation)
+      if(is_void_pointer(*pointer_type))
       {
-        pointer = operand;
+        pointer_size_expr = from_integer(1, size_type());
       }
+      else
+      {
+        auto pointer_size_opt = size_of_expr(pointer_type->base_type(), ns);
+        PRECONDITION(pointer_size_opt.has_value());
+        pointer_size_expr = pointer_size_opt.value();
+      }
+      auto pointer_size_term = convert_expr_to_smt(
+        pointer_size_expr, object_map, pointer_size_map, object_size);
+      pointer_size_map.emplace_hint(
+        find_result, pointer_type->base_type(), pointer_size_term);
     }
-
-    auto pointer_type = to_pointer_type(pointer.type());
-    auto pointer_base_type = pointer_type.base_type();
-    exprt pointer_size_expr;
-    // There's a special case for a pointer subtype here: the case where the pointer is `void *`. This means
-    // that we don't know the underlying base type, so we're just assigning a size expression value of 1 (given
-    // that this is going to be used in a multiplication and 1 is the identity value for multiplcation)
-    if(is_void_pointer(pointer_type))
-    {
-      pointer_size_expr = from_integer(1, size_type());
-    }
-    else
-    {
-      auto pointer_size_opt = size_of_expr(pointer_base_type, ns);
-      PRECONDITION(pointer_size_opt.has_value());
-      pointer_size_expr = pointer_size_opt.value();
-    }
-    auto pointer_size_term = convert_expr_to_smt(
-      pointer_size_expr, object_map, pointer_size_map, object_size);
-
-    const auto find_result = pointer_size_map.find(pointer_base_type);
-    if(find_result != pointer_size_map.cend())
-      return;
-    pointer_size_map.emplace_hint(
-      find_result, pointer_base_type, pointer_size_term);
-  }
+  });
 }