CBMC
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
20
22
23#include "dirty.h"
24#include "is_threaded.h"
25
26#include <memory>
27
31class rd_range_domain_factoryt : public ai_domain_factoryt<rd_range_domaint>
32{
33public:
41
42 std::unique_ptr<statet> make(locationt) const override
43 {
44 auto p = std::make_unique<rd_range_domaint>(bv_container, message_handler);
45 CHECK_RETURN(p->is_bottom());
46 return std::unique_ptr<statet>(p.release());
47 }
48
49private:
52};
53
62
64
73void rd_range_domaint::populate_cache(const irep_idt &identifier) const
74{
76
77 valuest::const_iterator v_entry=values.find(identifier);
78 if(v_entry==values.end() ||
79 v_entry->second.empty())
80 return;
81
83
84 for(const auto &id : v_entry->second)
85 {
87
89 std::make_pair(v.bit_begin, v.bit_end));
90 }
91}
92
96 const irep_idt &function_to,
98 ai_baset &ai,
99 const namespacet &ns)
100{
101 locationt from{trace_from->current_location()};
102 locationt to{trace_to->current_location()};
103
105 dynamic_cast<reaching_definitions_analysist*>(&ai);
107 rd!=nullptr,
109 "ai has type reaching_definitions_analysist");
110
112
113 // kill values
114 if(from->is_dead())
115 transform_dead(ns, from);
116 // kill thread-local values
117 else if(from->is_start_thread())
118 transform_start_thread(ns, *rd);
119 // do argument-to-parameter assignments
120 else if(from->is_function_call())
122 // cleanup parameters
123 else if(from->is_end_function())
125 // lhs assignments
126 else if(from->is_assign())
128 // initial (non-deterministic) value
129 else if(from->is_decl())
131 // array_set, array_copy, array_replace have side effects
132 else if(from->is_other())
134}
135
139 const namespacet &,
141{
142 const irep_idt &identifier = from->dead_symbol().get_identifier();
143
144 valuest::iterator entry=values.find(identifier);
145
146 if(entry!=values.end())
147 {
148 values.erase(entry);
149 export_cache.erase(identifier);
150 }
151}
152
154 const namespacet &ns,
156{
157 for(valuest::iterator it=values.begin();
158 it!=values.end();
159 ) // no ++it
160 {
161 const irep_idt &identifier=it->first;
162
163 if(!ns.lookup(identifier).is_shared() &&
164 !rd.get_is_dirty()(identifier))
165 {
166 export_cache.erase(identifier);
167
168 valuest::iterator next=it;
169 ++next;
170 values.erase(it);
171 it=next;
172 }
173 else
174 ++it;
175 }
176}
177
179 const namespacet &ns,
180 const irep_idt &function_from,
182 const irep_idt &function_to,
184{
185 // only if there is an actual call, i.e., we have a body
186 const symbol_exprt &fn_symbol_expr = to_symbol_expr(from->call_function());
187 if(function_to == fn_symbol_expr.get_identifier())
188 {
189 for(valuest::iterator it=values.begin();
190 it!=values.end();
191 ) // no ++it
192 {
193 const irep_idt &identifier=it->first;
194
195 // dereferencing may introduce extra symbols
196 const symbolt *sym;
197 if((ns.lookup(identifier, sym) ||
198 !sym->is_shared()) &&
199 !rd.get_is_dirty()(identifier))
200 {
201 export_cache.erase(identifier);
202
203 valuest::iterator next=it;
204 ++next;
205 values.erase(it);
206 it=next;
207 }
208 else
209 ++it;
210 }
211
212 const code_typet &code_type=
213 to_code_type(ns.lookup(fn_symbol_expr.get_identifier()).type);
214
215 for(const auto &param : code_type.parameters())
216 {
217 const irep_idt &identifier=param.get_identifier();
218
219 if(identifier.empty())
220 continue;
221
222 auto param_bits = pointer_offset_bits(param.type(), ns);
223 if(param_bits.has_value())
224 {
225 gen(
226 from,
227 identifier,
228 range_spect{0},
230 }
231 else
232 gen(from, identifier, range_spect{0}, range_spect::unknown());
233 }
234 }
235 else
236 {
237 // handle return values of undefined functions
238 if(from->call_lhs().is_not_nil())
240 }
241}
242
244 const namespacet &ns,
245 const irep_idt &function_from,
247 const irep_idt &function_to,
250{
251 locationt call = to;
252 --call;
253
255 new_values.swap(values);
256 values=rd[call].values;
257
258 for(const auto &new_value : new_values)
259 {
260 const irep_idt &identifier=new_value.first;
261
262 if(!rd.get_is_threaded()(call) ||
263 (!ns.lookup(identifier).is_shared() &&
264 !rd.get_is_dirty()(identifier)))
265 {
266 for(const auto &id : new_value.second)
267 {
270 }
271 }
272
273 for(const auto &id : new_value.second)
274 {
277 }
278 }
279
281
282 for(const auto &param : code_type.parameters())
283 {
284 const irep_idt &identifier=param.get_identifier();
285
286 if(identifier.empty())
287 continue;
288
289 valuest::iterator entry=values.find(identifier);
290
291 if(entry!=values.end())
292 {
293 values.erase(entry);
294 export_cache.erase(identifier);
295 }
296 }
297
298 // handle return values
299 if(call->call_lhs().is_not_nil())
300 {
302 }
303}
304
306 const namespacet &ns,
308 const irep_idt &function_to,
311{
314 const bool is_must_alias=rw_set.get_w_set().size()==1;
315
316 for(const auto &written_object_entry : rw_set.get_w_set())
317 {
318 const irep_idt &identifier = written_object_entry.first;
319 // ignore symex::invalid_object
320 const symbolt *symbol_ptr;
321 if(ns.lookup(identifier, symbol_ptr))
322 continue;
324 symbol_ptr!=nullptr,
326 "Symbol is in symbol table");
327
328 const range_domaint &ranges =
329 rw_set.get_ranges(written_object_entry.second);
330
331 if(is_must_alias &&
332 (!rd.get_is_threaded()(from) ||
333 (!symbol_ptr->is_shared() &&
334 !rd.get_is_dirty()(identifier))))
335 for(const auto &range : ranges)
336 kill(identifier, range.first, range.second);
337
338 for(const auto &range : ranges)
339 gen(from, identifier, range.first, range.second);
340 }
341}
342
344 const irep_idt &identifier,
346 const range_spect &range_end)
347{
349
350 if(range_end.is_unknown())
351 {
352 kill_inf(identifier, range_start);
353 return;
354 }
355
357
358 valuest::iterator entry=values.find(identifier);
359 if(entry==values.end())
360 return;
361
362 bool clear_export_cache=false;
364
365 for(values_innert::iterator
366 it=entry->second.begin();
367 it!=entry->second.end();
368 ) // no ++it
369 {
371
372 if(v.bit_begin >= range_end)
373 ++it;
374 else if(!v.bit_end.is_unknown() && v.bit_end <= range_start)
375 {
376 ++it;
377 }
378 else if(
380 v.bit_end <= range_end) // rs <= a < b <= re
381 {
383
384 entry->second.erase(it++);
385 }
386 else if(v.bit_begin >= range_start) // rs <= a <= re < b
387 {
389
391 v_new.bit_begin=range_end;
393
394 entry->second.erase(it++);
395 }
396 else if(v.bit_end.is_unknown() || v.bit_end > range_end) // a <= rs < re < b
397 {
399
401 v_new.bit_end=range_start;
402
404 v_new2.bit_begin=range_end;
405
408
409 entry->second.erase(it++);
410 }
411 else // a <= rs < b <= re
412 {
414
416 v_new.bit_end=range_start;
418
419 entry->second.erase(it++);
420 }
421 }
422
424 export_cache.erase(identifier);
425
426 values_innert::iterator it=entry->second.begin();
427 for(const auto &id : new_values)
428 {
429 while(it!=entry->second.end() && *it<id)
430 ++it;
431 if(it==entry->second.end() || id<*it)
432 {
433 entry->second.insert(it, id);
434 }
435 else if(it!=entry->second.end())
436 {
437 DATA_INVARIANT(*it == id, "entries must match");
438 ++it;
439 }
440 }
441}
442
444 const irep_idt &,
446{
448
449#if 0
450 valuest::iterator entry=values.find(identifier);
451 if(entry==values.end())
452 return;
453
455
456 // makes the analysis underapproximating
457 rangest &ranges=entry->second;
458
459 for(rangest::iterator it=ranges.begin();
460 it!=ranges.end();
461 ) // no ++it
462 if(it->second.first!=-1 &&
463 it->second.first <= range_start)
464 ++it;
465 else if(it->first >= range_start) // rs <= a < b <= re
466 {
467 ranges.erase(it++);
468 }
469 else // a <= rs < b < re
470 {
471 it->second.first=range_start;
472 ++it;
473 }
474#endif
475}
476
483 const irep_idt &identifier,
485 const range_spect &range_end)
486{
487 // objects of size 0 like union U { signed : 0; };
489 return false;
490
493
495 if(!values[identifier].insert(bv_container->add(v)).second)
496 return false;
497
498 export_cache.erase(identifier);
499
500#if 0
502
503 std::pair<valuest::iterator, bool> entry=
504 values.insert(std::make_pair(identifier, rangest()));
505 rangest &ranges=entry.first->second;
506
507 if(!entry.second)
508 {
509 for(rangest::iterator it=ranges.begin();
510 it!=ranges.end();
511 ) // no ++it
512 {
513 if(it->second.second!=from ||
514 (it->second.first!=-1 && it->second.first <= range_start) ||
515 (range_end!=-1 && it->first >= range_end))
516 ++it;
517 else if(it->first > range_start) // rs < a < b,re
518 {
519 if(range_end!=-1)
520 merged_range_end=std::max(range_end, it->second.first);
521 ranges.erase(it++);
522 }
523 else if(it->second.first==-1 ||
524 (range_end!=-1 &&
525 it->second.first >= range_end)) // a <= rs < re <= b
526 {
527 // nothing to do
528 return false;
529 }
530 else // a <= rs < b < re
531 {
532 it->second.first=range_end;
533 return true;
534 }
535 }
536 }
537
538 ranges.insert(std::make_pair(
540 std::make_pair(merged_range_end, from)));
541#endif
542
543 return true;
544}
545
546void rd_range_domaint::output(std::ostream &out) const
547{
548 out << "Reaching definitions:\n";
549
550 if(has_values.is_known())
551 {
552 out << has_values.to_string() << '\n';
553 return;
554 }
555
556 for(const auto &value : values)
557 {
558 const irep_idt &identifier=value.first;
559
560 const ranges_at_loct &ranges=get(identifier);
561
562 out << " " << identifier << "[";
563
564 for(ranges_at_loct::const_iterator itl=ranges.begin();
565 itl!=ranges.end();
566 ++itl)
567 for(rangest::const_iterator itr=itl->second.begin();
568 itr!=itl->second.end();
569 ++itr)
570 {
571 if(itr!=itl->second.begin() ||
572 itl!=ranges.begin())
573 out << ";";
574
575 out << itr->first << ":" << itr->second;
576 out << "@" << itl->first->location_number;
577 }
578
579 out << "]\n";
580
581 clear_cache(identifier);
582 }
583}
584
587 values_innert &dest,
588 const values_innert &other)
589{
590 bool more=false;
591
592#if 0
593 ranges_at_loct::iterator itr=it->second.begin();
594 for(const auto &o : ito->second)
595 {
596 while(itr!=it->second.end() && itr->first<o.first)
597 ++itr;
598 if(itr==it->second.end() || o.first<itr->first)
599 {
600 it->second.insert(o);
601 more=true;
602 }
603 else if(itr!=it->second.end())
604 {
605 assert(itr->first==o.first);
606
607 for(const auto &o_range : o.second)
608 more=gen(itr->second, o_range.first, o_range.second) ||
609 more;
610
611 ++itr;
612 }
613 }
614#else
615 values_innert::iterator itr=dest.begin();
616 for(const auto &id : other)
617 {
618 while(itr!=dest.end() && *itr<id)
619 ++itr;
620 if(itr==dest.end() || id<*itr)
621 {
622 dest.insert(itr, id);
623 more=true;
624 }
625 else if(itr!=dest.end())
626 {
627 DATA_INVARIANT(*itr == id, "entries must match");
628 ++itr;
629 }
630 }
631#endif
632
633 return more;
634}
635
637 const rd_range_domaint &other,
640{
641 bool changed=has_values.is_false();
643
644 valuest::iterator it=values.begin();
645 for(const auto &value : other.values)
646 {
647 while(it!=values.end() && it->first<value.first)
648 ++it;
649 if(it==values.end() || value.first<it->first)
650 {
651 values.insert(value);
652 changed=true;
653 }
654 else if(it!=values.end())
655 {
656 DATA_INVARIANT(it->first == value.first, "entries must match");
657
658 if(merge_inner(it->second, value.second))
659 {
660 changed=true;
661 export_cache.erase(it->first);
662 }
663
664 ++it;
665 }
666 }
667
668 return changed;
669}
670
673 const rd_range_domaint &other,
674 locationt,
675 locationt,
676 const namespacet &ns)
677{
678 // TODO: dirty vars
679#if 0
681 dynamic_cast<reaching_definitions_analysist*>(&ai);
682 assert(rd!=0);
683#endif
684
685 bool changed=has_values.is_false();
687
688 valuest::iterator it=values.begin();
689 for(const auto &value : other.values)
690 {
691 const irep_idt &identifier=value.first;
692
693 if(!ns.lookup(identifier).is_shared()
694 /*&& !rd.get_is_dirty()(identifier)*/)
695 continue;
696
697 while(it!=values.end() && it->first<value.first)
698 ++it;
699 if(it==values.end() || value.first<it->first)
700 {
701 values.insert(value);
702 changed=true;
703 }
704 else if(it!=values.end())
705 {
706 DATA_INVARIANT(it->first == value.first, "entries must match");
707
708 if(merge_inner(it->second, value.second))
709 {
710 changed=true;
711 export_cache.erase(it->first);
712 }
713
714 ++it;
715 }
716 }
717
718 return changed;
719}
720
722 const irep_idt &identifier) const
723{
724 populate_cache(identifier);
725
726 static ranges_at_loct empty;
727
728 export_cachet::const_iterator entry=export_cache.find(identifier);
729
730 if(entry==export_cache.end())
731 return empty;
732 else
733 return entry->second;
734}
735
737 const goto_functionst &goto_functions)
738{
739 auto value_sets_ = std::make_unique<value_set_analysis_fit>(ns);
740 (*value_sets_)(goto_functions);
741 value_sets=std::move(value_sets_);
742
743 is_threaded = std::make_unique<is_threadedt>(goto_functions);
744
745 is_dirty = std::make_unique<dirtyt>(goto_functions);
746
748}
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:117
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:73
goto_programt::const_targett locationt
Definition ai_domain.h:72
ai_domain_factory_baset::locationt locationt
Definition ai_domain.h:203
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base type of functions.
Definition std_types.h:583
Base class for concurrency-aware abstract interpretation.
Definition ai.h:651
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool empty() const
Definition dstring.h:89
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...
rd_range_domain_factoryt(sparse_bitvector_analysist< reaching_definitiont > *_bv_container, message_handlert &message_handler)
std::unique_ptr< statet > make(locationt) const override
sparse_bitvector_analysist< reaching_definitiont > *const 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
message_handlert & message_handler
std::unique_ptr< is_threadedt > is_threaded
const is_threadedt & get_is_threaded() const
std::unique_ptr< dirtyt > is_dirty
std::unique_ptr< value_setst > value_sets
reaching_definitions_analysist(const namespacet &_ns, message_handlert &)
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:131
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:845
Over-approximate Concurrency for Threaded Goto Programs.
STL namespace.
std::optional< 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:272
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
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)