Fix skeleton in shift_indexed_access_to_lhs

src/goto-symex/expr_skeleton.cpp

@@ -11,23 +11,31 @@ Author: Romain Brenguier, [email protected]
 
 #include "expr_skeleton.h"
 
+#include <util/arith_tools.h>
+#include <util/byte_operators.h>
+#include <util/mp_arith.h>
+#include <util/pointer_offset_size.h>
+#include <util/simplify_expr.h>
 #include <util/std_expr.h>
 
-expr_skeletont::expr_skeletont() : skeleton(nil_exprt{})
+expr_skeletont::expr_skeletont(typet missing_type)
+  : skeleton(nil_exprt{}), type_of_missing_part(std::move(missing_type))
 {
 }
 
 expr_skeletont expr_skeletont::remove_op0(exprt e)
 {
   PRECONDITION(e.id() != ID_symbol);
   PRECONDITION(e.operands().size() >= 1);
+  typet missing = std::move(e.op0().type());
   e.op0().make_nil();
-  return expr_skeletont{std::move(e)};
+  return expr_skeletont{std::move(e), std::move(missing)};
 }
 
 exprt expr_skeletont::apply(exprt expr) const
 {
   PRECONDITION(skeleton.id() != ID_symbol);
+  PRECONDITION(expr.type() == type_of_missing_part);
   exprt result = skeleton;
   exprt *p = &result;
 
@@ -50,13 +58,18 @@ exprt expr_skeletont::apply(exprt expr) const
 
 expr_skeletont expr_skeletont::compose(expr_skeletont other) const
 {
-  return expr_skeletont(apply(other.skeleton));
+  typet missing_type = other.type_of_missing_part;
+  return expr_skeletont{apply(std::move(other.skeleton)),
+                        std::move(missing_type)};
 }
 
 /// In the expression corresponding to a skeleton returns a pointer to the
 /// deepest subexpression before we encounter nil.
+/// Returns nullptr if \p e is nil
 static exprt *deepest_not_nil(exprt &e)
 {
+  if(e.is_nil())
+    return nullptr;
   exprt *ptr = &e;
   while(!ptr->op0().is_nil())
     ptr = &ptr->op0();
@@ -67,10 +80,14 @@ optionalt<expr_skeletont>
 expr_skeletont::clear_innermost_index_expr(expr_skeletont skeleton)
 {
   exprt *to_update = deepest_not_nil(skeleton.skeleton);
+  if(to_update == nullptr)
+    return {};
   if(index_exprt *index_expr = expr_try_dynamic_cast<index_exprt>(*to_update))
   {
+    typet new_missing_type = index_expr->type();
     index_expr->make_nil();
-    return expr_skeletont{std::move(skeleton)};
+    return expr_skeletont{std::move(skeleton.skeleton),
+                          std::move(new_missing_type)};
   }
   return {};
 }
@@ -79,10 +96,14 @@ optionalt<expr_skeletont>
 expr_skeletont::clear_innermost_member_expr(expr_skeletont skeleton)
 {
   exprt *to_update = deepest_not_nil(skeleton.skeleton);
+  if(to_update == nullptr)
+    return {};
   if(member_exprt *member = expr_try_dynamic_cast<member_exprt>(*to_update))
   {
+    typet new_missing_type = member->type();
     member->make_nil();
-    return expr_skeletont{std::move(skeleton)};
+    return expr_skeletont{std::move(skeleton.skeleton),
+                          std::move(new_missing_type)};
   }
   return {};
 }
@@ -91,12 +112,96 @@ optionalt<expr_skeletont>
 expr_skeletont::clear_innermost_byte_extract_expr(expr_skeletont skeleton)
 {
   exprt *to_update = deepest_not_nil(skeleton.skeleton);
+  if(to_update == nullptr)
+    return {};
   if(
     to_update->id() != ID_byte_extract_big_endian &&
     to_update->id() != ID_byte_extract_little_endian)
   {
     return {};
   }
+  typet new_missing_type = to_update->type();
   to_update->make_nil();
-  return expr_skeletont{std::move(skeleton.skeleton)};
+  return expr_skeletont{std::move(skeleton.skeleton),
+                        std::move(new_missing_type)};
+}
+
+expr_skeletont expr_skeletont::revert_byte_extract_aux(
+  expr_skeletont skeleton,
+  exprt offset,
+  const typet &type,
+  const namespacet &ns,
+  exprt offset_already_removed)
+{
+  offset = simplify_expr(std::move(offset), ns);
+  const exprt offset_reached =
+    simplify_expr(equal_exprt{offset_already_removed, offset}, ns);
+  if(offset_reached.is_true() && type == skeleton.type_of_missing_part)
+    return expr_skeletont{std::move(skeleton)};
+  const exprt offset_exceeded = simplify_expr(
+    binary_relation_exprt{offset_already_removed, ID_gt, offset}, ns);
+  exprt *deepest = deepest_not_nil(skeleton.skeleton);
+  if(deepest == nullptr || offset_exceeded.is_true())
+  {
+    // In case of empty skeleton or if the offset has been exceeded, compose
+    // with `byte_extract(☐, offset_already_removed - offset)`
+    const minus_exprt offset_diff{std::move(offset_already_removed), offset};
+    const auto simplified = simplify_expr(offset_diff, ns);
+    return skeleton.compose(expr_skeletont{
+      byte_extract_exprt{byte_extract_id(), nil_exprt{}, simplified, type},
+      skeleton.type_of_missing_part});
+  }
+  const auto offset_resulting_from_deepest_operation = [&]() -> exprt {
+    if(auto byte_extract = expr_try_dynamic_cast<byte_extract_exprt>(*deepest))
+      return byte_extract->offset();
+    if(auto index_expr = expr_try_dynamic_cast<index_exprt>(*deepest))
+    {
+      auto element_size_in_bits = pointer_offset_bits(index_expr->type(), ns);
+      CHECK_RETURN(element_size_in_bits);
+      mult_exprt offset_in_bits{
+        index_expr->index(),
+        from_integer(*element_size_in_bits, index_expr->index().type())};
+      return div_exprt{offset_in_bits, from_integer(8, offset_in_bits.type())};
+    }
+    auto member_expr = expr_try_dynamic_cast<member_exprt>(*deepest);
+    INVARIANT(
+      member_expr,
+      "Skeleton should only be composed of byte_extract, index and member "
+      "exprts");
+    auto struct_type =
+      type_try_dynamic_cast<struct_typet>(skeleton.type_of_missing_part);
+    INVARIANT(
+      struct_type,
+      "In member_exprt skeleton the missing part should have struct type");
+    auto member_offset =
+      member_offset_expr(*struct_type, member_expr->get_component_name(), ns);
+    CHECK_RETURN(member_offset);
+    return *member_offset;
+  }();
+
+  typet new_missing_type = deepest->type();
+  deepest->make_nil();
+  skeleton.type_of_missing_part = new_missing_type;
+  return revert_byte_extract_aux(
+    skeleton,
+    offset,
+    type,
+    ns,
+    plus_exprt{std::move(offset_already_removed),
+               offset_resulting_from_deepest_operation});
+}
+
+expr_skeletont expr_skeletont::revert_byte_extract(
+  expr_skeletont skeleton,
+  exprt offset,
+  const typet &type,
+  const namespacet &ns)
+{
+  exprt init_already_removed = from_integer(0, offset.type());
+  return revert_byte_extract_aux(
+    std::move(skeleton),
+    std::move(offset),
+    type,
+    ns,
+    std::move(init_already_removed));
 }

src/goto-symex/expr_skeleton.h

@@ -13,6 +13,7 @@ Author: Romain Brenguier, [email protected]
 #define CPROVER_GOTO_SYMEX_EXPR_SKELETON_H
 
 #include <util/expr.h>
+#include <util/mp_arith.h>
 
 /// Expression in which some part is missing and can be substituted for another
 /// expression.
@@ -27,7 +28,7 @@ class expr_skeletont final
 public:
   /// Empty skeleton. Applying it to an expression would give the same
   /// expression unchanged
-  expr_skeletont();
+  explicit expr_skeletont(typet missing_type);
 
   /// Replace the missing part of the current skeleton by another skeleton,
   /// ending in a bigger skeleton corresponding to the two combined.
@@ -61,16 +62,43 @@ class expr_skeletont final
   static optionalt<expr_skeletont>
   clear_innermost_byte_extract_expr(expr_skeletont skeleton);
 
+  /// Attempt to return a skeleton `s` such that for all expression \c x,
+  /// `s.apply(byte_extract(x, offset, type))` would be semantically equivalent
+  /// to `skeleton.apply(x)`.
+  /// If offset + type size exceeds the size (in bytes) of the skeleton then
+  /// an empty optional is returned.
+  /// This is done by removing operations of the skeleton (starting by the
+  /// deepest ones), until the accumulated offset match or exceed \p offset.
+  /// If it does not exactly match then one of the operation will be replaced
+  /// by a byte_extract.
+  static expr_skeletont revert_byte_extract(
+    expr_skeletont skeleton,
+    exprt offset,
+    const typet &type,
+    const namespacet &ns);
+
 private:
   /// In \c skeleton, nil_exprt is used to mark the sub expression to be
   /// substituted. The nil_exprt always appears recursively following the first
   /// operands because the only way to get a skeleton is by removing the first
   /// operand.
   exprt skeleton;
+  typet type_of_missing_part;
 
-  explicit expr_skeletont(exprt e) : skeleton(std::move(e))
+  expr_skeletont(exprt e, typet missing)
+    : skeleton(std::move(e)), type_of_missing_part(std::move(missing))
   {
   }
+
+  /// Auxiliary function for revert_byte_extract.
+  /// It is recursive and has an extra argument for keeping track of the offset
+  /// that has been removed by the recursive calls.
+  static expr_skeletont revert_byte_extract_aux(
+    expr_skeletont skeleton,
+    exprt offset,
+    const typet &type,
+    const namespacet &ns,
+    exprt offset_already_removed);
 };
 
 #endif // CPROVER_GOTO_SYMEX_EXPR_SKELETON_H

src/goto-symex/goto_symex.cpp

@@ -82,6 +82,6 @@ void goto_symext::symex_assign(statet &state, const code_assignt &code)
 
     exprt::operandst lhs_if_then_else_conditions;
     symex_assignt{state, assignment_type, ns, symex_config, target}.assign_rec(
-      lhs, expr_skeletont{}, rhs, lhs_if_then_else_conditions);
+      lhs, expr_skeletont{lhs.type()}, rhs, lhs_if_then_else_conditions);
   }
 }