ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
goto_convert_functionst Class Reference

#include <goto_convert_functions.h>

Inheritance diagram for goto_convert_functionst:
[legend]

Public Types

typedef std::map< irep_idt, std::set< irep_idt > > typename_mapt
typedef std::set< irep_idt > typename_sett

Public Member Functions

void goto_convert ()
void convert_function (symbolt &symbol)
void thrash_type_symbols ()
void collect_type (const irept &type, typename_sett &set)
void collect_expr (const irept &expr, typename_sett &set)
void rename_types (irept &type, const symbolt &cur_name_sym, const irep_idt &sname)
void rename_exprs (irept &expr, const symbolt &cur_name_sym, const irep_idt &sname)
bool type_needs_rename (const irept &type, const irep_idt &sname) const
bool expr_needs_rename (const irept &expr, const irep_idt &sname) const
void wallop_type (irep_idt name, typename_mapt &typenames, const irep_idt &sname)
 goto_convert_functionst (contextt &_context, optionst &_options, goto_functionst &_functions)
Public Member Functions inherited from goto_convertt
void goto_convert (const codet &code, goto_programt &dest)
 goto_convertt (contextt &_context, optionst &_options)

Protected Member Functions

void add_return (goto_functiont &f, const irep_idt &identifier, const locationt &location)
bool try_convert_body_native (const expr2tc &body2, goto_programt &dest)
bool convert_native_rec (const expr2tc &code2, goto_programt &dest, const locationt &inherited)
bool convert_native_full_expression (const expr2tc &code2, goto_programt &dest, const locationt &inherited)
void wallop_type_impl (irep_idt name, typename_mapt &typenames, const irep_idt &sname, std::set< irep_idt > &in_progress)
Protected Member Functions inherited from goto_convertt
void goto_convert_rec (const codet &code, goto_programt &dest)
void new_name (symbolt &symbol)
symbolt & new_tmp_symbol (const typet &type)
symbolt & new_cftest_symbol (const typet &type)
void make_temp_symbol (exprt &expr, goto_programt &dest)
void guard_program (const guard2tc &guard, goto_programt &dest)
void remove_sideeffects (exprt &expr, goto_programt &dest, bool result_is_used=true)
void remove_sideeffects (expr2tc &expr, goto_programt &dest, bool result_is_used=true)
void remove_condition_sideeffects (exprt &cond, goto_programt &dest)
 Lowers the condition of an if, loop, for or switch statement, a full-expression whose temporaries are destroyed before the branch ([class.temporary]/4).
void flatten_contract_clause (exprt &clause, goto_programt &dest)
 Recursively flatten a (possibly nested) &&/|| tree forming a contract clause, hoisting side effects (e.g.
void address_of_replace_objects (exprt &expr, goto_programt &dest)
bool rewrite_vla_decl (typet &var_type, goto_programt &dest)
bool rewrite_vla_decl_size (exprt &size, goto_programt &dest)
void generate_dynamic_size_vla (exprt &var, const locationt &loc, goto_programt &dest, bool allow_zero_size=false)
bool has_sideeffect (const exprt &expr)
bool has_sideeffect (const expr2tc &expr)
bool has_destructible_sideeffect (const exprt &expr)
 True if lowering expr may create a temporary with a destructor.
bool splits_and_condition (const exprt &cond)
void remove_sideeffects_for_quantifier_body (exprt &body, const std::set< irep_idt > &bound_vars, goto_programt &dest)
void inline_calls_in_quantifier_body (exprt &expr, unsigned depth)
 Inline calls to pure single-return functions occurring under a quantifier binder, so that the bound variable stays visible in the body for replace_name_in_body() in smt_solver.cpp.
bool try_inline_pure_call (const symbolt &fsym, const exprt &call, exprt &out)
 Build the inlined form of call to fsym: the callee's body must be local declarations with initializers followed by a single return <expr>;.
bool summarize_pure_call (const symbolt &fsym, const exprt &call, exprt &out)
const exprt * find_sideeffect_on_bound_var (const exprt &expr, const std::set< irep_idt > &bound_vars)
 Find a side effect that mentions one of bound_vars.
void skolemize_asserted_foralls (exprt &expr, goto_programt &dest)
 In an assertion, a __ESBMC_forall in positive polarity is equivalent to its body over a fresh unconstrained variable: assert(forall x.
void convert_quantifier_calls (exprt &expr)
void remove_assignment (exprt &expr, goto_programt &dest, bool result_is_used)
void remove_post (exprt &expr, goto_programt &dest, bool result_is_used)
void remove_pre (exprt &expr, goto_programt &dest, bool result_is_used)
void remove_function_call (exprt &expr, goto_programt &dest, bool result_is_used)
void remove_cpp_new (exprt &expr, goto_programt &dest, bool result_is_used)
void remove_cpp_delete (exprt &expr, goto_programt &dest)
void remove_operand_sideeffects (exprt &expr, goto_programt &dest)
 Remove the side effects of expr's operands.
void drop_destructor (const symbol_exprt &object, std::size_t from)
 Unschedule the destructor call on object among the scope-exit entries pushed since the stack held from of them.
void remove_temporary_object (exprt &expr, goto_programt &dest)
void remove_statement_expression (exprt &expr, goto_programt &dest, bool result_is_used)
void remove_gcc_conditional_expression (exprt &expr, goto_programt &dest)
virtual void do_cpp_new (const exprt &lhs, const exprt &rhs, goto_programt &dest)
void cpp_new_at (const exprt &lhs, const exprt &placement, const locationt &location, goto_programt &dest)
void cpp_new_initializer (const exprt &lhs, const exprt &rhs, const exprt &elem_count, goto_programt &dest)
void cpp_new_zero_fill (const exprt &lhs, const exprt &rhs, const exprt &elem_count, goto_programt &dest)
void cpp_new_store_element (const exprt &base, const exprt &offset, const exprt &init, const locationt &location, const exprt &built, code_blockt &out)
bool cpp_new_init_list (const exprt &lhs, const exprt &rhs, const exprt &init, const exprt &elem_count, const exprt &built, code_blockt &out)
void convert_cpp_new_elements (const exprt &base, const exprt &built, const codet &construction, goto_programt &dest)
bool user_code_throws ()
virtual void do_function_call (const exprt &lhs, const exprt &function, const exprt::operandst &arguments, const locationt &location, goto_programt &dest)
virtual void do_function_call_if (const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest)
bool drop_inactive_contract_clause (bool is_clause) const
 True when a contract clause should be dropped: no contract mode is active, so the clause states nothing.
virtual void do_function_call_symbol (const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest)
virtual void do_function_call_dereference (const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest)
void convert_block (const codet &code, goto_programt &dest)
void convert_controlled (const codet &code, goto_programt &dest)
void convert_decl (const codet &code, goto_programt &dest)
void discard_comma_operands (exprt &initializer, goto_programt &dest)
 A comma's left operands are discarded-value expressions and its right operand is its result ([expr.comma]/1), so that operand initialises the variable: a class prvalue there is the variable, not a copied temporary.
void remove_comma_operand (exprt &operand, goto_programt &dest)
 A comma's operand is a discarded-value expression ([expr.comma]/1), but a temporary object it creates lives until the end of the enclosing full-expression ([class.temporary]/4).
void destroy_comma_operand_temporaries (std::size_t stack_size, const locationt &location, goto_programt &dest)
 A reference declaration keeps its initializer's temporaries to the end of the scope, but those of a discarded comma operand still die with it.
void convert_decl_initializer (const exprt &var, exprt &initializer, const codet &new_code, const symbolt &s, goto_programt &dest)
 Lower the initializer of a declaration into dest.
bool construct_in_place (const exprt &object, const exprt &initializer, goto_programt &dest)
 Construct object from initializer directly when it is a class temporary: a constructor call retargeted at object, or a call returning by value made with object as its lhs.
void remove_initializer_sideeffects (const exprt &object, exprt &initializer, goto_programt &dest)
 Remove the side effects of initializer, the value of object.
void convert_dynamic_static_init (const codet &decl, const symbolt &s, const symbolt &guard, goto_programt &dest)
 A C++ function-local static with a dynamic initializer is initialized the first time control passes its declaration, and concurrent callers wait for it ([stmt.dcl]/3): atomic { if (!guard) { init; guard = 1; } }.
void construct_array_elements (const exprt &base, const typet &type, const side_effect_expr_function_callt &ctor, goto_programt &dest)
 The frontend gives an array of a class one constructor call; every element is constructed by it, in increasing index order ([dcl.init]/7).
void schedule_array_element_destructors (const exprt &base, const typet &type)
 Push a destructor call for every element of an array of class objects, recursing through nested array types so a multi-dimensional array reaches its leaves.
void convert_decl_block (const codet &code, goto_programt &dest)
void convert_expression (const codet &code, goto_programt &dest)
void convert_assign (const code_assignt &code, goto_programt &dest)
void convert_assign_atomic (const exprt &lhs, const exprt &rhs, const locationt &location, goto_programt &dest)
void convert_assign_rmw_atomic (const exprt &lhs, const exprt &rhs, const locationt &location, goto_programt &dest)
void convert_cpp_delete (const codet &code, goto_programt &dest)
void convert_for (const codet &code, goto_programt &dest)
void convert_while (const codet &code, goto_programt &dest)
void convert_dowhile (const codet &code, goto_programt &dest)
void convert_assume (const codet &code, goto_programt &dest)
void convert_assert (const codet &code, goto_programt &dest)
bool emits_assert (const locationt &location) const
void assume_if_ends_path (const expr2tc &guard, const locationt &location, goto_programt &dest)
void convert_switch (const codet &code, goto_programt &dest)
void convert_break (const code_breakt &code, goto_programt &dest)
void convert_return (const code_returnt &code, goto_programt &dest)
void remove_return_value_sideeffects (exprt &value, goto_programt &dest)
void convert_continue (const code_continuet &code, goto_programt &dest)
void convert_ifthenelse (const codet &code, goto_programt &dest)
void convert_init (const codet &code, goto_programt &dest)
void convert_goto (const codet &code, goto_programt &dest)
void convert_skip (const codet &code, goto_programt &dest)
void convert_non_deterministic_goto (const codet &code, goto_programt &dest)
void convert_label (const code_labelt &code, goto_programt &dest)
void convert_switch_case (const code_switch_caset &code, goto_programt &dest)
void convert_function_call (const code_function_callt &code, goto_programt &dest)
void convert_atomic_begin (const codet &code, goto_programt &dest)
void convert_atomic_end (const codet &code, goto_programt &dest)
void convert (const codet &code, goto_programt &dest)
void copy (const codet &code, goto_program_instruction_typet type, goto_programt &dest)
void convert_full_expression (const codet &code, goto_programt &dest)
 Converts a statement that is a full-expression ([class.temporary]/4), so the temporaries it creates are destroyed when it ends.
bool destroy_full_expression_temporaries (std::size_t stack_size, const locationt &, goto_programt &dest)
 Emits the scope-exit entries pushed above stack_size when one of them is a destructor call, as the temporaries of a full-expression; plain DEADs of C temporaries keep block scope.
std::size_t keep_reference_member_temporaries (const exprt &initializer, std::size_t stack_size)
 A temporary bound to a reference member of a declared aggregate lives as long as the aggregate ([class.temporary]/6).
void unwind_destructor_stack (const locationt &, std::size_t stack_size, goto_programt &dest)
void unwind_destructor_stack (const locationt &, std::size_t stack_size, goto_programt &dest, destructor_stackt &stack)
void declare_skipped_locals (const destructor_stackt &stack, std::size_t from, const locationt &location, goto_programt &dest)
 Declares the locals stack holds past its first from entries: a jump to where stack is live skips their declarations.
goto_programt::targett case_entry (goto_programt::targett target, std::size_t switch_stack_size, const locationt &location, goto_programt &stubs)
 Where a switch dispatch jumps to reach target: the target itself, or a stub in stubs that first declares the locals the jump skips.
void kill_condition_temporaries (std::size_t stack_size, const locationt &location, goto_programt &branch, goto_programt &exit)
 End a loop condition's temporaries, pushed since stack_size, on both edges of its branch, so each iteration's instance dies in that iteration (#9150): after branch, and ahead of the break target that starts exit, where the branch's jumps to it now land.
void guard_arm_destructors (exprt &cond, std::size_t true_size, std::size_t false_size, const locationt &location, goto_programt &dest)
void record_exception_unwind (goto_programt::instructiont &call)
 Attach to call the cleanup an exception leaving it runs: the automatic objects constructed since the nearest enclosing try, newest first ([except.ctor]/1), as convert_throw unwinds for a throw in this function.
void convert_catch (const codet &code, goto_programt &dest)
void convert_throw (const exprt &expr, goto_programt &dest)
void finish_gotos (goto_programt &dest)
void optimize_guarded_gotos (goto_programt &dest)
 Rewrite "if(x) goto z; goto y; z:" into "if(!x) goto y;" This only works if the "goto y" is not a branch target.
void case_guard (const exprt &value, const caset &case_op, exprt &dest)
void generate_ifthenelse (const exprt &cond, goto_programt &true_case, goto_programt &false_case, const locationt &location, goto_programt &dest)
 if(guard) true_case; else false_case;
void generate_conditional_branch (const exprt &guard, goto_programt::targett target_true, goto_programt::targett target_false, const locationt &location, goto_programt &dest)
void generate_conditional_branch (const exprt &guard, goto_programt::targett target_true, const locationt &location, goto_programt &dest)
void emit_assert_fail_noreturn (const locationt &location, goto_programt &dest)
bool lower_discarded_short_circuit (exprt &expr, goto_programt &dest, bool result_is_used)
 Lower a value-discarding A && B as if (A) B;, A || B as if (!A) B;.
void rewrite_short_circuit_as_ternary (exprt &expr)
 Rebuild A && B as A ?
void do_assert_fail (const exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &base_name, std::size_t arity, std::size_t expr_arg)
void do_abort (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void do_atomic_begin (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void do_atomic_end (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void do_create_thread (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void do_malloc (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void do_realloc (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void do_alloca (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void do_free (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void do_sync (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void do_exit (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void do_printf (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest, const std::string &bs_name)
void do_operator_new (const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest)
 Lower a call to ::operator new(n) into a cpp_new side effect.
void do_mem (bool is_malloc, const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void get_alloc_size (typet &alloc_type, exprt &alloc_size)

Static Protected Member Functions

static bool hide (const goto_programt &goto_program)
Static Protected Member Functions inherited from goto_convertt
static void replace_new_object (const exprt &object, exprt &dest)
static bool is_destructor_entry (const codet &entry)
 A destructor call on the destructor stack, possibly guarded by guard_arm_destructors; the other entries are DEADs.
static exprt case_label (const exprt &lo, const exprt &hi)
static void collect_operands (const exprt &expr, const irep_idt &id, std::list< exprt > &dest)

Protected Attributes

goto_functionst & functions
Protected Attributes inherited from goto_convertt
contextt & context
optionst & options
namespacet ns
symbol_generator tmp_symbol
bool in_short_circuit = false
std::map< std::string, std::string > summary_reject_reasons
std::optional< bool > user_code_throws_cache
std::set< irep_idt > comma_operand_temporaries
 Temporaries created by a comma's discarded operands.
struct goto_convertt::targetst targets

Additional Inherited Members

Static Public Member Functions inherited from goto_convertt
static bool is_atomic_symbol (const exprt &expr, const namespacet &ns)
 Returns true iff expr is a direct reference to a C11 _Atomic variable.
static bool has_atomic_read (const exprt &expr, const namespacet &ns)
 Returns true iff expr contains a direct read of any C11 _Atomic variable (does not recurse into address_of).
Protected Types inherited from goto_convertt
typedef std::vector< codet > destructor_stackt
typedef std::map< irep_idt, std::pair< goto_programt::targett, destructor_stackt > > labelst
typedef std::list< std::pair< goto_programt::targett, destructor_stackt > > gotost
typedef std::list< goto_programt::targett > computed_gotost
typedef exprt::operandst caset
typedef std::list< std::pair< goto_programt::targett, caset > > casest
typedef std::map< goto_programt::targett, casest::iterator > cases_mapt
typedef std::map< goto_programt::targett, destructor_stackt > case_stackst

Member Typedef Documentation

◆ typename_mapt

typedef std::map<irep_idt, std::set<irep_idt> > goto_convert_functionst::typename_mapt

◆ typename_sett

typedef std::set<irep_idt> goto_convert_functionst::typename_sett

Constructor & Destructor Documentation

◆ goto_convert_functionst()

goto_convert_functionst::goto_convert_functionst ( contextt & _context,
optionst & _options,
goto_functionst & _functions )

Member Function Documentation

◆ add_return()

void goto_convert_functionst::add_return ( goto_functiont & f,
const irep_idt & identifier,
const locationt & location )
protected

◆ collect_expr()

void goto_convert_functionst::collect_expr ( const irept & expr,
typename_sett & set )

◆ collect_type()

void goto_convert_functionst::collect_type ( const irept & type,
typename_sett & set )

◆ convert_function()

void goto_convert_functionst::convert_function ( symbolt & symbol)

◆ convert_native_full_expression()

bool goto_convert_functionst::convert_native_full_expression ( const expr2tc & code2,
goto_programt & dest,
const locationt & inherited )
protected

◆ convert_native_rec()

bool goto_convert_functionst::convert_native_rec ( const expr2tc & code2,
goto_programt & dest,
const locationt & inherited )
protected

◆ expr_needs_rename()

bool goto_convert_functionst::expr_needs_rename ( const irept & expr,
const irep_idt & sname ) const

◆ goto_convert()

void goto_convert_functionst::goto_convert ( )

◆ hide()

bool goto_convert_functionst::hide ( const goto_programt & goto_program)
staticprotected

◆ rename_exprs()

void goto_convert_functionst::rename_exprs ( irept & expr,
const symbolt & cur_name_sym,
const irep_idt & sname )

◆ rename_types()

void goto_convert_functionst::rename_types ( irept & type,
const symbolt & cur_name_sym,
const irep_idt & sname )

◆ thrash_type_symbols()

void goto_convert_functionst::thrash_type_symbols ( )

◆ try_convert_body_native()

bool goto_convert_functionst::try_convert_body_native ( const expr2tc & body2,
goto_programt & dest )
protected

◆ type_needs_rename()

bool goto_convert_functionst::type_needs_rename ( const irept & type,
const irep_idt & sname ) const

◆ wallop_type()

void goto_convert_functionst::wallop_type ( irep_idt name,
typename_mapt & typenames,
const irep_idt & sname )

◆ wallop_type_impl()

void goto_convert_functionst::wallop_type_impl ( irep_idt name,
typename_mapt & typenames,
const irep_idt & sname,
std::set< irep_idt > & in_progress )
protected

Member Data Documentation

◆ functions

goto_functionst& goto_convert_functionst::functions
protected
The documentation for this class was generated from the following files: