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))
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
72 }
73 
74 /* Used to determine whether or not an identifier can be built
75  * before trying and getting an exception */
77 {
78  if(expr.id()==ID_symbol)
79  return true;
80  else if(expr.id()==ID_member ||
81  expr.id()==ID_index)
82  return can_build_identifier(expr.op0());
83  else
84  return false;
85 }
86 
87 std::pair<irep_idt, irep_idt> ssa_exprt::build_identifier(
88  const exprt &expr,
89  const irep_idt &l0,
90  const irep_idt &l1,
91  const irep_idt &l2)
92 {
93  std::ostringstream oss;
94  std::ostringstream l1_object_oss;
95 
96  build_ssa_identifier_rec(expr, l0, l1, l2, oss, l1_object_oss);
97 
98  return std::make_pair(irep_idt(oss.str()), irep_idt(l1_object_oss.str()));
99 }
BigInt mp_integer
Definition: mp_arith.h:22
exprt & op0()
Definition: expr.h:72
const irep_idt & get_identifier() const
Definition: std_expr.h:128
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:87
Extract member of struct or union.
Definition: std_expr.h:3871
const irep_idt & id() const
Definition: irep.h:189
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3955
static bool can_build_identifier(const exprt &src)
Definition: ssa_expr.cpp:76
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4465
exprt & index()
Definition: std_expr.h:1496
Base class for all expressions.
Definition: expr.h:42
const exprt & struct_op() const
Definition: std_expr.h:3911
irep_idt get_component_name() const
Definition: std_expr.h:3895
#define UNREACHABLE
Definition: invariant.h:250
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
dstringt irep_idt
Definition: irep.h:31
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:1486
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
array index operator
Definition: std_expr.h:1462