CBMC
dfcc_instrument.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 // TODO apply loop contracts transformations as part of function instrumentation
10 
11 #include "dfcc_instrument.h"
12 
13 #include <util/format_expr.h>
14 #include <util/fresh_symbol.h>
15 #include <util/namespace.h>
16 #include <util/pointer_expr.h>
18 #include <util/prefix.h>
19 #include <util/suffix.h>
20 
23 
24 #include <ansi-c/c_expr.h>
28 #include <goto-instrument/unwind.h>
30 #include <langapi/language_util.h>
31 
32 #include "dfcc_cfg_info.h"
34 #include "dfcc_instrument_loop.h"
35 #include "dfcc_is_cprover_symbol.h"
36 #include "dfcc_is_freeable.h"
37 #include "dfcc_is_fresh.h"
38 #include "dfcc_library.h"
39 #include "dfcc_obeys_contract.h"
40 #include "dfcc_pointer_in_range.h"
41 #include "dfcc_spec_functions.h"
42 #include "dfcc_utils.h"
43 
44 #include <memory>
45 
46 std::set<irep_idt> dfcc_instrumentt::function_cache;
47 
49  goto_modelt &goto_model,
50  message_handlert &message_handler,
51  dfcc_libraryt &library,
52  dfcc_spec_functionst &spec_functions,
53  dfcc_contract_clauses_codegent &contract_clauses_codegen)
54  : goto_model(goto_model),
55  message_handler(message_handler),
56  log(message_handler),
57  library(library),
58  spec_functions(spec_functions),
59  contract_clauses_codegen(contract_clauses_codegen),
60  instrument_loop(
61  goto_model,
62  message_handler,
63  library,
64  spec_functions,
65  contract_clauses_codegen),
66  ns(goto_model.symbol_table)
67 {
68  // these come from different assert.h implementation on different systems
69  // and eventually become ASSERT instructions and must not be instrumented
70  internal_symbols.insert("__assert_fail");
71  internal_symbols.insert("_assert");
72  internal_symbols.insert("__assert_c99");
73  internal_symbols.insert("_wassert");
74  internal_symbols.insert("__assert_rtn");
75  internal_symbols.insert("__assert");
76  internal_symbols.insert("__assert_func");
77 
79  internal_symbols.insert("__builtin_prefetch");
80  internal_symbols.insert("__builtin_unreachable");
81 
85  internal_symbols.insert(ID_gcc_builtin_va_arg);
86  internal_symbols.insert("__builtin_va_copy");
87  internal_symbols.insert("__builtin_va_start");
88  internal_symbols.insert("__va_start");
89  internal_symbols.insert("__builtin_va_end");
90 
93  internal_symbols.insert("__builtin_isgreater");
94  internal_symbols.insert("__builtin_isgreaterequal");
95  internal_symbols.insert("__builtin_isless");
96  internal_symbols.insert("__builtin_islessequal");
97  internal_symbols.insert("__builtin_islessgreater");
98  internal_symbols.insert("__builtin_isunordered");
99 }
100 
102  std::set<irep_idt> &dest) const
103 {
104  dest.insert(
107 }
108 
110 {
112 }
113 
114 /*
115  A word on built-ins:
116 
117  C compiler builtins are declared in
118  - src/ansi-c/clang_builtin_headers*.h
119  - src/ansi-c/gcc_builtin_headers*.h
120  - src/ansi-c/windows_builtin_headers.h
121 
122  Some gcc builtins are compiled down to goto instructions
123  and inlined in place during type-checking:
124  - src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp
125  - src/ansi-c/c_typecheck_expr.cpp, method do_special_functions
126  so they essentially disappear from the model.
127 
128  Builtins are also handled in:
129  - src/goto-programs/builtin_functions.cpp
130  - src/goto-symex/symex_builtin_functions.cpp
131 
132  Some compiler builtins have implementations defined as C functions in the
133  cprover library, and these should be instrumented just like other functions.
134 
135  Last, some compiler built-ins might have just a declaration but
136  no conversion or library implementation.
137  They might then persist in the program as functions which return a nondet
138  value or transformed into side_effect_nondet_exprt during conversion
139  If they survive as functions we should be able to add an extra parameter
140  to these functions even if they have no body.
141 
142  The CPROVER built-ins are declared here:
143  - src/ansi-c/cprover_builtin_headers.h
144  - src/ansi-c/cprover_library.h
145  - src/ansi-c/library/cprover_contracts.c
146  and should not be instrumented.
147 
148  The case of __CPROVER_deallocate is special: it is a wrapper for an assignment
149  to the __CPROVER_deallocated_object global. We do not want to
150  instrument this function, but we still want to check that its parameters
151  are allowed for deallocation by the write set.
152 
153  There is also a number of CPROVER global static symbols that are used to
154  support memory safety property instrumentation, and assignments to these
155  statics should always be allowed (i.e not instrumented):
156  - __CPROVER_alloca_object,
157  - __CPROVER_dead_object,
158  - __CPROVER_deallocated,
159  - __CPROVER_malloc_is_new_array,
160  - __CPROVER_max_malloc_size,
161  - __CPROVER_memory_leak,
162  - __CPROVER_new_object,
163  - __CPROVER_next_thread_id,
164  - __CPROVER_next_thread_key,
165  - __CPROVER_pipe_count,
166  - __CPROVER_rounding_mode,
167  - __CPROVER_thread_id,
168  - __CPROVER_thread_key_dtors,
169  - __CPROVER_thread_keys,
170  - __CPROVER_threads_exited,
171  - ... (and more of them)
172 
174  static std::set<irep_idt> alloca_builtins = {"alloca", "__builtin_alloca"};
175 
177  static std::set<std::string> builtins_with_cprover_impl = {
178  "__builtin_ia32_sfence",
179  "__builtin_ia32_lfence",
180  "__builtin_ia32_mfence",
181  "__builtin_ffs",
182  "__builtin_ffsl",
183  "__builtin_ffsll",
184  "__builtin_ia32_vec_ext_v4hi",
185  "__builtin_ia32_vec_ext_v8hi",
186  "__builtin_ia32_vec_ext_v4si",
187  "__builtin_ia32_vec_ext_v2di",
188  "__builtin_ia32_vec_ext_v16qi",
189  "__builtin_ia32_vec_ext_v4sf",
190  "__builtin_ia32_psubsw128",
191  "__builtin_ia32_psubusw128",
192  "__builtin_ia32_paddsw",
193  "__builtin_ia32_psubsw",
194  "__builtin_ia32_vec_init_v4hi",
195  "__builtin_flt_rounds",
196  "__builtin_fabs",
197  "__builtin_fabsl",
198  "__builtin_fabsf",
199  "__builtin_inff",
200  "__builtin_inf",
201  "__builtin_infl",
202  "__builtin_isinf",
203  "__builtin_isinff",
204  "__builtin_isinf",
205  "__builtin_isnan",
206  "__builtin_isnanf",
207  "__builtin_huge_valf",
208  "__builtin_huge_val",
209  "__builtin_huge_vall",
210  "__builtin_nan",
211  "__builtin_nanf",
212  "__builtin_abs",
213  "__builtin_labs",
214  "__builtin_llabs",
215  "__builtin_alloca",
216  "__builtin___strcpy_chk",
217  "__builtin___strcat_chk",
218  "__builtin___strncat_chk",
219  "__builtin___strncpy_chk",
220  "__builtin___memcpy_chk",
221  "__builtin_memset",
222  "__builtin___memset_chk",
223  "__builtin___memmove_chk"};
224 */
225 
228 {
229  return internal_symbols.find(id) != internal_symbols.end();
230 }
231 
233 {
234  return !has_prefix(id2string(id), CPROVER_PREFIX "file_local") &&
236 }
237 
239  const irep_idt &function_id,
240  const loop_contract_configt &loop_contract_config,
241  std::set<irep_idt> &function_pointer_contracts)
242 {
243  // never instrument a function twice
244  bool inserted = dfcc_instrumentt::function_cache.insert(function_id).second;
245  if(!inserted)
246  return;
247 
248  auto found = goto_model.goto_functions.function_map.find(function_id);
250  found != goto_model.goto_functions.function_map.end(),
251  "Function '" + id2string(function_id) + "' must exist in the model.");
252 
253  const null_pointer_exprt null_expr(
255 
256  // create a local write set symbol
257  const auto &function_symbol =
259  const auto write_set = dfcc_utilst::create_symbol(
262  function_id,
263  "__write_set_to_check",
264  function_symbol.location);
265 
266  std::set<symbol_exprt> local_statics = get_local_statics(function_id);
267 
268  goto_functiont &goto_function = found->second;
269 
271  function_id,
272  goto_function,
273  write_set,
274  local_statics,
275  loop_contract_config,
276  function_pointer_contracts);
277 
278  auto &body = goto_function.body;
279 
280  // add write set definitions at the top of the function
281  // DECL write_set_harness
282  // ASSIGN write_set_harness := NULL
283  auto first_instr = body.instructions.begin();
284 
285  body.insert_before(
286  first_instr,
287  goto_programt::make_decl(write_set, first_instr->source_location()));
288  body.update();
289 
290  body.insert_before(
291  first_instr,
293  write_set, null_expr, first_instr->source_location()));
294 
296 }
297 
298 std::set<symbol_exprt>
300 {
301  std::set<symbol_exprt> local_statics;
302  for(const auto &sym_pair : goto_model.symbol_table)
303  {
304  const auto &sym = sym_pair.second;
305  if(sym.is_static_lifetime)
306  {
307  const auto &loc = sym.location;
308  if(!loc.get_function().empty() && loc.get_function() == function_id)
309  {
310  local_statics.insert(sym.symbol_expr());
311  }
312  }
313  }
314  return local_statics;
315 }
316 
318  const irep_idt &function_id,
319  const loop_contract_configt &loop_contract_config,
320  std::set<irep_idt> &function_pointer_contracts)
321 {
322  // never instrument a function twice
323  bool inserted = dfcc_instrumentt::function_cache.insert(function_id).second;
324  if(!inserted)
325  return;
326 
327  auto found = goto_model.goto_functions.function_map.find(function_id);
329  found != goto_model.goto_functions.function_map.end(),
330  "Function '" + id2string(function_id) + "' must exist in the model.");
331 
332  const auto &write_set = dfcc_utilst::add_parameter(
333  goto_model,
334  function_id,
335  "__write_set_to_check",
337  .symbol_expr();
338 
339  std::set<symbol_exprt> local_statics = get_local_statics(function_id);
340 
341  goto_functiont &goto_function = found->second;
342 
344  function_id,
345  goto_function,
346  write_set,
347  local_statics,
348  loop_contract_config,
349  function_pointer_contracts);
350 }
351 
353  const irep_idt &wrapped_function_id,
354  const irep_idt &initial_function_id,
355  const loop_contract_configt &loop_contract_config,
356  std::set<irep_idt> &function_pointer_contracts)
357 {
358  // never instrument a function twice
359  bool inserted =
360  dfcc_instrumentt::function_cache.insert(wrapped_function_id).second;
361  if(!inserted)
362  return;
363 
364  auto found = goto_model.goto_functions.function_map.find(wrapped_function_id);
366  found != goto_model.goto_functions.function_map.end(),
367  "Function '" + id2string(wrapped_function_id) +
368  "' must exist in the model.");
369 
370  const auto &write_set = dfcc_utilst::add_parameter(
371  goto_model,
372  wrapped_function_id,
373  "__write_set_to_check",
375  .symbol_expr();
376 
377  std::set<symbol_exprt> local_statics = get_local_statics(initial_function_id);
378 
379  goto_functiont &goto_function = found->second;
380 
382  wrapped_function_id,
383  goto_function,
384  write_set,
385  local_statics,
386  loop_contract_config,
387  function_pointer_contracts);
388 }
389 
391  const irep_idt &function_id,
392  goto_programt &goto_program,
393  const exprt &write_set,
394  std::set<irep_idt> &function_pointer_contracts)
395 {
396  // create a dummy goto function with empty parameters
397  goto_functiont goto_function;
398  goto_function.body.copy_from(goto_program);
399 
400  // build control flow graph information
401  dfcc_cfg_infot cfg_info(
402  goto_model,
403  function_id,
404  goto_function,
405  write_set,
406  loop_contract_configt{false},
409  library);
410 
411  // instrument instructions
412  goto_programt &body = goto_function.body;
414  function_id,
415  body,
416  body.instructions.begin(),
417  body.instructions.end(),
418  cfg_info,
419  function_pointer_contracts);
420 
421  // cleanup
422  goto_program.clear();
423  goto_program.copy_from(goto_function.body);
424  remove_skip(goto_program);
426 }
427 
429  const irep_idt &function_id,
430  goto_functiont &goto_function,
431  const exprt &write_set,
432  const std::set<symbol_exprt> &local_statics,
433  const loop_contract_configt &loop_contract_config,
434  std::set<irep_idt> &function_pointer_contracts)
435 {
436  if(!goto_function.body_available())
437  {
438  // generate a default body `assert(false);assume(false);`
439  std::string options = "assert-false-assume-false";
440  c_object_factory_parameterst object_factory_params;
442  options, object_factory_params, goto_model.symbol_table, message_handler);
443  generate_function_bodies->generate_function_body(
444  goto_function, goto_model.symbol_table, function_id);
445  return;
446  }
447 
448  auto &body = goto_function.body;
449 
450  // build control flow graph information
451  dfcc_cfg_infot cfg_info(
452  goto_model,
453  function_id,
454  goto_function,
455  write_set,
456  loop_contract_config,
459  library);
460 
461  // instrument instructions
463  function_id,
464  body,
465  body.instructions.begin(),
466  body.instructions.end(),
467  cfg_info,
468  function_pointer_contracts);
469 
470  // recalculate numbers, etc.
472 
473  if(loop_contract_config.apply_loop_contracts)
474  {
476  function_id,
477  goto_function,
478  cfg_info,
479  loop_contract_config,
480  local_statics,
481  function_pointer_contracts);
482  }
483 
484  // insert add/remove instructions for local statics in the top level write set
485  auto begin = body.instructions.begin();
486  auto end = std::prev(body.instructions.end());
487 
488  // automatically add/remove local statics from the top level write set
489  for(const auto &local_static : local_statics)
490  {
491  insert_add_decl_call(function_id, write_set, local_static, begin, body);
492  insert_record_dead_call(function_id, write_set, local_static, end, body);
493  }
494 
495  const code_typet &code_type = to_code_type(
497  .type);
498  const auto &top_level_tracked = cfg_info.get_top_level_tracked();
499 
500  // automatically add/remove function parameters that must be tracked in the
501  // function write set (they must be explicitly tracked if they are assigned
502  // in the body of a loop)
503  for(const auto &param : code_type.parameters())
504  {
505  const irep_idt &param_id = param.get_identifier();
506  if(top_level_tracked.find(param_id) != top_level_tracked.end())
507  {
508  symbol_exprt param_symbol{param.get_identifier(), param.type()};
509  insert_add_decl_call(function_id, write_set, param_symbol, begin, body);
510  insert_record_dead_call(function_id, write_set, param_symbol, end, body);
511  }
512  }
513 
514  remove_skip(body);
515 
516  // recalculate numbers, etc.
518 }
519 
521  const irep_idt &function_id,
522  goto_programt &goto_program,
523  goto_programt::targett first_instruction,
524  const goto_programt::targett &last_instruction,
525  dfcc_cfg_infot &cfg_info,
526  std::set<irep_idt> &function_pointer_contracts)
527 {
528  // rewrite pointer_in_range calls
530  pointer_in_range.rewrite_calls(
531  goto_program, first_instruction, last_instruction, cfg_info);
532 
533  // rewrite is_fresh calls
535  is_fresh.rewrite_calls(
536  goto_program, first_instruction, last_instruction, cfg_info);
537 
538  // rewrite is_freeable/was_freed calls
540  is_freeable.rewrite_calls(
541  goto_program, first_instruction, last_instruction, cfg_info);
542 
543  // rewrite obeys_contract calls
545  obeys_contract.rewrite_calls(
546  goto_program,
547  first_instruction,
548  last_instruction,
549  cfg_info,
550  function_pointer_contracts);
551 
553  auto &target = first_instruction;
554 
555  // excluding the last
556  while(target != last_instruction)
557  {
558  if(target->is_decl())
559  {
560  instrument_decl(function_id, target, goto_program, cfg_info);
561  }
562  if(target->is_dead())
563  {
564  instrument_dead(function_id, target, goto_program, cfg_info);
565  }
566  else if(target->is_assign())
567  {
568  instrument_assign(function_id, target, goto_program, cfg_info);
569  }
570  else if(target->is_function_call())
571  {
572  instrument_function_call(function_id, target, goto_program, cfg_info);
573  }
574  else if(target->is_other())
575  {
576  instrument_other(function_id, target, goto_program, cfg_info);
577  }
578  // else do nothing
579  target++;
580  }
581 }
582 
584  const irep_idt &function_id,
585  const exprt &write_set,
586  const symbol_exprt &symbol_expr,
587  goto_programt::targett &target,
588  goto_programt &goto_program)
589 {
590  goto_programt payload;
591  const auto &target_location = target->source_location();
592  auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
593  dfcc_utilst::make_null_check_expr(write_set), target_location));
594 
597  write_set, address_of_exprt(symbol_expr), target_location),
598  target_location));
599 
600  auto label_instruction =
601  payload.add(goto_programt::make_skip(target_location));
602  goto_instruction->complete_goto(label_instruction);
603 
604  insert_before_swap_and_advance(goto_program, target, payload);
605 }
606 
614  const irep_idt &function_id,
615  goto_programt::targett &target,
616  goto_programt &goto_program,
617  dfcc_cfg_infot &cfg_info)
618 {
619  if(!cfg_info.must_track_decl_or_dead(target))
620  return;
621  const auto &decl_symbol = target->decl_symbol();
622  auto &write_set = cfg_info.get_write_set(target);
623 
624  target++;
626  function_id, write_set, decl_symbol, target, goto_program);
627  target--;
628 }
629 
631  const irep_idt &function_id,
632  const exprt &write_set,
633  const symbol_exprt &symbol_expr,
634  goto_programt::targett &target,
635  goto_programt &goto_program)
636 {
637  goto_programt payload;
638  const auto &target_location = target->source_location();
639  auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
640  dfcc_utilst::make_null_check_expr(write_set), target_location));
641 
644  write_set, address_of_exprt(symbol_expr), target_location),
645  target_location));
646 
647  auto label_instruction =
648  payload.add(goto_programt::make_skip(target_location));
649 
650  goto_instruction->complete_goto(label_instruction);
651 
652  insert_before_swap_and_advance(goto_program, target, payload);
653 }
654 
662  const irep_idt &function_id,
663  goto_programt::targett &target,
664  goto_programt &goto_program,
665  dfcc_cfg_infot &cfg_info)
666 {
667  if(!cfg_info.must_track_decl_or_dead(target))
668  return;
669 
670  const auto &decl_symbol = target->dead_symbol();
671  auto &write_set = cfg_info.get_write_set(target);
673  function_id, write_set, decl_symbol, target, goto_program);
674 }
675 
677  const irep_idt &function_id,
678  goto_programt::targett &target,
679  const exprt &lhs,
680  goto_programt &goto_program,
681  dfcc_cfg_infot &cfg_info)
682 {
683  const irep_idt &mode =
685 
686  goto_programt payload;
687 
688  const auto &lhs_source_location = target->source_location();
689  auto &write_set = cfg_info.get_write_set(target);
690  auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
691  dfcc_utilst::make_null_check_expr(write_set), lhs_source_location));
692 
693  source_locationt check_source_location(target->source_location());
694  check_source_location.set_property_class("assigns");
695  check_source_location.set_comment(
696  "Check that " + from_expr_using_mode(ns, mode, lhs) + " is assignable");
697 
698  // ```
699  // IF !write_set GOTO skip_target;
700  // DECL check_assign: bool;
701  // CALL check_assign = check_assignment(write_set, &lhs, sizeof(lhs));
702  // ASSERT(check_assign);
703  // DEAD check_assign;
704  // skip_target: SKIP;
705  // ----
706  // ASSIGN lhs := rhs;
707  // ```
708 
709  const auto check_var = dfcc_utilst::create_symbol(
711  bool_typet(),
712  function_id,
713  "__check_lhs_assignment",
714  lhs_source_location);
715 
716  payload.add(goto_programt::make_decl(check_var, lhs_source_location));
717 
720  check_var,
721  write_set,
725  lhs_source_location),
726  lhs_source_location));
727 
728  payload.add(goto_programt::make_assertion(check_var, check_source_location));
729  payload.add(goto_programt::make_dead(check_var, check_source_location));
730 
731  auto label_instruction =
732  payload.add(goto_programt::make_skip(lhs_source_location));
733  goto_instruction->complete_goto(label_instruction);
734 
735  insert_before_swap_and_advance(goto_program, target, payload);
736 }
737 
741 std::optional<exprt>
743 {
744  if(
745  lhs.id() == ID_symbol &&
746  to_symbol_expr(lhs).get_identifier() == CPROVER_PREFIX "dead_object" &&
747  rhs.id() == ID_if)
748  {
749  // only handle `if_exprt(nondet, ptr, dead_object)`
750  auto &if_expr = to_if_expr(rhs);
751  if(
752  if_expr.cond().id() == ID_side_effect &&
753  to_side_effect_expr(if_expr.cond()).get_statement() == ID_nondet &&
754  if_expr.false_case() == lhs)
755  {
756  return if_expr.true_case();
757  }
758  }
759 
760  return {};
761 }
762 
764  const irep_idt &function_id,
765  goto_programt::targett &target,
766  goto_programt &goto_program,
767  dfcc_cfg_infot &cfg_info)
768 {
769  const auto &lhs = target->assign_lhs();
770  const auto &rhs = target->assign_rhs();
771  const auto &target_location = target->source_location();
772  auto &write_set = cfg_info.get_write_set(target);
773 
774  // check the lhs
775  if(cfg_info.must_check_lhs(target))
776  instrument_lhs(function_id, target, lhs, goto_program, cfg_info);
777 
778  // handle dead_object updates (created by __builtin_alloca for instance)
779  // Remark: we do not really need to track this deallocation since the default
780  // CBMC checks are already able to detect writes to DEAD objects
781  const auto dead_ptr = is_dead_object_update(lhs, rhs);
782  if(dead_ptr.has_value())
783  {
784  // ```
785  // ASSIGN dead_object := if_exprt(nondet, ptr, dead_object);
786  // ----
787  // IF !write_set GOTO skip_target;
788  // CALL record_deallocated(write_set, ptr);
789  // skip_target: SKIP;
790  // ```
791 
792  // step over the instruction
793  target++;
794 
795  goto_programt payload;
796 
797  auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
798  dfcc_utilst::make_null_check_expr(write_set), target_location));
799 
802  write_set, dead_ptr.value(), target_location),
803  target_location));
804 
805  auto label_instruction =
806  payload.add(goto_programt::make_skip(target_location));
807  goto_instruction->complete_goto(label_instruction);
808 
809  insert_before_swap_and_advance(goto_program, target, payload);
810 
811  // step back
812  target--;
813  }
814 
815  // is the rhs expression a side_effect("allocate") expression ?
816  if(rhs.id() == ID_side_effect && rhs.get(ID_statement) == ID_allocate)
817  {
818  // ```
819  // CALL lhs := side_effect(statement = ID_allocate, args = {size, clear});
820  // ----
821  // IF !write_set GOTO skip_target;
822  // CALL add_allocated(write_set, lhs);
823  // skip_target: SKIP;
824  // ```
825 
826  // step over the instruction
827  target++;
828 
829  goto_programt payload;
830  auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
831  dfcc_utilst::make_null_check_expr(write_set), target_location));
832 
834  library.write_set_add_allocated_call(write_set, lhs, target_location),
835  target_location));
836 
837  auto label_instruction =
838  payload.add(goto_programt::make_skip(target_location));
839  goto_instruction->complete_goto(label_instruction);
840 
841  insert_before_swap_and_advance(goto_program, target, payload);
842 
843  // step back
844  target--;
845  }
846 }
847 
849  const exprt &write_set,
850  goto_programt::targett &target,
851  goto_programt &goto_program)
852 {
853  // Insert a dynamic lookup in __instrumented_functions_map
854  // and pass the write set only to functions that are known to be able
855  // to accept it.
856  //
857  // ```
858  // IF __instrumented_functions_map[__CPROVER_POINTER_OBJECT(fptr)] != 1
859  // GOTO no_inst;
860  // CALL [lhs] = fptr(params, write_set);
861  // GOTO end;
862  // no_inst:
863  // CALL [lhs] = fptr(params);
864  // end:
865  // SKIP;
866  // ---
867  // SKIP // [lhs] = fptr(params) turned into SKIP
868  // ```
869  const auto &target_location = target->source_location();
870  const auto &callf = target->call_function();
871  auto object_id = pointer_object(
872  (callf.id() == ID_dereference) ? to_dereference_expr(callf).pointer()
873  : address_of_exprt(callf));
874  auto index_expr = index_exprt(
876  auto cond = notequal_exprt(index_expr, from_integer(1, unsigned_char_type()));
877  goto_programt payload;
878  auto goto_no_inst =
879  payload.add(goto_programt::make_incomplete_goto(cond, target_location));
880  code_function_callt call_inst(
881  target->call_lhs(), target->call_function(), target->call_arguments());
882  call_inst.arguments().push_back(write_set);
883  payload.add(goto_programt::make_function_call(call_inst, target_location));
884  auto goto_end_inst = payload.add(
885  goto_programt::make_incomplete_goto(true_exprt(), target_location));
886  auto no_inst_label = payload.add(goto_programt::make_skip(target_location));
887  goto_no_inst->complete_goto(no_inst_label);
888  code_function_callt call_no_inst(
889  target->call_lhs(), target->call_function(), target->call_arguments());
890  payload.add(goto_programt::make_function_call(call_no_inst, target_location));
891  auto end_label = payload.add(goto_programt::make_skip(target_location));
892  goto_end_inst->complete_goto(end_label);
893  // erase the original call
894  target->turn_into_skip();
895  insert_before_swap_and_advance(goto_program, target, payload);
896 }
897 
899  const exprt &write_set,
900  goto_programt::targett &target,
901  goto_programt &goto_program)
902 {
903  if(target->is_function_call())
904  {
905  if(target->call_function().id() == ID_symbol)
906  {
907  // this is a function call
908  if(!do_not_instrument(
909  to_symbol_expr(target->call_function()).get_identifier()))
910  {
911  // pass write set argument only if function is known to be instrumented
912  target->call_arguments().push_back(write_set);
913  }
914  }
915  else
916  {
917  // This is a function pointer call. We insert a dynamic lookup into the
918  // map of instrumented functions to determine if the target function is
919  // able to accept a write set parameter.
921  write_set, target, goto_program);
922  }
923  }
924 }
925 
927  const irep_idt &function_id,
928  const exprt &write_set,
929  goto_programt::targett &target,
930  goto_programt &goto_program)
931 {
932  INVARIANT(target->is_function_call(), "target must be a function call");
933  INVARIANT(
934  target->call_function().id() == ID_symbol &&
935  (id2string(to_symbol_expr(target->call_function()).get_identifier()) ==
936  CPROVER_PREFIX "deallocate"),
937  "target must be a call to" CPROVER_PREFIX "deallocate");
938 
939  auto &target_location = target->source_location();
940  // ```
941  // IF !write_set GOTO skip_target;
942  // DECL check_deallocate: bool;
943  // CALL check_deallocate := check_deallocate(write_set, ptr);
944  // ASSERT(check_deallocate);
945  // DEAD check_deallocate;
946  // CALL record_deallocated(write_set, lhs);
947  // skip_target: SKIP;
948  // ----
949  // CALL __CPROVER_deallocate(ptr);
950  // ```
951  goto_programt payload;
952 
953  auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
954  dfcc_utilst::make_null_check_expr(write_set), target_location));
955 
956  const auto check_var = dfcc_utilst::create_symbol(
958  bool_typet(),
959  function_id,
960  "__check_deallocate",
961  target_location);
962 
963  payload.add(goto_programt::make_decl(check_var, target_location));
964 
965  const auto &ptr = target->call_arguments().at(0);
966 
969  check_var, write_set, ptr, target_location),
970  target_location));
971 
972  // add property class on assertion source_location
973  const irep_idt &mode =
975  source_locationt check_location(target_location);
976  check_location.set_property_class("frees");
977  std::string comment =
978  "Check that " + from_expr_using_mode(ns, mode, ptr) + " is freeable";
979  check_location.set_comment(comment);
980 
981  payload.add(goto_programt::make_assertion(check_var, check_location));
982  payload.add(goto_programt::make_dead(check_var, target_location));
983 
985  library.write_set_record_deallocated_call(write_set, ptr, target_location),
986  target_location));
987 
988  auto label_instruction =
989  payload.add(goto_programt::make_skip(target_location));
990  goto_instruction->complete_goto(label_instruction);
991 
992  insert_before_swap_and_advance(goto_program, target, payload);
993 }
994 
996  const irep_idt &function_id,
997  goto_programt::targett &target,
998  goto_programt &goto_program,
999  dfcc_cfg_infot &cfg_info)
1000 {
1001  INVARIANT(
1002  target->is_function_call(),
1003  "the target must be a function call instruction");
1004 
1005  auto &write_set = cfg_info.get_write_set(target);
1006 
1007  // Instrument the lhs if any.
1008  if(target->call_lhs().is_not_nil() && cfg_info.must_check_lhs(target))
1009  {
1011  function_id, target, target->call_lhs(), goto_program, cfg_info);
1012  }
1013 
1014  const auto &call_function = target->call_function();
1015  if(
1016  call_function.id() == ID_symbol &&
1017  (id2string(to_symbol_expr(call_function).get_identifier()) == CPROVER_PREFIX
1018  "deallocate"))
1019  {
1020  instrument_deallocate_call(function_id, write_set, target, goto_program);
1021  }
1022  else
1023  {
1024  // instrument as a normal function/function pointer call
1025  instrument_call_instruction(write_set, target, goto_program);
1026  }
1027 }
1028 
1030  const irep_idt &function_id,
1031  goto_programt::targett &target,
1032  goto_programt &goto_program,
1033  dfcc_cfg_infot &cfg_info)
1034 {
1035  const auto &target_location = target->source_location();
1036  auto &statement = target->get_other().get_statement();
1037  auto &write_set = cfg_info.get_write_set(target);
1038  const irep_idt &mode =
1040 
1041  if(statement == ID_array_set || statement == ID_array_copy)
1042  {
1043  const bool is_array_set = statement == ID_array_set;
1044  // ```
1045  // IF !write_set GOTO skip_target;
1046  // DECL check_array_set: bool;
1047  // CALL check_array_set = check_array_set(write_set, dest);
1048  // ASSERT(check_array_set);
1049  // DEAD check_array_set;
1050  // skip_target: SKIP;
1051  // ----
1052  // OTHER {statement = array_set, args = {dest, value}};
1053  // ```
1054  goto_programt payload;
1055 
1056  auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
1057  dfcc_utilst::make_null_check_expr(write_set), target_location));
1058 
1059  const auto check_var = dfcc_utilst::create_symbol(
1061  bool_typet(),
1062  function_id,
1063  is_array_set ? "__check_array_set" : "__check_array_copy",
1064  target_location);
1065 
1066  payload.add(goto_programt::make_decl(check_var, target_location));
1067 
1068  const auto &dest = target->get_other().operands().at(0);
1069 
1071  is_array_set ? library.write_set_check_array_set_call(
1072  check_var, write_set, dest, target_location)
1074  check_var, write_set, dest, target_location),
1075  target_location));
1076 
1077  // add property class on assertion source_location
1078  source_locationt check_location(target_location);
1079  check_location.set_property_class("assigns");
1080 
1081  std::string fun_name = is_array_set ? "array_set" : "array_copy";
1082 
1083  std::string comment = "Check that " + fun_name + "(" +
1084  from_expr_using_mode(ns, mode, dest) +
1085  ", ...) is allowed by the assigns clause";
1086  check_location.set_comment(comment);
1087 
1088  payload.add(goto_programt::make_assertion(check_var, check_location));
1089  payload.add(goto_programt::make_dead(check_var, target_location));
1090 
1091  auto label_instruction =
1092  payload.add(goto_programt::make_skip(target_location));
1093  goto_instruction->complete_goto(label_instruction);
1094 
1095  insert_before_swap_and_advance(goto_program, target, payload);
1096  }
1097  else if(statement == ID_array_replace)
1098  {
1099  // ```
1100  // IF !write_set GOTO skip_target;
1101  // DECL check_array_replace: bool;
1102  // CALL check_array_replace = check_array_replace(write_set, dest);
1103  // ASSERT(check_array_replace);
1104  // DEAD check_array_replace;
1105  // skip_target: SKIP;
1106  // ----
1107  // OTHER {statement = array_replace, args = {dest, src}};
1108  // ```
1109  goto_programt payload;
1110 
1111  auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
1112  dfcc_utilst::make_null_check_expr(write_set), target_location));
1113 
1114  const auto check_var = dfcc_utilst::create_symbol(
1116  bool_typet(),
1117  function_id,
1118  "__check_array_replace",
1119  target_location);
1120 
1121  payload.add(goto_programt::make_decl(check_var, target_location));
1122 
1123  const auto &dest = target->get_other().operands().at(0);
1124  const auto &src = target->get_other().operands().at(1);
1125 
1128  check_var, write_set, dest, src, target_location),
1129  target_location));
1130 
1131  // add property class on assertion source_location
1132  source_locationt check_location(target_location);
1133  check_location.set_property_class("assigns");
1134  std::string comment = "Check that array_replace(" +
1135  from_expr_using_mode(ns, mode, dest) +
1136  ", ...) is allowed by the assigns clause";
1137  check_location.set_comment(comment);
1138 
1139  payload.add(goto_programt::make_assertion(check_var, check_location));
1140  payload.add(goto_programt::make_dead(check_var, target_location));
1141 
1142  auto label_instruction =
1143  payload.add(goto_programt::make_skip(target_location));
1144  goto_instruction->complete_goto(label_instruction);
1145 
1146  insert_before_swap_and_advance(goto_program, target, payload);
1147  }
1148  else if(statement == ID_havoc_object)
1149  {
1150  // insert before instruction
1151  // ```
1152  // IF !write_set GOTO skip_target;
1153  // DECL check_havoc_object: bool;
1154  // CALL check_havoc_object = check_havoc_object(write_set, ptr);
1155  // ASSERT(check_havoc_object);
1156  // DEAD check_havoc_object;
1157  // ```
1158  goto_programt payload;
1159 
1160  auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
1161  dfcc_utilst::make_null_check_expr(write_set), target_location));
1162 
1163  const auto check_var = dfcc_utilst::create_symbol(
1165  bool_typet(),
1166  function_id,
1167  "__check_havoc_object",
1168  target_location);
1169 
1170  payload.add(goto_programt::make_decl(check_var, target_location));
1171 
1172  const auto &ptr = target->get_other().operands().at(0);
1173 
1176  check_var, write_set, ptr, target_location),
1177  target_location));
1178 
1179  // add property class on assertion source_location
1180  source_locationt check_location(target_location);
1181  check_location.set_property_class("assigns");
1182  std::string comment = "Check that havoc_object(" +
1183  from_expr_using_mode(ns, mode, ptr) +
1184  ") is allowed by the assigns clause";
1185  check_location.set_comment(comment);
1186 
1187  payload.add(goto_programt::make_assertion(check_var, check_location));
1188  payload.add(goto_programt::make_dead(check_var, target_location));
1189 
1190  auto label_instruction =
1191  payload.add(goto_programt::make_skip(target_location));
1192  goto_instruction->complete_goto(label_instruction);
1193 
1194  insert_before_swap_and_advance(goto_program, target, payload);
1195  }
1196  else if(statement == ID_expression)
1197  {
1198  // When in Rome do like the Romans (cf src/pointer_analysis/value_set.cpp)
1199  // can be ignored, we don't expect side effects here
1200  }
1201  else
1202  {
1203  // Other cases not presently handled
1204  // * ID_array_equal
1205  // * ID_decl track new symbol ?
1206  // * ID_cpp_delete
1207  // * ID_printf track as side effect on stdout ?
1208  // * code_inputt track as nondet ?
1209  // * code_outputt track as side effect on stdout ?
1210  // * ID_nondet track as nondet ?
1211  // * ID_asm track as side effect depending on the instruction ?
1212  // * ID_user_specified_predicate
1213  // should be pure ?
1214  // * ID_user_specified_parameter_predicates
1215  // should be pure ?
1216  // * ID_user_specified_return_predicates
1217  // should be pure ?
1218  // * ID_fence
1219  // bail out ?
1220  log.warning().source_location = target_location;
1221  log.warning() << "dfcc_instrument::instrument_other: statement type '"
1222  << statement << "' is not supported, analysis may be unsound"
1223  << messaget::eom;
1224  }
1225 }
1226 
1228  const irep_idt &function_id,
1229  goto_functiont &goto_function,
1230  dfcc_cfg_infot &cfg_info,
1231  const loop_contract_configt &loop_contract_config,
1232  const std::set<symbol_exprt> &local_statics,
1233  std::set<irep_idt> &function_pointer_contracts)
1234 {
1235  PRECONDITION(loop_contract_config.apply_loop_contracts);
1236  cfg_info.get_loops_toposorted();
1237 
1238  std::list<std::string> to_unwind;
1239 
1240  // Apply loop contract transformations in topological order
1241  for(const auto &loop_id : cfg_info.get_loops_toposorted())
1242  {
1243  const auto &loop = cfg_info.get_loop_info(loop_id);
1244  if(loop.must_skip())
1245  {
1246  // skip loops that do not have contracts
1247  log.warning() << "loop " << function_id << "." << loop.cbmc_loop_id
1248  << " does not have a contract, skipping instrumentation"
1249  << messaget::eom;
1250  continue;
1251  }
1252 
1254  loop_id,
1255  function_id,
1256  goto_function,
1257  cfg_info,
1258  local_statics,
1259  function_pointer_contracts);
1260  to_unwind.push_back(
1261  id2string(function_id) + "." + std::to_string(loop.cbmc_loop_id) + ":2");
1262  }
1263 
1264  // If required, unwind all transformed loops to yield base and step cases
1265  if(loop_contract_config.unwind_transformed_loops)
1266  {
1267  unwindsett unwindset{goto_model};
1268  unwindset.parse_unwindset(to_unwind, log.get_message_handler());
1269  goto_unwindt goto_unwind;
1270  goto_unwind(goto_model, unwindset, goto_unwindt::unwind_strategyt::ASSUME);
1271  }
1272 
1273  remove_skip(goto_function.body);
1274 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
API to expression classes that are internal to the C frontend.
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:235
unsignedbv_typet unsigned_char_type()
Definition: c_types.cpp:127
Operator to return the address of an object.
Definition: pointer_expr.h:540
The Boolean type.
Definition: std_types.h:36
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
Computes natural loops, enforces normal form conditions, computes the nesting graph,...
const std::vector< std::size_t > & get_loops_toposorted() const
const std::unordered_set< irep_idt > & get_top_level_tracked()
Returns the set of top level symbols that must be tracked explicitly in the top level write set of th...
const dfcc_loop_infot & get_loop_info(const std::size_t loop_id) const
Returns the loop info for that loop_id.
bool must_check_lhs(goto_programt::const_targett target) const
True iff the lhs of an assignment must be checked against the ambient write set.
const exprt & get_write_set(goto_programt::const_targett target) const
Returns the write set variable to use for the given instruction Returns the write set for the loop,...
bool must_track_decl_or_dead(goto_programt::const_targett target) const
True iff a DECL ident must be tracked in the write set of the loop that contains the DECL.
Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that ...
std::size_t get_max_assigns_clause_size() const
Maximum number of assigns clause targets.
void instrument_function(const irep_idt &function_id, const loop_contract_configt &loop_contract_config, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO function by adding an extra write set parameter and instrumenting its body instruc...
dfcc_libraryt & library
void instrument_goto_program(const irep_idt &function_id, goto_programt &goto_program, const exprt &write_set, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO program against a given write set variable.
void instrument_call_instruction(const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program)
Adds the write_set as extra argument to a function of function pointer call instruction.
void instrument_lhs(const irep_idt &function_id, goto_programt::targett &target, const exprt &lhs, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)
Instruments the LHS of an assignment instruction instruction by adding an inclusion check of lhs in w...
void instrument_other(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)
Instruments a OTHER statement; instruction.
void instrument_assign(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)
Instrument the lhs of an ASSIGN lhs := rhs instruction by adding an inclusion check of lhs in write_s...
void instrument_deallocate_call(const irep_idt &function_id, const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program)
Inserts deallocation checks and a write set update before a call to the __CPROVER_deallocate function...
std::set< irep_idt > internal_symbols
Set of internal symbols which implementation is generated and inlined into the model at conversion or...
dfcc_instrument_loopt instrument_loop
void get_instrumented_functions(std::set< irep_idt > &dest) const
Adds the names of instrumented functions to dest.
message_handlert & message_handler
static std::set< irep_idt > function_cache
Keeps track of instrumented functions, so that no function gets instrumented more than once.
void instrument_goto_function(const irep_idt &function_id, goto_functiont &goto_function, const exprt &write_set, const std::set< symbol_exprt > &local_statics, const loop_contract_configt &loop_contract_config, std::set< irep_idt > &function_pointer_contracts)
Instruments the body of a GOTO function against a given write set.
void instrument_function_call(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)
Instruments a CALL lhs := function(params) instruction by adding an inclusion check of lhs in write_s...
void instrument_wrapped_function(const irep_idt &wrapped_function_id, const irep_idt &initial_function_id, const loop_contract_configt &loop_contract_config, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO function by adding an extra write set parameter and inserting frame condition chec...
void instrument_instructions(const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett first_instruction, const goto_programt::targett &last_instruction, dfcc_cfg_infot &cfg_info, std::set< irep_idt > &function_pointer_contracts)
Instruments the instructions found between first_instruction and last_instruction in the instructions...
std::optional< exprt > is_dead_object_update(const exprt &lhs, const exprt &rhs)
Checks if lhs is the dead_object, and if rhs is an if_exprt(nondet, ptr, dead_object) expression.
dfcc_instrumentt(goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_spec_functionst &spec_functions, dfcc_contract_clauses_codegent &contract_clauses_codegen)
void instrument_decl(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)
Instruments a DECL x instruction.
std::size_t get_max_assigns_clause_size() const
bool do_not_instrument(const irep_idt &id) const
True iff the symbol must not be instrumented because it is an internal symbol or a CPROVER symbol.
void apply_loop_contracts(const irep_idt &function_id, goto_functiont &goto_function, dfcc_cfg_infot &cfg_info, const loop_contract_configt &loop_contract_config, const std::set< symbol_exprt > &local_statics, std::set< irep_idt > &function_pointer_contracts)
Applies loop contracts transformations to the given GOTO function, using the given cfg_info instance ...
void instrument_dead(const irep_idt &function_id, goto_programt::targett &target, goto_programt &goto_program, dfcc_cfg_infot &cfg_info)
Instruments a DEAD x instruction.
void instrument_harness_function(const irep_idt &function_id, const loop_contract_configt &loop_contract_config, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO function used as a proof harness.
goto_modelt & goto_model
void insert_record_dead_call(const irep_idt &function_id, const exprt &write_set, const symbol_exprt &symbol_expr, goto_programt::targett &target, goto_programt &goto_program)
Generates a guarded call to record the death of a local symbol and inserts it in the goto_program at ...
std::set< symbol_exprt > get_local_statics(const irep_idt &function_id)
Returns the set of names from the symbol table that have the static flag set to true and have a sourc...
bool is_internal_symbol(const irep_idt &id) const
True iff the symbol an internal symbol.
void insert_add_decl_call(const irep_idt &function_id, const exprt &write_set, const symbol_exprt &symbol_expr, goto_programt::targett &target, goto_programt &goto_program)
Generates a guarded call to record a locally allocated symbol and inserts it in the goto_program at t...
void instrument_fptr_call_instruction_dynamic_lookup(const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program)
Before calling a function pointer, performs a dynamic lookup into the map of instrumented function pr...
Rewrites calls to is_freeable and was_freed predicates in goto programs encoding pre and post conditi...
void rewrite_calls(goto_programt &program, dfcc_cfg_infot &cfg_info)
Rewrites calls to is_freeable and was_freed predicates into calls to the library implementation in th...
Rewrites calls to is_fresh predicates into calls to the library implementation.
Definition: dfcc_is_fresh.h:30
void rewrite_calls(goto_programt &program, dfcc_cfg_infot &cfg_info)
Rewrites calls to is_fresh predicates into calls to the library implementation in the given program,...
Class interface to library types and functions defined in cprover_contracts.c.
Definition: dfcc_library.h:154
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 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.
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.
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.
const symbolt & get_instrumented_functions_map_symbol()
Returns the "__dfcc_instrumented_functions" symbol or creates it if it does not exist already.
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_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.
std::map< dfcc_typet, typet > dfcc_type
Maps enum values to the actual types (dynamically loaded)
Definition: dfcc_library.h:214
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.
Rewrites calls to obeys_contract predicates into calls to the library implementation.
void rewrite_calls(goto_programt &program, dfcc_cfg_infot &cfg_info, std::set< irep_idt > &function_pointer_contracts)
Rewrites calls to obeys_contract predicates into calls to the library implementation in the given pro...
Rewrites calls to pointer_in_range predicates into calls to the library implementation.
void rewrite_calls(goto_programt &program, dfcc_cfg_infot cfg_info)
Rewrites calls to pointer_in_range predicates into calls to the library implementation in the given p...
This class rewrites GOTO functions that use the built-ins:
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
std::string::const_iterator begin() const
Definition: dstring.h:193
The empty type.
Definition: std_types.h:51
Base class for all expressions.
Definition: expr.h:56
const source_locationt & source_location() const
Definition: expr.h:231
function_mapt function_map
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
goto_programt body
Definition: goto_function.h:26
bool body_available() const
Definition: goto_function.h:35
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
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
void clear()
Clear the goto program.
Definition: goto_program.h:820
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:971
instructionst::iterator targett
Definition: goto_program.h:614
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:891
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:739
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:964
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:933
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
Array index operator.
Definition: std_expr.h:1465
const irep_idt & id() const
Definition: irep.h:388
source_locationt source_location
Definition: message.h:239
mstreamt & warning() const
Definition: message.h:396
message_handlert & get_message_handler()
Definition: message.h:183
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
Disequality.
Definition: std_expr.h:1420
The null pointer constant.
Definition: pointer_expr.h:909
const irep_idt & get_statement() const
Definition: std_code.h:1472
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
Expression to hold a symbol (variable)
Definition: std_expr.h:131
const irep_idt & get_identifier() const
Definition: std_expr.h:160
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt mode
Language mode.
Definition: symbol.h:49
The Boolean constant true.
Definition: std_expr.h:3063
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2076
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define CPROVER_PREFIX
Class that computes CFG information about the loop structure of a GOTO function for the purpose of dy...
Translates assigns and frees clauses of a function contract or loop contract into goto programs that ...
Add instrumentation to a goto program to perform frame condition checks.
This class applies the loop contract transformation to a loop in a goto function.
bool dfcc_is_cprover_function_symbol(const irep_idt &id)
Returns true iff id is one of the known CPROVER functions or starts with __VERIFIER or nondet.
Instruments occurrences of is_freeable predicates in programs encoding requires and ensures clauses o...
Instruments occurrences of is_fresh predicates in programs encoding requires and ensures clauses of c...
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.
Dynamic frame condition checking library loading.
@ WRITE_SET_PTR
type of pointers to descriptors of assignable/freeable sets of locations
Instruments occurrences of obeys_contract predicates in programs encoding requires and ensures clause...
Instruments occurrences of pointer_in_range predicates in programs encoding requires and ensures clau...
Translate functions that specify assignable and freeable targets declaratively into active functions ...
Dynamic frame condition checking utility functions.
Fresh auxiliary symbol creation.
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-...
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::string from_expr_using_mode(const namespacet &ns, const irep_idt &mode, const exprt &expr)
Formats an expression using the given namespace, using the given mode to retrieve the language printe...
double log(double x)
Definition: math.c:2776
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:890
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
exprt pointer_object(const exprt &p)
Various predicates over pointers in programs.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:108
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:87
Program Transformation.
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition: invariant.h:464
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1506
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2450
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
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
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 const exprt make_null_check_expr(const exprt &ptr)
Returns the expression expr == NULL.
Definition: dfcc_utils.cpp:406
static exprt make_sizeof_expr(const exprt &expr, const namespacet &)
Returns the expression sizeof(expr).
Definition: dfcc_utils.cpp:411
static void add_parameter(goto_modelt &, const symbolt &symbol, const irep_idt &function_id)
Adds the given symbol as parameter to the function symbol's code_type.
Definition: dfcc_utils.cpp:156
static symbol_exprt create_symbol(symbol_table_baset &, const typet &type, const irep_idt &function_id, const std::string &base_name, const source_locationt &source_location)
Adds a new symbol named function_id::base_name of type type with given attributes in the symbol table...
Definition: dfcc_utils.cpp:81
Loop contract configurations.
Loop unwinding.
Loop unwinding.
void insert_before_swap_and_advance(goto_programt &destination, goto_programt::targett &target, goto_programt &payload)
Insert a goto program before a target instruction iterator and advance the iterator.
Definition: utils.cpp:237