cprover
Loading...
Searching...
No Matches
dfcc_cfg_info.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking for function and loop contracts.
4
5Author: Qinheping Hu, qinhh@amazon.com
6Author: Remi Delmas delmasrd@amazon.com
7
8Date: March 2023
9
10\*******************************************************************/
11
16
17#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CFG_INFO_H
18#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CFG_INFO_H
19
20#include <util/namespace.h>
21#include <util/std_expr.h>
22#include <util/symbol_table.h>
23
25
27
28#include <map>
29#include <set>
30#include <unordered_set>
31
32class dfcc_libraryt;
33class goto_functiont;
35
39{
40public:
42 std::size_t loop_id,
43 std::size_t cbmc_loop_id,
44 const std::set<exprt> &assigns,
47 const std::unordered_set<irep_idt> &local,
48 const std::unordered_set<irep_idt> &tracked,
49 std::set<std::size_t> inner_loops,
50 std::set<std::size_t> outer_loops,
58 local(local),
64 {
65 }
66
68 void output(std::ostream &out) const;
69
96 find_head(goto_programt &goto_program) const;
97
98 // Finds the last instruction tagged as loop latch and having the same loop
99 // identifier as this struct in the given program. The goto program passed as
100 // argument to this method must be the program from which that dfcc_loop_infot
101 // instance was initially generated. Technically it will not be the exact same
102 // program because the whole point of contract instrumentation is to
103 // instrument the program into a different program by adding new instructions
104 // in the program and turning loops into non-loops. For an explanation of why
105 // this would work please read the documentation of find head, and mentally
106 // replace `head` by `latch` and `start` by `end` in the explanation.
108 find_latch(goto_programt &goto_program) const;
109
111 const std::size_t loop_id;
112
114 const std::size_t cbmc_loop_id;
115
117 const std::set<exprt> assigns;
118
121
124
127 const std::unordered_set<irep_idt> local;
128
132 const std::unordered_set<irep_idt> tracked;
133
135 const std::set<std::size_t> inner_loops;
136
138 const std::set<std::size_t> outer_loops;
139
142
147};
148
235{
236public:
238 const irep_idt &function_id,
241 const dfcc_loop_contract_modet loop_contract_mode,
242 symbol_table_baset &symbol_table,
243 message_handlert &message_handler,
244 dfcc_libraryt &library);
245
246 void output(std::ostream &out) const;
247
249 const dfcc_loop_infot &get_loop_info(const std::size_t loop_id) const;
250
253
256 const std::unordered_set<irep_idt> &
258
261 const std::unordered_set<irep_idt> &
263
266 const exprt &get_outer_write_set(std::size_t loop_id) const;
267
268 const std::vector<std::size_t> &get_loops_toposorted() const
269 {
270 return topsorted_loops;
271 }
272
276 get_outer_loop_identifier(const std::size_t loop_id) const;
277
281
288
290 {
291 return top_level_write_set;
292 }
293
296 const std::unordered_set<irep_idt> &get_top_level_tracked()
297 {
298 return top_level_tracked;
299 }
300
301private:
306
309 bool is_valid_loop_or_top_level_id(const std::size_t id) const;
310
312 bool is_valid_loop_id(const std::size_t id) const;
313
315 bool is_top_level_id(const std::size_t id) const;
316
318 std::vector<std::size_t> topsorted_loops;
319
322 std::vector<std::size_t> top_level_loops;
323
325 std::unordered_set<irep_idt> top_level_local;
326
328 std::unordered_set<irep_idt> top_level_tracked;
329
331 std::map<std::size_t, dfcc_loop_infot> loop_info_map;
332};
333
334#endif
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Computes natural loops, enforces normal form conditions, computes the nesting graph,...
std::unordered_set< irep_idt > top_level_local
Set of identifiers DECL at top level.
const exprt & top_level_write_set
const namespacet ns
const std::unordered_set< irep_idt > & get_top_level_tracked()
Returns the set of top level symbols that must be tracked explicitly in the top level write set of th...
std::vector< std::size_t > topsorted_loops
Loop identifiers sorted from most deeply nested to less deeply nested.
std::unordered_set< irep_idt > top_level_tracked
Set of identifiers DECL at top level.
bool is_top_level_id(const std::size_t id) const
True iff id is in the valid range for a loop id for this function.
const dfcc_loop_infot & get_loop_info(const std::size_t loop_id) const
Returns the loop info for that loop_id.
void output(std::ostream &out) const
const std::vector< std::size_t > & get_loops_toposorted() const
const optionalt< std::size_t > get_outer_loop_identifier(const std::size_t loop_id) const
Finds the DFCC id of the loop that contains the given loop, returns nullopt when the loop has no oute...
goto_functiont & goto_function
std::vector< std::size_t > top_level_loops
Loop identifiers for top level loops (ie for loops that are not nested in in another loop).
const std::unordered_set< irep_idt > & get_tracked_set(goto_programt::const_targett target) const
Returns the subset of local variable that are explicitly tracked in the write set for the scope where...
bool must_check_lhs(goto_programt::const_targett target) const
True iff the lhs of an assignment must be checked against the ambient write set.
dfcc_cfg_infot(const irep_idt &function_id, goto_functiont &goto_function, const exprt &top_level_write_set, const dfcc_loop_contract_modet loop_contract_mode, symbol_table_baset &symbol_table, message_handlert &message_handler, dfcc_libraryt &library)
const std::unordered_set< irep_idt > & get_local_set(goto_programt::const_targett target) const
Returns the set of local variable for the scope where that target instruction is found.
const exprt & get_outer_write_set(std::size_t loop_id) const
Returns the write set of the outer loop of that loop or the top level write set if that loop has no o...
const exprt & get_write_set(goto_programt::const_targett target) const
Returns the write set variable for that instruction.
bool must_track_decl_or_dead(goto_programt::const_targett target) const
True iff a DECL ident must be tracked in the write set of the loop that contains the DECL.
bool is_valid_loop_id(const std::size_t id) const
True iff id is in the valid range for a loop id for this function.
const irep_idt & function_id
std::map< std::size_t, dfcc_loop_infot > loop_info_map
Map from loop identifier to loop info struct.
bool is_valid_loop_or_top_level_id(const std::size_t id) const
True iff id is in the valid range for a loop id or is equal to the top level id for this function.
const exprt & get_top_level_write_set() const
Class interface to library types and functions defined in cprover_contracts.c.
Describes a single loop for the purpose of DFCC loop contract instrumentation.
const symbol_exprt addr_of_write_set_var
Symbol representing pointer to the stack allocated write set object for this loop.
optionalt< goto_programt::targett > find_head(goto_programt &goto_program) const
Finds the first instruction tagged as loop head and having the same loop identifier as this struct in...
void output(std::ostream &out) const
Prints a textual representation of the struct to out.
const exprt::operandst decreases
Decreases clause expression.
const std::unordered_set< irep_idt > local
Set of local identifiers locally DECL in loop instructions, excluding identifiers declared in nested ...
const std::set< exprt > assigns
Set of targets assigned by the loop, either user-provided or inferred.
const std::size_t cbmc_loop_id
Loop identifier assigned to this loop by traditional CBMC loop numbering.
const std::unordered_set< irep_idt > tracked
Subset of locals that must be tracked in the loop's write set.
dfcc_loop_infot(std::size_t loop_id, std::size_t cbmc_loop_id, const std::set< exprt > &assigns, exprt invariant, exprt::operandst decreases, const std::unordered_set< irep_idt > &local, const std::unordered_set< irep_idt > &tracked, std::set< std::size_t > inner_loops, std::set< std::size_t > outer_loops, symbol_exprt write_set_var, symbol_exprt addr_of_write_set_var)
const std::size_t loop_id
Loop identifier assigned by DFCC to this loop.
const exprt invariant
Loop invariant expression.
const std::set< std::size_t > outer_loops
Integer identifier of the outer loop(s) if they exists.
const std::set< std::size_t > inner_loops
Integer identifiers of inner loops of that loop.
optionalt< goto_programt::targett > find_latch(goto_programt &goto_program) const
const symbol_exprt write_set_var
Symbol representing the stack-allocated write set object for this loop.
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
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Expression to hold a symbol (variable)
Definition std_expr.h:113
The symbol table base class interface.
Enumeration representing the instrumentation mode for loop contracts.
dfcc_loop_contract_modet
Enumeration representing the instrumentation mode for loop contracts.
Concrete Goto Program.
API to expression classes.
Author: Diffblue Ltd.