CBMC
utils.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Utility functions for code contracts.
4 
5 Author: Saswat Padhi, saspadhi@amazon.com
6 
7 Date: September 2021
8 
9 \*******************************************************************/
10 
11 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H
12 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H
13 
15 
17 #include <goto-programs/loop_ids.h>
18 
22 
23 #include <vector>
24 
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"
29 
30 template <class T, typename C>
31 class loop_templatet;
32 typedef std::map<loop_idt, exprt> invariant_mapt;
33 
36 class cleanert : public goto_convertt
37 {
38 public:
40  symbol_table_baset &_symbol_table,
41  message_handlert &_message_handler)
42  : goto_convertt(_symbol_table, _message_handler)
43  {
44  }
45 
46  [[nodiscard]] std::list<irep_idt>
47  clean(exprt &guard, goto_programt &dest, const irep_idt &mode)
48  {
49  auto clean_result = goto_convertt::clean_expr(guard, mode, true);
50  dest.destructive_append(clean_result.side_effects);
51  return clean_result.temporaries;
52  }
53 
55  const symbol_exprt &function,
56  const exprt::operandst &arguments,
57  goto_programt &dest,
58  const irep_idt &mode)
59  {
60  goto_convertt::do_havoc_slice(nil_exprt{}, function, arguments, dest, mode);
61  }
62 };
63 
68 {
69 public:
70  havoc_if_validt(const assignst &mod, const namespacet &ns)
71  : havoc_utilst(mod, ns), ns(ns)
72  {
73  }
74 
76  const source_locationt location,
77  const exprt &expr,
78  goto_programt &dest) const override;
79 
81  const source_locationt location,
82  const exprt &expr,
83  goto_programt &dest) const override;
84 
85 protected:
86  const namespacet &ns;
87 };
88 
92 {
93 public:
95  const assignst &mod,
96  symbol_tablet &st,
97  message_handlert &message_handler,
98  const irep_idt &mode)
99  : havoc_if_validt(mod, ns),
100  ns(st),
101  cleaner(st, message_handler),
102  log(message_handler),
103  mode(mode)
104  {
105  }
106 
108  const source_locationt location,
109  const exprt &ptr_to_ptr,
110  goto_programt &dest);
111 
113  const source_locationt location,
114  const exprt &ptr,
115  const exprt &size,
116  goto_programt &dest);
117 
119  const source_locationt location,
120  const exprt &expr,
121  goto_programt &dest);
122 
126  const irep_idt &mode;
127 };
128 
144 exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns);
145 
156  const std::vector<symbol_exprt> &lhs,
157  const std::vector<symbol_exprt> &rhs);
158 
172  goto_programt &destination,
173  goto_programt::targett &target,
174  goto_programt &payload);
175 
196  goto_programt &destination,
197  goto_programt::targett &target,
198  const goto_programt::instructiont &i);
199 
202 void simplify_gotos(goto_programt &goto_program, const namespacet &ns);
203 
206 bool is_loop_free(
207  const goto_programt &goto_program,
208  const namespacet &ns,
209  messaget &log);
210 
214  const exprt &target,
215  const irep_idt &function_id,
216  const namespacet &ns);
217 
221 
223 void infer_loop_assigns(
224  const local_may_aliast &local_may_alias,
225  const loopt &loop,
226  assignst &assigns);
227 
233 void widen_assigns(assignst &assigns, const namespacet &ns);
234 
236 {
238  std::unordered_map<exprt, symbol_exprt, irep_hash> parameter_to_history;
240 };
241 
245  symbol_table_baset &symbol_table,
246  const exprt &expr,
247  const source_locationt &location,
248  const irep_idt &mode);
249 
253  symbol_table_baset &symbol_table,
254  const exprt &expr,
255  const source_locationt &location,
256  const irep_idt &mode);
257 
261  symbol_table_baset &symbol_table,
262  exprt &clause,
263  const irep_idt &mode,
264  goto_programt &program);
265 
268 
271 
275  const goto_programt::const_targett &target,
276  std::string var_name);
277 
279 unsigned get_suffix_unsigned(const std::string &str, const std::string &prefix);
280 
283  const goto_programt::targett &loop_head,
285  &loop);
286 
288  const goto_programt::const_targett &loop_head,
289  const loop_templatet<
292 
296  const unsigned int loop_number,
297  goto_functiont &function,
298  bool finding_head);
299 
303 get_loop_end(const unsigned int loop_number, goto_functiont &function);
304 
308 get_loop_head(const unsigned int loop_number, goto_functiont &function);
309 
314  const goto_programt::const_targett &loop_end,
315  const bool check_side_effect = true);
316 
319 
324  const goto_programt::const_targett &loop_end,
325  const bool check_side_effect = true);
326 
330  const invariant_mapt &invariant_map,
331  goto_modelt &goto_model);
332 
335 void annotate_assigns(
336  const std::map<loop_idt, std::set<exprt>> &assigns_map,
337  goto_modelt &goto_model);
338 
339 void annotate_assigns(
340  const std::map<loop_idt, exprt> &assigns_map,
341  goto_modelt &goto_model);
342 
345 void annotate_decreases(
346  const std::map<loop_idt, std::vector<exprt>> &decreases_map,
347  goto_modelt &goto_model);
348 
349 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H
static exprt guard(const exprt::operandst &guards, exprt cond)
Class that allows to clean expressions of side effects and to generate havoc_slice expressions.
Definition: utils.h:37
cleanert(symbol_table_baset &_symbol_table, message_handlert &_message_handler)
Definition: utils.h:39
void do_havoc_slice(const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
Definition: utils.h:54
std::list< irep_idt > clean(exprt &guard, goto_programt &dest, const irep_idt &mode)
Definition: utils.h:47
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
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)
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...
Definition: goto_function.h:24
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::iterator targett
Definition: goto_program.h:614
instructionst::const_iterator const_targett
Definition: goto_program.h:615
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:722
A class that further overrides the "safe" havoc utilities, and adds support for havocing pointer_obje...
Definition: utils.h:92
void append_havoc_pointer_code(const source_locationt location, const exprt &ptr_to_ptr, goto_programt &dest)
Definition: utils.cpp:76
void append_havoc_slice_code(const source_locationt location, const exprt &ptr, const exprt &size, goto_programt &dest)
Definition: utils.cpp:54
const irep_idt & mode
Definition: utils.h:126
cleanert cleaner
Definition: utils.h:124
namespacet ns
Definition: utils.h:123
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:108
havoc_assigns_targetst(const assignst &mod, symbol_tablet &st, message_handlert &message_handler, const irep_idt &mode)
Definition: utils.h:94
A class that overrides the low-level havocing functions in the base utility class,...
Definition: utils.h:68
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:88
havoc_if_validt(const assignst &mod, const namespacet &ns)
Definition: utils.h:70
const namespacet & ns
Definition: utils.h:86
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:98
A loop, specified as a set of instructions.
Definition: loop_analysis.h:24
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
The NIL expression.
Definition: std_expr.h:3086
Expression to hold a symbol (variable)
Definition: std_expr.h:131
The symbol table base class interface.
The symbol table.
Definition: symbol_table.h:14
Program Transformation.
Symbol Table + CFG.
Utilities for building havoc code for expressions.
std::set< exprt > assignst
Definition: havoc_utils.h:22
Field-insensitive, location-sensitive may-alias analysis.
Loop IDs.
Helper functions for k-induction and loop invariants.
natural_loops_mutablet::natural_loopt loopt
Definition: loop_utils.h:20
double log(double x)
Definition: math.c:2776
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:108
A total order over targett and const_targett.
Definition: goto_program.h:392
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:238
goto_programt history_construction
Definition: utils.h:239
exprt expression_after_replacement
Definition: utils.h:237
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:456
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:494
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:524
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:329
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:560
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:247
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: utils.cpp:344
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.
Definition: utils.cpp:271
exprt get_loop_assigns(const goto_programt::const_targett &loop_end)
Extract loop assigns from annotated loop end.
Definition: utils.cpp:683
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:475
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:508
exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns)
Generate a validity check over all dereferences in an expression.
Definition: utils.cpp:175
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:640
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:338
std::map< loop_idt, exprt > invariant_mapt
Definition: utils.h:31
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:766
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:237
void widen_assigns(assignst &assigns, const namespacet &ns)
Widen expressions in assigns with the following strategy.
Definition: utils.cpp:360
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...
Definition: utils.cpp:260
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:607
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:516
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:584
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:705
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:725
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:634
exprt get_loop_decreases(const goto_programt::const_targett &loop_end, const bool check_side_effect=true)
Extract loop decreases from annotated loop end.
Definition: utils.cpp:688
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:546
exprt get_loop_invariants(const goto_programt::const_targett &loop_end, const bool check_side_effect=true)
Extract loop invariants from annotated loop end.
Definition: utils.cpp:666
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:193