Go to the documentation of this file.
36 exprt::operandst::const_iterator it1=arguments.begin();
39 for(
const auto &identifier : parameter_identifiers)
43 source_location.
as_string() +
": no identifier for function parameter");
48 const typet ¶meter_type = symbol.
type;
52 decl->code_nonconst().add_source_location() = source_location;
58 if(it1==arguments.end())
61 log.
warning() <<
"call to '" << function_name <<
"': "
62 <<
"not enough arguments, "
78 if(parameter_type != actual.
type())
80 const typet &f_partype = parameter_type;
84 if((f_partype.
id()==ID_pointer &&
85 f_acttype.
id()==ID_pointer) ||
86 (f_partype.
id()==ID_pointer &&
87 f_acttype.
id()==ID_array &&
92 else if((f_partype.
id()==ID_signedbv ||
93 f_partype.
id()==ID_unsignedbv ||
94 f_partype.
id()==ID_bool) &&
95 (f_acttype.
id()==ID_signedbv ||
96 f_acttype.
id()==ID_unsignedbv ||
97 f_acttype.
id()==ID_bool))
114 if(it1!=arguments.end())
118 if(it1!=arguments.end())
134 for(
const auto &identifier : parameter_identifiers)
138 source_location.
as_string() +
": no identifier for function parameter");
145 dead->code_nonconst().add_source_location() = source_location;
154 for(goto_programt::instructionst::iterator
159 if(it->is_set_return_value())
195 if(!property_class.
empty())
198 if(!property_id.
empty())
225 const irep_idt identifier=
function.get_identifier();
234 "final instruction of a function must be an END_FUNCTION");
260 unsigned begin_location_number=t_it->location_number;
263 t_it->is_end_function(),
264 "final instruction of a function must be an END_FUNCTION");
265 unsigned end_location_number=t_it->location_number;
267 unsigned call_location_number=target->location_number;
271 begin_location_number,
273 call_location_number,
283 if(instruction.has_condition())
285 exprt c = instruction.get_condition();
287 instruction.set_condition(c);
294 target->code_nonconst().clear();
305 const bool transitive,
306 const bool force_full,
314 std::cout <<
"Expanding call:\n";
322 get_call(target, lhs, function_expr, arguments);
324 if(function_expr.
id()!=ID_symbol)
329 const irep_idt identifier=
function.get_identifier();
340 log.
warning() <<
"recursion is ignored on call to '" << identifier <<
"'"
344 target->turn_into_skip();
349 goto_functionst::function_mapt::iterator f_it=
355 log.
warning() <<
"missing function '" << identifier <<
"' is ignored"
359 target->turn_into_skip();
386 log.
progress() <<
"Inserting " << identifier <<
" into caller"
393 log.
progress() <<
"Removing " << identifier <<
" from cache"
399 cache.erase(identifier);
426 log.
warning() <<
"no body for function '" << identifier <<
"'"
440 lhs = it->call_lhs();
441 function = it->call_function();
442 arguments = it->call_arguments();
452 const bool force_full)
458 const irep_idt identifier = gf_entry.first;
465 goto_inline(identifier, goto_function, inline_map, force_full);
480 const bool force_full)
495 const bool force_full)
499 finished_sett::const_iterator f_it=
finished_set.find(identifier);
508 const inline_mapt::const_iterator im_it=inline_map.find(identifier);
510 if(im_it==inline_map.end())
515 if(call_list.empty())
520 for(
const auto &call : call_list)
522 const bool transitive=call.second;
546 const bool force_full)
550 cachet::const_iterator c_it=
cache.find(identifier);
552 if(c_it!=
cache.end())
557 "body of cached functions must be available");
563 cached.
body.
empty(),
"body of new function in cache must be empty");
578 if(i_it->is_function_call())
579 call_list.push_back(i_it);
582 if(call_list.empty())
587 for(
const auto &call : call_list)
616 goto_functionst::function_mapt::const_iterator f_it=
621 inline_mapt::const_iterator im_it=inline_map.find(identifier);
623 if(im_it==inline_map.end())
628 if(call_list.empty())
633 for(
const auto &call : call_list)
639 if(target->function!=identifier)
646 target->location_number <= ln)
651 if(!target->is_function_call())
654 ln=target->location_number;
677 for(
const auto &it : inline_map)
682 out <<
"Function: " <<
id <<
"\n";
684 goto_functionst::function_mapt::const_iterator f_it=
693 "cannot inline function with empty body");
697 for(
const auto &call : call_list)
700 bool transitive=call.second;
704 out <<
" Transitive: " << transitive <<
"\n";
716 for(
auto it=
cache.begin(); it!=
cache.end(); it++)
718 if(it!=
cache.begin())
721 out << it->first <<
"\n";
736 for(
const auto &it : function_map)
743 cleanup(goto_function.
body);
749 const unsigned begin_location_number,
750 const unsigned end_location_number,
751 const unsigned call_location_number,
756 PRECONDITION(end_location_number >= begin_location_number);
760 log_map.find(start) == log_map.end(),
761 "inline function should be registered once in map of inline functions");
789 "'to' target function is not allowed to be empty");
791 it1->location_number == it2->location_number,
792 "both functions' instruction should point to the same source");
794 log_mapt::const_iterator l_it=log_map.find(it1);
795 if(l_it!=log_map.end())
799 log_map.find(it2) == log_map.end(),
800 "'to' target is not expected to be in the log_map");
827 for(
const auto &it : log_map)
833 PRECONDITION(start->location_number <= end->location_number);
844 {
"originalSegment", std::move(json_orig)},
845 {
"inlinedSegment", std::move(json_new)}};
847 json_inlined.
push_back(std::move(
object));
850 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)
Inline all of the chosen calls in a given function.
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().
bool body_available() const
Function Inlining This is a class that encapsulates the state and functionality needed to do inline m...
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 body (see body) and parameter identifiers (see parameter_iden...
std::vector< exprt > operandst
json_arrayt & make_array()
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.
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)
Inlines a single function call Calls out to goto_inline_transitive or goto_inline_nontransitive.
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
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
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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
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)