CBMC
dfcc_spec_functions.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dynamic frame condition checking
4 
5 Author: Remi Delmas, delmarsd@amazon.com
6 
7 \*******************************************************************/
8 
9 #include "dfcc_spec_functions.h"
11 
12 #include <util/format_expr.h>
13 #include <util/namespace.h>
14 
16 
17 #include <langapi/language_util.h>
18 
19 #include "dfcc_library.h"
20 
22  goto_modelt &goto_model,
23  message_handlert &message_handler,
24  dfcc_libraryt &library)
25  : goto_model(goto_model),
26  message_handler(message_handler),
27  log(message_handler),
28  library(library),
29  ns(goto_model.symbol_table)
30 {
31 }
32 
34 {
35  INVARIANT(
36  expr.id() == ID_typecast && expr.type().id() == ID_pointer &&
37  expr.operands().at(0).id() == ID_address_of,
38  "target expression must be of the form `cast(address_of(target), empty*)`");
39 
40  return expr.operands().at(0).operands().at(0).type();
41 }
42 
44  const irep_idt &function_id,
45  const irep_idt &havoc_function_id,
46  std::size_t &nof_targets)
47 {
48  INVARIANT(
49  !goto_model.symbol_table.has_symbol(havoc_function_id),
50  "DFCC: havoc function id '" + id2string(havoc_function_id) +
51  "' already exists");
52 
53  const auto &function_symbol =
55 
56  // create the code type that goes on the function symbol
57  const typet &write_set_param_type =
59  code_typet::parametert write_set_param{write_set_param_type};
60  code_typet havoc_code_type({std::move(write_set_param)}, empty_typet());
61 
62  // create the havoc function symbol
63  symbolt havoc_function_symbol;
64  havoc_function_symbol.base_name = havoc_function_id;
65  havoc_function_symbol.name = havoc_function_id;
66  havoc_function_symbol.pretty_name = havoc_function_id;
67  havoc_function_symbol.type = havoc_code_type;
68  havoc_function_symbol.mode = function_symbol.mode;
69  havoc_function_symbol.module = function_symbol.module;
70  havoc_function_symbol.location = function_symbol.location;
71  havoc_function_symbol.set_compiled();
72  bool add_function_failed = goto_model.symbol_table.add(havoc_function_symbol);
73  INVARIANT(
74  !add_function_failed,
75  "DFCC: could not insert havoc function '" + id2string(havoc_function_id) +
76  "' in the symbol table");
77 
78  // create the write_set symbol used as input by the havoc function
79  const auto &write_set_symbol = dfcc_utilst::create_new_parameter_symbol(
81  havoc_function_id,
82  "__write_set_to_havoc",
83  write_set_param_type);
85  goto_model.symbol_table.get_writeable_ref(havoc_function_id).type)
86  .parameters()[0]
87  .set_identifier(write_set_symbol.name);
88 
89  // create new goto_function
90  goto_functiont dummy_havoc_function;
91  dummy_havoc_function.parameter_identifiers = {write_set_symbol.name};
92  goto_model.goto_functions.function_map[havoc_function_id].copy_from(
93  dummy_havoc_function);
94 
95  // body will be filled with instructions
96  auto &havoc_program =
97  goto_model.goto_functions.function_map.at(havoc_function_id).body;
98 
99  const goto_programt &original_program =
100  goto_model.goto_functions.function_map.at(function_id).body;
101 
103  havoc_function_id,
104  original_program,
105  write_set_symbol.symbol_expr(),
106  havoc_program,
107  nof_targets);
108 
109  havoc_program.add(goto_programt::make_end_function());
110 
112 
113  std::set<irep_idt> no_body;
114  std::set<irep_idt> missing_function;
115  std::set<irep_idt> recursive_call;
116  std::set<irep_idt> not_enough_arguments;
118  goto_model,
119  havoc_function_id,
120  no_body,
121  recursive_call,
122  missing_function,
123  not_enough_arguments,
125  INVARIANT(
126  no_body.empty(),
127  "no body warnings when inlining " + id2string(havoc_function_id));
128  INVARIANT(
129  missing_function.empty(),
130  "missing function warnings when inlining " + id2string(havoc_function_id));
131  INVARIANT(
132  recursive_call.empty(),
133  "recursive calls when inlining " + id2string(havoc_function_id));
134  INVARIANT(
135  not_enough_arguments.empty(),
136  "not enough arguments when inlining " + id2string(havoc_function_id));
137 
138  goto_model.goto_functions.function_map.at(havoc_function_id).make_hidden();
139 
141 }
142 
144  const irep_idt &function_id,
145  const goto_programt &original_program,
146  const exprt &write_set_to_havoc,
147  goto_programt &havoc_program,
148  std::size_t &nof_targets)
149 {
150  // index of the CAR to havoc in the write set
151  std::size_t next_idx = 0;
152 
153  // iterate on the body of the original function and emit one havoc instruction
154  // per target
155  forall_goto_program_instructions(ins_it, original_program)
156  {
157  if(ins_it->is_function_call())
158  {
159  if(ins_it->call_function().id() != ID_symbol)
160  {
162  "Function pointer calls are not supported in assigns clauses: '" +
163  from_expr(ns, function_id, ins_it->call_function()) +
164  "' called in function '" + id2string(function_id) + "'",
165  ins_it->source_location());
166  }
167 
168  const irep_idt &callee_id =
169  to_symbol_expr(ins_it->call_function()).get_identifier();
170 
171  // Only process built-in functions that represent assigns clause targets,
172  // and error-out on any other function call
173 
174  // Find the corresponding instrumentation hook
175  auto hook_opt = library.get_havoc_hook(callee_id);
176  INVARIANT(
177  hook_opt.has_value(),
178  "dfcc_spec_functionst::generate_havoc_instructions: function calls "
179  "must be inlined before calling this function");
180 
181  // Use same source location as original call
182  source_locationt location(ins_it->source_location());
183  auto hook = hook_opt.value();
184  code_function_callt call(
185  library.dfcc_fun_symbol.at(hook).symbol_expr(),
186  {write_set_to_havoc, from_integer(next_idx, size_type())});
187 
189  {
190  // ```
191  // DECL __havoc_target;
192  // CALL __havoc_target = havoc_hook(set, next_idx);
193  // IF !__havoc_target GOTO label;
194  // ASSIGN *__havoc_target = nondet(target_type);
195  // label: DEAD __havoc_target;
196  // ```
197  // declare a local var to store targets havoced via nondet assignment
198  auto &target_type = get_target_type(ins_it->call_arguments().at(0));
199 
200  const auto target_expr = dfcc_utilst::create_symbol(
202  pointer_type(target_type),
203  function_id,
204  "__havoc_target",
205  location);
206 
207  havoc_program.add(goto_programt::make_decl(target_expr, location));
208 
209  call.lhs() = target_expr;
210  havoc_program.add(goto_programt::make_function_call(call, location));
211 
212  auto goto_instruction =
214  dfcc_utilst::make_null_check_expr(target_expr), location));
215 
216  // create nondet assignment to the target
217  side_effect_expr_nondett nondet(target_type, location);
218  havoc_program.add(goto_programt::make_assignment(
220  target_expr, pointer_type(target_type))},
221  nondet,
222  location));
223  auto label =
224  havoc_program.add(goto_programt::make_dead(target_expr, location));
225  goto_instruction->complete_goto(label);
226  }
227  else if(
230  {
231  // ```
232  // CALL havoc_hook(set, next_idx);
233  // ```
234  havoc_program.add(goto_programt::make_function_call(call, location));
235  }
236  else
237  {
238  UNREACHABLE;
239  }
240  ++next_idx;
241  }
242  }
243  nof_targets = next_idx;
244 }
245 
247  const irep_idt &function_id,
248  std::size_t &nof_targets)
249 {
250  auto &goto_function = goto_model.goto_functions.function_map.at(function_id);
251 
252  // add write_set parameter
253  const exprt write_set_to_fill =
255  goto_model,
256  function_id,
257  "__write_set_to_fill",
259  .symbol_expr();
260 
262  write_set_to_fill,
264  goto_function.body,
265  nof_targets);
266 
268 
269  goto_model.goto_functions.function_map.at(function_id).make_hidden();
270 }
271 
273  const exprt &write_set_to_fill,
274  const irep_idt &language_mode,
275  goto_programt &program,
276  std::size_t &nof_targets)
277 {
278  // counts the number of calls to built-ins to get an over approximation
279  // of the size of the set
280  std::size_t next_idx = 0;
281 
282  // rewrite calls
283  Forall_goto_program_instructions(ins_it, program)
284  {
285  if(ins_it->is_function_call())
286  {
287  if(ins_it->call_function().id() != ID_symbol)
288  {
290  "Function pointer calls are not supported in assigns clauses '" +
291  from_expr_using_mode(ns, language_mode, ins_it->call_function()) +
292  "'",
293  ins_it->source_location());
294  }
295 
296  const irep_idt &callee_id =
297  to_symbol_expr(ins_it->call_function()).get_identifier();
298 
299  // Only process built-in functions that specify assignable targets
300  // and error-out on any other function call
301 
302  // Find the corresponding instrumentation hook
303  INVARIANT(
304  library.is_front_end_builtin(callee_id),
305  "dfcc_spec_functionst::to_spec_assigns_function: function calls must "
306  "be inlined before calling this function");
307 
308  auto hook = library.get_hook(callee_id);
309  // redirect the call to the hook
310  ins_it->call_function() = library.dfcc_fun_symbol.at(hook).symbol_expr();
311  // insert insertion index argument
312  ins_it->call_arguments().insert(
313  ins_it->call_arguments().begin(), from_integer(next_idx, size_type()));
314  // insert write set argument
315  ins_it->call_arguments().insert(
316  ins_it->call_arguments().begin(), write_set_to_fill);
317 
318  // remove the is_pointer_to_pointer argument which is not used in the
319  // hook for insert assignable
321  ins_it->call_arguments().pop_back();
322 
323  ++next_idx;
324  }
325  }
326  nof_targets = next_idx;
327 }
328 
330  const irep_idt &function_id,
331  std::size_t &nof_targets)
332 {
333  auto &goto_function = goto_model.goto_functions.function_map.at(function_id);
334 
335  // add __dfcc_set parameter
336  const exprt &write_set_to_fill =
338  goto_model,
339  function_id,
340  "__write_set_to_fill",
342  .symbol_expr();
343 
345  write_set_to_fill,
347  goto_function.body,
348  nof_targets);
349 
351 
352  goto_model.goto_functions.function_map.at(function_id).make_hidden();
353 }
354 
356  const exprt &write_set_to_fill,
357  const irep_idt &language_mode,
358  goto_programt &program,
359  std::size_t &nof_targets)
360 {
361  // counts the number of calls to the `freeable` builtin
362  std::size_t next_idx = 0;
363  Forall_goto_program_instructions(ins_it, program)
364  {
365  if(ins_it->is_function_call())
366  {
367  if(ins_it->call_function().id() != ID_symbol)
368  {
370  "Function pointer calls are not supported in frees clauses: '" +
371  from_expr_using_mode(ns, language_mode, ins_it->call_function()) +
372  "'",
373  ins_it->source_location());
374  }
375 
376  const irep_idt &callee_id =
377  to_symbol_expr(ins_it->call_function()).get_identifier();
378 
379  // only process the built-in `freeable` function
380  // error out on any other function call
381  INVARIANT(
382  callee_id == CPROVER_PREFIX "freeable",
383  "dfcc_spec_functionst::to_spec_frees_function: function calls must "
384  "be inlined before calling this function");
385 
386  ins_it->call_function() =
388  .symbol_expr();
389  ins_it->call_arguments().insert(
390  ins_it->call_arguments().begin(), write_set_to_fill);
391  ++next_idx;
392  }
393  }
394 
395  nof_targets = next_idx;
396 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:235
goto_instruction_codet representation of a function call statement.
Base type of functions.
Definition: std_types.h:583
const parameterst & parameters() const
Definition: std_types.h:699
Operator to dereference a pointer.
Definition: pointer_expr.h:834
Class interface to library types and functions defined in cprover_contracts.c.
Definition: dfcc_library.h:154
bool is_front_end_builtin(const irep_idt &function_id) const
Returns true iff the given function_id is one of __CPROVER_assignable, __CPROVER_object_whole,...
dfcc_funt get_hook(const irep_idt &function_id) const
Returns the library instrumentation hook for the given front-end function.
std::map< dfcc_typet, typet > dfcc_type
Maps enum values to the actual types (dynamically loaded)
Definition: dfcc_library.h:214
std::map< dfcc_funt, symbolt > dfcc_fun_symbol
Maps enum values to the actual function symbols (dynamically loaded)
Definition: dfcc_library.h:217
std::optional< dfcc_funt > get_havoc_hook(const irep_idt &function_id) const
Returns the library instrumentation hook for the given built-in.
void to_spec_assigns_function(const irep_idt &function_id, std::size_t &nof_targets)
Transforms (in place) a function.
void to_spec_frees_instructions(const exprt &write_set_to_fill, const irep_idt &language_mode, goto_programt &program, std::size_t &nof_targets)
Rewrites in place program expressed in terms of built-ins specifying freeable targets declaratively u...
void generate_havoc_function(const irep_idt &function_id, const irep_idt &havoc_function_id, std::size_t &nof_targets)
From a function:
void generate_havoc_instructions(const irep_idt &function_id, const goto_programt &original_program, const exprt &write_set_to_havoc, goto_programt &havoc_program, std::size_t &nof_targets)
Translates original_program that specifies assignable targets into a program that havocs the targets.
message_handlert & message_handler
void to_spec_assigns_instructions(const exprt &write_set_to_fill, const irep_idt &language_mode, goto_programt &program, std::size_t &nof_targets)
Rewrites in place program expressed in terms of built-ins specifying assignable targets declaratively...
const typet & get_target_type(const exprt &expr)
Extracts the type of an assigns clause target expression The expression must be of the form: expr = c...
dfcc_spec_functionst(goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library)
void to_spec_frees_function(const irep_idt &function_id, std::size_t &nof_targets)
Transforms (in place) a function.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
The empty type.
Definition: std_types.h:51
Base class for all expressions.
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:84
operandst & operands()
Definition: expr.h:94
function_mapt function_map
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
Definition: goto_function.h:33
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:971
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:739
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:964
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
Thrown when we can't handle something in an input source file.
const irep_idt & id() const
Definition: irep.h:388
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1520
const irep_idt & get_identifier() const
Definition: std_expr.h:160
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt mode
Language mode.
Definition: symbol.h:49
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2081
The type of an expression, extends irept.
Definition: type.h:29
#define CPROVER_PREFIX
Dynamic frame condition checking library loading.
@ WRITE_SET_INSERT_ASSIGNABLE
@ WRITE_SET_HAVOC_SLICE
@ WRITE_SET_HAVOC_GET_ASSIGNABLE_TARGET
@ WRITE_SET_ADD_FREEABLE
@ WRITE_SET_HAVOC_OBJECT_WHOLE
@ CAR_SET_PTR
type of pointers to sets of CAR
@ WRITE_SET_PTR
type of pointers to descriptors of assignable/freeable sets of locations
Translate functions that specify assignable and freeable targets declaratively into active functions ...
Program Transformation.
Symbol Table + CFG.
#define forall_goto_program_instructions(it, program)
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::string from_expr_using_mode(const namespacet &ns, const irep_idt &mode, const exprt &expr)
Formats an expression using the given namespace, using the given mode to retrieve the language printe...
double log(double x)
Definition: math.c:2776
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:788
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
Definition: dfcc_utils.cpp:72
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
static const exprt make_null_check_expr(const exprt &ptr)
Returns the expression expr == NULL.
Definition: dfcc_utils.cpp:406
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
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
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
#define size_type
Definition: unistd.c:347