CBMC
utils.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Utility functions for code contracts.
4 
5 Author: Saswat Padhi, saspadhi@amazon.com
6 
7 Date: September 2021
8 
9 \*******************************************************************/
10 
11 #include "utils.h"
12 
13 #include <util/c_types.h>
14 #include <util/fresh_symbol.h>
15 #include <util/graph.h>
16 #include <util/mathematical_expr.h>
17 #include <util/message.h>
18 #include <util/pointer_expr.h>
21 #include <util/prefix.h>
22 #include <util/simplify_expr.h>
23 #include <util/symbol.h>
24 
25 #include <goto-programs/cfg.h>
26 
27 #include <analyses/natural_loops.h>
28 #include <ansi-c/c_expr.h>
29 #include <langapi/language_util.h>
30 
32  const source_locationt location,
33  const namespacet &ns,
34  const exprt &expr,
35  goto_programt &dest,
36  const std::function<void()> &havoc_code_impl)
37 {
38  goto_programt skip_program;
39  const auto skip_target = skip_program.add(goto_programt::make_skip(location));
40 
41  // skip havocing only if all pointer derefs in the expression are valid
42  // (to avoid spurious pointer deref errors)
44  skip_target,
46  location));
47 
48  havoc_code_impl();
49 
50  // add the final skip target
51  dest.destructive_append(skip_program);
52 }
53 
55  const source_locationt location,
56  const exprt &ptr,
57  const exprt &size,
58  goto_programt &dest)
59 {
61  location,
62  ns,
63  ptr,
64  dest,
65  // clang-format off
66  [&]() {
67  symbol_exprt function{CPROVER_PREFIX "havoc_slice", empty_typet()};
68  function.add_source_location() = location;
69  // havoc slice is lowered to array operations during goto conversion
70  // so we use goto_convertt directly as provided by clearnert
71  cleaner.do_havoc_slice(function, {ptr, size}, dest, mode);
72  });
73  // clang-format on
74 }
75 
77  const source_locationt location,
78  const exprt &ptr_to_ptr,
79  goto_programt &dest)
80 {
81  append_safe_havoc_code_for_expr(location, ns, ptr_to_ptr, dest, [&]() {
82  auto ptr = dereference_exprt(ptr_to_ptr);
84  ptr, side_effect_expr_nondett(ptr.type(), location), location));
85  });
86 }
87 
89  const source_locationt location,
90  const exprt &expr,
91  goto_programt &dest) const
92 {
93  append_safe_havoc_code_for_expr(location, ns, expr, dest, [&]() {
95  });
96 }
97 
99  const source_locationt location,
100  const exprt &expr,
101  goto_programt &dest) const
102 {
103  append_safe_havoc_code_for_expr(location, ns, expr, dest, [&]() {
105  });
106 }
107 
109  const source_locationt location,
110  const exprt &expr,
111  goto_programt &dest)
112 {
113  if(expr.id() == ID_pointer_object)
114  {
115  // pointer_object is still used internally to support malloc/free
117  location, to_pointer_object_expr(expr).pointer(), dest);
118  return;
119  }
121  {
122  const auto &funcall = to_side_effect_expr_function_call(expr);
123  // type-checking ensures the function expression is necessarily a symbol
124  const auto &ident = to_symbol_expr(funcall.function()).get_identifier();
125  if(ident == CPROVER_PREFIX "object_whole")
126  {
128  location, funcall.arguments().at(0), dest);
129  }
130  else if(ident == CPROVER_PREFIX "object_from")
131  {
132  const auto ptr = typecast_exprt::conditional_cast(
133  funcall.arguments().at(0), pointer_type(char_type()));
134 
135  exprt obj_size = object_size(ptr);
136  minus_exprt size{
137  obj_size,
139 
140  append_havoc_slice_code(expr.source_location(), ptr, size, dest);
141  }
142  else if(ident == CPROVER_PREFIX "object_upto")
143  {
144  const auto ptr = typecast_exprt::conditional_cast(
145  funcall.arguments().at(0), pointer_type(char_type()));
146  const auto size = typecast_exprt::conditional_cast(
147  funcall.arguments().at(1), size_type());
148  append_havoc_slice_code(expr.source_location(), ptr, size, dest);
149  }
150  else if(ident == CPROVER_PREFIX "assignable")
151  {
152  const auto &ptr = funcall.arguments().at(0);
153  const auto &size = funcall.arguments().at(1);
154  if(funcall.arguments().at(2).is_true())
155  {
156  append_havoc_pointer_code(expr.source_location(), ptr, dest);
157  }
158  else
159  {
160  append_havoc_slice_code(expr.source_location(), ptr, size, dest);
161  }
162  }
163  else
164  {
165  UNREACHABLE;
166  }
167  }
168  else
169  {
170  // we have an lvalue expression, make nondet assignment
171  havoc_utilst::append_havoc_code_for_expr(location, expr, dest);
172  }
173 }
174 
176 {
177  exprt::operandst validity_checks;
178 
179  if(auto deref = expr_try_dynamic_cast<dereference_exprt>(expr))
180  {
181  const auto size_of_expr_opt = size_of_expr(expr.type(), ns);
182  CHECK_RETURN(size_of_expr_opt.has_value());
183 
184  validity_checks.push_back(r_ok_exprt{deref->pointer(), *size_of_expr_opt});
185  }
186 
187  for(const auto &op : expr.operands())
188  validity_checks.push_back(all_dereferences_are_valid(op, ns));
189 
190  return conjunction(validity_checks);
191 }
192 
194  const std::vector<symbol_exprt> &lhs,
195  const std::vector<symbol_exprt> &rhs)
196 {
197  PRECONDITION(lhs.size() == rhs.size());
198 
199  if(lhs.empty())
200  {
201  return false_exprt();
202  }
203 
204  // Store conjunctions of equalities.
205  // For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
206  // l2, l3>.
207  // Then this vector stores <s1 == l1, s1 == l1 && s2 == l2,
208  // s1 == l1 && s2 == l2 && s3 == l3>.
209  // In fact, the last element is unnecessary, so we do not create it.
210  exprt::operandst equality_conjunctions(lhs.size());
211  equality_conjunctions[0] = binary_relation_exprt(lhs[0], ID_equal, rhs[0]);
212  for(size_t i = 1; i < equality_conjunctions.size() - 1; i++)
213  {
214  binary_relation_exprt component_i_equality{lhs[i], ID_equal, rhs[i]};
215  equality_conjunctions[i] =
216  and_exprt(equality_conjunctions[i - 1], component_i_equality);
217  }
218 
219  // Store inequalities between the i-th components of the input vectors
220  // (i.e. lhs and rhs).
221  // For example, suppose that the two input vectors are <s1, s2, s3> and <l1,
222  // l2, l3>.
223  // Then this vector stores <s1 < l1, s1 == l1 && s2 < l2, s1 == l1 &&
224  // s2 == l2 && s3 < l3>.
225  exprt::operandst lexicographic_individual_comparisons(lhs.size());
226  lexicographic_individual_comparisons[0] =
227  binary_relation_exprt(lhs[0], ID_lt, rhs[0]);
228  for(size_t i = 1; i < lexicographic_individual_comparisons.size(); i++)
229  {
230  binary_relation_exprt component_i_less_than{lhs[i], ID_lt, rhs[i]};
231  lexicographic_individual_comparisons[i] =
232  and_exprt(equality_conjunctions[i - 1], component_i_less_than);
233  }
234  return disjunction(lexicographic_individual_comparisons);
235 }
236 
238  goto_programt &destination,
239  goto_programt::targett &target,
240  goto_programt &payload)
241 {
242  const auto offset = payload.instructions.size();
243  destination.insert_before_swap(target, payload);
244  std::advance(target, offset);
245 }
246 
248  goto_programt &destination,
249  goto_programt::targett &target,
251 {
252  const auto new_target = destination.insert_before(target, i);
253  for(auto it : target->incoming_edges)
254  {
255  if(it->is_goto() && it->get_target() == target)
256  it->set_target(new_target);
257  }
258 }
259 
260 void simplify_gotos(goto_programt &goto_program, const namespacet &ns)
261 {
262  for(auto &instruction : goto_program.instructions)
263  {
264  if(
265  instruction.is_goto() &&
266  simplify_expr(instruction.condition(), ns).is_false())
267  instruction.turn_into_skip();
268  }
269 }
270 
272  const goto_programt &goto_program,
273  const namespacet &ns,
274  messaget &log)
275 {
276  // create cfg from instruction list
278  cfg(goto_program);
279 
280  // check that all nodes are there
281  INVARIANT(
282  goto_program.instructions.size() == cfg.size(),
283  "Instruction list vs CFG size mismatch.");
284 
285  // compute SCCs
287  std::vector<idxt> node_to_scc(cfg.size(), -1);
288  auto nof_sccs = cfg.SCCs(node_to_scc);
289 
290  // compute size of each SCC
291  std::vector<int> scc_size(nof_sccs, 0);
292  for(auto scc : node_to_scc)
293  {
294  INVARIANT(
295  0 <= scc && scc < nof_sccs, "Could not determine SCC for instruction");
296  scc_size[scc]++;
297  }
298 
299  // check they are all of size 1
300  for(size_t scc_id = 0; scc_id < nof_sccs; scc_id++)
301  {
302  auto size = scc_size[scc_id];
303  if(size > 1)
304  {
305  log.conditional_output(
306  log.error(),
307  [&cfg, &node_to_scc, &scc_id, &size](messaget::mstreamt &mstream) {
308  mstream << "Found CFG SCC with size " << size << messaget::eom;
309  for(const auto &node_id : node_to_scc)
310  {
311  if(node_to_scc[node_id] == scc_id)
312  {
313  const auto &pc = cfg[node_id].PC;
314  pc->output(mstream);
315  mstream << messaget::eom;
316  }
317  }
318  });
319  return false;
320  }
321  }
322  return true;
323 }
324 
327  " (assigned by the contract of ";
328 
330  const exprt &target,
331  const irep_idt &function_id,
332  const namespacet &ns)
333 {
334  return from_expr(ns, target.id(), target) +
335  ASSIGNS_CLAUSE_REPLACEMENT_TRACKING + id2string(function_id) + ")";
336 }
337 
339 {
341  std::string::npos;
342 }
343 
345  const local_may_aliast &local_may_alias,
346  const loopt &loop,
347  assignst &assigns)
348 {
349  // Assign targets should not include cprover symbols.
350  get_assigns(local_may_alias, loop, assigns, [](const exprt &e) {
351  if(e.id() == ID_symbol)
352  {
353  const auto &s = expr_try_dynamic_cast<symbol_exprt>(e);
354  return !has_prefix(id2string(s->get_identifier()), CPROVER_PREFIX);
355  }
356  return true;
357  });
358 }
359 
360 void widen_assigns(assignst &assigns, const namespacet &ns)
361 {
362  assignst result;
363 
365 
366  for(const auto &e : assigns)
367  {
368  if(e.id() == ID_index || e.id() == ID_dereference)
369  {
370  address_of_exprt address_of_expr(e);
371 
372  // index or offset is non-constant.
373  if(!is_constant(address_of_expr))
374  {
375  result.emplace(pointer_object(address_of_expr));
376  }
377  else
378  result.emplace(e);
379  }
380  else
381  result.emplace(e);
382  }
383  assigns = result;
384 }
385 
387  symbol_table_baset &symbol_table,
388  exprt &expr,
389  std::unordered_map<exprt, symbol_exprt, irep_hash> &parameter2history,
390  const source_locationt &location,
391  const irep_idt &mode,
392  goto_programt &history,
393  const irep_idt &history_id)
394 {
395  for(auto &op : expr.operands())
396  {
398  symbol_table, op, parameter2history, location, mode, history, history_id);
399  }
400 
401  if(expr.id() != ID_old && expr.id() != ID_loop_entry)
402  return;
403 
404  const auto &parameter = to_history_expr(expr, history_id).expression();
405  const auto &id = parameter.id();
407  id == ID_dereference || id == ID_member || id == ID_symbol ||
408  id == ID_ptrmember || id == ID_constant || id == ID_typecast ||
409  id == ID_index,
410  "Tracking history of " + id2string(id) +
411  " expressions is not supported yet.",
412  parameter.pretty());
413 
414  // speculatively insert a dummy, which will be replaced below if the insert
415  // actually happened
416  auto entry =
417  parameter2history.insert({parameter, symbol_exprt::typeless(ID_nil)});
418 
419  if(entry.second)
420  {
421  // 1. Create a temporary symbol expression that represents the
422  // history variable
423  entry.first->second = get_fresh_aux_symbol(
424  parameter.type(),
425  id2string(location.get_function()),
426  "tmp_cc",
427  location,
428  mode,
429  symbol_table)
430  .symbol_expr();
431 
432  // 2. Add the required instructions to the instructions list
433  // 2.1. Declare the newly created temporary variable
434  history.add(goto_programt::make_decl(entry.first->second, location));
435 
436  // 2.2. Skip storing the history if the expression is invalid
437  auto goto_instruction = history.add(goto_programt::make_incomplete_goto(
439  all_dereferences_are_valid(parameter, namespacet(symbol_table))),
440  location));
441 
442  // 2.3. Add an assignment such that the value pointed to by the new
443  // temporary variable is equal to the value of the corresponding
444  // parameter
445  history.add(
446  goto_programt::make_assignment(entry.first->second, parameter, location));
447 
448  // 2.4. Complete conditional jump for invalid-parameter case
449  auto label_instruction = history.add(goto_programt::make_skip(location));
450  goto_instruction->complete_goto(label_instruction);
451  }
452 
453  expr = entry.first->second;
454 }
455 
457  symbol_table_baset &symbol_table,
458  const exprt &expr,
459  const source_locationt &location,
460  const irep_idt &mode)
461 {
463  result.expression_after_replacement = expr;
465  symbol_table,
467  result.parameter_to_history,
468  location,
469  mode,
470  result.history_construction,
471  ID_old);
472  return result;
473 }
474 
476  symbol_table_baset &symbol_table,
477  const exprt &expr,
478  const source_locationt &location,
479  const irep_idt &mode)
480 {
482  result.expression_after_replacement = expr;
484  symbol_table,
486  result.parameter_to_history,
487  location,
488  mode,
489  result.history_construction,
490  ID_loop_entry);
491  return result;
492 }
493 
495  symbol_table_baset &symbol_table,
496  exprt &clause,
497  const irep_idt &mode,
498  goto_programt &program)
499 {
500  // Find and replace "old" expression in the "expression" variable
501  auto result =
502  replace_history_old(symbol_table, clause, clause.source_location(), mode);
503  clause.swap(result.expression_after_replacement);
504  // Add all the history variable initialization instructions
505  program.destructive_append(result.history_construction);
506 }
507 
509 {
510  // The head of a transformed loop is
511  // ASSIGN entered_loop = false
513  target->assign_rhs() == false_exprt();
514 }
515 
517 {
518  // The end of a transformed loop is
519  // ASSIGN entered_loop = true
521  target->assign_rhs() == true_exprt();
522 }
523 
525  const goto_programt::const_targett &target,
526  std::string var_name)
527 {
528  INVARIANT(
529  var_name == IN_BASE_CASE || var_name == ENTERED_LOOP ||
530  var_name == IN_LOOP_HAVOC_BLOCK,
531  "var_name is not of instrumented variables.");
532 
533  if(!target->is_assign())
534  return false;
535 
536  if(can_cast_expr<symbol_exprt>(target->assign_lhs()))
537  {
538  const auto &lhs = to_symbol_expr(target->assign_lhs());
539  return id2string(lhs.get_identifier()).find("::" + var_name) !=
540  std::string::npos;
541  }
542 
543  return false;
544 }
545 
546 unsigned get_suffix_unsigned(const std::string &str, const std::string &prefix)
547 {
548  // first_index is the end of the `prefix`.
549  auto first_index = str.find(prefix);
550  INVARIANT(
551  first_index != std::string::npos, "Prefix not found in the given string");
552  first_index += prefix.length();
553 
554  // last_index is the index of not-digit.
555  auto last_index = str.find_first_not_of("0123456789", first_index);
556  std::string result = str.substr(first_index, last_index - first_index);
557  return std::stol(result);
558 }
559 
561  const goto_programt::const_targett &loop_head,
562  const loop_templatet<
565 {
566  goto_programt::const_targett loop_end = loop_head;
567  for(const auto &t : loop)
568  {
569  // an instruction is the loop end if it is a goto instruction
570  // and it jumps backward to the loop head
571  if(
572  t->is_goto() && t->get_target() == loop_head &&
573  t->location_number > loop_end->location_number)
574  loop_end = t;
575  }
576  INVARIANT(
577  loop_head != loop_end,
578  "Could not find end of the loop starting at: " +
579  loop_head->source_location().as_string());
580 
581  return loop_end;
582 }
583 
585  const goto_programt::targett &loop_head,
587  &loop)
588 {
589  goto_programt::targett loop_end = loop_head;
590  for(const auto &t : loop)
591  {
592  // an instruction is the loop end if it is a goto instruction
593  // and it jumps backward to the loop head
594  if(
595  t->is_goto() && t->get_target() == loop_head &&
596  t->location_number > loop_end->location_number)
597  loop_end = t;
598  }
599  INVARIANT(
600  loop_head != loop_end,
601  "Could not find end of the loop starting at: " +
602  loop_head->source_location().as_string());
603 
604  return loop_end;
605 }
606 
608  const unsigned int target_loop_number,
609  goto_functiont &function,
610  bool finding_head)
611 {
612  natural_loops_mutablet natural_loops(function.body);
613 
614  // iterate over all natural loops to find the loop with `target_loop_number`
615  for(const auto &loop_p : natural_loops.loop_map)
616  {
617  const goto_programt::targett loop_head = loop_p.first;
618  goto_programt::targett loop_end =
619  get_loop_end_from_loop_head_and_content_mutable(loop_head, loop_p.second);
620  // check if the current loop is the target loop by comparing loop number
621  if(loop_end->loop_number == target_loop_number)
622  {
623  if(finding_head)
624  return loop_head;
625  else
626  return loop_end;
627  }
628  }
629 
630  UNREACHABLE;
631 }
632 
634 get_loop_end(const unsigned int target_loop_number, goto_functiont &function)
635 {
636  return get_loop_head_or_end(target_loop_number, function, false);
637 }
638 
640 get_loop_head(const unsigned int target_loop_number, goto_functiont &function)
641 {
642  return get_loop_head_or_end(target_loop_number, function, true);
643 }
644 
646 static exprt
648 {
649  return static_cast<const exprt &>(
650  loop_end->condition().find(ID_C_spec_loop_invariant));
651 }
652 
654 {
655  return static_cast<const exprt &>(
656  loop_end->condition().find(ID_C_spec_assigns));
657 }
658 
659 static exprt
661 {
662  return static_cast<const exprt &>(
663  loop_end->condition().find(ID_C_spec_decreases));
664 }
665 
667  const goto_programt::const_targett &loop_end,
668  const bool check_side_effect)
669 {
670  auto invariant = extract_loop_invariants(loop_end);
671  if(!invariant.is_nil() && check_side_effect)
672  {
673  if(has_subexpr(invariant, ID_side_effect))
674  {
676  "Loop invariant is not side-effect free.",
677  loop_end->condition().find_source_location());
678  }
679  }
680  return invariant;
681 }
682 
684 {
685  return extract_loop_assigns(loop_end);
686 }
687 
689  const goto_programt::const_targett &loop_end,
690  const bool check_side_effect)
691 {
692  auto decreases_clause = extract_loop_decreases(loop_end);
693  if(!decreases_clause.is_nil() && check_side_effect)
694  {
695  if(has_subexpr(decreases_clause, ID_side_effect))
696  {
698  "Decreases clause is not side-effect free.",
699  loop_end->condition().find_source_location());
700  }
701  }
702  return decreases_clause;
703 }
704 
706  const invariant_mapt &invariant_map,
707  goto_modelt &goto_model)
708 {
709  for(const auto &invariant_map_entry : invariant_map)
710  {
711  loop_idt loop_id = invariant_map_entry.first;
712  irep_idt function_id = loop_id.function_id;
713  unsigned int loop_number = loop_id.loop_number;
714 
715  // get the last instruction of the target loop
716  auto &function = goto_model.goto_functions.function_map[function_id];
717  goto_programt::targett loop_end = get_loop_end(loop_number, function);
718 
719  // annotate the invariant to the condition of `loop_end`
720  loop_end->condition_nonconst().add(ID_C_spec_loop_invariant) =
721  invariant_map_entry.second;
722  }
723 }
724 
726  const std::map<loop_idt, std::set<exprt>> &assigns_map,
727  goto_modelt &goto_model)
728 {
729  for(const auto &assigns_map_entry : assigns_map)
730  {
731  loop_idt loop_id = assigns_map_entry.first;
732  irep_idt function_id = loop_id.function_id;
733  unsigned int loop_number = loop_id.loop_number;
734 
735  // get the last instruction of the target loop
736  auto &function = goto_model.goto_functions.function_map[function_id];
737  goto_programt::targett loop_end = get_loop_end(loop_number, function);
738 
739  exprt &condition = loop_end->condition_nonconst();
740  auto assigns = exprt(ID_target_list);
741  for(const auto &e : assigns_map_entry.second)
742  assigns.add_to_operands(e);
743  condition.add(ID_C_spec_assigns) = assigns;
744  }
745 }
746 
748  const std::map<loop_idt, exprt> &assigns_map,
749  goto_modelt &goto_model)
750 {
751  for(const auto &assigns_map_entry : assigns_map)
752  {
753  loop_idt loop_id = assigns_map_entry.first;
754  irep_idt function_id = loop_id.function_id;
755  unsigned int loop_number = loop_id.loop_number;
756 
757  // get the last instruction of the target loop
758  auto &function = goto_model.goto_functions.function_map[function_id];
759  goto_programt::targett loop_end = get_loop_end(loop_number, function);
760 
761  exprt &condition = loop_end->condition_nonconst();
762  condition.add(ID_C_spec_assigns) = assigns_map_entry.second;
763  }
764 }
765 
767  const std::map<loop_idt, std::vector<exprt>> &decreases_map,
768  goto_modelt &goto_model)
769 {
770  for(const auto &decreases_map_entry : decreases_map)
771  {
772  loop_idt loop_id = decreases_map_entry.first;
773  irep_idt function_id = loop_id.function_id;
774  unsigned int loop_number = loop_id.loop_number;
775 
776  // get the last instruction of the target loop
777  auto &function = goto_model.goto_functions.function_map[function_id];
778  goto_programt::targett loop_end = get_loop_end(loop_number, function);
779 
780  exprt &condition = loop_end->condition_nonconst();
781  auto decreases = exprt(ID_target_list);
782  for(const auto &e : decreases_map_entry.second)
783  decreases.add_to_operands(e);
784  condition.add(ID_C_spec_decreases) = decreases;
785  }
786 }
API to expression classes that are internal to the C frontend.
const history_exprt & to_history_expr(const exprt &expr, const irep_idt &id)
Definition: c_expr.h:220
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:235
bitvector_typet char_type()
Definition: c_types.cpp:106
Control Flow Graph.
Operator to return the address of an object.
Definition: pointer_expr.h:540
Boolean AND.
Definition: std_expr.h:2125
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:762
void do_havoc_slice(const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
Definition: utils.h:54
Operator to dereference a pointer.
Definition: pointer_expr.h:834
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
The empty type.
Definition: std_types.h:51
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
const source_locationt & source_location() const
Definition: expr.h:231
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:34
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:3077
function_mapt function_map
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
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
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:643
instructionst::iterator targett
Definition: goto_program.h:614
instructionst::const_iterator const_targett
Definition: goto_program.h:615
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
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
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:692
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
std::size_t node_indext
Definition: graph.h:37
std::size_t SCCs(std::vector< node_indext > &subgraph_nr) const
Computes strongly-connected components of a graph and yields a vector expressing a mapping from nodes...
Definition: graph.h:832
std::size_t size() const
Definition: graph.h:212
void append_havoc_pointer_code(const source_locationt location, const exprt &ptr_to_ptr, goto_programt &dest)
Definition: utils.cpp:76
void append_havoc_slice_code(const source_locationt location, const exprt &ptr, const exprt &size, goto_programt &dest)
Definition: utils.cpp:54
const irep_idt & mode
Definition: utils.h:126
cleanert cleaner
Definition: utils.h:124
namespacet ns
Definition: utils.h:123
void append_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest)
Append goto instructions to havoc a single expression expr
Definition: utils.cpp:108
void append_object_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const override
Append goto instructions to havoc the underlying object of expr
Definition: utils.cpp:88
const namespacet & ns
Definition: utils.h:86
void append_scalar_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const override
Append goto instructions to havoc the value of expr
Definition: utils.cpp:98
A class containing utility functions for havocing expressions.
Definition: havoc_utils.h:28
virtual void append_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest)
Append goto instructions to havoc a single expression expr
Definition: havoc_utils.cpp:29
virtual void append_object_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const
Append goto instructions to havoc the underlying object of expr
Definition: havoc_utils.cpp:46
virtual void append_scalar_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const
Append goto instructions to havoc the value of expr
Definition: havoc_utils.cpp:57
const exprt & expression() const
Definition: c_expr.h:213
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
const irep_idt & id() const
Definition: irep.h:388
void swap(irept &irep)
Definition: irep.h:434
irept & add(const irep_idt &name)
Definition: irep.cpp:103
loop_mapt loop_map
Definition: loop_analysis.h:88
A loop, specified as a set of instructions.
Definition: loop_analysis.h:24
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
Binary minus.
Definition: std_expr.h:1061
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
A predicate that indicates that an address range is ok to read.
Definition: pointer_expr.h:960
const exprt & pointer() const
Definition: pointer_expr.h:927
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1520
const irep_idt & get_function() const
Expression to hold a symbol (variable)
Definition: std_expr.h:131
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:150
const irep_idt & get_identifier() const
Definition: std_expr.h:160
The symbol table base class interface.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
The Boolean constant true.
Definition: std_expr.h:3068
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2081
source_locationt & add_source_location()
Definition: type.h:77
#define CPROVER_PREFIX
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:115
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
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
A Template Class for Graphs.
std::set< exprt > assignst
Definition: havoc_utils.h:22
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
void get_assigns(const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns)
Definition: loop_utils.cpp:142
natural_loops_mutablet::natural_loopt loopt
Definition: loop_utils.h:20
double log(double x)
Definition: math.c:2776
API to expression classes for 'mathematical' expressions.
Compute natural loops in a goto_function.
API to expression classes for Pointers.
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
exprt pointer_offset(const exprt &pointer)
exprt object_size(const exprt &pointer)
exprt pointer_object(const exprt &p)
Various predicates over pointers in programs.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:108
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:535
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1739
bool can_cast_expr< side_effect_expr_function_callt >(const exprt &base)
Definition: std_code.h:1730
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
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:71
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition: std_expr.h:256
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition: std_types.h:29
A total order over targett and const_targett.
Definition: goto_program.h:392
Loop id used to identify loops.
Definition: loop_ids.h:28
irep_idt function_id
Definition: loop_ids.h:36
unsigned int loop_number
Definition: loop_ids.h:37
std::unordered_map< exprt, symbol_exprt, irep_hash > parameter_to_history
Definition: utils.h:238
goto_programt history_construction
Definition: utils.h:239
exprt expression_after_replacement
Definition: utils.h:237
Symbol table entry.
#define size_type
Definition: unistd.c:347
replace_history_parametert replace_history_old(symbol_table_baset &symbol_table, const exprt &expr, const source_locationt &location, const irep_idt &mode)
This function recursively identifies the "old" expressions within expr and replaces them with corresp...
Definition: utils.cpp:456
void generate_history_variables_initialization(symbol_table_baset &symbol_table, exprt &clause, const irep_idt &mode, goto_programt &program)
This function generates all the instructions required to initialize history variables.
Definition: utils.cpp:494
bool is_assignment_to_instrumented_variable(const goto_programt::const_targett &target, std::string var_name)
Return true if target is an assignment to an instrumented variable with name var_name.
Definition: utils.cpp:524
irep_idt make_assigns_clause_replacement_tracking_comment(const exprt &target, const irep_idt &function_id, const namespacet &ns)
Returns an irep_idt that essentially says that target was assigned by the contract of function_id.
Definition: utils.cpp:329
goto_programt::targett get_loop_end(const unsigned int target_loop_number, goto_functiont &function)
Find and return the last instruction of the natural loop with loop_number in function.
Definition: utils.cpp:634
static void append_safe_havoc_code_for_expr(const source_locationt location, const namespacet &ns, const exprt &expr, goto_programt &dest, const std::function< void()> &havoc_code_impl)
Definition: utils.cpp:31
goto_programt::const_targett get_loop_end_from_loop_head_and_content(const goto_programt::const_targett &loop_head, const loop_templatet< goto_programt::const_targett, goto_programt::target_less_than > &loop)
Definition: utils.cpp:560
void insert_before_and_update_jumps(goto_programt &destination, goto_programt::targett &target, const goto_programt::instructiont &i)
Insert a goto instruction before a target instruction iterator and update targets of all jumps that p...
Definition: utils.cpp:247
void infer_loop_assigns(const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns)
Infer loop assigns using alias analysis result local_may_alias.
Definition: utils.cpp:344
bool is_loop_free(const goto_programt &goto_program, const namespacet &ns, messaget &log)
Returns true iff the given program is loop-free, i.e.
Definition: utils.cpp:271
exprt get_loop_assigns(const goto_programt::const_targett &loop_end)
Extract loop assigns from annotated loop end.
Definition: utils.cpp:683
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
goto_programt::targett get_loop_head(const unsigned int target_loop_number, goto_functiont &function)
Find and return the first instruction of the natural loop with loop_number in function.
Definition: utils.cpp:640
bool is_transformed_loop_head(const goto_programt::const_targett &target)
Return true if target is the head of some transformed loop.
Definition: utils.cpp:508
exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns)
Generate a validity check over all dereferences in an expression.
Definition: utils.cpp:175
bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment)
Returns true if the given comment matches the type of comments created by make_assigns_clause_replace...
Definition: utils.cpp:338
void annotate_decreases(const std::map< loop_idt, std::vector< exprt >> &decreases_map, goto_modelt &goto_model)
Annotate the decreases in decreases_map to their corresponding loops.
Definition: utils.cpp:766
goto_programt::targett get_loop_head_or_end(const unsigned int target_loop_number, goto_functiont &function, bool finding_head)
Return loop head if finding_head is true, Otherwise return loop end.
Definition: utils.cpp:607
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
static exprt extract_loop_assigns(const goto_programt::const_targett &loop_end)
Definition: utils.cpp:653
void widen_assigns(assignst &assigns, const namespacet &ns)
Widen expressions in assigns with the following strategy.
Definition: utils.cpp:360
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
bool is_transformed_loop_end(const goto_programt::const_targett &target)
Return true if target is the end of some transformed loop.
Definition: utils.cpp:516
goto_programt::targett get_loop_end_from_loop_head_and_content_mutable(const goto_programt::targett &loop_head, const loop_templatet< goto_programt::targett, goto_programt::target_less_than > &loop)
Find the goto instruction of loop that jumps to loop_head
Definition: utils.cpp:584
void annotate_invariants(const invariant_mapt &invariant_map, goto_modelt &goto_model)
Annotate the invariants in invariant_map to their corresponding loops.
Definition: utils.cpp:705
void annotate_assigns(const std::map< loop_idt, std::set< exprt >> &assigns_map, goto_modelt &goto_model)
Annotate the assigns in assigns_map to their corresponding loops.
Definition: utils.cpp:725
static void replace_history_parameter_rec(symbol_table_baset &symbol_table, exprt &expr, std::unordered_map< exprt, symbol_exprt, irep_hash > &parameter2history, const source_locationt &location, const irep_idt &mode, goto_programt &history, const irep_idt &history_id)
Definition: utils.cpp:386
static const char ASSIGNS_CLAUSE_REPLACEMENT_TRACKING[]
Prefix for comments added to track assigns clause replacement.
Definition: utils.cpp:326
static exprt extract_loop_decreases(const goto_programt::const_targett &loop_end)
Definition: utils.cpp:660
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
unsigned get_suffix_unsigned(const std::string &str, const std::string &prefix)
Convert the suffix digits right after prefix of str into unsigned.
Definition: utils.cpp:546
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
static exprt extract_loop_invariants(const goto_programt::const_targett &loop_end)
Extract loop invariants from loop end without any checks.
Definition: utils.cpp:647
#define ENTERED_LOOP
Definition: utils.h:26
std::map< loop_idt, exprt > invariant_mapt
Definition: utils.h:31
#define IN_BASE_CASE
Definition: utils.h:25
#define IN_LOOP_HAVOC_BLOCK
Definition: utils.h:27