cprover
Loading...
Searching...
No Matches
value_set_fi.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Value Set (Flow Insensitive, Sharing)
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "value_set_fi.h"
13
14#include <ostream>
15
17
18#include <util/arith_tools.h>
19#include <util/byte_operators.h>
20#include <util/c_types.h>
21#include <util/namespace.h>
22#include <util/pointer_expr.h>
23#include <util/prefix.h>
24#include <util/simplify_expr.h>
25#include <util/std_code.h>
26#include <util/symbol.h>
27
29
31
34
35static const char *alloc_adapter_prefix="alloc_adaptor::";
36
38 const namespacet &ns,
39 std::ostream &out) const
40{
41 for(valuest::const_iterator
42 v_it=values.begin();
43 v_it!=values.end();
44 v_it++)
45 {
46 irep_idt identifier, display_name;
47
48 const entryt &e=v_it->second;
49
50 if(has_prefix(id2string(e.identifier), "value_set::dynamic_object"))
51 {
52 display_name=id2string(e.identifier)+e.suffix;
53 identifier.clear();
54 }
55 else
56 {
57 #if 0
58 const symbolt &symbol=ns.lookup(id2string(e.identifier));
59 display_name=symbol.display_name()+e.suffix;
60 identifier=symbol.name;
61 #else
62 identifier=id2string(e.identifier);
63 display_name=id2string(identifier)+e.suffix;
64 #endif
65 }
66
67 out << display_name;
68
69 out << " = { ";
70
71 object_mapt object_map;
72 flatten(e, object_map);
73
74 std::size_t width=0;
75
76 const auto &entries = object_map.read();
77 for(object_map_dt::const_iterator o_it = entries.begin();
78 o_it != entries.end();
79 ++o_it)
80 {
81 const exprt &o=object_numbering[o_it->first];
82
83 std::string result;
84
85 if(o.id()==ID_invalid || o.id()==ID_unknown)
86 {
87 result="<";
88 result+=from_expr(ns, identifier, o);
89 result+=", *, "; // offset unknown
90 if(o.type().id()==ID_unknown)
91 result+='*';
92 else
93 result+=from_type(ns, identifier, o.type());
94 result+='>';
95 }
96 else
97 {
98 result="<"+from_expr(ns, identifier, o)+", ";
99
100 if(o_it->second)
101 result += integer2string(*o_it->second);
102 else
103 result+='*';
104
105 result+=", ";
106
107 if(o.type().id()==ID_unknown)
108 result+='*';
109 else
110 result+=from_type(ns, identifier, o.type());
111
112 result+='>';
113 }
114
115 out << result;
116
117 width+=result.size();
118
120 next++;
121
122 if(next != entries.end())
123 {
124 out << ", ";
125 if(width>=40)
126 out << "\n ";
127 }
128 }
129
130 out << " } \n";
131 }
132}
133
135 const entryt &e,
136 object_mapt &dest) const
137{
138 #if 0
139 std::cout << "FLATTEN: " << e.identifier << e.suffix << '\n';
140 #endif
141
142 flatten_seent seen;
143 flatten_rec(e, dest, seen);
144
145 #if 0
146 std::cout << "FLATTEN: Done.\n";
147 #endif
148}
149
151 const entryt &e,
152 object_mapt &dest,
153 flatten_seent &seen) const
154{
155 #if 0
156 std::cout << "FLATTEN_REC: " << e.identifier << e.suffix << '\n';
157 #endif
158
159 std::string identifier = id2string(e.identifier);
160 assert(seen.find(identifier + e.suffix)==seen.end());
161
162 bool generalize_index = false;
163
164 seen.insert(identifier + e.suffix);
165
166 for(const auto &object_entry : e.object_map.read())
167 {
168 const exprt &o = object_numbering[object_entry.first];
169
170 if(o.type().id()=="#REF#")
171 {
172 if(seen.find(o.get(ID_identifier))!=seen.end())
173 {
174 generalize_index = true;
175 continue;
176 }
177
178 valuest::const_iterator fi = values.find(o.get(ID_identifier));
179 if(fi==values.end())
180 {
181 // this is some static object, keep it in.
182 const symbol_exprt se(o.get(ID_identifier), o.type().subtype());
183 insert(dest, se, 0);
184 }
185 else
186 {
187 object_mapt temp;
188 flatten_rec(fi->second, temp, seen);
189
190 for(object_map_dt::iterator t_it=temp.write().begin();
191 t_it!=temp.write().end();
192 t_it++)
193 {
194 if(t_it->second && object_entry.second)
195 {
196 *t_it->second += *object_entry.second;
197 }
198 else
199 t_it->second.reset();
200 }
201
202 for(const auto &object_entry : temp.read())
203 insert(dest, object_entry);
204 }
205 }
206 else
207 insert(dest, object_entry);
208 }
209
210 if(generalize_index) // this means we had recursive symbols in there
211 {
212 for(auto &object_entry : dest.write())
213 object_entry.second.reset();
214 }
215
216 seen.erase(identifier + e.suffix);
217}
218
220{
221 const exprt &object=object_numbering[it.first];
222
223 if(object.id()==ID_invalid ||
224 object.id()==ID_unknown)
225 return object;
226
228
229 od.object()=object;
230
231 if(it.second)
232 od.offset() = from_integer(*it.second, c_index_type());
233
234 od.type()=od.object().type();
235
236 return std::move(od);
237}
238
240{
242 bool result=false;
243
244 for(valuest::const_iterator
245 it=new_values.begin();
246 it!=new_values.end();
247 it++)
248 {
249 valuest::iterator it2=values.find(it->first);
250
251 if(it2==values.end())
252 {
253 // we always track these
254 if(has_prefix(id2string(it->second.identifier),
255 "value_set::dynamic_object") ||
256 has_prefix(id2string(it->second.identifier),
257 "value_set::return_value"))
258 {
259 values.insert(*it);
260 result=true;
261 }
262
263 continue;
264 }
265
266 entryt &e=it2->second;
267 const entryt &new_e=it->second;
268
269 if(make_union(e.object_map, new_e.object_map))
270 result=true;
271 }
272
273 changed = result;
274
275 return result;
276}
277
279{
280 bool result=false;
281
282 for(const auto &object_entry : src.read())
283 {
284 if(insert(dest, object_entry))
285 result=true;
286 }
287
288 return result;
289}
290
291std::vector<exprt>
292value_set_fit::get_value_set(const exprt &expr, const namespacet &ns) const
293{
294 object_mapt object_map;
295 get_value_set(expr, object_map, ns);
296
297 object_mapt flat_map;
298
299 for(const auto &object_entry : object_map.read())
300 {
301 const exprt &object = object_numbering[object_entry.first];
302 if(object.type().id()=="#REF#")
303 {
304 assert(object.id()==ID_symbol);
305
306 const irep_idt &ident = object.get(ID_identifier);
307 valuest::const_iterator v_it = values.find(ident);
308
309 if(v_it!=values.end())
310 {
311 object_mapt temp;
312 flatten(v_it->second, temp);
313
314 for(object_map_dt::iterator t_it=temp.write().begin();
315 t_it!=temp.write().end();
316 t_it++)
317 {
318 if(t_it->second && object_entry.second)
319 {
320 *t_it->second += *object_entry.second;
321 }
322 else
323 t_it->second.reset();
324
325 flat_map.write()[t_it->first]=t_it->second;
326 }
327 }
328 }
329 else
330 flat_map.write()[object_entry.first] = object_entry.second;
331 }
332
333 std::vector<exprt> result;
334 for(const auto &object_entry : flat_map.read())
335 result.push_back(to_expr(object_entry));
336
337#if 0
338 // Sanity check!
339 for(std::list<exprt>::const_iterator it=value_set.begin();
340 it!=value_set.end();
341 it++)
342 assert(it->type().id()!="#REF");
343#endif
344
345#if 0
346 for(expr_sett::const_iterator it=value_set.begin(); it!=value_set.end(); it++)
347 std::cout << "GET_VALUE_SET: " << format(*it) << '\n';
348#endif
349
350 return result;
351}
352
354 const exprt &expr,
355 object_mapt &dest,
356 const namespacet &ns) const
357{
358 exprt tmp(expr);
359 simplify(tmp, ns);
360
361 gvs_recursion_sett recset;
362 get_value_set_rec(tmp, dest, "", tmp.type(), ns, recset);
363}
364
366 const exprt &expr,
367 object_mapt &dest,
368 const std::string &suffix,
369 const typet &original_type,
370 const namespacet &ns,
371 gvs_recursion_sett &recursion_set) const
372{
373 #if 0
374 std::cout << "GET_VALUE_SET_REC EXPR: " << format(expr)
375 << '\n';
376 std::cout << "GET_VALUE_SET_REC SUFFIX: " << suffix << '\n';
377 std::cout << '\n';
378 #endif
379
380 if(expr.type().id()=="#REF#")
381 {
382 valuest::const_iterator fi = values.find(expr.get(ID_identifier));
383
384 if(fi!=values.end())
385 {
386 for(const auto &object_entry : fi->second.object_map.read())
387 {
389 object_numbering[object_entry.first],
390 dest,
391 suffix,
392 original_type,
393 ns,
394 recursion_set);
395 }
396 return;
397 }
398 else
399 {
400 insert(dest, exprt(ID_unknown, original_type));
401 return;
402 }
403 }
404 else if(expr.id()==ID_unknown || expr.id()==ID_invalid)
405 {
406 insert(dest, exprt(ID_unknown, original_type));
407 return;
408 }
409 else if(expr.id()==ID_index)
410 {
411 const typet &type = to_index_expr(expr).array().type();
412
413 DATA_INVARIANT(type.id()==ID_array ||
414 type.id()=="#REF#",
415 "operand 0 of index expression must be an array");
416
418 to_index_expr(expr).array(),
419 dest,
420 "[]" + suffix,
421 original_type,
422 ns,
423 recursion_set);
424
425 return;
426 }
427 else if(expr.id()==ID_member)
428 {
429 const auto &compound = to_member_expr(expr).compound();
430
431 if(compound.is_not_nil())
432 {
433 const typet &type = ns.follow(compound.type());
434
436 type.id() == ID_struct || type.id() == ID_union,
437 "operand 0 of member expression must be struct or union");
438
439 const std::string &component_name =
440 id2string(to_member_expr(expr).get_component_name());
441
443 compound,
444 dest,
445 "." + component_name + suffix,
446 original_type,
447 ns,
448 recursion_set);
449
450 return;
451 }
452 }
453 else if(expr.id()==ID_symbol)
454 {
455 // just keep a reference to the ident in the set
456 // (if it exists)
457 irep_idt ident = id2string(to_symbol_expr(expr).get_identifier()) + suffix;
458 valuest::const_iterator v_it=values.find(ident);
459
461 {
462 insert(dest, expr, 0);
463 return;
464 }
465 else if(v_it!=values.end())
466 {
467 typet t("#REF#");
468 t.subtype() = expr.type();
469 symbol_exprt sym(ident, t);
470 insert(dest, sym, 0);
471 return;
472 }
473 }
474 else if(expr.id()==ID_if)
475 {
477 to_if_expr(expr).true_case(),
478 dest,
479 suffix,
480 original_type,
481 ns,
482 recursion_set);
484 to_if_expr(expr).false_case(),
485 dest,
486 suffix,
487 original_type,
488 ns,
489 recursion_set);
490
491 return;
492 }
493 else if(expr.id()==ID_address_of)
494 {
495 get_reference_set_sharing(to_address_of_expr(expr).object(), dest, ns);
496
497 return;
498 }
499 else if(expr.id()==ID_dereference)
500 {
501 object_mapt reference_set;
502 get_reference_set_sharing(expr, reference_set, ns);
503 const object_map_dt &object_map=reference_set.read();
504
505 if(object_map.begin()!=object_map.end())
506 {
507 for(const auto &object_entry : object_map)
508 {
509 const exprt &object = object_numbering[object_entry.first];
510 get_value_set_rec(object, dest, suffix,
511 original_type, ns, recursion_set);
512 }
513
514 return;
515 }
516 }
517 else if(expr.is_constant())
518 {
519 // check if NULL
520 if(expr.get(ID_value)==ID_NULL &&
521 expr.type().id()==ID_pointer)
522 {
523 insert(dest, exprt(ID_null_object, expr.type().subtype()), 0);
524 return;
525 }
526 }
527 else if(expr.id()==ID_typecast)
528 {
530 to_typecast_expr(expr).op(),
531 dest,
532 suffix,
533 original_type,
534 ns,
535 recursion_set);
536
537 return;
538 }
539 else if(expr.id()==ID_plus || expr.id()==ID_minus)
540 {
541 if(expr.operands().size()<2)
542 throw expr.id_string()+" expected to have at least two operands";
543
544 if(expr.type().id()==ID_pointer)
545 {
546 // find the pointer operand
547 const exprt *ptr_operand=nullptr;
548
549 forall_operands(it, expr)
550 if(it->type().id()==ID_pointer)
551 {
552 if(ptr_operand==nullptr)
553 ptr_operand=&(*it);
554 else
555 throw "more than one pointer operand in pointer arithmetic";
556 }
557
558 if(ptr_operand==nullptr)
559 throw "pointer type sum expected to have pointer operand";
560
561 object_mapt pointer_expr_set;
562 get_value_set_rec(*ptr_operand, pointer_expr_set, "",
563 ptr_operand->type(), ns, recursion_set);
564
565 for(const auto &object_entry : pointer_expr_set.read())
566 {
567 offsett offset = object_entry.second;
568
569 if(offset_is_zero(offset) && expr.operands().size() == 2)
570 {
571 if(to_binary_expr(expr).op0().type().id() != ID_pointer)
572 {
573 const auto i = numeric_cast<mp_integer>(to_binary_expr(expr).op0());
574 if(!i.has_value())
575 offset.reset();
576 else
577 *offset = (expr.id() == ID_plus) ? *i : -*i;
578 }
579 else
580 {
581 const auto i = numeric_cast<mp_integer>(to_binary_expr(expr).op1());
582 if(!i.has_value())
583 offset.reset();
584 else
585 *offset = (expr.id() == ID_plus) ? *i : -*i;
586 }
587 }
588 else
589 offset.reset();
590
591 insert(dest, object_entry.first, offset);
592 }
593
594 return;
595 }
596 }
597 else if(expr.id()==ID_side_effect)
598 {
599 const irep_idt &statement = to_side_effect_expr(expr).get_statement();
600
601 if(statement==ID_function_call)
602 {
603 // these should be gone
604 throw "unexpected function_call sideeffect";
605 }
606 else if(statement==ID_allocate)
607 {
608 if(expr.type().id()!=ID_pointer)
609 throw "malloc expected to return pointer type";
610
611 PRECONDITION(suffix.empty());
612
613 const typet &dynamic_type=
614 static_cast<const typet &>(expr.find(ID_C_cxx_alloc_type));
615
617 // let's make up a `unique' number for this object...
618 dynamic_object.set_instance(
620 dynamic_object.valid()=true_exprt();
621
622 insert(dest, dynamic_object, 0);
623 return;
624 }
625 else if(statement==ID_cpp_new ||
626 statement==ID_cpp_new_array)
627 {
628 PRECONDITION(suffix.empty());
629 assert(expr.type().id()==ID_pointer);
630
632 dynamic_object.set_instance(
634 dynamic_object.valid()=true_exprt();
635
636 insert(dest, dynamic_object, 0);
637 return;
638 }
639 }
640 else if(expr.id()==ID_struct)
641 {
642 // this is like a static struct object
643 insert(dest, address_of_exprt(expr), 0);
644 return;
645 }
646 else if(expr.id()==ID_with)
647 {
648 // these are supposed to be done by assign()
649 throw "unexpected value in get_value_set: "+expr.id_string();
650 }
651 else if(expr.id()==ID_array_of ||
652 expr.id()==ID_array)
653 {
654 // an array constructor, possibly containing addresses
655 forall_operands(it, expr)
656 get_value_set_rec(*it, dest, suffix, original_type, ns, recursion_set);
657 }
658 else if(expr.id()==ID_dynamic_object)
659 {
662
663 const std::string name=
664 "value_set::dynamic_object"+
665 std::to_string(dynamic_object.get_instance())+
666 suffix;
667
668 // look it up
669 valuest::const_iterator v_it=values.find(name);
670
671 if(v_it!=values.end())
672 {
673 make_union(dest, v_it->second.object_map);
674 return;
675 }
676 }
677
678 insert(dest, exprt(ID_unknown, original_type));
679}
680
682 const exprt &src,
683 exprt &dest) const
684{
685 // remove pointer typecasts
686 if(src.id()==ID_typecast)
687 {
688 assert(src.type().id()==ID_pointer);
689
690 dereference_rec(to_typecast_expr(src).op(), dest);
691 }
692 else
693 dest=src;
694}
695
697 const exprt &expr,
698 expr_sett &dest,
699 const namespacet &ns) const
700{
701 object_mapt object_map;
702 get_reference_set_sharing(expr, object_map, ns);
703
704 for(const auto &object_entry : object_map.read())
705 {
706 const exprt &object = object_numbering[object_entry.first];
707
708 if(object.type().id() == "#REF#")
709 {
710 const irep_idt &ident = object.get(ID_identifier);
711 valuest::const_iterator vit = values.find(ident);
712 if(vit==values.end())
713 {
714 // Assume the variable never was assigned,
715 // so assume it's reference set is unknown.
716 dest.insert(exprt(ID_unknown, object.type()));
717 }
718 else
719 {
720 object_mapt omt;
721 flatten(vit->second, omt);
722
723 for(object_map_dt::iterator t_it=omt.write().begin();
724 t_it!=omt.write().end();
725 t_it++)
726 {
727 if(t_it->second && object_entry.second)
728 {
729 *t_it->second += *object_entry.second;
730 }
731 else
732 t_it->second.reset();
733 }
734
735 for(const auto &o : omt.read())
736 dest.insert(to_expr(o));
737 }
738 }
739 else
740 dest.insert(to_expr(object_entry));
741 }
742}
743
745 const exprt &expr,
746 expr_sett &dest,
747 const namespacet &ns) const
748{
749 object_mapt object_map;
750 get_reference_set_sharing(expr, object_map, ns);
751
752 for(const auto &object_entry : object_map.read())
753 dest.insert(to_expr(object_entry));
754}
755
757 const exprt &expr,
758 object_mapt &dest,
759 const namespacet &ns) const
760{
761 #if 0
762 std::cout << "GET_REFERENCE_SET_REC EXPR: " << format(expr)
763 << '\n';
764 #endif
765
766 if(expr.type().id()=="#REF#")
767 {
768 valuest::const_iterator fi = values.find(expr.get(ID_identifier));
769 if(fi!=values.end())
770 {
771 for(const auto &object_entry : fi->second.object_map.read())
772 {
774 object_numbering[object_entry.first], dest, ns);
775 }
776 return;
777 }
778 }
779 else if(expr.id()==ID_symbol ||
780 expr.id()==ID_dynamic_object ||
781 expr.id()==ID_string_constant)
782 {
783 if(expr.type().id()==ID_array &&
784 expr.type().subtype().id()==ID_array)
785 insert(dest, expr);
786 else
787 insert(dest, expr, 0);
788
789 return;
790 }
791 else if(expr.id()==ID_dereference)
792 {
793 gvs_recursion_sett recset;
794 object_mapt temp;
796 to_dereference_expr(expr).pointer(),
797 temp,
798 "",
799 to_dereference_expr(expr).pointer().type(),
800 ns,
801 recset);
802
803 // REF's need to be dereferenced manually!
804 for(const auto &object_entry : temp.read())
805 {
806 const exprt &obj = object_numbering[object_entry.first];
807 if(obj.type().id()=="#REF#")
808 {
809 const irep_idt &ident = obj.get(ID_identifier);
810 valuest::const_iterator v_it = values.find(ident);
811
812 if(v_it!=values.end())
813 {
814 object_mapt t2;
815 flatten(v_it->second, t2);
816
817 for(object_map_dt::iterator t_it=t2.write().begin();
818 t_it!=t2.write().end();
819 t_it++)
820 {
821 if(t_it->second && object_entry.second)
822 {
823 *t_it->second += *object_entry.second;
824 }
825 else
826 t_it->second.reset();
827 }
828
829 for(const auto &t2_object_entry : t2.read())
830 insert(dest, t2_object_entry);
831 }
832 else
833 insert(dest, exprt(ID_unknown, obj.type().subtype()));
834 }
835 else
836 insert(dest, object_entry);
837 }
838
839 #if 0
840 for(expr_sett::const_iterator it=value_set.begin();
841 it!=value_set.end();
842 it++)
843 std::cout << "VALUE_SET: " << format(*it) << '\n';
844 #endif
845
846 return;
847 }
848 else if(expr.id()==ID_index)
849 {
850 const exprt &array = to_index_expr(expr).array();
851 const exprt &offset = to_index_expr(expr).index();
852 const typet &array_type = array.type();
853
855 array_type.id() == ID_array, "index takes array-typed operand");
856
857 object_mapt array_references;
858 get_reference_set_sharing(array, array_references, ns);
859
860 const object_map_dt &object_map=array_references.read();
861
862 for(const auto &object_entry : object_map)
863 {
864 const exprt &object = object_numbering[object_entry.first];
865
866 if(object.id()==ID_unknown)
867 insert(dest, exprt(ID_unknown, expr.type()));
868 else
869 {
870 index_exprt index_expr(
871 object, from_integer(0, c_index_type()), expr.type());
872
873 exprt casted_index;
874
875 // adjust type?
876 if(object.type().id() != "#REF#" && object.type() != array_type)
877 casted_index = typecast_exprt(index_expr, array.type());
878 else
879 casted_index = index_expr;
880
881 offsett o = object_entry.second;
882 const auto i = numeric_cast<mp_integer>(offset);
883
884 if(offset.is_zero())
885 {
886 }
887 else if(i.has_value() && offset_is_zero(o))
888 *o = *i;
889 else
890 o.reset();
891
892 insert(dest, casted_index, o);
893 }
894 }
895
896 return;
897 }
898 else if(expr.id()==ID_member)
899 {
900 const irep_idt &component_name=expr.get(ID_component_name);
901
902 const exprt &struct_op = to_member_expr(expr).compound();
903
904 object_mapt struct_references;
905 get_reference_set_sharing(struct_op, struct_references, ns);
906
907 for(const auto &object_entry : struct_references.read())
908 {
909 const exprt &object = object_numbering[object_entry.first];
910 const typet &obj_type = object.type();
911
912 if(object.id()==ID_unknown)
913 insert(dest, exprt(ID_unknown, expr.type()));
914 else if(
915 object.id() == ID_dynamic_object && obj_type.id() != ID_struct &&
916 obj_type.id() != ID_union && obj_type.id() != ID_struct_tag &&
917 obj_type.id() != ID_union_tag)
918 {
919 // we catch dynamic objects of the wrong type,
920 // to avoid non-integral typecasts.
921 insert(dest, exprt(ID_unknown, expr.type()));
922 }
923 else
924 {
925 offsett o = object_entry.second;
926
927 member_exprt member_expr(object, component_name, expr.type());
928
929 // adjust type?
930 if(ns.follow(struct_op.type())!=ns.follow(object.type()))
931 {
932 member_expr.compound() =
933 typecast_exprt(member_expr.compound(), struct_op.type());
934 }
935
936 insert(dest, member_expr, o);
937 }
938 }
939
940 return;
941 }
942 else if(expr.id()==ID_if)
943 {
944 get_reference_set_sharing_rec(to_if_expr(expr).true_case(), dest, ns);
945 get_reference_set_sharing_rec(to_if_expr(expr).false_case(), dest, ns);
946 return;
947 }
948
949 insert(dest, exprt(ID_unknown, expr.type()));
950}
951
953 const exprt &lhs,
954 const exprt &rhs,
955 const namespacet &ns)
956{
957 #if 0
958 std::cout << "ASSIGN LHS: " << format(lhs) << '\n';
959 std::cout << "ASSIGN RHS: " << format(rhs) << '\n';
960 #endif
961
962 if(rhs.id()==ID_if)
963 {
964 assign(lhs, to_if_expr(rhs).true_case(), ns);
965 assign(lhs, to_if_expr(rhs).false_case(), ns);
966 return;
967 }
968
969 const typet &type=ns.follow(lhs.type());
970
971 if(type.id()==ID_struct ||
972 type.id()==ID_union)
973 {
974 const struct_union_typet &struct_type=to_struct_union_type(type);
975
976 std::size_t no=0;
977
978 for(struct_typet::componentst::const_iterator
979 c_it=struct_type.components().begin();
980 c_it!=struct_type.components().end();
981 c_it++, no++)
982 {
983 const typet &subtype=c_it->type();
984 const irep_idt &name = c_it->get_name();
985
986 // ignore methods
987 if(subtype.id()==ID_code)
988 continue;
989
990 member_exprt lhs_member(lhs, name, subtype);
991
992 exprt rhs_member;
993
994 if(rhs.id()==ID_unknown ||
995 rhs.id()==ID_invalid)
996 {
997 rhs_member=exprt(rhs.id(), subtype);
998 }
999 else
1000 {
1001 if(rhs.type() != lhs.type())
1002 throw "value_set_fit::assign type mismatch: "
1003 "rhs.type():\n"+rhs.type().pretty()+"\n"+
1004 "type:\n"+lhs.type().pretty();
1005
1006 if(rhs.id()==ID_struct ||
1007 rhs.id()==ID_constant)
1008 {
1009 assert(no<rhs.operands().size());
1010 rhs_member=rhs.operands()[no];
1011 }
1012 else if(rhs.id()==ID_with)
1013 {
1014 // see if this is the member we want
1015 const auto &rhs_with = to_with_expr(rhs);
1016 const exprt &member_operand = rhs_with.where();
1017
1018 const irep_idt &component_name=
1019 member_operand.get(ID_component_name);
1020
1021 if(component_name==name)
1022 {
1023 // yes! just take op2
1024 rhs_member = rhs_with.new_value();
1025 }
1026 else
1027 {
1028 // no! do op0
1029 rhs_member=exprt(ID_member, subtype);
1030 rhs_member.copy_to_operands(rhs_with.old());
1031 rhs_member.set(ID_component_name, name);
1032 }
1033 }
1034 else
1035 {
1036 rhs_member=exprt(ID_member, subtype);
1037 rhs_member.copy_to_operands(rhs);
1038 rhs_member.set(ID_component_name, name);
1039 }
1040
1041 assign(lhs_member, rhs_member, ns);
1042 }
1043 }
1044 }
1045 else if(type.id()==ID_array)
1046 {
1047 const index_exprt lhs_index(
1048 lhs, exprt(ID_unknown, c_index_type()), type.subtype());
1049
1050 if(rhs.id()==ID_unknown ||
1051 rhs.id()==ID_invalid)
1052 {
1053 assign(lhs_index, exprt(rhs.id(), type.subtype()), ns);
1054 }
1055 else if(rhs.is_nil())
1056 {
1057 // do nothing
1058 }
1059 else
1060 {
1061 if(rhs.type() != type)
1062 throw "value_set_fit::assign type mismatch: "
1063 "rhs.type():\n"+rhs.type().pretty()+"\n"+
1064 "type:\n"+type.pretty();
1065
1066 if(rhs.id()==ID_array_of)
1067 {
1068 assign(lhs_index, to_array_of_expr(rhs).what(), ns);
1069 }
1070 else if(rhs.id()==ID_array ||
1071 rhs.id()==ID_constant)
1072 {
1073 forall_operands(o_it, rhs)
1074 {
1075 assign(lhs_index, *o_it, ns);
1076 }
1077 }
1078 else if(rhs.id()==ID_with)
1079 {
1080 const index_exprt op0_index(
1081 to_with_expr(rhs).old(),
1082 exprt(ID_unknown, c_index_type()),
1083 type.subtype());
1084
1085 assign(lhs_index, op0_index, ns);
1086 assign(lhs_index, to_with_expr(rhs).new_value(), ns);
1087 }
1088 else
1089 {
1090 const index_exprt rhs_index(
1091 rhs, exprt(ID_unknown, c_index_type()), type.subtype());
1092 assign(lhs_index, rhs_index, ns);
1093 }
1094 }
1095 }
1096 else
1097 {
1098 // basic type
1099 object_mapt values_rhs;
1100
1101 get_value_set(rhs, values_rhs, ns);
1102
1103 assign_recursion_sett recset;
1104 assign_rec(lhs, values_rhs, "", ns, recset);
1105 }
1106}
1107
1109 const exprt &lhs,
1110 const object_mapt &values_rhs,
1111 const std::string &suffix,
1112 const namespacet &ns,
1113 assign_recursion_sett &recursion_set)
1114{
1115 #if 0
1116 std::cout << "ASSIGN_REC LHS: " << format(lhs) << '\n';
1117 std::cout << "ASSIGN_REC SUFFIX: " << suffix << '\n';
1118
1119 for(object_map_dt::const_iterator it=values_rhs.read().begin();
1120 it!=values_rhs.read().end(); it++)
1121 std::cout << "ASSIGN_REC RHS: " << to_expr(it) << '\n';
1122 #endif
1123
1124 if(lhs.type().id()=="#REF#")
1125 {
1126 const irep_idt &ident = lhs.get(ID_identifier);
1127 object_mapt temp;
1128 gvs_recursion_sett recset;
1129 get_value_set_rec(lhs, temp, "", lhs.type().subtype(), ns, recset);
1130
1131 if(recursion_set.find(ident)!=recursion_set.end())
1132 {
1133 recursion_set.insert(ident);
1134
1135 for(const auto &object_entry : temp.read())
1136 {
1137 const exprt &object = object_numbering[object_entry.first];
1138
1139 if(object.id() != ID_unknown)
1140 assign_rec(object, values_rhs, suffix, ns, recursion_set);
1141 }
1142
1143 recursion_set.erase(ident);
1144 }
1145 }
1146 else if(lhs.id()==ID_symbol)
1147 {
1148 const irep_idt &identifier = to_symbol_expr(lhs).get_identifier();
1149
1150 if(has_prefix(id2string(identifier),
1151 "value_set::dynamic_object") ||
1152 has_prefix(id2string(identifier),
1153 "value_set::return_value") ||
1154 values.find(id2string(identifier)+suffix)!=values.end())
1155 // otherwise we don't track this value
1156 {
1157 entryt &entry = get_entry(identifier, suffix);
1158
1159 if(make_union(entry.object_map, values_rhs))
1160 changed = true;
1161 }
1162 }
1163 else if(lhs.id()==ID_dynamic_object)
1164 {
1167
1168 const std::string name=
1169 "value_set::dynamic_object"+
1170 std::to_string(dynamic_object.get_instance());
1171
1172 if(make_union(get_entry(name, suffix).object_map, values_rhs))
1173 changed = true;
1174 }
1175 else if(lhs.id()==ID_dereference)
1176 {
1177 if(lhs.operands().size()!=1)
1178 throw lhs.id_string()+" expected to have one operand";
1179
1180 object_mapt reference_set;
1181 get_reference_set_sharing(lhs, reference_set, ns);
1182
1183 for(const auto &object_entry : reference_set.read())
1184 {
1185 const exprt &object = object_numbering[object_entry.first];
1186
1187 if(object.id()!=ID_unknown)
1188 assign_rec(object, values_rhs, suffix, ns, recursion_set);
1189 }
1190 }
1191 else if(lhs.id()==ID_index)
1192 {
1193 const typet &type = to_index_expr(lhs).array().type();
1194
1195 DATA_INVARIANT(type.id()==ID_array ||
1196 type.id()=="#REF#",
1197 "operand 0 of index expression must be an array");
1198
1199 assign_rec(
1200 to_index_expr(lhs).array(), values_rhs, "[]" + suffix, ns, recursion_set);
1201 }
1202 else if(lhs.id()==ID_member)
1203 {
1204 if(to_member_expr(lhs).compound().is_nil())
1205 return;
1206
1207 const std::string &component_name=lhs.get_string(ID_component_name);
1208
1209 const typet &type = ns.follow(to_member_expr(lhs).compound().type());
1210
1212 type.id() == ID_struct || type.id() == ID_union,
1213 "operand 0 of member expression must be struct or union");
1214
1215 assign_rec(
1216 to_member_expr(lhs).compound(),
1217 values_rhs,
1218 "." + component_name + suffix,
1219 ns,
1220 recursion_set);
1221 }
1222 else if(lhs.id()=="valid_object" ||
1223 lhs.id()=="dynamic_type")
1224 {
1225 // we ignore this here
1226 }
1227 else if(lhs.id()==ID_string_constant)
1228 {
1229 // someone writes into a string-constant
1230 // evil guy
1231 }
1232 else if(lhs.id() == ID_null_object)
1233 {
1234 // evil as well
1235 }
1236 else if(lhs.id()==ID_typecast)
1237 {
1238 const typecast_exprt &typecast_expr=to_typecast_expr(lhs);
1239
1240 assign_rec(typecast_expr.op(), values_rhs, suffix, ns, recursion_set);
1241 }
1242 else if(lhs.id()=="zero_string" ||
1243 lhs.id()=="is_zero_string" ||
1244 lhs.id()=="zero_string_length")
1245 {
1246 // ignore
1247 }
1248 else if(lhs.id()==ID_byte_extract_little_endian ||
1249 lhs.id()==ID_byte_extract_big_endian)
1250 {
1251 assign_rec(
1252 to_byte_extract_expr(lhs).op(), values_rhs, suffix, ns, recursion_set);
1253 }
1254 else
1255 throw "assign NYI: '" + lhs.id_string() + "'";
1256}
1257
1259 const irep_idt &function,
1260 const exprt::operandst &arguments,
1261 const namespacet &ns)
1262{
1263 const symbolt &symbol=ns.lookup(function);
1264
1265 const code_typet &type=to_code_type(symbol.type);
1266 const code_typet::parameterst &parameter_types=type.parameters();
1267
1268 // these first need to be assigned to dummy, temporary arguments
1269 // and only thereafter to the actuals, in order
1270 // to avoid overwriting actuals that are needed for recursive
1271 // calls
1272
1273 for(std::size_t i=0; i<arguments.size(); i++)
1274 {
1275 const std::string identifier="value_set::" + id2string(function) + "::" +
1276 "argument$"+std::to_string(i);
1277 add_var(identifier);
1278 const symbol_exprt dummy_lhs(identifier, arguments[i].type());
1279 assign(dummy_lhs, arguments[i], ns);
1280 }
1281
1282 // now assign to 'actual actuals'
1283
1284 std::size_t i=0;
1285
1286 for(code_typet::parameterst::const_iterator
1287 it=parameter_types.begin();
1288 it!=parameter_types.end();
1289 it++)
1290 {
1291 const irep_idt &identifier=it->get_identifier();
1292 if(identifier.empty())
1293 continue;
1294
1295 add_var(identifier);
1296
1297 const exprt v_expr=
1298 symbol_exprt("value_set::" + id2string(function) + "::" +
1299 "argument$"+std::to_string(i), it->type());
1300
1301 const symbol_exprt actual_lhs(identifier, it->type());
1302 assign(actual_lhs, v_expr, ns);
1303 i++;
1304 }
1305}
1306
1308 const exprt &lhs,
1309 const namespacet &ns)
1310{
1311 if(lhs.is_nil())
1312 return;
1313
1314 std::string rvs = "value_set::return_value" + std::to_string(from_function);
1315 symbol_exprt rhs(rvs, lhs.type());
1316
1317 assign(lhs, rhs, ns);
1318}
1319
1320void value_set_fit::apply_code(const codet &code, const namespacet &ns)
1321{
1322 const irep_idt &statement=code.get(ID_statement);
1323
1324 if(statement==ID_block)
1325 {
1326 for(const auto &stmt : to_code_block(code).statements())
1327 apply_code(stmt, ns);
1328 }
1329 else if(statement==ID_function_call)
1330 {
1331 // shouldn't be here
1333 }
1334 else if(statement==ID_assign)
1335 {
1336 if(code.operands().size()!=2)
1337 throw "assignment expected to have two operands";
1338
1339 assign(code.op0(), code.op1(), ns);
1340 }
1341 else if(statement==ID_decl)
1342 {
1343 if(code.operands().size()!=1)
1344 throw "decl expected to have one operand";
1345
1346 const exprt &lhs=code.op0();
1347
1348 if(lhs.id()!=ID_symbol)
1349 throw "decl expected to have symbol on lhs";
1350
1351 assign(lhs, exprt(ID_invalid, lhs.type()), ns);
1352 }
1353 else if(statement==ID_expression)
1354 {
1355 // can be ignored, we don't expect side effects here
1356 }
1357 else if(statement==ID_cpp_delete ||
1358 statement==ID_cpp_delete_array)
1359 {
1360 // does nothing
1361 }
1362 else if(statement=="lock" || statement=="unlock")
1363 {
1364 // ignore for now
1365 }
1366 else if(statement==ID_asm)
1367 {
1368 // ignore for now, probably not safe
1369 }
1370 else if(statement==ID_nondet)
1371 {
1372 // doesn't do anything
1373 }
1374 else if(statement==ID_printf)
1375 {
1376 // doesn't do anything
1377 }
1378 else if(statement==ID_return)
1379 {
1380 const code_returnt &code_return = to_code_return(code);
1381 // this is turned into an assignment
1382 std::string rvs = "value_set::return_value" + std::to_string(from_function);
1383 symbol_exprt lhs(rvs, code_return.return_value().type());
1384 assign(lhs, code_return.return_value(), ns);
1385 }
1386 else if(statement==ID_fence)
1387 {
1388 }
1389 else if(statement==ID_array_copy ||
1390 statement==ID_array_replace ||
1391 statement==ID_array_set)
1392 {
1393 }
1395 {
1396 // doesn't do anything
1397 }
1398 else
1399 throw
1400 code.pretty()+"\n"+
1401 "value_set_fit: unexpected statement: "+id2string(statement);
1402}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
bitvector_typet c_index_type()
Definition c_types.cpp:16
Operator to return the address of an object.
exprt & op0()
Definition expr.h:99
code_operandst & statements()
Definition std_code.h:138
codet representation of a "return from a function" statement.
const exprt & return_value() const
Base type of functions.
Definition std_types.h:539
std::vector< parametert > parameterst
Definition std_types.h:542
const parameterst & parameters() const
Definition std_types.h:655
Data structure for representing an arbitrary statement in a program.
exprt & op0()
Definition expr.h:99
exprt & op1()
Definition expr.h:102
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
bool empty() const
Definition dstring.h:88
void clear()
Definition dstring.h:142
Representation of heap-allocated objects.
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition expr.h:129
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition expr.cpp:64
bool is_constant() const
Return whether the expression is a constant.
Definition expr.cpp:26
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
Array index operator.
Definition std_expr.h:1328
exprt & index()
Definition std_expr.h:1363
exprt & array()
Definition std_expr.h:1353
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:495
const irept & find(const irep_idt &name) const
Definition irep.cpp:106
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:45
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
const std::string & id_string() const
Definition irep.h:399
const irep_idt & id() const
Definition irep.h:396
bool is_nil() const
Definition irep.h:376
const std::string & get_string(const irep_idt &name) const
Definition irep.h:409
Extract member of struct or union.
Definition std_expr.h:2667
const exprt & compound() const
Definition std_expr.h:2708
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
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().
Split an expression into a base object and a (byte) offset.
const T & read() const
const irep_idt & get_statement() const
Definition std_code.h:1472
Base type for structs and unions.
Definition std_types.h:62
const componentst & components() const
Definition std_types.h:147
Expression to hold a symbol (variable)
Definition std_expr.h:80
const irep_idt & get_identifier() const
Definition std_expr.h:109
Symbol table entry.
Definition symbol.h:28
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
const irep_idt & display_name() const
Return language specific display name if present.
Definition symbol.h:55
The Boolean constant true.
Definition std_expr.h:2856
Semantic type conversion.
Definition std_expr.h:1920
The type of an expression, extends irept.
Definition type.h:29
const typet & subtype() const
Definition type.h:48
const exprt & op() const
Definition std_expr.h:293
data_typet::value_type value_type
data_typet::const_iterator const_iterator
static const object_map_dt blank
data_typet::iterator iterator
void get_reference_set_sharing(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value,...
static object_numberingt object_numbering
std::unordered_set< idt, string_hash > gvs_recursion_sett
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns)
static numberingt< irep_idt > function_numbering
void add_var(const idt &id)
bool make_union(object_mapt &dest, const object_mapt &src) const
std::vector< exprt > get_value_set(const exprt &expr, const namespacet &ns) const
unsigned from_function
void apply_code(const codet &code, const namespacet &ns)
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, assign_recursion_sett &recursion_set)
void get_value_set_rec(const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns, gvs_recursion_sett &recursion_set) const
void dereference_rec(const exprt &src, exprt &dest) const
std::unordered_map< idt, entryt, string_hash > valuest
std::unordered_set< idt, string_hash > assign_recursion_sett
void output(const namespacet &ns, std::ostream &out) const
void flatten_rec(const entryt &, object_mapt &, flatten_seent &) const
std::unordered_set< exprt, irep_hash > expr_sett
void do_end_function(const exprt &lhs, const namespacet &ns)
void flatten(const entryt &e, object_mapt &dest) const
bool offset_is_zero(const offsett &offset) const
entryt & get_entry(const idt &id, const std::string &suffix)
unsigned from_target_index
bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
std::unordered_set< idt, string_hash > flatten_seent
exprt to_expr(const object_map_dt::value_type &it) const
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
void get_reference_set_sharing_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#define forall_operands(it, expr)
Definition expr.h:18
static format_containert< T > format(const T &o)
Definition format.h:37
bool can_cast_expr< code_inputt >(const exprt &base)
bool can_cast_expr< code_outputt >(const exprt &base)
const code_returnt & to_code_return(const codet &code)
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)
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
const std::string integer2string(const mp_integer &n, unsigned base)
Definition mp_arith.cpp:103
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
exprt dynamic_object(const exprt &pointer)
bool simplify(exprt &expr, const namespacet &ns)
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
#define PRECONDITION(CONDITION)
Definition invariant.h:463
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition std_code.h:1506
const code_blockt & to_code_block(const codet &code)
Definition std_code.h:203
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition std_expr.h:1456
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1391
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:1954
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:627
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2751
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2374
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition std_types.h:214
Symbol table entry.
static const char * alloc_adapter_prefix
Value Set (Flow Insensitive, Sharing)