cprover
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
11
12#include <util/format_expr.h>
13#include <util/namespace.h>
14
16
18
19#include "dfcc_library.h"
20
32
34{
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{
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 =
54 dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id);
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);
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(
80 goto_model.symbol_table,
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(),
107 havoc_program,
108 nof_targets);
109
110 havoc_program.add(goto_programt::make_end_function());
111
112 goto_model.goto_functions.update();
113
114 std::set<irep_idt> no_body;
115 std::set<irep_idt> missing_function;
116 std::set<irep_idt> recursive_call;
117 std::set<irep_idt> not_enough_arguments;
120 havoc_function_id,
121 no_body,
122 recursive_call,
123 missing_function,
124 not_enough_arguments,
126 INVARIANT(
127 no_body.empty(),
128 "no body warnings when inlining " + id2string(havoc_function_id));
129 INVARIANT(
130 missing_function.empty(),
131 "missing function warnings when inlining " + id2string(havoc_function_id));
132 INVARIANT(
133 recursive_call.empty(),
134 "recursive calls when inlining " + id2string(havoc_function_id));
135 INVARIANT(
136 not_enough_arguments.empty(),
137 "not enough arguments when inlining " + id2string(havoc_function_id));
138
139 goto_model.goto_functions.function_map.at(havoc_function_id).make_hidden();
140
141 goto_model.goto_functions.update();
142}
143
145 const irep_idt &function_id,
146 const goto_programt &original_program,
147 const exprt &write_set_to_havoc,
148 dfcc_ptr_havoc_modet ptr_havoc_mode,
149 goto_programt &havoc_program,
150 std::size_t &nof_targets)
151{
152 // index of the CAR to havoc in the write set
153 std::size_t next_idx = 0;
154
155 // iterate on the body of the original function and emit one havoc instruction
156 // per target
157 forall_goto_program_instructions(ins_it, original_program)
158 {
159 if(ins_it->is_function_call())
160 {
161 if(ins_it->call_function().id() != ID_symbol)
162 {
164 "Function pointer calls are not supported in assigns clauses: '" +
165 from_expr(ns, function_id, ins_it->call_function()) +
166 "' called in function '" + id2string(function_id) + "'",
167 ins_it->source_location());
168 }
169
170 const irep_idt &callee_id =
171 to_symbol_expr(ins_it->call_function()).get_identifier();
172
173 // Only process built-in functions that represent assigns clause targets,
174 // and error-out on any other function call
175
176 // Find the corresponding instrumentation hook
177 auto hook_opt = library.get_havoc_hook(callee_id);
178 INVARIANT(
179 hook_opt.has_value(),
180 "dfcc_spec_functionst::generate_havoc_instructions: function calls "
181 "must be inlined before calling this function");
182
183 // Use same source location as original call
184 source_locationt location(ins_it->source_location());
185 auto hook = hook_opt.value();
187 library.dfcc_fun_symbol.at(hook).symbol_expr(),
188 {write_set_to_havoc, from_integer(next_idx, size_type())});
189
191 {
192 // ```
193 // DECL __havoc_target;
194 // CALL __havoc_target = havoc_hook(set, next_idx);
195 // IF !__havoc_target GOTO label;
196 // .... add code for scalar or pointer targets ...
197 // label:
198 // DEAD __havoc_target;
199 // ```
200 // declare a local var to store targets havoced via nondet assignment
201 auto &target_type = get_target_type(ins_it->call_arguments().at(0));
202
203 const auto target_expr = dfcc_utilst::create_symbol(
204 goto_model.symbol_table,
205 pointer_type(target_type),
206 function_id,
207 "__havoc_target",
208 location);
209
210 havoc_program.add(goto_programt::make_decl(target_expr, location));
211
212 call.lhs() = target_expr;
213 havoc_program.add(goto_programt::make_function_call(call, location));
214
215 auto goto_instruction =
217 dfcc_utilst::make_null_check_expr(target_expr), location));
218
219 if(
220 ptr_havoc_mode == dfcc_ptr_havoc_modet::INVALID &&
221 target_type.id() == ID_pointer)
222 {
223 // ```
224 // DECL *__invalid_ptr;
225 // ASSIGN *__havoc_target = __invalid_ptr;
226 // DEAD __invalid_ptr;
227 // ```
228 const auto invalid_ptr_expr = dfcc_utilst::create_symbol(
229 goto_model.symbol_table,
230 target_type,
231 function_id,
232 "__invalid_ptr",
233 location);
234
237 target_expr, pointer_type(target_type))},
238 invalid_ptr_expr,
239 location));
240 havoc_program.add(
241 goto_programt::make_dead(invalid_ptr_expr, location));
242 }
243 else
244 {
245 // ```
246 // ASSIGN *__havoc_target = nondet(target_type);
247 // ```
248 side_effect_expr_nondett nondet(target_type, location);
251 target_expr, pointer_type(target_type))},
252 nondet,
253 location));
254 }
255 auto label =
256 havoc_program.add(goto_programt::make_dead(target_expr, location));
257 goto_instruction->complete_goto(label);
258 }
259 else if(
262 {
263 // ```
264 // CALL havoc_hook(set, next_idx);
265 // ```
266 havoc_program.add(goto_programt::make_function_call(call, location));
267 }
268 else
269 {
271 }
272 ++next_idx;
273 }
274 }
275 nof_targets = next_idx;
276}
277
279 const irep_idt &function_id,
280 std::size_t &nof_targets)
281{
282 auto &goto_function = goto_model.goto_functions.function_map.at(function_id);
283
284 // add write_set parameter
285 const exprt write_set_to_fill =
288 function_id,
289 "__write_set_to_fill",
291 .symbol_expr();
292
294 write_set_to_fill,
295 dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id).mode,
296 goto_function.body,
297 nof_targets);
298
299 goto_model.goto_functions.update();
300
301 goto_model.goto_functions.function_map.at(function_id).make_hidden();
302}
303
305 const exprt &write_set_to_fill,
306 const irep_idt &language_mode,
307 goto_programt &program,
308 std::size_t &nof_targets)
309{
310 // counts the number of calls to built-ins to get an over approximation
311 // of the size of the set
312 std::size_t next_idx = 0;
313
314 // rewrite calls
315 Forall_goto_program_instructions(ins_it, program)
316 {
317 if(ins_it->is_function_call())
318 {
319 if(ins_it->call_function().id() != ID_symbol)
320 {
322 "Function pointer calls are not supported in assigns clauses '" +
323 from_expr_using_mode(ns, language_mode, ins_it->call_function()) +
324 "'",
325 ins_it->source_location());
326 }
327
328 const irep_idt &callee_id =
329 to_symbol_expr(ins_it->call_function()).get_identifier();
330
331 // Only process built-in functions that specify assignable targets
332 // and error-out on any other function call
333
334 // Find the corresponding instrumentation hook
335 INVARIANT(
336 library.is_front_end_builtin(callee_id),
337 "dfcc_spec_functionst::to_spec_assigns_function: function calls must "
338 "be inlined before calling this function");
339
340 auto hook = library.get_hook(callee_id);
341 // redirect the call to the hook
342 ins_it->call_function() = library.dfcc_fun_symbol.at(hook).symbol_expr();
343 // insert insertion index argument
344 ins_it->call_arguments().insert(
345 ins_it->call_arguments().begin(), from_integer(next_idx, size_type()));
346 // insert write set argument
347 ins_it->call_arguments().insert(
348 ins_it->call_arguments().begin(), write_set_to_fill);
349
350 // remove the is_pointer_to_pointer argument which is not used in the
351 // hook for insert assignable
353 ins_it->call_arguments().pop_back();
354
355 ++next_idx;
356 }
357 }
358 nof_targets = next_idx;
359}
360
362 const irep_idt &function_id,
363 std::size_t &nof_targets)
364{
365 auto &goto_function = goto_model.goto_functions.function_map.at(function_id);
366
367 // add __dfcc_set parameter
368 const exprt &write_set_to_fill =
371 function_id,
372 "__write_set_to_fill",
374 .symbol_expr();
375
377 write_set_to_fill,
378 dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id).mode,
379 goto_function.body,
380 nof_targets);
381
382 goto_model.goto_functions.update();
383
384 goto_model.goto_functions.function_map.at(function_id).make_hidden();
385}
386
388 const exprt &write_set_to_fill,
389 const irep_idt &language_mode,
390 goto_programt &program,
391 std::size_t &nof_targets)
392{
393 // counts the number of calls to the `freeable` builtin
394 std::size_t next_idx = 0;
395 Forall_goto_program_instructions(ins_it, program)
396 {
397 if(ins_it->is_function_call())
398 {
399 if(ins_it->call_function().id() != ID_symbol)
400 {
402 "Function pointer calls are not supported in frees clauses: '" +
403 from_expr_using_mode(ns, language_mode, ins_it->call_function()) +
404 "'",
405 ins_it->source_location());
406 }
407
408 const irep_idt &callee_id =
409 to_symbol_expr(ins_it->call_function()).get_identifier();
410
411 // only process the built-in `freeable` function
412 // error out on any other function call
413 INVARIANT(
414 callee_id == CPROVER_PREFIX "freeable",
415 "dfcc_spec_functionst::to_spec_frees_function: function calls must "
416 "be inlined before calling this function");
417
418 ins_it->call_function() =
420 .symbol_expr();
421 ins_it->call_arguments().insert(
422 ins_it->call_arguments().begin(), write_set_to_fill);
423 ++next_idx;
424 }
425 }
426
427 nof_targets = next_idx;
428}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
unsignedbv_typet size_type()
Definition c_types.cpp:50
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.
Class interface to library types and functions defined in cprover_contracts.c.
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.
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
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
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.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
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
const irep_idt & get_identifier() const
Definition std_expr.h:160
Symbol table entry.
Definition symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition symbol.h:46
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
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...
#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...
dstringt irep_idt