cprover
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 
14 #include <vector>
15 
16 #include <analyses/dirty.h>
17 #include <analyses/locals.h>
18 
20 
23 
24 #include <util/expr_cast.h>
25 #include <util/message.h>
26 
27 #define CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK "contracts:disable:assigns-check"
28 
33 {
34 public:
35  havoc_if_validt(const assignst &mod, const namespacet &ns)
36  : havoc_utilst(mod), ns(ns)
37  {
38  }
39 
41  const source_locationt location,
42  const exprt &expr,
43  goto_programt &dest) const override;
44 
46  const source_locationt location,
47  const exprt &expr,
48  goto_programt &dest) const override;
49 
50 protected:
51  const namespacet &ns;
52 };
53 
57 {
58 public:
60  : havoc_if_validt(mod, ns)
61  {
62  }
63 
65  const source_locationt location,
66  const exprt &expr,
67  goto_programt &dest) const override;
68 };
69 
74 // "unsigned-overflow-check", "conversion-check".
76 
83 
90 
93 
100 
107 
123 exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns);
124 
135  const std::vector<symbol_exprt> &lhs,
136  const std::vector<symbol_exprt> &rhs);
137 
151  goto_programt &destination,
152  goto_programt::targett &target,
153  goto_programt &payload);
154 
164 const symbolt &new_tmp_symbol(
165  const typet &type,
166  const source_locationt &location,
167  const irep_idt &mode,
168  symbol_table_baset &symtab,
169  std::string suffix = "tmp_cc",
170  bool is_auxiliary = true);
171 
174 void simplify_gotos(goto_programt &goto_program, namespacet &ns);
175 
178 bool is_loop_free(
179  const goto_programt &goto_program,
180  namespacet &ns,
181  messaget &log);
182 
190 {
191 public:
192  cfg_infot(const namespacet &_ns, goto_functiont &_goto_function)
193  : ns(_ns),
194  goto_function(_goto_function),
195  target(goto_function.body.instructions.begin()),
198  {
199  }
200 
202  void step()
203  {
204  target++;
205  }
206 
210  {
211  if(is_local(ident))
212  return dirty_analysis.get_dirty_ids().find(ident) !=
214  else
215  return true;
216  }
217 
220  bool is_maybe_alive(const symbol_exprt &symbol_expr)
221  {
222  // TODO query the static analysis when available
223  return true;
224  }
225 
227  bool is_local(irep_idt ident) const
228  {
229  const auto &symbol = ns.lookup(ident);
230  return locals.is_local(ident) || symbol.is_parameter;
231  }
232 
235  {
236  return target;
237  }
238 
239 private:
240  const namespacet &ns;
245 };
246 
248 class cleanert : public goto_convertt
249 {
250 public:
252  symbol_table_baset &_symbol_table,
253  message_handlert &_message_handler)
254  : goto_convertt(_symbol_table, _message_handler)
255  {
256  }
257 
258  void clean(exprt &guard, goto_programt &dest, const irep_idt &mode)
259  {
260  goto_convertt::clean_expr(guard, dest, mode, true);
261  }
262 };
263 
267  const exprt &target,
268  const irep_idt &function_id,
269  const namespacet &ns);
270 
274 
275 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H
Stores information about a goto function computed from its CFG, together with a target iterator into ...
Definition: utils.h:190
goto_programt::targett target
Definition: utils.h:242
const namespacet & ns
Definition: utils.h:240
const dirtyt dirty_analysis
Definition: utils.h:243
const goto_programt::targett & get_current_target() const
returns the current target instruction
Definition: utils.h:234
void step()
Steps the target iterator forward.
Definition: utils.h:202
cfg_infot(const namespacet &_ns, goto_functiont &_goto_function)
Definition: utils.h:192
const localst locals
Definition: utils.h:244
bool is_not_local_or_dirty_local(irep_idt ident) const
Returns true iff the given ident is either not a goto_function local or is a local that is dirty.
Definition: utils.h:209
bool is_local(irep_idt ident) const
Returns true iff ident is a local (or parameter) of goto_function.
Definition: utils.h:227
goto_functiont & goto_function
Definition: utils.h:241
bool is_maybe_alive(const symbol_exprt &symbol_expr)
Returns true whenever the given symbol_expr might be alive at the current target instruction.
Definition: utils.h:220
Allows to clean expressions of side effects.
Definition: utils.h:249
void clean(exprt &guard, goto_programt &dest, const irep_idt &mode)
Definition: utils.h:258
cleanert(symbol_table_baset &_symbol_table, message_handlert &_message_handler)
Definition: utils.h:251
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
Definition: dirty.h:27
const std::unordered_set< irep_idt > & get_dirty_ids() const
Definition: dirty.h:77
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
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...
Definition: goto_function.h:24
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::iterator targett
Definition: goto_program.h:592
A class that further overrides the "safe" havoc utilities, and adds support for havocing pointer_obje...
Definition: utils.h:57
havoc_assigns_targetst(const assignst &mod, const namespacet &ns)
Definition: utils.h:59
void append_havoc_code_for_expr(const source_locationt location, const exprt &expr, goto_programt &dest) const override
Append goto instructions to havoc a single expression expr
Definition: utils.cpp:65
A class that overrides the low-level havocing functions in the base utility class,...
Definition: utils.h:33
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:45
havoc_if_validt(const assignst &mod, const namespacet &ns)
Definition: utils.h:35
const namespacet & ns
Definition: utils.h:51
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:55
Definition: locals.h:25
bool is_local(const irep_idt &identifier) const
Definition: locals.h:37
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
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
Expression to hold a symbol (variable)
Definition: std_expr.h:80
The symbol table base class interface.
Symbol table entry.
Definition: symbol.h:28
The type of an expression, extends irept.
Definition: type.h:29
Variables whose address is taken.
Templated functions to cast to specific exprt-derived classes.
Program Transformation.
Symbol Table + CFG.
Utilities for building havoc code for expressions.
std::set< exprt > assignst
Definition: havoc_utils.h:23
Local variables whose address is taken.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
void add_pragma_disable_pointer_checks(source_locationt &source_location)
Adds a pragma on a source location disable all pointer checks.
Definition: utils.cpp:79
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:269
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:215
exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns)
Generate a validity check over all dereferences in an expression.
Definition: utils.cpp:122
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &location, const irep_idt &mode, symbol_table_baset &symtab, std::string suffix="tmp_cc", bool is_auxiliary=true)
Adds a fresh and uniquely named symbol to the symbol table.
Definition: utils.cpp:190
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:278
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:180
void add_pragma_disable_assigns_check(source_locationt &source_location)
Adds a pragma on a source_locationt to disable inclusion checking.
Definition: utils.cpp:103
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:204
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:136