cprover
|
#include <goto_convert_class.h>
Classes | |
struct | break_continue_targetst |
struct | break_switch_targetst |
struct | leave_targett |
struct | targetst |
struct | throw_targett |
Public Member Functions | |
void | goto_convert (const codet &code, goto_programt &dest, const irep_idt &mode) |
goto_convertt (symbol_table_baset &_symbol_table, message_handlert &_message_handler) | |
virtual | ~goto_convertt () |
Protected Types | |
typedef std::map< irep_idt, std::pair< goto_programt::targett, node_indext > > | labelst |
typedef std::list< std::pair< goto_programt::targett, node_indext > > | 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 |
Protected Member Functions | |
void | goto_convert_rec (const codet &code, goto_programt &dest, const irep_idt &mode) |
symbolt & | new_tmp_symbol (const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode) |
symbol_exprt | make_compound_literal (const exprt &expr, goto_programt &dest, const irep_idt &mode) |
void | clean_expr (exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true) |
void | clean_expr_address_of (exprt &expr, goto_programt &dest, const irep_idt &mode) |
void | make_temp_symbol (exprt &expr, const std::string &suffix, goto_programt &, const irep_idt &mode) |
void | rewrite_boolean (exprt &dest) |
re-write boolean operators into ?: More... | |
void | remove_side_effect (side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used, bool address_taken) |
void | remove_assignment (side_effect_exprt &expr, goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode) |
void | remove_pre (side_effect_exprt &expr, goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode) |
void | remove_post (side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used) |
void | remove_function_call (side_effect_expr_function_callt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used) |
void | remove_cpp_new (side_effect_exprt &expr, goto_programt &dest, bool result_is_used) |
void | remove_cpp_delete (side_effect_exprt &expr, goto_programt &dest) |
void | remove_malloc (side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used) |
void | remove_temporary_object (side_effect_exprt &expr, goto_programt &dest) |
void | remove_statement_expression (side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used) |
void | remove_gcc_conditional_expression (exprt &expr, goto_programt &dest, const irep_idt &mode) |
virtual void | do_cpp_new (const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest) |
void | do_java_new (const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest) |
void | do_java_new_array (const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest) |
void | cpp_new_initializer (const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest) |
builds a goto program for object initialization after new More... | |
virtual void | do_function_call (const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode) |
virtual void | do_function_call_if (const exprt &lhs, const if_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode) |
virtual void | do_function_call_symbol (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest) |
add function calls to function queue for later processing More... | |
virtual void | do_function_call_symbol (const symbolt &) |
virtual void | do_function_call_other (const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest) |
void | convert_block (const code_blockt &code, goto_programt &dest, const irep_idt &mode) |
void | convert_decl (const code_declt &code, goto_programt &dest, const irep_idt &mode) |
void | convert_decl_type (const codet &code, goto_programt &dest) |
void | convert_expression (const code_expressiont &code, goto_programt &dest, const irep_idt &mode) |
void | convert_assign (const code_assignt &code, goto_programt &dest, const irep_idt &mode) |
void | convert_cpp_delete (const codet &code, goto_programt &dest) |
void | convert_loop_invariant (const codet &code, goto_programt::targett loop, const irep_idt &mode) |
void | convert_for (const code_fort &code, goto_programt &dest, const irep_idt &mode) |
void | convert_while (const code_whilet &code, goto_programt &dest, const irep_idt &mode) |
void | convert_dowhile (const code_dowhilet &code, goto_programt &dest, const irep_idt &mode) |
void | convert_assume (const code_assumet &code, goto_programt &dest, const irep_idt &mode) |
void | convert_assert (const code_assertt &code, goto_programt &dest, const irep_idt &mode) |
void | convert_switch (const code_switcht &code, goto_programt &dest, const irep_idt &mode) |
void | convert_break (const code_breakt &code, goto_programt &dest, const irep_idt &mode) |
void | convert_return (const code_returnt &code, goto_programt &dest, const irep_idt &mode) |
void | convert_continue (const code_continuet &code, goto_programt &dest, const irep_idt &mode) |
void | convert_ifthenelse (const code_ifthenelset &code, goto_programt &dest, const irep_idt &mode) |
void | convert_goto (const code_gotot &code, goto_programt &dest) |
void | convert_gcc_computed_goto (const codet &code, goto_programt &dest) |
void | convert_skip (const codet &code, goto_programt &dest) |
void | convert_label (const code_labelt &code, goto_programt &dest, const irep_idt &mode) |
void | convert_gcc_local_label (const codet &code, goto_programt &dest) |
void | convert_switch_case (const code_switch_caset &code, goto_programt &dest, const irep_idt &mode) |
void | convert_gcc_switch_case_range (const code_gcc_switch_case_ranget &, goto_programt &dest, const irep_idt &mode) |
void | convert_function_call (const code_function_callt &code, goto_programt &dest, const irep_idt &mode) |
void | convert_start_thread (const codet &code, goto_programt &dest) |
void | convert_end_thread (const codet &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_msc_try_finally (const codet &code, goto_programt &dest, const irep_idt &mode) |
void | convert_msc_try_except (const codet &code, goto_programt &dest, const irep_idt &mode) |
void | convert_msc_leave (const codet &code, goto_programt &dest, const irep_idt &mode) |
void | convert_try_catch (const codet &code, goto_programt &dest, const irep_idt &mode) |
void | convert_CPROVER_try_catch (const codet &code, goto_programt &dest, const irep_idt &mode) |
void | convert_CPROVER_try_finally (const codet &code, goto_programt &dest, const irep_idt &mode) |
void | convert_CPROVER_throw (const codet &code, goto_programt &dest, const irep_idt &mode) |
void | convert_asm (const code_asmt &code, goto_programt &dest) |
void | convert (const codet &code, goto_programt &dest, const irep_idt &mode) |
converts 'code' and appends the result to 'dest' More... | |
void | copy (const codet &code, goto_program_instruction_typet type, goto_programt &dest) |
symbol_exprt | exception_flag (const irep_idt &mode) |
void | unwind_destructor_stack (const source_locationt &source_location, goto_programt &dest, const irep_idt &mode, optionalt< node_indext > destructor_start_point={}, optionalt< node_indext > destructor_end_point={}) |
Unwinds the destructor stack and creates destructors for each node between destructor_start_point and destructor_end_point (including the start, excluding the end). More... | |
void | finish_gotos (goto_programt &dest, const irep_idt &mode) |
void | finish_computed_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. More... | |
exprt | case_guard (const exprt &value, const caset &case_op) |
void | generate_ifthenelse (const exprt &cond, goto_programt &true_case, goto_programt &false_case, const source_locationt &, goto_programt &dest, const irep_idt &mode) |
if(guard) true_case; else false_case; More... | |
void | generate_conditional_branch (const exprt &guard, goto_programt::targett target_true, goto_programt::targett target_false, const source_locationt &, goto_programt &dest, const irep_idt &mode) |
if(guard) goto target_true; else goto target_false; More... | |
void | generate_conditional_branch (const exprt &guard, goto_programt::targett target_true, const source_locationt &, goto_programt &dest, const irep_idt &mode) |
void | generate_thread_block (const code_blockt &thread_body, goto_programt &dest, const irep_idt &mode) |
Generates the necessary goto-instructions to represent a thread-block. More... | |
irep_idt | get_string_constant (const exprt &expr) |
bool | get_string_constant (const exprt &expr, irep_idt &) |
exprt | get_constant (const exprt &expr) |
void | do_enum_is_in_range (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest) |
Converts calls to the built in enum_is_in_range function to a test that the given enum value is in the valid range of values for that enum type. More... | |
void | do_atomic_begin (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest) |
void | do_atomic_end (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest) |
void | do_create_thread (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest) |
void | do_array_equal (const exprt &lhs, const symbol_exprt &rhs, const exprt::operandst &arguments, goto_programt &dest) |
void | do_array_op (const irep_idt &id, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest) |
void | do_printf (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest) |
void | do_scanf (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest) |
void | do_input (const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest) |
void | do_output (const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest) |
void | do_prob_coin (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest) |
void | do_prob_uniform (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest) |
exprt | get_array_argument (const exprt &src) |
Static Protected Member Functions | |
static bool | needs_cleaning (const exprt &expr) |
static bool | has_sideeffect (const exprt &expr) |
static bool | has_function_call (const exprt &expr) |
static void | replace_new_object (const exprt &object, exprt &dest) |
static void | collect_operands (const exprt &expr, const irep_idt &id, std::list< exprt > &dest) |
Protected Attributes | |
symbol_table_baset & | symbol_table |
namespacet | ns |
std::string | tmp_symbol_prefix |
lifetimet | lifetime = lifetimet::STATIC_GLOBAL |
struct goto_convertt::targetst | targets |
Additional Inherited Members |
Definition at line 28 of file goto_convert_class.h.
|
protected |
Definition at line 365 of file goto_convert_class.h.
|
protected |
Definition at line 364 of file goto_convert_class.h.
|
protected |
Definition at line 363 of file goto_convert_class.h.
|
protected |
Definition at line 362 of file goto_convert_class.h.
|
protected |
Definition at line 361 of file goto_convert_class.h.
|
protected |
Definition at line 359 of file goto_convert_class.h.
|
inline |
Definition at line 34 of file goto_convert_class.h.
|
inlinevirtual |
Definition at line 44 of file goto_convert_class.h.
Definition at line 1100 of file goto_convert.cpp.
|
protected |
Definition at line 162 of file goto_clean_expr.cpp.
|
protected |
Definition at line 434 of file goto_clean_expr.cpp.
|
staticprotected |
Definition at line 1440 of file goto_convert.cpp.
|
protected |
converts 'code' and appends the result to 'dest'
Definition at line 429 of file goto_convert.cpp.
|
protected |
Definition at line 14 of file goto_asm.cpp.
|
protected |
Definition at line 825 of file goto_convert.cpp.
|
protected |
Definition at line 680 of file goto_convert.cpp.
|
protected |
Definition at line 848 of file goto_convert.cpp.
|
protected |
Definition at line 1370 of file goto_convert.cpp.
|
protected |
Definition at line 1382 of file goto_convert.cpp.
|
protected |
Definition at line 542 of file goto_convert.cpp.
|
protected |
Definition at line 1229 of file goto_convert.cpp.
|
protected |
Definition at line 1305 of file goto_convert.cpp.
|
protected |
Definition at line 763 of file goto_convert.cpp.
|
protected |
Definition at line 180 of file goto_convert_exceptions.cpp.
|
protected |
Definition at line 144 of file goto_convert_exceptions.cpp.
|
protected |
Definition at line 211 of file goto_convert_exceptions.cpp.
|
protected |
Definition at line 609 of file goto_convert.cpp.
|
protected |
Definition at line 673 of file goto_convert.cpp.
|
protected |
Definition at line 1031 of file goto_convert.cpp.
|
protected |
Definition at line 1358 of file goto_convert.cpp.
|
protected |
Definition at line 572 of file goto_convert.cpp.
|
protected |
Definition at line 883 of file goto_convert.cpp.
|
protected |
Definition at line 24 of file goto_convert_function_call.cpp.
|
protected |
Definition at line 1334 of file goto_convert.cpp.
|
protected |
Definition at line 349 of file goto_convert.cpp.
|
protected |
Definition at line 388 of file goto_convert.cpp.
|
protected |
Definition at line 1324 of file goto_convert.cpp.
|
protected |
Definition at line 1394 of file goto_convert.cpp.
|
protected |
Definition at line 308 of file goto_convert.cpp.
|
protected |
Definition at line 860 of file goto_convert.cpp.
|
protected |
Definition at line 69 of file goto_convert_exceptions.cpp.
|
protected |
Definition at line 54 of file goto_convert_exceptions.cpp.
|
protected |
Definition at line 16 of file goto_convert_exceptions.cpp.
|
protected |
Definition at line 1246 of file goto_convert.cpp.
|
protected |
Definition at line 840 of file goto_convert.cpp.
|
protected |
Definition at line 1346 of file goto_convert.cpp.
|
protected |
Definition at line 1129 of file goto_convert.cpp.
|
protected |
Definition at line 356 of file goto_convert.cpp.
|
protected |
Definition at line 85 of file goto_convert_exceptions.cpp.
|
protected |
Definition at line 975 of file goto_convert.cpp.
|
protected |
Definition at line 299 of file goto_convert.cpp.
|
protected |
builds a goto program for object initialization after new
Definition at line 507 of file builtin_functions.cpp.
|
protected |
|
protected |
Definition at line 567 of file builtin_functions.cpp.
|
protected |
Definition at line 342 of file builtin_functions.cpp.
|
protected |
Definition at line 365 of file builtin_functions.cpp.
|
protectedvirtual |
Definition at line 388 of file builtin_functions.cpp.
|
protected |
|
protected |
Converts calls to the built in enum_is_in_range
function to a test that the given enum value is in the valid range of values for that enum type.
Note that the check for the range of values is done by creating a disjunction comparing the expression with each possible valid value.
lhs | The destination for the generated assignment. |
function | The enum_is_in_range symbol of the source function call. |
arguments | A collection of arguments, which is expected to contain a single argument which is an expression that resolves to a value of enum type. The arguments are expected to have been prevalidated by the typechecking process. |
dest | The goto program into which the generated assignment is copied. |
Definition at line 614 of file builtin_functions.cpp.
|
protectedvirtual |
Definition at line 37 of file goto_convert_function_call.cpp.
|
protectedvirtual |
Definition at line 89 of file goto_convert_function_call.cpp.
|
protectedvirtual |
Definition at line 152 of file goto_convert_function_call.cpp.
|
protectedvirtual |
add function calls to function queue for later processing
Definition at line 641 of file builtin_functions.cpp.
|
inlineprotectedvirtual |
Definition at line 202 of file goto_convert_class.h.
|
protected |
Definition at line 312 of file builtin_functions.cpp.
|
protected |
|
protected |
|
protected |
Definition at line 327 of file builtin_functions.cpp.
|
protected |
Definition at line 196 of file builtin_functions.cpp.
|
protected |
Definition at line 110 of file builtin_functions.cpp.
|
protected |
Definition at line 32 of file builtin_functions.cpp.
|
protected |
Definition at line 210 of file builtin_functions.cpp.
|
protected |
Definition at line 235 of file goto_convert_exceptions.cpp.
|
protected |
Definition at line 202 of file goto_convert.cpp.
|
protected |
Definition at line 109 of file goto_convert.cpp.
|
protected |
Definition at line 1624 of file goto_convert.cpp.
|
protected |
if(guard) goto target_true; else goto target_false;
Definition at line 1658 of file goto_convert.cpp.
|
protected |
if(guard) true_case; else false_case;
Definition at line 1467 of file goto_convert.cpp.
|
protected |
Generates the necessary goto-instructions to represent a thread-block.
Specifically, the following instructions are generated:
A: START_THREAD : C B: GOTO Z C: SKIP D: {THREAD BODY} E: END_THREAD Z: SKIP
thread_body | Sequence of codet's that can be executed in parallel | |
[out] | dest | Resulting goto-instructions |
mode | Language mode |
Definition at line 1908 of file goto_convert.cpp.
Definition at line 534 of file builtin_functions.cpp.
Definition at line 1793 of file goto_convert.cpp.
Definition at line 1779 of file goto_convert.cpp.
Definition at line 1732 of file goto_convert.cpp.
void goto_convertt::goto_convert | ( | const codet & | code, |
goto_programt & | dest, | ||
const irep_idt & | mode | ||
) |
Definition at line 278 of file goto_convert.cpp.
|
protected |
Definition at line 286 of file goto_convert.cpp.
|
staticprotected |
Definition at line 24 of file goto_convert_side_effect.cpp.
|
staticprotected |
|
protected |
Definition at line 24 of file goto_clean_expr.cpp.
|
protected |
Definition at line 1842 of file goto_convert.cpp.
|
staticprotected |
Definition at line 66 of file goto_clean_expr.cpp.
|
protected |
Definition at line 1819 of file goto_convert.cpp.
|
protected |
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.
Definition at line 234 of file goto_convert.cpp.
|
protected |
Definition at line 37 of file goto_convert_side_effect.cpp.
|
protected |
Definition at line 437 of file goto_convert_side_effect.cpp.
|
protected |
Definition at line 410 of file goto_convert_side_effect.cpp.
|
protected |
Definition at line 344 of file goto_convert_side_effect.cpp.
|
protected |
Definition at line 503 of file goto_clean_expr.cpp.
|
protected |
Definition at line 453 of file goto_convert_side_effect.cpp.
|
protected |
Definition at line 263 of file goto_convert_side_effect.cpp.
|
protected |
Definition at line 180 of file goto_convert_side_effect.cpp.
|
protected |
Definition at line 591 of file goto_convert_side_effect.cpp.
|
protected |
Definition at line 522 of file goto_convert_side_effect.cpp.
|
protected |
Definition at line 486 of file goto_convert_side_effect.cpp.
Definition at line 399 of file goto_convert_side_effect.cpp.
|
protected |
re-write boolean operators into ?:
Definition at line 111 of file goto_clean_expr.cpp.
|
protected |
Unwinds the destructor stack and creates destructors for each node between destructor_start_point and destructor_end_point (including the start, excluding the end).
If end_index
isn't passed, it will unwind the whole stack. If start_index
isn't passed, it will unwind from the current node.
When destructors are non-trivial (i.e. if they contain DECL or GOTO statements) then unwinding becomes more complicated because when we call convert on the destructor code it may recursively invoke this function.
Say we have a tree of [3, 2, 1, 0] and we start unwinding from top to bottom. If node 1 has such a non-trivial destructor during the convert it will add nodes to the tree so it ends up looking like this:
3, 2, 1, 0 5, 4,/
If for example the destructor contained a THROW statement then it would unwind destroying variables 5, 4 and finally 0. Note that we don't have 1 here even if that was the instruction that triggered the recursive unwind because it's already been popped off before convert is called.
After our unwind has finished, we return to our [3, 2, 1, 0] branch and continue processing the branch for destructor 0.
Definition at line 283 of file goto_convert_exceptions.cpp.
|
protected |
Definition at line 52 of file goto_convert_class.h.
|
protected |
Definition at line 50 of file goto_convert_class.h.
|
protected |
Definition at line 49 of file goto_convert_class.h.
|
protected |
|
protected |
Definition at line 51 of file goto_convert_class.h.