CBMC
dfcc_contract_functions.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 Date: August 2022
7 
8 \*******************************************************************/
10 
11 #include <util/expr_util.h>
12 #include <util/fresh_symbol.h>
13 #include <util/invariant.h>
14 #include <util/mathematical_expr.h>
15 #include <util/namespace.h>
17 #include <util/std_expr.h>
18 
20 
21 #include <ansi-c/c_expr.h>
23 #include <langapi/language_util.h>
24 
26 #include "dfcc_instrument.h"
27 #include "dfcc_library.h"
28 #include "dfcc_spec_functions.h"
29 
31  const symbolt &pure_contract_symbol,
32  goto_modelt &goto_model,
33  message_handlert &message_handler,
34  dfcc_libraryt &library,
35  dfcc_spec_functionst &spec_functions,
36  dfcc_contract_clauses_codegent &contract_clauses_codegen,
37  dfcc_instrumentt &instrument)
38  : pure_contract_symbol(pure_contract_symbol),
39  code_with_contract(to_code_with_contract_type(pure_contract_symbol.type)),
40  spec_assigns_function_id(
41  id2string(pure_contract_symbol.name) + "::assigns"),
42  spec_assigns_havoc_function_id(
43  id2string(pure_contract_symbol.name) + "::assigns::havoc"),
44  spec_frees_function_id(id2string(pure_contract_symbol.name) + "::frees"),
45  language_mode(pure_contract_symbol.mode),
46  goto_model(goto_model),
47  message_handler(message_handler),
48  log(message_handler),
49  library(library),
50  spec_functions(spec_functions),
51  contract_clauses_codegen(contract_clauses_codegen),
52  instrument(instrument),
53  ns(goto_model.symbol_table)
54 {
56 
61 
64 
66 
69 
72 
75 }
76 
79  const irep_idt &spec_function_id)
80 {
81  std::set<irep_idt> function_pointer_contracts;
83  spec_function_id, loop_contract_configt{false}, function_pointer_contracts);
84 
85  INVARIANT(
86  function_pointer_contracts.empty(),
87  id2string(spec_function_id) + " shall not contain calls to " CPROVER_PREFIX
88  "obeys_contract");
89 }
90 
91 const symbolt &
93 {
95 }
96 
97 const symbolt &
99 {
101 }
102 
104 {
106 }
107 
109 {
110  return nof_assigns_targets;
111 }
112 
114 {
115  return nof_frees_targets;
116 }
117 
119 {
120  const auto &spec_function_symbol = dfcc_utilst::clone_and_rename_function(
121  goto_model,
124  empty_typet());
125 
126  const auto &spec_function_id = spec_function_symbol.name;
127 
128  auto &spec_code_type = to_code_type(spec_function_symbol.type);
129 
130  exprt::operandst lambda_parameters;
131 
132  if(code_with_contract.return_type().id() != ID_empty)
133  {
134  // use a dummy symbol for __CPROVER_return_value
135  // which does occur in the assigns clause anyway
136  lambda_parameters.push_back(
137  symbol_exprt("dummy_return_value", code_with_contract.return_type()));
138  }
139 
140  for(const auto &param_id : spec_code_type.parameter_identifiers())
141  {
142  lambda_parameters.push_back(ns.lookup(param_id).symbol_expr());
143  }
144 
145  // fetch the goto_function to add instructions to
146  goto_functiont &goto_function =
147  goto_model.goto_functions.function_map.at(spec_function_id);
148 
149  exprt::operandst targets;
150 
151  for(const exprt &target : code_with_contract.c_assigns())
152  {
153  auto new_target = to_lambda_expr(target).application(lambda_parameters);
154  new_target.add_source_location() = target.source_location();
155  targets.push_back(new_target);
156  }
157 
158  goto_programt &body = goto_function.body;
160  spec_function_symbol.mode, targets, body);
161  body.add(goto_programt::make_end_function(spec_function_symbol.location));
162 
164 }
165 
167 {
168  // fetch pure contract symbol
169  const auto &code_with_contract =
171 
172  auto &spec_function_symbol = dfcc_utilst::clone_and_rename_function(
173  goto_model,
176  empty_typet());
177 
178  const auto &spec_function_id = spec_function_symbol.name;
179 
180  auto &spec_code_type = to_code_type(spec_function_symbol.type);
181 
182  exprt::operandst lambda_parameters;
183 
184  if(code_with_contract.return_type().id() != ID_empty)
185  {
186  // use a dummy symbol for __CPROVER_return_value
187  // which does occur in the assigns clause anyway
188  symbolt dummy;
189  dummy.name = "dummy_return_value";
191  lambda_parameters.push_back(dummy.symbol_expr());
192  }
193 
194  for(const auto &param_id : spec_code_type.parameter_identifiers())
195  {
196  lambda_parameters.push_back(ns.lookup(param_id).symbol_expr());
197  }
198 
199  // fetch the goto_function to add instructions to
200  goto_functiont &goto_function =
201  goto_model.goto_functions.function_map.at(spec_function_id);
202 
203  exprt::operandst targets;
204 
205  for(const exprt &target : code_with_contract.c_frees())
206  {
207  auto new_target = to_lambda_expr(target).application(lambda_parameters);
208  new_target.add_source_location() = target.source_location();
209  targets.push_back(new_target);
210  }
211 
212  goto_programt &body = goto_function.body;
214  spec_function_symbol.mode, targets, body);
215  body.add(goto_programt::make_end_function(spec_function_symbol.location));
216 
218 }
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
const typet & return_type() const
Definition: std_types.h:689
const exprt::operandst & c_assigns() const
Definition: c_types.h:408
const exprt::operandst & c_frees() const
Definition: c_types.h:418
Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that ...
void gen_spec_assigns_instructions(const irep_idt &language_mode, const exprt::operandst &assigns_clause, goto_programt &dest)
Generates instructions encoding the assigns_clause targets and adds them to dest.
void gen_spec_frees_instructions(const irep_idt &language_mode, const exprt::operandst &frees_clause, goto_programt &dest)
Generates instructions encoding the frees_clause targets and adds them to dest.
void gen_spec_frees_function()
Translates the contract's frees clause to a GOTO function that uses the freeable built-in to express ...
const irep_idt spec_assigns_havoc_function_id
Identifier of the contract::c_assigns::havoc function.
const code_with_contract_typet & code_with_contract
The code_with_contract_type carrying the contract clauses.
const symbolt & get_spec_frees_function_symbol() const
Returns the contract::frees function symbol.
dfcc_contract_clauses_codegent & contract_clauses_codegen
const irep_idt spec_assigns_function_id
Identifier of the contract::c_assigns function.
void instrument_without_loop_contracts_check_no_pointer_contracts(const irep_idt &spec_function_id)
Instruments the given function without loop contracts and checks that no function pointer contracts w...
dfcc_contract_functionst(const symbolt &pure_contract_symbol, goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_spec_functionst &spec_functions, dfcc_contract_clauses_codegent &contract_clauses_codegen, dfcc_instrumentt &instrument)
const symbolt & get_spec_assigns_function_symbol() const
Returns the contract::c_assigns function symbol.
const symbolt & pure_contract_symbol
The function symbol carrying the contract.
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.
void gen_spec_assigns_function()
Translates the contract's assigns clause to a GOTO function that uses the assignable,...
const irep_idt spec_frees_function_id
Identifier of the contract::frees function.
dfcc_spec_functionst & spec_functions
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_function(const irep_idt &function_id, const loop_contract_configt &loop_contract_config, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO function by adding an extra write set parameter and instrumenting its body instruc...
Class interface to library types and functions defined in cprover_contracts.c.
Definition: dfcc_library.h:154
This class rewrites GOTO functions that use the built-ins:
void to_spec_assigns_function(const irep_idt &function_id, std::size_t &nof_targets)
Transforms (in place) a function.
void generate_havoc_function(const irep_idt &function_id, const irep_idt &havoc_function_id, std::size_t &nof_targets)
From a function:
void to_spec_frees_function(const irep_idt &function_id, std::size_t &nof_targets)
Transforms (in place) a function.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
The empty type.
Definition: std_types.h:51
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
source_locationt & add_source_location()
Definition: expr.h:236
function_mapt function_map
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
goto_programt body
Definition: goto_function.h:26
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:739
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
Expression to hold a symbol (variable)
Definition: std_expr.h:131
Symbol table entry.
Definition: symbol.h:28
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
#define CPROVER_PREFIX
Translates assigns and frees clauses of a function contract or loop contract into goto programs that ...
Translates assigns and frees clauses of a function contract into goto functions that allow to build a...
Add instrumentation to a goto program to perform frame condition checks.
Dynamic frame condition checking library loading.
Translate functions that specify assignable and freeable targets declaratively into active functions ...
Deprecated expression utility functions.
Fresh auxiliary symbol creation.
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
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.
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 const symbolt & clone_and_rename_function(goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &new_function_id, std::optional< typet > new_return_type)
Creates a new function symbol and goto_function entry in the goto_functions_map by cloning the given ...
Definition: dfcc_utils.cpp:300
Loop contract configurations.