cprover
uncaught_exceptions_analysis.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Over-approximating uncaught exceptions analysis
4 
5 Author: Cristina David
6 
7 \*******************************************************************/
8 
11 
12 #ifdef DEBUG
13 #include <iostream>
14 #endif
16 
19 {
20  PRECONDITION(type.id()==ID_pointer);
21 
22  if(type.subtype().id()==ID_symbol)
23  {
24  return to_symbol_type(type.subtype()).get_identifier();
25  }
26  return ID_empty;
27 }
28 
31 {
32  if(expr.id()!=ID_symbol && expr.has_operands())
33  return get_exception_symbol(expr.op0());
34 
35  return expr;
36 }
37 
40  const irep_idt &element)
41 {
42  thrown.insert(element);
43 }
44 
46  const std::set<irep_idt> &elements)
47 {
48  thrown.insert(elements.begin(), elements.end());
49 }
50 
52  const std::vector<irep_idt> &elements)
53 {
54  thrown.insert(elements.begin(), elements.end());
55 }
56 
57 
62  const namespacet &)
63 {
64  const goto_programt::instructiont &instruction=*from;
65 
66  switch(instruction.type)
67  {
68  case THROW:
69  {
70  const exprt &exc_symbol=get_exception_symbol(instruction.code);
71  // retrieve the static type of the thrown exception
72  const irep_idt &type_id=get_exception_type(exc_symbol.type());
73  join(type_id);
74  // we must consider all the subtypes given that
75  // the runtime type is a subtype of the static type
76  std::vector<irep_idt> subtypes =
78  join(subtypes);
79  break;
80  }
81  case CATCH:
82  {
83  if(!instruction.code.has_operands())
84  {
85  if(!instruction.targets.empty()) // push
86  {
87  std::set<irep_idt> caught;
88  stack_caught.push_back(caught);
89  std::set<irep_idt> &last_caught=stack_caught.back();
90  const irept::subt &exception_list=
91  instruction.code.find(ID_exception_list).get_sub();
92 
93  for(const auto &exc : exception_list)
94  {
95  last_caught.insert(exc.id());
96  std::vector<irep_idt> subtypes=
98  last_caught.insert(subtypes.begin(), subtypes.end());
99  }
100  }
101  else // pop
102  {
103  if(!stack_caught.empty())
104  {
105  const std::set<irep_idt> &caught=stack_caught.back();
106  join(caught);
107  // remove the caught exceptions
108  for(const auto &exc_id : caught)
109  thrown.erase(exc_id);
110  stack_caught.pop_back();
111  }
112  }
113  }
114  break;
115  }
116  case FUNCTION_CALL:
117  {
118  const exprt &function_expr=
119  to_code_function_call(instruction.code).function();
121  function_expr.id()==ID_symbol,
122  "identifier expected to be a symbol");
123  const irep_idt &function_name=
124  to_symbol_expr(function_expr).get_identifier();
125  // use the current information about the callee
126  join(uea.exceptions_map[function_name]);
127  break;
128  }
129  default:
130  {}
131  }
132 }
133 
135 const std::set<irep_idt> &uncaught_exceptions_domaint::get_elements() const
136 {
137  return thrown;
138 }
139 
142  const namespacet &ns)
143 {
145 }
146 
149  const goto_functionst &goto_functions,
150  const namespacet &ns)
151 {
152  bool change=true;
153 
154  while(change)
155  {
156  change=false;
157  // add all the functions to the worklist
158  forall_goto_functions(current_function, goto_functions)
159  {
160  domain.make_top();
161  const goto_programt &goto_program=current_function->second.body;
162 
163  if(goto_program.empty())
164  continue;
165 
167  {
168  domain.transform(instr_it, *this, ns);
169  }
170  // did our estimation for the current function improve?
171  const std::set<irep_idt> &elements=domain.get_elements();
172  if(exceptions_map[current_function->first].size()<elements.size())
173  {
174  change=true;
175  exceptions_map[current_function->first]=elements;
176  }
177  }
178  }
179 }
180 
184  const goto_functionst &goto_functions) const
185 {
186 #ifdef DEBUG
187  forall_goto_functions(it, goto_functions)
188  {
189  const auto fn=it->first;
190  const exceptions_mapt::const_iterator found=exceptions_map.find(fn);
191  // Functions like __CPROVER_assert and __CPROVER_assume are replaced by
192  // explicit GOTO instructions and will not show up in exceptions_map.
193  if(found==exceptions_map.end())
194  continue;
195 
196  const auto &fs=found->second;
197  if(!fs.empty())
198  {
199  std::cout << "Uncaught exceptions in function " <<
200  fn << ": " << std::endl;
201  for(const auto exc_id : fs)
202  std::cout << id2string(exc_id) << " ";
203  std::cout << std::endl;
204  }
205  }
206 #endif
207 }
208 
211  const goto_functionst &goto_functions,
212  const namespacet &ns,
213  exceptions_mapt &exceptions)
214 {
215  domain(ns);
216  collect_uncaught_exceptions(goto_functions, ns);
217  exceptions=exceptions_map;
218  output(goto_functions);
219 }
220 
223  const goto_functionst &goto_functions,
224  const namespacet &ns,
225  std::map<irep_idt, std::set<irep_idt>> &exceptions_map)
226 {
228  exceptions(goto_functions, ns, exceptions_map);
229 }
The type of an expression.
Definition: type.h:22
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
Over-approximative uncaught exceptions analysis.
const symbol_tablet & get_symbol_table() const
Definition: namespace.h:106
void output(const goto_functionst &) const
Prints the exceptions map that maps each method to the set of exceptions that may escape it...
exprt & op0()
Definition: expr.h:72
std::vector< irept > subt
Definition: irep.h:160
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:185
const irep_idt & get_identifier() const
Definition: std_expr.h:128
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
typet & type()
Definition: expr.h:56
subt & get_sub()
Definition: irep.h:317
targetst targets
The list of successor instructions.
Definition: goto_program.h:198
void transform(const goto_programt::const_targett, uncaught_exceptions_analysist &, const namespacet &)
The transformer for the uncaught exceptions domain.
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
const std::set< irep_idt > & get_elements() const
Returns the value of the private member thrown.
std::map< irep_idt, std::set< irep_idt > > exceptions_mapt
const irep_idt & id() const
Definition: irep.h:259
void uncaught_exceptions(const goto_functionst &goto_functions, const namespacet &ns, std::map< irep_idt, std::set< irep_idt >> &exceptions_map)
Applies the uncaught exceptions analysis and outputs the result.
void join(const irep_idt &)
The join operator for the uncaught exceptions domain.
instructionst::const_iterator const_targett
Definition: goto_program.h:398
static irep_idt get_exception_type(const typet &type)
Returns the compile type of an exception.
TO_BE_DOCUMENTED.
Definition: namespace.h:74
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
void collect_uncaught_exceptions(const goto_functionst &, const namespacet &)
Runs the uncaught exceptions analysis, which populates the exceptions map.
static exprt get_exception_symbol(const exprt &exor)
Returns the symbol corresponding to an exception.
bool has_operands() const
Definition: expr.h:63
void operator()(const namespacet &ns)
Constructs the class hierarchy.
void operator()(const goto_functionst &, const namespacet &, exceptions_mapt &)
Applies the uncaught exceptions analysis and outputs the result.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
exprt & function()
Definition: std_code.h:878
Base class for all expressions.
Definition: expr.h:42
bool empty() const
Is the program empty?
Definition: goto_program.h:590
goto_programt & goto_program
Definition: cover.cpp:63
const typet & subtype() const
Definition: type.h:33
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
#define forall_goto_functions(it, functions)
idst get_children_trans(const irep_idt &id) const
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
computes in exceptions_map an overapproximation of the exceptions thrown by each method ...
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909