cprover
Loading...
Searching...
No Matches
dfcc_contract_functions.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
6Date: August 2022
7
8\*******************************************************************/
10
11#include <util/expr_util.h>
12#include <util/fresh_symbol.h>
13#include <util/invariant.h>
15#include <util/namespace.h>
17#include <util/std_expr.h>
18
20
21#include <ansi-c/c_expr.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{
55 gen_spec_assigns_function();
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,
85 function_pointer_contracts);
86
88 function_pointer_contracts.empty(),
89 id2string(spec_function_id) + " shall not contain calls to " CPROVER_PREFIX
90 "obeys_contract");
91}
92
93const symbolt &
98
99const symbolt &
104
109
111{
112 return nof_assigns_targets;
113}
114
116{
117 return nof_frees_targets;
118}
119
120void dfcc_contract_functionst::gen_spec_assigns_function()
121{
122 const auto &spec_function_symbol = dfcc_utilst::clone_and_rename_function(
126 empty_typet());
127
128 const auto &spec_function_id = spec_function_symbol.name;
129
130 auto &spec_code_type = to_code_type(spec_function_symbol.type);
131
132 exprt::operandst lambda_parameters;
133
134 if(code_with_contract.return_type().id() != ID_empty)
135 {
136 // use a dummy symbol for __CPROVER_return_value
137 // which does occur in the assigns clause anyway
138 lambda_parameters.push_back(
139 symbol_exprt("dummy_return_value", code_with_contract.return_type()));
140 }
141
142 for(const auto &param_id : spec_code_type.parameter_identifiers())
143 {
144 lambda_parameters.push_back(ns.lookup(param_id).symbol_expr());
145 }
146
147 // fetch the goto_function to add instructions to
148 goto_functiont &goto_function =
149 goto_model.goto_functions.function_map.at(spec_function_id);
150
151 exprt::operandst targets;
152
153 for(const exprt &target : code_with_contract.c_assigns())
154 {
155 auto new_target = to_lambda_expr(target).application(lambda_parameters);
156 new_target.add_source_location() = target.source_location();
157 targets.push_back(new_target);
158 }
159
160 goto_programt &body = goto_function.body;
162 spec_function_symbol.mode, targets, body);
163 body.add(goto_programt::make_end_function(spec_function_symbol.location));
164
166}
167
169{
170 // fetch pure contract symbol
171 const auto &code_with_contract =
173
174 auto &spec_function_symbol = dfcc_utilst::clone_and_rename_function(
178 empty_typet());
179
180 const auto &spec_function_id = spec_function_symbol.name;
181
182 auto &spec_code_type = to_code_type(spec_function_symbol.type);
183
184 exprt::operandst lambda_parameters;
185
186 if(code_with_contract.return_type().id() != ID_empty)
187 {
188 // use a dummy symbol for __CPROVER_return_value
189 // which does occur in the assigns clause anyway
190 symbolt dummy;
191 dummy.name = "dummy_return_value";
193 lambda_parameters.push_back(dummy.symbol_expr());
194 }
195
196 for(const auto &param_id : spec_code_type.parameter_identifiers())
197 {
198 lambda_parameters.push_back(ns.lookup(param_id).symbol_expr());
199 }
200
201 // fetch the goto_function to add instructions to
202 goto_functiont &goto_function =
203 goto_model.goto_functions.function_map.at(spec_function_id);
204
205 exprt::operandst targets;
206
207 for(const exprt &target : code_with_contract.c_frees())
208 {
209 auto new_target = to_lambda_expr(target).application(lambda_parameters);
210 new_target.add_source_location() = target.source_location();
211 targets.push_back(new_target);
212 }
213
214 goto_programt &body = goto_function.body;
216 spec_function_symbol.mode, targets, body);
217 body.add(goto_programt::make_end_function(spec_function_symbol.location));
218
220}
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:645
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 assigns clause to a GOTO function that uses the assignable,...
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.
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 dfcc_loop_contract_modet loop_contract_mode, 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.
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:39
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:228
function_mapt function_map
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_programt body
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
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().
Expression to hold a symbol (variable)
Definition std_expr.h:113
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.
@ NONE
Do not apply loop contracts.
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:47
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 INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
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 const symbolt & clone_and_rename_function(goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &new_function_id, optionalt< typet > new_return_type)
Creates a new function symbol and goto_function entry in the goto_functions_map by cloning the given ...