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 
17 #include <util/namespace.h>
18 #include <util/symbol_table.h>
19 
21 
24 {
25  PRECONDITION(type.id()==ID_pointer);
26 
27  if(type.subtype().id() == ID_struct_tag)
28  return to_struct_tag_type(type.subtype()).get_identifier();
29  else
30  return ID_empty;
31 }
32 
35 {
36  if(expr.id() != ID_symbol && expr.operands().size() >= 1)
37  return get_exception_symbol(to_multi_ary_expr(expr).op0());
38 
39  return expr;
40 }
41 
44  const irep_idt &element)
45 {
46  thrown.insert(element);
47 }
48 
50  const std::set<irep_idt> &elements)
51 {
52  thrown.insert(elements.begin(), elements.end());
53 }
54 
56  const std::vector<irep_idt> &elements)
57 {
58  thrown.insert(elements.begin(), elements.end());
59 }
60 
61 
66  const namespacet &)
67 {
68  const goto_programt::instructiont &instruction=*from;
69 
70  switch(instruction.type)
71  {
72  case THROW:
73  {
74  const exprt &exc_symbol = get_exception_symbol(instruction.get_code());
75  // retrieve the static type of the thrown exception
76  const irep_idt &type_id=get_exception_type(exc_symbol.type());
77  join(type_id);
78  // we must consider all the subtypes given that
79  // the runtime type is a subtype of the static type
80  std::vector<irep_idt> subtypes =
82  join(subtypes);
83  break;
84  }
85  case CATCH:
86  {
87  if(!instruction.get_code().has_operands())
88  {
89  if(!instruction.targets.empty()) // push
90  {
91  std::set<irep_idt> caught;
92  stack_caught.push_back(caught);
93  std::set<irep_idt> &last_caught=stack_caught.back();
94  const irept::subt &exception_list =
95  instruction.get_code().find(ID_exception_list).get_sub();
96 
97  for(const auto &exc : exception_list)
98  {
99  last_caught.insert(exc.id());
100  std::vector<irep_idt> subtypes=
102  last_caught.insert(subtypes.begin(), subtypes.end());
103  }
104  }
105  else // pop
106  {
107  if(!stack_caught.empty())
108  {
109  const std::set<irep_idt> &caught=stack_caught.back();
110  join(caught);
111  // remove the caught exceptions
112  for(const auto &exc_id : caught)
113  thrown.erase(exc_id);
114  stack_caught.pop_back();
115  }
116  }
117  }
118  break;
119  }
120  case FUNCTION_CALL:
121  {
122  const exprt &function_expr = instruction.call_function();
124  function_expr.id()==ID_symbol,
125  "identifier expected to be a symbol");
126  const irep_idt &function_name=
127  to_symbol_expr(function_expr).get_identifier();
128  // use the current information about the callee
129  join(uea.exceptions_map[function_name]);
130  break;
131  }
132  case DECL: // Safe to ignore in this context
133  case DEAD: // Safe to ignore in this context
134  case ASSIGN: // Safe to ignore in this context
135  break;
136  case SET_RETURN_VALUE:
137 #if 0
138  DATA_INVARIANT(false, "Returns must be removed before analysis");
139 #endif
140  break;
141  case GOTO: // Ignoring the guard is a valid over-approximation
142  case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
143  case ATOMIC_END: // Ignoring is a valid over-approximation
144  case START_THREAD: // Require a concurrent analysis at higher level
145  case END_THREAD: // Require a concurrent analysis at higher level
146  case END_FUNCTION: // No action required
147  case ASSERT: // No action required
148  case ASSUME: // Ignoring is a valid over-approximation
149  case LOCATION: // No action required
150  case SKIP: // No action required
151  break;
152  case OTHER:
153 #if 0
154  DATA_INVARIANT(false, "Unclear what is a safe over-approximation of OTHER");
155 #endif
156  break;
157  case INCOMPLETE_GOTO:
158  case NO_INSTRUCTION_TYPE:
159  DATA_INVARIANT(false, "Only complete instructions can be analyzed");
160  break;
161  }
162 }
163 
165 const std::set<irep_idt> &uncaught_exceptions_domaint::get_elements() const
166 {
167  return thrown;
168 }
169 
172  const namespacet &ns)
173 {
175 }
176 
179  const goto_functionst &goto_functions,
180  const namespacet &ns)
181 {
182  bool change=true;
183 
184  while(change)
185  {
186  change=false;
187  // add all the functions to the worklist
188  for(const auto &gf_entry : goto_functions.function_map)
189  {
190  domain.make_top();
191  const goto_programt &goto_program = gf_entry.second.body;
192 
193  if(goto_program.empty())
194  continue;
195 
196  forall_goto_program_instructions(instr_it, goto_program)
197  {
198  domain.transform(instr_it, *this, ns);
199  }
200  // did our estimation for the current function improve?
201  const std::set<irep_idt> &elements=domain.get_elements();
202  if(exceptions_map[gf_entry.first].size() < elements.size())
203  {
204  change=true;
205  exceptions_map[gf_entry.first] = elements;
206  }
207  }
208  }
209 }
210 
214  const goto_functionst &goto_functions) const
215 {
216  (void)goto_functions; // unused parameter
217 #ifdef DEBUG
218  for(const auto &gf_entry : goto_functions.function_map)
219  {
220  const auto fn = gf_entry.first;
221  const exceptions_mapt::const_iterator found=exceptions_map.find(fn);
222  // Functions like __CPROVER_assert and __CPROVER_assume are replaced by
223  // explicit GOTO instructions and will not show up in exceptions_map.
224  if(found==exceptions_map.end())
225  continue;
226 
227  const auto &fs=found->second;
228  if(!fs.empty())
229  {
230  std::cout << "Uncaught exceptions in function " <<
231  fn << ": " << std::endl;
232  for(const auto exc_id : fs)
233  std::cout << id2string(exc_id) << " ";
234  std::cout << std::endl;
235  }
236  }
237 #endif
238 }
239 
242  const goto_functionst &goto_functions,
243  const namespacet &ns,
244  exceptions_mapt &exceptions)
245 {
246  domain(ns);
247  collect_uncaught_exceptions(goto_functions, ns);
248  exceptions=exceptions_map;
249  output(goto_functions);
250 }
251 
254  const goto_functionst &goto_functions,
255  const namespacet &ns,
256  std::map<irep_idt, std::set<irep_idt>> &exceptions_map)
257 {
259  exceptions(goto_functions, ns, exceptions_map);
260 }
idst get_children_trans(const irep_idt &id) const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:89
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
A collection of goto functions.
function_mapt function_map
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
Definition: goto_program.h:361
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:434
targetst targets
The list of successor instructions.
Definition: goto_program.h:468
const codet & get_code() const
Get the code represented by this instruction.
Definition: goto_program.h:185
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
instructionst::const_iterator const_targett
Definition: goto_program.h:647
bool empty() const
Is the program empty?
Definition: goto_program.h:826
subt & get_sub()
Definition: irep.h:467
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
const irep_idt & id() const
Definition: irep.h:407
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:123
const irep_idt & get_identifier() const
Definition: std_expr.h:109
const irep_idt & get_identifier() const
Definition: std_types.h:410
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
computes in exceptions_map an overapproximation of the exceptions thrown by each method
void operator()(const goto_functionst &, const namespacet &, exceptions_mapt &)
Applies the uncaught exceptions analysis and outputs the result.
void output(const goto_functionst &) const
Prints the exceptions map that maps each method to the set of exceptions that may escape it.
std::map< irep_idt, std::set< irep_idt > > exceptions_mapt
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.
void transform(const goto_programt::const_targett, uncaught_exceptions_analysist &, const namespacet &)
The transformer for the uncaught exceptions domain.
void operator()(const namespacet &ns)
Constructs the class hierarchy.
static irep_idt get_exception_type(const typet &type)
Returns the compile type of an exception.
const std::set< irep_idt > & get_elements() const
Returns the value of the private member thrown.
void join(const irep_idt &)
The join operator for the uncaught exceptions domain.
Goto Programs with Functions.
#define forall_goto_program_instructions(it, program)
@ FUNCTION_CALL
Definition: goto_program.h:47
@ ATOMIC_END
Definition: goto_program.h:42
@ DEAD
Definition: goto_program.h:46
@ END_FUNCTION
Definition: goto_program.h:40
@ ASSIGN
Definition: goto_program.h:44
@ ASSERT
Definition: goto_program.h:34
@ SET_RETURN_VALUE
Definition: goto_program.h:43
@ ATOMIC_BEGIN
Definition: goto_program.h:41
@ CATCH
Definition: goto_program.h:49
@ END_THREAD
Definition: goto_program.h:38
@ SKIP
Definition: goto_program.h:36
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:31
@ START_THREAD
Definition: goto_program.h:37
@ THROW
Definition: goto_program.h:48
@ DECL
Definition: goto_program.h:45
@ OTHER
Definition: goto_program.h:35
@ GOTO
Definition: goto_program.h:32
@ INCOMPLETE_GOTO
Definition: goto_program.h:50
@ ASSUME
Definition: goto_program.h:33
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:899
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
Author: Diffblue Ltd.
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.
Over-approximative uncaught exceptions analysis.