CBMC
dfcc_instrument_loop.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dynamic frame condition checking for loop contracts
4 
5 Author: Qinheping Hu, qinhh@amazon.com
6 
7 Author: Remi Delmas, delmasrd@amazon.com
8 
9 Date: April 2023
10 
11 \*******************************************************************/
12 
13 #include "dfcc_instrument_loop.h"
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 
28  goto_modelt &goto_model,
29  message_handlert &message_handler,
30  dfcc_libraryt &library,
31  dfcc_spec_functionst &spec_functions,
32  dfcc_contract_clauses_codegent &contract_clauses_codegen)
33  : goto_model(goto_model),
34  log(message_handler),
35  library(library),
36  spec_functions(spec_functions),
37  contract_clauses_codegen(contract_clauses_codegen),
38  ns(goto_model.symbol_table)
39 {
40 }
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;
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 
121  function_id,
122  write_set_populate_instrs,
124  havoc_instrs,
125  nof_targets);
128  language_mode,
129  write_set_populate_instrs,
130  nof_targets);
131 
132  // ---------- Add instrumented instructions ----------
133  goto_programt::targett loop_latch =
134  loop.find_latch(goto_function.body).value();
135  exprt invariant(loop.invariant);
136  const auto history_var_map = add_prehead_instructions(
137  loop_id,
138  goto_function,
139  symbol_table,
140  head,
141  loop_latch,
142  write_set_populate_instrs,
143  invariant,
144  assigns,
145  loop.write_set_var,
147  entered_loop,
148  initial_invariant,
149  in_base_case,
150  language_mode);
151 
152  const auto step_target = add_step_instructions(
153  loop_id,
154  cbmc_loop_id,
155  function_id,
156  goto_function,
157  symbol_table,
158  head,
159  loop_latch,
160  havoc_instrs,
161  invariant,
162  decreases_clauses,
164  outer_write_set,
165  initial_invariant,
166  in_base_case,
167  old_decreases_vars);
168 
170  loop_id,
171  cbmc_loop_id,
172  goto_function,
173  symbol_table,
174  head,
175  loop_latch,
176  invariant,
177  decreases_clauses,
178  entered_loop,
179  in_base_case,
180  old_decreases_vars,
181  new_decreases_vars,
182  step_target,
183  language_mode);
184 
186  loop_id,
187  cbmc_loop_id,
188  goto_function,
189  head,
190  loop.write_set_var,
192  history_var_map,
193  entered_loop,
194  initial_invariant,
195  in_base_case,
196  old_decreases_vars,
197  new_decreases_vars);
198 
199  goto_function.body.update();
200 }
201 
202 std::unordered_map<exprt, symbol_exprt, irep_hash>
204  const std::size_t loop_id,
205  goto_functionst::goto_functiont &goto_function,
206  symbol_table_baset &symbol_table,
207  goto_programt::targett loop_head,
208  goto_programt::targett loop_latch,
209  goto_programt &assigns_instrs,
210  exprt &invariant,
211  const exprt::operandst &assigns,
212  const symbol_exprt &loop_write_set,
213  const symbol_exprt &addr_of_loop_write_set,
214  const symbol_exprt &entered_loop,
215  const symbol_exprt &initial_invariant,
216  const symbol_exprt &in_base_case,
217  const irep_idt &language_mode)
218 {
219  auto loop_head_location(loop_head->source_location());
220  dfcc_remove_loop_tags(loop_head_location);
221 
222  // ```
223  // ... preamble ...
224  //
225  // // Prehead block: Declare & initialize instrumentation variables
226  // snapshot loop_entry history vars;
227  // entered_loop = false
228  // initial_invariant = loop_invariant;
229  // in_base_case = true;
230  // __ws_loop;
231  // ws_loop := address_of(__ws_loop);
232  // __write_set_create(ws_loop);
233  // __write_set_add(ws_loop, loop_assigns);
234  // __write_set_add(ws_loop, local_statics);
235  // GOTO HEAD;
236  // ```
237 
238  // initialize loop_entry history vars;
239  auto replace_history_result = replace_history_loop_entry(
240  symbol_table, invariant, loop_head_location, language_mode);
241  invariant.swap(replace_history_result.expression_after_replacement);
242  goto_programt &pre_loop_head_instrs =
243  replace_history_result.history_construction;
244 
245  // entered_loop = false
246  {
247  pre_loop_head_instrs.add(
248  goto_programt::make_decl(entered_loop, loop_head_location));
249  pre_loop_head_instrs.add(goto_programt::make_assignment(
250  entered_loop, false_exprt{}, loop_head_location));
251  }
252 
253  // initial_invariant = <loop_invariant>;
254  {
255  // Create a snapshot of the invariant so that we can check the base case,
256  // if the loop is not vacuous and must be abstracted with contracts.
257  pre_loop_head_instrs.add(
258  goto_programt::make_decl(initial_invariant, loop_head_location));
259 
260  // Although the invariant at this point will not have side effects,
261  // it is still a C expression, and needs to be "goto_convert"ed.
262  // Note that this conversion may emit many GOTO instructions.
263  code_frontend_assignt initial_invariant_assignment{
264  initial_invariant, invariant, loop_head_location};
265  goto_convertt converter(symbol_table, log.get_message_handler());
266  converter.goto_convert(
267  initial_invariant_assignment, pre_loop_head_instrs, language_mode);
268  }
269 
270  {
271  // Create a temporary variable to track base case vs inductive case
272  // instrumentation of the loop.
273  // in_base_case = true;
274  pre_loop_head_instrs.add(
275  goto_programt::make_decl(in_base_case, loop_head_location));
276  pre_loop_head_instrs.add(goto_programt::make_assignment(
277  in_base_case, true_exprt{}, loop_head_location));
278  }
279 
280  {
281  // Create and populate the write set.
282  // DECL loop_write_set
283  // DECL addr_of_loop_write_set
284  // ASSIGN write_set_ptr := address_of(write_set)
285  // CALL __CPROVER_contracts_write_set_create(write_set_ptr,
286  // contracts_assigns_size, contracts_assigns_frees_size,
287  // assume_require_ctx, assert_require_ctx, assume_ensures_ctx,
288  // assert_ensures_ctx, allow_allocate, allow_deallocate);
289  pre_loop_head_instrs.add(
290  goto_programt::make_decl(loop_write_set, loop_head_location));
291  pre_loop_head_instrs.add(
292  goto_programt::make_decl(addr_of_loop_write_set, loop_head_location));
293  pre_loop_head_instrs.add(goto_programt::make_assignment(
294  addr_of_loop_write_set,
295  address_of_exprt(loop_write_set),
296  loop_head_location));
297 
299  addr_of_loop_write_set,
300  from_integer(assigns.size(), size_type()),
301  loop_head_location);
302  pre_loop_head_instrs.add(
303  goto_programt::make_function_call(call, loop_head_location));
304 
305  pre_loop_head_instrs.destructive_append(assigns_instrs);
306  }
307 
308  // goto HEAD;
309  pre_loop_head_instrs.add(
310  goto_programt::make_goto(loop_head, true_exprt{}, loop_head_location));
311 
312  goto_function.body.destructive_insert(loop_head, pre_loop_head_instrs);
313  return replace_history_result.parameter_to_history;
314 }
315 
318  const std::size_t loop_id,
319  const std::size_t cbmc_loop_id,
320  const irep_idt &function_id,
321  goto_functionst::goto_functiont &goto_function,
322  symbol_table_baset &symbol_table,
323  goto_programt::targett loop_head,
324  goto_programt::targett loop_latch,
325  goto_programt &havoc_instrs,
326  exprt &invariant,
327  const exprt::operandst &decreases_clauses,
328  const symbol_exprt &addr_of_loop_write_set,
329  const exprt &outer_write_set,
330  const symbol_exprt &initial_invariant,
331  const symbol_exprt &in_base_case,
332  const std::vector<symbol_exprt> &old_decreases_vars)
333 {
334  auto loop_head_location(loop_head->source_location());
335  dfcc_remove_loop_tags(loop_head_location);
336 
337  // ```
338  // STEP: // Loop step block: havoc the loop state
339  // ASSERT(initial_invariant);
340  // __write_set_check_inclusion(ws_loop, ws_parent);
341  // in_base_case = false;
342  // in_loop_havoc_block = true;
343  // havoc(assigns_clause_targets);
344  // in_loop_havoc_block = false;
345  // ASSUME(loop_invariant);
346  // old_variant = loop_decreases;
347  // ```
348 
349  goto_programt step_instrs;
350 
351  // We skip past it initially, because of the unconditional jump above,
352  // but jump back here if we get past the loop guard while in_base_case.
353  // `in_base_case = false;`
354  goto_programt::instructiont::targett step_case_target =
356  in_base_case, false_exprt{}, loop_head_location));
357 
358  {
359  // If we jump here, then the loop runs at least once,
360  // so add the base case assertion: `assert(initial_invariant)`.
361  source_locationt check_location(loop_head_location);
362  check_location.set_property_class("loop_invariant_base");
363  check_location.set_comment(
364  "Check invariant before entry for loop " +
365  id2string(check_location.get_function()) + "." +
366  std::to_string(cbmc_loop_id));
367  step_instrs.add(
368  goto_programt::make_assertion(initial_invariant, check_location));
369  }
370 
371  {
372  // Check assigns clause inclusion with parent write set
373  // skip the check when if w_parent is NULL.
374  auto goto_instruction = step_instrs.add(goto_programt::make_incomplete_goto(
375  equal_exprt(
376  outer_write_set,
377  null_pointer_exprt(to_pointer_type(outer_write_set.type()))),
378  loop_head_location));
379 
380  const auto check_var = dfcc_utilst::create_symbol(
381  symbol_table,
382  bool_typet(),
383  function_id,
384  "__check_assigns_clause_incl_loop_" + std::to_string(cbmc_loop_id),
385  loop_head_location);
386 
387  step_instrs.add(goto_programt::make_decl(check_var, loop_head_location));
390  check_var, outer_write_set, addr_of_loop_write_set, loop_head_location),
391  loop_head_location));
392 
393  source_locationt check_location(loop_head_location);
394  check_location.set_property_class("loop_assigns");
395  check_location.set_comment(
396  "Check assigns clause inclusion for loop " +
397  id2string(check_location.get_function()) + "." +
398  std::to_string(cbmc_loop_id));
399  step_instrs.add(goto_programt::make_assertion(check_var, check_location));
400  step_instrs.add(goto_programt::make_dead(check_var, loop_head_location));
401 
402  auto label_instruction =
403  step_instrs.add(goto_programt::make_skip(loop_head_location));
404  goto_instruction->complete_goto(label_instruction);
405  }
406 
407  {
408  // Generate havocing code for assigns targets.
409  const auto in_loop_havoc_block = dfcc_utilst::create_symbol(
410  symbol_table,
411  bool_typet(),
412  function_id,
413  std::string(IN_LOOP_HAVOC_BLOCK) + +"__" + std::to_string(cbmc_loop_id),
414  loop_head_location);
415  step_instrs.add(
416  goto_programt::make_decl(in_loop_havoc_block, loop_head_location));
418  in_loop_havoc_block, true_exprt{}, loop_head_location));
419  step_instrs.destructive_append(havoc_instrs);
421  in_loop_havoc_block, false_exprt{}, loop_head_location));
422  }
423 
424  goto_convertt converter(symbol_table, log.get_message_handler());
425  const irep_idt &language_mode =
426  dfcc_utilst::get_function_symbol(symbol_table, function_id).mode;
427  {
428  // Assume the loop invariant after havocing the state; produce one
429  // assumption per conjunct to ease analysis of counterexamples, and possibly
430  // also improve solver performance (observed with Bitwuzla)
431  if(invariant.id() == ID_and)
432  {
433  for(const auto &op : invariant.operands())
434  {
435  code_assumet assumption{op};
436  assumption.add_source_location() = loop_head_location;
437  converter.goto_convert(assumption, step_instrs, language_mode);
438  }
439  }
440  else
441  {
442  code_assumet assumption{invariant};
443  assumption.add_source_location() = loop_head_location;
444  converter.goto_convert(assumption, step_instrs, language_mode);
445  }
446  }
447 
448  {
449  // Generate assignments to store the multidimensional decreases clause's
450  // value just before the loop_head.
451  for(size_t i = 0; i < old_decreases_vars.size(); i++)
452  {
453  code_frontend_assignt old_decreases_assignment{
454  old_decreases_vars[i], decreases_clauses[i], loop_head_location};
455  converter.goto_convert(
456  old_decreases_assignment, step_instrs, language_mode);
457  }
458  }
459 
460  goto_function.body.destructive_insert(loop_head, step_instrs);
461 
462  return step_case_target;
463 }
464 
466  const std::size_t loop_id,
467  const std::size_t cbmc_loop_id,
468  goto_functionst::goto_functiont &goto_function,
469  symbol_table_baset &symbol_table,
470  goto_programt::targett loop_head,
471  goto_programt::targett loop_latch,
472  exprt &invariant,
473  const exprt::operandst &decreases_clauses,
474  const symbol_exprt &entered_loop,
475  const symbol_exprt &in_base_case,
476  const std::vector<symbol_exprt> &old_decreases_vars,
477  const std::vector<symbol_exprt> &new_decreases_vars,
478  const goto_programt::instructiont::targett &step_case_target,
479  const irep_idt &language_mode)
480 {
481  auto loop_head_location(loop_head->source_location());
482  dfcc_remove_loop_tags(loop_head_location);
483 
484  // HEAD: // Loop body block
485  // ... eval guard ...
486  // IF (!guard) GOTO EXIT;
487  // ... loop body ...
488  // // instrumentation
489  // entered_loop = true
490  // // Jump back to the step case if the loop can run at least once
491  // IF (in_base_case) GOTO STEP;
492  // ASSERT(<loop_invariant>);
493  // new_variant = <loop_decreases>;
494  // ASSERT(new_variant < old_variant);
495  // ASSUME(false);
496 
497  goto_programt pre_loop_latch_instrs;
498 
499  {
500  // Record that we entered the loop with `entered_loop = true`.
501  pre_loop_latch_instrs.add(goto_programt::make_assignment(
502  entered_loop, true_exprt{}, loop_head_location));
503  }
504 
505  {
506  // Jump back to the step case to havoc the write set, assume the invariant,
507  // and execute an arbitrary iteration.
508  pre_loop_latch_instrs.add(goto_programt::make_goto(
509  step_case_target, in_base_case, loop_head_location));
510  }
511 
512  goto_convertt converter(symbol_table, log.get_message_handler());
513  {
514  // Because of the unconditional jump above the following code is only
515  // reachable in the step case. Generate the inductive invariant check
516  // `ASSERT(invariant)`.
517  source_locationt check_location(loop_head_location);
518  check_location.set_property_class("loop_invariant_step");
519  check_location.set_comment(
520  "Check invariant after step for loop " +
521  id2string(check_location.get_function()) + "." +
522  std::to_string(cbmc_loop_id));
523  // Assert the loop invariant after havocing the state; produce one assertion
524  // per conjunct to ease analysis of counterexamples, and possibly also
525  // improve solver performance (observed with Bitwuzla)
526  if(invariant.id() == ID_and)
527  {
528  for(const auto &op : invariant.operands())
529  {
530  code_assertt assertion{op};
531  assertion.add_source_location() = check_location;
532  converter.goto_convert(assertion, pre_loop_latch_instrs, language_mode);
533  }
534  }
535  else
536  {
537  code_assertt assertion{invariant};
538  assertion.add_source_location() = check_location;
539  converter.goto_convert(assertion, pre_loop_latch_instrs, language_mode);
540  }
541  }
542 
543  {
544  // Generate assignments to store the multidimensional decreases clause's
545  // value after one iteration of the loop.
546  if(!decreases_clauses.empty())
547  {
548  for(size_t i = 0; i < new_decreases_vars.size(); i++)
549  {
550  code_frontend_assignt new_decreases_assignment{
551  new_decreases_vars[i], decreases_clauses[i], loop_head_location};
552  converter.goto_convert(
553  new_decreases_assignment, pre_loop_latch_instrs, language_mode);
554  }
555 
556  // Generate assertion that the multidimensional decreases clause's value
557  // after the loop is lexicographically smaller than its initial value.
558  source_locationt check_location(loop_head_location);
559  check_location.set_property_class("loop_decreases");
560  check_location.set_comment(
561  "Check variant decreases after step for loop " +
562  id2string(check_location.get_function()) + "." +
563  std::to_string(cbmc_loop_id));
564  pre_loop_latch_instrs.add(goto_programt::make_assertion(
566  new_decreases_vars, old_decreases_vars),
567  check_location));
568 
569  // Discard the temporary variables that store decreases clause's value.
570  for(size_t i = 0; i < old_decreases_vars.size(); i++)
571  {
572  pre_loop_latch_instrs.add(
573  goto_programt::make_dead(old_decreases_vars[i], loop_head_location));
574  pre_loop_latch_instrs.add(
575  goto_programt::make_dead(new_decreases_vars[i], loop_head_location));
576  }
577  }
578  }
579 
581  goto_function.body, loop_latch, pre_loop_latch_instrs);
582 
583  {
584  // Change the back edge into assume(false) or assume(!guard).
585  loop_latch->turn_into_assume();
586  loop_latch->condition_nonconst() = boolean_negate(loop_latch->condition());
587  }
588 }
589 
591  const std::size_t loop_id,
592  const std::size_t cbmc_loop_id,
593  goto_functionst::goto_functiont &goto_function,
594  goto_programt::targett loop_head,
595  const symbol_exprt &loop_write_set,
596  const symbol_exprt &addr_of_loop_write_set,
597  const std::unordered_map<exprt, symbol_exprt, irep_hash> &history_var_map,
598  const symbol_exprt &entered_loop,
599  const symbol_exprt &initial_invariant,
600  const symbol_exprt &in_base_case,
601  const std::vector<symbol_exprt> &old_decreases_vars,
602  const std::vector<symbol_exprt> &new_decreases_vars)
603 {
604  // Collect all exit targets of the loop.
605  std::set<goto_programt::targett, goto_programt::target_less_than>
606  exit_targets;
607 
609  goto_function.body.instructions.begin();
610  target != goto_function.body.instructions.end();
611  target++)
612  {
613  if(!dfcc_is_loop_exiting(target) || !dfcc_has_loop_id(target, loop_id))
614  continue;
615  INVARIANT(target->is_goto(), "Exiting instructions must be GOTOs");
616  auto exit_target = target->get_target();
617  auto exit_loop_id_opt = dfcc_get_loop_id(exit_target);
618  INVARIANT(
619  exit_loop_id_opt.has_value() && exit_loop_id_opt.value() != loop_id,
620  "Exiting instructions must jump out of the loop");
621  exit_targets.insert(exit_target);
622  }
623 
624  // For each exit target of the loop, insert a code block:
625  // ```
626  // EXIT:
627  // // check that step case was checked if loop can run once
628  // ASSUME (entered_loop ==> !in_base_case);
629  // DEAD loop_entry history vars, in_base_case;
630  // DEAD initial_invariant, entered_loop;
631  // DEAD old_variant, in_loop_havoc_block;
632  // __write_set_release(w_loop);
633  // DEAD __ws_loop, ws_loop;
634  // ```
635 
636  for(auto exit_target : exit_targets)
637  {
638  goto_programt loop_exit_program;
639 
640  // Use the head location for this check as well so that all checks related
641  // to a given loop are presented as coming from the loop head.
642  source_locationt check_location = loop_head->source_location();
643  check_location.set_property_class("loop_step_unwinding");
644  check_location.set_comment(
645  "Check step was unwound for loop " +
646  id2string(check_location.get_function()) + "." +
647  std::to_string(cbmc_loop_id));
648  loop_exit_program.add(goto_programt::make_assertion(
649  or_exprt{not_exprt{entered_loop}, not_exprt{in_base_case}},
650  check_location));
651 
652  // Mark instrumentation variables as going out of scope.
653  const source_locationt &exit_location = exit_target->source_location();
654  loop_exit_program.add(
655  goto_programt::make_dead(in_base_case, exit_location));
656  loop_exit_program.add(
657  goto_programt::make_dead(entered_loop, exit_location));
658  loop_exit_program.add(
659  goto_programt::make_dead(initial_invariant, exit_location));
660 
661  // Release the write set resources.
662  loop_exit_program.add(goto_programt::make_function_call(
663  library.write_set_release_call(addr_of_loop_write_set, exit_location),
664  exit_location));
665 
666  // Mark write set as going out of scope.
667  loop_exit_program.add(
668  goto_programt::make_dead(to_symbol_expr(loop_write_set), exit_location));
669  loop_exit_program.add(goto_programt::make_dead(
670  to_symbol_expr(addr_of_loop_write_set), exit_location));
671 
672  // Mark history variables as going out of scope.
673  for(const auto &v : history_var_map)
674  loop_exit_program.add(goto_programt::make_dead(v.second, exit_location));
675 
676  // Mark decreases clause snapshots as gong out of scope.
677  for(size_t i = 0; i < old_decreases_vars.size(); i++)
678  {
679  loop_exit_program.add(
680  goto_programt::make_dead(old_decreases_vars[i], exit_location));
681  loop_exit_program.add(
682  goto_programt::make_dead(new_decreases_vars[i], exit_location));
683  }
684 
685  // Insert the exit block, preserving the loop end target.
687  goto_function.body, exit_target, loop_exit_program);
688  }
689 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Operator to return the address of an object.
Definition: pointer_expr.h:540
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 gen_spec_assigns_instructions(const irep_idt &language_mode, const exprt::operandst &assigns_clause, goto_programt &dest)
Generates instructions encoding the assigns_clause targets and adds them to dest.
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.
Definition: dfcc_library.h:154
const code_function_callt write_set_release_call(const exprt &write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_release.
const code_function_callt write_set_check_assigns_clause_inclusion_call(const exprt &check_var, const exprt &reference_write_set_ptr, const exprt &candidate_write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_assigns_clause_inclusion.
const code_function_callt write_set_create_call(const exprt &write_set_ptr, const exprt &contract_assigns_size, const exprt &contract_frees_size, const exprt &assume_requires_ctx, const exprt &assert_requires_ctx, const exprt &assume_ensures_ctx, const exprt &assert_ensures_ctx, const exprt &allow_allocate, const exprt &allow_deallocate, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_create.
Describes a single loop for the purpose of DFCC loop contract instrumentation.
Definition: dfcc_cfg_info.h:40
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:
void generate_havoc_instructions(const irep_idt &function_id, const goto_programt &original_program, const exprt &write_set_to_havoc, goto_programt &havoc_program, std::size_t &nof_targets)
Translates original_program that specifies assignable targets into a program that havocs the targets.
void to_spec_assigns_instructions(const exprt &write_set_to_fill, const irep_idt &language_mode, goto_programt &program, std::size_t &nof_targets)
Rewrites in place program expressed in terms of built-ins specifying assignable targets declaratively...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Equality.
Definition: std_expr.h:1361
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
source_locationt & add_source_location()
Definition: expr.h:236
typet & type()
Return the type of the expression.
Definition: expr.h:84
operandst & operands()
Definition: expr.h:94
The Boolean constant false.
Definition: std_expr.h:3072
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...
Definition: goto_function.h:24
goto_programt body
Definition: goto_function.h:26
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:31
std::list< instructiont >::iterator targett
The target for gotos and for start_thread nodes.
Definition: goto_program.h:381
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:971
void update()
Update all indices.
instructionst::iterator targett
Definition: goto_program.h:614
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:722
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())
Definition: goto_program.h:891
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.
Definition: goto_program.h:739
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())
Definition: goto_program.h:964
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:933
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
const irep_idt & id() const
Definition: irep.h:388
void swap(irept &irep)
Definition: irep.h:434
message_handlert & get_message_handler()
Definition: message.h:183
Boolean negation.
Definition: std_expr.h:2327
The null pointer constant.
Definition: pointer_expr.h:909
Boolean OR.
Definition: std_expr.h:2228
const irep_idt & get_function() const
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
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:3063
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 ...
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:103
Fresh auxiliary symbol creation.
Program Transformation.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
double log(double x)
Definition: math.c:2776
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
Definition: dfcc_utils.cpp:72
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...
Definition: dfcc_utils.cpp:81
#define size_type
Definition: unistd.c:347
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