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
41 id2string(pure_contract_symbol.name) + "::assigns"),
43 id2string(pure_contract_symbol.name) + "::assigns::havoc"),
53 ns(goto_model.symbol_table)
54{
55 gen_spec_assigns_function();
56
57 spec_functions.generate_havoc_function(
61
62 spec_functions.to_spec_assigns_function(
64
66
67 spec_functions.to_spec_frees_function(
69
72
75}
76
79 const irep_idt &spec_function_id)
80{
81 std::set<irep_idt> function_pointer_contracts;
82 instrument.instrument_function(
83 spec_function_id, loop_contract_configt{false}, function_pointer_contracts);
84
86 function_pointer_contracts.empty(),
87 id2string(spec_function_id) + " shall not contain calls to " CPROVER_PREFIX
88 "obeys_contract");
89}
90
91const symbolt &
96
97const symbolt &
102
107
109{
110 return nof_assigns_targets;
111}
112
114{
115 return nof_frees_targets;
116}
117
118void dfcc_contract_functionst::gen_spec_assigns_function()
119{
120 const auto &spec_function_symbol = dfcc_utilst::clone_and_rename_function(
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;
159 contract_clauses_codegen.gen_spec_assigns_instructions(
160 spec_function_symbol.mode, targets, body);
161 body.add(goto_programt::make_end_function(spec_function_symbol.location));
162
163 goto_model.goto_functions.update();
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(
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";
190 dummy.type = code_with_contract.return_type();
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;
213 contract_clauses_codegen.gen_spec_frees_instructions(
214 spec_function_symbol.mode, targets, body);
215 body.add(goto_programt::make_end_function(spec_function_symbol.location));
216
217 goto_model.goto_functions.update();
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
Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that ...
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 irep_idt & language_mode
Language mode of the contract 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 ...
Class interface to library types and functions defined in cprover_contracts.c.
This class rewrites GOTO functions that use the built-ins:
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
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_programt body
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:388
exprt application(const operandst &arguments) const
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
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: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 ...
Loop contract configurations.
dstringt irep_idt