12 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
13 #define CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
245 const auto &decl = expr_checked_cast<code_declt>(
code);
247 !decl.initial_value(),
248 "code_declt in goto program may not contain initialization.");
256 auto &decl = expr_checked_cast<code_declt>(
code);
258 !decl.initial_value(),
259 "code_declt in goto program may not contain initialization.");
260 return decl.symbol();
267 auto &decl = expr_checked_cast<code_declt>(
code);
269 !decl.initial_value(),
270 "code_declt in goto program may not contain initialization.");
271 return decl.symbol();
281 "Initialization must be separated from code_declt before adding to "
282 "goto_instructiont.");
352 "Use call_function(), call_lhs(), call_arguments() instead"))
408 "Use call_function(), call_lhs(), call_arguments() instead"))
457 guard = std::move(c);
462 typedef std::list<instructiont>::iterator
targett;
568 :
code(std::move(_code)),
571 guard(std::move(_guard)),
589 std::numeric_limits<unsigned>::max();
618 std::ostringstream instruction_id_builder;
619 instruction_id_builder <<
type;
620 return instruction_id_builder.str();
640 void apply(std::function<
void(
const exprt &)>)
const;
667 template <
typename Target>
676 const auto next=std::next(target);
685 target->swap(instruction);
698 auto next=std::next(target);
777 std::ostream &out)
const;
780 std::ostream &
output(std::ostream &out)
const;
787 const instructionst::value_type &instruction)
const;
798 nr != std::numeric_limits<unsigned>::max(),
799 "Too many location numbers assigned");
800 i.location_number=nr++;
859 "goto program ends on END_FUNCTION");
870 "goto program ends on END_FUNCTION");
897 ins.validate(ns, vm);
1142 template <
typename Target>
1144 Target target)
const
1147 return std::list<Target>();
1149 const auto next=std::next(target);
1155 std::list<Target> successors(i.
targets.begin(), i.
targets.end());
1158 successors.push_back(next);
1165 std::list<Target> successors(i.
targets.begin(), i.
targets.end());
1168 successors.push_back(next);
1176 return std::list<Target>();
1182 return std::list<Target>();
1188 ? std::list<Target>{next}
1189 : std::list<Target>();
1194 return std::list<Target>{next};
1197 return std::list<Target>();
1215 using hash_typet = decltype(&(*t));
1216 return std::hash<hash_typet>{}(&(*t));
1224 template <
class A,
class B>
1227 return &(*a) == &(*b);
1231 template <
typename GotoFunctionT,
typename PredicateT,
typename HandlerT>
1233 GotoFunctionT &&goto_function,
1234 PredicateT predicate,
1237 auto &&instructions = goto_function.body.instructions;
1238 for(
auto it = instructions.begin(); it != instructions.end(); ++it)
1247 template <
typename GotoFunctionT,
typename HandlerT>
1250 using iterator_t = decltype(goto_function.body.instructions.begin());
1252 goto_function, [](
const iterator_t &) {
return true; }, handler);
1255 #define forall_goto_program_instructions(it, program) \
1256 for(goto_programt::instructionst::const_iterator \
1257 it=(program).instructions.begin(); \
1258 it!=(program).instructions.end(); it++)
1260 #define Forall_goto_program_instructions(it, program) \
1261 for(goto_programt::instructionst::iterator \
1262 it=(program).instructions.begin(); \
1263 it!=(program).instructions.end(); it++)
1276 return &(*i1)<&(*i2);
A codet representing an assignment in the program.
A codet representing the removal of a local variable going out of scope.
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.
codet representation of a "return from a function" statement.
const exprt & return_value() const
Data structure for representing an arbitrary statement in a program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
bool is_true() const
Return whether the expression is a constant representing true.
bool is_false() const
Return whether the expression is a constant representing false.
typet & type()
Return the type of the expression.
This class represents an instruction in the GOTO intermediate representation.
bool is_end_function() const
unsigned target_number
A number to identify branch targets.
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.
void clear(goto_program_instruction_typet _type)
Clear the node.
symbol_exprt & dead_symbol()
Get the symbol for DEAD.
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
void set_function_call(code_function_callt c)
Set the function call for FUNCTION_CALL.
void complete_goto(targett _target)
bool is_target() const
Is this node a branch target?
codet code
Do not read or modify directly – use get_X() instead.
void set_target(targett t)
Sets the first (and only) successor for the usual case of a single target.
std::list< targett > targetst
bool is_set_return_value() const
const codet & get_other() const
Get the statement for OTHER.
const code_deadt & get_dead() const
Get the dead statement for DEAD.
instructiont(goto_program_instruction_typet _type)
std::set< targett > incoming_edges
source_locationt source_location
The location of the instruction in the source file.
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
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.
bool has_condition() const
Does this instruction have a condition?
goto_program_instruction_typet type
What kind of instruction?
bool is_end_thread() const
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.
targetst targets
The list of successor instructions.
unsigned loop_number
Number unique per function to identify loops.
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
const code_function_callt & get_function_call() const
Get the function call for FUNCTION_CALL.
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
exprt & return_value()
Get the return value of a SET_RETURN_VALUE instruction.
const codet & get_code() const
Get the code represented by this instruction.
void set_return(code_returnt c)
Set the return statement for SET_RETURN_VALUE.
bool equals(const instructiont &other) const
Syntactic equality: two instructiont are equal if they have the same type, code, guard,...
bool is_start_thread() const
symbol_exprt & decl_symbol()
Get the declared symbol for DECL.
bool is_atomic_end() const
exprt & call_function()
Get the function that is called for FUNCTION_CALL.
std::string to_string() const
unsigned location_number
A globally unique number to identify a program location.
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
void set_dead(code_deadt c)
Set the dead statement for DEAD.
void set_assign(code_assignt c)
Set the assignment for ASSIGN.
std::list< instructiont >::const_iterator const_targett
static const unsigned nil_target
Uniquely identify an invalid target or location.
bool is_atomic_begin() const
std::list< const_targett > const_targetst
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
codet & code_nonconst()
Set the code represented by this instruction.
std::list< instructiont >::iterator targett
The target for gotos and for start_thread nodes.
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
exprt::operandst & call_arguments()
Get the arguments of a FUNCTION_CALL.
exprt guard
Guard for gotos, assume, assert Use get_condition() to read, and set_condition(c) to write.
bool is_function_call() const
exprt & call_lhs()
Get the lhs of a FUNCTION_CALL (may be nil)
void set_decl(code_declt c)
Set the declaration for DECL.
const code_returnt & get_return() const
Get the return statement for READ.
const code_declt & get_decl() const
Get the declaration for DECL.
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
void swap(instructiont &instruction)
Swap two instructions.
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
std::list< irep_idt > labelst
Goto target labels.
void set_other(codet &c)
Set the statement for OTHER.
bool is_incomplete_goto() const
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
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.
exprt & assign_lhs_nonconst()
Get the lhs of the assignment for ASSIGN.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst instructions
The list of instructions in the goto program.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
void clear()
Clear the goto program.
void insert_before_swap(targett target, instructiont &instruction)
Insertion that preserves jumps to "target".
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.
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
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.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
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.
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
targett insert_before(const_targett target, const instructiont &i)
Insertion before the instruction pointed-to by the given instruction iterator target.
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
instructionst::iterator targett
goto_programt & operator=(goto_programt &&other)
instructionst::const_iterator const_targett
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto program is well-formed.
targett add_instruction(goto_program_instruction_typet type)
Adds an instruction of given type at the end.
targett add_instruction()
Adds an instruction at the end.
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
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".
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
static instructiont make_return(code_returnt c, const source_locationt &l=source_locationt::nil())
goto_programt()
Constructor.
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.
std::list< instructiont > instructionst
std::set< irep_idt > decl_identifierst
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
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
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())
const_targett const_cast_target(const_targett t) const
Dummy for templates with possible const contexts.
void compute_location_numbers(unsigned &nr)
Compute location numbers.
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.
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())
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
goto_programt(goto_programt &&other)
void compute_location_numbers()
Compute location numbers.
void swap(goto_programt &program)
Swap the goto program.
goto_programt & operator=(const goto_programt &)=delete
static instructiont make_location(const source_locationt &l)
static instructiont make_incomplete_goto(const code_gotot &_code, const source_locationt &l=source_locationt::nil())
void compute_target_numbers()
Compute the target numbers.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
bool empty() const
Is the program empty?
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())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
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())
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
void compute_loop_numbers()
Compute loop numbers.
std::list< targett > targetst
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static const source_locationt & nil()
Expression to hold a symbol (variable)
The Boolean constant true.
#define SINCE(year, month, day, msg)
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.
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()
const std::string & id2string(const irep_idt &d)
nonstd::optional< T > optionalt
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
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)
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