Merge pull request diffblue#252 from diffblue/issue207and178

Fix write_stack to correctly complete types for index_exprt expressions

Author: chrisr-diffblue

regression/goto-analyzer/write-stack-types/test.desc

@@ -0,0 +1,8 @@
+CORE
+write-stack-address-of.c
+--variable --structs --pointers --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[func1.assertion.1\] .* func1.a == 0: Unknown$
+--
+^warning: ignoring

regression/goto-analyzer/write-stack-types/write-stack-address-of.c

@@ -0,0 +1,34 @@
+typedef unsigned short uint16;
+
+struct st {
+  uint16 data1;
+} str1;
+
+extern struct {
+  struct st data2;
+} g_sts;
+
+void func1(uint16 a)
+{
+  // Expect the assert to be 'Unknown' because we would expect 'a' to be TOP
+  // here because p->data1 passed in as argument should be TOP. 
+  __CPROVER_assert(a == 0, "func1.a == 0");
+}
+
+void func2(struct st *p)
+{
+    func1(p->data1);
+}
+
+void main(void)
+{
+    const int s_map_data[] = { 2, 10, 20, 100, 110 };
+
+  	int *p_map_x = &s_map_data[1];
+  	int *p_map_y = p_map_x + 1 ;
+
+  	// Tests that the write_stack handles &smap_data[1]
+  	__CPROVER_assert(*p_map_y == 20, "*main.p_map_y == 20");
+
+  	func2(&g_sts.data2);
+}

src/analyses/variable-sensitivity/write_stack.cpp

@@ -188,6 +188,9 @@ exprt write_stackt::to_expression() const
       }
       new_expr.op0()=access_expr;
 
+      // If neccesary, complete the type of the new access expression
+      entry->adjust_access_type(new_expr);
+
       access_expr=new_expr;
     }
   }

src/analyses/variable-sensitivity/write_stack_entry.cpp

@@ -35,6 +35,11 @@ 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
+{
+}
+
 offset_entryt::offset_entryt(abstract_object_pointert offset_value):
   offset(offset_value)
 {
@@ -46,13 +51,28 @@ 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
-/// \return The expression to read this part of the stack
+/// 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(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
+{
+  PRECONDITION(expr.id() == ID_index);
+  expr.type()=expr.op0().type().subtype();
+}
+
 /// Try to combine a new stack element with the current top of the stack. This
 /// will succeed if they are both offsets as we can combine these offsets into
 /// the sum of the offsets

src/analyses/variable-sensitivity/write_stack_entry.h

@@ -25,6 +25,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 bool try_squash_in(
     std::shared_ptr<const write_stack_entryt> new_entry,
     const abstract_environmentt &enviroment,
@@ -36,6 +37,7 @@ class simple_entryt:public write_stack_entryt
 public:
   explicit simple_entryt(exprt expr);
   virtual exprt get_access_expr() const override;
+  virtual void adjust_access_type(exprt &expr) const override;
 private:
   exprt simple_entry;
 };
@@ -45,6 +47,7 @@ class offset_entryt:public write_stack_entryt
 public:
   explicit offset_entryt(abstract_object_pointert offset_value);
   virtual exprt get_access_expr() const override;
+  virtual void adjust_access_type(exprt &expr) const override;
   virtual bool try_squash_in(
     std::shared_ptr<const write_stack_entryt> new_entry,
     const abstract_environmentt &enviroment,