CBMC
dfcc_utils.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dynamic frame condition checking for function contracts
4 
5 Author: Remi Delmas, delmasrd@amazon.com
6 Date: August 2022
7 
8 \*******************************************************************/
9 
12 
13 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_UTILS_H
14 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_UTILS_H
15 
16 #include <util/message.h>
17 #include <util/namespace.h>
18 #include <util/std_expr.h>
19 
20 #include <set>
21 
22 class goto_modelt;
23 class goto_programt;
24 class message_handlert;
25 class symbolt;
26 
27 struct dfcc_utilst
28 {
30  static bool
31  function_symbol_exists(const goto_modelt &, const irep_idt &function_id);
32  static bool function_symbol_with_body_exists(
33  const goto_modelt &,
34  const irep_idt &function_id);
35 
37  static symbolt &
38  get_function_symbol(symbol_table_baset &, const irep_idt &function_id);
39 
45  static symbol_exprt create_symbol(
46  symbol_table_baset &,
47  const typet &type,
48  const irep_idt &function_id,
49  const std::string &base_name,
50  const source_locationt &source_location);
51 
63  static const symbolt &create_static_symbol(
64  symbol_table_baset &,
65  const typet &type,
66  const std::string &prefix,
67  const std::string &base_name,
68  const source_locationt &source_location,
69  const irep_idt &mode,
70  const irep_idt &module,
71  const exprt &initial_value,
72  const bool no_nondet_initialization = true);
73 
75 #if defined(__GNUC__) && __GNUC__ >= 14
76  [[gnu::no_dangling]]
77 #endif
78  static const symbolt &
79  create_new_parameter_symbol(
80  symbol_table_baset &,
81  const irep_idt &function_id,
82  const std::string &base_name,
83  const typet &type);
84 
88  static void add_parameter(
89  goto_modelt &,
90  const symbolt &symbol,
91  const irep_idt &function_id);
92 
95  static const symbolt &add_parameter(
96  goto_modelt &,
97  const irep_idt &function_id,
98  const std::string &base_name,
99  const typet &type);
100 
107 #if defined(__GNUC__) && __GNUC__ >= 14
108  [[gnu::no_dangling]]
109 #endif
110  static const symbolt &
111  clone_and_rename_function(
112  goto_modelt &goto_model,
113  const irep_idt &function_id,
114  const irep_idt &new_function_id,
115  std::optional<typet> new_return_type);
116 
145  static void wrap_function(
146  goto_modelt &goto_model,
147  const irep_idt &function_id,
148  const irep_idt &wrapped_function_id);
149 
151  static const exprt make_null_check_expr(const exprt &ptr);
152 
154  static exprt make_sizeof_expr(const exprt &expr, const namespacet &);
155 
158  static void inline_function(
159  goto_modelt &goto_model,
160  const irep_idt &function_id,
161  message_handlert &message_handler);
162 
165  static void inline_function(
166  goto_modelt &goto_model,
167  const irep_idt &function_id,
168  std::set<irep_idt> &no_body,
169  std::set<irep_idt> &recursive_call,
170  std::set<irep_idt> &missing_function,
171  std::set<irep_idt> &not_enough_arguments,
172  message_handlert &message_handler);
173 
176  static void inline_program(
177  goto_modelt &goto_model,
178  goto_programt &goto_program,
179  std::set<irep_idt> &no_body,
180  std::set<irep_idt> &recursive_call,
181  std::set<irep_idt> &missing_function,
182  std::set<irep_idt> &not_enough_arguments,
183  message_handlert &message_handler);
184 };
185 
186 #endif
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
exprt
Base class for all expressions.
Definition: expr.h:56
goto_modelt
Definition: goto_model.h:27
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
message_handlert
Definition: message.h:27
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
source_locationt
Definition: source_location.h:20
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:131
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:23
symbolt
Symbol table entry.
Definition: symbol.h:28
typet
The type of an expression, extends irept.
Definition: type.h:29
std_expr.h
API to expression classes.
dfcc_utilst
Definition: dfcc_utils.h:28
dfcc_utilst::get_function_symbol
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
Definition: dfcc_utils.cpp:72
dfcc_utilst::inline_function
static void inline_function(goto_modelt &goto_model, const irep_idt &function_id, message_handlert &message_handler)
Inlines the given function, aborts on recursive calls during inlining.
Definition: dfcc_utils.cpp:443
dfcc_utilst::function_symbol_with_body_exists
static bool function_symbol_with_body_exists(const goto_modelt &, const irep_idt &function_id)
Definition: dfcc_utils.cpp:65
dfcc_utilst::make_null_check_expr
static const exprt make_null_check_expr(const exprt &ptr)
Returns the expression expr == NULL.
Definition: dfcc_utils.cpp:406
dfcc_utilst::function_symbol_exists
static bool function_symbol_exists(const goto_modelt &, const irep_idt &function_id)
Returns true iff the given symbol exists and satisfies requirements.
Definition: dfcc_utils.cpp:58
dfcc_utilst::make_sizeof_expr
static exprt make_sizeof_expr(const exprt &expr, const namespacet &)
Returns the expression sizeof(expr).
Definition: dfcc_utils.cpp:411
dfcc_utilst::create_new_parameter_symbol
static const symbolt & create_new_parameter_symbol(symbol_table_baset &, const irep_idt &function_id, const std::string &base_name, const typet &type)
Creates a new parameter symbol for the given function_id.
Definition: dfcc_utils.cpp:124
dfcc_utilst::wrap_function
static void wrap_function(goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &wrapped_function_id)
Given a function to wrap foo and a new name wrapped_foo
Definition: dfcc_utils.cpp:324
dfcc_utilst::create_static_symbol
static const symbolt & create_static_symbol(symbol_table_baset &, const typet &type, const std::string &prefix, const std::string &base_name, const source_locationt &source_location, const irep_idt &mode, const irep_idt &module, const exprt &initial_value, const bool no_nondet_initialization=true)
Adds a new static symbol named prefix::base_name of type type with value initial_value in the symbol ...
Definition: dfcc_utils.cpp:103
dfcc_utilst::clone_and_rename_function
static const symbolt & clone_and_rename_function(goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &new_function_id, std::optional< typet > new_return_type)
Creates a new function symbol and goto_function entry in the goto_functions_map by cloning the given ...
Definition: dfcc_utils.cpp:300
dfcc_utilst::add_parameter
static void add_parameter(goto_modelt &, const symbolt &symbol, const irep_idt &function_id)
Adds the given symbol as parameter to the function symbol's code_type.
Definition: dfcc_utils.cpp:156
dfcc_utilst::inline_program
static void inline_program(goto_modelt &goto_model, goto_programt &goto_program, std::set< irep_idt > &no_body, std::set< irep_idt > &recursive_call, std::set< irep_idt > &missing_function, std::set< irep_idt > &not_enough_arguments, message_handlert &message_handler)
Inlines the given program, and returns function symbols that caused warnings.
Definition: dfcc_utils.cpp:487
dfcc_utilst::create_symbol
static symbol_exprt create_symbol(symbol_table_baset &, const typet &type, const irep_idt &function_id, const std::string &base_name, const source_locationt &source_location)
Adds a new symbol named function_id::base_name of type type with given attributes in the symbol table...
Definition: dfcc_utils.cpp:81