cprover
Loading...
Searching...
No Matches
instrument_spec_assigns.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Instrument assigns clauses in code contracts.
4
5Author: Remi Delmas
6
7Date: January 2022
8
9\*******************************************************************/
10
13
15
16#include <util/arith_tools.h>
17#include <util/c_types.h>
18#include <util/expr_util.h>
19#include <util/format_expr.h>
22#include <util/simplify_expr.h>
23
24#include <analyses/call_graph.h>
25
27
28#include "utils.h"
29
31
33 const exprt &expr,
34 goto_programt &dest)
35{
36 if(auto target = expr_try_dynamic_cast<conditional_target_group_exprt>(expr))
37 track_spec_target_group(*target, dest);
38 else
39 track_plain_spec_target(expr, dest);
40}
41
43 const symbol_exprt &symbol_expr,
44 goto_programt &dest)
45{
47}
48
50 const symbol_exprt &symbol_expr) const
51{
52 return from_stack_alloc.find(symbol_expr) != from_stack_alloc.end();
53}
54
56 const symbol_exprt &symbol_expr,
57 goto_programt &dest)
58{
59 // ensure it is tracked
61 stack_allocated_is_tracked(symbol_expr),
62 "symbol is not tracked :" + from_expr(ns, "", symbol_expr));
63
64 const auto &car = from_stack_alloc.find(symbol_expr)->second;
65
66 source_locationt source_location(symbol_expr.source_location());
67 add_pragma_disable_pointer_checks(source_location);
68 add_pragma_disable_assigns_check(source_location);
69
71 car.valid_var(), false_exprt{}, source_location));
72}
73
75 const exprt &expr,
76 goto_programt &dest)
77{
79}
80
82 const exprt &lhs,
83 optionalt<cfg_infot> &cfg_info_opt,
84 goto_programt &dest)
85{
86 // create temporary car but do not track
87 const auto car = create_car_expr(true_exprt{}, lhs);
88 create_snapshot(car, dest);
89 inclusion_check_assertion(car, false, true, cfg_info_opt, dest);
90}
91
93{
94 auto call_graph =
97
98 for(const auto &sym_pair : st)
99 {
100 const auto &sym = sym_pair.second;
101 if(sym.is_static_lifetime)
102 {
103 auto fname = sym.location.get_function();
104 if(
105 !fname.empty() &&
106 (fname == function_id || call_graph.get_node_index(fname).has_value()))
107 {
108 // We found a symbol with
109 // - a static lifetime
110 // - non empty location function
111 // - this function appears in the call graph of the function
112
113 // insert in tracking set and generate snapshot instructions
114 // for this target.
115 create_snapshot(create_car_from_stack_alloc(sym.symbol_expr()), dest);
116 }
117 }
118 }
119}
120
123 const exprt &expr,
124 optionalt<cfg_infot> &cfg_info_opt,
125 goto_programt &dest)
126{
127 // create temporary car but do not track
128 const auto car = create_car_expr(true_exprt{}, expr);
129
130 // generate snapshot instructions for this target.
131 create_snapshot(car, dest);
132
133 // check inclusion, allowing null and not allowing stack allocated locals
134 inclusion_check_assertion(car, true, false, cfg_info_opt, dest);
135
136 // invalidate aliases of the freed object
138}
139
141
144 goto_programt &dest)
145{
146 // clean up side effects from the guard expression if needed
148 exprt condition(group.condition());
149 if(has_subexpr(condition, ID_side_effect))
150 cleaner.clean(condition, dest, st.lookup_ref(function_id).mode);
151
152 // create conditional address ranges by distributing the condition
153 for(const auto &target : group.targets())
154 {
155 // insert in tracking set
156 const auto &car = create_car_from_spec_assigns(condition, target);
157
158 // generate target validity check for this target.
159 target_validity_assertion(car, true, dest);
160
161 // generate snapshot instructions for this target.
162 create_snapshot(car, dest);
163 }
164}
165
167 const exprt &expr,
168 goto_programt &dest)
169{
170 // insert in tracking set
171 const auto &car = create_car_from_spec_assigns(true_exprt{}, expr);
172
173 // generate target validity check for this target.
174 target_validity_assertion(car, true, dest);
175
176 // generate snapshot instructions for this target.
177 create_snapshot(car, dest);
178}
179
181 const std::string &suffix,
182 const typet &type,
183 const source_locationt &location) const
184{
185 return new_tmp_symbol(
186 type, location, st.lookup_ref(function_id).mode, st, suffix);
187}
188
190 const exprt &condition,
191 const exprt &target) const
192{
193 const source_locationt &source_location = target.source_location();
194 const auto &valid_var =
195 create_fresh_symbol("__car_valid", bool_typet(), source_location)
196 .symbol_expr();
197
198 const auto &lower_bound_var =
199 create_fresh_symbol("__car_lb", pointer_type(char_type()), source_location)
200 .symbol_expr();
201
202 const auto &upper_bound_var =
203 create_fresh_symbol("__car_ub", pointer_type(char_type()), source_location)
204 .symbol_expr();
205
206 if(target.id() == ID_pointer_object)
207 {
208 const auto &arg = to_unary_expr(target).op();
209 return {
210 condition,
211 target,
214 pointer_offset(arg)),
216 valid_var,
217 lower_bound_var,
218 upper_bound_var};
219 }
220 else if(is_assignable(target))
221 {
222 const auto &size = size_of_expr(target.type(), ns);
223
224 INVARIANT(
225 size.has_value(),
226 "no definite size for lvalue target:\n" + target.pretty());
227
228 return {condition,
229 target,
233 valid_var,
234 lower_bound_var,
235 upper_bound_var};
236 };
237
239}
240
242 const car_exprt &car,
243 goto_programt &dest) const
244{
245 source_locationt source_location(car.source_location());
246 add_pragma_disable_pointer_checks(source_location);
247 add_pragma_disable_assigns_check(source_location);
248
249 dest.add(goto_programt::make_decl(car.valid_var(), source_location));
250
252 car.valid_var(),
254 and_exprt{car.condition(),
256 ns),
257 source_location));
258
259 dest.add(goto_programt::make_decl(car.lower_bound_var(), source_location));
260
262 car.lower_bound_var(), car.target_start_address(), source_location));
263
264 dest.add(goto_programt::make_decl(car.upper_bound_var(), source_location));
265
267 car.upper_bound_var(),
270 source_location));
271}
272
274 const car_exprt &car,
275 bool allow_null_target) const
276{
277 // If requested, we check that when guard condition is true,
278 // the target's `start_address` pointer satisfies w_ok with the expected size
279 // (or is NULL if we allow it explicitly).
280 // This assertion will be falsified whenever `start_address` is invalid or
281 // not of the right size (or is NULL if we dot not allow it expliclitly).
282 auto result =
285
286 if(allow_null_target)
288
289 return simplify_expr(result, ns);
290}
291
293 const car_exprt &car,
294 bool allow_null_target,
295 goto_programt &dest) const
296{
297 // since assigns clauses are declared outside of their function body
298 // their source location might not have a function attribute
299 source_locationt source_location(car.source_location());
300 if(source_location.get_function().empty())
301 source_location.set_function(function_id);
302
303 source_location.set_property_class("assigns");
304
305 add_pragma_disable_pointer_checks(source_location);
306 add_pragma_disable_assigns_check(source_location);
307
308 std::string comment = "Check that ";
309 comment += from_expr(ns, "", car.target());
310 comment += " is valid";
311 if(!car.condition().is_true())
312 {
313 comment += " when ";
314 comment += from_expr(ns, "", car.condition());
315 }
316
317 source_location.set_comment(comment);
318
320 target_validity_expr(car, allow_null_target), source_location));
321}
322
324 const car_exprt &car,
325 bool allow_null_lhs,
326 bool include_stack_allocated,
327 optionalt<cfg_infot> &cfg_info_opt,
328 goto_programt &dest) const
329{
330 source_locationt source_location(car.source_location());
331
332 // since assigns clauses are declared outside of their function body
333 // their source location might not have a function attribute
334 if(source_location.get_function().empty())
335 source_location.set_function(function_id);
336
337 add_pragma_disable_pointer_checks(source_location);
338 add_pragma_disable_assigns_check(source_location);
339
340 source_location.set_property_class("assigns");
341
342 const auto &orig_comment = source_location.get_comment();
343 std::string comment = "Check that ";
345 {
346 if(!car.condition().is_true())
347 comment += from_expr(ns, "", car.condition()) + ": ";
348 comment += from_expr(ns, "", car.target());
349 }
350 else
351 comment += id2string(orig_comment);
352
353 comment += " is assignable";
354 source_location.set_comment(comment);
355
358 car, allow_null_lhs, include_stack_allocated, cfg_info_opt),
359 source_location));
360}
361
363 const car_exprt &car,
364 const car_exprt &candidate_car) const
365{
366 // remark: both lb and ub are derived from the same object so checking
367 // same_object(upper_bound_address_var, lhs.upper_bound_address_var)
368 // is redundant
369 return simplify_expr(
370 and_exprt{
371 {candidate_car.valid_var(),
372 same_object(candidate_car.lower_bound_var(), car.lower_bound_var()),
373 less_than_or_equal_exprt{pointer_offset(candidate_car.lower_bound_var()),
374 pointer_offset(car.lower_bound_var())},
376 pointer_offset(car.upper_bound_var()),
377 pointer_offset(candidate_car.upper_bound_var())}}},
378 ns);
379}
380
382 const car_exprt &car,
383 bool allow_null_lhs,
384 bool include_stack_allocated,
385 optionalt<cfg_infot> &cfg_info_opt) const
386{
387 bool no_targets = from_spec_assigns.empty() && from_heap_alloc.empty() &&
388 (!include_stack_allocated || from_stack_alloc.empty());
389
390 // inclusion check expression
391 if(no_targets)
392 {
393 // if null lhs are allowed then we should have a null lhs when
394 // we reach this program point, otherwise we should never reach
395 // this program point
396 if(allow_null_lhs)
398 else
399 return false_exprt{};
400 }
401
402 // Build a disjunction over all tracked locations
403 exprt::operandst disjuncts;
404
405 for(const auto &pair : from_spec_assigns)
406 disjuncts.push_back(inclusion_check_single(car, pair.second));
407
408 for(const auto &pair : from_heap_alloc)
409 disjuncts.push_back(inclusion_check_single(car, pair.second));
410
411 if(include_stack_allocated)
412 {
413 for(const auto &pair : from_stack_alloc)
414 {
415 // skip dead targets
416 if(
417 cfg_info_opt.has_value() &&
418 !cfg_info_opt.value().is_maybe_alive(pair.first))
419 continue;
420
421 disjuncts.push_back(inclusion_check_single(car, pair.second));
422 }
423 }
424
425 if(allow_null_lhs)
427 and_exprt{car.valid_var(), disjunction(disjuncts)}};
428 else
429 return and_exprt{car.valid_var(), disjunction(disjuncts)};
430}
431
433 const exprt &condition,
434 const exprt &target)
435{
436 conditional_target_exprt key{condition, target};
437 const auto &found = from_spec_assigns.find(key);
438 if(found != from_spec_assigns.end())
439 {
440 log.warning() << "Ignored duplicate expression '"
441 << from_expr(ns, target.id(), target)
442 << "' in assigns clause spec at "
443 << target.source_location().as_string() << messaget::eom;
444 return found->second;
445 }
446 else
447 {
448 from_spec_assigns.insert({key, create_car_expr(condition, target)});
449 return from_spec_assigns.find(key)->second;
450 }
451}
452
454 const symbol_exprt &target)
455{
456 const auto &found = from_stack_alloc.find(target);
457 if(found != from_stack_alloc.end())
458 {
459 log.warning() << "Ignored duplicate stack-allocated target '"
460 << from_expr(ns, target.id(), target) << "' at "
461 << target.source_location().as_string() << messaget::eom;
462 return found->second;
463 }
464 else
465 {
466 from_stack_alloc.insert({target, create_car_expr(true_exprt{}, target)});
467 return from_stack_alloc.find(target)->second;
468 }
469}
470
471const car_exprt &
473{
474 const auto &found = from_heap_alloc.find(target);
475 if(found != from_heap_alloc.end())
476 {
477 log.warning() << "Ignored duplicate heap-allocated target '"
478 << from_expr(ns, target.id(), target) << "' at "
479 << target.source_location().as_string() << messaget::eom;
480 return found->second;
481 }
482 else
483 {
484 from_heap_alloc.insert({target, create_car_expr(true_exprt{}, target)});
485 return from_heap_alloc.find(target)->second;
486 }
487}
488
490 const car_exprt &tracked_car,
491 const car_exprt &freed_car,
492 goto_programt &result) const
493{
494 source_locationt source_location(freed_car.source_location());
495 add_pragma_disable_pointer_checks(source_location);
496 add_pragma_disable_assigns_check(source_location);
497
499 tracked_car.valid_var(),
500 and_exprt{tracked_car.valid_var(),
501 not_exprt{same_object(
502 tracked_car.lower_bound_var(), freed_car.lower_bound_var())}},
503 source_location));
504}
505
507 const car_exprt &freed_car,
508 goto_programt &dest) const
509{
510 for(const auto &pair : from_spec_assigns)
511 invalidate_car(pair.second, freed_car, dest);
512
513 for(const auto &pair : from_heap_alloc)
514 invalidate_car(pair.second, freed_car, dest);
515}
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
signedbv_typet signed_size_type()
Definition: c_types.cpp:84
bitvector_typet char_type()
Definition: c_types.cpp:124
Function Call Graphs.
Operator to return the address of an object.
Definition: pointer_expr.h:361
Boolean AND.
Definition: std_expr.h:1974
The Boolean type.
Definition: std_types.h:36
directed_grapht get_directed_graph() const
Returns a grapht representation of this call graph, suitable for use with generic grapht algorithms.
Definition: call_graph.cpp:209
static call_grapht create_from_root_function(const goto_modelt &model, const irep_idt &root, bool collect_callsites)
Definition: call_graph.h:53
Class that represents a normalized conditional address range, with:
const symbol_exprt & upper_bound_var() const
Identifier of the upper address bound snapshot variable.
const exprt & target_start_address() const
Start address of the target.
const symbol_exprt & valid_var() const
Identifier of the validity snapshot variable.
const exprt & target() const
The target expression.
const symbol_exprt & lower_bound_var() const
Identifier of the lower address bound snapshot variable.
const exprt & target_size() const
Size of the target in bytes.
const exprt & condition() const
Condition expression. When this condition holds the target is allowed.
Allows to clean expressions of side effects.
Definition: utils.h:249
void clean(exprt &guard, goto_programt &dest, const irep_idt &mode)
Definition: utils.h:258
Class that represents a single conditional target.
A class for an expression that represents a conditional target or a list of targets sharing a common ...
Definition: c_expr.h:232
const exprt::operandst & targets() const
Definition: c_expr.h:276
const exprt & condition() const
Definition: c_expr.h:266
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
typet & type()
Return the type of the expression.
Definition: expr.h:82
const source_locationt & source_location() const
Definition: expr.h:230
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
The Boolean constant false.
Definition: std_expr.h:2865
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:715
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:949
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:922
void invalidate_stack_allocated(const symbol_exprt &symbol_expr, goto_programt &dest)
Generate instructions to invalidate a stack-allocated object that goes DEAD in dest.
const goto_functionst & functions
Other functions of the model.
void track_spec_target(const exprt &expr, goto_programt &dest)
Track an assigns clause target and generate snaphsot instructions and well-definedness assertions in ...
symbol_exprt_to_car_mapt from_stack_alloc
Map to from DECL symbols to corresponding conditional address ranges.
void track_stack_allocated(const symbol_exprt &symbol_expr, goto_programt &dest)
Track a stack-allocated object and generate snaphsot instructions in dest.
void inclusion_check_assertion(const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated, optionalt< cfg_infot > &cfg_info_opt, goto_programt &dest) const
Returns an inclusion check assertion of lhs over all tracked cars.
cond_target_exprt_to_car_mapt from_spec_assigns
Map to from conditional target expressions of assigns clauses to corresponding conditional address ra...
void track_heap_allocated(const exprt &expr, goto_programt &dest)
Track a whole heap-alloc object and generate snaphsot instructions in dest.
const car_exprt & create_car_from_spec_assigns(const exprt &condition, const exprt &target)
void invalidate_car(const car_exprt &tracked_car, const car_exprt &freed_car, goto_programt &result) const
Adds an assignment in dest to invalidate the tracked car if was valid before and was pointing to the ...
exprt_to_car_mapt from_heap_alloc
Map to from malloc'd symbols to corresponding conditional address ranges.
car_exprt create_car_expr(const exprt &condition, const exprt &target) const
Creates a conditional address range expression from a cleaned-up condition and target expression.
void track_spec_target_group(const conditional_target_group_exprt &group, goto_programt &dest)
Track and generate snaphsot instructions and target validity checking assertions for a conditional ta...
void target_validity_assertion(const car_exprt &car, bool allow_null_target, goto_programt &dest) const
Generates the target validity assertion for the given car and adds it to dest.
exprt inclusion_check_full(const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated, optionalt< cfg_infot > &cfg_info_opt) const
Returns an inclusion check expression of lhs over all tracked cars.
void track_static_locals(goto_programt &dest)
Search the call graph reachable from the instrumented function to identify local static variables use...
void track_plain_spec_target(const exprt &expr, goto_programt &dest)
Track and generate snaphsot instructions and target validity checking assertions for a conditional ta...
const symbolt create_fresh_symbol(const std::string &suffix, const typet &type, const source_locationt &location) const
Creates a fresh symbolt with given suffix, scoped to function_id.
void invalidate_heap_and_spec_aliases(const car_exprt &freed_car, goto_programt &dest) const
Generates instructions to invalidate all targets aliased with a car that was passed to free,...
const car_exprt & create_car_from_stack_alloc(const symbol_exprt &target)
const car_exprt & create_car_from_heap_alloc(const exprt &target)
exprt inclusion_check_single(const car_exprt &lhs, const car_exprt &candidate_car) const
Returns inclusion check expression for a single candidate location.
const namespacet ns
Program namespace.
exprt target_validity_expr(const car_exprt &car, bool allow_null_target) const
Returns the target validity expression for a car_exprt.
void create_snapshot(const car_exprt &car, goto_programt &dest) const
Returns snapshot instructions for a car_exprt.
symbol_tablet & st
Program symbol table.
const irep_idt & function_id
Name of the instrumented function.
void check_inclusion_assignment(const exprt &lhs, optionalt< cfg_infot > &cfg_info_opt, goto_programt &dest)
Generates inclusion check instructions for an assignment, havoc or havoc_object instruction.
bool stack_allocated_is_tracked(const symbol_exprt &symbol_expr) const
Returns true if the expression is tracked.
void check_inclusion_heap_allocated_and_invalidate_aliases(const exprt &expr, optionalt< cfg_infot > &cfg_info_opt, goto_programt &dest)
Generates inclusion check instructions for an argument passed to free.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const irep_idt & id() const
Definition: irep.h:396
Binary less than or equal operator expression.
Definition: std_expr.h:782
message_handlert & get_message_handler()
Definition: message.h:184
mstreamt & warning() const
Definition: message.h:404
static eomt eom
Definition: message.h:297
Binary minus.
Definition: std_expr.h:973
Boolean negation.
Definition: std_expr.h:2181
Boolean OR.
Definition: std_expr.h:2082
The plus expression Associativity is not specified.
Definition: std_expr.h:914
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
const irep_idt & get_function() const
std::string as_string() const
const irep_idt & get_comment() const
void set_function(const irep_idt &function)
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Symbol table entry.
Definition: symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
irep_idt mode
Language mode.
Definition: symbol.h:49
The Boolean constant true.
Definition: std_expr.h:2856
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:293
A predicate that indicates that an address range is ok to write.
Definition: pointer_expr.h:781
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
Definition: expr_util.cpp:21
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:138
Deprecated expression utility functions.
Specify write set in function contracts.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
nonstd::optional< T > optionalt
Definition: optional.h:35
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
exprt pointer_offset(const exprt &pointer)
exprt object_size(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
exprt null_pointer(const exprt &pointer)
Various predicates over pointers in programs.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
exprt simplify_expr(exprt src, const namespacet &ns)
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition: invariant.h:464
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:22
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
void add_pragma_disable_pointer_checks(source_locationt &location)
Adds a pragma on a source location disable all pointer checks.
Definition: utils.cpp:79
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &location, const irep_idt &mode, symbol_table_baset &symtab, std::string suffix, bool is_auxiliary)
Adds a fresh and uniquely named symbol to the symbol table.
Definition: utils.cpp:190
bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment)
Returns true if the given comment matches the type of comments created by make_assigns_clause_replace...
Definition: utils.cpp:278
void add_pragma_disable_assigns_check(source_locationt &location)
Adds a pragma on a source_locationt to disable inclusion checking.
Definition: utils.cpp:103