- Generated by
1.15.0
|
cprover
|
#include "utils.h"#include <util/c_types.h>#include <util/fresh_symbol.h>#include <util/graph.h>#include <util/mathematical_expr.h>#include <util/message.h>#include <util/pointer_expr.h>#include <util/pointer_offset_size.h>#include <util/pointer_predicates.h>#include <util/prefix.h>#include <util/simplify_expr.h>#include <util/symbol.h>#include <goto-programs/cfg.h>#include <analyses/natural_loops.h>#include <ansi-c/c_expr.h>#include <langapi/language_util.h>Go to the source code of this file.
Functions | |
| static void | append_safe_havoc_code_for_expr (const source_locationt location, const namespacet &ns, const exprt &expr, goto_programt &dest, const std::function< void()> &havoc_code_impl) |
| 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. | |
| static void | replace_history_parameter_rec (symbol_table_baset &symbol_table, exprt &expr, std::unordered_map< exprt, symbol_exprt, irep_hash > ¶meter2history, const source_locationt &location, const irep_idt &mode, goto_programt &history, const irep_idt &history_id) |
| 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::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) |
| Find the goto instruction of loop that jumps to loop_head. | |
| goto_programt::targett | get_loop_head_or_end (const unsigned int target_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 target_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 target_loop_number, goto_functiont &function) |
| Find and return the first instruction of the natural loop with loop_number in function. | |
| static exprt | extract_loop_invariants (const goto_programt::const_targett &loop_end) |
| Extract loop invariants from loop end without any checks. | |
| static exprt | extract_loop_assigns (const goto_programt::const_targett &loop_end) |
| static exprt | extract_loop_decreases (const goto_programt::const_targett &loop_end) |
| exprt | get_loop_invariants (const goto_programt::const_targett &loop_end, const bool check_side_effect) |
| exprt | get_loop_assigns (const goto_programt::const_targett &loop_end) |
| exprt | get_loop_decreases (const goto_programt::const_targett &loop_end, const bool check_side_effect) |
| void | annotate_invariants (const invariant_mapt &invariant_map, goto_modelt &goto_model) |
| Extract loop invariants from annotated loop end. | |
| 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. | |
Variables | |
| static const char | ASSIGNS_CLAUSE_REPLACEMENT_TRACKING [] |
| Prefix for comments added to track assigns clause replacement. | |
| 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. |
| 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 ) |
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. */ exprt get_loop_decreases( const goto_programt::const_targett &loop_end, const bool check_side_effect = true);
/** Annotate the invariants in invariant_map to their corresponding loops. Corresponding loops are specified by keys of invariant_map
|
static |
|
static |
|
static |
|
static |
| 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_assigns | ( | const goto_programt::const_targett & | loop_end | ) |
| exprt get_loop_decreases | ( | const goto_programt::const_targett & | loop_end, |
| const bool | check_side_effect ) |
| 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 | target_loop_number, |
| goto_functiont & | function, | ||
| bool | finding_head ) |
| exprt get_loop_invariants | ( | const goto_programt::const_targett & | loop_end, |
| const bool | check_side_effect ) |
| 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 ) |
|
static |
| 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.
1.15.0