cprover
Loading...
Searching...
No Matches
reaching_definitions.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Range-based reaching definitions analysis (following Field-
4 Sensitive Program Dependence Analysis, Litvak et al., FSE 2010)
5
6Author: Michael Tautschnig
7
8Date: February 2013
9
10\*******************************************************************/
11
15
17
18#include <util/base_exceptions.h> // IWYU pragma: keep
19#include <util/make_unique.h>
21
23
24#include "dirty.h"
25#include "is_threaded.h"
26
27#include <memory>
28
32class rd_range_domain_factoryt : public ai_domain_factoryt<rd_range_domaint>
33{
34public:
41
42 std::unique_ptr<statet> make(locationt) const override
43 {
45 CHECK_RETURN(p->is_bottom());
46 return std::unique_ptr<statet>(p.release());
47 }
48
49private:
51};
52
60
62
71void rd_range_domaint::populate_cache(const irep_idt &identifier) const
72{
74
75 valuest::const_iterator v_entry=values.find(identifier);
76 if(v_entry==values.end() ||
77 v_entry->second.empty())
78 return;
79
81
82 for(const auto &id : v_entry->second)
83 {
85
87 std::make_pair(v.bit_begin, v.bit_end));
88 }
89}
90
94 const irep_idt &function_to,
96 ai_baset &ai,
97 const namespacet &ns)
98{
99 locationt from{trace_from->current_location()};
100 locationt to{trace_to->current_location()};
101
103 dynamic_cast<reaching_definitions_analysist*>(&ai);
105 rd!=nullptr,
107 "ai has type reaching_definitions_analysist");
108
110
111 // kill values
112 if(from->is_dead())
113 transform_dead(ns, from);
114 // kill thread-local values
115 else if(from->is_start_thread())
116 transform_start_thread(ns, *rd);
117 // do argument-to-parameter assignments
118 else if(from->is_function_call())
120 // cleanup parameters
121 else if(from->is_end_function())
123 // lhs assignments
124 else if(from->is_assign())
126 // initial (non-deterministic) value
127 else if(from->is_decl())
129 // array_set, array_copy, array_replace have side effects
130 else if(from->is_other())
132}
133
137 const namespacet &,
139{
140 const irep_idt &identifier = from->dead_symbol().get_identifier();
141
142 valuest::iterator entry=values.find(identifier);
143
144 if(entry!=values.end())
145 {
146 values.erase(entry);
147 export_cache.erase(identifier);
148 }
149}
150
152 const namespacet &ns,
154{
155 for(valuest::iterator it=values.begin();
156 it!=values.end();
157 ) // no ++it
158 {
159 const irep_idt &identifier=it->first;
160
161 if(!ns.lookup(identifier).is_shared() &&
162 !rd.get_is_dirty()(identifier))
163 {
164 export_cache.erase(identifier);
165
166 valuest::iterator next=it;
167 ++next;
168 values.erase(it);
169 it=next;
170 }
171 else
172 ++it;
173 }
174}
175
177 const namespacet &ns,
178 const irep_idt &function_from,
180 const irep_idt &function_to,
182{
183 // only if there is an actual call, i.e., we have a body
184 const symbol_exprt &fn_symbol_expr = to_symbol_expr(from->call_function());
185 if(function_to == fn_symbol_expr.get_identifier())
186 {
187 for(valuest::iterator it=values.begin();
188 it!=values.end();
189 ) // no ++it
190 {
191 const irep_idt &identifier=it->first;
192
193 // dereferencing may introduce extra symbols
194 const symbolt *sym;
195 if((ns.lookup(identifier, sym) ||
196 !sym->is_shared()) &&
197 !rd.get_is_dirty()(identifier))
198 {
199 export_cache.erase(identifier);
200
201 valuest::iterator next=it;
202 ++next;
203 values.erase(it);
204 it=next;
205 }
206 else
207 ++it;
208 }
209
210 const code_typet &code_type=
211 to_code_type(ns.lookup(fn_symbol_expr.get_identifier()).type);
212
213 for(const auto &param : code_type.parameters())
214 {
215 const irep_idt &identifier=param.get_identifier();
216
217 if(identifier.empty())
218 continue;
219
220 auto param_bits = pointer_offset_bits(param.type(), ns);
221 if(param_bits.has_value())
222 {
223 gen(
224 from,
225 identifier,
226 range_spect{0},
228 }
229 else
230 gen(from, identifier, range_spect{0}, range_spect::unknown());
231 }
232 }
233 else
234 {
235 // handle return values of undefined functions
236 if(from->call_lhs().is_not_nil())
238 }
239}
240
242 const namespacet &ns,
243 const irep_idt &function_from,
245 const irep_idt &function_to,
248{
249 locationt call = to;
250 --call;
251
253 new_values.swap(values);
254 values=rd[call].values;
255
256 for(const auto &new_value : new_values)
257 {
258 const irep_idt &identifier=new_value.first;
259
260 if(!rd.get_is_threaded()(call) ||
261 (!ns.lookup(identifier).is_shared() &&
262 !rd.get_is_dirty()(identifier)))
263 {
264 for(const auto &id : new_value.second)
265 {
268 }
269 }
270
271 for(const auto &id : new_value.second)
272 {
275 }
276 }
277
279
280 for(const auto &param : code_type.parameters())
281 {
282 const irep_idt &identifier=param.get_identifier();
283
284 if(identifier.empty())
285 continue;
286
287 valuest::iterator entry=values.find(identifier);
288
289 if(entry!=values.end())
290 {
291 values.erase(entry);
292 export_cache.erase(identifier);
293 }
294 }
295
296 // handle return values
297 if(call->call_lhs().is_not_nil())
298 {
300 }
301}
302
304 const namespacet &ns,
306 const irep_idt &function_to,
309{
312 const bool is_must_alias=rw_set.get_w_set().size()==1;
313
314 for(const auto &written_object_entry : rw_set.get_w_set())
315 {
316 const irep_idt &identifier = written_object_entry.first;
317 // ignore symex::invalid_object
318 const symbolt *symbol_ptr;
319 if(ns.lookup(identifier, symbol_ptr))
320 continue;
322 symbol_ptr!=nullptr,
324 "Symbol is in symbol table");
325
326 const range_domaint &ranges =
327 rw_set.get_ranges(written_object_entry.second);
328
329 if(is_must_alias &&
330 (!rd.get_is_threaded()(from) ||
331 (!symbol_ptr->is_shared() &&
332 !rd.get_is_dirty()(identifier))))
333 for(const auto &range : ranges)
334 kill(identifier, range.first, range.second);
335
336 for(const auto &range : ranges)
337 gen(from, identifier, range.first, range.second);
338 }
339}
340
342 const irep_idt &identifier,
344 const range_spect &range_end)
345{
347
348 if(range_end.is_unknown())
349 {
350 kill_inf(identifier, range_start);
351 return;
352 }
353
355
356 valuest::iterator entry=values.find(identifier);
357 if(entry==values.end())
358 return;
359
360 bool clear_export_cache=false;
362
363 for(values_innert::iterator
364 it=entry->second.begin();
365 it!=entry->second.end();
366 ) // no ++it
367 {
369
370 if(v.bit_begin >= range_end)
371 ++it;
372 else if(!v.bit_end.is_unknown() && v.bit_end <= range_start)
373 {
374 ++it;
375 }
376 else if(
378 v.bit_end <= range_end) // rs <= a < b <= re
379 {
381
382 entry->second.erase(it++);
383 }
384 else if(v.bit_begin >= range_start) // rs <= a <= re < b
385 {
387
389 v_new.bit_begin=range_end;
391
392 entry->second.erase(it++);
393 }
394 else if(v.bit_end.is_unknown() || v.bit_end > range_end) // a <= rs < re < b
395 {
397
399 v_new.bit_end=range_start;
400
402 v_new2.bit_begin=range_end;
403
406
407 entry->second.erase(it++);
408 }
409 else // a <= rs < b <= re
410 {
412
414 v_new.bit_end=range_start;
416
417 entry->second.erase(it++);
418 }
419 }
420
422 export_cache.erase(identifier);
423
424 values_innert::iterator it=entry->second.begin();
425 for(const auto &id : new_values)
426 {
427 while(it!=entry->second.end() && *it<id)
428 ++it;
429 if(it==entry->second.end() || id<*it)
430 {
431 entry->second.insert(it, id);
432 }
433 else if(it!=entry->second.end())
434 {
435 DATA_INVARIANT(*it == id, "entries must match");
436 ++it;
437 }
438 }
439}
440
442 const irep_idt &,
444{
446
447#if 0
448 valuest::iterator entry=values.find(identifier);
449 if(entry==values.end())
450 return;
451
453
454 // makes the analysis underapproximating
455 rangest &ranges=entry->second;
456
457 for(rangest::iterator it=ranges.begin();
458 it!=ranges.end();
459 ) // no ++it
460 if(it->second.first!=-1 &&
461 it->second.first <= range_start)
462 ++it;
463 else if(it->first >= range_start) // rs <= a < b <= re
464 {
465 ranges.erase(it++);
466 }
467 else // a <= rs < b < re
468 {
469 it->second.first=range_start;
470 ++it;
471 }
472#endif
473}
474
481 const irep_idt &identifier,
483 const range_spect &range_end)
484{
485 // objects of size 0 like union U { signed : 0; };
487 return false;
488
491
493 if(!values[identifier].insert(bv_container->add(v)).second)
494 return false;
495
496 export_cache.erase(identifier);
497
498#if 0
500
501 std::pair<valuest::iterator, bool> entry=
502 values.insert(std::make_pair(identifier, rangest()));
503 rangest &ranges=entry.first->second;
504
505 if(!entry.second)
506 {
507 for(rangest::iterator it=ranges.begin();
508 it!=ranges.end();
509 ) // no ++it
510 {
511 if(it->second.second!=from ||
512 (it->second.first!=-1 && it->second.first <= range_start) ||
513 (range_end!=-1 && it->first >= range_end))
514 ++it;
515 else if(it->first > range_start) // rs < a < b,re
516 {
517 if(range_end!=-1)
518 merged_range_end=std::max(range_end, it->second.first);
519 ranges.erase(it++);
520 }
521 else if(it->second.first==-1 ||
522 (range_end!=-1 &&
523 it->second.first >= range_end)) // a <= rs < re <= b
524 {
525 // nothing to do
526 return false;
527 }
528 else // a <= rs < b < re
529 {
530 it->second.first=range_end;
531 return true;
532 }
533 }
534 }
535
536 ranges.insert(std::make_pair(
538 std::make_pair(merged_range_end, from)));
539#endif
540
541 return true;
542}
543
544void rd_range_domaint::output(std::ostream &out) const
545{
546 out << "Reaching definitions:\n";
547
548 if(has_values.is_known())
549 {
550 out << has_values.to_string() << '\n';
551 return;
552 }
553
554 for(const auto &value : values)
555 {
556 const irep_idt &identifier=value.first;
557
558 const ranges_at_loct &ranges=get(identifier);
559
560 out << " " << identifier << "[";
561
562 for(ranges_at_loct::const_iterator itl=ranges.begin();
563 itl!=ranges.end();
564 ++itl)
565 for(rangest::const_iterator itr=itl->second.begin();
566 itr!=itl->second.end();
567 ++itr)
568 {
569 if(itr!=itl->second.begin() ||
570 itl!=ranges.begin())
571 out << ";";
572
573 out << itr->first << ":" << itr->second;
574 out << "@" << itl->first->location_number;
575 }
576
577 out << "]\n";
578
579 clear_cache(identifier);
580 }
581}
582
585 values_innert &dest,
586 const values_innert &other)
587{
588 bool more=false;
589
590#if 0
591 ranges_at_loct::iterator itr=it->second.begin();
592 for(const auto &o : ito->second)
593 {
594 while(itr!=it->second.end() && itr->first<o.first)
595 ++itr;
596 if(itr==it->second.end() || o.first<itr->first)
597 {
598 it->second.insert(o);
599 more=true;
600 }
601 else if(itr!=it->second.end())
602 {
603 assert(itr->first==o.first);
604
605 for(const auto &o_range : o.second)
606 more=gen(itr->second, o_range.first, o_range.second) ||
607 more;
608
609 ++itr;
610 }
611 }
612#else
613 values_innert::iterator itr=dest.begin();
614 for(const auto &id : other)
615 {
616 while(itr!=dest.end() && *itr<id)
617 ++itr;
618 if(itr==dest.end() || id<*itr)
619 {
620 dest.insert(itr, id);
621 more=true;
622 }
623 else if(itr!=dest.end())
624 {
625 DATA_INVARIANT(*itr == id, "entries must match");
626 ++itr;
627 }
628 }
629#endif
630
631 return more;
632}
633
635 const rd_range_domaint &other,
638{
639 bool changed=has_values.is_false();
641
642 valuest::iterator it=values.begin();
643 for(const auto &value : other.values)
644 {
645 while(it!=values.end() && it->first<value.first)
646 ++it;
647 if(it==values.end() || value.first<it->first)
648 {
649 values.insert(value);
650 changed=true;
651 }
652 else if(it!=values.end())
653 {
654 DATA_INVARIANT(it->first == value.first, "entries must match");
655
656 if(merge_inner(it->second, value.second))
657 {
658 changed=true;
659 export_cache.erase(it->first);
660 }
661
662 ++it;
663 }
664 }
665
666 return changed;
667}
668
671 const rd_range_domaint &other,
672 locationt,
673 locationt,
674 const namespacet &ns)
675{
676 // TODO: dirty vars
677#if 0
679 dynamic_cast<reaching_definitions_analysist*>(&ai);
680 assert(rd!=0);
681#endif
682
683 bool changed=has_values.is_false();
685
686 valuest::iterator it=values.begin();
687 for(const auto &value : other.values)
688 {
689 const irep_idt &identifier=value.first;
690
691 if(!ns.lookup(identifier).is_shared()
692 /*&& !rd.get_is_dirty()(identifier)*/)
693 continue;
694
695 while(it!=values.end() && it->first<value.first)
696 ++it;
697 if(it==values.end() || value.first<it->first)
698 {
699 values.insert(value);
700 changed=true;
701 }
702 else if(it!=values.end())
703 {
704 DATA_INVARIANT(it->first == value.first, "entries must match");
705
706 if(merge_inner(it->second, value.second))
707 {
708 changed=true;
709 export_cache.erase(it->first);
710 }
711
712 ++it;
713 }
714 }
715
716 return changed;
717}
718
720 const irep_idt &identifier) const
721{
722 populate_cache(identifier);
723
724 static ranges_at_loct empty;
725
726 export_cachet::const_iterator entry=export_cache.find(identifier);
727
728 if(entry==export_cache.end())
729 return empty;
730 else
731 return entry->second;
732}
733
735 const goto_functionst &goto_functions)
736{
738 (*value_sets_)(goto_functions);
739 value_sets=std::move(value_sets_);
740
742
743 is_dirty=util_make_unique<dirtyt>(goto_functions);
744
746}
Generic exception types primarily designed for use with invariants.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:118
virtual void initialize(const irep_idt &function_id, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
Definition ai.cpp:194
ai_history_baset::trace_ptrt trace_ptrt
Definition ai_domain.h:74
goto_programt::const_targett locationt
Definition ai_domain.h:73
ai_domain_factory_baset::locationt locationt
Definition ai_domain.h:204
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
ait()
Definition ai.h:566
Base type of functions.
Definition std_types.h:539
Base class for concurrency-aware abstract interpretation.
Definition ai.h:652
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
bool empty() const
Definition dstring.h:90
A collection of goto functions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Data type to describe upper and lower bounds of the range of bits that a read or write access may aff...
Definition goto_rw.h:61
static range_spect unknown()
Definition goto_rw.h:69
static range_spect to_range_spect(const mp_integer &size)
Definition goto_rw.h:79
bool is_unknown() const
Definition goto_rw.h:74
This ensures that all domains are constructed with the appropriate pointer back to the analysis engin...
std::unique_ptr< statet > make(locationt) const override
sparse_bitvector_analysist< reaching_definitiont > *const bv_container
rd_range_domain_factoryt(sparse_bitvector_analysist< reaching_definitiont > *_bv_container)
Because the class is inherited from ai_domain_baset, its instance represents an element of a domain o...
void populate_cache(const irep_idt &identifier) const
Given the passed variable name identifier it collects data from bv_container for each ID in values[id...
export_cachet export_cache
It is a helper data structure.
void output(std::ostream &out, const ai_baset &, const namespacet &) const final override
void kill_inf(const irep_idt &identifier, const range_spect &range_start)
void transform_dead(const namespacet &ns, locationt from)
Computes an instance obtained from a *this by transformation over DEAD v GOTO instruction.
void transform_start_thread(const namespacet &ns, reaching_definitions_analysist &rd)
const ranges_at_loct & get(const irep_idt &identifier) const
void clear_cache(const irep_idt &identifier) const
sparse_bitvector_analysist< reaching_definitiont > *const bv_container
It points to the actual reaching definitions data of individual program variables.
void transform_function_call(const namespacet &ns, const irep_idt &function_from, locationt from, const irep_idt &function_to, reaching_definitions_analysist &rd)
bool merge(const rd_range_domaint &other, trace_ptrt from, trace_ptrt to)
Implements the "join" operation of two instances *this and other.
void transform_end_function(const namespacet &ns, const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, reaching_definitions_analysist &rd)
void transform_assign(const namespacet &ns, locationt from, const irep_idt &function_to, locationt to, reaching_definitions_analysist &rd)
bool merge_inner(values_innert &dest, const values_innert &other)
std::multimap< range_spect, range_spect > rangest
bool gen(locationt from, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
A utility function which updates internal data structures by inserting a new reaching definition reco...
void kill(const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
std::map< locationt, rangest, goto_programt::target_less_than > ranges_at_loct
tvt has_values
This (three value logic) flag determines, whether the instance represents top, bottom,...
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) final override
Computes an instance obtained from the instance *this by transformation over a GOTO instruction refer...
std::map< irep_idt, values_innert > valuest
valuest values
It is an ordered map from program variable names to IDs of reaching_definitiont instances stored in m...
bool merge_shared(const rd_range_domaint &other, locationt from, locationt to, const namespacet &ns)
std::set< std::size_t > values_innert
std::unique_ptr< is_threadedt > is_threaded
reaching_definitions_analysist(const namespacet &_ns)
const is_threadedt & get_is_threaded() const
std::unique_ptr< dirtyt > is_dirty
std::unique_ptr< value_setst > value_sets
void initialize(const goto_functionst &goto_functions) override
Initialize all the abstract states for a whole program.
const V & get(const std::size_t value_index) const
std::vector< typename inner_mapt::const_iterator > values
It is a map from an ID to the corresponding reaching_definitiont instance inside the map value_map.
std::size_t add(const V &value)
Expression to hold a symbol (variable)
Definition std_expr.h:113
Symbol table entry.
Definition symbol.h:28
bool is_known() const
Definition threeval.h:28
const char * to_string() const
Definition threeval.cpp:13
bool is_false() const
Definition threeval.h:26
static tvt unknown()
Definition threeval.h:33
Variables whose address is taken.
static void goto_rw(const irep_idt &function, goto_programt::const_targett target, const exprt &lhs, const exprt &function_expr, const exprt::operandst &arguments, rw_range_sett &rw_set)
Definition goto_rw.cpp:842
Over-approximate Concurrency for Threaded Goto Programs.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition make_unique.h:19
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis,...
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
Definition invariant.h:407
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
Identifies a GOTO instruction where a given variable is defined (i.e.
range_spect bit_begin
The two integers below define a range of bits (i.e.
ai_domain_baset::locationt definition_at
The iterator to the GOTO instruction where the variable has been written to.
irep_idt identifier
The name of the variable which was defined.
Value Set Propagation (flow insensitive)