52 if(!instruction.
labels.empty())
55 for(
const auto &label : instruction.
labels)
66 switch(instruction.
type)
69 out <<
"NO INSTRUCTION TYPE SET" <<
'\n';
82 for(instructiont::targetst::const_iterator
83 gt_it=instruction.
targets.begin();
84 gt_it!=instruction.
targets.end();
87 if(gt_it!=instruction.
targets.begin())
89 out << (*gt_it)->target_number;
123 out <<
"SKIP" <<
'\n';
127 out <<
"END_FUNCTION" <<
'\n';
131 out <<
"LOCATION" <<
'\n';
141 for(
const auto &ex : exception_list)
142 out <<
" " << ex.id();
156 out <<
"EXCEPTION LANDING PAD (" 157 <<
from_type(ns, identifier, landingpad.catch_expr().type())
159 <<
from_expr(ns, identifier, landingpad.catch_expr())
164 out <<
"CATCH-PUSH ";
170 instruction.
targets.size() == exception_list.size(),
171 "unexpected discrepancy between sizes of instruction" 172 "targets and exception list");
173 for(instructiont::targetst::const_iterator
174 gt_it=instruction.
targets.begin();
175 gt_it!=instruction.
targets.end();
178 if(gt_it!=instruction.
targets.begin())
180 out << exception_list[i].id() <<
"->" 181 << (*gt_it)->target_number;
198 out <<
"ATOMIC_BEGIN" <<
'\n';
202 out <<
"ATOMIC_END" <<
'\n';
206 out <<
"START THREAD " 212 out <<
"END THREAD" <<
'\n';
230 it->code.get_statement() == ID_decl,
231 "expected statement to be declaration statement");
233 it->code.operands().size() == 1,
234 "declaration statement expects one operand");
236 decl_identifiers.insert(symbol_expr.get_identifier());
243 if(src.
id()==ID_dereference)
247 else if(src.
id()==ID_index)
250 dest.push_back(index_expr.index());
253 else if(src.
id()==ID_member)
257 else if(src.
id()==ID_if)
260 dest.push_back(if_expr.cond());
269 std::list<exprt> dest;
271 switch(instruction.
type)
276 dest.push_back(instruction.
guard);
298 dest.push_back(assignment.
rhs());
314 std::list<exprt> dest;
316 switch(instruction.
type)
323 dest.push_back(function_call.
lhs());
341 std::list<exprt> &dest)
343 if(src.
id()==ID_symbol)
345 else if(src.
id()==ID_address_of)
349 else if(src.
id()==ID_dereference)
353 dest.push_back(deref);
368 std::list<exprt> dest;
370 for(
const auto &expr : expressions)
378 std::list<exprt> &dest)
395 std::list<exprt> dest;
397 for(
const auto &expr : expressions)
412 return "(NO INSTRUCTION TYPE)";
424 for(goto_programt::instructiont::targetst::const_iterator
463 return "END_FUNCTION";
475 return "ATOMIC_BEGIN";
481 result+=
"START THREAD ";
502 if(i.is_backwards_goto())
517 std::ostream &out)
const 548 for(
const auto &t : i.targets)
562 i.target_number=++cnt;
564 i.target_number != 0,
"GOTO instruction target cannot be zero");
573 for(
const auto &t : i.targets)
578 t->target_number != 0,
"instruction's number cannot be zero");
581 "GOTO instruction target cannot be nil_target");
594 typedef std::map<const_targett, targett> targets_mappingt;
595 targets_mappingt targets_mapping;
601 for(instructionst::const_iterator
607 targets_mapping[it]=new_instruction;
608 *new_instruction=*it;
615 for(
auto &t : i.targets)
617 targets_mappingt::iterator
618 m_target_it=targets_mapping.find(t);
622 t=m_target_it->second;
635 if(i.is_assert() && !i.guard.is_true())
646 i.incoming_edges.clear();
649 for(instructionst::iterator
657 s->incoming_edges.insert(it);
684 !ns.
lookup(
function, table_symbol),
688 auto expr_symbol_finder = [&](
const exprt &e) {
693 for(
const auto &identifier : typetags)
697 !ns.
lookup(identifier, symbol),
703 auto ¤t_source_location = source_location;
705 [&ns, vm, &table_symbol, ¤t_source_location](
const exprt &e) {
706 if(e.id() == ID_symbol)
709 const auto &goto_id = goto_symbol_expr.get_identifier();
711 if(!ns.
lookup(goto_id, table_symbol))
714 base_type_eq(goto_symbol_expr.type(), table_symbol->type, ns),
715 id2string(goto_id) +
" type inconsistency\n" +
716 "goto program type: " + goto_symbol_expr.type().id_string() +
717 "\n" +
"symbol table type: " + table_symbol->type.id_string(),
718 current_source_location);
730 "goto instruction expects at least one target",
735 get_target()->is_target() && get_target()->target_number != 0,
736 "goto target has to be a target",
743 "assume instruction should not have a target",
750 "assert instruction should not have a target",
753 std::for_each(guard.depth_begin(), guard.depth_end(), expr_symbol_finder);
754 std::for_each(guard.depth_begin(), guard.depth_end(), type_finder);
775 code.get_statement() == ID_return,
776 "return instruction should contain a return statement",
782 code.get_statement() == ID_assign,
783 "assign instruction should contain an assign statement");
785 vm, targets.empty(),
"assign instruction should not have a target");
790 code.get_statement() == ID_decl,
791 "declaration instructions should contain a declaration statement",
796 "declared symbols should be known",
803 code.get_statement() == ID_dead,
804 "dead instructions should contain a dead statement",
809 "removed symbols should be known",
816 code.get_statement() == ID_function_call,
817 "function call instruction should contain a call statement",
820 std::for_each(code.depth_begin(), code.depth_end(), expr_symbol_finder);
821 std::for_each(code.depth_begin(), code.depth_end(), type_finder);
840 if(!ins.equals(*other_it))
844 auto other_target_it = other_it->targets.begin();
845 for(
const auto t : ins.targets)
848 t->location_number - ins.location_number !=
849 (*other_target_it)->location_number - other_it->location_number)
869 out <<
"NO_INSTRUCTION_TYPE";
893 out <<
"START_THREAD";
902 out <<
"END_FUNCTION";
905 out <<
"ATOMIC_BEGIN";
917 out <<
"FUNCTION_CALL";
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
exprt guard
Guard for gotos, assume, assert.
const irep_idt & get_statement() const
irep_idt function
The function this instruction belongs to.
void update()
Update all indices.
const exprt & return_value() const
const code_declt & to_code_decl(const codet &code)
const std::string & id2string(const irep_idt &d)
void compute_loop_numbers()
Compute loop numbers.
void validate(const namespacet &ns, const validation_modet vm) const
Check that the instruction is well-formed.
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
const code_deadt & to_code_dead(const codet &code)
unsigned location_number
A globally unique number to identify a program location.
std::vector< irept > subt
std::string comment(const rw_set_baset::entryt &entry, bool write)
goto_program_instruction_typet type
What kind of instruction?
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
#define forall_expr(it, expr)
std::string as_string() const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
bool has_assertion() const
Does the goto program have an assertion?
bool is_true() const
Return whether the expression is a constant representing true.
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
static const unsigned nil_target
Uniquely identify an invalid target or location.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
std::string as_string(const class namespacet &ns, const goto_programt::instructiont &i)
#define CHECK_RETURN(CONDITION)
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
Forward depth-first search iterators These iterators' copy operations are expensive,...
bool equals(const instructiont &other) const
Syntactic equality: two instructiont are equal if they have the same type, code, guard,...
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
targetst targets
The list of successor instructions.
This class represents an instruction in the GOTO intermediate representation.
void clear()
Clear the goto program.
unsigned target_number
A number to identify branch targets.
std::list< exprt > expressions_read(const goto_programt::instructiont &instruction)
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...
const code_assignt & to_code_assign(const codet &code)
std::set< irep_idt > decl_identifierst
const irep_idt & id() const
void compute_incoming_edges()
Compute for each instruction the set of instructions it is a successor of.
void validate_full_expr(const exprt &expr, const namespacet &ns, const validation_modet vm)
Check that the given expression is well-formed (full check, including checks of all subexpressions an...
void validate_full_code(const codet &code, const namespacet &ns, const validation_modet vm)
Check that the given code statement is well-formed (full check, including checks of all subexpression...
instructionst instructions
The list of instructions in the goto program.
API to expression classes.
instructionst::const_iterator const_targett
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
goto_program_instruction_typet
The type of an instruction in a GOTO program.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const code_returnt & to_code_return(const codet &code)
codet representation of a function call statement.
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
void objects_read(const exprt &src, std::list< exprt > &dest)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
void compute_location_numbers()
Compute location numbers.
A generic container class for the GOTO intermediate representation of one function.
std::list< exprt > expressions_written(const goto_programt::instructiont &instruction)
std::ostream & operator<<(std::ostream &out, goto_program_instruction_typet t)
Outputs a string representation of a goto_program_instruction_typet
static code_landingpadt & to_code_landingpad(codet &code)
source_locationt source_location
The location of the instruction in the source file.
targett add_instruction()
Adds an instruction at the end.
Base class for all expressions.
void parse_lhs_read(const exprt &src, std::list< exprt > &dest)
void compute_target_numbers()
Compute the target numbers.
#define UNREACHABLE
This should be used to mark dead code.
void objects_written(const exprt &src, std::list< exprt > &dest)
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Expression to hold a symbol (variable)
std::unordered_set< irep_idt > find_symbols_sett
const irep_idt & get_comment() const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
void find_type_symbols(const exprt &src, find_symbols_sett &dest)
#define forall_goto_program_instructions(it, program)
bool is_target() const
Is this node a branch target?
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const irept & find(const irep_namet &name) const
void find_symbols(const exprt &src, find_symbols_sett &dest)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
A codet representing an assignment in the program.
const code_function_callt & to_code_function_call(const codet &code)
#define DATA_CHECK_WITH_DIAGNOSTICS(vm, condition, message,...)