cprover
Loading...
Searching...
No Matches
dfcc_instrument.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking
4
5Author: Remi Delmas, delmarsd@amazon.com
6
7\*******************************************************************/
8
9// 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>
31
32#include "dfcc_cfg_info.h"
36#include "dfcc_is_freeable.h"
37#include "dfcc_is_fresh.h"
38#include "dfcc_library.h"
39#include "dfcc_obeys_contract.h"
41#include "dfcc_spec_functions.h"
42#include "dfcc_utils.h"
43
44#include <memory>
45
46std::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
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
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 dfcc_loop_contract_modet loop_contract_mode,
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);
251 "Function '" + id2string(function_id) + "' must exist in the model.");
252
255
256 // create a local write set symbol
257 const auto &function_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,
275 loop_contract_mode,
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(
287 goto_programt::make_decl(write_set, first_instr->source_location()));
288 body.update();
289
290 body.insert_before(
293 write_set, null_expr, first_instr->source_location()));
294
296}
297
298std::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 dfcc_loop_contract_modet loop_contract_mode,
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);
330 "Function '" + id2string(function_id) + "' must exist in the model.");
331
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,
348 loop_contract_mode,
349 function_pointer_contracts);
350}
351
355 const dfcc_loop_contract_modet loop_contract_mode,
356 std::set<irep_idt> &function_pointer_contracts)
357{
358 // never instrument a function twice
359 bool inserted =
361 if(!inserted)
362 return;
363
367 "Function '" + id2string(wrapped_function_id) +
368 "' must exist in the model.");
369
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
383 goto_function,
384 write_set,
386 loop_contract_mode,
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 function_id,
403 goto_function,
404 write_set,
408 library);
409
410 // instrument instructions
411 goto_programt &body = goto_function.body;
413 function_id,
414 body,
415 body.instructions.begin(),
416 body.instructions.end(),
417 cfg_info,
418 function_pointer_contracts);
419
420 // cleanup
421 goto_program.clear();
422 goto_program.copy_from(goto_function.body);
423 remove_skip(goto_program);
425}
426
428 const irep_idt &function_id,
429 goto_functiont &goto_function,
430 const exprt &write_set,
431 const std::set<symbol_exprt> &local_statics,
432 const dfcc_loop_contract_modet loop_contract_mode,
433 std::set<irep_idt> &function_pointer_contracts)
434{
435 if(!goto_function.body_available())
436 {
437 // generate a default body `assert(false);assume(false);`
438 std::string options = "assert-false-assume-false";
439 c_object_factory_parameterst object_factory_params;
441 options, object_factory_params, goto_model.symbol_table, message_handler);
442 generate_function_bodies->generate_function_body(
443 goto_function, goto_model.symbol_table, function_id);
444 return;
445 }
446
447 auto &body = goto_function.body;
448
449 // build control flow graph information
450 dfcc_cfg_infot cfg_info(
451 function_id,
452 goto_function,
453 write_set,
454 loop_contract_mode,
457 library);
458
459 // instrument instructions
461 function_id,
462 body,
463 body.instructions.begin(),
464 body.instructions.end(),
465 cfg_info,
466 function_pointer_contracts);
467
468 // recalculate numbers, etc.
470
471 if(loop_contract_mode != dfcc_loop_contract_modet::NONE)
472 {
474 function_id,
475 goto_function,
476 cfg_info,
477 loop_contract_mode,
479 function_pointer_contracts);
480 }
481
482 // insert add/remove instructions for local statics in the top level write set
483 auto begin = body.instructions.begin();
484 auto end = std::prev(body.instructions.end());
485
486 // automatically add/remove local statics from the top level write set
487 for(const auto &local_static : local_statics)
488 {
489 insert_add_decl_call(function_id, write_set, local_static, begin, body);
490 insert_record_dead_call(function_id, write_set, local_static, end, body);
491 }
492
495 .type);
496 const auto &top_level_tracked = cfg_info.get_top_level_tracked();
497
498 // automatically add/remove function parameters that must be tracked in the
499 // function write set (they must be explicitly tracked if they are assigned
500 // in the body of a loop)
501 for(const auto &param : code_type.parameters())
502 {
503 const irep_idt &param_id = param.get_identifier();
504 if(top_level_tracked.find(param_id) != top_level_tracked.end())
505 {
506 symbol_exprt param_symbol{param.get_identifier(), param.type()};
507 insert_add_decl_call(function_id, write_set, param_symbol, begin, body);
508 insert_record_dead_call(function_id, write_set, param_symbol, end, body);
509 }
510 }
511
512 remove_skip(body);
513
514 // recalculate numbers, etc.
516}
517
519 const irep_idt &function_id,
520 goto_programt &goto_program,
523 dfcc_cfg_infot &cfg_info,
524 std::set<irep_idt> &function_pointer_contracts)
525{
526 // rewrite pointer_in_range calls
528 pointer_in_range.rewrite_calls(
529 goto_program, first_instruction, last_instruction, cfg_info);
530
531 // rewrite is_fresh calls
533 is_fresh.rewrite_calls(
534 goto_program, first_instruction, last_instruction, cfg_info);
535
536 // rewrite is_freeable/was_freed calls
538 is_freeable.rewrite_calls(
539 goto_program, first_instruction, last_instruction, cfg_info);
540
541 // rewrite obeys_contract calls
543 obeys_contract.rewrite_calls(
544 goto_program,
547 cfg_info,
548 function_pointer_contracts);
549
551 auto &target = first_instruction;
552
553 // excluding the last
554 while(target != last_instruction)
555 {
556 if(target->is_decl())
557 {
558 instrument_decl(function_id, target, goto_program, cfg_info);
559 }
560 if(target->is_dead())
561 {
562 instrument_dead(function_id, target, goto_program, cfg_info);
563 }
564 else if(target->is_assign())
565 {
566 instrument_assign(function_id, target, goto_program, cfg_info);
567 }
568 else if(target->is_function_call())
569 {
570 instrument_function_call(function_id, target, goto_program, cfg_info);
571 }
572 else if(target->is_other())
573 {
574 instrument_other(function_id, target, goto_program, cfg_info);
575 }
576 // else do nothing
577 target++;
578 }
579}
580
582 const irep_idt &function_id,
583 const exprt &write_set,
584 const symbol_exprt &symbol_expr,
586 goto_programt &goto_program)
587{
589 const auto &target_location = target->source_location();
590 auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
592
597
598 auto label_instruction =
600 goto_instruction->complete_goto(label_instruction);
601
602 insert_before_swap_and_advance(goto_program, target, payload);
603}
604
612 const irep_idt &function_id,
614 goto_programt &goto_program,
615 dfcc_cfg_infot &cfg_info)
616{
617 if(!cfg_info.must_track_decl_or_dead(target))
618 return;
619 const auto &decl_symbol = target->decl_symbol();
620 auto &write_set = cfg_info.get_write_set(target);
621
622 target++;
624 function_id, write_set, decl_symbol, target, goto_program);
625 target--;
626}
627
629 const irep_idt &function_id,
630 const exprt &write_set,
631 const symbol_exprt &symbol_expr,
633 goto_programt &goto_program)
634{
636 const auto &target_location = target->source_location();
637 auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
639
644
645 auto label_instruction =
647
648 goto_instruction->complete_goto(label_instruction);
649
650 insert_before_swap_and_advance(goto_program, target, payload);
651}
652
660 const irep_idt &function_id,
662 goto_programt &goto_program,
663 dfcc_cfg_infot &cfg_info)
664{
665 if(!cfg_info.must_track_decl_or_dead(target))
666 return;
667
668 const auto &decl_symbol = target->dead_symbol();
669 auto &write_set = cfg_info.get_write_set(target);
671 function_id, write_set, decl_symbol, target, goto_program);
672}
673
675 const irep_idt &function_id,
677 const exprt &lhs,
678 goto_programt &goto_program,
679 dfcc_cfg_infot &cfg_info)
680{
681 const irep_idt &mode =
683
685
686 const auto &lhs_source_location = target->source_location();
687 auto &write_set = cfg_info.get_write_set(target);
688 auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
690
691 source_locationt check_source_location(target->source_location());
692 check_source_location.set_property_class("assigns");
693 check_source_location.set_comment(
694 "Check that " + from_expr_using_mode(ns, mode, lhs) + " is assignable");
695
696 if(cfg_info.must_check_lhs(target))
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
711 bool_typet(),
712 function_id,
713 "__check_lhs_assignment",
715
717
720 check_var,
721 write_set,
727
728 payload.add(
731 }
732 else
733 {
734 // ```
735 // IF !write_set GOTO skip_target;
736 // ASSERT(true);
737 // skip_target: SKIP;
738 // ----
739 // ASSIGN lhs := rhs;
740 // ```
741 payload.add(
743 }
744
745 auto label_instruction =
747 goto_instruction->complete_goto(label_instruction);
748
749 insert_before_swap_and_advance(goto_program, target, payload);
750}
751
757{
758 if(
759 lhs.id() == ID_symbol &&
760 to_symbol_expr(lhs).get_identifier() == CPROVER_PREFIX "dead_object")
761 {
762 // error out if rhs is different from `if_exprt(nondet, ptr, dead_object)`
763 PRECONDITION(rhs.id() == ID_if);
764 auto &if_expr = to_if_expr(rhs);
766 PRECONDITION(if_expr.false_case() == lhs);
767 return if_expr.true_case();
768 }
769 else
770 {
771 return {};
772 }
773}
774
776 const irep_idt &function_id,
778 goto_programt &goto_program,
779 dfcc_cfg_infot &cfg_info)
780{
781 const auto &lhs = target->assign_lhs();
782 const auto &rhs = target->assign_rhs();
783 const auto &target_location = target->source_location();
784 auto &write_set = cfg_info.get_write_set(target);
785
786 // check the lhs
787 instrument_lhs(function_id, target, lhs, goto_program, cfg_info);
788
789 // handle dead_object updates (created by __builtin_alloca for instance)
790 // Remark: we do not really need to track this deallocation since the default
791 // CBMC checks are already able to detect writes to DEAD objects
792 const auto dead_ptr = is_dead_object_update(lhs, rhs);
793 if(dead_ptr.has_value())
794 {
795 // ```
796 // ASSIGN dead_object := if_exprt(nondet, ptr, dead_object);
797 // ----
798 // IF !write_set GOTO skip_target;
799 // CALL record_deallocated(write_set, ptr);
800 // skip_target: SKIP;
801 // ```
802
803 // step over the instruction
804 target++;
805
807
808 auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
810
813 write_set, dead_ptr.value(), target_location),
815
816 auto label_instruction =
818 goto_instruction->complete_goto(label_instruction);
819
820 insert_before_swap_and_advance(goto_program, target, payload);
821
822 // step back
823 target--;
824 }
825
826 // is the rhs expression a side_effect("allocate") expression ?
827 if(rhs.id() == ID_side_effect && rhs.get(ID_statement) == ID_allocate)
828 {
829 // ```
830 // CALL lhs := side_effect(statement = ID_allocate, args = {size, clear});
831 // ----
832 // IF !write_set GOTO skip_target;
833 // CALL add_allocated(write_set, lhs);
834 // skip_target: SKIP;
835 // ```
836
837 // step over the instruction
838 target++;
839
841 auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
843
847
848 auto label_instruction =
850 goto_instruction->complete_goto(label_instruction);
851
852 insert_before_swap_and_advance(goto_program, target, payload);
853
854 // step back
855 target--;
856 }
857}
858
860 const exprt &write_set,
862 goto_programt &goto_program)
863{
864 // Insert a dynamic lookup in __instrumented_functions_map
865 // and pass the write set only to functions that are known to be able
866 // to accept it.
867 //
868 // ```
869 // IF __instrumented_functions_map[__CPROVER_POINTER_OBJECT(fptr)] != 1
870 // GOTO no_inst;
871 // CALL [lhs] = fptr(params, write_set);
872 // GOTO end;
873 // no_inst:
874 // CALL [lhs] = fptr(params);
875 // end:
876 // SKIP;
877 // ---
878 // SKIP // [lhs] = fptr(params) turned into SKIP
879 // ```
880 const auto &target_location = target->source_location();
881 const auto &callf = target->call_function();
883 (callf.id() == ID_dereference) ? to_dereference_expr(callf).pointer()
885 auto index_expr = index_exprt(
889 auto goto_no_inst =
892 target->call_lhs(), target->call_function(), target->call_arguments());
893 call_inst.arguments().push_back(write_set);
895 auto goto_end_inst = payload.add(
898 goto_no_inst->complete_goto(no_inst_label);
900 target->call_lhs(), target->call_function(), target->call_arguments());
903 goto_end_inst->complete_goto(end_label);
904 // erase the original call
905 target->turn_into_skip();
906 insert_before_swap_and_advance(goto_program, target, payload);
907}
908
910 const exprt &write_set,
912 goto_programt &goto_program)
913{
914 if(target->is_function_call())
915 {
916 if(target->call_function().id() == ID_symbol)
917 {
918 // this is a function call
920 to_symbol_expr(target->call_function()).get_identifier()))
921 {
922 // pass write set argument only if function is known to be instrumented
923 target->call_arguments().push_back(write_set);
924 }
925 }
926 else
927 {
928 // This is a function pointer call. We insert a dynamic lookup into the
929 // map of instrumented functions to determine if the target function is
930 // able to accept a write set parameter.
932 write_set, target, goto_program);
933 }
934 }
935}
936
938 const irep_idt &function_id,
939 const exprt &write_set,
941 goto_programt &goto_program)
942{
943 INVARIANT(target->is_function_call(), "target must be a function call");
944 INVARIANT(
945 target->call_function().id() == ID_symbol &&
946 (id2string(to_symbol_expr(target->call_function()).get_identifier()) ==
947 CPROVER_PREFIX "deallocate"),
948 "target must be a call to" CPROVER_PREFIX "deallocate");
949
950 auto &target_location = target->source_location();
951 // ```
952 // IF !write_set GOTO skip_target;
953 // DECL check_deallocate: bool;
954 // CALL check_deallocate := check_deallocate(write_set, ptr);
955 // ASSERT(check_deallocate);
956 // DEAD check_deallocate;
957 // CALL record_deallocated(write_set, lhs);
958 // skip_target: SKIP;
959 // ----
960 // CALL __CPROVER_deallocate(ptr);
961 // ```
963
964 auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
966
969 bool_typet(),
970 function_id,
971 "__check_deallocate",
973
975
976 const auto &ptr = target->call_arguments().at(0);
977
982
983 // add property class on assertion source_location
984 const irep_idt &mode =
987 check_location.set_property_class("frees");
988 std::string comment =
989 "Check that " + from_expr_using_mode(ns, mode, ptr) + " is freeable";
990 check_location.set_comment(comment);
991
994
998
999 auto label_instruction =
1001 goto_instruction->complete_goto(label_instruction);
1002
1003 insert_before_swap_and_advance(goto_program, target, payload);
1004}
1005
1007 const irep_idt &function_id,
1008 goto_programt::targett &target,
1009 goto_programt &goto_program,
1010 dfcc_cfg_infot &cfg_info)
1011{
1012 INVARIANT(
1013 target->is_function_call(),
1014 "the target must be a function call instruction");
1015
1016 auto &write_set = cfg_info.get_write_set(target);
1017
1018 // Instrument the lhs if any.
1019 if(target->call_lhs().is_not_nil())
1020 {
1022 function_id, target, target->call_lhs(), goto_program, cfg_info);
1023 }
1024
1025 const auto &call_function = target->call_function();
1026 if(
1027 call_function.id() == ID_symbol &&
1028 (id2string(to_symbol_expr(call_function).get_identifier()) == CPROVER_PREFIX
1029 "deallocate"))
1030 {
1031 instrument_deallocate_call(function_id, write_set, target, goto_program);
1032 }
1033 else
1034 {
1035 // instrument as a normal function/function pointer call
1036 instrument_call_instruction(write_set, target, goto_program);
1037 }
1038}
1039
1041 const irep_idt &function_id,
1042 goto_programt::targett &target,
1043 goto_programt &goto_program,
1044 dfcc_cfg_infot &cfg_info)
1045{
1046 const auto &target_location = target->source_location();
1047 auto &statement = target->get_other().get_statement();
1048 auto &write_set = cfg_info.get_write_set(target);
1049 const irep_idt &mode =
1051
1052 if(statement == ID_array_set || statement == ID_array_copy)
1053 {
1054 const bool is_array_set = statement == ID_array_set;
1055 // ```
1056 // IF !write_set GOTO skip_target;
1057 // DECL check_array_set: bool;
1058 // CALL check_array_set = check_array_set(write_set, dest);
1059 // ASSERT(check_array_set);
1060 // DEAD check_array_set;
1061 // skip_target: SKIP;
1062 // ----
1063 // OTHER {statement = array_set, args = {dest, value}};
1064 // ```
1066
1067 auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
1069
1072 bool_typet(),
1073 function_id,
1074 is_array_set ? "__check_array_set" : "__check_array_copy",
1076
1078
1079 const auto &dest = target->get_other().operands().at(0);
1080
1087
1088 // add property class on assertion source_location
1090 check_location.set_property_class("assigns");
1091
1092 std::string fun_name = is_array_set ? "array_set" : "array_copy";
1093
1094 std::string comment = "Check that " + fun_name + "(" +
1095 from_expr_using_mode(ns, mode, dest) +
1096 ", ...) is allowed by the assigns clause";
1097 check_location.set_comment(comment);
1098
1101
1102 auto label_instruction =
1104 goto_instruction->complete_goto(label_instruction);
1105
1106 insert_before_swap_and_advance(goto_program, target, payload);
1107 }
1108 else if(statement == ID_array_replace)
1109 {
1110 // ```
1111 // IF !write_set GOTO skip_target;
1112 // DECL check_array_replace: bool;
1113 // CALL check_array_replace = check_array_replace(write_set, dest);
1114 // ASSERT(check_array_replace);
1115 // DEAD check_array_replace;
1116 // skip_target: SKIP;
1117 // ----
1118 // OTHER {statement = array_replace, args = {dest, src}};
1119 // ```
1121
1122 auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
1124
1127 bool_typet(),
1128 function_id,
1129 "__check_array_replace",
1131
1133
1134 const auto &dest = target->get_other().operands().at(0);
1135 const auto &src = target->get_other().operands().at(1);
1136
1139 check_var, write_set, dest, src, target_location),
1141
1142 // add property class on assertion source_location
1144 check_location.set_property_class("assigns");
1145 std::string comment = "Check that array_replace(" +
1146 from_expr_using_mode(ns, mode, dest) +
1147 ", ...) is allowed by the assigns clause";
1148 check_location.set_comment(comment);
1149
1152
1153 auto label_instruction =
1155 goto_instruction->complete_goto(label_instruction);
1156
1157 insert_before_swap_and_advance(goto_program, target, payload);
1158 }
1159 else if(statement == ID_havoc_object)
1160 {
1161 // insert before instruction
1162 // ```
1163 // IF !write_set GOTO skip_target;
1164 // DECL check_havoc_object: bool;
1165 // CALL check_havoc_object = check_havoc_object(write_set, ptr);
1166 // ASSERT(check_havoc_object);
1167 // DEAD check_havoc_object;
1168 // ```
1170
1171 auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
1173
1176 bool_typet(),
1177 function_id,
1178 "__check_havoc_object",
1180
1182
1183 const auto &ptr = target->get_other().operands().at(0);
1184
1189
1190 // add property class on assertion source_location
1192 check_location.set_property_class("assigns");
1193 std::string comment = "Check that havoc_object(" +
1194 from_expr_using_mode(ns, mode, ptr) +
1195 ") is allowed by the assigns clause";
1196 check_location.set_comment(comment);
1197
1200
1201 auto label_instruction =
1203 goto_instruction->complete_goto(label_instruction);
1204
1205 insert_before_swap_and_advance(goto_program, target, payload);
1206 }
1207 else if(statement == ID_expression)
1208 {
1209 // When in Rome do like the Romans (cf src/pointer_analysis/value_set.cpp)
1210 // can be ignored, we don't expect side effects here
1211 }
1212 else
1213 {
1214 // Other cases not presently handled
1215 // * ID_array_equal
1216 // * ID_decl track new symbol ?
1217 // * ID_cpp_delete
1218 // * ID_printf track as side effect on stdout ?
1219 // * code_inputt track as nondet ?
1220 // * code_outputt track as side effect on stdout ?
1221 // * ID_nondet track as nondet ?
1222 // * ID_asm track as side effect depending on the instruction ?
1223 // * ID_user_specified_predicate
1224 // should be pure ?
1225 // * ID_user_specified_parameter_predicates
1226 // should be pure ?
1227 // * ID_user_specified_return_predicates
1228 // should be pure ?
1229 // * ID_fence
1230 // bail out ?
1232 log.warning() << "dfcc_instrument::instrument_other: statement type '"
1233 << statement << "' is not supported, analysis may be unsound"
1234 << messaget::eom;
1235 }
1236}
1237
1239 const irep_idt &function_id,
1240 goto_functiont &goto_function,
1241 dfcc_cfg_infot &cfg_info,
1242 const dfcc_loop_contract_modet loop_contract_mode,
1243 const std::set<symbol_exprt> &local_statics,
1244 std::set<irep_idt> &function_pointer_contracts)
1245{
1246 PRECONDITION(loop_contract_mode != dfcc_loop_contract_modet::NONE);
1247 cfg_info.get_loops_toposorted();
1248
1249 std::list<std::string> to_unwind;
1250
1251 // Apply loop contract transformations in topological order
1252 for(const auto &loop_id : cfg_info.get_loops_toposorted())
1253 {
1254 const auto &loop = cfg_info.get_loop_info(loop_id);
1255 if(loop.invariant.is_nil() && loop.decreases.empty())
1256 {
1257 // skip loops that do not have contracts
1258 log.warning() << "loop " << function_id << "." << loop.cbmc_loop_id
1259 << " does not have a contract, skipping instrumentation"
1260 << messaget::eom;
1261 continue;
1262 }
1263
1265 loop_id,
1266 function_id,
1267 goto_function,
1268 cfg_info,
1270 function_pointer_contracts);
1271 to_unwind.push_back(
1272 id2string(function_id) + "." + std::to_string(loop.cbmc_loop_id) + ":2");
1273 }
1274
1275 // If required, unwind all transformed loops to yield base and step cases
1276 if(loop_contract_mode == dfcc_loop_contract_modet::APPLY_UNWIND)
1277 {
1278 unwindsett unwindset{goto_model};
1279 unwindset.parse_unwindset(to_unwind, log.get_message_handler());
1282 }
1283
1284 remove_skip(goto_function.body);
1285}
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:240
unsignedbv_typet unsigned_char_type()
Definition c_types.cpp:132
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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:539
Computes natural loops, enforces normal form conditions, computes the nesting graph,...
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.
const std::vector< std::size_t > & get_loops_toposorted() const
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 for that instruction.
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.
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 apply_loop_contracts(const irep_idt &function_id, goto_functiont &goto_function, dfcc_cfg_infot &cfg_info, const dfcc_loop_contract_modet loop_contract_mode, 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_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
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 dfcc_loop_contract_modet loop_contract_mode, std::set< irep_idt > &function_pointer_contracts)
Instruments the body of a GOTO function against a given write set.
static std::set< irep_idt > function_cache
Keeps track of instrumented functions, so that no function gets instrumented more than once.
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_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...
void instrument_wrapped_function(const irep_idt &wrapped_function_id, const irep_idt &initial_function_id, const dfcc_loop_contract_modet loop_contract_mode, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO function by adding an extra write set parameter and inserting frame condition chec...
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
void instrument_harness_function(const irep_idt &function_id, const dfcc_loop_contract_modet loop_contract_mode, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO function used as a proof harness.
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 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_function(const irep_idt &function_id, const dfcc_loop_contract_modet loop_contract_mode, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO function by adding an extra write set parameter and instrumenting its body instruc...
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...
optionalt< 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.
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...
Rewrites calls to is_fresh predicates into calls to the library implementation.
Class interface to library types and functions defined in cprover_contracts.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 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)
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.
Rewrites calls to pointer_in_range predicates into calls to the library implementation.
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:39
std::string::const_iterator begin() const
Definition dstring.h:194
The empty type.
Definition std_types.h:51
Base class for all expressions.
Definition expr.h:56
function_mapt function_map
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_programt body
bool body_available() const
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.
instructionst instructions
The list of instructions in the goto program.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
void clear()
Clear the goto program.
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
instructionst::iterator targett
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())
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
Array index operator.
Definition std_expr.h:1410
const irep_idt & id() const
Definition irep.h:396
source_locationt source_location
Definition message.h:247
message_handlert & get_message_handler()
Definition message.h:184
mstreamt & warning() const
Definition message.h:404
static eomt eom
Definition message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Disequality.
Definition std_expr.h:1365
The null pointer constant.
Expression to hold a symbol (variable)
Definition std_expr.h:113
The Boolean constant true.
Definition std_expr.h:3008
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
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
dfcc_loop_contract_modet
Enumeration representing the instrumentation mode for loop contracts.
@ NONE
Do not apply loop contracts.
@ APPLY_UNWIND
Apply loop contracts and unwind the resulting base + step encoding.
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:47
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...
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
exprt pointer_object(const exprt &p)
Various predicates over pointers in programs.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Program Transformation.
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition invariant.h:464
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2403
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
static const exprt make_null_check_expr(const exprt &ptr)
Returns the expression expr == NULL.
static exprt make_sizeof_expr(const exprt &expr, const namespacet &)
Returns the expression sizeof(expr).
static void add_parameter(goto_modelt &, const symbolt &symbol, const irep_idt &function_id)
Adds the given symbol as parameter to the function symbol's code_type.
static symbol_exprt create_symbol(symbol_table_baset &, const typet &type, const irep_idt &function_id, const std::string &base_name, const source_locationt &source_location)
Adds a new symbol named function_id::base_name of type type with given attributes in the symbol table...
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:234