Merge pull request #3156 from tautschnig/get_subexpr-interface

Make get_subexpression_at_offset return an exprt for consistency

Author: Daniel Kroening

src/pointer-analysis/value_set_dereference.cpp

@@ -466,18 +466,18 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
       if(ns.follow(result.value.type())!=ns.follow(dereference_type))
         result.value.make_typecast(dereference_type);
     }
-    else if(get_subexpression_at_offset(
-        root_object_subexpression,
-        o.offset(),
-        dereference_type,
-        ns))
-    {
-      // Successfully found a member, array index, or combination thereof
-      // that matches the desired type and offset:
-      result.value=root_object_subexpression;
-    }
     else
     {
+      exprt subexpr = get_subexpression_at_offset(
+        root_object_subexpression, o.offset(), dereference_type, ns);
+      if(subexpr.is_not_nil())
+      {
+        // Successfully found a member, array index, or combination thereof
+        // that matches the desired type and offset:
+        result.value = subexpr;
+        return result;
+      }
+
       // we extract something from the root object
       result.value=o.root_object();
 

src/util/pointer_offset_size.cpp

@@ -630,17 +630,18 @@ exprt build_sizeof_expr(
   return result;
 }
 
-bool get_subexpression_at_offset(
-  exprt &result,
+exprt get_subexpression_at_offset(
+  const exprt &expr,
   mp_integer offset,
   const typet &target_type_raw,
   const namespacet &ns)
 {
+  exprt result = expr;
   const typet &source_type=ns.follow(result.type());
   const typet &target_type=ns.follow(target_type_raw);
 
   if(offset==0 && source_type==target_type)
-    return true;
+    return result;
 
   if(source_type.id()==ID_struct)
   {
@@ -667,7 +668,7 @@ bool get_subexpression_at_offset(
       }
       ++offsets;
     }
-    return false;
+    return nil_exprt();
   }
   else if(source_type.id()==ID_array)
   {
@@ -678,32 +679,32 @@ bool get_subexpression_at_offset(
     auto elem_size = pointer_offset_size(at.subtype(), ns);
 
     if(!elem_size.has_value())
-      return false;
+      return nil_exprt();
 
     mp_integer cellidx = offset / (*elem_size);
 
     if(cellidx < 0 || !cellidx.is_long())
-      return false;
+      return nil_exprt();
 
     offset = offset % (*elem_size);
 
     result=index_exprt(result, from_integer(cellidx, unsignedbv_typet(64)));
     return get_subexpression_at_offset(result, offset, target_type, ns);
   }
   else
-    return false;
+    return nil_exprt();
 }
 
-bool get_subexpression_at_offset(
-  exprt &result,
+exprt get_subexpression_at_offset(
+  const exprt &expr,
   const exprt &offset,
   const typet &target_type,
   const namespacet &ns)
 {
   mp_integer offset_const;
 
   if(to_integer(offset, offset_const))
-    return false;
+    return nil_exprt();
   else
-    return get_subexpression_at_offset(result, offset_const, target_type, ns);
+    return get_subexpression_at_offset(expr, offset_const, target_type, ns);
 }

src/util/pointer_offset_size.h

@@ -79,14 +79,14 @@ exprt build_sizeof_expr(
   const constant_exprt &expr,
   const namespacet &ns);
 
-bool get_subexpression_at_offset(
-  exprt &result,
+exprt get_subexpression_at_offset(
+  const exprt &expr,
   mp_integer offset,
   const typet &target_type,
   const namespacet &ns);
 
-bool get_subexpression_at_offset(
-  exprt &result,
+exprt get_subexpression_at_offset(
+  const exprt &expr,
   const exprt &offset,
   const typet &target_type,
   const namespacet &ns);