72 if(!instruction.
labels.empty())
75 for(
const auto &label : instruction.
labels)
86 switch(instruction.
type())
89 out <<
"NO INSTRUCTION TYPE SET" <<
'\n';
103 out <<
"(incomplete)";
107 for(
auto gt_it = instruction.
targets.begin();
108 gt_it != instruction.
targets.end();
111 if(gt_it != instruction.
targets.begin())
113 out << (*gt_it)->target_number;
123 const auto &code = instruction.
get_other();
124 if(code.get_statement() == ID_havoc_object)
126 out <<
"HAVOC_OBJECT " <<
format(code.op0()) <<
'\n';
193 out <<
"SKIP" <<
'\n';
197 out <<
"END_FUNCTION" <<
'\n';
201 out <<
"LOCATION" <<
'\n';
211 for(
const auto &ex : exception_list)
212 out <<
" " << ex.id();
226 out <<
"EXCEPTION LANDING PAD (" <<
format(landingpad.catch_expr().type())
227 <<
' ' <<
format(landingpad.catch_expr()) <<
")";
231 out <<
"CATCH-PUSH ";
237 instruction.
targets.size() == exception_list.size(),
238 "unexpected discrepancy between sizes of instruction"
239 "targets and exception list");
240 for(instructiont::targetst::const_iterator
241 gt_it=instruction.
targets.begin();
242 gt_it!=instruction.
targets.end();
245 if(gt_it!=instruction.
targets.begin())
247 out << exception_list[i].id() <<
"->"
248 << (*gt_it)->target_number;
265 out <<
"ATOMIC_BEGIN" <<
'\n';
269 out <<
"ATOMIC_END" <<
'\n';
273 out <<
"START THREAD "
279 out <<
"END THREAD" <<
'\n';
291 if(instruction.is_decl())
294 instruction.get_code().get_statement() == ID_decl,
295 "expected statement to be declaration statement");
297 instruction.get_code().operands().size() == 1,
298 "declaration statement expects one operand");
299 decl_identifiers.insert(instruction.decl_symbol().get_identifier());
306 if(src.
id()==ID_dereference)
310 else if(src.
id()==ID_index)
313 dest.push_back(index_expr.index());
316 else if(src.
id()==ID_member)
320 else if(src.
id()==ID_if)
323 dest.push_back(if_expr.cond());
332 std::list<exprt> dest;
334 switch(instruction.
type())
348 dest.push_back(argument);
381 std::list<exprt> dest;
383 switch(instruction.
type())
387 dest.push_back(instruction.
call_lhs());
420 std::list<exprt> &dest)
422 if(src.
id()==ID_symbol)
424 else if(src.
id()==ID_address_of)
428 else if(src.
id()==ID_dereference)
432 dest.push_back(deref);
447 std::list<exprt> dest;
449 for(
const auto &expr : expressions)
457 std::list<exprt> &dest)
474 std::list<exprt> dest;
476 for(
const auto &expr : expressions)
492 return "(NO INSTRUCTION TYPE)";
502 for(goto_programt::instructiont::targetst::const_iterator
541 return "END_FUNCTION";
553 return "ATOMIC_BEGIN";
559 result+=
"START THREAD ";
582 if(i.is_backwards_goto())
597 std::ostream &out)
const
628 for(
const auto &t : i.targets)
642 i.target_number=++cnt;
644 i.target_number != 0,
"GOTO instruction target cannot be zero");
653 for(
const auto &t : i.targets)
658 t->target_number != 0,
"instruction's number cannot be zero");
661 "GOTO instruction target cannot be nil_target");
674 typedef std::map<const_targett, targett> targets_mappingt;
675 targets_mappingt targets_mapping;
681 for(instructionst::const_iterator
687 targets_mapping[it]=new_instruction;
688 *new_instruction=*it;
695 for(
auto &t : i.targets)
697 targets_mappingt::iterator
698 m_target_it=targets_mapping.find(t);
702 t=m_target_it->second;
715 if(i.is_assert() && !i.get_condition().is_true())
726 i.incoming_edges.clear();
729 for(instructionst::iterator
737 s->incoming_edges.insert(it);
761 auto expr_symbol_finder = [&](
const exprt &e) {
766 for(
const auto &identifier : typetags)
770 !ns.
lookup(identifier, symbol),
776 auto ¤t_source_location = source_location();
778 [&ns, vm, ¤t_source_location](
const exprt &e) {
779 if(e.id() == ID_symbol)
782 const auto &goto_id = goto_symbol_expr.get_identifier();
785 if(!ns.
lookup(goto_id, table_symbol))
787 bool symbol_expr_type_matches_symbol_table =
791 !symbol_expr_type_matches_symbol_table &&
792 table_symbol->
type.
id() == ID_code)
799 goto_symbol_expr.type().source_location().get_file() !=
803 auto goto_symbol_expr_type =
807 goto_symbol_expr_type.return_type() =
808 table_symbol_type.return_type();
810 symbol_expr_type_matches_symbol_table =
811 base_type_eq(goto_symbol_expr_type, table_symbol_type, ns);
816 !symbol_expr_type_matches_symbol_table &&
817 goto_symbol_expr.type().id() == ID_array &&
823 if(table_symbol->
type.
id() == ID_array)
826 symbol_table_array_type.size() =
nil_exprt();
828 symbol_expr_type_matches_symbol_table =
829 goto_symbol_expr.type() == symbol_table_array_type;
835 symbol_expr_type_matches_symbol_table,
836 id2string(goto_id) +
" type inconsistency\n" +
837 "goto program type: " + goto_symbol_expr.type().id_string() +
838 "\n" +
"symbol table type: " + table_symbol->
type.
id_string(),
839 current_source_location);
853 "goto instruction expects at least one target",
858 get_target()->is_target() && get_target()->target_number != 0,
859 "goto target has to be a target",
866 "assume instruction should not have a target",
873 "assert instruction should not have a target",
876 std::for_each(guard.depth_begin(), guard.depth_end(), expr_symbol_finder);
877 std::for_each(guard.depth_begin(), guard.depth_end(), type_finder);
898 code.get_statement() == ID_return,
899 "SET_RETURN_VALUE instruction should contain a return statement",
905 code.get_statement() == ID_assign,
906 "assign instruction should contain an assign statement");
908 vm, targets.empty(),
"assign instruction should not have a target");
913 code.get_statement() == ID_decl,
914 "declaration instructions should contain a declaration statement",
919 "declared symbols should be known",
926 code.get_statement() == ID_dead,
927 "dead instructions should contain a dead statement",
932 "removed symbols should be known",
939 code.get_statement() == ID_function_call,
940 "function call instruction should contain a call statement",
943 std::for_each(code.depth_begin(), code.depth_end(), expr_symbol_finder);
944 std::for_each(code.depth_begin(), code.depth_end(), type_finder);
961 if(get_other().get_statement() == ID_expression)
964 if(new_expression.has_value())
967 new_other.expression() = *new_expression;
968 set_other(new_other);
975 auto new_return_value = f(return_value());
976 if(new_return_value.has_value())
977 return_value() = *new_return_value;
983 auto new_assign_lhs = f(assign_lhs());
984 auto new_assign_rhs = f(assign_rhs());
985 if(new_assign_lhs.has_value())
986 assign_lhs_nonconst() = new_assign_lhs.value();
987 if(new_assign_rhs.has_value())
988 assign_rhs_nonconst() = new_assign_rhs.value();
994 auto new_symbol = f(decl_symbol());
995 if(new_symbol.has_value())
1002 auto new_symbol = f(dead_symbol());
1003 if(new_symbol.has_value())
1010 auto new_lhs = f(
as_const(*this).call_lhs());
1011 if(new_lhs.has_value())
1012 call_lhs() = *new_lhs;
1014 auto new_call_function = f(
as_const(*this).call_function());
1015 if(new_call_function.has_value())
1016 call_function() = *new_call_function;
1019 bool argument_changed =
false;
1021 for(
auto &a : new_arguments)
1024 if(new_a.has_value())
1027 argument_changed =
true;
1031 if(argument_changed)
1032 call_arguments() = std::move(new_arguments);
1052 auto new_condition = f(get_condition());
1053 if(new_condition.has_value())
1054 set_condition(new_condition.value());
1060 std::function<
void(
const exprt &)> f)
const
1065 if(get_other().get_statement() == ID_expression)
1088 for(
auto &a : call_arguments())
1119 if(!ins.equals(*other_it))
1123 auto other_target_it = other_it->targets.begin();
1124 for(
const auto &t : ins.targets)
1127 t->location_number - ins.location_number !=
1128 (*other_target_it)->location_number - other_it->location_number)
1148 out <<
"NO_INSTRUCTION_TYPE";
1172 out <<
"START_THREAD";
1175 out <<
"END_THREAD";
1181 out <<
"END_FUNCTION";
1184 out <<
"ATOMIC_BEGIN";
1187 out <<
"ATOMIC_END";
1190 out <<
"SET_RETURN_VALUE";
1196 out <<
"FUNCTION_CALL";
1205 out <<
"INCOMPLETE_GOTO";
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
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
codet representation of a goto 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.
std::vector< exprt > operandst
bool is_true() const
Return whether the expression is a constant representing true.
typet & type()
Return the type of the expression.
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.
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
bool is_target() const
Is this node a branch target?
codet code
Do not read or modify directly – use get_X() instead.
const codet & get_other() const
Get the statement for OTHER.
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
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 SET_RETURN_VALUE instruction.
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
const codet & get_code() const
Get the code represented by this instruction.
goto_program_instruction_typet _type
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.
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
const source_locationt & source_location() const
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 guard
Guard for gotos, assume, assert Use condition() method to access.
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
bool is_incomplete_goto() const
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
goto_program_instruction_typet type() const
What kind of instruction?
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.
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...
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
void compute_loop_numbers()
Compute loop numbers.
const irept & find(const irep_idt &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.
The Boolean constant true.
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)
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)
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#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...