cprover
goto_program.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Program Transformation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_program.h"
13 
14 #include <iomanip>
15 
16 #include <util/base_type.h>
17 #include <util/expr_iterator.h>
18 #include <util/find_symbols.h>
19 #include <util/format_expr.h>
20 #include <util/format_type.h>
21 #include <util/invariant.h>
22 #include <util/pointer_expr.h>
23 #include <util/std_expr.h>
24 #include <util/symbol_table.h>
25 #include <util/validate.h>
26 
27 #include <langapi/language_util.h>
28 
29 std::ostream &goto_programt::output(std::ostream &out) const
30 {
31  return output(namespacet(symbol_tablet()), irep_idt(), out);
32 }
33 
48  const namespacet &ns,
49  const irep_idt &identifier,
50  std::ostream &out,
51  const instructiont &instruction) const
52 {
53  out << " // " << instruction.location_number << " ";
54 
55  if(!instruction.source_location.is_nil())
56  out << instruction.source_location.as_string();
57  else
58  out << "no location";
59 
60  out << "\n";
61 
62  if(!instruction.labels.empty())
63  {
64  out << " // Labels:";
65  for(const auto &label : instruction.labels)
66  out << " " << label;
67 
68  out << '\n';
69  }
70 
71  if(instruction.is_target())
72  out << std::setw(6) << instruction.target_number << ": ";
73  else
74  out << " ";
75 
76  switch(instruction.type)
77  {
79  out << "NO INSTRUCTION TYPE SET" << '\n';
80  break;
81 
82  case GOTO:
83  case INCOMPLETE_GOTO:
84  if(!instruction.get_condition().is_true())
85  {
86  out << "IF " << format(instruction.get_condition()) << " THEN ";
87  }
88 
89  out << "GOTO ";
90 
91  if(instruction.is_incomplete_goto())
92  {
93  out << "(incomplete)";
94  }
95  else
96  {
97  for(auto gt_it = instruction.targets.begin();
98  gt_it != instruction.targets.end();
99  gt_it++)
100  {
101  if(gt_it != instruction.targets.begin())
102  out << ", ";
103  out << (*gt_it)->target_number;
104  }
105  }
106 
107  out << '\n';
108  break;
109 
110  case OTHER:
111  if(instruction.get_other().id() == ID_code)
112  {
113  const auto &code = instruction.get_other();
114  if(code.get_statement() == ID_havoc_object)
115  {
116  out << "HAVOC_OBJECT " << format(code.op0()) << '\n';
117  break;
118  }
119  // fallthrough
120  }
121 
122  out << "OTHER " << format(instruction.get_other());
123  break;
124 
125  case SET_RETURN_VALUE:
126  out << "RETURN " << format(instruction.return_value()) << '\n';
127  break;
128 
129  case DECL:
130  out << "DECL " << format(instruction.decl_symbol()) << " : "
131  << format(instruction.decl_symbol().type()) << '\n';
132  break;
133 
134  case DEAD:
135  out << "DEAD " << format(instruction.dead_symbol()) << '\n';
136  break;
137 
138  case FUNCTION_CALL:
139  out << "CALL ";
140  {
141  if(instruction.call_lhs().is_not_nil())
142  out << format(instruction.call_lhs()) << " := ";
143  out << format(instruction.call_function());
144  out << '(';
145  bool first = true;
146  for(const auto &argument : instruction.call_arguments())
147  {
148  if(first)
149  first = false;
150  else
151  out << ", ";
152  out << format(argument);
153  }
154  out << ')';
155  out << '\n';
156  }
157  break;
158 
159  case ASSIGN:
160  out << "ASSIGN " << format(instruction.assign_lhs())
161  << " := " << format(instruction.assign_rhs()) << '\n';
162  break;
163 
164  case ASSUME:
165  case ASSERT:
166  if(instruction.is_assume())
167  out << "ASSUME ";
168  else
169  out << "ASSERT ";
170 
171  {
172  out << format(instruction.get_condition());
173 
174  const irep_idt &comment=instruction.source_location.get_comment();
175  if(!comment.empty())
176  out << " // " << comment;
177  }
178 
179  out << '\n';
180  break;
181 
182  case SKIP:
183  out << "SKIP" << '\n';
184  break;
185 
186  case END_FUNCTION:
187  out << "END_FUNCTION" << '\n';
188  break;
189 
190  case LOCATION:
191  out << "LOCATION" << '\n';
192  break;
193 
194  case THROW:
195  out << "THROW";
196 
197  {
198  const irept::subt &exception_list =
199  instruction.get_code().find(ID_exception_list).get_sub();
200 
201  for(const auto &ex : exception_list)
202  out << " " << ex.id();
203  }
204 
205  if(instruction.get_code().operands().size() == 1)
206  out << ": " << format(instruction.get_code().op0());
207 
208  out << '\n';
209  break;
210 
211  case CATCH:
212  {
213  if(instruction.get_code().get_statement() == ID_exception_landingpad)
214  {
215  const auto &landingpad = to_code_landingpad(instruction.get_code());
216  out << "EXCEPTION LANDING PAD (" << format(landingpad.catch_expr().type())
217  << ' ' << format(landingpad.catch_expr()) << ")";
218  }
219  else if(instruction.get_code().get_statement() == ID_push_catch)
220  {
221  out << "CATCH-PUSH ";
222 
223  unsigned i=0;
224  const irept::subt &exception_list =
225  instruction.get_code().find(ID_exception_list).get_sub();
227  instruction.targets.size() == exception_list.size(),
228  "unexpected discrepancy between sizes of instruction"
229  "targets and exception list");
230  for(instructiont::targetst::const_iterator
231  gt_it=instruction.targets.begin();
232  gt_it!=instruction.targets.end();
233  gt_it++, i++)
234  {
235  if(gt_it!=instruction.targets.begin())
236  out << ", ";
237  out << exception_list[i].id() << "->"
238  << (*gt_it)->target_number;
239  }
240  }
241  else if(instruction.get_code().get_statement() == ID_pop_catch)
242  {
243  out << "CATCH-POP";
244  }
245  else
246  {
247  UNREACHABLE;
248  }
249 
250  out << '\n';
251  break;
252  }
253 
254  case ATOMIC_BEGIN:
255  out << "ATOMIC_BEGIN" << '\n';
256  break;
257 
258  case ATOMIC_END:
259  out << "ATOMIC_END" << '\n';
260  break;
261 
262  case START_THREAD:
263  out << "START THREAD "
264  << instruction.get_target()->target_number
265  << '\n';
266  break;
267 
268  case END_THREAD:
269  out << "END THREAD" << '\n';
270  break;
271  }
272 
273  return out;
274 }
275 
277  decl_identifierst &decl_identifiers) const
278 {
279  for(const auto &instruction : instructions)
280  {
281  if(instruction.is_decl())
282  {
284  instruction.get_code().get_statement() == ID_decl,
285  "expected statement to be declaration statement");
287  instruction.get_code().operands().size() == 1,
288  "declaration statement expects one operand");
289  decl_identifiers.insert(instruction.decl_symbol().get_identifier());
290  }
291  }
292 }
293 
294 void parse_lhs_read(const exprt &src, std::list<exprt> &dest)
295 {
296  if(src.id()==ID_dereference)
297  {
298  dest.push_back(to_dereference_expr(src).pointer());
299  }
300  else if(src.id()==ID_index)
301  {
302  auto &index_expr = to_index_expr(src);
303  dest.push_back(index_expr.index());
304  parse_lhs_read(index_expr.array(), dest);
305  }
306  else if(src.id()==ID_member)
307  {
308  parse_lhs_read(to_member_expr(src).compound(), dest);
309  }
310  else if(src.id()==ID_if)
311  {
312  auto &if_expr = to_if_expr(src);
313  dest.push_back(if_expr.cond());
314  parse_lhs_read(if_expr.true_case(), dest);
315  parse_lhs_read(if_expr.false_case(), dest);
316  }
317 }
318 
319 std::list<exprt> expressions_read(
320  const goto_programt::instructiont &instruction)
321 {
322  std::list<exprt> dest;
323 
324  switch(instruction.type)
325  {
326  case ASSUME:
327  case ASSERT:
328  case GOTO:
329  dest.push_back(instruction.get_condition());
330  break;
331 
332  case SET_RETURN_VALUE:
333  dest.push_back(instruction.return_value());
334  break;
335 
336  case FUNCTION_CALL:
337  for(const auto &argument : instruction.call_arguments())
338  dest.push_back(argument);
339  if(instruction.call_lhs().is_not_nil())
340  parse_lhs_read(instruction.call_lhs(), dest);
341  break;
342 
343  case ASSIGN:
344  dest.push_back(instruction.assign_rhs());
345  parse_lhs_read(instruction.assign_lhs(), dest);
346  break;
347 
348  case CATCH:
349  case THROW:
350  case DEAD:
351  case DECL:
352  case ATOMIC_BEGIN:
353  case ATOMIC_END:
354  case START_THREAD:
355  case END_THREAD:
356  case END_FUNCTION:
357  case LOCATION:
358  case SKIP:
359  case OTHER:
360  case INCOMPLETE_GOTO:
361  case NO_INSTRUCTION_TYPE:
362  break;
363  }
364 
365  return dest;
366 }
367 
368 std::list<exprt> expressions_written(
369  const goto_programt::instructiont &instruction)
370 {
371  std::list<exprt> dest;
372 
373  switch(instruction.type)
374  {
375  case FUNCTION_CALL:
376  if(instruction.call_lhs().is_not_nil())
377  dest.push_back(instruction.call_lhs());
378  break;
379 
380  case ASSIGN:
381  dest.push_back(instruction.assign_lhs());
382  break;
383 
384  case CATCH:
385  case THROW:
386  case GOTO:
387  case SET_RETURN_VALUE:
388  case DEAD:
389  case DECL:
390  case ATOMIC_BEGIN:
391  case ATOMIC_END:
392  case START_THREAD:
393  case END_THREAD:
394  case END_FUNCTION:
395  case ASSERT:
396  case ASSUME:
397  case LOCATION:
398  case SKIP:
399  case OTHER:
400  case INCOMPLETE_GOTO:
401  case NO_INSTRUCTION_TYPE:
402  break;
403  }
404 
405  return dest;
406 }
407 
409  const exprt &src,
410  std::list<exprt> &dest)
411 {
412  if(src.id()==ID_symbol)
413  dest.push_back(src);
414  else if(src.id()==ID_address_of)
415  {
416  // don't traverse!
417  }
418  else if(src.id()==ID_dereference)
419  {
420  // this reads what is pointed to plus the pointer
421  auto &deref = to_dereference_expr(src);
422  dest.push_back(deref);
423  objects_read(deref.pointer(), dest);
424  }
425  else
426  {
427  forall_operands(it, src)
428  objects_read(*it, dest);
429  }
430 }
431 
432 std::list<exprt> objects_read(
433  const goto_programt::instructiont &instruction)
434 {
435  std::list<exprt> expressions=expressions_read(instruction);
436 
437  std::list<exprt> dest;
438 
439  for(const auto &expr : expressions)
440  objects_read(expr, dest);
441 
442  return dest;
443 }
444 
446  const exprt &src,
447  std::list<exprt> &dest)
448 {
449  if(src.id()==ID_if)
450  {
451  auto &if_expr = to_if_expr(src);
452  objects_written(if_expr.true_case(), dest);
453  objects_written(if_expr.false_case(), dest);
454  }
455  else
456  dest.push_back(src);
457 }
458 
459 std::list<exprt> objects_written(
460  const goto_programt::instructiont &instruction)
461 {
462  std::list<exprt> expressions=expressions_written(instruction);
463 
464  std::list<exprt> dest;
465 
466  for(const auto &expr : expressions)
467  objects_written(expr, dest);
468 
469  return dest;
470 }
471 
472 std::string as_string(
473  const class namespacet &ns,
474  const irep_idt &function,
476 {
477  std::string result;
478 
479  switch(i.type)
480  {
481  case NO_INSTRUCTION_TYPE:
482  return "(NO INSTRUCTION TYPE)";
483 
484  case GOTO:
485  if(!i.get_condition().is_true())
486  {
487  result += "IF " + from_expr(ns, function, i.get_condition()) + " THEN ";
488  }
489 
490  result+="GOTO ";
491 
492  for(goto_programt::instructiont::targetst::const_iterator
493  gt_it=i.targets.begin();
494  gt_it!=i.targets.end();
495  gt_it++)
496  {
497  if(gt_it!=i.targets.begin())
498  result+=", ";
499  result+=std::to_string((*gt_it)->target_number);
500  }
501  return result;
502 
503  case SET_RETURN_VALUE:
504  case OTHER:
505  case DECL:
506  case DEAD:
507  case FUNCTION_CALL:
508  case ASSIGN:
509  return from_expr(ns, function, i.get_code());
510 
511  case ASSUME:
512  case ASSERT:
513  if(i.is_assume())
514  result+="ASSUME ";
515  else
516  result+="ASSERT ";
517 
518  result += from_expr(ns, function, i.get_condition());
519 
520  {
522  if(!comment.empty())
523  result+=" /* "+id2string(comment)+" */";
524  }
525  return result;
526 
527  case SKIP:
528  return "SKIP";
529 
530  case END_FUNCTION:
531  return "END_FUNCTION";
532 
533  case LOCATION:
534  return "LOCATION";
535 
536  case THROW:
537  return "THROW";
538 
539  case CATCH:
540  return "CATCH";
541 
542  case ATOMIC_BEGIN:
543  return "ATOMIC_BEGIN";
544 
545  case ATOMIC_END:
546  return "ATOMIC_END";
547 
548  case START_THREAD:
549  result+="START THREAD ";
550 
551  if(i.targets.size()==1)
552  result+=std::to_string(i.targets.front()->target_number);
553  return result;
554 
555  case END_THREAD:
556  return "END THREAD";
557 
558  case INCOMPLETE_GOTO:
559  UNREACHABLE;
560  }
561 
562  UNREACHABLE;
563 }
564 
569 {
570  unsigned nr=0;
571  for(auto &i : instructions)
572  if(i.is_backwards_goto())
573  i.loop_number=nr++;
574 }
575 
577 {
582 }
583 
584 std::ostream &goto_programt::output(
585  const namespacet &ns,
586  const irep_idt &identifier,
587  std::ostream &out) const
588 {
589  // output program
590 
591  for(const auto &instruction : instructions)
592  output_instruction(ns, identifier, out, instruction);
593 
594  return out;
595 }
596 
608 {
609  // reset marking
610 
611  for(auto &i : instructions)
612  i.target_number=instructiont::nil_target;
613 
614  // mark the goto targets
615 
616  for(const auto &i : instructions)
617  {
618  for(const auto &t : i.targets)
619  {
620  if(t!=instructions.end())
621  t->target_number=0;
622  }
623  }
624 
625  // number the targets properly
626  unsigned cnt=0;
627 
628  for(auto &i : instructions)
629  {
630  if(i.is_target())
631  {
632  i.target_number=++cnt;
634  i.target_number != 0, "GOTO instruction target cannot be zero");
635  }
636  }
637 
638  // check the targets!
639  // (this is a consistency check only)
640 
641  for(const auto &i : instructions)
642  {
643  for(const auto &t : i.targets)
644  {
645  if(t!=instructions.end())
646  {
648  t->target_number != 0, "instruction's number cannot be zero");
650  t->target_number != instructiont::nil_target,
651  "GOTO instruction target cannot be nil_target");
652  }
653  }
654  }
655 }
656 
662 {
663  // Definitions for mapping between the two programs
664  typedef std::map<const_targett, targett> targets_mappingt;
665  targets_mappingt targets_mapping;
666 
667  clear();
668 
669  // Loop over program - 1st time collects targets and copy
670 
671  for(instructionst::const_iterator
672  it=src.instructions.begin();
673  it!=src.instructions.end();
674  ++it)
675  {
676  auto new_instruction=add_instruction();
677  targets_mapping[it]=new_instruction;
678  *new_instruction=*it;
679  }
680 
681  // Loop over program - 2nd time updates targets
682 
683  for(auto &i : instructions)
684  {
685  for(auto &t : i.targets)
686  {
687  targets_mappingt::iterator
688  m_target_it=targets_mapping.find(t);
689 
690  CHECK_RETURN(m_target_it != targets_mapping.end());
691 
692  t=m_target_it->second;
693  }
694  }
695 
698 }
699 
703 {
704  for(const auto &i : instructions)
705  if(i.is_assert() && !i.get_condition().is_true())
706  return true;
707 
708  return false;
709 }
710 
713 {
714  for(auto &i : instructions)
715  {
716  i.incoming_edges.clear();
717  }
718 
719  for(instructionst::iterator
720  it=instructions.begin();
721  it!=instructions.end();
722  ++it)
723  {
724  for(const auto &s : get_successors(it))
725  {
726  if(s!=instructions.end())
727  s->incoming_edges.insert(it);
728  }
729  }
730 }
731 
733 {
734  // clang-format off
735  return
736  type == other.type &&
737  code == other.code &&
738  guard == other.guard &&
739  targets.size() == other.targets.size() &&
740  labels == other.labels;
741  // clang-format on
742 }
743 
745  const namespacet &ns,
746  const validation_modet vm) const
747 {
748  validate_full_code(code, ns, vm);
749  validate_full_expr(guard, ns, vm);
750 
751  auto expr_symbol_finder = [&](const exprt &e) {
752  find_symbols_sett typetags;
753  find_type_symbols(e.type(), typetags);
754  find_symbols_or_nexts(e, typetags);
755  const symbolt *symbol;
756  for(const auto &identifier : typetags)
757  {
759  vm,
760  !ns.lookup(identifier, symbol),
761  id2string(identifier) + " not found",
762  source_location);
763  }
764  };
765 
766  auto &current_source_location = source_location;
767  auto type_finder =
768  [&ns, vm, &current_source_location](const exprt &e) {
769  if(e.id() == ID_symbol)
770  {
771  const auto &goto_symbol_expr = to_symbol_expr(e);
772  const auto &goto_id = goto_symbol_expr.get_identifier();
773 
774  const symbolt *table_symbol;
775  if(!ns.lookup(goto_id, table_symbol))
776  {
777  bool symbol_expr_type_matches_symbol_table =
778  base_type_eq(goto_symbol_expr.type(), table_symbol->type, ns);
779 
780  if(
781  !symbol_expr_type_matches_symbol_table &&
782  table_symbol->type.id() == ID_code)
783  {
784  // If a function declaration and its definition are in different
785  // translation units they may have different return types.
786  // Thus, the return type in the symbol table may differ
787  // from the return type in the symbol expr.
788  if(
789  goto_symbol_expr.type().source_location().get_file() !=
790  table_symbol->type.source_location().get_file())
791  {
792  // temporarily fixup the return types
793  auto goto_symbol_expr_type =
794  to_code_type(goto_symbol_expr.type());
795  auto table_symbol_type = to_code_type(table_symbol->type);
796 
797  goto_symbol_expr_type.return_type() =
798  table_symbol_type.return_type();
799 
800  symbol_expr_type_matches_symbol_table =
801  base_type_eq(goto_symbol_expr_type, table_symbol_type, ns);
802  }
803  }
804 
805  if(
806  !symbol_expr_type_matches_symbol_table &&
807  goto_symbol_expr.type().id() == ID_array &&
808  to_array_type(goto_symbol_expr.type()).is_incomplete())
809  {
810  // If the symbol expr has an incomplete array type, it may not have
811  // a constant size value, whereas the symbol table entry may have
812  // an (assumed) constant size of 1 (which mimics gcc behaviour)
813  if(table_symbol->type.id() == ID_array)
814  {
815  auto symbol_table_array_type = to_array_type(table_symbol->type);
816  symbol_table_array_type.size() = nil_exprt();
817 
818  symbol_expr_type_matches_symbol_table =
819  goto_symbol_expr.type() == symbol_table_array_type;
820  }
821  }
822 
824  vm,
825  symbol_expr_type_matches_symbol_table,
826  id2string(goto_id) + " type inconsistency\n" +
827  "goto program type: " + goto_symbol_expr.type().id_string() +
828  "\n" + "symbol table type: " + table_symbol->type.id_string(),
829  current_source_location);
830  }
831  }
832  };
833 
834  const symbolt *table_symbol;
835  switch(type)
836  {
837  case NO_INSTRUCTION_TYPE:
838  break;
839  case GOTO:
841  vm,
842  has_target(),
843  "goto instruction expects at least one target",
844  source_location);
845  // get_target checks that targets.size()==1
847  vm,
848  get_target()->is_target() && get_target()->target_number != 0,
849  "goto target has to be a target",
850  source_location);
851  break;
852  case ASSUME:
854  vm,
855  targets.empty(),
856  "assume instruction should not have a target",
857  source_location);
858  break;
859  case ASSERT:
861  vm,
862  targets.empty(),
863  "assert instruction should not have a target",
864  source_location);
865 
866  std::for_each(guard.depth_begin(), guard.depth_end(), expr_symbol_finder);
867  std::for_each(guard.depth_begin(), guard.depth_end(), type_finder);
868  break;
869  case OTHER:
870  break;
871  case SKIP:
872  break;
873  case START_THREAD:
874  break;
875  case END_THREAD:
876  break;
877  case LOCATION:
878  break;
879  case END_FUNCTION:
880  break;
881  case ATOMIC_BEGIN:
882  break;
883  case ATOMIC_END:
884  break;
885  case SET_RETURN_VALUE:
887  vm,
888  code.get_statement() == ID_return,
889  "SET_RETURN_VALUE instruction should contain a return statement",
890  source_location);
891  break;
892  case ASSIGN:
893  DATA_CHECK(
894  vm,
895  code.get_statement() == ID_assign,
896  "assign instruction should contain an assign statement");
897  DATA_CHECK(
898  vm, targets.empty(), "assign instruction should not have a target");
899  break;
900  case DECL:
902  vm,
903  code.get_statement() == ID_decl,
904  "declaration instructions should contain a declaration statement",
905  source_location);
907  vm,
908  !ns.lookup(decl_symbol().get_identifier(), table_symbol),
909  "declared symbols should be known",
910  id2string(decl_symbol().get_identifier()),
911  source_location);
912  break;
913  case DEAD:
915  vm,
916  code.get_statement() == ID_dead,
917  "dead instructions should contain a dead statement",
918  source_location);
920  vm,
921  !ns.lookup(dead_symbol().get_identifier(), table_symbol),
922  "removed symbols should be known",
923  id2string(dead_symbol().get_identifier()),
924  source_location);
925  break;
926  case FUNCTION_CALL:
928  vm,
929  code.get_statement() == ID_function_call,
930  "function call instruction should contain a call statement",
931  source_location);
932 
933  std::for_each(code.depth_begin(), code.depth_end(), expr_symbol_finder);
934  std::for_each(code.depth_begin(), code.depth_end(), type_finder);
935  break;
936  case THROW:
937  break;
938  case CATCH:
939  break;
940  case INCOMPLETE_GOTO:
941  break;
942  }
943 }
944 
946  std::function<optionalt<exprt>(exprt)> f)
947 {
948  switch(type)
949  {
950  case OTHER:
951  if(get_other().get_statement() == ID_expression)
952  {
953  auto new_expression = f(to_code_expression(get_other()).expression());
954  if(new_expression.has_value())
955  {
956  auto new_other = to_code_expression(get_other());
957  new_other.expression() = *new_expression;
958  set_other(new_other);
959  }
960  }
961  break;
962 
963  case SET_RETURN_VALUE:
964  {
965  auto new_return_value = f(return_value());
966  if(new_return_value.has_value())
967  return_value() = *new_return_value;
968  }
969  break;
970 
971  case ASSIGN:
972  {
973  auto new_assign_lhs = f(assign_lhs());
974  auto new_assign_rhs = f(assign_rhs());
975  if(new_assign_lhs.has_value())
976  assign_lhs_nonconst() = new_assign_lhs.value();
977  if(new_assign_rhs.has_value())
978  assign_rhs_nonconst() = new_assign_rhs.value();
979  }
980  break;
981 
982  case DECL:
983  {
984  auto new_symbol = f(decl_symbol());
985  if(new_symbol.has_value())
986  decl_symbol() = to_symbol_expr(*new_symbol);
987  }
988  break;
989 
990  case DEAD:
991  {
992  auto new_symbol = f(dead_symbol());
993  if(new_symbol.has_value())
994  dead_symbol() = to_symbol_expr(*new_symbol);
995  }
996  break;
997 
998  case FUNCTION_CALL:
999  {
1000  auto new_lhs = f(as_const(*this).call_lhs());
1001  if(new_lhs.has_value())
1002  call_lhs() = *new_lhs;
1003 
1004  auto new_call_function = f(as_const(*this).call_function());
1005  if(new_call_function.has_value())
1006  call_function() = *new_call_function;
1007 
1008  exprt::operandst new_arguments = as_const(*this).call_arguments();
1009  bool argument_changed = false;
1010 
1011  for(auto &a : new_arguments)
1012  {
1013  auto new_a = f(a);
1014  if(new_a.has_value())
1015  {
1016  a = *new_a;
1017  argument_changed = true;
1018  }
1019  }
1020 
1021  if(argument_changed)
1022  call_arguments() = std::move(new_arguments);
1023  }
1024  break;
1025 
1026  case GOTO:
1027  case ASSUME:
1028  case ASSERT:
1029  case SKIP:
1030  case START_THREAD:
1031  case END_THREAD:
1032  case LOCATION:
1033  case END_FUNCTION:
1034  case ATOMIC_BEGIN:
1035  case ATOMIC_END:
1036  case THROW:
1037  case CATCH:
1038  case INCOMPLETE_GOTO:
1039  case NO_INSTRUCTION_TYPE:
1040  if(has_condition())
1041  {
1042  auto new_condition = f(get_condition());
1043  if(new_condition.has_value())
1044  set_condition(new_condition.value());
1045  }
1046  }
1047 }
1048 
1050  std::function<void(const exprt &)> f) const
1051 {
1052  switch(type)
1053  {
1054  case OTHER:
1055  if(get_other().get_statement() == ID_expression)
1056  f(to_code_expression(get_other()).expression());
1057  break;
1058 
1059  case SET_RETURN_VALUE:
1060  f(return_value());
1061  break;
1062 
1063  case ASSIGN:
1064  f(assign_lhs());
1065  f(assign_rhs());
1066  break;
1067 
1068  case DECL:
1069  f(decl_symbol());
1070  break;
1071 
1072  case DEAD:
1073  f(dead_symbol());
1074  break;
1075 
1076  case FUNCTION_CALL:
1077  f(call_lhs());
1078  for(auto &a : call_arguments())
1079  f(a);
1080  break;
1081 
1082  case GOTO:
1083  case ASSUME:
1084  case ASSERT:
1085  case SKIP:
1086  case START_THREAD:
1087  case END_THREAD:
1088  case LOCATION:
1089  case END_FUNCTION:
1090  case ATOMIC_BEGIN:
1091  case ATOMIC_END:
1092  case THROW:
1093  case CATCH:
1094  case INCOMPLETE_GOTO:
1095  case NO_INSTRUCTION_TYPE:
1096  if(has_condition())
1097  f(get_condition());
1098  }
1099 }
1100 
1101 bool goto_programt::equals(const goto_programt &other) const
1102 {
1103  if(instructions.size() != other.instructions.size())
1104  return false;
1105 
1106  goto_programt::const_targett other_it = other.instructions.begin();
1107  for(const auto &ins : instructions)
1108  {
1109  if(!ins.equals(*other_it))
1110  return false;
1111 
1112  // the number of targets is the same as instructiont::equals returned "true"
1113  auto other_target_it = other_it->targets.begin();
1114  for(const auto &t : ins.targets)
1115  {
1116  if(
1117  t->location_number - ins.location_number !=
1118  (*other_target_it)->location_number - other_it->location_number)
1119  {
1120  return false;
1121  }
1122 
1123  ++other_target_it;
1124  }
1125 
1126  ++other_it;
1127  }
1128 
1129  return true;
1130 }
1131 
1133 std::ostream &operator<<(std::ostream &out, goto_program_instruction_typet t)
1134 {
1135  switch(t)
1136  {
1137  case NO_INSTRUCTION_TYPE:
1138  out << "NO_INSTRUCTION_TYPE";
1139  break;
1140  case GOTO:
1141  out << "GOTO";
1142  break;
1143  case ASSUME:
1144  out << "ASSUME";
1145  break;
1146  case ASSERT:
1147  out << "ASSERT";
1148  break;
1149  case OTHER:
1150  out << "OTHER";
1151  break;
1152  case DECL:
1153  out << "DECL";
1154  break;
1155  case DEAD:
1156  out << "DEAD";
1157  break;
1158  case SKIP:
1159  out << "SKIP";
1160  break;
1161  case START_THREAD:
1162  out << "START_THREAD";
1163  break;
1164  case END_THREAD:
1165  out << "END_THREAD";
1166  break;
1167  case LOCATION:
1168  out << "LOCATION";
1169  break;
1170  case END_FUNCTION:
1171  out << "END_FUNCTION";
1172  break;
1173  case ATOMIC_BEGIN:
1174  out << "ATOMIC_BEGIN";
1175  break;
1176  case ATOMIC_END:
1177  out << "ATOMIC_END";
1178  break;
1179  case SET_RETURN_VALUE:
1180  out << "SET_RETURN_VALUE";
1181  break;
1182  case ASSIGN:
1183  out << "ASSIGN";
1184  break;
1185  case FUNCTION_CALL:
1186  out << "FUNCTION_CALL";
1187  break;
1188  case THROW:
1189  out << "THROW";
1190  break;
1191  case CATCH:
1192  out << "CATCH";
1193  break;
1194  case INCOMPLETE_GOTO:
1195  out << "INCOMPLETE_GOTO";
1196  break;
1197  }
1198 
1199  return out;
1200 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
source_locationt::get_comment
const irep_idt & get_comment() const
Definition: source_location.h:70
format
static format_containert< T > format(const T &o)
Definition: format.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
DATA_CHECK
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
to_code_expression
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1874
goto_programt::instructiont::source_location
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:431
array_typet::is_incomplete
bool is_incomplete() const
Definition: std_types.h:786
source_locationt::as_string
std::string as_string() const
Definition: source_location.h:25
SET_RETURN_VALUE
@ SET_RETURN_VALUE
Definition: goto_program.h:43
codet::op0
exprt & op0()
Definition: expr.h:99
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:684
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
goto_programt::compute_loop_numbers
void compute_loop_numbers()
Compute loop numbers.
Definition: goto_program.cpp:568
find_symbols_or_nexts
void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
Add to the set dest the sub-expressions of src with id ID_symbol or ID_next_symbol.
Definition: find_symbols.cpp:18
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2237
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
goto_programt::instructiont::type
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:434
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
goto_programt::update
void update()
Update all indices.
Definition: goto_program.cpp:576
goto_programt::copy_from
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
Definition: goto_program.cpp:661
goto_programt::instructiont::apply
void apply(std::function< void(const exprt &)>) const
Apply given function to all expressions.
Definition: goto_program.cpp:1049
invariant.h
goto_programt::instructiont::transform
void transform(std::function< optionalt< exprt >(exprt)>)
Apply given transformer to all expressions; no return value means no change needed.
Definition: goto_program.cpp:945
exprt
Base class for all expressions.
Definition: expr.h:54
goto_programt::get_decl_identifiers
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
Definition: goto_program.cpp:276
goto_programt::has_assertion
bool has_assertion() const
Does the goto program have an assertion?
Definition: goto_program.cpp:702
as_string
std::string as_string(const class namespacet &ns, const irep_idt &function, const goto_programt::instructiont &i)
Definition: goto_program.cpp:472
irep_idt
dstringt irep_idt
Definition: irep.h:37
DATA_CHECK_WITH_DIAGNOSTICS
#define DATA_CHECK_WITH_DIAGNOSTICS(vm, condition, message,...)
Definition: validate.h:37
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:57
goto_programt::instructiont::targets
targetst targets
The list of successor instructions.
Definition: goto_program.h:468
goto_programt::instructiont::is_incomplete_goto
bool is_incomplete_goto() const
Definition: goto_program.h:545
goto_programt::get_successors
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
Definition: goto_program.h:1143
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
expressions_written
std::list< exprt > expressions_written(const goto_programt::instructiont &instruction)
Definition: goto_program.cpp:368
goto_programt::instructiont::decl_symbol
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
Definition: goto_program.h:253
goto_programt::instructiont::call_arguments
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
Definition: goto_program.h:389
goto_programt::instructiont::get_other
const codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:417
goto_programt::instructiont::get_code
const codet & get_code() const
Get the code represented by this instruction.
Definition: goto_program.h:185
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
goto_programt::add_instruction
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:761
THROW
@ THROW
Definition: goto_program.h:48
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
GOTO
@ GOTO
Definition: goto_program.h:32
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
goto_programt::equals
bool equals(const goto_programt &other) const
Syntactic equality: two goto_programt are equal if, and only if, they have the same number of instruc...
Definition: goto_program.cpp:1101
goto_programt::instructiont::validate
void validate(const namespacet &ns, const validation_modet vm) const
Check that the instruction is well-formed.
Definition: goto_program.cpp:744
as_const
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
find_symbols.h
goto_programt::compute_target_numbers
void compute_target_numbers()
Compute the target numbers.
Definition: goto_program.cpp:607
validate_full_code
void validate_full_code(const codet &code, const namespacet &ns, const validation_modet vm)
Check that the given code statement is well-formed (full check, including checks of all subexpression...
Definition: validate_code.cpp:98
base_type.h
Base Type Computation.
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
goto_programt::instructiont::dead_symbol
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Definition: goto_program.h:295
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
goto_programt::output_instruction
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
Definition: goto_program.cpp:47
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:181
operator<<
std::ostream & operator<<(std::ostream &out, goto_program_instruction_typet t)
Outputs a string representation of a goto_program_instruction_typet
Definition: goto_program.cpp:1133
goto_programt::output
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
Definition: goto_program.cpp:584
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
language_util.h
base_type_eq
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:290
typet::source_location
const source_locationt & source_location() const
Definition: type.h:71
objects_read
void objects_read(const exprt &src, std::list< exprt > &dest)
Definition: goto_program.cpp:408
nil_exprt
The NIL expression.
Definition: std_expr.h:2820
pointer_expr.h
API to expression classes for Pointers.
goto_programt::instructiont::labels
labelst labels
Definition: goto_program.h:493
find_type_symbols
void find_type_symbols(const exprt &src, find_symbols_sett &dest)
Definition: find_symbols.cpp:176
goto_programt::instructiont::equals
bool equals(const instructiont &other) const
Syntactic equality: two instructiont are equal if they have the same type, code, guard,...
Definition: goto_program.cpp:732
irept::id_string
const std::string & id_string() const
Definition: irep.h:410
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:31
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
OTHER
@ OTHER
Definition: goto_program.h:35
validation_modet
validation_modet
Definition: validation_mode.h:13
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
objects_written
void objects_written(const exprt &src, std::list< exprt > &dest)
Definition: goto_program.cpp:445
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
goto_programt::instructiont::assign_rhs
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
Definition: goto_program.h:219
goto_programt::instructiont::call_lhs
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
Definition: goto_program.h:375
END_FUNCTION
@ END_FUNCTION
Definition: goto_program.h:40
SKIP
@ SKIP
Definition: goto_program.h:36
goto_programt::compute_incoming_edges
void compute_incoming_edges()
Compute for each instruction the set of instructions it is a successor of.
Definition: goto_program.cpp:712
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
sharing_treet< irept, forward_list_as_mapt< irep_namet, irept > >::subt
typename dt::subt subt
Definition: irep.h:171
goto_programt::clear
void clear()
Clear the goto program.
Definition: goto_program.h:847
goto_programt::instructiont::return_value
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
Definition: goto_program.h:325
goto_program.h
Concrete Goto Program.
goto_program_instruction_typet
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:30
goto_programt::compute_location_numbers
void compute_location_numbers()
Compute location numbers.
Definition: goto_program.h:805
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
ASSIGN
@ ASSIGN
Definition: goto_program.h:44
format_expr.h
to_code_landingpad
static code_landingpadt & to_code_landingpad(codet &code)
Definition: std_code.h:2418
goto_programt::instructiont::target_number
unsigned target_number
A number to identify branch targets.
Definition: goto_program.h:601
CATCH
@ CATCH
Definition: goto_program.h:49
expr_iterator.h
Forward depth-first search iterators These iterators' copy operations are expensive,...
find_symbols_sett
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:21
DECL
@ DECL
Definition: goto_program.h:45
goto_programt::instructiont::assign_lhs
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:205
goto_programt::instructiont::location_number
unsigned location_number
A globally unique number to identify a program location.
Definition: goto_program.h:594
symbolt
Symbol table entry.
Definition: symbol.h:28
ASSUME
@ ASSUME
Definition: goto_program.h:33
expressions_read
std::list< exprt > expressions_read(const goto_programt::instructiont &instruction)
Definition: goto_program.cpp:319
goto_programt::instructiont::guard
exprt guard
Guard for gotos, assume, assert Use get_condition() to read, and set_condition(c) to write.
Definition: goto_program.h:438
irept::get_sub
subt & get_sub()
Definition: irep.h:467
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:813
START_THREAD
@ START_THREAD
Definition: goto_program.h:37
validate.h
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:47
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
validate_full_expr
void validate_full_expr(const exprt &expr, const namespacet &ns, const validation_modet vm)
Check that the given expression is well-formed (full check, including checks of all subexpressions an...
Definition: validate_expressions.cpp:93
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:35
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
ATOMIC_END
@ ATOMIC_END
Definition: goto_program.h:42
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:647
DEAD
@ DEAD
Definition: goto_program.h:46
exprt::operands
operandst & operands()
Definition: expr.h:92
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition: goto_program.h:41
goto_programt::instructiont::is_assume
bool is_assume() const
Definition: goto_program.h:538
symbol_table.h
Author: Diffblue Ltd.
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:69
goto_programt::instructiont::get_condition
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:447
LOCATION
@ LOCATION
Definition: goto_program.h:39
ASSERT
@ ASSERT
Definition: goto_program.h:34
goto_programt::decl_identifierst
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:880
comment
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
std_expr.h
API to expression classes.
goto_programt::instructiont::is_target
bool is_target() const
Is this node a branch target?
Definition: goto_program.h:499
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
goto_programt::instructiont::nil_target
static const unsigned nil_target
Uniquely identify an invalid target or location.
Definition: goto_program.h:588
goto_programt::instructiont::call_function
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
Definition: goto_program.h:361
format_type.h
goto_programt::instructiont::get_target
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:472
END_THREAD
@ END_THREAD
Definition: goto_program.h:38
INCOMPLETE_GOTO
@ INCOMPLETE_GOTO
Definition: goto_program.h:50
parse_lhs_read
void parse_lhs_read(const exprt &src, std::list< exprt > &dest)
Definition: goto_program.cpp:294