CBMC
dfcc_cfg_info.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dynamic frame condition checking for function and loop contracts.
4 
5 Author: Qinheping Hu, qinhh@amazon.com
6 Author: Remi Delmas delmasrd@amazon.com
7 
8 Date: March 2023
9 
10 \*******************************************************************/
11 
12 #include "dfcc_cfg_info.h"
13 
14 #include <util/c_types.h>
15 #include <util/format_expr.h>
16 #include <util/fresh_symbol.h>
17 #include <util/pointer_expr.h>
18 
20 #include <analyses/natural_loops.h>
22 
25 #include "dfcc_is_cprover_symbol.h"
26 #include "dfcc_library.h"
28 #include "dfcc_loop_tags.h"
29 #include "dfcc_root_object.h"
30 #include "dfcc_utils.h"
31 
34 static bool has_contract(
35  const goto_programt::const_targett &latch_target,
36  const bool check_side_effect)
37 {
38  return get_loop_assigns(latch_target).is_not_nil() ||
39  get_loop_invariants(latch_target, check_side_effect).is_not_nil() ||
40  get_loop_decreases(latch_target, check_side_effect).is_not_nil();
41 }
42 
43 void dfcc_loop_infot::output(std::ostream &out) const
44 {
45  out << "dfcc_loop_id: " << loop_id << "\n";
46  out << "cbmc_loop_id: " << cbmc_loop_id << "\n";
47  out << "local: {";
48  for(auto &id : local)
49  {
50  out << id << ", ";
51  }
52  out << "}\n";
53 
54  out << "tracked: {";
55  for(auto &id : tracked)
56  {
57  out << id << ", ";
58  }
59  out << "}\n";
60 
61  out << "write_set: " << format(write_set_var) << "\n";
62 
63  out << "addr_of_write_set: " << format(addr_of_write_set_var) << "\n";
64 
65  out << "assigns: {";
66  for(auto &expr : assigns)
67  {
68  out << format(expr) << ", ";
69  }
70  out << "}\n";
71 
72  out << "invariant: " << format(invariant) << "\n";
73 
74  out << "decreases: {";
75  for(auto &expr : decreases)
76  {
77  out << format(expr) << ", ";
78  }
79  out << "}\n";
80 
81  out << "inner loops: {"
82  << "\n";
83  for(auto &id : inner_loops)
84  {
85  out << id << ", ";
86  }
87  out << "}\n";
88 
89  out << "outer loops: {"
90  << "\n";
91  for(auto &id : outer_loops)
92  {
93  out << id << ", ";
94  }
95  out << "}\n";
96 }
97 
98 std::optional<goto_programt::targett>
100 {
101  for(auto target = goto_program.instructions.begin();
102  target != goto_program.instructions.end();
103  target++)
104  {
105  if(dfcc_is_loop_head(target) && dfcc_has_loop_id(target, loop_id))
106  {
107  return target;
108  }
109  }
110  return {};
111 }
112 
113 std::optional<goto_programt::targett>
115 {
116  std::optional<goto_programt::targett> result = std::nullopt;
117  for(auto target = goto_program.instructions.begin();
118  target != goto_program.instructions.end();
119  target++)
120  {
121  // go until the end because we want to find the very last occurrence
122  if(dfcc_is_loop_latch(target) && dfcc_has_loop_id(target, loop_id))
123  {
124  result = target;
125  }
126  }
127  return result;
128 }
129 
130 static std::optional<goto_programt::targett> check_has_contract_rec(
131  const dfcc_loop_nesting_grapht &loop_nesting_graph,
132  const std::size_t loop_idx,
133  const bool must_have_contract,
134  const bool check_side_effect)
135 {
136  const auto &node = loop_nesting_graph[loop_idx];
137  if(must_have_contract && !has_contract(node.latch, check_side_effect))
138  return node.head;
139 
140  for(const auto pred_idx : loop_nesting_graph.get_predecessors(loop_idx))
141  {
142  auto result = check_has_contract_rec(
143  loop_nesting_graph,
144  pred_idx,
145  has_contract(node.latch, check_side_effect),
146  check_side_effect);
147  if(result.has_value())
148  return result;
149  }
150  return {};
151 }
152 
156 static std::optional<goto_programt::targett> check_inner_loops_have_contracts(
157  const dfcc_loop_nesting_grapht &loop_nesting_graph,
158  const bool check_side_effect)
159 {
160  for(std::size_t idx = 0; idx < loop_nesting_graph.size(); idx++)
161  {
162  if(loop_nesting_graph.get_successors(idx).empty())
163  {
164  auto result = check_has_contract_rec(
165  loop_nesting_graph, idx, false, check_side_effect);
166  if(result.has_value())
167  return result;
168  }
169  }
170  return {};
171 }
172 
177  goto_programt &goto_program,
178  dfcc_loop_nesting_grapht &loop_nesting_graph)
179 {
180  for(const auto &idx : loop_nesting_graph.topsort())
181  {
182  auto &node = loop_nesting_graph[idx];
183  auto &head = node.head;
184  auto &latch = node.latch;
185  auto &instruction_iterators = node.instructions;
186 
187  dfcc_set_loop_head(head);
188  dfcc_set_loop_latch(latch);
189 
190  for(goto_programt::targett t : instruction_iterators)
191  {
192  // Skip instructions that are already tagged and belong to inner loops.
193  auto loop_id_opt = dfcc_get_loop_id(t);
194  if(loop_id_opt.has_value())
195  continue;
196 
197  dfcc_set_loop_id(t, idx);
198 
199  if(t != head && t != latch)
201 
202  if(t->is_goto() && !instruction_iterators.contains(t->get_target()))
203  {
205  }
206  }
207  }
208 
209  auto top_level_id = loop_nesting_graph.size();
210 
211  // tag remaining instructions as top level
212  for(auto target = goto_program.instructions.begin();
213  target != goto_program.instructions.end();
214  target++)
215  {
216  // Skip instructions that are already tagged (belong to loops).
217  auto loop_id_opt = dfcc_get_loop_id(target);
218  if(loop_id_opt.has_value())
219  {
220  continue;
221  }
222  dfcc_set_loop_id(target, top_level_id);
223  dfcc_set_loop_top_level(target);
224  }
225 }
226 
227 static bool is_assigned(dirtyt &dirty, const irep_idt &ident, assignst assigns)
228 {
229  PRECONDITION(!dirty(ident));
230  // For each assigns clause target
231  for(const auto &expr : assigns)
232  {
233  auto root_objects = dfcc_root_objects(expr);
234  for(const auto &root_object : root_objects)
235  {
236  if(
237  root_object.id() == ID_symbol &&
238  expr_try_dynamic_cast<symbol_exprt>(root_object)->get_identifier() ==
239  ident)
240  {
241  return true;
242  }
243  // If `root_object` is not a symbol, then it contains a combination of
244  // address-of and dereference operators that cannot be statically
245  // resolved to a symbol.
246  // Since we know `ident` is not dirty, we know that dereference
247  // operations cannot land on that `ident`. So the root_object cannot
248  // describe a memory location within the object backing that ident.
249  // We conclude that ident is not assigned by this target and move on to
250  // the next target.
251  }
252  }
253  return false;
254 }
255 
269 static std::unordered_set<irep_idt> gen_tracked_set(
270  const std::vector<std::size_t> &inner_loops_ids,
271  const std::unordered_set<irep_idt> &locals,
272  dirtyt &dirty,
273  const std::map<std::size_t, dfcc_loop_infot> &loop_info_map)
274 {
275  std::unordered_set<irep_idt> tracked;
276  for(const auto &ident : locals)
277  {
278  if(dirty(ident))
279  {
280  tracked.insert(ident);
281  }
282  else
283  {
284  // Check if this ident is touched by one of the inner loops
285  for(const auto inner_loop_id : inner_loops_ids)
286  {
287  if(is_assigned(dirty, ident, loop_info_map.at(inner_loop_id).assigns))
288  tracked.insert(ident);
289  }
290  }
291  }
292  return tracked;
293 }
294 
296 {
297  explicit contract_clausest(const exprt::operandst &decreases)
299  {
300  }
304 };
305 
309  const dfcc_loop_nesting_grapht &loop_nesting_graph,
310  const std::size_t loop_id,
311  const irep_idt &function_id,
312  const assignst &inferred_assigns,
313  const bool check_side_effect,
314  message_handlert &message_handler,
315  const namespacet &ns)
316 {
317  messaget log(message_handler);
318  const auto &loop = loop_nesting_graph[loop_id];
319 
320  // Process loop contract clauses
321  exprt::operandst invariant_clauses =
322  get_loop_invariants(loop.latch, check_side_effect).operands();
323  exprt::operandst assigns_clauses = get_loop_assigns(loop.latch).operands();
324 
325  // Initialise defaults
326  struct contract_clausest result(
327  get_loop_decreases(loop.latch, check_side_effect).operands());
328 
329  // Generate defaults for all clauses if at least one type of clause is defined
330  if(
331  !invariant_clauses.empty() || !result.decreases_clauses.empty() ||
332  !assigns_clauses.empty())
333  {
334  if(invariant_clauses.empty())
335  {
336  // use a default invariant if none given.
337  result.invariant_expr = true_exprt{};
338  // assigns clause is missing; we will try to automatic inference
339  log.warning() << "No invariant provided for loop " << function_id << "."
340  << loop.latch->loop_number << " at "
341  << loop.head->source_location()
342  << ". Using 'true' as a sound default invariant. Please "
343  "provide an invariant the default is too weak."
344  << messaget::eom;
345  }
346  else
347  {
348  // conjoin all invariant clauses
349  result.invariant_expr = conjunction(invariant_clauses);
350  }
351 
352  // unpack assigns clause targets
353  if(!assigns_clauses.empty())
354  {
355  for(auto &operand : assigns_clauses)
356  {
357  result.assigns.insert(operand);
358  }
359  }
360  else
361  {
362  // infer assigns clause targets if none given
363  log.warning() << "No assigns clause provided for loop " << function_id
364  << "." << loop.latch->loop_number << " at "
365  << loop.head->source_location() << ". The inferred set {";
366  bool first = true;
367  for(const auto &expr : inferred_assigns)
368  {
369  if(!first)
370  {
371  log.warning() << ", ";
372  }
373  first = false;
374  log.warning() << format(expr);
375  }
376  log.warning() << "} might be incomplete or imprecise, please provide an "
377  "assigns clause if the analysis fails."
378  << messaget::eom;
379  result.assigns = inferred_assigns;
380  }
381 
382  if(result.decreases_clauses.empty())
383  {
384  log.warning() << "No decrease clause provided for loop " << function_id
385  << "." << loop.latch->loop_number << " at "
386  << loop.head->source_location()
387  << ". Termination will not be checked." << messaget::eom;
388  }
389  }
390  return result;
391 }
392 
394  const dfcc_loop_nesting_grapht &loop_nesting_graph,
395  const std::size_t loop_id,
396  const irep_idt &function_id,
397  goto_functiont &goto_function,
398  const std::map<std::size_t, dfcc_loop_infot> &loop_info_map,
399  dirtyt &dirty,
400  const assignst &inferred_assigns,
401  const bool check_side_effect,
402  message_handlert &message_handler,
403  dfcc_libraryt &library,
404  symbol_table_baset &symbol_table)
405 {
406  const namespacet ns(symbol_table);
407  std::unordered_set<irep_idt> loop_locals = gen_loop_locals_set(
408  function_id,
409  goto_function,
410  loop_nesting_graph[loop_id],
411  message_handler,
412  ns);
413 
414  // Exclude locals of inner nested loops.
415  for(const auto &inner_loop : loop_nesting_graph.get_predecessors(loop_id))
416  {
417  INVARIANT(
418  loop_info_map.find(inner_loop) != loop_info_map.end(),
419  "DFCC should gen_dfcc_loop_info for inner loops first.");
420  for(const auto &inner_local : loop_info_map.at(inner_loop).local)
421  {
422  loop_locals.erase(inner_local);
423  }
424  }
425 
426  std::unordered_set<irep_idt> loop_tracked = gen_tracked_set(
427  loop_nesting_graph.get_predecessors(loop_id),
428  loop_locals,
429  dirty,
430  loop_info_map);
431 
432  struct contract_clausest contract_clauses = default_loop_contract_clauses(
433  loop_nesting_graph,
434  loop_id,
435  function_id,
436  inferred_assigns,
437  check_side_effect,
438  message_handler,
439  ns);
440 
441  std::set<std::size_t> inner_loops;
442  for(auto pred_idx : loop_nesting_graph.get_predecessors(loop_id))
443  {
444  inner_loops.insert(pred_idx);
445  }
446 
447  std::set<std::size_t> outer_loops;
448  for(auto succ_idx : loop_nesting_graph.get_successors(loop_id))
449  {
450  outer_loops.insert(succ_idx);
451  }
452 
453  auto &loop = loop_nesting_graph[loop_id];
454  const auto cbmc_loop_number = loop.latch->loop_number;
455 
456  // Generate "write set" variable
457  const auto write_set_var = dfcc_utilst::create_symbol(
458  symbol_table,
460  function_id,
461  "__write_set_loop_" + std::to_string(cbmc_loop_number),
462  loop.head->source_location());
463 
464  // Generate "address of write set" variable
465  const auto &addr_of_write_set_var = dfcc_utilst::create_symbol(
466  symbol_table,
468  function_id,
469  "__address_of_write_set_loop_" + std::to_string(cbmc_loop_number),
470  loop.head->source_location());
471 
472  return {
473  loop_id,
474  cbmc_loop_number,
475  contract_clauses.assigns,
476  contract_clauses.invariant_expr,
477  contract_clauses.decreases_clauses,
478  loop_locals,
479  loop_tracked,
480  inner_loops,
481  outer_loops,
482  write_set_var,
483  addr_of_write_set_var};
484 }
485 
487  goto_modelt &goto_model,
488  const irep_idt &function_id,
489  goto_functiont &goto_function,
490  const exprt &top_level_write_set,
491  const loop_contract_configt &loop_contract_config,
492  symbol_table_baset &symbol_table,
493  message_handlert &message_handler,
494  dfcc_libraryt &library)
495  : function_id(function_id),
496  goto_function(goto_function),
497  top_level_write_set(top_level_write_set),
498  ns(symbol_table)
499 {
500  dfcc_loop_nesting_grapht loop_nesting_graph;
501  goto_programt &goto_program = goto_function.body;
502 
503  // Clean up possible fake loops that are due to do { ... } while(0);
504  simplify_gotos(goto_program, ns);
505 
506  // From loop number to the inferred loop assigns.
507  std::map<std::size_t, assignst> inferred_loop_assigns_map;
508 
509  if(loop_contract_config.apply_loop_contracts)
510  {
511  messaget log(message_handler);
512  dfcc_check_loop_normal_form(goto_program, log);
513  loop_nesting_graph = build_loop_nesting_graph(goto_program);
514 
515  const auto head = check_inner_loops_have_contracts(
516  loop_nesting_graph, loop_contract_config.check_side_effect);
517  if(head.has_value())
518  {
520  "Found loop without contract nested in a loop with a "
521  "contract.\nPlease "
522  "provide a contract or unwind this loop before applying loop "
523  "contracts.",
524  head.value()->source_location());
525  }
526 
527  auto topsorted = loop_nesting_graph.topsort();
528 
529  bool has_loops_with_contracts = false;
530  for(const auto idx : topsorted)
531  {
532  topsorted_loops.push_back(idx);
533  has_loops_with_contracts |= has_contract(
534  loop_nesting_graph[idx].latch, loop_contract_config.check_side_effect);
535  }
536 
537  // We infer loop assigns for all loops in the function.
538  if(has_loops_with_contracts)
539  {
541  inferred_loop_assigns_map,
542  goto_model.goto_functions,
544  message_handler,
545  ns);
546  }
547  }
548 
549  // At this point, either loop contracts were activated and the loop nesting
550  // graph describes the loop structure of the function,
551  // or loop contracts were not activated and the loop nesting graph is empty
552  // (i.e. there might be some loops in the function but we won't consider them
553  // for the instrumentation).
554  // In both cases, we tag program instructions and generate the dfcc_cfg_infot
555  // instance from that graph's contents. The tags will decide against which
556  // write set the instructions are going to be instrumented (either the
557  // function's write set, or the write set of a loop), and each dfcc_loop_infot
558  // contained in the loop_info_map describes a loop to be abstracted by a
559  // contract.
560 
561  tag_loop_instructions(goto_program, loop_nesting_graph);
562 
563  // generate dfcc_cfg_loop_info for loops and add to loop_info_map
564  dirtyt dirty(goto_function);
565 
566  for(const auto &loop_id : topsorted_loops)
567  {
568  auto inferred_loop_assigns =
569  inferred_loop_assigns_map[loop_nesting_graph[loop_id].latch->loop_number];
570  loop_info_map.insert(
571  {loop_id,
573  loop_nesting_graph,
574  loop_id,
575  function_id,
578  dirty,
579  inferred_loop_assigns,
580  loop_contract_config.check_side_effect,
581  message_handler,
582  library,
583  symbol_table)});
584 
585  if(loop_nesting_graph.get_successors(loop_id).empty())
586  top_level_loops.push_back(loop_id);
587  }
588 
589  // generate set of top level of locals
590  top_level_local.insert(
593 
594  for(auto target = goto_function.body.instructions.begin();
595  target != goto_function.body.instructions.end();
596  target++)
597  {
598  if(target->is_decl() && dfcc_is_loop_top_level(target))
599  top_level_local.insert(target->decl_symbol().get_identifier());
600  }
601 
604 }
605 
606 void dfcc_cfg_infot::output(std::ostream &out) const
607 {
608  out << "// dfcc_cfg_infot for: " << function_id << "\n";
609  out << "// top_level_local: {";
610  for(auto &id : top_level_local)
611  {
612  out << id << ", ";
613  }
614  out << "}\n";
615 
616  out << "// top_level_tracked: {";
617  for(auto &id : top_level_tracked)
618  {
619  out << id << ", ";
620  }
621  out << "}\n";
622 
623  out << "// loop:\n";
624  for(auto &loop : loop_info_map)
625  {
626  out << "// dfcc-loop_id:" << loop.first << "\n";
627  auto head = loop.second.find_head(goto_function.body);
628  auto latch = loop.second.find_latch(goto_function.body);
629  out << "// head:\n";
630  head.value()->output(out);
631  out << "// latch:\n";
632  latch.value()->output(out);
633  loop.second.output(out);
634  }
635  out << "// program:\n";
637  {
638  out << "// dfcc-loop-id:" << dfcc_get_loop_id(target).value();
639  out << " cbmc-loop-number:" << target->loop_number;
640  out << " top-level:" << dfcc_is_loop_top_level(target);
641  out << " head:" << dfcc_is_loop_head(target);
642  out << " body:" << dfcc_is_loop_body(target);
643  out << " exiting:" << dfcc_is_loop_exiting(target);
644  out << " latch:" << dfcc_is_loop_latch(target);
645  out << "\n";
646  target->output(out);
647  }
648 }
649 
651  const std::size_t loop_id) const
652 {
653  if(is_top_level_id(loop_id) || !get_loop_info(loop_id).must_skip())
654  {
655  return loop_id;
656  }
658  get_outer_loop_identifier(loop_id).value_or(top_level_id()));
659 }
660 
661 const exprt &
663 {
664  auto loop_id_opt = dfcc_get_loop_id(target);
665  PRECONDITION(
666  loop_id_opt.has_value() &&
667  is_valid_loop_or_top_level_id(loop_id_opt.value()));
668  auto loop_id = get_first_id_not_skipped_or_top_level_id(loop_id_opt.value());
669  if(is_top_level_id(loop_id))
670  {
671  return top_level_write_set;
672  }
673  else
674  {
675  return loop_info_map.at(loop_id).addr_of_write_set_var;
676  }
677 }
678 
679 const std::unordered_set<irep_idt> &
681 {
682  auto loop_id_opt = dfcc_get_loop_id(target);
683  PRECONDITION(
684  loop_id_opt.has_value() &&
685  is_valid_loop_or_top_level_id(loop_id_opt.value()));
686  auto loop_id = loop_id_opt.value();
687  if(is_top_level_id(loop_id))
688  {
689  return top_level_tracked;
690  }
691  else
692  {
693  return loop_info_map.at(loop_id).tracked;
694  }
695 }
696 
697 const std::unordered_set<irep_idt> &
699 {
700  auto loop_id_opt = dfcc_get_loop_id(target);
701  PRECONDITION(
702  loop_id_opt.has_value() &&
703  is_valid_loop_or_top_level_id(loop_id_opt.value()));
704  auto loop_id = loop_id_opt.value();
705  if(is_top_level_id(loop_id))
706  {
707  return top_level_local;
708  }
709  else
710  {
711  return loop_info_map.at(loop_id).local;
712  }
713 }
714 
715 const exprt &dfcc_cfg_infot::get_outer_write_set(std::size_t loop_id) const
716 {
717  PRECONDITION(is_valid_loop_id(loop_id));
718  auto outer_loop_opt = get_outer_loop_identifier(loop_id);
719  return outer_loop_opt.has_value()
720  ? get_loop_info(outer_loop_opt.value()).addr_of_write_set_var
722 }
723 
724 const dfcc_loop_infot &
725 dfcc_cfg_infot::get_loop_info(const std::size_t loop_id) const
726 {
727  return loop_info_map.at(loop_id);
728 }
729 
730 // find the identifier or the immediately enclosing loop in topological order
731 const std::optional<std::size_t>
732 dfcc_cfg_infot::get_outer_loop_identifier(const std::size_t loop_id) const
733 {
734  PRECONDITION(is_valid_loop_id(loop_id));
735  auto outer_loops = get_loop_info(loop_id).outer_loops;
736 
737  // find the first loop in the topological order that is connected
738  // to our node.
739  for(const auto &idx : get_loops_toposorted())
740  {
741  if(
742  std::find(outer_loops.begin(), outer_loops.end(), idx) !=
743  outer_loops.end())
744  {
745  return idx;
746  }
747  }
748  // return nullopt for loops that are not nested in other loops
749  return std::nullopt;
750 }
751 
752 bool dfcc_cfg_infot::is_valid_loop_or_top_level_id(const std::size_t id) const
753 {
754  return id <= loop_info_map.size();
755 }
756 
757 bool dfcc_cfg_infot::is_valid_loop_id(const std::size_t id) const
758 {
759  return id < loop_info_map.size();
760 }
761 
762 bool dfcc_cfg_infot::is_top_level_id(const std::size_t id) const
763 {
764  return id == loop_info_map.size();
765 }
766 
768 {
769  return loop_info_map.size();
770 }
771 
773  goto_programt::const_targett target) const
774 {
775  PRECONDITION(target->is_decl() || target->is_dead());
776  auto &ident = target->is_decl() ? target->decl_symbol().get_identifier()
777  : target->dead_symbol().get_identifier();
778  auto &tracked = get_tracked_set(target);
779  return tracked.find(ident) != tracked.end();
780 }
781 
787  const exprt &lhs,
788  const std::unordered_set<irep_idt> &local,
789  const std::unordered_set<irep_idt> &tracked)
790 {
791  auto root_objects = dfcc_root_objects(lhs);
792 
793  // Check wether all root_objects can be resolved to actual identifiers.
794  std::unordered_set<irep_idt> root_idents;
795  for(const auto &expr : root_objects)
796  {
797  if(expr.id() != ID_symbol)
798  {
799  // This means that lhs contains either an address-of operation or a
800  // dereference operation, and we cannot really know statically which
801  // object it refers to without using the may_alias analysis.
802  // Since the may_alias analysis is also used to infer targets, for
803  // soundness reasons we cannot also use it to skip checks, so we check
804  // the assignment. If happens to assign to a mix of tracked and
805  // non-tracked identifiers the check will fail but this is sound anyway.
806  return true;
807  }
808  const auto &id = to_symbol_expr(expr).get_identifier();
810  {
811  // Skip the check if we have a single cprover symbol as root object
812  // cprover symbols are used for generic checks instrumentation and are
813  // de-facto ghost code. We implicitly allow assignments to these symbols.
814  // To make this really sound we should use a white list of known
815  // CPROVER symbols, because right now simply naming a symbol with the
816  // CPROVER prefix bypasses the checks.
817  if(root_objects.size() == 1)
818  {
819  return false;
820  }
821  else
822  {
823  // error out if we have a cprover symbol and something else in the set
824  throw analysis_exceptiont(
825  "LHS expression `" + format_to_string(lhs) +
826  "` in assignment refers to a cprover symbol and something else.");
827  }
828  }
829  root_idents.insert(id);
830  }
831 
832  // The root idents set is Non-empty.
833  // true iff root_idents contains non-local idents
834  bool some_non_local = false;
835  // true iff root_idents contains some local that is not tracked
836  bool some_local_not_tracked = false;
837  // true iff root_idents contains only local that are not tracked
838  bool all_local_not_tracked = true;
839  // true iff root_idents contains only local that are tracked
840  bool all_local_tracked = true;
841  for(const auto &root_ident : root_idents)
842  {
843  bool loc = local.find(root_ident) != local.end();
844  bool tra = tracked.find(root_ident) != tracked.end();
845  bool local_tracked = loc && tra;
846  bool local_not_tracked = loc && !tra;
847  some_non_local |= !loc;
848  some_local_not_tracked |= local_not_tracked;
849  all_local_not_tracked &= local_not_tracked;
850  all_local_tracked &= local_tracked;
851  }
852 
853  // some root identifier is not local, the lhs must be checked
854  if(some_non_local)
855  {
856  // if we also have a local that is not tracked, we know the check will
857  // fail with the current algorithm, error out.
858  if(some_local_not_tracked)
859  {
860  throw analysis_exceptiont(
861  "LHS expression `" + format_to_string(lhs) +
862  "` in assignment mentions both explicitly and implicitly tracked "
863  "memory locations. DFCC does not yet handle that case, please "
864  "reformulate the assignment into separate assignments to either "
865  "memory locations.");
866  }
867  return true;
868  }
869  else
870  {
871  // all root identifiers are local
872  // if they are all not tracked, we *have* to skip the check
873  // (and it is sound to do so, because we know that the identifiers that
874  // are not tracked explicitly are not dirty and not assigned to outside of
875  // their scope).
876  // if they are all tracked, we *can* skip the check, because they are all
877  // local to that scope anyway and implicitly allowed.
878  if(all_local_not_tracked || all_local_tracked)
879  {
880  return false;
881  }
882  else
883  {
884  // we have a combination of tracked and not-tracked locals, we know
885  // the check will fail with the current algorithm, error out.
886  throw analysis_exceptiont(
887  "LHS expression `" + format_to_string(lhs) +
888  "` in assignment mentions both explicitly and implicitly tracked "
889  "memory locations. DFCC does not yet handle that case, please "
890  "reformulate the assignment into separate assignments to either "
891  "memory locations.");
892  }
893  }
894 }
895 
897 {
898  PRECONDITION(target->is_assign() || target->is_function_call());
899  const exprt &lhs =
900  target->is_assign() ? target->assign_lhs() : target->call_lhs();
901  if(lhs.is_nil())
902  return false;
904  lhs, get_local_set(target), get_tracked_set(target));
905 }
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
const std::optional< std::size_t > get_outer_loop_identifier(const std::size_t loop_id) const
Finds the DFCC id of the loop that contains the given loop, returns nullopt when the loop has no oute...
const std::vector< std::size_t > & get_loops_toposorted() const
std::unordered_set< irep_idt > top_level_local
Set of identifiers DECL at top level.
const exprt & top_level_write_set
std::size_t get_first_id_not_skipped_or_top_level_id(const std::size_t loop_id) const
Returns the id of the first outer loop (including this one) that is not skipped, or the top level id.
const namespacet ns
std::vector< std::size_t > topsorted_loops
Loop identifiers sorted from most deeply nested to less deeply nested.
std::unordered_set< irep_idt > top_level_tracked
Set of identifiers DECL at top level.
bool is_top_level_id(const std::size_t id) const
True iff id is in the valid range for a loop id for this function.
const dfcc_loop_infot & get_loop_info(const std::size_t loop_id) const
Returns the loop info for that loop_id.
void output(std::ostream &out) const
goto_functiont & goto_function
std::vector< std::size_t > top_level_loops
Loop identifiers for top level loops (ie for loops that are not nested in in another loop).
const std::unordered_set< irep_idt > & get_tracked_set(goto_programt::const_targett target) const
Returns the subset of local variable that are explicitly tracked in the write set for the scope where...
dfcc_cfg_infot(goto_modelt &goto_model, const irep_idt &function_id, goto_functiont &goto_function, const exprt &top_level_write_set, const loop_contract_configt &loop_contract_config, symbol_table_baset &symbol_table, message_handlert &message_handler, dfcc_libraryt &library)
bool must_check_lhs(goto_programt::const_targett target) const
True iff the lhs of an assignment must be checked against the ambient write set.
const std::unordered_set< irep_idt > & get_local_set(goto_programt::const_targett target) const
Returns the set of local variable for the scope where that target instruction is found.
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...
const exprt & get_write_set(goto_programt::const_targett target) const
Returns the write set variable to use for the given instruction Returns the write set for the loop,...
bool must_track_decl_or_dead(goto_programt::const_targett target) const
True iff a DECL ident must be tracked in the write set of the loop that contains the DECL.
size_t top_level_id() const
Returns the top level ID.
bool is_valid_loop_id(const std::size_t id) const
True iff id is in the valid range for a loop id for this function.
const irep_idt & function_id
std::map< std::size_t, dfcc_loop_infot > loop_info_map
Map from loop identifier to loop info struct.
bool is_valid_loop_or_top_level_id(const std::size_t id) const
True iff id is in the valid range for a loop id or is equal to the top level id for this function.
Class interface to library types and functions defined in cprover_contracts.c.
Definition: dfcc_library.h:154
std::map< dfcc_typet, typet > dfcc_type
Maps enum values to the actual types (dynamically loaded)
Definition: dfcc_library.h:214
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.
void output(std::ostream &out) const
Prints a textual representation of the struct to out.
const exprt::operandst decreases
Decreases clause expression.
const std::unordered_set< irep_idt > local
Set of local identifiers locally DECL in loop instructions, excluding identifiers declared in nested ...
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 std::unordered_set< irep_idt > tracked
Subset of locals that must be tracked in the loop's write set.
const std::size_t loop_id
Loop identifier assigned by DFCC to this loop.
const exprt invariant
Loop invariant expression.
const std::set< std::size_t > outer_loops
Integer identifier of the outer loop(s) if they exists.
const std::set< std::size_t > inner_loops
Integer identifiers of inner loops of that loop.
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.
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
Definition: dirty.h:28
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
operandst & operands()
Definition: expr.h:94
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
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
Definition: goto_function.h:33
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
instructionst::iterator targett
Definition: goto_program.h:614
instructionst::const_iterator const_targett
Definition: goto_program.h:615
A generic directed graph with a parametric node type.
Definition: graph.h:167
std::vector< node_indext > get_predecessors(const node_indext &n) const
Definition: graph.h:943
std::size_t size() const
Definition: graph.h:212
std::vector< node_indext > get_successors(const node_indext &n) const
Definition: graph.h:956
std::list< node_indext > topsort() const
Find a topological order of the nodes if graph is DAG, return empty list for non-DAG or empty graph.
Definition: graph.h:879
Thrown when we can't handle something in an input source file.
bool is_not_nil() const
Definition: irep.h:372
bool is_nil() const
Definition: irep.h:368
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
static eomt eom
Definition: message.h:289
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
The NIL expression.
Definition: std_expr.h:3081
const irep_idt & get_identifier() const
Definition: std_expr.h:160
The symbol table base class interface.
The Boolean constant true.
Definition: std_expr.h:3063
static bool is_assigned(dirtyt &dirty, const irep_idt &ident, assignst assigns)
static std::optional< goto_programt::targett > check_inner_loops_have_contracts(const dfcc_loop_nesting_grapht &loop_nesting_graph, const bool check_side_effect)
Traverses the loop nesting graph from top level loops and checks if all loops nested in loops that ha...
static bool has_contract(const goto_programt::const_targett &latch_target, const bool check_side_effect)
Returns true iff some contract clause expression is attached to the latch condition of this loop.
static void tag_loop_instructions(goto_programt &goto_program, dfcc_loop_nesting_grapht &loop_nesting_graph)
Tags instructions of loops found in loop_nesting_graph with the loop identifier of the innermost loop...
static bool must_check_lhs_from_local_and_tracked(const exprt &lhs, const std::unordered_set< irep_idt > &local, const std::unordered_set< irep_idt > &tracked)
Returns true if the lhs to an assignment must be checked against its write set.
static struct contract_clausest default_loop_contract_clauses(const dfcc_loop_nesting_grapht &loop_nesting_graph, const std::size_t loop_id, const irep_idt &function_id, const assignst &inferred_assigns, const bool check_side_effect, message_handlert &message_handler, const namespacet &ns)
Generate defaults for all contract clauses of the loop with ID loop_id if at least one type of clause...
static std::unordered_set< irep_idt > gen_tracked_set(const std::vector< std::size_t > &inner_loops_ids, const std::unordered_set< irep_idt > &locals, dirtyt &dirty, const std::map< std::size_t, dfcc_loop_infot > &loop_info_map)
Compute subset of locals that must be tracked in the loop's write set.
static dfcc_loop_infot gen_dfcc_loop_info(const dfcc_loop_nesting_grapht &loop_nesting_graph, const std::size_t loop_id, const irep_idt &function_id, goto_functiont &goto_function, const std::map< std::size_t, dfcc_loop_infot > &loop_info_map, dirtyt &dirty, const assignst &inferred_assigns, const bool check_side_effect, message_handlert &message_handler, dfcc_libraryt &library, symbol_table_baset &symbol_table)
static std::optional< goto_programt::targett > check_has_contract_rec(const dfcc_loop_nesting_grapht &loop_nesting_graph, const std::size_t loop_idx, const bool must_have_contract, const bool check_side_effect)
Class that computes CFG information about the loop structure of a GOTO function for the purpose of dy...
void dfcc_check_loop_normal_form(goto_programt &goto_program, messaget &log)
Checks and enforces normal form properties for natural loops of the given goto_program.
Checks normal form properties of natural loops in a GOTO program.
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.
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...
Infer a set of assigns clause targets for a natural loop.
bool dfcc_is_cprover_static_symbol(const irep_idt &id)
Returns true iff the symbol is one of the known CPROVER static instrumentation variables or ends with...
Dynamic frame condition checking library loading.
@ WRITE_SET
type of descriptors of assignable/freeable sets of locations
@ WRITE_SET_PTR
type of pointers to descriptors of assignable/freeable sets of locations
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.
bool dfcc_has_loop_id(const goto_programt::instructiont::const_targett &target, std::size_t loop_id)
void dfcc_set_loop_exiting(goto_programt::instructiont::targett &target)
void dfcc_set_loop_latch(goto_programt::instructiont::targett &target)
bool dfcc_is_loop_head(const goto_programt::instructiont::const_targett &target)
bool dfcc_is_loop_latch(const goto_programt::instructiont::const_targett &target)
bool dfcc_is_loop_top_level(const goto_programt::instructiont::const_targett &target)
void dfcc_set_loop_top_level(goto_programt::instructiont::targett &target)
void dfcc_set_loop_body(goto_programt::instructiont::targett &target)
std::optional< std::size_t > dfcc_get_loop_id(const goto_programt::instructiont::const_targett &target)
void dfcc_set_loop_id(goto_programt::instructiont::targett &target, const std::size_t loop_id)
bool dfcc_is_loop_exiting(const goto_programt::instructiont::const_targett &target)
bool dfcc_is_loop_body(const goto_programt::instructiont::const_targett &target)
void dfcc_set_loop_head(goto_programt::instructiont::targett &target)
Functions that allow to tag GOTO instructions with loop identifiers and loop instruction type: head,...
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...
Dynamic frame condition checking utility functions.
std::string format_to_string(const T &o)
Definition: format.h:43
static format_containert< T > format(const T &o)
Definition: format.h:37
Fresh auxiliary symbol creation.
#define Forall_goto_program_instructions(it, program)
std::set< exprt > assignst
Definition: havoc_utils.h:22
Field-insensitive, location-sensitive may-alias analysis.
double log(double x)
Definition: math.c:2776
Compute natural loops in a goto_function.
API to expression classes for Pointers.
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:83
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.
exprt::operandst decreases_clauses
contract_clausest(const exprt::operandst &decreases)
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
Loop contract configurations.
exprt get_loop_assigns(const goto_programt::const_targett &loop_end)
Extract loop assigns from annotated loop end.
Definition: utils.cpp:683
void simplify_gotos(goto_programt &goto_program, const namespacet &ns)
Turns goto instructions IF cond GOTO label where the condition statically simplifies to false into SK...
Definition: utils.cpp:260
exprt get_loop_invariants(const goto_programt::const_targett &loop_end, const bool check_side_effect)
Extract loop invariants from annotated loop end.
Definition: utils.cpp:666
exprt get_loop_decreases(const goto_programt::const_targett &loop_end, const bool check_side_effect)
Extract loop decreases from annotated loop end.
Definition: utils.cpp:688