cprover
Loading...
Searching...
No Matches
dfcc_library.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
9#include "dfcc_library.h"
10
11#include <util/arith_tools.h>
12#include <util/c_types.h>
13#include <util/config.h>
14#include <util/cprover_prefix.h>
15#include <util/message.h>
16#include <util/pointer_expr.h>
18#include <util/std_code.h>
19#include <util/std_expr.h>
20
24
25#include <ansi-c/c_expr.h>
32
33#include "dfcc_utils.h"
34
36template <typename K, typename V>
37std::map<V, K> swap_map(std::map<K, V> const &map)
38{
39 std::map<V, K> result;
40 for(auto const &pair : map)
41 result.insert({pair.second, pair.first});
42 return result;
43}
44
45// NOLINTNEXTLINE(build/deprecated)
46#define CONTRACTS_PREFIX CPROVER_PREFIX "contracts_"
47
49const std::map<dfcc_typet, irep_idt> create_dfcc_type_to_name()
50{
51 return std::map<dfcc_typet, irep_idt>{
58 {dfcc_typet::WRITE_SET_PTR, CONTRACTS_PREFIX "write_set_ptr_t"}};
59}
60
61const std::map<dfcc_funt, irep_idt> create_dfcc_fun_to_name()
62{
63 return {
70 CONTRACTS_PREFIX "obj_set_create_indexed_by_object_id"},
72 CONTRACTS_PREFIX "obj_set_create_append"},
79 CONTRACTS_PREFIX "obj_set_contains_exact"},
83 CONTRACTS_PREFIX "write_set_insert_assignable"},
85 CONTRACTS_PREFIX "write_set_insert_object_whole"},
87 CONTRACTS_PREFIX "write_set_insert_object_from"},
89 CONTRACTS_PREFIX "write_set_insert_object_upto"},
91 CONTRACTS_PREFIX "write_set_add_freeable"},
93 CONTRACTS_PREFIX "write_set_add_allocated"},
94 {dfcc_funt::WRITE_SET_ADD_DECL, CONTRACTS_PREFIX "write_set_add_decl"},
96 CONTRACTS_PREFIX "write_set_record_dead"},
98 CONTRACTS_PREFIX "write_set_record_deallocated"},
100 CONTRACTS_PREFIX "write_set_check_allocated_deallocated_is_empty"},
102 CONTRACTS_PREFIX "write_set_check_assignment"},
104 CONTRACTS_PREFIX "write_set_check_array_set"},
106 CONTRACTS_PREFIX "write_set_check_array_copy"},
108 CONTRACTS_PREFIX "write_set_check_array_replace"},
110 CONTRACTS_PREFIX "write_set_check_havoc_object"},
112 CONTRACTS_PREFIX "write_set_check_deallocate"},
114 CONTRACTS_PREFIX "write_set_check_assigns_clause_inclusion"},
116 CONTRACTS_PREFIX "write_set_check_frees_clause_inclusion"},
118 CONTRACTS_PREFIX "write_set_deallocate_freeable"},
120 CONTRACTS_PREFIX "write_set_havoc_get_assignable_target"},
122 CONTRACTS_PREFIX "write_set_havoc_object_whole"},
124 CONTRACTS_PREFIX "write_set_havoc_slice"},
127 {dfcc_funt::LINK_DEALLOCATED, CONTRACTS_PREFIX "link_deallocated"},
130 CONTRACTS_PREFIX "pointer_in_range_dfcc"},
134 CONTRACTS_PREFIX "check_replace_ensures_was_freed_preconditions"},
135 {dfcc_funt::OBEYS_CONTRACT, CONTRACTS_PREFIX "obeys_contract"}};
136}
137
147
148const std::map<irep_idt, dfcc_funt> create_havoc_hook()
149{
150 return {
151 {CPROVER_PREFIX "assignable",
156}
157
158const std::set<irep_idt> create_assignable_builtin_names()
159{
160 return {
161 CPROVER_PREFIX "assignable",
162 CPROVER_PREFIX "assignable_set_insert_assignable",
163 CPROVER_PREFIX "object_whole",
164 CPROVER_PREFIX "assignable_set_insert_object_whole",
165 CPROVER_PREFIX "object_from",
166 CPROVER_PREFIX "assignable_set_insert_object_from",
167 CPROVER_PREFIX "object_upto",
168 CPROVER_PREFIX "assignable_set_insert_object_upto",
169 CPROVER_PREFIX "freeable",
170 CPROVER_PREFIX "assignable_set_add_freeable"};
171}
172
175 goto_modelt &goto_model,
176 message_handlert &message_handler)
177 : goto_model(goto_model),
178 message_handler(message_handler),
179 log(message_handler),
180 dfcc_type_to_name(create_dfcc_type_to_name()),
181 dfcc_name_to_type(swap_map<dfcc_typet, irep_idt>(dfcc_type_to_name)),
182 dfcc_fun_to_name(create_dfcc_fun_to_name()),
183 dfcc_name_to_fun(swap_map<dfcc_funt, irep_idt>(dfcc_fun_to_name)),
184 dfcc_hook(create_dfcc_hook()),
185 havoc_hook(create_havoc_hook()),
186 assignable_builtin_names(create_assignable_builtin_names())
187{
188 // Add the instrumented map symbol to the symbol table.
190}
191
193bool dfcc_libraryt::is_front_end_builtin(const irep_idt &function_id) const
194{
195 return dfcc_hook.find(function_id) != dfcc_hook.end();
196}
197
200{
202 return dfcc_hook.find(function_id)->second;
203}
204
205// Returns the havoc function to use for a given front-end function
208{
209 auto found = havoc_hook.find(function_id);
210 if(found != havoc_hook.end())
211 return {found->second};
212 else
213 return {};
214}
215
217{
218 sl.add_pragma("disable:pointer-check");
219 sl.add_pragma("disable:pointer-primitive-check");
220 sl.add_pragma("disable:pointer-overflow-check");
221 sl.add_pragma("disable:signed-overflow-check");
222 sl.add_pragma("disable:unsigned-overflow-check");
223 sl.add_pragma("disable:conversion-check");
224 sl.add_pragma("disable:undefined-shift-check");
225}
226
228{
229 for(const auto &pair : dfcc_fun_to_name)
230 {
231 auto &function = goto_model.goto_functions.function_map[pair.second];
232 for(auto &inst : function.body.instructions)
233 {
234 add_checked_pragmas(inst.source_location_nonconst());
235 }
236 }
237}
238
240{
241 std::set<irep_idt> missing;
242
243 // add `malloc` since it is needed used by the `is_fresh` function
244 missing.insert("malloc");
245
246 // add `free` and `__CPROVER_deallocate` since they are used by the
247 // `write_set_deallocate_freeable`
248 missing.insert("free");
249
250 // used by `write_set_release`
251 missing.insert(CPROVER_PREFIX "deallocate");
252
253 // Make sure all front end functions are loaded
254 missing.insert(CPROVER_PREFIX "assignable");
255 missing.insert(CPROVER_PREFIX "object_from");
256 missing.insert(CPROVER_PREFIX "object_upto");
257 missing.insert(CPROVER_PREFIX "object_whole");
258 missing.insert(CPROVER_PREFIX "freeable");
259
260 // go over all library functions
261 for(const auto &pair : dfcc_fun_to_name)
262 {
263 symbol_tablet::symbolst::const_iterator found =
264 goto_model.symbol_table.symbols.find(pair.second);
265
266 if(
268 found->second.value.is_nil())
269 {
270 missing.insert(pair.second);
271 }
272 }
273 return missing;
274}
275
276bool dfcc_libraryt::loaded = false;
277
278void dfcc_libraryt::load(std::set<irep_idt> &to_instrument)
279{
281 !loaded, "the cprover_contracts library can only be loaded once");
282 loaded = true;
283
284 log.status() << "Adding the cprover_contracts library (" << config.ansi_c.arch
285 << ")" << messaget::eom;
286
287 // these will need to get instrumented as well
288 to_instrument.insert("malloc");
289 to_instrument.insert("free");
290 to_instrument.insert(CPROVER_PREFIX "deallocate");
291
292 std::set<irep_idt> to_load;
293
294 // add the whole library
295 to_load.insert(CPROVER_PREFIX "contracts_library");
296
297 // add front end functions
298 to_load.insert(CPROVER_PREFIX "assignable");
299 to_load.insert(CPROVER_PREFIX "object_from");
300 to_load.insert(CPROVER_PREFIX "object_upto");
301 to_load.insert(CPROVER_PREFIX "object_whole");
302 to_load.insert(CPROVER_PREFIX "freeable");
303
304 // add stdlib dependences
305 to_load.insert("malloc");
306 to_load.insert("free");
307 to_load.insert(CPROVER_PREFIX "deallocate");
308
312
313 // compute missing library functions before modifying the symbol table
314 std::set<irep_idt> missing = get_missing_funs();
315
316 // copy all loaded symbols to the main symbol table
317 for(const auto &symbol_pair : tmp_symbol_table.symbols)
318 {
319 const auto &sym = symbol_pair.first;
322 }
323
324 // compile all missing library functions to GOTO
325 for(const auto &id : missing)
326 {
329 }
330
331 // check that all symbols have a goto_implementation
332 // and populate symbol maps
334 for(const auto &pair : dfcc_fun_to_name)
335 {
336 const auto &found =
337 goto_model.goto_functions.function_map.find(pair.second);
338
339 INVARIANT(
341 found->second.body_available(),
342 "The body of DFCC library function " + id2string(pair.second) +
343 " could not be found");
344
345 dfcc_fun_symbol[pair.first] = ns.lookup(pair.second);
346 }
347
348 // populate symbol maps for easy access to symbols during translation
349 for(const auto &pair : dfcc_type_to_name)
350 {
351 dfcc_type[pair.first] = ns.lookup(pair.second).type;
352 }
353
354 // fix malloc and free calls
356
357 // inline the functions that need to be inlined for perf reasons
359
360 // hide all instructions in counter example traces
361 for(auto it : dfcc_fun_symbol)
362 goto_model.goto_functions.function_map.at(it.second.name).make_hidden();
363}
364
366{
367 auto found = dfcc_name_to_fun.find(id);
368 if(found != dfcc_name_to_fun.end())
369 return {found->second};
370 else
371 return {};
372}
373
375{
376 return get_dfcc_fun(id).has_value();
377}
378
383
403
404bool dfcc_libraryt::inlined = false;
405
407{
408 INVARIANT(!inlined, "inline_functions can only be called once");
409 inlined = true;
410 for(const auto &function_id : to_inline)
411 {
414 }
415}
416
426
427bool dfcc_libraryt::specialized = false;
428
430{
431 INVARIANT(
433 "dfcc_libraryt::specialize_functions can only be called once");
434
435 specialized = true;
436 unwindsett unwindset{goto_model};
437 std::list<std::string> loop_names;
438
439 for(const auto &entry : to_unwind)
440 {
441 const auto &function = entry.first;
442 const auto &loop_id = entry.second;
443 std::stringstream stream;
444 stream << id2string(dfcc_fun_to_name.at(function)) << "." << loop_id << ":"
446 const auto &str = stream.str();
447 loop_names.push_back(str);
448 }
449 unwindset.parse_unwindset(loop_names, message_handler);
453}
454
459
462
464{
465 INVARIANT(
467 "dfcc_libraryt::fix_malloc_free_calls can only be called once");
468 malloc_free_fixed = true;
469 for(const auto fun : fix_malloc_free_set)
470 {
473
475 {
476 if(ins->is_function_call())
477 {
478 const auto &function = ins->call_function();
479
480 if(function.id() == ID_symbol)
481 {
482 const irep_idt &fun_name = to_symbol_expr(function).get_identifier();
483
484 if(fun_name == (CONTRACTS_PREFIX "malloc"))
485 to_symbol_expr(ins->call_function()).set_identifier("malloc");
486 else if(fun_name == (CONTRACTS_PREFIX "free"))
487 to_symbol_expr(ins->call_function()).set_identifier("free");
488 }
489 }
490 }
491 }
492}
493
495{
496 // not using assume-false in order not to hinder coverage
497 std::string options = "assert-false";
498 c_object_factory_parameterst object_factory_params;
500 options, object_factory_params, goto_model.symbol_table, message_handler);
501 for(const auto &it : dfcc_hook)
502 {
503 const auto &function_id = it.first;
504 if(goto_model.symbol_table.has_symbol(function_id))
505 {
506 auto &goto_function =
507 goto_model.goto_functions.function_map.at(function_id);
508
509 generate_function_bodies->generate_function_body(
510 goto_function, goto_model.symbol_table, function_id);
511 }
512 }
513}
514
516{
517 const irep_idt map_name = "__dfcc_instrumented_functions";
518
521
522 auto map_type =
524
527 map_type,
528 "",
529 "__dfcc_instrumented_functions",
531 ID_C,
532 "<built-in-library>",
533 array_of_exprt(from_integer(0, map_type.element_type()), map_type),
534 true);
535}
536
556
559 const exprt &max_assigns_clause_size,
561 const exprt &assume_requires_ctx,
562 const exprt &assert_requires_ctx,
563 const exprt &assume_ensures_ctx,
564 const exprt &assert_ensures_ctx,
565 const exprt &allow_allocate,
566 const exprt &allow_deallocate,
567 const source_locationt &source_location)
568{
569 auto function_symbol =
572 auto &arguments = call.arguments();
573 // check that address_of_write_set.type() is dfcc_typet::WRITE_SET_PTR
574 arguments.emplace_back(address_of_write_set);
575 PRECONDITION(max_assigns_clause_size.type() == size_type());
576 arguments.emplace_back(max_assigns_clause_size);
578 arguments.emplace_back(max_frees_clause_size);
579 arguments.push_back(assume_requires_ctx);
580 arguments.push_back(assert_requires_ctx);
581 arguments.push_back(assume_ensures_ctx);
582 arguments.push_back(assert_ensures_ctx);
583 arguments.push_back(allow_allocate);
584 arguments.push_back(allow_deallocate);
585 call.add_source_location() = source_location;
586 return call;
587}
588
591 const exprt &max_assigns_clause_size,
592 const source_locationt &source_location)
593{
596 max_assigns_clause_size,
598 false_exprt(),
599 false_exprt(),
600 false_exprt(),
601 false_exprt(),
602 false_exprt(),
603 false_exprt(),
604 source_location);
605}
606
608 const exprt &write_set_ptr,
609 const source_locationt &source_location)
610{
613 {write_set_ptr});
614 call.add_source_location() = source_location;
615 return call;
616}
617
619 const exprt &write_set_ptr,
620 const exprt &ptr,
621 const source_locationt &source_location)
622{
625 {write_set_ptr, ptr});
626 call.add_source_location() = source_location;
627 return call;
628}
629
631 const exprt &write_set_ptr,
632 const exprt &ptr,
633 const source_locationt &source_location)
634{
637 {write_set_ptr, ptr});
638 call.add_source_location() = source_location;
639 return call;
640}
641
643 const exprt &write_set_ptr,
644 const exprt &ptr,
645 const source_locationt &source_location)
646{
649 {write_set_ptr, ptr});
650 call.add_source_location() = source_location;
651 return call;
652}
653
655 const exprt &write_set_ptr,
656 const exprt &ptr,
657 const source_locationt &source_location)
658{
661 {write_set_ptr, ptr});
662 call.add_source_location() = source_location;
663 return call;
664}
665
668 const exprt &check_var,
669 const exprt &write_set_ptr,
670 const source_locationt &source_location)
671{
673 check_var,
675 .symbol_expr(),
676 {write_set_ptr});
677 call.add_source_location() = source_location;
678 return call;
679}
680
682 const exprt &check_var,
683 const exprt &write_set_ptr,
684 const exprt &ptr,
685 const exprt &size,
686 const source_locationt &source_location)
687{
689 check_var,
691 {write_set_ptr, ptr, size});
692 call.add_source_location() = source_location;
693 return call;
694}
695
697 const exprt &check_var,
698 const exprt &write_set_ptr,
699 const exprt &dest,
700 const source_locationt &source_location)
701{
703 check_var,
705 {write_set_ptr, dest});
706 call.add_source_location() = source_location;
707 return call;
708}
709
711 const exprt &check_var,
712 const exprt &write_set_ptr,
713 const exprt &dest,
714 const source_locationt &source_location)
715{
717 check_var,
719 {write_set_ptr, dest});
720 call.add_source_location() = source_location;
721 return call;
722}
723
725 const exprt &check_var,
726 const exprt &write_set_ptr,
727 const exprt &dest,
728 const exprt &src,
729 const source_locationt &source_location)
730{
732 check_var,
734 {write_set_ptr, dest, src});
735 call.add_source_location() = source_location;
736 return call;
737}
738
740 const exprt &check_var,
741 const exprt &write_set_ptr,
742 const exprt &ptr,
743 const source_locationt &source_location)
744{
746 check_var,
748 {write_set_ptr, ptr});
749 call.add_source_location() = source_location;
750 return call;
751}
752
754 const exprt &check_var,
755 const exprt &write_set_ptr,
756 const exprt &ptr,
757 const source_locationt &source_location)
758{
760 check_var,
762 {write_set_ptr, ptr});
763 call.add_source_location() = source_location;
764 return call;
765}
766
782
798
800 const exprt &write_set_ptr,
802 const source_locationt &source_location)
803{
807 call.add_source_location() = source_location;
808 return call;
809}
810
812 const exprt &write_set_ptr,
814 const source_locationt &source_location)
815{
819 call.add_source_location() = source_location;
820 return call;
821}
822
826 const source_locationt &source_location)
827{
831 call.add_source_location() = source_location;
832 return call;
833}
834
838 const source_locationt &source_location)
839{
843 call.add_source_location() = source_location;
844 return call;
845}
846
849 const exprt &ptr,
850 const exprt &write_set_ptr,
851 const source_locationt &source_location)
852{
855 .symbol_expr(),
856 {ptr, write_set_ptr});
857 call.add_source_location() = source_location;
858 return call;
859}
860
863 const exprt &obj_set_ptr,
864 const source_locationt &source_location)
865{
868 .symbol_expr(),
869 {obj_set_ptr});
870 call.add_source_location() = source_location;
871 return call;
872}
873
875 const exprt &obj_set_ptr,
876 const source_locationt &source_location)
877{
880 call.add_source_location() = source_location;
881 return call;
882}
void cprover_c_library_factory_force_load(const std::set< irep_idt > &functions, symbol_table_baset &symbol_table, message_handlert &message_handler)
Load the requested function symbols from the cprover library and add them to the symbol table regardl...
configt config
Definition config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
API to expression classes that are internal to the C frontend.
unsignedbv_typet size_type()
Definition c_types.cpp:55
unsignedbv_typet unsigned_char_type()
Definition c_types.cpp:132
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Array constructor from single element.
Definition std_expr.h:1498
Arrays with given size.
Definition std_types.h:763
goto_instruction_codet representation of a function call statement.
struct configt::ansi_ct ansi_c
const code_function_callt write_set_record_dead_call(const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_record_dead.
const std::map< irep_idt, dfcc_funt > havoc_hook
Maps front-end functions to library functions giving their havoc semantics.
const code_function_callt write_set_check_allocated_deallocated_is_empty_call(const exprt &check_var, const exprt &write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_allocated_deallocated_is_empty.
const code_function_callt obj_set_create_indexed_by_object_id_call(const exprt &obj_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_obj_set_create_indexed_by_object_id.
static bool inlined
True iff the library functions are inlined.
const std::map< irep_idt, dfcc_funt > dfcc_hook
Maps built-in function names to enums to use for instrumentation.
const code_function_callt write_set_check_assignment_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &ptr, const exprt &size, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_assignment.
static bool loaded
True iff the contracts library symbols are loaded.
dfcc_libraryt(goto_modelt &goto_model, message_handlert &lmessage_handler)
Class constructor.
void fix_malloc_free_calls()
Fixes function calls to malloc and free in library functions.
static bool malloc_free_fixed
True iff the library functions uses of malloc and free are fixed.
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,...
const code_function_callt link_allocated_call(const exprt &write_set_postconditions_ptr, const exprt &write_set_to_link_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_link_allocated.
const code_function_callt write_set_record_deallocated_call(const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_record_deallocated.
const code_function_callt write_set_add_decl_call(const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_add_decl.
void inline_functions()
Inlines library functions that need to be inlined before use.
const code_function_callt write_set_check_array_copy_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &dest, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_array_copy.
const code_function_callt write_set_add_allocated_call(const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_add_allocated.
void add_instrumented_functions_map_init_instructions(const std::set< irep_idt > &instrumented_functions, const source_locationt &source_location, goto_programt &dest)
Generates instructions to initialize the instrumented function map symbol from the given set of instr...
const std::map< dfcc_typet, irep_idt > dfcc_type_to_name
Enum to type name mapping.
const symbolt & get_instrumented_functions_map_symbol()
Returns the "__dfcc_instrumented_functions" symbol or creates it if it does not exist already.
const std::map< dfcc_funt, irep_idt > dfcc_fun_to_name
enum to function name mapping
const std::map< irep_idt, dfcc_funt > dfcc_name_to_fun
const code_function_callt write_set_check_array_set_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &dest, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_array_set.
const code_function_callt write_set_check_array_replace_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &dest, const exprt &src, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_array_replace.
const code_function_callt write_set_release_call(const exprt &write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_release.
void inhibit_front_end_builtins()
Adds an ASSERT(false) body to all front-end functions __CPROVER_object_whole __CPROVER_object_upto __...
const code_function_callt obj_set_release_call(const exprt &obj_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_obj_set_release.
const irep_idt & get_dfcc_fun_name(dfcc_funt fun) const
Returns the name of the given dfcc_funt.
dfcc_funt get_hook(const irep_idt &function_id) const
Returns the library instrumentation hook for the given front-end function.
bool is_dfcc_library_symbol(const irep_idt &id) const
True iff the given id is one of the library symbols.
const code_function_callt write_set_check_deallocate_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_deallocate.
const code_function_callt link_deallocated_call(const exprt &write_set_postconditions_ptr, const exprt &write_set_to_link_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_link_deallocated.
goto_modelt & goto_model
const code_function_callt write_set_check_assigns_clause_inclusion_call(const exprt &check_var, const exprt &reference_write_set_ptr, const exprt &candidate_write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_assigns_clause_inclusion.
const code_function_callt link_is_fresh_call(const exprt &write_set_ptr, const exprt &is_fresh_obj_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_link_is_fresh.
message_handlert & message_handler
std::map< dfcc_typet, typet > dfcc_type
Maps enum values to the actual types (dynamically loaded)
std::set< irep_idt > get_missing_funs()
Collects the names of all library functions currently missing from the goto_model into missing.
const code_function_callt write_set_create_call(const exprt &write_set_ptr, const exprt &contract_assigns_size, const exprt &contract_frees_size, const exprt &assume_requires_ctx, const exprt &assert_requires_ctx, const exprt &assume_ensures_ctx, const exprt &assert_ensures_ctx, const exprt &allow_allocate, const exprt &allow_deallocate, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_create.
const code_function_callt write_set_check_frees_clause_inclusion_call(const exprt &check_var, const exprt &reference_write_set_ptr, const exprt &candidate_write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_frees_clause_inclusion.
optionalt< dfcc_funt > get_dfcc_fun(const irep_idt &id) const
Returns the dfcc_funt that corresponds to the given id if any.
const code_function_callt write_set_check_havoc_object_call(const exprt &check_var, const exprt &write_set_ptr, const exprt &ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_havoc_object.
void disable_checks()
Adds "checked" pragmas to instructions of all library functions instructions.
const code_function_callt check_replace_ensures_was_freed_preconditions_call(const exprt &ptr, const exprt &write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_check_replace_ensures_was_freed_preconditions.
const code_function_callt write_set_deallocate_freeable_call(const exprt &write_set_ptr, const exprt &target_write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_deallocate_freeable.
void specialize(const std::size_t contract_assigns_size_hint)
Specializes the library by unwinding loops in library functions to the given assigns clause size.
optionalt< dfcc_funt > get_havoc_hook(const irep_idt &function_id) const
Returns the library instrumentation hook for the given built-in.
std::map< dfcc_funt, symbolt > dfcc_fun_symbol
Maps enum values to the actual function symbols (dynamically loaded)
void load(std::set< irep_idt > &to_instrument)
After calling this function, all library types and functions are present in the the goto_model.
static bool specialized
True iff the library functions are specialized to a particular contract.
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
typet & type()
Return the type of the expression.
Definition expr.h:84
The Boolean constant false.
Definition std_expr.h:3017
function_mapt function_map
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_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Array index operator.
Definition std_expr.h:1410
An expression denoting infinity.
Definition std_expr.h:3042
static eomt eom
Definition message.h:297
mstreamt & status() const
Definition message.h:414
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition symbol.h:28
#define CPROVER_PREFIX
#define CONTRACTS_PREFIX
const std::map< irep_idt, dfcc_funt > create_havoc_hook()
static const std::set< dfcc_funt > to_inline
set of functions that need to be inlined
const std::map< dfcc_funt, irep_idt > create_dfcc_fun_to_name()
const std::set< irep_idt > create_assignable_builtin_names()
static void add_checked_pragmas(source_locationt &sl)
const std::map< dfcc_typet, irep_idt > create_dfcc_type_to_name()
Creates the enum to type name mapping.
std::map< V, K > swap_map(std::map< K, V > const &map)
Swaps keys and values in a map.
static const std::set< dfcc_funt > fix_malloc_free_set
Set of functions that contain calls to assignable_malloc or assignable_free.
static const std::map< dfcc_funt, int > to_unwind
set of functions that need to be unwound to assigns clause size with corresponding loop identifiers.
const std::map< irep_idt, dfcc_funt > create_dfcc_hook()
Dynamic frame condition checking library loading.
dfcc_funt
One enum value per function defined by the cprover_dfcc.c library file.
@ WRITE_SET_INSERT_OBJECT_UPTO
@ CAR_SET_CONTAINS
@ WRITE_SET_CHECK_ASSIGNMENT
@ WRITE_SET_INSERT_ASSIGNABLE
@ WRITE_SET_CHECK_FREES_CLAUSE_INCLUSION
@ POINTER_IN_RANGE_DFCC
@ OBJ_SET_CREATE_APPEND
@ WRITE_SET_RELEASE
@ WRITE_SET_INSERT_OBJECT_WHOLE
@ WRITE_SET_DEALLOCATE_FREEABLE
@ WRITE_SET_CHECK_ARRAY_REPLACE
@ LINK_DEALLOCATED
@ WRITE_SET_CHECK_HAVOC_OBJECT
@ OBJ_SET_CREATE_INDEXED_BY_OBJECT_ID
@ WRITE_SET_CHECK_DEALLOCATE
@ WRITE_SET_CHECK_ALLOCATED_DEALLOCATED_IS_EMPTY
@ WRITE_SET_CHECK_ARRAY_SET
@ WRITE_SET_RECORD_DEAD
@ WRITE_SET_HAVOC_SLICE
@ WRITE_SET_CHECK_ASSIGNS_CLAUSE_INCLUSION
@ WRITE_SET_HAVOC_GET_ASSIGNABLE_TARGET
@ OBJ_SET_CONTAINS
@ WRITE_SET_CREATE
@ WRITE_SET_CHECK_ARRAY_COPY
@ WRITE_SET_ADD_FREEABLE
@ REPLACE_ENSURES_WAS_FREED_PRECONDITIONS
@ WRITE_SET_ADD_DECL
@ WRITE_SET_RECORD_DEALLOCATED
@ OBJ_SET_CONTAINS_EXACT
@ WRITE_SET_ADD_ALLOCATED
@ WRITE_SET_HAVOC_OBJECT_WHOLE
@ WRITE_SET_INSERT_OBJECT_FROM
dfcc_typet
One enum value per type defined by the cprover_dfcc.c library file.
@ WRITE_SET
type of descriptors of assignable/freeable sets of locations
@ CAR_SET_PTR
type of pointers to sets of CAR
@ CAR_SET
type of sets of CAR
@ OBJ_SET_PTR
type of pointers to sets of object identifiers
@ OBJ_SET
type of sets of object identifiers
@ WRITE_SET_PTR
type of pointers to descriptors of assignable/freeable sets of locations
@ CAR
type of descriptors of conditionally assignable ranges of bytes
Dynamic frame condition checking utility functions.
std::unique_ptr< generate_function_bodiest > generate_function_bodies_factory(const std::string &options, const c_object_factory_parameterst &object_factory_parameters, const symbol_tablet &symbol_table, message_handlert &message_handler)
Create the type that actually generates the functions.
void generate_function_bodies(const std::regex &functions_regex, const generate_function_bodiest &generate_function_body, goto_modelt &model, message_handlert &message_handler)
Generate function bodies with some default behavior: assert-false, assume-false, assert-false-assume-...
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Goto Programs with Functions.
Goto Function.
Symbol Table + CFG.
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
API to expression classes for Pointers.
exprt pointer_object(const exprt &p)
Various predicates over pointers in programs.
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition invariant.h:464
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
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 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 ...
Loop unwinding.
Loop unwinding.