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 
17  const exprt &expr,
18  const irep_idt &l0,
19  const irep_idt &l1,
20  const irep_idt &l2,
21  std::ostream &os,
22  std::ostream &l1_object_os)
23 {
24  if(expr.id()==ID_member)
25  {
26  const member_exprt &member=to_member_expr(expr);
27 
28  build_ssa_identifier_rec(member.struct_op(), l0, l1, l2, os, l1_object_os);
29 
30  os << '.' << member.get_component_name();
31  }
32  else if(expr.id()==ID_index)
33  {
34  const index_exprt &index=to_index_expr(expr);
35 
36  build_ssa_identifier_rec(index.array(), l0, l1, l2, os, l1_object_os);
37 
38  mp_integer idx;
39  if(to_integer(to_constant_expr(index.index()), idx))
40  assert(false);
41 
42  os << '[' << idx << ']';
43  }
44  else if(expr.id()==ID_symbol)
45  {
46  auto symid=to_symbol_expr(expr).get_identifier();
47  os << symid;
48  l1_object_os << symid;
49 
50  if(!l0.empty())
51  {
52  // Distinguish different threads of execution
53  os << '!' << l0;
54  l1_object_os << '!' << l0;
55  }
56 
57  if(!l1.empty())
58  {
59  // Distinguish different calls to the same function (~stack frame)
60  os << '@' << l1;
61  l1_object_os << '@' << l1;
62  }
63 
64  if(!l2.empty())
65  {
66  // Distinguish SSA steps for the same variable
67  os << '#' << l2;
68  }
69  }
70  else
71  assert(false);
72 }
73 
74 std::pair<irep_idt, irep_idt> ssa_exprt::build_identifier(
75  const exprt &expr,
76  const irep_idt &l0,
77  const irep_idt &l1,
78  const irep_idt &l2)
79 {
80  std::ostringstream oss;
81  std::ostringstream l1_object_oss;
82 
83  build_ssa_identifier_rec(expr, l0, l1, l2, oss, l1_object_oss);
84 
85  return std::make_pair(irep_idt(oss.str()), irep_idt(l1_object_oss.str()));
86 }
BigInt mp_integer
Definition: mp_arith.h:19
const irep_idt & get_identifier() const
Definition: std_expr.h:120
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
static std::pair< irep_idt, irep_idt > build_identifier(const exprt &src, const irep_idt &l0, const irep_idt &l1, const irep_idt &l2)
Definition: ssa_expr.cpp:74
Extract member of struct or union.
Definition: std_expr.h:3214
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
const irep_idt & id() const
Definition: irep.h:189
exprt & index()
Definition: std_expr.h:1208
Base class for all expressions.
Definition: expr.h:46
const exprt & struct_op() const
Definition: std_expr.h:3270
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
irep_idt get_component_name() const
Definition: std_expr.h:3249
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
dstringt irep_idt
Definition: irep.h:32
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
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)
Definition: ssa_expr.cpp:16
bool empty() const
Definition: dstring.h:61
exprt & array()
Definition: std_expr.h:1198
array index operator
Definition: std_expr.h:1170