Merge pull request #4251 from tautschnig/parameter-identifiers-locals

Local bitvector analysis: use parameter_identifiers [blocks: #4167]

Author: tautschnig

src/analyses/goto_check.cpp

@@ -1675,7 +1675,7 @@ void goto_checkt::goto_check(
 
   if(enable_pointer_check)
     local_bitvector_analysis =
-      util_make_unique<local_bitvector_analysist>(goto_function);
+      util_make_unique<local_bitvector_analysist>(goto_function, ns);
 
   goto_programt &goto_program=goto_function.body;
 

src/analyses/local_bitvector_analysis.cpp

@@ -60,13 +60,9 @@ bool local_bitvector_analysist::merge(points_tot &a, points_tot &b)
 /// \return return 'true' iff we track the object with given identifier
 bool local_bitvector_analysist::is_tracked(const irep_idt &identifier)
 {
-  localst::locals_mapt::const_iterator it=locals.locals_map.find(identifier);
-  if(it==locals.locals_map.end() ||
-     it->second.type().id()!=ID_pointer ||
-     dirty(identifier))
-    return false;
-
-  return true;
+  localst::locals_sett::const_iterator it = locals.locals.find(identifier);
+  return it != locals.locals.end() && ns.lookup(*it).type.id() == ID_pointer &&
+         !dirty(identifier);
 }
 
 void local_bitvector_analysist::assign_lhs(
@@ -254,9 +250,11 @@ void local_bitvector_analysist::build()
   // Gather the objects we track, and
   // feed in sufficiently bad defaults for their value
   // in the entry location.
-  for(const auto &local : locals.locals_map)
-    if(is_tracked(local.first))
-      loc_infos[0][pointers.number(local.first)]=flagst::mk_unknown();
+  for(const auto &local : locals.locals)
+  {
+    if(is_tracked(local))
+      loc_infos[0][pointers.number(local)] = flagst::mk_unknown();
+  }
 
   while(!work_queue.empty())
   {

src/analyses/local_bitvector_analysis.h

@@ -25,11 +25,13 @@ class local_bitvector_analysist
 public:
   typedef goto_functionst::goto_functiont goto_functiont;
 
-  explicit local_bitvector_analysist(
-    const goto_functiont &_goto_function):
-    dirty(_goto_function),
-    locals(_goto_function),
-    cfg(_goto_function.body)
+  local_bitvector_analysist(
+    const goto_functiont &_goto_function,
+    const namespacet &ns)
+    : dirty(_goto_function),
+      locals(_goto_function),
+      cfg(_goto_function.body),
+      ns(ns)
   {
     build();
   }
@@ -176,6 +178,7 @@ class local_bitvector_analysist
     const exprt &src);
 
 protected:
+  const namespacet &ns;
   void build();
 
   typedef std::stack<unsigned> work_queuet;

src/analyses/locals.cpp

@@ -18,20 +18,18 @@ Date: March 2013
 void localst::build(const goto_functiont &goto_function)
 {
   forall_goto_program_instructions(it, goto_function.body)
+  {
     if(it->is_decl())
-    {
-      const code_declt &code_decl=to_code_decl(it->code);
-      locals_map.emplace(code_decl.get_identifier(), code_decl.symbol());
-    }
-
-  for(const auto &param : goto_function.type.parameters())
-    locals_map.emplace(
-      param.get_identifier(),
-      symbol_exprt(param.get_identifier(), param.type()));
+      locals.insert(it->get_decl().get_identifier());
+  }
+
+  locals.insert(
+    goto_function.parameter_identifiers.begin(),
+    goto_function.parameter_identifiers.end());
 }
 
 void localst::output(std::ostream &out) const
 {
-  for(const auto &local : locals_map)
-    out << local.first << "\n";
+  for(const auto &local : locals)
+    out << local << "\n";
 }

src/analyses/locals.h

@@ -31,11 +31,11 @@ class localst
   // but including the function parameters.
   bool is_local(const irep_idt &identifier) const
   {
-    return locals_map.find(identifier)!=locals_map.end();
+    return locals.find(identifier) != locals.end();
   }
 
-  typedef std::map<irep_idt, symbol_exprt> locals_mapt;
-  locals_mapt locals_map;
+  typedef std::unordered_set<irep_idt> locals_sett;
+  locals_sett locals;
 
 protected:
   void build(const goto_functiont &goto_function);

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -299,7 +299,7 @@ int goto_instrument_parse_optionst::doit()
 
       forall_goto_functions(it, goto_model.goto_functions)
       {
-        local_bitvector_analysist local_bitvector_analysis(it->second);
+        local_bitvector_analysist local_bitvector_analysis(it->second, ns);
         std::cout << ">>>>\n";
         std::cout << ">>>> " << it->first << '\n';
         std::cout << ">>>>\n";