Merge pull request #7106 from remi-delmas-3000/fix-dirtyt

Make dirtyt traverse operands of OTHER instructions

Author: tautschnig

src/analyses/dirty.cpp

@@ -19,14 +19,49 @@ Date: March 2013
 void dirtyt::build(const goto_functiont &goto_function)
 {
   for(const auto &i : goto_function.body.instructions)
-    i.apply([this](const exprt &e) { find_dirty(e); });
+  {
+    if(i.is_other())
+    {
+      search_other(i);
+    }
+    else
+    {
+      i.apply([this](const exprt &e) { find_dirty(e); });
+    }
+  }
+}
+
+void dirtyt::search_other(const goto_programt::instructiont &instruction)
+{
+  INVARIANT(instruction.is_other(), "instruction type must be OTHER");
+  if(instruction.get_other().id() == ID_code)
+  {
+    const codet &code = instruction.get_other();
+    const irep_idt &statement = code.get_statement();
+    if(
+      statement == ID_expression || statement == ID_array_set ||
+      statement == ID_array_equal || statement == ID_array_copy ||
+      statement == ID_array_replace || statement == ID_havoc_object ||
+      statement == ID_input || statement == ID_output)
+    {
+      forall_operands(it, code)
+        find_dirty(*it);
+    }
+    // other possible cases according to goto_programt::instructiont::output
+    // and goto_symext::symex_other:
+    // statement == ID_fence ||
+    // statement == ID_user_specified_predicate ||
+    // statement == ID_user_specified_parameter_predicates ||
+    // statement == ID_user_specified_return_predicates ||
+    // statement == ID_decl || statement == ID_nondet || statement == ID_asm)
+  }
 }
 
 void dirtyt::find_dirty(const exprt &expr)
 {
-  if(expr.id()==ID_address_of)
+  if(expr.id() == ID_address_of)
   {
-    const address_of_exprt &address_of_expr=to_address_of_expr(expr);
+    const address_of_exprt &address_of_expr = to_address_of_expr(expr);
     find_dirty_address_of(address_of_expr.object());
     return;
   }
@@ -37,27 +72,26 @@ void dirtyt::find_dirty(const exprt &expr)
 
 void dirtyt::find_dirty_address_of(const exprt &expr)
 {
-  if(expr.id()==ID_symbol)
+  if(expr.id() == ID_symbol)
   {
-    const irep_idt &identifier=
-      to_symbol_expr(expr).get_identifier();
+    const irep_idt &identifier = to_symbol_expr(expr).get_identifier();
 
     dirty.insert(identifier);
   }
-  else if(expr.id()==ID_member)
+  else if(expr.id() == ID_member)
   {
     find_dirty_address_of(to_member_expr(expr).struct_op());
   }
-  else if(expr.id()==ID_index)
+  else if(expr.id() == ID_index)
   {
     find_dirty_address_of(to_index_expr(expr).array());
     find_dirty(to_index_expr(expr).index());
   }
-  else if(expr.id()==ID_dereference)
+  else if(expr.id() == ID_dereference)
   {
     find_dirty(to_dereference_expr(expr).pointer());
   }
-  else if(expr.id()==ID_if)
+  else if(expr.id() == ID_if)
   {
     find_dirty_address_of(to_if_expr(expr).true_case());
     find_dirty_address_of(to_if_expr(expr).false_case());
@@ -76,7 +110,8 @@ void dirtyt::output(std::ostream &out) const
 /// \param id: function id to analyse
 /// \param function: function to analyse
 void incremental_dirtyt::populate_dirty_for_function(
-  const irep_idt &id, const goto_functionst::goto_functiont &function)
+  const irep_idt &id,
+  const goto_functionst::goto_functiont &function)
 {
   auto insert_result = dirty_processed_functions.insert(id);
   if(insert_result.second)

src/analyses/dirty.h

@@ -14,12 +14,13 @@ Date: March 2013
 #ifndef CPROVER_ANALYSES_DIRTY_H
 #define CPROVER_ANALYSES_DIRTY_H
 
-#include <unordered_set>
-
-#include <util/std_expr.h>
 #include <util/invariant.h>
+#include <util/std_expr.h>
+
 #include <goto-programs/goto_functions.h>
 
+#include <unordered_set>
+
 /// Dirty variables are ones which have their address taken so we can't
 /// reliably work out where they may be assigned and are also considered shared
 /// state in the presence of multi-threading.
@@ -65,7 +66,7 @@ class dirtyt
   bool operator()(const irep_idt &id) const
   {
     die_if_uninitialized();
-    return dirty.find(id)!=dirty.end();
+    return dirty.find(id) != dirty.end();
   }
 
   bool operator()(const symbol_exprt &expr) const
@@ -100,14 +101,12 @@ class dirtyt
 
   // variables whose address is taken
   std::unordered_set<irep_idt> dirty;
-
+  void search_other(const goto_programt::instructiont &instruction);
   void find_dirty(const exprt &expr);
   void find_dirty_address_of(const exprt &expr);
 };
 
-inline std::ostream &operator<<(
-  std::ostream &out,
-  const dirtyt &dirty)
+inline std::ostream &operator<<(std::ostream &out, const dirtyt &dirty)
 {
   dirty.output(out);
   return out;
@@ -119,7 +118,8 @@ class incremental_dirtyt
 {
 public:
   void populate_dirty_for_function(
-    const irep_idt &id, const goto_functionst::goto_functiont &function);
+    const irep_idt &id,
+    const goto_functionst::goto_functiont &function);
 
   bool operator()(const irep_idt &id) const
   {

src/goto-instrument/contracts/cfg_info.h

@@ -31,51 +31,6 @@ Date: June 2022
 #include <set>
 #include <vector>
 
-/// Work around the fact that dirtyt does not look into
-/// OTHER instructions
-class dirty_altt : public dirtyt
-{
-public:
-  dirty_altt() : dirtyt()
-  {
-  }
-
-  explicit dirty_altt(const goto_functiont &goto_function)
-    : dirtyt(goto_function)
-  {
-    collect_other(goto_function);
-  }
-
-  explicit dirty_altt(const goto_functionst &goto_functions)
-    : dirtyt(goto_functions)
-  {
-    for(const auto &gf_entry : goto_functions.function_map)
-      collect_other(gf_entry.second);
-  }
-
-protected:
-  void collect_other(const goto_functiont &goto_function)
-  {
-    for(const auto &i : goto_function.body.instructions)
-    {
-      if(i.is_other())
-      {
-        auto &statement = i.get_other().get_statement();
-        if(
-          statement == ID_array_set || statement == ID_array_copy ||
-          statement == ID_array_replace || statement == ID_array_equal ||
-          statement == ID_havoc_object)
-        {
-          for(const auto &op : i.get_other().operands())
-          {
-            find_dirty(op);
-          }
-        }
-      }
-    }
-  }
-};
-
 /// Stores information about a goto function computed from its CFG.
 ///
 /// The methods of this class provide information about identifiers
@@ -177,7 +132,7 @@ class function_cfg_infot : public cfg_infot
   }
 
 private:
-  const dirty_altt is_dirty;
+  const dirtyt is_dirty;
   const localst locals;
   std::unordered_set<irep_idt> parameters;
 };
@@ -230,7 +185,7 @@ class loop_cfg_infot : public cfg_infot
   }
 
 private:
-  const dirty_altt is_dirty;
+  const dirtyt is_dirty;
   std::unordered_set<irep_idt> locals;
 };
 #endif