cprover
|
#include <ansi-c/goto-conversion/goto_convert_class.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/loop_ids.h>
#include <analyses/local_may_alias.h>
#include <goto-instrument/havoc_utils.h>
#include <goto-instrument/loop_utils.h>
#include <vector>
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_decreases (const goto_programt::const_targett &loop_end, const bool check_side_effect=true) |
Extract loop invariants 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. | |
typedef std::map<loop_idt, exprt> invariant_mapt |
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
.
expr | The expression that contains dereferences to be validated. |
ns | The namespace that defines all symbols appearing in expr . |
expr
. void annotate_assigns | ( | const std::map< loop_idt, exprt > & | assigns_map, |
goto_modelt & | goto_model ) |
void annotate_assigns | ( | const std::map< loop_idt, std::set< exprt > > & | assigns_map, |
goto_modelt & | goto_model ) |
void annotate_decreases | ( | const std::map< loop_idt, std::vector< exprt > > & | decreases_map, |
goto_modelt & | goto_model ) |
void annotate_invariants | ( | const invariant_mapt & | invariant_map, |
goto_modelt & | goto_model ) |
void generate_history_variables_initialization | ( | symbol_table_baset & | symbol_table, |
exprt & | clause, | ||
const irep_idt & | mode, | ||
goto_programt & | program ) |
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.
lhs | A vector of variables representing the LHS of the comparison. |
rhs | A vector of variables representing the RHS of the comparison. |
exprt get_loop_decreases | ( | 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. exprt get_loop_invariants( const goto_programt::const_targett &loop_end, const bool check_side_effect = true);
/ Extract loop assigns from annotated loop end. exprt get_loop_assigns(const goto_programt::const_targett &loop_end);
/ Extract loop decreases from annotated loop end. / Will check if the loop decreases is side-effect free if / check_side_effect`
is set.
goto_programt::targett get_loop_end | ( | const unsigned int | loop_number, |
goto_functiont & | function ) |
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_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 ) |
goto_programt::targett get_loop_head | ( | const unsigned int | loop_number, |
goto_functiont & | function ) |
goto_programt::targett get_loop_head_or_end | ( | const unsigned int | loop_number, |
goto_functiont & | function, | ||
bool | finding_head ) |
unsigned get_suffix_unsigned | ( | const std::string & | str, |
const std::string & | prefix ) |
void infer_loop_assigns | ( | const local_may_aliast & | local_may_alias, |
const loopt & | loop, | ||
assignst & | assigns ) |
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.
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 . |
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.
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 . |
bool is_assignment_to_instrumented_variable | ( | const goto_programt::const_targett & | target, |
std::string | var_name ) |
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.
bool is_loop_free | ( | const goto_programt & | goto_program, |
const namespacet & | ns, | ||
messaget & | log ) |
bool is_transformed_loop_end | ( | const goto_programt::const_targett & | target | ) |
bool is_transformed_loop_head | ( | const goto_programt::const_targett & | target | ) |
irep_idt make_assigns_clause_replacement_tracking_comment | ( | const exprt & | target, |
const irep_idt & | function_id, | ||
const namespacet & | ns ) |
replace_history_parametert replace_history_loop_entry | ( | symbol_table_baset & | symbol_table, |
const exprt & | expr, | ||
const source_locationt & | location, | ||
const irep_idt & | mode ) |
replace_history_parametert replace_history_old | ( | symbol_table_baset & | symbol_table, |
const exprt & | expr, | ||
const source_locationt & | location, | ||
const irep_idt & | mode ) |
void simplify_gotos | ( | goto_programt & | goto_program, |
const namespacet & | ns ) |
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.