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!="")
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  default:
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 =
290  instruction.get_function_call();
291  forall_expr(it, function_call.arguments())
292  dest.push_back(*it);
293  if(function_call.lhs().is_not_nil())
294  parse_lhs_read(function_call.lhs(), dest);
295  }
296  break;
297 
298  case ASSIGN:
299  {
300  const code_assignt &assignment = instruction.get_assign();
301  dest.push_back(assignment.rhs());
302  parse_lhs_read(assignment.lhs(), dest);
303  }
304  break;
305 
306  default:
307  {
308  }
309  }
310 
311  return dest;
312 }
313 
314 std::list<exprt> expressions_written(
315  const goto_programt::instructiont &instruction)
316 {
317  std::list<exprt> dest;
318 
319  switch(instruction.type)
320  {
321  case FUNCTION_CALL:
322  {
323  const code_function_callt &function_call =
324  instruction.get_function_call();
325  if(function_call.lhs().is_not_nil())
326  dest.push_back(function_call.lhs());
327  }
328  break;
329 
330  case ASSIGN:
331  dest.push_back(instruction.get_assign().lhs());
332  break;
333 
334  default:
335  {
336  }
337  }
338 
339  return dest;
340 }
341 
343  const exprt &src,
344  std::list<exprt> &dest)
345 {
346  if(src.id()==ID_symbol)
347  dest.push_back(src);
348  else if(src.id()==ID_address_of)
349  {
350  // don't traverse!
351  }
352  else if(src.id()==ID_dereference)
353  {
354  // this reads what is pointed to plus the pointer
355  auto &deref = to_dereference_expr(src);
356  dest.push_back(deref);
357  objects_read(deref.pointer(), dest);
358  }
359  else
360  {
361  forall_operands(it, src)
362  objects_read(*it, dest);
363  }
364 }
365 
366 std::list<exprt> objects_read(
367  const goto_programt::instructiont &instruction)
368 {
369  std::list<exprt> expressions=expressions_read(instruction);
370 
371  std::list<exprt> dest;
372 
373  for(const auto &expr : expressions)
374  objects_read(expr, dest);
375 
376  return dest;
377 }
378 
380  const exprt &src,
381  std::list<exprt> &dest)
382 {
383  if(src.id()==ID_if)
384  {
385  auto &if_expr = to_if_expr(src);
386  objects_written(if_expr.true_case(), dest);
387  objects_written(if_expr.false_case(), dest);
388  }
389  else
390  dest.push_back(src);
391 }
392 
393 std::list<exprt> objects_written(
394  const goto_programt::instructiont &instruction)
395 {
396  std::list<exprt> expressions=expressions_written(instruction);
397 
398  std::list<exprt> dest;
399 
400  for(const auto &expr : expressions)
401  objects_written(expr, dest);
402 
403  return dest;
404 }
405 
406 std::string as_string(
407  const class namespacet &ns,
408  const irep_idt &function,
410 {
411  std::string result;
412 
413  switch(i.type)
414  {
415  case NO_INSTRUCTION_TYPE:
416  return "(NO INSTRUCTION TYPE)";
417 
418  case GOTO:
419  if(!i.get_condition().is_true())
420  {
421  result += "IF " + from_expr(ns, function, i.get_condition()) + " THEN ";
422  }
423 
424  result+="GOTO ";
425 
426  for(goto_programt::instructiont::targetst::const_iterator
427  gt_it=i.targets.begin();
428  gt_it!=i.targets.end();
429  gt_it++)
430  {
431  if(gt_it!=i.targets.begin())
432  result+=", ";
433  result+=std::to_string((*gt_it)->target_number);
434  }
435  return result;
436 
437  case RETURN:
438  case OTHER:
439  case DECL:
440  case DEAD:
441  case FUNCTION_CALL:
442  case ASSIGN:
443  return from_expr(ns, function, i.code);
444 
445  case ASSUME:
446  case ASSERT:
447  if(i.is_assume())
448  result+="ASSUME ";
449  else
450  result+="ASSERT ";
451 
452  result += from_expr(ns, function, i.get_condition());
453 
454  {
456  if(comment!="")
457  result+=" /* "+id2string(comment)+" */";
458  }
459  return result;
460 
461  case SKIP:
462  return "SKIP";
463 
464  case END_FUNCTION:
465  return "END_FUNCTION";
466 
467  case LOCATION:
468  return "LOCATION";
469 
470  case THROW:
471  return "THROW";
472 
473  case CATCH:
474  return "CATCH";
475 
476  case ATOMIC_BEGIN:
477  return "ATOMIC_BEGIN";
478 
479  case ATOMIC_END:
480  return "ATOMIC_END";
481 
482  case START_THREAD:
483  result+="START THREAD ";
484 
485  if(i.targets.size()==1)
486  result+=std::to_string(i.targets.front()->target_number);
487  return result;
488 
489  case END_THREAD:
490  return "END THREAD";
491 
492  default:
493  UNREACHABLE;
494  }
495 }
496 
501 {
502  unsigned nr=0;
503  for(auto &i : instructions)
504  if(i.is_backwards_goto())
505  i.loop_number=nr++;
506 }
507 
509 {
514 }
515 
516 std::ostream &goto_programt::output(
517  const namespacet &ns,
518  const irep_idt &identifier,
519  std::ostream &out) const
520 {
521  // output program
522 
523  for(const auto &instruction : instructions)
524  output_instruction(ns, identifier, out, instruction);
525 
526  return out;
527 }
528 
540 {
541  // reset marking
542 
543  for(auto &i : instructions)
544  i.target_number=instructiont::nil_target;
545 
546  // mark the goto targets
547 
548  for(const auto &i : instructions)
549  {
550  for(const auto &t : i.targets)
551  {
552  if(t!=instructions.end())
553  t->target_number=0;
554  }
555  }
556 
557  // number the targets properly
558  unsigned cnt=0;
559 
560  for(auto &i : instructions)
561  {
562  if(i.is_target())
563  {
564  i.target_number=++cnt;
566  i.target_number != 0, "GOTO instruction target cannot be zero");
567  }
568  }
569 
570  // check the targets!
571  // (this is a consistency check only)
572 
573  for(const auto &i : instructions)
574  {
575  for(const auto &t : i.targets)
576  {
577  if(t!=instructions.end())
578  {
580  t->target_number != 0, "instruction's number cannot be zero");
582  t->target_number != instructiont::nil_target,
583  "GOTO instruction target cannot be nil_target");
584  }
585  }
586  }
587 }
588 
594 {
595  // Definitions for mapping between the two programs
596  typedef std::map<const_targett, targett> targets_mappingt;
597  targets_mappingt targets_mapping;
598 
599  clear();
600 
601  // Loop over program - 1st time collects targets and copy
602 
603  for(instructionst::const_iterator
604  it=src.instructions.begin();
605  it!=src.instructions.end();
606  ++it)
607  {
608  auto new_instruction=add_instruction();
609  targets_mapping[it]=new_instruction;
610  *new_instruction=*it;
611  }
612 
613  // Loop over program - 2nd time updates targets
614 
615  for(auto &i : instructions)
616  {
617  for(auto &t : i.targets)
618  {
619  targets_mappingt::iterator
620  m_target_it=targets_mapping.find(t);
621 
622  CHECK_RETURN(m_target_it != targets_mapping.end());
623 
624  t=m_target_it->second;
625  }
626  }
627 
630 }
631 
635 {
636  for(const auto &i : instructions)
637  if(i.is_assert() && !i.get_condition().is_true())
638  return true;
639 
640  return false;
641 }
642 
645 {
646  for(auto &i : instructions)
647  {
648  i.incoming_edges.clear();
649  }
650 
651  for(instructionst::iterator
652  it=instructions.begin();
653  it!=instructions.end();
654  ++it)
655  {
656  for(const auto &s : get_successors(it))
657  {
658  if(s!=instructions.end())
659  s->incoming_edges.insert(it);
660  }
661  }
662 }
663 
665 {
666  // clang-format off
667  return
668  type == other.type &&
669  code == other.code &&
670  guard == other.guard &&
671  targets.size() == other.targets.size() &&
672  labels == other.labels;
673  // clang-format on
674 }
675 
677  const namespacet &ns,
678  const validation_modet vm) const
679 {
680  validate_full_code(code, ns, vm);
681  validate_full_expr(guard, ns, vm);
682 
683  auto expr_symbol_finder = [&](const exprt &e) {
684  find_symbols_sett typetags;
685  find_type_symbols(e.type(), typetags);
686  find_symbols(e, typetags);
687  const symbolt *symbol;
688  for(const auto &identifier : typetags)
689  {
691  vm,
692  !ns.lookup(identifier, symbol),
693  id2string(identifier) + " not found",
694  source_location);
695  }
696  };
697 
698  auto &current_source_location = source_location;
699  auto type_finder =
700  [&ns, vm, &current_source_location](const exprt &e) {
701  if(e.id() == ID_symbol)
702  {
703  const auto &goto_symbol_expr = to_symbol_expr(e);
704  const auto &goto_id = goto_symbol_expr.get_identifier();
705 
706  const symbolt *table_symbol;
707  if(!ns.lookup(goto_id, table_symbol))
708  {
709  bool symbol_expr_type_matches_symbol_table =
710  base_type_eq(goto_symbol_expr.type(), table_symbol->type, ns);
711 
712  if(
713  !symbol_expr_type_matches_symbol_table &&
714  table_symbol->type.id() == ID_code)
715  {
716  // If a function declaration and its definition are in different
717  // translation units they may have different return types.
718  // Thus, the return type in the symbol table may differ
719  // from the return type in the symbol expr.
720  if(
721  goto_symbol_expr.type().source_location().get_file() !=
722  table_symbol->type.source_location().get_file())
723  {
724  // temporarily fixup the return types
725  auto goto_symbol_expr_type =
726  to_code_type(goto_symbol_expr.type());
727  auto table_symbol_type = to_code_type(table_symbol->type);
728 
729  goto_symbol_expr_type.return_type() =
730  table_symbol_type.return_type();
731 
732  symbol_expr_type_matches_symbol_table =
733  base_type_eq(goto_symbol_expr_type, table_symbol_type, ns);
734  }
735  }
736 
737  if(
738  !symbol_expr_type_matches_symbol_table &&
739  goto_symbol_expr.type().id() == ID_array &&
740  to_array_type(goto_symbol_expr.type()).is_incomplete())
741  {
742  // If the symbol expr has an incomplete array type, it may not have
743  // a constant size value, whereas the symbol table entry may have
744  // an (assumed) constant size of 1 (which mimics gcc behaviour)
745  if(table_symbol->type.id() == ID_array)
746  {
747  auto symbol_table_array_type = to_array_type(table_symbol->type);
748  symbol_table_array_type.size() = nil_exprt();
749 
750  symbol_expr_type_matches_symbol_table =
751  goto_symbol_expr.type() == symbol_table_array_type;
752  }
753  }
754 
756  vm,
757  symbol_expr_type_matches_symbol_table,
758  id2string(goto_id) + " type inconsistency\n" +
759  "goto program type: " + goto_symbol_expr.type().id_string() +
760  "\n" + "symbol table type: " + table_symbol->type.id_string(),
761  current_source_location);
762  }
763  }
764  };
765 
766  const symbolt *table_symbol;
767  switch(type)
768  {
769  case NO_INSTRUCTION_TYPE:
770  break;
771  case GOTO:
773  vm,
774  has_target(),
775  "goto instruction expects at least one target",
776  source_location);
777  // get_target checks that targets.size()==1
779  vm,
780  get_target()->is_target() && get_target()->target_number != 0,
781  "goto target has to be a target",
782  source_location);
783  break;
784  case ASSUME:
786  vm,
787  targets.empty(),
788  "assume instruction should not have a target",
789  source_location);
790  break;
791  case ASSERT:
793  vm,
794  targets.empty(),
795  "assert instruction should not have a target",
796  source_location);
797 
798  std::for_each(guard.depth_begin(), guard.depth_end(), expr_symbol_finder);
799  std::for_each(guard.depth_begin(), guard.depth_end(), type_finder);
800  break;
801  case OTHER:
802  break;
803  case SKIP:
804  break;
805  case START_THREAD:
806  break;
807  case END_THREAD:
808  break;
809  case LOCATION:
810  break;
811  case END_FUNCTION:
812  break;
813  case ATOMIC_BEGIN:
814  break;
815  case ATOMIC_END:
816  break;
817  case RETURN:
819  vm,
820  code.get_statement() == ID_return,
821  "return instruction should contain a return statement",
822  source_location);
823  break;
824  case ASSIGN:
825  DATA_CHECK(
826  vm,
827  code.get_statement() == ID_assign,
828  "assign instruction should contain an assign statement");
829  DATA_CHECK(
830  vm, targets.empty(), "assign instruction should not have a target");
831  break;
832  case DECL:
834  vm,
835  code.get_statement() == ID_decl,
836  "declaration instructions should contain a declaration statement",
837  source_location);
839  vm,
840  !ns.lookup(get_decl().get_identifier(), table_symbol),
841  "declared symbols should be known",
842  id2string(get_decl().get_identifier()),
843  source_location);
844  break;
845  case DEAD:
847  vm,
848  code.get_statement() == ID_dead,
849  "dead instructions should contain a dead statement",
850  source_location);
852  vm,
853  !ns.lookup(get_dead().get_identifier(), table_symbol),
854  "removed symbols should be known",
855  id2string(get_dead().get_identifier()),
856  source_location);
857  break;
858  case FUNCTION_CALL:
860  vm,
861  code.get_statement() == ID_function_call,
862  "function call instruction should contain a call statement",
863  source_location);
864 
865  std::for_each(code.depth_begin(), code.depth_end(), expr_symbol_finder);
866  std::for_each(code.depth_begin(), code.depth_end(), type_finder);
867  break;
868  case THROW:
869  break;
870  case CATCH:
871  break;
872  case INCOMPLETE_GOTO:
873  break;
874  }
875 }
876 
878  std::function<optionalt<exprt>(exprt)> f)
879 {
880  switch(type)
881  {
882  case OTHER:
883  if(get_other().get_statement() == ID_expression)
884  {
885  auto new_expression = f(to_code_expression(get_other()).expression());
886  if(new_expression.has_value())
887  {
888  auto new_other = to_code_expression(get_other());
889  new_other.expression() = *new_expression;
890  set_other(new_other);
891  }
892  }
893  break;
894 
895  case RETURN:
896  {
897  auto new_return_value = f(get_return().return_value());
898  if(new_return_value.has_value())
899  {
900  auto new_return = get_return();
901  new_return.return_value() = *new_return_value;
902  set_return(new_return);
903  }
904  }
905  break;
906 
907  case ASSIGN:
908  {
909  auto new_assign_lhs = f(get_assign().lhs());
910  auto new_assign_rhs = f(get_assign().rhs());
911  if(new_assign_lhs.has_value() || new_assign_rhs.has_value())
912  {
913  auto new_assignment = get_assign();
914  new_assignment.lhs() = new_assign_lhs.value_or(new_assignment.lhs());
915  new_assignment.rhs() = new_assign_rhs.value_or(new_assignment.rhs());
916  set_assign(new_assignment);
917  }
918  }
919  break;
920 
921  case DECL:
922  {
923  auto new_symbol = f(get_decl().symbol());
924  if(new_symbol.has_value())
925  {
926  auto new_decl = get_decl();
927  new_decl.symbol() = to_symbol_expr(*new_symbol);
928  set_decl(new_decl);
929  }
930  }
931  break;
932 
933  case DEAD:
934  {
935  auto new_symbol = f(get_dead().symbol());
936  if(new_symbol.has_value())
937  {
938  auto new_dead = get_dead();
939  new_dead.symbol() = to_symbol_expr(*new_symbol);
940  set_dead(new_dead);
941  }
942  }
943  break;
944 
945  case FUNCTION_CALL:
946  {
947  auto new_call = get_function_call();
948  bool change = false;
949 
950  auto new_lhs = f(new_call.lhs());
951  if(new_lhs.has_value())
952  {
953  new_call.lhs() = *new_lhs;
954  change = true;
955  }
956 
957  for(auto &a : new_call.arguments())
958  {
959  auto new_a = f(a);
960  if(new_a.has_value())
961  {
962  a = *new_a;
963  change = true;
964  }
965  }
966 
967  if(change)
968  set_function_call(new_call);
969  }
970  break;
971 
972  default:
973  if(has_condition())
974  {
975  auto new_condition = f(get_condition());
976  if(new_condition.has_value())
977  set_condition(new_condition.value());
978  }
979  }
980 }
981 
983  std::function<void(const exprt &)> f) const
984 {
985  switch(type)
986  {
987  case OTHER:
988  if(get_other().get_statement() == ID_expression)
989  f(to_code_expression(get_other()).expression());
990  break;
991 
992  case RETURN:
993  f(get_return().return_value());
994  break;
995 
996  case ASSIGN:
997  f(get_assign().lhs());
998  f(get_assign().rhs());
999  break;
1000 
1001  case DECL:
1002  f(get_decl().symbol());
1003  break;
1004 
1005  case DEAD:
1006  f(get_dead().symbol());
1007  break;
1008 
1009  case FUNCTION_CALL:
1010  {
1011  const auto &call = get_function_call();
1012  f(call.lhs());
1013  for(auto &a : call.arguments())
1014  f(a);
1015  }
1016  break;
1017 
1018  default:
1019  if(has_condition())
1020  f(get_condition());
1021  }
1022 }
1023 
1024 bool goto_programt::equals(const goto_programt &other) const
1025 {
1026  if(instructions.size() != other.instructions.size())
1027  return false;
1028 
1029  goto_programt::const_targett other_it = other.instructions.begin();
1030  for(const auto &ins : instructions)
1031  {
1032  if(!ins.equals(*other_it))
1033  return false;
1034 
1035  // the number of targets is the same as instructiont::equals returned "true"
1036  auto other_target_it = other_it->targets.begin();
1037  for(const auto t : ins.targets)
1038  {
1039  if(
1040  t->location_number - ins.location_number !=
1041  (*other_target_it)->location_number - other_it->location_number)
1042  {
1043  return false;
1044  }
1045 
1046  ++other_target_it;
1047  }
1048 
1049  ++other_it;
1050  }
1051 
1052  return true;
1053 }
1054 
1056 std::ostream &operator<<(std::ostream &out, goto_program_instruction_typet t)
1057 {
1058  switch(t)
1059  {
1060  case NO_INSTRUCTION_TYPE:
1061  out << "NO_INSTRUCTION_TYPE";
1062  break;
1063  case GOTO:
1064  out << "GOTO";
1065  break;
1066  case ASSUME:
1067  out << "ASSUME";
1068  break;
1069  case ASSERT:
1070  out << "ASSERT";
1071  break;
1072  case OTHER:
1073  out << "OTHER";
1074  break;
1075  case DECL:
1076  out << "DECL";
1077  break;
1078  case DEAD:
1079  out << "DEAD";
1080  break;
1081  case SKIP:
1082  out << "SKIP";
1083  break;
1084  case START_THREAD:
1085  out << "START_THREAD";
1086  break;
1087  case END_THREAD:
1088  out << "END_THREAD";
1089  break;
1090  case LOCATION:
1091  out << "LOCATION";
1092  break;
1093  case END_FUNCTION:
1094  out << "END_FUNCTION";
1095  break;
1096  case ATOMIC_BEGIN:
1097  out << "ATOMIC_BEGIN";
1098  break;
1099  case ATOMIC_END:
1100  out << "ATOMIC_END";
1101  break;
1102  case RETURN:
1103  out << "RETURN";
1104  break;
1105  case ASSIGN:
1106  out << "ASSIGN";
1107  break;
1108  case FUNCTION_CALL:
1109  out << "FUNCTION_CALL";
1110  break;
1111  default:
1112  out << "?";
1113  }
1114 
1115  return out;
1116 }
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3359
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:64
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:1253
bool is_nil() const
Definition: irep.h:393
const std::string & id2string(const irep_idt &d)
Definition: irep.h:42
bool is_not_nil() const
Definition: irep.h:397
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:91
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:518
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:957
#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:512
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
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:1802
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:3269
subt & get_sub()
Definition: irep.h:472
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:796
unsigned target_number
A number to identify branch targets.
Definition: goto_program.h:525
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:829
const irep_idt & id() const
Definition: irep.h:413
exprt & lhs()
Definition: std_code.h:298
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
Definition: goto_program.h:185
argumentst & arguments()
Definition: std_code.h:1161
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:4344
exprt & rhs()
Definition: std_code.h:303
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:576
API to expression classes.
instructionst::const_iterator const_targett
Definition: goto_program.h:571
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:3841
codet representation of a function call statement.
Definition: std_code.h:1107
#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:227
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:754
const source_locationt & source_location() const
Definition: type.h:64
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:2362
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:707
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1022
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:478
typename dt::subt subt
Definition: irep.h:185
void objects_written(const exprt &src, std::list< exprt > &dest)
const std::string & id_string() const
Definition: irep.h:416
#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:100
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:485
void find_type_symbols(const exprt &src, find_symbols_sett &dest)
operandst & operands()
Definition: expr.h:85
#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:1556
const irept & find(const irep_namet &name) const
Definition: irep.cpp:150
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:285
optionalt< const_targett > get_target(const unsigned location_number) const
Definition: goto_program.h:591
#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