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/invariant.h>
22 #include <util/namespace.h>
23 #include <util/symbol_table.h>
24 #include <util/source_location.h>
25 #include <util/std_expr.h>
26 #include <util/std_code.h>
27 
30 {
32  GOTO = 1, // branch, possibly guarded
33  ASSUME = 2, // non-failing guarded self loop
34  ASSERT = 3, // assertions
35  OTHER = 4, // anything else
36  SKIP = 5, // just advance the PC
37  START_THREAD = 6, // spawns an asynchronous thread
38  END_THREAD = 7, // end the current thread
39  LOCATION = 8, // semantically like SKIP
40  END_FUNCTION = 9, // exit point of a function
41  ATOMIC_BEGIN = 10, // marks a block without interleavings
42  ATOMIC_END = 11, // end of a block without interleavings
43  RETURN = 12, // set function return value (no control-flow change)
44  ASSIGN = 13, // assignment lhs:=rhs
45  DECL = 14, // declare a local variable
46  DEAD = 15, // marks the end-of-live of a local variable
47  FUNCTION_CALL = 16, // call a function
48  THROW = 17, // throw an exception
49  CATCH = 18, // push, pop or enter an exception handler
50  INCOMPLETE_GOTO = 19 // goto where target is yet to be determined
51 };
52 
53 std::ostream &operator<<(std::ostream &, goto_program_instruction_typet);
54 
71 {
72 public:
74  goto_programt(const goto_programt &)=delete;
75  goto_programt &operator=(const goto_programt &)=delete;
76 
77  // Move operations need to be explicitly enabled as they are deleted with the
78  // copy operations
79  // default for move operations isn't available on Windows yet, so define
80  // explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx
81  // under "Defaulted and Deleted Functions")
82 
84  instructions(std::move(other.instructions))
85  {
86  }
87 
89  {
90  instructions=std::move(other.instructions);
91  return *this;
92  }
93 
173  class instructiont final
174  {
175  public:
177 
179  irep_idt function;
180 
183 
186 
189 
190  // The below will eventually become a single target only.
192  typedef std::list<instructiont>::iterator targett;
193  typedef std::list<instructiont>::const_iterator const_targett;
194  typedef std::list<targett> targetst;
195  typedef std::list<const_targett> const_targetst;
196 
199 
203  {
204  PRECONDITION(targets.size()==1);
205  return targets.front();
206  }
207 
211  {
212  targets.clear();
213  targets.push_back(t);
214  }
215 
216  bool has_target() const
217  {
218  return !targets.empty();
219  }
220 
222  typedef std::list<irep_idt> labelst;
224 
225  // will go away
226  std::set<targett> incoming_edges;
227 
229  bool is_target() const
230  { return target_number!=nil_target; }
231 
234  {
235  type=_type;
236  targets.clear();
237  guard=true_exprt();
238  code.make_nil();
239  }
240 
241  void make_return() { clear(RETURN); }
242  void make_skip() { clear(SKIP); }
245  void make_throw() { clear(THROW); }
246  void make_catch() { clear(CATCH); }
247  void make_assertion(const exprt &g) { clear(ASSERT); guard=g; }
248  void make_assumption(const exprt &g) { clear(ASSUME); guard=g; }
250  void make_other(const codet &_code) { clear(OTHER); code=_code; }
251  void make_decl() { clear(DECL); }
252  void make_dead() { clear(DEAD); }
256 
257  void make_incomplete_goto(const code_gotot &_code)
258  {
260  code = _code;
261  }
262 
263  void make_goto(targett _target)
264  {
265  clear(GOTO);
266  targets.push_back(_target);
267  }
268 
269  void make_goto(targett _target, const exprt &g)
270  {
271  make_goto(_target);
272  guard=g;
273  }
274 
275  void complete_goto(targett _target)
276  {
278  targets.push_back(_target);
279  type = GOTO;
280  }
281 
282  void make_assignment(const codet &_code)
283  {
284  clear(ASSIGN);
285  code=_code;
286  }
287 
288  void make_decl(const codet &_code)
289  {
290  clear(DECL);
291  code=_code;
292  }
293 
294  void make_function_call(const codet &_code)
295  {
297  code=_code;
298  }
299 
300  bool is_goto () const { return type==GOTO; }
301  bool is_return () const { return type==RETURN; }
302  bool is_assign () const { return type==ASSIGN; }
303  bool is_function_call() const { return type==FUNCTION_CALL; }
304  bool is_throw () const { return type==THROW; }
305  bool is_catch () const { return type==CATCH; }
306  bool is_skip () const { return type==SKIP; }
307  bool is_location () const { return type==LOCATION; }
308  bool is_other () const { return type==OTHER; }
309  bool is_decl () const { return type==DECL; }
310  bool is_dead () const { return type==DEAD; }
311  bool is_assume () const { return type==ASSUME; }
312  bool is_assert () const { return type==ASSERT; }
313  bool is_atomic_begin () const { return type==ATOMIC_BEGIN; }
314  bool is_atomic_end () const { return type==ATOMIC_END; }
315  bool is_start_thread () const { return type==START_THREAD; }
316  bool is_end_thread () const { return type==END_THREAD; }
317  bool is_end_function () const { return type==END_FUNCTION; }
318  bool is_incomplete_goto() const
319  {
320  return type == INCOMPLETE_GOTO;
321  }
322 
324  instructiont(NO_INSTRUCTION_TYPE) // NOLINT(runtime/explicit)
325  {
326  }
327 
329  source_location(static_cast<const source_locationt &>(get_nil_irep())),
330  type(_type),
331  guard(true_exprt()),
332  location_number(0),
333  loop_number(0),
335  {
336  }
337 
339  void swap(instructiont &instruction)
340  {
341  using std::swap;
342  swap(instruction.code, code);
343  swap(instruction.source_location, source_location);
344  swap(instruction.type, type);
345  swap(instruction.guard, guard);
346  swap(instruction.targets, targets);
347  swap(instruction.function, function);
348  }
349 
350  #if (defined _MSC_VER && _MSC_VER <= 1800)
351  // Visual Studio <= 2013 does not support constexpr, making
352  // numeric_limits::max() unviable for a static const member
353  static const unsigned nil_target=
354  static_cast<unsigned>(-1);
355  #else
356  static const unsigned nil_target=
358  std::numeric_limits<unsigned>::max();
359  #endif
360 
364  unsigned location_number;
365 
367  unsigned loop_number;
368 
371  unsigned target_number;
372 
374  bool is_backwards_goto() const
375  {
376  if(!is_goto())
377  return false;
378 
379  for(const auto &t : targets)
380  if(t->location_number<=location_number)
381  return true;
382 
383  return false;
384  }
385 
386  std::string to_string() const
387  {
388  std::ostringstream instruction_id_builder;
389  instruction_id_builder << type;
390  return instruction_id_builder.str();
391  }
392  };
393 
394  // Never try to change this to vector-we mutate the list while iterating
395  typedef std::list<instructiont> instructionst;
396 
397  typedef instructionst::iterator targett;
398  typedef instructionst::const_iterator const_targett;
399  typedef std::list<targett> targetst;
400  typedef std::list<const_targett> const_targetst;
401 
404 
408  {
409  return instructions.erase(t, t);
410  }
411 
414  {
415  return t;
416  }
417 
418  static const irep_idt get_function_id(
419  const_targett l)
420  {
421  while(!l->is_end_function())
422  ++l;
423 
424  return l->function;
425  }
426 
427  static const irep_idt get_function_id(
428  const goto_programt &p)
429  {
430  PRECONDITION(!p.empty());
431 
432  return get_function_id(--p.instructions.end());
433  }
434 
435  template <typename Target>
436  std::list<Target> get_successors(Target target) const;
437 
438  void compute_incoming_edges();
439 
442  {
443  PRECONDITION(target!=instructions.end());
444  const auto next=std::next(target);
445  instructions.insert(next, instructiont())->swap(*target);
446  }
447 
450  void insert_before_swap(targett target, instructiont &instruction)
451  {
452  insert_before_swap(target);
453  target->swap(instruction);
454  }
455 
459  targett target,
460  goto_programt &p)
461  {
462  PRECONDITION(target!=instructions.end());
463  if(p.instructions.empty())
464  return;
465  insert_before_swap(target, p.instructions.front());
466  auto next=std::next(target);
467  p.instructions.erase(p.instructions.begin());
468  instructions.splice(next, p.instructions);
469  }
470 
474  {
475  return instructions.insert(target, instructiont());
476  }
477 
481  {
482  return instructions.insert(std::next(target), instructiont());
483  }
484 
487  {
488  instructions.splice(instructions.end(),
489  p.instructions);
490  // BUG: The iterators to p-instructions are invalidated!
491  }
492 
496  const_targett target,
497  goto_programt &p)
498  {
499  instructions.splice(target, p.instructions);
500  // BUG: The iterators to p-instructions are invalidated!
501  }
502 
506  {
507  instructions.push_back(instructiont());
508  return --instructions.end();
509  }
510 
514  {
515  instructions.push_back(instructiont(type));
516  return --instructions.end();
517  }
518 
520  std::ostream &output(
521  const namespacet &ns,
522  const irep_idt &identifier,
523  std::ostream &out) const;
524 
526  std::ostream &output(std::ostream &out) const
527  {
528  return output(namespacet(symbol_tablet()), "", out);
529  }
530 
532  std::ostream &output_instruction(
533  const namespacet &ns,
534  const irep_idt &identifier,
535  std::ostream &out,
536  const instructionst::value_type &it) const;
537 
539  void compute_target_numbers();
540 
542  void compute_location_numbers(unsigned &nr)
543  {
544  for(auto &i : instructions)
545  {
546  INVARIANT(
547  nr != std::numeric_limits<unsigned>::max(),
548  "Too many location numbers assigned");
549  i.location_number=nr++;
550  }
551  }
552 
558  void update_instructions_function(const irep_idt &function_id)
559  {
560  for(auto &instruction : instructions)
561  {
562  if(instruction.function.empty())
563  {
564  instruction.function = function_id;
565  }
566  }
567  }
568 
571  {
572  unsigned nr=0;
574  }
575 
577  void compute_loop_numbers();
578 
580  void update();
581 
583  static irep_idt loop_id(const instructiont &instruction)
584  {
585  return id2string(instruction.function)+"."+
586  std::to_string(instruction.loop_number);
587  }
588 
590  bool empty() const
591  {
592  return instructions.empty();
593  }
594 
597  {
598  }
599 
601  {
602  }
603 
605  void swap(goto_programt &program)
606  {
607  program.instructions.swap(instructions);
608  }
609 
611  void clear()
612  {
613  instructions.clear();
614  }
615 
617  {
618  PRECONDITION(!instructions.empty());
619  const auto end_function=std::prev(instructions.end());
620  DATA_INVARIANT(end_function->is_end_function(),
621  "goto program ends on END_FUNCTION");
622  return end_function;
623  }
624 
626  {
627  PRECONDITION(!instructions.empty());
628  const auto end_function=std::prev(instructions.end());
629  DATA_INVARIANT(end_function->is_end_function(),
630  "goto program ends on END_FUNCTION");
631  return end_function;
632  }
633 
635  void copy_from(const goto_programt &src);
636 
638  bool has_assertion() const;
639 
640  typedef std::set<irep_idt> decl_identifierst;
642  void get_decl_identifiers(decl_identifierst &decl_identifiers) const;
643 };
644 
645 template <typename Target>
647  Target target) const
648 {
649  if(target==instructions.end())
650  return std::list<Target>();
651 
652  const auto next=std::next(target);
653 
654  const instructiont &i=*target;
655 
656  if(i.is_goto())
657  {
658  std::list<Target> successors(i.targets.begin(), i.targets.end());
659 
660  if(!i.guard.is_true() && next!=instructions.end())
661  successors.push_back(next);
662 
663  return successors;
664  }
665 
666  if(i.is_start_thread())
667  {
668  std::list<Target> successors(i.targets.begin(), i.targets.end());
669 
670  if(next!=instructions.end())
671  successors.push_back(next);
672 
673  return successors;
674  }
675 
676  if(i.is_end_thread())
677  {
678  // no successors
679  return std::list<Target>();
680  }
681 
682  if(i.is_throw())
683  {
684  // the successors are non-obvious
685  return std::list<Target>();
686  }
687 
688  if(i.is_assume())
689  {
690  return
691  !i.guard.is_false() && next!=instructions.end() ?
692  std::list<Target>{next} :
693  std::list<Target>();
694  }
695 
696  if(next!=instructions.end())
697  {
698  return std::list<Target>{next};
699  }
700 
701  return std::list<Target>();
702 }
703 
704 inline bool order_const_target(
707 {
708  const goto_programt::instructiont &_i1=*i1;
709  const goto_programt::instructiont &_i2=*i2;
710  return &_i1<&_i2;
711 }
712 
713 // NOLINTNEXTLINE(readability/identifiers)
715 {
716  std::size_t operator()(
717  const goto_programt::const_targett t) const
718  {
719  using hash_typet = decltype(&(*t));
720  return std::hash<hash_typet>{}(&(*t));
721  }
722 };
723 
727 {
728  template <class A, class B>
729  bool operator()(const A &a, const B &b) const
730  {
731  return &(*a) == &(*b);
732  }
733 };
734 
735 #define forall_goto_program_instructions(it, program) \
736  for(goto_programt::instructionst::const_iterator \
737  it=(program).instructions.begin(); \
738  it!=(program).instructions.end(); it++)
739 
740 #define Forall_goto_program_instructions(it, program) \
741  for(goto_programt::instructionst::iterator \
742  it=(program).instructions.begin(); \
743  it!=(program).instructions.end(); it++)
744 
745 inline bool operator<(
748 {
749  return order_const_target(i1, i2);
750 }
751 
752 inline bool operator<(
753  const goto_programt::targett &i1,
754  const goto_programt::targett &i2)
755 {
756  return &(*i1)<&(*i2);
757 }
758 
759 std::list<exprt> objects_read(const goto_programt::instructiont &);
760 std::list<exprt> objects_written(const goto_programt::instructiont &);
761 
762 std::list<exprt> expressions_read(const goto_programt::instructiont &);
763 std::list<exprt> expressions_written(const goto_programt::instructiont &);
764 
765 std::string as_string(
766  const namespacet &ns,
768 
769 #endif // CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
const irept & get_nil_irep()
Definition: irep.cpp:56
goto_programt(goto_programt &&other)
Definition: goto_program.h:83
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:188
irep_idt function
The function this instruction belongs to.
Definition: goto_program.h:179
void update()
Update all indices.
targett add_instruction(goto_program_instruction_typet type)
Adds an instruction of given type at the end.
Definition: goto_program.h:513
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:441
std::list< targett > targetst
Definition: goto_program.h:399
targett insert_before(const_targett target)
Insertion before the given target.
Definition: goto_program.h:473
void compute_loop_numbers()
Compute loop numbers.
std::set< targett > incoming_edges
Definition: goto_program.h:226
std::string to_string() const
Definition: goto_program.h:386
void make_assumption(const exprt &g)
Definition: goto_program.h:248
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
unsigned location_number
A globally unique number to identify a program location.
Definition: goto_program.h:364
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:185
void compute_location_numbers(unsigned &nr)
Compute location numbers.
Definition: goto_program.h:542
std::size_t operator()(const goto_programt::const_targett t) const
Definition: goto_program.h:716
bool is_false() const
Definition: expr.cpp:131
bool has_assertion() const
Does the goto program have an assertion?
std::list< exprt > objects_written(const goto_programt::instructiont &)
void destructive_append(goto_programt &p)
Appends the given program, which is destroyed.
Definition: goto_program.h:486
const_targett const_cast_target(const_targett t) const
Dummy for templates with possible const contexts.
Definition: goto_program.h:413
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:407
bool operator<(const goto_programt::const_targett &i1, const goto_programt::const_targett &i2)
Definition: goto_program.h:745
bool is_true() const
Definition: expr.cpp:124
A ‘goto’ instruction.
Definition: std_code.h:803
STL namespace.
static const unsigned nil_target
Uniquely identify an invalid target or location.
Definition: goto_program.h:357
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
void make_assignment(const codet &_code)
Definition: goto_program.h:282
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:202
bool operator()(const A &a, const B &b) const
Definition: goto_program.h:729
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
Definition: goto_program.h:374
void make_function_call(const codet &_code)
Definition: goto_program.h:294
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
targetst targets
The list of successor instructions.
Definition: goto_program.h:198
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
void clear()
Clear the goto program.
Definition: goto_program.h:611
static const irep_idt get_function_id(const goto_programt &p)
Definition: goto_program.h:427
std::list< instructiont > instructionst
Definition: goto_program.h:395
std::list< exprt > expressions_read(const goto_programt::instructiont &)
unsigned target_number
A number to identify branch targets.
Definition: goto_program.h:371
std::list< instructiont >::const_iterator const_targett
Definition: goto_program.h:193
std::list< const_targett > const_targetst
Definition: goto_program.h:400
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:640
const_targett get_end_function() const
Definition: goto_program.h:625
unsigned loop_number
Number unique per function to identify loops.
Definition: goto_program.h:367
std::list< exprt > expressions_written(const goto_programt::instructiont &)
The boolean constant true.
Definition: std_expr.h:4486
void compute_incoming_edges()
instructionst::iterator targett
Definition: goto_program.h:397
void complete_goto(targett _target)
Definition: goto_program.h:275
void make_location(const source_locationt &l)
Definition: goto_program.h:243
std::string as_string(const namespacet &ns, const goto_programt::instructiont &)
void make_other(const codet &_code)
Definition: goto_program.h:250
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
API to expression classes.
The symbol table.
Definition: symbol_table.h:19
instructionst::const_iterator const_targett
Definition: goto_program.h:398
std::list< Target > get_successors(Target target) const
Definition: goto_program.h:646
TO_BE_DOCUMENTED.
Definition: namespace.h:74
goto_programt & operator=(goto_programt &&other)
Definition: goto_program.h:88
std::list< exprt > objects_read(const goto_programt::instructiont &)
static irep_idt loop_id(const instructiont &instruction)
Human-readable loop name.
Definition: goto_program.h:583
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:29
targett insert_after(const_targett target)
Insertion after the given target.
Definition: goto_program.h:480
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program at the given location.
Definition: goto_program.h:495
void insert_before_swap(targett target, goto_programt &p)
Insertion that preserves jumps to "target".
Definition: goto_program.h:458
Functor to check whether iterators from different collections point at the same object.
Definition: goto_program.h:726
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Author: Diffblue Ltd.
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
void compute_location_numbers()
Compute location numbers.
Definition: goto_program.h:570
bool order_const_target(const goto_programt::const_targett i1, const goto_programt::const_targett i2)
Definition: goto_program.h:704
void swap(goto_programt &program)
Swap the goto program.
Definition: goto_program.h:605
void insert_before_swap(targett target, instructiont &instruction)
Insertion that preserves jumps to "target".
Definition: goto_program.h:450
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
std::ostream & operator<<(std::ostream &, goto_program_instruction_typet)
std::list< targett > targetst
Definition: goto_program.h:194
std::list< irep_idt > labelst
Goto target labels.
Definition: goto_program.h:222
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const
Output a single instruction.
void update_instructions_function(const irep_idt &function_id)
Sets the function member of each instruction if not yet set Note that a goto program need not be a go...
Definition: goto_program.h:558
void make_decl(const codet &_code)
Definition: goto_program.h:288
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:182
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
Base class for all expressions.
Definition: expr.h:42
goto_programt()
Constructor.
Definition: goto_program.h:596
targett get_end_function()
Definition: goto_program.h:616
void make_goto(targett _target, const exprt &g)
Definition: goto_program.h:269
std::string to_string(const string_constraintt &expr)
Used for debug printing.
bool empty() const
Is the program empty?
Definition: goto_program.h:590
void compute_target_numbers()
Compute the target numbers.
void swap(instructiont &instruction)
Swap two instructions.
Definition: goto_program.h:339
std::list< const_targett > const_targetst
Definition: goto_program.h:195
void clear(goto_program_instruction_typet _type)
Clear the node.
Definition: goto_program.h:233
static const irep_idt get_function_id(const_targett l)
Definition: goto_program.h:418
void make_nil()
Definition: irep.h:315
void make_incomplete_goto(const code_gotot &_code)
Definition: goto_program.h:257
std::list< instructiont >::iterator targett
The target for gotos and for start_thread nodes.
Definition: goto_program.h:192
void make_assertion(const exprt &g)
Definition: goto_program.h:247
A statement in a programming language.
Definition: std_code.h:21
void set_target(targett t)
Sets the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:210
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
goto_programt & operator=(const goto_programt &)=delete
instructiont(goto_program_instruction_typet _type)
Definition: goto_program.h:328
bool is_target() const
Is this node a branch target?
Definition: goto_program.h:229
void make_goto(targett _target)
Definition: goto_program.h:263
std::ostream & output(std::ostream &out) const
Output goto-program to given stream.
Definition: goto_program.h:526