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