44 exprt::operandst::const_iterator it1=arguments.begin();
50 for(
const auto ¶meter : parameter_types)
55 const irep_idt &identifier=parameter.get_identifier();
59 source_location.as_string() +
": no identifier for function parameter");
68 decl->source_location=source_location;
76 if(it1==arguments.end())
79 warning() <<
"call to `" << function_name <<
"': " 80 <<
"not enough arguments, " 81 <<
"inserting non-deterministic value" <<
eom;
102 if((f_partype.
id()==ID_pointer &&
103 f_acttype.
id()==ID_pointer) ||
104 (f_partype.
id()==ID_pointer &&
105 f_acttype.
id()==ID_array &&
110 else if((f_partype.
id()==ID_signedbv ||
111 f_partype.
id()==ID_unsignedbv ||
112 f_partype.
id()==ID_bool) &&
113 (f_acttype.
id()==ID_signedbv ||
114 f_acttype.
id()==ID_unsignedbv ||
115 f_acttype.
id()==ID_bool))
130 dest.
instructions.back().source_location=source_location;
136 if(it1!=arguments.end())
140 if(it1!=arguments.end())
161 for(
const auto ¶meter : parameter_types)
163 const irep_idt &identifier=parameter.get_identifier();
167 source_location.as_string() +
": no identifier for function parameter");
176 dead->source_location=source_location;
186 for(goto_programt::instructionst::iterator
195 if(it->code.operands().size()!=1)
198 warning() <<
"return expects one operand!\n" 199 << it->code.pretty() <<
eom;
207 if(code_assign.lhs().type()!=
208 code_assign.rhs().type())
211 it->code=code_assign;
216 else if(!it->code.operands().empty())
242 if(!property_class.
empty())
245 if(!property_id.
empty())
272 const irep_idt identifier=
function.get_identifier();
281 "final instruction of a function must be an END_FUNCTION");
286 instruction.function=target->function;
315 unsigned begin_location_number=t_it->location_number;
318 t_it->is_end_function(),
319 "final instruction of a function must be an END_FUNCTION");
320 unsigned end_location_number=t_it->location_number;
322 unsigned call_location_number=target->location_number;
326 begin_location_number,
328 call_location_number,
335 function.find_source_location();
343 if(it->function==identifier)
356 it->function=target->function;
365 target->code.clear();
374 const bool transitive,
375 const bool force_full,
383 std::cout <<
"Expanding call:\n";
391 get_call(target, lhs, function_expr, arguments);
393 if(function_expr.
id()!=ID_symbol)
398 const irep_idt identifier=
function.get_identifier();
409 warning() <<
"recursion is ignored on call to `" << identifier <<
"'" 418 goto_functionst::function_mapt::iterator f_it=
424 warning() <<
"missing function `" << identifier <<
"' is ignored" <<
eom;
454 progress() <<
"Inserting " << identifier <<
" into caller" <<
eom;
455 progress() <<
"Number of instructions: " 460 progress() <<
"Removing " << identifier <<
" from cache" <<
eom;
461 progress() <<
"Number of instructions: " 465 cache.erase(identifier);
492 warning() <<
"no body for function `" << identifier <<
"'" <<
eom;
508 function=call.function();
509 arguments=call.arguments();
514 const bool force_full)
520 const irep_idt identifier=f_it->first;
524 if(!goto_function.body_available())
527 goto_inline(identifier, goto_function, inline_map, force_full);
535 const bool force_full)
550 const bool force_full)
554 finished_sett::const_iterator f_it=
finished_set.find(identifier);
563 const inline_mapt::const_iterator im_it=inline_map.find(identifier);
565 if(im_it==inline_map.end())
570 if(call_list.empty())
575 for(
const auto &call : call_list)
577 const bool transitive=call.second;
601 const bool force_full)
605 cachet::const_iterator c_it=
cache.find(identifier);
607 if(c_it!=
cache.end())
612 "body of cached functions must be available");
618 cached.
body.
empty(),
"body of new function in cache must be empty");
620 progress() <<
"Creating copy of " << identifier <<
eom;
621 progress() <<
"Number of instructions: " 633 if(i_it->is_function_call())
634 call_list.push_back(i_it);
637 if(call_list.empty())
642 for(
const auto &call : call_list)
671 goto_functionst::function_mapt::const_iterator f_it=
676 inline_mapt::const_iterator im_it=inline_map.find(identifier);
678 if(im_it==inline_map.end())
683 if(call_list.empty())
688 for(
const auto &call : call_list)
694 if(target->function!=identifier)
701 target->location_number <= ln)
706 if(!target->is_function_call())
709 ln=target->location_number;
732 for(
const auto &it : inline_map)
737 out <<
"Function: " <<
id <<
"\n";
739 goto_functionst::function_mapt::const_iterator f_it=
742 std::string call=
"-";
750 "cannot inline function with empty body");
754 for(
const auto &call : call_list)
757 bool transitive=call.second;
761 out <<
" Transitive: " << transitive <<
"\n";
773 for(
auto it=
cache.begin(); it!=
cache.end(); it++)
775 if(it!=
cache.begin())
778 out << it->first <<
"\n";
793 for(
const auto &it : function_map)
800 cleanup(goto_function.
body);
806 const unsigned begin_location_number,
807 const unsigned end_location_number,
808 const unsigned call_location_number,
813 PRECONDITION(end_location_number >= begin_location_number);
817 log_map.find(start) == log_map.end(),
818 "inline function should be registered once in map of inline functions");
846 "'to' target function is not allowed to be empty");
848 it1->location_number == it2->location_number,
849 "both functions' instruction should point to the same source");
851 log_mapt::const_iterator l_it=log_map.find(it1);
852 if(l_it!=log_map.end())
856 log_map.find(it2) == log_map.end(),
857 "'to' target is not expected to be in the log_map");
884 for(
const auto &it : log_map)
892 PRECONDITION(start->location_number <= end->location_number);
908 return std::move(json_result);
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)
std::list< targett > targetst
goto_inline_logt inline_log
void set_property_class(const irep_idt &property_class)
mstreamt & progress() const
std::string comment(const rw_set_baset::entryt &entry, bool write)
goto_program_instruction_typet type
What kind of instruction?
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
bool is_ignored(const irep_idt id) const
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Deprecated expression utility functions.
void set_comment(const irep_idt &comment)
void cleanup(const goto_programt &goto_program)
std::vector< parametert > parameterst
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
function_mapt function_map
typet & type()
Return the type of the expression.
void replace_return(goto_programt &body, const exprt &lhs)
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
static const unsigned nil_target
Uniquely identify an invalid target or location.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
codet representation of an expression statement.
json_arrayt & make_array()
void set_property_id(const irep_idt &property_id)
void parameter_destruction(const goto_programt::targett target, const irep_idt &function_name, const code_typet &code_type, goto_programt &dest)
mstreamt & warning() const
This class represents an instruction in the GOTO intermediate representation.
jsont & push_back(const jsont &json)
bool is_end_function() const
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
void goto_inline(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full=false)
std::map< irep_idt, call_listt > inline_mapt
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
jsont output_inline_log_json() const
instructionst::iterator targett
A codet representing the declaration of a local variable.
recursion_sett recursion_set
source_locationt source_location
instructionst instructions
The list of instructions in the goto program.
API to expression classes.
instructionst::const_iterator const_targett
void expand_function_call(goto_programt &dest, const inline_mapt &inline_map, const bool transitive, const bool force_full, goto_programt::targett target)
#define PRECONDITION(CONDITION)
A side_effect_exprt that returns a non-deterministically chosen value.
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
codet representation of a function call statement.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
bool check_inline_map(const inline_mapt &inline_map) const
std::map< irep_idt, goto_functiont > function_mapt
void copy_from(const goto_functiont &other)
unsigned call_location_number
code_typet type
The type of the function, indicating the return type and parameter types.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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)
goto_programt::const_targett end
const goto_functiont & goto_inline_transitive(const irep_idt identifier, const goto_functiont &goto_function, const bool force_full)
static void get_call(goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments)
std::vector< exprt > operandst
A goto function, consisting of function type (see type), function body (see body),...
const bool adjust_function
A generic container class for the GOTO intermediate representation of one function.
goto_functionst & goto_functions
finished_sett finished_set
void output_cache(std::ostream &out) const
bool body_available() const
unsigned end_location_number
void parameter_assignments(const goto_programt::targett target, const irep_idt &function_name, const code_typet &code_type, const exprt::operandst &arguments, goto_programt &dest)
targett add_instruction()
Adds an instruction at the end.
Base class for all expressions.
const parameterst & parameters() const
#define Forall_goto_functions(it, functions)
bool empty() const
Is the program empty?
#define UNREACHABLE
This should be used to mark dead code.
void replace_location(source_locationt &dest, const source_locationt &new_location)
void copy_from(const goto_programt &from, const goto_programt &to)
A codet representing the removal of a local variable going out of scope.
#define Forall_operands(it, expr)
source_locationt & add_source_location()
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
const char * c_str() const
unsigned begin_location_number
json_objectt & make_object()
const irep_idt & get_comment() const
void goto_inline_nontransitive(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full)
goto_functionst::goto_functiont goto_functiont
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define forall_goto_functions(it, functions)
const irep_idt & get_property_id() const
const irep_idt & get_property_class() const
#define forall_goto_program_instructions(it, program)
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
const irept & find(const irep_namet &name) const
void output_inline_map(std::ostream &out, const inline_mapt &inline_map)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
A codet representing an assignment in the program.
const code_function_callt & to_code_function_call(const codet &code)