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
24
25#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"
40#include "dfcc_pointer_equals.h"
42#include "dfcc_spec_functions.h"
43#include "dfcc_utils.h"
44
45#include <memory>
46
47std::set<irep_idt> dfcc_instrumentt::function_cache;
48
64 library,
67 ns(goto_model.symbol_table)
68{
69 // these come from different assert.h implementation on different systems
70 // and eventually become ASSERT instructions and must not be instrumented
71 internal_symbols.insert("__assert_fail");
72 internal_symbols.insert("_assert");
73 internal_symbols.insert("__assert_c99");
74 internal_symbols.insert("_wassert");
75 internal_symbols.insert("__assert_rtn");
76 internal_symbols.insert("__assert");
77 internal_symbols.insert("__assert_func");
78
80 internal_symbols.insert("__builtin_prefetch");
81 internal_symbols.insert("__builtin_unreachable");
82
86 internal_symbols.insert(ID_gcc_builtin_va_arg);
87 internal_symbols.insert("__builtin_va_copy");
88 internal_symbols.insert("__builtin_va_start");
89 internal_symbols.insert("__va_start");
90 internal_symbols.insert("__builtin_va_end");
91
94 internal_symbols.insert("__builtin_isgreater");
95 internal_symbols.insert("__builtin_isgreaterequal");
96 internal_symbols.insert("__builtin_isless");
97 internal_symbols.insert("__builtin_islessequal");
98 internal_symbols.insert("__builtin_islessgreater");
99 internal_symbols.insert("__builtin_isunordered");
100}
101
103 std::set<irep_idt> &dest) const
104{
105 dest.insert(
108}
109
111{
112 return instrument_loop.get_max_assigns_clause_size();
113}
114
115/*
116 A word on built-ins:
117
118 C compiler builtins are declared in
119 - src/ansi-c/clang_builtin_headers*.h
120 - src/ansi-c/gcc_builtin_headers*.h
121 - src/ansi-c/windows_builtin_headers.h
122
123 Some gcc builtins are compiled down to goto instructions
124 and inlined in place during type-checking:
125 - src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp
126 - src/ansi-c/c_typecheck_expr.cpp, method do_special_functions
127 so they essentially disappear from the model.
128
129 Builtins are also handled in:
130 - src/goto-programs/builtin_functions.cpp
131 - src/goto-symex/symex_builtin_functions.cpp
132
133 Some compiler builtins have implementations defined as C functions in the
134 cprover library, and these should be instrumented just like other functions.
135
136 Last, some compiler built-ins might have just a declaration but
137 no conversion or library implementation.
138 They might then persist in the program as functions which return a nondet
139 value or transformed into side_effect_nondet_exprt during conversion
140 If they survive as functions we should be able to add an extra parameter
141 to these functions even if they have no body.
142
143 The CPROVER built-ins are declared here:
144 - src/ansi-c/cprover_builtin_headers.h
145 - src/ansi-c/cprover_library.h
146 - src/ansi-c/library/cprover_contracts.c
147 and should not be instrumented.
148
149 The case of __CPROVER_deallocate is special: it is a wrapper for an assignment
150 to the __CPROVER_deallocated_object global. We do not want to
151 instrument this function, but we still want to check that its parameters
152 are allowed for deallocation by the write set.
153
154 There is also a number of CPROVER global static symbols that are used to
155 support memory safety property instrumentation, and assignments to these
156 statics should always be allowed (i.e not instrumented):
157 - __CPROVER_alloca_object,
158 - __CPROVER_dead_object,
159 - __CPROVER_deallocated,
160 - __CPROVER_malloc_is_new_array,
161 - __CPROVER_max_malloc_size,
162 - __CPROVER_memory_leak,
163 - __CPROVER_new_object,
164 - __CPROVER_next_thread_id,
165 - __CPROVER_next_thread_key,
166 - __CPROVER_pipe_count,
167 - __CPROVER_rounding_mode,
168 - __CPROVER_thread_id,
169 - __CPROVER_thread_key_dtors,
170 - __CPROVER_thread_keys,
171 - __CPROVER_threads_exited,
172 - ... (and more of them)
173
175 static std::set<irep_idt> alloca_builtins = {"alloca", "__builtin_alloca"};
176
178 static std::set<std::string> builtins_with_cprover_impl = {
179 "__builtin_ia32_sfence",
180 "__builtin_ia32_lfence",
181 "__builtin_ia32_mfence",
182 "__builtin_ffs",
183 "__builtin_ffsl",
184 "__builtin_ffsll",
185 "__builtin_ia32_vec_ext_v4hi",
186 "__builtin_ia32_vec_ext_v8hi",
187 "__builtin_ia32_vec_ext_v4si",
188 "__builtin_ia32_vec_ext_v2di",
189 "__builtin_ia32_vec_ext_v16qi",
190 "__builtin_ia32_vec_ext_v4sf",
191 "__builtin_ia32_psubsw128",
192 "__builtin_ia32_psubusw128",
193 "__builtin_ia32_paddsw",
194 "__builtin_ia32_psubsw",
195 "__builtin_ia32_vec_init_v4hi",
196 "__builtin_flt_rounds",
197 "__builtin_fabs",
198 "__builtin_fabsl",
199 "__builtin_fabsf",
200 "__builtin_inff",
201 "__builtin_inf",
202 "__builtin_infl",
203 "__builtin_isinf",
204 "__builtin_isinff",
205 "__builtin_isinf",
206 "__builtin_isnan",
207 "__builtin_isnanf",
208 "__builtin_huge_valf",
209 "__builtin_huge_val",
210 "__builtin_huge_vall",
211 "__builtin_nan",
212 "__builtin_nanf",
213 "__builtin_abs",
214 "__builtin_labs",
215 "__builtin_llabs",
216 "__builtin_alloca",
217 "__builtin___strcpy_chk",
218 "__builtin___strcat_chk",
219 "__builtin___strncat_chk",
220 "__builtin___strncpy_chk",
221 "__builtin___memcpy_chk",
222 "__builtin_memset",
223 "__builtin___memset_chk",
224 "__builtin___memmove_chk"};
225*/
226
229{
230 return internal_symbols.find(id) != internal_symbols.end();
231}
232
234{
235 return !has_prefix(id2string(id), CPROVER_PREFIX "file_local") &&
237}
238
240 const irep_idt &function_id,
241 const loop_contract_configt &loop_contract_config,
242 std::set<irep_idt> &function_pointer_contracts)
243{
244 // never instrument a function twice
245 bool inserted = dfcc_instrumentt::function_cache.insert(function_id).second;
246 if(!inserted)
247 return;
248
249 auto found = goto_model.goto_functions.function_map.find(function_id);
251 found != goto_model.goto_functions.function_map.end(),
252 "Function '" + id2string(function_id) + "' must exist in the model.");
253
254 const null_pointer_exprt null_expr(
256
257 // create a local write set symbol
258 const auto &function_symbol =
259 dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id);
260 const auto write_set = dfcc_utilst::create_symbol(
261 goto_model.symbol_table,
263 function_id,
264 "__write_set_to_check",
265 function_symbol.location);
266
267 std::set<symbol_exprt> local_statics = get_local_statics(function_id);
268
269 goto_functiont &goto_function = found->second;
270
272 function_id,
273 goto_function,
274 write_set,
275 local_statics,
276 loop_contract_config,
277 function_pointer_contracts);
278
279 auto &body = goto_function.body;
280
281 // add write set definitions at the top of the function
282 // DECL write_set_harness
283 // ASSIGN write_set_harness := NULL
284 auto first_instr = body.instructions.begin();
285
286 body.insert_before(
287 first_instr,
288 goto_programt::make_decl(write_set, first_instr->source_location()));
289 body.update();
290
291 body.insert_before(
292 first_instr,
294 write_set, null_expr, first_instr->source_location()));
295
296 goto_model.goto_functions.update();
297}
298
299std::set<symbol_exprt>
301{
302 std::set<symbol_exprt> local_statics;
303 for(const auto &sym_pair : goto_model.symbol_table)
304 {
305 const auto &sym = sym_pair.second;
306 if(sym.is_static_lifetime)
307 {
308 const auto &loc = sym.location;
309 if(!loc.get_function().empty() && loc.get_function() == function_id)
310 {
311 local_statics.insert(sym.symbol_expr());
312 }
313 }
314 }
315 return local_statics;
316}
317
319 const irep_idt &function_id,
320 const loop_contract_configt &loop_contract_config,
321 std::set<irep_idt> &function_pointer_contracts)
322{
323 // never instrument a function twice
324 bool inserted = dfcc_instrumentt::function_cache.insert(function_id).second;
325 if(!inserted)
326 return;
327
328 auto found = goto_model.goto_functions.function_map.find(function_id);
330 found != goto_model.goto_functions.function_map.end(),
331 "Function '" + id2string(function_id) + "' must exist in the model.");
332
333 const auto &write_set = dfcc_utilst::add_parameter(
335 function_id,
336 "__write_set_to_check",
338 .symbol_expr();
339
340 std::set<symbol_exprt> local_statics = get_local_statics(function_id);
341
342 goto_functiont &goto_function = found->second;
343
345 function_id,
346 goto_function,
347 write_set,
348 local_statics,
349 loop_contract_config,
350 function_pointer_contracts);
351}
352
354 const irep_idt &wrapped_function_id,
355 const irep_idt &initial_function_id,
356 const loop_contract_configt &loop_contract_config,
357 std::set<irep_idt> &function_pointer_contracts)
358{
359 // never instrument a function twice
360 bool inserted =
361 dfcc_instrumentt::function_cache.insert(wrapped_function_id).second;
362 if(!inserted)
363 return;
364
365 auto found = goto_model.goto_functions.function_map.find(wrapped_function_id);
367 found != goto_model.goto_functions.function_map.end(),
368 "Function '" + id2string(wrapped_function_id) +
369 "' must exist in the model.");
370
371 const auto &write_set = dfcc_utilst::add_parameter(
373 wrapped_function_id,
374 "__write_set_to_check",
376 .symbol_expr();
377
378 std::set<symbol_exprt> local_statics = get_local_statics(initial_function_id);
379
380 goto_functiont &goto_function = found->second;
381
383 wrapped_function_id,
384 goto_function,
385 write_set,
386 local_statics,
387 loop_contract_config,
388 function_pointer_contracts);
389}
390
392 const irep_idt &function_id,
393 goto_programt &goto_program,
394 const exprt &write_set,
395 std::set<irep_idt> &function_pointer_contracts)
396{
397 // create a dummy goto function with empty parameters
398 goto_functiont goto_function;
399 goto_function.body.copy_from(goto_program);
400
401 // build control flow graph information
402 dfcc_cfg_infot cfg_info(
404 function_id,
405 goto_function,
406 write_set,
408 goto_model.symbol_table,
410 library);
411
412 // instrument instructions
413 goto_programt &body = goto_function.body;
415 function_id,
416 body,
417 body.instructions.begin(),
418 body.instructions.end(),
419 cfg_info,
420 function_pointer_contracts);
421
422 // cleanup
423 goto_program.clear();
424 goto_program.copy_from(goto_function.body);
425 remove_skip(goto_program);
426 goto_model.goto_functions.update();
427}
428
430 const irep_idt &function_id,
431 goto_functiont &goto_function,
432 const exprt &write_set,
433 const std::set<symbol_exprt> &local_statics,
434 const loop_contract_configt &loop_contract_config,
435 std::set<irep_idt> &function_pointer_contracts)
436{
437 if(!goto_function.body_available())
438 {
439 // generate a default body `assert(false);assume(false);`
440 std::string options = "assert-false-assume-false";
441 c_object_factory_parameterst object_factory_params;
443 options, object_factory_params, goto_model.symbol_table, message_handler);
444 generate_function_bodies->generate_function_body(
445 goto_function, goto_model.symbol_table, function_id);
446 return;
447 }
448
449 auto &body = goto_function.body;
450
451 // build control flow graph information
452 dfcc_cfg_infot cfg_info(
454 function_id,
455 goto_function,
456 write_set,
457 loop_contract_config,
458 goto_model.symbol_table,
460 library);
461
462 // instrument instructions
464 function_id,
465 body,
466 body.instructions.begin(),
467 body.instructions.end(),
468 cfg_info,
469 function_pointer_contracts);
470
471 // recalculate numbers, etc.
472 goto_model.goto_functions.update();
473
474 if(loop_contract_config.apply_loop_contracts)
475 {
477 function_id,
478 goto_function,
479 cfg_info,
480 loop_contract_config,
481 local_statics,
482 function_pointer_contracts);
483 }
484
485 // insert add/remove instructions for local statics in the top level write set
486 auto begin = body.instructions.begin();
487 auto end = std::prev(body.instructions.end());
488
489 // automatically add/remove local statics from the top level write set
490 for(const auto &local_static : local_statics)
491 {
492 insert_add_decl_call(function_id, write_set, local_static, begin, body);
493 insert_record_dead_call(function_id, write_set, local_static, end, body);
494 }
495
496 const code_typet &code_type = to_code_type(
497 dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id)
498 .type);
499 const auto &top_level_tracked = cfg_info.get_top_level_tracked();
500
501 // automatically add/remove function parameters that must be tracked in the
502 // function write set (they must be explicitly tracked if they are assigned
503 // in the body of a loop)
504 for(const auto &param : code_type.parameters())
505 {
506 const irep_idt &param_id = param.get_identifier();
507 if(top_level_tracked.find(param_id) != top_level_tracked.end())
508 {
509 symbol_exprt param_symbol{param.get_identifier(), param.type()};
510 insert_add_decl_call(function_id, write_set, param_symbol, begin, body);
511 insert_record_dead_call(function_id, write_set, param_symbol, end, body);
512 }
513 }
514
515 remove_skip(body);
516
517 // recalculate numbers, etc.
518 goto_model.goto_functions.update();
519}
520
522 const irep_idt &function_id,
523 goto_programt &goto_program,
524 goto_programt::targett first_instruction,
525 const goto_programt::targett &last_instruction,
526 dfcc_cfg_infot &cfg_info,
527 std::set<irep_idt> &function_pointer_contracts)
528{
529 // rewrite pointer_equals calls
531 pointer_equals.rewrite_calls(
532 goto_program, first_instruction, last_instruction, cfg_info);
533
534 // rewrite pointer_in_range calls
536 pointer_in_range.rewrite_calls(
537 goto_program, first_instruction, last_instruction, cfg_info);
538
539 // rewrite is_fresh calls
541 is_fresh.rewrite_calls(
542 goto_program, first_instruction, last_instruction, cfg_info);
543
544 // rewrite is_freeable/was_freed calls
546 is_freeable.rewrite_calls(
547 goto_program, first_instruction, last_instruction, cfg_info);
548
549 // rewrite obeys_contract calls
551 obeys_contract.rewrite_calls(
552 goto_program,
553 first_instruction,
554 last_instruction,
555 cfg_info,
556 function_pointer_contracts);
557
558 const namespacet ns(goto_model.symbol_table);
559 auto &target = first_instruction;
560
561 // excluding the last
562 while(target != last_instruction)
563 {
564 if(target->is_decl())
565 {
566 instrument_decl(function_id, target, goto_program, cfg_info);
567 }
568 if(target->is_dead())
569 {
570 instrument_dead(function_id, target, goto_program, cfg_info);
571 }
572 else if(target->is_assign())
573 {
574 instrument_assign(function_id, target, goto_program, cfg_info);
575 }
576 else if(target->is_function_call())
577 {
578 instrument_function_call(function_id, target, goto_program, cfg_info);
579 }
580 else if(target->is_other())
581 {
582 instrument_other(function_id, target, goto_program, cfg_info);
583 }
584 // else do nothing
585 target++;
586 }
587}
588
590 const irep_idt &function_id,
591 const exprt &write_set,
592 const symbol_exprt &symbol_expr,
594 goto_programt &goto_program)
595{
596 goto_programt payload;
597 const auto &target_location = target->source_location();
598 auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
599 dfcc_utilst::make_null_check_expr(write_set), target_location));
600
602 library.write_set_add_decl_call(
603 write_set, address_of_exprt(symbol_expr), target_location),
604 target_location));
605
606 auto label_instruction =
607 payload.add(goto_programt::make_skip(target_location));
608 goto_instruction->complete_goto(label_instruction);
609
610 insert_before_swap_and_advance(goto_program, target, payload);
611}
612
620 const irep_idt &function_id,
622 goto_programt &goto_program,
623 dfcc_cfg_infot &cfg_info)
624{
625 if(!cfg_info.must_track_decl_or_dead(target))
626 return;
627 const auto &decl_symbol = target->decl_symbol();
628 auto &write_set = cfg_info.get_write_set(target);
629
630 target++;
632 function_id, write_set, decl_symbol, target, goto_program);
633 target--;
634}
635
637 const irep_idt &function_id,
638 const exprt &write_set,
639 const symbol_exprt &symbol_expr,
641 goto_programt &goto_program)
642{
643 goto_programt payload;
644 const auto &target_location = target->source_location();
645 auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
646 dfcc_utilst::make_null_check_expr(write_set), target_location));
647
649 library.write_set_record_dead_call(
650 write_set, address_of_exprt(symbol_expr), target_location),
651 target_location));
652
653 auto label_instruction =
654 payload.add(goto_programt::make_skip(target_location));
655
656 goto_instruction->complete_goto(label_instruction);
657
658 insert_before_swap_and_advance(goto_program, target, payload);
659}
660
668 const irep_idt &function_id,
670 goto_programt &goto_program,
671 dfcc_cfg_infot &cfg_info)
672{
673 if(!cfg_info.must_track_decl_or_dead(target))
674 return;
675
676 const auto &decl_symbol = target->dead_symbol();
677 auto &write_set = cfg_info.get_write_set(target);
679 function_id, write_set, decl_symbol, target, goto_program);
680}
681
683 const irep_idt &function_id,
685 const exprt &lhs,
686 goto_programt &goto_program,
687 dfcc_cfg_infot &cfg_info)
688{
689 const irep_idt &mode =
690 dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id).mode;
691
692 goto_programt payload;
693
694 const auto &lhs_source_location = target->source_location();
695 auto &write_set = cfg_info.get_write_set(target);
696 auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
697 dfcc_utilst::make_null_check_expr(write_set), lhs_source_location));
698
699 source_locationt check_source_location(target->source_location());
700 check_source_location.set_property_class("assigns");
701 check_source_location.set_comment(
702 "Check that " + from_expr_using_mode(ns, mode, lhs) + " is assignable");
703
704 // ```
705 // IF !write_set GOTO skip_target;
706 // DECL check_assign: bool;
707 // CALL check_assign = check_assignment(write_set, &lhs, sizeof(lhs));
708 // ASSERT(check_assign);
709 // DEAD check_assign;
710 // skip_target: SKIP;
711 // ----
712 // ASSIGN lhs := rhs;
713 // ```
714
715 const auto check_var = dfcc_utilst::create_symbol(
716 goto_model.symbol_table,
717 bool_typet(),
718 function_id,
719 "__check_lhs_assignment",
720 lhs_source_location);
721
722 payload.add(goto_programt::make_decl(check_var, lhs_source_location));
723
725 library.write_set_check_assignment_call(
726 check_var,
727 write_set,
731 lhs_source_location),
732 lhs_source_location));
733
734 payload.add(goto_programt::make_assertion(check_var, check_source_location));
735 payload.add(goto_programt::make_dead(check_var, check_source_location));
736
737 auto label_instruction =
738 payload.add(goto_programt::make_skip(lhs_source_location));
739 goto_instruction->complete_goto(label_instruction);
740
741 insert_before_swap_and_advance(goto_program, target, payload);
742}
743
745 const irep_idt &function_id,
747 goto_programt &goto_program,
748 dfcc_cfg_infot &cfg_info)
749{
750 const auto &lhs = target->assign_lhs();
751 const auto &rhs = target->assign_rhs();
752 const auto &target_location = target->source_location();
753 auto &write_set = cfg_info.get_write_set(target);
754
755 // check the lhs
756 if(cfg_info.must_check_lhs(target))
757 instrument_lhs(function_id, target, lhs, goto_program, cfg_info);
758
759 // is the rhs expression a side_effect("allocate") expression ?
760 if(rhs.id() == ID_side_effect && rhs.get(ID_statement) == ID_allocate)
761 {
762 // ```
763 // CALL lhs := side_effect(statement = ID_allocate, args = {size, clear});
764 // ----
765 // IF !write_set GOTO skip_target;
766 // CALL add_allocated(write_set, lhs);
767 // skip_target: SKIP;
768 // ```
769
770 // step over the instruction
771 target++;
772
773 goto_programt payload;
774 auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
775 dfcc_utilst::make_null_check_expr(write_set), target_location));
776
778 library.write_set_add_allocated_call(write_set, lhs, target_location),
779 target_location));
780
781 auto label_instruction =
782 payload.add(goto_programt::make_skip(target_location));
783 goto_instruction->complete_goto(label_instruction);
784
785 insert_before_swap_and_advance(goto_program, target, payload);
786
787 // step back
788 target--;
789 }
790}
791
793 const exprt &write_set,
795 goto_programt &goto_program)
796{
797 // Insert a dynamic lookup in __instrumented_functions_map
798 // and pass the write set only to functions that are known to be able
799 // to accept it.
800 //
801 // ```
802 // IF __instrumented_functions_map[__CPROVER_POINTER_OBJECT(fptr)] != 1
803 // GOTO no_inst;
804 // CALL [lhs] = fptr(params, write_set);
805 // GOTO end;
806 // no_inst:
807 // CALL [lhs] = fptr(params);
808 // end:
809 // SKIP;
810 // ---
811 // SKIP // [lhs] = fptr(params) turned into SKIP
812 // ```
813 const auto &target_location = target->source_location();
814 const auto &callf = target->call_function();
815 auto object_id = pointer_object(
816 (callf.id() == ID_dereference) ? to_dereference_expr(callf).pointer()
817 : address_of_exprt(callf));
818 auto index_expr = index_exprt(
819 library.get_instrumented_functions_map_symbol().symbol_expr(), object_id);
820 auto cond = notequal_exprt(index_expr, from_integer(1, unsigned_char_type()));
821 goto_programt payload;
822 auto goto_no_inst =
823 payload.add(goto_programt::make_incomplete_goto(cond, target_location));
824 code_function_callt call_inst(
825 target->call_lhs(), target->call_function(), target->call_arguments());
826 call_inst.arguments().push_back(write_set);
827 payload.add(goto_programt::make_function_call(call_inst, target_location));
828 auto goto_end_inst = payload.add(
830 auto no_inst_label = payload.add(goto_programt::make_skip(target_location));
831 goto_no_inst->complete_goto(no_inst_label);
832 code_function_callt call_no_inst(
833 target->call_lhs(), target->call_function(), target->call_arguments());
834 payload.add(goto_programt::make_function_call(call_no_inst, target_location));
835 auto end_label = payload.add(goto_programt::make_skip(target_location));
836 goto_end_inst->complete_goto(end_label);
837 // erase the original call
838 target->turn_into_skip();
839 insert_before_swap_and_advance(goto_program, target, payload);
840}
841
843 const exprt &write_set,
845 goto_programt &goto_program)
846{
847 if(target->is_function_call())
848 {
849 if(target->call_function().id() == ID_symbol)
850 {
851 // this is a function call
853 to_symbol_expr(target->call_function()).get_identifier()))
854 {
855 // pass write set argument only if function is known to be instrumented
856 target->call_arguments().push_back(write_set);
857 }
858 }
859 else
860 {
861 // This is a function pointer call. We insert a dynamic lookup into the
862 // map of instrumented functions to determine if the target function is
863 // able to accept a write set parameter.
865 write_set, target, goto_program);
866 }
867 }
868}
869
871 const irep_idt &function_id,
872 const exprt &write_set,
874 goto_programt &goto_program)
875{
876 INVARIANT(target->is_function_call(), "target must be a function call");
877 INVARIANT(
878 target->call_function().id() == ID_symbol &&
879 (id2string(to_symbol_expr(target->call_function()).get_identifier()) ==
880 CPROVER_PREFIX "deallocate"),
881 "target must be a call to" CPROVER_PREFIX "deallocate");
882
883 auto &target_location = target->source_location();
884 // ```
885 // IF !write_set GOTO skip_target;
886 // DECL check_deallocate: bool;
887 // CALL check_deallocate := check_deallocate(write_set, ptr);
888 // ASSERT(check_deallocate);
889 // DEAD check_deallocate;
890 // CALL record_deallocated(write_set, lhs);
891 // skip_target: SKIP;
892 // ----
893 // CALL __CPROVER_deallocate(ptr);
894 // ```
895 goto_programt payload;
896
897 auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
898 dfcc_utilst::make_null_check_expr(write_set), target_location));
899
900 const auto check_var = dfcc_utilst::create_symbol(
901 goto_model.symbol_table,
902 bool_typet(),
903 function_id,
904 "__check_deallocate",
905 target_location);
906
907 payload.add(goto_programt::make_decl(check_var, target_location));
908
909 const auto &ptr = target->call_arguments().at(0);
910
912 library.write_set_check_deallocate_call(
913 check_var, write_set, ptr, target_location),
914 target_location));
915
916 // add property class on assertion source_location
917 const irep_idt &mode =
918 dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id).mode;
919 source_locationt check_location(target_location);
920 check_location.set_property_class("frees");
921 std::string comment =
922 "Check that " + from_expr_using_mode(ns, mode, ptr) + " is freeable";
923 check_location.set_comment(comment);
924
925 payload.add(goto_programt::make_assertion(check_var, check_location));
926 payload.add(goto_programt::make_dead(check_var, target_location));
927
929 library.write_set_record_deallocated_call(write_set, ptr, target_location),
930 target_location));
931
932 auto label_instruction =
933 payload.add(goto_programt::make_skip(target_location));
934 goto_instruction->complete_goto(label_instruction);
935
936 insert_before_swap_and_advance(goto_program, target, payload);
937}
938
940 const irep_idt &function_id,
942 goto_programt &goto_program,
943 dfcc_cfg_infot &cfg_info)
944{
945 INVARIANT(
946 target->is_function_call(),
947 "the target must be a function call instruction");
948
949 auto &write_set = cfg_info.get_write_set(target);
950
951 // Instrument the lhs if any.
952 if(target->call_lhs().is_not_nil() && cfg_info.must_check_lhs(target))
953 {
955 function_id, target, target->call_lhs(), goto_program, cfg_info);
956 }
957
958 const auto &call_function = target->call_function();
959 if(
960 call_function.id() == ID_symbol &&
961 (id2string(to_symbol_expr(call_function).get_identifier()) == CPROVER_PREFIX
962 "deallocate"))
963 {
964 instrument_deallocate_call(function_id, write_set, target, goto_program);
965 }
966 else
967 {
968 // instrument as a normal function/function pointer call
969 instrument_call_instruction(write_set, target, goto_program);
970 }
971}
972
974 const irep_idt &function_id,
976 goto_programt &goto_program,
977 dfcc_cfg_infot &cfg_info)
978{
979 const auto &target_location = target->source_location();
980 auto &statement = target->get_other().get_statement();
981 auto &write_set = cfg_info.get_write_set(target);
982 const irep_idt &mode =
983 dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id).mode;
984
985 if(statement == ID_array_set || statement == ID_array_copy)
986 {
987 const bool is_array_set = statement == ID_array_set;
988 // ```
989 // IF !write_set GOTO skip_target;
990 // DECL check_array_set: bool;
991 // CALL check_array_set = check_array_set(write_set, dest);
992 // ASSERT(check_array_set);
993 // DEAD check_array_set;
994 // skip_target: SKIP;
995 // ----
996 // OTHER {statement = array_set, args = {dest, value}};
997 // ```
998 goto_programt payload;
999
1000 auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
1001 dfcc_utilst::make_null_check_expr(write_set), target_location));
1002
1003 const auto check_var = dfcc_utilst::create_symbol(
1004 goto_model.symbol_table,
1005 bool_typet(),
1006 function_id,
1007 is_array_set ? "__check_array_set" : "__check_array_copy",
1008 target_location);
1009
1010 payload.add(goto_programt::make_decl(check_var, target_location));
1011
1012 const auto &dest = target->get_other().operands().at(0);
1013
1015 is_array_set ? library.write_set_check_array_set_call(
1016 check_var, write_set, dest, target_location)
1017 : library.write_set_check_array_copy_call(
1018 check_var, write_set, dest, target_location),
1019 target_location));
1020
1021 // add property class on assertion source_location
1022 source_locationt check_location(target_location);
1023 check_location.set_property_class("assigns");
1024
1025 std::string fun_name = is_array_set ? "array_set" : "array_copy";
1026
1027 std::string comment = "Check that " + fun_name + "(" +
1028 from_expr_using_mode(ns, mode, dest) +
1029 ", ...) is allowed by the assigns clause";
1030 check_location.set_comment(comment);
1031
1032 payload.add(goto_programt::make_assertion(check_var, check_location));
1033 payload.add(goto_programt::make_dead(check_var, target_location));
1034
1035 auto label_instruction =
1036 payload.add(goto_programt::make_skip(target_location));
1037 goto_instruction->complete_goto(label_instruction);
1038
1039 insert_before_swap_and_advance(goto_program, target, payload);
1040 }
1041 else if(statement == ID_array_replace)
1042 {
1043 // ```
1044 // IF !write_set GOTO skip_target;
1045 // DECL check_array_replace: bool;
1046 // CALL check_array_replace = check_array_replace(write_set, dest);
1047 // ASSERT(check_array_replace);
1048 // DEAD check_array_replace;
1049 // skip_target: SKIP;
1050 // ----
1051 // OTHER {statement = array_replace, args = {dest, src}};
1052 // ```
1053 goto_programt payload;
1054
1055 auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
1056 dfcc_utilst::make_null_check_expr(write_set), target_location));
1057
1058 const auto check_var = dfcc_utilst::create_symbol(
1059 goto_model.symbol_table,
1060 bool_typet(),
1061 function_id,
1062 "__check_array_replace",
1063 target_location);
1064
1065 payload.add(goto_programt::make_decl(check_var, target_location));
1066
1067 const auto &dest = target->get_other().operands().at(0);
1068 const auto &src = target->get_other().operands().at(1);
1069
1071 library.write_set_check_array_replace_call(
1072 check_var, write_set, dest, src, target_location),
1073 target_location));
1074
1075 // add property class on assertion source_location
1076 source_locationt check_location(target_location);
1077 check_location.set_property_class("assigns");
1078 std::string comment = "Check that array_replace(" +
1079 from_expr_using_mode(ns, mode, dest) +
1080 ", ...) is allowed by the assigns clause";
1081 check_location.set_comment(comment);
1082
1083 payload.add(goto_programt::make_assertion(check_var, check_location));
1084 payload.add(goto_programt::make_dead(check_var, target_location));
1085
1086 auto label_instruction =
1087 payload.add(goto_programt::make_skip(target_location));
1088 goto_instruction->complete_goto(label_instruction);
1089
1090 insert_before_swap_and_advance(goto_program, target, payload);
1091 }
1092 else if(statement == ID_havoc_object)
1093 {
1094 // insert before instruction
1095 // ```
1096 // IF !write_set GOTO skip_target;
1097 // DECL check_havoc_object: bool;
1098 // CALL check_havoc_object = check_havoc_object(write_set, ptr);
1099 // ASSERT(check_havoc_object);
1100 // DEAD check_havoc_object;
1101 // ```
1102 goto_programt payload;
1103
1104 auto goto_instruction = payload.add(goto_programt::make_incomplete_goto(
1105 dfcc_utilst::make_null_check_expr(write_set), target_location));
1106
1107 const auto check_var = dfcc_utilst::create_symbol(
1108 goto_model.symbol_table,
1109 bool_typet(),
1110 function_id,
1111 "__check_havoc_object",
1112 target_location);
1113
1114 payload.add(goto_programt::make_decl(check_var, target_location));
1115
1116 const auto &ptr = target->get_other().operands().at(0);
1117
1119 library.write_set_check_havoc_object_call(
1120 check_var, write_set, ptr, target_location),
1121 target_location));
1122
1123 // add property class on assertion source_location
1124 source_locationt check_location(target_location);
1125 check_location.set_property_class("assigns");
1126 std::string comment = "Check that havoc_object(" +
1127 from_expr_using_mode(ns, mode, ptr) +
1128 ") is allowed by the assigns clause";
1129 check_location.set_comment(comment);
1130
1131 payload.add(goto_programt::make_assertion(check_var, check_location));
1132 payload.add(goto_programt::make_dead(check_var, target_location));
1133
1134 auto label_instruction =
1135 payload.add(goto_programt::make_skip(target_location));
1136 goto_instruction->complete_goto(label_instruction);
1137
1138 insert_before_swap_and_advance(goto_program, target, payload);
1139 }
1140 else if(statement == ID_expression)
1141 {
1142 // When in Rome do like the Romans (cf src/pointer_analysis/value_set.cpp)
1143 // can be ignored, we don't expect side effects here
1144 }
1145 else
1146 {
1147 // Other cases not presently handled
1148 // * ID_array_equal
1149 // * ID_decl track new symbol ?
1150 // * ID_cpp_delete
1151 // * ID_printf track as side effect on stdout ?
1152 // * code_inputt track as nondet ?
1153 // * code_outputt track as side effect on stdout ?
1154 // * ID_nondet track as nondet ?
1155 // * ID_asm track as side effect depending on the instruction ?
1156 // * ID_user_specified_predicate
1157 // should be pure ?
1158 // * ID_user_specified_parameter_predicates
1159 // should be pure ?
1160 // * ID_user_specified_return_predicates
1161 // should be pure ?
1162 // * ID_fence
1163 // bail out ?
1164 log.warning().source_location = target_location;
1165 log.warning() << "dfcc_instrument::instrument_other: statement type '"
1166 << statement << "' is not supported, analysis may be unsound"
1167 << messaget::eom;
1168 }
1169}
1170
1172 const irep_idt &function_id,
1173 goto_functiont &goto_function,
1174 dfcc_cfg_infot &cfg_info,
1175 const loop_contract_configt &loop_contract_config,
1176 const std::set<symbol_exprt> &local_statics,
1177 std::set<irep_idt> &function_pointer_contracts)
1178{
1179 PRECONDITION(loop_contract_config.apply_loop_contracts);
1180 cfg_info.get_loops_toposorted();
1181
1182 std::list<std::string> to_unwind;
1183
1184 // Apply loop contract transformations in topological order
1185 for(const auto &loop_id : cfg_info.get_loops_toposorted())
1186 {
1187 const auto &loop = cfg_info.get_loop_info(loop_id);
1188 if(loop.must_skip())
1189 {
1190 // skip loops that do not have contracts
1191 log.warning() << "loop " << function_id << "." << loop.cbmc_loop_id
1192 << " does not have a contract, skipping instrumentation"
1193 << messaget::eom;
1194 continue;
1195 }
1196
1198 loop_id,
1199 function_id,
1200 goto_function,
1201 cfg_info,
1202 local_statics,
1203 function_pointer_contracts);
1204 to_unwind.push_back(
1205 id2string(function_id) + "." + std::to_string(loop.cbmc_loop_id) + ":2");
1206 }
1207
1208 // If required, unwind all transformed loops to yield base and step cases
1209 if(loop_contract_config.unwind_transformed_loops)
1210 {
1211 unwindsett unwindset{goto_model};
1212 unwindset.parse_unwindset(to_unwind, log.get_message_handler());
1213 goto_unwindt goto_unwind;
1214 goto_unwind(goto_model, unwindset, goto_unwindt::unwind_strategyt::ASSUME);
1215 }
1216
1217 remove_skip(goto_function.body);
1218}
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 ...
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_contract_clauses_codegent & contract_clauses_codegen
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...
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.
dfcc_spec_functionst & spec_functions
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.
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_equals predicates into calls to the library implementation.
void rewrite_calls(goto_programt &program, dfcc_cfg_infot cfg_info)
Rewrites calls to pointer_equals 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:
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
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_programt body
bool body_available() const
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.
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
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:91
Disequality.
Definition std_expr.h:1425
The null pointer constant.
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
irep_idt mode
Language mode.
Definition symbol.h:49
The Boolean constant true.
Definition std_expr.h:3195
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_equals 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
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
dstringt irep_idt