cprover
ssa_expr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "ssa_expr.h"
10 
11 #include <sstream>
12 #include <cassert>
13 
14 #include <util/arith_tools.h>
15 
21  const exprt &expr,
22  const irep_idt &l0,
23  const irep_idt &l1,
24  const irep_idt &l2,
25  std::ostream &os,
26  std::ostream &l1_object_os)
27 {
28  if(expr.id()==ID_member)
29  {
30  const member_exprt &member=to_member_expr(expr);
31 
32  build_ssa_identifier_rec(member.struct_op(), l0, l1, l2, os, l1_object_os);
33 
34  os << '.' << member.get_component_name();
35  }
36  else if(expr.id()==ID_index)
37  {
38  const index_exprt &index=to_index_expr(expr);
39 
40  build_ssa_identifier_rec(index.array(), l0, l1, l2, os, l1_object_os);
41 
42  const mp_integer idx = numeric_cast_v<mp_integer>(index.index());
43  os << '[' << idx << ']';
44  }
45  else if(expr.id()==ID_symbol)
46  {
47  auto symid=to_symbol_expr(expr).get_identifier();
48  os << symid;
49  l1_object_os << symid;
50 
51  if(!l0.empty())
52  {
53  // Distinguish different threads of execution
54  os << '!' << l0;
55  l1_object_os << '!' << l0;
56  }
57 
58  if(!l1.empty())
59  {
60  // Distinguish different calls to the same function (~stack frame)
61  os << '@' << l1;
62  l1_object_os << '@' << l1;
63  }
64 
65  if(!l2.empty())
66  {
67  // Distinguish SSA steps for the same variable
68  os << '#' << l2;
69  }
70  }
71  else
73 }
74 
75 /* Used to determine whether or not an identifier can be built
76  * before trying and getting an exception */
78 {
79  if(expr.id()==ID_symbol)
80  return true;
81  else if(expr.id() == ID_member)
82  return can_build_identifier(to_member_expr(expr).compound());
83  else if(expr.id() == ID_index)
84  return can_build_identifier(to_index_expr(expr).array());
85  else
86  return false;
87 }
88 
89 static std::pair<irep_idt, irep_idt> build_identifier(
90  const exprt &expr,
91  const irep_idt &l0,
92  const irep_idt &l1,
93  const irep_idt &l2)
94 {
95  std::ostringstream oss;
96  std::ostringstream l1_object_oss;
97 
98  build_ssa_identifier_rec(expr, l0, l1, l2, oss, l1_object_oss);
99 
100  return std::make_pair(irep_idt(oss.str()), irep_idt(l1_object_oss.str()));
101 }
102 
104 {
105  const irep_idt &l0 = get_level_0();
106  const irep_idt &l1 = get_level_1();
107  const irep_idt &l2 = get_level_2();
108 
109  auto idpair = build_identifier(get_original_expr(), l0, l1, l2);
110  set_identifier(idpair.first);
111  set(ID_L1_object_identifier, idpair.second);
112 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
arith_tools.h
ssa_exprt::get_level_0
const irep_idt get_level_0() const
Definition: ssa_expr.h:107
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
build_identifier
static std::pair< irep_idt, irep_idt > build_identifier(const exprt &expr, const irep_idt &l0, const irep_idt &l1, const irep_idt &l2)
Definition: ssa_expr.cpp:89
exprt
Base class for all expressions.
Definition: expr.h:54
irep_idt
dstringt irep_idt
Definition: irep.h:32
ssa_exprt::get_original_expr
const exprt & get_original_expr() const
Definition: ssa_expr.h:41
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
build_ssa_identifier_rec
static void build_ssa_identifier_rec(const exprt &expr, const irep_idt &l0, const irep_idt &l1, const irep_idt &l2, std::ostream &os, std::ostream &l1_object_os)
If expr is a symbol "s" add to os "s!l0@l1#l2" and to l1_object_os "s!l0@l1".
Definition: ssa_expr.cpp:20
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3931
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
index_exprt::index
exprt & index()
Definition: std_expr.h:1631
ssa_exprt::get_level_2
const irep_idt get_level_2() const
Definition: ssa_expr.h:117
index_exprt::array
exprt & array()
Definition: std_expr.h:1621
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
irept::id
const irep_idt & id() const
Definition: irep.h:259
dstringt::empty
bool empty() const
Definition: dstring.h:75
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3890
ssa_expr.h
ssa_exprt::update_identifier
void update_identifier()
Definition: ssa_expr.cpp:103
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
ssa_exprt::get_level_1
const irep_idt get_level_1() const
Definition: ssa_expr.h:112
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3915
index_exprt
Array index operator.
Definition: std_expr.h:1595
ssa_exprt::can_build_identifier
static bool can_build_identifier(const exprt &src)
Definition: ssa_expr.cpp:77
symbol_exprt::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:171