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;
190 assert(targets.size()==1);
191 return targets.front();
199 targets.push_back(t);
239 targets.push_back(_target);
300 #if (defined _MSC_VER && _MSC_VER <= 1800) 304 static_cast<unsigned>(-1);
306 static const unsigned nil_target=
308 std::numeric_limits<unsigned>::max();
329 for(
const auto &t : targets)
330 if(t->location_number<=location_number)
338 std::ostringstream instruction_id_builder;
339 instruction_id_builder <<
type;
340 return instruction_id_builder.str();
346 typedef typename instructionst::iterator
targett;
358 return instructions.erase(t, t);
370 while(!l->is_end_function())
384 template <
typename Target>
392 assert(target!=instructions.end());
393 const auto next=std::next(target);
394 instructions.insert(next,
instructiont())->swap(*target);
402 target->swap(instruction);
411 assert(target!=instructions.end());
415 auto next=std::next(target);
431 return instructions.insert(std::next(target),
instructiont());
437 instructions.splice(instructions.end(),
445 const_targett target,
457 return --instructions.end();
465 return --instructions.end();
472 std::ostream &out)
const;
475 std::ostream &
output(std::ostream &out)
const 485 typename instructionst::const_iterator it)
const=0;
493 for(
auto &i : instructions)
494 i.location_number=nr++;
514 std::to_string(target->loop_number);
520 return instructions.empty();
541 instructions.clear();
546 assert(!instructions.empty());
547 const auto end_function=std::prev(instructions.end());
548 assert(end_function->is_end_function());
559 template <
class codeT,
class guardT>
564 if(i.is_backwards_goto())
568 template <
class codeT,
class guardT>
569 template <
typename Target>
574 return std::list<Target>();
576 const auto next=std::next(target);
582 std::list<Target> successors(i.targets.begin(), i.targets.end());
585 successors.push_back(next);
590 if(i.is_start_thread())
592 std::list<Target> successors(i.targets.begin(), i.targets.end());
595 successors.push_back(next);
600 if(i.is_end_thread())
603 return std::list<Target>();
609 return std::list<Target>();
616 std::list<Target>{next} :
622 return std::list<Target>{next};
625 return std::list<Target>();
631 template <
class codeT,
class guardT>
639 template <
class codeT,
class guardT>
643 std::ostream &out)
const 647 for(
typename instructionst::const_iterator
656 template <
class codeT,
class guardT>
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);
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
721 targets_mapping[it]=new_instruction;
722 *new_instruction=*it;
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;
746 template <
class codeT,
class guardT>
750 if(i.is_assert() && !i.guard.is_true())
756 template <
class codeT,
class guardT>
761 i.incoming_edges.clear();
764 for(
typename instructionst::iterator
765 it=instructions.begin();
766 it!=instructions.end();
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()