1/*******************************************************************\
3Module: Dynamic frame condition checking
5Author: Remi Delmas, delmasrd@amazon.com
7\*******************************************************************/
33 expr.source_location());
42 for(
const auto &
id :
ids)
44 if(identifiers.find(
id) != identifiers.end())
65 const auto &loop =
loop_node.instructions;
67 // All identifiers declared outside the loop.
69 // Ranges of all read/write outside the loop.
74 // All variables declared in loops are loop locals.
75 if(
i_it->is_decl() && loop.contains(
i_it))
79 // Record all other declared variables and their ranges.
80 else if(
i_it->is_decl())
84 // Record all writing/reading outside the loop.
86 (
i_it->is_assign() ||
i_it->is_function_call()) && !loop.contains(
i_it))
92 // Check if declared variables are loop locals.
96 // No write to the declared variable.
106 // No read to the declared variable.
118 // Loop locals are not used in loop contracts.
149 // Collect all loop locals.
158static std::unordered_set<irep_idt>
161 std::unordered_set<irep_idt> identifiers;
164 // compute forward edges first
165 switch(instruction.type())
175 for(
const auto &e : instruction.call_arguments())
184 for(
const auto &e : instruction.code().operands())
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.
234 for(
const auto &expr : assigns)
236 // Skip targets that only depend on non-visible identifiers.
244 // Target depends on loop locals, attempt widening to the root object
252 root_object.source_location();
262 // Widen assigns targets to object_whole if `expr` is a dereference or
263 // with constant address.
266 // Target address is not constant, widening to the whole object
271 result.emplace(expr);
285 if(
i_it->is_assign())
287 auto &lhs =
i_it->assign_lhs();
293 i_it->turn_into_skip();
308 // Collect all candidate targets---identifiers visible in `goto_function`.
311 // We infer loop assigns based on the copy of `goto_function`.
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.
320 // skip function without loop.
324 // Map from targett in `goto_function_copy` to loop number.
326 unordered_map<goto_programt::const_targett, std::size_t, const_target_hash>
335 // We avoid inlining `malloc` and `free` whose variables are not assigns.
339 // Inline all function calls in goto_function_copy; this is best-effort
340 // inlining, we can safely ignore warnings here.
344 // Update the body to make sure all goto correctly jump to valid targets.
346 // Build the loop graph after inlining.
358 // We only infer loop assigns for loops in the original function.
363 const auto loop_number =
376 // Restore the function boyd of `malloc` and `free`.
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
A collection of goto functions.
function_mapt function_map
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
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.
Class that provides messages with a built-in verbosity 'level'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
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.
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)
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)
std::set< exprt > assignst
Field-insensitive, location-sensitive may-alias analysis.
API to expression classes for Pointers.
#define UNREACHABLE
This should be used to mark dead code.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
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
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.
exprt get_loop_assigns(const goto_programt::const_targett &loop_end)
Extract loop assigns from annotated loop end.
exprt get_loop_invariants(const goto_programt::const_targett &loop_end, const bool check_side_effect)
Extract loop invariants from annotated loop end.
exprt get_loop_decreases(const goto_programt::const_targett &loop_end, const bool check_side_effect)
Extract loop decreases from annotated loop end.