cprover
goto_program_template.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Program Template
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_TEMPLATE_H
13 #define CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_TEMPLATE_H
14 
15 #include <cassert>
16 #include <iosfwd>
17 #include <set>
18 #include <limits>
19 #include <sstream>
20 #include <string>
21 
22 #include <util/namespace.h>
23 #include <util/symbol_table.h>
24 #include <util/source_location.h>
25 #include <util/std_expr.h>
26 
29 {
31  GOTO=1, // branch, possibly guarded
32  ASSUME=2, // non-failing guarded self loop
33  ASSERT=3, // assertions
34  OTHER=4, // anything else
35  SKIP=5, // just advance the PC
36  START_THREAD=6, // spawns an asynchronous thread
37  END_THREAD=7, // end the current thread
38  LOCATION=8, // semantically like SKIP
39  END_FUNCTION=9, // exit point of a function
40  ATOMIC_BEGIN=10, // marks a block without interleavings
41  ATOMIC_END=11, // end of a block without interleavings
42  RETURN=12, // set function return value (no control-flow change)
43  ASSIGN=13, // assignment lhs:=rhs
44  DECL=14, // declare a local variable
45  DEAD=15, // marks the end-of-live of a local variable
46  FUNCTION_CALL=16, // call a function
47  THROW=17, // throw an exception
48  CATCH=18 // catch an exception
49 };
50 
51 std::ostream &operator<<(std::ostream &, goto_program_instruction_typet);
52 
68 template <class codeT, class guardT>
70 {
71 public:
75 
76  // Move operations need to be explicitly enabled as they are deleted with the
77  // copy operations
78  // default for move operations isn't available on Windows yet, so define
79  // explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx
80  // under "Defaulted and Deleted Functions")
81 
83  instructions(std::move(other.instructions))
84  {
85  }
86 
88  {
89  instructions=std::move(other.instructions);
90  return *this;
91  }
92 
160  {
161  public:
162  codeT code;
163 
165  irep_idt function;
166 
169 
172 
174  guardT guard;
175 
176  // The below will eventually become a single target only.
178  typedef typename std::list<instructiont>::iterator targett;
179  typedef typename std::list<instructiont>::const_iterator const_targett;
180  typedef std::list<targett> targetst;
181  typedef std::list<const_targett> const_targetst;
182 
185 
189  {
190  assert(targets.size()==1);
191  return targets.front();
192  }
193 
197  {
198  targets.clear();
199  targets.push_back(t);
200  }
201 
203  typedef std::list<irep_idt> labelst;
205 
206  // will go away
207  std::set<targett> incoming_edges;
208 
210  bool is_target() const
211  { return target_number!=nil_target; }
212 
215  {
216  type=_type;
217  targets.clear();
218  guard=true_exprt();
219  code.make_nil();
220  }
221 
222  void make_goto() { clear(GOTO); }
223  void make_return() { clear(RETURN); }
224  void make_skip() { clear(SKIP); }
225  void make_throw() { clear(THROW); }
226  void make_catch() { clear(CATCH); }
227  void make_assertion(const guardT &g) { clear(ASSERT); guard=g; }
228  void make_assumption(const guardT &g) { clear(ASSUME); guard=g; }
230  void make_other(const codeT &_code) { clear(OTHER); code=_code; }
231  void make_decl() { clear(DECL); }
232  void make_dead() { clear(DEAD); }
235 
236  void make_goto(targett _target)
237  {
238  make_goto();
239  targets.push_back(_target);
240  }
241 
242  void make_goto(targett _target, const guardT &g)
243  {
244  make_goto(_target);
245  guard=g;
246  }
247 
248  void make_function_call(const codeT &_code)
249  {
251  code=_code;
252  }
253 
254  bool is_goto () const { return type==GOTO; }
255  bool is_return () const { return type==RETURN; }
256  bool is_assign () const { return type==ASSIGN; }
257  bool is_function_call() const { return type==FUNCTION_CALL; }
258  bool is_throw () const { return type==THROW; }
259  bool is_catch () const { return type==CATCH; }
260  bool is_skip () const { return type==SKIP; }
261  bool is_location () const { return type==LOCATION; }
262  bool is_other () const { return type==OTHER; }
263  bool is_decl () const { return type==DECL; }
264  bool is_dead () const { return type==DEAD; }
265  bool is_assume () const { return type==ASSUME; }
266  bool is_assert () const { return type==ASSERT; }
267  bool is_atomic_begin () const { return type==ATOMIC_BEGIN; }
268  bool is_atomic_end () const { return type==ATOMIC_END; }
269  bool is_start_thread () const { return type==START_THREAD; }
270  bool is_end_thread () const { return type==END_THREAD; }
271  bool is_end_function () const { return type==END_FUNCTION; }
272 
274  instructiont(NO_INSTRUCTION_TYPE) // NOLINT(runtime/explicit)
275  {
276  }
277 
279  source_location(static_cast<const source_locationt &>(get_nil_irep())),
280  type(_type),
281  guard(true_exprt()),
282  location_number(0),
283  loop_number(0),
285  {
286  }
287 
289  void swap(instructiont &instruction)
290  {
291  using std::swap;
292  swap(instruction.code, code);
293  swap(instruction.source_location, source_location);
294  swap(instruction.type, type);
295  swap(instruction.guard, guard);
296  swap(instruction.targets, targets);
297  swap(instruction.function, function);
298  }
299 
300  #if (defined _MSC_VER && _MSC_VER <= 1800)
301  // Visual Studio <= 2013 does not support constexpr, making
302  // numeric_limits::max() unviable for a static const member
303  static const unsigned nil_target=
304  static_cast<unsigned>(-1);
305  #else
306  static const unsigned nil_target=
308  std::numeric_limits<unsigned>::max();
309  #endif
310 
314  unsigned location_number;
315 
317  unsigned loop_number;
318 
321  unsigned target_number;
322 
324  bool is_backwards_goto() const
325  {
326  if(!is_goto())
327  return false;
328 
329  for(const auto &t : targets)
330  if(t->location_number<=location_number)
331  return true;
332 
333  return false;
334  }
335 
336  std::string to_string() const
337  {
338  std::ostringstream instruction_id_builder;
339  instruction_id_builder << type;
340  return instruction_id_builder.str();
341  }
342  };
343 
344  typedef std::list<instructiont> instructionst;
345 
346  typedef typename instructionst::iterator targett;
347  typedef typename instructionst::const_iterator const_targett;
348  typedef typename std::list<targett> targetst;
349  typedef typename std::list<const_targett> const_targetst;
350 
353 
357  {
358  return instructions.erase(t, t);
359  }
360 
363  {
364  return t;
365  }
366 
367  static const irep_idt get_function_id(
368  const_targett l)
369  {
370  while(!l->is_end_function())
371  ++l;
372 
373  return l->function;
374  }
375 
376  static const irep_idt get_function_id(
378  {
379  assert(!p.empty());
380 
381  return get_function_id(--p.instructions.end());
382  }
383 
384  template <typename Target>
385  std::list<Target> get_successors(Target target) const;
386 
387  void compute_incoming_edges();
388 
391  {
392  assert(target!=instructions.end());
393  const auto next=std::next(target);
394  instructions.insert(next, instructiont())->swap(*target);
395  }
396 
399  void insert_before_swap(targett target, instructiont &instruction)
400  {
401  insert_before_swap(target);
402  target->swap(instruction);
403  }
404 
408  targett target,
410  {
411  assert(target!=instructions.end());
412  if(p.instructions.empty())
413  return;
414  insert_before_swap(target, p.instructions.front());
415  auto next=std::next(target);
416  p.instructions.erase(p.instructions.begin());
417  instructions.splice(next, p.instructions);
418  }
419 
423  {
424  return instructions.insert(target, instructiont());
425  }
426 
430  {
431  return instructions.insert(std::next(target), instructiont());
432  }
433 
436  {
437  instructions.splice(instructions.end(),
438  p.instructions);
439  // BUG: The iterators to p-instructions are invalidated!
440  }
441 
445  const_targett target,
447  {
448  instructions.splice(target, p.instructions);
449  // BUG: The iterators to p-instructions are invalidated!
450  }
451 
455  {
456  instructions.push_back(instructiont());
457  return --instructions.end();
458  }
459 
463  {
464  instructions.push_back(instructiont(type));
465  return --instructions.end();
466  }
467 
469  std::ostream &output(
470  const namespacet &ns,
471  const irep_idt &identifier,
472  std::ostream &out) const;
473 
475  std::ostream &output(std::ostream &out) const
476  {
477  return output(namespacet(symbol_tablet()), "", out);
478  }
479 
481  virtual std::ostream &output_instruction(
482  const namespacet &ns,
483  const irep_idt &identifier,
484  std::ostream &out,
485  typename instructionst::const_iterator it) const=0;
486 
488  void compute_target_numbers();
489 
491  void compute_location_numbers(unsigned &nr)
492  {
493  for(auto &i : instructions)
494  i.location_number=nr++;
495  }
496 
499  {
500  unsigned nr=0;
502  }
503 
505  void compute_loop_numbers();
506 
508  void update();
509 
512  {
513  return id2string(target->function)+"."+
514  std::to_string(target->loop_number);
515  }
516 
518  bool empty() const
519  {
520  return instructions.empty();
521  }
522 
525  {
526  }
527 
529  {
530  }
531 
534  {
535  program.instructions.swap(instructions);
536  }
537 
539  void clear()
540  {
541  instructions.clear();
542  }
543 
545  {
546  assert(!instructions.empty());
547  const auto end_function=std::prev(instructions.end());
548  assert(end_function->is_end_function());
549  return end_function;
550  }
551 
554 
556  bool has_assertion() const;
557 };
558 
559 template <class codeT, class guardT>
561 {
562  unsigned nr=0;
563  for(auto &i : instructions)
564  if(i.is_backwards_goto())
565  i.loop_number=nr++;
566 }
567 
568 template <class codeT, class guardT>
569 template <typename Target>
571  Target target) const
572 {
573  if(target==instructions.end())
574  return std::list<Target>();
575 
576  const auto next=std::next(target);
577 
578  const instructiont &i=*target;
579 
580  if(i.is_goto())
581  {
582  std::list<Target> successors(i.targets.begin(), i.targets.end());
583 
584  if(!i.guard.is_true() && next!=instructions.end())
585  successors.push_back(next);
586 
587  return successors;
588  }
589 
590  if(i.is_start_thread())
591  {
592  std::list<Target> successors(i.targets.begin(), i.targets.end());
593 
594  if(next!=instructions.end())
595  successors.push_back(next);
596 
597  return successors;
598  }
599 
600  if(i.is_end_thread())
601  {
602  // no successors
603  return std::list<Target>();
604  }
605 
606  if(i.is_throw())
607  {
608  // the successors are non-obvious
609  return std::list<Target>();
610  }
611 
612  if(i.is_assume())
613  {
614  return
615  !i.guard.is_false() && next!=instructions.end() ?
616  std::list<Target>{next} :
617  std::list<Target>();
618  }
619 
620  if(next!=instructions.end())
621  {
622  return std::list<Target>{next};
623  }
624 
625  return std::list<Target>();
626 }
627 
628 #include <langapi/language_util.h>
629 #include <iomanip>
630 
631 template <class codeT, class guardT>
633 {
634  compute_incoming_edges();
635  compute_target_numbers();
636  compute_location_numbers();
637 }
638 
639 template <class codeT, class guardT>
641  const namespacet &ns,
642  const irep_idt &identifier,
643  std::ostream &out) const
644 {
645  // output program
646 
647  for(typename instructionst::const_iterator
648  it=instructions.begin();
649  it!=instructions.end();
650  ++it)
651  output_instruction(ns, identifier, out, it);
652 
653  return out;
654 }
655 
656 template <class codeT, class guardT>
658 {
659  // reset marking
660 
661  for(auto &i : instructions)
662  i.target_number=instructiont::nil_target;
663 
664  // mark the goto targets
665 
666  for(const auto &i : instructions)
667  {
668  for(const auto &t : i.targets)
669  {
670  if(t!=instructions.end())
671  t->target_number=0;
672  }
673  }
674 
675  // number the targets properly
676  unsigned cnt=0;
677 
678  for(auto &i : instructions)
679  {
680  if(i.is_target())
681  {
682  i.target_number=++cnt;
683  assert(i.target_number!=0);
684  }
685  }
686 
687  // check the targets!
688  // (this is a consistency check only)
689 
690  for(const auto &i : instructions)
691  {
692  for(const auto &t : i.targets)
693  {
694  if(t!=instructions.end())
695  {
696  assert(t->target_number!=0);
697  assert(t->target_number!=instructiont::nil_target);
698  }
699  }
700  }
701 }
702 
703 template <class codeT, class guardT>
706 {
707  // Definitions for mapping between the two programs
708  typedef std::map<const_targett, targett> targets_mappingt;
709  targets_mappingt targets_mapping;
710 
711  clear();
712 
713  // Loop over program - 1st time collects targets and copy
714 
715  for(typename instructionst::const_iterator
716  it=src.instructions.begin();
717  it!=src.instructions.end();
718  ++it)
719  {
720  auto new_instruction=add_instruction();
721  targets_mapping[it]=new_instruction;
722  *new_instruction=*it;
723  }
724 
725  // Loop over program - 2nd time updates targets
726 
727  for(auto &i : instructions)
728  {
729  for(auto &t : i.targets)
730  {
731  typename targets_mappingt::iterator
732  m_target_it=targets_mapping.find(t);
733 
734  if(m_target_it==targets_mapping.end())
735  throw "copy_from: target not found";
736 
737  t=m_target_it->second;
738  }
739  }
740 
741  compute_incoming_edges();
742  compute_target_numbers();
743 }
744 
745 // number them
746 template <class codeT, class guardT>
748 {
749  for(const auto &i : instructions)
750  if(i.is_assert() && !i.guard.is_true())
751  return true;
752 
753  return false;
754 }
755 
756 template <class codeT, class guardT>
758 {
759  for(auto &i : instructions)
760  {
761  i.incoming_edges.clear();
762  }
763 
764  for(typename instructionst::iterator
765  it=instructions.begin();
766  it!=instructions.end();
767  ++it)
768  {
769  for(const auto &s : get_successors(it))
770  {
771  if(s!=instructions.end())
772  s->incoming_edges.insert(it);
773  }
774  }
775 }
776 
777 template <class codeT, class guardT>
778 inline bool order_const_target(
781 {
784  return &_i1<&_i2;
785 }
786 
787 template <class codeT, class guardT>
789 {
790  std::size_t operator()(
792  { return t->location_number; }
793 };
794 
795 #endif // CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_TEMPLATE_H
const irept & get_nil_irep()
Definition: irep.cpp:56
goto_program_instruction_typet
The type of an instruction in a GOTO program.
void compute_location_numbers()
Compute location numbers.
void swap(instructiont &instruction)
Swap two instructions.
void update()
Update all indices.
targett add_instruction()
Adds an instruction at the end.
static irep_idt loop_id(const_targett target)
Human-readable loop name.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::list< instructiont > instructionst
unsigned target_number
A number to identify branch targets.
instructiont(goto_program_instruction_typet _type)
void clear()
Clear the goto program.
instructionst instructions
The list of instructions in the goto program.
goto_program_templatet()
Constructor.
goto_program_instruction_typet type
What kind of instruction?
std::list< instructiont >::iterator targett
The target for gotos and for start_thread nodes.
This class represents an instruction in the GOTO intermediate representation.
void compute_location_numbers(unsigned &nr)
Compute location numbers.
goto_program_templatet(goto_program_templatet &&other)
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
irep_idt function
The function this instruction belongs to.
std::ostream & operator<<(std::ostream &, goto_program_instruction_typet)
static const irep_idt get_function_id(const_targett l)
bool empty() const
Is the program empty?
A generic container class for the GOTO intermediate representation of one function.
STL namespace.
std::list< Target > get_successors(Target target) const
std::list< instructiont >::const_iterator const_targett
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
instructionst::const_iterator const_targett
The boolean constant true.
Definition: std_expr.h:3742
void insert_before_swap(targett target, goto_program_templatet< codeT, guardT > &p)
Insertion that preserves jumps to "target".
void compute_target_numbers()
Compute the target numbers.
API to expression classes.
The symbol table.
Definition: symbol_table.h:52
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
targett const_cast_target(const_targett t)
Convert a const_targett to a targett - use with care and avoid whenever possible. ...
std::list< targett > targetst
void compute_loop_numbers()
Compute loop numbers.
targett add_instruction(goto_program_instruction_typet type)
Adds an instruction of given type at the end.
targett insert_after(const_targett target)
Insertion after the given target.
static const irep_idt get_function_id(const goto_program_templatet< codeT, guardT > &p)
Symbol table.
bool has_assertion() const
Does the goto program have an assertion?
unsigned loop_number
Number unique per function to identify loops.
goto_program_templatet & operator=(const goto_program_templatet &)=delete
targett insert_before(const_targett target)
Insertion before the given target.
unsigned location_number
A globally unique number to identify a program location.
void copy_from(const goto_program_templatet< codeT, guardT > &src)
Copy a full goto program, preserving targets.
std::size_t operator()(const typename goto_program_templatet< codeT, guardT >::const_targett t) const
guardT guard
Guard for gotos, assume, assert.
static const unsigned nil_target
Uniquely identify an invalid target or location.
void make_goto(targett _target, const guardT &g)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
const_targett const_cast_target(const_targett t) const
Dummy for templates with possible const contexts.
void destructive_insert(const_targett target, goto_program_templatet< codeT, guardT > &p)
Inserts the given program at the given location.
void insert_before_swap(targett target, instructiont &instruction)
Insertion that preserves jumps to "target".
void destructive_append(goto_program_templatet< codeT, guardT > &p)
Appends the given program, which is destroyed.
source_locationt source_location
The location of the instruction in the source file.
virtual std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, typename instructionst::const_iterator it) const =0
Output a single instruction.
void clear(goto_program_instruction_typet _type)
Clear the node.
void set_target(targett t)
Sets the first (and only) successor for the usual case of a single target.
targetst targets
The list of successor instructions.
std::list< const_targett > const_targetst
goto_program_templatet & operator=(goto_program_templatet &&other)
std::list< const_targett > const_targetst
bool order_const_target(const typename goto_program_templatet< codeT, guardT >::const_targett i1, const typename goto_program_templatet< codeT, guardT >::const_targett i2)
std::list< irep_idt > labelst
Goto target labels.
bool is_target() const
Is this node a branch target?
std::ostream & output(std::ostream &out) const
Output goto-program to given stream.
void swap(goto_program_templatet< codeT, guardT > &program)
Swap the goto program.
instructionst::iterator targett