cprover
Loading...
Searching...
No Matches
dfcc_instrument_loop.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking for loop contracts
4
5Author: Qinheping Hu, qinhh@amazon.com
6
7Author: Remi Delmas, delmasrd@amazon.com
8
9Date: April 2023
10
11\*******************************************************************/
12
15
16#include <util/format_expr.h>
17#include <util/fresh_symbol.h>
18
20
21#include "dfcc_cfg_info.h"
23#include "dfcc_instrument.h"
24#include "dfcc_loop_tags.h"
25#include "dfcc_spec_functions.h"
26
41
43 const std::size_t loop_id,
44 const irep_idt &function_id,
45 goto_functiont &goto_function,
46 dfcc_cfg_infot &cfg_info,
47 const std::set<symbol_exprt> &local_statics,
48 std::set<irep_idt> &function_pointer_contracts)
49{
50 const dfcc_loop_infot &loop = cfg_info.get_loop_info(loop_id);
51 const std::size_t cbmc_loop_id = loop.cbmc_loop_id;
52 const exprt &outer_write_set = cfg_info.get_outer_write_set(loop_id);
53 goto_programt::targett head = loop.find_head(goto_function.body).value();
54 auto head_location(head->source_location());
55
56 auto &symbol_table = goto_model.symbol_table;
57
58 // Temporary variables:
59 // Create a temporary to track if we entered the loop,
60 // i.e., the loop guard was satisfied.
61 const auto entered_loop = dfcc_utilst::create_symbol(
62 symbol_table,
63 bool_typet(),
64 function_id,
65 std::string(ENTERED_LOOP) + "__" + std::to_string(cbmc_loop_id),
66 head_location);
67
68 // Create a snapshot of the invariant so that we can check the base case,
69 // if the loop is not vacuous and must be abstracted with contracts.
70 const auto initial_invariant = dfcc_utilst::create_symbol(
71 symbol_table, bool_typet(), function_id, INIT_INVARIANT, head_location);
72
73 // Create a temporary variable to track base case vs inductive case
74 // instrumentation of the loop.
75 const auto in_base_case = dfcc_utilst::create_symbol(
76 symbol_table, bool_typet(), function_id, IN_BASE_CASE, head_location);
77
78 // Temporary variables for storing the multidimensional decreases clause
79 // at the start of and end of a loop body.
80 exprt::operandst decreases_clauses = loop.decreases;
81 std::vector<symbol_exprt> old_decreases_vars, new_decreases_vars;
82 for(const auto &clause : decreases_clauses)
83 {
84 // old
85 const auto old_decreases_var = dfcc_utilst::create_symbol(
86 symbol_table, clause.type(), function_id, "tmp_cc", head_location);
87 old_decreases_vars.push_back(old_decreases_var);
88 // new
89 const auto new_decreases_var = dfcc_utilst::create_symbol(
90 symbol_table, clause.type(), function_id, "tmp_cc", head_location);
91 new_decreases_vars.push_back(new_decreases_var);
92 }
93
94 // Convert the assigns clause to the required type.
95 exprt::operandst assigns(loop.assigns.begin(), loop.assigns.end());
96
97 // Add local statics to the assigns clause.
98 for(auto &local_static : local_statics)
99 {
100 assigns.push_back(local_static);
101 }
102
103 auto nof_targets = assigns.size();
104 max_assigns_clause_size = std::max(nof_targets, max_assigns_clause_size);
105
106 // populate(w_loop, <loop_assigns>);
107 // Construct the write set from loop assigns target. That is, contract_assigns
108 // in the result __CPROVER_contracts_write_set_t should be the set of CAR
109 // of the loop assign targets.
110 goto_programt write_set_populate_instrs;
111 const irep_idt &language_mode =
112 dfcc_utilst::get_function_symbol(symbol_table, function_id).mode;
113 contract_clauses_codegen.gen_spec_assigns_instructions(
114 language_mode, assigns, write_set_populate_instrs);
115
116 // havoc(w_loop);
117 // The generated GOTO instructions havoc the write set of the loop.
118 goto_programt havoc_instrs;
119
120 spec_functions.generate_havoc_instructions(
121 function_id,
122 write_set_populate_instrs,
125 havoc_instrs,
126 nof_targets);
127 spec_functions.to_spec_assigns_instructions(
129 language_mode,
130 write_set_populate_instrs,
131 nof_targets);
132
133 // ---------- Add instrumented instructions ----------
134 goto_programt::targett loop_latch =
135 loop.find_latch(goto_function.body).value();
136 exprt invariant(loop.invariant);
137 const auto history_var_map = add_prehead_instructions(
138 loop_id,
139 goto_function,
140 symbol_table,
141 head,
142 loop_latch,
143 write_set_populate_instrs,
144 invariant,
145 assigns,
146 loop.write_set_var,
148 entered_loop,
149 initial_invariant,
150 in_base_case,
151 language_mode);
152
153 const auto step_target = add_step_instructions(
154 loop_id,
155 cbmc_loop_id,
156 function_id,
157 goto_function,
158 symbol_table,
159 head,
160 loop_latch,
161 havoc_instrs,
162 invariant,
163 decreases_clauses,
165 outer_write_set,
166 initial_invariant,
167 in_base_case,
168 old_decreases_vars);
169
171 loop_id,
172 cbmc_loop_id,
173 goto_function,
174 symbol_table,
175 head,
176 loop_latch,
177 invariant,
178 decreases_clauses,
179 entered_loop,
180 in_base_case,
181 old_decreases_vars,
182 new_decreases_vars,
183 step_target,
184 language_mode);
185
187 loop_id,
188 cbmc_loop_id,
189 goto_function,
190 head,
191 loop.write_set_var,
193 history_var_map,
194 entered_loop,
195 initial_invariant,
196 in_base_case,
197 old_decreases_vars,
198 new_decreases_vars);
199
200 goto_function.body.update();
201}
202
203std::unordered_map<exprt, symbol_exprt, irep_hash>
205 const std::size_t loop_id,
206 goto_functionst::goto_functiont &goto_function,
207 symbol_table_baset &symbol_table,
208 goto_programt::targett loop_head,
209 goto_programt::targett loop_latch,
210 goto_programt &assigns_instrs,
211 exprt &invariant,
212 const exprt::operandst &assigns,
213 const symbol_exprt &loop_write_set,
214 const symbol_exprt &addr_of_loop_write_set,
215 const symbol_exprt &entered_loop,
216 const symbol_exprt &initial_invariant,
217 const symbol_exprt &in_base_case,
218 const irep_idt &language_mode)
219{
220 auto loop_head_location(loop_head->source_location());
221 dfcc_remove_loop_tags(loop_head_location);
222
223 // ```
224 // ... preamble ...
225 //
226 // // Prehead block: Declare & initialize instrumentation variables
227 // snapshot loop_entry history vars;
228 // entered_loop = false
229 // initial_invariant = loop_invariant;
230 // in_base_case = true;
231 // __ws_loop;
232 // ws_loop := address_of(__ws_loop);
233 // __write_set_create(ws_loop);
234 // __write_set_add(ws_loop, loop_assigns);
235 // __write_set_add(ws_loop, local_statics);
236 // GOTO HEAD;
237 // ```
238
239 // initialize loop_entry history vars;
240 auto replace_history_result = replace_history_loop_entry(
241 symbol_table, invariant, loop_head_location, language_mode);
242 invariant.swap(replace_history_result.expression_after_replacement);
243 goto_programt &pre_loop_head_instrs =
244 replace_history_result.history_construction;
245
246 // entered_loop = false
247 {
248 pre_loop_head_instrs.add(
249 goto_programt::make_decl(entered_loop, loop_head_location));
250 pre_loop_head_instrs.add(goto_programt::make_assignment(
251 entered_loop, false_exprt{}, loop_head_location));
252 }
253
254 // initial_invariant = <loop_invariant>;
255 {
256 // Create a snapshot of the invariant so that we can check the base case,
257 // if the loop is not vacuous and must be abstracted with contracts.
258 pre_loop_head_instrs.add(
259 goto_programt::make_decl(initial_invariant, loop_head_location));
260
261 // Although the invariant at this point will not have side effects,
262 // it is still a C expression, and needs to be "goto_convert"ed.
263 // Note that this conversion may emit many GOTO instructions.
264 code_frontend_assignt initial_invariant_assignment{
265 initial_invariant, invariant, loop_head_location};
266 goto_convertt converter(symbol_table, log.get_message_handler());
267 converter.goto_convert(
268 initial_invariant_assignment, pre_loop_head_instrs, language_mode);
269 }
270
271 {
272 // Create a temporary variable to track base case vs inductive case
273 // instrumentation of the loop.
274 // in_base_case = true;
275 pre_loop_head_instrs.add(
276 goto_programt::make_decl(in_base_case, loop_head_location));
277 pre_loop_head_instrs.add(goto_programt::make_assignment(
278 in_base_case, true_exprt{}, loop_head_location));
279 }
280
281 {
282 // Create and populate the write set.
283 // DECL loop_write_set
284 // DECL addr_of_loop_write_set
285 // ASSIGN write_set_ptr := address_of(write_set)
286 // CALL __CPROVER_contracts_write_set_create(write_set_ptr,
287 // contracts_assigns_size, contracts_assigns_frees_size,
288 // assume_require_ctx, assert_require_ctx, assume_ensures_ctx,
289 // assert_ensures_ctx, allow_allocate, allow_deallocate);
290 pre_loop_head_instrs.add(
291 goto_programt::make_decl(loop_write_set, loop_head_location));
292 pre_loop_head_instrs.add(
293 goto_programt::make_decl(addr_of_loop_write_set, loop_head_location));
294 pre_loop_head_instrs.add(goto_programt::make_assignment(
295 addr_of_loop_write_set,
296 address_of_exprt(loop_write_set),
297 loop_head_location));
298
299 code_function_callt call = library.write_set_create_call(
300 addr_of_loop_write_set,
301 from_integer(assigns.size(), size_type()),
302 loop_head_location);
303 pre_loop_head_instrs.add(
304 goto_programt::make_function_call(call, loop_head_location));
305
306 pre_loop_head_instrs.destructive_append(assigns_instrs);
307 }
308
309 // goto HEAD;
310 pre_loop_head_instrs.add(
311 goto_programt::make_goto(loop_head, true_exprt{}, loop_head_location));
312
313 goto_function.body.destructive_insert(loop_head, pre_loop_head_instrs);
314 return replace_history_result.parameter_to_history;
315}
316
319 const std::size_t loop_id,
320 const std::size_t cbmc_loop_id,
321 const irep_idt &function_id,
322 goto_functionst::goto_functiont &goto_function,
323 symbol_table_baset &symbol_table,
324 goto_programt::targett loop_head,
325 goto_programt::targett loop_latch,
326 goto_programt &havoc_instrs,
327 exprt &invariant,
328 const exprt::operandst &decreases_clauses,
329 const symbol_exprt &addr_of_loop_write_set,
330 const exprt &outer_write_set,
331 const symbol_exprt &initial_invariant,
332 const symbol_exprt &in_base_case,
333 const std::vector<symbol_exprt> &old_decreases_vars)
334{
335 auto loop_head_location(loop_head->source_location());
336 dfcc_remove_loop_tags(loop_head_location);
337
338 // ```
339 // STEP: // Loop step block: havoc the loop state
340 // ASSERT(initial_invariant);
341 // __write_set_check_inclusion(ws_loop, ws_parent);
342 // in_base_case = false;
343 // in_loop_havoc_block = true;
344 // havoc(assigns_clause_targets);
345 // in_loop_havoc_block = false;
346 // ASSUME(loop_invariant);
347 // old_variant = loop_decreases;
348 // ```
349
350 goto_programt step_instrs;
351
352 // We skip past it initially, because of the unconditional jump above,
353 // but jump back here if we get past the loop guard while in_base_case.
354 // `in_base_case = false;`
355 goto_programt::instructiont::targett step_case_target =
357 in_base_case, false_exprt{}, loop_head_location));
358
359 {
360 // If we jump here, then the loop runs at least once,
361 // so add the base case assertion: `assert(initial_invariant)`.
362 source_locationt check_location(loop_head_location);
363 check_location.set_property_class("loop_invariant_base");
364 check_location.set_comment(
365 "Check invariant before entry for loop " +
366 id2string(check_location.get_function()) + "." +
367 std::to_string(cbmc_loop_id));
368 step_instrs.add(
369 goto_programt::make_assertion(initial_invariant, check_location));
370 }
371
372 {
373 // Check assigns clause inclusion with parent write set
374 // skip the check when if w_parent is NULL.
375 auto goto_instruction = step_instrs.add(goto_programt::make_incomplete_goto(
377 outer_write_set,
378 null_pointer_exprt(to_pointer_type(outer_write_set.type()))),
379 loop_head_location));
380
381 const auto check_var = dfcc_utilst::create_symbol(
382 symbol_table,
383 bool_typet(),
384 function_id,
385 "__check_assigns_clause_incl_loop_" + std::to_string(cbmc_loop_id),
386 loop_head_location);
387
388 step_instrs.add(goto_programt::make_decl(check_var, loop_head_location));
390 library.write_set_check_assigns_clause_inclusion_call(
391 check_var, outer_write_set, addr_of_loop_write_set, loop_head_location),
392 loop_head_location));
393
394 source_locationt check_location(loop_head_location);
395 check_location.set_property_class("loop_assigns");
396 check_location.set_comment(
397 "Check assigns clause inclusion for loop " +
398 id2string(check_location.get_function()) + "." +
399 std::to_string(cbmc_loop_id));
400 step_instrs.add(goto_programt::make_assertion(check_var, check_location));
401 step_instrs.add(goto_programt::make_dead(check_var, loop_head_location));
402
403 auto label_instruction =
404 step_instrs.add(goto_programt::make_skip(loop_head_location));
405 goto_instruction->complete_goto(label_instruction);
406 }
407
408 {
409 // Generate havocing code for assigns targets.
410 const auto in_loop_havoc_block = dfcc_utilst::create_symbol(
411 symbol_table,
412 bool_typet(),
413 function_id,
414 std::string(IN_LOOP_HAVOC_BLOCK) + +"__" + std::to_string(cbmc_loop_id),
415 loop_head_location);
416 step_instrs.add(
417 goto_programt::make_decl(in_loop_havoc_block, loop_head_location));
419 in_loop_havoc_block, true_exprt{}, loop_head_location));
420 step_instrs.destructive_append(havoc_instrs);
422 in_loop_havoc_block, false_exprt{}, loop_head_location));
423 }
424
425 goto_convertt converter(symbol_table, log.get_message_handler());
426 const irep_idt &language_mode =
427 dfcc_utilst::get_function_symbol(symbol_table, function_id).mode;
428 {
429 // Assume the loop invariant after havocing the state; produce one
430 // assumption per conjunct to ease analysis of counterexamples, and possibly
431 // also improve solver performance (observed with Bitwuzla)
432 if(invariant.id() == ID_and)
433 {
434 for(const auto &op : invariant.operands())
435 {
436 code_assumet assumption{op};
437 assumption.add_source_location() = loop_head_location;
438 converter.goto_convert(assumption, step_instrs, language_mode);
439 }
440 }
441 else
442 {
443 code_assumet assumption{invariant};
444 assumption.add_source_location() = loop_head_location;
445 converter.goto_convert(assumption, step_instrs, language_mode);
446 }
447 }
448
449 {
450 // Generate assignments to store the multidimensional decreases clause's
451 // value just before the loop_head.
452 for(size_t i = 0; i < old_decreases_vars.size(); i++)
453 {
454 code_frontend_assignt old_decreases_assignment{
455 old_decreases_vars[i], decreases_clauses[i], loop_head_location};
456 converter.goto_convert(
457 old_decreases_assignment, step_instrs, language_mode);
458 }
459 }
460
461 goto_function.body.destructive_insert(loop_head, step_instrs);
462
463 return step_case_target;
464}
465
467 const std::size_t loop_id,
468 const std::size_t cbmc_loop_id,
469 goto_functionst::goto_functiont &goto_function,
470 symbol_table_baset &symbol_table,
471 goto_programt::targett loop_head,
472 goto_programt::targett loop_latch,
473 exprt &invariant,
474 const exprt::operandst &decreases_clauses,
475 const symbol_exprt &entered_loop,
476 const symbol_exprt &in_base_case,
477 const std::vector<symbol_exprt> &old_decreases_vars,
478 const std::vector<symbol_exprt> &new_decreases_vars,
479 const goto_programt::instructiont::targett &step_case_target,
480 const irep_idt &language_mode)
481{
482 auto loop_head_location(loop_head->source_location());
483 dfcc_remove_loop_tags(loop_head_location);
484
485 // HEAD: // Loop body block
486 // ... eval guard ...
487 // IF (!guard) GOTO EXIT;
488 // ... loop body ...
489 // // instrumentation
490 // entered_loop = true
491 // // Jump back to the step case if the loop can run at least once
492 // IF (in_base_case) GOTO STEP;
493 // ASSERT(<loop_invariant>);
494 // new_variant = <loop_decreases>;
495 // ASSERT(new_variant < old_variant);
496 // ASSUME(false);
497
498 goto_programt pre_loop_latch_instrs;
499
500 {
501 // Record that we entered the loop with `entered_loop = true`.
502 pre_loop_latch_instrs.add(goto_programt::make_assignment(
503 entered_loop, true_exprt{}, loop_head_location));
504 }
505
506 {
507 // Jump back to the step case to havoc the write set, assume the invariant,
508 // and execute an arbitrary iteration.
509 pre_loop_latch_instrs.add(goto_programt::make_goto(
510 step_case_target, in_base_case, loop_head_location));
511 }
512
513 goto_convertt converter(symbol_table, log.get_message_handler());
514 {
515 // Because of the unconditional jump above the following code is only
516 // reachable in the step case. Generate the inductive invariant check
517 // `ASSERT(invariant)`.
518 source_locationt check_location(loop_head_location);
519 check_location.set_property_class("loop_invariant_step");
520 check_location.set_comment(
521 "Check invariant after step for loop " +
522 id2string(check_location.get_function()) + "." +
523 std::to_string(cbmc_loop_id));
524 // Assert the loop invariant after havocing the state; produce one assertion
525 // per conjunct to ease analysis of counterexamples, and possibly also
526 // improve solver performance (observed with Bitwuzla)
527 if(invariant.id() == ID_and)
528 {
529 for(const auto &op : invariant.operands())
530 {
531 code_assertt assertion{op};
532 assertion.add_source_location() = check_location;
533 converter.goto_convert(assertion, pre_loop_latch_instrs, language_mode);
534 }
535 }
536 else
537 {
538 code_assertt assertion{invariant};
539 assertion.add_source_location() = check_location;
540 converter.goto_convert(assertion, pre_loop_latch_instrs, language_mode);
541 }
542 }
543
544 {
545 // Generate assignments to store the multidimensional decreases clause's
546 // value after one iteration of the loop.
547 if(!decreases_clauses.empty())
548 {
549 for(size_t i = 0; i < new_decreases_vars.size(); i++)
550 {
551 code_frontend_assignt new_decreases_assignment{
552 new_decreases_vars[i], decreases_clauses[i], loop_head_location};
553 converter.goto_convert(
554 new_decreases_assignment, pre_loop_latch_instrs, language_mode);
555 }
556
557 // Generate assertion that the multidimensional decreases clause's value
558 // after the loop is lexicographically smaller than its initial value.
559 source_locationt check_location(loop_head_location);
560 check_location.set_property_class("loop_decreases");
561 check_location.set_comment(
562 "Check variant decreases after step for loop " +
563 id2string(check_location.get_function()) + "." +
564 std::to_string(cbmc_loop_id));
565 pre_loop_latch_instrs.add(goto_programt::make_assertion(
567 new_decreases_vars, old_decreases_vars),
568 check_location));
569
570 // Discard the temporary variables that store decreases clause's value.
571 for(size_t i = 0; i < old_decreases_vars.size(); i++)
572 {
573 pre_loop_latch_instrs.add(
574 goto_programt::make_dead(old_decreases_vars[i], loop_head_location));
575 pre_loop_latch_instrs.add(
576 goto_programt::make_dead(new_decreases_vars[i], loop_head_location));
577 }
578 }
579 }
580
582 goto_function.body, loop_latch, pre_loop_latch_instrs);
583
584 {
585 // Change the back edge into assume(false) or assume(!guard).
586 loop_latch->turn_into_assume();
587 loop_latch->condition_nonconst() = boolean_negate(loop_latch->condition());
588 }
589}
590
592 const std::size_t loop_id,
593 const std::size_t cbmc_loop_id,
594 goto_functionst::goto_functiont &goto_function,
595 goto_programt::targett loop_head,
596 const symbol_exprt &loop_write_set,
597 const symbol_exprt &addr_of_loop_write_set,
598 const std::unordered_map<exprt, symbol_exprt, irep_hash> &history_var_map,
599 const symbol_exprt &entered_loop,
600 const symbol_exprt &initial_invariant,
601 const symbol_exprt &in_base_case,
602 const std::vector<symbol_exprt> &old_decreases_vars,
603 const std::vector<symbol_exprt> &new_decreases_vars)
604{
605 // Collect all exit targets of the loop.
606 std::set<goto_programt::targett, goto_programt::target_less_than>
607 exit_targets;
608
610 goto_function.body.instructions.begin();
611 target != goto_function.body.instructions.end();
612 target++)
613 {
614 if(!dfcc_is_loop_exiting(target) || !dfcc_has_loop_id(target, loop_id))
615 continue;
616 INVARIANT(target->is_goto(), "Exiting instructions must be GOTOs");
617 auto exit_target = target->get_target();
618 auto exit_loop_id_opt = dfcc_get_loop_id(exit_target);
619 INVARIANT(
620 exit_loop_id_opt.has_value() && exit_loop_id_opt.value() != loop_id,
621 "Exiting instructions must jump out of the loop");
622 exit_targets.insert(exit_target);
623 }
624
625 // For each exit target of the loop, insert a code block:
626 // ```
627 // EXIT:
628 // // check that step case was checked if loop can run once
629 // ASSUME (entered_loop ==> !in_base_case);
630 // DEAD loop_entry history vars, in_base_case;
631 // DEAD initial_invariant, entered_loop;
632 // DEAD old_variant, in_loop_havoc_block;
633 // __write_set_release(w_loop);
634 // DEAD __ws_loop, ws_loop;
635 // ```
636
637 for(auto exit_target : exit_targets)
638 {
639 goto_programt loop_exit_program;
640
641 // Use the head location for this check as well so that all checks related
642 // to a given loop are presented as coming from the loop head.
643 source_locationt check_location = loop_head->source_location();
644 check_location.set_property_class("loop_step_unwinding");
645 check_location.set_comment(
646 "Check step was unwound for loop " +
647 id2string(check_location.get_function()) + "." +
648 std::to_string(cbmc_loop_id));
649 loop_exit_program.add(goto_programt::make_assertion(
650 or_exprt{not_exprt{entered_loop}, not_exprt{in_base_case}},
651 check_location));
652
653 // Mark instrumentation variables as going out of scope.
654 const source_locationt &exit_location = exit_target->source_location();
655 loop_exit_program.add(
656 goto_programt::make_dead(in_base_case, exit_location));
657 loop_exit_program.add(
658 goto_programt::make_dead(entered_loop, exit_location));
659 loop_exit_program.add(
660 goto_programt::make_dead(initial_invariant, exit_location));
661
662 // Release the write set resources.
663 loop_exit_program.add(goto_programt::make_function_call(
664 library.write_set_release_call(addr_of_loop_write_set, exit_location),
665 exit_location));
666
667 // Mark write set as going out of scope.
668 loop_exit_program.add(
669 goto_programt::make_dead(to_symbol_expr(loop_write_set), exit_location));
670 loop_exit_program.add(goto_programt::make_dead(
671 to_symbol_expr(addr_of_loop_write_set), exit_location));
672
673 // Mark history variables as going out of scope.
674 for(const auto &v : history_var_map)
675 loop_exit_program.add(goto_programt::make_dead(v.second, exit_location));
676
677 // Mark decreases clause snapshots as gong out of scope.
678 for(size_t i = 0; i < old_decreases_vars.size(); i++)
679 {
680 loop_exit_program.add(
681 goto_programt::make_dead(old_decreases_vars[i], exit_location));
682 loop_exit_program.add(
683 goto_programt::make_dead(new_decreases_vars[i], exit_location));
684 }
685
686 // Insert the exit block, preserving the loop end target.
688 goto_function.body, exit_target, loop_exit_program);
689 }
690}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
unsignedbv_typet size_type()
Definition c_types.cpp:50
Operator to return the address of an object.
The Boolean type.
Definition std_types.h:36
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition std_code.h:270
An assumption, which must hold in subsequent code.
Definition std_code.h:217
A codet representing an assignment in the program.
Definition std_code.h:24
goto_instruction_codet representation of a function call statement.
Computes natural loops, enforces normal form conditions, computes the nesting graph,...
const dfcc_loop_infot & get_loop_info(const std::size_t loop_id) const
Returns the loop info for that loop_id.
const exprt & get_outer_write_set(std::size_t loop_id) const
Returns the write set of the outer loop of that loop or the top level write set if that loop has no o...
Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that ...
void add_exit_instructions(const std::size_t loop_id, const std::size_t cbmc_loop_id, goto_functionst::goto_functiont &goto_function, goto_programt::targett loop_head, const symbol_exprt &loop_write_set, const symbol_exprt &addr_of_loop_write_set, const std::unordered_map< exprt, symbol_exprt, irep_hash > &history_var_map, const symbol_exprt &entered_loop, const symbol_exprt &initial_invariant, const symbol_exprt &in_base_case, const std::vector< symbol_exprt > &old_decreases_vars, const std::vector< symbol_exprt > &new_decreases_vars)
Adds instructions of the exit block.
dfcc_spec_functionst & spec_functions
dfcc_instrument_loopt(goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_spec_functionst &spec_functions, dfcc_contract_clauses_codegent &contract_clauses_codegen)
Constructor for the loop contract instrumentation class.
void add_body_instructions(const std::size_t loop_id, const std::size_t cbmc_loop_id, goto_functionst::goto_functiont &goto_function, symbol_table_baset &symbol_table, goto_programt::targett loop_head, goto_programt::targett loop_latch, exprt &invariant, const exprt::operandst &decreases_clauses, const symbol_exprt &entered_loop, const symbol_exprt &in_base_case, const std::vector< symbol_exprt > &old_decreases_vars, const std::vector< symbol_exprt > &new_decreases_vars, const goto_programt::instructiont::targett &step_case_target, const irep_idt &symbol_mode)
Adds instructions of the body block.
std::unordered_map< exprt, symbol_exprt, irep_hash > add_prehead_instructions(const std::size_t loop_id, goto_functionst::goto_functiont &goto_function, symbol_table_baset &symbol_table, goto_programt::targett loop_head, goto_programt::targett loop_latch, goto_programt &assigns_instrs, exprt &invariant, const exprt::operandst &assigns, const symbol_exprt &loop_write_set, const symbol_exprt &addr_of_loop_write_set, const symbol_exprt &entered_loop, const symbol_exprt &initial_invariant, const symbol_exprt &in_base_case, const irep_idt &symbol_mode)
Adds instructions of prehead block, and return history variables.
void operator()(const std::size_t loop_id, const irep_idt &function_id, goto_functiont &goto_function, dfcc_cfg_infot &cfg_info, const std::set< symbol_exprt > &local_statics, std::set< irep_idt > &function_pointer_contracts)
Replaces a loop by a base + step abstraction generated from its contract.
goto_programt::instructiont::targett add_step_instructions(const std::size_t loop_id, const std::size_t cbmc_loop_id, const irep_idt &function_id, goto_functionst::goto_functiont &goto_function, symbol_table_baset &symbol_table, goto_programt::targett loop_head, goto_programt::targett loop_latch, goto_programt &havoc_instrs, exprt &invariant, const exprt::operandst &decreases_clauses, const symbol_exprt &loop_write_set, const exprt &outer_write_set, const symbol_exprt &initial_invariant, const symbol_exprt &in_base_case, const std::vector< symbol_exprt > &old_decreases_vars)
Adds instructions of the step block, and returns the STEP jump target so that it can be used to jump ...
dfcc_contract_clauses_codegent & contract_clauses_codegen
Class interface to library types and functions defined in cprover_contracts.c.
Describes a single loop for the purpose of DFCC loop contract instrumentation.
const symbol_exprt addr_of_write_set_var
Symbol representing pointer to the stack allocated write set object for this loop.
const exprt::operandst decreases
Decreases clause expression.
const std::set< exprt > assigns
Set of targets assigned by the loop, either user-provided or inferred.
const std::size_t cbmc_loop_id
Loop identifier assigned to this loop by traditional CBMC loop numbering.
std::optional< goto_programt::targett > find_latch(goto_programt &goto_program) const
const exprt invariant
Loop invariant expression.
std::optional< goto_programt::targett > find_head(goto_programt &goto_program) const
Finds the first instruction tagged as loop head and having the same loop identifier as this struct in...
const symbol_exprt write_set_var
Symbol representing the stack-allocated write set object for this loop.
This class rewrites GOTO functions that use the built-ins:
Equality.
Definition std_expr.h:1366
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
source_locationt & add_source_location()
Definition expr.h:236
The Boolean constant false.
Definition std_expr.h:3199
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_programt body
std::list< instructiont >::iterator targett
The target for gotos and for start_thread nodes.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
void update()
Update all indices.
instructionst::iterator targett
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
Boolean negation.
Definition std_expr.h:2454
The null pointer constant.
Boolean OR.
Definition std_expr.h:2270
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
const irep_idt & get_function() const
Expression to hold a symbol (variable)
Definition std_expr.h:131
The symbol table base class interface.
irep_idt mode
Language mode.
Definition symbol.h:49
The Boolean constant true.
Definition std_expr.h:3190
Class that computes CFG information about the loop structure of a GOTO function for the purpose of dy...
Translates assigns and frees clauses of a function contract or loop contract into goto programs that ...
Add instrumentation to a goto program to perform frame condition checks.
This class applies the loop contract transformation to a loop in a goto function.
bool dfcc_has_loop_id(const goto_programt::instructiont::const_targett &target, std::size_t loop_id)
void dfcc_remove_loop_tags(source_locationt &source_location)
std::optional< std::size_t > dfcc_get_loop_id(const goto_programt::instructiont::const_targett &target)
bool dfcc_is_loop_exiting(const goto_programt::instructiont::const_targett &target)
Functions that allow to tag GOTO instructions with loop identifiers and loop instruction type: head,...
Translate functions that specify assignable and freeable targets declaratively into active functions ...
@ NONDET
havocs the pointer to an nondet pointer
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Fresh auxiliary symbol creation.
Program Transformation.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
static symbol_exprt create_symbol(symbol_table_baset &, const typet &type, const irep_idt &function_id, const std::string &base_name, const source_locationt &source_location)
Adds a new symbol named function_id::base_name of type type with given attributes in the symbol table...
replace_history_parametert replace_history_loop_entry(symbol_table_baset &symbol_table, const exprt &expr, const source_locationt &location, const irep_idt &mode)
This function recursively identifies the "loop_entry" expressions within expr and replaces them with ...
Definition utils.cpp:475
void insert_before_swap_and_advance(goto_programt &destination, goto_programt::targett &target, goto_programt &payload)
Insert a goto program before a target instruction iterator and advance the iterator.
Definition utils.cpp:237
exprt generate_lexicographic_less_than_check(const std::vector< symbol_exprt > &lhs, const std::vector< symbol_exprt > &rhs)
Generate a lexicographic less-than comparison over ordered tuples.
Definition utils.cpp:193
#define ENTERED_LOOP
Definition utils.h:26
#define INIT_INVARIANT
Definition utils.h:28
#define IN_BASE_CASE
Definition utils.h:25
#define IN_LOOP_HAVOC_BLOCK
Definition utils.h:27
dstringt irep_idt