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