cprover
Loading...
Searching...
No Matches
uncaught_exceptions_analysis.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Over-approximating uncaught exceptions analysis
4
5Author: Cristina David
6
7\*******************************************************************/
8
11
12#ifdef DEBUG
13#include <iostream>
14#endif
16
17#include <util/namespace.h>
18#include <util/pointer_expr.h>
19#include <util/symbol_table.h>
20
22
26{
27 if(type.base_type().id() == ID_struct_tag)
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 =
78 join(type_id);
79 // we must consider all the subtypes given that
80 // the runtime type is a subtype of the static type
81 std::vector<irep_idt> subtypes =
83 join(subtypes);
84 break;
85 }
86 case CATCH:
87 {
88 if(!instruction.get_code().has_operands())
89 {
90 if(!instruction.targets.empty()) // push
91 {
92 std::set<irep_idt> caught;
93 stack_caught.push_back(caught);
94 std::set<irep_idt> &last_caught=stack_caught.back();
95 const irept::subt &exception_list =
96 instruction.get_code().find(ID_exception_list).get_sub();
97
98 for(const auto &exc : exception_list)
99 {
100 last_caught.insert(exc.id());
101 std::vector<irep_idt> subtypes=
103 last_caught.insert(subtypes.begin(), subtypes.end());
104 }
105 }
106 else // pop
107 {
108 if(!stack_caught.empty())
109 {
110 const std::set<irep_idt> &caught=stack_caught.back();
111 join(caught);
112 // remove the caught exceptions
113 for(const auto &exc_id : caught)
114 thrown.erase(exc_id);
115 stack_caught.pop_back();
116 }
117 }
118 }
119 break;
120 }
121 case FUNCTION_CALL:
122 {
123 const exprt &function_expr = instruction.call_function();
125 function_expr.id()==ID_symbol,
126 "identifier expected to be a symbol");
127 const irep_idt &function_name=
128 to_symbol_expr(function_expr).get_identifier();
129 // use the current information about the callee
130 join(uea.exceptions_map[function_name]);
131 break;
132 }
133 case DECL: // Safe to ignore in this context
134 case DEAD: // Safe to ignore in this context
135 case ASSIGN: // Safe to ignore in this context
136 break;
137 case SET_RETURN_VALUE:
138#if 0
139 DATA_INVARIANT(false, "Returns must be removed before analysis");
140#endif
141 break;
142 case GOTO: // Ignoring the guard is a valid over-approximation
143 case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
144 case ATOMIC_END: // Ignoring is a valid over-approximation
145 case START_THREAD: // Require a concurrent analysis at higher level
146 case END_THREAD: // Require a concurrent analysis at higher level
147 case END_FUNCTION: // No action required
148 case ASSERT: // No action required
149 case ASSUME: // Ignoring is a valid over-approximation
150 case LOCATION: // No action required
151 case SKIP: // No action required
152 break;
153 case OTHER:
154#if 0
155 DATA_INVARIANT(false, "Unclear what is a safe over-approximation of OTHER");
156#endif
157 break;
158 case INCOMPLETE_GOTO:
160 DATA_INVARIANT(false, "Only complete instructions can be analyzed");
161 break;
162 }
163}
164
166const std::set<irep_idt> &uncaught_exceptions_domaint::get_elements() const
167{
168 return thrown;
169}
170
173 const namespacet &ns)
174{
176}
177
180 const goto_functionst &goto_functions,
181 const namespacet &ns)
182{
183 bool change=true;
184
185 while(change)
186 {
187 change=false;
188 // add all the functions to the worklist
189 for(const auto &gf_entry : goto_functions.function_map)
190 {
192 const goto_programt &goto_program = gf_entry.second.body;
193
194 if(goto_program.empty())
195 continue;
196
197 forall_goto_program_instructions(instr_it, goto_program)
198 {
199 domain.transform(instr_it, *this, ns);
200 }
201 // did our estimation for the current function improve?
202 const std::set<irep_idt> &elements=domain.get_elements();
203 if(exceptions_map[gf_entry.first].size() < elements.size())
204 {
205 change=true;
206 exceptions_map[gf_entry.first] = elements;
207 }
208 }
209 }
210}
211
215 const goto_functionst &goto_functions) const
216{
217 (void)goto_functions; // unused parameter
218#ifdef DEBUG
219 for(const auto &gf_entry : goto_functions.function_map)
220 {
221 const auto fn = gf_entry.first;
222 const exceptions_mapt::const_iterator found=exceptions_map.find(fn);
223 // Functions like __CPROVER_assert and __CPROVER_assume are replaced by
224 // explicit GOTO instructions and will not show up in exceptions_map.
225 if(found==exceptions_map.end())
226 continue;
227
228 const auto &fs=found->second;
229 if(!fs.empty())
230 {
231 std::cout << "Uncaught exceptions in function " <<
232 fn << ": " << std::endl;
233 for(const auto exc_id : fs)
234 std::cout << id2string(exc_id) << " ";
235 std::cout << std::endl;
236 }
237 }
238#endif
239}
240
243 const goto_functionst &goto_functions,
244 const namespacet &ns,
245 exceptions_mapt &exceptions)
246{
247 domain(ns);
248 collect_uncaught_exceptions(goto_functions, ns);
249 exceptions=exceptions_map;
250 output(goto_functions);
251}
252
255 const goto_functionst &goto_functions,
256 const namespacet &ns,
257 std::map<irep_idt, std::set<irep_idt>> &exceptions_map)
258{
260 exceptions(goto_functions, ns, exceptions_map);
261}
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.
const codet & get_code() const
Get the code represented by this instruction.
targetst targets
The list of successor instructions.
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
goto_program_instruction_typet type() const
What kind of instruction?
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
bool empty() const
Is the program empty?
const irept & find(const irep_idt &name) const
Definition irep.cpp:106
subt & get_sub()
Definition irep.h:456
const irep_idt & id() const
Definition irep.h:396
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
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
const irep_idt & get_identifier() const
Definition std_expr.h:109
const irep_idt & get_identifier() const
Definition std_types.h:410
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.
const std::set< irep_idt > & get_elements() const
Returns the value of the private member thrown.
static irep_idt get_exception_type(const pointer_typet &)
Returns the compile type of an exception.
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
@ ATOMIC_END
@ DEAD
@ LOCATION
@ END_FUNCTION
@ ASSIGN
@ ASSERT
@ SET_RETURN_VALUE
@ ATOMIC_BEGIN
@ CATCH
@ END_THREAD
@ SKIP
@ NO_INSTRUCTION_TYPE
@ START_THREAD
@ THROW
@ DECL
@ OTHER
@ GOTO
@ INCOMPLETE_GOTO
@ ASSUME
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
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 symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
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.