Merge pull request #6710 from tautschnig/bugfixes/array-ops-dependence-graph

Handle array_{copy,replace,set} in dependence graph

Author: tautschnig

regression/cbmc/Bool5/full-slice.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--full-slice
+Generated 4 VCC\(s\), 0 remaining after simplification
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/analyses/goto_rw.cpp

@@ -621,6 +621,17 @@ void rw_range_sett::get_objects_rec(const typet &type)
   }
 }
 
+void rw_range_sett::get_array_objects(
+  const irep_idt &,
+  goto_programt::const_targett,
+  get_modet mode,
+  const exprt &pointer)
+{
+  object_descriptor_exprt ode;
+  ode.build(dereference_exprt{skip_typecast(pointer)}, ns);
+  get_objects_rec(mode, ode.root_object(), -1, -1);
+}
+
 void rw_range_set_value_sett::get_objects_dereference(
   get_modet mode,
   const dereference_exprt &deref,
@@ -737,6 +748,50 @@ static void goto_rw_assign(
   rw_set.get_objects_rec(function, target, rw_range_sett::get_modet::READ, rhs);
 }
 
+static void goto_rw_other(
+  const irep_idt &function,
+  goto_programt::const_targett target,
+  const codet &code,
+  rw_range_sett &rw_set)
+{
+  const irep_idt &statement = code.get_statement();
+
+  if(statement == ID_printf)
+  {
+    // if it's printf, mark the operands as read here
+    for(const auto &op : code.operands())
+    {
+      rw_set.get_objects_rec(
+        function, target, rw_range_sett::get_modet::READ, op);
+    }
+  }
+  else if(statement == ID_array_equal)
+  {
+    // mark the dereferenced operands as being read
+    for(const auto &op : code.operands())
+    {
+      rw_set.get_array_objects(
+        function, target, rw_range_sett::get_modet::READ, op);
+    }
+  }
+  else if(statement == ID_array_set)
+  {
+    PRECONDITION(code.operands().size() == 2);
+    rw_set.get_array_objects(
+      function, target, rw_range_sett::get_modet::LHS_W, code.op0());
+    rw_set.get_objects_rec(
+      function, target, rw_range_sett::get_modet::READ, code.op1());
+  }
+  else if(statement == ID_array_copy || statement == ID_array_replace)
+  {
+    PRECONDITION(code.operands().size() == 2);
+    rw_set.get_array_objects(
+      function, target, rw_range_sett::get_modet::LHS_W, code.op0());
+    rw_set.get_array_objects(
+      function, target, rw_range_sett::get_modet::READ, code.op1());
+  }
+}
+
 static void goto_rw(
   const irep_idt &function,
   goto_programt::const_targett target,
@@ -787,13 +842,7 @@ void goto_rw(
     break;
 
   case OTHER:
-    // if it's printf, mark the operands as read here
-    if(target->get_other().get_statement() == ID_printf)
-    {
-      for(const auto &op : target->get_other().operands())
-        rw_set.get_objects_rec(
-          function, target, rw_range_sett::get_modet::READ, op);
-    }
+    goto_rw_other(function, target, target->get_other(), rw_set);
     break;
 
   case SKIP:

src/analyses/goto_rw.h

@@ -148,6 +148,12 @@ class rw_range_sett
     get_objects_rec(type);
   }
 
+  virtual void get_array_objects(
+    const irep_idt &,
+    goto_programt::const_targett,
+    get_modet,
+    const exprt &);
+
   void output(std::ostream &out) const;
 
 protected:
@@ -288,6 +294,18 @@ class rw_range_set_value_sett:public rw_range_sett
     rw_range_sett::get_objects_rec(type);
   }
 
+  void get_array_objects(
+    const irep_idt &_function,
+    goto_programt::const_targett _target,
+    get_modet mode,
+    const exprt &pointer) override
+  {
+    function = _function;
+    target = _target;
+
+    rw_range_sett::get_array_objects(_function, _target, mode, pointer);
+  }
+
 protected:
   value_setst &value_sets;
   irep_idt function;

src/analyses/reaching_definitions.cpp

@@ -126,6 +126,9 @@ void rd_range_domaint::transform(
   // initial (non-deterministic) value
   else if(from->is_decl())
     transform_assign(ns, from, function_from, from, *rd);
+  // array_set, array_copy, array_replace have side effects
+  else if(from->is_other())
+    transform_assign(ns, from, function_from, from, *rd);
 }
 
 /// Computes an instance obtained from a `*this` by transformation over `DEAD v`