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
145 const dfcc_contract_modet contract_mode,
146 const symbolt &wrapper_symbol,
147 const symbolt &wrapped_symbol,
148 const dfcc_contract_functionst &contract_functions,
149 const symbolt &caller_write_set_symbol,
150 goto_modelt &goto_model,
151 message_handlert &message_handler,
152 dfcc_libraryt &library,
153 dfcc_instrumentt &instrument,
154 dfcc_lift_memory_predicatest &memory_predicates)
155 : contract_mode(contract_mode),
156 wrapper_symbol(wrapper_symbol),
157 wrapped_symbol(wrapped_symbol),
158 contract_functions(contract_functions),
159 contract_symbol(contract_functions.pure_contract_symbol),
160 contract_code_type(to_code_with_contract_type(contract_symbol.type)),
161 caller_write_set(caller_write_set_symbol.symbol_expr()),
162 wrapper_sl(wrapper_symbol.location),
163 return_value_opt(),
164 contract_write_set(create_contract_write_set(
165 goto_model.symbol_table,
166 library,
167 wrapper_symbol)),
168 addr_of_contract_write_set(create_addr_of_contract_write_set(
169 goto_model.symbol_table,
170 library,
171 wrapper_symbol)),
172 requires_write_set(create_requires_write_set(
173 goto_model.symbol_table,
174 library,
175 wrapper_symbol)),
176 addr_of_requires_write_set(create_addr_of_requires_write_set(
177 goto_model.symbol_table,
178 library,
179 wrapper_symbol)),
180 ensures_write_set(create_ensures_write_set(
181 goto_model.symbol_table,
182 library,
183 wrapper_symbol)),
184 addr_of_ensures_write_set(create_addr_of_ensures_write_set(
185 goto_model.symbol_table,
186 library,
187 wrapper_symbol)),
188 is_fresh_set(
189 create_is_fresh_set(goto_model.symbol_table, library, wrapper_symbol)),
190 addr_of_is_fresh_set(create_addr_of_is_fresh_set(
191 goto_model.symbol_table,
192 library,
193 wrapper_symbol)),
194 function_pointer_contracts(),
195 goto_model(goto_model),
196 message_handler(message_handler),
197 log(message_handler),
198 library(library),
199 instrument(instrument),
200 memory_predicates(memory_predicates),
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 {
211 "__contract_return_value",
213
214 // build contract_lambda_parameters
216 }
217
218 // build contract_lambda_parameters
219 for(const auto &param_id :
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
278 wrapper_sl));
279
280 bool check_mode = contract_mode == dfcc_contract_modet::CHECK;
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(
304 bool_typet(),
306 "__no_alloc_dealloc_in_requires",
307 wrapper_sl);
308
310
314 wrapper_sl));
315
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
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
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 {
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(
384 bool_typet(),
386 "__no_alloc_dealloc_in_ensures_clauses",
387 wrapper_sl);
388
390
394 wrapper_sl));
395
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
408 wrapper_sl));
409
410 // declare write set DEAD
412}
413
415{
417
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 {
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 {
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 {
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
497 wrapper_sl));
500}
501
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 =
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 requires_lmbd.add_source_location() = r.source_location();
559 if(
560 has_subexpr(requires_lmbd, ID_exists) ||
561 has_subexpr(requires_lmbd, ID_forall))
563 goto_model.symbol_table, requires_lmbd, language_mode);
564
565 source_locationt sl(r.source_location());
566 if(statement_type == ID_assert)
567 {
568 sl.set_property_class(ID_precondition);
569 sl.set_comment(
570 "Check requires clause of contract " + id2string(contract_symbol.name) +
571 " for function " + id2string(wrapper_id));
572 }
573 codet requires_statement(statement_type, {std::move(requires_lmbd)}, sl);
574 converter.goto_convert(requires_statement, requires_program, language_mode);
575 }
576
577 // fix calls to user-defined memory predicates
578 memory_predicates.fix_calls(requires_program);
579
580 // instrument for side effects
581 // make the program well-formed
582 requires_program.add(goto_programt::make_end_function());
584 wrapper_id,
585 requires_program,
588 // turn it back into a sequence of statements
589 requires_program.instructions.back().turn_into_skip();
590
591 // append resulting program to preconditions section
592 preconditions.destructive_append(requires_program);
593}
594
596{
597 const auto &language_mode = wrapper_symbol.mode;
598 const auto &wrapper_id = wrapper_symbol.name;
599 const auto &statement_type =
600 (contract_mode == dfcc_contract_modet::CHECK) ? ID_assert : ID_assume;
601
602 // goto program where all requires are added
603 goto_programt ensures_program;
604
605 // translate each ensures clause
606 for(const auto &e : contract_code_type.c_ensures())
607 {
608 exprt ensures = to_lambda_expr(e)
611
612 if(has_subexpr(ensures, ID_exists) || has_subexpr(ensures, ID_forall))
613 add_quantified_variable(goto_model.symbol_table, ensures, language_mode);
614
615 // this also rewrites ID_old expressions to fresh variables
617 goto_model.symbol_table, ensures, language_mode, history);
618
619 source_locationt sl(e.source_location());
620 if(statement_type == ID_assert)
621 {
622 sl.set_property_class(ID_postcondition);
623 sl.set_comment(
624 "Check ensures clause of contract " + id2string(contract_symbol.name) +
625 " for function " + id2string(wrapper_id));
626 }
627
628 codet ensures_statement(statement_type, {std::move(ensures)}, sl);
629 converter.goto_convert(ensures_statement, ensures_program, language_mode);
630 }
631
632 // When checking an ensures clause we link the contract write set to the
633 // ensures write set to know what was deallocated by the function so that
634 // the was_freed predicate can perform its checks
638 wrapper_sl));
639
640 // fix calls to user-defined user-defined memory predicates
641 memory_predicates.fix_calls(ensures_program);
642
643 // instrument for side effects
644 // make the program well-formed
645 ensures_program.add(goto_programt::make_end_function());
647 wrapper_id,
648 ensures_program,
651 // turn it back into a sequence of statements
652 ensures_program.instructions.back().turn_into_skip();
653
654 // add the ensures program to the postconditions section
655 postconditions.destructive_append(ensures_program);
656}
657
665
667{
668 // build call to the wrapped function
670
672 {
673 symbol_exprt return_value = return_value_opt.value();
674 // DECL
676 call.lhs() = return_value;
677
678 // SET_RETURN_VALUE
681
682 // DEAD
684 }
685
686 // forward wrapper arguments
687 const auto &wrapper_code_type = to_code_type(wrapper_symbol.type);
688
689 for(const auto &parameter : wrapper_code_type.parameter_identifiers())
690 {
691 PRECONDITION(!parameter.empty());
692 const symbolt &parameter_symbol = ns.lookup(parameter);
693 call.arguments().push_back(parameter_symbol.symbol_expr());
694 }
695
696 // pass write set to check against
697 call.arguments().push_back(addr_of_contract_write_set);
698
700}
701
703{
704 // generate local write set and add as parameter to the call
705 exprt::operandst write_set_arguments;
706 for(const auto &parameter :
708 {
709 PRECONDITION(!parameter.empty());
710 const symbolt &parameter_symbol = ns.lookup(parameter);
711 write_set_arguments.push_back(parameter_symbol.symbol_expr());
712 }
713
714 // check assigns clause inclusion
715 // IF __caller_write_set==NULL GOTO skip_target;
716 // DECL check: bool;
717 // CALL check = __CPROVER_contracts_write_set_check_assigns_clause_inclusion(
718 // __caller_write_set, &__local_write_set);
719 // ASSERT check;
720 // CALL check = __CPROVER_contracts_write_set_check_frees_clause_inclusion(
721 // __caller_write_set, &__local_write_set);
722 // ASSERT check;
723 // DEAD check;
724 // skip_target: skip;
725
726 auto goto_instruction =
729
730 {
731 // assigns clause inclusion
732 const auto check_var = dfcc_utilst::create_symbol(
734 bool_typet(),
736 "__check_assigns_clause_incl",
737 wrapper_sl);
738
740
744 wrapper_sl));
745
748 check_sl.set_property_class("assigns");
749 check_sl.set_comment(
750 "Check that the assigns clause of " + id2string(contract_symbol.name) +
751 " is included in the caller's assigns clause");
754 }
755
756 {
757 // frees clause inclusion
758 const auto check_var = dfcc_utilst::create_symbol(
760 bool_typet(),
762 "__check_frees_clause_incl",
763 wrapper_sl);
764
766
770 wrapper_sl));
771
774 check_sl.set_property_class("frees");
775 check_sl.set_comment(
776 "Check that the frees clause of " + id2string(contract_symbol.name) +
777 " is included in the caller's frees clause");
780 }
781
782 auto label_instruction =
784 goto_instruction->complete_goto(label_instruction);
785
786 code_function_callt havoc_call(
788 {addr_of_contract_write_set});
789
791
792 // assign nondet to the return value
793 if(return_value_opt.has_value())
794 {
795 symbol_exprt return_value = return_value_opt.value();
796
797 // DECL
799
800 // ASSIGN NONDET
802 return_value,
804 wrapper_sl));
805
806 // SET RETURN VALUE
809
810 // DEAD
812 }
813
814 // nondet free the freeable set, record effects in both the contract write
815 // set and the caller write set
819 wrapper_sl));
820}
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:55
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.
const typet & return_type() const
Definition std_types.h:645
std::vector< irep_idt > parameter_identifiers() const
Produces the list of parameter identifiers.
Definition std_types.h:696
const exprt::operandst & c_requires() const
Definition c_types.h:428
const exprt::operandst & c_ensures() const
Definition c_types.h:438
Data structure for representing an arbitrary statement in a program.
Generates GOTO functions modelling a contract assigns and frees clauses.
const symbolt & get_spec_frees_function_symbol() const
Returns the contract::frees function symbol.
const symbolt & get_spec_assigns_function_symbol() const
Returns the contract::c_assigns function symbol.
const std::size_t get_nof_assigns_targets() const
Returns the maximum number of targets in the assigns clause.
const symbolt & get_spec_assigns_havoc_function_symbol() const
Returns the contract::c_assigns::havoc function symbol.
const std::size_t get_nof_frees_targets() const
Returns the maximum number of targets in the frees clause.
This class instruments GOTO functions or instruction sequences for frame condition checking and loop ...
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.
Class interface to library types and functions defined in cprover_contracts.c.
const code_function_callt write_set_check_allocated_deallocated_is_empty_call(const exprt &check_var, const exprt &write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_allocated_deallocated_is_empty.
const code_function_callt obj_set_create_indexed_by_object_id_call(const exprt &obj_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_obj_set_create_indexed_by_object_id.
const code_function_callt link_allocated_call(const exprt &write_set_postconditions_ptr, const exprt &write_set_to_link_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_link_allocated.
const code_function_callt write_set_release_call(const exprt &write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_release.
const code_function_callt obj_set_release_call(const exprt &obj_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_obj_set_release.
const code_function_callt link_deallocated_call(const exprt &write_set_postconditions_ptr, const exprt &write_set_to_link_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_link_deallocated.
const code_function_callt write_set_check_assigns_clause_inclusion_call(const exprt &check_var, const exprt &reference_write_set_ptr, const exprt &candidate_write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_assigns_clause_inclusion.
const code_function_callt link_is_fresh_call(const exprt &write_set_ptr, const exprt &is_fresh_obj_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_link_is_fresh.
std::map< dfcc_typet, typet > dfcc_type
Maps enum values to the actual types (dynamically loaded)
const code_function_callt write_set_create_call(const exprt &write_set_ptr, const exprt &contract_assigns_size, const exprt &contract_frees_size, const exprt &assume_requires_ctx, const exprt &assert_requires_ctx, const exprt &assume_ensures_ctx, const exprt &assert_ensures_ctx, const exprt &allow_allocate, const exprt &allow_deallocate, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_create.
const code_function_callt write_set_check_frees_clause_inclusion_call(const exprt &check_var, const exprt &reference_write_set_ptr, const exprt &candidate_write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_check_frees_clause_inclusion.
const code_function_callt write_set_deallocate_freeable_call(const exprt &write_set_ptr, const exprt &target_write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_write_set_deallocate_freeable.
void fix_calls(goto_programt &program)
Fixes calls to user-defined memory predicates in the given program, by adding an address-of to argume...
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
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.
dfcc_instrumentt & instrument
void encode_ensures_write_set()
Encodes the empty write set used to check for side effects in ensures.
optionalt< symbol_exprt > return_value_opt
Symbol for the return value of the wrapped function.
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
source_locationt & add_source_location()
Definition expr.h:228
T & with_source_location(const exprt &other) &
Add the source location from other, if it has any.
Definition expr.h:102
The Boolean constant false.
Definition std_expr.h:3017
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
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())
const irep_idt & id() const
Definition irep.h:396
exprt application(const operandst &arguments) const
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
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:113
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
typet type
Type of symbol.
Definition symbol.h:31
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:3008
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
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Deprecated expression utility functions.
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
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:744
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
static const exprt make_null_check_expr(const exprt &ptr)
Returns the expression expr == NULL.
static 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:549
void add_quantified_variable(symbol_table_baset &symbol_table, exprt &expression, const irep_idt &mode)
This function recursively searches expression to find nested or non-nested quantified expressions.
Definition utils.cpp:367