CBMC
dfcc_wrapper_program.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dynamic frame condition checking for function contracts
4 
5 Author: Remi Delmas, delmasrd@amazon.com
6 
7 \*******************************************************************/
8 #include "dfcc_wrapper_program.h"
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>
15 #include <util/mathematical_expr.h>
16 #include <util/namespace.h>
18 #include <util/std_expr.h>
19 
21 
22 #include <ansi-c/c_expr.h>
24 #include <langapi/language_util.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
215  contract_lambda_parameters.push_back(return_value_opt.value());
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 
245 {
246  // add code to dest in the right order
257 }
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;
283  from_integer(0, size_type()),
284  from_integer(0, size_type()),
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 
316  source_locationt check_sl(wrapper_sl);
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
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 
354  from_integer(0, size_type()),
355  from_integer(0, size_type()),
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 
396  source_locationt check_sl(wrapper_sl);
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
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  {
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  {
457  code_function_callt call(
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  {
477  code_function_callt call(
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));
498  postamble.add(
500 }
501 
503 {
505 
509 
510  // CALL obj_set_create_indexed_by_object_id(is_fresh_set) in preamble
514  wrapper_sl));
515 
516  // link to requires write set
520  wrapper_sl));
521 
522  // link to ensures write set
526  wrapper_sl));
527 
528  // release call in postamble
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 =
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());
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
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());
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 
649 {
652  else
654 }
655 
657 {
658  // build call to the wrapped function
660 
661  if(return_value_opt)
662  {
663  symbol_exprt return_value = return_value_opt.value();
664  // DECL
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(
724  bool_typet(),
726  "__check_assigns_clause_incl",
727  wrapper_sl);
728 
730 
734  wrapper_sl));
735 
736  source_locationt check_sl(wrapper_sl);
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(
750  bool_typet(),
752  "__check_frees_clause_incl",
753  wrapper_sl);
754 
756 
760  wrapper_sl));
761 
762  source_locationt check_sl(wrapper_sl);
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(
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
789 
790  // ASSIGN NONDET
792  return_value,
793  side_effect_expr_nondett(return_value.type(), wrapper_sl),
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
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.
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.
Definition: pointer_expr.h:540
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:689
std::vector< irep_idt > parameter_identifiers() const
Produces the list of parameter identifiers.
Definition: std_types.h:740
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.
Definition: std_code_base.h:29
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.
Definition: dfcc_library.h:154
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)
Definition: dfcc_library.h:214
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
goto_programt link_allocated_caller
const code_with_contract_typet & contract_code_type
const symbolt & contract_symbol
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
const symbolt & wrapper_symbol
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.
const symbolt & wrapped_symbol
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
exprt & with_source_location(source_locationt location) &
Add the source location from location, if it is non-nil.
Definition: expr.h:101
typet & type()
Return the type of the expression.
Definition: expr.h:84
The Boolean constant false.
Definition: std_expr.h:3072
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.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
static instructiont make_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:874
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:971
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.
Definition: goto_program.h:722
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())
Definition: goto_program.h:891
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.
Definition: goto_program.h:739
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:964
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:933
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
const irep_idt & id() const
Definition: irep.h:388
exprt application(const operandst &arguments) const
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:148
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
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:3063
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
Definition: expr_util.cpp:313
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
double log(double x)
Definition: math.c:2776
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.
Definition: dfcc_utils.cpp:72
static const exprt make_null_check_expr(const exprt &ptr)
Returns the expression expr == NULL.
Definition: dfcc_utils.cpp:406
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...
Definition: dfcc_utils.cpp:81
#define size_type
Definition: unistd.c:347
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