byte_extract lowering: also use a lower bound

We already limited extraction at an uppper bound, but when we know the offset we
can also start as late as possible. For structs, for example, we now do not
expand components that will be irrelevant to the final result.

Author: tautschnig

src/solvers/lowering/byte_operators.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 static exprt unpack_rec(
   const exprt &src,
   bool little_endian,
+  const exprt &offset,
   const exprt &max_bytes,
   const namespacet &ns,
   bool unpack_byte_array = false);
@@ -30,6 +31,7 @@ static exprt unpack_rec(
 /// \param src_size: array/vector size
 /// \param element_width: bit width of array/vector elements
 /// \param little_endian: true, iff assumed endianness is little-endian
+/// \param offset: if not nil, use as lower bound for non-nil bytes to return
 /// \param max_bytes: if not nil, use as upper bound of the number of bytes to
 ///                   unpack
 /// \param ns: namespace for type lookups
@@ -39,6 +41,7 @@ static void unpack_array_vector(
   const exprt &src_size,
   const mp_integer &element_width,
   bool little_endian,
+  const exprt &offset,
   const exprt &max_bytes,
   const namespacet &ns,
   array_exprt &dest_array)
@@ -67,6 +70,17 @@ static void unpack_array_vector(
 
       *max_bytes_int /= el_bytes;
     }
+
+    if(auto offset_bytes = numeric_cast<mp_integer>(offset))
+    {
+      // compute offset as number of elements
+      first_element = *offset_bytes / el_bytes;
+      // insert offset_bytes-many nil bytes into the output array
+      *offset_bytes -= *offset_bytes % el_bytes;
+      dest_array.operands().resize(
+        numeric_cast_v<std::size_t>(*offset_bytes),
+        from_integer(0, unsignedbv_typet(8)));
+    }
   }
 
   // the maximum number of bytes is an upper bound in case the size of the
@@ -91,7 +105,8 @@ static void unpack_array_vector(
       element = src_simp.operands()[index_int];
     }
 
-    exprt sub = unpack_rec(element, little_endian, max_bytes, ns, true);
+    exprt sub =
+      unpack_rec(element, little_endian, nil_exprt(), max_bytes, ns, true);
     dest_array.operands().insert(
       dest_array.operands().end(),
       sub.operands().begin(),
@@ -102,6 +117,7 @@ static void unpack_array_vector(
 /// rewrite an object into its individual bytes
 /// \param src: object to unpack
 /// \param little_endian: true, iff assumed endianness is little-endian
+/// \param offset: if not nil, use as lower bound for non-nil bytes to return
 /// \param max_bytes: if not nil, use as upper bound of the number of bytes to
 ///                   unpack
 /// \param ns: namespace for type lookups
@@ -114,6 +130,7 @@ static void unpack_array_vector(
 static exprt unpack_rec(
   const exprt &src,
   bool little_endian,
+  const exprt &offset,
   const exprt &max_bytes,
   const namespacet &ns,
   bool unpack_byte_array)
@@ -141,6 +158,7 @@ static exprt unpack_rec(
       array_type.size(),
       *element_width,
       little_endian,
+      offset,
       max_bytes,
       ns,
       array);
@@ -161,6 +179,7 @@ static exprt unpack_rec(
       vector_type.size(),
       *element_width,
       little_endian,
+      offset,
       max_bytes,
       ns,
       array);
@@ -170,6 +189,8 @@ static exprt unpack_rec(
     const struct_typet &struct_type=to_struct_type(ns.follow(src.type()));
     const struct_typet::componentst &components=struct_type.components();
 
+    mp_integer member_offset_bits = 0;
+
     for(const auto &comp : components)
     {
       auto element_width = pointer_offset_bits(comp.type(), ns);
@@ -182,11 +203,38 @@ static exprt unpack_rec(
         throw non_byte_alignedt(struct_type, comp, *element_width);
       }
 
+      exprt new_offset = nil_exprt();
+      auto new_offset_int = numeric_cast<mp_integer>(offset);
+      exprt new_max_bytes = nil_exprt();
+      auto new_max_bytes_int = numeric_cast<mp_integer>(max_bytes);
+
+      if(new_offset_int.has_value())
+      {
+        *new_offset_int -= member_offset_bits / 8;
+        if(*new_offset_int >= 0)
+          new_offset = from_integer(*new_offset_int, offset.type());
+      }
+
+      if(new_max_bytes_int.has_value())
+      {
+        *new_max_bytes_int -= member_offset_bits / 8;
+        if(*new_max_bytes_int >= 0)
+          new_max_bytes = from_integer(*new_max_bytes_int, max_bytes.type());
+        else
+          break;
+      }
+
       member_exprt member(src, comp.get_name(), comp.type());
-      exprt sub=unpack_rec(member, little_endian, max_bytes, ns, true);
+      if(src.id() == ID_struct)
+        simplify(member, ns);
+
+      exprt sub =
+        unpack_rec(member, little_endian, new_offset, new_max_bytes, ns, true);
 
       for(const auto& op : sub.operands())
         array.copy_to_operands(op);
+
+      member_offset_bits += *element_width;
     }
   }
   else if(src.type().id()!=ID_empty)
@@ -294,9 +342,12 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
           typecast_exprt(src.offset(), upper_bound.type())),
         ns);
 
+  exprt lb = src.offset();
+  if(!lb.is_constant())
+    lb.make_nil();
+
   byte_extract_exprt unpacked(src);
-  unpacked.op()=
-    unpack_rec(src.op(), little_endian, upper_bound, ns);
+  unpacked.op() = unpack_rec(src.op(), little_endian, lb, upper_bound, ns);
 
   if(src.type().id()==ID_array)
   {