Go to the documentation of this file.
56 if(!instruction.
labels.empty())
59 for(
const auto &label : instruction.
labels)
70 switch(instruction.
type)
73 out <<
"NO INSTRUCTION TYPE SET" <<
'\n';
88 out <<
"(incomplete)";
92 for(
auto gt_it = instruction.
targets.begin();
93 gt_it != instruction.
targets.end();
96 if(gt_it != instruction.
targets.begin())
98 out << (*gt_it)->target_number;
133 out <<
"SKIP" <<
'\n';
137 out <<
"END_FUNCTION" <<
'\n';
141 out <<
"LOCATION" <<
'\n';
151 for(
const auto &ex : exception_list)
152 out <<
" " << ex.id();
166 out <<
"EXCEPTION LANDING PAD ("
167 <<
from_type(ns, identifier, landingpad.catch_expr().type())
169 <<
from_expr(ns, identifier, landingpad.catch_expr())
174 out <<
"CATCH-PUSH ";
180 instruction.
targets.size() == exception_list.size(),
181 "unexpected discrepancy between sizes of instruction"
182 "targets and exception list");
183 for(instructiont::targetst::const_iterator
184 gt_it=instruction.
targets.begin();
185 gt_it!=instruction.
targets.end();
188 if(gt_it!=instruction.
targets.begin())
190 out << exception_list[i].id() <<
"->"
191 << (*gt_it)->target_number;
208 out <<
"ATOMIC_BEGIN" <<
'\n';
212 out <<
"ATOMIC_END" <<
'\n';
216 out <<
"START THREAD "
222 out <<
"END THREAD" <<
'\n';
237 it->code.get_statement() == ID_decl,
238 "expected statement to be declaration statement");
240 it->code.operands().size() == 1,
241 "declaration statement expects one operand");
250 if(src.
id()==ID_dereference)
254 else if(src.
id()==ID_index)
257 dest.push_back(index_expr.index());
260 else if(src.
id()==ID_member)
264 else if(src.
id()==ID_if)
267 dest.push_back(if_expr.cond());
276 std::list<exprt> dest;
278 switch(instruction.
type)
304 dest.push_back(assignment.
rhs());
332 std::list<exprt> dest;
334 switch(instruction.
type)
341 dest.push_back(function_call.
lhs());
375 std::list<exprt> &dest)
377 if(src.
id()==ID_symbol)
379 else if(src.
id()==ID_address_of)
383 else if(src.
id()==ID_dereference)
387 dest.push_back(deref);
402 std::list<exprt> dest;
404 for(
const auto &expr : expressions)
412 std::list<exprt> &dest)
429 std::list<exprt> dest;
431 for(
const auto &expr : expressions)
447 return "(NO INSTRUCTION TYPE)";
457 for(goto_programt::instructiont::targetst::const_iterator
496 return "END_FUNCTION";
508 return "ATOMIC_BEGIN";
514 result+=
"START THREAD ";
537 if(i.is_backwards_goto())
552 std::ostream &out)
const
583 for(
const auto &t : i.targets)
597 i.target_number=++cnt;
599 i.target_number != 0,
"GOTO instruction target cannot be zero");
608 for(
const auto &t : i.targets)
613 t->target_number != 0,
"instruction's number cannot be zero");
616 "GOTO instruction target cannot be nil_target");
629 typedef std::map<const_targett, targett> targets_mappingt;
630 targets_mappingt targets_mapping;
636 for(instructionst::const_iterator
642 targets_mapping[it]=new_instruction;
643 *new_instruction=*it;
650 for(
auto &t : i.targets)
652 targets_mappingt::iterator
653 m_target_it=targets_mapping.find(t);
657 t=m_target_it->second;
670 if(i.is_assert() && !i.get_condition().is_true())
681 i.incoming_edges.clear();
684 for(instructionst::iterator
692 s->incoming_edges.insert(it);
716 auto expr_symbol_finder = [&](
const exprt &e) {
721 for(
const auto &identifier : typetags)
725 !ns.
lookup(identifier, symbol),
731 auto ¤t_source_location = source_location;
733 [&ns, vm, ¤t_source_location](
const exprt &e) {
734 if(e.id() == ID_symbol)
737 const auto &goto_id = goto_symbol_expr.get_identifier();
740 if(!ns.
lookup(goto_id, table_symbol))
742 bool symbol_expr_type_matches_symbol_table =
746 !symbol_expr_type_matches_symbol_table &&
747 table_symbol->
type.
id() == ID_code)
754 goto_symbol_expr.type().source_location().get_file() !=
758 auto goto_symbol_expr_type =
762 goto_symbol_expr_type.return_type() =
763 table_symbol_type.return_type();
765 symbol_expr_type_matches_symbol_table =
766 base_type_eq(goto_symbol_expr_type, table_symbol_type, ns);
771 !symbol_expr_type_matches_symbol_table &&
772 goto_symbol_expr.type().id() == ID_array &&
778 if(table_symbol->
type.
id() == ID_array)
781 symbol_table_array_type.size() =
nil_exprt();
783 symbol_expr_type_matches_symbol_table =
784 goto_symbol_expr.type() == symbol_table_array_type;
790 symbol_expr_type_matches_symbol_table,
791 id2string(goto_id) +
" type inconsistency\n" +
792 "goto program type: " + goto_symbol_expr.type().id_string() +
793 "\n" +
"symbol table type: " + table_symbol->
type.
id_string(),
794 current_source_location);
808 "goto instruction expects at least one target",
813 get_target()->is_target() && get_target()->target_number != 0,
814 "goto target has to be a target",
821 "assume instruction should not have a target",
828 "assert instruction should not have a target",
831 std::for_each(guard.depth_begin(), guard.depth_end(), expr_symbol_finder);
832 std::for_each(guard.depth_begin(), guard.depth_end(), type_finder);
853 code.get_statement() == ID_return,
854 "return instruction should contain a return statement",
860 code.get_statement() == ID_assign,
861 "assign instruction should contain an assign statement");
863 vm, targets.empty(),
"assign instruction should not have a target");
868 code.get_statement() == ID_decl,
869 "declaration instructions should contain a declaration statement",
873 !ns.
lookup(get_decl().get_identifier(), table_symbol),
874 "declared symbols should be known",
881 code.get_statement() == ID_dead,
882 "dead instructions should contain a dead statement",
886 !ns.
lookup(get_dead().get_identifier(), table_symbol),
887 "removed symbols should be known",
894 code.get_statement() == ID_function_call,
895 "function call instruction should contain a call statement",
898 std::for_each(code.depth_begin(), code.depth_end(), expr_symbol_finder);
899 std::for_each(code.depth_begin(), code.depth_end(), type_finder);
916 if(get_other().get_statement() == ID_expression)
919 if(new_expression.has_value())
922 new_other.expression() = *new_expression;
923 set_other(new_other);
930 auto new_return_value = f(get_return().return_value());
931 if(new_return_value.has_value())
933 auto new_return = get_return();
934 new_return.return_value() = *new_return_value;
935 set_return(new_return);
942 auto new_assign_lhs = f(get_assign().lhs());
943 auto new_assign_rhs = f(get_assign().rhs());
944 if(new_assign_lhs.has_value() || new_assign_rhs.has_value())
946 auto new_assignment = get_assign();
947 new_assignment.lhs() = new_assign_lhs.value_or(new_assignment.lhs());
948 new_assignment.rhs() = new_assign_rhs.value_or(new_assignment.rhs());
949 set_assign(new_assignment);
956 auto new_symbol = f(get_decl().symbol());
957 if(new_symbol.has_value())
959 auto new_decl = get_decl();
968 auto new_symbol = f(get_dead().symbol());
969 if(new_symbol.has_value())
971 auto new_dead = get_dead();
980 auto new_call = get_function_call();
983 auto new_lhs = f(new_call.lhs());
984 if(new_lhs.has_value())
986 new_call.lhs() = *new_lhs;
990 for(
auto &a : new_call.arguments())
993 if(new_a.has_value())
1001 set_function_call(new_call);
1021 auto new_condition = f(get_condition());
1022 if(new_condition.has_value())
1023 set_condition(new_condition.value());
1029 std::function<
void(
const exprt &)> f)
const
1034 if(get_other().get_statement() == ID_expression)
1039 f(get_return().return_value());
1043 f(get_assign().lhs());
1044 f(get_assign().rhs());
1048 f(get_decl().symbol());
1052 f(get_dead().symbol());
1057 const auto &call = get_function_call();
1059 for(
auto &a : call.arguments())
1091 if(!ins.equals(*other_it))
1095 auto other_target_it = other_it->targets.begin();
1096 for(
const auto &t : ins.targets)
1099 t->location_number - ins.location_number !=
1100 (*other_target_it)->location_number - other_it->location_number)
1120 out <<
"NO_INSTRUCTION_TYPE";
1144 out <<
"START_THREAD";
1147 out <<
"END_THREAD";
1153 out <<
"END_FUNCTION";
1156 out <<
"ATOMIC_BEGIN";
1159 out <<
"ATOMIC_END";
1168 out <<
"FUNCTION_CALL";
1177 out <<
"INCOMPLETE_GOTO";
#define UNREACHABLE
This should be used to mark dead code.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const irep_idt & get_comment() const
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
code_expressiont & to_code_expression(codet &code)
source_locationt source_location
The location of the instruction in the source file.
bool is_incomplete() const
std::string as_string() const
#define CHECK_RETURN(CONDITION)
void compute_loop_numbers()
Compute loop numbers.
const code_returnt & get_return() const
Get the return statement for READ.
void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
Add to the set dest the sub-expressions of src with id ID_symbol or ID_next_symbol.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
typet type
Type of symbol.
goto_program_instruction_typet type
What kind of instruction?
const irept & find(const irep_namet &name) const
void update()
Update all indices.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
void apply(std::function< void(const exprt &)>) const
Apply given function to all expressions.
void transform(std::function< optionalt< exprt >(exprt)>)
Apply given transformer to all expressions; no return value means no change needed.
Base class for all expressions.
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
bool has_assertion() const
Does the goto program have an assertion?
std::string as_string(const class namespacet &ns, const irep_idt &function, const goto_programt::instructiont &i)
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
#define DATA_CHECK_WITH_DIAGNOSTICS(vm, condition, message,...)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
targetst targets
The list of successor instructions.
bool is_incomplete_goto() const
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
bool is_true() const
Return whether the expression is a constant representing true.
std::list< exprt > expressions_written(const goto_programt::instructiont &instruction)
Expression to hold a symbol (variable)
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
targett add_instruction()
Adds an instruction at the end.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
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...
void validate(const namespacet &ns, const validation_modet vm) const
Check that the instruction is well-formed.
void compute_target_numbers()
Compute the target numbers.
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...
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const std::string & id2string(const irep_idt &d)
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
codet code
Do not read or modify directly – use get_X() instead.
std::ostream & operator<<(std::ostream &out, goto_program_instruction_typet t)
Outputs a string representation of a goto_program_instruction_typet
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
#define forall_operands(it, expr)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
const source_locationt & source_location() const
const irep_idt & get_identifier() const
void objects_read(const exprt &src, std::list< exprt > &dest)
void find_type_symbols(const exprt &src, find_symbols_sett &dest)
const code_function_callt & get_function_call() const
Get the function call for FUNCTION_CALL.
bool equals(const instructiont &other) const
Syntactic equality: two instructiont are equal if they have the same type, code, guard,...
const std::string & id_string() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
void objects_written(const exprt &src, std::list< exprt > &dest)
void compute_incoming_edges()
Compute for each instruction the set of instructions it is a successor of.
nonstd::optional< T > optionalt
Replace function returns by assignments to global variables.
void clear()
Clear the goto program.
goto_program_instruction_typet
The type of an instruction in a GOTO program.
void compute_location_numbers()
Compute location numbers.
instructionst instructions
The list of instructions in the goto program.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
static code_landingpadt & to_code_landingpad(codet &code)
unsigned target_number
A number to identify branch targets.
Forward depth-first search iterators These iterators' copy operations are expensive,...
std::unordered_set< irep_idt > find_symbols_sett
unsigned location_number
A globally unique number to identify a program location.
std::list< exprt > expressions_read(const goto_programt::instructiont &instruction)
exprt guard
Guard for gotos, assume, assert Use get_condition() to read, and set_condition(c) to write.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
A generic container class for the GOTO intermediate representation of one function.
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...
const irep_idt & get_file() const
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
instructionst::const_iterator const_targett
#define forall_expr(it, expr)
const exprt & return_value() const
A codet representing an assignment in the program.
const irep_idt & get_statement() const
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
std::set< irep_idt > decl_identifierst
static std::string comment(const rw_set_baset::entryt &entry, bool write)
This class represents an instruction in the GOTO intermediate representation.
API to expression classes.
bool is_target() const
Is this node a branch target?
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
static const unsigned nil_target
Uniquely identify an invalid target or location.
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
#define forall_goto_program_instructions(it, program)
void parse_lhs_read(const exprt &src, std::list< exprt > &dest)