cprover
Loading...
Searching...
No Matches
utils.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Utility functions for code contracts.
4
5Author: Saswat Padhi, saspadhi@amazon.com
6
7Date: September 2021
8
9\*******************************************************************/
10
11#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H
12#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H
13
15
18
20
21#include <vector>
22
23#define IN_BASE_CASE "__in_base_case"
24#define ENTERED_LOOP "__entered_loop"
25#define IN_LOOP_HAVOC_BLOCK "__in_loop_havoc_block"
26#define INIT_INVARIANT "__init_invariant"
27
28template <class T, typename C>
29class loop_templatet;
30typedef std::map<loop_idt, exprt> invariant_mapt;
31
34class cleanert : public goto_convertt
35{
36public:
43
44 void clean(exprt &guard, goto_programt &dest, const irep_idt &mode)
45 {
46 goto_convertt::clean_expr(guard, dest, mode, true);
47 }
48
50 const symbol_exprt &function,
51 const exprt::operandst &arguments,
52 goto_programt &dest,
53 const irep_idt &mode)
54 {
55 goto_convertt::do_havoc_slice(nil_exprt{}, function, arguments, dest, mode);
56 }
57};
58
63{
64public:
66 : havoc_utilst(mod, ns), ns(ns)
67 {
68 }
69
71 const source_locationt location,
72 const exprt &expr,
73 goto_programt &dest) const override;
74
76 const source_locationt location,
77 const exprt &expr,
78 goto_programt &dest) const override;
79
80protected:
81 const namespacet &ns;
82};
83
87{
88public:
90 const assignst &mod,
91 symbol_tablet &st,
92 message_handlert &message_handler,
93 const irep_idt &mode)
95 ns(st),
96 cleaner(st, message_handler),
97 log(message_handler),
98 mode(mode)
99 {
100 }
101
103 const source_locationt location,
104 const exprt &ptr_to_ptr,
105 goto_programt &dest);
106
108 const source_locationt location,
109 const exprt &ptr,
110 const exprt &size,
111 goto_programt &dest);
112
114 const source_locationt location,
115 const exprt &expr,
116 goto_programt &dest);
117
122};
123
139exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns);
140
151 const std::vector<symbol_exprt> &lhs,
152 const std::vector<symbol_exprt> &rhs);
153
170
194
197void simplify_gotos(goto_programt &goto_program, namespacet &ns);
198
201bool is_loop_free(
202 const goto_programt &goto_program,
203 namespacet &ns,
204 messaget &log);
205
209 const exprt &target,
210 const irep_idt &function_id,
211 const namespacet &ns);
212
216
222void widen_assigns(assignst &assigns, const namespacet &ns);
223
229 symbol_table_baset &symbol_table,
230 exprt &expression,
231 const irep_idt &mode);
232
239
243 symbol_table_baset &symbol_table,
244 const exprt &expr,
245 const source_locationt &location,
246 const irep_idt &mode);
247
251 symbol_table_baset &symbol_table,
252 const exprt &expr,
253 const source_locationt &location,
254 const irep_idt &mode);
255
259 symbol_table_baset &symbol_table,
260 exprt &clause,
261 const irep_idt &mode,
262 goto_programt &program);
263
266
269
273 const goto_programt::const_targett &target,
274 std::string var_name);
275
277unsigned get_suffix_unsigned(const std::string &str, const std::string &prefix);
278
283 &loop);
284
287 const loop_templatet<
290
294 const unsigned int loop_number,
295 goto_functiont &function,
296 bool finding_head);
297
301get_loop_end(const unsigned int loop_number, goto_functiont &function);
302
306get_loop_head(const unsigned int loop_number, goto_functiont &function);
307
312 goto_modelt &goto_model);
313
317 const std::map<loop_idt, std::set<exprt>> &assigns_map,
318 goto_modelt &goto_model);
319
321 const std::map<loop_idt, exprt> &assigns_map,
322 goto_modelt &goto_model);
323
327 const std::map<loop_idt, std::vector<exprt>> &decreases_map,
328 goto_modelt &goto_model);
329
330#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H
static exprt guard(const exprt::operandst &guards, exprt cond)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Class that allows to clean expressions of side effects and to generate havoc_slice expressions.
Definition utils.h:35
void clean(exprt &guard, goto_programt &dest, const irep_idt &mode)
Definition utils.h:44
cleanert(symbol_table_baset &_symbol_table, message_handlert &_message_handler)
Definition utils.h:37
void do_havoc_slice(const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
Definition utils.h:49
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
void do_havoc_slice(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
void clean_expr(exprt &expr, goto_programt &dest, 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
A class that further overrides the "safe" havoc utilities, and adds support for havocing pointer_obje...
Definition utils.h:87
void append_havoc_pointer_code(const source_locationt location, const exprt &ptr_to_ptr, goto_programt &dest)
Definition utils.cpp:73
void append_havoc_slice_code(const source_locationt location, const exprt &ptr, const exprt &size, goto_programt &dest)
Definition utils.cpp:51
const irep_idt & mode
Definition utils.h:121
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
Definition utils.cpp:105
havoc_assigns_targetst(const assignst &mod, symbol_tablet &st, message_handlert &message_handler, const irep_idt &mode)
Definition utils.h:89
A class that overrides the low-level havocing functions in the base utility class,...
Definition utils.h:63
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
Definition utils.cpp:85
havoc_if_validt(const assignst &mod, const namespacet &ns)
Definition utils.h:65
const namespacet & ns
Definition utils.h:81
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
Definition utils.cpp:95
A loop, specified as a set of instructions.
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The NIL expression.
Definition std_expr.h:3026
Expression to hold a symbol (variable)
Definition std_expr.h:113
The symbol table base class interface.
The symbol table.
Program Transformation.
Symbol Table + CFG.
Utilities for building havoc code for expressions.
std::set< exprt > assignst
Definition havoc_utils.h:24
Loop IDs.
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.
Definition loop_ids.h:28
std::unordered_map< exprt, symbol_exprt, irep_hash > parameter_to_history
Definition utils.h:236
goto_programt history_construction
Definition utils.h:237
exprt expression_after_replacement
Definition utils.h:235
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...
Definition utils.cpp:511
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 utils.cpp:549
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 utils.cpp:579
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 utils.cpp:326
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 utils.cpp:615
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...
Definition utils.cpp:244
void add_quantified_variable(symbol_table_baset &symbol_table, exprt &expression, const irep_idt &mode)
This function recursively searches expression to find nested or non-nested quantified expressions.
Definition utils.cpp:367
bool is_loop_free(const goto_programt &goto_program, namespacet &ns, messaget &log)
Returns true iff the given program is loop-free, i.e.
Definition utils.cpp:268
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 ...
Definition utils.cpp:530
bool is_transformed_loop_head(const goto_programt::const_targett &target)
Return true if target is the head of some transformed loop.
Definition utils.cpp:563
exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns)
Generate a validity check over all dereferences in an expression.
Definition utils.cpp:172
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.
Definition utils.cpp:695
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.
Definition utils.cpp:761
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...
Definition utils.cpp:335
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.
Definition utils.cpp:720
std::map< loop_idt, exprt > invariant_mapt
Definition utils.h:30
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.
Definition utils.cpp:234
void widen_assigns(assignst &assigns, const namespacet &ns)
Widen expressions in assigns with the following strategy.
Definition utils.cpp:341
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 utils.cpp:662
bool is_transformed_loop_end(const goto_programt::const_targett &target)
Return true if target is the end of some transformed loop.
Definition utils.cpp:571
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 utils.cpp:639
void annotate_invariants(const invariant_mapt &invariant_map, goto_modelt &goto_model)
Annotate the invariants in invariant_map to their corresponding loops.
Definition utils.cpp:700
void simplify_gotos(goto_programt &goto_program, namespacet &ns)
Turns goto instructions IF cond GOTO label where the condition statically simplifies to false into SK...
Definition utils.cpp:257
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.
Definition utils.cpp:689
unsigned get_suffix_unsigned(const std::string &str, const std::string &prefix)
Convert the suffix digits right after prefix of str into unsigned.
Definition utils.cpp:601
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.
Definition utils.cpp:190