CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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/namespace.h>
18#include <util/pointer_expr.h>
19#include <util/simplify_expr.h>
20#include <util/std_code.h>
21#include <util/symbol.h>
22
24
26
27#include <ostream>
28
30
33
34static const char *alloc_adapter_prefix="alloc_adaptor::";
35
37 const namespacet &ns,
38 std::ostream &out) const
39{
40 for(valuest::const_iterator
41 v_it=values.begin();
42 v_it!=values.end();
43 v_it++)
44 {
45 irep_idt identifier, display_name;
46
47 const entryt &e=v_it->second;
48
49 if(e.identifier.starts_with("value_set::dynamic_object"))
50 {
51 display_name=id2string(e.identifier)+e.suffix;
52 identifier.clear();
53 }
54 else
55 {
56 #if 0
57 const symbolt &symbol=ns.lookup(id2string(e.identifier));
58 display_name=symbol.display_name()+e.suffix;
59 identifier=symbol.name;
60 #else
61 identifier=id2string(e.identifier);
62 display_name=id2string(identifier)+e.suffix;
63 #endif
64 }
65
66 out << display_name;
67
68 out << " = { ";
69
70 object_mapt object_map;
71 flatten(e, object_map);
72
73 std::size_t width=0;
74
75 const auto &entries = object_map.read();
76 for(object_map_dt::const_iterator o_it = entries.begin();
77 o_it != entries.end();
78 ++o_it)
79 {
80 const exprt &o=object_numbering[o_it->first];
81
82 std::string result;
83
84 if(o.id()==ID_invalid || o.id()==ID_unknown)
85 {
86 result="<";
87 result+=from_expr(ns, identifier, o);
88 result+=", *, "; // offset unknown
89 if(o.type().id()==ID_unknown)
90 result+='*';
91 else
92 result+=from_type(ns, identifier, o.type());
93 result+='>';
94 }
95 else
96 {
97 result="<"+from_expr(ns, identifier, o)+", ";
98
99 if(o_it->second)
100 result += integer2string(*o_it->second);
101 else
102 result+='*';
103
104 result+=", ";
105
106 if(o.type().id()==ID_unknown)
107 result+='*';
108 else
109 result+=from_type(ns, identifier, o.type());
110
111 result+='>';
112 }
113
114 out << result;
115
116 width+=result.size();
117
119 next++;
120
121 if(next != entries.end())
122 {
123 out << ", ";
124 if(width>=40)
125 out << "\n ";
126 }
127 }
128
129 out << " } \n";
130 }
131}
132
134 const entryt &e,
135 object_mapt &dest) const
136{
137 #if 0
138 std::cout << "FLATTEN: " << e.identifier << e.suffix << '\n';
139 #endif
140
141 flatten_seent seen;
142 flatten_rec(e, dest, seen);
143
144 #if 0
145 std::cout << "FLATTEN: Done.\n";
146 #endif
147}
148
150 const entryt &e,
151 object_mapt &dest,
152 flatten_seent &seen) const
153{
154 #if 0
155 std::cout << "FLATTEN_REC: " << e.identifier << e.suffix << '\n';
156 #endif
157
158 std::string identifier = id2string(e.identifier);
159 CHECK_RETURN(seen.find(identifier + e.suffix) == seen.end());
160
161 bool generalize_index = false;
162
163 seen.insert(identifier + e.suffix);
164
165 for(const auto &object_entry : e.object_map.read())
166 {
167 const exprt &o = object_numbering[object_entry.first];
168
169 if(o.type().id()=="#REF#")
170 {
171 if(seen.find(o.get(ID_identifier))!=seen.end())
172 {
173 generalize_index = true;
174 continue;
175 }
176
177 valuest::const_iterator fi = values.find(o.get(ID_identifier));
178 if(fi==values.end())
179 {
180 // this is some static object, keep it in.
181 const symbol_exprt se(
182 o.get(ID_identifier), to_type_with_subtype(o.type()).subtype());
183 insert(dest, se, mp_integer{0});
184 }
185 else
186 {
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(
255 it->second.identifier.starts_with("value_set::dynamic_object") ||
256 it->second.identifier.starts_with("value_set::return_value"))
257 {
258 values.insert(*it);
259 result=true;
260 }
261
262 continue;
263 }
264
265 entryt &e=it2->second;
266 const entryt &new_e=it->second;
267
268 if(make_union(e.object_map, new_e.object_map))
269 result=true;
270 }
271
272 changed = result;
273
274 return result;
275}
276
278{
279 bool result=false;
280
281 for(const auto &object_entry : src.read())
282 {
283 if(insert(dest, object_entry))
284 result=true;
285 }
286
287 return result;
288}
289
290std::vector<exprt>
291value_set_fit::get_value_set(const exprt &expr, const namespacet &ns) const
292{
293 object_mapt object_map;
294 get_value_set(expr, object_map, ns);
295
297
298 for(const auto &object_entry : object_map.read())
299 {
300 const exprt &object = object_numbering[object_entry.first];
301 if(object.type().id()=="#REF#")
302 {
303 DATA_INVARIANT(object.id() == ID_symbol, "reference to symbol required");
304
305 const irep_idt &ident = object.get(ID_identifier);
306 valuest::const_iterator v_it = values.find(ident);
307
308 if(v_it!=values.end())
309 {
311 flatten(v_it->second, temp);
312
313 for(object_map_dt::iterator t_it=temp.write().begin();
314 t_it!=temp.write().end();
315 t_it++)
316 {
317 if(t_it->second && object_entry.second)
318 {
319 *t_it->second += *object_entry.second;
320 }
321 else
322 t_it->second.reset();
323
324 flat_map.write()[t_it->first]=t_it->second;
325 }
326 }
327 }
328 else
329 flat_map.write()[object_entry.first] = object_entry.second;
330 }
331
332 std::vector<exprt> result;
333 for(const auto &object_entry : flat_map.read())
334 result.push_back(to_expr(object_entry));
335
336#if 0
337 // Sanity check!
338 for(std::list<exprt>::const_iterator it=value_set.begin();
339 it!=value_set.end();
340 it++)
341 assert(it->type().id()!="#REF");
342#endif
343
344#if 0
345 for(expr_sett::const_iterator it=value_set.begin(); it!=value_set.end(); it++)
346 std::cout << "GET_VALUE_SET: " << format(*it) << '\n';
347#endif
348
349 return result;
350}
351
353 const exprt &expr,
354 object_mapt &dest,
355 const namespacet &ns) const
356{
357 exprt tmp(expr);
358 simplify(tmp, ns);
359
361 bool includes_nondet_pointer = false;
363 tmp, dest, includes_nondet_pointer, "", tmp.type(), ns, recset);
364}
365
367 const exprt &expr,
368 object_mapt &dest,
370 const std::string &suffix,
371 const typet &original_type,
372 const namespacet &ns,
373 gvs_recursion_sett &recursion_set) const
374{
375 #if 0
376 std::cout << "GET_VALUE_SET_REC EXPR: " << format(expr)
377 << '\n';
378 std::cout << "GET_VALUE_SET_REC SUFFIX: " << suffix << '\n';
379 std::cout << '\n';
380 #endif
381
382 if(expr.type().id()=="#REF#")
383 {
384 valuest::const_iterator fi = values.find(expr.get(ID_identifier));
385
386 if(fi!=values.end())
387 {
388 for(const auto &object_entry : fi->second.object_map.read())
389 {
392 dest,
394 suffix,
396 ns,
397 recursion_set);
398 }
399 return;
400 }
401 else
402 {
404 return;
405 }
406 }
407 else if(expr.id()==ID_unknown || expr.id()==ID_invalid)
408 {
410 return;
411 }
412 else if(expr.id()==ID_index)
413 {
414 const typet &type = to_index_expr(expr).array().type();
415
416 if(type.id() == ID_array)
417 {
419 to_index_expr(expr).array(),
420 dest,
422 "[]" + suffix,
424 ns,
425 recursion_set);
426 }
427 else
429
430 return;
431 }
432 else if(expr.id()==ID_member)
433 {
434 const auto &compound = to_member_expr(expr).compound();
435
436 if(compound.is_not_nil())
437 {
439 compound.type().id() == ID_struct ||
440 compound.type().id() == ID_struct_tag ||
441 compound.type().id() == ID_union ||
442 compound.type().id() == ID_union_tag,
443 "operand 0 of member expression must be struct or union");
444
445 const std::string &component_name =
446 id2string(to_member_expr(expr).get_component_name());
447
449 compound,
450 dest,
452 "." + component_name + suffix,
454 ns,
455 recursion_set);
456
457 return;
458 }
459 }
460 else if(expr.id()==ID_symbol)
461 {
462 // just keep a reference to the ident in the set
463 // (if it exists)
464 irep_idt ident = id2string(to_symbol_expr(expr).get_identifier()) + suffix;
465 valuest::const_iterator v_it=values.find(ident);
466
467 if(ident.starts_with(alloc_adapter_prefix))
468 {
469 insert(dest, expr, mp_integer{0});
470 return;
471 }
472 else if(v_it!=values.end())
473 {
474 type_with_subtypet t("#REF#", expr.type());
476 insert(dest, sym, mp_integer{0});
477 return;
478 }
479 }
480 else if(expr.id()==ID_if)
481 {
483 to_if_expr(expr).true_case(),
484 dest,
486 suffix,
488 ns,
489 recursion_set);
491 to_if_expr(expr).false_case(),
492 dest,
494 suffix,
496 ns,
497 recursion_set);
498
499 return;
500 }
501 else if(expr.id()==ID_address_of)
502 {
503 get_reference_set_sharing(to_address_of_expr(expr).object(), dest, ns);
504
505 return;
506 }
507 else if(expr.id()==ID_dereference)
508 {
511 const object_map_dt &object_map=reference_set.read();
512
513 if(object_map.begin()!=object_map.end())
514 {
515 for(const auto &object_entry : object_map)
516 {
517 const exprt &object = object_numbering[object_entry.first];
519 object,
520 dest,
522 suffix,
524 ns,
525 recursion_set);
526 }
527
528 return;
529 }
530 }
531 else if(expr.is_constant())
532 {
533 // check if NULL
535 {
536 insert(
537 dest,
538 exprt(ID_null_object, to_pointer_type(expr.type()).base_type()),
539 mp_integer{0});
540 return;
541 }
542 }
543 else if(expr.id()==ID_typecast)
544 {
546 to_typecast_expr(expr).op(),
547 dest,
549 suffix,
551 ns,
552 recursion_set);
553
554 return;
555 }
556 else if(expr.id()==ID_plus || expr.id()==ID_minus)
557 {
558 if(expr.operands().size()<2)
559 throw expr.id_string()+" expected to have at least two operands";
560
561 if(expr.type().id()==ID_pointer)
562 {
563 // find the pointer operand
564 const exprt *ptr_operand=nullptr;
565
566 for(const auto &op : expr.operands())
567 {
568 if(op.type().id() == ID_pointer)
569 {
570 if(ptr_operand==nullptr)
571 ptr_operand = &op;
572 else
573 throw "more than one pointer operand in pointer arithmetic";
574 }
575 }
576
577 if(ptr_operand==nullptr)
578 throw "pointer type sum expected to have pointer operand";
579
585 "",
586 ptr_operand->type(),
587 ns,
588 recursion_set);
589
590 for(const auto &object_entry : pointer_expr_set.read())
591 {
592 offsett offset = object_entry.second;
593
594 if(offset_is_zero(offset) && expr.operands().size() == 2)
595 {
596 if(to_binary_expr(expr).op0().type().id() != ID_pointer)
597 {
598 const auto i = numeric_cast<mp_integer>(to_binary_expr(expr).op0());
599 if(!i.has_value())
600 offset.reset();
601 else
602 *offset = (expr.id() == ID_plus) ? *i : -*i;
603 }
604 else
605 {
606 const auto i = numeric_cast<mp_integer>(to_binary_expr(expr).op1());
607 if(!i.has_value())
608 offset.reset();
609 else
610 *offset = (expr.id() == ID_plus) ? *i : -*i;
611 }
612 }
613 else
614 offset.reset();
615
616 insert(dest, object_entry.first, offset);
617 }
618
619 return;
620 }
621 }
622 else if(expr.id()==ID_side_effect)
623 {
624 const irep_idt &statement = to_side_effect_expr(expr).get_statement();
625
626 if(statement==ID_function_call)
627 {
628 // these should be gone
629 throw "unexpected function_call sideeffect";
630 }
631 else if(statement==ID_allocate)
632 {
633 if(expr.type().id()!=ID_pointer)
634 throw "malloc expected to return pointer type";
635
636 PRECONDITION(suffix.empty());
637
638 const typet &dynamic_type=
639 static_cast<const typet &>(expr.find(ID_C_cxx_alloc_type));
640
642 // let's make up a `unique' number for this object...
643 dynamic_object.set_instance(
645 dynamic_object.valid()=true_exprt();
646
648 return;
649 }
650 else if(statement==ID_cpp_new ||
651 statement==ID_cpp_new_array)
652 {
653 PRECONDITION(suffix.empty());
654 PRECONDITION(expr.type().id() == ID_pointer);
655
657 to_pointer_type(expr.type()).base_type());
658 dynamic_object.set_instance(
660 dynamic_object.valid()=true_exprt();
661
663 return;
664 }
665 }
666 else if(expr.id()==ID_struct)
667 {
668 // this is like a static struct object
669 insert(dest, address_of_exprt(expr), mp_integer{0});
670 return;
671 }
672 else if(expr.id()==ID_with)
673 {
674 // these are supposed to be done by assign()
675 throw "unexpected value in get_value_set: "+expr.id_string();
676 }
677 else if(expr.id()==ID_array_of ||
678 expr.id()==ID_array)
679 {
680 // an array constructor, possibly containing addresses
681 for(const auto &op : expr.operands())
682 {
684 op,
685 dest,
687 suffix,
689 ns,
690 recursion_set);
691 }
692 }
693 else if(expr.id()==ID_dynamic_object)
694 {
697
698 const std::string name=
699 "value_set::dynamic_object"+
700 std::to_string(dynamic_object.get_instance())+
701 suffix;
702
703 // look it up
704 valuest::const_iterator v_it=values.find(name);
705
706 if(v_it!=values.end())
707 {
708 make_union(dest, v_it->second.object_map);
709 return;
710 }
711 }
712
714}
715
717 const exprt &src,
718 exprt &dest) const
719{
720 // remove pointer typecasts
721 if(src.id()==ID_typecast)
722 {
723 PRECONDITION(src.type().id() == ID_pointer);
724
725 dereference_rec(to_typecast_expr(src).op(), dest);
726 }
727 else
728 dest=src;
729}
730
732 const exprt &expr,
733 expr_sett &dest,
734 const namespacet &ns) const
735{
736 object_mapt object_map;
737 get_reference_set_sharing(expr, object_map, ns);
738
739 for(const auto &object_entry : object_map.read())
740 {
741 const exprt &object = object_numbering[object_entry.first];
742
743 if(object.type().id() == "#REF#")
744 {
745 const irep_idt &ident = object.get(ID_identifier);
746 valuest::const_iterator vit = values.find(ident);
747 if(vit==values.end())
748 {
749 // Assume the variable never was assigned,
750 // so assume it's reference set is unknown.
751 dest.insert(exprt(ID_unknown, object.type()));
752 }
753 else
754 {
756 flatten(vit->second, omt);
757
758 for(object_map_dt::iterator t_it=omt.write().begin();
759 t_it!=omt.write().end();
760 t_it++)
761 {
762 if(t_it->second && object_entry.second)
763 {
764 *t_it->second += *object_entry.second;
765 }
766 else
767 t_it->second.reset();
768 }
769
770 for(const auto &o : omt.read())
771 dest.insert(to_expr(o));
772 }
773 }
774 else
775 dest.insert(to_expr(object_entry));
776 }
777}
778
780 const exprt &expr,
781 expr_sett &dest,
782 const namespacet &ns) const
783{
784 object_mapt object_map;
785 get_reference_set_sharing(expr, object_map, ns);
786
787 for(const auto &object_entry : object_map.read())
788 dest.insert(to_expr(object_entry));
789}
790
792 const exprt &expr,
793 object_mapt &dest,
794 const namespacet &ns) const
795{
796 #if 0
797 std::cout << "GET_REFERENCE_SET_REC EXPR: " << format(expr)
798 << '\n';
799 #endif
800
801 if(expr.type().id()=="#REF#")
802 {
803 valuest::const_iterator fi = values.find(expr.get(ID_identifier));
804 if(fi!=values.end())
805 {
806 for(const auto &object_entry : fi->second.object_map.read())
807 {
809 object_numbering[object_entry.first], dest, ns);
810 }
811 return;
812 }
813 }
814 else if(expr.id()==ID_symbol ||
815 expr.id()==ID_dynamic_object ||
816 expr.id()==ID_string_constant)
817 {
818 if(
819 expr.type().id() == ID_array &&
820 to_array_type(expr.type()).element_type().id() == ID_array)
821 {
822 insert(dest, expr);
823 }
824 else
825 insert(dest, expr, mp_integer{0});
826
827 return;
828 }
829 else if(expr.id()==ID_dereference)
830 {
833 bool includes_nondet_pointer = false;
835 to_dereference_expr(expr).pointer(),
836 temp,
838 "",
839 to_dereference_expr(expr).pointer().type(),
840 ns,
841 recset);
842
843 // REF's need to be dereferenced manually!
844 for(const auto &object_entry : temp.read())
845 {
846 const exprt &obj = object_numbering[object_entry.first];
847 if(obj.type().id()=="#REF#")
848 {
849 const irep_idt &ident = obj.get(ID_identifier);
850 valuest::const_iterator v_it = values.find(ident);
851
852 if(v_it!=values.end())
853 {
855 flatten(v_it->second, t2);
856
857 for(object_map_dt::iterator t_it=t2.write().begin();
858 t_it!=t2.write().end();
859 t_it++)
860 {
861 if(t_it->second && object_entry.second)
862 {
863 *t_it->second += *object_entry.second;
864 }
865 else
866 t_it->second.reset();
867 }
868
869 for(const auto &t2_object_entry : t2.read())
870 insert(dest, t2_object_entry);
871 }
872 else
873 insert(
874 dest,
875 exprt(ID_unknown, to_type_with_subtype(obj.type()).subtype()));
876 }
877 else
878 insert(dest, object_entry);
879 }
880
881 #if 0
882 for(expr_sett::const_iterator it=value_set.begin();
883 it!=value_set.end();
884 it++)
885 std::cout << "VALUE_SET: " << format(*it) << '\n';
886 #endif
887
888 return;
889 }
890 else if(expr.id()==ID_index)
891 {
892 const exprt &array = to_index_expr(expr).array();
893 const exprt &offset = to_index_expr(expr).index();
894 const typet &array_type = array.type();
895
897 array_type.id() == ID_array, "index takes array-typed operand");
898
901
902 const object_map_dt &object_map=array_references.read();
903
904 for(const auto &object_entry : object_map)
905 {
906 const exprt &object = object_numbering[object_entry.first];
907
908 if(object.id()==ID_unknown)
909 insert(dest, exprt(ID_unknown, expr.type()));
910 else
911 {
913 object, from_integer(0, c_index_type()), expr.type());
914
916
917 // adjust type?
918 if(object.type().id() != "#REF#" && object.type() != array_type)
920 else
922
923 offsett o = object_entry.second;
924 const auto i = numeric_cast<mp_integer>(offset);
925
926 if(offset.is_zero())
927 {
928 }
929 else if(i.has_value() && offset_is_zero(o))
930 *o = *i;
931 else
932 o.reset();
933
934 insert(dest, casted_index, o);
935 }
936 }
937
938 return;
939 }
940 else if(expr.id()==ID_member)
941 {
942 const irep_idt &component_name=expr.get(ID_component_name);
943
944 const exprt &struct_op = to_member_expr(expr).compound();
945
948
949 for(const auto &object_entry : struct_references.read())
950 {
951 const exprt &object = object_numbering[object_entry.first];
952 const typet &obj_type = object.type();
953
954 if(object.id()==ID_unknown)
955 insert(dest, exprt(ID_unknown, expr.type()));
956 else if(
957 obj_type.id() != ID_struct && obj_type.id() != ID_union &&
958 obj_type.id() != ID_struct_tag && obj_type.id() != ID_union_tag)
959 {
960 // we catch objects of the wrong type,
961 // to avoid non-integral typecasts.
962 insert(dest, exprt(ID_unknown, expr.type()));
963 }
964 else
965 {
966 offsett o = object_entry.second;
967
968 member_exprt member_expr(object, component_name, expr.type());
969
970 // adjust type?
971 if(struct_op.type() != object.type())
972 {
973 member_expr.compound() =
974 typecast_exprt(member_expr.compound(), struct_op.type());
975 }
976
977 insert(dest, member_expr, o);
978 }
979 }
980
981 return;
982 }
983 else if(expr.id()==ID_if)
984 {
985 get_reference_set_sharing_rec(to_if_expr(expr).true_case(), dest, ns);
986 get_reference_set_sharing_rec(to_if_expr(expr).false_case(), dest, ns);
987 return;
988 }
989
990 insert(dest, exprt(ID_unknown, expr.type()));
991}
992
994 const exprt &lhs,
995 const exprt &rhs,
996 const namespacet &ns)
997{
998 #if 0
999 std::cout << "ASSIGN LHS: " << format(lhs) << '\n';
1000 std::cout << "ASSIGN RHS: " << format(rhs) << '\n';
1001 #endif
1002
1003 if(rhs.id()==ID_if)
1004 {
1005 assign(lhs, to_if_expr(rhs).true_case(), ns);
1006 assign(lhs, to_if_expr(rhs).false_case(), ns);
1007 return;
1008 }
1009
1010 if(
1011 lhs.type().id() == ID_struct || lhs.type().id() == ID_struct_tag ||
1012 lhs.type().id() == ID_union || lhs.type().id() == ID_union_tag)
1013 {
1014 const auto &components =
1015 (lhs.type().id() == ID_struct_tag || lhs.type().id() == ID_union_tag)
1016 ? ns.follow_tag(to_struct_or_union_tag_type(lhs.type())).components()
1017 : to_struct_union_type(lhs.type()).components();
1018
1019 std::size_t no=0;
1020
1021 for(struct_typet::componentst::const_iterator c_it = components.begin();
1022 c_it != components.end();
1023 c_it++, no++)
1024 {
1025 const typet &subtype=c_it->type();
1026 const irep_idt &name = c_it->get_name();
1027
1028 // ignore padding
1030 subtype.id() != ID_code,
1031 "struct/union member must not be of code type");
1032 if(c_it->get_is_padding())
1033 continue;
1034
1035 member_exprt lhs_member(lhs, name, subtype);
1036
1038
1039 if(rhs.id()==ID_unknown ||
1040 rhs.id()==ID_invalid)
1041 {
1042 rhs_member=exprt(rhs.id(), subtype);
1043 }
1044 else
1045 {
1046 if(rhs.type() != lhs.type())
1047 throw "value_set_fit::assign type mismatch: "
1048 "rhs.type():\n"+rhs.type().pretty()+"\n"+
1049 "type:\n"+lhs.type().pretty();
1050
1051 if(rhs.id() == ID_struct || rhs.is_constant())
1052 {
1054 no < rhs.operands().size(), "component index must be in bounds");
1055 rhs_member=rhs.operands()[no];
1056 }
1057 else if(rhs.id()==ID_with)
1058 {
1059 // see if this is the member we want
1060 const auto &rhs_with = to_with_expr(rhs);
1061 const exprt &member_operand = rhs_with.where();
1062
1063 const irep_idt &component_name=
1065
1066 if(component_name==name)
1067 {
1068 // yes! just take op2
1069 rhs_member = rhs_with.new_value();
1070 }
1071 else
1072 {
1073 // no! do op0
1074 rhs_member=exprt(ID_member, subtype);
1075 rhs_member.copy_to_operands(rhs_with.old());
1076 rhs_member.set(ID_component_name, name);
1077 }
1078 }
1079 else
1080 {
1081 rhs_member=exprt(ID_member, subtype);
1082 rhs_member.copy_to_operands(rhs);
1083 rhs_member.set(ID_component_name, name);
1084 }
1085
1087 }
1088 }
1089 }
1090 else if(lhs.type().id() == ID_array)
1091 {
1092 const index_exprt lhs_index(
1093 lhs,
1095 to_array_type(lhs.type()).element_type());
1096
1097 if(rhs.id()==ID_unknown ||
1098 rhs.id()==ID_invalid)
1099 {
1100 assign(
1101 lhs_index,
1102 exprt(rhs.id(), to_array_type(lhs.type()).element_type()),
1103 ns);
1104 }
1105 else if(rhs.is_nil())
1106 {
1107 // do nothing
1108 }
1109 else
1110 {
1111 if(rhs.type() != lhs.type())
1112 throw "value_set_fit::assign type mismatch: "
1113 "rhs.type():\n"+rhs.type().pretty()+"\n"+
1114 "type:\n"+lhs.type().pretty();
1115
1116 if(rhs.id()==ID_array_of)
1117 {
1118 assign(lhs_index, to_array_of_expr(rhs).what(), ns);
1119 }
1120 else if(rhs.id() == ID_array || rhs.is_constant())
1121 {
1122 for(const auto &op : rhs.operands())
1123 {
1124 assign(lhs_index, op, ns);
1125 }
1126 }
1127 else if(rhs.id()==ID_with)
1128 {
1129 const index_exprt op0_index(
1130 to_with_expr(rhs).old(),
1132 to_array_type(lhs.type()).element_type());
1133
1135 assign(lhs_index, to_with_expr(rhs).new_value(), ns);
1136 }
1137 else
1138 {
1139 const index_exprt rhs_index(
1140 rhs,
1142 to_array_type(lhs.type()).element_type());
1144 }
1145 }
1146 }
1147 else
1148 {
1149 // basic type
1151
1152 get_value_set(rhs, values_rhs, ns);
1153
1155 assign_rec(lhs, values_rhs, "", ns, recset);
1156 }
1157}
1158
1160 const exprt &lhs,
1161 const object_mapt &values_rhs,
1162 const std::string &suffix,
1163 const namespacet &ns,
1164 assign_recursion_sett &recursion_set)
1165{
1166 #if 0
1167 std::cout << "ASSIGN_REC LHS: " << format(lhs) << '\n';
1168 std::cout << "ASSIGN_REC SUFFIX: " << suffix << '\n';
1169
1170 for(object_map_dt::const_iterator it=values_rhs.read().begin();
1171 it!=values_rhs.read().end(); it++)
1172 std::cout << "ASSIGN_REC RHS: " << to_expr(it) << '\n';
1173 #endif
1174
1175 if(lhs.type().id()=="#REF#")
1176 {
1177 const irep_idt &ident = lhs.get(ID_identifier);
1180 bool includes_nondet_pointer = false;
1182 lhs,
1183 temp,
1185 "",
1186 to_type_with_subtype(lhs.type()).subtype(),
1187 ns,
1188 recset);
1189
1190 if(recursion_set.find(ident)!=recursion_set.end())
1191 {
1192 recursion_set.insert(ident);
1193
1194 for(const auto &object_entry : temp.read())
1195 {
1196 const exprt &object = object_numbering[object_entry.first];
1197
1198 if(object.id() != ID_unknown)
1199 assign_rec(object, values_rhs, suffix, ns, recursion_set);
1200 }
1201
1202 recursion_set.erase(ident);
1203 }
1204 }
1205 else if(lhs.id()==ID_symbol)
1206 {
1207 const irep_idt &identifier = to_symbol_expr(lhs).get_identifier();
1208
1209 if(
1210 identifier.starts_with("value_set::dynamic_object") ||
1211 identifier.starts_with("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 const exprt &compound = to_member_expr(lhs).compound();
1270
1272 compound.type().id() == ID_struct ||
1273 compound.type().id() == ID_struct_tag ||
1274 compound.type().id() == ID_union ||
1275 compound.type().id() == ID_union_tag,
1276 "operand 0 of member expression must be struct or union");
1277
1278 assign_rec(
1279 compound, values_rhs, "." + component_name + suffix, ns, recursion_set);
1280 }
1281 else if(lhs.id()=="valid_object" ||
1282 lhs.id()=="dynamic_type")
1283 {
1284 // we ignore this here
1285 }
1286 else if(lhs.id()==ID_string_constant)
1287 {
1288 // someone writes into a string-constant
1289 // evil guy
1290 }
1291 else if(lhs.id() == ID_null_object)
1292 {
1293 // evil as well
1294 }
1295 else if(lhs.id()==ID_typecast)
1296 {
1298
1299 assign_rec(typecast_expr.op(), values_rhs, suffix, ns, recursion_set);
1300 }
1301 else if(
1302 lhs.id() == "zero_string" || lhs.id() == "is_zero_string" ||
1303 lhs.id() == "zero_string_length" || lhs.id() == ID_address_of)
1304 {
1305 // ignore
1306 }
1307 else if(lhs.id()==ID_byte_extract_little_endian ||
1309 {
1310 assign_rec(
1311 to_byte_extract_expr(lhs).op(), values_rhs, suffix, ns, recursion_set);
1312 }
1313 else
1314 throw "assign NYI: '" + lhs.id_string() + "'";
1315}
1316
1318 const irep_idt &function,
1319 const exprt::operandst &arguments,
1320 const namespacet &ns)
1321{
1322 const symbolt &symbol=ns.lookup(function);
1323
1324 const code_typet &type=to_code_type(symbol.type);
1326
1327 // these first need to be assigned to dummy, temporary arguments
1328 // and only thereafter to the actuals, in order
1329 // to avoid overwriting actuals that are needed for recursive
1330 // calls
1331
1332 for(std::size_t i=0; i<arguments.size(); i++)
1333 {
1334 const std::string identifier="value_set::" + id2string(function) + "::" +
1335 "argument$"+std::to_string(i);
1336 add_var(identifier);
1337 const symbol_exprt dummy_lhs(identifier, arguments[i].type());
1338 assign(dummy_lhs, arguments[i], ns);
1339 }
1340
1341 // now assign to 'actual actuals'
1342
1343 std::size_t i=0;
1344
1345 for(code_typet::parameterst::const_iterator
1346 it=parameter_types.begin();
1347 it!=parameter_types.end();
1348 it++)
1349 {
1350 const irep_idt &identifier=it->get_identifier();
1351 if(identifier.empty())
1352 continue;
1353
1354 add_var(identifier);
1355
1356 const exprt v_expr=
1357 symbol_exprt("value_set::" + id2string(function) + "::" +
1358 "argument$"+std::to_string(i), it->type());
1359
1360 const symbol_exprt actual_lhs(identifier, it->type());
1361 assign(actual_lhs, v_expr, ns);
1362 i++;
1363 }
1364}
1365
1367 const exprt &lhs,
1368 const namespacet &ns)
1369{
1370 if(lhs.is_nil())
1371 return;
1372
1373 std::string rvs = "value_set::return_value" + std::to_string(from_function);
1374 symbol_exprt rhs(rvs, lhs.type());
1375
1376 assign(lhs, rhs, ns);
1377}
1378
1379void value_set_fit::apply_code(const codet &code, const namespacet &ns)
1380{
1381 const irep_idt &statement=code.get(ID_statement);
1382
1383 if(statement==ID_block)
1384 {
1385 for(const auto &stmt : to_code_block(code).statements())
1386 apply_code(stmt, ns);
1387 }
1388 else if(statement==ID_function_call)
1389 {
1390 // shouldn't be here
1392 }
1393 else if(statement==ID_assign)
1394 {
1395 if(code.operands().size()!=2)
1396 throw "assignment expected to have two operands";
1397
1398 assign(code.op0(), code.op1(), ns);
1399 }
1400 else if(statement==ID_decl)
1401 {
1402 if(code.operands().size()!=1)
1403 throw "decl expected to have one operand";
1404
1405 const exprt &lhs=code.op0();
1406
1407 if(lhs.id()!=ID_symbol)
1408 throw "decl expected to have symbol on lhs";
1409
1410 assign(lhs, exprt(ID_invalid, lhs.type()), ns);
1411 }
1412 else if(statement==ID_expression)
1413 {
1414 // can be ignored, we don't expect side effects here
1415 }
1416 else if(statement==ID_cpp_delete ||
1417 statement==ID_cpp_delete_array)
1418 {
1419 // does nothing
1420 }
1421 else if(statement=="lock" || statement=="unlock")
1422 {
1423 // ignore for now
1424 }
1425 else if(statement==ID_asm)
1426 {
1427 // ignore for now, probably not safe
1428 }
1429 else if(statement==ID_nondet)
1430 {
1431 // doesn't do anything
1432 }
1433 else if(statement==ID_printf)
1434 {
1435 // doesn't do anything
1436 }
1437 else if(statement==ID_return)
1438 {
1440 // this is turned into an assignment
1441 std::string rvs = "value_set::return_value" + std::to_string(from_function);
1442 symbol_exprt lhs(rvs, code_return.return_value().type());
1443 assign(lhs, code_return.return_value(), ns);
1444 }
1445 else if(statement==ID_fence)
1446 {
1447 }
1448 else if(
1449 statement == ID_array_copy || statement == ID_array_replace ||
1450 statement == ID_array_set || statement == ID_array_equal)
1451 {
1452 }
1454 {
1455 // doesn't do anything
1456 }
1457 else if(statement == ID_havoc_object)
1458 {
1459 }
1460 else
1461 throw
1462 code.pretty()+"\n"+
1463 "value_set_fit: unexpected statement: "+id2string(statement);
1464}
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:562
goto_instruction_codet representation of a "return from a function" statement.
Base type of functions.
Definition std_types.h:583
std::vector< parametert > parameterst
Definition std_types.h:586
const parameterst & parameters() const
Definition std_types.h:699
Data structure for representing an arbitrary statement in a program.
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Definition dstring.h:95
bool empty() const
Definition dstring.h:89
void clear()
Definition dstring.h:159
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:212
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:1470
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
const irept & find(const irep_idt &name) const
Definition irep.cpp:93
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
const std::string & id_string() const
Definition irep.h:391
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
const std::string & get_string(const irep_idt &name) const
Definition irep.h:401
Extract member of struct or union.
Definition std_expr.h:2971
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
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
Expression to hold a symbol (variable)
Definition std_expr.h:131
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:3190
Type with a single subtype.
Definition type.h:180
Semantic type conversion.
Definition std_expr.h:2073
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
std::optional< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value,...
void get_reference_set_sharing(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
static object_numberingt object_numbering
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)
std::unordered_set< idt > assign_recursion_sett
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
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)
std::set< idt > flatten_seent
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 > gvs_recursion_sett
std::map< idt, entryt > valuest
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 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...
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:44
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:1603
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2577
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3063
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3172
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2660
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
const struct_or_union_tag_typet & to_struct_or_union_tag_type(const typet &type)
Cast a typet to a struct_or_union_tag_typet.
Definition std_types.h:478
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
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:208
static const char * alloc_adapter_prefix
Value Set (Flow Insensitive, Sharing)