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
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{
34public:
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
50protected:
51 const namespacet &ns;
52};
53
57{
58public:
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
123exprt 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
154
165 const typet &type,
166 const source_locationt &location,
167 const irep_idt &mode,
169 std::string suffix = "tmp_cc",
170 bool is_auxiliary = true);
171
174void simplify_gotos(goto_programt &goto_program, namespacet &ns);
175
178bool is_loop_free(
179 const goto_programt &goto_program,
180 namespacet &ns,
181 messaget &log);
182
190{
191public:
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
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
239private:
245};
246
249{
250public:
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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 goto_programt::targett & get_current_target() const
returns the current target instruction
Definition utils.h:234
const namespacet & ns
Definition utils.h:240
const dirtyt dirty_analysis
Definition utils.h:243
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...
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
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
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().
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)
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
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
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