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.has_operands())
32  return get_exception_symbol(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  default:
129  {}
130  }
131 }
132 
134 const std::set<irep_idt> &uncaught_exceptions_domaint::get_elements() const
135 {
136  return thrown;
137 }
138 
141  const namespacet &ns)
142 {
144 }
145 
148  const goto_functionst &goto_functions,
149  const namespacet &ns)
150 {
151  bool change=true;
152 
153  while(change)
154  {
155  change=false;
156  // add all the functions to the worklist
157  forall_goto_functions(current_function, goto_functions)
158  {
159  domain.make_top();
160  const goto_programt &goto_program=current_function->second.body;
161 
162  if(goto_program.empty())
163  continue;
164 
165  forall_goto_program_instructions(instr_it, goto_program)
166  {
167  domain.transform(instr_it, *this, ns);
168  }
169  // did our estimation for the current function improve?
170  const std::set<irep_idt> &elements=domain.get_elements();
171  if(exceptions_map[current_function->first].size()<elements.size())
172  {
173  change=true;
174  exceptions_map[current_function->first]=elements;
175  }
176  }
177  }
178 }
179 
183  const goto_functionst &goto_functions) const
184 {
185  (void)goto_functions; // unused parameter
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 }
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:479
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:35
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
typet::subtype
const typet & subtype() const
Definition: type.h:38
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:485
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:210
typet
The type of an expression, extends irept.
Definition: type.h:27
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:182
goto_programt::instructiont::type
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:190
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:134
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
goto_programt::empty
bool empty() const
Is the program empty?
Definition: goto_program.h:626
exprt
Base class for all expressions.
Definition: expr.h:54
exprt::op0
exprt & op0()
Definition: expr.h:84
goto_programt::instructiont::targets
targetst targets
The list of successor instructions.
Definition: goto_program.h:203
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:147
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:93
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
THROW
@ THROW
Definition: goto_program.h:50
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:75
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
Definition: goto_program.h:181
uncaught_exceptions_domaint::join
void join(const irep_idt &)
The join operator for the uncaught exceptions domain.
Definition: uncaught_exceptions_analysis.cpp:38
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
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
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
irept::id
const irep_idt & id() const
Definition: irep.h:259
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:543
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
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
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
uncaught_exceptions_analysist::domain
uncaught_exceptions_domaint domain
Definition: uncaught_exceptions_analysis.h:77
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
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:222
namespacet::get_symbol_table
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:126
CATCH
@ CATCH
Definition: goto_program.h:51
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:140
uncaught_exceptions_analysis.h
irept::get_sub
subt & get_sub()
Definition: irep.h:317
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:72
uncaught_exceptions_analysist
computes in exceptions_map an overapproximation of the exceptions thrown by each method
Definition: uncaught_exceptions_analysis.h:58
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:149
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
irept::subt
std::vector< irept > subt
Definition: irep.h:160
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
code_function_callt::function
exprt & function()
Definition: std_code.h:1099
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
class_hierarchyt::get_children_trans
idst get_children_trans(const irep_idt &id) const
Definition: class_hierarchy.h:68