cprover
Loading...
Searching...
No Matches
dfcc_contract_handler.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\*******************************************************************/
9
11
12#include <util/arith_tools.h>
13#include <util/c_types.h>
14#include <util/expr_util.h>
15#include <util/format_type.h>
16#include <util/fresh_symbol.h>
17#include <util/invariant.h>
19#include <util/namespace.h>
21#include <util/std_expr.h>
22
25
26#include <ansi-c/c_expr.h>
29
30#include "dfcc_instrument.h"
31#include "dfcc_library.h"
32#include "dfcc_spec_functions.h"
34
35std::map<irep_idt, dfcc_contract_functionst>
37
57
60{
61 auto iter = dfcc_contract_handlert::contract_cache.find(contract_id);
62
63 // return existing value
65 return iter->second;
66
67 // insert new value
69 .insert(
70 {contract_id,
72 get_pure_contract_symbol(contract_id),
75 library,
78 instrument)})
79 .first->second;
80}
81
82const std::size_t
87
89 const dfcc_contract_modet contract_mode,
90 const irep_idt &wrapper_id,
91 const irep_idt &wrapped_id,
92 const irep_idt &contract_id,
93 const symbolt &wrapper_write_set_symbol,
94 goto_programt &dest,
95 std::set<irep_idt> &function_pointer_contracts)
96{
98 contract_mode,
99 dfcc_utilst::get_function_symbol(goto_model.symbol_table, wrapper_id),
100 dfcc_utilst::get_function_symbol(goto_model.symbol_table, wrapped_id),
101 get_contract_functions(contract_id),
102 wrapper_write_set_symbol,
105 library,
108 .add_to_dest(dest, function_pointer_contracts);
109}
110
112 const irep_idt &contract_id,
113 const std::optional<irep_idt> function_id_opt)
114{
115 auto pure_contract_id = "contract::" + id2string(contract_id);
116 const symbolt *pure_contract_symbol = nullptr;
117 if(!ns.lookup(pure_contract_id, pure_contract_symbol))
118 {
119 if(function_id_opt.has_value())
120 {
121 auto function_id = function_id_opt.value();
122 const auto &function_symbol =
123 dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id);
125 function_id,
126 to_code_type(function_symbol.type),
127 pure_contract_id,
128 to_code_type(pure_contract_symbol->type));
129 }
130 return *pure_contract_symbol;
131 }
132 else
133 {
134 // The contract symbol might not have been created if the function had
135 // no contract or a contract with all empty clauses (which is equivalent).
136 // in that case we create a fresh symbol again with empty clauses.
138 function_id_opt.has_value(),
139 "Contract '" + pure_contract_id +
140 "' not found, the identifier of an existing function must be provided "
141 "to derive a default contract");
142
143 auto function_id = function_id_opt.value();
144 const auto &function_symbol =
145 dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id);
146
147 log.warning() << "Contract '" << contract_id
148 << "' not found, deriving empty pure contract '"
149 << pure_contract_id << "' from function '" << function_id
150 << "'" << messaget::eom;
151
152 symbolt new_symbol{
153 pure_contract_id, function_symbol.type, function_symbol.mode};
154 new_symbol.base_name = pure_contract_id;
155 new_symbol.pretty_name = pure_contract_id;
156 new_symbol.is_property = true;
157 new_symbol.module = function_symbol.module;
158 new_symbol.location = function_symbol.location;
159 auto entry = goto_model.symbol_table.insert(std::move(new_symbol));
160 INVARIANT(
161 entry.second,
162 "contract '" + id2string(function_symbol.display_name()) +
163 "' already set at " + id2string(entry.first.location.as_string()));
164 // this lookup will work and set the pointer
165 // no need to check for signature compatibility
166 ns.lookup(pure_contract_id, pure_contract_symbol);
167 return *pure_contract_symbol;
168 }
169}
170
172 const irep_idt &contract_id,
173 const code_typet &contract_type,
174 const irep_idt &pure_contract_id,
175 const code_typet &pure_contract_type)
176{
177 // can we turn a call to `contract` into a call to `pure_contract` ?
178 bool compatible =
179 function_is_type_compatible(true, contract_type, pure_contract_type, ns);
180
181 if(!compatible)
182 {
183 std::ostringstream err_msg;
184 err_msg << "dfcc_contract_handlert: function '" << contract_id
185 << "' and the corresponding pure contract symbol '"
186 << pure_contract_id << "' have incompatible type signatures:\n";
187
188 err_msg << "- contract return type "
189 << from_type(ns, contract_id, contract_type.return_type()) << "\n";
190
191 for(const auto &param : contract_type.parameters())
192 {
193 err_msg << "- contract param type "
194 << from_type(ns, contract_id, param.type()) << "\n";
195 }
196
197 err_msg << "- pure contract return type "
198 << from_type(ns, pure_contract_id, pure_contract_type.return_type())
199 << "\n";
200
201 for(const auto &param : pure_contract_type.parameters())
202 {
203 err_msg << "- pure contract param type "
204 << from_type(ns, pure_contract_id, param.type()) << "\n";
205 }
206
207 err_msg << "aborting."
208 << "\n";
210 err_msg.str(), contract_type.source_location());
211 }
212}
API to expression classes that are internal to the C frontend.
Base type of functions.
Definition std_types.h:583
const parameterst & parameters() const
Definition std_types.h:699
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 ...
Generates GOTO functions modelling a contract assigns and frees clauses.
const std::size_t get_nof_assigns_targets() const
Returns the maximum number of targets in the assigns clause.
void check_signature_compat(const irep_idt &contract_id, const code_typet &contract_type, const irep_idt &pure_contract_id, const code_typet &pure_contract_type)
Throws an error if the type signatures are not compatible.
dfcc_spec_functionst & spec_functions
const symbolt & get_pure_contract_symbol(const irep_idt &contract_id, const std::optional< irep_idt > function_id_opt={})
Searches for a symbol named "contract::contract_id" in the symbol table.
static std::map< irep_idt, dfcc_contract_functionst > contract_cache
dfcc_lift_memory_predicatest & memory_predicates
message_handlert & message_handler
dfcc_contract_clauses_codegent & contract_clauses_codegen
const std::size_t get_assigns_clause_size(const irep_idt &contract_id)
Returns the size assigns clause of the given contract in number of targets.
void add_contract_instructions(const dfcc_contract_modet contract_mode, const irep_idt &wrapper_id, const irep_idt &wrapped_id, const irep_idt &contract_id, const symbolt &wrapper_write_set_symbol, goto_programt &dest, std::set< irep_idt > &function_pointer_contracts)
Adds instructions in dest modeling contract checking, assuming that ret_t wrapper_id(params) is the f...
dfcc_contract_handlert(goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_instrumentt &instrument, dfcc_lift_memory_predicatest &memory_predicates, dfcc_spec_functionst &spec_functions, dfcc_contract_clauses_codegent &contract_clauses_codegen)
const dfcc_contract_functionst & get_contract_functions(const irep_idt &contract_id)
Returns the dfcc_contract_functionst object for the given contract from the cache,...
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:
Generates the body of a wrapper function from a contract specified using requires,...
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.
A generic container class for the GOTO intermediate representation of one function.
Thrown when we can't handle something in an input source file.
static eomt eom
Definition message.h:289
Symbol table entry.
Definition symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition symbol.h:46
irep_idt module
Name of module the symbol belongs to.
Definition symbol.h:43
bool is_property
Definition symbol.h:67
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
typet type
Type of symbol.
Definition symbol.h:31
irep_idt pretty_name
Language-specific display name.
Definition symbol.h:52
const source_locationt & source_location() const
Definition type.h:72
Specialisation of dfcc_contract_handlert for contracts.
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.
Translate functions that specify assignable and freeable targets declaratively into active functions ...
Generates the body of a wrapper function from a contract for contract checking or contract replacemen...
Deprecated expression utility functions.
Fresh auxiliary symbol creation.
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
API to expression classes for 'mathematical' expressions.
Pointer Logic.
bool function_is_type_compatible(bool return_value_used, const code_typet &call_type, const code_typet &function_type, const namespacet &ns)
Returns true iff call_type can be converted to produce a function call of the same type as function_t...
Remove Indirect Function Calls.
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition invariant.h:464
#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 symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
dstringt irep_idt