CBMC
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 <util/invariant.h>
16 #include <util/source_location.h>
17 
18 #include "goto_instruction_code.h"
19 
20 #include <iosfwd>
21 #include <limits>
22 #include <list>
23 #include <set>
24 #include <string>
25 
26 class code_gotot;
27 class namespacet;
28 enum class validation_modet;
29 
32 {
34  GOTO = 1, // branch, possibly guarded
35  ASSUME = 2, // non-failing guarded self loop
36  ASSERT = 3, // assertions
37  OTHER = 4, // anything else
38  SKIP = 5, // just advance the PC
39  START_THREAD = 6, // spawns an asynchronous thread
40  END_THREAD = 7, // end the current thread
41  LOCATION = 8, // semantically like SKIP
42  END_FUNCTION = 9, // exit point of a function
43  ATOMIC_BEGIN = 10, // marks a block without interleavings
44  ATOMIC_END = 11, // end of a block without interleavings
45  SET_RETURN_VALUE = 12, // set function return value (no control-flow change)
46  ASSIGN = 13, // assignment lhs:=rhs
47  DECL = 14, // declare a local variable
48  DEAD = 15, // marks the end-of-live of a local variable
49  FUNCTION_CALL = 16, // call a function
50  THROW = 17, // throw an exception
51  CATCH = 18, // push, pop or enter an exception handler
52  INCOMPLETE_GOTO = 19 // goto where target is yet to be determined
53 };
54 
55 std::ostream &operator<<(std::ostream &, goto_program_instruction_typet);
56 
73 {
74 public:
76  goto_programt(const goto_programt &)=delete;
78 
79  // Move operations need to be explicitly enabled as they are deleted with the
80  // copy operations
81  // default for move operations isn't available on Windows yet, so define
82  // explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx
83  // under "Defaulted and Deleted Functions")
84 
86  instructions(std::move(other.instructions))
87  {
88  }
89 
91  {
92  instructions=std::move(other.instructions);
93  return *this;
94  }
95 
180  class instructiont final
181  {
182  protected:
185 
186  public:
189  {
190  return _code;
191  }
192 
195  {
196  return _code;
197  }
198 
200  const exprt &assign_lhs() const
201  {
203  return to_code_assign(_code).lhs();
204  }
205 
208  {
210  return to_code_assign(_code).lhs();
211  }
212 
214  const exprt &assign_rhs() const
215  {
217  return to_code_assign(_code).rhs();
218  }
219 
222  {
224  return to_code_assign(_code).rhs();
225  }
226 
228  const symbol_exprt &decl_symbol() const
229  {
231  auto &decl = expr_checked_cast<code_declt>(_code);
232  return decl.symbol();
233  }
234 
237  {
239  auto &decl = expr_checked_cast<code_declt>(_code);
240  return decl.symbol();
241  }
242 
244  const symbol_exprt &dead_symbol() const
245  {
247  return to_code_dead(_code).symbol();
248  }
249 
252  {
254  return to_code_dead(_code).symbol();
255  }
256 
258  const exprt &return_value() const
259  {
262  }
263 
266  {
269  }
270 
272  const exprt &call_function() const
273  {
276  }
277 
280  {
283  }
284 
286  const exprt &call_lhs() const
287  {
289  return to_code_function_call(_code).lhs();
290  }
291 
294  {
296  return to_code_function_call(_code).lhs();
297  }
298 
301  {
304  }
305 
308  {
311  }
312 
315  {
317  return _code;
318  }
319 
322  {
324  _code = std::move(c);
325  }
326 
329  protected:
331 
332  public:
334  {
335  return _source_location;
336  }
337 
339  {
340  return _source_location;
341  }
342 
345  {
346  return _type;
347  }
348 
349  protected:
350  // Use type() to access. To prevent malformed instructions, no non-const
351  // access method is provided.
353 
357 
358  public:
360  bool has_condition() const
361  {
362  return is_goto() || is_incomplete_goto() || is_assume() || is_assert();
363  }
364 
366  const exprt &condition() const
367  {
369  return guard;
370  }
371 
374  {
376  return guard;
377  }
378 
379  // The below will eventually become a single target only.
381  typedef std::list<instructiont>::iterator targett;
382  typedef std::list<instructiont>::const_iterator const_targett;
383  typedef std::list<targett> targetst;
384  typedef std::list<const_targett> const_targetst;
385 
391  struct target_less_than // NOLINT(readability/identifiers)
392  {
393  static inline bool
395  {
396  const instructiont &_i1 = *i1;
397  const instructiont &_i2 = *i2;
398  return &_i1 < &_i2;
399  }
400 
401  inline bool
402  operator()(const const_targett &i1, const const_targett &i2) const
403  {
404  return order_const_target(i1, i2);
405  }
406 
407  inline bool operator()(const targett &i1, const targett &i2) const
408  {
409  return &(*i1) < &(*i2);
410  }
411  };
412 
415 
419  {
420  PRECONDITION(targets.size() == 1);
421  return targets.front();
422  }
423 
427  {
428  PRECONDITION(targets.size()==1);
429  return targets.front();
430  }
431 
435  {
436  targets.clear();
437  targets.push_back(t);
438  }
439 
440  bool has_target() const
441  {
442  return !targets.empty();
443  }
444 
446  typedef std::list<irep_idt> labelst;
448 
449  // will go away
450  std::set<targett, target_less_than> incoming_edges;
451 
453  bool is_target() const
454  { return target_number!=nil_target; }
455 
458  {
459  _type = __type;
460  targets.clear();
461  guard=true_exprt();
462  _code.make_nil();
463  }
464 
468  {
469  clear(SKIP);
470  }
471 
475  {
476  PRECONDITION(_type == GOTO || _type == ASSERT);
477  _type = ASSUME;
478  targets.clear();
479  _code.make_nil();
480  }
481 
482  void complete_goto(targett _target)
483  {
485  _code.make_nil();
486  targets.push_back(_target);
487  _type = GOTO;
488  }
489 
490  // clang-format off
491  bool is_goto () const { return _type == GOTO; }
492  bool is_set_return_value() const { return _type == SET_RETURN_VALUE; }
493  bool is_assign () const { return _type == ASSIGN; }
494  bool is_function_call () const { return _type == FUNCTION_CALL; }
495  bool is_throw () const { return _type == THROW; }
496  bool is_catch () const { return _type == CATCH; }
497  bool is_skip () const { return _type == SKIP; }
498  bool is_location () const { return _type == LOCATION; }
499  bool is_other () const { return _type == OTHER; }
500  bool is_decl () const { return _type == DECL; }
501  bool is_dead () const { return _type == DEAD; }
502  bool is_assume () const { return _type == ASSUME; }
503  bool is_assert () const { return _type == ASSERT; }
504  bool is_atomic_begin () const { return _type == ATOMIC_BEGIN; }
505  bool is_atomic_end () const { return _type == ATOMIC_END; }
506  bool is_start_thread () const { return _type == START_THREAD; }
507  bool is_end_thread () const { return _type == END_THREAD; }
508  bool is_end_function () const { return _type == END_FUNCTION; }
509  bool is_incomplete_goto () const { return _type == INCOMPLETE_GOTO; }
510  // clang-format on
511 
513  instructiont(NO_INSTRUCTION_TYPE) // NOLINT(runtime/explicit)
514  {
515  }
516 
518  : _code(static_cast<const goto_instruction_codet &>(get_nil_irep())),
520  _type(__type),
521  guard(true_exprt())
522  {
523  }
524 
527  goto_instruction_codet __code,
528  source_locationt __source_location,
530  exprt _guard,
531  targetst _targets)
532  : _code(std::move(__code)),
533  _source_location(std::move(__source_location)),
534  _type(__type),
535  guard(std::move(_guard)),
536  targets(std::move(_targets))
537  {
538  }
539 
541  void swap(instructiont &instruction)
542  {
543  using std::swap;
544  swap(instruction._code, _code);
545  swap(instruction._source_location, _source_location);
546  swap(instruction._type, _type);
547  swap(instruction.guard, guard);
548  swap(instruction.targets, targets);
549  swap(instruction.labels, labels);
550  }
551 
553  static const unsigned nil_target=
554  std::numeric_limits<unsigned>::max();
555 
559  unsigned location_number = 0;
560 
562  unsigned loop_number = 0;
563 
567 
569  bool is_backwards_goto() const
570  {
571  if(!is_goto())
572  return false;
573 
574  for(const auto &t : targets)
575  if(t->location_number<=location_number)
576  return true;
577 
578  return false;
579  }
580 
581  std::string to_string() const
582  {
583  std::ostringstream instruction_id_builder;
584  instruction_id_builder << _type;
585  return instruction_id_builder.str();
586  }
587 
592  bool equals(const instructiont &other) const;
593 
598  void validate(const namespacet &ns, const validation_modet vm) const;
599 
602  void transform(std::function<std::optional<exprt>(exprt)>);
603 
605  void apply(std::function<void(const exprt &)>) const;
606 
608  std::ostream &output(std::ostream &) const;
609  };
610 
611  // Never try to change this to vector-we mutate the list while iterating
612  typedef std::list<instructiont> instructionst;
613 
614  typedef instructionst::iterator targett;
615  typedef instructionst::const_iterator const_targett;
616  typedef std::list<targett> targetst;
617  typedef std::list<const_targett> const_targetst;
618  // NOLINTNEXTLINE(readability/identifiers)
620 
623 
627  {
628  return instructions.erase(t, t);
629  }
630 
633  {
634  return t;
635  }
636 
637  template <typename Target>
638  std::list<Target> get_successors(Target target) const;
639 
640  void compute_incoming_edges();
641 
644  {
645  PRECONDITION(target!=instructions.end());
646  const auto next=std::next(target);
647  instructions.insert(next, instructiont())->swap(*target);
648  }
649 
668  void insert_before_swap(targett target, instructiont &instruction)
669  {
670  insert_before_swap(target);
671  target->swap(instruction);
672  }
673 
677  targett target,
678  goto_programt &p)
679  {
680  PRECONDITION(target!=instructions.end());
681  if(p.instructions.empty())
682  return;
683  insert_before_swap(target, p.instructions.front());
684  auto next=std::next(target);
685  p.instructions.erase(p.instructions.begin());
686  instructions.splice(next, p.instructions);
687  }
688 
693  {
694  return instructions.insert(target, instructiont());
695  }
696 
701  {
702  return instructions.insert(target, i);
703  }
704 
709  {
710  return instructions.insert(std::next(target), instructiont());
711  }
712 
717  {
718  return instructions.insert(std::next(target), i);
719  }
720 
723  {
724  instructions.splice(instructions.end(),
725  p.instructions);
726  }
727 
731  const_targett target,
732  goto_programt &p)
733  {
734  instructions.splice(target, p.instructions);
735  }
736 
739  targett add(instructiont &&instruction)
740  {
741  instructions.push_back(std::move(instruction));
742  return --instructions.end();
743  }
744 
748  {
749  return add(instructiont());
750  }
751 
755  {
756  return add(instructiont(type));
757  }
758 
760  std::ostream &output(std::ostream &out) const;
761 
763  void compute_target_numbers();
764 
766  void compute_location_numbers(unsigned &nr)
767  {
768  for(auto &i : instructions)
769  {
770  INVARIANT(
771  nr != std::numeric_limits<unsigned>::max(),
772  "Too many location numbers assigned");
773  i.location_number=nr++;
774  }
775  }
776 
779  {
780  unsigned nr=0;
782  }
783 
785  void compute_loop_numbers();
786 
788  void update();
789 
791  static irep_idt
792  loop_id(const irep_idt &function_id, const instructiont &instruction)
793  {
794  return id2string(function_id) + "." +
795  std::to_string(instruction.loop_number);
796  }
797 
799  bool empty() const
800  {
801  return instructions.empty();
802  }
803 
806  {
807  }
808 
810  {
811  }
812 
814  void swap(goto_programt &program)
815  {
816  program.instructions.swap(instructions);
817  }
818 
820  void clear()
821  {
822  instructions.clear();
823  }
824 
828  {
829  PRECONDITION(!instructions.empty());
830  const auto end_function=std::prev(instructions.end());
831  DATA_INVARIANT(end_function->is_end_function(),
832  "goto program ends on END_FUNCTION");
833  return end_function;
834  }
835 
839  {
840  PRECONDITION(!instructions.empty());
841  const auto end_function=std::prev(instructions.end());
842  DATA_INVARIANT(end_function->is_end_function(),
843  "goto program ends on END_FUNCTION");
844  return end_function;
845  }
846 
848  void copy_from(const goto_programt &src);
849 
851  bool has_assertion() const;
852 
853  typedef std::set<irep_idt> decl_identifierst;
855  void get_decl_identifiers(decl_identifierst &decl_identifiers) const;
856 
860  bool equals(const goto_programt &other) const;
861 
866  void validate(const namespacet &ns, const validation_modet vm) const
867  {
868  for(const instructiont &ins : instructions)
869  {
870  ins.validate(ns, vm);
871  }
872  }
873 
875  exprt return_value,
877  {
878  return instructiont(
879  code_returnt(std::move(return_value)),
880  l,
882  nil_exprt(),
883  {});
884  }
885 
887  const code_returnt &code,
888  const source_locationt &l = source_locationt::nil()) = delete;
889 
890  static instructiont
892  {
893  return instructiont(
894  static_cast<const goto_instruction_codet &>(get_nil_irep()),
895  l,
896  SKIP,
897  nil_exprt(),
898  {});
899  }
900 
902  {
903  return instructiont(
904  static_cast<const goto_instruction_codet &>(get_nil_irep()),
905  l,
906  LOCATION,
907  nil_exprt(),
908  {});
909  }
910 
911  static instructiont
913  {
914  return instructiont(
915  static_cast<const goto_instruction_codet &>(get_nil_irep()),
916  l,
917  THROW,
918  nil_exprt(),
919  {});
920  }
921 
922  static instructiont
924  {
925  return instructiont(
926  static_cast<const goto_instruction_codet &>(get_nil_irep()),
927  l,
928  CATCH,
929  nil_exprt(),
930  {});
931  }
932 
934  const exprt &g,
936  {
937  return instructiont(
938  static_cast<const goto_instruction_codet &>(get_nil_irep()),
939  l,
940  ASSERT,
941  exprt(g),
942  {});
943  }
944 
946  const exprt &g,
948  {
949  return instructiont(
950  static_cast<const goto_instruction_codet &>(get_nil_irep()),
951  l,
952  ASSUME,
953  g,
954  {});
955  }
956 
958  const goto_instruction_codet &_code,
960  {
961  return instructiont(_code, l, OTHER, nil_exprt(), {});
962  }
963 
965  const symbol_exprt &symbol,
967  {
968  return instructiont(code_declt(symbol), l, DECL, nil_exprt(), {});
969  }
970 
972  const symbol_exprt &symbol,
974  {
975  return instructiont(code_deadt(symbol), l, DEAD, nil_exprt(), {});
976  }
977 
978  static instructiont
980  {
981  return instructiont(
982  static_cast<const goto_instruction_codet &>(get_nil_irep()),
983  l,
984  ATOMIC_BEGIN,
985  nil_exprt(),
986  {});
987  }
988 
989  static instructiont
991  {
992  return instructiont(
993  static_cast<const goto_instruction_codet &>(get_nil_irep()),
994  l,
995  ATOMIC_END,
996  nil_exprt(),
997  {});
998  }
999 
1000  static instructiont
1002  {
1003  return instructiont(
1004  static_cast<const goto_instruction_codet &>(get_nil_irep()),
1005  l,
1006  END_FUNCTION,
1007  nil_exprt(),
1008  {});
1009  }
1010 
1012  const exprt &_cond,
1014  {
1015  PRECONDITION(_cond.is_boolean());
1016  return instructiont(
1017  static_cast<const goto_instruction_codet &>(get_nil_irep()),
1018  l,
1020  _cond,
1021  {});
1022  }
1023 
1024  static instructiont
1026  {
1027  return instructiont(
1028  static_cast<const goto_instruction_codet &>(get_nil_irep()),
1029  l,
1031  true_exprt(),
1032  {});
1033  }
1034 
1035  static instructiont make_incomplete_goto(
1036  const code_gotot &,
1038 
1040  targett _target,
1042  {
1043  return instructiont(
1044  static_cast<const goto_instruction_codet &>(get_nil_irep()),
1045  l,
1046  GOTO,
1047  true_exprt(),
1048  {_target});
1049  }
1050 
1052  targett _target,
1053  const exprt &g,
1055  {
1056  return instructiont(
1057  static_cast<const goto_instruction_codet &>(get_nil_irep()),
1058  l,
1059  GOTO,
1060  g,
1061  {_target});
1062  }
1063 
1066  const code_assignt &_code,
1068  {
1069  return instructiont(_code, l, ASSIGN, nil_exprt(), {});
1070  }
1071 
1074  exprt lhs,
1075  exprt rhs,
1077  {
1078  return instructiont(
1079  code_assignt(std::move(lhs), std::move(rhs)), l, ASSIGN, nil_exprt(), {});
1080  }
1081 
1083  const code_declt &_code,
1085  {
1086  return instructiont(_code, l, DECL, nil_exprt(), {});
1087  }
1088 
1091  const code_function_callt &_code,
1093  {
1094  return instructiont(_code, l, FUNCTION_CALL, nil_exprt(), {});
1095  }
1096 
1099  exprt lhs,
1100  exprt function,
1103  {
1104  return instructiont(
1105  code_function_callt(lhs, std::move(function), std::move(arguments)),
1106  l,
1107  FUNCTION_CALL,
1108  nil_exprt(),
1109  {});
1110  }
1111 };
1112 
1125 template <typename Target>
1127  Target target) const
1128 {
1129  if(target==instructions.end())
1130  return std::list<Target>();
1131 
1132  const auto next=std::next(target);
1133 
1134  const instructiont &i=*target;
1135 
1136  if(i.is_goto())
1137  {
1138  std::list<Target> successors(i.targets.begin(), i.targets.end());
1139 
1140  if(!i.condition().is_true() && next != instructions.end())
1141  successors.push_back(next);
1142 
1143  return successors;
1144  }
1145 
1146  if(i.is_start_thread())
1147  {
1148  std::list<Target> successors(i.targets.begin(), i.targets.end());
1149 
1150  if(next!=instructions.end())
1151  successors.push_back(next);
1152 
1153  return successors;
1154  }
1155 
1156  if(i.is_end_thread())
1157  {
1158  // no successors
1159  return std::list<Target>();
1160  }
1161 
1162  if(i.is_throw())
1163  {
1164  // the successors are non-obvious
1165  return std::list<Target>();
1166  }
1167 
1168  if(i.is_assume())
1169  {
1170  return !i.condition().is_false() && next != instructions.end()
1171  ? std::list<Target>{next}
1172  : std::list<Target>();
1173  }
1174 
1175  if(next!=instructions.end())
1176  {
1177  return std::list<Target>{next};
1178  }
1179 
1180  return std::list<Target>();
1181 }
1182 
1183 // NOLINTNEXTLINE(readability/identifiers)
1185 {
1186  std::size_t operator()(
1187  const goto_programt::const_targett t) const
1188  {
1189  using hash_typet = decltype(&(*t));
1190  return std::hash<hash_typet>{}(&(*t));
1191  }
1192 };
1193 
1197 {
1198  template <class A, class B>
1199  bool operator()(const A &a, const B &b) const
1200  {
1201  return &(*a) == &(*b);
1202  }
1203 };
1204 
1205 template <typename GotoFunctionT, typename PredicateT, typename HandlerT>
1207  GotoFunctionT &&goto_function,
1208  PredicateT predicate,
1209  HandlerT handler)
1210 {
1211  auto &&instructions = goto_function.body.instructions;
1212  for(auto it = instructions.begin(); it != instructions.end(); ++it)
1213  {
1214  if(predicate(it))
1215  {
1216  handler(it);
1217  }
1218  }
1219 }
1220 
1221 template <typename GotoFunctionT, typename HandlerT>
1222 void for_each_instruction(GotoFunctionT &&goto_function, HandlerT handler)
1223 {
1224  using iterator_t = decltype(goto_function.body.instructions.begin());
1226  goto_function, [](const iterator_t &) { return true; }, handler);
1227 }
1228 
1229 #define forall_goto_program_instructions(it, program) \
1230  for(goto_programt::instructionst::const_iterator \
1231  it=(program).instructions.begin(); \
1232  it!=(program).instructions.end(); it++)
1233 
1234 #define Forall_goto_program_instructions(it, program) \
1235  for(goto_programt::instructionst::iterator \
1236  it=(program).instructions.begin(); \
1237  it!=(program).instructions.end(); it++)
1238 
1239 std::list<exprt> objects_read(const goto_programt::instructiont &);
1240 std::list<exprt> objects_written(const goto_programt::instructiont &);
1241 
1242 std::list<exprt> expressions_read(const goto_programt::instructiont &);
1243 std::list<exprt> expressions_written(const goto_programt::instructiont &);
1244 
1245 std::string as_string(
1246  const namespacet &ns,
1247  const irep_idt &function,
1248  const goto_programt::instructiont &);
1249 
1250 #endif // CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
A goto_instruction_codet representing an assignment in the program.
A goto_instruction_codet representing the removal of a local variable going out of scope.
symbol_exprt & symbol()
A goto_instruction_codet representing the declaration of a local variable.
goto_instruction_codet representation of a function call statement.
exprt::operandst argumentst
codet representation of a goto statement.
Definition: std_code.h:841
goto_instruction_codet representation of a "return from a function" statement.
const exprt & return_value() const
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:27
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.h:224
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:34
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
unsigned target_number
A number to identify branch targets.
Definition: goto_program.h:566
const exprt & condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:366
void turn_into_skip()
Transforms an existing instruction into a skip, retaining the source_location.
Definition: goto_program.h:467
symbol_exprt & dead_symbol()
Get the symbol for DEAD.
Definition: goto_program.h:251
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
Definition: goto_program.h:286
void complete_goto(targett _target)
Definition: goto_program.h:482
bool is_target() const
Is this node a branch target?
Definition: goto_program.h:453
void set_target(targett t)
Sets the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:434
std::list< targett > targetst
Definition: goto_program.h:383
bool is_set_return_value() const
Definition: goto_program.h:492
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
Definition: goto_program.h:272
goto_instruction_codet _code
Do not read or modify directly – use code() and code_nonconst() instead.
Definition: goto_program.h:184
bool has_condition() const
Does this instruction have a condition?
Definition: goto_program.h:360
void apply(std::function< void(const exprt &)>) const
Apply given function to all expressions.
exprt & assign_rhs_nonconst()
Get the rhs of the assignment for ASSIGN.
Definition: goto_program.h:221
targetst targets
The list of successor instructions.
Definition: goto_program.h:414
exprt & condition_nonconst()
Get the condition of gotos, assume, assert.
Definition: goto_program.h:373
unsigned loop_number
Number unique per function to identify loops.
Definition: goto_program.h:562
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
Definition: goto_program.h:258
targett get_target()
Returns the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:426
const goto_instruction_codet & code() const
Get the code represented by this instruction.
Definition: goto_program.h:188
void turn_into_assume()
Transforms either an assertion or a GOTO instruction into an assumption, with the same condition.
Definition: goto_program.h:474
exprt & return_value()
Get the return value of a SET_RETURN_VALUE instruction.
Definition: goto_program.h:265
goto_program_instruction_typet _type
Definition: goto_program.h:352
const goto_instruction_codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:314
bool equals(const instructiont &other) const
Syntactic equality: two instructiont are equal if they have the same type, code, guard,...
symbol_exprt & decl_symbol()
Get the declared symbol for DECL.
Definition: goto_program.h:236
void transform(std::function< std::optional< exprt >(exprt)>)
Apply given transformer to all expressions; no return value means no change needed.
source_locationt & source_location_nonconst()
Definition: goto_program.h:338
exprt & call_function()
Get the function that is called for FUNCTION_CALL.
Definition: goto_program.h:279
std::string to_string() const
Definition: goto_program.h:581
unsigned location_number
A globally unique number to identify a program location.
Definition: goto_program.h:559
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
Definition: goto_program.h:569
source_locationt _source_location
The location of the instruction in the source file.
Definition: goto_program.h:330
std::list< instructiont >::const_iterator const_targett
Definition: goto_program.h:382
static const unsigned nil_target
Uniquely identify an invalid target or location.
Definition: goto_program.h:553
std::list< const_targett > const_targetst
Definition: goto_program.h:384
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
Definition: goto_program.h:214
std::set< targett, target_less_than > incoming_edges
Definition: goto_program.h:450
void clear(goto_program_instruction_typet __type)
Clear the node.
Definition: goto_program.h:457
const source_locationt & source_location() const
Definition: goto_program.h:333
std::list< instructiont >::iterator targett
The target for gotos and for start_thread nodes.
Definition: goto_program.h:381
goto_instruction_codet & code_nonconst()
Set the code represented by this instruction.
Definition: goto_program.h:194
std::ostream & output(std::ostream &) const
Output this instruction to the given stream.
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Definition: goto_program.h:244
exprt::operandst & call_arguments()
Get the arguments of a FUNCTION_CALL.
Definition: goto_program.h:307
instructiont(goto_instruction_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:526
exprt guard
Guard for gotos, assume, assert Use condition() method to access.
Definition: goto_program.h:356
exprt & call_lhs()
Get the lhs of a FUNCTION_CALL (may be nil)
Definition: goto_program.h:293
void set_other(goto_instruction_codet &c)
Set the statement for OTHER.
Definition: goto_program.h:321
instructiont(goto_program_instruction_typet __type)
Definition: goto_program.h:517
void swap(instructiont &instruction)
Swap two instructions.
Definition: goto_program.h:541
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
Definition: goto_program.h:228
std::list< irep_idt > labelst
Goto target labels.
Definition: goto_program.h:446
const_targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:418
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:200
goto_program_instruction_typet type() const
What kind of instruction?
Definition: goto_program.h:344
void validate(const namespacet &ns, const validation_modet vm) const
Check that the instruction is well-formed.
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
Definition: goto_program.h:300
exprt & assign_lhs_nonconst()
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:207
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:945
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
static instructiont make_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:874
void clear()
Clear the goto program.
Definition: goto_program.h:820
void insert_before_swap(targett target, instructiont &instruction)
Insertion that preserves jumps to "target".
Definition: goto_program.h:668
static instructiont make_decl(const code_declt &_code, const source_locationt &l=source_locationt::nil())
static instructiont make_incomplete_goto(const source_locationt &l=source_locationt::nil())
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:716
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:971
void update()
Update all indices.
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:626
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:643
std::ostream & output(std::ostream &out) const
Output goto-program to given stream.
bool has_assertion() const
Does the goto program have an assertion?
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:730
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
Definition: goto_program.h:792
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:700
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
instructionst::iterator targett
Definition: goto_program.h:614
goto_programt & operator=(goto_programt &&other)
Definition: goto_program.h:90
instructionst::const_iterator const_targett
Definition: goto_program.h:615
static instructiont make_set_return_value(const code_returnt &code, const source_locationt &l=source_locationt::nil())=delete
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto program is well-formed.
Definition: goto_program.h:866
targett add_instruction(goto_program_instruction_typet type)
Adds an instruction of given type at the end.
Definition: goto_program.h:754
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:747
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:722
static instructiont make_goto(targett _target, const exprt &g, const source_locationt &l=source_locationt::nil())
void insert_before_swap(targett target, goto_programt &p)
Insertion that preserves jumps to "target".
Definition: goto_program.h:676
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:990
goto_programt()
Constructor.
Definition: goto_program.h:805
void compute_incoming_edges()
Compute for each instruction the set of instructions it is a successor of.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett get_end_function()
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
Definition: goto_program.h:827
std::list< instructiont > instructionst
Definition: goto_program.h:612
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:853
std::list< const_targett > const_targetst
Definition: goto_program.h:617
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:891
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:708
goto_programt(const goto_programt &)=delete
Copying is deleted as this class contains pointers that cannot be copied.
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
static instructiont make_throw(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:912
static instructiont make_other(const goto_instruction_codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:957
const_targett const_cast_target(const_targett t) const
Dummy for templates with possible const contexts.
Definition: goto_program.h:632
void compute_location_numbers(unsigned &nr)
Compute location numbers.
Definition: goto_program.h:766
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
instructiont::target_less_than target_less_than
Definition: goto_program.h:619
const_targett get_end_function() const
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
Definition: goto_program.h:838
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
static instructiont make_catch(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:923
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:979
goto_programt(goto_programt &&other)
Definition: goto_program.h:85
void compute_location_numbers()
Compute location numbers.
Definition: goto_program.h:778
void swap(goto_programt &program)
Swap the goto program.
Definition: goto_program.h:814
goto_programt & operator=(const goto_programt &)=delete
static instructiont make_location(const source_locationt &l)
Definition: goto_program.h:901
void compute_target_numbers()
Compute the target numbers.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:739
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
bool empty() const
Is the program empty?
Definition: goto_program.h:799
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...
static instructiont make_function_call(exprt lhs, exprt function, code_function_callt::argumentst arguments, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:964
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:933
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:692
static instructiont make_assignment(exprt lhs, exprt rhs, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
void compute_loop_numbers()
Compute loop numbers.
std::list< targett > targetst
Definition: goto_program.h:616
void make_nil()
Definition: irep.h:446
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
The NIL expression.
Definition: std_expr.h:3081
static const source_locationt & nil()
Expression to hold a symbol (variable)
Definition: std_expr.h:131
The Boolean constant true.
Definition: std_expr.h:3063
const code_returnt & to_code_return(const goto_instruction_codet &code)
const code_assignt & to_code_assign(const goto_instruction_codet &code)
const code_deadt & to_code_dead(const goto_instruction_codet &code)
const code_function_callt & to_code_function_call(const goto_instruction_codet &code)
std::list< exprt > expressions_read(const goto_programt::instructiont &)
std::list< exprt > objects_written(const goto_programt::instructiont &)
void for_each_instruction(GotoFunctionT &&goto_function, HandlerT handler)
std::list< exprt > expressions_written(const goto_programt::instructiont &)
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:32
@ FUNCTION_CALL
Definition: goto_program.h:49
@ ATOMIC_END
Definition: goto_program.h:44
@ DEAD
Definition: goto_program.h:48
@ LOCATION
Definition: goto_program.h:41
@ END_FUNCTION
Definition: goto_program.h:42
@ ASSIGN
Definition: goto_program.h:46
@ ASSERT
Definition: goto_program.h:36
@ SET_RETURN_VALUE
Definition: goto_program.h:45
@ ATOMIC_BEGIN
Definition: goto_program.h:43
@ CATCH
Definition: goto_program.h:51
@ END_THREAD
Definition: goto_program.h:40
@ SKIP
Definition: goto_program.h:38
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
@ START_THREAD
Definition: goto_program.h:39
@ THROW
Definition: goto_program.h:50
@ DECL
Definition: goto_program.h:47
@ OTHER
Definition: goto_program.h:37
@ GOTO
Definition: goto_program.h:34
@ INCOMPLETE_GOTO
Definition: goto_program.h:52
@ ASSUME
Definition: goto_program.h:35
std::string as_string(const namespacet &ns, const irep_idt &function, const goto_programt::instructiont &)
void for_each_instruction_if(GotoFunctionT &&goto_function, PredicateT predicate, HandlerT handler)
std::ostream & operator<<(std::ostream &, goto_program_instruction_typet)
Outputs a string representation of a goto_program_instruction_typet
std::list< exprt > objects_read(const goto_programt::instructiont &)
const irept & get_nil_irep()
Definition: irep.cpp:19
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::size_t operator()(const goto_programt::const_targett t) const
A total order over targett and const_targett.
Definition: goto_program.h:392
static bool order_const_target(const const_targett i1, const const_targett i2)
Definition: goto_program.h:394
bool operator()(const targett &i1, const targett &i2) const
Definition: goto_program.h:407
bool operator()(const const_targett &i1, const const_targett &i2) const
Definition: goto_program.h:402
Functor to check whether iterators from different collections point at the same object.
bool operator()(const A &a, const B &b) const
validation_modet