Skip to content

Commit fd6c193

Browse files
committed
GOTO conversion: Declaration hops must not invalidate incomplete gotos
Declaration hops are built as part of finish_gotos, and must not invalidate goto-instructions that are yet to be finished. To accomplish this, collect all instructions that are to be inserted and do the insertion after having finished all gotos. Bug was observed when invoking CBMC from Kani.
1 parent 50bfa4e commit fd6c193

File tree

2 files changed

+34
-12
lines changed

2 files changed

+34
-12
lines changed

src/ansi-c/goto-conversion/goto_convert.cpp

Lines changed: 30 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -103,13 +103,14 @@ struct build_declaration_hops_inputst
103103
node_indext end_scope_index = 0;
104104
};
105105

106-
void goto_convertt::build_declaration_hops(
106+
goto_convertt::declaration_hop_instrumentationt
107+
goto_convertt::build_declaration_hops(
107108
goto_programt &program,
108109
std::unordered_map<irep_idt, symbolt, irep_id_hash> &label_flags,
109110
const build_declaration_hops_inputst &inputs)
110111
{
111112
// In the case of a goto jumping into a scope, the declarations (but not the
112-
// initialisations) need to be executed. This function performs a
113+
// initialisations) need to be executed. This function prepares a
113114
// transformation from code that looks like -
114115
// {
115116
// statement_block_a();
@@ -150,9 +151,14 @@ void goto_convertt::build_declaration_hops(
150151
// __CPROVER_going_to::user_label = false;
151152
// statement_block_e();
152153
// }
154+
//
155+
// The actual insertion of instructions needs to be performed by the caller,
156+
// which needs to use the result of this method.
153157

154158
PRECONDITION(inputs.label_scope_index != inputs.end_scope_index);
155159

160+
declaration_hop_instrumentationt instructions_to_add;
161+
156162
const auto flag = [&]() -> symbolt {
157163
const auto existing_flag = label_flags.find(inputs.label);
158164
if(existing_flag != label_flags.end())
@@ -170,19 +176,20 @@ void goto_convertt::build_declaration_hops(
170176
label_flags.emplace(inputs.label, new_flag);
171177

172178
// Create and initialise flag.
173-
goto_programt flag_creation;
174-
flag_creation.instructions.push_back(
179+
instructions_to_add.emplace_back(
180+
program.instructions.begin(),
175181
goto_programt::make_decl(new_flag.symbol_expr(), label_location));
176182
const auto make_clear_flag = [&]() -> goto_programt::instructiont {
177183
return goto_programt::make_assignment(
178184
new_flag.symbol_expr(), false_exprt{}, label_location);
179185
};
180-
flag_creation.instructions.push_back(make_clear_flag());
181-
program.destructive_insert(program.instructions.begin(), flag_creation);
186+
instructions_to_add.emplace_back(
187+
program.instructions.begin(), make_clear_flag());
182188

183189
// Clear flag on arrival at label.
184190
auto clear_on_arrival = make_clear_flag();
185-
program.insert_before_swap(inputs.label_instruction, clear_on_arrival);
191+
instructions_to_add.emplace_back(
192+
inputs.label_instruction, clear_on_arrival);
186193
return new_flag;
187194
}();
188195

@@ -193,9 +200,7 @@ void goto_convertt::build_declaration_hops(
193200
goto_location.set_hide();
194201
auto set_flag = goto_programt::make_assignment(
195202
flag.symbol_expr(), true_exprt{}, goto_location);
196-
program.insert_before_swap(goto_instruction, set_flag);
197-
// Keep this iterator referring to the goto instruction, not the assignment.
198-
++goto_instruction;
203+
instructions_to_add.emplace_back(goto_instruction, set_flag);
199204
}
200205

201206
auto target = inputs.label_instruction;
@@ -216,6 +221,8 @@ void goto_convertt::build_declaration_hops(
216221
declaration_location.set_hide();
217222
auto if_goto = goto_programt::make_goto(
218223
target, flag.symbol_expr(), declaration_location);
224+
// this isn't changing any previously existing instruction so we insert
225+
// directly rather than going through instructions_to_add
219226
program.instructions.insert(
220227
std::next(declaration->instruction), std::move(if_goto));
221228
declaration->accounted_flags.insert(flag.name);
@@ -226,6 +233,8 @@ void goto_convertt::build_declaration_hops(
226233
// Update the goto so that it goes to the first declaration rather than its
227234
// original/final destination.
228235
goto_instruction->set_target(target);
236+
237+
return instructions_to_add;
229238
}
230239

231240
/******************************************************************* \
@@ -243,6 +252,7 @@ Function: goto_convertt::finish_gotos
243252
void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
244253
{
245254
std::unordered_map<irep_idt, symbolt, irep_id_hash> label_flags;
255+
declaration_hop_instrumentationt instructions_to_insert;
246256

247257
for(const auto &g_it : targets.gotos)
248258
{
@@ -331,7 +341,9 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
331341
inputs.label_instruction = l_it->second.first;
332342
inputs.label_scope_index = label_target;
333343
inputs.end_scope_index = intersection_result.common_ancestor;
334-
build_declaration_hops(dest, label_flags, inputs);
344+
instructions_to_insert.splice(
345+
instructions_to_insert.end(),
346+
build_declaration_hops(dest, label_flags, inputs));
335347
}
336348
}
337349
else
@@ -340,6 +352,13 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
340352
}
341353
}
342354

355+
for(auto r_it = instructions_to_insert.rbegin();
356+
r_it != instructions_to_insert.rend();
357+
++r_it)
358+
{
359+
dest.insert_before_swap(r_it->first, r_it->second);
360+
}
361+
343362
targets.gotos.clear();
344363
}
345364

src/ansi-c/goto-conversion/goto_convert_class.h

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -354,7 +354,10 @@ class goto_convertt : public messaget
354354
std::optional<node_indext> destructor_end_point = {},
355355
std::optional<node_indext> destructor_start_point = {});
356356

357-
void build_declaration_hops(
357+
typedef std::list<
358+
std::pair<goto_programt::targett, goto_programt::instructiont>>
359+
declaration_hop_instrumentationt;
360+
[[nodiscard]] declaration_hop_instrumentationt build_declaration_hops(
358361
goto_programt &dest,
359362
std::unordered_map<irep_idt, symbolt, irep_id_hash> &label_flags,
360363
const build_declaration_hops_inputst &inputs);

0 commit comments

Comments
 (0)