cprover
goto_program.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Concrete Goto Program
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
13 #define CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
14 
15 #include <iosfwd>
16 #include <set>
17 #include <limits>
18 #include <sstream>
19 #include <string>
20 
21 #include <util/deprecate.h>
22 #include <util/invariant.h>
23 #include <util/namespace.h>
24 #include <util/source_location.h>
25 #include <util/std_code.h>
26 #include <util/std_expr.h>
27 #include <util/symbol_table.h>
28 
29 enum class validation_modet;
30 
33 {
35  GOTO = 1, // branch, possibly guarded
36  ASSUME = 2, // non-failing guarded self loop
37  ASSERT = 3, // assertions
38  OTHER = 4, // anything else
39  SKIP = 5, // just advance the PC
40  START_THREAD = 6, // spawns an asynchronous thread
41  END_THREAD = 7, // end the current thread
42  LOCATION = 8, // semantically like SKIP
43  END_FUNCTION = 9, // exit point of a function
44  ATOMIC_BEGIN = 10, // marks a block without interleavings
45  ATOMIC_END = 11, // end of a block without interleavings
46  RETURN = 12, // set function return value (no control-flow change)
47  ASSIGN = 13, // assignment lhs:=rhs
48  DECL = 14, // declare a local variable
49  DEAD = 15, // marks the end-of-live of a local variable
50  FUNCTION_CALL = 16, // call a function
51  THROW = 17, // throw an exception
52  CATCH = 18, // push, pop or enter an exception handler
53  INCOMPLETE_GOTO = 19 // goto where target is yet to be determined
54 };
55 
56 std::ostream &operator<<(std::ostream &, goto_program_instruction_typet);
57 
74 {
75 public:
77  goto_programt(const goto_programt &)=delete;
79 
80  // Move operations need to be explicitly enabled as they are deleted with the
81  // copy operations
82  // default for move operations isn't available on Windows yet, so define
83  // explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx
84  // under "Defaulted and Deleted Functions")
85 
87  instructions(std::move(other.instructions))
88  {
89  }
90 
92  {
93  instructions=std::move(other.instructions);
94  return *this;
95  }
96 
179  class instructiont final
180  {
181  protected:
184 
185  public:
187  const codet &get_code() const
188  {
189  return code;
190  }
191 
194  {
195  return code;
196  }
197 
199  const code_assignt &get_assign() const
200  {
202  return to_code_assign(code);
203  }
204 
207  {
209  code = std::move(c);
210  }
211 
213  DEPRECATED(SINCE(2021, 2, 24, "Use decl_symbol instead"))
214  const code_declt &get_decl() const
215  {
217  const auto &decl = expr_checked_cast<code_declt>(code);
218  INVARIANT(
219  !decl.initial_value(),
220  "code_declt in goto program may not contain initialization.");
221  return decl;
222  }
223 
225  const symbol_exprt &decl_symbol() const
226  {
228  auto &decl = expr_checked_cast<code_declt>(code);
229  INVARIANT(
230  !decl.initial_value(),
231  "code_declt in goto program may not contain initialization.");
232  return decl.symbol();
233  }
234 
237  {
239  auto &decl = expr_checked_cast<code_declt>(code);
240  INVARIANT(
241  !decl.initial_value(),
242  "code_declt in goto program may not contain initialization.");
243  return decl.symbol();
244  }
245 
247  DEPRECATED(SINCE(2021, 2, 24, "Use decl_symbol instead"))
249  {
251  INVARIANT(
252  !c.initial_value(),
253  "Initialization must be separated from code_declt before adding to "
254  "goto_instructiont.");
255  code = std::move(c);
256  }
257 
259  DEPRECATED(SINCE(2021, 2, 24, "Use dead_symbol instead"))
260  const code_deadt &get_dead() const
261  {
263  return to_code_dead(code);
264  }
265 
267  const symbol_exprt &dead_symbol() const
268  {
270  return to_code_dead(code).symbol();
271  }
272 
275  {
277  return to_code_dead(code).symbol();
278  }
279 
281  DEPRECATED(SINCE(2021, 2, 24, "Use dead_symbol instead"))
283  {
285  code = std::move(c);
286  }
287 
289  DEPRECATED(SINCE(2021, 2, 24, "Use return_value instead"))
290  const code_returnt &get_return() const
291  {
293  return to_code_return(code);
294  }
295 
297  const exprt &return_value() const
298  {
300  return to_code_return(code).return_value();
301  }
302 
305  {
307  return to_code_return(code).return_value();
308  }
309 
311  DEPRECATED(SINCE(2021, 2, 24, "Use return_value instead"))
313  {
315  code = std::move(c);
316  }
317 
320  {
322  return to_code_function_call(code);
323  }
324 
327  {
329  code = std::move(c);
330  }
331 
333  const codet &get_other() const
334  {
336  return code;
337  }
338 
340  void set_other(codet &c)
341  {
343  code = std::move(c);
344  }
345 
348 
351 
355 
357  bool has_condition() const
358  {
359  return is_goto() || is_incomplete_goto() || is_assume() || is_assert();
360  }
361 
363  const exprt &get_condition() const
364  {
366  return guard;
367  }
368 
371  {
373  guard = std::move(c);
374  }
375 
376  // The below will eventually become a single target only.
378  typedef std::list<instructiont>::iterator targett;
379  typedef std::list<instructiont>::const_iterator const_targett;
380  typedef std::list<targett> targetst;
381  typedef std::list<const_targett> const_targetst;
382 
385 
389  {
390  PRECONDITION(targets.size()==1);
391  return targets.front();
392  }
393 
397  {
398  targets.clear();
399  targets.push_back(t);
400  }
401 
402  bool has_target() const
403  {
404  return !targets.empty();
405  }
406 
408  typedef std::list<irep_idt> labelst;
410 
411  // will go away
412  std::set<targett> incoming_edges;
413 
415  bool is_target() const
416  { return target_number!=nil_target; }
417 
420  {
421  type=_type;
422  targets.clear();
423  guard=true_exprt();
424  code.make_nil();
425  }
426 
430  {
431  clear(SKIP);
432  }
433 
434  void complete_goto(targett _target)
435  {
437  code.make_nil();
438  targets.push_back(_target);
439  type = GOTO;
440  }
441 
442  bool is_goto () const { return type==GOTO; }
443  bool is_return () const { return type==RETURN; }
444  bool is_assign () const { return type==ASSIGN; }
445  bool is_function_call() const { return type==FUNCTION_CALL; }
446  bool is_throw () const { return type==THROW; }
447  bool is_catch () const { return type==CATCH; }
448  bool is_skip () const { return type==SKIP; }
449  bool is_location () const { return type==LOCATION; }
450  bool is_other () const { return type==OTHER; }
451  bool is_decl () const { return type==DECL; }
452  bool is_dead () const { return type==DEAD; }
453  bool is_assume () const { return type==ASSUME; }
454  bool is_assert () const { return type==ASSERT; }
455  bool is_atomic_begin () const { return type==ATOMIC_BEGIN; }
456  bool is_atomic_end () const { return type==ATOMIC_END; }
457  bool is_start_thread () const { return type==START_THREAD; }
458  bool is_end_thread () const { return type==END_THREAD; }
459  bool is_end_function () const { return type==END_FUNCTION; }
460  bool is_incomplete_goto() const
461  {
462  return type == INCOMPLETE_GOTO;
463  }
464 
466  instructiont(NO_INSTRUCTION_TYPE) // NOLINT(runtime/explicit)
467  {
468  }
469 
471  : code(static_cast<const codet &>(get_nil_irep())),
472  source_location(static_cast<const source_locationt &>(get_nil_irep())),
473  type(_type),
474  guard(true_exprt())
475  {
476  }
477 
480  codet _code,
481  source_locationt _source_location,
483  exprt _guard,
484  targetst _targets)
485  : code(std::move(_code)),
486  source_location(std::move(_source_location)),
487  type(_type),
488  guard(std::move(_guard)),
489  targets(std::move(_targets))
490  {
491  }
492 
494  void swap(instructiont &instruction)
495  {
496  using std::swap;
497  swap(instruction.code, code);
498  swap(instruction.source_location, source_location);
499  swap(instruction.type, type);
500  swap(instruction.guard, guard);
501  swap(instruction.targets, targets);
502  }
503 
505  static const unsigned nil_target=
506  std::numeric_limits<unsigned>::max();
507 
511  unsigned location_number = 0;
512 
514  unsigned loop_number = 0;
515 
519 
521  bool is_backwards_goto() const
522  {
523  if(!is_goto())
524  return false;
525 
526  for(const auto &t : targets)
527  if(t->location_number<=location_number)
528  return true;
529 
530  return false;
531  }
532 
533  std::string to_string() const
534  {
535  std::ostringstream instruction_id_builder;
536  instruction_id_builder << type;
537  return instruction_id_builder.str();
538  }
539 
544  bool equals(const instructiont &other) const;
545 
550  void validate(const namespacet &ns, const validation_modet vm) const;
551 
554  void transform(std::function<optionalt<exprt>(exprt)>);
555 
557  void apply(std::function<void(const exprt &)>) const;
558  };
559 
560  // Never try to change this to vector-we mutate the list while iterating
561  typedef std::list<instructiont> instructionst;
562 
563  typedef instructionst::iterator targett;
564  typedef instructionst::const_iterator const_targett;
565  typedef std::list<targett> targetst;
566  typedef std::list<const_targett> const_targetst;
567 
570 
574  {
575  return instructions.erase(t, t);
576  }
577 
580  {
581  return t;
582  }
583 
584  template <typename Target>
585  std::list<Target> get_successors(Target target) const;
586 
587  void compute_incoming_edges();
588 
591  {
592  PRECONDITION(target!=instructions.end());
593  const auto next=std::next(target);
594  instructions.insert(next, instructiont())->swap(*target);
595  }
596 
599  void insert_before_swap(targett target, instructiont &instruction)
600  {
601  insert_before_swap(target);
602  target->swap(instruction);
603  }
604 
608  targett target,
609  goto_programt &p)
610  {
611  PRECONDITION(target!=instructions.end());
612  if(p.instructions.empty())
613  return;
614  insert_before_swap(target, p.instructions.front());
615  auto next=std::next(target);
616  p.instructions.erase(p.instructions.begin());
617  instructions.splice(next, p.instructions);
618  }
619 
624  {
625  return instructions.insert(target, instructiont());
626  }
627 
632  {
633  return instructions.insert(target, i);
634  }
635 
640  {
641  return instructions.insert(std::next(target), instructiont());
642  }
643 
648  {
649  return instructions.insert(std::next(target), i);
650  }
651 
654  {
655  instructions.splice(instructions.end(),
656  p.instructions);
657  }
658 
662  const_targett target,
663  goto_programt &p)
664  {
665  instructions.splice(target, p.instructions);
666  }
667 
670  targett add(instructiont &&instruction)
671  {
672  instructions.push_back(std::move(instruction));
673  return --instructions.end();
674  }
675 
679  {
680  return add(instructiont());
681  }
682 
686  {
687  return add(instructiont(type));
688  }
689 
691  std::ostream &output(
692  const namespacet &ns,
693  const irep_idt &identifier,
694  std::ostream &out) const;
695 
697  std::ostream &output(std::ostream &out) const
698  {
699  return output(namespacet(symbol_tablet()), irep_idt(), out);
700  }
701 
703  std::ostream &output_instruction(
704  const namespacet &ns,
705  const irep_idt &identifier,
706  std::ostream &out,
707  const instructionst::value_type &instruction) const;
708 
710  void compute_target_numbers();
711 
713  void compute_location_numbers(unsigned &nr)
714  {
715  for(auto &i : instructions)
716  {
717  INVARIANT(
718  nr != std::numeric_limits<unsigned>::max(),
719  "Too many location numbers assigned");
720  i.location_number=nr++;
721  }
722  }
723 
726  {
727  unsigned nr=0;
729  }
730 
732  void compute_loop_numbers();
733 
735  void update();
736 
738  static irep_idt
739  loop_id(const irep_idt &function_id, const instructiont &instruction)
740  {
741  return id2string(function_id) + "." +
742  std::to_string(instruction.loop_number);
743  }
744 
746  bool empty() const
747  {
748  return instructions.empty();
749  }
750 
753  {
754  }
755 
757  {
758  }
759 
761  void swap(goto_programt &program)
762  {
763  program.instructions.swap(instructions);
764  }
765 
767  void clear()
768  {
769  instructions.clear();
770  }
771 
775  {
776  PRECONDITION(!instructions.empty());
777  const auto end_function=std::prev(instructions.end());
778  DATA_INVARIANT(end_function->is_end_function(),
779  "goto program ends on END_FUNCTION");
780  return end_function;
781  }
782 
786  {
787  PRECONDITION(!instructions.empty());
788  const auto end_function=std::prev(instructions.end());
789  DATA_INVARIANT(end_function->is_end_function(),
790  "goto program ends on END_FUNCTION");
791  return end_function;
792  }
793 
795  void copy_from(const goto_programt &src);
796 
798  bool has_assertion() const;
799 
800  typedef std::set<irep_idt> decl_identifierst;
802  void get_decl_identifiers(decl_identifierst &decl_identifiers) const;
803 
807  bool equals(const goto_programt &other) const;
808 
813  void validate(const namespacet &ns, const validation_modet vm) const
814  {
815  for(const instructiont &ins : instructions)
816  {
817  ins.validate(ns, vm);
818  }
819  }
820 
821  static instructiont
823  {
824  return instructiont(code_returnt(), l, RETURN, nil_exprt(), {});
825  }
826 
828  code_returnt c,
830  {
831  return instructiont(std::move(c), l, RETURN, nil_exprt(), {});
832  }
833 
834  static instructiont
836  {
837  return instructiont(
838  static_cast<const codet &>(get_nil_irep()),
839  l,
840  SKIP,
841  nil_exprt(),
842  {});
843  }
844 
846  {
847  return instructiont(
848  static_cast<const codet &>(get_nil_irep()),
849  l,
850  LOCATION,
851  nil_exprt(),
852  {});
853  }
854 
855  static instructiont
857  {
858  return instructiont(
859  static_cast<const codet &>(get_nil_irep()),
860  l,
861  THROW,
862  nil_exprt(),
863  {});
864  }
865 
866  static instructiont
868  {
869  return instructiont(
870  static_cast<const codet &>(get_nil_irep()),
871  l,
872  CATCH,
873  nil_exprt(),
874  {});
875  }
876 
878  const exprt &g,
880  {
881  return instructiont(
882  static_cast<const codet &>(get_nil_irep()),
883  l,
884  ASSERT,
885  exprt(g),
886  {});
887  }
888 
890  const exprt &g,
892  {
893  return instructiont(
894  static_cast<const codet &>(get_nil_irep()), l, ASSUME, g, {});
895  }
896 
898  const codet &_code,
900  {
901  return instructiont(_code, l, OTHER, nil_exprt(), {});
902  }
903 
905  const symbol_exprt &symbol,
907  {
908  return instructiont(code_declt(symbol), l, DECL, nil_exprt(), {});
909  }
910 
912  const symbol_exprt &symbol,
914  {
915  return instructiont(code_deadt(symbol), l, DEAD, nil_exprt(), {});
916  }
917 
918  static instructiont
920  {
921  return instructiont(
922  static_cast<const codet &>(get_nil_irep()),
923  l,
924  ATOMIC_BEGIN,
925  nil_exprt(),
926  {});
927  }
928 
929  static instructiont
931  {
932  return instructiont(
933  static_cast<const codet &>(get_nil_irep()),
934  l,
935  ATOMIC_END,
936  nil_exprt(),
937  {});
938  }
939 
940  static instructiont
942  {
943  return instructiont(
944  static_cast<const codet &>(get_nil_irep()),
945  l,
946  END_FUNCTION,
947  nil_exprt(),
948  {});
949  }
950 
952  const exprt &_cond,
954  {
955  PRECONDITION(_cond.type().id() == ID_bool);
956  return instructiont(
957  static_cast<const codet &>(get_nil_irep()),
958  l,
960  _cond,
961  {});
962  }
963 
964  static instructiont
966  {
967  return instructiont(
968  static_cast<const codet &>(get_nil_irep()),
969  l,
971  true_exprt(),
972  {});
973  }
974 
976  const code_gotot &_code,
978  {
979  return instructiont(_code, l, INCOMPLETE_GOTO, true_exprt(), {});
980  }
981 
983  targett _target,
985  {
986  return instructiont(
987  static_cast<const codet &>(get_nil_irep()),
988  l,
989  GOTO,
990  true_exprt(),
991  {_target});
992  }
993 
995  targett _target,
996  const exprt &g,
998  {
999  return instructiont(
1000  static_cast<const codet &>(get_nil_irep()),
1001  l,
1002  GOTO,
1003  g,
1004  {_target});
1005  }
1006 
1009  const code_assignt &_code,
1011  {
1012  return instructiont(_code, l, ASSIGN, nil_exprt(), {});
1013  }
1014 
1017  exprt lhs,
1018  exprt rhs,
1020  {
1021  return instructiont(
1022  code_assignt(std::move(lhs), std::move(rhs)), l, ASSIGN, nil_exprt(), {});
1023  }
1024 
1026  const code_declt &_code,
1028  {
1029  return instructiont(_code, l, DECL, nil_exprt(), {});
1030  }
1031 
1034  const code_function_callt &_code,
1036  {
1037  return instructiont(_code, l, FUNCTION_CALL, nil_exprt(), {});
1038  }
1039 
1042  exprt function,
1045  {
1046  return instructiont(
1047  code_function_callt(std::move(function), std::move(arguments)),
1048  l,
1049  FUNCTION_CALL,
1050  nil_exprt(),
1051  {});
1052  }
1053 };
1054 
1067 template <typename Target>
1069  Target target) const
1070 {
1071  if(target==instructions.end())
1072  return std::list<Target>();
1073 
1074  const auto next=std::next(target);
1075 
1076  const instructiont &i=*target;
1077 
1078  if(i.is_goto())
1079  {
1080  std::list<Target> successors(i.targets.begin(), i.targets.end());
1081 
1082  if(!i.get_condition().is_true() && next != instructions.end())
1083  successors.push_back(next);
1084 
1085  return successors;
1086  }
1087 
1088  if(i.is_start_thread())
1089  {
1090  std::list<Target> successors(i.targets.begin(), i.targets.end());
1091 
1092  if(next!=instructions.end())
1093  successors.push_back(next);
1094 
1095  return successors;
1096  }
1097 
1098  if(i.is_end_thread())
1099  {
1100  // no successors
1101  return std::list<Target>();
1102  }
1103 
1104  if(i.is_throw())
1105  {
1106  // the successors are non-obvious
1107  return std::list<Target>();
1108  }
1109 
1110  if(i.is_assume())
1111  {
1112  return !i.get_condition().is_false() && next != instructions.end()
1113  ? std::list<Target>{next}
1114  : std::list<Target>();
1115  }
1116 
1117  if(next!=instructions.end())
1118  {
1119  return std::list<Target>{next};
1120  }
1121 
1122  return std::list<Target>();
1123 }
1124 
1128 {
1129  const goto_programt::instructiont &_i1=*i1;
1130  const goto_programt::instructiont &_i2=*i2;
1131  return &_i1<&_i2;
1132 }
1133 
1134 // NOLINTNEXTLINE(readability/identifiers)
1136 {
1137  std::size_t operator()(
1138  const goto_programt::const_targett t) const
1139  {
1140  using hash_typet = decltype(&(*t));
1141  return std::hash<hash_typet>{}(&(*t));
1142  }
1143 };
1144 
1148 {
1149  template <class A, class B>
1150  bool operator()(const A &a, const B &b) const
1151  {
1152  return &(*a) == &(*b);
1153  }
1154 };
1155 
1156 template <typename GotoFunctionT, typename PredicateT, typename HandlerT>
1158  GotoFunctionT &&goto_function,
1159  PredicateT predicate,
1160  HandlerT handler)
1161 {
1162  auto &&instructions = goto_function.body.instructions;
1163  for(auto it = instructions.begin(); it != instructions.end(); ++it)
1164  {
1165  if(predicate(it))
1166  {
1167  handler(it);
1168  }
1169  }
1170 }
1171 
1172 template <typename GotoFunctionT, typename HandlerT>
1173 void for_each_instruction(GotoFunctionT &&goto_function, HandlerT handler)
1174 {
1175  using iterator_t = decltype(goto_function.body.instructions.begin());
1177  goto_function, [](const iterator_t &) { return true; }, handler);
1178 }
1179 
1180 #define forall_goto_program_instructions(it, program) \
1181  for(goto_programt::instructionst::const_iterator \
1182  it=(program).instructions.begin(); \
1183  it!=(program).instructions.end(); it++)
1184 
1185 #define Forall_goto_program_instructions(it, program) \
1186  for(goto_programt::instructionst::iterator \
1187  it=(program).instructions.begin(); \
1188  it!=(program).instructions.end(); it++)
1189 
1190 inline bool operator<(
1191  const goto_programt::const_targett &i1,
1192  const goto_programt::const_targett &i2)
1193 {
1194  return order_const_target(i1, i2);
1195 }
1196 
1197 inline bool operator<(
1198  const goto_programt::targett &i1,
1199  const goto_programt::targett &i2)
1200 {
1201  return &(*i1)<&(*i2);
1202 }
1203 
1204 std::list<exprt> objects_read(const goto_programt::instructiont &);
1205 std::list<exprt> objects_written(const goto_programt::instructiont &);
1206 
1207 std::list<exprt> expressions_read(const goto_programt::instructiont &);
1208 std::list<exprt> expressions_written(const goto_programt::instructiont &);
1209 
1210 std::string as_string(
1211  const namespacet &ns,
1212  const irep_idt &function,
1213  const goto_programt::instructiont &);
1214 
1215 #endif // CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
goto_programt::instructiont::is_skip
bool is_skip() const
Definition: goto_program.h:448
goto_programt::instructiont::get_dead
const code_deadt & get_dead() const
Get the dead statement for DEAD.
Definition: goto_program.h:260
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
goto_programt::instructiont::is_throw
bool is_throw() const
Definition: goto_program.h:446
goto_programt::instructiont::has_target
bool has_target() const
Definition: goto_program.h:402
goto_programt::instructiont::set_other
void set_other(codet &c)
Set the statement for OTHER.
Definition: goto_program.h:340
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
goto_programt::~goto_programt
~goto_programt()
Definition: goto_program.h:756
operator<
bool operator<(const goto_programt::const_targett &i1, const goto_programt::const_targett &i2)
Definition: goto_program.h:1190
goto_programt::instructiont::source_location
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:347
goto_programt::instructiont::labelst
std::list< irep_idt > labelst
Goto target labels.
Definition: goto_program.h:408
goto_programt::instructiont::complete_goto
void complete_goto(targett _target)
Definition: goto_program.h:434
goto_programt::insert_after
targett insert_after(const_targett target, const instructiont &i)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:647
goto_programt::make_dead
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:911
goto_programt::instructiont::set_assign
void set_assign(code_assignt c)
Set the assignment for ASSIGN.
Definition: goto_program.h:206
goto_programt::instructiont::to_string
std::string to_string() const
Definition: goto_program.h:533
goto_programt::instructiont::is_other
bool is_other() const
Definition: goto_program.h:450
irept::make_nil
void make_nil()
Definition: irep.h:465
goto_programt::instructiont::swap
void swap(instructiont &instruction)
Swap two instructions.
Definition: goto_program.h:494
goto_programt::const_cast_target
const_targett const_cast_target(const_targett t) const
Dummy for templates with possible const contexts.
Definition: goto_program.h:579
goto_programt::instructiont::clear
void clear(goto_program_instruction_typet _type)
Clear the node.
Definition: goto_program.h:419
goto_programt::compute_loop_numbers
void compute_loop_numbers()
Compute loop numbers.
Definition: goto_program.cpp:532
goto_programt::const_targetst
std::list< const_targett > const_targetst
Definition: goto_program.h:566
goto_programt::instructiont::get_return
const code_returnt & get_return() const
Get the return statement for READ.
Definition: goto_program.h:290
goto_programt::goto_programt
goto_programt(const goto_programt &)=delete
Copying is deleted as this class contains pointers that cannot be copied.
goto_programt::instructiont::set_return
void set_return(code_returnt c)
Set the return statement for READ.
Definition: goto_program.h:312
goto_programt::instructionst
std::list< instructiont > instructionst
Definition: goto_program.h:561
for_each_instruction_if
void for_each_instruction_if(GotoFunctionT &&goto_function, PredicateT predicate, HandlerT handler)
Definition: goto_program.h:1157
goto_programt::instructiont::type
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:350
goto_programt::instructiont::is_dead
bool is_dead() const
Definition: goto_program.h:452
source_locationt::nil
static const source_locationt & nil()
Definition: source_location.h:188
expressions_read
std::list< exprt > expressions_read(const goto_programt::instructiont &)
Definition: goto_program.cpp:273
goto_programt::instructiont::decl_symbol
symbol_exprt & decl_symbol()
Get the declared symbol for DECL.
Definition: goto_program.h:236
goto_programt::instructiont::is_catch
bool is_catch() const
Definition: goto_program.h:447
goto_programt::update
void update()
Update all indices.
Definition: goto_program.cpp:540
goto_programt::copy_from
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
Definition: goto_program.cpp:625
goto_programt::instructiont::apply
void apply(std::function< void(const exprt &)>) const
Apply given function to all expressions.
Definition: goto_program.cpp:1022
invariant.h
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
goto_programt::make_end_function
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:941
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:670
goto_programt::instructiont::transform
void transform(std::function< optionalt< exprt >(exprt)>)
Apply given transformer to all expressions; no return value means no change needed.
Definition: goto_program.cpp:909
goto_programt::empty
bool empty() const
Is the program empty?
Definition: goto_program.h:746
exprt
Base class for all expressions.
Definition: expr.h:54
pointee_address_equalt
Functor to check whether iterators from different collections point at the same object.
Definition: goto_program.h:1148
goto_programt::insert_before_swap
void insert_before_swap(targett target, goto_programt &p)
Insertion that preserves jumps to "target".
Definition: goto_program.h:607
goto_programt::instructiont::set_decl
void set_decl(code_declt c)
Set the declaration for DECL.
Definition: goto_program.h:248
goto_programt::get_decl_identifiers
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
Definition: goto_program.cpp:230
objects_written
std::list< exprt > objects_written(const goto_programt::instructiont &)
Definition: goto_program.cpp:423
goto_programt::has_assertion
bool has_assertion() const
Does the goto program have an assertion?
Definition: goto_program.cpp:666
irep_idt
dstringt irep_idt
Definition: irep.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:384
goto_programt::instructiont::is_incomplete_goto
bool is_incomplete_goto() const
Definition: goto_program.h:460
goto_programt::make_return
static instructiont make_return(code_returnt c, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:827
goto_programt::get_successors
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
Definition: goto_program.h:1068
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:60
goto_programt::insert_before_swap
void insert_before_swap(targett target, instructiont &instruction)
Insertion that preserves jumps to "target".
Definition: goto_program.h:599
goto_programt::instructiont::is_end_thread
bool is_end_thread() const
Definition: goto_program.h:458
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
goto_programt::make_decl
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:904
namespace.h
goto_programt::instructiont::decl_symbol
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
Definition: goto_program.h:225
goto_programt::instructiont::is_atomic_end
bool is_atomic_end() const
Definition: goto_program.h:456
goto_programt::instructiont::instructiont
instructiont()
Definition: goto_program.h:465
goto_programt::instructiont::get_assign
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
Definition: goto_program.h:199
objects_read
std::list< exprt > objects_read(const goto_programt::instructiont &)
Definition: goto_program.cpp:396
goto_programt::get_end_function
const_targett get_end_function() const
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
Definition: goto_program.h:785
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:1008
goto_programt::make_goto
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:982
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:69
goto_programt::instructiont::get_other
const codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:333
goto_programt::instructiont::get_code
const codet & get_code() const
Get the code represented by this instruction.
Definition: goto_program.h:187
goto_programt::instructiont::const_targett
std::list< instructiont >::const_iterator const_targett
Definition: goto_program.h:379
goto_programt::loop_id
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
Definition: goto_program.h:739
goto_programt::instructiont::is_atomic_begin
bool is_atomic_begin() const
Definition: goto_program.h:455
goto_programt::instructiont::set_function_call
void set_function_call(code_function_callt c)
Set the function call for FUNCTION_CALL.
Definition: goto_program.h:326
goto_programt::targetst
std::list< targett > targetst
Definition: goto_program.h:565
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
goto_programt::make_function_call
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
Definition: goto_program.h:1033
goto_programt::add_instruction
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:678
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
THROW
@ THROW
Definition: goto_program.h:51
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
goto_programt::insert_before
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:623
GOTO
@ GOTO
Definition: goto_program.h:35
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:1077
goto_programt::instructiont::validate
void validate(const namespacet &ns, const validation_modet vm) const
Check that the instruction is well-formed.
Definition: goto_program.cpp:708
goto_programt::instructiont::turn_into_skip
void turn_into_skip()
Transforms an existing instruction into a skip, retaining the source_location.
Definition: goto_program.h:429
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:877
goto_programt::compute_target_numbers
void compute_target_numbers()
Compute the target numbers.
Definition: goto_program.cpp:571
goto_programt::make_decl
static instructiont make_decl(const code_declt &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:1025
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
goto_programt::destructive_insert
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:661
goto_programt::instructiont::dead_symbol
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Definition: goto_program.h:267
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
deprecate.h
goto_programt::goto_programt
goto_programt(goto_programt &&other)
Definition: goto_program.h:86
goto_programt::output_instruction
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
Definition: goto_program.cpp:42
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:183
goto_programt::output
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
Definition: goto_program.cpp:548
goto_programt::instructiont::targett
std::list< instructiont >::iterator targett
The target for gotos and for start_thread nodes.
Definition: goto_program.h:378
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:835
goto_programt::instructiont::is_decl
bool is_decl() const
Definition: goto_program.h:451
code_gotot
codet representation of a goto statement.
Definition: std_code.h:1159
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
goto_programt::compute_location_numbers
void compute_location_numbers(unsigned &nr)
Compute location numbers.
Definition: goto_program.h:713
to_code_dead
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:551
nil_exprt
The NIL expression.
Definition: std_expr.h:2734
goto_programt::instructiont::is_backwards_goto
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
Definition: goto_program.h:521
goto_programt::instructiont::is_location
bool is_location() const
Definition: goto_program.h:449
pointee_address_equalt::operator()
bool operator()(const A &a, const B &b) const
Definition: goto_program.h:1150
goto_programt::instructiont::labels
labelst labels
Definition: goto_program.h:409
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:319
goto_programt::instructiont::equals
bool equals(const instructiont &other) const
Syntactic equality: two instructiont are equal if they have the same type, code, guard,...
Definition: goto_program.cpp:696
expressions_written
std::list< exprt > expressions_written(const goto_programt::instructiont &)
Definition: goto_program.cpp:328
source_location.h
goto_programt::instructiont::has_condition
bool has_condition() const
Does this instruction have a condition?
Definition: goto_program.h:357
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:34
goto_programt::make_atomic_begin
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:919
OTHER
@ OTHER
Definition: goto_program.h:38
goto_programt::goto_programt
goto_programt()
Constructor.
Definition: goto_program.h:752
validation_modet
validation_modet
Definition: validation_mode.h:13
code_deadt::symbol
symbol_exprt & symbol()
Definition: std_code.h:505
irept::id
const irep_idt & id() const
Definition: irep.h:407
goto_programt::instructiont::is_end_function
bool is_end_function() const
Definition: goto_program.h:459
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1326
goto_programt::validate
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto program is well-formed.
Definition: goto_program.h:813
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1224
to_code_return
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1391
const_target_hash
Definition: goto_program.h:1136
goto_programt::add_instruction
targett add_instruction(goto_program_instruction_typet type)
Adds an instruction of given type at the end.
Definition: goto_program.h:685
END_FUNCTION
@ END_FUNCTION
Definition: goto_program.h:43
SKIP
@ SKIP
Definition: goto_program.h:39
code_deadt
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:499
goto_programt::instructiont::set_target
void set_target(targett t)
Sets the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:396
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
goto_programt::instructiont::return_value
exprt & return_value()
Get the return value of a RETURN instruction.
Definition: goto_program.h:304
goto_programt::compute_incoming_edges
void compute_incoming_edges()
Compute for each instruction the set of instructions it is a successor of.
Definition: goto_program.cpp:676
std_code.h
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
goto_programt::instructiont::targetst
std::list< targett > targetst
Definition: goto_program.h:380
goto_programt::clear
void clear()
Clear the goto program.
Definition: goto_program.h:767
goto_programt::instructiont::return_value
const exprt & return_value() const
Get the return value of a RETURN instruction.
Definition: goto_program.h:297
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:653
goto_programt::output
std::ostream & output(std::ostream &out) const
Output goto-program to given stream.
Definition: goto_program.h:697
goto_program_instruction_typet
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:33
goto_programt::instructiont::is_goto
bool is_goto() const
Definition: goto_program.h:442
goto_programt::make_return
static instructiont make_return(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:822
source_locationt
Definition: source_location.h:20
goto_programt::instructiont::get_decl
const code_declt & get_decl() const
Get the declaration for DECL.
Definition: goto_program.h:214
RETURN
@ RETURN
Definition: goto_program.h:46
goto_programt::get_end_function
targett get_end_function()
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
Definition: goto_program.h:774
goto_programt::compute_location_numbers
void compute_location_numbers()
Compute location numbers.
Definition: goto_program.h:725
goto_programt::make_goto
static instructiont make_goto(targett _target, const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:994
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:569
ASSIGN
@ ASSIGN
Definition: goto_program.h:47
goto_programt::instructiont::is_assert
bool is_assert() const
Definition: goto_program.h:454
goto_programt::instructiont::target_number
unsigned target_number
A number to identify branch targets.
Definition: goto_program.h:518
goto_programt::operator=
goto_programt & operator=(goto_programt &&other)
Definition: goto_program.h:91
CATCH
@ CATCH
Definition: goto_program.h:52
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1342
DECL
@ DECL
Definition: goto_program.h:48
goto_programt::instructiont::incoming_edges
std::set< targett > incoming_edges
Definition: goto_program.h:412
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
goto_programt::make_function_call
static instructiont make_function_call(exprt function, code_function_callt::argumentst arguments, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
Definition: goto_program.h:1041
goto_programt::instructiont::location_number
unsigned location_number
A globally unique number to identify a program location.
Definition: goto_program.h:511
goto_programt::insert_before
targett insert_before(const_targett target, const instructiont &i)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:631
goto_programt::const_cast_target
targett const_cast_target(const_targett t)
Convert a const_targett to a targett - use with care and avoid whenever possible.
Definition: goto_program.h:573
as_string
std::string as_string(const namespacet &ns, const irep_idt &function, const goto_programt::instructiont &)
goto_programt::instructiont::dead_symbol
symbol_exprt & dead_symbol()
Get the symbol for DEAD.
Definition: goto_program.h:274
ASSUME
@ ASSUME
Definition: goto_program.h:36
goto_programt::make_other
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:897
goto_programt::make_incomplete_goto
static instructiont make_incomplete_goto(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:965
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:354
goto_programt::instructiont::is_assign
bool is_assign() const
Definition: goto_program.h:444
order_const_target
bool order_const_target(const goto_programt::const_targett i1, const goto_programt::const_targett i2)
Definition: goto_program.h:1125
goto_programt::instructiont::loop_number
unsigned loop_number
Number unique per function to identify loops.
Definition: goto_program.h:514
START_THREAD
@ START_THREAD
Definition: goto_program.h:40
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:50
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
operator<<
std::ostream & operator<<(std::ostream &, goto_program_instruction_typet)
Outputs a string representation of a goto_program_instruction_typet
Definition: goto_program.cpp:1109
goto_programt::insert_after
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:639
goto_programt::instructiont::set_condition
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
Definition: goto_program.h:370
ATOMIC_END
@ ATOMIC_END
Definition: goto_program.h:45
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:564
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:26
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:889
DEAD
@ DEAD
Definition: goto_program.h:49
goto_programt::instructiont::const_targetst
std::list< const_targett > const_targetst
Definition: goto_program.h:381
goto_programt::operator=
goto_programt & operator=(const goto_programt &)=delete
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition: goto_program.h:44
goto_programt::make_incomplete_goto
static instructiont make_incomplete_goto(const code_gotot &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:975
goto_programt::instructiont::is_assume
bool is_assume() const
Definition: goto_program.h:453
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
goto_programt::instructiont::set_dead
void set_dead(code_deadt c)
Set the dead statement for DEAD.
Definition: goto_program.h:282
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:590
symbol_table.h
Author: Diffblue Ltd.
goto_programt::make_throw
static instructiont make_throw(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:856
for_each_instruction
void for_each_instruction(GotoFunctionT &&goto_function, HandlerT handler)
Definition: goto_program.h:1173
code_returnt::return_value
const exprt & return_value() const
Definition: std_code.h:1352
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
goto_programt::instructiont::is_start_thread
bool is_start_thread() const
Definition: goto_program.h:457
true_exprt
The Boolean constant true.
Definition: std_expr.h:2716
goto_programt::instructiont::get_condition
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:363
LOCATION
@ LOCATION
Definition: goto_program.h:42
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:445
ASSERT
@ ASSERT
Definition: goto_program.h:37
goto_programt::decl_identifierst
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:800
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
std_expr.h
API to expression classes.
goto_programt::instructiont::is_target
bool is_target() const
Is this node a branch target?
Definition: goto_program.h:415
goto_programt::instructiont::instructiont
instructiont(codet _code, source_locationt _source_location, goto_program_instruction_typet _type, exprt _guard, targetst _targets)
Constructor that can set all members, passed by value.
Definition: goto_program.h:479
goto_programt::instructiont::code_nonconst
codet & code_nonconst()
Set the code represented by this instruction.
Definition: goto_program.h:193
goto_programt::instructiont::nil_target
static const unsigned nil_target
Uniquely identify an invalid target or location.
Definition: goto_program.h:505
goto_programt::make_location
static instructiont make_location(const source_locationt &l)
Definition: goto_program.h:845
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:388
END_THREAD
@ END_THREAD
Definition: goto_program.h:41
goto_programt::swap
void swap(goto_programt &program)
Swap the goto program.
Definition: goto_program.h:761
INCOMPLETE_GOTO
@ INCOMPLETE_GOTO
Definition: goto_program.h:53
goto_programt::make_assignment
static instructiont make_assignment(exprt lhs, exprt rhs, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:1016
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:563
goto_programt::instructiont::instructiont
instructiont(goto_program_instruction_typet _type)
Definition: goto_program.h:470
goto_programt::make_incomplete_goto
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:951
const_target_hash::operator()
std::size_t operator()(const goto_programt::const_targett t) const
Definition: goto_program.h:1137
goto_programt::make_catch
static instructiont make_catch(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:867
goto_programt::instructiont::is_return
bool is_return() const
Definition: goto_program.h:443
goto_programt::make_atomic_end
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:930
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35