57 if(!instruction.
labels.empty())
60 for(
const auto &label : instruction.
labels)
71 switch(instruction.
type)
74 out <<
"NO INSTRUCTION TYPE SET" <<
'\n';
89 out <<
"(incomplete)";
93 for(
auto gt_it = instruction.
targets.begin();
94 gt_it != instruction.
targets.end();
97 if(gt_it != instruction.
targets.begin())
99 out << (*gt_it)->target_number;
134 out <<
"SKIP" <<
'\n';
138 out <<
"END_FUNCTION" <<
'\n';
142 out <<
"LOCATION" <<
'\n';
152 for(
const auto &ex : exception_list)
153 out <<
" " << ex.id();
167 out <<
"EXCEPTION LANDING PAD ("
168 <<
from_type(ns, identifier, landingpad.catch_expr().type())
170 <<
from_expr(ns, identifier, landingpad.catch_expr())
175 out <<
"CATCH-PUSH ";
181 instruction.
targets.size() == exception_list.size(),
182 "unexpected discrepancy between sizes of instruction"
183 "targets and exception list");
184 for(instructiont::targetst::const_iterator
185 gt_it=instruction.
targets.begin();
186 gt_it!=instruction.
targets.end();
189 if(gt_it!=instruction.
targets.begin())
191 out << exception_list[i].id() <<
"->"
192 << (*gt_it)->target_number;
209 out <<
"ATOMIC_BEGIN" <<
'\n';
213 out <<
"ATOMIC_END" <<
'\n';
217 out <<
"START THREAD "
223 out <<
"END THREAD" <<
'\n';
235 if(instruction.is_decl())
238 instruction.code.get_statement() == ID_decl,
239 "expected statement to be declaration statement");
241 instruction.code.operands().size() == 1,
242 "declaration statement expects one operand");
243 decl_identifiers.insert(instruction.decl_symbol().get_identifier());
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)
293 for(
const auto &argument : function_call.
arguments())
294 dest.push_back(argument);
303 dest.push_back(assignment.
rhs());
331 std::list<exprt> dest;
333 switch(instruction.
type)
340 dest.push_back(function_call.
lhs());
374 std::list<exprt> &dest)
376 if(src.
id()==ID_symbol)
378 else if(src.
id()==ID_address_of)
382 else if(src.
id()==ID_dereference)
386 dest.push_back(deref);
401 std::list<exprt> dest;
403 for(
const auto &expr : expressions)
411 std::list<exprt> &dest)
428 std::list<exprt> dest;
430 for(
const auto &expr : expressions)
446 return "(NO INSTRUCTION TYPE)";
456 for(goto_programt::instructiont::targetst::const_iterator
495 return "END_FUNCTION";
507 return "ATOMIC_BEGIN";
513 result+=
"START THREAD ";
536 if(i.is_backwards_goto())
551 std::ostream &out)
const
582 for(
const auto &t : i.targets)
596 i.target_number=++cnt;
598 i.target_number != 0,
"GOTO instruction target cannot be zero");
607 for(
const auto &t : i.targets)
612 t->target_number != 0,
"instruction's number cannot be zero");
615 "GOTO instruction target cannot be nil_target");
628 typedef std::map<const_targett, targett> targets_mappingt;
629 targets_mappingt targets_mapping;
635 for(instructionst::const_iterator
641 targets_mapping[it]=new_instruction;
642 *new_instruction=*it;
649 for(
auto &t : i.targets)
651 targets_mappingt::iterator
652 m_target_it=targets_mapping.find(t);
656 t=m_target_it->second;
669 if(i.is_assert() && !i.get_condition().is_true())
680 i.incoming_edges.clear();
683 for(instructionst::iterator
691 s->incoming_edges.insert(it);
715 auto expr_symbol_finder = [&](
const exprt &e) {
720 for(
const auto &identifier : typetags)
724 !ns.
lookup(identifier, symbol),
730 auto ¤t_source_location = source_location;
732 [&ns, vm, ¤t_source_location](
const exprt &e) {
733 if(e.id() == ID_symbol)
736 const auto &goto_id = goto_symbol_expr.get_identifier();
739 if(!ns.
lookup(goto_id, table_symbol))
741 bool symbol_expr_type_matches_symbol_table =
745 !symbol_expr_type_matches_symbol_table &&
746 table_symbol->
type.
id() == ID_code)
753 goto_symbol_expr.type().source_location().get_file() !=
757 auto goto_symbol_expr_type =
761 goto_symbol_expr_type.return_type() =
762 table_symbol_type.return_type();
764 symbol_expr_type_matches_symbol_table =
765 base_type_eq(goto_symbol_expr_type, table_symbol_type, ns);
770 !symbol_expr_type_matches_symbol_table &&
771 goto_symbol_expr.type().id() == ID_array &&
777 if(table_symbol->
type.
id() == ID_array)
780 symbol_table_array_type.size() =
nil_exprt();
782 symbol_expr_type_matches_symbol_table =
783 goto_symbol_expr.type() == symbol_table_array_type;
789 symbol_expr_type_matches_symbol_table,
790 id2string(goto_id) +
" type inconsistency\n" +
791 "goto program type: " + goto_symbol_expr.type().id_string() +
792 "\n" +
"symbol table type: " + table_symbol->
type.
id_string(),
793 current_source_location);
807 "goto instruction expects at least one target",
812 get_target()->is_target() && get_target()->target_number != 0,
813 "goto target has to be a target",
820 "assume instruction should not have a target",
827 "assert instruction should not have a target",
830 std::for_each(guard.depth_begin(), guard.depth_end(), expr_symbol_finder);
831 std::for_each(guard.depth_begin(), guard.depth_end(), type_finder);
852 code.get_statement() == ID_return,
853 "return instruction should contain a return statement",
859 code.get_statement() == ID_assign,
860 "assign instruction should contain an assign statement");
862 vm, targets.empty(),
"assign instruction should not have a target");
867 code.get_statement() == ID_decl,
868 "declaration instructions should contain a declaration statement",
872 !ns.
lookup(decl_symbol().get_identifier(), table_symbol),
873 "declared symbols should be known",
874 id2string(decl_symbol().get_identifier()),
880 code.get_statement() == ID_dead,
881 "dead instructions should contain a dead statement",
885 !ns.
lookup(dead_symbol().get_identifier(), table_symbol),
886 "removed symbols should be known",
887 id2string(dead_symbol().get_identifier()),
893 code.get_statement() == ID_function_call,
894 "function call instruction should contain a call statement",
897 std::for_each(code.depth_begin(), code.depth_end(), expr_symbol_finder);
898 std::for_each(code.depth_begin(), code.depth_end(), type_finder);
915 if(get_other().get_statement() == ID_expression)
918 if(new_expression.has_value())
921 new_other.expression() = *new_expression;
922 set_other(new_other);
929 auto new_return_value = f(return_value());
930 if(new_return_value.has_value())
931 return_value() = *new_return_value;
937 auto new_assign_lhs = f(get_assign().lhs());
938 auto new_assign_rhs = f(get_assign().rhs());
939 if(new_assign_lhs.has_value() || new_assign_rhs.has_value())
941 auto new_assignment = get_assign();
942 new_assignment.lhs() = new_assign_lhs.value_or(new_assignment.lhs());
943 new_assignment.rhs() = new_assign_rhs.value_or(new_assignment.rhs());
944 set_assign(new_assignment);
951 auto new_symbol = f(decl_symbol());
952 if(new_symbol.has_value())
959 auto new_symbol = f(dead_symbol());
960 if(new_symbol.has_value())
967 auto new_call = get_function_call();
970 auto new_lhs = f(new_call.lhs());
971 if(new_lhs.has_value())
973 new_call.lhs() = *new_lhs;
977 for(
auto &a : new_call.arguments())
980 if(new_a.has_value())
988 set_function_call(new_call);
1008 auto new_condition = f(get_condition());
1009 if(new_condition.has_value())
1010 set_condition(new_condition.value());
1016 std::function<
void(
const exprt &)> f)
const
1021 if(get_other().get_statement() == ID_expression)
1030 f(get_assign().lhs());
1031 f(get_assign().rhs());
1044 const auto &call = get_function_call();
1046 for(
auto &a : call.arguments())
1078 if(!ins.equals(*other_it))
1082 auto other_target_it = other_it->targets.begin();
1083 for(
const auto &t : ins.targets)
1086 t->location_number - ins.location_number !=
1087 (*other_target_it)->location_number - other_it->location_number)
1107 out <<
"NO_INSTRUCTION_TYPE";
1131 out <<
"START_THREAD";
1134 out <<
"END_THREAD";
1140 out <<
"END_FUNCTION";
1143 out <<
"ATOMIC_BEGIN";
1146 out <<
"ATOMIC_END";
1155 out <<
"FUNCTION_CALL";
1164 out <<
"INCOMPLETE_GOTO";
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
bool is_incomplete() const
A codet representing an assignment in the program.
codet representation of a function call statement.
const irep_idt & get_statement() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
This class represents an instruction in the GOTO intermediate representation.
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.
bool is_target() const
Is this node a branch target?
codet code
Do not read or modify directly – use get_X() instead.
source_locationt source_location
The location of the instruction in the source file.
goto_program_instruction_typet type
What kind of instruction?
void apply(std::function< void(const exprt &)>) const
Apply given function to all expressions.
targetst targets
The list of successor instructions.
const exprt & return_value() const
Get the return value of a RETURN 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.
bool equals(const instructiont &other) const
Syntactic equality: two instructiont are equal if they have the same type, code, guard,...
unsigned location_number
A globally unique number to identify a program location.
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.
exprt guard
Guard for gotos, assume, assert Use get_condition() to read, and set_condition(c) to write.
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
bool is_incomplete_goto() const
void validate(const namespacet &ns, const validation_modet vm) const
Check that the instruction is well-formed.
A generic container class for the GOTO intermediate representation of one function.
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 update()
Update all indices.
bool has_assertion() const
Does the goto program have an assertion?
instructionst::const_iterator const_targett
targett add_instruction()
Adds an instruction at the end.
void compute_incoming_edges()
Compute for each instruction the set of instructions it is a successor of.
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.
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
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.
void compute_location_numbers()
Compute location numbers.
void compute_target_numbers()
Compute the target numbers.
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 compute_loop_numbers()
Compute loop numbers.
const irept & find(const irep_namet &name) const
const std::string & id_string() const
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const irep_idt & get_comment() const
const irep_idt & get_file() const
std::string as_string() const
typet type
Type of symbol.
const source_locationt & source_location() const
#define forall_operands(it, expr)
Forward depth-first search iterators These iterators' copy operations are expensive,...
void find_type_symbols(const exprt &src, find_symbols_sett &dest)
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.
std::unordered_set< irep_idt > find_symbols_sett
void parse_lhs_read(const exprt &src, std::list< exprt > &dest)
std::list< exprt > expressions_written(const goto_programt::instructiont &instruction)
std::string as_string(const class namespacet &ns, const irep_idt &function, const goto_programt::instructiont &i)
void objects_read(const exprt &src, std::list< exprt > &dest)
std::ostream & operator<<(std::ostream &out, goto_program_instruction_typet t)
Outputs a string representation of a goto_program_instruction_typet
void objects_written(const exprt &src, std::list< exprt > &dest)
std::list< exprt > expressions_read(const goto_programt::instructiont &instruction)
goto_program_instruction_typet
The type of an instruction in a GOTO program.
const std::string & id2string(const irep_idt &d)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
nonstd::optional< T > optionalt
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Replace function returns by assignments to global variables.
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
static code_landingpadt & to_code_landingpad(codet &code)
code_expressiont & to_code_expression(codet &code)
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
#define DATA_CHECK_WITH_DIAGNOSTICS(vm, condition, message,...)
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
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...
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...