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