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
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
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);
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
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 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);
330 "Function '" + id2string(function_id) + "' must exist in the model.");
331
332 const auto &write_set = dfcc_utilst::add_parameter(
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);
367 "Function '" + id2string(wrapped_function_id) +
368 "' must exist in the model.");
369
370 const auto &write_set = dfcc_utilst::add_parameter(
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(
403 function_id,
404 goto_function,
405 write_set,
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(
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,
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,
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,
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,
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,
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
741std::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,
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,
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(
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,
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
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,
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,
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
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};
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.
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::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 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.
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.
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.
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...
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())
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
instructionst::iterator targett
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.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_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:1470
const irep_idt & id() const
Definition irep.h:388
source_locationt source_location
Definition message.h:239
message_handlert & get_message_handler()
Definition message.h:183
mstreamt & warning() const
Definition message.h:396
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:1425
The null pointer constant.
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:3068
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
void parse_unwindset(const std::list< std::string > &unwindset, message_handlert &message_handler)
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...
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
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:2455
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
static 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 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