@@ -13,6 +13,7 @@ Author: Remi Delmas, delmasrd@amazon.com
1313#include < util/pointer_expr.h>
1414#include < util/std_code.h>
1515
16+ #include < analyses/goto_rw.h>
1617#include < goto-instrument/contracts/utils.h>
1718#include < goto-instrument/havoc_utils.h>
1819
@@ -46,23 +47,127 @@ depends_on(const exprt &expr, std::unordered_set<irep_idt> identifiers)
4647 return false ;
4748}
4849
50+ // / Collect identifiers that are local to this loop.
51+ // / A identifier is or is equivalent to a loop local if
52+ // / 1. it is declared inside the loop, or
53+ // / 2. there is no write or read of it outside the loop.
54+ // / 3. it is not used in loop contracts.
55+ std::unordered_set<irep_idt> gen_loop_locals_set (
56+ const irep_idt &function_id,
57+ goto_functiont &goto_function,
58+ const dfcc_loop_nesting_graph_nodet &loop_node,
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+
72+ Forall_goto_program_instructions (i_it, goto_function.body )
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 :
120+ find_symbol_identifiers (get_loop_assigns (latch_target)))
121+ {
122+ if (decl_id == id)
123+ {
124+ is_loop_local = false ;
125+ break ;
126+ }
127+ }
128+
129+ for (const auto &id :
130+ find_symbol_identifiers (get_loop_invariants (latch_target, false )))
131+ {
132+ if (decl_id == id)
133+ {
134+ is_loop_local = false ;
135+ break ;
136+ }
137+ }
138+
139+ for (const auto &id :
140+ find_symbol_identifiers (get_loop_decreases (latch_target, false )))
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+
49157assignst dfcc_infer_loop_assigns (
50158 const local_may_aliast &local_may_alias,
51- const loopt &loop_instructions,
52- const source_locationt &loop_head_location,
159+ goto_functiont &goto_function,
160+ const dfcc_loop_nesting_graph_nodet &loop,
161+ message_handlert &message_handler,
53162 const namespacet &ns)
54163{
55164 // infer
56165 assignst assigns;
57- infer_loop_assigns (local_may_alias, loop_instructions , assigns);
166+ infer_loop_assigns (local_may_alias, loop. instructions , assigns);
58167
59168 // compute locals
60- std::unordered_set<irep_idt> loop_locals;
61- for (const auto &target : loop_instructions)
62- {
63- if (target->is_decl ())
64- loop_locals.insert (target->decl_symbol ().get_identifier ());
65- }
169+ std::unordered_set<irep_idt> loop_locals =
170+ gen_loop_locals_set (irep_idt (), goto_function, loop, message_handler, ns);
66171
67172 // widen or drop targets that depend on loop-locals or are non-constant,
68173 // ie. depend on other locations assigned by the loop.
0 commit comments