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