cprover
renaming_level.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Romain Brenguier, romain.brenguier@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #include "renaming_level.h"
13 
14 #include <util/namespace.h>
15 #include <util/ssa_expr.h>
16 #include <util/symbol.h>
17 
18 void symex_level0t::
19 operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr)
20 {
21  // already renamed?
22  if(!ssa_expr.get_level_0().empty())
23  return;
24 
25  const irep_idt &obj_identifier = ssa_expr.get_object_name();
26 
27  // guards are not L0-renamed
28  if(obj_identifier == "goto_symex::\\guard")
29  return;
30 
31  const symbolt *s;
32  const bool found_l0 = !ns.lookup(obj_identifier, s);
33  INVARIANT(found_l0, "level0: failed to find " + id2string(obj_identifier));
34 
35  // don't rename shared variables or functions
36  if(s->type.id() == ID_code || s->is_shared())
37  return;
38 
39  // rename!
40  ssa_expr.set_level_0(thread_nr);
41 }
42 
44 {
45  // already renamed?
46  if(!ssa_expr.get_level_1().empty())
47  return;
48 
49  const irep_idt l0_name = ssa_expr.get_l1_object_identifier();
50 
51  const auto it = current_names.find(l0_name);
52  if(it == current_names.end())
53  return;
54 
55  // rename!
56  ssa_expr.set_level_1(it->second.second);
57 }
58 
61 {
62  auto it = current_names.begin();
63  for(const auto &pair : other)
64  {
65  while(it != current_names.end() && it->first < pair.first)
66  ++it;
67  if(it == current_names.end() || pair.first < it->first)
68  current_names.insert(it, pair);
69  else if(it != current_names.end())
70  {
71  PRECONDITION(it->first == pair.first);
72  it->second = pair.second;
73  ++it;
74  }
75  }
76 }
bool is_shared() const
Definition: symbol.h:95
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
Symbol table entry.
void set_level_1(unsigned i)
Definition: ssa_expr.h:89
Symbol table entry.
Definition: symbol.h:27
const irep_idt get_l1_object_identifier() const
Definition: ssa_expr.h:66
const irep_idt get_level_1() const
Definition: ssa_expr.h:112
const irep_idt & id() const
Definition: irep.h:259
void set_level_0(unsigned i)
Definition: ssa_expr.h:83
void operator()(ssa_exprt &ssa_expr)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
const irep_idt get_level_0() const
Definition: ssa_expr.h:107
current_namest current_names
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
void operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr)
typet type
Type of symbol.
Definition: symbol.h:31
void restore_from(const current_namest &other)
Insert the content of other into this renaming.
std::map< irep_idt, std::pair< ssa_exprt, unsigned > > current_namest
Map identifier to ssa_exprt and counter.
irep_idt get_object_name() const
Definition: ssa_expr.h:46
bool empty() const
Definition: dstring.h:75
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
Renaming levels.