11 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H
12 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H
25 #define IN_BASE_CASE "__in_base_case"
26 #define ENTERED_LOOP "__entered_loop"
27 #define IN_LOOP_HAVOC_BLOCK "__in_loop_havoc_block"
28 #define INIT_INVARIANT "__init_invariant"
30 template <
class T,
typename C>
46 [[nodiscard]] std::list<irep_idt>
51 return clean_result.temporaries;
102 log(message_handler),
109 const exprt &ptr_to_ptr,
156 const std::vector<symbol_exprt> &lhs,
157 const std::vector<symbol_exprt> &rhs);
276 std::string var_name);
296 const unsigned int loop_number,
315 const bool check_side_effect =
true);
325 const bool check_side_effect =
true);
336 const std::map<
loop_idt, std::set<exprt>> &assigns_map,
340 const std::map<loop_idt, exprt> &assigns_map,
346 const std::map<
loop_idt, std::vector<exprt>> &decreases_map,
static exprt guard(const exprt::operandst &guards, exprt cond)
Class that allows to clean expressions of side effects and to generate havoc_slice expressions.
cleanert(symbol_table_baset &_symbol_table, message_handlert &_message_handler)
void do_havoc_slice(const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
std::list< irep_idt > clean(exprt &guard, goto_programt &dest, const irep_idt &mode)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
void do_havoc_slice(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
clean_expr_resultt clean_expr(exprt &expr, const irep_idt &mode, bool result_is_used=true)
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
instructionst::const_iterator const_targett
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
A class that further overrides the "safe" havoc utilities, and adds support for havocing pointer_obje...
void append_havoc_pointer_code(const source_locationt location, const exprt &ptr_to_ptr, goto_programt &dest)
void append_havoc_slice_code(const source_locationt location, const exprt &ptr, const exprt &size, goto_programt &dest)
void append_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest)
Append goto instructions to havoc a single expression expr
havoc_assigns_targetst(const assignst &mod, symbol_tablet &st, message_handlert &message_handler, const irep_idt &mode)
A class that overrides the low-level havocing functions in the base utility class,...
void append_object_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const override
Append goto instructions to havoc the underlying object of expr
havoc_if_validt(const assignst &mod, const namespacet &ns)
void append_scalar_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const override
Append goto instructions to havoc the value of expr
A loop, specified as a set of instructions.
Class that provides messages with a built-in verbosity 'level'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Expression to hold a symbol (variable)
The symbol table base class interface.
Utilities for building havoc code for expressions.
std::set< exprt > assignst
Field-insensitive, location-sensitive may-alias analysis.
Helper functions for k-induction and loop invariants.
natural_loops_mutablet::natural_loopt loopt
static std::string comment(const rw_set_baset::entryt &entry, bool write)
A total order over targett and const_targett.
Loop id used to identify loops.
std::unordered_map< exprt, symbol_exprt, irep_hash > parameter_to_history
goto_programt history_construction
exprt expression_after_replacement
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 corresp...
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_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.
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.
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)
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 p...
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.
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.
exprt get_loop_assigns(const goto_programt::const_targett &loop_end)
Extract loop assigns from annotated loop end.
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 ...
bool is_transformed_loop_head(const goto_programt::const_targett &target)
Return true if target is the head of some transformed loop.
exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns)
Generate a validity check over all dereferences in an expression.
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.
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_replace...
std::map< loop_idt, exprt > invariant_mapt
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.
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 widen_assigns(assignst &assigns, const namespacet &ns)
Widen expressions in assigns with the following strategy.
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 SK...
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.
bool is_transformed_loop_end(const goto_programt::const_targett &target)
Return true if target is the end of some transformed 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
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.
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.
exprt get_loop_decreases(const goto_programt::const_targett &loop_end, const bool check_side_effect=true)
Extract loop decreases from annotated loop end.
unsigned get_suffix_unsigned(const std::string &str, const std::string &prefix)
Convert the suffix digits right after prefix of str into unsigned.
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 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.