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