Go to the documentation of this file.
62 if(!instruction.
labels.empty())
65 for(
const auto &label : instruction.
labels)
76 switch(instruction.
type)
79 out <<
"NO INSTRUCTION TYPE SET" <<
'\n';
93 out <<
"(incomplete)";
97 for(
auto gt_it = instruction.
targets.begin();
98 gt_it != instruction.
targets.end();
101 if(gt_it != instruction.
targets.begin())
103 out << (*gt_it)->target_number;
113 const auto &code = instruction.
get_other();
114 if(code.get_statement() == ID_havoc_object)
116 out <<
"HAVOC_OBJECT " <<
format(code.op0()) <<
'\n';
183 out <<
"SKIP" <<
'\n';
187 out <<
"END_FUNCTION" <<
'\n';
191 out <<
"LOCATION" <<
'\n';
201 for(
const auto &ex : exception_list)
202 out <<
" " << ex.id();
216 out <<
"EXCEPTION LANDING PAD (" <<
format(landingpad.catch_expr().type())
217 <<
' ' <<
format(landingpad.catch_expr()) <<
")";
221 out <<
"CATCH-PUSH ";
227 instruction.
targets.size() == exception_list.size(),
228 "unexpected discrepancy between sizes of instruction"
229 "targets and exception list");
230 for(instructiont::targetst::const_iterator
231 gt_it=instruction.
targets.begin();
232 gt_it!=instruction.
targets.end();
235 if(gt_it!=instruction.
targets.begin())
237 out << exception_list[i].id() <<
"->"
238 << (*gt_it)->target_number;
255 out <<
"ATOMIC_BEGIN" <<
'\n';
259 out <<
"ATOMIC_END" <<
'\n';
263 out <<
"START THREAD "
269 out <<
"END THREAD" <<
'\n';
281 if(instruction.is_decl())
284 instruction.get_code().get_statement() == ID_decl,
285 "expected statement to be declaration statement");
287 instruction.get_code().operands().size() == 1,
288 "declaration statement expects one operand");
289 decl_identifiers.insert(instruction.decl_symbol().get_identifier());
296 if(src.
id()==ID_dereference)
300 else if(src.
id()==ID_index)
303 dest.push_back(index_expr.index());
306 else if(src.
id()==ID_member)
310 else if(src.
id()==ID_if)
313 dest.push_back(if_expr.cond());
322 std::list<exprt> dest;
324 switch(instruction.
type)
338 dest.push_back(argument);
371 std::list<exprt> dest;
373 switch(instruction.
type)
377 dest.push_back(instruction.
call_lhs());
410 std::list<exprt> &dest)
412 if(src.
id()==ID_symbol)
414 else if(src.
id()==ID_address_of)
418 else if(src.
id()==ID_dereference)
422 dest.push_back(deref);
437 std::list<exprt> dest;
439 for(
const auto &expr : expressions)
447 std::list<exprt> &dest)
464 std::list<exprt> dest;
466 for(
const auto &expr : expressions)
482 return "(NO INSTRUCTION TYPE)";
492 for(goto_programt::instructiont::targetst::const_iterator
531 return "END_FUNCTION";
543 return "ATOMIC_BEGIN";
549 result+=
"START THREAD ";
572 if(i.is_backwards_goto())
587 std::ostream &out)
const
618 for(
const auto &t : i.targets)
632 i.target_number=++cnt;
634 i.target_number != 0,
"GOTO instruction target cannot be zero");
643 for(
const auto &t : i.targets)
648 t->target_number != 0,
"instruction's number cannot be zero");
651 "GOTO instruction target cannot be nil_target");
664 typedef std::map<const_targett, targett> targets_mappingt;
665 targets_mappingt targets_mapping;
671 for(instructionst::const_iterator
677 targets_mapping[it]=new_instruction;
678 *new_instruction=*it;
685 for(
auto &t : i.targets)
687 targets_mappingt::iterator
688 m_target_it=targets_mapping.find(t);
692 t=m_target_it->second;
705 if(i.is_assert() && !i.get_condition().is_true())
716 i.incoming_edges.clear();
719 for(instructionst::iterator
727 s->incoming_edges.insert(it);
751 auto expr_symbol_finder = [&](
const exprt &e) {
756 for(
const auto &identifier : typetags)
760 !ns.
lookup(identifier, symbol),
766 auto ¤t_source_location = source_location;
768 [&ns, vm, ¤t_source_location](
const exprt &e) {
769 if(e.id() == ID_symbol)
772 const auto &goto_id = goto_symbol_expr.get_identifier();
775 if(!ns.
lookup(goto_id, table_symbol))
777 bool symbol_expr_type_matches_symbol_table =
781 !symbol_expr_type_matches_symbol_table &&
782 table_symbol->
type.
id() == ID_code)
789 goto_symbol_expr.type().source_location().get_file() !=
793 auto goto_symbol_expr_type =
797 goto_symbol_expr_type.return_type() =
798 table_symbol_type.return_type();
800 symbol_expr_type_matches_symbol_table =
801 base_type_eq(goto_symbol_expr_type, table_symbol_type, ns);
806 !symbol_expr_type_matches_symbol_table &&
807 goto_symbol_expr.type().id() == ID_array &&
813 if(table_symbol->
type.
id() == ID_array)
816 symbol_table_array_type.size() =
nil_exprt();
818 symbol_expr_type_matches_symbol_table =
819 goto_symbol_expr.type() == symbol_table_array_type;
825 symbol_expr_type_matches_symbol_table,
826 id2string(goto_id) +
" type inconsistency\n" +
827 "goto program type: " + goto_symbol_expr.type().id_string() +
828 "\n" +
"symbol table type: " + table_symbol->
type.
id_string(),
829 current_source_location);
843 "goto instruction expects at least one target",
848 get_target()->is_target() && get_target()->target_number != 0,
849 "goto target has to be a target",
856 "assume instruction should not have a target",
863 "assert instruction should not have a target",
866 std::for_each(guard.depth_begin(), guard.depth_end(), expr_symbol_finder);
867 std::for_each(guard.depth_begin(), guard.depth_end(), type_finder);
888 code.get_statement() == ID_return,
889 "SET_RETURN_VALUE instruction should contain a return statement",
895 code.get_statement() == ID_assign,
896 "assign instruction should contain an assign statement");
898 vm, targets.empty(),
"assign instruction should not have a target");
903 code.get_statement() == ID_decl,
904 "declaration instructions should contain a declaration statement",
908 !ns.
lookup(decl_symbol().get_identifier(), table_symbol),
909 "declared symbols should be known",
910 id2string(decl_symbol().get_identifier()),
916 code.get_statement() == ID_dead,
917 "dead instructions should contain a dead statement",
921 !ns.
lookup(dead_symbol().get_identifier(), table_symbol),
922 "removed symbols should be known",
923 id2string(dead_symbol().get_identifier()),
929 code.get_statement() == ID_function_call,
930 "function call instruction should contain a call statement",
933 std::for_each(code.depth_begin(), code.depth_end(), expr_symbol_finder);
934 std::for_each(code.depth_begin(), code.depth_end(), type_finder);
951 if(get_other().get_statement() == ID_expression)
954 if(new_expression.has_value())
957 new_other.expression() = *new_expression;
958 set_other(new_other);
965 auto new_return_value = f(return_value());
966 if(new_return_value.has_value())
967 return_value() = *new_return_value;
973 auto new_assign_lhs = f(assign_lhs());
974 auto new_assign_rhs = f(assign_rhs());
975 if(new_assign_lhs.has_value())
976 assign_lhs_nonconst() = new_assign_lhs.value();
977 if(new_assign_rhs.has_value())
978 assign_rhs_nonconst() = new_assign_rhs.value();
984 auto new_symbol = f(decl_symbol());
985 if(new_symbol.has_value())
992 auto new_symbol = f(dead_symbol());
993 if(new_symbol.has_value())
1000 auto new_lhs = f(
as_const(*this).call_lhs());
1001 if(new_lhs.has_value())
1002 call_lhs() = *new_lhs;
1004 auto new_call_function = f(
as_const(*this).call_function());
1005 if(new_call_function.has_value())
1006 call_function() = *new_call_function;
1009 bool argument_changed =
false;
1011 for(
auto &a : new_arguments)
1014 if(new_a.has_value())
1017 argument_changed =
true;
1021 if(argument_changed)
1022 call_arguments() = std::move(new_arguments);
1042 auto new_condition = f(get_condition());
1043 if(new_condition.has_value())
1044 set_condition(new_condition.value());
1050 std::function<
void(
const exprt &)> f)
const
1055 if(get_other().get_statement() == ID_expression)
1078 for(
auto &a : call_arguments())
1109 if(!ins.equals(*other_it))
1113 auto other_target_it = other_it->targets.begin();
1114 for(
const auto &t : ins.targets)
1117 t->location_number - ins.location_number !=
1118 (*other_target_it)->location_number - other_it->location_number)
1138 out <<
"NO_INSTRUCTION_TYPE";
1162 out <<
"START_THREAD";
1165 out <<
"END_THREAD";
1171 out <<
"END_FUNCTION";
1174 out <<
"ATOMIC_BEGIN";
1177 out <<
"ATOMIC_END";
1180 out <<
"SET_RETURN_VALUE";
1186 out <<
"FUNCTION_CALL";
1195 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
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
#define CHECK_RETURN(CONDITION)
void compute_loop_numbers()
Compute loop numbers.
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)
#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)
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
const codet & get_other() const
Get the statement for OTHER.
const codet & get_code() const
Get the code represented by this instruction.
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.
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
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.
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
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 symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
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
void objects_read(const exprt &src, std::list< exprt > &dest)
API to expression classes for Pointers.
void find_type_symbols(const exprt &src, find_symbols_sett &dest)
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)
std::vector< exprt > operandst
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
void compute_incoming_edges()
Compute for each instruction the set of instructions it is a successor of.
nonstd::optional< T > optionalt
void clear()
Clear the goto program.
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
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.
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
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
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
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.
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
void parse_lhs_read(const exprt &src, std::list< exprt > &dest)