cprover
Loading...
Searching...
No Matches
dfcc_lift_memory_predicates.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
10// TODO when scanning the goto functions to detect pointer predicates,
11// replace pointer equality p == q with __CPROVER_pointer_equals(p,q)
12// in all user-defined memory predicates.
13
15
16#include <util/cprover_prefix.h>
17#include <util/format_expr.h>
18#include <util/graph.h>
19#include <util/pointer_expr.h>
20#include <util/replace_symbol.h>
21#include <util/symbol.h>
22
24
25#include "dfcc_instrument.h"
26#include "dfcc_library.h"
27#include "dfcc_utils.h"
28
40
43 const irep_idt &function_id)
44{
45 return lifted_parameters.find(function_id) != lifted_parameters.end();
46}
47
49static bool is_core_memory_predicate(const irep_idt &function_id)
50{
51 return (function_id == CPROVER_PREFIX "pointer_equals") ||
52 (function_id == CPROVER_PREFIX "is_fresh") ||
53 (function_id == CPROVER_PREFIX "pointer_in_range_dfcc") ||
54 (function_id == CPROVER_PREFIX "obeys_contract");
55}
56
58 const goto_programt &goto_program,
59 const std::set<irep_idt> &predicates)
60{
61 for(const auto &instruction : goto_program.instructions)
62 {
63 if(
64 instruction.is_function_call() &&
65 instruction.call_function().id() == ID_symbol)
66 {
67 const auto &callee_id =
68 to_symbol_expr(instruction.call_function()).get_identifier();
69
70 if(
71 is_core_memory_predicate(callee_id) ||
72 predicates.find(callee_id) != predicates.end())
73 {
74 return true;
75 }
76 }
77 }
78 return false;
79}
80
82 std::set<irep_idt> &discovered_function_pointer_contracts)
83{
84 std::set<irep_idt> candidates;
85 for(const auto &pair : goto_model.symbol_table)
86 {
87 if(
88 pair.second.type.id() == ID_code &&
89 !instrument.do_not_instrument(pair.first))
90 {
91 const auto &iter =
92 goto_model.goto_functions.function_map.find(pair.first);
93 if(
94 iter != goto_model.goto_functions.function_map.end() &&
95 iter->second.body_available())
96 {
97 candidates.insert(pair.first);
98 }
99 }
100 }
101
102 std::set<irep_idt> predicates;
103
104 // iterate until no new predicate is found
105 bool new_predicates_found = true;
106 while(new_predicates_found)
107 {
108 new_predicates_found = false;
109 for(const auto &function_id : candidates)
110 {
111 if(
112 predicates.find(function_id) == predicates.end() &&
114 goto_model.goto_functions.function_map[function_id].body, predicates))
115 {
116 predicates.insert(function_id);
117 new_predicates_found = true;
118 }
119 }
120 }
121
122 if(predicates.empty())
123 return predicates;
124
125 // some predicates were found, build dependency graph
126 struct dep_graph_nodet : public graph_nodet<empty_edget>
127 {
128 const irep_idt &function_id;
129 explicit dep_graph_nodet(const irep_idt &function_id)
130 : function_id(function_id)
131 {
132 }
133 };
134
135 grapht<dep_graph_nodet> dep_graph;
136
137 // inverse mapping from names to dep_graph_nodet identifiers
138 std::map<irep_idt, std::size_t> id_to_node_map;
139 // create all nodes
140 for(auto &predicate : predicates)
141 {
142 id_to_node_map.insert({predicate, dep_graph.add_node(predicate)});
143 }
144
145 // create all edges
146 for(auto &caller : predicates)
147 {
148 const auto caller_id = id_to_node_map[caller];
149 for(const auto &instruction :
150 goto_model.goto_functions.function_map[caller].body.instructions)
151 {
152 if(
153 instruction.is_function_call() &&
154 instruction.call_function().id() == ID_symbol)
155 {
156 const auto &callee =
157 to_symbol_expr(instruction.call_function()).get_identifier();
158 if(predicates.find(callee) != predicates.end())
159 {
160 log.conditional_output(log.debug(), [&](messaget::mstreamt &mstream) {
161 mstream << "Memory predicate dependency " << caller << " -> "
162 << callee << messaget::eom;
163 });
164 const auto callee_id = id_to_node_map[callee];
165 if(callee != caller) // do not add edges for self-recursive functions
166 dep_graph.add_edge(callee_id, caller_id);
167 }
168 }
169 }
170 }
171
172 // lift in dependency order
173 auto sorted = dep_graph.topsort();
175 !sorted.empty(),
176 "could not determine instrumentation order for memory predicates, most "
177 "likely due to mutual recursion");
178 for(const auto &idx : sorted)
179 {
181 dep_graph[idx].function_id, discovered_function_pointer_contracts);
182 }
183
184 return predicates;
185}
186
187// returns an optional rank
188static std::optional<std::size_t> is_param_expr(
189 const exprt &expr,
190 const std::map<irep_idt, std::size_t> &parameter_rank)
191{
192 if(expr.id() == ID_typecast)
193 {
194 // ignore typecasts
195 return is_param_expr(to_typecast_expr(expr).op(), parameter_rank);
196 }
197 else if(expr.id() == ID_symbol)
198 {
199 const irep_idt &ident = to_symbol_expr(expr).get_identifier();
200 const auto found = parameter_rank.find(ident);
201 if(found != parameter_rank.end())
202 {
203 return {found->second};
204 }
205 else
206 {
207 return {};
208 }
209 }
210 else
211 {
212 // bail on anything else
213 return {};
214 }
215}
216
218 const irep_idt &function_id)
219{
220 const symbolt &function_symbol =
221 dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id);
222 // map of parameter name to its rank in the signature
223 std::map<irep_idt, std::size_t> parameter_rank;
224 const auto &parameters = to_code_type(function_symbol.type).parameters();
225 for(std::size_t rank = 0; rank < parameters.size(); rank++)
226 {
227 parameter_rank[parameters[rank].get_identifier()] = rank;
228 }
229 const goto_programt &body =
230 goto_model.goto_functions.function_map[function_id].body;
231 for(const auto &it : body.instructions)
232 {
233 // for all function calls, if a parameter of function_id is passed
234 // in a lifted position, add its rank to the set of lifted parameters
235 if(it.is_function_call() && it.call_function().id() == ID_symbol)
236 {
237 const irep_idt &callee_id =
238 to_symbol_expr(it.call_function()).get_identifier();
239 if(callee_id == CPROVER_PREFIX "pointer_equals")
240 {
241 auto opt_rank = is_param_expr(it.call_arguments()[0], parameter_rank);
242 if(opt_rank.has_value())
243 {
244 lifted_parameters[function_id].insert(opt_rank.value());
245 }
246 }
247 else if(callee_id == CPROVER_PREFIX "is_fresh")
248 {
249 auto opt_rank = is_param_expr(it.call_arguments()[0], parameter_rank);
250 if(opt_rank.has_value())
251 {
252 lifted_parameters[function_id].insert(opt_rank.value());
253 }
254 }
255 else if(callee_id == CPROVER_PREFIX "pointer_in_range_dfcc")
256 {
257 auto opt_rank = is_param_expr(it.call_arguments()[1], parameter_rank);
258 if(opt_rank.has_value())
259 {
260 lifted_parameters[function_id].insert(opt_rank.value());
261 }
262 }
263 else if(callee_id == CPROVER_PREFIX "obeys_contract")
264 {
265 auto opt_rank = is_param_expr(it.call_arguments()[0], parameter_rank);
266 if(opt_rank.has_value())
267 {
268 lifted_parameters[function_id].insert(opt_rank.value());
269 }
270 }
271 else if(is_lifted_function(callee_id))
272 {
273 // search wether a parameter of function_id is passed to a lifted
274 // parameter of callee_id
275 for(const std::size_t callee_rank : lifted_parameters[callee_id])
276 {
277 auto opt_rank =
278 is_param_expr(it.call_arguments()[callee_rank], parameter_rank);
279 if(opt_rank.has_value())
280 {
281 lifted_parameters[function_id].insert(opt_rank.value());
282 }
283 }
284 }
285 }
286 }
287}
288
290 const irep_idt &function_id,
291 const std::size_t parameter_rank,
292 replace_symbolt &replace_lifted_param)
293{
294 symbolt &function_symbol =
295 dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id);
296 code_typet &code_type = to_code_type(function_symbol.type);
297 auto &parameters = code_type.parameters();
298 auto &parameter_id = parameters[parameter_rank].get_identifier();
299 auto entry = goto_model.symbol_table.symbols.find(parameter_id);
300 log.conditional_output(log.debug(), [&](messaget::mstreamt &mstream) {
301 mstream << "adding pointer type to " << function_id << " " << parameter_id
302 << messaget::eom;
303 });
304 const symbolt &old_symbol = entry->second;
305 const auto &old_symbol_expr = old_symbol.symbol_expr();
306 // create new parameter symbol, same everything except type
307 symbolt new_symbol(
308 old_symbol.name, pointer_type(old_symbol.type), old_symbol.mode);
309 new_symbol.base_name = old_symbol.base_name;
310 new_symbol.location = old_symbol.location;
311 new_symbol.module = old_symbol.module;
312 new_symbol.is_lvalue = old_symbol.is_lvalue;
313 new_symbol.is_state_var = old_symbol.is_state_var;
314 new_symbol.is_thread_local = old_symbol.is_thread_local;
315 new_symbol.is_file_local = old_symbol.is_file_local;
316 new_symbol.is_auxiliary = old_symbol.is_auxiliary;
317 new_symbol.is_parameter = old_symbol.is_parameter;
318 goto_model.symbol_table.erase(entry);
319 std::pair<symbolt &, bool> res =
320 goto_model.symbol_table.insert(std::move(new_symbol));
321 CHECK_RETURN(res.second);
322 replace_lifted_param.insert(
323 old_symbol_expr, dereference_exprt(res.first.symbol_expr()));
324 code_typet::parametert parameter(res.first.type);
325 parameter.set_base_name(res.first.base_name);
326 parameter.set_identifier(res.first.name);
327 parameters[parameter_rank] = parameter;
328}
329
331 const irep_idt &function_id,
332 std::set<irep_idt> &discovered_function_pointer_contracts)
333{
334 replace_symbolt replace_lifted_params;
335 // add pointer types to all parameters that require it
336 for(const auto rank : lifted_parameters[function_id])
337 {
338 add_pointer_type(function_id, rank, replace_lifted_params);
339 }
340 auto &body = goto_model.goto_functions.function_map[function_id].body;
341 // update the function body
342 for(auto &instruction : body.instructions)
343 {
344 // rewrite all occurrences of lifted parameters
345 instruction.transform([&replace_lifted_params](exprt expr) {
346 const bool changed = !replace_lifted_params.replace(expr);
347 return changed ? std::optional<exprt>{expr} : std::nullopt;
348 });
349
350 // add address-of to all arguments expressions passed in lifted position to
351 // another memory predicate
352 if(
353 instruction.is_function_call() &&
354 instruction.call_function().id() == ID_symbol)
355 {
356 // add address-of to arguments that are passed in lifted position
357 auto &callee_id =
358 to_symbol_expr(instruction.call_function()).get_identifier();
359 if(is_lifted_function(callee_id))
360 {
361 for(const auto &rank : lifted_parameters[callee_id])
362 {
363 const auto arg = instruction.call_arguments()[rank];
364 log.conditional_output(log.debug(), [&](messaget::mstreamt &mstream) {
365 mstream << "Adding address_of to call " << callee_id
366 << ", argument " << format(arg) << messaget::eom;
367 });
368 instruction.call_arguments()[rank] = address_of_exprt(arg);
369 }
370 }
371 }
372 }
373}
374
376 const irep_idt &function_id,
377 std::set<irep_idt> &discovered_function_pointer_contracts)
378{
379 // when this function_id gets processed, any memory predicate it calls has
380 // already been processed (except itself if it is recursive);
381
382 log.status() << "Instrumenting memory predicate '" << function_id << "'"
383 << messaget::eom;
384
385 // first step: identify which parameters are passed directly to core
386 // predicates of lifted positions in user-defined memory predicates and mark
387 // them as lifted
388 collect_parameters_to_lift(function_id);
390 function_id, discovered_function_pointer_contracts);
391
392 log.conditional_output(log.debug(), [&](messaget::mstreamt &mstream) {
393 mstream << "Ranks of lifted parameters for " << function_id << ": ";
394 for(const auto rank : lifted_parameters[function_id])
395 mstream << rank << ", ";
396 mstream << messaget::eom;
397 });
398
399 // instrument the function for side effects: adds the write_set parameter,
400 // adds checks for side effects, maps core predicates to their implementation.
401 instrument.instrument_function(
402 function_id,
404 discovered_function_pointer_contracts);
405}
406
408{
409 fix_calls(program, program.instructions.begin(), program.instructions.end());
410}
411
413 goto_programt &program,
414 goto_programt::targett first_instruction,
415 const goto_programt::targett &last_instruction)
416{
417 for(auto target = first_instruction; target != last_instruction; target++)
418 {
419 if(target->is_function_call())
420 {
421 const auto &function = target->call_function();
422
423 if(function.id() == ID_symbol)
424 {
425 const irep_idt &fun_name = to_symbol_expr(function).get_identifier();
426
427 if(is_lifted_function(fun_name))
428 {
429 // add address-of on all lifted argumnents
430 for(const auto rank : lifted_parameters[fun_name])
431 {
432 target->call_arguments()[rank] =
433 address_of_exprt(target->call_arguments()[rank]);
434 }
435 }
436 }
437 }
438 }
439}
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
Operator to return the address of an object.
void set_base_name(const irep_idt &name)
Definition std_types.h:629
void set_identifier(const irep_idt &identifier)
Definition std_types.h:624
Base type of functions.
Definition std_types.h:583
const parameterst & parameters() const
Definition std_types.h:699
Operator to dereference a pointer.
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.
void fix_calls(goto_programt &program)
Fixes calls to user-defined memory predicates in the given program, by adding an address-of to argume...
void collect_parameters_to_lift(const irep_idt &function_id)
Computes the subset of function parameters of function_id that are passed directly to core predicates...
void lift_predicate(const irep_idt &function_id, std::set< irep_idt > &discovered_function_pointer_contracts)
void add_pointer_type(const irep_idt &function_id, const std::size_t parameter_rank, replace_symbolt &replace_lifted_param)
adds a pointer_type to the parameter of a function
dfcc_lift_memory_predicatest(goto_modelt &goto_model, dfcc_libraryt &library, dfcc_instrumentt &instrument, message_handlert &message_handler)
std::map< irep_idt, std::set< std::size_t > > lifted_parameters
void lift_parameters_and_update_body(const irep_idt &function_id, std::set< irep_idt > &discovered_function_pointer_contracts)
bool calls_memory_predicates(const goto_programt &goto_program, const std::set< irep_idt > &predicates)
Returns true iff goto_program calls core memory predicates.
bool is_lifted_function(const irep_idt &function_id)
True if a function at least had one of its parameters lifted.
std::set< irep_idt > lift_predicates(std::set< irep_idt > &discovered_function_pointer_contracts)
Collects and lifts all user-defined memory predicates.
Base class for all expressions.
Definition expr.h:56
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::iterator targett
This class represents a node in a directed graph.
Definition graph.h:35
A generic directed graph with a parametric node type.
Definition graph.h:167
node_indext add_node(arguments &&... values)
Definition graph.h:180
void add_edge(node_indext a, node_indext b)
Definition graph.h:232
std::list< node_indext > topsort() const
Find a topological order of the nodes if graph is DAG, return empty list for non-DAG or empty graph.
Definition graph.h:879
const irep_idt & id() const
Definition irep.h:388
static eomt eom
Definition message.h:289
Replace a symbol expression by a given expression.
virtual bool replace(exprt &dest) const
void insert(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothi...
const irep_idt & get_identifier() const
Definition std_expr.h:160
Symbol table entry.
Definition symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition symbol.h:46
bool is_auxiliary
Definition symbol.h:77
bool is_file_local
Definition symbol.h:73
irep_idt module
Name of module the symbol belongs to.
Definition symbol.h:43
bool is_parameter
Definition symbol.h:76
bool is_thread_local
Definition symbol.h:71
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
bool is_state_var
Definition symbol.h:66
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
bool is_lvalue
Definition symbol.h:72
irep_idt mode
Language mode.
Definition symbol.h:49
#define CPROVER_PREFIX
Add instrumentation to a goto program to perform frame condition checks.
Dynamic frame condition checking library loading.
static bool is_core_memory_predicate(const irep_idt &function_id)
True iff function_id is a core memory predicate.
static std::optional< std::size_t > is_param_expr(const exprt &expr, const std::map< irep_idt, std::size_t > &parameter_rank)
Collects all user-defined predicates that call functions is_fresh, pointer_in_range,...
Dynamic frame condition checking utility functions.
Symbol Table + CFG.
A Template Class for Graphs.
API to expression classes for Pointers.
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition invariant.h:464
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
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.
Loop contract configurations.
Symbol table entry.
dstringt irep_idt