CBMC
dfcc_library.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_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 
23 
24 #include <ansi-c/c_expr.h>
26 #include <ansi-c/cprover_library.h>
29 #include <goto-instrument/unwind.h>
32 
33 #include "dfcc_utils.h"
34 
36 template <typename K, typename V>
37 std::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 
49 const std::map<dfcc_typet, irep_idt> create_dfcc_type_to_name()
50 {
51  return std::map<dfcc_typet, irep_idt>{
54  {dfcc_typet::CAR_SET_PTR, CONTRACTS_PREFIX "car_set_ptr_t"},
56  {dfcc_typet::OBJ_SET_PTR, CONTRACTS_PREFIX "obj_set_ptr_t"},
57  {dfcc_typet::WRITE_SET, CONTRACTS_PREFIX "write_set_t"},
58  {dfcc_typet::WRITE_SET_PTR, CONTRACTS_PREFIX "write_set_ptr_t"}};
59 }
60 
61 const std::map<dfcc_funt, irep_idt> create_dfcc_fun_to_name()
62 {
63  return {
65  {dfcc_funt::CAR_SET_CREATE, CONTRACTS_PREFIX "car_set_create"},
66  {dfcc_funt::CAR_SET_INSERT, CONTRACTS_PREFIX "car_set_insert"},
67  {dfcc_funt::CAR_SET_REMOVE, CONTRACTS_PREFIX "car_set_remove"},
68  {dfcc_funt::CAR_SET_CONTAINS, CONTRACTS_PREFIX "car_set_contains"},
70  CONTRACTS_PREFIX "obj_set_create_indexed_by_object_id"},
72  CONTRACTS_PREFIX "obj_set_create_append"},
73  {dfcc_funt::OBJ_SET_RELEASE, CONTRACTS_PREFIX "obj_set_release"},
75  {dfcc_funt::OBJ_SET_APPEND, CONTRACTS_PREFIX "obj_set_append"},
76  {dfcc_funt::OBJ_SET_REMOVE, CONTRACTS_PREFIX "obj_set_remove"},
77  {dfcc_funt::OBJ_SET_CONTAINS, CONTRACTS_PREFIX "obj_set_contains"},
79  CONTRACTS_PREFIX "obj_set_contains_exact"},
80  {dfcc_funt::WRITE_SET_CREATE, CONTRACTS_PREFIX "write_set_create"},
81  {dfcc_funt::WRITE_SET_RELEASE, CONTRACTS_PREFIX "write_set_release"},
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"},
125  {dfcc_funt::LINK_IS_FRESH, CONTRACTS_PREFIX "link_is_fresh"},
126  {dfcc_funt::LINK_ALLOCATED, CONTRACTS_PREFIX "link_allocated"},
127  {dfcc_funt::LINK_DEALLOCATED, CONTRACTS_PREFIX "link_deallocated"},
130  CONTRACTS_PREFIX "pointer_in_range_dfcc"},
131  {dfcc_funt::IS_FREEABLE, CONTRACTS_PREFIX "is_freeable"},
132  {dfcc_funt::WAS_FREED, CONTRACTS_PREFIX "was_freed"},
134  CONTRACTS_PREFIX "check_replace_ensures_was_freed_preconditions"},
135  {dfcc_funt::OBEYS_CONTRACT, CONTRACTS_PREFIX "obeys_contract"}};
136 }
137 
138 const std::map<irep_idt, dfcc_funt> create_dfcc_hook()
139 {
140  return {
146 }
147 
148 const std::map<irep_idt, dfcc_funt> create_havoc_hook()
149 {
150  return {
151  {CPROVER_PREFIX "assignable",
156 }
157 
158 const 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 
193 bool 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 
199 dfcc_funt dfcc_libraryt::get_hook(const irep_idt &function_id) const
200 {
201  PRECONDITION(is_front_end_builtin(function_id));
202  return dfcc_hook.find(function_id)->second;
203 }
204 
205 // Returns the havoc function to use for a given front-end function
206 std::optional<dfcc_funt>
207 dfcc_libraryt::get_havoc_hook(const irep_idt &function_id) const
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(
267  found == goto_model.symbol_table.symbols.end() ||
268  found->second.value.is_nil())
269  {
270  missing.insert(pair.second);
271  }
272  }
273  return missing;
274 }
275 
276 bool dfcc_libraryt::loaded = false;
277 
278 void 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 
309  symbol_tablet tmp_symbol_table;
311  to_load, tmp_symbol_table, message_handler);
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;
321  goto_model.symbol_table.insert(symbol_pair.second);
322  }
323 
324  // compile all missing library functions to GOTO
325  for(const auto &id : missing)
326  {
327  goto_convert(
330  }
331 
332  // check that all symbols have a goto_implementation
333  // and populate symbol maps
335  for(const auto &pair : dfcc_fun_to_name)
336  {
337  const auto &found =
338  goto_model.goto_functions.function_map.find(pair.second);
339 
340  INVARIANT(
341  found != goto_model.goto_functions.function_map.end() &&
342  found->second.body_available(),
343  "The body of DFCC library function " + id2string(pair.second) +
344  " could not be found");
345 
346  dfcc_fun_symbol[pair.first] = ns.lookup(pair.second);
347  }
348 
349  // populate symbol maps for easy access to symbols during translation
350  for(const auto &pair : dfcc_type_to_name)
351  {
352  dfcc_type[pair.first] = ns.lookup(pair.second).type;
353  }
354 
355  // fix malloc and free calls
357 
358  // inline the functions that need to be inlined for perf reasons
360 
361  // hide all instructions in counter example traces
362  for(auto it : dfcc_fun_symbol)
363  goto_model.goto_functions.function_map.at(it.second.name).make_hidden();
364 }
365 
366 std::optional<dfcc_funt> dfcc_libraryt::get_dfcc_fun(const irep_idt &id) const
367 {
368  auto found = dfcc_name_to_fun.find(id);
369  if(found != dfcc_name_to_fun.end())
370  return {found->second};
371  else
372  return {};
373 }
374 
376 {
377  return get_dfcc_fun(id).has_value();
378 }
379 
381 {
382  return dfcc_fun_to_name.at(fun);
383 }
384 
386 static const std::set<dfcc_funt> to_inline = {
404 
405 bool dfcc_libraryt::inlined = false;
406 
408 {
409  INVARIANT(!inlined, "inline_functions can only be called once");
410  inlined = true;
411  for(const auto &function_id : to_inline)
412  {
414  goto_model, dfcc_fun_to_name.at(function_id), message_handler);
415  }
416 }
417 
420 static const std::map<dfcc_funt, int> to_unwind = {
427 
428 bool dfcc_libraryt::specialized = false;
429 
430 void dfcc_libraryt::specialize(const std::size_t contract_assigns_size)
431 {
432  INVARIANT(
433  !specialized,
434  "dfcc_libraryt::specialize_functions can only be called once");
435 
436  specialized = true;
437  unwindsett unwindset{goto_model};
438  std::list<std::string> loop_names;
439 
440  for(const auto &entry : to_unwind)
441  {
442  const auto &function = entry.first;
443  const auto &loop_id = entry.second;
444  std::stringstream stream;
445  stream << id2string(dfcc_fun_to_name.at(function)) << "." << loop_id << ":"
446  << contract_assigns_size + 1;
447  const auto &str = stream.str();
448  loop_names.push_back(str);
449  }
450  unwindset.parse_unwindset(loop_names, message_handler);
451  goto_unwindt goto_unwind;
452  goto_unwind(
454 }
455 
457 static const std::set<dfcc_funt> fix_malloc_free_set = {
460 
463 
465 {
466  INVARIANT(
468  "dfcc_libraryt::fix_malloc_free_calls can only be called once");
469  malloc_free_fixed = true;
470  for(const auto fun : fix_malloc_free_set)
471  {
472  goto_programt &prog =
474 
476  {
477  if(ins->is_function_call())
478  {
479  const auto &function = ins->call_function();
480 
481  if(function.id() == ID_symbol)
482  {
483  const irep_idt &fun_name = to_symbol_expr(function).get_identifier();
484 
485  if(fun_name == (CONTRACTS_PREFIX "malloc"))
486  to_symbol_expr(ins->call_function()).set_identifier("malloc");
487  else if(fun_name == (CONTRACTS_PREFIX "free"))
488  to_symbol_expr(ins->call_function()).set_identifier("free");
489  }
490  }
491  }
492  }
493 }
494 
496 {
497  // not using assume-false in order not to hinder coverage
498  std::string options = "assert-false";
499  c_object_factory_parameterst object_factory_params;
501  options, object_factory_params, goto_model.symbol_table, message_handler);
502  for(const auto &it : dfcc_hook)
503  {
504  const auto &function_id = it.first;
505  if(goto_model.symbol_table.has_symbol(function_id))
506  {
507  auto &goto_function =
508  goto_model.goto_functions.function_map.at(function_id);
509 
510  generate_function_bodies->generate_function_body(
511  goto_function, goto_model.symbol_table, function_id);
512  }
513  }
514 }
515 
517 {
518  const irep_idt map_name = "__dfcc_instrumented_functions";
519 
520  if(goto_model.symbol_table.has_symbol(map_name))
521  return goto_model.symbol_table.lookup_ref(map_name);
522 
523  auto map_type =
525 
528  map_type,
529  "",
530  "__dfcc_instrumented_functions",
532  ID_C,
533  "<built-in-library>",
534  array_of_exprt(from_integer(0, map_type.element_type()), map_type),
535  true);
536 }
537 
539  const std::set<irep_idt> &instrumented_functions,
540  const source_locationt &source_location,
541  goto_programt &dest)
542 {
543  auto instrumented_functions_map =
545 
546  for(auto &function_id : instrumented_functions)
547  {
548  auto object_id = pointer_object(address_of_exprt(
550  .symbol_expr()));
551  auto index_expr = index_exprt(instrumented_functions_map, object_id);
553  index_expr, from_integer(1, unsigned_char_type()), source_location));
554  }
556 }
557 
559  const exprt &address_of_write_set,
560  const exprt &max_assigns_clause_size,
561  const exprt &max_frees_clause_size,
562  const exprt &assume_requires_ctx,
563  const exprt &assert_requires_ctx,
564  const exprt &assume_ensures_ctx,
565  const exprt &assert_ensures_ctx,
566  const exprt &allow_allocate,
567  const exprt &allow_deallocate,
568  const source_locationt &source_location)
569 {
570  auto function_symbol =
572  code_function_callt call(function_symbol);
573  auto &arguments = call.arguments();
574  // check that address_of_write_set.type() is dfcc_typet::WRITE_SET_PTR
575  arguments.emplace_back(address_of_write_set);
576  PRECONDITION(max_assigns_clause_size.type() == size_type());
577  arguments.emplace_back(max_assigns_clause_size);
578  PRECONDITION(max_frees_clause_size.type() == size_type());
579  arguments.emplace_back(max_frees_clause_size);
580  arguments.push_back(assume_requires_ctx);
581  arguments.push_back(assert_requires_ctx);
582  arguments.push_back(assume_ensures_ctx);
583  arguments.push_back(assert_ensures_ctx);
584  arguments.push_back(allow_allocate);
585  arguments.push_back(allow_deallocate);
586  call.add_source_location() = source_location;
587  return call;
588 }
589 
591  const exprt &address_of_write_set,
592  const exprt &max_assigns_clause_size,
593  const source_locationt &source_location)
594 {
595  return write_set_create_call(
596  address_of_write_set,
597  max_assigns_clause_size,
598  from_integer(0, size_type()),
599  false_exprt(),
600  false_exprt(),
601  false_exprt(),
602  false_exprt(),
603  false_exprt(),
604  false_exprt(),
605  source_location);
606 }
607 
609  const exprt &write_set_ptr,
610  const source_locationt &source_location)
611 {
612  code_function_callt call(
614  {write_set_ptr});
615  call.add_source_location() = source_location;
616  return call;
617 }
618 
620  const exprt &write_set_ptr,
621  const exprt &ptr,
622  const source_locationt &source_location)
623 {
624  code_function_callt call(
626  {write_set_ptr, ptr});
627  call.add_source_location() = source_location;
628  return call;
629 }
630 
632  const exprt &write_set_ptr,
633  const exprt &ptr,
634  const source_locationt &source_location)
635 {
636  code_function_callt call(
638  {write_set_ptr, ptr});
639  call.add_source_location() = source_location;
640  return call;
641 }
642 
644  const exprt &write_set_ptr,
645  const exprt &ptr,
646  const source_locationt &source_location)
647 {
648  code_function_callt call(
650  {write_set_ptr, ptr});
651  call.add_source_location() = source_location;
652  return call;
653 }
654 
656  const exprt &write_set_ptr,
657  const exprt &ptr,
658  const source_locationt &source_location)
659 {
660  code_function_callt call(
662  {write_set_ptr, ptr});
663  call.add_source_location() = source_location;
664  return call;
665 }
666 
669  const exprt &check_var,
670  const exprt &write_set_ptr,
671  const source_locationt &source_location)
672 {
673  code_function_callt call(
674  check_var,
676  .symbol_expr(),
677  {write_set_ptr});
678  call.add_source_location() = source_location;
679  return call;
680 }
681 
683  const exprt &check_var,
684  const exprt &write_set_ptr,
685  const exprt &ptr,
686  const exprt &size,
687  const source_locationt &source_location)
688 {
689  code_function_callt call(
690  check_var,
692  {write_set_ptr, ptr, size});
693  call.add_source_location() = source_location;
694  return call;
695 }
696 
698  const exprt &check_var,
699  const exprt &write_set_ptr,
700  const exprt &dest,
701  const source_locationt &source_location)
702 {
703  code_function_callt call(
704  check_var,
706  {write_set_ptr, dest});
707  call.add_source_location() = source_location;
708  return call;
709 }
710 
712  const exprt &check_var,
713  const exprt &write_set_ptr,
714  const exprt &dest,
715  const source_locationt &source_location)
716 {
717  code_function_callt call(
718  check_var,
720  {write_set_ptr, dest});
721  call.add_source_location() = source_location;
722  return call;
723 }
724 
726  const exprt &check_var,
727  const exprt &write_set_ptr,
728  const exprt &dest,
729  const exprt &src,
730  const source_locationt &source_location)
731 {
732  code_function_callt call(
733  check_var,
735  {write_set_ptr, dest, src});
736  call.add_source_location() = source_location;
737  return call;
738 }
739 
741  const exprt &check_var,
742  const exprt &write_set_ptr,
743  const exprt &ptr,
744  const source_locationt &source_location)
745 {
746  code_function_callt call(
747  check_var,
749  {write_set_ptr, ptr});
750  call.add_source_location() = source_location;
751  return call;
752 }
753 
755  const exprt &check_var,
756  const exprt &write_set_ptr,
757  const exprt &ptr,
758  const source_locationt &source_location)
759 {
760  code_function_callt call(
761  check_var,
763  {write_set_ptr, ptr});
764  call.add_source_location() = source_location;
765  return call;
766 }
767 
770  const exprt &check_var,
771  const exprt &reference_write_set_ptr,
772  const exprt &candidate_write_set_ptr,
773  const source_locationt &source_location)
774 {
775  code_function_callt call(
776  check_var,
778  .symbol_expr(),
779  {reference_write_set_ptr, candidate_write_set_ptr});
780  call.add_source_location() = source_location;
781  return call;
782 }
783 
786  const exprt &check_var,
787  const exprt &reference_write_set_ptr,
788  const exprt &candidate_write_set_ptr,
789  const source_locationt &source_location)
790 {
791  code_function_callt call(
792  check_var,
794  .symbol_expr(),
795  {reference_write_set_ptr, candidate_write_set_ptr});
796  call.add_source_location() = source_location;
797  return call;
798 }
799 
801  const exprt &write_set_ptr,
802  const exprt &target_write_set_ptr,
803  const source_locationt &source_location)
804 {
805  code_function_callt call(
807  {write_set_ptr, target_write_set_ptr});
808  call.add_source_location() = source_location;
809  return call;
810 }
811 
813  const exprt &write_set_ptr,
814  const exprt &is_fresh_obj_set_ptr,
815  const source_locationt &source_location)
816 {
817  code_function_callt call(
819  {write_set_ptr, is_fresh_obj_set_ptr});
820  call.add_source_location() = source_location;
821  return call;
822 }
823 
825  const exprt &write_set_postconditions_ptr,
826  const exprt &write_set_to_link_ptr,
827  const source_locationt &source_location)
828 {
829  code_function_callt call(
831  {write_set_postconditions_ptr, write_set_to_link_ptr});
832  call.add_source_location() = source_location;
833  return call;
834 }
835 
837  const exprt &write_set_postconditions_ptr,
838  const exprt &write_set_to_link_ptr,
839  const source_locationt &source_location)
840 {
841  code_function_callt call(
843  {write_set_postconditions_ptr, write_set_to_link_ptr});
844  call.add_source_location() = source_location;
845  return call;
846 }
847 
850  const exprt &ptr,
851  const exprt &write_set_ptr,
852  const source_locationt &source_location)
853 {
854  code_function_callt call(
856  .symbol_expr(),
857  {ptr, write_set_ptr});
858  call.add_source_location() = source_location;
859  return call;
860 }
861 
864  const exprt &obj_set_ptr,
865  const source_locationt &source_location)
866 {
867  code_function_callt call(
869  .symbol_expr(),
870  {obj_set_ptr});
871  call.add_source_location() = source_location;
872  return call;
873 }
874 
876  const exprt &obj_set_ptr,
877  const source_locationt &source_location)
878 {
879  code_function_callt call(
880  dfcc_fun_symbol[dfcc_funt::OBJ_SET_RELEASE].symbol_expr(), {obj_set_ptr});
881  call.add_source_location() = source_location;
882  return call;
883 }
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 unsigned_char_type()
Definition: c_types.cpp:127
Operator to return the address of an object.
Definition: pointer_expr.h:540
Array constructor from single element.
Definition: std_expr.h:1553
Arrays with given size.
Definition: std_types.h:807
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.
Definition: dfcc_library.h:207
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.
Definition: dfcc_library.h:165
const std::map< irep_idt, dfcc_funt > dfcc_hook
Maps built-in function names to enums to use for instrumentation.
Definition: dfcc_library.h:204
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.
Definition: dfcc_library.h:162
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.
Definition: dfcc_library.h:172
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.
std::optional< dfcc_funt > get_dfcc_fun(const irep_idt &id) const
Returns the dfcc_funt that corresponds to the given id if any.
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.
Definition: dfcc_library.h:192
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
Definition: dfcc_library.h:198
const std::map< irep_idt, dfcc_funt > dfcc_name_to_fun
Definition: dfcc_library.h:201
messaget log
Definition: dfcc_library.h:176
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
Definition: dfcc_library.h:174
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
Definition: dfcc_library.h:175
std::map< dfcc_typet, typet > dfcc_type
Maps enum values to the actual types (dynamically loaded)
Definition: dfcc_library.h:214
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.
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.
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 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.
Definition: dfcc_library.h:169
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
source_locationt & add_source_location()
Definition: expr.h:236
typet & type()
Return the type of the expression.
Definition: expr.h:84
The Boolean constant false.
Definition: std_expr.h:3072
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.
Definition: goto_program.h:73
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.
Definition: goto_program.h:739
Array index operator.
Definition: std_expr.h:1465
An expression denoting infinity.
Definition: std_expr.h:3097
mstreamt & status() const
Definition: message.h:406
static eomt eom
Definition: message.h:289
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:148
void add_pragma(const irep_idt &pragma)
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:155
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.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
The symbol table.
Definition: symbol_table.h:14
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition: symbol.h:28
void set_compiled()
Set the symbol's value to "compiled"; to be used once the code-typed value has been converted to a go...
Definition: symbol.h:120
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
#define CPROVER_PREFIX
const std::map< dfcc_funt, irep_idt > create_dfcc_fun_to_name()
const std::map< irep_idt, dfcc_funt > create_dfcc_hook()
#define CONTRACTS_PREFIX
static const std::set< dfcc_funt > to_inline
set of functions that need to be inlined
const std::map< irep_idt, dfcc_funt > create_havoc_hook()
std::map< V, K > swap_map(std::map< K, V > const &map)
Swaps keys and values in a map.
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.
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::set< irep_idt > create_assignable_builtin_names()
Dynamic frame condition checking library loading.
dfcc_funt
One enum value per function defined by the cprover_dfcc.c library file.
Definition: dfcc_library.h:48
@ 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.
Definition: dfcc_library.h:27
@ 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:44
double log(double x)
Definition: math.c:2776
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
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
irep_idt arch
Definition: config.h:223
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 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
#define size_type
Definition: unistd.c:347
Loop unwinding.
Loop unwinding.