12 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_TEMPLATE_H 13 #define CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_TEMPLATE_H 68 template <
class codeT,
class guardT>
178 typedef typename std::list<instructiont>::iterator
targett;
300 #if (defined _MSC_VER && _MSC_VER <= 1800) 304 static_cast<unsigned>(-1);
308 std::numeric_limits<unsigned>::max();
338 std::ostringstream instruction_id_builder;
339 instruction_id_builder <<
type;
340 return instruction_id_builder.str();
346 typedef typename instructionst::iterator
targett;
370 while(!l->is_end_function())
384 template <
typename Target>
393 const auto next=std::next(target);
394 instructions.insert(next, instructiont())->swap(*target);
402 target->swap(instruction);
415 auto next=std::next(target);
431 return instructions.insert(std::next(target), instructiont());
472 std::ostream &out)
const;
475 std::ostream &
output(std::ostream &out)
const 485 typename instructionst::const_iterator it)
const=0;
494 i.location_number=nr++;
514 std::to_string(target->loop_number);
548 assert(end_function->is_end_function());
559 template <
class codeT,
class guardT>
563 for(
auto &i : instructions)
564 if(i.is_backwards_goto())
568 template <
class codeT,
class guardT>
569 template <
typename Target>
573 if(target==instructions.end())
574 return std::list<Target>();
576 const auto next=std::next(target);
578 const instructiont &i=*target;
582 std::list<Target> successors(i.targets.begin(), i.targets.end());
584 if(!i.guard.is_true() && next!=instructions.end())
585 successors.push_back(next);
590 if(i.is_start_thread())
592 std::list<Target> successors(i.targets.begin(), i.targets.end());
594 if(next!=instructions.end())
595 successors.push_back(next);
600 if(i.is_end_thread())
603 return std::list<Target>();
609 return std::list<Target>();
615 !i.guard.is_false() && next!=instructions.end() ?
616 std::list<Target>{next} :
620 if(next!=instructions.end())
622 return std::list<Target>{next};
625 return std::list<Target>();
631 template <
class codeT,
class guardT>
634 compute_incoming_edges();
635 compute_target_numbers();
636 compute_location_numbers();
639 template <
class codeT,
class guardT>
643 std::ostream &out)
const 647 for(
typename instructionst::const_iterator
648 it=instructions.begin();
649 it!=instructions.end();
651 output_instruction(ns, identifier, out, it);
656 template <
class codeT,
class guardT>
661 for(
auto &i : instructions)
662 i.target_number=instructiont::nil_target;
666 for(
const auto &i : instructions)
668 for(
const auto &t : i.targets)
670 if(t!=instructions.end())
678 for(
auto &i : instructions)
682 i.target_number=++cnt;
683 assert(i.target_number!=0);
690 for(
const auto &i : instructions)
692 for(
const auto &t : i.targets)
694 if(t!=instructions.end())
696 assert(t->target_number!=0);
697 assert(t->target_number!=instructiont::nil_target);
703 template <
class codeT,
class guardT>
708 typedef std::map<const_targett, targett> targets_mappingt;
709 targets_mappingt targets_mapping;
715 for(
typename instructionst::const_iterator
720 auto new_instruction=add_instruction();
721 targets_mapping[it]=new_instruction;
722 *new_instruction=*it;
727 for(
auto &i : instructions)
729 for(
auto &t : i.targets)
731 typename targets_mappingt::iterator
732 m_target_it=targets_mapping.find(t);
734 if(m_target_it==targets_mapping.end())
735 throw "copy_from: target not found";
737 t=m_target_it->second;
741 compute_incoming_edges();
742 compute_target_numbers();
746 template <
class codeT,
class guardT>
749 for(
const auto &i : instructions)
750 if(i.is_assert() && !i.guard.is_true())
756 template <
class codeT,
class guardT>
759 for(
auto &i : instructions)
761 i.incoming_edges.clear();
764 for(
typename instructionst::iterator
765 it=instructions.begin();
766 it!=instructions.end();
769 for(
const auto &s : get_successors(it))
771 if(s!=instructions.end())
772 s->incoming_edges.insert(it);
777 template <
class codeT,
class guardT>
787 template <
class codeT,
class guardT>
792 {
return t->location_number; }
795 #endif // CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_TEMPLATE_H const irept & get_nil_irep()
void make_assumption(const guardT &g)
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)
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.
bool is_function_call() const
std::list< targett > targetst
instructionst instructions
The list of instructions in the goto program.
goto_program_templatet()
Constructor.
goto_program_instruction_typet type
What kind of instruction?
bool is_start_thread() const
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.
void make_goto(targett _target)
std::list< Target > get_successors(Target target) const
void compute_incoming_edges()
std::list< instructiont >::const_iterator const_targett
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
void make_function_call(const codeT &_code)
instructionst::const_iterator const_targett
The boolean constant true.
void insert_before_swap(targett target, goto_program_templatet< codeT, guardT > &p)
Insertion that preserves jumps to "target".
bool is_end_function() const
void compute_target_numbers()
Compute the target numbers.
API to expression classes.
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
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)
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
bool is_atomic_end() const
targett insert_before(const_targett target)
Insertion before the given target.
unsigned location_number
A globally unique number to identify a program location.
bool is_end_thread() const
void copy_from(const goto_program_templatet< codeT, guardT > &src)
Copy a full goto program, preserving targets.
std::set< targett > incoming_edges
void make_assertion(const guardT &g)
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.
std::string to_string() const
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 make_other(const codeT &_code)
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 is_atomic_begin() const
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.
virtual ~goto_program_templatet()
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
targett get_end_function()