Loading...

Searching...

No Matches

utils.h File Reference

#include <ansi-c/goto-conversion/goto_convert_class.h>
#include <goto-programs/loop_ids.h>
#include <goto-instrument/havoc_utils.h>
#include <goto-instrument/loop_utils.h>
#include <vector>

+ Include dependency graph for utils.h:

[フレーム]

+ This graph shows which files directly or indirectly include this file:

[フレーム]

Go to the source code of this file.

Classes

class cleanert

Class that allows to clean expressions of side effects and to generate havoc_slice expressions. More...

class havoc_if_validt

A class that overrides the low-level havocing functions in the base utility class, to havoc only when expressions point to valid memory, i.e. More...

class havoc_assigns_targetst

A class that further overrides the "safe" havoc utilities, and adds support for havocing pointer_object expressions. More...

struct replace_history_parametert

Macros

#define IN_BASE_CASE "__in_base_case"

#define ENTERED_LOOP "__entered_loop"

#define IN_LOOP_HAVOC_BLOCK "__in_loop_havoc_block"

#define INIT_INVARIANT "__init_invariant"

Typedefs

typedef std::map< loop_idt, exprt > invariant_mapt

Functions

exprt all_dereferences_are_valid (const exprt &expr, const namespacet &ns)

Generate a validity check over all dereferences in an expression.

exprt generate_lexicographic_less_than_check (const std::vector< symbol_exprt > &lhs, const std::vector< symbol_exprt > &rhs)

Generate a lexicographic less-than comparison over ordered tuples.

void insert_before_swap_and_advance (goto_programt &destination, goto_programt::targett &target, goto_programt &payload)

Insert a goto program before a target instruction iterator and advance the iterator.

void insert_before_and_update_jumps (goto_programt &destination, goto_programt::targett &target, const goto_programt::instructiont &i)

Insert a goto instruction before a target instruction iterator and update targets of all jumps that points to the iterator to jumping to the inserted instruction.

void simplify_gotos (goto_programt &goto_program, const namespacet &ns)

Turns goto instructions IF cond GOTO label where the condition statically simplifies to false into SKIP instructions.

bool is_loop_free (const goto_programt &goto_program, const namespacet &ns, messaget &log)

Returns true iff the given program is loop-free, i.e.

irep_idt make_assigns_clause_replacement_tracking_comment (const exprt &target, const irep_idt &function_id, const namespacet &ns)

Returns an irep_idt that essentially says that target was assigned by the contract of function_id.

bool is_assigns_clause_replacement_tracking_comment (const irep_idt &comment)

Returns true if the given comment matches the type of comments created by make_assigns_clause_replacement_tracking_comment.

void infer_loop_assigns (const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns)

Infer loop assigns using alias analysis result local_may_alias.

void widen_assigns (assignst &assigns, const namespacet &ns)

Widen expressions in assigns with the following strategy.

replace_history_parametert replace_history_old (symbol_table_baset &symbol_table, const exprt &expr, const source_locationt &location, const irep_idt &mode)

This function recursively identifies the "old" expressions within expr and replaces them with corresponding history variables.

replace_history_parametert replace_history_loop_entry (symbol_table_baset &symbol_table, const exprt &expr, const source_locationt &location, const irep_idt &mode)

This function recursively identifies the "loop_entry" expressions within expr and replaces them with corresponding history variables.

void generate_history_variables_initialization (symbol_table_baset &symbol_table, exprt &clause, const irep_idt &mode, goto_programt &program)

This function generates all the instructions required to initialize history variables.

bool is_transformed_loop_head (const goto_programt::const_targett &target)

Return true if target is the head of some transformed loop.

bool is_transformed_loop_end (const goto_programt::const_targett &target)

Return true if target is the end of some transformed loop.

bool is_assignment_to_instrumented_variable (const goto_programt::const_targett &target, std::string var_name)

Return true if target is an assignment to an instrumented variable with name var_name.

unsigned get_suffix_unsigned (const std::string &str, const std::string &prefix)

Convert the suffix digits right after prefix of str into unsigned.

goto_programt::targett get_loop_end_from_loop_head_and_content_mutable (const goto_programt::targett &loop_head, const loop_templatet< goto_programt::targett, goto_programt::target_less_than > &loop)

Find the goto instruction of loop that jumps to loop_head

goto_programt::const_targett get_loop_end_from_loop_head_and_content (const goto_programt::const_targett &loop_head, const loop_templatet< goto_programt::const_targett, goto_programt::target_less_than > &loop)

goto_programt::targett get_loop_head_or_end (const unsigned int loop_number, goto_functiont &function, bool finding_head)

Return loop head if finding_head is true, Otherwise return loop end.

goto_programt::targett get_loop_end (const unsigned int loop_number, goto_functiont &function)

Find and return the last instruction of the natural loop with loop_number in function.

goto_programt::targett get_loop_head (const unsigned int loop_number, goto_functiont &function)

Find and return the first instruction of the natural loop with loop_number in function.

exprt get_loop_invariants (const goto_programt::const_targett &loop_end, const bool check_side_effect=true)

Extract loop invariants from annotated loop end.

exprt get_loop_assigns (const goto_programt::const_targett &loop_end)

Extract loop assigns from annotated loop end.

exprt get_loop_decreases (const goto_programt::const_targett &loop_end, const bool check_side_effect=true)

Extract loop decreases from annotated loop end.

void annotate_invariants (const invariant_mapt &invariant_map, goto_modelt &goto_model)

Annotate the invariants in invariant_map to their corresponding loops.

void annotate_assigns (const std::map< loop_idt, std::set< exprt > > &assigns_map, goto_modelt &goto_model)

Annotate the assigns in assigns_map to their corresponding loops.

void annotate_assigns (const std::map< loop_idt, exprt > &assigns_map, goto_modelt &goto_model)

void annotate_decreases (const std::map< loop_idt, std::vector< exprt > > &decreases_map, goto_modelt &goto_model)

Annotate the decreases in decreases_map to their corresponding loops.

Macro Definition Documentation

◆ ENTERED_LOOP

#define ENTERED_LOOP "__entered_loop"

Definition at line 24 of file utils.h.

◆ IN_BASE_CASE

#define IN_BASE_CASE "__in_base_case"

Definition at line 23 of file utils.h.

◆ IN_LOOP_HAVOC_BLOCK

#define IN_LOOP_HAVOC_BLOCK "__in_loop_havoc_block"

Definition at line 25 of file utils.h.

◆ INIT_INVARIANT

#define INIT_INVARIANT "__init_invariant"

Definition at line 26 of file utils.h.

Typedef Documentation

◆ invariant_mapt

typedef std::map<loop_idt, exprt> invariant_mapt

Definition at line 30 of file utils.h.

Function Documentation

◆ all_dereferences_are_valid()

exprt all_dereferences_are_valid ( const exprt & expr,

const namespacet & ns

)

Generate a validity check over all dereferences in an expression.

This function generates a formula:

r_ok_exprt(pexpr_1, sizeof(*pexpr_1)) && r_ok_exprt(pexpr_2, sizeof(*pexpr_1)) && ...

over all dereferenced pointer expressions *(pexpr_1), *(pexpr_2), ... found in the AST of expr.

Parameters: expr The expression that contains dereferences to be validated.

ns The namespace that defines all symbols appearing in expr.

Returns: A conjunctive expression that checks validity of all pointers that are dereferenced within expr.

Definition at line 175 of file utils.cpp.

◆ annotate_assigns() [1/2]

void annotate_assigns ( const std::map< loop_idt, exprt > & assigns_map,

goto_modelt & goto_model

)

Definition at line 747 of file utils.cpp.

◆ annotate_assigns() [2/2]

void annotate_assigns ( const std::map< loop_idt, std::set< exprt > > & assigns_map,

goto_modelt & goto_model

)

Annotate the assigns in assigns_map to their corresponding loops.

Corresponding loops are specified by keys of assigns_map

Definition at line 725 of file utils.cpp.

◆ annotate_decreases()

void annotate_decreases ( const std::map< loop_idt, std::vector< exprt > > & decreases_map,

goto_modelt & goto_model

)

Annotate the decreases in decreases_map to their corresponding loops.

Corresponding loops are specified by keys of decreases_map

Definition at line 766 of file utils.cpp.

◆ annotate_invariants()

void annotate_invariants ( const invariant_mapt & invariant_map,

goto_modelt & goto_model

)

Annotate the invariants in invariant_map to their corresponding loops.

Corresponding loops are specified by keys of invariant_map

Definition at line 705 of file utils.cpp.

◆ generate_history_variables_initialization()

void generate_history_variables_initialization ( symbol_table_baset & symbol_table,

exprt & clause,

const irep_idt & mode,

goto_programt & program

)

This function generates all the instructions required to initialize history variables.

Definition at line 494 of file utils.cpp.

◆ generate_lexicographic_less_than_check()

exprt generate_lexicographic_less_than_check ( const std::vector< symbol_exprt > & lhs,

const std::vector< symbol_exprt > & rhs

)

Generate a lexicographic less-than comparison over ordered tuples.

This function creates an expression representing a lexicographic less-than comparison, lhs < rhs, between two ordered tuples of variables. This is used in instrumentation of decreases clauses.

Parameters: lhs A vector of variables representing the LHS of the comparison.

rhs A vector of variables representing the RHS of the comparison.

Returns: A lexicographic less-than comparison expression: LHS < RHS.

Definition at line 193 of file utils.cpp.

◆ get_loop_assigns()

exprt get_loop_assigns ( const goto_programt::const_targett & loop_end )

Extract loop assigns from annotated loop end.

Definition at line 683 of file utils.cpp.

◆ get_loop_decreases()

exprt get_loop_decreases ( const goto_programt::const_targett & loop_end,

const bool check_side_effect = true

)

Extract loop decreases from annotated loop end.

Will check if the loop decreases is side-effect free if check_side_effect` is set.

Definition at line 688 of file utils.cpp.

◆ get_loop_end()

goto_programt::targett get_loop_end ( const unsigned int loop_number,

goto_functiont & function

)

Find and return the last instruction of the natural loop with loop_number in function.

loop_end -> loop_head

Definition at line 634 of file utils.cpp.

◆ get_loop_end_from_loop_head_and_content()

goto_programt::const_targett get_loop_end_from_loop_head_and_content ( const goto_programt::const_targett & loop_head,

const loop_templatet< goto_programt::const_targett, goto_programt::target_less_than > & loop

)

Definition at line 560 of file utils.cpp.

◆ get_loop_end_from_loop_head_and_content_mutable()

goto_programt::targett get_loop_end_from_loop_head_and_content_mutable ( const goto_programt::targett & loop_head,

const loop_templatet< goto_programt::targett, goto_programt::target_less_than > & loop

)

Find the goto instruction of loop that jumps to loop_head

Definition at line 584 of file utils.cpp.

◆ get_loop_head()

goto_programt::targett get_loop_head ( const unsigned int loop_number,

goto_functiont & function

)

Find and return the first instruction of the natural loop with loop_number in function.

loop_end -> loop_head

Definition at line 640 of file utils.cpp.

◆ get_loop_head_or_end()

goto_programt::targett get_loop_head_or_end ( const unsigned int loop_number,

goto_functiont & function,

bool finding_head

)

Return loop head if finding_head is true, Otherwise return loop end.

Definition at line 607 of file utils.cpp.

◆ get_loop_invariants()

exprt get_loop_invariants ( const goto_programt::const_targett & loop_end,

const bool check_side_effect = true

)

Extract loop invariants from annotated loop end.

Will check if the loop invariant is side-effect free if check_side_effect` is set.

Definition at line 666 of file utils.cpp.

◆ get_suffix_unsigned()

unsigned get_suffix_unsigned ( const std::string & str,

const std::string & prefix

)

Convert the suffix digits right after prefix of str into unsigned.

Definition at line 546 of file utils.cpp.

◆ infer_loop_assigns()

void infer_loop_assigns ( const local_may_aliast & local_may_alias,

const loopt & loop,

assignst & assigns

)

Infer loop assigns using alias analysis result local_may_alias.

Definition at line 344 of file utils.cpp.

◆ insert_before_and_update_jumps()

void insert_before_and_update_jumps ( goto_programt & destination,

goto_programt::targett & target,

const goto_programt::instructiont & i

)

Insert a goto instruction before a target instruction iterator and update targets of all jumps that points to the iterator to jumping to the inserted instruction.

This method is intended to keep external instruction::targett stable, i.e. they will still point to the same instruction after inserting the new one

This function inserts a instruction i into a destination program destination immediately before a specified instruction iterator target. After insertion, update all jumps that pointing to target to jumping to i instead.

Different from insert_before_swap_and_advance, this function doesn't invalidate the iterator target after insertion. That is, target and all other instruction iterators same as target will still point to the same instruction after insertion.

Parameters: destination The destination program for inserting the i.

target The instruction iterator at which to insert the i.

i The goto instruction to be inserted into the destination.

Definition at line 247 of file utils.cpp.

◆ insert_before_swap_and_advance()

void insert_before_swap_and_advance ( goto_programt & destination,

goto_programt::targett & target,

goto_programt & payload

)

Insert a goto program before a target instruction iterator and advance the iterator.

This function inserts all instruction from a goto program payload into a destination program destination immediately before a specified instruction iterator target. After insertion, target is advanced by the size of the payload, and payload is destroyed.

Parameters: destination The destination program for inserting the payload.

target The instruction iterator at which to insert the payload.

payload The goto program to be inserted into the destination.

Definition at line 237 of file utils.cpp.

◆ is_assignment_to_instrumented_variable()

bool is_assignment_to_instrumented_variable ( const goto_programt::const_targett & target,

std::string var_name

)

Return true if target is an assignment to an instrumented variable with name var_name.

Definition at line 524 of file utils.cpp.

◆ is_assigns_clause_replacement_tracking_comment()

bool is_assigns_clause_replacement_tracking_comment ( const irep_idt & comment )

Returns true if the given comment matches the type of comments created by make_assigns_clause_replacement_tracking_comment.

Definition at line 338 of file utils.cpp.

◆ is_loop_free()

bool is_loop_free ( const goto_programt & goto_program,

const namespacet & ns,

messaget & log

)

Returns true iff the given program is loop-free, i.e.

if each SCC of its CFG contains a single element.

Definition at line 271 of file utils.cpp.

◆ is_transformed_loop_end()

bool is_transformed_loop_end ( const goto_programt::const_targett & target )

Return true if target is the end of some transformed loop.

Definition at line 516 of file utils.cpp.

◆ is_transformed_loop_head()

bool is_transformed_loop_head ( const goto_programt::const_targett & target )

Return true if target is the head of some transformed loop.

Definition at line 508 of file utils.cpp.

◆ make_assigns_clause_replacement_tracking_comment()

irep_idt make_assigns_clause_replacement_tracking_comment ( const exprt & target,

const irep_idt & function_id,

const namespacet & ns

)

Returns an irep_idt that essentially says that target was assigned by the contract of function_id.

Definition at line 329 of file utils.cpp.

◆ replace_history_loop_entry()

replace_history_parametert replace_history_loop_entry ( symbol_table_baset & symbol_table,

const exprt & expr,

const source_locationt & location,

const irep_idt & mode

)

This function recursively identifies the "loop_entry" expressions within expr and replaces them with corresponding history variables.

Definition at line 475 of file utils.cpp.

◆ replace_history_old()

replace_history_parametert replace_history_old ( symbol_table_baset & symbol_table,

const exprt & expr,

const source_locationt & location,

const irep_idt & mode

)

This function recursively identifies the "old" expressions within expr and replaces them with corresponding history variables.

Definition at line 456 of file utils.cpp.

◆ simplify_gotos()

void simplify_gotos ( goto_programt & goto_program,

const namespacet & ns

)

Turns goto instructions IF cond GOTO label where the condition statically simplifies to false into SKIP instructions.

Definition at line 260 of file utils.cpp.

◆ widen_assigns()

void widen_assigns ( assignst & assigns,

const namespacet & ns

)

Widen expressions in assigns with the following strategy.

If an expression is an array index or object dereference expression, with a non-constant offset, e.g. a[i] or *(b+i) with a non-constant i, then replace it by the entire underlying object. Otherwise, e.g. for a[i] or *(b+i) when i is a known constant, keep the expression in the result.

Definition at line 360 of file utils.cpp.