cprover
Loading...
Searching...
No Matches
dfcc_wrapper_program.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking for function contracts
4
5Author: Remi Delmas, delmasrd@amazon.com
6
7\*******************************************************************/
9
10#include <util/arith_tools.h>
11#include <util/c_types.h>
12#include <util/expr_util.h>
13#include <util/format_expr.h>
14#include <util/invariant.h>
16#include <util/namespace.h>
18#include <util/std_expr.h>
19
21
22#include <ansi-c/c_expr.h>
25
27#include "dfcc_instrument.h"
28#include "dfcc_library.h"
30#include "dfcc_utils.h"
31
34 symbol_table_baset &symbol_table,
35 dfcc_libraryt &library,
36 const symbolt &wrapper_symbol)
37{
39 symbol_table,
41 wrapper_symbol.name,
42 "__contract_write_set",
43 wrapper_symbol.location);
44}
45
48 symbol_table_baset &symbol_table,
49 dfcc_libraryt &library,
50 const symbolt &wrapper_symbol)
51{
53 symbol_table,
55 wrapper_symbol.name,
56 "__address_of_contract_write_set",
57 wrapper_symbol.location);
58}
59
60// Generate the write set to check for side effects in requires clauses
62 symbol_table_baset &symbol_table,
63 dfcc_libraryt &library,
64 const symbolt &wrapper_symbol)
65{
67 symbol_table,
69 wrapper_symbol.name,
70 "__requires_write_set",
71 wrapper_symbol.location);
72}
73
76 symbol_table_baset &symbol_table,
77 dfcc_libraryt &library,
78 const symbolt &wrapper_symbol)
79{
81 symbol_table,
83 wrapper_symbol.name,
84 "__address_of_requires_write_set",
85 wrapper_symbol.location);
86}
87
90 symbol_table_baset &symbol_table,
91 dfcc_libraryt &library,
92 const symbolt &wrapper_symbol)
93{
95 symbol_table,
97 wrapper_symbol.name,
98 "__ensures_write_set",
99 wrapper_symbol.location);
100}
101
104 symbol_table_baset &symbol_table,
105 dfcc_libraryt &library,
106 const symbolt &wrapper_symbol)
107{
109 symbol_table,
111 wrapper_symbol.name,
112 "__address_of_ensures_write_set",
113 wrapper_symbol.location);
114}
115
118 symbol_table_baset &symbol_table,
119 dfcc_libraryt &library,
120 const symbolt &wrapper_symbol)
121{
123 symbol_table,
125 wrapper_symbol.name,
126 "__is_fresh_set",
127 wrapper_symbol.location);
128}
129
132 symbol_table_baset &symbol_table,
133 dfcc_libraryt &library,
134 const symbolt &wrapper_symbol)
135{
137 symbol_table,
139 wrapper_symbol.name,
140 "__address_of_is_fresh_set",
141 wrapper_symbol.location);
142}
143
146 const symbolt &wrapper_symbol,
147 const symbolt &wrapped_symbol,
149 const symbolt &caller_write_set_symbol,
159 contract_symbol(contract_functions.pure_contract_symbol),
161 caller_write_set(caller_write_set_symbol.symbol_expr()),
162 wrapper_sl(wrapper_symbol.location),
165 goto_model.symbol_table,
166 library,
169 goto_model.symbol_table,
170 library,
173 goto_model.symbol_table,
174 library,
177 goto_model.symbol_table,
178 library,
181 goto_model.symbol_table,
182 library,
185 goto_model.symbol_table,
186 library,
191 goto_model.symbol_table,
192 library,
201 ns(goto_model.symbol_table),
202 converter(goto_model.symbol_table, log.get_message_handler())
203{
204 // generate a return value symbol (needed to instantiate all contract lambdas)
205 if(contract_code_type.return_type().id() != ID_empty)
206 {
207 return_value_opt = dfcc_utilst::create_symbol(
208 goto_model.symbol_table,
209 contract_code_type.return_type(),
210 wrapper_symbol.name,
211 "__contract_return_value",
212 wrapper_symbol.location);
213
214 // build contract_lambda_parameters
215 contract_lambda_parameters.push_back(return_value_opt.value());
216 }
217
218 // build contract_lambda_parameters
219 for(const auto &param_id :
220 to_code_type(wrapper_symbol.type).parameter_identifiers())
221 {
222 contract_lambda_parameters.push_back(ns.lookup(param_id).symbol_expr());
223 }
224
225 // encode all contract clauses
233}
234
236 goto_programt &dest,
237 std::set<irep_idt> &dest_fp_contracts)
238{
239 add_to_dest(dest);
240 dest_fp_contracts.insert(
242}
243
258
260{
261 // call write_set_create(
262 // requires_write_set,
263 // assigns_size = 0,
264 // frees_size = 0,
265 // replacement_mode = false,
266 // assume_requires_ctx = contract_mode == check,
267 // assert_requires_ctx = contract_mode != check,
268 // assume_ensures_ctx = false,
269 // assert_ensures_ctx = false,
270 // )
272
273 preamble.add(
278 wrapper_sl));
279
280 bool check_mode = contract_mode == dfcc_contract_modet::CHECK;
281 code_function_callt call = library.write_set_create_call(
285 make_boolean_expr(check_mode),
286 make_boolean_expr(!check_mode),
287 false_exprt(),
288 false_exprt(),
289 true_exprt(),
290 true_exprt(),
291 wrapper_sl);
292
294
295 // check for absence of allocation/deallocation in requires clauses
296 // ```c
297 // DECL __check_no_alloc: bool;
298 // CALL __check_no_alloc = check_empty_alloc_dealloc(requilres_write_set);
299 // ASSERT __check_no_alloc;
300 // DEAD __check_no_alloc: bool;
301 // ```
302 const auto check_var = dfcc_utilst::create_symbol(
303 goto_model.symbol_table,
304 bool_typet(),
305 wrapper_symbol.name,
306 "__no_alloc_dealloc_in_requires",
307 wrapper_sl);
308
310
312 library.write_set_check_allocated_deallocated_is_empty_call(
314 wrapper_sl));
315
317 check_sl.set_function(wrapper_symbol.name);
318 check_sl.set_property_class("no_alloc_dealloc_in_requires");
319 check_sl.set_comment(
320 "Check that requires do not allocate or deallocate memory");
321 postamble.add(goto_programt::make_assertion(check_var, check_sl));
323
324 // generate write set release and DEAD instructions
326 library.write_set_release_call(addr_of_requires_write_set, wrapper_sl),
327 wrapper_sl));
329}
330
332{
333 // call write_set_create(
334 // ensures_write_set,
335 // assigns_size = 0,
336 // frees_size = 0,
337 // assume_requires_ctx = false,
338 // assert_requires_ctx = false,
339 // assume_ensures_ctx = contract_mode != check,
340 // assert_ensures_ctx = contract_mode == check,
341 // )
343
348 wrapper_sl));
349
350 bool check_mode = contract_mode == dfcc_contract_modet::CHECK;
351
352 code_function_callt call = library.write_set_create_call(
356 false_exprt(),
357 false_exprt(),
358 make_boolean_expr(!check_mode),
359 make_boolean_expr(check_mode),
360 true_exprt(),
361 true_exprt(),
362 wrapper_sl);
363
365
366 // call link_allocated(pre_post, caller) if in REPLACE MODE
368 {
370 library.link_allocated_call(
372 wrapper_sl));
373 }
374
375 // check for absence of allocation/deallocation in contract clauses
376 // ```c
377 // DECL __check_no_alloc: bool;
378 // CALL __check_no_alloc = check_empty_alloc_dealloc(ensures_write_set);
379 // ASSERT __check_no_alloc;
380 // DEAD __check_no_alloc: bool;
381 // ```
382 const auto check_var = dfcc_utilst::create_symbol(
383 goto_model.symbol_table,
384 bool_typet(),
385 wrapper_symbol.name,
386 "__no_alloc_dealloc_in_ensures_clauses",
387 wrapper_sl);
388
390
392 library.write_set_check_allocated_deallocated_is_empty_call(
394 wrapper_sl));
395
397 check_sl.set_function(wrapper_symbol.name);
398 check_sl.set_property_class("no_alloc_dealloc_in_ensures");
399 check_sl.set_comment(
400 "Check that ensures do not allocate or deallocate memory");
401
402 postamble.add(goto_programt::make_assertion(check_var, check_sl));
404
405 // generate write set release
407 library.write_set_release_call(addr_of_ensures_write_set, wrapper_sl),
408 wrapper_sl));
409
410 // declare write set DEAD
412}
413
415{
417
418 preamble.add(
423 wrapper_sl));
424
425 // We use the empty write set used to check ensures for side effects
426 // to check for side effects in the assigns and frees functions as well
427 // TODO: I don't know what the above comment means, why was there an empty
428 // write set here?
429
430 // call write_set_create
431 {
432 code_function_callt call = library.write_set_create_call(
434 from_integer(contract_functions.get_nof_assigns_targets(), size_type()),
435 from_integer(contract_functions.get_nof_frees_targets(), size_type()),
436 false_exprt(),
437 false_exprt(),
438 false_exprt(),
439 false_exprt(),
440 true_exprt(),
441 true_exprt(),
442 wrapper_sl);
444 }
445
446 // build arguments for assigns and frees clauses functions
447 exprt::operandst wrapper_arguments;
448 const auto &wrapper_code_type = to_code_type(wrapper_symbol.type);
449 for(const auto &parameter : wrapper_code_type.parameter_identifiers())
450 {
451 const symbolt &parameter_symbol = ns.lookup(parameter);
452 wrapper_arguments.push_back(parameter_symbol.symbol_expr());
453 }
454
455 // call spec_assigns to build the contract write set
456 {
458 contract_functions.get_spec_assigns_function_symbol().symbol_expr());
459
460 auto &arguments = call.arguments();
461
462 // forward wrapper arguments
463 for(const auto &arg : wrapper_arguments)
464 arguments.push_back(arg);
465
466 // pass write set to populate
467 arguments.emplace_back(addr_of_contract_write_set);
468
469 // pass the empty write set to check side effects against
470 arguments.emplace_back(addr_of_requires_write_set);
471
473 }
474
475 // call spec_frees to build the contract write set
476 {
478 contract_functions.get_spec_frees_function_symbol().symbol_expr());
479 auto &arguments = call.arguments();
480
481 // forward wrapper arguments
482 for(const auto &arg : wrapper_arguments)
483 arguments.push_back(arg);
484
485 // pass write set to populate
486 arguments.emplace_back(addr_of_contract_write_set);
487
488 // pass the empty write set to check side effects against
489 arguments.emplace_back(addr_of_requires_write_set);
490
492 }
493
494 // generate write set release and DEAD instructions
496 library.write_set_release_call(addr_of_contract_write_set, wrapper_sl),
497 wrapper_sl));
498 postamble.add(
500}
501
503{
505
509
510 // CALL obj_set_create_indexed_by_object_id(is_fresh_set) in preamble
512 library.obj_set_create_indexed_by_object_id_call(
514 wrapper_sl));
515
516 // link to requires write set
518 library.link_is_fresh_call(
520 wrapper_sl));
521
522 // link to ensures write set
524 library.link_is_fresh_call(
526 wrapper_sl));
527
528 // release call in postamble
530 library.obj_set_release_call(addr_of_is_fresh_set, wrapper_sl),
531 wrapper_sl));
532
533 // DEAD instructions in postamble
535}
536
538{
539 // we use this empty requires write set to check for the absence of side
540 // effects in the requires clauses
541 const auto &wrapper_id = wrapper_symbol.name;
542 const auto &language_mode =
543 dfcc_utilst::get_function_symbol(goto_model.symbol_table, wrapper_id).mode;
544
545 // if in replacement mode, check that assertions hold in the current context,
546 // otherwise assume
547 const auto &statement_type =
548 (contract_mode == dfcc_contract_modet::REPLACE) ? ID_assert : ID_assume;
549
550 // goto program where all requires are added
551 goto_programt requires_program;
552
553 // translate each requires clause
554 for(const auto &r : contract_code_type.c_requires())
555 {
556 exprt requires_lmbd =
558 source_locationt sl(r.source_location());
559 if(statement_type == ID_assert)
560 {
561 sl.set_property_class(ID_precondition);
562 sl.set_comment(
563 "Check requires clause of contract " + id2string(contract_symbol.name) +
564 " for function " + id2string(wrapper_id));
565 }
566 codet requires_statement(statement_type, {std::move(requires_lmbd)}, sl);
567 converter.goto_convert(requires_statement, requires_program, language_mode);
568 }
569
570 // fix calls to user-defined memory predicates
571 memory_predicates.fix_calls(requires_program);
572
573 // instrument for side effects
574 // make the program well-formed
575 requires_program.add(goto_programt::make_end_function());
576 instrument.instrument_goto_program(
577 wrapper_id,
578 requires_program,
581 // turn it back into a sequence of statements
582 requires_program.instructions.back().turn_into_skip();
583
584 // append resulting program to preconditions section
585 preconditions.destructive_append(requires_program);
586}
587
589{
590 const auto &language_mode = wrapper_symbol.mode;
591 const auto &wrapper_id = wrapper_symbol.name;
592 const auto &statement_type =
593 (contract_mode == dfcc_contract_modet::CHECK) ? ID_assert : ID_assume;
594
595 // goto program where all requires are added
596 goto_programt ensures_program;
597
598 // translate each ensures clause
599 for(const auto &e : contract_code_type.c_ensures())
600 {
601 exprt ensures = to_lambda_expr(e)
604
605 // this also rewrites ID_old expressions to fresh variables
607 goto_model.symbol_table, ensures, language_mode, history);
608
609 source_locationt sl(e.source_location());
610 if(statement_type == ID_assert)
611 {
612 sl.set_property_class(ID_postcondition);
613 sl.set_comment(
614 "Check ensures clause of contract " + id2string(contract_symbol.name) +
615 " for function " + id2string(wrapper_id));
616 }
617
618 codet ensures_statement(statement_type, {std::move(ensures)}, sl);
619 converter.goto_convert(ensures_statement, ensures_program, language_mode);
620 }
621
622 // When checking an ensures clause we link the contract write set to the
623 // ensures write set to know what was deallocated by the function so that
624 // the was_freed predicate can perform its checks
626 library.link_deallocated_call(
628 wrapper_sl));
629
630 // fix calls to user-defined user-defined memory predicates
631 memory_predicates.fix_calls(ensures_program);
632
633 // instrument for side effects
634 // make the program well-formed
635 ensures_program.add(goto_programt::make_end_function());
636 instrument.instrument_goto_program(
637 wrapper_id,
638 ensures_program,
641 // turn it back into a sequence of statements
642 ensures_program.instructions.back().turn_into_skip();
643
644 // add the ensures program to the postconditions section
645 postconditions.destructive_append(ensures_program);
646}
647
655
657{
658 // build call to the wrapped function
659 code_function_callt call(wrapped_symbol.symbol_expr());
660
662 {
663 symbol_exprt return_value = return_value_opt.value();
664 // DECL
665 preamble.add(goto_programt::make_decl(return_value, wrapper_sl));
666 call.lhs() = return_value;
667
668 // SET_RETURN_VALUE
669 postamble.add(
671
672 // DEAD
674 }
675
676 // forward wrapper arguments
677 const auto &wrapper_code_type = to_code_type(wrapper_symbol.type);
678
679 for(const auto &parameter : wrapper_code_type.parameter_identifiers())
680 {
681 PRECONDITION(!parameter.empty());
682 const symbolt &parameter_symbol = ns.lookup(parameter);
683 call.arguments().push_back(parameter_symbol.symbol_expr());
684 }
685
686 // pass write set to check against
687 call.arguments().push_back(addr_of_contract_write_set);
688
690}
691
693{
694 // generate local write set and add as parameter to the call
695 exprt::operandst write_set_arguments;
696 for(const auto &parameter :
698 {
699 PRECONDITION(!parameter.empty());
700 const symbolt &parameter_symbol = ns.lookup(parameter);
701 write_set_arguments.push_back(parameter_symbol.symbol_expr());
702 }
703
704 // check assigns clause inclusion
705 // IF __caller_write_set==NULL GOTO skip_target;
706 // DECL check: bool;
707 // CALL check = __CPROVER_contracts_write_set_check_assigns_clause_inclusion(
708 // __caller_write_set, &__local_write_set);
709 // ASSERT check;
710 // CALL check = __CPROVER_contracts_write_set_check_frees_clause_inclusion(
711 // __caller_write_set, &__local_write_set);
712 // ASSERT check;
713 // DEAD check;
714 // skip_target: skip;
715
716 auto goto_instruction =
719
720 {
721 // assigns clause inclusion
722 const auto check_var = dfcc_utilst::create_symbol(
723 goto_model.symbol_table,
724 bool_typet(),
725 wrapper_symbol.name,
726 "__check_assigns_clause_incl",
727 wrapper_sl);
728
730
732 library.write_set_check_assigns_clause_inclusion_call(
734 wrapper_sl));
735
737 check_sl.set_function(wrapper_symbol.name);
738 check_sl.set_property_class("assigns");
739 check_sl.set_comment(
740 "Check that the assigns clause of " + id2string(contract_symbol.name) +
741 " is included in the caller's assigns clause");
742 write_set_checks.add(goto_programt::make_assertion(check_var, check_sl));
744 }
745
746 {
747 // frees clause inclusion
748 const auto check_var = dfcc_utilst::create_symbol(
749 goto_model.symbol_table,
750 bool_typet(),
751 wrapper_symbol.name,
752 "__check_frees_clause_incl",
753 wrapper_sl);
754
756
758 library.write_set_check_frees_clause_inclusion_call(
760 wrapper_sl));
761
763 check_sl.set_function(wrapper_symbol.name);
764 check_sl.set_property_class("frees");
765 check_sl.set_comment(
766 "Check that the frees clause of " + id2string(contract_symbol.name) +
767 " is included in the caller's frees clause");
768 write_set_checks.add(goto_programt::make_assertion(check_var, check_sl));
770 }
771
772 auto label_instruction =
774 goto_instruction->complete_goto(label_instruction);
775
776 code_function_callt havoc_call(
777 contract_functions.get_spec_assigns_havoc_function_symbol().symbol_expr(),
778 {addr_of_contract_write_set});
779
781
782 // assign nondet to the return value
783 if(return_value_opt.has_value())
784 {
785 symbol_exprt return_value = return_value_opt.value();
786
787 // DECL
788 preamble.add(goto_programt::make_decl(return_value, wrapper_sl));
789
790 // ASSIGN NONDET
792 return_value,
794 wrapper_sl));
795
796 // SET RETURN VALUE
797 postamble.add(
799
800 // DEAD
802 }
803
804 // nondet free the freeable set, record effects in both the contract write
805 // set and the caller write set
807 library.write_set_deallocate_freeable_call(
809 wrapper_sl));
810}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
API to expression classes that are internal to the C frontend.
unsignedbv_typet size_type()
Definition c_types.cpp:50
const code_with_contract_typet & to_code_with_contract_type(const typet &type)
Cast a typet to a code_with_contract_typet.
Definition c_types.h:467
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.
std::vector< irep_idt > parameter_identifiers() const
Produces the list of parameter identifiers.
Definition std_types.h:740
Data structure for representing an arbitrary statement in a program.
Generates GOTO functions modelling a contract assigns and frees clauses.
This class instruments GOTO functions or instruction sequences for frame condition checking and loop ...
Class interface to library types and functions defined in cprover_contracts.c.
std::map< dfcc_typet, typet > dfcc_type
Maps enum values to the actual types (dynamically loaded)
const source_locationt wrapper_sl
Source location with wrapper function name as function name.
void encode_ensures_clauses()
Encodes postconditions, instruments them to check for side effects.
const symbol_exprt contract_write_set
Symbol for the write set object derived from the contract.
void encode_havoced_function_call()
Creates instructions that havoc the contract write set, create a nondet return value,...
const symbol_exprt caller_write_set
void encode_requires_write_set()
Encodes the empty write set used to check for side effects in requires.
void encode_requires_clauses()
Encodes preconditions, instruments them to check for side effects.
void encode_is_fresh_set()
Encodes the object set used to evaluate is fresh predicates,.
const symbol_exprt addr_of_requires_write_set
Symbol for the pointer to the write set used to check requires clauses.
void encode_contract_write_set()
Encodes the write set of the contract being checked/replaced (populated by calling functions provided...
const dfcc_contract_functionst & contract_functions
message_handlert & message_handler
const code_with_contract_typet & contract_code_type
const symbol_exprt requires_write_set
Symbol for the write set used to check requires clauses for side effects.
exprt::operandst contract_lambda_parameters
Vector of arguments to use to instantiate the lambdas wrapping the contract clauses.
const symbol_exprt addr_of_ensures_write_set
Symbol for the pointer to the write set used to check ensures clauses.
const dfcc_contract_modet contract_mode
void encode_checked_function_call()
Creates a checked function call to the wrapped function, passing it the contract-derived write set as...
std::set< irep_idt > function_pointer_contracts
Set of required or ensured contracts for function pointers discovered when processing the contract of...
const symbol_exprt addr_of_is_fresh_set
Symbol for the pointer to the is_fresh object set.
dfcc_lift_memory_predicatest & memory_predicates
void add_to_dest(goto_programt &dest, std::set< irep_idt > &dest_fp_contracts)
Adds the whole program to dest and the discovered function pointer contracts dest_fp_contracts.
void encode_function_call()
Encodes the function call section of the wrapper program.
dfcc_wrapper_programt(const dfcc_contract_modet contract_mode, const symbolt &wrapper_symbol, const symbolt &wrapped_symbol, const dfcc_contract_functionst &contract_functions, const symbolt &caller_write_set_symbol, goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_instrumentt &instrument, dfcc_lift_memory_predicatest &memory_predicates)
const symbol_exprt addr_of_contract_write_set
Symbol for the pointer to the write set object derived from the contract.
const symbol_exprt ensures_write_set
Symbol for the write set used to check ensures clauses for side effects.
std::optional< symbol_exprt > return_value_opt
Symbol for the return value of the wrapped function.
dfcc_instrumentt & instrument
void encode_ensures_write_set()
Encodes the empty write set used to check for side effects in ensures.
goto_programt link_deallocated_contract
const symbol_exprt is_fresh_set
Symbol for the object set used to evaluate is_fresh predicates.
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
typet & type()
Return the type of the expression.
Definition expr.h:84
exprt & with_source_location(source_locationt location) &
Add the source location from location, if it is non-nil.
Definition expr.h:101
The Boolean constant false.
Definition std_expr.h:3077
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
static instructiont make_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
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())
exprt application(const operandst &arguments) const
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
void set_function(const irep_idt &function)
Expression to hold a symbol (variable)
Definition std_expr.h:131
The symbol table base class interface.
Symbol table entry.
Definition symbol.h:28
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
irep_idt name
The unique identifier.
Definition symbol.h:40
irep_idt mode
Language mode.
Definition symbol.h:49
The Boolean constant true.
Definition std_expr.h:3068
Translates assigns and frees clauses of a function contract into goto functions that allow to build a...
dfcc_contract_modet
Enum type representing the contract checking and replacement modes.
Add instrumentation to a goto program to perform frame condition checks.
Dynamic frame condition checking library loading.
@ WRITE_SET
type of descriptors of assignable/freeable sets of locations
@ OBJ_SET_PTR
type of pointers to sets of object identifiers
@ OBJ_SET
type of sets of object identifiers
@ WRITE_SET_PTR
type of pointers to descriptors of assignable/freeable sets of locations
Collects all user-defined predicates that call functions is_fresh, pointer_in_range,...
Dynamic frame condition checking utility functions.
static symbol_exprt create_requires_write_set(symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
static symbol_exprt create_addr_of_contract_write_set(symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
Generate the contract write set pointer.
static symbol_exprt create_addr_of_ensures_write_set(symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
Generate the write set pointer to check side effects in ensures clauses.
static symbol_exprt create_addr_of_is_fresh_set(symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
Generate object set pointer used to support is_fresh predicates.
static symbol_exprt create_addr_of_requires_write_set(symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
Generate the write set pointer to check side effects in requires clauses.
static symbol_exprt create_ensures_write_set(symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
Generate the write set to check side effects in ensures clauses.
static symbol_exprt create_contract_write_set(symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
Generate the contract write set.
static symbol_exprt create_is_fresh_set(symbol_table_baset &symbol_table, dfcc_libraryt &library, const symbolt &wrapper_symbol)
Generate object set used to support is_fresh predicates.
Generates the body of a wrapper function from a contract for contract checking or contract replacemen...
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Deprecated expression utility functions.
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
static int8_t r
Definition irep_hash.h:60
API to expression classes for 'mathematical' expressions.
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
Pointer Logic.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
API to expression classes.
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 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...
void generate_history_variables_initialization(symbol_table_baset &symbol_table, exprt &clause, const irep_idt &mode, goto_programt &program)
This function generates all the instructions required to initialize history variables.
Definition utils.cpp:494