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 "goto_instruction_code.h"
16 
17 #include <iosfwd>
18 #include <set>
19 #include <limits>
20 #include <string>
21 
22 #include <util/deprecate.h>
23 #include <util/invariant.h>
24 #include <util/namespace.h>
25 #include <util/source_location.h>
26 
27 class code_gotot;
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 
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 exprt &assign_lhs() const
200  {
202  return to_code_assign(code).lhs();
203  }
204 
207  {
209  return to_code_assign(code).lhs();
210  }
211 
213  const exprt &assign_rhs() const
214  {
216  return to_code_assign(code).rhs();
217  }
218 
221  {
223  return to_code_assign(code).rhs();
224  }
225 
227  const symbol_exprt &decl_symbol() const
228  {
230  auto &decl = expr_checked_cast<code_declt>(code);
231  return decl.symbol();
232  }
233 
236  {
238  auto &decl = expr_checked_cast<code_declt>(code);
239  return decl.symbol();
240  }
241 
243  const symbol_exprt &dead_symbol() const
244  {
246  return to_code_dead(code).symbol();
247  }
248 
251  {
253  return to_code_dead(code).symbol();
254  }
255 
257  const exprt &return_value() const
258  {
260  return to_code_return(code).return_value();
261  }
262 
265  {
267  return to_code_return(code).return_value();
268  }
269 
271  const exprt &call_function() const
272  {
275  }
276 
279  {
282  }
283 
285  const exprt &call_lhs() const
286  {
288  return to_code_function_call(code).lhs();
289  }
290 
293  {
295  return to_code_function_call(code).lhs();
296  }
297 
300  {
303  }
304 
307  {
310  }
311 
313  const codet &get_other() const
314  {
316  return code;
317  }
318 
320  void set_other(codet &c)
321  {
323  code = std::move(c);
324  }
325 
328  protected:
330 
331  public:
333  {
334  return _source_location;
335  }
336 
338  {
339  return _source_location;
340  }
341 
344  {
345  return _type;
346  }
347 
348  protected:
349  // Use type() to access. To prevent malformed instructions, no non-const
350  // access method is provided.
352 
353  public:
358 
360  bool has_condition() const
361  {
362  return is_goto() || is_incomplete_goto() || is_assume() || is_assert();
363  }
364 
366  DEPRECATED(SINCE(2021, 10, 12, "Use condition() instead"))
367  const exprt &get_condition() const
368  {
370  return guard;
371  }
372 
374  DEPRECATED(SINCE(2021, 10, 12, "Use condition_nonconst() instead"))
376  {
378  guard = std::move(c);
379  }
380 
382  const exprt &condition() const
383  {
385  return guard;
386  }
387 
390  {
392  return guard;
393  }
394 
395  // The below will eventually become a single target only.
397  typedef std::list<instructiont>::iterator targett;
398  typedef std::list<instructiont>::const_iterator const_targett;
399  typedef std::list<targett> targetst;
400  typedef std::list<const_targett> const_targetst;
401 
404 
408  {
409  PRECONDITION(targets.size()==1);
410  return targets.front();
411  }
412 
416  {
417  targets.clear();
418  targets.push_back(t);
419  }
420 
421  bool has_target() const
422  {
423  return !targets.empty();
424  }
425 
427  typedef std::list<irep_idt> labelst;
429 
430  // will go away
431  std::set<targett> incoming_edges;
432 
434  bool is_target() const
435  { return target_number!=nil_target; }
436 
439  {
440  _type = __type;
441  targets.clear();
442  guard=true_exprt();
443  code.make_nil();
444  }
445 
449  {
450  clear(SKIP);
451  }
452 
456  {
457  PRECONDITION(_type == GOTO || _type == ASSERT);
458  _type = ASSUME;
459  targets.clear();
460  code.make_nil();
461  }
462 
463  void complete_goto(targett _target)
464  {
466  code.make_nil();
467  targets.push_back(_target);
468  _type = GOTO;
469  }
470 
471  // clang-format off
472  bool is_goto () const { return _type == GOTO; }
473  bool is_set_return_value() const { return _type == SET_RETURN_VALUE; }
474  bool is_assign () const { return _type == ASSIGN; }
475  bool is_function_call () const { return _type == FUNCTION_CALL; }
476  bool is_throw () const { return _type == THROW; }
477  bool is_catch () const { return _type == CATCH; }
478  bool is_skip () const { return _type == SKIP; }
479  bool is_location () const { return _type == LOCATION; }
480  bool is_other () const { return _type == OTHER; }
481  bool is_decl () const { return _type == DECL; }
482  bool is_dead () const { return _type == DEAD; }
483  bool is_assume () const { return _type == ASSUME; }
484  bool is_assert () const { return _type == ASSERT; }
485  bool is_atomic_begin () const { return _type == ATOMIC_BEGIN; }
486  bool is_atomic_end () const { return _type == ATOMIC_END; }
487  bool is_start_thread () const { return _type == START_THREAD; }
488  bool is_end_thread () const { return _type == END_THREAD; }
489  bool is_end_function () const { return _type == END_FUNCTION; }
490  bool is_incomplete_goto () const { return _type == INCOMPLETE_GOTO; }
491  // clang-format on
492 
494  instructiont(NO_INSTRUCTION_TYPE) // NOLINT(runtime/explicit)
495  {
496  }
497 
499  : code(static_cast<const codet &>(get_nil_irep())),
500  _source_location(static_cast<const source_locationt &>(get_nil_irep())),
501  _type(__type),
502  guard(true_exprt())
503  {
504  }
505 
508  codet _code,
509  source_locationt __source_location,
511  exprt _guard,
512  targetst _targets)
513  : code(std::move(_code)),
514  _source_location(std::move(__source_location)),
515  _type(__type),
516  guard(std::move(_guard)),
517  targets(std::move(_targets))
518  {
519  }
520 
522  void swap(instructiont &instruction)
523  {
524  using std::swap;
525  swap(instruction.code, code);
526  swap(instruction._source_location, _source_location);
527  swap(instruction._type, _type);
528  swap(instruction.guard, guard);
529  swap(instruction.targets, targets);
530  swap(instruction.labels, labels);
531  }
532 
534  static const unsigned nil_target=
535  std::numeric_limits<unsigned>::max();
536 
540  unsigned location_number = 0;
541 
543  unsigned loop_number = 0;
544 
548 
550  bool is_backwards_goto() const
551  {
552  if(!is_goto())
553  return false;
554 
555  for(const auto &t : targets)
556  if(t->location_number<=location_number)
557  return true;
558 
559  return false;
560  }
561 
562  std::string to_string() const
563  {
564  std::ostringstream instruction_id_builder;
565  instruction_id_builder << _type;
566  return instruction_id_builder.str();
567  }
568 
573  bool equals(const instructiont &other) const;
574 
579  void validate(const namespacet &ns, const validation_modet vm) const;
580 
583  void transform(std::function<optionalt<exprt>(exprt)>);
584 
586  void apply(std::function<void(const exprt &)>) const;
587  };
588 
589  // Never try to change this to vector-we mutate the list while iterating
590  typedef std::list<instructiont> instructionst;
591 
592  typedef instructionst::iterator targett;
593  typedef instructionst::const_iterator const_targett;
594  typedef std::list<targett> targetst;
595  typedef std::list<const_targett> const_targetst;
596 
599 
603  {
604  return instructions.erase(t, t);
605  }
606 
609  {
610  return t;
611  }
612 
613  template <typename Target>
614  std::list<Target> get_successors(Target target) const;
615 
616  void compute_incoming_edges();
617 
620  {
621  PRECONDITION(target!=instructions.end());
622  const auto next=std::next(target);
623  instructions.insert(next, instructiont())->swap(*target);
624  }
625 
644  void insert_before_swap(targett target, instructiont &instruction)
645  {
646  insert_before_swap(target);
647  target->swap(instruction);
648  }
649 
653  targett target,
654  goto_programt &p)
655  {
656  PRECONDITION(target!=instructions.end());
657  if(p.instructions.empty())
658  return;
659  insert_before_swap(target, p.instructions.front());
660  auto next=std::next(target);
661  p.instructions.erase(p.instructions.begin());
662  instructions.splice(next, p.instructions);
663  }
664 
669  {
670  return instructions.insert(target, instructiont());
671  }
672 
677  {
678  return instructions.insert(target, i);
679  }
680 
685  {
686  return instructions.insert(std::next(target), instructiont());
687  }
688 
693  {
694  return instructions.insert(std::next(target), i);
695  }
696 
699  {
700  instructions.splice(instructions.end(),
701  p.instructions);
702  }
703 
707  const_targett target,
708  goto_programt &p)
709  {
710  instructions.splice(target, p.instructions);
711  }
712 
715  targett add(instructiont &&instruction)
716  {
717  instructions.push_back(std::move(instruction));
718  return --instructions.end();
719  }
720 
724  {
725  return add(instructiont());
726  }
727 
731  {
732  return add(instructiont(type));
733  }
734 
736  std::ostream &output(
737  const namespacet &ns,
738  const irep_idt &identifier,
739  std::ostream &out) const;
740 
742  std::ostream &output(std::ostream &out) const;
743 
745  std::ostream &output_instruction(
746  const namespacet &ns,
747  const irep_idt &identifier,
748  std::ostream &out,
749  const instructionst::value_type &instruction) const;
750 
752  void compute_target_numbers();
753 
755  void compute_location_numbers(unsigned &nr)
756  {
757  for(auto &i : instructions)
758  {
759  INVARIANT(
760  nr != std::numeric_limits<unsigned>::max(),
761  "Too many location numbers assigned");
762  i.location_number=nr++;
763  }
764  }
765 
768  {
769  unsigned nr=0;
771  }
772 
774  void compute_loop_numbers();
775 
777  void update();
778 
780  static irep_idt
781  loop_id(const irep_idt &function_id, const instructiont &instruction)
782  {
783  return id2string(function_id) + "." +
784  std::to_string(instruction.loop_number);
785  }
786 
788  bool empty() const
789  {
790  return instructions.empty();
791  }
792 
795  {
796  }
797 
799  {
800  }
801 
803  void swap(goto_programt &program)
804  {
805  program.instructions.swap(instructions);
806  }
807 
809  void clear()
810  {
811  instructions.clear();
812  }
813 
817  {
818  PRECONDITION(!instructions.empty());
819  const auto end_function=std::prev(instructions.end());
820  DATA_INVARIANT(end_function->is_end_function(),
821  "goto program ends on END_FUNCTION");
822  return end_function;
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 
837  void copy_from(const goto_programt &src);
838 
840  bool has_assertion() const;
841 
842  typedef std::set<irep_idt> decl_identifierst;
844  void get_decl_identifiers(decl_identifierst &decl_identifiers) const;
845 
849  bool equals(const goto_programt &other) const;
850 
855  void validate(const namespacet &ns, const validation_modet vm) const
856  {
857  for(const instructiont &ins : instructions)
858  {
859  ins.validate(ns, vm);
860  }
861  }
862 
864  exprt return_value,
866  {
867  return instructiont(
868  code_returnt(std::move(return_value)),
869  l,
871  nil_exprt(),
872  {});
873  }
874 
876  const code_returnt &code,
877  const source_locationt &l = source_locationt::nil()) = delete;
878 
879  static instructiont
881  {
882  return instructiont(
883  static_cast<const codet &>(get_nil_irep()),
884  l,
885  SKIP,
886  nil_exprt(),
887  {});
888  }
889 
891  {
892  return instructiont(
893  static_cast<const codet &>(get_nil_irep()),
894  l,
895  LOCATION,
896  nil_exprt(),
897  {});
898  }
899 
900  static instructiont
902  {
903  return instructiont(
904  static_cast<const codet &>(get_nil_irep()),
905  l,
906  THROW,
907  nil_exprt(),
908  {});
909  }
910 
911  static instructiont
913  {
914  return instructiont(
915  static_cast<const codet &>(get_nil_irep()),
916  l,
917  CATCH,
918  nil_exprt(),
919  {});
920  }
921 
923  const exprt &g,
925  {
926  return instructiont(
927  static_cast<const codet &>(get_nil_irep()),
928  l,
929  ASSERT,
930  exprt(g),
931  {});
932  }
933 
935  const exprt &g,
937  {
938  return instructiont(
939  static_cast<const codet &>(get_nil_irep()), l, ASSUME, g, {});
940  }
941 
943  const codet &_code,
945  {
946  return instructiont(_code, l, OTHER, nil_exprt(), {});
947  }
948 
950  const symbol_exprt &symbol,
952  {
953  return instructiont(code_declt(symbol), l, DECL, nil_exprt(), {});
954  }
955 
957  const symbol_exprt &symbol,
959  {
960  return instructiont(code_deadt(symbol), l, DEAD, nil_exprt(), {});
961  }
962 
963  static instructiont
965  {
966  return instructiont(
967  static_cast<const codet &>(get_nil_irep()),
968  l,
969  ATOMIC_BEGIN,
970  nil_exprt(),
971  {});
972  }
973 
974  static instructiont
976  {
977  return instructiont(
978  static_cast<const codet &>(get_nil_irep()),
979  l,
980  ATOMIC_END,
981  nil_exprt(),
982  {});
983  }
984 
985  static instructiont
987  {
988  return instructiont(
989  static_cast<const codet &>(get_nil_irep()),
990  l,
991  END_FUNCTION,
992  nil_exprt(),
993  {});
994  }
995 
997  const exprt &_cond,
999  {
1000  PRECONDITION(_cond.type().id() == ID_bool);
1001  return instructiont(
1002  static_cast<const codet &>(get_nil_irep()),
1003  l,
1005  _cond,
1006  {});
1007  }
1008 
1009  static instructiont
1011  {
1012  return instructiont(
1013  static_cast<const codet &>(get_nil_irep()),
1014  l,
1016  true_exprt(),
1017  {});
1018  }
1019 
1020  static instructiont make_incomplete_goto(
1021  const code_gotot &,
1023 
1025  targett _target,
1027  {
1028  return instructiont(
1029  static_cast<const codet &>(get_nil_irep()),
1030  l,
1031  GOTO,
1032  true_exprt(),
1033  {_target});
1034  }
1035 
1037  targett _target,
1038  const exprt &g,
1040  {
1041  return instructiont(
1042  static_cast<const codet &>(get_nil_irep()),
1043  l,
1044  GOTO,
1045  g,
1046  {_target});
1047  }
1048 
1051  const code_assignt &_code,
1053  {
1054  return instructiont(_code, l, ASSIGN, nil_exprt(), {});
1055  }
1056 
1059  exprt lhs,
1060  exprt rhs,
1062  {
1063  return instructiont(
1064  code_assignt(std::move(lhs), std::move(rhs)), l, ASSIGN, nil_exprt(), {});
1065  }
1066 
1068  const code_declt &_code,
1070  {
1071  return instructiont(_code, l, DECL, nil_exprt(), {});
1072  }
1073 
1076  const code_function_callt &_code,
1078  {
1079  return instructiont(_code, l, FUNCTION_CALL, nil_exprt(), {});
1080  }
1081 
1084  exprt lhs,
1085  exprt function,
1088  {
1089  return instructiont(
1090  code_function_callt(lhs, std::move(function), std::move(arguments)),
1091  l,
1092  FUNCTION_CALL,
1093  nil_exprt(),
1094  {});
1095  }
1096 };
1097 
1110 template <typename Target>
1112  Target target) const
1113 {
1114  if(target==instructions.end())
1115  return std::list<Target>();
1116 
1117  const auto next=std::next(target);
1118 
1119  const instructiont &i=*target;
1120 
1121  if(i.is_goto())
1122  {
1123  std::list<Target> successors(i.targets.begin(), i.targets.end());
1124 
1125  if(!i.get_condition().is_true() && next != instructions.end())
1126  successors.push_back(next);
1127 
1128  return successors;
1129  }
1130 
1131  if(i.is_start_thread())
1132  {
1133  std::list<Target> successors(i.targets.begin(), i.targets.end());
1134 
1135  if(next!=instructions.end())
1136  successors.push_back(next);
1137 
1138  return successors;
1139  }
1140 
1141  if(i.is_end_thread())
1142  {
1143  // no successors
1144  return std::list<Target>();
1145  }
1146 
1147  if(i.is_throw())
1148  {
1149  // the successors are non-obvious
1150  return std::list<Target>();
1151  }
1152 
1153  if(i.is_assume())
1154  {
1155  return !i.get_condition().is_false() && next != instructions.end()
1156  ? std::list<Target>{next}
1157  : std::list<Target>();
1158  }
1159 
1160  if(next!=instructions.end())
1161  {
1162  return std::list<Target>{next};
1163  }
1164 
1165  return std::list<Target>();
1166 }
1167 
1171 {
1172  const goto_programt::instructiont &_i1=*i1;
1173  const goto_programt::instructiont &_i2=*i2;
1174  return &_i1<&_i2;
1175 }
1176 
1177 // NOLINTNEXTLINE(readability/identifiers)
1179 {
1180  std::size_t operator()(
1181  const goto_programt::const_targett t) const
1182  {
1183  using hash_typet = decltype(&(*t));
1184  return std::hash<hash_typet>{}(&(*t));
1185  }
1186 };
1187 
1191 {
1192  template <class A, class B>
1193  bool operator()(const A &a, const B &b) const
1194  {
1195  return &(*a) == &(*b);
1196  }
1197 };
1198 
1199 template <typename GotoFunctionT, typename PredicateT, typename HandlerT>
1201  GotoFunctionT &&goto_function,
1202  PredicateT predicate,
1203  HandlerT handler)
1204 {
1205  auto &&instructions = goto_function.body.instructions;
1206  for(auto it = instructions.begin(); it != instructions.end(); ++it)
1207  {
1208  if(predicate(it))
1209  {
1210  handler(it);
1211  }
1212  }
1213 }
1214 
1215 template <typename GotoFunctionT, typename HandlerT>
1216 void for_each_instruction(GotoFunctionT &&goto_function, HandlerT handler)
1217 {
1218  using iterator_t = decltype(goto_function.body.instructions.begin());
1220  goto_function, [](const iterator_t &) { return true; }, handler);
1221 }
1222 
1223 #define forall_goto_program_instructions(it, program) \
1224  for(goto_programt::instructionst::const_iterator \
1225  it=(program).instructions.begin(); \
1226  it!=(program).instructions.end(); it++)
1227 
1228 #define Forall_goto_program_instructions(it, program) \
1229  for(goto_programt::instructionst::iterator \
1230  it=(program).instructions.begin(); \
1231  it!=(program).instructions.end(); it++)
1232 
1233 inline bool operator<(
1234  const goto_programt::const_targett &i1,
1235  const goto_programt::const_targett &i2)
1236 {
1237  return order_const_target(i1, i2);
1238 }
1239 
1240 inline bool operator<(
1241  const goto_programt::targett &i1,
1242  const goto_programt::targett &i2)
1243 {
1244  return &(*i1)<&(*i2);
1245 }
1246 
1247 std::list<exprt> objects_read(const goto_programt::instructiont &);
1248 std::list<exprt> objects_written(const goto_programt::instructiont &);
1249 
1250 std::list<exprt> expressions_read(const goto_programt::instructiont &);
1251 std::list<exprt> expressions_written(const goto_programt::instructiont &);
1252 
1253 std::string as_string(
1254  const namespacet &ns,
1255  const irep_idt &function,
1256  const goto_programt::instructiont &);
1257 
1258 #endif // CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
A codet representing an assignment in the program.
A codet representing the removal of a local variable going out of scope.
symbol_exprt & symbol()
A codet representing the declaration of a local variable.
codet representation of a function call statement.
exprt::operandst argumentst
codet representation of a goto statement.
Definition: std_code.h:841
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:37
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
typet & type()
Return the type of the expression.
Definition: expr.h:82
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
unsigned target_number
A number to identify branch targets.
Definition: goto_program.h:547
const exprt & condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:382
void transform(std::function< optionalt< exprt >(exprt)>)
Apply given transformer to all expressions; no return value means no change needed.
void turn_into_skip()
Transforms an existing instruction into a skip, retaining the source_location.
Definition: goto_program.h:448
symbol_exprt & dead_symbol()
Get the symbol for DEAD.
Definition: goto_program.h:250
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
Definition: goto_program.h:285
void complete_goto(targett _target)
Definition: goto_program.h:463
bool is_target() const
Is this node a branch target?
Definition: goto_program.h:434
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:183
void set_target(targett t)
Sets the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:415
std::list< targett > targetst
Definition: goto_program.h:399
bool is_set_return_value() const
Definition: goto_program.h:473
const codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:313
std::set< targett > incoming_edges
Definition: goto_program.h:431
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
Definition: goto_program.h:271
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:220
targetst targets
The list of successor instructions.
Definition: goto_program.h:403
exprt & condition_nonconst()
Get the condition of gotos, assume, assert.
Definition: goto_program.h:389
unsigned loop_number
Number unique per function to identify loops.
Definition: goto_program.h:543
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
Definition: goto_program.h:257
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:367
void turn_into_assume()
Transforms either an assertion or a GOTO instruction into an assumption, with the same condition.
Definition: goto_program.h:455
exprt & return_value()
Get the return value of a SET_RETURN_VALUE instruction.
Definition: goto_program.h:264
const codet & get_code() const
Get the code represented by this instruction.
Definition: goto_program.h:187
goto_program_instruction_typet _type
Definition: goto_program.h:351
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:235
source_locationt & source_location_nonconst()
Definition: goto_program.h:337
exprt & call_function()
Get the function that is called for FUNCTION_CALL.
Definition: goto_program.h:278
std::string to_string() const
Definition: goto_program.h:562
unsigned location_number
A globally unique number to identify a program location.
Definition: goto_program.h:540
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
Definition: goto_program.h:550
source_locationt _source_location
The location of the instruction in the source file.
Definition: goto_program.h:329
std::list< instructiont >::const_iterator const_targett
Definition: goto_program.h:398
static const unsigned nil_target
Uniquely identify an invalid target or location.
Definition: goto_program.h:534
std::list< const_targett > const_targetst
Definition: goto_program.h:400
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:507
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
Definition: goto_program.h:213
void clear(goto_program_instruction_typet __type)
Clear the node.
Definition: goto_program.h:438
codet & code_nonconst()
Set the code represented by this instruction.
Definition: goto_program.h:193
const source_locationt & source_location() const
Definition: goto_program.h:332
std::list< instructiont >::iterator targett
The target for gotos and for start_thread nodes.
Definition: goto_program.h:397
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
Definition: goto_program.h:375
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Definition: goto_program.h:243
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:407
exprt::operandst & call_arguments()
Get the arguments of a FUNCTION_CALL.
Definition: goto_program.h:306
exprt guard
Guard for gotos, assume, assert Use condition() method to access.
Definition: goto_program.h:357
exprt & call_lhs()
Get the lhs of a FUNCTION_CALL (may be nil)
Definition: goto_program.h:292
instructiont(goto_program_instruction_typet __type)
Definition: goto_program.h:498
void swap(instructiont &instruction)
Swap two instructions.
Definition: goto_program.h:522
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
Definition: goto_program.h:227
std::list< irep_idt > labelst
Goto target labels.
Definition: goto_program.h:427
void set_other(codet &c)
Set the statement for OTHER.
Definition: goto_program.h:320
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:199
goto_program_instruction_typet type() const
What kind of instruction?
Definition: goto_program.h:343
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:299
exprt & assign_lhs_nonconst()
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:206
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:934
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
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:863
void clear()
Clear the goto program.
Definition: goto_program.h:809
void insert_before_swap(targett target, instructiont &instruction)
Insertion that preserves jumps to "target".
Definition: goto_program.h:644
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:692
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:956
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:602
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:619
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:706
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
Definition: goto_program.h:781
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:676
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:986
instructionst::iterator targett
Definition: goto_program.h:592
goto_programt & operator=(goto_programt &&other)
Definition: goto_program.h:90
instructionst::const_iterator const_targett
Definition: goto_program.h:593
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:855
targett add_instruction(goto_program_instruction_typet type)
Adds an instruction of given type at the end.
Definition: goto_program.h:730
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:723
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:698
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:652
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:975
goto_programt()
Constructor.
Definition: goto_program.h:794
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:816
std::list< instructiont > instructionst
Definition: goto_program.h:590
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:842
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
std::list< const_targett > const_targetst
Definition: goto_program.h:595
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:880
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:684
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:901
const_targett const_cast_target(const_targett t) const
Dummy for templates with possible const contexts.
Definition: goto_program.h:608
void compute_location_numbers(unsigned &nr)
Compute location numbers.
Definition: goto_program.h:755
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
const_targett get_end_function() const
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
Definition: goto_program.h:827
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
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:912
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:964
goto_programt(goto_programt &&other)
Definition: goto_program.h:85
void compute_location_numbers()
Compute location numbers.
Definition: goto_program.h:767
void swap(goto_programt &program)
Swap the goto program.
Definition: goto_program.h:803
goto_programt & operator=(const goto_programt &)=delete
static instructiont make_location(const source_locationt &l)
Definition: goto_program.h:890
void compute_target_numbers()
Compute the target numbers.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:715
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
bool empty() const
Is the program empty?
Definition: goto_program.h:788
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:949
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:922
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:668
static instructiont make_assignment(exprt lhs, exprt rhs, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:942
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:996
void compute_loop_numbers()
Compute loop numbers.
std::list< targett > targetst
Definition: goto_program.h:594
const irep_idt & id() const
Definition: irep.h:396
void make_nil()
Definition: irep.h:454
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The NIL expression.
Definition: std_expr.h:2874
static const source_locationt & nil()
Expression to hold a symbol (variable)
Definition: std_expr.h:80
The Boolean constant true.
Definition: std_expr.h:2856
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
#define DEPRECATED(msg)
Definition: deprecate.h:23
const code_returnt & to_code_return(const codet &code)
const code_deadt & to_code_dead(const codet &code)
const code_function_callt & to_code_function_call(const codet &code)
const code_assignt & to_code_assign(const codet &code)
bool order_const_target(const goto_programt::const_targett i1, const goto_programt::const_targett i2)
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)
bool operator<(const goto_programt::const_targett &i1, const goto_programt::const_targett &i2)
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:20
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
nonstd::optional< T > optionalt
Definition: optional.h:35
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#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
Functor to check whether iterators from different collections point at the same object.
bool operator()(const A &a, const B &b) const
validation_modet