Go to the documentation of this file.
43 exprt::operandst::const_iterator it1=arguments.begin();
46 for(
const auto &identifier : parameter_identifiers)
50 source_location.
as_string() +
": no identifier for function parameter");
55 const typet ¶meter_type = symbol.
type;
59 decl->code.add_source_location() = source_location;
65 if(it1==arguments.end())
68 warning() <<
"call to '" << function_name <<
"': "
69 <<
"not enough arguments, "
70 <<
"inserting non-deterministic value" <<
eom;
85 if(parameter_type != actual.
type())
87 const typet &f_partype = parameter_type;
91 if((f_partype.
id()==ID_pointer &&
92 f_acttype.
id()==ID_pointer) ||
93 (f_partype.
id()==ID_pointer &&
94 f_acttype.
id()==ID_array &&
99 else if((f_partype.
id()==ID_signedbv ||
100 f_partype.
id()==ID_unsignedbv ||
101 f_partype.
id()==ID_bool) &&
102 (f_acttype.
id()==ID_signedbv ||
103 f_acttype.
id()==ID_unsignedbv ||
104 f_acttype.
id()==ID_bool))
121 if(it1!=arguments.end())
125 if(it1!=arguments.end())
141 for(
const auto &identifier : parameter_identifiers)
145 source_location.
as_string() +
": no identifier for function parameter");
152 dead->code.add_source_location()=source_location;
161 for(goto_programt::instructionst::iterator
168 const auto &code_return = it->get_return();
172 if(!code_return.has_return_value())
175 warning() <<
"return expects one operand!\n"
176 << it->code.pretty() <<
eom;
185 code_return.return_value(), lhs.
type()));
190 else if(code_return.has_return_value())
216 if(!property_class.
empty())
219 if(!property_id.
empty())
246 const irep_idt identifier=
function.get_identifier();
255 "final instruction of a function must be an END_FUNCTION");
259 if(
ns.
lookup(identifier).is_hidden())
281 unsigned begin_location_number=t_it->location_number;
284 t_it->is_end_function(),
285 "final instruction of a function must be an END_FUNCTION");
286 unsigned end_location_number=t_it->location_number;
288 unsigned call_location_number=target->location_number;
292 begin_location_number,
294 call_location_number,
304 if(it->has_condition())
306 exprt c = it->get_condition();
308 it->set_condition(c);
315 target->code.clear();
324 const bool transitive,
325 const bool force_full,
333 std::cout <<
"Expanding call:\n";
341 get_call(target, lhs, function_expr, arguments);
343 if(function_expr.
id()!=ID_symbol)
348 const irep_idt identifier=
function.get_identifier();
359 warning() <<
"recursion is ignored on call to '" << identifier <<
"'"
363 target->turn_into_skip();
368 goto_functionst::function_mapt::iterator f_it=
374 warning() <<
"missing function '" << identifier <<
"' is ignored" <<
eom;
377 target->turn_into_skip();
404 progress() <<
"Inserting " << identifier <<
" into caller" <<
eom;
405 progress() <<
"Number of instructions: "
410 progress() <<
"Removing " << identifier <<
" from cache" <<
eom;
411 progress() <<
"Number of instructions: "
415 cache.erase(identifier);
442 warning() <<
"no body for function '" << identifier <<
"'" <<
eom;
464 const bool force_full)
470 const irep_idt identifier=f_it->first;
477 goto_inline(identifier, goto_function, inline_map, force_full);
485 const bool force_full)
500 const bool force_full)
504 finished_sett::const_iterator f_it=
finished_set.find(identifier);
513 const inline_mapt::const_iterator im_it=inline_map.find(identifier);
515 if(im_it==inline_map.end())
520 if(call_list.empty())
525 for(
const auto &call : call_list)
527 const bool transitive=call.second;
551 const bool force_full)
555 cachet::const_iterator c_it=
cache.find(identifier);
557 if(c_it!=
cache.end())
562 "body of cached functions must be available");
568 cached.
body.
empty(),
"body of new function in cache must be empty");
570 progress() <<
"Creating copy of " << identifier <<
eom;
571 progress() <<
"Number of instructions: "
583 if(i_it->is_function_call())
584 call_list.push_back(i_it);
587 if(call_list.empty())
592 for(
const auto &call : call_list)
621 goto_functionst::function_mapt::const_iterator f_it=
626 inline_mapt::const_iterator im_it=inline_map.find(identifier);
628 if(im_it==inline_map.end())
633 if(call_list.empty())
638 for(
const auto &call : call_list)
644 if(target->function!=identifier)
651 target->location_number <= ln)
656 if(!target->is_function_call())
659 ln=target->location_number;
682 for(
const auto &it : inline_map)
687 out <<
"Function: " <<
id <<
"\n";
689 goto_functionst::function_mapt::const_iterator f_it=
698 "cannot inline function with empty body");
702 for(
const auto &call : call_list)
705 bool transitive=call.second;
709 out <<
" Transitive: " << transitive <<
"\n";
721 for(
auto it=
cache.begin(); it!=
cache.end(); it++)
723 if(it!=
cache.begin())
726 out << it->first <<
"\n";
741 for(
const auto &it : function_map)
748 cleanup(goto_function.
body);
754 const unsigned begin_location_number,
755 const unsigned end_location_number,
756 const unsigned call_location_number,
761 PRECONDITION(end_location_number >= begin_location_number);
765 log_map.find(start) == log_map.end(),
766 "inline function should be registered once in map of inline functions");
794 "'to' target function is not allowed to be empty");
796 it1->location_number == it2->location_number,
797 "both functions' instruction should point to the same source");
799 log_mapt::const_iterator l_it=log_map.find(it1);
800 if(l_it!=log_map.end())
804 log_map.find(it2) == log_map.end(),
805 "'to' target is not expected to be in the log_map");
832 for(
const auto &it : log_map)
838 PRECONDITION(start->location_number <= end->location_number);
849 {
"originalSegment", std::move(json_orig)},
850 {
"inlinedSegment", std::move(json_new)}};
852 json_inlined.
push_back(std::move(
object));
855 return std::move(json_result);
#define Forall_goto_program_instructions(it, program)
#define UNREACHABLE
This should be used to mark dead code.
unsigned begin_location_number
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const irep_idt & get_comment() const
const irep_idt & get_property_id() const
static exprt conditional_cast(const exprt &expr, const typet &type)
const char * c_str() const
const irep_idt & get_property_class() const
const typet & subtype() const
std::string as_string() const
void set_comment(const irep_idt &comment)
#define Forall_operands(it, expr)
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
void insert_function_body(const goto_functiont &f, goto_programt &dest, goto_programt::targett target, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments)
The type of an expression, extends irept.
std::list< callt > call_listt
void add_segment(const goto_programt &goto_program, const unsigned begin_location_number, const unsigned end_location_number, const unsigned call_location_number, const irep_idt function)
unsigned call_location_number
void replace_return(goto_programt &body, const exprt &lhs)
static void get_call(goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments)
typet type
Type of symbol.
goto_program_instruction_typet type
What kind of instruction?
const irept & find(const irep_namet &name) const
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
void set_property_id(const irep_idt &property_id)
bool empty() const
Is the program empty?
Base class for all expressions.
void goto_inline(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full=false)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void cleanup(const goto_programt &goto_program)
function_mapt function_map
Expression to hold a symbol (variable)
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
unsigned end_location_number
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
const bool adjust_function
void goto_inline_nontransitive(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full)
std::list< targett > targetst
recursion_sett recursion_set
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().
codet representation of a function call statement.
bool body_available() const
std::map< irep_idt, goto_functiont > function_mapt
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
source_locationt source_location
jsont output_inline_log_json() const
#define PRECONDITION(CONDITION)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
void parameter_destruction(const goto_programt::targett target, const goto_functiont::parameter_identifierst ¶meter_identifiers, goto_programt &dest)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
goto_programt::const_targett end
void replace_location(source_locationt &dest, const source_locationt &new_location)
const irep_idt & id() const
goto_functionst & goto_functions
bool is_end_function() const
A goto function, consisting of function type (see type), function body (see body),...
std::vector< exprt > operandst
json_arrayt & make_array()
#define Forall_goto_functions(it, functions)
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
void output_inline_map(std::ostream &out, const inline_mapt &inline_map)
std::map< irep_idt, call_listt > inline_mapt
A side_effect_exprt that returns a non-deterministically chosen value.
void parameter_assignments(const goto_programt::targett target, const irep_idt &function_name, const goto_functiont::parameter_identifierst ¶meter_identifiers, const exprt::operandst &arguments, goto_programt &dest)
instructionst instructions
The list of instructions in the goto program.
Deprecated expression utility functions.
finished_sett finished_set
const goto_functiont & goto_inline_transitive(const irep_idt identifier, const goto_functiont &goto_function, const bool force_full)
void expand_function_call(goto_programt &dest, const inline_mapt &inline_map, const bool transitive, const bool force_full, goto_programt::targett target)
bool check_inline_map(const inline_mapt &inline_map) const
void copy_from(const goto_functiont &other)
goto_inline_logt inline_log
A generic container class for the GOTO intermediate representation of one function.
std::vector< irep_idt > parameter_identifierst
#define forall_goto_functions(it, functions)
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
instructionst::const_iterator const_targett
bool is_ignored(const irep_idt id) const
mstreamt & progress() const
source_locationt & add_source_location()
Semantic type conversion.
A codet representing an assignment in the program.
mstreamt & warning() const
void copy_from(const goto_programt &from, const goto_programt &to)
static std::string comment(const rw_set_baset::entryt &entry, bool write)
This class represents an instruction in the GOTO intermediate representation.
void output_cache(std::ostream &out) const
API to expression classes.
const source_locationt & source_location() const
static const unsigned nil_target
Uniquely identify an invalid target or location.
jsont & push_back(const jsont &json)
instructionst::iterator targett
#define forall_goto_program_instructions(it, program)
codet representation of an expression statement.
goto_functionst::goto_functiont goto_functiont
void set_property_class(const irep_idt &property_class)