Merge pull request #6950 from diffblue/index_exprt_check

index_exprt now requires a type with subtype

Author: tautschnig

src/analyses/variable-sensitivity/write_stack.cpp

@@ -102,12 +102,12 @@ void write_stackt::construct_stack_to_pointer(
     if(!top_stack)
     {
       // check the symbol at the bottom of the stack
-      std::shared_ptr<const write_stack_entryt> entry = *stack.cbegin();
+      const auto access = stack.front()->get_access_expr();
       INVARIANT(
-        entry->get_access_expr().id() == ID_symbol,
+        !access.second && access.first.id() == ID_symbol,
         "The base should be an addressable location (i.e. symbol)");
 
-      if(entry->get_access_expr().type().id() != ID_array)
+      if(access.first.type().id() != ID_array)
       {
         top_stack = true;
       }
@@ -176,27 +176,15 @@ exprt write_stackt::to_expression() const
 {
   // A top stack is useless and its expression should not be evaluated
   PRECONDITION(!is_top_value());
-  exprt access_expr = nil_exprt();
-  for(const std::shared_ptr<write_stack_entryt> &entry : stack)
+  PRECONDITION(!stack.empty());
+  exprt access_expr = stack.front()->get_access_expr().first;
+  for(auto it = std::next(stack.begin()); it != stack.end(); ++it)
   {
-    exprt new_expr = entry->get_access_expr();
-    if(access_expr.id() == ID_nil)
-    {
-      access_expr = new_expr;
-    }
+    const auto access = (*it)->get_access_expr();
+    if(access.second)
+      access_expr = index_exprt{access_expr, access.first};
     else
-    {
-      if(new_expr.operands().size() == 0)
-      {
-        new_expr.operands().resize(1);
-      }
-      new_expr.operands()[0] = access_expr;
-
-      // If necessary, complete the type of the new access expression
-      entry->adjust_access_type(new_expr);
-
-      access_expr = new_expr;
-    }
+      access_expr = access.first;
   }
   address_of_exprt top_expr(access_expr);
   return std::move(top_expr);
@@ -210,19 +198,22 @@ size_t write_stackt::depth() const
 exprt write_stackt::target_expression(size_t depth) const
 {
   PRECONDITION(!is_top_value());
-  return stack[depth]->get_access_expr();
+  return stack[depth]->get_access_expr().first;
 }
 
 exprt write_stackt::offset_expression() const
 {
   PRECONDITION(!is_top_value());
-  auto const &access = stack.back()->get_access_expr();
+  auto const access = stack.back()->get_access_expr();
+
+  if(access.second)
+    return access.first;
 
-  if(access.id() == ID_member || access.id() == ID_symbol)
-    return access;
+  if(access.first.id() == ID_member || access.first.id() == ID_symbol)
+    return access.first;
 
-  if(access.id() == ID_index)
-    return to_index_expr(access).index();
+  if(access.first.id() == ID_index)
+    return to_index_expr(access.first).index();
 
   return from_integer(0, unsigned_long_int_type());
 }

src/analyses/variable-sensitivity/write_stack_entry.cpp

@@ -39,15 +39,10 @@ simple_entryt::simple_entryt(exprt expr) : simple_entry(expr)
 
 /// Get the expression part needed to read this stack entry. For simple
 /// expressions this is just the expression itself.
-/// \return The expression to read this part of the stack
-exprt simple_entryt::get_access_expr() const
-{
-  return simple_entry;
-}
-
-/// For a simple entry, no type adjustment is needed for the access expression
-void simple_entryt::adjust_access_type(exprt &expr) const
+/// \return The expression to read this part of the stack and false
+std::pair<exprt, bool> simple_entryt::get_access_expr() const
 {
+  return {simple_entry, false};
 }
 
 offset_entryt::offset_entryt(abstract_object_pointert offset_value)
@@ -61,26 +56,11 @@ offset_entryt::offset_entryt(abstract_object_pointert offset_value)
 }
 
 /// Get the expression part needed to read this stack entry. For offset entries
-/// this is an index expression with the index() part the offset.
-/// It is important to note that the returned index_exprt does not have a type,
-/// so it will be necessary for the caller to update the type whenever the index
-/// expression is completed using `adjust_access_type` on the resulting exprt.
-/// \return The untyped expression to read this part of the stack
-exprt offset_entryt::get_access_expr() const
-{
-  // This constructs a something that is basicallyt '(null)[offset])'
-  // meaning that we don't know what the type is at this point, as the
-  // array part will be filled in later.
-  return index_exprt(nil_exprt(), offset->to_constant());
-}
-
-/// For an offset entry, the type of the access expression can only be
-/// determined once the access expression has been completed with the next
-/// entry on the write stack.
-void offset_entryt::adjust_access_type(exprt &expr) const
+/// this is the offset for an index expression.
+/// \return The offset expression to read this part of the stack and true
+std::pair<exprt, bool> offset_entryt::get_access_expr() const
 {
-  PRECONDITION(expr.id() == ID_index);
-  expr.type() = to_index_expr(expr).array().type().subtype();
+  return {offset->to_constant(), true};
 }
 
 /// Try to combine a new stack element with the current top of the stack. This

src/analyses/variable-sensitivity/write_stack_entry.h

@@ -21,8 +21,7 @@ class write_stack_entryt
 {
 public:
   virtual ~write_stack_entryt() = default;
-  virtual exprt get_access_expr() const = 0;
-  virtual void adjust_access_type(exprt &expr) const = 0;
+  virtual std::pair<exprt, bool> get_access_expr() const = 0;
   virtual bool try_squash_in(
     std::shared_ptr<const write_stack_entryt> new_entry,
     const abstract_environmentt &enviroment,
@@ -33,8 +32,7 @@ class simple_entryt : public write_stack_entryt
 {
 public:
   explicit simple_entryt(exprt expr);
-  exprt get_access_expr() const override;
-  void adjust_access_type(exprt &expr) const override;
+  std::pair<exprt, bool> get_access_expr() const override;
 
 private:
   exprt simple_entry;
@@ -44,8 +42,7 @@ class offset_entryt : public write_stack_entryt
 {
 public:
   explicit offset_entryt(abstract_object_pointert offset_value);
-  exprt get_access_expr() const override;
-  void adjust_access_type(exprt &expr) const override;
+  std::pair<exprt, bool> get_access_expr() const override;
   bool try_squash_in(
     std::shared_ptr<const write_stack_entryt> new_entry,
     const abstract_environmentt &enviroment,

src/cpp/cpp_constructor.cpp

@@ -100,7 +100,7 @@ optionalt<codet> cpp_typecheckt::cpp_constructor(
         exprt constant = from_integer(i, c_index_type());
         constant.add_source_location()=source_location;
 
-        index_exprt index(object, constant);
+        index_exprt index = index_exprt(object_tc, constant);
         index.add_source_location()=source_location;
 
         if(!operands.empty())

src/util/std_expr.h

@@ -1417,9 +1417,7 @@ class index_exprt:public binary_exprt
         _array,
         ID_index,
         std::move(_index),
-        _array.type().has_subtype()
-          ? to_type_with_subtype(_array.type()).subtype()
-          : typet(ID_nil))
+        to_type_with_subtype(_array.type()).subtype())
   {
   }
 

unit/solvers/smt2_incremental/object_tracking.cpp

@@ -29,8 +29,7 @@ TEST_CASE("find_object_base_expression", "[core][smt2_incremental]")
       {member_exprt{object_base, "baz", unsignedbv_typet{8}}, pointer_type}},
     rowt{
       "Address of index of struct member",
-      {index_exprt{
-         member_exprt{object_base, "baz", unsignedbv_typet{8}}, index},
+      {index_exprt{member_exprt{object_base, "baz", base_type}, index},
        pointer_type}},
     rowt{
       "Address of struct member at index",