CBMC
Loading...
Searching...
No Matches
dfcc_infer_loop_assigns.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking
4
5Author: Remi Delmas, delmasrd@amazon.com
6
7\*******************************************************************/
9
10#include <util/find_symbols.h>
11#include <util/pointer_expr.h>
12
14
15#include <analyses/goto_rw.h>
18
20#include "dfcc_root_object.h"
21
23static exprt
25{
26 const symbolt &object_whole_sym = ns.lookup(CPROVER_PREFIX "object_whole");
30 object_whole_sym.symbol_expr(),
31 {{expr}},
32 object_whole_code_type.return_type(),
33 expr.source_location());
34}
35
38static bool
39depends_on(const exprt &expr, std::unordered_set<irep_idt> identifiers)
40{
41 const std::unordered_set<irep_idt> ids = find_symbol_identifiers(expr);
42 for(const auto &id : ids)
43 {
44 if(identifiers.find(id) != identifiers.end())
45 return true;
46 }
47 return false;
48}
49
55std::unordered_set<irep_idt> gen_loop_locals_set(
56 const irep_idt &function_id,
57 goto_functiont &goto_function,
59 message_handlert &message_handler,
60 const namespacet &ns)
61{
62 std::unordered_set<irep_idt> loop_locals;
63 std::unordered_set<irep_idt> non_loop_locals;
64
65 const auto &loop = loop_node.instructions;
66
67 // All identifiers declared outside the loop.
68 std::unordered_set<irep_idt> non_loop_decls;
69 // Ranges of all read/write outside the loop.
70 rw_range_sett non_loop_rw_range_set(ns, message_handler);
71
73 {
74 // All variables declared in loops are loop locals.
75 if(i_it->is_decl() && loop.contains(i_it))
76 {
77 loop_locals.insert(i_it->decl_symbol().get_identifier());
78 }
79 // Record all other declared variables and their ranges.
80 else if(i_it->is_decl())
81 {
82 non_loop_decls.insert(i_it->decl_symbol().get_identifier());
83 }
84 // Record all writing/reading outside the loop.
85 else if(
86 (i_it->is_assign() || i_it->is_function_call()) && !loop.contains(i_it))
87 {
88 goto_rw(function_id, i_it, non_loop_rw_range_set);
89 }
90 }
91
92 // Check if declared variables are loop locals.
93 for(const auto &decl_id : non_loop_decls)
94 {
95 bool is_loop_local = true;
96 // No write to the declared variable.
97 for(const auto &writing_rw : non_loop_rw_range_set.get_w_set())
98 {
99 if(decl_id == writing_rw.first)
100 {
101 is_loop_local = false;
102 break;
103 }
104 }
105
106 // No read to the declared variable.
107 for(const auto &writing_rw : non_loop_rw_range_set.get_r_set())
108 {
109 if(decl_id == writing_rw.first)
110 {
111 is_loop_local = false;
112 break;
113 }
114 }
115
116 const auto latch_target = loop_node.latch;
117
118 // Loop locals are not used in loop contracts.
119 for(const auto &id :
121 {
122 if(decl_id == id)
123 {
124 is_loop_local = false;
125 break;
126 }
127 }
128
129 for(const auto &id :
131 {
132 if(decl_id == id)
133 {
134 is_loop_local = false;
135 break;
136 }
137 }
138
139 for(const auto &id :
141 {
142 if(decl_id == id)
143 {
144 is_loop_local = false;
145 break;
146 }
147 }
148
149 // Collect all loop locals.
150 if(is_loop_local)
151 loop_locals.insert(decl_id);
152 }
153
154 return loop_locals;
155}
156
158static std::unordered_set<irep_idt>
160{
161 std::unordered_set<irep_idt> identifiers;
162 for(const auto &instruction : src.instructions)
163 {
164 // compute forward edges first
165 switch(instruction.type())
166 {
167 case ASSERT:
168 case ASSUME:
169 case GOTO:
170 find_symbols(instruction.condition(), identifiers);
171 break;
172
173 case FUNCTION_CALL:
174 find_symbols(instruction.call_lhs(), identifiers);
175 for(const auto &e : instruction.call_arguments())
176 find_symbols(e, identifiers);
177 break;
178 case ASSIGN:
179 case OTHER:
180
181 case SET_RETURN_VALUE:
182 case DECL:
183 case DEAD:
184 for(const auto &e : instruction.code().operands())
185 {
186 find_symbols(e, identifiers);
187 }
188 break;
189
190 case END_THREAD:
191 case END_FUNCTION:
192 case ATOMIC_BEGIN:
193 case ATOMIC_END:
194 case SKIP:
195 case LOCATION:
196 case CATCH:
197 case THROW:
198 case START_THREAD:
199 break;
201 case INCOMPLETE_GOTO:
203 break;
204 }
205 }
206 return identifiers;
207}
208
214 const local_may_aliast &local_may_alias,
215 goto_functiont &goto_function,
217 const std::unordered_set<irep_idt> &candidate_targets,
218 message_handlert &message_handler,
219 const namespacet &ns)
220{
221 // infer
222 assignst assigns;
223 infer_loop_assigns(local_may_alias, loop.instructions, assigns);
224
225 // compute locals
226 std::unordered_set<irep_idt> loop_locals =
227 gen_loop_locals_set(irep_idt(), goto_function, loop, message_handler, ns);
228
229 // widen or drop targets that depend on loop-locals or are non-constant,
230 // ie. depend on other locations assigned by the loop.
231 // e.g: if the loop assigns {i, a[i]}, then a[i] is non-constant.
233 assignst result;
234 for(const auto &expr : assigns)
235 {
236 // Skip targets that only depend on non-visible identifiers.
237 if(!depends_on(expr, candidate_targets))
238 {
239 continue;
240 }
241
242 if(depends_on(expr, loop_locals))
243 {
244 // Target depends on loop locals, attempt widening to the root object
245 auto root_objects = dfcc_root_objects(expr);
246 for(const auto &root_object : root_objects)
247 {
248 if(!depends_on(root_object, loop_locals))
249 {
251 address_of_root_object.add_source_location() =
252 root_object.source_location();
253 result.emplace(
255 }
256 }
257 }
258 else
259 {
261 address_of_expr.add_source_location() = expr.source_location();
262 // Widen assigns targets to object_whole if `expr` is a dereference or
263 // with constant address.
264 if(expr.id() == ID_dereference || !is_constant(address_of_expr))
265 {
266 // Target address is not constant, widening to the whole object
267 result.emplace(make_object_whole_call_expr(address_of_expr, ns));
268 }
269 else
270 {
271 result.emplace(expr);
272 }
273 }
274 }
275
276 return result;
277}
278
282{
284 {
285 if(i_it->is_assign())
286 {
287 auto &lhs = i_it->assign_lhs();
288
289 if(
290 lhs.id() == ID_symbol &&
291 to_symbol_expr(lhs).get_identifier() == CPROVER_PREFIX "dead_object")
292 {
293 i_it->turn_into_skip();
294 }
295 }
296 }
297}
298
300 std::map<std::size_t, assignst> &inferred_loop_assigns_map,
301 goto_functionst &goto_functions,
302 const goto_functiont &goto_function,
303 message_handlert &message_handler,
304 const namespacet &ns)
305{
306 messaget log(message_handler);
307
308 // Collect all candidate targets---identifiers visible in `goto_function`.
309 const auto candidate_targets = find_symbol_identifiers(goto_function.body);
310
311 // We infer loop assigns based on the copy of `goto_function`.
313 goto_function_copy.copy_from(goto_function);
314
315 // Build the loop id map before inlining attempt. So that we can later
316 // distinguish loops in the original body and loops added by inlining.
317 const auto loop_nesting_graph =
319 auto topsorted = loop_nesting_graph.topsort();
320 // skip function without loop.
321 if(topsorted.empty())
322 return;
323
324 // Map from targett in `goto_function_copy` to loop number.
325 std::
326 unordered_map<goto_programt::const_targett, std::size_t, const_target_hash>
328
329 for(const auto id : topsorted)
330 {
331 loop_number_map.emplace(
332 loop_nesting_graph[id].head, loop_nesting_graph[id].latch->loop_number);
333 }
334
335 // We avoid inlining `malloc` and `free` whose variables are not assigns.
336 auto malloc_body = goto_functions.function_map.extract(irep_idt("malloc"));
337 auto free_body = goto_functions.function_map.extract(irep_idt("free"));
338
339 // Inline all function calls in goto_function_copy; this is best-effort
340 // inlining, we can safely ignore warnings here.
343 goto_functions, goto_function_copy.body, ns, null_message_handler);
344 // Update the body to make sure all goto correctly jump to valid targets.
345 goto_function_copy.body.update();
346 // Build the loop graph after inlining.
347 const auto inlined_loop_nesting_graph =
349
350 // Alias analysis.
352 local_may_aliast local_may_alias(goto_function_copy);
353
355
356 for(const auto inlined_id : inlined_topsorted)
357 {
358 // We only infer loop assigns for loops in the original function.
359 if(
361 loop_number_map.end())
362 {
363 const auto loop_number =
366
368 local_may_alias,
372 message_handler,
373 ns);
374 }
375 }
376 // Restore the function boyd of `malloc` and `free`.
377 goto_functions.function_map.insert(std::move(malloc_body));
378 goto_functions.function_map.insert(std::move(free_body));
379}
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base type of functions.
Definition std_types.h:583
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
A collection of goto functions.
function_mapt function_map
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_programt body
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
A class containing utility functions for havocing expressions.
Definition havoc_utils.h:28
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
A side_effect_exprt representation of a function call side effect.
Definition std_code.h:1692
Symbol table entry.
Definition symbol.h:28
#define CPROVER_PREFIX
std::unordered_set< irep_idt > gen_loop_locals_set(const irep_idt &function_id, goto_functiont &goto_function, const dfcc_loop_nesting_graph_nodet &loop_node, message_handlert &message_handler, const namespacet &ns)
Collect identifiers that are local to this loop.
static assignst dfcc_infer_loop_assigns_for_loop(const local_may_aliast &local_may_alias, goto_functiont &goto_function, const dfcc_loop_nesting_graph_nodet &loop, const std::unordered_set< irep_idt > &candidate_targets, message_handlert &message_handler, const namespacet &ns)
Infer loop assigns in the given loop.
static std::unordered_set< irep_idt > find_symbol_identifiers(const goto_programt &src)
Find all identifiers in src.
static exprt make_object_whole_call_expr(const exprt &expr, const namespacet &ns)
Builds a call expression object_whole(expr)
static void remove_dead_object_assignment(goto_functiont &goto_function)
Remove assignments to __CPROVER_dead_object to avoid aliasing all targets that are assigned to __CPRO...
void dfcc_infer_loop_assigns_for_function(std::map< std::size_t, assignst > &inferred_loop_assigns_map, goto_functionst &goto_functions, const goto_functiont &goto_function, message_handlert &message_handler, const namespacet &ns)
Infer assigns clause targets for loops in goto_function from their instructions and an alias analysis...
static bool depends_on(const exprt &expr, std::unordered_set< irep_idt > identifiers)
Returns true iff expr contains at least one identifier found in identifiers.
Infer a set of assigns clause targets for a natural loop.
dfcc_loop_nesting_grapht build_loop_nesting_graph(goto_programt &goto_program)
Builds a graph instance describing the nesting structure of natural loops in the given goto_program.
Builds a graph describing how loops are nested in a GOTO program.
std::unordered_set< exprt, irep_hash > dfcc_root_objects(const exprt &expr)
Computes a set of root object expressions from an lvalue or assigns clause target expression.
Utility functions that compute root object expressions for assigns clause targets and LHS expressions...
static bool find_symbols(symbol_kindt, const typet &, std::function< bool(const symbol_exprt &)>, std::unordered_set< irep_idt > &bindings, const std::vector< irep_idt > &subs_to_find)
Find identifiers with id ID_symbol of the sub expressions and the subs with ID in subs_to_find consid...
void goto_program_inline(goto_functionst &goto_functions, goto_programt &goto_program, const namespacet &ns, message_handlert &message_handler, bool adjust_function, bool caching)
Transitively inline all function calls found in a particular program.
Function Inlining This gives a number of different interfaces to the function inlining functionality ...
#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
static void goto_rw(const irep_idt &function, goto_programt::const_targett target, const exprt &lhs, const exprt &function_expr, const exprt::operandst &arguments, rw_range_sett &rw_set)
Definition goto_rw.cpp:845
std::set< exprt > assignst
Definition havoc_utils.h:24
Field-insensitive, location-sensitive may-alias analysis.
double log(double x)
Definition math.c:2449
API to expression classes for Pointers.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition std_types.h:29
A graph node that stores information about a natural loop.
loop_templatet< goto_programt::targett, goto_programt::target_less_than > instructions
Set of loop instructions.
null_message_handlert null_message_handler
Definition message.cpp:14
void infer_loop_assigns(const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns)
Infer loop assigns using alias analysis result local_may_alias.
Definition utils.cpp:344
exprt get_loop_assigns(const goto_programt::const_targett &loop_end)
Extract loop assigns from annotated loop end.
Definition utils.cpp:683
exprt get_loop_invariants(const goto_programt::const_targett &loop_end, const bool check_side_effect)
Extract loop invariants from annotated loop end.
Definition utils.cpp:666
exprt get_loop_decreases(const goto_programt::const_targett &loop_end, const bool check_side_effect)
Extract loop decreases from annotated loop end.
Definition utils.cpp:688
dstringt irep_idt