Merge pull request diffblue#239 from diffblue/bugfix/value_sets_fi_and_reaching_defs_retrievals_of_dynamic_objects

SEC-41 : Bugfix: value_sets and reaching_defs retrievals of dynamic objects

Author: smowton

regression/goto-instrument/slice24/main.c

@@ -0,0 +1,26 @@
+#include <assert.h>
+#include <malloc.h>
+
+struct rrr
+{
+  char j;
+  int y;
+};
+
+void foo(struct rrr *r)
+{
+  r->j = 1;
+}
+
+int main(int argc, char* argv[])
+{
+  struct rrr* r=malloc(sizeof(struct rrr));
+  foo(r);
+  if (r->j==1)
+  {
+    assert(1);
+    return 0;
+  }
+  return -1;
+}
+

regression/goto-instrument/slice24/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+--full-slice --add-library
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$

src/analyses/goto_rw.cpp

@@ -613,6 +613,22 @@ void rw_range_set_value_sett::get_objects_dereference(
     new_size=std::min(size, new_size);
   }
 
+  // We must ensure that the artificial reference (introduced in
+  // 'value_set_dereferencet::build_reference_to') to a dynamic object
+  // obtained by dereferencing the pointer in 'deref' gets to the resulting
+  // points-to-set. The following condition check whether the obtained
+  // object is the artificial reference.
+  if(object.is_not_nil() && object.id()==ID_symbol &&
+    as_string(to_symbol_expr(object).get_identifier()).find(
+      get_vsderef_dynamic_object_prefix())==0UL)
+  {
+    add(
+      mode,
+      to_symbol_expr(object).get_identifier(),
+      range_start,
+      range_start+new_size);
+  }
+
   // value_set_dereferencet::build_reference_to will turn *p into
   // DYNAMIC_OBJECT(p) ? *p : invalid_objectN
   if(object.is_not_nil() &&

src/analyses/reaching_definitions.cpp

@@ -22,6 +22,7 @@ Date: February 2013
 #include <util/make_unique.h>
 
 #include <pointer-analysis/value_set_analysis_fi.h>
+#include <pointer-analysis/value_set_dereference.h>
 
 #include "is_threaded.h"
 #include "dirty.h"
@@ -309,21 +310,25 @@ void rd_range_domaint::transform_assign(
   forall_rw_range_set_w_objects(it, rw_set)
   {
     const irep_idt &identifier=it->first;
-    // ignore symex::invalid_object
+    bool do_kill=is_must_alias;
     const symbolt *symbol_ptr;
     if(ns.lookup(identifier, symbol_ptr))
-      continue;
-    INVARIANT_STRUCTURED(
-      symbol_ptr!=nullptr,
-      nullptr_exceptiont,
-      "Symbol is in symbol table");
+    {
+      if(as_string(identifier).find(get_vsderef_dynamic_object_prefix())!=0UL)
+        // ignore symex::invalid_object
+        continue;
+    }
+    else
+    {
+      do_kill=do_kill &&
+       (!rd.get_is_threaded()(from) ||
+        (!symbol_ptr->is_shared() &&
+         !rd.get_is_dirty()(identifier)));
+    }
 
     const range_domaint &ranges=rw_set.get_ranges(it);
 
-    if(is_must_alias &&
-       (!rd.get_is_threaded()(from) ||
-        (!symbol_ptr->is_shared() &&
-         !rd.get_is_dirty()(identifier))))
+    if(do_kill)
       for(const auto &range : ranges)
         kill(identifier, range.first, range.second);
 

src/pointer-analysis/value_set_dereference.cpp

@@ -60,6 +60,12 @@ const exprt &value_set_dereferencet::get_symbol(const exprt &expr)
   return expr;
 }
 
+const std::string &get_vsderef_dynamic_object_prefix()
+{
+  static std::string prefix(CPROVER_PREFIX "_VSDEREF_");
+  return prefix;
+}
+
 /// \par parameters: expression dest, to be dereferenced under given guard,
 /// and given mode
 /// \return returns pointer after dereferencing
@@ -344,7 +350,9 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
     result.pointer_guard=dynamic_object_expr;
 
     // can't remove here, turn into *p
-    result.value=dereference_exprt(pointer_expr, dereference_type);
+    result.value=symbol_exprt(
+      get_vsderef_dynamic_object_prefix()+from_expr(root_object),
+      ns.follow(dereference_type));
 
     if(options.get_bool_option("pointer-check"))
     {

src/pointer-analysis/value_set_dereference.h

@@ -144,4 +144,6 @@ class value_set_dereferencet
     const exprt &offset);
 };
 
+const std::string &get_vsderef_dynamic_object_prefix();
+
 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H