CBMC
Loading...
Searching...
No Matches
dfcc_spec_functions.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking
4
5Author: Remi Delmas, delmarsd@amazon.com
6
7\*******************************************************************/
8
10
11#include <util/arith_tools.h>
12#include <util/c_types.h>
13#include <util/std_code.h>
14
16
18
19#include "dfcc_library.h"
20#include "dfcc_utils.h"
21
23 goto_modelt &goto_model,
24 message_handlert &message_handler,
25 dfcc_libraryt &library)
26 : goto_model(goto_model),
27 message_handler(message_handler),
28 log(message_handler),
29 library(library),
30 ns(goto_model.symbol_table)
31{
32}
33
35{
37 expr.id() == ID_typecast && expr.type().id() == ID_pointer &&
38 expr.operands().at(0).id() == ID_address_of,
39 "target expression must be of the form `cast(address_of(target), empty*)`");
40
41 return expr.operands().at(0).operands().at(0).type();
42}
43
45 const irep_idt &function_id,
47 std::size_t &nof_targets)
48{
51 "DFCC: havoc function id '" + id2string(havoc_function_id) +
52 "' already exists");
53
54 const auto &function_symbol =
56
57 // create the code type that goes on the function symbol
62
63 // create the havoc function symbol
71 havoc_function_symbol.location = function_symbol.location;
72 havoc_function_symbol.set_compiled();
76 "DFCC: could not insert havoc function '" + id2string(havoc_function_id) +
77 "' in the symbol table");
78
79 // create the write_set symbol used as input by the havoc function
83 "__write_set_to_havoc",
87 .parameters()[0]
88 .set_identifier(write_set_symbol.name);
89
90 // create new goto_function
92 dummy_havoc_function.parameter_identifiers = {write_set_symbol.name};
95
96 // body will be filled with instructions
97 auto &havoc_program =
99
101 goto_model.goto_functions.function_map.at(function_id).body;
102
106 write_set_symbol.symbol_expr(),
110
112
114
115 std::set<irep_idt> no_body;
116 std::set<irep_idt> missing_function;
117 std::set<irep_idt> recursive_call;
118 std::set<irep_idt> not_enough_arguments;
122 no_body,
127 INVARIANT(
128 no_body.empty(),
129 "no body warnings when inlining " + id2string(havoc_function_id));
130 INVARIANT(
131 missing_function.empty(),
132 "missing function warnings when inlining " + id2string(havoc_function_id));
133 INVARIANT(
134 recursive_call.empty(),
135 "recursive calls when inlining " + id2string(havoc_function_id));
136 INVARIANT(
137 not_enough_arguments.empty(),
138 "not enough arguments when inlining " + id2string(havoc_function_id));
139
141
143}
144
146 const irep_idt &function_id,
151 std::size_t &nof_targets)
152{
153 // index of the CAR to havoc in the write set
154 std::size_t next_idx = 0;
155
156 // iterate on the body of the original function and emit one havoc instruction
157 // per target
159 {
160 if(ins_it->is_function_call())
161 {
162 if(ins_it->call_function().id() != ID_symbol)
163 {
165 "Function pointer calls are not supported in assigns clauses: '" +
166 from_expr(ns, function_id, ins_it->call_function()) +
167 "' called in function '" + id2string(function_id) + "'",
168 ins_it->source_location());
169 }
170
171 const irep_idt &callee_id =
172 to_symbol_expr(ins_it->call_function()).get_identifier();
173
174 // Only process built-in functions that represent assigns clause targets,
175 // and error-out on any other function call
176
177 // Find the corresponding instrumentation hook
179 INVARIANT(
180 hook_opt.has_value(),
181 "dfcc_spec_functionst::generate_havoc_instructions: function calls "
182 "must be inlined before calling this function");
183
184 // Use same source location as original call
185 source_locationt location(ins_it->source_location());
186 auto hook = hook_opt.value();
188 library.dfcc_fun_symbol.at(hook).symbol_expr(),
189 {write_set_to_havoc, from_integer(next_idx, size_type())});
190
192 {
193 // ```
194 // DECL __havoc_target;
195 // CALL __havoc_target = havoc_hook(set, next_idx);
196 // IF !__havoc_target GOTO label;
197 // .... add code for scalar or pointer targets ...
198 // label:
199 // DEAD __havoc_target;
200 // ```
201 // declare a local var to store targets havoced via nondet assignment
202 auto &target_type = get_target_type(ins_it->call_arguments().at(0));
203
206 pointer_type(target_type),
207 function_id,
208 "__havoc_target",
209 location);
210
212
213 call.lhs() = target_expr;
215
216 auto goto_instruction =
219
220 if(
222 target_type.id() == ID_pointer)
223 {
224 // ```
225 // DECL *__invalid_ptr;
226 // ASSIGN *__havoc_target = __invalid_ptr;
227 // DEAD __invalid_ptr;
228 // ```
231 target_type,
232 function_id,
233 "__invalid_ptr",
234 location);
235
238 target_expr, pointer_type(target_type))},
240 location));
241 havoc_program.add(
243 }
244 else
245 {
246 // ```
247 // ASSIGN *__havoc_target = nondet(target_type);
248 // ```
249 side_effect_expr_nondett nondet(target_type, location);
252 target_expr, pointer_type(target_type))},
253 nondet,
254 location));
255 }
256 auto label =
258 goto_instruction->complete_goto(label);
259 }
260 else if(
263 {
264 // ```
265 // CALL havoc_hook(set, next_idx);
266 // ```
268 }
269 else
270 {
272 }
273 ++next_idx;
274 }
275 }
277}
278
280 const irep_idt &function_id,
281 std::size_t &nof_targets)
282{
283 auto &goto_function = goto_model.goto_functions.function_map.at(function_id);
284
285 // add write_set parameter
289 function_id,
290 "__write_set_to_fill",
292 .symbol_expr();
293
297 goto_function.body,
299
301
302 goto_model.goto_functions.function_map.at(function_id).make_hidden();
303}
304
307 const irep_idt &language_mode,
308 goto_programt &program,
309 std::size_t &nof_targets)
310{
311 // counts the number of calls to built-ins to get an over approximation
312 // of the size of the set
313 std::size_t next_idx = 0;
314
315 // rewrite calls
317 {
318 if(ins_it->is_function_call())
319 {
320 if(ins_it->call_function().id() != ID_symbol)
321 {
323 "Function pointer calls are not supported in assigns clauses '" +
324 from_expr_using_mode(ns, language_mode, ins_it->call_function()) +
325 "'",
326 ins_it->source_location());
327 }
328
329 const irep_idt &callee_id =
330 to_symbol_expr(ins_it->call_function()).get_identifier();
331
332 // Only process built-in functions that specify assignable targets
333 // and error-out on any other function call
334
335 // Find the corresponding instrumentation hook
336 INVARIANT(
338 "dfcc_spec_functionst::to_spec_assigns_function: function calls must "
339 "be inlined before calling this function");
340
342 // redirect the call to the hook
343 ins_it->call_function() = library.dfcc_fun_symbol.at(hook).symbol_expr();
344 // insert insertion index argument
345 ins_it->call_arguments().insert(
346 ins_it->call_arguments().begin(), from_integer(next_idx, size_type()));
347 // insert write set argument
348 ins_it->call_arguments().insert(
349 ins_it->call_arguments().begin(), write_set_to_fill);
350
351 // remove the is_pointer_to_pointer argument which is not used in the
352 // hook for insert assignable
354 ins_it->call_arguments().pop_back();
355
356 ++next_idx;
357 }
358 }
360}
361
363 const irep_idt &function_id,
364 std::size_t &nof_targets)
365{
366 auto &goto_function = goto_model.goto_functions.function_map.at(function_id);
367
368 // add __dfcc_set parameter
369 const exprt &write_set_to_fill =
372 function_id,
373 "__write_set_to_fill",
375 .symbol_expr();
376
380 goto_function.body,
382
384
385 goto_model.goto_functions.function_map.at(function_id).make_hidden();
386}
387
390 const irep_idt &language_mode,
391 goto_programt &program,
392 std::size_t &nof_targets)
393{
394 // counts the number of calls to the `freeable` builtin
395 std::size_t next_idx = 0;
397 {
398 if(ins_it->is_function_call())
399 {
400 if(ins_it->call_function().id() != ID_symbol)
401 {
403 "Function pointer calls are not supported in frees clauses: '" +
404 from_expr_using_mode(ns, language_mode, ins_it->call_function()) +
405 "'",
406 ins_it->source_location());
407 }
408
409 const irep_idt &callee_id =
410 to_symbol_expr(ins_it->call_function()).get_identifier();
411
412 // only process the built-in `freeable` function
413 // error out on any other function call
414 INVARIANT(
415 callee_id == CPROVER_PREFIX "freeable",
416 "dfcc_spec_functionst::to_spec_frees_function: function calls must "
417 "be inlined before calling this function");
418
419 ins_it->call_function() =
421 .symbol_expr();
422 ins_it->call_arguments().insert(
423 ins_it->call_arguments().begin(), write_set_to_fill);
424 ++next_idx;
425 }
426 }
427
429}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
goto_instruction_codet representation of a function call statement.
Base type of functions.
Definition std_types.h:583
Operator to dereference a pointer.
Class interface to library types and functions defined in cprover_contracts.c.
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)
std::map< dfcc_funt, symbolt > dfcc_fun_symbol
Maps enum values to the actual function symbols (dynamically loaded)
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)
Generates the havoc function for a function contract.
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...
void generate_havoc_instructions(const irep_idt &function_id, const goto_programt &original_program, const exprt &write_set_to_havoc, dfcc_ptr_havoc_modet ptr_havoc_mode, goto_programt &havoc_program, std::size_t &nof_targets)
Translates original_program that specifies assignable targets into a program that havocs the targets.
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...
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.
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
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.
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
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
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
typet type
Type of symbol.
Definition symbol.h:31
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 ...
dfcc_ptr_havoc_modet
Represents the different ways to havoc pointers.
@ INVALID
havocs the pointer to an invalid pointer
Dynamic frame condition checking utility functions.
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:2449
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
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.
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.
static const exprt make_null_check_expr(const exprt &ptr)
Returns the expression expr == NULL.
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.
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.
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...
#define size_type
Definition unistd.c:186